spec: Inline PC memory access into CPU (#501)

* spec: Inline PC memory access into CPU

* Apply suggestions from code review

Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com>
Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

* Apply review suggestion

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

* Remove `pc_double_read` constraints and clarify why in cpu.typ

* Potential optimization -> subsubsection

* Address review comments

* Clarifying remark on register initialization

---------

Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com>
Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

Author: 3 people

spec/cpu.typ

@@ -56,16 +56,26 @@ The ALU functionality is then obtained through judicious dispatching to the corr
 
 #render_constraint_table(chip, config, groups: "alu")
 
-== Memory
+== Memory<cpu:memory>
 
 The interactions with the memory, both for register loading and storing, as for `LOAD` and `STORE` instructions are handled.
 Note that since registers need no byte-addressing, we store them in the memory argument with `Word` limbs.
-The timestamps are ensured to be disjoint for disjoint memory locations.
+The `pc` register behaves very predictably with respect to its timestamps and when it is being read,
+so for performance reasons, we inline its memory interactions directly into the #cpu chip.
+
+Potentially overlapping memory accesses are ensured to have disjoint timestamps.
 One consequence of that is that `next_pc` is written at `timestamp + 1`
-to ensure the access is disjoint with the `pc` read into `rv1` as part of the `AUIPC` instruction.
+to ensure the access is disjoint with the `pc` read into `rv1` as part of the `AUIPC` instruction (see @cpu:c:read_rv1 and @decode:decoding-overview).
+Constraints regarding whether `pc_double_read` corresponds to an `AUIPC` instruction are not necessary,
+as regardless of its value, the old timestamp is guaranteed smaller than the new timestamp,
+and the integrity of the memory argument therefore ensures the correctness of this bit.
 
 #render_constraint_table(chip, config, groups: "mem")
 
+=== Potential optimizations
+
+- `double_pc_read` could be integrated into decoding, so that `AUIPC` could set `read_register1 = 0` and no extra MEMW access for `rv1` is needed at this point.
+
 == System
 
 The interactions with the wider system.

spec/decode.typ

@@ -39,7 +39,7 @@ Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this
 Note moreover that the `pc` is set to $7$.
 This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link(<cpu-padding-decode-row>)[additional instruction] referred to by `CPU`-padding lines).
 
-= Decoding
+= Decoding<decode:decoding-overview>
 For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables.
 Note that the below table is _not_ used in practice: it is solely used for the purposes of this explanation.
 
@@ -64,12 +64,6 @@ For the purpose of brevity and readability, the table uses the following rules-o
 
 Further clarification is provided in the notes following the table.
 
-== C-type instructions
-The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size.
-This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$.
-To indicate an instruction is provided in compressed form, the `c_type` flag is introduced.
-*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.*
-
 /// Add a reference to one or more notes following this table.
 #let ref_note(..refs) = {
   super("[" + refs.pos().map(r => ref(r)).join(",") + "]")
@@ -152,6 +146,12 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
 
 #decoding_table(decoding)
 
+== C-type instructions
+The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size.
+This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$.
+To indicate an instruction is provided in compressed form, the `c_type` flag is introduced.
+*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.*
+
 // Construct a note that can be referenced through `lbl`
 #let referenceable_note(lbl, note) = {
   show figure: (it) => align(left, [#it])

spec/memory.typ

@@ -136,6 +136,8 @@ The initialization will need to correspond to a fixed initial register state for
 as well as the memory loaded from the program binary, zero-initialization of memory elsewhere, and private input provided by the prover.
 The contribution of initialization with static data from the ELF executable and the initial register state to the sum
 can be handled directly by the verifier, ensuring correctness corresponding to the ELF binary being proven.
+To enable the loading of the PC in @cpu:memory, register initialization happens at timestamp 1.
+Register finalization is made possible for the verifier by having a known state from the HALT chip (@halt).
 This leaves only zero-initialization and prover input as prover-side concerns for initialization,
 alongside the finalization of the entire used memory.
 

spec/src/cpu.toml

@@ -221,6 +221,18 @@ desc = "The value to (maybe) be written back to rvd"
 pad = 0
 
 # Auxiliary
+[[variables.auxiliary]]
+name = "prev_pc_timestamp_borrow"
+type = "Bit"
+desc = "The borrow bit for computing the previous timestamp the PC was accessed"
+pad = 0
+
+[[variables.auxiliary]]
+name = "pc_double_read"
+type = "Bit"
+desc = "Whether the PC is being read as a general purpose register (`rs1`) this cycle"
+pad = 0
+
 [[variables.auxiliary]]
 name = "rv1"
 type = "DWordWHH"
@@ -652,6 +664,7 @@ tag = "MEMW"
 input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
 output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register1"
+ref = "cpu:c:read_rv1"
 
 [[constraints.mem]]
 kind = "arith"
@@ -691,12 +704,29 @@ tag = "MEMW"
 input = [0, ["cast", "res", "DWordWL"], ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
 multiplicity = "STORE"
 
+[[constraints.mem]]
+kind = "template"
+tag = "IS_BIT"
+input = ["pc_double_read"]
+
+[[constraints.mem]]
+kind = "template"
+tag = "IS_BIT"
+input = ["prev_pc_timestamp_borrow"]
+
 [[constraints.mem]]
 kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 255], "DWordWL"], ["arr", ["idx", "next_pc", 0], ["idx", "next_pc", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
-output = ["arr", ["idx", "pc", 0], ["idx", "pc", 1], 0, 0, 0, 0, 0, 0]
+tag = "memory"
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["-", ["idx", "timestamp", 0], ["*", 3, ["not", "pc_double_read"]]], ["*", ["^", 2, 32], "prev_pc_timestamp_borrow"]], ["-", ["idx", "timestamp", 1], "prev_pc_timestamp_borrow"]], ["idx", "pc", "i"]]
 multiplicity = ["not", "pad"]
+iter = ["i", 0, 1]
+
+[[constraints.mem]]
+kind = "interaction"
+tag = "memory"
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], ["idx", "next_pc", "i"]]
+multiplicity = ["-", ["not", "pad"]]
+iter = ["i", 0, 1]
 
 
 [[constraint_groups]]