From 1a6468e730faee72967f3376ff902e4a8c7e7848 Mon Sep 17 00:00:00 2001 From: teddav Date: Tue, 18 Jun 2024 15:11:25 +0200 Subject: [PATCH] feat: MockProver cell override (#352) --- .github/workflows/coverage.yml | 2 +- halo2_frontend/src/dev.rs | 133 +++++++++++++++++++++++++++++ halo2_frontend/src/dev/failure.rs | 2 +- halo2_frontend/src/dev/metadata.rs | 2 +- halo2_proofs/src/lib.rs | 4 +- 5 files changed, 139 insertions(+), 4 deletions(-) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 21896f49de..5b19738928 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -16,7 +16,7 @@ jobs: - name: Generate code coverage run: cargo llvm-cov --all-features --workspace --lcov --output-path lcov.info - name: Upload coverage to Codecov - uses: codecov/codecov-action@v3 + uses: codecov/codecov-action@v4 with: token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos files: lcov.info diff --git a/halo2_frontend/src/dev.rs b/halo2_frontend/src/dev.rs index bdea7ec883..438648a18d 100644 --- a/halo2_frontend/src/dev.rs +++ b/halo2_frontend/src/dev.rs @@ -342,6 +342,18 @@ impl MockProver { } } +impl MockProver { + /// Return the content of an advice column as mutable + pub fn advice_mut(&mut self, column_index: usize) -> &mut [CellValue] { + self.advice[column_index].as_mut_slice() + } + + /// Return the content of an instance column as mutable + pub fn instance_mut(&mut self, column_index: usize) -> &mut [InstanceValue] { + self.instance[column_index].as_mut_slice() + } +} + impl Assignment for MockProver { fn enter_region(&mut self, name: N) where @@ -1246,6 +1258,7 @@ mod tests { use super::{FailureLocation, MockProver, VerifyFailure}; use crate::circuit::{Layouter, SimpleFloorPlanner, Value}; + use crate::dev::{CellValue, InstanceValue}; use crate::plonk::{ Advice, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Instance, Selector, TableColumn, @@ -2120,4 +2133,124 @@ mod tests { },]) ) } + + #[test] + fn modify_proof() { + const K: u32 = 4; + + struct EasyCircuit {} + + #[derive(Clone)] + struct EasyCircuitConfig { + a: Column, + b: Column, + q: Selector, + } + + impl Circuit for EasyCircuit { + type Config = EasyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let b = meta.instance_column(); + let q = meta.selector(); + + meta.enable_equality(a); + meta.enable_equality(b); + + meta.create_gate("squared", |cells| { + let cur = cells.query_advice(a, Rotation::cur()); + let next = cells.query_advice(a, Rotation::next()); + let q = cells.query_selector(q); + + vec![q * (next - cur.clone() * cur)] + }); + + EasyCircuitConfig { a, b, q } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let out = layouter.assign_region( + || "main region", + |mut region| { + config.q.enable(&mut region, 0)?; + config.q.enable(&mut region, 1)?; + + region.assign_advice(|| "a0", config.a, 0, || Value::known(Fp::from(3)))?; + region.assign_advice(|| "a1", config.a, 1, || Value::known(Fp::from(9)))?; + region.assign_advice(|| "a2", config.a, 2, || Value::known(Fp::from(81))) + }, + )?; + + layouter.constrain_instance(out.cell(), config.b, 0) + } + } + + let mut prover = MockProver::run(K, &EasyCircuit {}, vec![vec![Fp::from(81)]]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + + let err1 = VerifyFailure::ConstraintNotSatisfied { + constraint: ((0, "squared").into(), 0, "").into(), + location: FailureLocation::InRegion { + region: (0, "main region").into(), + offset: 1, + }, + cell_values: vec![ + ( + (ColumnMid::new(Any::Advice, 0), 0).into(), + "0x9".to_string(), + ), + ( + (ColumnMid::new(Any::Advice, 0), 1).into(), + "0xa".to_string(), + ), + ], + }; + + let err2 = VerifyFailure::Permutation { + column: ColumnMid::new(Any::Advice, 0), + location: FailureLocation::InRegion { + region: (0, "main region").into(), + offset: 2, + }, + }; + + // first we modify the instance -> this results in the permutation being unsatisfied + let instance = prover.instance_mut(0); + instance[0] = InstanceValue::Assigned(Fp::from(11)); + assert_eq!(prover.verify(), Err(vec![err2.clone()])); + + // then we modify the witness -> the contraint `squared` will fail + let advice0 = prover.advice_mut(0); + advice0[2] = CellValue::Assigned(Fp::from(10)); + assert_eq!(prover.verify(), Err(vec![err1, err2])); + + // we reset back to original values + let instance = prover.instance_mut(0); + instance[0] = InstanceValue::Assigned(Fp::from(81)); + let advice0 = prover.advice_mut(0); + advice0[2] = CellValue::Assigned(Fp::from(81)); + assert_eq!(prover.verify(), Ok(())); + + // and now we try to trick the verifier + // we assign on row 0 `Fp - 3`, which is also a square root of 9 + // but will overflow the prime field + let sqrt_9 = Fp::zero() - Fp::from(3); + let advice0 = prover.advice_mut(0); + advice0[0] = CellValue::Assigned(sqrt_9); + + // if this verifies correctly -> we have an issue and we are missing a range check + assert_eq!(prover.verify(), Ok(())); + } } diff --git a/halo2_frontend/src/dev/failure.rs b/halo2_frontend/src/dev/failure.rs index f7c663381c..a11d382afa 100644 --- a/halo2_frontend/src/dev/failure.rs +++ b/halo2_frontend/src/dev/failure.rs @@ -126,7 +126,7 @@ impl FailureLocation { } /// The reasons why a particular circuit is not satisfied. -#[derive(PartialEq, Eq)] +#[derive(PartialEq, Eq, Clone)] pub enum VerifyFailure { /// A cell used in an active gate was not assigned to. CellNotAssigned { diff --git a/halo2_frontend/src/dev/metadata.rs b/halo2_frontend/src/dev/metadata.rs index 291032ce3b..ca9152534a 100644 --- a/halo2_frontend/src/dev/metadata.rs +++ b/halo2_frontend/src/dev/metadata.rs @@ -46,7 +46,7 @@ impl fmt::Display for DebugColumn { /// A "virtual cell" is a PLONK cell that has been queried at a particular relative offset /// within a custom gate. -#[derive(Debug, PartialEq, Eq, PartialOrd, Ord)] +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] pub struct VirtualCell { name: String, pub(super) column: Column, diff --git a/halo2_proofs/src/lib.rs b/halo2_proofs/src/lib.rs index bb89e1d6fe..03386ea0e8 100644 --- a/halo2_proofs/src/lib.rs +++ b/halo2_proofs/src/lib.rs @@ -28,7 +28,9 @@ pub mod arithmetic { } /// Tools for developing circuits. pub mod dev { - pub use halo2_frontend::dev::{metadata, FailureLocation, MockProver, VerifyFailure}; + pub use halo2_frontend::dev::{ + metadata, CellValue, FailureLocation, InstanceValue, MockProver, VerifyFailure, + }; #[cfg(feature = "cost-estimator")] pub use halo2_frontend::dev::cost_model;