spec: Move to the epoch system

[RobinJadoul]

After initial discussion, the choice was made for epoch-based proving, so this PR now formalizes this.
Additionally, it deals with the integration of COMMIT into this new paradigm by use of memory domain separation.
Since epochs are short, we can also reduce the surface area everywhere by only using Word variables for timestamps. This leaves open potential optimizations in MEMW where now only single-limb values need to be compared.

[github-actions]

Codex Code Review

Findings

Low: spec/streaming.typ has an unfinished sentence in the LogUp re-execution bullet: “Again, this can be optimized for memory usage by only keeping”. This leaves the proposed proving flow ambiguous; finish or remove the sentence before merging.

No security vulnerabilities, VM behavior bugs, or significant performance issues found in the PR diff. The changes are documentation-only. I could not run a Typst/Shiroa build because neither typst nor shiroa is installed in this environment.

[claude]

Medium — Cryptographic soundness concern: Decoupling Fiat-Shamir challenges across retirement batches is non-trivial. If batches can derive challenges before all prior commitments from other concurrent batches are fixed, an adversary might be able to adaptively choose table contents in a later batch based on a challenge sampled by an earlier one, breaking the soundness reduction.

Before this claim is carried into implementation it should either:

• Reference a known-safe technique (e.g. parallel composition with independent random oracles, a random beacon, etc.), or
• Precisely define what "decouple" means here and argue why cross-batch influence is impossible given the ordering constraints.

[RobinJadoul]

The underlying idea is that the randomizer for a batch depends on the batch itself, so any offset elsewhere will be randomized with a different challenge

[claude]

Bug (editorial) + Medium — Soundness gap:

1. Typo: "initialiation" → "initialization".
2. The spec does not state what prevents the same address from appearing in more than one epoch's initialization segment simultaneously. If a malicious prover can claim a memory cell is "initialized" (with an arbitrary value) in two different epochs' local-to-global tables, it could forge values. The spec should explicitly state the constraint that enforces each address has at most one initialization across all epochs, and reference how this ties into the global LogUp token balance in memory.typ.

[RobinJadoul]

2 is clearly enforced by the global memory LogUp described by the approach

[claude]

Review Summary

This is a pure specification document (no code changes). Findings are focused on correctness of the prose and cryptographic protocol descriptions.

Editorial (fix before merging)

• L17: Duplicate word (suggestion posted inline)
• L21: Sentence starts lowercase (suggestion posted inline)
• L36: Incomplete sentence cut off mid-thought; the optimization being described is unfinished
• L60: Typo 'initialiation' should be 'initialization'

Medium - Cryptographic soundness (address before implementation)

• L49 (Approach 1 - decoupled Fiat-Shamir): The claim that retirement-batch challenges can be decoupled without a soundness gap needs more precision. Concurrent batches sampling independent challenges while tables from other batches are still being built could allow adaptive influence across batches. Needs either a reference to a known-safe parallelism technique or an explicit argument that inter-batch influence is impossible given the protocol ordering.
• L60 (Approach 2 - epoch double-initialization): The spec does not state what prevents a malicious prover from claiming the same address as initialized in two different epochs local-to-global tables simultaneously. Should explicitly reference the global LogUp token-balance constraint from the memory argument that enforces at-most-one initialization per address.

No Rust code, unsafe blocks, or cryptographic implementations were changed.

[erik-3milabs]

solid outline.

[RobinJadoul]

/ai-review

[github-actions]

AI Review

PR #642 · 24 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[github-actions]

Codex Code Review

Findings

• High spec/src/commit.toml: commit_value_out and commit_value_in use the exact same memory tuple with opposite multiplicities at timestamp 0. These cancel inside the same LogUp contribution, so they do not force the committed byte to match any verifier-initialized claimed commitment. This undermines the new public-commitment check described in spec/commit.typ. Use a non-cancelling read/write chain, a verifier-backed lookup table, or otherwise ensure the commitment-domain token must be supplied by global initialization/finalization rather than self-cancelled by the COMMIT chip.

• Medium spec/src/config.toml: Timestamp is now a 32-bit Word, and spec/streaming.typ only says an epoch “should not” exceed 2^30 cycles. If the verifier does not enforce this as a hard bound on CPU rows per epoch, the preprocessed CPU timestamp 4 * (i + 1) can exceed 32 bits and collide/wrap in the epoch-local memory argument. That can break temporal uniqueness for memory accesses. The spec should make this a required verifier check.

• Low spec/memory.typ: the domain list says committed values use domain separator 2, but the new COMMIT constraints and prose use domain 3 (spec/src/commit.toml, spec/commit.typ). This is an easy integration trap for verifier/global-memory initialization. Pick one value and make the spec consistent.

I did not run builds or tests, per the review constraints.

[claude]

Stale description: subtypes is now Word, but the desc still says "holding timestamps as DWordWL". Update the text to Word so it matches the type (this PR moves all timestamps to single-limb Word).

[claude]

Spec review — epoch system

Reviewed the diff (Typst + TOML chip definitions). This is a well-structured formalization of the epoch-based proving system. The move to single-limb Word timestamps looks internally consistent across the chips (MEMW/MEMW_A/MEMW_R ALU wrapping, CPU/HALT pc-timestamp constraints, signatures). The L2G local↔global bridging and its padding scheme (fini_value = init_value, fini_timestamp = 0) are sound, and the IS_B20[fini_epoch - init_epoch - 1] check correctly enforces strictly-increasing epochs.

A few consistency issues, none blocking:

Medium

• Domain separator mismatch (2 vs 3). memory.typ lists Committed values: 2, but the COMMIT chip uses domain 3 (commit.typ text and commit.toml input = [3, ...]). Domain 2 is declared but unused; domain 3 (used) is undocumented. See inline comment.

Low

• config.toml: the Timestamp desc still says "as DWordWL" after the subtype changed to Word. See inline.
• streaming.typ: typos — "each epoch proceeds by commiting" → committing; "interactions that are pare of the global memory consistency proof" → part.

Nit / question

• cpu.toml cpu:c:consume_pc: the new expr is ["+", ["-", "timestamp", ["*", 3, ["not", "pc_double_read"]]]] — a single-argument + wrapping the subtraction. Sibling constraints use the two-arg form (e.g. ["+", "timestamp", 1]). If the unary + is just a leftover from removing the limb array, consider dropping it for clarity.

Note: I could not build the Typst (blocked/no network), so the new @memory:aside:granularity and @streaming cross-references and load_chip("src/l2g.toml") rendering weren't verified to compile — worth confirming CI renders the book.

[cdesaintguilhem]

The big changes look good to me. I notice the text still mentions 3 for the domain separator value for commitment values whereas other parts use 2. Also, I spotted a typo.