From a35c65ab18c76b2219c8921542e7d0a56d6da334 Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Tue, 8 Aug 2023 22:21:44 +0800 Subject: [PATCH] fix soundness by constaint constant forcely --- nova/Cargo.toml | 2 +- nova/src/circuit_builder.rs | 53 ++++++++++++++++------------- nova/src/utils.rs | 66 +++++++++++++++++++++++++++++++++++-- 3 files changed, 96 insertions(+), 25 deletions(-) diff --git a/nova/Cargo.toml b/nova/Cargo.toml index 322edfe8e8..5dd8e8370b 100644 --- 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 index 49fd39db56..5ec4c223f2 100644 --- 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> 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 = + 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 to AllocatedNum 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 index c9ea14f6fd..4fc3beb1c1 100644 --- 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>( Ok(one) } +/// alloc a field num as a constant +/// where every bit is deterministic constraint in R1CS +pub fn alloc_const>( + mut cs: CS, + value: F, + n_bits: usize, +) -> Result, SynthesisError> { + let allocations: Vec = value.to_repr().as_bits::()[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::, 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() - ∑ + 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( mut cs: CS,