chore: add some test for "failure" mod

privacy-scaling-explorations · Aug 6, 2024 · 671a802 · 671a802
1 parent 17a3f07
commit 671a802
Showing 1 changed file with 285 additions and 0 deletions.
diff --git a/halo2_frontend/src/dev/failure.rs b/halo2_frontend/src/dev/failure.rs
@@ -876,3 +876,288 @@ impl VerifyFailure {
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use halo2_middleware::poly::Rotation;
+    use halo2curves::pasta::Fp;
+
+    use crate::{
+        circuit::{Layouter, SimpleFloorPlanner, Value},
+        plonk::{Advice, Circuit, Error, Fixed, Selector},
+    };
+
+    use super::*;
+
+    #[test]
+    fn test_failure_constraint_not_satisfied() {
+        const K: u32 = 4;
+
+        #[derive(Clone)]
+        struct FaultyCircuitConfig {
+            a: Column<Advice>,
+            b: Column<Advice>,
+            c: Column<Advice>,
+            d: Column<Fixed>,
+            q: Selector,
+        }
+
+        struct FaultyCircuit {}
+
+        impl Circuit<Fp> for FaultyCircuit {
+            type Config = FaultyCircuitConfig;
+            type FloorPlanner = SimpleFloorPlanner;
+            #[cfg(feature = "circuit-params")]
+            type Params = ();
+
+            fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
+                let a = meta.advice_column();
+                let b = meta.advice_column();
+                let c = meta.advice_column();
+                let d = meta.fixed_column();
+                let q = meta.selector();
+
+                meta.create_gate("Equality check", |cells| {
+                    let a = cells.query_advice(a, Rotation::cur());
+                    let b = cells.query_advice(b, Rotation::cur());
+                    let c = cells.query_advice(c, Rotation::cur());
+                    let d = cells.query_fixed(d, Rotation::cur());
+                    let q = cells.query_selector(q);
+
+                    // If q is enabled, a and b must be assigned to.
+                    vec![q * (a - b) * (c - d)]
+                });
+
+                FaultyCircuitConfig { a, b, c, d, q }
+            }
+
+            fn without_witnesses(&self) -> Self {
+                Self {}
+            }
+
+            fn synthesize(
+                &self,
+                config: Self::Config,
+                mut layouter: impl Layouter<Fp>,
+            ) -> Result<(), Error> {
+                layouter.assign_region(
+                    || "Correct synthesis",
+                    |mut region| {
+                        // Enable the equality gate.
+                        config.q.enable(&mut region, 0)?;
+
+                        // Assign a = 1.
+                        region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?;
+
+                        // Assign b = 1.
+                        region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?;
+
+                        // Assign c = 5.
+                        region.assign_advice(
+                            || "c",
+                            config.c,
+                            0,
+                            || Value::known(Fp::from(5u64)),
+                        )?;
+                        // Assign d = 7.
+                        region.assign_fixed(
+                            || "d",
+                            config.d,
+                            0,
+                            || Value::known(Fp::from(7u64)),
+                        )?;
+                        Ok(())
+                    },
+                )?;
+                layouter.assign_region(
+                    || "Wrong synthesis",
+                    |mut region| {
+                        // Enable the equality gate.
+                        config.q.enable(&mut region, 0)?;
+
+                        // Assign a = 1.
+                        region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?;
+
+                        // Assign b = 0.
+                        region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::zero()))?;
+
+                        // Name Column a
+                        region.name_column(|| "This is Advice!", config.a);
+                        // Name Column b
+                        region.name_column(|| "This is Advice too!", config.b);
+
+                        // Assign c = 5.
+                        region.assign_advice(
+                            || "c",
+                            config.c,
+                            0,
+                            || Value::known(Fp::from(5u64)),
+                        )?;
+                        // Assign d = 7.
+                        region.assign_fixed(
+                            || "d",
+                            config.d,
+                            0,
+                            || Value::known(Fp::from(7u64)),
+                        )?;
+
+                        // Name Column c
+                        region.name_column(|| "Another one!", config.c);
+                        // Name Column d
+                        region.name_column(|| "This is a Fixed!", config.d);
+
+                        // Note that none of the terms cancel eachother. Therefore we will have a constraint that is non satisfied for
+                        // the `Equalty check` gate.
+                        Ok(())
+                    },
+                )
+            }
+        }
+
+        let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap();
+        let errs = prover.verify().unwrap_err();
+
+        assert_eq!(errs.len(), 1);
+        assert_eq!(
+            format!("{}", errs[0]),
+            r#####"Constraint 0 in gate 0 ('Equality check') is not satisfied in Region 1 ('Wrong synthesis') at offset 0
+- Column('Advice', 0 - This is Advice!)@0 = 1
+- Column('Advice', 1 - This is Advice too!)@0 = 0
+- Column('Advice', 2 - Another one!)@0 = 0x5
+- Column('Fixed', 0 - This is a Fixed!)@0 = 0x7
+"#####
+        );
+    }
+
+    #[test]
+    fn test_failure_cell_not_assigned() {
+        const K: u32 = 4;
+
+        #[derive(Clone)]
+        struct FaultyCircuitConfig {
+            a: Column<Advice>,
+            b: Column<Advice>,
+            c: Column<Advice>,
+            d: Column<Fixed>,
+            q: Selector,
+        }
+
+        struct FaultyCircuit {}
+
+        impl Circuit<Fp> for FaultyCircuit {
+            type Config = FaultyCircuitConfig;
+            type FloorPlanner = SimpleFloorPlanner;
+            #[cfg(feature = "circuit-params")]
+            type Params = ();
+
+            fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
+                let a = meta.advice_column();
+                let b = meta.advice_column();
+                let c = meta.advice_column();
+                let d = meta.fixed_column();
+                let q = meta.selector();
+
+                meta.create_gate("Equality check", |cells| {
+                    let a = cells.query_advice(a, Rotation::cur());
+                    let b = cells.query_advice(b, Rotation::cur());
+                    let c = cells.query_advice(c, Rotation::cur());
+                    let d = cells.query_fixed(d, Rotation::cur());
+                    let q = cells.query_selector(q);
+
+                    // If q is enabled, a and b must be assigned to.
+                    vec![q * (a - b) * (c - d)]
+                });
+
+                FaultyCircuitConfig { a, b, c, d, q }
+            }
+
+            fn without_witnesses(&self) -> Self {
+                Self {}
+            }
+
+            fn synthesize(
+                &self,
+                config: Self::Config,
+                mut layouter: impl Layouter<Fp>,
+            ) -> Result<(), Error> {
+                layouter.assign_region(
+                    || "Correct synthesis",
+                    |mut region| {
+                        // Enable the equality gate.
+                        config.q.enable(&mut region, 0)?;
+
+                        // Assign a = 1.
+                        region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?;
+
+                        // Assign b = 1.
+                        region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?;
+
+                        // Assign c = 5.
+                        region.assign_advice(
+                            || "c",
+                            config.c,
+                            0,
+                            || Value::known(Fp::from(5u64)),
+                        )?;
+                        // Assign d = 7.
+                        region.assign_fixed(
+                            || "d",
+                            config.d,
+                            0,
+                            || Value::known(Fp::from(7u64)),
+                        )?;
+                        Ok(())
+                    },
+                )?;
+                layouter.assign_region(
+                    || "Wrong synthesis",
+                    |mut region| {
+                        // Enable the equality gate.
+                        config.q.enable(&mut region, 0)?;
+
+                        // Assign a = 1.
+                        region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?;
+
+                        // Name Column a
+                        region.name_column(|| "This is Advice!", config.a);
+                        // Name Column b
+                        region.name_column(|| "This is Advice too!", config.b);
+
+                        // Assign c = 5.
+                        region.assign_advice(
+                            || "c",
+                            config.c,
+                            0,
+                            || Value::known(Fp::from(5u64)),
+                        )?;
+                        // Assign d = 7.
+                        region.assign_fixed(
+                            || "d",
+                            config.d,
+                            0,
+                            || Value::known(Fp::from(7u64)),
+                        )?;
+
+                        // Name Column c
+                        region.name_column(|| "Another one!", config.c);
+                        // Name Column d
+                        region.name_column(|| "This is a Fixed!", config.d);
+
+                        // Note that none of the terms cancel eachother. Therefore we will have a constraint that is non satisfied for
+                        // the `Equalty check` gate.
+                        Ok(())
+                    },
+                )
+            }
+        }
+
+        let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap();
+        let errs = prover.verify().unwrap_err();
+
+        assert_eq!(errs.len(), 2);
+        assert_eq!(
+            format!("{}", errs[0]),
+            r#####"Region 1 ('Wrong synthesis') uses Gate 0 ('Equality check') at offset 1, which requires cell in column Column { index: 1, column_type: Advice } at offset 0 with annotation Some("This is Advice too!") to be assigned."#####
+        );
+    }
+}