mirror of
https://github.com/arnaucube/Nova.git
synced 2026-01-10 16:11:29 +01:00
Verifier circuit (#23)
* ECC scalar multiplication (first draft) * fix clippy nits * start implementing the ro gadget: 1st design Poseidon + truncate * truncate to 128 bits * implement add + double in constraints * finish implementing constraints for ecc * cargo fmt * input of smul should be an array of bits * cleanup ro a bit. Make the challenge returned be a vec of allocated bits * switch to neptune 6.0 * start implementing high level circuit * incomplete version of the verifier circuit with many TODOS * optimize ecc ops. add i ==0 case to the circuit * fix 0/1 constants at the circuit * wrap CompressedGroupElement of Pallas and Vesta * cargo fmt * generate poseidon constants once instead of every time we call get_challenge * Implement RO-based poseidon to use outside of circuit. Reorganize the repo * add inner circuit to verification circuit * start adding folding of the io. there is an error in the first call to mult_mod * add test to check that bellperson-nonnative is compatible with nova * remove swap file * add another test that fails * add inputs to the circuits in tests * rename q to m in circuit.rs. add more tests in test_bellperson_non_native. change a in test_mult_mod to expose error * push test for equal_with_carried. fix the issue is src/r1cs.rs * cargo fmt + update the verifier circuit: add folding of X and update all hashes with X * make limb_width and n_limbs parameters * make params part of h1 * allocate the field order as constant. add check that z0 == zi when i == 0 * fix error in test_poseidon_ro * remove merge error * small fixes * small fixes to comments * clippy lints * small edits; rename tests * move inputize before from_num * _limbs --> _bn * _limbs --> _bn Co-authored-by: Ioanna <iontzialla@gmail.com>
This commit is contained in:
Srinath Setty
GitHub
50
tests/bit.rs
Normal file
50
tests/bit.rs
Normal file
@@ -0,0 +1,50 @@
|
||||
use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
|
||||
use ff::PrimeField;
|
||||
use nova_snark::bellperson::{
|
||||
r1cs::{NovaShape, NovaWitness},
|
||||
shape_cs::ShapeCS,
|
||||
solver::SatisfyingAssignment,
|
||||
};
|
||||
|
||||
fn synthesize_alloc_bit<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
|
||||
cs: &mut CS,
|
||||
) -> Result<(), SynthesisError> {
|
||||
//get two bits as input and check that they are indeed bits
|
||||
let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
|
||||
let _ = a.inputize(cs.namespace(|| "a is input"));
|
||||
cs.enforce(
|
||||
|| "check a is 0 or 1",
|
||||
|lc| lc + CS::one() - a.get_variable(),
|
||||
|lc| lc + a.get_variable(),
|
||||
|lc| lc,
|
||||
);
|
||||
let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
|
||||
let _ = b.inputize(cs.namespace(|| "b is input"));
|
||||
cs.enforce(
|
||||
|| "check b is 0 or 1",
|
||||
|lc| lc + CS::one() - b.get_variable(),
|
||||
|lc| lc + b.get_variable(),
|
||||
|lc| lc,
|
||||
);
|
||||
Ok(())
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_alloc_bit() {
|
||||
type G = pasta_curves::pallas::Point;
|
||||
|
||||
//First create the shape
|
||||
let mut cs: ShapeCS<G> = ShapeCS::new();
|
||||
let _ = synthesize_alloc_bit(&mut cs);
|
||||
let shape = cs.r1cs_shape();
|
||||
let gens = cs.r1cs_gens();
|
||||
println!("Mult mod constraint no: {}", cs.num_constraints());
|
||||
|
||||
//Now get the assignment
|
||||
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
|
||||
let _ = synthesize_alloc_bit(&mut cs);
|
||||
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
|
||||
|
||||
//Make sure that this is satisfiable
|
||||
assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
|
||||
}
|
||||
307
tests/nonnative.rs
Normal file
307
tests/nonnative.rs
Normal file
@@ -0,0 +1,307 @@
|
||||
use bellperson::{ConstraintSystem, SynthesisError};
|
||||
use bellperson_nonnative::{
|
||||
mp::bignat::BigNat,
|
||||
util::{convert::nat_to_f, num::Num},
|
||||
};
|
||||
use ff::PrimeField;
|
||||
use nova_snark::bellperson::{
|
||||
r1cs::{NovaShape, NovaWitness},
|
||||
shape_cs::ShapeCS,
|
||||
solver::SatisfyingAssignment,
|
||||
};
|
||||
use rug::Integer;
|
||||
|
||||
fn synthesize_is_equal<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
|
||||
cs: &mut CS,
|
||||
a_val: &Integer,
|
||||
limb_width: usize,
|
||||
n_limbs: usize,
|
||||
) -> Result<(), SynthesisError> {
|
||||
let a1 = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "alloc a2"),
|
||||
|| Ok(a_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = a1.inputize(cs.namespace(|| "make a input"));
|
||||
|
||||
let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
|
||||
Ok(nat_to_f(a_val).unwrap())
|
||||
})?;
|
||||
let a2 = BigNat::from_num(
|
||||
cs.namespace(|| "allocate a1_limbs"),
|
||||
a_num,
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
|
||||
let _ = a1.equal_when_carried(cs.namespace(|| "check equal"), &a2)?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
#[allow(clippy::too_many_arguments)]
|
||||
fn synthesize_mult_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
|
||||
cs: &mut CS,
|
||||
a_val: &Integer,
|
||||
b_val: &Integer,
|
||||
m_val: &Integer,
|
||||
q_val: &Integer,
|
||||
r_val: &Integer,
|
||||
limb_width: usize,
|
||||
n_limbs: usize,
|
||||
) -> Result<(), SynthesisError> {
|
||||
let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
|
||||
Ok(nat_to_f(a_val).unwrap())
|
||||
})?;
|
||||
let m = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "m"),
|
||||
|| Ok(m_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = m.inputize(cs.namespace(|| "modulus m"))?;
|
||||
|
||||
let a = BigNat::from_num(
|
||||
cs.namespace(|| "allocate a_limbs"),
|
||||
a_num,
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let b = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "b"),
|
||||
|| Ok(b_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let q = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "q"),
|
||||
|| Ok(q_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let r = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "r"),
|
||||
|| Ok(r_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let (qa, ra) = a.mult_mod(cs.namespace(|| "prod"), &b, &m)?;
|
||||
qa.equal(cs.namespace(|| "qcheck"), &q)?;
|
||||
ra.equal(cs.namespace(|| "rcheck"), &r)?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn synthesize_add<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
|
||||
cs: &mut CS,
|
||||
a_val: &Integer,
|
||||
b_val: &Integer,
|
||||
c_val: &Integer,
|
||||
limb_width: usize,
|
||||
n_limbs: usize,
|
||||
) -> Result<(), SynthesisError> {
|
||||
let a = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "a"),
|
||||
|| Ok(a_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = a.inputize(cs.namespace(|| "input a"))?;
|
||||
let b = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "b"),
|
||||
|| Ok(b_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = b.inputize(cs.namespace(|| "input b"))?;
|
||||
let c = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "c"),
|
||||
|| Ok(c_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let ca = a.add::<CS>(&b)?;
|
||||
ca.equal(cs.namespace(|| "ccheck"), &c)?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn synthesize_add_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
|
||||
cs: &mut CS,
|
||||
a_val: &Integer,
|
||||
b_val: &Integer,
|
||||
c_val: &Integer,
|
||||
m_val: &Integer,
|
||||
limb_width: usize,
|
||||
n_limbs: usize,
|
||||
) -> Result<(), SynthesisError> {
|
||||
let a = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "a"),
|
||||
|| Ok(a_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = a.inputize(cs.namespace(|| "input a"))?;
|
||||
let b = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "b"),
|
||||
|| Ok(b_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let _ = b.inputize(cs.namespace(|| "input b"))?;
|
||||
let c = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "c"),
|
||||
|| Ok(c_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let m = BigNat::alloc_from_nat(
|
||||
cs.namespace(|| "m"),
|
||||
|| Ok(m_val.clone()),
|
||||
limb_width,
|
||||
n_limbs,
|
||||
)?;
|
||||
let d = a.add::<CS>(&b)?;
|
||||
let ca = d.red_mod(cs.namespace(|| "reduce"), &m)?;
|
||||
ca.equal(cs.namespace(|| "ccheck"), &c)?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_mult_mod() {
|
||||
type G = pasta_curves::pallas::Point;
|
||||
|
||||
//Set the inputs
|
||||
let a_val = Integer::from_str_radix(
|
||||
"11572336752428856981970994795408771577024165681374400871001196932361466228192",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let b_val = Integer::from_str_radix(
|
||||
"87673389408848523602668121701204553693362841135953267897017930941776218798802",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let m_val = Integer::from_str_radix(
|
||||
"40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
|
||||
16,
|
||||
)
|
||||
.unwrap();
|
||||
let q_val = Integer::from_str_radix(
|
||||
"35048542371029440058224000662033175648615707461806414787901284501179083518342",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let r_val = Integer::from_str_radix(
|
||||
"26362617993085418618858432307761590013874563896298265114483698919121453084730",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
|
||||
//First create the shape
|
||||
let mut cs: ShapeCS<G> = ShapeCS::new();
|
||||
let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
|
||||
let shape = cs.r1cs_shape();
|
||||
let gens = cs.r1cs_gens();
|
||||
println!("Mult mod constraint no: {}", cs.num_constraints());
|
||||
|
||||
//Now get the assignment
|
||||
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
|
||||
let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
|
||||
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
|
||||
|
||||
//Make sure that this is satisfiable
|
||||
assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_add() {
|
||||
type G = pasta_curves::pallas::Point;
|
||||
|
||||
//Set the inputs
|
||||
let a_val = Integer::from_str_radix(
|
||||
"11572336752428856981970994795408771577024165681374400871001196932361466228192",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let b_val = Integer::from_str_radix("1", 10).unwrap();
|
||||
let c_val = Integer::from_str_radix(
|
||||
"11572336752428856981970994795408771577024165681374400871001196932361466228193",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
|
||||
//First create the shape
|
||||
let mut cs: ShapeCS<G> = ShapeCS::new();
|
||||
let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
|
||||
let shape = cs.r1cs_shape();
|
||||
let gens = cs.r1cs_gens();
|
||||
println!("Add mod constraint no: {}", cs.num_constraints());
|
||||
|
||||
//Now get the assignment
|
||||
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
|
||||
let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
|
||||
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
|
||||
|
||||
//Make sure that this is satisfiable
|
||||
assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_add_mod() {
|
||||
type G = pasta_curves::pallas::Point;
|
||||
|
||||
//Set the inputs
|
||||
let a_val = Integer::from_str_radix(
|
||||
"11572336752428856981970994795408771577024165681374400871001196932361466228192",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let b_val = Integer::from_str_radix("1", 10).unwrap();
|
||||
let c_val = Integer::from_str_radix(
|
||||
"11572336752428856981970994795408771577024165681374400871001196932361466228193",
|
||||
10,
|
||||
)
|
||||
.unwrap();
|
||||
let m_val = Integer::from_str_radix(
|
||||
"40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
|
||||
16,
|
||||
)
|
||||
.unwrap();
|
||||
|
||||
//First create the shape
|
||||
let mut cs: ShapeCS<G> = ShapeCS::new();
|
||||
let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
|
||||
let shape = cs.r1cs_shape();
|
||||
let gens = cs.r1cs_gens();
|
||||
println!("Add mod constraint no: {}", cs.num_constraints());
|
||||
|
||||
//Now get the assignment
|
||||
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
|
||||
let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
|
||||
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
|
||||
|
||||
//Make sure that this is satisfiable
|
||||
assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_equal() {
|
||||
type G = pasta_curves::pallas::Point;
|
||||
|
||||
//Set the inputs
|
||||
let a_val = Integer::from_str_radix("1157233675242885698197099479540877", 10).unwrap();
|
||||
|
||||
//First create the shape
|
||||
let mut cs: ShapeCS<G> = ShapeCS::new();
|
||||
let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
|
||||
let shape = cs.r1cs_shape();
|
||||
let gens = cs.r1cs_gens();
|
||||
println!("Equal constraint no: {}", cs.num_constraints());
|
||||
|
||||
//Now get the assignment
|
||||
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
|
||||
let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
|
||||
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
|
||||
|
||||
//Make sure that this is satisfiable
|
||||
assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
|
||||
}
|
||||
Reference in New Issue
Block a user