From 2c7e2e1661ec5dc7cfa96a1319ed5da7c35bd2e9 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 10:04:35 +0900 Subject: [PATCH 01/11] test(halo2_ivc): add public-input failure-signature helper --- .../tests/common/failure_signature.rs | 306 ++++++++++++++++++ .../circuits/halo2_ivc/tests/common/mod.rs | 2 + .../tests/common/public_input_layout.rs | 197 +++++++++++ 3 files changed, 505 insertions(+) create mode 100644 mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs create mode 100644 mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs new file mode 100644 index 00000000000..c62b31df88d --- /dev/null +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -0,0 +1,306 @@ +//! Classifies `MockProver` failures by the public-statement rows they implicate. +//! +//! A negative test that asserts only `verify().is_err()` can pass for the wrong reason. The +//! recursive circuit binds every element of its public statement with a copy constraint, so a +//! tampered element surfaces as a [`VerifyFailure::Permutation`] on the public-statement instance +//! column at that element's row. Asserting the exact set of those rows turns "something failed" +//! into "these public inputs, and only these, stopped being satisfiable". +//! +//! The contract is deliberately two-sided: an **exact** public-statement row signature, plus a +//! **permitted failure class** for everything else. The advice-side halves of a broken copy +//! constraint, and the message-preimage equality, are also permutation failures, but the columns +//! and regions they name belong to the gadget layer and carry no stability guarantee — so they are +//! constrained by class and not enumerated. + +use std::collections::{BTreeMap, BTreeSet}; + +use ff::Field; +use midnight_proofs::{ + dev::{FailureLocation, MockProver, VerifyFailure}, + plonk::{Any, Circuit}, +}; + +use crate::circuits::halo2_ivc::{NativeField, circuit::IvcCircuitData}; + +/// Index of the instance column carrying the circuit's public statement. +/// +/// The recursive circuit declares the committed-instance column first and leaves it empty, so the +/// public statement lands in the second column. Filtering on this index is what keeps a failure in +/// the committed column from being mistaken for a public-statement failure. +pub(crate) const PUBLIC_STATEMENT_INSTANCE_COLUMN: usize = 1; + +/// Mutates the public input at `row` by a guaranteed nonzero delta. +/// +/// Adding one rather than assigning a fixed value keeps the mutation effective whatever the +/// original held: assigning `ONE` is a no-op wherever the honest value already is one, as the +/// genesis step counter is. +pub(crate) fn mutate_public_input(public_inputs: &mut [NativeField], row: usize) { + public_inputs[row] += NativeField::ONE; +} + +/// True when `failure` is a permutation failure on the public-statement column. +fn is_public_statement_failure(failure: &VerifyFailure) -> bool { + matches!( + failure, + VerifyFailure::Permutation { column, .. } + if column.column_type() == Any::Instance + && column.index() == PUBLIC_STATEMENT_INSTANCE_COLUMN + ) +} + +/// Returns the public-statement row implicated by `failure`, if it implicates one. +/// +/// Public-statement cells are assigned outside any region, so their failures carry an absolute row. +fn public_statement_row(failure: &VerifyFailure) -> Option { + match failure { + VerifyFailure::Permutation { + location: FailureLocation::OutsideRegion { row }, + .. + } if is_public_statement_failure(failure) => Some(*row), + _ => None, + } +} + +/// Runs `MockProver` on any circuit, requires rejection, and asserts that the public-statement rows +/// implicated are exactly the keys of `expected_rows`. +/// +/// `expected_rows` maps each expected row to the field name reported in diagnostics; rows that fail +/// unexpectedly are reported by index, since a generic circuit has no field names to resolve them +/// against. Every returned failure must be a permutation failure, and every permutation failure on +/// the public-statement column must carry an absolute row — anything else means the circuit rejected +/// in a way this helper cannot account for, and is surfaced rather than dropped. +pub(crate) fn assert_circuit_rejects_public_input_rows>( + circuit: &C, + instances: Vec>, + expected_rows: &BTreeMap, +) { + let prover = MockProver::run(circuit, instances).expect("MockProver setup should succeed"); + let failures = prover + .verify() + .expect_err("the circuit should reject the tampered public inputs"); + + let unexpected_classes: Vec = failures + .iter() + .filter(|failure| !matches!(failure, VerifyFailure::Permutation { .. })) + .map(|failure| format!("{failure:?}")) + .collect(); + assert!( + unexpected_classes.is_empty(), + "every failure should be a permutation failure, since the public statement is bound by \ + copy constraints; got {} of another class:\n{}", + unexpected_classes.len(), + unexpected_classes.join("\n") + ); + + // Without this, a public-statement failure reported against a region would be dropped by + // `public_statement_row` and an empty expected signature would pass on a circuit that had in + // fact broken a public-input binding. + let unlocatable: Vec = failures + .iter() + .filter(|failure| { + is_public_statement_failure(failure) && public_statement_row(failure).is_none() + }) + .map(|failure| format!("{failure:?}")) + .collect(); + assert!( + unlocatable.is_empty(), + "every public-statement failure should carry an absolute row; got {} that did not:\n{}", + unlocatable.len(), + unlocatable.join("\n") + ); + + let observed: BTreeSet = failures.iter().filter_map(public_statement_row).collect(); + let expected: BTreeSet = expected_rows.keys().copied().collect(); + let describe = |rows: &BTreeSet| { + rows.iter() + .map(|row| match expected_rows.get(row) { + Some(name) => format!("{row} ({name})"), + None => format!("{row} (not expected to fail)"), + }) + .collect::>() + .join(", ") + }; + assert_eq!( + observed, + expected, + "public-input failure signature mismatch\n failed: [{}]\n expected: [{}]", + describe(&observed), + describe(&expected) + ); +} + +/// Recursive-circuit wrapper over [`assert_circuit_rejects_public_input_rows`]. +/// +/// The empty first column is the committed-instance column the circuit declares and never uses. +#[allow(dead_code)] +pub(crate) fn assert_recursive_mock_prover_rejects_public_input_rows( + ivc_circuit_data: IvcCircuitData, + public_inputs: Vec, + expected_rows: &BTreeMap, +) { + assert_circuit_rejects_public_input_rows( + &ivc_circuit_data, + vec![vec![], public_inputs], + expected_rows, + ); +} + +#[cfg(test)] +mod tests { + use midnight_proofs::{ + circuit::{Layouter, SimpleFloorPlanner, Value}, + plonk::{Advice, Column, ConstraintSystem, Error, Instance}, + }; + + use super::*; + + /// Advice values assigned by the minimal circuit. The third is bound to the committed column. + const MINIMAL_CIRCUIT_VALUES: [u64; 3] = [10, 20, 30]; + + /// Public-statement row left deliberately unbound by the minimal circuit. + const UNBOUND_PUBLIC_STATEMENT_ROW: usize = 2; + + #[derive(Clone)] + struct MinimalConfig { + advice: Column, + committed_instance: Column, + public_statement_instance: Column, + } + + /// Smallest circuit that reproduces the two-instance-column shape of the recursive circuit. + /// + /// Two of its public-statement inputs are bound by copy constraints, one is left unbound, and a + /// third cell is bound to the committed column. That is exactly the discrimination the helper + /// claims: it must report the bound public-statement rows, and neither the unbound row nor the + /// committed-column failure. + struct MinimalCircuit; + + impl Circuit for MinimalCircuit { + type Config = MinimalConfig; + type FloorPlanner = SimpleFloorPlanner; + type Params = (); + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let advice = meta.advice_column(); + // Declaration order mirrors the recursive circuit: committed column first. + let committed_instance = meta.instance_column(); + let public_statement_instance = meta.instance_column(); + meta.enable_equality(advice); + meta.enable_equality(committed_instance); + meta.enable_equality(public_statement_instance); + MinimalConfig { + advice, + committed_instance, + public_statement_instance, + } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let cells = layouter.assign_region( + || "values", + |mut region| { + let mut assigned = Vec::with_capacity(MINIMAL_CIRCUIT_VALUES.len()); + for (offset, value) in MINIMAL_CIRCUIT_VALUES.iter().enumerate() { + assigned.push(region.assign_advice( + || "value", + config.advice, + offset, + || Value::known(NativeField::from(*value)), + )?); + } + Ok(assigned) + }, + )?; + layouter.constrain_instance(cells[0].cell(), config.public_statement_instance, 0)?; + layouter.constrain_instance(cells[1].cell(), config.public_statement_instance, 1)?; + layouter.constrain_instance(cells[2].cell(), config.committed_instance, 0) + } + } + + /// `[committed, public statement]` instances satisfying the minimal circuit. + fn honest_minimal_instances() -> Vec> { + vec![ + vec![NativeField::from(MINIMAL_CIRCUIT_VALUES[2])], + vec![ + NativeField::from(MINIMAL_CIRCUIT_VALUES[0]), + NativeField::from(MINIMAL_CIRCUIT_VALUES[1]), + // Unbound row: any value satisfies the circuit. + NativeField::from(777u64), + ], + ] + } + + #[test] + fn minimal_circuit_accepts_honest_instances() { + // Canary: without it, a helper that always found failures would look correct. + let prover = MockProver::run(&MinimalCircuit, honest_minimal_instances()) + .expect("MockProver setup should succeed"); + prover + .verify() + .expect("the minimal circuit should accept its honest instances"); + } + + #[test] + fn helper_reports_bound_public_statement_rows_only() { + let mut instances = honest_minimal_instances(); + // Tamper every kind of row at once: both bound public-statement rows, the unbound one, and + // the committed column. Only the bound public-statement rows may be reported. + mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); + mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 1); + mutate_public_input( + &mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], + UNBOUND_PUBLIC_STATEMENT_ROW, + ); + mutate_public_input(&mut instances[0], 0); + + assert_circuit_rejects_public_input_rows( + &MinimalCircuit, + instances, + &BTreeMap::from([(0, "first bound input"), (1, "second bound input")]), + ); + } + + #[test] + fn helper_accepts_rejection_with_an_empty_expected_signature() { + // A rejection caused by the message-preimage equality implicates no public-statement row. + // Tampering only the committed column reproduces that shape here. + let mut instances = honest_minimal_instances(); + mutate_public_input(&mut instances[0], 0); + + assert_circuit_rejects_public_input_rows(&MinimalCircuit, instances, &BTreeMap::new()); + } + + #[test] + #[should_panic(expected = "public-input failure signature mismatch")] + fn helper_rejects_an_incomplete_expected_signature() { + // Proves the assertion has teeth: two rows fail, so expecting one must not pass. + let mut instances = honest_minimal_instances(); + mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); + mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 1); + + assert_circuit_rejects_public_input_rows( + &MinimalCircuit, + instances, + &BTreeMap::from([(0, "first bound input")]), + ); + } + + #[test] + #[should_panic(expected = "public-input failure signature mismatch")] + fn helper_rejects_an_empty_signature_when_a_row_did_fail() { + // The counterpart to the empty-signature case above: an empty expectation must not absorb a + // real public-statement failure. + let mut instances = honest_minimal_instances(); + mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); + + assert_circuit_rejects_public_input_rows(&MinimalCircuit, instances, &BTreeMap::new()); + } +} diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/mod.rs index ac182454c67..1c2921ce50e 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/mod.rs @@ -12,6 +12,8 @@ pub(crate) const CERTIFICATE_CIRCUIT_DEGREE: u32 = 13; const _: () = assert!(ASSET_SEED == crate::circuits::trusted_setup::UNSAFE_SRS_SEED); pub(crate) mod asset_readers; +pub(crate) mod failure_signature; pub(crate) mod field_encoding; pub(crate) mod generators; pub(crate) mod helpers; +pub(crate) mod public_input_layout; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs new file mode 100644 index 00000000000..f943dcc66dc --- /dev/null +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -0,0 +1,197 @@ +//! Row indices of the recursive circuit's public statement. +//! +//! The circuit lays out its statement through a single shared offset counter: the global +//! root-of-trust first, then the next state, then the accumulator. Tests build the same vector as +//! `[global, state, accumulator].concat()`, so a row index here is an index into that vector and +//! into the public-statement instance column alike. +//! +//! Keeping the mapping in one place is what lets a failure-signature assertion name the field that +//! broke instead of a bare integer, and it keeps row literals out of the test bodies. + +/// Rows occupied by the global root-of-trust section. +pub(crate) const GLOBAL_SECTION_ROWS: usize = 5; + +/// Rows occupied by the next-state section. +pub(crate) const STATE_SECTION_ROWS: usize = 7; + +/// A field of the global root-of-trust section, in the order the circuit constrains it. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) enum GlobalField { + GenesisMessage, + GenesisVerificationKeyX, + GenesisVerificationKeyY, + CertificateCircuitVerificationKeyRepresentation, + IvcCircuitVerificationKeyRepresentation, +} + +impl GlobalField { + /// Every global field, in layout order. + pub(crate) const ALL: [Self; GLOBAL_SECTION_ROWS] = [ + Self::GenesisMessage, + Self::GenesisVerificationKeyX, + Self::GenesisVerificationKeyY, + Self::CertificateCircuitVerificationKeyRepresentation, + Self::IvcCircuitVerificationKeyRepresentation, + ]; + + /// Row of this field in the public statement. + pub(crate) fn row(self) -> usize { + self as usize + } + + /// Name used in failure diagnostics. + pub(crate) fn name(self) -> &'static str { + match self { + Self::GenesisMessage => "global.genesis_message", + Self::GenesisVerificationKeyX => "global.genesis_verification_key.x", + Self::GenesisVerificationKeyY => "global.genesis_verification_key.y", + Self::CertificateCircuitVerificationKeyRepresentation => { + "global.certificate_circuit_verification_key_representation" + } + Self::IvcCircuitVerificationKeyRepresentation => { + "global.ivc_circuit_verification_key_representation" + } + } + } +} + +/// A field of the next-state section, in the order the circuit constrains it. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) enum StateField { + StepCounter, + Message, + MerkleTreeCommitment, + NextMerkleTreeCommitment, + ProtocolParameters, + NextProtocolParameters, + CurrentEpoch, +} + +impl StateField { + /// Every state field, in layout order. + pub(crate) const ALL: [Self; STATE_SECTION_ROWS] = [ + Self::StepCounter, + Self::Message, + Self::MerkleTreeCommitment, + Self::NextMerkleTreeCommitment, + Self::ProtocolParameters, + Self::NextProtocolParameters, + Self::CurrentEpoch, + ]; + + /// Row of this field in the public statement, after the global section. + pub(crate) fn row(self) -> usize { + GLOBAL_SECTION_ROWS + self as usize + } + + /// Name used in failure diagnostics. + pub(crate) fn name(self) -> &'static str { + match self { + Self::StepCounter => "state.step_counter", + Self::Message => "state.message", + Self::MerkleTreeCommitment => "state.merkle_tree_commitment", + Self::NextMerkleTreeCommitment => "state.next_merkle_tree_commitment", + Self::ProtocolParameters => "state.protocol_parameters", + Self::NextProtocolParameters => "state.next_protocol_parameters", + Self::CurrentEpoch => "state.current_epoch", + } + } +} + +/// Row of the accumulator encoding element at `offset`, after the global and state sections. +pub(crate) fn accumulator_row(offset: usize) -> usize { + GLOBAL_SECTION_ROWS + STATE_SECTION_ROWS + offset +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::circuits::halo2_ivc::{ + NativeField, + state::State, + tests::common::asset_readers::load_embedded_verification_context_asset, + types::{ + EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolParametersHash, StepCounter, + }, + }; + + #[test] + fn layout_matches_the_circuit_statement_contract() { + let verification_context = load_embedded_verification_context_asset() + .expect("verification context asset should load"); + assert_eq!( + verification_context.global_field_elements.len(), + GLOBAL_SECTION_ROWS, + "global section length changed; every expected public-input row shifts with it" + ); + assert_eq!( + State::genesis().as_public_input().len(), + STATE_SECTION_ROWS, + "state section length changed; every expected public-input row shifts with it" + ); + for (offset, field) in GlobalField::ALL.iter().enumerate() { + assert_eq!( + field.row(), + offset, + "{} is not at global row {offset}", + field.name() + ); + } + for (offset, field) in StateField::ALL.iter().enumerate() { + assert_eq!( + field.row(), + GLOBAL_SECTION_ROWS + offset, + "{} is not at state row {}", + field.name(), + GLOBAL_SECTION_ROWS + offset + ); + } + assert_eq!( + accumulator_row(0), + GLOBAL_SECTION_ROWS + STATE_SECTION_ROWS, + "the accumulator section follows the global and state sections" + ); + } + + #[test] + fn state_public_input_order_matches_the_layout() { + // Each variant is paired with its own sentinel, so a variant naming the wrong field fails + // even if the declaration order and the pairs were changed together. + const SENTINELS: [(StateField, u64); STATE_SECTION_ROWS] = [ + (StateField::StepCounter, 11), + (StateField::Message, 22), + (StateField::MerkleTreeCommitment, 33), + (StateField::NextMerkleTreeCommitment, 44), + (StateField::ProtocolParameters, 55), + (StateField::NextProtocolParameters, 66), + (StateField::CurrentEpoch, 77), + ]; + + assert_eq!( + SENTINELS.map(|(field, _)| field), + StateField::ALL, + "every state field needs its own sentinel, so a new field cannot go untested" + ); + + let state = State::new( + StepCounter::from_field(NativeField::from(11u64)), + MessageHash::from_field(NativeField::from(22u64)), + MerkleTreeCommitment::from_field(NativeField::from(33u64)), + MerkleTreeCommitment::from_field(NativeField::from(44u64)), + ProtocolParametersHash::from_field(NativeField::from(55u64)), + ProtocolParametersHash::from_field(NativeField::from(66u64)), + EpochNumber::from_field(NativeField::from(77u64)), + ); + let public_input = state.as_public_input(); + + for (field, sentinel) in SENTINELS { + let offset = field.row() - GLOBAL_SECTION_ROWS; + assert_eq!( + public_input[offset], + NativeField::from(sentinel), + "{} is not at state offset {offset}", + field.name() + ); + } + } +} From 923be239011f0ae748488a5870726670d82d04ee Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 10:41:09 +0900 Subject: [PATCH 02/11] test(halo2_ivc): add satisfiable non-genesis MockProver fixtures --- .../halo2_ivc/tests/common/helpers.rs | 124 +++++++++++++++++- .../halo2_ivc/tests/golden/positive.rs | 17 +-- .../halo2_ivc/tests/transitions/positive.rs | 46 ++++++- 3 files changed, 171 insertions(+), 16 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs index 256f534dba2..ce37b39b846 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs @@ -8,12 +8,12 @@ use midnight_proofs::{ }; use crate::circuits::halo2_ivc::{ - Accumulator, AssignedAccumulator, EmulatedCurve, NativeField, PairingEngine, + Accumulator, AssignedAccumulator, EmulatedCurve, NativeField, PREIMAGE_SIZE, PairingEngine, RecursiveEmulation, accumulator::trivial_accumulator, circuit::IvcCircuitData, state::{Global, State, Witness}, - types::{CertificateProofBytes, IvcProofBytes}, + types::{CertificateProofBytes, IvcProofBytes, MerkleTreeCommitment, ProtocolMessagePreimage}, }; use crate::circuits::halo2_ivc::{IVC_FIXED_BASES_PREFIX, keys::RecursiveCircuitVerifyingKey}; use crate::circuits::{ @@ -27,8 +27,9 @@ pub(crate) use super::generators::{ }; use super::{ asset_readers::{ - RecursiveChainStateAsset, load_embedded_next_epoch_step_output_asset, - load_embedded_recursive_chain_state_asset, load_embedded_verification_context_asset, + RecursiveChainStateAsset, load_embedded_following_certificate_in_epoch_asset, + load_embedded_next_epoch_step_output_asset, load_embedded_recursive_chain_state_asset, + load_embedded_verification_context_asset, }, generators::{ AssetGenerationSetup, build_recursive_fixed_bases, build_recursive_global, @@ -273,6 +274,121 @@ pub(crate) fn prepare_stored_step_certificate_accumulator( certificate_accumulator } +/// A non-genesis MockProver stimulus assembled entirely from committed step assets. +/// +/// Unlike [`build_trivial_mock_prover_circuit`], this carries the stored certificate proof, the +/// stored previous recursive proof and the stored previous accumulator, so the accumulator the +/// circuit computes is the stored next accumulator. That is what makes it satisfiable at a +/// non-genesis step, where the accumulator contributions are no longer gated to the group identity. +pub(crate) struct AssetBackedStepFixture { + /// Circuit data for the step. + pub(crate) ivc_circuit_data: IvcCircuitData, + /// Public statement the step is expected to satisfy. + pub(crate) public_inputs: Vec, +} + +/// The stored half of one recursive step, plus the commitment its certificate was produced against. +/// +/// That commitment is not read from the step-output asset but chosen by transition type: a +/// same-epoch certificate is produced against the checkpoint's current Merkle-tree commitment, a +/// next-epoch one against its next commitment. The stored final recursive proof is deliberately +/// absent — MockProver checks the step's constraints and never verifies the step's own output. +struct StepFixtureData { + certificate_merkle_tree_commitment: MerkleTreeCommitment, + certificate_proof: CertificateProofBytes, + message_preimage: [u8; PREIMAGE_SIZE], + next_state: State, + next_accumulator: Accumulator, +} + +/// Assembles a non-genesis fixture from a stored chain checkpoint and a stored step output. +fn build_asset_backed_step_fixture( + mock_prover_setup: &MockProverSetup, + recursive_chain_state: RecursiveChainStateAsset, + stored: StepFixtureData, +) -> AssetBackedStepFixture { + let RecursiveChainStateAsset { + global_field_elements, + state, + ivc_proof, + accumulator, + genesis_signature, + } = recursive_chain_state; + + // Turns a future drift between the reconstructed global and the stored one into a direct + // coherence error instead of an opaque constraint failure. + assert_eq!( + mock_prover_setup.global.as_public_input(), + global_field_elements, + "the reconstructed global should match the one the stored checkpoint was proved against" + ); + + let witness = Witness::new( + genesis_signature, + stored.next_state.message, + stored.certificate_merkle_tree_commitment, + ProtocolMessagePreimage::new(stored.message_preimage), + ); + let public_inputs = [ + mock_prover_setup.global.as_public_input(), + stored.next_state.as_public_input(), + AssignedAccumulator::as_public_input(&stored.next_accumulator), + ] + .concat(); + let ivc_circuit_data = IvcCircuitData::try_new( + mock_prover_setup.global.clone(), + state, + witness, + stored.certificate_proof, + ivc_proof, + accumulator, + &mock_prover_setup.certificate_verifying_key, + &mock_prover_setup.recursive_verifying_key, + ) + .expect("valid IvcCircuitData construction"); + + AssetBackedStepFixture { + ivc_circuit_data, + public_inputs, + } +} + +/// Builds the satisfiable same-epoch fixture from the committed assets. +pub(crate) fn build_asset_backed_same_epoch_fixture( + mock_prover_setup: &MockProverSetup, +) -> AssetBackedStepFixture { + let recursive_chain_state = load_embedded_recursive_chain_state_asset() + .expect("recursive chain state asset should load"); + let step_output = load_embedded_following_certificate_in_epoch_asset() + .expect("following certificate in epoch asset should load"); + let stored = StepFixtureData { + certificate_merkle_tree_commitment: recursive_chain_state.state.merkle_tree_commitment, + certificate_proof: step_output.certificate_proof, + message_preimage: step_output.message_preimage, + next_state: step_output.next_state, + next_accumulator: step_output.next_accumulator, + }; + build_asset_backed_step_fixture(mock_prover_setup, recursive_chain_state, stored) +} + +/// Builds the satisfiable next-epoch fixture from the committed assets. +pub(crate) fn build_asset_backed_next_epoch_fixture( + mock_prover_setup: &MockProverSetup, +) -> AssetBackedStepFixture { + let recursive_chain_state = load_embedded_recursive_chain_state_asset() + .expect("recursive chain state asset should load"); + let step_output = load_embedded_next_epoch_step_output_asset() + .expect("recursive step output asset should load"); + let stored = StepFixtureData { + certificate_merkle_tree_commitment: recursive_chain_state.state.next_merkle_tree_commitment, + certificate_proof: step_output.certificate_proof, + message_preimage: step_output.message_preimage, + next_state: step_output.next_state, + next_accumulator: step_output.next_accumulator, + }; + build_asset_backed_step_fixture(mock_prover_setup, recursive_chain_state, stored) +} + /// Builds an `IvcCircuitData` with empty proof slots and a trivial accumulator for /// MockProver-based constraint checks. /// diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs b/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs index 4a40ef2d187..ab4c53096dd 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs @@ -1,10 +1,9 @@ //! Positive golden tests for the recursive Halo2 IVC flow. //! -//! Fast tests verify stored proof artifacts against the full verifier. The slow -//! `MockProver` check covers the genesis base case in-circuit (the unique code path -//! that has no stored proof to verify against). Same-epoch and next-epoch positive -//! constraint coverage is provided by the stored-asset verification tests above, -//! which use the full prover output: a valid proof implies all constraints hold. +//! Fast tests verify stored proof artifacts against the full verifier, and the slow `MockProver` +//! check covers the genesis base case in-circuit — the unique code path with no stored proof to +//! verify against. In-circuit positive coverage of the same-epoch and next-epoch contexts lives in +//! `transitions::positive::slow`. use midnight_circuits::types::Instantiable; use sha2::{Digest, Sha256}; @@ -147,12 +146,8 @@ mod slow { #[test] fn genesis_base_case_circuit_is_accepted() { - // MockProver constraint check for the genesis base case: no previous proof, - // trivial accumulator, all accumulator contributions gated to the group identity. - // Same-epoch and next-epoch positive constraint coverage is provided by - // `recursive_chain_state_asset_proof_and_accumulator_are_valid` and - // `recursive_step_output_asset_proof_and_accumulator_are_valid` above — a valid - // full proof implies all constraints held when the proof was generated. + // MockProver constraint check for the genesis base case: no previous proof, trivial + // accumulator, all accumulator contributions gated to the group identity. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs index 5258e07be1d..da996498b7f 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs @@ -1,4 +1,8 @@ -//! Positive transition tests: stored proofs verified against correct public inputs. +//! Positive transition tests. +//! +//! Fast tests verify the stored output proof of each transition context against the full verifier. +//! The slow `MockProver` checks in `slow` synthesize the current circuit over the stored inputs and +//! assert it accepts the stored expected output, which the stored proof alone cannot establish. use midnight_circuits::types::Instantiable; @@ -78,3 +82,43 @@ fn next_epoch_step_proof_verifies() { "next-epoch step proof should verify against the correct public inputs", ); } + +mod slow { + use crate::circuits::halo2_ivc::tests::common::{ + generators::build_asset_generation_setup_from_cache, + helpers::{ + assert_recursive_mock_prover_accepts_with_label, build_asset_backed_next_epoch_fixture, + build_asset_backed_same_epoch_fixture, build_mock_prover_setup_from_assets, + }, + }; + + #[test] + fn same_epoch_step_circuit_is_accepted() { + // Satisfiable canary for the same-epoch context: outside genesis the accumulator + // contributions are no longer gated away, so only a stored step whose accumulator the + // circuit can reproduce is accepted. + let setup = build_asset_generation_setup_from_cache(); + let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); + let fixture = build_asset_backed_same_epoch_fixture(&mock_prover_setup); + + assert_recursive_mock_prover_accepts_with_label( + fixture.ivc_circuit_data, + fixture.public_inputs, + "same-epoch step from committed assets", + ); + } + + #[test] + fn next_epoch_step_circuit_is_accepted() { + // Satisfiable canary for the next-epoch context. + let setup = build_asset_generation_setup_from_cache(); + let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); + let fixture = build_asset_backed_next_epoch_fixture(&mock_prover_setup); + + assert_recursive_mock_prover_accepts_with_label( + fixture.ivc_circuit_data, + fixture.public_inputs, + "next-epoch step from committed assets", + ); + } +} From 689f047b942ce131fadb7dde2dc279c6204fc51c Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 10:54:00 +0900 Subject: [PATCH 03/11] test(halo2_ivc): consolidate public-statement binding cases per transition context --- .../tests/common/failure_signature.rs | 1 - .../halo2_ivc/tests/common/generators/mod.rs | 1 - .../halo2_ivc/tests/common/helpers.rs | 26 ++-- .../tests/common/public_input_layout.rs | 18 +++ .../halo2_ivc/tests/encoding/negative.rs | 19 +-- .../halo2_ivc/tests/golden/positive.rs | 15 +- .../halo2_ivc/tests/in_circuit/mod.rs | 2 - .../tests/in_circuit/public_inputs.rs | 85 +---------- .../tests/in_circuit/state_transition.rs | 134 ------------------ .../tests/transitions/negative/genesis.rs | 79 ++++++----- .../tests/transitions/negative/next_epoch.rs | 130 +++-------------- .../tests/transitions/negative/same_epoch.rs | 134 +++--------------- 12 files changed, 148 insertions(+), 496 deletions(-) delete mode 100644 mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/state_transition.rs diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index c62b31df88d..17fcfbcaae4 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -132,7 +132,6 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( /// Recursive-circuit wrapper over [`assert_circuit_rejects_public_input_rows`]. /// /// The empty first column is the committed-instance column the circuit declares and never uses. -#[allow(dead_code)] pub(crate) fn assert_recursive_mock_prover_rejects_public_input_rows( ivc_circuit_data: IvcCircuitData, public_inputs: Vec, diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/generators/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/generators/mod.rs index 53d3eb74597..d49843dbd65 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/generators/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/generators/mod.rs @@ -18,6 +18,5 @@ pub(crate) use transitions::{ build_genesis_base_case_next_state, build_genesis_base_case_witness, build_genesis_protocol_message_preimage, build_same_epoch_certificate_asset_data, certificate_public_inputs_for_step, next_message_and_preimage_for_step, next_state_for_step, - same_epoch_message_and_preimage_for_step, same_epoch_next_state_for_step, }; pub(crate) use verification_key::golden_recursive_circuit_verification_key_bytes; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs index ce37b39b846..ecff95e5953 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs @@ -276,7 +276,7 @@ pub(crate) fn prepare_stored_step_certificate_accumulator( /// A non-genesis MockProver stimulus assembled entirely from committed step assets. /// -/// Unlike [`build_trivial_mock_prover_circuit`], this carries the stored certificate proof, the +/// Unlike [`build_genesis_mock_prover_circuit`], this carries the stored certificate proof, the /// stored previous recursive proof and the stored previous accumulator, so the accumulator the /// circuit computes is the stored next accumulator. That is what makes it satisfiable at a /// non-genesis step, where the accumulator contributions are no longer gated to the group identity. @@ -389,16 +389,23 @@ pub(crate) fn build_asset_backed_next_epoch_fixture( build_asset_backed_step_fixture(mock_prover_setup, recursive_chain_state, stored) } -/// Builds an `IvcCircuitData` with empty proof slots and a trivial accumulator for -/// MockProver-based constraint checks. +/// Builds an `IvcCircuitData` with empty proof slots and a trivial accumulator, for MockProver +/// constraint checks at the genesis step only. /// -/// MockProver evaluates algebraic constraints directly without running the -/// KZG prover, so embedded proof bytes are irrelevant and can be left empty. -pub(crate) fn build_trivial_mock_prover_circuit( +/// Empty proof slots work here because genesis gating scales both accumulator contributions to the +/// group identity, so the trivial input accumulator is also the expected output. At any later step +/// the contributions are live and the circuit derives an output accumulator no trivial instance can +/// match — see [`build_asset_backed_same_epoch_fixture`] for the non-genesis stimulus. +pub(crate) fn build_genesis_mock_prover_circuit( setup: &MockProverSetup, prev_state: State, witness: Witness, ) -> IvcCircuitData { + assert_eq!( + prev_state.step_counter.as_u64(), + 0, + "the trivial-accumulator stimulus is satisfiable only at genesis" + ); IvcCircuitData::try_new( setup.global.clone(), prev_state, @@ -412,8 +419,11 @@ pub(crate) fn build_trivial_mock_prover_circuit( .expect("valid IvcCircuitData construction") } -/// Builds the public-input vector for a MockProver-based negative test. -pub(crate) fn build_mock_prover_public_inputs( +/// Builds the public-input vector for a genesis MockProver stimulus. +/// +/// The accumulator section carries the trivial accumulator, which is the expected output only while +/// genesis gating scales both contributions to the group identity. +pub(crate) fn build_genesis_mock_prover_public_inputs( setup: &MockProverSetup, next_state: &State, ) -> Vec { diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs index f943dcc66dc..d232a5d5564 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -8,6 +8,8 @@ //! Keeping the mapping in one place is what lets a failure-signature assertion name the field that //! broke instead of a bare integer, and it keeps row literals out of the test bodies. +use std::collections::BTreeMap; + /// Rows occupied by the global root-of-trust section. pub(crate) const GLOBAL_SECTION_ROWS: usize = 5; @@ -103,6 +105,22 @@ pub(crate) fn accumulator_row(offset: usize) -> usize { GLOBAL_SECTION_ROWS + STATE_SECTION_ROWS + offset } +/// Row-to-name map for every global field, for use as an expected failure signature. +pub(crate) fn all_global_rows() -> BTreeMap { + GlobalField::ALL + .iter() + .map(|field| (field.row(), field.name())) + .collect() +} + +/// Row-to-name map for every state field, for use as an expected failure signature. +pub(crate) fn all_state_rows() -> BTreeMap { + StateField::ALL + .iter() + .map(|field| (field.row(), field.name())) + .collect() +} + #[cfg(test)] mod tests { use super::*; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs index 511a709153b..dd0fb50c879 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs @@ -18,8 +18,8 @@ use crate::circuits::halo2_ivc::{ build_genesis_base_case_next_state, build_genesis_base_case_witness, }, helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, + assert_recursive_mock_prover_rejects_with_label, build_genesis_mock_prover_circuit, + build_genesis_mock_prover_public_inputs, build_mock_prover_setup_from_assets, verify_prepare_blake2b_recursive_proof, }, }, @@ -201,13 +201,14 @@ mod slow { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let public_inputs = + build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); let mut witness = build_genesis_base_case_witness(&setup); witness.message_preimage.as_mut_bytes()[PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES] .fill(0xff); let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); + build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); assert_recursive_mock_prover_rejects_with_label( ivc_circuit_data, public_inputs, @@ -222,12 +223,13 @@ mod slow { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let public_inputs = + build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); let mut witness = build_genesis_base_case_witness(&setup); witness.message_preimage.as_mut_bytes()[PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES].fill(0xff); let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); + build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); assert_recursive_mock_prover_rejects_with_label( ivc_circuit_data, public_inputs, @@ -242,12 +244,13 @@ mod slow { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let public_inputs = + build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); let mut witness = build_genesis_base_case_witness(&setup); witness.message_preimage.as_mut_bytes()[PREIMAGE_CURRENT_EPOCH_BYTES].fill(0xff); let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); + build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); assert_recursive_mock_prover_rejects_with_label( ivc_circuit_data, public_inputs, diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs b/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs index ab4c53096dd..f8b384ec58e 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/golden/positive.rs @@ -2,8 +2,8 @@ //! //! Fast tests verify stored proof artifacts against the full verifier, and the slow `MockProver` //! check covers the genesis base case in-circuit — the unique code path with no stored proof to -//! verify against. In-circuit positive coverage of the same-epoch and next-epoch contexts lives in -//! `transitions::positive::slow`. +//! verify against. In-circuit positive coverage of the same-epoch and next-epoch contexts lives with +//! the positive transition tests. use midnight_circuits::types::Instantiable; use sha2::{Digest, Sha256}; @@ -20,9 +20,9 @@ use crate::circuits::halo2_ivc::tests::common::{ next_message_and_preimage_for_step, next_state_for_step, }, helpers::{ - assert_recursive_mock_prover_accepts_with_label, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_recursive_mock_prover_setup, - build_trivial_mock_prover_circuit, compute_exact_next_accumulator_from_assets, + assert_recursive_mock_prover_accepts_with_label, build_genesis_mock_prover_circuit, + build_genesis_mock_prover_public_inputs, build_mock_prover_setup_from_assets, + build_recursive_mock_prover_setup, compute_exact_next_accumulator_from_assets, verify_prepare_blake2b_recursive_proof, verify_prepare_poseidon_recursive_proof, }, }; @@ -151,12 +151,13 @@ mod slow { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let ivc_circuit_data = build_trivial_mock_prover_circuit( + let ivc_circuit_data = build_genesis_mock_prover_circuit( &mock_prover_setup, State::genesis(), build_genesis_base_case_witness(&setup), ); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let public_inputs = + build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); assert_recursive_mock_prover_accepts_with_label( ivc_circuit_data, public_inputs, diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs index 379535389a6..2bc201fefb4 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs @@ -9,11 +9,9 @@ //! `certificate_proof` — tampered certificate proof is rejected in non-genesis steps. //! `previous_ivc_proof` — tampered previous IVC proof is rejected in non-genesis steps. //! `accumulator` — tampered next_accumulator output is rejected. -//! `state_transition` — next_merkle_tree_commitment, next_protocol_parameters consistency and message hash constraint. mod accumulator; mod certificate_proof; mod genesis_gating; mod previous_ivc_proof; mod public_inputs; -mod state_transition; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs index a2d32b4a987..6a89ac21ead 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs @@ -1,24 +1,17 @@ -//! Negative public-input tests: tampered global fields and accumulator (fast CI) -//! and MockProver constraint checks (in `mod slow`). +//! Negative public-input tests: tampered global fields and accumulator, checked against the stored +//! proof by the verifier. In-circuit binding of the same elements is covered by +//! `transitions::negative::genesis::slow`. use ff::Field; use midnight_circuits::types::Instantiable; use crate::circuits::halo2_ivc::{ AssignedAccumulator, NativeField, - state::State, tests::common::{ asset_readers::{ load_embedded_genesis_step_output_asset, load_embedded_verification_context_asset, }, - generators::{ - GENESIS_EPOCH, build_asset_generation_setup_from_cache, - build_genesis_base_case_next_state, build_genesis_base_case_witness, - }, - helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_mock_prover_setup_from_assets, - build_trivial_mock_prover_circuit, verify_prepare_blake2b_recursive_proof, - }, + helpers::verify_prepare_blake2b_recursive_proof, }, }; @@ -118,73 +111,3 @@ fn next_accumulator_tampered_public_input_is_rejected() { "proof with tampered next_accumulator should be rejected by the verifier", ); } - -mod slow { - use super::*; - - #[test] - fn circuit_rejects_wrong_genesis_message_global_field() { - // MockProver constraint check: global[0] (genesis_message) set to ONE must violate - // the in-circuit constraint that pins the genesis message to the global public input. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let witness = build_genesis_base_case_witness(&setup); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - let mut global = mock_prover_setup.global.as_public_input(); - let state = next_state.as_public_input(); - let accumulator_encoding = - AssignedAccumulator::as_public_input(&mock_prover_setup.trivial_accumulator); - global[0] = NativeField::ONE; - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - [global, state, accumulator_encoding].concat(), - "global[0] (genesis_message) set to ONE", - ); - } - - #[test] - fn circuit_rejects_wrong_certificate_circuit_verification_key_representation_global_field() { - // MockProver constraint check: global[3] (certificate_circuit_verification_key_representation) set to ONE - // must violate the in-circuit constraint that pins the certificate circuit verification key representation. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let witness = build_genesis_base_case_witness(&setup); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - let mut global = mock_prover_setup.global.as_public_input(); - let state = next_state.as_public_input(); - let accumulator_encoding = - AssignedAccumulator::as_public_input(&mock_prover_setup.trivial_accumulator); - global[3] = NativeField::ONE; - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - [global, state, accumulator_encoding].concat(), - "global[3] (certificate_circuit_verification_key_representation) set to ONE", - ); - } - - #[test] - fn circuit_rejects_wrong_ivc_circuit_verification_key_representation_global_field() { - // MockProver constraint check: global[4] (ivc_circuit_verification_key_representation) set to ONE - // must violate the in-circuit constraint that pins the IVC circuit verification key representation. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let witness = build_genesis_base_case_witness(&setup); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - let mut global = mock_prover_setup.global.as_public_input(); - let state = next_state.as_public_input(); - let accumulator_encoding = - AssignedAccumulator::as_public_input(&mock_prover_setup.trivial_accumulator); - global[4] = NativeField::ONE; - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - [global, state, accumulator_encoding].concat(), - "global[4] (ivc_circuit_verification_key_representation) set to ONE", - ); - } -} diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/state_transition.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/state_transition.rs deleted file mode 100644 index 5775559e1e9..00000000000 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/state_transition.rs +++ /dev/null @@ -1,134 +0,0 @@ -//! Tests that the circuit correctly enforces constraints linking the witness, -//! current state, and next state for same-epoch transitions. -//! -//! All tests are slow MockProver checks confirming the arithmetic constraint -//! wiring for the following in-circuit invariants: -//! -//! `next_merkle_tree_commitment` consistency — must equal `prev_state.next_merkle_tree_commitment`. -//! `next_protocol_parameters` consistency — must equal `prev_state.next_protocol_parameters`. -//! `message = Blake2b(preimage)` — must equal the Blake2b hash of the message preimage. -//! -//! The `message = Blake2b(preimage)` constraint is the same gate for same-epoch and -//! next-epoch paths, so only the same-epoch witness is exercised here. - -mod slow { - use ff::Field; - - use crate::circuits::halo2_ivc::{ - NativeField, - state::Witness, - tests::common::{ - asset_readers::load_embedded_recursive_chain_state_asset, - generators::{ - build_asset_generation_setup_from_cache, same_epoch_message_and_preimage_for_step, - same_epoch_next_state_for_step, - }, - helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, - }, - }, - types::{ - MerkleTreeCommitment, MessageHash, ProtocolMessagePreimage, ProtocolParametersHash, - }, - }; - - #[test] - fn circuit_rejects_wrong_same_epoch_next_merkle_tree_commitment() { - // MockProver constraint check: next_merkle_tree_commitment set to ONE must violate the - // in-circuit constraint that pins it to prev_state.next_merkle_tree_commitment. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (same_epoch_message, same_epoch_message_preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(same_epoch_message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - same_epoch_message_preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, same_epoch_message); - tampered_state.next_merkle_tree_commitment = - MerkleTreeCommitment::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state), - "next_merkle_tree_commitment set to ONE (must equal prev_state.next_merkle_tree_commitment)", - ); - } - - #[test] - fn circuit_rejects_wrong_same_epoch_next_protocol_parameters() { - // MockProver constraint check: next_protocol_parameters set to ONE must violate the - // in-circuit constraint that pins it to prev_state.next_protocol_parameters. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (same_epoch_message, same_epoch_message_preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(same_epoch_message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - same_epoch_message_preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, same_epoch_message); - tampered_state.next_protocol_parameters = - ProtocolParametersHash::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state), - "next_protocol_parameters set to ONE (must equal prev_state.next_protocol_parameters)", - ); - } - - #[test] - fn circuit_rejects_wrong_same_epoch_msg_blake2b_constraint() { - // MockProver constraint check: message set to ONE must violate the in-circuit - // Blake2b constraint enforcing message = Blake2b(message_preimage). The same gate - // is exercised by both same-epoch and next-epoch paths, so testing it once suffices. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (same_epoch_message, same_epoch_message_preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(same_epoch_message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - same_epoch_message_preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, same_epoch_message); - tampered_state.message = MessageHash::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state), - "message set to ONE (must equal Blake2b(message_preimage))", - ); - } -} diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs index d0bd22c84cb..9f497e1ae61 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs @@ -1,18 +1,7 @@ use super::*; use crate::circuits::halo2_ivc::{ - state::State, - tests::common::{ - asset_readers::load_embedded_genesis_step_output_asset, - generators::{ - GENESIS_EPOCH, build_asset_generation_setup_from_cache, - build_genesis_base_case_next_state, build_genesis_base_case_witness, - }, - helpers::{ - assert_recursive_mock_prover_rejects, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, - }, - }, + tests::common::asset_readers::load_embedded_genesis_step_output_asset, types::{EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolParametersHash, StepCounter}, }; @@ -94,34 +83,52 @@ fn msg_tampered_is_rejected() { } mod slow { - use super::*; + use std::collections::BTreeMap; - /// Builds a genesis circuit with a tampered next state and asserts the MockProver rejects it. - /// - /// `tamper` receives the correct genesis next state before it is passed to the - /// public inputs, allowing each test to corrupt exactly the field it wants to verify. - fn assert_genesis_circuit_rejects_tampered_next_state(tamper: impl FnOnce(&mut State)) { + use crate::circuits::halo2_ivc::{ + state::State, + tests::common::{ + failure_signature::{ + assert_recursive_mock_prover_rejects_public_input_rows, mutate_public_input, + }, + generators::{ + GENESIS_EPOCH, build_asset_generation_setup_from_cache, + build_genesis_base_case_next_state, build_genesis_base_case_witness, + }, + helpers::{ + build_genesis_mock_prover_circuit, build_genesis_mock_prover_public_inputs, + build_mock_prover_setup_from_assets, + }, + public_input_layout::{all_global_rows, all_state_rows}, + }, + }; + + #[test] + fn circuit_rejects_tampered_genesis_global_and_state_public_inputs() { + // Every global and next-state element is bound to the value the circuit derives, so + // tampering all of them must break exactly their own copy constraints. One synthesis covers + // every element because MockProver reports all failures, not only the first. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); + let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); + let ivc_circuit_data = build_genesis_mock_prover_circuit( + &mock_prover_setup, + State::genesis(), + build_genesis_base_case_witness(&setup), + ); - let witness = build_genesis_base_case_witness(&setup); + let mut public_inputs = + build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let expected_rows: BTreeMap = + all_global_rows().into_iter().chain(all_state_rows()).collect(); + for row in expected_rows.keys() { + mutate_public_input(&mut public_inputs, *row); + } - let mut tampered_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - tamper(&mut tampered_state); - - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - - assert_recursive_mock_prover_rejects(ivc_circuit_data, public_inputs); - } - - #[test] - fn circuit_rejects_msg_inconsistent_with_preimage() { - // MockProver check that the in-circuit Blake2b hash constraint between - // message_preimage bytes and the resulting message field is wired correctly. - assert_genesis_circuit_rejects_tampered_next_state(|s| { - s.message = MessageHash::from_field(NativeField::ONE) - }); + assert_recursive_mock_prover_rejects_public_input_rows( + ivc_circuit_data, + public_inputs, + &expected_rows, + ); } } diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs index ca0420a3923..5fabba210e0 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs @@ -1,24 +1,8 @@ use super::*; use crate::circuits::halo2_ivc::{ - state::Witness, - tests::common::{ - asset_readers::{ - load_embedded_next_epoch_step_output_asset, load_embedded_recursive_chain_state_asset, - }, - generators::{ - build_asset_generation_setup_from_cache, next_message_and_preimage_for_step, - next_state_for_step, - }, - helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, - }, - }, - types::{ - EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolMessagePreimage, - ProtocolParametersHash, StepCounter, - }, + tests::common::asset_readers::load_embedded_next_epoch_step_output_asset, + types::{EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolParametersHash, StepCounter}, }; #[test] @@ -99,101 +83,33 @@ fn msg_tampered_is_rejected() { } mod slow { - use super::*; + use crate::circuits::halo2_ivc::tests::common::{ + failure_signature::{ + assert_recursive_mock_prover_rejects_public_input_rows, mutate_public_input, + }, + generators::build_asset_generation_setup_from_cache, + helpers::{build_asset_backed_next_epoch_fixture, build_mock_prover_setup_from_assets}, + public_input_layout::all_state_rows, + }; #[test] - fn circuit_rejects_protocol_parameters_non_advance_in_next_epoch_step() { - // MockProver constraint check: in a next-epoch transition the circuit must advance - // protocol_parameters to prev_state.next_protocol_parameters. Setting it to ONE violates that. + fn circuit_rejects_tampered_next_epoch_state_public_inputs() { + // Every next-state element is bound to the value the circuit derives for a next-epoch step, so + // tampering all of them must break exactly their own copy constraints. The fixture is the + // committed step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = next_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.next_merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("next-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = next_state_for_step(&prev_state, message); - tampered_state.protocol_parameters = ProtocolParametersHash::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "protocol_parameters set to ONE (next-epoch: must advance to prev.next_protocol_parameters)", - ); - } + let mut fixture = build_asset_backed_next_epoch_fixture(&mock_prover_setup); - #[test] - fn circuit_rejects_merkle_tree_commitment_non_advance_in_next_epoch_step() { - // MockProver constraint check: in a next-epoch transition the circuit must advance - // merkle_tree_commitment to prev_state.next_merkle_tree_commitment. Setting it to ONE violates that. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = next_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.next_merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("next-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = next_state_for_step(&prev_state, message); - tampered_state.merkle_tree_commitment = MerkleTreeCommitment::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "merkle_tree_commitment set to ONE (next-epoch: must advance to prev.next_merkle_tree_commitment)", - ); - } + let expected_rows = all_state_rows(); + for row in expected_rows.keys() { + mutate_public_input(&mut fixture.public_inputs, *row); + } - #[test] - fn circuit_rejects_epoch_non_increment_in_next_epoch_step() { - // MockProver constraint check: in a next-epoch transition the circuit must increment - // current_epoch by exactly one. Decrementing it violates that constraint. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = next_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.next_merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("next-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = next_state_for_step(&prev_state, message); - tampered_state.current_epoch = EpochNumber::new(tampered_state.current_epoch.as_u64() - 1); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "current_epoch decremented (next-epoch: must increment by exactly one)", + assert_recursive_mock_prover_rejects_public_input_rows( + fixture.ivc_circuit_data, + fixture.public_inputs, + &expected_rows, ); } } diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs index a2165498bc5..9cd3270e65b 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs @@ -1,25 +1,8 @@ use super::*; use crate::circuits::halo2_ivc::{ - state::Witness, - tests::common::{ - asset_readers::{ - load_embedded_following_certificate_in_epoch_asset, - load_embedded_recursive_chain_state_asset, - }, - generators::{ - build_asset_generation_setup_from_cache, same_epoch_message_and_preimage_for_step, - same_epoch_next_state_for_step, - }, - helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, - }, - }, - types::{ - EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolMessagePreimage, - ProtocolParametersHash, StepCounter, - }, + tests::common::asset_readers::load_embedded_following_certificate_in_epoch_asset, + types::{EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolParametersHash, StepCounter}, }; #[test] @@ -100,104 +83,33 @@ fn msg_tampered_is_rejected() { } mod slow { - use super::*; + use crate::circuits::halo2_ivc::tests::common::{ + failure_signature::{ + assert_recursive_mock_prover_rejects_public_input_rows, mutate_public_input, + }, + generators::build_asset_generation_setup_from_cache, + helpers::{build_asset_backed_same_epoch_fixture, build_mock_prover_setup_from_assets}, + public_input_layout::all_state_rows, + }; #[test] - fn circuit_rejects_merkle_tree_commitment_carry_violation_in_same_epoch_step() { - // MockProver constraint check: in a same-epoch transition the circuit must carry - // merkle_tree_commitment unchanged from prev_state. Setting it to ONE violates that constraint. + fn circuit_rejects_tampered_same_epoch_state_public_inputs() { + // Every next-state element is bound to the value the circuit derives for a same-epoch step, so + // tampering all of them must break exactly their own copy constraints. The fixture is the + // committed step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, message); - tampered_state.merkle_tree_commitment = MerkleTreeCommitment::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "merkle_tree_commitment set to ONE (same-epoch: must carry prev.merkle_tree_commitment unchanged)", - ); - } + let mut fixture = build_asset_backed_same_epoch_fixture(&mock_prover_setup); - #[test] - fn circuit_rejects_protocol_parameters_carry_violation_in_same_epoch_step() { - // MockProver constraint check: in a same-epoch transition the circuit must carry - // protocol_parameters unchanged from prev_state. Setting it to ONE violates that constraint. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, message); - tampered_state.protocol_parameters = ProtocolParametersHash::from_field(NativeField::ONE); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "protocol_parameters set to ONE (same-epoch: must carry prev.protocol_parameters unchanged)", - ); - } + let expected_rows = all_state_rows(); + for row in expected_rows.keys() { + mutate_public_input(&mut fixture.public_inputs, *row); + } - #[test] - fn circuit_rejects_epoch_advance_in_same_epoch_step() { - // MockProver constraint check: in a same-epoch transition the circuit must keep - // current_epoch equal to prev_state.current_epoch. Incrementing it violates that constraint. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let prev_state = load_embedded_recursive_chain_state_asset() - .expect("recursive chain state asset should load") - .state; - let (message, preimage_bytes) = - same_epoch_message_and_preimage_for_step(&setup, &prev_state); - let witness = Witness::new( - setup.genesis_signature, - MessageHash::from_field(message), - prev_state.merkle_tree_commitment, - ProtocolMessagePreimage::new( - preimage_bytes - .try_into() - .expect("same-epoch preimage should be PREIMAGE_SIZE bytes"), - ), - ); - let mut tampered_state = same_epoch_next_state_for_step(&prev_state, message); - tampered_state.current_epoch = EpochNumber::new(tampered_state.current_epoch.as_u64() + 1); - let ivc_circuit_data = - build_trivial_mock_prover_circuit(&mock_prover_setup, prev_state, witness); - let public_inputs = build_mock_prover_public_inputs(&mock_prover_setup, &tampered_state); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "current_epoch incremented (same-epoch: must equal prev.current_epoch)", + assert_recursive_mock_prover_rejects_public_input_rows( + fixture.ivc_circuit_data, + fixture.public_inputs, + &expected_rows, ); } } From baac0d933e25940dfd07f84d26c356d407fbe27e Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 11:11:08 +0900 Subject: [PATCH 04/11] test(halo2_ivc): assert exact failure rows for preimage encoding cases --- .../tests/common/failure_signature.rs | 17 ++- .../halo2_ivc/tests/common/helpers.rs | 15 -- .../halo2_ivc/tests/encoding/negative.rs | 130 ++++++++++++------ 3 files changed, 101 insertions(+), 61 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index 17fcfbcaae4..8b3687fbe9e 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -7,10 +7,13 @@ //! into "these public inputs, and only these, stopped being satisfiable". //! //! The contract is deliberately two-sided: an **exact** public-statement row signature, plus a -//! **permitted failure class** for everything else. The advice-side halves of a broken copy -//! constraint, and the message-preimage equality, are also permutation failures, but the columns -//! and regions they name belong to the gadget layer and carry no stability guarantee — so they are -//! constrained by class and not enumerated. +//! **permitted failure class** for everything else. Advice-side members of a broken permutation +//! class are constrained by class and never enumerated, because the columns and regions they name +//! belong to the gadget layer and carry no stability guarantee. +//! +//! An internal copy constraint can still implicate a named public row, when its equality class also +//! contains an instance-bound cell. The state message and its preimage hash are joined that way, so +//! corrupting only the witness preimage legitimately yields an exact public-row signature. use std::collections::{BTreeMap, BTreeSet}; @@ -77,7 +80,7 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( let prover = MockProver::run(circuit, instances).expect("MockProver setup should succeed"); let failures = prover .verify() - .expect_err("the circuit should reject the tampered public inputs"); + .expect_err("the circuit should reject the provided circuit and instances"); let unexpected_classes: Vec = failures .iter() @@ -269,8 +272,8 @@ mod tests { #[test] fn helper_accepts_rejection_with_an_empty_expected_signature() { - // A rejection caused by the message-preimage equality implicates no public-statement row. - // Tampering only the committed column reproduces that shape here. + // A break confined to the committed column implicates no public-statement row, so the + // helper must report an empty signature rather than treating rejection alone as a match. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[0], 0); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs index ecff95e5953..379f5db5f8d 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs @@ -157,21 +157,6 @@ pub(crate) fn assert_recursive_mock_prover_accepts_with_label( }); } -/// Runs `MockProver` and asserts at least one constraint fails, printing `label` on failure -/// so the scenario that unexpectedly passed is identifiable when multiple scenarios share one `#[test]` function. -pub(crate) fn assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data: IvcCircuitData, - public_inputs: Vec, - label: &str, -) { - let prover = MockProver::run(&ivc_circuit_data, vec![vec![], public_inputs]) - .expect("recursive MockProver setup should succeed"); - assert!( - prover.verify().is_err(), - "MockProver should reject the circuit and public inputs — case: {label}" - ); -} - /// Prepares the stored previous recursive proof and returns its accumulator contribution. /// /// This mirrors the first half of the normal recursive-step asset generation: diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs index dd0fb50c879..704ed6392bf 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs @@ -7,21 +7,24 @@ use midnight_circuits::types::Instantiable; use crate::circuits::halo2_ivc::{ AssignedAccumulator, NativeField, PREIMAGE_CURRENT_EPOCH_BYTES, PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES, PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES, + circuit::IvcCircuitData, protocol_message::{DynamicProtocolMessagePartKey, ProtocolMessage}, state::State, tests::common::{ asset_readers::{ load_embedded_next_epoch_step_output_asset, load_embedded_verification_context_asset, }, + failure_signature::assert_recursive_mock_prover_rejects_public_input_rows, generators::{ - GENESIS_EPOCH, build_asset_generation_setup_from_cache, + AssetGenerationSetup, GENESIS_EPOCH, build_asset_generation_setup_from_cache, build_genesis_base_case_next_state, build_genesis_base_case_witness, }, + helpers::MockProverSetup, helpers::{ - assert_recursive_mock_prover_rejects_with_label, build_genesis_mock_prover_circuit, - build_genesis_mock_prover_public_inputs, build_mock_prover_setup_from_assets, - verify_prepare_blake2b_recursive_proof, + build_genesis_mock_prover_circuit, build_genesis_mock_prover_public_inputs, + build_mock_prover_setup_from_assets, verify_prepare_blake2b_recursive_proof, }, + public_input_layout::StateField, }, types::{EpochNumber, MerkleTreeCommitment, ProtocolParametersHash}, }; @@ -192,69 +195,118 @@ fn current_epoch_tampered_public_input_is_rejected() { } mod slow { + use std::collections::BTreeMap; + use std::ops::Range; + use super::*; - #[test] - fn circuit_rejects_wrong_next_merkle_tree_commitment_byte_range() { - // MockProver constraint check: filling PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES with 0xff - // must violate the in-circuit byte-extraction constraint for that preimage region. + /// Preimage byte mutated to break the message equality without moving any extracted field. + /// + /// It falls inside the dynamic-parts digest, which the circuit hashes but never decodes. + const MESSAGE_EQUALITY_TAMPER_OFFSET: usize = 6; + + /// Flips the byte at `offset` in the genesis witness preimage and returns the resulting circuit. + /// + /// The mutation is an exclusive-or so it cannot land on the value already there, and it touches + /// a single byte, so at most the one decoded field that byte feeds can move. + fn build_genesis_circuit_with_flipped_preimage_byte( + setup: &AssetGenerationSetup, + mock_prover_setup: &MockProverSetup, + offset: usize, + ) -> IvcCircuitData { + let mut witness = build_genesis_base_case_witness(setup); + witness.message_preimage.as_mut_bytes()[offset] ^= 0xff; + build_genesis_mock_prover_circuit(mock_prover_setup, State::genesis(), witness) + } + + /// Asserts that flipping the first byte of `range` breaks exactly the message equality and + /// `field`'s public-input binding. + /// + /// Any change to the preimage invalidates the whole-preimage hash. In the current layout that + /// inconsistent equality class reports the message row, and `field` is the one decoded value the + /// byte window feeds. + fn assert_flipped_range_breaks_message_and_field(range: Range, field: StateField) { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); let public_inputs = build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let ivc_circuit_data = build_genesis_circuit_with_flipped_preimage_byte( + &setup, + &mock_prover_setup, + range.start, + ); - let mut witness = build_genesis_base_case_witness(&setup); - witness.message_preimage.as_mut_bytes()[PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES] - .fill(0xff); - let ivc_circuit_data = - build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - assert_recursive_mock_prover_rejects_with_label( + assert_recursive_mock_prover_rejects_public_input_rows( ivc_circuit_data, public_inputs, - "message_preimage[PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES] filled with 0xff", + &BTreeMap::from([ + (StateField::Message.row(), StateField::Message.name()), + (field.row(), field.name()), + ]), ); } #[test] - fn circuit_rejects_wrong_next_protocol_parameters_byte_range() { - // MockProver constraint check: filling PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES with 0xff - // must violate the in-circuit byte-extraction constraint for that preimage region. - let setup = build_asset_generation_setup_from_cache(); - let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); - let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); - let public_inputs = - build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); + fn circuit_rejects_wrong_next_merkle_tree_commitment_byte_range() { + // Flipping a byte here invalidates the whole-preimage hash and changes exactly the next + // Merkle-tree commitment. A different decoded row moving would mean the circuit reads the + // wrong window. + assert_flipped_range_breaks_message_and_field( + PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES, + StateField::NextMerkleTreeCommitment, + ); + } - let mut witness = build_genesis_base_case_witness(&setup); - witness.message_preimage.as_mut_bytes()[PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES].fill(0xff); - let ivc_circuit_data = - build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - assert_recursive_mock_prover_rejects_with_label( - ivc_circuit_data, - public_inputs, - "message_preimage[PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES] filled with 0xff", + #[test] + fn circuit_rejects_wrong_next_protocol_parameters_byte_range() { + // Same for the next protocol parameters. + assert_flipped_range_breaks_message_and_field( + PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES, + StateField::NextProtocolParameters, ); } #[test] fn circuit_rejects_wrong_current_epoch_byte_range() { - // MockProver constraint check: filling PREIMAGE_CURRENT_EPOCH_BYTES with 0xff - // must violate the in-circuit byte-extraction constraint for that preimage region. + // Same for the current epoch. + assert_flipped_range_breaks_message_and_field( + PREIMAGE_CURRENT_EPOCH_BYTES, + StateField::CurrentEpoch, + ); + } + + #[test] + fn circuit_rejects_preimage_inconsistent_with_the_message() { + // Isolates the message equality. The byte is outside every decoded range, so no decoded + // state field changes and the public values are left untouched; the message row is reported + // because, in the current layout, that equality class contains the cell bound to it. + for range in [ + PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES, + PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES, + PREIMAGE_CURRENT_EPOCH_BYTES, + ] { + assert!( + !range.contains(&MESSAGE_EQUALITY_TAMPER_OFFSET), + "the tampered byte must sit outside every decoded range" + ); + } + let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); let public_inputs = build_genesis_mock_prover_public_inputs(&mock_prover_setup, &next_state); + let ivc_circuit_data = build_genesis_circuit_with_flipped_preimage_byte( + &setup, + &mock_prover_setup, + MESSAGE_EQUALITY_TAMPER_OFFSET, + ); - let mut witness = build_genesis_base_case_witness(&setup); - witness.message_preimage.as_mut_bytes()[PREIMAGE_CURRENT_EPOCH_BYTES].fill(0xff); - let ivc_circuit_data = - build_genesis_mock_prover_circuit(&mock_prover_setup, State::genesis(), witness); - assert_recursive_mock_prover_rejects_with_label( + assert_recursive_mock_prover_rejects_public_input_rows( ivc_circuit_data, public_inputs, - "message_preimage[PREIMAGE_CURRENT_EPOCH_BYTES] filled with 0xff", + &BTreeMap::from([(StateField::Message.row(), StateField::Message.name())]), ); } } From 86895f5336cab410da762b28e666e94c6a224237 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 11:35:21 +0900 Subject: [PATCH 05/11] test(halo2_ivc): assert the exact accumulator failure signature --- .../tests/common/failure_signature.rs | 35 +++++++++--- .../halo2_ivc/tests/common/helpers.rs | 12 ----- .../halo2_ivc/tests/in_circuit/accumulator.rs | 54 ++++++++++++++----- 3 files changed, 71 insertions(+), 30 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index 8b3687fbe9e..bdb239b28d3 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -17,7 +17,6 @@ use std::collections::{BTreeMap, BTreeSet}; -use ff::Field; use midnight_proofs::{ dev::{FailureLocation, MockProver, VerifyFailure}, plonk::{Any, Circuit}, @@ -32,13 +31,17 @@ use crate::circuits::halo2_ivc::{NativeField, circuit::IvcCircuitData}; /// the committed column from being mistaken for a public-statement failure. pub(crate) const PUBLIC_STATEMENT_INSTANCE_COLUMN: usize = 1; -/// Mutates the public input at `row` by a guaranteed nonzero delta. +/// Mutates the public input at `row` by a nonzero, row-dependent delta. /// -/// Adding one rather than assigning a fixed value keeps the mutation effective whatever the -/// original held: assigning `ONE` is a no-op wherever the honest value already is one, as the -/// genesis step counter is. +/// Adding rather than assigning keeps the mutation effective whatever the original held: assigning +/// `ONE` is a no-op wherever the honest value already is one, as the genesis step counter is. +/// +/// The delta varies with the row because a permutation class is checked as a cycle. Two tampered +/// cells in one class that started equal would stay equal under a shared delta, leaving the mapping +/// free to report neither, so a whole-section mutation could hide a bound row. Distinct deltas keep +/// that from happening for the known-satisfiable baselines this helper is used with. pub(crate) fn mutate_public_input(public_inputs: &mut [NativeField], row: usize) { - public_inputs[row] += NativeField::ONE; + public_inputs[row] += NativeField::from(row as u64 + 1); } /// True when `failure` is a permutation failure on the public-statement column. @@ -240,6 +243,26 @@ mod tests { ] } + #[test] + fn mutation_gives_equal_valued_rows_distinct_nonzero_deltas() { + // Equal-valued rows in one permutation class mask each other under a shared delta. + const SHARED: u64 = 7; + let mut public_inputs = vec![NativeField::from(SHARED); 4]; + for row in 0..public_inputs.len() { + mutate_public_input(&mut public_inputs, row); + } + + assert!( + public_inputs.iter().all(|value| *value != NativeField::from(SHARED)), + "every mutation must change its row" + ); + assert_eq!( + public_inputs.iter().copied().collect::>().len(), + public_inputs.len(), + "rows that started equal must end distinct" + ); + } + #[test] fn minimal_circuit_accepts_honest_instances() { // Canary: without it, a helper that always found failures would look correct. diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs index 379f5db5f8d..58f4bee7c01 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs @@ -128,18 +128,6 @@ pub(crate) fn build_recursive_mock_prover_setup( } } -/// Runs `MockProver` on the recursive circuit and asserts that at least one constraint fails. -pub(crate) fn assert_recursive_mock_prover_rejects( - ivc_circuit_data: IvcCircuitData, - public_inputs: Vec, -) { - let prover = MockProver::run(&ivc_circuit_data, vec![vec![], public_inputs]) - .expect("recursive MockProver setup should succeed"); - prover - .verify() - .expect_err("recursive MockProver should reject the provided circuit and public inputs"); -} - /// Runs `MockProver` and asserts all constraints hold, printing `label` on failure so /// the failing case is identifiable when multiple scenarios share one `#[test]` function. pub(crate) fn assert_recursive_mock_prover_accepts_with_label( diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs index 2ce40d7b1fe..9d2520d012c 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs @@ -87,29 +87,40 @@ fn next_epoch_step_rejects_tampered_next_accumulator() { } mod slow { - use ff::Field; + use std::collections::BTreeMap; + use midnight_circuits::types::Instantiable; use crate::circuits::halo2_ivc::{ - AssignedAccumulator, NativeField, + AssignedAccumulator, circuit::IvcCircuitData, tests::common::{ asset_readers::load_embedded_recursive_chain_state_asset, + failure_signature::{ + assert_recursive_mock_prover_rejects_public_input_rows, mutate_public_input, + }, generators::{ build_asset_generation_setup_from_cache, build_same_epoch_certificate_asset_data, }, helpers::{ - assert_recursive_mock_prover_rejects, build_recursive_mock_prover_setup, + assert_recursive_mock_prover_accepts_with_label, build_recursive_mock_prover_setup, compute_expected_next_accumulator, }, + public_input_layout::accumulator_row, }, }; #[test] - fn circuit_rejects_with_wrong_next_accumulator_in_same_epoch_step() { - // MockProver check that the in-circuit accumulator update constraint holds for - // a same-epoch step; substituting a wrong next_accumulator in the public inputs - // causes MockProver to detect the arithmetic constraint violation. + fn circuit_rejects_tampered_same_epoch_accumulator_public_inputs() { + // The accumulator the circuit folds for a same-epoch step is bound to the public statement, + // so moving every element of its encoding must implicate exactly the accumulator section's + // public rows and no other public row. The encoding is heterogeneous — both MSM sides, curve + // coordinates, variable-base and fixed-base scalars — so covering the whole section rather + // than one element exercises each binding path at no extra synthesis. + // + // The certificate proof is proved here rather than read from an asset: this is the only + // place the circuit verifies a certificate proof it has not seen before, and certificate + // proofs are randomized, so a stored one would fix the blinding for every run. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_recursive_mock_prover_setup(&setup); @@ -144,16 +155,35 @@ mod slow { ) .expect("valid IvcCircuitData construction"); - let mut accumulator_encoding = AssignedAccumulator::as_public_input(&next_accumulator); - accumulator_encoding[0] = NativeField::ONE; - let public_inputs = [ mock_prover_setup.global.as_public_input(), next_state.as_public_input(), - accumulator_encoding, + AssignedAccumulator::as_public_input(&next_accumulator), ] .concat(); - assert_recursive_mock_prover_rejects(ivc_circuit_data, public_inputs); + // Establishes that this fixture is satisfiable before anything is tampered, so the exact + // signature below cannot be satisfied by a rejection that was already present. The circuit + // data is cloned so the certificate is proved once. + assert_recursive_mock_prover_accepts_with_label( + ivc_circuit_data.clone(), + public_inputs.clone(), + "same-epoch step with a freshly proved certificate", + ); + + let mut tampered_public_inputs = public_inputs; + let expected_rows: BTreeMap = (accumulator_row(0) + ..tampered_public_inputs.len()) + .map(|row| (row, "next_accumulator")) + .collect(); + for row in expected_rows.keys() { + mutate_public_input(&mut tampered_public_inputs, *row); + } + + assert_recursive_mock_prover_rejects_public_input_rows( + ivc_circuit_data, + tampered_public_inputs, + &expected_rows, + ); } } From ee7575c0c57bffe64cac5a27cc2956063fd11da2 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 11:57:36 +0900 Subject: [PATCH 06/11] docs(halo2_ivc): correct the coverage claims in the recursive test module docs --- .../halo2_ivc/tests/common/failure_signature.rs | 8 +++++++- .../src/circuits/halo2_ivc/tests/in_circuit/mod.rs | 9 ++++++--- .../halo2_ivc/tests/in_circuit/public_inputs.rs | 7 +++++-- .../circuits/halo2_ivc/tests/transitions/mod.rs | 14 ++++++++++---- .../tests/transitions/negative/genesis.rs | 2 +- .../tests/transitions/negative/next_epoch.rs | 2 +- .../tests/transitions/negative/same_epoch.rs | 2 +- 7 files changed, 31 insertions(+), 13 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index bdb239b28d3..58e6f0b15d9 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -72,7 +72,13 @@ fn public_statement_row(failure: &VerifyFailure) -> Option { /// /// `expected_rows` maps each expected row to the field name reported in diagnostics; rows that fail /// unexpectedly are reported by index, since a generic circuit has no field names to resolve them -/// against. Every returned failure must be a permutation failure, and every permutation failure on +/// against. +/// +/// What an exact row set does **not** establish: that each row carries the field the caller named. +/// Dropping one public-input assignment shifts every later binding down a row, and every expected +/// row still fails; two fields whose honest values are equal can also swap invisibly. The layout +/// guards beside this helper pin section lengths and the state serialization order, which is not the +/// same as proving the field-to-row mapping. Mutating several rows at once inherits that boundary. Every returned failure must be a permutation failure, and every permutation failure on /// the public-statement column must carry an absolute row — anything else means the circuit rejected /// in a way this helper cannot account for, and is surfaced rather than dropped. pub(crate) fn assert_circuit_rejects_public_input_rows>( diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs index 2bc201fefb4..1a7c1671210 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs @@ -1,8 +1,11 @@ //! Layer C1: in-circuit verification mechanics tests for the recursive Halo2 IVC circuit. //! -//! These tests validate what the circuit enforces internally — proof verification -//! wiring, genesis gating bypass, and accumulator update constraints — as opposed -//! to the off-circuit state transition rules covered by Layer B. +//! These tests validate what the circuit enforces internally: proof verification wiring, genesis +//! gating bypass, and the binding of the accumulator it folds. +//! +//! The chain-link rules are not covered negatively here or in Layer B. Every negative case in the +//! module mutates the public statement, which establishes bindings rather than the transition +//! constraints that produce the bound values. //! //! `public_inputs` — tampered global fields and accumulator in public inputs. //! `genesis_gating` — garbage proof bytes are accepted at genesis (step 0). diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs index 6a89ac21ead..448653cc3dc 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs @@ -1,6 +1,9 @@ //! Negative public-input tests: tampered global fields and accumulator, checked against the stored -//! proof by the verifier. In-circuit binding of the same elements is covered by -//! `transitions::negative::genesis::slow`. +//! proof by the verifier. +//! +//! In-circuit binding of the same elements lives elsewhere, split by responsibility: the global +//! fields with the genesis negative transition case, the accumulator with the negative accumulator +//! case. use ff::Field; use midnight_circuits::types::Instantiable; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs index faea99823e8..159384c1674 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs @@ -1,9 +1,15 @@ //! Layer B: state transition rule tests for the recursive Halo2 IVC circuit. //! -//! These tests validate the chain link rules — genesis, same-epoch, and -//! next-epoch transitions — by verifying stored proofs with correct and -//! tampered public inputs. Most cases are fast (verifier only); slow checks -//! use MockProver to confirm the circuit enforces the rules in-circuit. +//! The fast cases verify stored proofs against correct and tampered public inputs, for each of the +//! genesis, same-epoch and next-epoch contexts. +//! +//! The slow `MockProver` cases establish something narrower than the rules themselves: that the +//! circuit binds each returned state cell to its public row, and that a satisfiable stimulus is +//! accepted. They mutate the instance vector only, so they do not isolate the chain-link +//! constraints — `classify_epoch`, `assert_first_step_is_next_epoch`, +//! `assert_merkle_tree_commitment_link`, `assert_next_values_consistency`. Removing one of those +//! need not make a public-output tamper accept, and acceptance cannot show one is necessary. +//! Exercising them requires mutating the witness. mod negative; mod positive; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs index 9f497e1ae61..3ee2d17b048 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs @@ -106,7 +106,7 @@ mod slow { #[test] fn circuit_rejects_tampered_genesis_global_and_state_public_inputs() { // Every global and next-state element is bound to the value the circuit derives, so - // tampering all of them must break exactly their own copy constraints. One synthesis covers + // tampering all of them must implicate exactly those public rows and no others. One synthesis covers // every element because MockProver reports all failures, not only the first. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs index 5fabba210e0..310bf8102d0 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs @@ -95,7 +95,7 @@ mod slow { #[test] fn circuit_rejects_tampered_next_epoch_state_public_inputs() { // Every next-state element is bound to the value the circuit derives for a next-epoch step, so - // tampering all of them must break exactly their own copy constraints. The fixture is the + // tampering all of them must implicate exactly those public rows and no others. The fixture is the // committed step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs index 9cd3270e65b..0c3a7ebf54e 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs @@ -95,7 +95,7 @@ mod slow { #[test] fn circuit_rejects_tampered_same_epoch_state_public_inputs() { // Every next-state element is bound to the value the circuit derives for a same-epoch step, so - // tampering all of them must break exactly their own copy constraints. The fixture is the + // tampering all of them must implicate exactly those public rows and no others. The fixture is the // committed step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); From e3754f139543a4c433774a1ecf5dd0550d73ef25 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Mon, 24 Aug 2026 12:04:00 +0900 Subject: [PATCH 07/11] docs(halo2_ivc): trim the recursive test comments to what the code does --- .../tests/common/failure_signature.rs | 79 ++++++------------- .../halo2_ivc/tests/common/helpers.rs | 30 +++---- .../tests/common/public_input_layout.rs | 10 +-- .../halo2_ivc/tests/encoding/negative.rs | 25 +++--- .../halo2_ivc/tests/in_circuit/accumulator.rs | 15 ++-- .../halo2_ivc/tests/in_circuit/mod.rs | 5 +- .../tests/in_circuit/public_inputs.rs | 5 +- .../halo2_ivc/tests/transitions/mod.rs | 14 ++-- .../tests/transitions/negative/genesis.rs | 4 +- .../tests/transitions/negative/next_epoch.rs | 4 +- .../tests/transitions/negative/same_epoch.rs | 4 +- .../halo2_ivc/tests/transitions/positive.rs | 10 +-- 12 files changed, 71 insertions(+), 134 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index 58e6f0b15d9..d07e404bedb 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -1,19 +1,9 @@ //! Classifies `MockProver` failures by the public-statement rows they implicate. //! -//! A negative test that asserts only `verify().is_err()` can pass for the wrong reason. The -//! recursive circuit binds every element of its public statement with a copy constraint, so a -//! tampered element surfaces as a [`VerifyFailure::Permutation`] on the public-statement instance -//! column at that element's row. Asserting the exact set of those rows turns "something failed" -//! into "these public inputs, and only these, stopped being satisfiable". -//! -//! The contract is deliberately two-sided: an **exact** public-statement row signature, plus a -//! **permitted failure class** for everything else. Advice-side members of a broken permutation -//! class are constrained by class and never enumerated, because the columns and regions they name -//! belong to the gadget layer and carry no stability guarantee. -//! -//! An internal copy constraint can still implicate a named public row, when its equality class also -//! contains an instance-bound cell. The state message and its preimage hash are joined that way, so -//! corrupting only the witness preimage legitimately yields an exact public-row signature. +//! The circuit binds every element of its public statement with a copy constraint, so a tampered +//! element fails as a permutation on the public-statement instance column at that element's row. +//! Advice-side members of a broken class are not enumerated: their columns and regions are named by +//! the gadget layer and carry no stability guarantee. use std::collections::{BTreeMap, BTreeSet}; @@ -26,20 +16,14 @@ use crate::circuits::halo2_ivc::{NativeField, circuit::IvcCircuitData}; /// Index of the instance column carrying the circuit's public statement. /// -/// The recursive circuit declares the committed-instance column first and leaves it empty, so the -/// public statement lands in the second column. Filtering on this index is what keeps a failure in -/// the committed column from being mistaken for a public-statement failure. +/// Column zero is the committed-instance column, which this circuit leaves empty. pub(crate) const PUBLIC_STATEMENT_INSTANCE_COLUMN: usize = 1; /// Mutates the public input at `row` by a nonzero, row-dependent delta. /// -/// Adding rather than assigning keeps the mutation effective whatever the original held: assigning -/// `ONE` is a no-op wherever the honest value already is one, as the genesis step counter is. -/// -/// The delta varies with the row because a permutation class is checked as a cycle. Two tampered -/// cells in one class that started equal would stay equal under a shared delta, leaving the mapping -/// free to report neither, so a whole-section mutation could hide a bound row. Distinct deltas keep -/// that from happening for the known-satisfiable baselines this helper is used with. +/// Adding rather than assigning keeps the mutation effective whatever the original value. The delta +/// varies by row so two tampered cells in one permutation class cannot stay equal to each other, +/// which would let the cycle check report neither. pub(crate) fn mutate_public_input(public_inputs: &mut [NativeField], row: usize) { public_inputs[row] += NativeField::from(row as u64 + 1); } @@ -56,7 +40,7 @@ fn is_public_statement_failure(failure: &VerifyFailure) -> bool { /// Returns the public-statement row implicated by `failure`, if it implicates one. /// -/// Public-statement cells are assigned outside any region, so their failures carry an absolute row. +/// Public-statement cells sit outside any region, so their failures carry an absolute row. fn public_statement_row(failure: &VerifyFailure) -> Option { match failure { VerifyFailure::Permutation { @@ -70,17 +54,12 @@ fn public_statement_row(failure: &VerifyFailure) -> Option { /// Runs `MockProver` on any circuit, requires rejection, and asserts that the public-statement rows /// implicated are exactly the keys of `expected_rows`. /// -/// `expected_rows` maps each expected row to the field name reported in diagnostics; rows that fail -/// unexpectedly are reported by index, since a generic circuit has no field names to resolve them -/// against. +/// `expected_rows` maps each row to the field name used in diagnostics. Every returned failure must +/// be a permutation failure, and every public-statement failure must carry an absolute row. /// -/// What an exact row set does **not** establish: that each row carries the field the caller named. -/// Dropping one public-input assignment shifts every later binding down a row, and every expected -/// row still fails; two fields whose honest values are equal can also swap invisibly. The layout -/// guards beside this helper pin section lengths and the state serialization order, which is not the -/// same as proving the field-to-row mapping. Mutating several rows at once inherits that boundary. Every returned failure must be a permutation failure, and every permutation failure on -/// the public-statement column must carry an absolute row — anything else means the circuit rejected -/// in a way this helper cannot account for, and is surfaced rather than dropped. +/// An exact row set does not prove each row carries the field named for it: dropping one +/// public-input assignment shifts every later binding while all expected rows still fail, and two +/// fields with equal honest values can swap invisibly. pub(crate) fn assert_circuit_rejects_public_input_rows>( circuit: &C, instances: Vec>, @@ -104,9 +83,8 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( unexpected_classes.join("\n") ); - // Without this, a public-statement failure reported against a region would be dropped by - // `public_statement_row` and an empty expected signature would pass on a circuit that had in - // fact broken a public-input binding. + // A row-less public-statement failure would otherwise be dropped, letting an empty expected + // signature pass on a circuit that had broken a binding. let unlocatable: Vec = failures .iter() .filter(|failure| { @@ -142,8 +120,6 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( } /// Recursive-circuit wrapper over [`assert_circuit_rejects_public_input_rows`]. -/// -/// The empty first column is the committed-instance column the circuit declares and never uses. pub(crate) fn assert_recursive_mock_prover_rejects_public_input_rows( ivc_circuit_data: IvcCircuitData, public_inputs: Vec, @@ -178,12 +154,10 @@ mod tests { public_statement_instance: Column, } - /// Smallest circuit that reproduces the two-instance-column shape of the recursive circuit. + /// Smallest circuit reproducing the two-instance-column shape of the recursive circuit. /// - /// Two of its public-statement inputs are bound by copy constraints, one is left unbound, and a - /// third cell is bound to the committed column. That is exactly the discrimination the helper - /// claims: it must report the bound public-statement rows, and neither the unbound row nor the - /// committed-column failure. + /// Two public-statement inputs are bound, one is left unbound, and a third cell is bound to the + /// committed column, so both the row and column filters are exercised. struct MinimalCircuit; impl Circuit for MinimalCircuit { @@ -251,7 +225,7 @@ mod tests { #[test] fn mutation_gives_equal_valued_rows_distinct_nonzero_deltas() { - // Equal-valued rows in one permutation class mask each other under a shared delta. + // Equal-valued rows in one permutation class would mask each other under a shared delta. const SHARED: u64 = 7; let mut public_inputs = vec![NativeField::from(SHARED); 4]; for row in 0..public_inputs.len() { @@ -271,7 +245,7 @@ mod tests { #[test] fn minimal_circuit_accepts_honest_instances() { - // Canary: without it, a helper that always found failures would look correct. + // Guards the cases below: a helper that always found failures would look correct. let prover = MockProver::run(&MinimalCircuit, honest_minimal_instances()) .expect("MockProver setup should succeed"); prover @@ -282,8 +256,7 @@ mod tests { #[test] fn helper_reports_bound_public_statement_rows_only() { let mut instances = honest_minimal_instances(); - // Tamper every kind of row at once: both bound public-statement rows, the unbound one, and - // the committed column. Only the bound public-statement rows may be reported. + // Only the bound public-statement rows may be reported. mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 1); mutate_public_input( @@ -301,8 +274,7 @@ mod tests { #[test] fn helper_accepts_rejection_with_an_empty_expected_signature() { - // A break confined to the committed column implicates no public-statement row, so the - // helper must report an empty signature rather than treating rejection alone as a match. + // A break confined to the committed column implicates no public-statement row. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[0], 0); @@ -312,7 +284,7 @@ mod tests { #[test] #[should_panic(expected = "public-input failure signature mismatch")] fn helper_rejects_an_incomplete_expected_signature() { - // Proves the assertion has teeth: two rows fail, so expecting one must not pass. + // Two rows fail, so expecting one must not pass. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 1); @@ -327,8 +299,7 @@ mod tests { #[test] #[should_panic(expected = "public-input failure signature mismatch")] fn helper_rejects_an_empty_signature_when_a_row_did_fail() { - // The counterpart to the empty-signature case above: an empty expectation must not absorb a - // real public-statement failure. + // An empty expectation must not absorb a real public-statement failure. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs index 58f4bee7c01..855e1ff016e 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/helpers.rs @@ -247,12 +247,11 @@ pub(crate) fn prepare_stored_step_certificate_accumulator( certificate_accumulator } -/// A non-genesis MockProver stimulus assembled entirely from committed step assets. +/// A non-genesis MockProver stimulus assembled from committed step assets. /// -/// Unlike [`build_genesis_mock_prover_circuit`], this carries the stored certificate proof, the -/// stored previous recursive proof and the stored previous accumulator, so the accumulator the -/// circuit computes is the stored next accumulator. That is what makes it satisfiable at a -/// non-genesis step, where the accumulator contributions are no longer gated to the group identity. +/// Carries the stored certificate proof, previous recursive proof and previous accumulator, so the +/// accumulator the circuit computes is the stored next one. Outside genesis the accumulator +/// contributions are no longer gated away, so a trivial accumulator would not match. pub(crate) struct AssetBackedStepFixture { /// Circuit data for the step. pub(crate) ivc_circuit_data: IvcCircuitData, @@ -262,10 +261,8 @@ pub(crate) struct AssetBackedStepFixture { /// The stored half of one recursive step, plus the commitment its certificate was produced against. /// -/// That commitment is not read from the step-output asset but chosen by transition type: a -/// same-epoch certificate is produced against the checkpoint's current Merkle-tree commitment, a -/// next-epoch one against its next commitment. The stored final recursive proof is deliberately -/// absent — MockProver checks the step's constraints and never verifies the step's own output. +/// The commitment is chosen by transition type rather than read from the asset. The step's own +/// output proof is absent: MockProver checks constraints and never verifies it. struct StepFixtureData { certificate_merkle_tree_commitment: MerkleTreeCommitment, certificate_proof: CertificateProofBytes, @@ -288,8 +285,7 @@ fn build_asset_backed_step_fixture( genesis_signature, } = recursive_chain_state; - // Turns a future drift between the reconstructed global and the stored one into a direct - // coherence error instead of an opaque constraint failure. + // Reports cross-asset drift directly rather than as an opaque constraint failure. assert_eq!( mock_prover_setup.global.as_public_input(), global_field_elements, @@ -363,12 +359,11 @@ pub(crate) fn build_asset_backed_next_epoch_fixture( } /// Builds an `IvcCircuitData` with empty proof slots and a trivial accumulator, for MockProver -/// constraint checks at the genesis step only. +/// checks at the genesis step only. /// -/// Empty proof slots work here because genesis gating scales both accumulator contributions to the -/// group identity, so the trivial input accumulator is also the expected output. At any later step -/// the contributions are live and the circuit derives an output accumulator no trivial instance can -/// match — see [`build_asset_backed_same_epoch_fixture`] for the non-genesis stimulus. +/// Genesis gating scales both accumulator contributions to the group identity, so the trivial input +/// accumulator is also the expected output. See [`build_asset_backed_same_epoch_fixture`] for the +/// non-genesis stimulus. pub(crate) fn build_genesis_mock_prover_circuit( setup: &MockProverSetup, prev_state: State, @@ -394,8 +389,7 @@ pub(crate) fn build_genesis_mock_prover_circuit( /// Builds the public-input vector for a genesis MockProver stimulus. /// -/// The accumulator section carries the trivial accumulator, which is the expected output only while -/// genesis gating scales both contributions to the group identity. +/// The accumulator section carries the trivial accumulator, correct only at genesis. pub(crate) fn build_genesis_mock_prover_public_inputs( setup: &MockProverSetup, next_state: &State, diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs index d232a5d5564..5ccc984dab9 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -1,12 +1,8 @@ //! Row indices of the recursive circuit's public statement. //! -//! The circuit lays out its statement through a single shared offset counter: the global -//! root-of-trust first, then the next state, then the accumulator. Tests build the same vector as -//! `[global, state, accumulator].concat()`, so a row index here is an index into that vector and -//! into the public-statement instance column alike. -//! -//! Keeping the mapping in one place is what lets a failure-signature assertion name the field that -//! broke instead of a bare integer, and it keeps row literals out of the test bodies. +//! The circuit constrains its statement through one shared offset counter: the global root of trust +//! first, then the next state, then the accumulator. Tests build the same vector, so a row index +//! here indexes both it and the public-statement instance column. use std::collections::BTreeMap; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs index 704ed6392bf..4ba16224069 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/encoding/negative.rs @@ -200,15 +200,15 @@ mod slow { use super::*; - /// Preimage byte mutated to break the message equality without moving any extracted field. + /// Preimage byte mutated to break the message equality without moving a decoded field. /// - /// It falls inside the dynamic-parts digest, which the circuit hashes but never decodes. + /// Falls inside the dynamic-parts digest, which the circuit hashes but never decodes. const MESSAGE_EQUALITY_TAMPER_OFFSET: usize = 6; /// Flips the byte at `offset` in the genesis witness preimage and returns the resulting circuit. /// - /// The mutation is an exclusive-or so it cannot land on the value already there, and it touches - /// a single byte, so at most the one decoded field that byte feeds can move. + /// An exclusive-or cannot land on the value already there, and one byte moves at most the one + /// decoded field it feeds. fn build_genesis_circuit_with_flipped_preimage_byte( setup: &AssetGenerationSetup, mock_prover_setup: &MockProverSetup, @@ -219,12 +219,10 @@ mod slow { build_genesis_mock_prover_circuit(mock_prover_setup, State::genesis(), witness) } - /// Asserts that flipping the first byte of `range` breaks exactly the message equality and - /// `field`'s public-input binding. + /// Asserts that flipping the first byte of `range` implicates the message row and `field`'s row. /// - /// Any change to the preimage invalidates the whole-preimage hash. In the current layout that - /// inconsistent equality class reports the message row, and `field` is the one decoded value the - /// byte window feeds. + /// Any preimage change invalidates the whole-preimage hash, which reports the message row; + /// `field` is the decoded value this window feeds. fn assert_flipped_range_breaks_message_and_field(range: Range, field: StateField) { let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); @@ -249,9 +247,7 @@ mod slow { #[test] fn circuit_rejects_wrong_next_merkle_tree_commitment_byte_range() { - // Flipping a byte here invalidates the whole-preimage hash and changes exactly the next - // Merkle-tree commitment. A different decoded row moving would mean the circuit reads the - // wrong window. + // A different decoded row moving would mean the circuit reads the wrong window. assert_flipped_range_breaks_message_and_field( PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES, StateField::NextMerkleTreeCommitment, @@ -278,9 +274,8 @@ mod slow { #[test] fn circuit_rejects_preimage_inconsistent_with_the_message() { - // Isolates the message equality. The byte is outside every decoded range, so no decoded - // state field changes and the public values are left untouched; the message row is reported - // because, in the current layout, that equality class contains the cell bound to it. + // Isolates the message equality: the byte is outside every decoded range, so no decoded + // field moves and the message row is the only one implicated. for range in [ PREIMAGE_NEXT_MERKLE_TREE_COMMITMENT_BYTES, PREIMAGE_NEXT_PROTOCOL_PARAMETERS_BYTES, diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs index 9d2520d012c..a86a06b5ead 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs @@ -112,15 +112,11 @@ mod slow { #[test] fn circuit_rejects_tampered_same_epoch_accumulator_public_inputs() { - // The accumulator the circuit folds for a same-epoch step is bound to the public statement, - // so moving every element of its encoding must implicate exactly the accumulator section's - // public rows and no other public row. The encoding is heterogeneous — both MSM sides, curve - // coordinates, variable-base and fixed-base scalars — so covering the whole section rather - // than one element exercises each binding path at no extra synthesis. + // The encoding is heterogeneous — both MSM sides, curve coordinates, variable-base and + // fixed-base scalars — so the whole section is covered rather than one element. // // The certificate proof is proved here rather than read from an asset: this is the only - // place the circuit verifies a certificate proof it has not seen before, and certificate - // proofs are randomized, so a stored one would fix the blinding for every run. + // place the circuit verifies a certificate proof it has not seen, and they are randomized. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_recursive_mock_prover_setup(&setup); @@ -162,9 +158,8 @@ mod slow { ] .concat(); - // Establishes that this fixture is satisfiable before anything is tampered, so the exact - // signature below cannot be satisfied by a rejection that was already present. The circuit - // data is cloned so the certificate is proved once. + // The signature below must not be satisfiable by a rejection that was already present. + // Cloning keeps the certificate proved once. assert_recursive_mock_prover_accepts_with_label( ivc_circuit_data.clone(), public_inputs.clone(), diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs index 1a7c1671210..951951ceb17 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/mod.rs @@ -3,9 +3,8 @@ //! These tests validate what the circuit enforces internally: proof verification wiring, genesis //! gating bypass, and the binding of the accumulator it folds. //! -//! The chain-link rules are not covered negatively here or in Layer B. Every negative case in the -//! module mutates the public statement, which establishes bindings rather than the transition -//! constraints that produce the bound values. +//! The negative cases mutate the public statement, so they establish bindings rather than the +//! transition constraints producing the bound values. Those have no negative coverage. //! //! `public_inputs` — tampered global fields and accumulator in public inputs. //! `genesis_gating` — garbage proof bytes are accepted at genesis (step 0). diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs index 448653cc3dc..bdc0c5232ab 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/public_inputs.rs @@ -1,9 +1,8 @@ //! Negative public-input tests: tampered global fields and accumulator, checked against the stored //! proof by the verifier. //! -//! In-circuit binding of the same elements lives elsewhere, split by responsibility: the global -//! fields with the genesis negative transition case, the accumulator with the negative accumulator -//! case. +//! In-circuit binding of the global fields lives with the genesis negative transition case, and of +//! the accumulator with the negative accumulator case. use ff::Field; use midnight_circuits::types::Instantiable; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs index 159384c1674..7a0b3d8cbc5 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs @@ -1,15 +1,11 @@ //! Layer B: state transition rule tests for the recursive Halo2 IVC circuit. //! -//! The fast cases verify stored proofs against correct and tampered public inputs, for each of the -//! genesis, same-epoch and next-epoch contexts. +//! The fast cases verify stored proofs against correct and tampered public inputs, per transition +//! context. //! -//! The slow `MockProver` cases establish something narrower than the rules themselves: that the -//! circuit binds each returned state cell to its public row, and that a satisfiable stimulus is -//! accepted. They mutate the instance vector only, so they do not isolate the chain-link -//! constraints — `classify_epoch`, `assert_first_step_is_next_epoch`, -//! `assert_merkle_tree_commitment_link`, `assert_next_values_consistency`. Removing one of those -//! need not make a public-output tamper accept, and acceptance cannot show one is necessary. -//! Exercising them requires mutating the witness. +//! The slow `MockProver` cases establish that the circuit binds each returned state cell to its +//! public row, and that a satisfiable stimulus is accepted. They mutate the instance vector only, +//! so they do not isolate the chain-link constraints; that needs witness-side mutation. mod negative; mod positive; diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs index 3ee2d17b048..a33d2695b82 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/genesis.rs @@ -105,9 +105,7 @@ mod slow { #[test] fn circuit_rejects_tampered_genesis_global_and_state_public_inputs() { - // Every global and next-state element is bound to the value the circuit derives, so - // tampering all of them must implicate exactly those public rows and no others. One synthesis covers - // every element because MockProver reports all failures, not only the first. + // One synthesis covers every element, since MockProver reports all failures, not the first. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let next_state = build_genesis_base_case_next_state(&setup, GENESIS_EPOCH); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs index 310bf8102d0..964ecaa2514 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/next_epoch.rs @@ -94,9 +94,7 @@ mod slow { #[test] fn circuit_rejects_tampered_next_epoch_state_public_inputs() { - // Every next-state element is bound to the value the circuit derives for a next-epoch step, so - // tampering all of them must implicate exactly those public rows and no others. The fixture is the - // committed step, which is accepted untampered. + // The fixture is the committed next-epoch step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let mut fixture = build_asset_backed_next_epoch_fixture(&mock_prover_setup); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs index 0c3a7ebf54e..52ba3823465 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/negative/same_epoch.rs @@ -94,9 +94,7 @@ mod slow { #[test] fn circuit_rejects_tampered_same_epoch_state_public_inputs() { - // Every next-state element is bound to the value the circuit derives for a same-epoch step, so - // tampering all of them must implicate exactly those public rows and no others. The fixture is the - // committed step, which is accepted untampered. + // The fixture is the committed same-epoch step, which is accepted untampered. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let mut fixture = build_asset_backed_same_epoch_fixture(&mock_prover_setup); diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs index da996498b7f..667314b24f5 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/positive.rs @@ -1,8 +1,8 @@ //! Positive transition tests. //! //! Fast tests verify the stored output proof of each transition context against the full verifier. -//! The slow `MockProver` checks in `slow` synthesize the current circuit over the stored inputs and -//! assert it accepts the stored expected output, which the stored proof alone cannot establish. +//! The slow checks synthesize the current circuit over the stored inputs and assert it accepts the +//! stored expected output, which the stored proof alone cannot establish. use midnight_circuits::types::Instantiable; @@ -94,9 +94,7 @@ mod slow { #[test] fn same_epoch_step_circuit_is_accepted() { - // Satisfiable canary for the same-epoch context: outside genesis the accumulator - // contributions are no longer gated away, so only a stored step whose accumulator the - // circuit can reproduce is accepted. + // Satisfiable baseline for the same-epoch negative case. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let fixture = build_asset_backed_same_epoch_fixture(&mock_prover_setup); @@ -110,7 +108,7 @@ mod slow { #[test] fn next_epoch_step_circuit_is_accepted() { - // Satisfiable canary for the next-epoch context. + // Satisfiable baseline for the next-epoch negative case. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_mock_prover_setup_from_assets(&setup); let fixture = build_asset_backed_next_epoch_fixture(&mock_prover_setup); From 53952e61b6007b13cbd8cdb684cb6e537486fa49 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Tue, 25 Aug 2026 10:06:03 +0900 Subject: [PATCH 08/11] docs(halo2_ivc): document the public-input layout enum variants --- .../halo2_ivc/tests/common/public_input_layout.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs index 5ccc984dab9..e1747df480b 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -15,10 +15,15 @@ pub(crate) const STATE_SECTION_ROWS: usize = 7; /// A field of the global root-of-trust section, in the order the circuit constrains it. #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub(crate) enum GlobalField { + /// Message the genesis signature was produced over. GenesisMessage, + /// X coordinate of the genesis verification key. GenesisVerificationKeyX, + /// Y coordinate of the genesis verification key. GenesisVerificationKeyY, + /// Transcript representation of the certificate circuit verifying key. CertificateCircuitVerificationKeyRepresentation, + /// Transcript representation of the recursive circuit verifying key. IvcCircuitVerificationKeyRepresentation, } @@ -56,12 +61,19 @@ impl GlobalField { /// A field of the next-state section, in the order the circuit constrains it. #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub(crate) enum StateField { + /// Number of recursive steps taken. StepCounter, + /// Message hash the step aggregates. Message, + /// Merkle-tree commitment the aggregated certificate was verified against. MerkleTreeCommitment, + /// Merkle-tree commitment decoded from the message preimage. NextMerkleTreeCommitment, + /// Protocol parameters in force for this step. ProtocolParameters, + /// Protocol parameters decoded from the message preimage. NextProtocolParameters, + /// Epoch decoded from the message preimage. CurrentEpoch, } From b96da8effe097f1e9435b22d6de1de544abed7a4 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Tue, 25 Aug 2026 10:06:04 +0900 Subject: [PATCH 09/11] test(halo2_ivc): pin the global public-input order with distinct sentinels --- .../tests/common/public_input_layout.rs | 78 ++++++++++++++++--- 1 file changed, 66 insertions(+), 12 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs index e1747df480b..20bedd01cb6 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -131,13 +131,19 @@ pub(crate) fn all_state_rows() -> BTreeMap { #[cfg(test)] mod tests { + use midnight_circuits::types::Instantiable; + use super::*; use crate::circuits::halo2_ivc::{ - NativeField, - state::State, - tests::common::asset_readers::load_embedded_verification_context_asset, + AssignedNativePoint, CircuitCurve, NativeField, + state::{Global, State}, + tests::common::asset_readers::{ + load_embedded_genesis_benchmark_fixture, load_embedded_verification_context_asset, + }, types::{ - EpochNumber, MerkleTreeCommitment, MessageHash, ProtocolParametersHash, StepCounter, + CertificateCircuitVerificationKeyRepresentation, EpochNumber, + IvcCircuitVerificationKeyRepresentation, MerkleTreeCommitment, MessageHash, + ProtocolParametersHash, StepCounter, }, }; @@ -155,14 +161,6 @@ mod tests { STATE_SECTION_ROWS, "state section length changed; every expected public-input row shifts with it" ); - for (offset, field) in GlobalField::ALL.iter().enumerate() { - assert_eq!( - field.row(), - offset, - "{} is not at global row {offset}", - field.name() - ); - } for (offset, field) in StateField::ALL.iter().enumerate() { assert_eq!( field.row(), @@ -179,6 +177,62 @@ mod tests { ); } + #[test] + fn global_public_input_order_matches_the_layout() { + // Distinct sentinels per settable field, so a reordering of `Global::as_public_input` or a + // name mapped to the wrong row fails here rather than producing a misleading signature. + const SENTINELS: [(GlobalField, u64); 3] = [ + (GlobalField::GenesisMessage, 11), + ( + GlobalField::CertificateCircuitVerificationKeyRepresentation, + 33, + ), + (GlobalField::IvcCircuitVerificationKeyRepresentation, 44), + ]; + + let fixture = load_embedded_genesis_benchmark_fixture() + .expect("genesis benchmark fixture should load"); + let genesis_verification_key = fixture.genesis_verification_key; + let global = Global { + genesis_message: MessageHash::from_field(NativeField::from(11u64)), + genesis_verification_key, + certificate_circuit_verification_key_representation: + CertificateCircuitVerificationKeyRepresentation::from_field(NativeField::from( + 33u64, + )), + ivc_circuit_verification_key_representation: + IvcCircuitVerificationKeyRepresentation::from_field(NativeField::from(44u64)), + }; + let public_input = global.as_public_input(); + + for (field, sentinel) in SENTINELS { + assert_eq!( + public_input[field.row()], + NativeField::from(sentinel), + "{} is not at global row {}", + field.name(), + field.row() + ); + } + + // The remaining two rows carry the key coordinates, in that order. + let key_coordinates = AssignedNativePoint::::as_public_input( + genesis_verification_key.as_jubjub_subgroup(), + ); + assert_eq!( + public_input[GlobalField::GenesisVerificationKeyX.row()], + key_coordinates[0], + "{} is not at its global row", + GlobalField::GenesisVerificationKeyX.name() + ); + assert_eq!( + public_input[GlobalField::GenesisVerificationKeyY.row()], + key_coordinates[1], + "{} is not at its global row", + GlobalField::GenesisVerificationKeyY.name() + ); + } + #[test] fn state_public_input_order_matches_the_layout() { // Each variant is paired with its own sentinel, so a variant naming the wrong field fails From 05b4ea293ec8eea8fb783c9ee2b32c2b5a99d956 Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Tue, 25 Aug 2026 10:06:04 +0900 Subject: [PATCH 10/11] test(halo2_ivc): cover the permitted failure class without should_panic --- .../tests/common/failure_signature.rs | 170 ++++++++++++++---- 1 file changed, 139 insertions(+), 31 deletions(-) diff --git a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs index d07e404bedb..7c1befbd4b3 100644 --- a/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -51,37 +51,39 @@ fn public_statement_row(failure: &VerifyFailure) -> Option { } } -/// Runs `MockProver` on any circuit, requires rejection, and asserts that the public-statement rows -/// implicated are exactly the keys of `expected_rows`. +/// Runs `MockProver` on any circuit and compares the resulting failure signature against +/// `expected_rows`, returning the diagnostic when they disagree. /// -/// `expected_rows` maps each row to the field name used in diagnostics. Every returned failure must -/// be a permutation failure, and every public-statement failure must carry an absolute row. +/// `expected_rows` maps each row to the field name used in diagnostics. The circuit must reject, +/// every returned failure must be a permutation failure, and every public-statement failure must +/// carry an absolute row. /// /// An exact row set does not prove each row carries the field named for it: dropping one /// public-input assignment shifts every later binding while all expected rows still fail, and two /// fields with equal honest values can swap invisibly. -pub(crate) fn assert_circuit_rejects_public_input_rows>( +fn check_public_input_row_signature>( circuit: &C, instances: Vec>, expected_rows: &BTreeMap, -) { +) -> Result<(), String> { let prover = MockProver::run(circuit, instances).expect("MockProver setup should succeed"); - let failures = prover - .verify() - .expect_err("the circuit should reject the provided circuit and instances"); + let Err(failures) = prover.verify() else { + return Err("the circuit should reject the provided circuit and instances".to_string()); + }; let unexpected_classes: Vec = failures .iter() .filter(|failure| !matches!(failure, VerifyFailure::Permutation { .. })) .map(|failure| format!("{failure:?}")) .collect(); - assert!( - unexpected_classes.is_empty(), - "every failure should be a permutation failure, since the public statement is bound by \ - copy constraints; got {} of another class:\n{}", - unexpected_classes.len(), - unexpected_classes.join("\n") - ); + if !unexpected_classes.is_empty() { + return Err(format!( + "every failure should be a permutation failure, since the public statement is bound by \ + copy constraints; got {} of another class:\n{}", + unexpected_classes.len(), + unexpected_classes.join("\n") + )); + } // A row-less public-statement failure would otherwise be dropped, letting an empty expected // signature pass on a circuit that had broken a binding. @@ -92,15 +94,19 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( }) .map(|failure| format!("{failure:?}")) .collect(); - assert!( - unlocatable.is_empty(), - "every public-statement failure should carry an absolute row; got {} that did not:\n{}", - unlocatable.len(), - unlocatable.join("\n") - ); + if !unlocatable.is_empty() { + return Err(format!( + "every public-statement failure should carry an absolute row; got {} that did not:\n{}", + unlocatable.len(), + unlocatable.join("\n") + )); + } let observed: BTreeSet = failures.iter().filter_map(public_statement_row).collect(); let expected: BTreeSet = expected_rows.keys().copied().collect(); + if observed == expected { + return Ok(()); + } let describe = |rows: &BTreeSet| { rows.iter() .map(|row| match expected_rows.get(row) { @@ -110,13 +116,22 @@ pub(crate) fn assert_circuit_rejects_public_input_rows>( .collect::>() .join(", ") }; - assert_eq!( - observed, - expected, + Err(format!( "public-input failure signature mismatch\n failed: [{}]\n expected: [{}]", describe(&observed), describe(&expected) - ); + )) +} + +/// Asserts the failure signature matches, panicking with the diagnostic when it does not. +pub(crate) fn assert_circuit_rejects_public_input_rows>( + circuit: &C, + instances: Vec>, + expected_rows: &BTreeMap, +) { + if let Err(diagnostic) = check_public_input_row_signature(circuit, instances, expected_rows) { + panic!("{diagnostic}"); + } } /// Recursive-circuit wrapper over [`assert_circuit_rejects_public_input_rows`]. @@ -136,7 +151,8 @@ pub(crate) fn assert_recursive_mock_prover_rejects_public_input_rows( mod tests { use midnight_proofs::{ circuit::{Layouter, SimpleFloorPlanner, Value}, - plonk::{Advice, Column, ConstraintSystem, Error, Instance}, + plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Instance, Selector}, + poly::Rotation, }; use super::*; @@ -147,6 +163,9 @@ mod tests { /// Public-statement row left deliberately unbound by the minimal circuit. const UNBOUND_PUBLIC_STATEMENT_ROW: usize = 2; + /// Value assigned by the gate-failure circuit, which its gate requires to be zero. + const GATE_FAILURE_VALUE: u64 = 5; + #[derive(Clone)] struct MinimalConfig { advice: Column, @@ -210,6 +229,67 @@ mod tests { } } + #[derive(Clone)] + struct GateFailureConfig { + advice: Column, + selector: Selector, + public_statement_instance: Column, + } + + /// Circuit whose only fault is an unsatisfied gate, with its public statement left consistent. + /// + /// The helper permits permutation failures alone, so this is what proves that rule is enforced. + struct GateFailureCircuit; + + impl Circuit for GateFailureCircuit { + type Config = GateFailureConfig; + type FloorPlanner = SimpleFloorPlanner; + type Params = (); + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let advice = meta.advice_column(); + let selector = meta.selector(); + // Declared first so the public statement lands in column one, as the recursive circuit does. + let _committed_instance = meta.instance_column(); + let public_statement_instance = meta.instance_column(); + meta.enable_equality(advice); + meta.enable_equality(public_statement_instance); + meta.create_gate("the assigned value must be zero", |meta| { + let value = meta.query_advice(advice, Rotation::cur()); + Constraints::with_selector(selector, vec![value]) + }); + GateFailureConfig { + advice, + selector, + public_statement_instance, + } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let cell = layouter.assign_region( + || "value", + |mut region| { + config.selector.enable(&mut region, 0)?; + region.assign_advice( + || "value", + config.advice, + 0, + || Value::known(NativeField::from(GATE_FAILURE_VALUE)), + ) + }, + )?; + layouter.constrain_instance(cell.cell(), config.public_statement_instance, 0) + } + } + /// `[committed, public statement]` instances satisfying the minimal circuit. fn honest_minimal_instances() -> Vec> { vec![ @@ -282,27 +362,55 @@ mod tests { } #[test] - #[should_panic(expected = "public-input failure signature mismatch")] + fn helper_rejects_a_non_permutation_failure() { + // The public statement matches, so the unsatisfied gate is the only fault and the helper + // must surface it rather than report an empty row set. + let diagnostic = check_public_input_row_signature( + &GateFailureCircuit, + vec![vec![], vec![NativeField::from(GATE_FAILURE_VALUE)]], + &BTreeMap::new(), + ) + .expect_err("a gate failure is not a permitted failure class"); + + assert!( + diagnostic.contains("every failure should be a permutation failure"), + "{diagnostic}" + ); + } + + #[test] fn helper_rejects_an_incomplete_expected_signature() { // Two rows fail, so expecting one must not pass. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 1); - assert_circuit_rejects_public_input_rows( + let diagnostic = check_public_input_row_signature( &MinimalCircuit, instances, &BTreeMap::from([(0, "first bound input")]), + ) + .expect_err("a row that failed unexpectedly should be reported"); + + assert!( + diagnostic.contains("public-input failure signature mismatch"), + "{diagnostic}" ); } #[test] - #[should_panic(expected = "public-input failure signature mismatch")] fn helper_rejects_an_empty_signature_when_a_row_did_fail() { // An empty expectation must not absorb a real public-statement failure. let mut instances = honest_minimal_instances(); mutate_public_input(&mut instances[PUBLIC_STATEMENT_INSTANCE_COLUMN], 0); - assert_circuit_rejects_public_input_rows(&MinimalCircuit, instances, &BTreeMap::new()); + let diagnostic = + check_public_input_row_signature(&MinimalCircuit, instances, &BTreeMap::new()) + .expect_err("a bound row that failed should be reported"); + + assert!( + diagnostic.contains("public-input failure signature mismatch"), + "{diagnostic}" + ); } } From 1b2d0520e42f136b2bfe7eaff687b7f5721ff62d Mon Sep 17 00:00:00 2001 From: Hamza Jeljeli Date: Wed, 26 Aug 2026 08:44:32 +0900 Subject: [PATCH 11/11] chore(stm): updated changelog and crate versions --- Cargo.lock | 2 +- mithril-common/Cargo.toml | 2 +- mithril-stm/CHANGELOG.md | 8 ++++++++ mithril-stm/Cargo.toml | 2 +- 4 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ccb2656d64c..f4585c5785f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4820,7 +4820,7 @@ dependencies = [ [[package]] name = "mithril-stm" -version = "0.12.8" +version = "0.12.9" dependencies = [ "anyhow", "blake2 0.10.6", diff --git a/mithril-common/Cargo.toml b/mithril-common/Cargo.toml index e6f426b8435..b30e55efe10 100644 --- a/mithril-common/Cargo.toml +++ b/mithril-common/Cargo.toml @@ -51,7 +51,7 @@ fixed = "1.31.0" hex = { workspace = true } kes-summed-ed25519 = { version = "0.2.1", features = ["serde_enabled", "sk_clone_enabled"] } mithril-merkle-tree = { path = "../internal/mithril-merkle-tree", version = "0.1.4" } -mithril-stm = { path = "../mithril-stm", version = "0.12.8", default-features = false } +mithril-stm = { path = "../mithril-stm", version = "0.12.9", default-features = false } nom = "8.0.0" rand_chacha = { workspace = true } rand_core = { workspace = true } diff --git a/mithril-stm/CHANGELOG.md b/mithril-stm/CHANGELOG.md index 33bace77b11..92881bed720 100644 --- a/mithril-stm/CHANGELOG.md +++ b/mithril-stm/CHANGELOG.md @@ -5,6 +5,14 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## 0.12.9 (08-26-2026) + +### Changed + +- Consolidated the recursive circuit `MockProver` negative tests into one case per transition context, so that the public-statement bindings of a context are covered by a single circuit synthesis instead of one per tampered field. +- Replaced the rejection-only assertions of the recursive circuit negative tests with exact failure signatures, so that each case now requires the circuit to reject through the expected failure class and to implicate exactly the expected public-statement rows. +- Rebuilt the non-genesis `MockProver` fixtures from the committed assets, which makes the same-epoch and next-epoch cases satisfiable when untampered and gives each of them an untampered canary. + ## 0.12.8 (08-20-2026) ### Changed diff --git a/mithril-stm/Cargo.toml b/mithril-stm/Cargo.toml index 89ea6218823..7bcbd177f23 100644 --- a/mithril-stm/Cargo.toml +++ b/mithril-stm/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "mithril-stm" -version = "0.12.8" +version = "0.12.9" edition = { workspace = true } authors = { workspace = true } homepage = { workspace = true }