Add test cases for lookup

pnyda · Jan 27, 2025 · b975ccf · b975ccf
1 parent 43f506a
commit b975ccf
Showing 1 changed file with 244 additions and 0 deletions.
diff --git a/src/lib.rs b/src/lib.rs
@@ -1182,4 +1182,248 @@ mod tests {
             layouter.constrain_instance(output.cell(), config.instance_column, 0)
         }
     }
+
+    #[derive(Debug, Clone)]
+    struct RangeConfig {
+        table: TableColumn,
+        advice: Column<Advice>,
+    }
+
+    #[derive(Debug)]
+    struct RangeCircuit {
+        bytes: Vec<Fp>,
+    }
+
+    impl Circuit<Fp> for RangeCircuit {
+        type Config = RangeConfig;
+        type FloorPlanner = SimpleFloorPlanner;
+
+        fn without_witnesses(&self) -> Self {
+            Self { bytes: Vec::new() }
+        }
+
+        fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
+            let advice = meta.advice_column();
+            let table = meta.lookup_table_column();
+
+            meta.lookup(|gate| {
+                let advice = gate.query_advice(advice, Rotation::cur());
+                vec![(advice, table)]
+            });
+
+            Self::Config { advice, table }
+        }
+
+        fn synthesize(
+            &self,
+            config: Self::Config,
+            mut layouter: impl Layouter<Fp>,
+        ) -> Result<(), Error> {
+            layouter.assign_region(
+                || "aa",
+                |mut region| {
+                    for (i, byte) in self.bytes.iter().enumerate() {
+                        region.assign_advice(|| "bb", config.advice, i, || Value::known(*byte))?;
+                    }
+                    Ok(())
+                },
+            )?;
+
+            layouter.assign_table(
+                || "range check",
+                |mut table| {
+                    for i in 0..(1 << 8) {
+                        table.assign_cell(
+                            || "a byte",
+                            config.table,
+                            i,
+                            || Value::known(Fp::from(i as u64)),
+                        )?;
+                    }
+                    Ok(())
+                },
+            )?;
+
+            Ok(())
+        }
+    }
+
+    // tests for the cases where the lookup input is a simple query
+    #[test]
+    fn test_range_success() -> Result<(), Error> {
+        let k = 9;
+        let circuit = RangeCircuit {
+            bytes: vec![1.into(), 2.into(), 3.into(), 255.into()],
+        };
+        let (ccs, z, lookups) = convert_halo2_circuit::<_, _, ark_pallas::Fq>(k, &circuit, &[])?;
+
+        let prover = MockProver::run(k, &circuit, vec![]).unwrap();
+        assert_eq!(prover.verify(), Ok(()));
+        assert!(is_zero_vec(&ccs.eval_at_z(&z).unwrap()));
+
+        let is_lookup_satisfied = lookups.into_iter().all(|(z_indices, table)| {
+            z_indices
+                .into_iter()
+                .map(|z_index| z[z_index])
+                .collect::<HashSet<_>>()
+                .is_subset(&table)
+        });
+        assert!(is_lookup_satisfied);
+
+        Ok(())
+    }
+
+    #[test]
+    fn test_range_failure() -> Result<(), Error> {
+        let k = 9;
+        let circuit = RangeCircuit {
+            bytes: vec![1.into(), 2.into(), 3.into(), 256.into()],
+        };
+        let (ccs, z, lookups) = convert_halo2_circuit::<_, _, ark_pallas::Fq>(k, &circuit, &[])?;
+
+        let prover = MockProver::run(k, &circuit, vec![]).unwrap();
+        assert!(prover.verify().is_err());
+
+        let is_lookup_satisfied = lookups.into_iter().all(|(z_indices, table)| {
+            z_indices
+                .into_iter()
+                .map(|z_index| z[z_index])
+                .collect::<HashSet<_>>()
+                .is_subset(&table)
+        });
+        assert!(!is_lookup_satisfied);
+
+        Ok(())
+    }
+
+    #[derive(Debug)]
+    struct LessThanCircuit {
+        less_than_200: Vec<Fp>,
+    }
+
+    #[derive(Debug, Clone)]
+    struct LessThanConfig {
+        table: TableColumn,
+        advice: Column<Advice>,
+        is_enabled: Column<Fixed>,
+    }
+
+    impl Circuit<Fp> for LessThanCircuit {
+        type Config = LessThanConfig;
+        type FloorPlanner = SimpleFloorPlanner;
+
+        fn without_witnesses(&self) -> Self {
+            Self {
+                less_than_200: Vec::new(),
+            }
+        }
+
+        fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
+            let advice = meta.advice_column();
+            let table = meta.lookup_table_column();
+            let is_enabled = meta.fixed_column();
+
+            meta.lookup(|gate| {
+                let advice = gate.query_advice(advice, Rotation::cur());
+                let is_enabled = gate.query_fixed(is_enabled);
+                vec![(
+                    is_enabled * (advice + Expression::Constant(Fp::from(56))),
+                    table,
+                )]
+            });
+
+            Self::Config {
+                advice,
+                table,
+                is_enabled,
+            }
+        }
+
+        fn synthesize(
+            &self,
+            config: Self::Config,
+            mut layouter: impl Layouter<Fp>,
+        ) -> Result<(), Error> {
+            layouter.assign_region(
+                || "aa",
+                |mut region| {
+                    for (i, byte) in self.less_than_200.iter().enumerate() {
+                        region.assign_fixed(
+                            || "cc",
+                            config.is_enabled,
+                            i,
+                            || Value::known(Fp::ONE),
+                        )?;
+                        region.assign_advice(|| "bb", config.advice, i, || Value::known(*byte))?;
+                    }
+                    Ok(())
+                },
+            )?;
+
+            layouter.assign_table(
+                || "range check",
+                |mut table| {
+                    for i in 0..(1 << 8) {
+                        table.assign_cell(
+                            || "a byte",
+                            config.table,
+                            i,
+                            || Value::known(Fp::from(i as u64)),
+                        )?;
+                    }
+                    Ok(())
+                },
+            )?;
+
+            Ok(())
+        }
+    }
+
+    // tests for the cases where the lookup input is a complex Expression
+    #[test]
+    fn test_less_than_success() -> Result<(), Error> {
+        let k = 9;
+        let circuit = LessThanCircuit {
+            less_than_200: vec![1.into(), 2.into(), 3.into(), 199.into()],
+        };
+        let (ccs, z, lookups) = convert_halo2_circuit::<_, _, ark_pallas::Fq>(k, &circuit, &[])?;
+
+        let prover = MockProver::run(k, &circuit, vec![]).unwrap();
+        assert_eq!(prover.verify(), Ok(()));
+        assert!(is_zero_vec(&ccs.eval_at_z(&z).unwrap()));
+
+        let is_lookup_satisfied = lookups.into_iter().all(|(z_indices, table)| {
+            z_indices
+                .into_iter()
+                .map(|z_index| z[z_index])
+                .collect::<HashSet<_>>()
+                .is_subset(&table)
+        });
+        assert!(is_lookup_satisfied);
+
+        Ok(())
+    }
+
+    #[test]
+    fn test_less_than_failure() -> Result<(), Error> {
+        let k = 9;
+        let circuit = LessThanCircuit {
+            less_than_200: vec![1.into(), 2.into(), 3.into(), 200.into()],
+        };
+        let (_, z, lookups) = convert_halo2_circuit::<_, _, ark_pallas::Fq>(k, &circuit, &[])?;
+
+        let prover = MockProver::run(k, &circuit, vec![]).unwrap();
+        assert!(prover.verify().is_err());
+
+        let is_lookup_satisfied = lookups.into_iter().all(|(z_indices, table)| {
+            z_indices
+                .into_iter()
+                .map(|z_index| z[z_index])
+                .collect::<HashSet<_>>()
+                .is_subset(&table)
+        });
+        assert!(!is_lookup_satisfied);
+
+        Ok(())
+    }
 }