diff --git a/Cargo.toml b/Cargo.toml index 99e0a0b..bc3f456 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "nova-snark" -version = "0.5.0" +version = "0.6.0" authors = ["Srinath Setty "] edition = "2021" description = "Recursive zkSNARKs without trusted setup" diff --git a/README.md b/README.md index 56b872c..acc2bfd 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,8 @@ # Nova: Recursive SNARKs without trusted setup -Nova is a high-speed recursive SNARK (a SNARK is type cryptographic proof system that enables a prover to prove a mathematical statement to a verifier with a short proof and succinct verification, and a recursive SNARK enables producing proofs that prove statements about prior proofs). The details of Nova are described in our [paper](https://eprint.iacr.org/2021/370). Recursive SNARKs including Nova have a wide variety of applications such as constructions of verifiable delay functions (VDFs), succinct blockchains, and incrementally verifiable versions of [verifiable state machines](https://eprint.iacr.org/2020/758.pdf). A distinctive aspect of Nova is that it is the simplest recursive proof system in the literature. Furthermore, it achieves the smallest verifier circuit (a key metric to minimize in this context): the circuit is constant-sized and its size is dominated by two group scalar multiplications. +Nova is a high-speed recursive SNARK (a SNARK is type cryptographic proof system that enables a prover to prove a mathematical statement to a verifier with a short proof and succinct verification, and a recursive SNARK enables producing proofs that prove statements about prior proofs). + +Recursive SNARKs including Nova have a wide variety of applications such as Rollups, verifiable delay functions (VDFs), succinct blockchains, and incrementally verifiable versions of [verifiable state machines](https://eprint.iacr.org/2020/758.pdf). A distinctive aspect of Nova is that it is the simplest recursive proof system in the literature, yet it provides the fastest prover. Furthermore, it achieves the smallest verifier circuit (a key metric to minimize in this context): the circuit is constant-sized and its size is dominated by two group scalar multiplications. The details of Nova are described in our CRYPTO 2022 [paper](https://eprint.iacr.org/2021/370). This repository provides `nova-snark,` a Rust library implementation of Nova. @@ -12,11 +14,10 @@ cargo test ## References [Nova: Recursive Zero-Knowledge Arguments from Folding Schemes](https://eprint.iacr.org/2021/370) \ Abhiram Kothapalli, Srinath Setty, and Ioanna Tzialla \ -Cryptology ePrint Archive: Report 2021/370 +CRYPTO 2022 -## Acknowledgements -The first version of the code was written by: Abhiram Kothapalli, Srinath Setty, and Ioanna Tzialla. -The latest code includes code contributions from Chhi'mèd Künzang and Friedel Ziegelmayer. +## Acknowledgments +See the contributors list [here](https://github.com/microsoft/Nova/graphs/contributors) ## Contributing diff --git a/src/bellperson/mod.rs b/src/bellperson/mod.rs index 12da92f..7d7e80e 100644 --- a/src/bellperson/mod.rs +++ b/src/bellperson/mod.rs @@ -5,3 +5,428 @@ pub mod r1cs; pub mod shape_cs; pub mod solver; + +#[cfg(test)] +mod tests { + use crate::bellperson::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, + }; + use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; + use bellperson_nonnative::{ + mp::bignat::BigNat, + util::{convert::nat_to_f, num::Num}, + }; + use ff::PrimeField; + use num_bigint::BigInt; + use num_traits::Num as OtherNum; + + fn synthesize_alloc_bit>( + 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 = 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 = 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()); + } + + fn synthesize_use_cs_one>( + cs: &mut CS, + ) -> Result<(), SynthesisError> { + let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; + let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; + cs.enforce( + || "check a = b", + |lc| lc + a.get_variable() - b.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + let _ = a.inputize(cs.namespace(|| "a is input")); + let _ = b.inputize(cs.namespace(|| "b is input")); + Ok(()) + } + + fn synthesize_use_cs_one_after_inputize>( + cs: &mut CS, + ) -> Result<(), SynthesisError> { + let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; + let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; + let _ = a.inputize(cs.namespace(|| "a is input")); + cs.enforce( + || "check a = b", + |lc| lc + a.get_variable() - b.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + let _ = b.inputize(cs.namespace(|| "b is input")); + Ok(()) + } + + #[test] + fn test_use_cs_one() { + type G = pasta_curves::pallas::Point; + + // First create the shape + let mut cs: ShapeCS = ShapeCS::new(); + let _ = synthesize_use_cs_one(&mut cs); + let shape = cs.r1cs_shape(); + let gens = cs.r1cs_gens(); + + // Now get the assignment + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + let _ = synthesize_use_cs_one(&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()); + } + + #[test] + fn test_use_cs_one_after_inputize() { + type G = pasta_curves::pallas::Point; + + // First create the shape + let mut cs: ShapeCS = ShapeCS::new(); + let _ = synthesize_use_cs_one_after_inputize(&mut cs); + let shape = cs.r1cs_shape(); + let gens = cs.r1cs_gens(); + + // Now get the assignment + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + let _ = synthesize_use_cs_one_after_inputize(&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()); + } + + fn synthesize_is_equal>( + cs: &mut CS, + a_val: &BigInt, + 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>( + cs: &mut CS, + a_val: &BigInt, + b_val: &BigInt, + m_val: &BigInt, + q_val: &BigInt, + r_val: &BigInt, + 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>( + cs: &mut CS, + a_val: &BigInt, + b_val: &BigInt, + c_val: &BigInt, + 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::(&b)?; + ca.equal(cs.namespace(|| "ccheck"), &c)?; + Ok(()) + } + + fn synthesize_add_mod>( + cs: &mut CS, + a_val: &BigInt, + b_val: &BigInt, + c_val: &BigInt, + m_val: &BigInt, + 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::(&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 = BigInt::from_str_radix( + "11572336752428856981970994795408771577024165681374400871001196932361466228192", + 10, + ) + .unwrap(); + let b_val = BigInt::from_str_radix( + "87673389408848523602668121701204553693362841135953267897017930941776218798802", + 10, + ) + .unwrap(); + let m_val = BigInt::from_str_radix( + "40000000000000000000000000000000224698fc094cf91b992d30ed00000001", + 16, + ) + .unwrap(); + let q_val = BigInt::from_str_radix( + "35048542371029440058224000662033175648615707461806414787901284501179083518342", + 10, + ) + .unwrap(); + let r_val = BigInt::from_str_radix( + "26362617993085418618858432307761590013874563896298265114483698919121453084730", + 10, + ) + .unwrap(); + + // First create the shape + let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix( + "11572336752428856981970994795408771577024165681374400871001196932361466228192", + 10, + ) + .unwrap(); + let b_val = BigInt::from_str_radix("1", 10).unwrap(); + let c_val = BigInt::from_str_radix( + "11572336752428856981970994795408771577024165681374400871001196932361466228193", + 10, + ) + .unwrap(); + + // First create the shape + let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix( + "11572336752428856981970994795408771577024165681374400871001196932361466228192", + 10, + ) + .unwrap(); + let b_val = BigInt::from_str_radix("1", 10).unwrap(); + let c_val = BigInt::from_str_radix( + "11572336752428856981970994795408771577024165681374400871001196932361466228193", + 10, + ) + .unwrap(); + let m_val = BigInt::from_str_radix( + "40000000000000000000000000000000224698fc094cf91b992d30ed00000001", + 16, + ) + .unwrap(); + + // First create the shape + let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix("1157233675242885698197099479540877", 10).unwrap(); + + // First create the shape + let mut cs: ShapeCS = 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 = 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()); + } +} diff --git a/src/bellperson/shape_cs.rs b/src/bellperson/shape_cs.rs index cb5c6f7..5b9ae60 100644 --- a/src/bellperson/shape_cs.rs +++ b/src/bellperson/shape_cs.rs @@ -117,6 +117,7 @@ where } /// Print all public inputs, aux inputs, and constraint names. + #[allow(dead_code)] pub fn pretty_print_list(&self) -> Vec { let mut result = Vec::new(); @@ -135,6 +136,7 @@ where } /// Print all iputs and a detailed representation of each constraint. + #[allow(dead_code)] pub fn pretty_print(&self) -> String { let mut s = String::new(); diff --git a/src/lib.rs b/src/lib.rs index cc22fdb..a9f7d57 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,7 @@ #![deny(missing_docs)] // private modules +mod bellperson; mod circuit; mod commitments; mod constants; @@ -12,7 +13,6 @@ mod poseidon; mod r1cs; // public modules -pub mod bellperson; pub mod errors; pub mod gadgets; pub mod pasta; diff --git a/tests/bit.rs b/tests/bit.rs deleted file mode 100644 index 65bc1ba..0000000 --- a/tests/bit.rs +++ /dev/null @@ -1,50 +0,0 @@ -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>( - 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 = 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 = 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()); -} diff --git a/tests/nonnative.rs b/tests/nonnative.rs deleted file mode 100644 index a88259e..0000000 --- a/tests/nonnative.rs +++ /dev/null @@ -1,308 +0,0 @@ -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 num_bigint::BigInt; -use num_traits::Num as OtherNum; - -fn synthesize_is_equal>( - cs: &mut CS, - a_val: &BigInt, - 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>( - cs: &mut CS, - a_val: &BigInt, - b_val: &BigInt, - m_val: &BigInt, - q_val: &BigInt, - r_val: &BigInt, - 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>( - cs: &mut CS, - a_val: &BigInt, - b_val: &BigInt, - c_val: &BigInt, - 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::(&b)?; - ca.equal(cs.namespace(|| "ccheck"), &c)?; - Ok(()) -} - -fn synthesize_add_mod>( - cs: &mut CS, - a_val: &BigInt, - b_val: &BigInt, - c_val: &BigInt, - m_val: &BigInt, - 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::(&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 = BigInt::from_str_radix( - "11572336752428856981970994795408771577024165681374400871001196932361466228192", - 10, - ) - .unwrap(); - let b_val = BigInt::from_str_radix( - "87673389408848523602668121701204553693362841135953267897017930941776218798802", - 10, - ) - .unwrap(); - let m_val = BigInt::from_str_radix( - "40000000000000000000000000000000224698fc094cf91b992d30ed00000001", - 16, - ) - .unwrap(); - let q_val = BigInt::from_str_radix( - "35048542371029440058224000662033175648615707461806414787901284501179083518342", - 10, - ) - .unwrap(); - let r_val = BigInt::from_str_radix( - "26362617993085418618858432307761590013874563896298265114483698919121453084730", - 10, - ) - .unwrap(); - - // First create the shape - let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix( - "11572336752428856981970994795408771577024165681374400871001196932361466228192", - 10, - ) - .unwrap(); - let b_val = BigInt::from_str_radix("1", 10).unwrap(); - let c_val = BigInt::from_str_radix( - "11572336752428856981970994795408771577024165681374400871001196932361466228193", - 10, - ) - .unwrap(); - - // First create the shape - let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix( - "11572336752428856981970994795408771577024165681374400871001196932361466228192", - 10, - ) - .unwrap(); - let b_val = BigInt::from_str_radix("1", 10).unwrap(); - let c_val = BigInt::from_str_radix( - "11572336752428856981970994795408771577024165681374400871001196932361466228193", - 10, - ) - .unwrap(); - let m_val = BigInt::from_str_radix( - "40000000000000000000000000000000224698fc094cf91b992d30ed00000001", - 16, - ) - .unwrap(); - - // First create the shape - let mut cs: ShapeCS = 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 = 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 = BigInt::from_str_radix("1157233675242885698197099479540877", 10).unwrap(); - - // First create the shape - let mut cs: ShapeCS = 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 = 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()); -} diff --git a/tests/num.rs b/tests/num.rs deleted file mode 100644 index 55b58d1..0000000 --- a/tests/num.rs +++ /dev/null @@ -1,77 +0,0 @@ -use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; -use ff::PrimeField; -use nova_snark::bellperson::{ - r1cs::{NovaShape, NovaWitness}, - shape_cs::ShapeCS, - solver::SatisfyingAssignment, -}; - -fn synthesize_use_cs_one>( - cs: &mut CS, -) -> Result<(), SynthesisError> { - let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; - let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; - cs.enforce( - || "check a = b", - |lc| lc + a.get_variable() - b.get_variable(), - |lc| lc + CS::one(), - |lc| lc, - ); - let _ = a.inputize(cs.namespace(|| "a is input")); - let _ = b.inputize(cs.namespace(|| "b is input")); - Ok(()) -} - -fn synthesize_use_cs_one_after_inputize>( - cs: &mut CS, -) -> Result<(), SynthesisError> { - let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?; - let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?; - let _ = a.inputize(cs.namespace(|| "a is input")); - cs.enforce( - || "check a = b", - |lc| lc + a.get_variable() - b.get_variable(), - |lc| lc + CS::one(), - |lc| lc, - ); - let _ = b.inputize(cs.namespace(|| "b is input")); - Ok(()) -} - -#[test] -fn test_use_cs_one() { - type G = pasta_curves::pallas::Point; - - // First create the shape - let mut cs: ShapeCS = ShapeCS::new(); - let _ = synthesize_use_cs_one(&mut cs); - let shape = cs.r1cs_shape(); - let gens = cs.r1cs_gens(); - - // Now get the assignment - let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); - let _ = synthesize_use_cs_one(&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()); -} - -#[test] -fn test_use_cs_one_after_inputize() { - type G = pasta_curves::pallas::Point; - - // First create the shape - let mut cs: ShapeCS = ShapeCS::new(); - let _ = synthesize_use_cs_one_after_inputize(&mut cs); - let shape = cs.r1cs_shape(); - let gens = cs.r1cs_gens(); - - // Now get the assignment - let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); - let _ = synthesize_use_cs_one_after_inputize(&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()); -}