spec: Move to the epoch system

spec/book.typ

@@ -12,6 +12,7 @@
     ("PROOF SYSTEM", (
         ("logup.typ", [`LogUp` argument], <logup>),
         ("memory.typ", [Memory argument], <memory>),
+        ("streaming.typ", [Streaming prover], <streaming>),
     )),
     ("OVERVIEW", (
         ("variables.typ", [Variables], <vars>),
@@ -71,6 +72,18 @@
 #let common-formatting(body) = {
   set footnote(numbering: "[1]")
   show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt)
+  show figure.where(kind: "aside"): it => {
+    set figure.caption(position: top)
+    show figure.caption: cap => block(
+      inset: (left: 1em, right: 1em, top: .75em, bottom: .75em),
+      outset: (left: 1em),
+      width: 100% + 1em,
+      fill: rgb("55aaff"),
+      stroke: luma(50%),
+      align(center, strong(text(fill: black, cap)))
+    )
+    block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it))
+  }
   show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label")
   body
 }
@@ -84,15 +97,14 @@
 #let et = todo.with(background: rgb("d4aa3a"), name: "Erik")
 #let cdsg = todo.with(background: olive, name: "Cyprien")
 
-#let aside(title, body) = context figure(
-  block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false)[
-    #block(inset: (left: 1em, right: 1em, top: .75em, bottom: .75em),
-           width: 100% + 2em,
-           fill: rgb("55aaff"),
-           stroke: luma(50%),
-           align(center, strong(text(fill: black, title))))
-    #align(left, body)
-])
+#let aside(title, body, ref: none) = [
+  #figure(
+    caption: title,
+    supplement: [Aside],
+    kind: "aside",
+    body
+  )#ref
+]
 
 
 #let is-shiroa = "x-target" in sys.inputs

spec/commit.typ

@@ -65,6 +65,21 @@ However, since it is practically impossible to commit more than $2^64-2^32$ byte
 
 Next, we read the `value` located at buffer address `address` and commit to it under the given `index`.
 This is only performed when we have not yet reached the `end` of the commit sequence.
+Values are committed by letting the verifier initialize and finalize the global memory argument (see @memory and @streaming),
+with the claimed commitments in its own domain separated part of memory, with domain separator value 2.#footnote[
+  In order to make sure the verifier can properly finalize the committed values, the last epoch can "bring forward"
+  all commitments from earlier epochs, similar to padded values, in the `L2G` table.
+  Then the contribution of the commitments only consists of the tuples `(2, address, last_epoch_index, value)`, which is entirely known to the verifier.
+]
+This chip then checks that the same value as the one being committed is then found at the corresponding address.
+In doing this, we enforce that all values being committed match the claimed commitment,
+and the verifier can additionally check that register 254 contains the correct value to ensure
+the correct amount of bytes have been committed.#footnote[
+  We additionally note here that for very large commitments (with index $>= 2^32$),
+  the address can potentially become denormalized, but since no other chips or systems interact with
+  this memory domain, there is no issue.
+  The usual consistency guarantee from the LogUp argument and correct initialization as for general addresses applies.
+]
 #render_constraint_table(chip, config, groups: "commit")
 
 In parallel, we compute $#`address_incr` = #`address` + 1$ (@commit:c:address_incr) as address of the next byte to commit, and $#`count_decr` = #`count` - 1$ (@commit:c:count_decr) as the number of bytes that still has to be committed after committing this byte.

spec/halt.typ

@@ -33,7 +33,7 @@ The #halt chip:
 + makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code),
 + writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and
 + sets `pc` equal to $1$ (@halt:c:consume_pc, @halt:c:emit_pc).
