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 } 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..7c1befbd4b3 --- /dev/null +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/failure_signature.rs @@ -0,0 +1,416 @@ +//! Classifies `MockProver` failures by the public-statement rows they implicate. +//! +//! 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}; + +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. +/// +/// 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 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); +} + +/// 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 sit 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 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. 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. +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 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(); + 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. + let unlocatable: Vec = failures + .iter() + .filter(|failure| { + is_public_statement_failure(failure) && public_statement_row(failure).is_none() + }) + .map(|failure| format!("{failure:?}")) + .collect(); + 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) { + Some(name) => format!("{row} ({name})"), + None => format!("{row} (not expected to fail)"), + }) + .collect::>() + .join(", ") + }; + 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`]. +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, Constraints, Error, Instance, Selector}, + poly::Rotation, + }; + + 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; + + /// 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, + committed_instance: Column, + public_statement_instance: Column, + } + + /// Smallest circuit reproducing the two-instance-column shape of the recursive circuit. + /// + /// 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 { + 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) + } + } + + #[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![ + 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 mutation_gives_equal_valued_rows_distinct_nonzero_deltas() { + // 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() { + 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() { + // 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 + .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(); + // 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 break confined to the committed column implicates no public-statement row. + let mut instances = honest_minimal_instances(); + mutate_public_input(&mut instances[0], 0); + + assert_circuit_rejects_public_input_rows(&MinimalCircuit, instances, &BTreeMap::new()); + } + + #[test] + 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); + + 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] + 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); + + 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}" + ); + } +} 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 256f534dba2..855e1ff016e 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, @@ -127,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( @@ -156,21 +145,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: @@ -273,16 +247,133 @@ pub(crate) fn prepare_stored_step_certificate_accumulator( certificate_accumulator } -/// Builds an `IvcCircuitData` with empty proof slots and a trivial accumulator for -/// MockProver-based constraint checks. +/// A non-genesis MockProver stimulus assembled from committed step assets. +/// +/// 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, + /// 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. +/// +/// 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, + 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; + + // Reports cross-asset drift directly rather than as 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 +/// 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( +/// 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, 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, @@ -296,8 +387,10 @@ 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, correct only at genesis. +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/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..20bedd01cb6 --- /dev/null +++ b/mithril-stm/src/circuits/halo2_ivc/tests/common/public_input_layout.rs @@ -0,0 +1,277 @@ +//! Row indices of the recursive circuit's public statement. +//! +//! 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; + +/// 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 { + /// 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, +} + +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 { + /// 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, +} + +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 +} + +/// 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 midnight_circuits::types::Instantiable; + + use super::*; + use crate::circuits::halo2_ivc::{ + AssignedNativePoint, CircuitCurve, NativeField, + state::{Global, State}, + tests::common::asset_readers::{ + load_embedded_genesis_benchmark_fixture, load_embedded_verification_context_asset, + }, + types::{ + CertificateCircuitVerificationKeyRepresentation, EpochNumber, + IvcCircuitVerificationKeyRepresentation, 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 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 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 + // 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() + ); + } + } +} 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..4ba16224069 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_mock_prover_public_inputs, - build_mock_prover_setup_from_assets, build_trivial_mock_prover_circuit, - 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,66 +195,113 @@ 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 a decoded field. + /// + /// 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. + /// + /// 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, + 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` implicates the message row and `field`'s row. + /// + /// 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); 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 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); - assert_recursive_mock_prover_rejects_with_label( + 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, + ); + + 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_mock_prover_public_inputs(&mock_prover_setup, &next_state); + fn circuit_rejects_wrong_next_merkle_tree_commitment_byte_range() { + // 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_trivial_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 + // 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, + 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_mock_prover_public_inputs(&mock_prover_setup, &next_state); + 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_trivial_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())]), ); } } 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..f8b384ec58e 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 with +//! the positive transition tests. use midnight_circuits::types::Instantiable; use sha2::{Digest, Sha256}; @@ -21,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, }, }; @@ -147,21 +146,18 @@ 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); - 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/accumulator.rs b/mithril-stm/src/circuits/halo2_ivc/tests/in_circuit/accumulator.rs index 2ce40d7b1fe..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 @@ -87,29 +87,36 @@ 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 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, and they are randomized. let setup = build_asset_generation_setup_from_cache(); let mock_prover_setup = build_recursive_mock_prover_setup(&setup); @@ -144,16 +151,34 @@ 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); + // 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(), + "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, + ); } } 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..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 @@ -1,19 +1,19 @@ //! 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 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). //! `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..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,24 +1,19 @@ -//! 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 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; 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 +113,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/mod.rs b/mithril-stm/src/circuits/halo2_ivc/tests/transitions/mod.rs index faea99823e8..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,9 +1,11 @@ //! 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, per transition +//! context. +//! +//! 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 d0bd22c84cb..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 @@ -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,50 @@ 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() { + // 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); + 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..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 @@ -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,31 @@ 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() { + // 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 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..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 @@ -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,31 @@ 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() { + // 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 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, ); } } 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..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,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 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; @@ -78,3 +82,41 @@ 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 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); + + 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 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); + + assert_recursive_mock_prover_accepts_with_label( + fixture.ivc_circuit_data, + fixture.public_inputs, + "next-epoch step from committed assets", + ); + } +}