support PIL constant constraints in R1CS forcely

powdr-labs · Aug 8, 2023 · a3078ae · a3078ae
1 parent 9bce29f
commit a3078ae
Show file tree

Hide file tree

Showing 3 changed files with 96 additions and 25 deletions.
diff --git a/nova/Cargo.toml b/nova/Cargo.toml
@@ -14,7 +14,7 @@ log = "0.4.17"
 rand = "0.8.5"
 pasta_curves = { version = "0.5", features = ["repr-c", "serde"] }
 ast = { version = "0.1.0", path = "../ast" }
-nova-snark = { git = "https://github.com/hero78119/SuperNova.git", branch = "supernova_trait_mut", default-features = false, features = ["supernova"] }
+nova-snark = { git = "https://github.com/hero78119/SuperNova.git", branch = "supernova", default-features = false, features = ["supernova"] }
 bellperson = { version = "0.25", default-features = false}
 ff = { version = "0.13.0", features = ["derive"] }
 polyexen = { git = "https://github.com/Dhole/polyexen", branch = "feature/shuffles" }

diff --git a/nova/src/circuit_builder.rs b/nova/src/circuit_builder.rs
@@ -38,8 +38,8 @@ use crate::{
         util::Num,
     },
     utils::{
-        add_allocated_num, alloc_num_equals, alloc_one, alloc_zero, conditionally_select,
-        mul_allocated_num, WitnessGen,
+        add_allocated_num, alloc_const, alloc_num_equals, alloc_one, alloc_zero,
+        conditionally_select, mul_allocated_num, WitnessGen,
     },
 };
 
@@ -442,8 +442,23 @@ fn evaluate_expr<'a, T: FieldElement, F: PrimeFieldExt, CS: ConstraintSystem<F>>
             match op {
                 BinaryOperator::Add => add_allocated_num(cs, &lhe, &rhe),
                 BinaryOperator::Sub => {
-                    let neg = &rhe.mul(cs.namespace(|| "neg"), &poly_map.get("-1").unwrap())?;
-                    add_allocated_num(cs, &lhe, neg)
+                    let rhe_neg: AllocatedNum<F> =
+                        AllocatedNum::alloc(cs.namespace(|| "inv"), || {
+                            rhe.get_value()
+                                .map(|v| v.neg())
+                                .ok_or_else(|| SynthesisError::AssignmentMissing)
+                        })?;
+
+                    // (a + a_neg) * 1 = 0
+                    cs.enforce(
+                        || "(a + a_neg) * 1 = 0",
+                        |lc| lc + rhe.get_variable() + rhe_neg.get_variable(),
+                        |lc| lc + CS::one(),
+                        |lc| lc,
+                    );
+
+                    // let neg = &rhe.mul(cs.namespace(|| "neg"), &poly_map.get("-1").unwrap())?;
+                    add_allocated_num(cs, &lhe, &rhe_neg)
                 }
                 BinaryOperator::Mul => mul_allocated_num(cs, &lhe, &rhe),
                 _ => unimplemented!("{}", expr),
@@ -550,29 +565,23 @@ where
         // mapping <name| can be register, constant, ...> to AllocatedNum<F>
         let mut poly_map = BTreeMap::new();
 
-        // process constants and build map for its reference
-        // pc
+        // process pc
         poly_map.insert("pc".to_string(), _pc_counter.clone());
 
-        // TODO Fixme: constant can not be witness!!
+        // process constants and build map for its reference
         self.analyzed.constants.iter().try_for_each(|(k, v)| {
-            let a = AllocatedNum::alloc(cs.namespace(|| format!("{:x?}", v.to_string())), || {
-                let mut v_le = v.to_bytes_le();
-                v_le.resize(64, 0);
-                Ok(F::from_uniform(&v_le[..]))
-            })?;
-            poly_map.insert(k.clone(), a);
+            let mut v_le = v.to_bytes_le();
+            v_le.resize(64, 0);
+            let v = alloc_const(
+                cs.namespace(|| format!("const {:?}", v)),
+                F::from_uniform(&v_le[..]),
+                64,
+            )?;
+            poly_map.insert(k.clone(), v);
             Ok::<(), SynthesisError>(())
         })?;
-        // add constant -1
-        poly_map.insert(
-            "-1".to_string(),
-            AllocatedNum::alloc(cs.namespace(|| "constant -1"), || Ok(F::from(1).neg()))?,
-        );
         // add constant 1
-        poly_map.insert("1".to_string(), alloc_one(cs.namespace(|| "constant 1"))?);
-        // add constant 0
-        poly_map.insert("0".to_string(), alloc_zero(cs.namespace(|| "constant 0"))?);
+        poly_map.insert("ONE".to_string(), alloc_one(cs.namespace(|| "constant 1"))?);
 
         // parse inst part to construct step circuit
         // decompose ROM[pc] into linear combination lc(opcode_index, operand_index1, operand_index2, ... operand_output)
@@ -813,7 +822,7 @@ where
                                     add_allocated_num(
                                         cs.namespace(|| format!("instr {} pc + 1", identity_name)),
                                         &poly_map["pc"],
-                                        &poly_map["1"],
+                                        &poly_map["ONE"],
                                     )
                                     .unwrap()
                                 });

