Skip to content

refactor(prover): bind the proven statement into the Fiat-Shamir transcript#610

Open
diegokingston wants to merge 2 commits into
mainfrom
harden/fiat-shamir-statement-binding
Open

refactor(prover): bind the proven statement into the Fiat-Shamir transcript#610
diegokingston wants to merge 2 commits into
mainfrom
harden/fiat-shamir-statement-binding

Conversation

@diegokingston
Copy link
Copy Markdown
Collaborator

Summary

The VM prover and verifier built their Fiat-Shamir transcript with
DefaultTranscript::new(&[])empty. The statement being proven (the
program, 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_counts cross-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

  • New prover/src/statement.rs: a canonical, versioned, length-prefixed,
    domain-tagged encoder that digests the full statement — ELF hash, public
    output, all table_counts fields, and page layout — into a 32-byte
    statement_seed.
  • Seeds the transcript with it at all three construction sites that must
    agree: the prove path, the verify path, and the bus-balance replay
    (replay_transcript_phase_a). For an honest proof every site derives
    identical challenges; any tampered statement field makes the verifier's seed
    diverge and verification rejects.
  • tiny-keccak is promoted from a dev-dependency to a dependency (already in
    the 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.
  • No regressions: full prover lib suite is 281 passed / 78 failed vs a
    baseline 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 the
    authoring environment
    — no RISC-V toolchain, and the checked-in asm
    fixtures are stale (sub.elf uses a removed syscall, which already breaks
    several pre-existing e2e tests). Please confirm this test passes in CI.

…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.
@diegokingston diegokingston force-pushed the harden/fiat-shamir-statement-binding branch from 08ec002 to 0ce7bac Compare May 22, 2026 14:43
@MauroToscano
Copy link
Copy Markdown
Contributor

I streamlined it here: #61

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants