ZKR-4188-Fixed-Permutations-SMT-Solver (#56)

ZKR-4188-Fixed-Permutations-SMT-Solver

Cargo.toml

@@ -20,4 +20,4 @@ pse_halo2_proofs = { git = "https://github.com/Analyzable-Halo2/pse-halo2.git",
 axiom_halo2_proofs = { git = "https://github.com/Analyzable-Halo2/axiom-halo2.git", package = "halo2-axiom"}
 
 [patch."https://github.com/scroll-tech/halo2.git"]
-axiom_halo2_proofs = { git = "https://github.com/Analyzable-Halo2/scroll-halo2.git", package = "halo2_proofs"}
+scroll_halo2_proofs = { git = "https://github.com/Analyzable-Halo2/scroll-halo2.git", package = "halo2_proofs"}

korrekt/src/circuit_analyzer/abstract_expr.rs

@@ -110,11 +110,8 @@ pub fn eval_abstract<F: AnalyzableField>(
                 advice_query.column_index,
                 advice_query.rotation.0 + row_num + region_begin as i32
             );
-            //println!("term: {:?}", term);
-            //println!("cell_to_cycle_head: {:?}", cell_to_cycle_head);
             if cell_to_cycle_head.contains_key(&term) {
                 if cycle_abs_value.contains_key(&cell_to_cycle_head[&term.clone()]) {
-                    //println!("cycle_abs_value[&cell_to_cycle_head[&term]]: {:?}", cycle_abs_value[&cell_to_cycle_head[&term]]);
                     return Ok(cycle_abs_value[&cell_to_cycle_head[&term]]);
                 }
             }

korrekt/src/circuit_analyzer/analyzable.rs

@@ -207,7 +207,13 @@ impl<F: AnalyzableField> Assignment<F> for Analyzable<F> {
 
         if let Some(region) = self.current_region.as_mut() {
             region.update_extent(column.into(), row);
-            #[cfg(any(feature = "use_pse_halo2_proofs", feature = "use_pse_v1_halo2_proofs"))]
+            #[cfg(any(feature = "use_zcash_halo2_proofs",))]
+            region.cells.push((column.into(), row));
+            #[cfg(any(
+                feature = "use_pse_halo2_proofs",
+                feature = "use_pse_v1_halo2_proofs",
+                feature = "use_scroll_halo2_proofs",
+            ))]
             region
                 .cells
                 .entry((column.into(), row))

korrekt/src/sample_circuits/pse/lookup_circuits/lookup_underconstrained.rs

@@ -146,6 +146,8 @@ impl<F: PrimeField> FibonacciChip<F> {
                     || a_cell.value().copied() + b_cell.value(),
                 )?;
 
+                self.config.s_add.enable(&mut region, 1)?;
+
                 // assign the rest of rows
                 for row in 2..nrows {
                     b_cell.copy_advice(|| "a", &mut region, self.config.advice[0], row)?;

korrekt/src/sample_circuits/pse/mod.rs

@@ -1,3 +1,4 @@
 pub mod bit_decomposition;
 pub mod copy_constraint;
 pub mod lookup_circuits;
+pub mod simple;

korrekt/src/sample_circuits/pse/simple/mod.rs

@@ -0,0 +1,4 @@
+pub mod mul;
+pub mod no_selector;
+pub mod steps;
+pub mod steps_with_fixed;

korrekt/src/sample_circuits/pse/simple/mul.rs

@@ -0,0 +1,153 @@
+use group::ff::Field;
+use pse_halo2_proofs::circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value};
+use pse_halo2_proofs::plonk::{
+    Advice, Circuit, Column, ConstraintSystem, Error, Fixed, Instance, Selector,
+};
+use pse_halo2_proofs::poly::Rotation;
+use std::marker::PhantomData;
+
+#[derive(Debug, Clone)]
+pub struct MulConfig {
+    pub col_fixed: Column<Fixed>,
+    pub col_a: Column<Advice>,
+    pub col_b: Column<Advice>,
+    pub col_c: Column<Advice>,
+    pub selector: Selector,
+    pub instance: Column<Instance>,
+}
+
+#[derive(Debug, Clone)]
+struct MulChip<F: Field> {
+    config: MulConfig,
+    _marker: PhantomData<F>,
+}
+
+impl<F: Field> MulChip<F> {
+    pub fn construct(config: MulConfig) -> Self {
+        Self {
+            config,
+            _marker: PhantomData,
+        }
+    }
+
+    pub fn configure(meta: &mut ConstraintSystem<F>) -> MulConfig {
+        let col_fixed = meta.fixed_column();
+        let col_a = meta.advice_column();
+        let col_b = meta.advice_column();
+        let col_c = meta.advice_column();
+        let selector = meta.selector();
+        let instance = meta.instance_column();
+
+        meta.enable_constant(col_fixed);
+        meta.enable_equality(col_a);
+        meta.enable_equality(col_b);
+        meta.enable_equality(col_c);
+        meta.enable_equality(instance);
+
+        // computes c = -a^2
+        meta.create_gate("mul", |meta| {
+            //
+            // col_fixed | col_a | col_b | col_c | selector
+            //      f       a      b        c       s
+            //
+            let s = meta.query_selector(selector);
+            let f = meta.query_fixed(col_fixed, Rotation::cur());
+            let a = meta.query_advice(col_a, Rotation::cur());
+            let b = meta.query_advice(col_b, Rotation::cur());
+            let c = meta.query_advice(col_c, Rotation::cur());
+
+            vec![s.clone() * (f * a.clone() - b.clone()), s * (a * b - c)]
+        });
+
+        MulConfig {
+            col_fixed,
+            col_a,
+            col_b,
+            col_c,
+            selector,
+            instance,
+        }
+    }
+
+    #[allow(clippy::type_complexity)]
+    pub fn assign_first_row(
+        &self,
+        mut layouter: impl Layouter<F>,
+    ) -> Result<AssignedCell<F, F>, Error> {
+        layouter.assign_region(
+            || "first row",
+            |mut region| {
+                self.config.selector.enable(&mut region, 0)?;
+
+                let fixed_cell = region.assign_fixed(
+                    || "-1",
+                    self.config.col_fixed,
+                    0,
+                    || -> Value<F> { Value::known(-F::ONE) },
+                )?;
+
+                let a_cell = region.assign_advice_from_instance(
+                    || "a",
+                    self.config.instance,
+                    0,
+                    self.config.col_a,
+                    0,
+                )?;
+
+                let b_cell = region.assign_advice(
+                    || "-1 * a",
+                    self.config.col_b,
+                    0,
+                    || a_cell.value().copied() * fixed_cell.value(),
+                )?;
+
+                let c_cell = region.assign_advice(
+                    || "a * b",
+                    self.config.col_c,
+                    0,
+                    || a_cell.value().copied() * b_cell.value(),
+                )?;
+
+                Ok(c_cell)
+            },
+        )
+    }
+
+    pub fn expose_public(
+        &self,
+        mut layouter: impl Layouter<F>,
+        cell: &AssignedCell<F, F>,
+        row: usize,
+    ) -> Result<(), Error> {
+        layouter.constrain_instance(cell.cell(), self.config.instance, row)
+    }
+}
+
+#[derive(Default)]
+pub struct MulCircuit<F>(pub PhantomData<F>);
+
+impl<F: Field> Circuit<F> for MulCircuit<F> {
+    type Config = MulConfig;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn without_witnesses(&self) -> Self {
+        Self::default()
+    }
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+        MulChip::configure(meta)
+    }
+
+    fn synthesize(
+        &self,
+        config: Self::Config,
+        mut layouter: impl Layouter<F>,
+    ) -> Result<(), Error> {
+        let chip = MulChip::construct(config);
+
+        let prev_c = chip.assign_first_row(layouter.namespace(|| "first row"))?;
+
+        chip.expose_public(layouter.namespace(|| "out"), &prev_c, 1)?;
+        Ok(())
+    }
+}