diff --git a/nova/src/utils.rs b/nova/src/utils.rs
@@ -2,6 +2,8 @@
 //! https://github.com/microsoft/Nova/blob/main/src/gadgets/mod.rs#L5
 use std::collections::BTreeMap;
 
+use crate::nonnative::util::Bit;
+
 #[allow(dead_code)]
 use super::nonnative::bignat::{nat_to_limbs, BigNat};
 use bellperson::{
@@ -10,9 +12,12 @@ use bellperson::{
         num::AllocatedNum,
         Assignment,
     },
-    ConstraintSystem, LinearCombination, SynthesisError,
+    ConstraintSystem, LinearCombination, SynthesisError, Variable,
+};
+use ff::{
+    derive::bitvec::{prelude::Lsb0, view::AsBits},
+    Field, PrimeField, PrimeFieldBits,
 };
-use ff::{Field, PrimeField, PrimeFieldBits};
 use nova_snark::traits::Group;
 use num_bigint::BigInt;
 use number::FieldElement;
@@ -79,6 +84,63 @@ pub fn alloc_one<F: PrimeField, CS: ConstraintSystem<F>>(
     Ok(one)
 }
 
+/// alloc a field num as a constant
+/// where every bit is deterministic constraint in R1CS
+pub fn alloc_const<F: PrimeField, CS: ConstraintSystem<F>>(
+    mut cs: CS,
+    value: F,
+    n_bits: usize,
+) -> Result<AllocatedNum<F>, SynthesisError> {
+    let allocations: Vec<Variable> = value.to_repr().as_bits::<Lsb0>()[0..n_bits]
+        .iter()
+        .map(|raw_bit| {
+            let bit = cs.alloc(
+                || "boolean",
+                || {
+                    if *raw_bit {
+                        Ok(F::ONE)
+                    } else {
+                        Ok(F::ZERO)
+                    }
+                },
+            )?;
+            if *raw_bit {
+                cs.enforce(
+                    || format!("bit{raw_bit} == 1"),
+                    |lc| lc + bit,
+                    |lc| lc + CS::one(),
+                    |lc| lc + CS::one(),
+                );
+            } else {
+                cs.enforce(
+                    || format!("bit{raw_bit} == 0"),
+                    |lc| lc + bit,
+                    |lc| lc + CS::one(),
+                    |lc| lc,
+                );
+            }
+            Ok(bit)
+        })
+        .collect::<Result<Vec<Variable>, SynthesisError>>()?;
+    let mut f = F::ONE;
+    let sum = allocations
+        .iter()
+        .fold(LinearCombination::zero(), |lc, bit| {
+            let l = lc + (f, *bit);
+            f = f.double();
+            l
+        });
+    let value = AllocatedNum::alloc(cs.namespace(|| "alloc const"), || Ok(value))?;
+    let sum_lc = LinearCombination::zero() + value.get_variable() - &sum;
+    cs.enforce(
+        || "sum - value = 0",
+        |lc| lc + &sum_lc,
+        |lc| lc + CS::one(),
+        |lc| lc,
+    );
+    Ok(value)
+}
+
 /// Allocate a scalar as a base. Only to be used is the scalar fits in base!
 pub fn alloc_scalar_as_base<G, CS>(
     mut cs: CS,