docs(yellowpaper): rewrite section on tagged memory, misc rewording/cleanup

yellow-paper/docs/public-vm/alu.md

@@ -6,7 +6,7 @@ This component of the VM circuit evaluates both base-2 arithmetic operations and
 
 The following block diagram maps out an draft of the internal components of the "ALU"
 
-![](./gen/images/alu/alu.png)
+![](./images/alu.png)
 
 Notes:
 

yellow-paper/docs/public-vm/control-flow.md

@@ -14,7 +14,7 @@ The intention is for sub-operations to be implementable as independent VM circui
 
 # Control flow
 
-![](./gen/images/control-flow/avm-control-flow.png)
+![](./images/avm-control-flow.png)
 
 > Notation note: whenever the VM "sends a signal" to one or more VM components, this is analogous to defining a boolean column in the execution trace that toggles on/off specific functionality
 

yellow-paper/docs/public-vm/security.md

@@ -0,0 +1,4 @@
+# VM threat model, security requirements
+
+An honest Prover must always be able to construct a satisfiable proof for an AVM program, even if the program throws an error.
+This implies constraints produced by the AVM **must** be satisfiable.

yellow-paper/docs/public-vm/state-model.md

@@ -1,12 +1,12 @@
-# The Aztec VM State Model
+# State Model
 
 The goal of this note is to describe the VM state model and to specify "internal" VM abstractions that can be mapped to circuit designs.
 
-# A memory-only state model
+## A memory-only state model
 
 The AVM possesses three distinct data regions, accessed via distinct VM instructions: memory, calldata and returndata
 
-![](./gen/images/state-model/memory.png)
+![](./images/memory.png)
 
 All data regions are linear blocks of memory where each memory cell stores a finite field element.
 
@@ -45,61 +45,130 @@ Indirect memory addressing is required in order to support read/writes into dyna
 
 Memory addresses must be tagged to be a `u32` type.
 
-# Tagged memory
+## Types and Tagged Memory
 