korrekt/src/sample_circuits/pse/simple/no_selector.rs

@@ -0,0 +1,145 @@
+use group::ff::Field;
+use pse_halo2_proofs::circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value};
+use pse_halo2_proofs::plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed, Instance};
+use pse_halo2_proofs::poly::Rotation;
+use std::marker::PhantomData;
+
+#[derive(Debug, Clone)]
+pub struct MulConfig {
+    pub col_fixed: Column<Fixed>,
+    pub col_a: Column<Advice>,
+    pub col_b: Column<Advice>,
+    pub col_c: Column<Advice>,
+    pub instance: Column<Instance>,
+}
+
+#[derive(Debug, Clone)]
+struct MulChip<F: Field> {
+    config: MulConfig,
+    _marker: PhantomData<F>,
+}
+
+impl<F: Field> MulChip<F> {
+    pub fn construct(config: MulConfig) -> Self {
+        Self {
+            config,
+            _marker: PhantomData,
+        }
+    }
+
+    pub fn configure(meta: &mut ConstraintSystem<F>) -> MulConfig {
+        let col_fixed = meta.fixed_column();
+        let col_a = meta.advice_column();
+        let col_b = meta.advice_column();
+        let col_c = meta.advice_column();
+        let instance = meta.instance_column();
+
+        meta.enable_constant(col_fixed);
+        meta.enable_equality(col_a);
+        meta.enable_equality(col_b);
+        meta.enable_equality(col_c);
+        meta.enable_equality(instance);
+
+        // computes c = -a^2
+        meta.create_gate("mul", |meta| {
+            //
+            // col_fixed | col_a | col_b | col_c
+            //      f       a      b        c
+            //
+            let f = meta.query_fixed(col_fixed, Rotation::cur());
+            let a = meta.query_advice(col_a, Rotation::cur());
+            let b = meta.query_advice(col_b, Rotation::cur());
+            let c = meta.query_advice(col_c, Rotation::cur());
+
+            vec![(f * a.clone() - b.clone()), (a * b - c)]
+        });
+
+        MulConfig {
+            col_fixed,
+            col_a,
+            col_b,
+            col_c,
+            instance,
+        }
+    }
+
+    #[allow(clippy::type_complexity)]
+    pub fn assign_first_row(
+        &self,
+        mut layouter: impl Layouter<F>,
+    ) -> Result<AssignedCell<F, F>, Error> {
+        layouter.assign_region(
+            || "first row",
+            |mut region| {
+                let fixed_cell = region.assign_fixed(
+                    || "-1",
+                    self.config.col_fixed,
+                    0,
+                    || -> Value<F> { Value::known(-F::ONE) },
+                )?;
+
+                let a_cell = region.assign_advice_from_instance(
+                    || "a",
+                    self.config.instance,
+                    0,
+                    self.config.col_a,
+                    0,
+                )?;
+
+                let b_cell = region.assign_advice(
+                    || "-1 * a",
+                    self.config.col_b,
+                    0,
+                    || a_cell.value().copied() * fixed_cell.value(),
+                )?;
+
+                let c_cell = region.assign_advice(
+                    || "a * b",
+                    self.config.col_c,
+                    0,
+                    || a_cell.value().copied() * b_cell.value(),
+                )?;
+
+                Ok(c_cell)
+            },
+        )
+    }
+
+    pub fn expose_public(
+        &self,
+        mut layouter: impl Layouter<F>,
+        cell: &AssignedCell<F, F>,
+        row: usize,
+    ) -> Result<(), Error> {
+        layouter.constrain_instance(cell.cell(), self.config.instance, row)
+    }
+}
+
+#[derive(Default)]
+pub struct MulCircuit<F>(pub PhantomData<F>);
+
+impl<F: Field> Circuit<F> for MulCircuit<F> {
+    type Config = MulConfig;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn without_witnesses(&self) -> Self {
+        Self::default()
+    }
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+        MulChip::configure(meta)
+    }
+
+    fn synthesize(
+        &self,
+        config: Self::Config,
+        mut layouter: impl Layouter<F>,
+    ) -> Result<(), Error> {
+        let chip = MulChip::construct(config);
+
+        let prev_c = chip.assign_first_row(layouter.namespace(|| "first row"))?;
+
+        chip.expose_public(layouter.namespace(|| "out"), &prev_c, 1)?;
+        Ok(())
+    }
+}