spec: Draft streaming prover approaches

[RobinJadoul]

The goal of this PR is to have a central place to discuss these options, so that we can potentially compare some implementation-based data and decide on which tradeoffs to go for.
The long-term goal is to pick a single approach and work that out properly in its own PR.

[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.