Skip to content

Commit

Permalink
fix proof generation, so the hash check matches
Browse files Browse the repository at this point in the history
  • Loading branch information
@KiriosK
KiriosK committed Dec 14, 2023
1 parent 23f7edb commit 43fab25
Show file tree
Hide file tree
Showing 6 changed files with 120 additions and 66 deletions.
33 changes: 21 additions & 12 deletions nova/src/circuit/augmented.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,8 @@ pub struct AugmentedFCircuit<C: CircuitDriver, FC: FunctionCircuit<C::Base>> {
pub z_i: Option<DenseVectors<C::Base>>,
pub u_single: Option<RelaxedR1csInstance<C>>,
pub u_range: Option<RelaxedR1csInstance<C>>,
pub u_range_next: Option<RelaxedR1csInstance<C>>, // Remove
pub commit_t: Option<C::Affine>,
pub f: PhantomData<FC>,
pub x: C::Base, // Remove
}

impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> Default for AugmentedFCircuit<C, FC> {
Expand All @@ -34,10 +32,8 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> Default for AugmentedFCircu
z_i: Some(DenseVectors::zero(1)),
u_single: Some(RelaxedR1csInstance::dummy(2)),
u_range: Some(RelaxedR1csInstance::dummy(2)),
u_range_next: Some(RelaxedR1csInstance::dummy(2)),
commit_t: Some(C::Affine::ADDITIVE_IDENTITY),
f: Default::default(),
x: C::Base::zero(),
}
}
}
Expand Down Expand Up @@ -94,7 +90,7 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {
let not_base_case = FieldAssignment::is_neq(cs, &i, &zero);

// base case
let u_single_next_base = if self.is_primary {
let u_range_next_base = if self.is_primary {
u_dummy
} else {
u_single.clone()
Expand Down Expand Up @@ -132,27 +128,40 @@ impl<C: CircuitDriver, FC: FunctionCircuit<C::Base>> AugmentedFCircuit<C, FC> {

// (3) Generate Ui+1 ← NIFS.V(vk, U, u, T)
let r = Self::get_challenge(cs, &u_range, commit_t.clone());
let u_single_next_non_base =
let u_range_next_non_base =
NifsCircuit::verify(cs, r, u_single.clone(), u_range.clone(), commit_t);

let u_single_next = RelaxedR1csInstanceAssignment::conditional_select(
let u_range_next = RelaxedR1csInstanceAssignment::conditional_select(
cs,
&u_single_next_base,
&u_single_next_non_base,
&u_range_next_base,
&u_range_next_non_base,
&base_case,
);

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

let u_next_x = u_single_next.hash(
// println!(
// "Hash(\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<_>>()
// );
// println!(
// "U = (\n{:?}\n{:?}\n{:?}\n)",
// u_range_next.u.value(cs),
// u_range_next.x0.value(cs),
// u_range_next.x1.value(cs)
// );
let u_next_x = u_range_next.hash(
cs,
&i + &FieldAssignment::constant(&C::Base::one()),
z_0,
z_next.clone(),
);

let x1 = FieldAssignment::inputize(cs, u_single.x1);
let u_next_x = FieldAssignment::inputize(cs, u_next_x);
let x0 = FieldAssignment::inputize(cs, u_single.x1);
let x1 = FieldAssignment::inputize(cs, u_next_x);

z_next
}

Expand Down
2 changes: 1 addition & 1 deletion nova/src/hash.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use zkstd::common::{BNAffine, IntGroup, PrimeField, Ring};

/// Amount of rounds calculated for the 254 bit field.
/// Doubled due to the usage of Feistel mode with zero key.
pub(crate) const MIMC_ROUNDS: usize = 2;
pub(crate) const MIMC_ROUNDS: usize = 0;

pub(crate) struct Mimc<const ROUND: usize, F: PrimeField> {
pub(crate) constants: [F; ROUND],
Expand Down
133 changes: 81 additions & 52 deletions nova/src/ivc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,10 @@ use rand_core::OsRng;
use std::marker::PhantomData;

use crate::circuit::AugmentedFCircuit;
use crate::relaxed_r1cs::{R1csShape, RelaxedR1csInstance, RelaxedR1csWitness};
use crate::relaxed_r1cs::{
r1cs_instance_and_witness, R1csShape, RelaxedR1csInstance, RelaxedR1csWitness,
};
use zkstd::circuit::prelude::{CircuitDriver, R1cs};
use zkstd::common::IntGroup;
use zkstd::matrix::DenseVectors;

pub struct Ivc<E1, E2, FC1, FC2>
Expand Down Expand Up @@ -50,27 +51,59 @@ where
pp: &PublicParams<E1, E2, FC1, FC2>,
z0_primary: DenseVectors<E1::Scalar>,
z0_secondary: DenseVectors<E2::Scalar>,
) -> (Self, RecursiveProof<E1, E2, FC1, FC2>) {
) -> Self {
println!("START");
let mut cs_primary = R1cs::<E1>::default();
let circuit_primary = AugmentedFCircuit::<E2, FC1>::default();
let zi_primary = circuit_primary.generate(&mut cs_primary); // get zi_primary
let circuit_primary = AugmentedFCircuit::<E2, FC1> {
is_primary: true,
i: 0,
z_0: z0_primary.clone(),
z_i: None,
u_single: None,
u_range: None,
commit_t: None,
f: Default::default(),
};
let zi_primary = circuit_primary.generate(&mut cs_primary);

// get u_single_next/w_single_next primary
println!("Primary out");
let (x, w) = r1cs_instance_and_witness(&cs_primary, &pp.r1cs_shape_primary);
let (u_single_next_primary, w_single_next_primary) = (
RelaxedR1csInstance::new(DenseVectors::new(x)),
RelaxedR1csWitness::new(DenseVectors::new(w), pp.r1cs_shape_primary.m()),
);

let prover_primary = Prover::new(R1csShape::from(cs_primary.clone()), rng);

let mut cs_secondary = R1cs::<E2>::default();
let circuit_secondary = AugmentedFCircuit::<E1, FC2>::default();
let circuit_secondary = AugmentedFCircuit::<E1, FC2> {
is_primary: false,
i: 0,
z_0: z0_secondary.clone(),
z_i: None,
u_single: Some(u_single_next_primary.clone()),
u_range: None,
commit_t: None,
f: Default::default(),
};
let zi_secondary = circuit_secondary.generate(&mut cs_secondary);

// get u_single_next/w_single_next secondary
println!("Secondary out");
let (x, w) = r1cs_instance_and_witness(&cs_secondary, &pp.r1cs_shape_secondary);
let (u_single_next_secondary, w_single_next_secondary) = (
RelaxedR1csInstance::new(DenseVectors::new(x)),
RelaxedR1csWitness::new(DenseVectors::new(w), pp.r1cs_shape_secondary.m()),
);

let prover_secondary = Prover::new(R1csShape::from(cs_secondary.clone()), rng);

let u_dummy = RelaxedR1csInstance::<E1>::dummy(cs_primary.l() - 1);
let w_dummy = RelaxedR1csWitness::<E1>::dummy(cs_primary.m_l_1(), cs_primary.m());
let u_dummy = RelaxedR1csInstance::<E2>::dummy(pp.r1cs_shape_secondary.l());
let w_dummy = RelaxedR1csWitness::<E2>::dummy(
pp.r1cs_shape_secondary.m_l_1(),
pp.r1cs_shape_secondary.m(),
);

let ivc = Self {
Self {
i: 0,
z0_primary,
z0_secondary,
Expand All @@ -88,31 +121,14 @@ where
),
prover_primary,
prover_secondary,
u_single_secondary: RelaxedR1csInstance::dummy(1),
w_single_secondary: RelaxedR1csWitness::dummy(1, 1),
u_range_primary: RelaxedR1csInstance::dummy(1),
w_range_primary: RelaxedR1csWitness::dummy(1, 1),
u_range_secondary: RelaxedR1csInstance::dummy(1),
w_range_secondary: RelaxedR1csWitness::dummy(1, 1),
u_single_secondary: u_single_next_secondary,
w_single_secondary: w_single_next_secondary,
u_range_primary: u_single_next_primary,
w_range_primary: w_single_next_primary,
u_range_secondary: u_dummy,
w_range_secondary: w_dummy,
f: PhantomData::default(),
};
let proof = RecursiveProof {
i: 0,
z0_primary: ivc.z0_primary.clone(),
z0_secondary: ivc.z0_secondary.clone(),
zi_primary: ivc.z0_primary.clone(),
zi_secondary: ivc.z0_secondary.clone(),
instances: (
(
ivc.u_single_secondary.clone(),
ivc.w_single_secondary.clone(),
),
(ivc.u_range_primary.clone(), ivc.w_range_primary.clone()),
(ivc.u_range_secondary.clone(), ivc.w_range_secondary.clone()),
),
marker: Default::default(),
};
(ivc, proof)
}
}

pub fn prove_step(
Expand All @@ -121,7 +137,25 @@ where
) -> RecursiveProof<E1, E2, FC1, FC2> {
if self.i == 0 {
self.i = 1;
// return
return RecursiveProof {
i: self.i,
z0_primary: self.z0_primary.clone(),
z0_secondary: self.z0_secondary.clone(),
zi_primary: self.zi_primary.clone(),
zi_secondary: self.zi_secondary.clone(),
instances: (
(
self.u_single_secondary.clone(),
self.w_single_secondary.clone(),
),
(self.u_range_primary.clone(), self.w_range_primary.clone()),
(
self.u_range_secondary.clone(),
self.w_range_secondary.clone(),
),
),
marker: Default::default(),
};
}
let z_next = FC1::invoke(&self.zi_primary);
let (u_range_next_secondary, w_range_next_secondary, commit_t_secondary) =
Expand All @@ -140,10 +174,8 @@ where
z_i: Some(self.zi_primary.clone()),
u_single: Some(self.u_single_secondary.clone()),
u_range: Some(self.u_range_secondary.clone()),
u_range_next: None,
commit_t: Some(commit_t_secondary),
f: Default::default(),
x: E2::Base::zero(),
};

circuit_primary.generate(&mut cs); // zi_primary
Expand All @@ -166,10 +198,8 @@ where
z_i: Some(self.zi_secondary.clone()),
u_single: Some(self.u_range_primary.clone()), // u_single_next_primary
u_range: Some(self.u_range_primary.clone()),
u_range_next: None,
commit_t: Some(commit_t_primary),
f: Default::default(),
x: E1::Base::zero(),
};

circuit_secondary.generate(&mut cs); // zi_secondary
Expand All @@ -188,7 +218,7 @@ where
// self.zi_secondary = zi_secondary;

RecursiveProof {
i: 0,
i: self.i,
z0_primary: self.z0_primary.clone(),
z0_secondary: self.z0_secondary.clone(),
zi_primary: self.z0_primary.clone(),
Expand Down Expand Up @@ -273,18 +303,17 @@ mod tests {
ExampleFunction<Fq>,
>::setup();

let z0_primary = DenseVectors::new(vec![Fr::from(3)]);
let z0_secondary = DenseVectors::new(vec![Fq::from(3)]);
let (mut ivc, proof_0) = Ivc::<
Bn254Driver,
GrumpkinDriver,
ExampleFunction<Fr>,
ExampleFunction<Fq>,
>::init(OsRng, &pp, z0_primary, z0_secondary);

assert!(proof_0.verify(&pp));
let z0_primary = DenseVectors::new(vec![Fr::from(0)]);
let z0_secondary = DenseVectors::new(vec![Fq::from(0)]);
let mut ivc =
Ivc::<Bn254Driver, GrumpkinDriver, ExampleFunction<Fr>, ExampleFunction<Fq>>::init(
OsRng,
&pp,
z0_primary,
z0_secondary,
);

for i in 0..2 {
for i in 0..1 {
let proof = ivc.prove_step(&pp);
assert!(proof.verify(&pp));
}
Expand Down
15 changes: 14 additions & 1 deletion nova/src/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,25 +44,38 @@ where
(u_range_primary, w_range_primary),
(u_range_secondary, w_range_secondary),
) = self.instances.clone();

if u_single_secondary.x.len() != 2
|| u_range_primary.x.len() != 2
|| u_range_secondary.x.len() != 2
{
println!("Length doesn't match");
return false;
}
let (hash_primary, hash_secondary) = {
(
u_range_secondary.hash::<E1>(self.i, &self.z0_primary, &self.zi_primary),
u_range_primary.hash::<E2>(self.i, &self.zi_secondary, &self.zi_secondary),
u_range_primary.hash::<E2>(self.i, &self.z0_secondary, &self.zi_secondary),
)
};

if hash_primary != u_single_secondary.x[0]
|| hash_secondary != scalar_as_base::<E2>(u_single_secondary.x[1])
{
println!("Hash doesn't match");
return false;
}

dbg!(pp
.r1cs_shape_primary
.is_sat(&u_range_primary, &w_range_primary));
dbg!(pp
.r1cs_shape_secondary
.is_sat(&u_range_secondary, &w_range_secondary));
dbg!(pp
.r1cs_shape_secondary
.is_sat(&u_single_secondary, &w_single_secondary));

pp.r1cs_shape_primary
.is_sat(&u_range_primary, &w_range_primary)
&& pp
Expand Down
1 change: 1 addition & 0 deletions nova/src/relaxed_r1cs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ pub(crate) fn r1cs_instance_and_witness<C: CircuitDriver>(
cs: &R1cs<C>,
shape: &R1csShape<C>,
) -> (Vec<C::Scalar>, Vec<C::Scalar>) {
println!("Cs.x = {:?}", cs.x());
assert_eq!(cs.m_l_1(), shape.m_l_1());
let w = cs.w();
let x = cs.x()[1..].to_vec();
Expand Down
2 changes: 2 additions & 0 deletions nova/src/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ pub(crate) struct ExampleFunction<F: PrimeField> {

impl<F: PrimeField> FunctionCircuit<F> for ExampleFunction<F> {
fn invoke(z: &DenseVectors<F>) -> DenseVectors<F> {
// z.clone()
let next_z = z[0] * z[0] * z[0] + z[0] + F::from(5);
DenseVectors::new(vec![next_z])
}
Expand All @@ -26,5 +27,6 @@ impl<F: PrimeField> FunctionCircuit<F> for ExampleFunction<F> {
let z_i_cube = FieldAssignment::mul(cs, &z_i_square, &z_i[0]);

vec![&(&z_i_cube + &z_i[0]) + &five]
// z_i
}
}

0 comments on commit 43fab25

Please sign in to comment.