refactor(prover): bind the proven statement into the Fiat-Shamir transcript#610
Open
diegokingston wants to merge 2 commits into
Open
refactor(prover): bind the proven statement into the Fiat-Shamir transcript#610diegokingston wants to merge 2 commits into
diegokingston wants to merge 2 commits into
Conversation
…script The VM prover and verifier built their transcript with `new(&[])` — the statement (program, public output, table layout) was never absorbed, so Fiat-Shamir challenges did not depend on it. Soundness was preserved only by out-of-band reconstruction checks in the verifier. Add a canonical, versioned, length-prefixed encoder (`prover/src/statement.rs`) that digests the full statement — ELF hash, public output, table counts, and page layout — into a 32-byte transcript seed. Seed the transcript with it on the prove path, the verify path, and the bus-balance replay (`replay_transcript_phase_a`), so all three derive identical challenges for an honest proof and diverge for any tampered statement. Closes the frozen-heart class of issue as defense-in-depth and is a prerequisite for recursion. Breaking proof-format change (challenges differ). `tiny-keccak` is promoted from a dev-dependency to a dependency for the statement digest.
08ec002 to
0ce7bac
Compare
Contributor
|
I streamlined it here: #61 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The VM prover and verifier built their Fiat-Shamir transcript with
DefaultTranscript::new(&[])— empty. The statement being proven (theprogram, its public output, the table layout) was never absorbed, so the
verifier's challenges did not depend on it. Soundness was preserved only by
out-of-band reconstruction checks in the verifier (recomputed preprocessed
commitments, recomputed
expected_bus_balance,table_countscross-check).This binds the statement directly into the transcript, so soundness no longer
depends on the completeness of that set of checks.
What it does
prover/src/statement.rs: a canonical, versioned, length-prefixed,domain-tagged encoder that digests the full statement — ELF hash, public
output, all
table_countsfields, and page layout — into a 32-bytestatement_seed.agree: the prove path, the verify path, and the bus-balance replay
(
replay_transcript_phase_a). For an honest proof every site derivesidentical challenges; any tampered statement field makes the verifier's seed
diverge and verification rejects.
tiny-keccakis promoted from a dev-dependency to a dependency (already inthe lockfile) for the statement digest.
Severity
This is hardening / defense-in-depth, not a patch for a live forgery — the
statement is currently bound out-of-band. The value is making the soundness
argument local and self-evident, and it is a prerequisite for recursion (a
recursive verifier derives challenges purely from the transcript). Peer systems
(Plonky3, SP1, ZisK) all bind the statement into the transcript.
Breaking proof-format change: challenges differ, so old proofs will not verify.
Test plan
prover/src/tests/statement_tests.rs— 8 encoder unit tests (determinism,per-field distinctness, domain tag, length-prefix boundary collision). All pass.
proverlib suite is 281 passed / 78 failed vs abaseline of 273 / 77 — i.e. +8 passing (the new encoder tests) and
+1 failing, which is the new e2e test below.
proof_binds_the_program_it_was_generated_for(e2e: honest roundtrip+ wrong-program rejection; this is what actually exercises seed
consistency across the three sites). It needs the compiled program
artifacts (
make compile-programs-rust). It could not be run in theauthoring environment — no RISC-V toolchain, and the checked-in asm
fixtures are stale (
sub.elfuses a removed syscall, which already breaksseveral pre-existing e2e tests). Please confirm this test passes in CI.