Skip to content

Commit

Permalink
fix the folding logic, make second argument non relaxed
Browse files Browse the repository at this point in the history
  • Loading branch information
KiriosK committed Dec 15, 2023
1 parent f4297c5 commit 567d4ba
Show file tree
Hide file tree
Showing 17 changed files with 547 additions and 224 deletions.
18 changes: 16 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions nova/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ bn-254 = { path = "../bn254", default-features = false }
grumpkin = { path = "../grumpkin", default-features = false }
zkgroth16 = { path = "../groth16", default-features = false }
serde = { version = "1.0.102", default-features = false, features = ["derive"] }
num-bigint = { version = "0.4", features = ["serde", "rand"] }
blake2b_simd = { version = "1", default-features = false }
rand_core = { version="0.6.4", default-features = false, features = ["getrandom"] }

Expand Down
61 changes: 31 additions & 30 deletions nova/src/circuit/augmented.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
use crate::circuit::nifs::NifsCircuit;
use crate::circuit::MimcROCircuit;
use crate::function::FunctionCircuit;
use crate::gadget::RelaxedR1csInstanceAssignment;
use crate::gadget::{R1csInstanceAssignment, RelaxedR1csInstanceAssignment};
use crate::hash::MIMC_ROUNDS;
use crate::relaxed_r1cs::RelaxedR1csInstance;
use std::any::type_name;
use crate::relaxed_r1cs::{R1csInstance, RelaxedR1csInstance};
use std::marker::PhantomData;
use zkstd::circuit::prelude::{FieldAssignment, PointAssignment};
use zkstd::circuit::CircuitDriver;
Expand All @@ -18,7 +17,7 @@ pub struct AugmentedFCircuit<C: CircuitDriver, FC: FunctionCircuit<C::Base>> {
pub i: usize,
pub z_0: DenseVectors<C::Base>,
pub z_i: Option<DenseVectors<C::Base>>,
pub u_single: Option<RelaxedR1csInstance<C>>,
pub u_single: Option<R1csInstance<C>>,
pub u_range: Option<RelaxedR1csInstance<C>>,
pub commit_t: Option<C::Affine>,
pub f: PhantomData<FC>,
Expand All @@ -31,7 +30,7 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> Default for AugmentedFCircu
i: 0,
z_0: DenseVectors::zero(1),
z_i: Some(DenseVectors::zero(1)),
u_single: Some(RelaxedR1csInstance::dummy(2)),
u_single: Some(R1csInstance::dummy(2)),
u_range: Some(RelaxedR1csInstance::dummy(2)),
commit_t: Some(C::Affine::ADDITIVE_IDENTITY),
f: Default::default(),
Expand Down Expand Up @@ -61,12 +60,12 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {

let u_dummy_native = RelaxedR1csInstance::<C>::dummy(2);
let u_dummy = RelaxedR1csInstanceAssignment::witness(cs, &u_dummy_native);
let u_single = RelaxedR1csInstanceAssignment::witness(
let u_single = R1csInstanceAssignment::witness(
cs,
&self
.u_single
.clone()
.unwrap_or_else(|| u_dummy_native.clone()),
.unwrap_or_else(|| R1csInstance::<C>::dummy(2)),
);
let u_range = RelaxedR1csInstanceAssignment::witness(
cs,
Expand All @@ -93,17 +92,24 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {
let u_range_next_base = if self.is_primary {
u_dummy
} else {
u_single.clone()
RelaxedR1csInstanceAssignment::from_r1cs_instance(cs, u_single.clone())
};

let u_i_x = u_range.hash(cs, i.clone(), z_0.clone(), z_i.clone());
FieldAssignment::conditional_enforce_equal(cs, &u_single.x0, &u_i_x, &not_base_case);

let r = Self::get_challenge(cs, &u_range, commit_t.clone());
let r = FieldAssignment::constant(&C::Base::one());
println!("R = {:?}", r.value(cs));
dbg!(type_name::<<C as CircuitDriver>::Base>());
println!(
"R_bits = {:?}",
FieldAssignment::to_bits(cs, &r)
.iter()
.map(|x| FieldAssignment::from(x).value(cs))
.collect::<Vec<_>>()
);
let u_range_next_non_base =
NifsCircuit::verify(cs, r, u_single.clone(), u_range.clone(), commit_t);
NifsCircuit::verify(cs, r, u_range.clone(), u_single.clone(), commit_t);

let u_range_next = RelaxedR1csInstanceAssignment::conditional_select(
cs,
Expand All @@ -114,21 +120,16 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {

let z_next = FC::invoke_cs(cs, z_i);

println!(
"Hash_circuit\ni = {:?}\nz0 = {:?}\nznext = {:?}\nu = {:?}\nx0 = {:?}\nx1 = {:?}\ne =\n({:?}, {:?}, {:?})\nw =\n({:?}, {:?}, {:?})",
(&i + &FieldAssignment::constant(&C::Base::one())).value(cs),
z_0.iter().map(|x| x.value(cs)).collect::<Vec<_>>(),
z_next.iter().map(|x| x.value(cs)).collect::<Vec<_>>(),
u_range_next.u.value(cs),
u_range_next.x0.value(cs),
u_range_next.x1.value(cs),
u_range_next.commit_e.get_x().value(cs),
u_range_next.commit_e.get_y().value(cs),
u_range_next.commit_e.get_z().value(cs),
u_range_next.commit_w.get_x().value(cs),
u_range_next.commit_w.get_y().value(cs),
u_range_next.commit_w.get_z().value(cs)
);
// println!(
// "Hash_circuit\n{:?},\n{:?},\n{:?},\n{:?},\n{:?},\n{:?},",
// (&i + &FieldAssignment::constant(&C::Base::one())).value(cs),
// z_0.iter().map(|x| x.value(cs)).collect::<Vec<_>>(),
// z_next.iter().map(|x| x.value(cs)).collect::<Vec<_>>(),
// u_range_next.u.value(cs),
// u_range_next.x0.value(cs),
// u_range_next.x1.value(cs),
// );
println!("HASH");
let u_next_x = u_range_next.hash(
cs,
&i + &FieldAssignment::constant(&C::Base::one()),
Expand Down Expand Up @@ -158,7 +159,7 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {
mod tests {
use super::*;
use crate::driver::{Bn254Driver, GrumpkinDriver};
use crate::ivc::PublicParams;

use crate::relaxed_r1cs::{r1cs_instance_and_witness, R1csShape, RelaxedR1csWitness};
use crate::test::ExampleFunction;
use crate::PedersenCommitment;
Expand Down Expand Up @@ -188,10 +189,10 @@ mod tests {

let (x, w) = r1cs_instance_and_witness(&cs, &shape, &ck);
let (instance, witness) = (
RelaxedR1csInstance::<Bn254Driver>::new(x.x),
RelaxedR1csWitness::<Bn254Driver>::new(w.w, shape.m()),
RelaxedR1csInstance::<Bn254Driver>::from_r1cs_instance(&ck, &shape, &x),
RelaxedR1csWitness::<Bn254Driver>::from_r1cs_witness(&shape, &w),
);
assert!(shape.is_sat(&u_dummy, &w_dummy));
assert!(shape.is_sat(&instance, &witness));
assert!(shape.is_sat_relaxed(&u_dummy, &w_dummy));
assert!(shape.is_sat_relaxed(&instance, &witness));
}
}
88 changes: 53 additions & 35 deletions nova/src/circuit/nifs.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
use core::marker::PhantomData;

use crate::gadget::RelaxedR1csInstanceAssignment;
use crate::gadget::{R1csInstanceAssignment, RelaxedR1csInstanceAssignment};
use zkstd::circuit::prelude::{CircuitDriver, FieldAssignment, PointAssignment, R1cs};
use zkstd::common::IntGroup;
use zkstd::common::{Group, IntGroup};

pub(crate) struct NifsCircuit<C: CircuitDriver> {
p: PhantomData<C>,
Expand All @@ -12,38 +12,50 @@ impl<C: CircuitDriver> NifsCircuit<C> {
pub(crate) fn verify<CS: CircuitDriver<Scalar = C::Base>>(
cs: &mut R1cs<CS>,
r: FieldAssignment<C::Base>,
u_single: RelaxedR1csInstanceAssignment<C>,
u_range: RelaxedR1csInstanceAssignment<C>,
u_single: R1csInstanceAssignment<C>,
commit_t: PointAssignment<C::Base>,
) -> RelaxedR1csInstanceAssignment<C> {
let r2 = FieldAssignment::square(cs, &r);
println!("R2 = {:?}", r2.value(cs));
println!(
"W1 = {:?}, {:?}, {:?}",
u_range.commit_w.get_x().value(cs),
u_range.commit_w.get_y().value(cs),
u_range.commit_w.get_z().value(cs)
);
println!(
"W2 = {:?}, {:?}, {:?}",
u_single.commit_w.get_x().value(cs),
u_single.commit_w.get_y().value(cs),
u_single.commit_w.get_z().value(cs)
);
// W_fold = U.W + r * u.W
let r_w = u_range.commit_w.scalar_point(cs, &r);
let r_w = u_single.commit_w.scalar_point(cs, &r);
let w_fold = u_range.commit_w.add(&r_w, cs);
let z_inv = w_fold
.get_z()
.value(cs)
.invert()
.unwrap_or_else(C::Base::zero);

// E_fold = u.E + r * T + U.E * r^2
// E_fold = U.E + r * T
let r_t = commit_t.scalar_point(cs, &r);
let r2_e = u_range.commit_e.scalar_point(cs, &r2);
let e_fold = u_range.commit_e.add(&r_t, cs);
let e_fold = e_fold.add(&r2_e, cs);

// u_fold = u.u + r * U.u
let r_u = FieldAssignment::mul(cs, &r, &u_range.u);
let u_fold = &u_single.u + &r_u;
FieldAssignment::enforce_eq_constant(
cs,
&(&(&u_fold - &u_single.u) - &r_u),
&C::Base::zero(),
);
// u_fold = U.u + r
let u_fold = &u_range.u + &r;
FieldAssignment::enforce_eq_constant(cs, &(&(&u_fold - &u_range.u) - &r), &C::Base::zero());

// Fold x0 + r * U.x0
let r_x0 = FieldAssignment::mul(cs, &r, &u_range.x0);
let x0_fold = &u_single.x0 + &r_x0;
// Fold U.x0 + r * x0
let r_x0 = FieldAssignment::mul(cs, &r, &u_single.x0);
let x0_fold = &u_range.x0 + &r_x0;

// Fold x1 + r * U.x1
let r_x1 = FieldAssignment::mul(cs, &r, &u_range.x1);
let x1_fold = &u_single.x1 + &r_x1;
println!("x1 = {:?}", u_range.x1.value(cs));
println!("x2 = {:?}", u_single.x1.value(cs));
// Fold U.x1 + r * x1
let r_x1 = FieldAssignment::mul(cs, &r, &u_single.x1);
println!("R_x1 = {:?}", r_x1.value(cs));
let x1_fold = &u_range.x1 + &r_x1;
println!("x1_fold = {:?}", x1_fold.value(cs));
RelaxedR1csInstanceAssignment {
commit_w: w_fold,
commit_e: e_fold,
Expand All @@ -58,45 +70,51 @@ impl<C: CircuitDriver> NifsCircuit<C> {
mod tests {
use super::*;
use crate::driver::{Bn254Driver, GrumpkinDriver};
use crate::gadget::R1csInstanceAssignment;
use crate::hash::{MimcRO, MIMC_ROUNDS};
use crate::prover::tests::example_prover;
use crate::relaxed_r1cs::{RelaxedR1csInstance, RelaxedR1csWitness};
use crate::relaxed_r1cs::{r1cs_instance_and_witness, RelaxedR1csInstance, RelaxedR1csWitness};
use crate::R1csShape;
use zkstd::common::CurveGroup;
use zkstd::matrix::DenseVectors;

use zkstd::r1cs::test::example_r1cs;

#[test]
#[ignore]
fn nifs_circuit() {
let prover = example_prover();
let r1cs = example_r1cs::<Bn254Driver>(1);
let running_instance = RelaxedR1csInstance::new(DenseVectors::new(r1cs.x()));
let running_witness = RelaxedR1csWitness::new(DenseVectors::new(r1cs.w()), r1cs.m());
let shape = R1csShape::from(r1cs.clone());
let (x, w) = r1cs_instance_and_witness(&r1cs, &shape, &prover.ck);
let running_instance = RelaxedR1csInstance::from_r1cs_instance(&prover.ck, &shape, &x);
let running_witness = RelaxedR1csWitness::from_r1cs_witness(&shape, &w);

let r1cs_2 = example_r1cs::<Bn254Driver>(2);
let instance_to_fold = RelaxedR1csInstance::new(DenseVectors::new(r1cs.x()));
let witness_to_fold = RelaxedR1csWitness::new(DenseVectors::new(r1cs.w()), r1cs.m());
let (instance_to_fold, witness_to_fold) =
r1cs_instance_and_witness(&r1cs, &shape, &prover.ck);

let (instance, witness, commit_t) = prover.prove(
&instance_to_fold,
&witness_to_fold,
&running_instance,
&running_witness,
&instance_to_fold,
&witness_to_fold,
);

let mut transcript = MimcRO::<MIMC_ROUNDS, Bn254Driver>::default();
transcript.append_point(commit_t);
running_instance.absorb_by_transcript(&mut transcript);
let t = prover.compute_cross_term(
&instance_to_fold,
&witness_to_fold,
&running_instance,
&running_witness,
&instance_to_fold,
&witness_to_fold,
);
let r = transcript.squeeze();

let mut cs = R1cs::<GrumpkinDriver>::default();
let r = FieldAssignment::witness(&mut cs, r.into());
let instance1 = RelaxedR1csInstanceAssignment::witness(&mut cs, &instance_to_fold);
let instance2 = RelaxedR1csInstanceAssignment::witness(&mut cs, &running_instance);
let instance1 = RelaxedR1csInstanceAssignment::witness(&mut cs, &running_instance);
let instance2 = R1csInstanceAssignment::witness(&mut cs, &instance_to_fold);
let commit_t = PointAssignment::witness(
&mut cs,
commit_t.get_x(),
Expand Down
46 changes: 46 additions & 0 deletions nova/src/driver.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use bn_254::{params::PARAM_B3 as BN254_PARAM_B3, Fq, Fr, G1Affine};
use grumpkin::{params::PARAM_B3 as GRUMPKIN_PARAM_B3, Affine};
use num_bigint::{BigInt, Sign};
use zkstd::circuit::CircuitDriver;
use zkstd::common::{IntGroup, PrimeField, Ring};

Expand Down Expand Up @@ -35,6 +36,51 @@ impl CircuitDriver for Bn254Driver {
}
}

/// Convert a field element to a natural number
pub fn f_to_nat<F: PrimeField>(f: &F) -> BigInt {
dbg!(f.to_raw_bytes());
BigInt::from_bytes_le(Sign::Plus, &f.to_raw_bytes())
}

/// Convert a natural number to a field element.
/// Returns `None` if the number is too big for the field.
pub fn nat_to_f<F: PrimeField>(n: &BigInt) -> F {
let bytes = n.to_signed_bytes_le();
if bytes.len() > 64 {
panic!("Length exceed the field size");
};

let mut res = [0; 64];
res[0..64].copy_from_slice(&bytes);

F::from_bytes_wide(&res)
}

/// Compute the limbs encoding a natural number.
/// The limbs are assumed to be based the `limb_width` power of 2.
pub fn nat_to_limbs<F: PrimeField>(nat: &BigInt, limb_width: usize, n_limbs: usize) -> Vec<F> {
let mask = int_with_n_ones(limb_width);
let mut nat = nat.clone();
if nat.bits() as usize <= n_limbs * limb_width {
(0..n_limbs)
.map(|_| {
let r = &nat & &mask;
nat >>= limb_width as u32;
nat_to_f(&r)
})
.collect()
} else {
panic!("Wrong amount of bits");
}
}

fn int_with_n_ones(n: usize) -> BigInt {
let mut m = BigInt::from(1);
m <<= n as u32;
m -= 1;
m
}

/// interpret scalar as base
pub fn scalar_as_base<C: CircuitDriver>(input: C::Scalar) -> C::Base {
let input_bits = input.to_bits();
Expand Down
3 changes: 3 additions & 0 deletions nova/src/gadget.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
mod big_nat;
mod instance;
mod mimc;
mod relaxed_instance;

pub(crate) use instance::R1csInstanceAssignment;
pub(crate) use mimc::MimcAssignment;
pub(crate) use relaxed_instance::RelaxedR1csInstanceAssignment;
Loading

0 comments on commit 567d4ba

Please sign in to comment.