From 18ffa535460eef214cd85706b2e447bbf81e4591 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 2 Jun 2026 14:48:01 +0200 Subject: [PATCH 01/11] spec: Draft streaming prover approaches --- spec/book.typ | 1 + spec/streaming.typ | 87 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 88 insertions(+) create mode 100644 spec/streaming.typ diff --git a/spec/book.typ b/spec/book.typ index 8bf8612af..c0ee0c465 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -11,6 +11,7 @@ ("PROOF SYSTEM", ( ("logup.typ", [`LogUp` argument], ), ("memory.typ", [Memory argument], ), + ("streaming.typ", [Streaming prover], ), )), ("OVERVIEW", ( ("variables.typ", [Variables], ), diff --git a/spec/streaming.typ b/spec/streaming.typ new file mode 100644 index 000000000..1f2b0354f --- /dev/null +++ b/spec/streaming.typ @@ -0,0 +1,87 @@ +#import "/book.typ": book-page, rj, aside, xref +#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") + +We present two potential approaches 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 +complications for the verifier to deal with cross-shard consistency constraints. + +The overarching idea in both 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. +the difference lies in exactly what and how much proving happens, and how much extra computation is needed +later on. + += Approach 1: Prove-and-retire + +In the first potential approach, we proceed in multiple passes: +- *Commit*: The prover proceeds through execution, witness generation and interpolation as usual + once the memory pressure becomes too large, the prover batch commits to all full (or large enough) tables + in memory; then these tables are dropped from memory ("retired"). + All FRI polynomials generated during this phase can already be accumulated in a single batch polynomial, + by sampling the batching coefficients after commiting to the polynomials they randomize. +- *Challenge*: At the end of the execution, the remaining tables are padded and commited to. + LogUp challenges are sampled. +- *LogUp re-execution*: The prover restarts execution from zero, performing the reduction to FRI polynomials + for the LogUp interactions, and batching the polynomials into the batch FRI polynomial from before. + Again, this can be optimized for memory usage by only keeping +- *FRI*: At this point, all FRI instances are available in a single batch polynomial, + and the FRI folding can be performed, resulting in a set of query opening points. +- *Open*: One final re-execution can now be performed to generate the requested Merkle openings. + +This approach comes at a clear cost of extra interpolations and Merkle tree evaluations, +but manages to keep a clean evaluation model that almost directly (apart from the early commitments and batching) +corresponds to the naive, memory-intensive proving model. +An optimization is possible to reduce the cost of the *Open* phase, by keeping the internal nodes of the merkle tree +in memory, obviating the need to recompute it; while still dropping the biggest memory cost (the leaves). + +To distribute this workload across worker nodes or multiple GPUs, it is possible to "send off" +each batch of tables being retired to the next available worker. +With some care, it is likely possible to decouple the Fiat-Shamir challenges of multiple retirement batches, +so that this doesn't introduce a dependency on a previous batch completing before the next one can happen. + += Approach 2: Prove-epoch + +In the second potential approach, 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. +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. + +To deal with cross-epoch memory, we introduce a "local-to-global" table per epoch that, in essence, +is an epoch-local memory initialiation and finalization mechanism. +It initializes any memory cell that is accessed in the epoch, by claiming its value, originating epoch, and timestamp. +Similarly, each accessed memory cell is finalized in the epoch-local LogUp, and claims the current value, epoch 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. + +As such, each epoch proceeds by commiting 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 re-execution (or interpolation and commitment) 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 no re-execution at all is required. + +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. + +Similarly to the previous approach, this should distribute cleanly across multiple worker nodes or GPUs. + +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 too 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. From c54be650787281fc7db1d6d73f6cc5697e0df70f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 2 Jun 2026 14:59:41 +0200 Subject: [PATCH 02/11] editorial --- spec/streaming.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/streaming.typ b/spec/streaming.typ index 1f2b0354f..04294cbf7 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -13,12 +13,12 @@ We present two potential approaches 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 +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 in both 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. -the difference lies in exactly what and how much proving happens, and how much extra computation is needed +The difference lies in exactly what and how much proving happens, and how much extra computation is needed later on. = Approach 1: Prove-and-retire @@ -33,7 +33,7 @@ In the first potential approach, we proceed in multiple passes: LogUp challenges are sampled. - *LogUp re-execution*: The prover restarts execution from zero, performing the reduction to FRI polynomials for the LogUp interactions, and batching the polynomials into the batch FRI polynomial from before. - Again, this can be optimized for memory usage by only keeping + Again, this can be optimized for memory usage by only instantiating the columns required for the LogUp. - *FRI*: At this point, all FRI instances are available in a single batch polynomial, and the FRI folding can be performed, resulting in a set of query opening points. - *Open*: One final re-execution can now be performed to generate the requested Merkle openings. @@ -57,7 +57,7 @@ As such, we proceed in "epochs" ---the size of which is again informed by the me all table-to-table interactions can be proven within a single epoch. To deal with cross-epoch memory, we introduce a "local-to-global" table per epoch that, in essence, -is an epoch-local memory initialiation and finalization mechanism. +is an epoch-local memory initialization and finalization mechanism. It initializes any memory cell that is accessed in the epoch, by claiming its value, originating epoch, and timestamp. Similarly, each accessed memory cell is finalized in the epoch-local LogUp, and claims the current value, epoch 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, From e8e1791fa92b06b7afbc94650e2633eeeebd3b42 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 8 Jun 2026 15:13:27 +0200 Subject: [PATCH 03/11] Update spec/streaming.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/streaming.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/streaming.typ b/spec/streaming.typ index 04294cbf7..75a8b1007 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -24,8 +24,8 @@ later on. = Approach 1: Prove-and-retire In the first potential approach, we proceed in multiple passes: -- *Commit*: The prover proceeds through execution, witness generation and interpolation as usual - once the memory pressure becomes too large, the prover batch commits to all full (or large enough) tables +- *Commit*: The prover proceeds through execution, witness generation and interpolation as usual. + Once the memory pressure becomes too large, the prover batch commits to all full (or large enough) tables in memory; then these tables are dropped from memory ("retired"). All FRI polynomials generated during this phase can already be accumulated in a single batch polynomial, by sampling the batching coefficients after commiting to the polynomials they randomize. From 36c40fc11fd24eb031d49046fb282fa13db40bb8 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 16:35:04 +0200 Subject: [PATCH 04/11] Make asides referenceable --- spec/book.typ | 29 ++++++++++++++++++++--------- spec/memory.typ | 2 +- 2 files changed, 21 insertions(+), 10 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index c0ee0c465..ee00759e1 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -68,6 +68,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)) + } body } @@ -80,15 +92,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/memory.typ b/spec/memory.typ index 6a204c1b7..942ed6da9 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -64,7 +64,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 From b2b5f57dd27891407d08e3a20333275979b8da1d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 16:37:07 +0200 Subject: [PATCH 05/11] Update continuations spec for chosen variant --- spec/memory.typ | 21 +----- spec/src/l2g.toml | 89 ++++++++++++++++++++++++ spec/src/page.toml | 19 ++---- spec/src/signatures.toml | 6 ++ spec/streaming.typ | 143 +++++++++++++++++++++++++++------------ 5 files changed, 202 insertions(+), 76 deletions(-) create mode 100644 spec/src/l2g.toml diff --git a/spec/memory.typ b/spec/memory.typ index 942ed6da9..d938e85bd 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -153,25 +153,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][ 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/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/signatures.toml b/spec/src/signatures.toml index 6ea23bb9e..a80ba9395 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -174,6 +174,12 @@ tag = "memory" kind = "interaction" input = ["Bit", "DWordWL", "DWordWL", "BaseField"] +# Global memory: is_register, address, epoch, value +[[signatures]] +tag = "GLOBAL_MEM" +kind = "interaction" +input = ["Bit", "DWordWL", "B20", "BaseField"] + # SHA256 things [[signatures]] tag = "SHA256_K" diff --git a/spec/streaming.typ b/spec/streaming.typ index 75a8b1007..645d0bcc7 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, rj, aside, xref +#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -11,73 +11,59 @@ #show: book-page("streaming.typ") -We present two potential approaches to reducing the required amount of prover working memory +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 in both is to let the prover build up tables, and once memory-pressure grows +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. -The difference lies in exactly what and how much proving happens, and how much extra computation is needed -later on. - -= Approach 1: Prove-and-retire - -In the first potential approach, we proceed in multiple passes: -- *Commit*: The prover proceeds through execution, witness generation and interpolation as usual. - Once the memory pressure becomes too large, the prover batch commits to all full (or large enough) tables - in memory; then these tables are dropped from memory ("retired"). - All FRI polynomials generated during this phase can already be accumulated in a single batch polynomial, - by sampling the batching coefficients after commiting to the polynomials they randomize. -- *Challenge*: At the end of the execution, the remaining tables are padded and commited to. - LogUp challenges are sampled. -- *LogUp re-execution*: The prover restarts execution from zero, performing the reduction to FRI polynomials - for the LogUp interactions, and batching the polynomials into the batch FRI polynomial from before. - Again, this can be optimized for memory usage by only instantiating the columns required for the LogUp. -- *FRI*: At this point, all FRI instances are available in a single batch polynomial, - and the FRI folding can be performed, resulting in a set of query opening points. -- *Open*: One final re-execution can now be performed to generate the requested Merkle openings. - -This approach comes at a clear cost of extra interpolations and Merkle tree evaluations, -but manages to keep a clean evaluation model that almost directly (apart from the early commitments and batching) -corresponds to the naive, memory-intensive proving model. -An optimization is possible to reduce the cost of the *Open* phase, by keeping the internal nodes of the merkle tree -in memory, obviating the need to recompute it; while still dropping the biggest memory cost (the leaves). - -To distribute this workload across worker nodes or multiple GPUs, it is possible to "send off" -each batch of tables being retired to the next available worker. -With some care, it is likely possible to decouple the Fiat-Shamir challenges of multiple retirement batches, -so that this doesn't introduce a dependency on a previous batch completing before the next one can happen. - -= Approach 2: Prove-epoch - -In the second potential approach, 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. + +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 per epoch that, in essence, +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, originating epoch, and timestamp. -Similarly, each accessed memory cell is finalized in the epoch-local LogUp, and claims the current value, epoch and last accessed timestamp. +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 commiting 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 re-execution (or interpolation and commitment) for these tables is required. +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 no re-execution at all is required. +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. -Similarly to the previous approach, this should distribute cleanly across multiple worker nodes or GPUs. +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 too comes with some tradeoffs: +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. @@ -85,3 +71,70 @@ it too comes with some tradeoffs: 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) From 5e6a2418c46126f67e0183ab5381911a87d533c1 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 16:38:30 +0200 Subject: [PATCH 06/11] Bring commit into the global memory argument --- spec/commit.typ | 11 +++++++++++ spec/memory.typ | 6 ++++++ spec/src/commit.toml | 13 ++++++++++--- spec/src/signatures.toml | 4 ++-- 4 files changed, 29 insertions(+), 5 deletions(-) diff --git a/spec/commit.typ b/spec/commit.typ index a6fea1b6c..b875c66aa 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -65,6 +65,17 @@ 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. +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/memory.typ b/spec/memory.typ index d938e85bd..6c561530d 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. diff --git a/spec/src/commit.toml b/spec/src/commit.toml index 89fa133c6..ea2f73ce1 100644 --- a/spec/src/commit.toml +++ b/spec/src/commit.toml @@ -160,10 +160,17 @@ ref = "commit:c:read_value" [[constraints.commit]] kind = "interaction" -tag = "COMMIT" -input = ["index", "value"] +tag = "memory" +input = [3, ["arr", "index", 0], ["cast", 0, "Word"], "value"] multiplicity = ["-", "μ", "end"] -ref = "commit:c:commit_value" +ref = "commit:c:commit_value_out" + +[[constraints.commit]] +kind = "interaction" +tag = "memory" +input = [3, ["arr", "index", 0], ["cast", 0, "Word"], "value"] +multiplicity = ["-", ["-", "μ", "end"]] +ref = "commit:c:commit_value_in" [[constraint_groups]] name = "end" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index a80ba9395..1640e2db8 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -172,13 +172,13 @@ output = ["Half", 2] [[signatures]] tag = "memory" kind = "interaction" -input = ["Bit", "DWordWL", "DWordWL", "BaseField"] +input = ["BaseField", "DWordWL", "DWordWL", "BaseField"] # Global memory: is_register, address, epoch, value [[signatures]] tag = "GLOBAL_MEM" kind = "interaction" -input = ["Bit", "DWordWL", "B20", "BaseField"] +input = ["BaseField", "DWordWL", "B20", "BaseField"] # SHA256 things [[signatures]] From c7d219d17bfb1cad3202537794f4fba647bb4413 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 16:40:31 +0200 Subject: [PATCH 07/11] Make timestamps 32-bits in the epoch world --- spec/halt.typ | 2 +- spec/memory.typ | 2 +- spec/memw.typ | 9 +++------ spec/src/commit.toml | 2 +- spec/src/config.toml | 2 +- spec/src/cpu.toml | 10 +++++----- spec/src/cpu32.toml | 11 +++++------ spec/src/halt.toml | 15 +++++++-------- spec/src/keccak.toml | 2 +- spec/src/keccak_round.toml | 2 +- spec/src/load.toml | 5 ++--- spec/src/memw.toml | 15 +++++++-------- spec/src/memw_aligned.toml | 9 ++++----- spec/src/memw_register.toml | 17 +++++------------ spec/src/sha256.toml | 4 ++-- spec/src/sha256msgsched.toml | 2 +- spec/src/sha256round.toml | 2 +- spec/src/signatures.toml | 32 +++++++++++++------------------- spec/src/store.toml | 5 ++--- 19 files changed, 63 insertions(+), 85 deletions(-) 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 6c561530d..998938a1d 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -111,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. 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 ea2f73ce1..24cc76bc6 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 diff --git a/spec/src/config.toml b/spec/src/config.toml index 9eac1d8c8..fba796af5 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -134,7 +134,7 @@ desc = """\ [[variables.types]] label = "Timestamp" -subtypes = ["DWordWL"] +subtypes = ["Word"] 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." preprocessed = true diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 85c3aaf70..9b14e90f8 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 1c3bade44..c9c6b8596 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/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/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 45da4d452..2405f4d84 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 1640e2db8..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,13 +162,13 @@ 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 = ["BaseField", "DWordWL", "DWordWL", "BaseField"] +input = ["BaseField", "DWordWL", "Word", "BaseField"] -# Global memory: is_register, address, epoch, value +# Global memory: domain, address, epoch, value [[signatures]] tag = "GLOBAL_MEM" kind = "interaction" @@ -190,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" @@ -208,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]] From a4cb36a2c38b78136835b135387fac4709e2352e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 16:42:17 +0200 Subject: [PATCH 08/11] Remove future note in favor of #694 --- spec/memory.typ | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/memory.typ b/spec/memory.typ index 998938a1d..bdd299b4b 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -217,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 From 142b9f50eacf084b3213a6cf09550b6570646d1a Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 17:01:49 +0200 Subject: [PATCH 09/11] AI review fixes --- spec/src/commit.toml | 4 ++-- spec/src/config.toml | 2 +- spec/src/cpu.toml | 2 +- spec/streaming.typ | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/src/commit.toml b/spec/src/commit.toml index 4b23b4d52..925d7f984 100644 --- a/spec/src/commit.toml +++ b/spec/src/commit.toml @@ -161,14 +161,14 @@ ref = "commit:c:read_value" [[constraints.commit]] kind = "interaction" tag = "memory" -input = [3, ["arr", "index", 0], ["cast", 0, "Word"], "value"] +input = [2, ["arr", "index", 0], 0, "value"] multiplicity = ["-", "μ", "end"] ref = "commit:c:commit_value_out" [[constraints.commit]] kind = "interaction" tag = "memory" -input = [3, ["arr", "index", 0], ["cast", 0, "Word"], "value"] +input = [2, ["arr", "index", 0], 1, "value"] multiplicity = ["-", ["-", "μ", "end"]] ref = "commit:c:commit_value_in" diff --git a/spec/src/config.toml b/spec/src/config.toml index fba796af5..c606eae1b 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -135,7 +135,7 @@ desc = """\ [[variables.types]] label = "Timestamp" subtypes = ["Word"] -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." +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 dbe45fd27..cdbceee81 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -488,7 +488,7 @@ input = ["prev_pc_timestamp_borrow"] [[constraints.mem]] kind = "interaction" tag = "memory" -input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", ["-", "timestamp", ["*", 3, ["not", "pc_double_read"]]]], ["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 diff --git a/spec/streaming.typ b/spec/streaming.typ index 645d0bcc7..5c8df43df 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -46,7 +46,7 @@ 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 commiting to all its tables,#footnote[ +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. From e9d49b1b8de53052fa59af03684541957ee5e476 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 6 Jul 2026 17:54:47 +0200 Subject: [PATCH 10/11] Elaborate on commitment cleanup by the verifier --- spec/commit.typ | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/spec/commit.typ b/spec/commit.typ index 89826bc9f..2bb966d03 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -66,7 +66,11 @@ 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. +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 From d8f92155dd51607189ae53f97ffc33e05ac0faee Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 9 Jul 2026 11:03:41 +0200 Subject: [PATCH 11/11] Apply suggestions from code review Co-authored-by: Cyprien de Saint Guilhem Co-authored-by: Robin Jadoul --- spec/commit.typ | 2 +- spec/streaming.typ | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/commit.typ b/spec/commit.typ index 2bb966d03..b15f75e3f 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -66,7 +66,7 @@ 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[ +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. diff --git a/spec/streaming.typ b/spec/streaming.typ index 5c8df43df..83b398fd2 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -96,7 +96,7 @@ 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. +And finally, the interactions that are part of the global memory consistency proof. #render_constraint_table(l2gchip, config, groups: "global")