-Note that the writes performed by all these interactions --- except for the `pc` --- are accompanied by the timestamp $2^64-1$; the maximum timestamp.
+Note that the writes performed by all these interactions --- except for the `pc` --- are accompanied by the timestamp $2^32-1$; the maximum timestamp.
 This prevents any other operation involving memory from being executed hereafter.
 The `pc` is consumed and re-emitted at the same timestamp to enable padding rows for the CPU.
 This means that the verifier will have to know the final timestamp at which a CPU padding `pc` was written

spec/memory.typ

@@ -24,6 +24,12 @@ and are therefore handled simultaneously.
 #footnote[
   While RAM is byte addressed, we do choose to store registers as a `DWordWL` over two word addresses.
 ]
+In particular, our memory addressing scheme will consist of two parts: a domain separator, and an address within the domain.
+For specific domains and domain separators, we use the following assignment.
+
+/ RAM memory: $0$
+/ Registers: $1$
+/ Committed values: $2$
 
 On a high level, we ensure memory consistency by an interacting system of
 reads and writes to a lookup argument, combined with an initialization and finalization scheme.
@@ -64,7 +70,7 @@ The $i$th possible memory access in cycle $c$ will obtain as timestamp the value
 For simplicity, we will always reserve a timestamp for every possible memory access, and leave the timestamp unused if an instruction does not use it.
 
 
-#aside[Note on "simultaneous" memory accesses][
+#aside(ref: <memory:aside:granularity>)[Note on "simultaneous" memory accesses][
   For reasons of completeness (since temporal integrity as discussed below is a security necessity),
   we cannot deal with multiple accesses to the same address at identical timestamps.
   However, if multiple accesses are guaranteed to be independent (that is, to different addresses), they can still share a timestamp
@@ -105,7 +111,7 @@ to have a strictly greater timestamp than the consumed token.
 This raises the question of how to represent timestamps and cleanly perform this check,
 as over a finite field the “less than” relation is ill-defined
 (though it is common and natural to consider it as the less than relation over the natural lift of the field into the integers).
-We choose to represent timestamps as machine words, using the existing `LT` chip (@lt) functionality for comparisons.
+We choose to represent timestamps as 32-bit words, using the existing `LT` chip (@lt) functionality for comparisons.
 The full implementation of the timestamp system can be seen in the `timestamp` column of the `CPU` (@cpu) and `MEMW` chips (@memw).
 The `CPU` merely passes in the current timestamp, while `MEMW` can recall the previously written timestamp and constrain the correct sequencing.
 
@@ -153,25 +159,8 @@ This table then feeds into the LogUp system in the normal way,
 emitting the initial tokens for all addresses in a page, without consuming any tokens.
 Since the `offset` column is always the same, it can be reused across all paged initialization and finalization tables.
 
-Concretely, each page gets an associated `PAGE` table, consisting of #total_nr_variables(chip) variables
-over #total_nr_instantiated_columns(chip, config) columns.
-For each such table, the `page` variable is instantiated as the constant base address of the page.
-The `offset` column is preprocessed, which helps the verifier ensure that each page has a single fixed size,
-but the verifier should still check that no pages overlap and all `page` values are page-aligned.
-
-== Page initialization
-
-#rj[check whether we need `fini` to be range-checked]
-We present here a set of constraints on the `PAGE` table that
-
-+ enforces the initial and final values of each address are bytes
-+ adds the initial and final interaction to the LogUp argument
-
-For zero-initialized pages, `init` can be a constant `0`,
-and hence doesn't need a column, nor a range check.
-
-#render_chip_variable_table(chip, config)
-#render_constraint_table(chip, config)
+Due to its interaction with the epoch-based proving system from @streaming,
+we defer a concrete instantiation and description of this scheme as an AIR table until then.
 
 
 #aside[Note on alternatives and trade-offs][
@@ -228,4 +217,3 @@ add the required balancing terms to the LogUp sum.
 = Future topics of interest
 
 - Optimize memory systems after determining factual bottlenecks (e.g. taking inspiration from Twist and Shout, or other recent research)
-- Double check whether IS_BYTE constraints are needed for fini

spec/memw.typ

@@ -124,9 +124,8 @@ This fast-path leverages that registers
 to achieve a footprint that is significantly smaller than both #memw and #aligned.
 
 Note: as a result of hard optimization, this chip can only be used for register accesses for which 
-+ $#`timestamp` - #`old_timestamp` in [1, 2^16]$, and
-+ $#`timestamp[0]` > #`old_timestamp[0]`$
-If either of these rules does not apply to your access, you should fall back to using `MEMW_A`.
+$#`timestamp` - #`old_timestamp` in [1, 2^16]$.
+If this does not apply to your access, you should fall back to using `MEMW_A`.
 
 Note moreover that this chip does not guard against misaligned register access faults: to access register with a given `address`, one must provide $2 dot #`address`$ in the lookup. 
 
@@ -144,10 +143,8 @@ The following range checks are assumed to be performed/enforced outside of this
 
 == Constraints
 Since most registers are frequently accessed, the difference between `timestamp` and `old_timestamp` is small most of the times.
-Rather than storing their (nearly) identical upper limbs twice, it is instead assumed that
-$#`old_timestamp[1]` = #`timestamp[1]`$; #aligned can be used for accesses where this is not the case.
 
-Verifying that $#`timestamp` > #`old_timestamp`$ now simplifies to verifying that $#`timestamp[0]` - #`old_timestamp[0]` > 0$.
+Verifying that $#`timestamp` > #`old_timestamp`$ now simplifies to verifying that $#`timestamp` - #`old_timestamp` > 0$.
 For most accesses, this value will be small enough to fit in a `Half`.
 This chip thus enforces this by means of the following constraint:
 #render_constraint_table(register_chip, config, groups: "diff")

spec/src/commit.toml

@@ -4,7 +4,7 @@ name = "COMMIT"
 
 [[variables.input]]
 name = "timestamp"
-type = "DWordWL"
+type = "Word"
 desc = "timestamp at which to commit"
 pad = 0
 
@@ -160,10 +160,17 @@ ref = "commit:c:read_value"
 
 [[constraints.commit]]
 kind = "interaction"
-tag = "COMMIT"
-input = ["index", "value"]
+tag = "memory"
+input = [2, ["arr", "index", 0], 0, "value"]
 multiplicity = ["-", "μ", "end"]
-ref = "commit:c:commit_value"
+ref = "commit:c:commit_value_out"
+
+[[constraints.commit]]
+kind = "interaction"
+tag = "memory"
+input = [2, ["arr", "index", 0], 1, "value"]
+multiplicity = ["-", ["-", "μ", "end"]]
+ref = "commit:c:commit_value_in"
 
 [[constraint_groups]]
 name = "end"

spec/src/config.toml