-We define a `tag` to refer to the potential maximum value of a cell of main memory. The following tags are supported:
+### Terminology/legend
+- `M[X]`: main memory cell at offset `X`
+- `tag`: a value referring to a memory cell's type (its maximum potential value)
+- `T[X]`: the tag associated with memory cell at offset `X`
+- `in-tag`: an instruction's tag to check input operands against. Present for many but not all instructions.
+- `dst-tag`: the target type of a `CAST` instruction, also used to tag the destination memory cell
+- `ADD<X>`: shorthand for an `ADD` instruction with `in-tag = X`
+- `ADD<X> aOffset bOffset dstOffset`: an full `ADD` instruction with `in-tag = X`. See [here](./InstructionSet#isa-section-add) for more details.
+- `CAST<X>`: a `CAST` instruction with `dst-tag`: `X`. `CAST` is the only instruction with a `dst-tag`. See [here](./InstructionSet#isa-section-cast) for more details.
 
-| tag value | maximum memory cell value |
-| --------- | ------------------------- |
-| 0         | 0                         |
-| 1         | $2^8 - 1$                 |
-| 2         | $2^{16} - 1$              |
-| 3         | $2^{32} - 1$              |
-| 4         | $2^{64} - 1$              |
-| 5         | $2^{128} - 1$             |
-| 6         | $p - 1$                   |
+### Tags and tagged memory
 
-Note: $p$ describes the modulus of the finite field that the AVM circuit is defined over (i.e. number of points on the BN254 curve).
+A `tag` refers to the maximum potential value of a cell of main memory. The following tags are supported:
 
-The purpose of a tag is to inform the VM of the maximum possible length of an operand value that has been loaded from memory.
+| tag value | maximum memory cell value | shorthand     |
+| --------- | ------------------------- | ------------- |
+| 0         | 0                         | uninitialized |
+| 1         | $2^8 - 1$                 | `u8`          |
+| 2         | $2^{16} - 1$              | `u16`         |
+| 3         | $2^{32} - 1$              | `u32`         |
+| 4         | $2^{64} - 1$              | `u64`         |
+| 5         | $2^{128} - 1$             | `u128`        |
+| 6         | $p - 1$                   | `field`       |
+| 7         | reserved                  | reserved      |
 
-Multiple AVM instructions explicitly operate over range-constrained input parameters (e.g. ADD32). The maximum allowable value for an instruction's input parameters is defined via an _instruction tag_. Two potential scenarios result:
+> Note: $p$ describes the modulus of the finite field that the AVM circuit is defined over (i.e. number of points on the BN254 curve).
+> Note: `u32` is used for offsets into the VM's 32-bit addressable main memory
 
-1. A VM instruction's tag value matches the input parameter tag values
-2. A VM instruction's tag value does not match the input parameter tag values
+The purpose of a tag is to inform the VM of the maximum possible length of an operand value that has been loaded from memory.
 
-If case 2 is triggered, an error flag is raised.
+#### Checking input operand tags
 
----
+Many AVM instructions explicitly operate over range-constrained input parameters (e.g. `ADD<in-tag>`). The maximum allowable value for an instruction's input parameters is defined via an `in-tag` (instruction/input tag). Two potential scenarios result:
 
-### Writing into memory
+1. A VM instruction's tag value matches the input parameter tag values
+2. A VM instruction's tag value does _not_ match the input parameter tag values
 
-It is required that all VM instructions that write into main memory explicitly define the tag of the output value and ensure the value is appropriately constrained to be consistent with the assigned tag.
+If case 2 is triggered, an error flag is raised and the current call's execution reverts.
 
----
+#### Writing into memory
 
-### MOV and tag conversions
+It is required that all VM instructions that write into main memory explicitly define the tag of the destination value and ensure the value is appropriately constrained to be consistent with the assigned tag. You can see an instruction's "**Tag updates**" in its section of the instruction set document (see [here for `ADD`](./InstructionSet#isa-section-add) and [here for `CAST`](./InstructionSet#isa-section-cast)).
 
-The MOV instruction copies data from between memory cell, perserving tags.
+#### Standard tagging example: `ADD`
 
-The only VM instruction that can be used to cast between tags is CAST. There are 2 modes to MOV:
+```
+# ADD<u32> aOffset bOffset dstOffset
+assert T[aOffset] == T[bOffset] == u32 // check inputs against in-tag, revert on mismatch
+T[dstOffset] = u32                     // tag destination with in-tag
+M[dstOffset] = M[aOffset] + M[bOffset] // perform the addition
+```
 
-1. The destination tag describes a maximum value that is _less than_ the source tag
-2. The destination tag describes a maximum value that is _greater than or equal to_ the source tag
+#### `MOV` and tag preservation
 
-For Case 1, range constraints must be applied to ensure the destination value is consistent with the source value after tag truncations have been applied.
-
-Case 2 is trivial as no additional consistency checks must be performed between soruce and destination values.
+The `MOV` instruction copies data from one memory cell to another, preserving tags. In other words, the destination cell's tag will adopt the value of the source:
+```
+# MOV srcOffset dstOffset
+T[dstOffset] = T[srcOffset] // preserve tag
+M[dstOffset] = M[srcOffset] // perform the move
+```
 
----
+Note that `MOV` does not have an `in-tag` and therefore does not need to make any assertions regarding the source memory cell's type.
 
-### Calldata/returndata and tag conversions
+#### `CAST` and tag conversions
 
-All elements in calldata/returndata are implicitly tagged as field elements (i.e. maximum value is $p - 1$). To perform a tag conversion, calldata/returndata must be copied into main memory, followed by an appropriate MOV instruction.
+The only VM instruction that can be used to cast between tags is `CAST`. Two potential scenarios result:
 
-## VM threat model, security requirements
+1. The destination tag describes a maximum value that is _less than_ the source tag
+2. The destination tag describes a maximum value that is _greater than or equal to_ the source tag
 
-TODO: move this somewhere else, doesn't quite fit.
+For Case 1, range constraints must be applied to ensure the destination value is consistent with the source value after tag truncations have been applied.
 
-An honest Prover must always be able to construct a satsisfiable proof for an AVM program, even if the program throws an error.
-This implies constraints produced by the AVM **must** be satisfiable.
+Case 2 is trivial as no additional consistency checks must be performed between source and destination values.
+
+```
+# CAST<u64> srcOffset dstOffset
+T[dstOffset] = u64                         // tag destination with dst-tag
+M[dstOffset] = cast<to: u64>(M[srcOffset]) // perform cast
+```
+
+#### Indirect `MOV` and extra tag checks
+
+A `MOV` instruction may flag its source and/or destination offsets as "indirect". An indirect memory access performs `M[M[offset]]` instead of the standard `M[offset]`. Memory offsets must be `u32`s since main memory is a 32-bit addressable space, and so indirect memory accesses include additional checks.
+
+Additional checks for a `MOV` with an indirect source offset:
+```
+# MOV srcOffset dstOffset      // with indirect source
+assert T[srcOffset] == u32     // enforce that `M[srcOffset]` is itself a valid memory offset
+T[dstOffset] = T[T[srcOffset]] // tag destination to match indirect source tag
+M[dstOffset] = M[M[srcOffset]] // perform move from indirect source
+```
+
+Additional checks for a `MOV` with an indirect destination offset:
+```
+# MOV srcOffset dstOffset      // with indirect destination
+assert T[dstOffset] == u32     // enforce that `M[dstOffset]` is itself a valid memory offset
+T[T[dstOffset]] = T[srcOffset] // tag indirect destination to match source tag
+M[M[dstOffset]] = M[srcOffset] // perform move to indirect destination
+```
+
+Additional checks for a `MOV` with both indirect source and destination offsets:
+```
+# MOV srcOffset dstOffset                  // with indirect source and destination
+assert T[srcOffset] == T[dstOffset] == u32 // enforce that `M[*Offset]` are valid memory offsets
+T[T[dstOffset]] = T[T[srcOffset]]          // tag indirect destination to match indirect source tag
+M[M[dstOffset]] = M[M[srcOffset]]          // perform move to indirect destination
+```
+
+#### Calldata/returndata and tag conversions
+
+All elements in calldata/returndata are implicitly tagged as field elements (i.e. maximum value is $p - 1$). To perform a tag conversion, calldata/returndata must be copied into main memory (via [`CALLDATACOPY`](./InstructionSet#isa-section-calldatacopy) or [`RETURN`'s `offset` and `size`](./InstructionSet#isa-section-return)), followed by an appropriate `CAST` instruction.
+```
+# Copy calldata to memory and cast a word to u64
+CALLDATACOPY cdOffset size offsetA // copy calldata to memory at offsetA
+CAST<u64> offsetA dstOffset        // cast first copied word to a u64
+```
+This would perform the following:
+```
+# CALLDATACOPY cdOffset size offsetA
+T[offsetA:offsetA+size] = field                            // CALLDATACOPY assigns the field tag
+M[offsetA:offsetA+size] = calldata[cdOffset:cdOffset+size] // copy calldata to memory
+# CAST<u64> offsetA dstOffset
+T[offsetA] = u64                                           // CAST assigns a new tag
+M[dstOffset] = cast<u64>(offsetA)                          // perform the cast operation
+```