Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions prover/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ serde = { version = "1.0", features = ["derive"] }
rayon = { version = "1.8.0", optional = true }
sysinfo = { version = "0.31", default-features = false, features = ["system"] }
log = "0.4"
sha3 = { version = "0.10.8", default-features = false }

[dev-dependencies]
env_logger = "*"
Expand Down
54 changes: 44 additions & 10 deletions prover/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ pub mod constraints;
mod debug_report;
#[cfg(feature = "instruments")]
pub mod instruments;
mod statement;
pub mod tables;
pub mod test_utils;
#[cfg(test)]
Expand All @@ -35,6 +36,7 @@ use stark::storage_mode::StorageMode;
use stark::traits::AIR;
use stark::verifier::{IsStarkVerifier, Verifier};

use crate::statement::absorb_statement;
pub use crate::tables::MaxRowsConfig;
use crate::tables::bitwise;
use crate::tables::decode;
Expand Down Expand Up @@ -445,8 +447,8 @@ impl VmAirs {
pub(crate) fn replay_transcript_phase_a(
airs: &[&dyn AIR<Field = F, FieldExtension = E, PublicInputs = ()>],
multi_proof: &MultiProof<F, E, ()>,
transcript: &mut DefaultTranscript<E>,
) -> (FieldElement<E>, FieldElement<E>) {
let mut transcript = DefaultTranscript::<E>::new(&[]);
for (air, proof) in airs.iter().zip(&multi_proof.proofs) {
if air.is_preprocessed() {
transcript.append_bytes(&air.precomputed_commitment());
Expand Down Expand Up @@ -512,8 +514,9 @@ pub(crate) fn compute_expected_commit_bus_balance(
airs: &[&dyn AIR<Field = F, FieldExtension = E, PublicInputs = ()>],
proof: &MultiProof<F, E, ()>,
public_output_bytes: &[u8],
transcript: &mut DefaultTranscript<E>,
) -> Option<FieldElement<E>> {
let (z, alpha) = replay_transcript_phase_a(airs, proof);
let (z, alpha) = replay_transcript_phase_a(airs, proof, transcript);
compute_commit_bus_offset(public_output_bytes, &z, &alpha)
}

Expand Down Expand Up @@ -652,10 +655,28 @@ pub fn prove_with_options_and_inputs(

let runtime_page_ranges = traces.runtime_page_ranges();

let num_private_input_pages = traces
.page_configs
.iter()
.filter(|c| c.is_private_input)
.count();

// Bind the full statement (program, public output, table layout) into the
// Fiat-Shamir transcript so every challenge depends on it.
let mut transcript = DefaultTranscript::<E>::new(&[]);
absorb_statement(
&mut transcript,
elf_bytes,
&traces.public_output_bytes,
&table_counts,
num_private_input_pages,
&runtime_page_ranges,
);

// Phase 4: Prove (multi_prove)
let proof = Prover::multi_prove(
airs.air_trace_pairs(&mut traces),
&mut DefaultTranscript::<E>::new(&[]),
&mut transcript,
#[cfg(feature = "disk-spill")]
storage_mode,
)
Expand All @@ -677,12 +698,6 @@ pub fn prove_with_options_and_inputs(
);
}

let num_private_input_pages = traces
.page_configs
.iter()
.filter(|c| c.is_private_input)
.count();

Ok(VmProof {
proof,
runtime_page_ranges,
Expand Down Expand Up @@ -765,10 +780,29 @@ pub fn verify_with_options(
// If public_output was tampered, the recomputed offset won't match the
// actual bus total in the proof, and multi_verify will reject.
let air_refs = airs.air_refs();

// Bind the statement into the verifier's transcript. A tampered statement
// field makes this diverge from the prover's transcript state, so every
// derived challenge differs and verification rejects.
let mut transcript = DefaultTranscript::<E>::new(&[]);
absorb_statement(
&mut transcript,
elf_bytes,
&vm_proof.public_output,
&vm_proof.table_counts,
vm_proof.num_private_input_pages,
&vm_proof.runtime_page_ranges,
);

// Fork the post-absorb state: the replay helper advances through Phase A
// independently of the multi_verify transcript, but both must start from
// the same statement-bound state.
let mut transcript_for_replay = transcript.clone();
let expected_bus_balance = match compute_expected_commit_bus_balance(
&air_refs,
&vm_proof.proof,
&vm_proof.public_output,
&mut transcript_for_replay,
) {
Some(balance) => balance,
None => return Ok(false),
Expand All @@ -777,7 +811,7 @@ pub fn verify_with_options(
Ok(Verifier::multi_verify(
&air_refs,
&vm_proof.proof,
&mut DefaultTranscript::<E>::new(&[]),
&mut transcript,
&expected_bus_balance,
))
}
Expand Down
85 changes: 85 additions & 0 deletions prover/src/statement.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
//! Statement absorbed into the Fiat-Shamir transcript before Phase A.
//!
//! Streams a canonical, domain-separated, length-prefixed encoding directly
//! into the transcript. The transcript is itself a Keccak256 absorber
//! (`DefaultTranscript`), so a single hash suffices — no external digest
//! needed beyond the ELF.
//!
//! All three call sites (prove, verify, bus-balance replay) must absorb
//! identical bytes; any divergence makes every derived challenge differ and
//! verification reject.

use crypto::fiat_shamir::is_transcript::IsTranscript;
use sha3::{Digest, Keccak256};

use crate::test_utils::E;
use crate::{RuntimePageRange, TableCounts};

/// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change.
const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V1";

fn elf_digest(elf: &[u8]) -> [u8; 32] {
let mut h = Keccak256::new();
h.update(elf);
h.finalize().into()
}

pub(crate) fn absorb_statement(
t: &mut impl IsTranscript<E>,
elf_bytes: &[u8],
public_output: &[u8],
table_counts: &TableCounts,
num_private_input_pages: usize,
runtime_page_ranges: &[RuntimePageRange],
) {
t.append_bytes(DOMAIN_TAG);

// ELF: fixed 32-byte digest — no length prefix needed.
t.append_bytes(&elf_digest(elf_bytes));

// public_output: variable length → length-prefix to prevent boundary collisions.
t.append_bytes(&(public_output.len() as u64).to_le_bytes());
t.append_bytes(public_output);

// table_counts: fixed-width u64s in declared order. The exhaustive
// destructure makes any field added to TableCounts a compile error here —
// that's the signal to extend the loop below and bump DOMAIN_TAG.
let &TableCounts {
cpu,
lt,
memw,
memw_aligned,
load,
mul,
dvrm,
shift,
branch,
memw_register,
} = table_counts;
for count in [
cpu,
lt,
memw,
memw_aligned,
load,
mul,
dvrm,
shift,
branch,
memw_register,
] {
t.append_bytes(&(count as u64).to_le_bytes());
}

t.append_bytes(&(num_private_input_pages as u64).to_le_bytes());

// runtime_page_ranges: count-prefixed; each entry fixed width.
Comment thread
MauroToscano marked this conversation as resolved.
t.append_bytes(&(runtime_page_ranges.len() as u64).to_le_bytes());
for r in runtime_page_ranges {
// Exhaustive destructure: any field added to RuntimePageRange becomes
// a compile error here.
let &RuntimePageRange { base, count } = r;
t.append_bytes(&base.to_le_bytes());
t.append_bytes(&count.to_le_bytes());
}
}
2 changes: 2 additions & 0 deletions prover/src/tests/decode_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1064,10 +1064,12 @@ fn test_decode_soundness_same_elf_accepted() {
&table_counts,
);
let verifier_air_refs = verifier_airs.air_refs();
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&verifier_air_refs,
&proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down
2 changes: 2 additions & 0 deletions prover/src/tests/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,6 @@ pub mod mul_tests;
#[cfg(test)]
pub mod prove_elfs_tests;
#[cfg(test)]
pub mod statement_tests;
#[cfg(test)]
pub mod trace_builder_tests;
10 changes: 10 additions & 0 deletions prover/src/tests/prove_elfs_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,10 +67,12 @@ fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool {
};

// Compute the verifier-side expected COMMIT bus balance from public output bytes
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&airs.air_refs(),
&multi_proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down Expand Up @@ -881,10 +883,12 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() {
let verifier_airs =
crate::VmAirs::new(&elf, &proof_options, true, &wrong_configs, &table_counts);
let verifier_air_refs = verifier_airs.air_refs();
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&verifier_air_refs,
&proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down Expand Up @@ -1617,10 +1621,12 @@ fn test_deep_stack_runtime_pages_roundtrip() {
let verifier_airs =
crate::VmAirs::new(&elf, &proof_options, true, &verifier_configs, &table_counts);
let verifier_air_refs = verifier_airs.air_refs();
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&verifier_air_refs,
&proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down Expand Up @@ -1672,10 +1678,12 @@ fn test_deep_stack_missing_pages_rejected() {
let verifier_airs =
crate::VmAirs::new(&elf, &proof_options, true, &wrong_configs, &table_counts);
let verifier_air_refs = verifier_airs.air_refs();
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&verifier_air_refs,
&proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down Expand Up @@ -1762,10 +1770,12 @@ fn test_heap_alloc_runtime_pages_roundtrip() {
let verifier_airs =
crate::VmAirs::new(&elf, &proof_options, true, &verifier_configs, &table_counts);
let verifier_air_refs = verifier_airs.air_refs();
let mut replay_transcript = DefaultTranscript::<E>::new(&[]);
let expected_bus_balance = crate::compute_expected_commit_bus_balance(
&verifier_air_refs,
&proof,
&traces.public_output_bytes,
&mut replay_transcript,
)
.expect("fingerprint collision in test");

Expand Down
Loading
Loading