@@ -134,8 +134,8 @@ desc = """\
 
 [[variables.types]]
 label = "Timestamp"
-subtypes = ["DWordWL"]
-desc = "A preprocessed column holding timestamps as `DWordWL`. Row `i` of the column contains the value $2^2 dot (i + 1)$. Used in the CPU chip (@cpu), see there for more details about the magic number."
+subtypes = ["Word"]
+desc = "A preprocessed column holding timestamps as `Word`. Row `i` of the column contains the value $2^2 dot (i + 1)$. Used in the CPU chip (@cpu), see there for more details about the magic number."
 preprocessed = true
 
 [[variables.types]]

spec/src/cpu.toml

@@ -432,7 +432,7 @@ prefix = "M"
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 0], 1, 0, 0]
 output = ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register1"
 ref = "cpu:c:read_rv1"
@@ -446,7 +446,7 @@ iter = ["i", 0, 1]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 1], 1, 0, 0]
 output = ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register2"
 
@@ -459,7 +459,7 @@ iter = ["i", 0, 1]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 2], 1, 0, 0]
 multiplicity = "write_register"
 
 [[constraints.mem]]
@@ -488,14 +488,14 @@ input = ["prev_pc_timestamp_borrow"]
 [[constraints.mem]]
 kind = "interaction"
 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"]]
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["-", "timestamp", ["*", 3, ["not", "pc_double_read"]]], ["idx", "pc", "i"]]
 iter = ["i", 0, 1]
 multiplicity = 1
 
 [[constraints.mem]]
 kind = "interaction"
 tag = "memory"
-input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], ["idx", "next_pc", "i"]]
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", 1], ["idx", "next_pc", "i"]]
 iter = ["i", 0, 1]
 multiplicity = -1
 

spec/src/cpu32.toml

@@ -2,7 +2,7 @@ name = "CPU32"
 
 [[variables.input]]
 name = "timestamp"
-type = "DWordWL"
+type = "Word"
 desc = "The timestamp for the CPU row"
 pad = 0
 
@@ -171,8 +171,7 @@ desc = ""
 pad = 0
 
 [[assumptions]]
-desc = "`IS_WORD[timestamp[i]]`"
-iter = ["i", 0, 1]
+desc = "`IS_WORD[timestamp]`"
 
 [[assumptions]]
 desc = "`IS_WORD[pc[i]]`"
@@ -318,7 +317,7 @@ prefix = "M"
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 0], 1, 0, 0]
 output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register1"
 
@@ -331,7 +330,7 @@ iter = ["i", 0, 2]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 1], 1, 0, 0]
 output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register2"
 
@@ -344,7 +343,7 @@ iter = ["i", 0, 2]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 2], 1, 0, 0]
 multiplicity = "write_register"
 
 [[constraint_groups]]

spec/src/halt.toml

@@ -2,7 +2,7 @@ name = "HALT"
 
 [[variables.input]]
 name = "timestamp"
-type = "DWordWL"
+type = "Word"
 desc = "timestamp at which to halt the program"
 
 [[variables.auxiliary]]
@@ -11,8 +11,7 @@ type = "DWordWL"
 desc = "The `next_pc` value the CPU wrote during the instruction HALT was invoked"
 
 [[assumptions]]
-desc = "`IS_WORD[timestamp[i]]`"
-iter = ["i", 0, 1]
+desc = "`IS_WORD[timestamp]`"
 
 
 [[constraint_groups]]
@@ -21,39 +20,39 @@ name = "all"
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
+input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
 iter = ["i", 1, 9]
 multiplicity = 1
 ref = "halt:c:zeroize_registers_lo"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
+input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
 output = ["cast", 0, ["BaseField", 8]]
 multiplicity = 1
 ref = "halt:c:read_zero_exit_code"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
+input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
 iter = ["i", 11, 31]
 multiplicity = 1
 ref = "halt:c:zeroize_registers_hi"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "memory"
-input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["idx", "timestamp", 0], 1], ["idx", "timestamp", 1]], ["idx", "pc", "i"]]
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", 1], ["idx", "pc", "i"]]
 multiplicity = 1
 iter = ["i", 0, 1]
 ref = "halt:c:consume_pc"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "memory"
-input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["idx", "timestamp", 0], 1], ["idx", "timestamp", 1]], ["idx", ["arr", 1, 0], "i"]]
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", 1], ["idx", ["arr", 1, 0], "i"]]
 multiplicity = -1
 iter = ["i", 0, 1]
 ref = "halt:c:emit_pc"

spec/src/keccak.toml

@@ -2,7 +2,7 @@ name = "KECCAK"
 
 [[variables.input]]
 name = "timestamp"
-type = "DWordWL"
+type = "Word"
 desc = "timestamp at which the permutation is performed"
 pad = 0
 

spec/src/keccak_round.toml

@@ -2,7 +2,7 @@ name = "KECCAK_RND"
 
 [[variables.input]]
 name = "timestamp"
-type = "DWordWL"
+type = "Word"
 desc = "timestamp at which the permutation is performed"