Skip to content

Commit

Permalink
Update Neptune & simplify SatisfyingAssignment (Arecibo backport) (ar…
Browse files Browse the repository at this point in the history
…gumentcomputer#256)

* chore: Update bellpepper and neptune dependencies

- Updated `bellpepper-core` and `bellpepper` dependencies to version `0.4.0`
- Upgraded `neptune` dependency to version `13.0.0`

* refactor of SatisfyingAssignment as type alias of WitnessCS (argumentcomputer#89)

* initial refactor of WitnessCS with ex of new constr generic changes

* explicit type information for usages of `SatisfyingAssignment::new`

* use `scalar_` public getters for the aliased WitnessCS

* go back to `_assignment` public fields

* remove reference

---------

Co-authored-by: johann bestowrous <[email protected]>
  • Loading branch information
huitseeker and jobez authored Nov 9, 2023
1 parent 713917c commit 93f5686
Show file tree
Hide file tree
Showing 10 changed files with 21 additions and 167 deletions.
6 changes: 3 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ keywords = ["zkSNARKs", "cryptography", "proofs"]
rust-version="1.67.1"

[dependencies]
bellpepper-core = { version="0.3.0", default-features = false }
bellpepper = { version="0.3.0", default-features = false }
bellpepper-core = { version="0.4.0", default-features = false }
bellpepper = { version="0.4.0", default-features = false }
ff = { version = "0.13.0", features = ["derive"] }
digest = "0.10"
sha3 = "0.10"
Expand All @@ -22,7 +22,7 @@ rand_core = { version = "0.6", default-features = false }
rand_chacha = "0.3"
subtle = "2.5"
pasta_curves = { version = "0.5", features = ["repr-c", "serde"] }
neptune = { version = "12.0.0", default-features = false }
neptune = { version = "13.0.0", default-features = false }
generic-array = "0.14"
num-bigint = { version = "0.4", features = ["serde", "rand"] }
num-traits = "0.2"
Expand Down
2 changes: 1 addition & 1 deletion src/bellpepper/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ mod tests {
let (shape, ck) = cs.r1cs_shape(&*default_commitment_key_hint());

// Now get the assignment
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G>::new();
synthesize_alloc_bit(&mut cs);
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();

Expand Down
4 changes: 2 additions & 2 deletions src/bellpepper/r1cs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ impl<G: Group> NovaWitness<G> for SatisfyingAssignment<G> {
shape: &R1CSShape<G>,
ck: &CommitmentKey<G>,
) -> Result<(R1CSInstance<G>, R1CSWitness<G>), NovaError> {
let W = R1CSWitness::<G>::new(shape, &self.aux_assignment)?;
let X = &self.input_assignment[1..];
let W = R1CSWitness::<G>::new(shape, self.aux_assignment())?;
let X = &self.input_assignment()[1..];

let comm_W = W.commit(ck);

Expand Down
150 changes: 2 additions & 148 deletions src/bellpepper/solver.rs
Original file line number Diff line number Diff line change
@@ -1,154 +1,8 @@
//! Support for generating R1CS witness using bellpepper.

use crate::traits::Group;
use ff::Field;

use bellpepper_core::{ConstraintSystem, Index, LinearCombination, SynthesisError, Variable};
use bellpepper::util_cs::witness_cs::WitnessCS;

/// A `ConstraintSystem` which calculates witness values for a concrete instance of an R1CS circuit.
pub struct SatisfyingAssignment<G: Group> {
// Assignments of variables
pub(crate) input_assignment: Vec<G::Scalar>,
pub(crate) aux_assignment: Vec<G::Scalar>,
}
use std::fmt;

impl<G: Group> fmt::Debug for SatisfyingAssignment<G> {
fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
fmt
.debug_struct("SatisfyingAssignment")
.field("input_assignment", &self.input_assignment)
.field("aux_assignment", &self.aux_assignment)
.finish()
}
}

impl<G: Group> PartialEq for SatisfyingAssignment<G> {
fn eq(&self, other: &SatisfyingAssignment<G>) -> bool {
self.input_assignment == other.input_assignment && self.aux_assignment == other.aux_assignment
}
}

impl<G: Group> ConstraintSystem<G::Scalar> for SatisfyingAssignment<G> {
type Root = Self;

fn new() -> Self {
let input_assignment = vec![G::Scalar::ONE];

Self {
input_assignment,
aux_assignment: vec![],
}
}

fn alloc<F, A, AR>(&mut self, _: A, f: F) -> Result<Variable, SynthesisError>
where
F: FnOnce() -> Result<G::Scalar, SynthesisError>,
A: FnOnce() -> AR,
AR: Into<String>,
{
self.aux_assignment.push(f()?);

Ok(Variable(Index::Aux(self.aux_assignment.len() - 1)))
}

fn alloc_input<F, A, AR>(&mut self, _: A, f: F) -> Result<Variable, SynthesisError>
where
F: FnOnce() -> Result<G::Scalar, SynthesisError>,
A: FnOnce() -> AR,
AR: Into<String>,
{
self.input_assignment.push(f()?);

Ok(Variable(Index::Input(self.input_assignment.len() - 1)))
}

fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _a: LA, _b: LB, _c: LC)
where
A: FnOnce() -> AR,
AR: Into<String>,
LA: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
LB: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
LC: FnOnce(LinearCombination<G::Scalar>) -> LinearCombination<G::Scalar>,
{
// Do nothing: we don't care about linear-combination evaluations in this context.
}

fn push_namespace<NR, N>(&mut self, _: N)
where
NR: Into<String>,
N: FnOnce() -> NR,
{
// Do nothing; we don't care about namespaces in this context.
}

fn pop_namespace(&mut self) {
// Do nothing; we don't care about namespaces in this context.
}

fn get_root(&mut self) -> &mut Self::Root {
self
}

fn is_extensible() -> bool {
true
}

fn extend(&mut self, other: &Self) {
self.input_assignment
// Skip first input, which must have been a temporarily allocated one variable.
.extend(&other.input_assignment[1..]);
self.aux_assignment.extend(&other.aux_assignment);
}

fn is_witness_generator(&self) -> bool {
true
}

fn extend_inputs(&mut self, new_inputs: &[G::Scalar]) {
self.input_assignment.extend(new_inputs);
}

fn extend_aux(&mut self, new_aux: &[G::Scalar]) {
self.aux_assignment.extend(new_aux);
}

fn allocate_empty(
&mut self,
aux_n: usize,
inputs_n: usize,
) -> (&mut [G::Scalar], &mut [G::Scalar]) {
let allocated_aux = {
let i = self.aux_assignment.len();
self.aux_assignment.resize(aux_n + i, G::Scalar::ZERO);
&mut self.aux_assignment[i..]
};

let allocated_inputs = {
let i = self.input_assignment.len();
self.input_assignment.resize(inputs_n + i, G::Scalar::ZERO);
&mut self.input_assignment[i..]
};

(allocated_aux, allocated_inputs)
}

fn inputs_slice(&self) -> &[G::Scalar] {
&self.input_assignment
}

fn aux_slice(&self) -> &[G::Scalar] {
&self.aux_assignment
}
}

#[allow(dead_code)]
impl<G: Group> SatisfyingAssignment<G> {
pub fn scalar_inputs(&self) -> Vec<G::Scalar> {
self.input_assignment.clone()
}

pub fn scalar_aux(&self) -> Vec<G::Scalar> {
self.aux_assignment.clone()
}
}
pub type SatisfyingAssignment<G> = WitnessCS<<G as Group>::Scalar>;
4 changes: 2 additions & 2 deletions src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -407,7 +407,7 @@ mod tests {

// Execute the base case for the primary
let zero1 = <<G2 as Group>::Base as Field>::ZERO;
let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
let mut cs1 = SatisfyingAssignment::<G1>::new();
let inputs1: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
scalar_as_base::<G1>(zero1), // pass zero for testing
zero1,
Expand All @@ -426,7 +426,7 @@ mod tests {

// Execute the base case for the secondary
let zero2 = <<G1 as Group>::Base as Field>::ZERO;
let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs2 = SatisfyingAssignment::<G2>::new();
let inputs2: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
scalar_as_base::<G2>(zero2), // pass zero for testing
zero2,
Expand Down
6 changes: 3 additions & 3 deletions src/gadgets/ecc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1006,7 +1006,7 @@ mod tests {
let (shape, ck) = cs.r1cs_shape(&*default_commitment_key_hint());

// Then the satisfying assignment
let mut cs: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G2>::new();
let (a, e, s) = synthesize_smul::<G1, _>(cs.namespace(|| "synthesize"));
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();

Expand Down Expand Up @@ -1062,7 +1062,7 @@ mod tests {
let (shape, ck) = cs.r1cs_shape(&*default_commitment_key_hint());

// Then the satisfying assignment
let mut cs: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G2>::new();
let (a, e) = synthesize_add_equal::<G1, _>(cs.namespace(|| "synthesize add equal"));
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();
let a_p: Point<G1> = Point::new(
Expand Down Expand Up @@ -1122,7 +1122,7 @@ mod tests {
let (shape, ck) = cs.r1cs_shape(&*default_commitment_key_hint());

// Then the satisfying assignment
let mut cs: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G2>::new();
let e = synthesize_add_negation::<G1, _>(cs.namespace(|| "synthesize add negation"));
let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();
let e_p: Point<G1> = Point::new(
Expand Down
8 changes: 4 additions & 4 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ where
}

// base case for the primary
let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
let mut cs_primary = SatisfyingAssignment::<G1>::new();
let inputs_primary: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
scalar_as_base::<G1>(pp.digest()),
G1::Scalar::ZERO,
Expand All @@ -297,7 +297,7 @@ where
.expect("Nova error unsat");

// base case for the secondary
let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs_secondary = SatisfyingAssignment::<G2>::new();
let inputs_secondary: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
pp.digest(),
G2::Scalar::ZERO,
Expand Down Expand Up @@ -397,7 +397,7 @@ where
)
.expect("Unable to fold secondary");

let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
let mut cs_primary = SatisfyingAssignment::<G1>::new();
let inputs_primary: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
scalar_as_base::<G1>(pp.digest()),
G1::Scalar::from(self.i as u64),
Expand Down Expand Up @@ -436,7 +436,7 @@ where
)
.expect("Unable to fold primary");

let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let mut cs_secondary = SatisfyingAssignment::<G2>::new();
let inputs_secondary: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
pp.digest(),
G2::Scalar::from(self.i as u64),
Expand Down
4 changes: 2 additions & 2 deletions src/nifs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -173,15 +173,15 @@ mod tests {
<<G as Group>::RO as ROTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants::default();

// Now get the instance and assignment for one instance
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G>::new();
let _ = synthesize_tiny_r1cs_bellpepper(&mut cs, Some(G::Scalar::from(5)));
let (U1, W1) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();

// Make sure that the first instance is satisfiable
assert!(shape.is_sat(&ck, &U1, &W1).is_ok());

// Now get the instance and assignment for second instance
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G>::new();
let _ = synthesize_tiny_r1cs_bellpepper(&mut cs, Some(G::Scalar::from(135)));
let (U2, W2) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();

Expand Down
2 changes: 1 addition & 1 deletion src/provider/poseidon.rs
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ mod tests {
let mut ro: PoseidonRO<G::Scalar, G::Base> = PoseidonRO::new(constants.clone(), num_absorbs);
let mut ro_gadget: PoseidonROCircuit<G::Scalar> =
PoseidonROCircuit::new(constants, num_absorbs);
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G>::new();
for i in 0..num_absorbs {
let num = G::Scalar::random(&mut csprng);
ro.absorb(num);
Expand Down
2 changes: 1 addition & 1 deletion src/spartan/direct.rs
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ impl<G: Group, S: RelaxedR1CSSNARKTrait<G>, C: StepCircuit<G::Scalar>> DirectSNA

/// Produces a proof of satisfiability of the provided circuit
pub fn prove(pk: &ProverKey<G, S>, sc: C, z_i: &[G::Scalar]) -> Result<Self, NovaError> {
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
let mut cs = SatisfyingAssignment::<G>::new();

let circuit: DirectCircuit<G, C> = DirectCircuit {
z_i: Some(z_i.to_vec()),
Expand Down

0 comments on commit 93f5686

Please sign in to comment.