diff --git a/spec/book.typ b/spec/book.typ index 11cc9acae..194689949 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -12,6 +12,7 @@ ("PROOF SYSTEM", ( ("logup.typ", [`LogUp` argument], ), ("memory.typ", [Memory argument], ), + ("streaming.typ", [Streaming prover], ), )), ("OVERVIEW", ( ("variables.typ", [Variables], ), @@ -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 diff --git a/spec/commit.typ b/spec/commit.typ index f9dc91a30..2bb966d03 100644 --- a/spec/commit.typ +++ b/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 3.#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. diff --git a/spec/halt.typ b/spec/halt.typ index 50a39ac40..930283a7b 100644 --- a/spec/halt.typ +++ b/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 diff --git a/spec/memory.typ b/spec/memory.typ index 6a204c1b7..bdd299b4b 100644 --- a/spec/memory.typ +++ b/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: )[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 diff --git a/spec/memw.typ b/spec/memw.typ index b963ea562..43c0d4e20 100644 --- a/spec/memw.typ +++ b/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") diff --git a/spec/src/commit.toml b/spec/src/commit.toml index fdfc19dfb..925d7f984 100644 --- a/spec/src/commit.toml +++ b/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" diff --git a/spec/src/config.toml b/spec/src/config.toml index 9eac1d8c8..c606eae1b 100644 --- a/spec/src/config.toml +++ b/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]] diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 4b2c538ca..cdbceee81 100644 --- a/spec/src/cpu.toml +++ b/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 diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index e226c847c..b9de9ddec 100644 --- a/spec/src/cpu32.toml +++ b/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]] diff --git a/spec/src/halt.toml b/spec/src/halt.toml index 6adc1efdb..303d9676f 100644 --- a/spec/src/halt.toml +++ b/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,7 +20,7 @@ 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" @@ -29,7 +28,7 @@ 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" @@ -37,7 +36,7 @@ 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" @@ -45,7 +44,7 @@ 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" @@ -53,7 +52,7 @@ 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" diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 23dedd208..e2916ab00 100644 --- a/spec/src/keccak.toml +++ b/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 diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 6ee05e29a..64fa60e18 100644 --- a/spec/src/keccak_round.toml +++ b/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" diff --git a/spec/src/l2g.toml b/spec/src/l2g.toml new file mode 100644 index 000000000..18dd256e8 --- /dev/null +++ b/spec/src/l2g.toml @@ -0,0 +1,89 @@ +name = "L2G" + +[[variables.input]] +name = "domain" +type = "BaseField" +desc = "The domain separator for different kinds of memory (RAM, register, commit, ...)" +pad = 0 + +[[variables.input]] +name = "address" +type = "DWordWL" +desc = "The address of this value" +pad = 0 + +[[variables.input]] +name = "init_epoch" +type = "B20" +desc = "The epoch in which we last saw this (domain, address)" +pad = 0 + +[[variables.input]] +name = "init_value" +type = "BaseField" +desc = "The value last written by `init_epoch`" +pad = 0 + +[[variables.output]] +name = "fini_timestamp" +type = "Word" +desc = "The last timestamp at which we wrote this value" +pad = 0 + +[[variables.output]] +name = "fini_value" +type = "BaseField" +desc = "The final value in this epoch" +pad = 0 + +[[variables.constant]] +name = "fini_epoch" +type = "B20" +desc = "This epoch's index" + + +[[constraint_groups]] +name = "consistency" + +[[constraints.consistency]] +kind = "interaction" +tag = "IS_B20" +input = ["init_epoch"] +multiplicity = 1 + +[[constraints.consistency]] +kind = "interaction" +tag = "IS_B20" +input = [["-", "fini_epoch", "init_epoch", 1]] +multiplicity = 1 + + +[[constraint_groups]] +name = "local" + +[[constraints.local]] +kind = "interaction" +tag = "memory" +input = ["domain", "address", 0, "init_value"] +multiplicity = -1 + +[[constraints.local]] +kind = "interaction" +tag = "memory" +input = ["domain", "address", "fini_timestamp", "fini_value"] +multiplicity = 1 + +[[constraint_groups]] +name = "global" + +[[constraints.global]] +kind = "interaction" +tag = "GLOBAL_MEM" +input = ["domain", "address", "init_epoch", "init_value"] +multiplicity = 1 + +[[constraints.global]] +kind = "interaction" +tag = "GLOBAL_MEM" +input = ["domain", "address", "fini_epoch", "fini_value"] +multiplicity = -1 diff --git a/spec/src/load.toml b/spec/src/load.toml index e6cf56f00..54493ce33 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -10,7 +10,7 @@ pad = 0 [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp at which this memory access is said to occur" pad = 0 @@ -76,8 +76,7 @@ desc = "`IS_WORD[base_address[i]]`" iter = ["i", 0, 1] [[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +desc = "`IS_WORD[timestamp]`" [[constraint_groups]] diff --git a/spec/src/memw.toml b/spec/src/memw.toml index c04fe5d34..ec0225e0c 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -22,7 +22,7 @@ pad = 0 [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp at which this memory access occurs" pad = 0 @@ -63,7 +63,7 @@ pad = 0 [[variables.auxiliary]] name = "old_timestamp" -type = ["DWordWL", 8] +type = ["Word", 8] desc = "The timestamp at which address `base_address + i` was last accessed" pad = 0 @@ -127,8 +127,7 @@ desc = "`IS_BIT`" desc = "`IS_BIT`" [[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +desc = "`IS_WORD[timestamp]`" [[constraint_groups]] name = "assumptions" @@ -185,21 +184,21 @@ iter = ["i", 0, 6] [[constraints.consistency]] kind = "interaction" tag = "ALU" -input = [["idx", "old_timestamp", 0], "timestamp", ["opsel", "LT"]] +input = [["arr", ["idx", "old_timestamp", 0], 0], ["arr", "timestamp", 0], ["opsel", "LT"]] output = ["arr", 1, 0] multiplicity = "μ_sum" [[constraints.consistency]] kind = "interaction" tag = "ALU" -input = [["idx", "old_timestamp", 1], "timestamp", ["opsel", "LT"]] +input = [["arr", ["idx", "old_timestamp", 1], 0], ["arr", "timestamp", 0], ["opsel", "LT"]] output = ["arr", 1, 0] multiplicity = "w2" [[constraints.consistency]] kind = "interaction" tag = "ALU" -input = [["idx", "old_timestamp", "i"], "timestamp", ["opsel", "LT"]] +input = [["arr", ["idx", "old_timestamp", "i"], 0], ["arr", "timestamp", 0], ["opsel", "LT"]] output = ["arr", 1, 0] iter = ["i", 2, 3] multiplicity = "w4" @@ -207,7 +206,7 @@ multiplicity = "w4" [[constraints.consistency]] kind = "interaction" tag = "ALU" -input = [["idx", "old_timestamp", "i"], "timestamp", ["opsel", "LT"]] +input = [["arr", ["idx", "old_timestamp", "i"], 0], ["arr", "timestamp", 0], ["opsel", "LT"]] output = ["arr", 1, 0] iter = ["i", 4, 7] multiplicity = "write8" diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 0e0e20d5d..60d3673c0 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -22,7 +22,7 @@ pad = 0 [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp at which this memory access is said to occur" pad = 0 @@ -57,7 +57,7 @@ pad = 0 [[variables.auxiliary]] name = "old_timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp at which the address was last accessed" pad = 0 @@ -115,8 +115,7 @@ desc = "`IS_BIT`" desc = "`IS_BIT`" [[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +desc = "`IS_WORD[timestamp]`" [[constraint_groups]] name = "assumptions" @@ -173,7 +172,7 @@ poly = ["*", "w2", ["not", "μ_sum"]] [[constraints.consistency]] kind = "interaction" tag = "ALU" -input = ["old_timestamp", "timestamp", ["opsel", "LT"]] +input = [["arr", "old_timestamp", 0], ["arr", "timestamp", 0], ["opsel", "LT"]] output = ["arr", 1, 0] multiplicity = "μ_sum" diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 3e7cdcf28..9b9dbd965 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -10,7 +10,7 @@ pad = 0 [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "timestamp at which the access takes place" pad = 0 @@ -27,17 +27,11 @@ desc = "value of this register at `old_timestamp`." pad = 0 [[variables.auxiliary]] -name = "old_timestamp_lo" +name = "old_timestamp" type = "Word" -desc = "the lower limb of `old_timestamp`" +desc = "The timestamp at which this register was last accessed" pad = 0 -[[variables.virtual]] -name = "old_timestamp" -type = "DWordWL" -desc = "timestamp at which this register was last accessed" -def = ["cast", ["arr", "old_timestamp_lo", ["idx", "timestamp", 1]], "DWordWL"] - [[variables.virtual]] name = "μ_sum" type = "Bit" @@ -66,8 +60,7 @@ iter = ["i", 0, 1] ref = "regw:a:val" [[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +desc = "`IS_WORD[timestamp]`" ref = "regw:a:timestamp" # Constraints @@ -78,7 +71,7 @@ name = "diff" [[constraints.diff]] kind = "interaction" tag = "IS_HALF" -input = [["-", ["idx", "timestamp", 0], ["idx", "old_timestamp", 0], 1]] +input = [["-", "timestamp", "old_timestamp", 1]] multiplicity = "μ_sum" ref = "regw:c:diff" diff --git a/spec/src/page.toml b/spec/src/page.toml index b6247a7c7..e12d89d82 100644 --- a/spec/src/page.toml +++ b/spec/src/page.toml @@ -23,9 +23,9 @@ type = "Byte" desc = "The final value this address took" [[variables.input]] -name = "timestamp" -type = "DWordWL" -desc = "The timestamp at which this address was last accessed" +name = "fini_epoch" +type = "B20" +desc = "The epoch at which this address was last accessed" # Virtual @@ -44,19 +44,14 @@ kind = "template" tag = "IS_BYTE" input = ["init"] -[[constraints.all]] -kind = "template" -tag = "IS_BYTE" -input = ["fini"] - [[constraints.all]] kind = "interaction" -tag = "memory" -input = [0, "address", ["cast", 0, "DWordWL"], "init"] +tag = "GLOBAL_MEM" +input = [0, "address", 0, "init"] multiplicity = -1 [[constraints.all]] kind = "interaction" -tag = "memory" -input = [0, "address", "timestamp", "fini"] +tag = "GLOBAL_MEM" +input = [0, "address", "fini_epoch", "fini"] multiplicity = 1 diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 8ef356578..ad92671ba 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -2,7 +2,7 @@ name = "SHA256" [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "Timestamp at which the ECALL is invoked. Used as unique identifier for this invocation." pad = 0 @@ -135,7 +135,7 @@ input = [ ["idx", "out", ["+", ["*", 8, "i"], 6]], ["idx", "out", ["+", ["*", 8, "i"], 5]], ["idx", "out", ["+", ["*", 8, "i"], 4]]], - ["+", "timestamp", ["cast", 1, "DWordWL"]], + ["+", "timestamp", 1], 0, 0, 1 ] output = ["arr", diff --git a/spec/src/sha256msgsched.toml b/spec/src/sha256msgsched.toml index 402f7459a..40f45378f 100644 --- a/spec/src/sha256msgsched.toml +++ b/spec/src/sha256msgsched.toml @@ -2,7 +2,7 @@ name = "SHA256MSGSCHED" [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp/identifier for this execution of the message schedule" pad = 0 diff --git a/spec/src/sha256round.toml b/spec/src/sha256round.toml index 0c05cdf4a..036b4a2c2 100644 --- a/spec/src/sha256round.toml +++ b/spec/src/sha256round.toml @@ -2,7 +2,7 @@ name = "SHA256ROUND" [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp/identifier for this execution of the round function" pad = 0 diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 6ea23bb9e..e7777d9f1 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -53,7 +53,7 @@ input = ["DWordWL", "DWordWL", "BaseField"] [[signatures]] tag = "CPU32" kind = "interaction" -input = ["DWordWL", "DWordWL"] +input = ["Word", "DWordWL"] output = "Byte" # ALU[out; in1, in2, flags] @@ -67,7 +67,7 @@ output = "DWordWL" [[signatures]] tag = "MEMOP" kind = "interaction" -input = ["DWordWL", "DWordWL", "DWordWL", "Byte"] +input = ["Word", "DWordWL", "DWordWL", "Byte"] output = "DWordWL" # BRANCH[next_pc; pc, offset, register, JALR] @@ -81,39 +81,33 @@ output = "DWordWL" [[signatures]] tag = "MEMW" kind = "interaction" -input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"] +input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] output = ["BaseField", 8] # MEMW[is_register, base_address, value, timestamp, write2, write4, write8] [[signatures]] tag = "MEMW" kind = "interaction" -input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"] +input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] # LOAD[res; base_address, timestamp, flags] [[signatures]] tag = "LOAD" kind = "interaction" -input = ["DWordWL", "DWordWL", "Byte"] +input = ["DWordWL", "Word", "Byte"] output = "DWordWL" # ECALL[timestamp, syscallnr] [[signatures]] tag = "ECALL" kind = "interaction" -input = ["DWordWL", "DWordWL"] +input = ["Word", "DWordWL"] # CNB[timestamp, index, address, count] [[signatures]] tag = "CNB" kind = "interaction" -input = ["DWordWL", "BaseField", "DWordWL", "DWordWL"] - -# COMMIT[index, value] -[[signatures]] -tag = "COMMIT" -kind = "interaction" -input = ["BaseField", "Byte"] +input = ["Word", "BaseField", "DWordWL", "DWordWL"] # BYTE_ALU[res; selector, X, Y] [[signatures]] @@ -168,11 +162,17 @@ kind = "interaction" input = ["Half", "B4"] output = ["Half", 2] -# The actual memory tokens, see MEMW and PAGE +# The actual memory tokens, see MEMW, L2G and PAGE [[signatures]] tag = "memory" kind = "interaction" -input = ["Bit", "DWordWL", "DWordWL", "BaseField"] +input = ["BaseField", "DWordWL", "Word", "BaseField"] + +# Global memory: domain, address, epoch, value +[[signatures]] +tag = "GLOBAL_MEM" +kind = "interaction" +input = ["BaseField", "DWordWL", "B20", "BaseField"] # SHA256 things [[signatures]] @@ -184,13 +184,13 @@ output = "Word" [[signatures]] tag = "SHA256_M" kind = "interaction" -input = ["DWordWL", "BaseField"] +input = ["Word", "BaseField"] output = "Word" [[signatures]] tag = "SHA256ROUND" kind = "interaction" -input = ["DWordWL", ["Word", 8], "BaseField"] +input = ["Word", ["Word", 8], "BaseField"] [[signatures]] tag = "ROTXOR" @@ -202,7 +202,7 @@ output = "Word" [[signatures]] tag = "KECCAK" kind = "interaction" -input = ["DWordWL", "BaseField", [[["Byte", 8], 5], 5]] +input = ["Word", "BaseField", [[["Byte", 8], 5], 5]] # Keccak round constants [[signatures]] diff --git a/spec/src/store.toml b/spec/src/store.toml index 2d97dd00b..cff3ca81d 100644 --- a/spec/src/store.toml +++ b/spec/src/store.toml @@ -10,7 +10,7 @@ pad = 0 [[variables.input]] name = "timestamp" -type = "DWordWL" +type = "Word" desc = "The timestamp at which this memory access is said to occur" pad = 0 @@ -60,8 +60,7 @@ desc = "`IS_WORD[base_address[i]]`" iter = ["i", 0, 1] [[assumptions]] -desc = "`IS_WORD[timestamp[i]]`" -iter = ["i", 0, 1] +desc = "`IS_WORD[timestamp]`" [[constraint_groups]] diff --git a/spec/streaming.typ b/spec/streaming.typ new file mode 100644 index 000000000..5c8df43df --- /dev/null +++ b/spec/streaming.typ @@ -0,0 +1,140 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + render_chip_padding_table, + render_constraint_table, + total_nr_instantiated_columns, + total_nr_variables, +) + +#show: book-page("streaming.typ") + +In this chapter, we present our approach, which we name "epoch proving",#footnote[ + We additionally considered a "streaming" prover approach, + proceeding in multiple phases (commit, logup, FRI, open), + where only the tables that are actively being filled are required in memory. + It comes at the cost of additional engineering complexity and re-executions. +] +to reducing the required amount of prover working memory +when proving larger programs. +We avoid resorting to a full-blown sharding+recursion approach, and as such avoid the +complications for the verifier to deal with cross-shard consistency constraints. + +The overarching idea is to let the prover build up tables, and once memory-pressure grows +too much, perform some prover work to allow evicting tables from memory. + +We observe that the majority of constraints on a contiguous section of cycles +is independent of the other cycles: only the consistency of the memory accesses has to cross all boundaries (see also @memory). +As such, we proceed in "epochs" ---the size of which is again informed by the memory pressure--- where +all table-to-table interactions can be proven within a single epoch. +One additional constraint on the size of an epoch comes from the padding scheme of the CPU (@cpu): +every epoch but the last should have a power-of-two number of rows for the CPU table(s) ---that is, it needs no padding--- +since padding the CPU table requires the program to have already halted. + +To deal with cross-epoch memory, we introduce a "local-to-global" table (`L2G`) per epoch that, in essence, +is an epoch-local memory initialization and finalization mechanism. +It initializes any memory cell that is accessed in the epoch, by claiming its value and originating epoch. +Similarly, it finalizes each accessed memory cell in the epoch-local LogUp, and claims the current value and last accessed timestamp. +This both allows frequent access to a small number of addresses within an epoch to have a small cross-epoch footprint, +and addresses that are not accessed for multiple consecutive epochs to not incur a cost when not accessed. +In this system, timestamp values only carry significance within the epoch they occur in, +and the ordered pair $(serif("epoch"), serif("timestamp"))$ can be considered as the "global timestamp", +although no part of the VM requires a global timestamp to be materialized. +Since we choose to represent the epoch-local timestamps as 32-bit `Word` values, +an epoch _should not_ consist of more than $2^30$ cycles +(refer to the scaling factor in @memory:aside:granularity). + +As such, each epoch proceeds by committing to all its tables,#footnote[ + The local-to-global will require a separate Merkle tree to allow the separation of epoch-local and cross-epoch proving. +] obtaining epoch-local LogUp challenges, +proving the epoch-local (that is, without cross-epoch memory interaction) LogUp sum is zero, and performing a full batch FRI, including the queries. +All tables other than the local-to-global ones can be permanently evicted from memory at this point, and no further work for these tables is required. +It is plausible that the total size of all local-to-global tables remains small enough across a 1B-cycle execution, +that their LDE and Merkle tree can be kept in memory throughout. + +Finally, one more LogUp is proven on the aggregation of all local-to-global tables, with the global memory initialization and finalization, to prove the global memory consistency. +Note that the Fiat-Shamir transcripts of both the epoch proofs and the global proof should be bound to +the same local-to-global commitments. + +This system should allow simple scaling across multiple GPU or worker nodes, as each epoch can be proven +in isolation by a worker, while the execution and proving continues with the next epoch in tandem. + +While this approach cleanly sidesteps the need for re-execution ---or if re-execution is needed still for +the local-to-global tables, avoids most of the computational work in interpolation and hashing--- +it comes with some tradeoffs: +- An extra table has to be introduced and proven. This is likely to be very minor compared to the overall work. +- By having a single cycle at which all tables need to be proven and retired, + rather than only retiring completed tables, a larger cost in padding is expected. + Having many tables that could consist of only a few rows is likely to make this even more pronounced. + Lowering the table size and proving more tables per epoch may alleviate this somewhat. +- The overall proof conceptually consists of several sub-proofs that should however _not_ be considered + in isolation, as there must be shared commitments between the epoch-local proofs and the global memory proof. + + +#let config = load_config() +#let l2gchip = load_chip("src/l2g.toml", config) +#let l2g = raw(l2gchip.name) += #l2g chip + +== Variables + +#render_chip_variable_table(l2gchip, config) + +== Constraints + +First, we have the consistency constraints that need to be enforced for the chip's correctness. +These can be enforced in the epoch-local proof, and will still hold during the global proof by +making sure the commitment matches between the local and global proof. +We currently assume that no more than $2^20$ epochs can occur in one execution. +This can be extended at the cost of extra interactions and potentially extra columns. + +#render_constraint_table(l2gchip, config, groups: "consistency") + +Then we have local constraints that should be enforced inside of the epoch. + +#render_constraint_table(l2gchip, config, groups: "local") + +And finally, the interactions that are pare of the global memory consistency proof. + +#render_constraint_table(l2gchip, config, groups: "global") + +== Padding + +Observe that all interactions in this table are unconditional. +As a result, padding rows need to be chosen such that they have no unwanted effects. +We achieve this by "bringing forward" unused values from an older epoch. +Even though they are not touched by the current epoch, the #l2g chips claims they are +and simply has finalization clean up the spurious initialization, by setting +`fini_value = init_value` and `fini_timestamp = 0`. + + +#let pagechip = load_chip("src/page.toml", config) +#let page = raw(pagechip.name) += #page chip + +We resume here the description of memory initialization and finalization from @memory, +as it applies after integration of the epoch system described above. +Concretely, each page gets an associated `PAGE` table, consisting of #total_nr_variables(pagechip) variables +over #total_nr_instantiated_columns(pagechip, 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. + +Observe that this table deals with boundaries on the RAM memory. +Registers can still be initialized and finalized in the global memory directly by the verifier, +and then transparently bridged between epochs in the same #l2g tables that are already present for RAM values too. + +== Constraints + +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 global memory 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(pagechip, config) +#render_constraint_table(pagechip, config)