Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parellel NIVC #256

Draft
wants to merge 28 commits into
base: dev
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,12 @@ readme = "README.md"
repository = "https://github.com/lurk-lab/arecibo"
license-file = "LICENSE"
keywords = ["zkSNARKs", "cryptography", "proofs"]
rust-version="1.71.0"
rust-version = "1.71.0"

[dependencies]
bellpepper-core = { version = "0.4.0", default-features = false }
bellpepper = { git="https://github.com/lurk-lab/bellpepper", branch="dev", default-features = false }
bellpepper = { git = "https://github.com/lurk-lab/bellpepper", branch = "dev", default-features = false }
bellpepper-emulated = { git = "https://github.com/lurk-lab/bellpepper-gadgets", branch = "main", default-features = false }
ff = { version = "0.13.0", features = ["derive"] }
digest = "0.10"
halo2curves = { version = "0.6.0", features = ["bits", "derive_serde"] }
Expand All @@ -23,7 +24,7 @@ rand_core = { version = "0.6", default-features = false }
rand_chacha = "0.3"
subtle = "2.5"
pasta_curves = { version = "0.5.0", features = ["repr-c", "serde"] }
neptune = { git = "https://github.com/lurk-lab/neptune", branch="dev", default-features = false, features = ["abomonation"] }
neptune = { git = "https://github.com/lurk-lab/neptune", branch = "dev", default-features = false, features = ["abomonation"] }
generic-array = "1.0.0"
num-bigint = { version = "0.4", features = ["serde", "rand"] }
num-traits = "0.2"
Expand Down
4 changes: 2 additions & 2 deletions src/gadgets/nonnative/bignat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ pub fn nat_to_limbs<Scalar: PrimeField>(
}
}

#[derive(Clone, PartialEq, Eq)]
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct BigNatParams {
pub min_bits: usize,
pub max_word: BigInt,
Expand All @@ -80,7 +80,7 @@ impl BigNatParams {
}

/// A representation of a large natural number (a member of {0, 1, 2, ... })
#[derive(Clone)]
#[derive(Debug, Clone)]
pub struct BigNat<Scalar: PrimeField> {
/// The linear combinations which constrain the value of each limb of the number
pub limbs: Vec<LinearCombination<Scalar>>,
Expand Down
1 change: 1 addition & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ pub mod r1cs;
pub mod spartan;
pub mod traits;

mod parafold;
pub mod supernova;

use once_cell::sync::OnceCell;
Expand Down
100 changes: 100 additions & 0 deletions src/parafold/cycle_fold/circuit.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
use bellpepper_core::{ConstraintSystem, SynthesisError, Variable};
use bellpepper_core::boolean::Boolean;
use ff::PrimeField;

use crate::parafold::gadgets::emulated::AllocatedBase;
use crate::parafold::gadgets::primary_commitment::AllocatedPrimaryCommitment;
use crate::parafold::nifs_secondary::circuit::AllocatedSecondaryRelaxedR1CSInstance;
use crate::parafold::nifs_secondary::NUM_IO_SECONDARY;
use crate::parafold::transcript::circuit::AllocatedTranscript;
use crate::traits::CurveCycleEquipped;

#[derive(Debug)]
pub struct AllocatedScalarMulAccumulator<E: CurveCycleEquipped> {
deferred: Vec<AllocatedScalarMulInstance<E>>,
}

#[derive(Debug, Clone)]
pub struct AllocatedScalarMulInstance<E: CurveCycleEquipped> {
A: AllocatedPrimaryCommitment<E>,
B: AllocatedPrimaryCommitment<E>,
x_bits: Vec<Boolean>,
C: AllocatedPrimaryCommitment<E>,
}

impl<E: CurveCycleEquipped> AllocatedScalarMulAccumulator<E> {
pub fn new() -> Self {
Self { deferred: vec![] }
}

/// Compute the result `C <- A + x * B` by folding a proof over the secondary curve.
pub fn scalar_mul<CS>(
&mut self,
mut cs: CS,
A: AllocatedPrimaryCommitment<E>,
B: AllocatedPrimaryCommitment<E>,
x_bits: Vec<Boolean>,
transcript: &mut AllocatedTranscript<E>,
) -> Result<AllocatedPrimaryCommitment<E>, SynthesisError>
where
CS: ConstraintSystem<E::Scalar>,
{
// Ensure the number of bits in the scalar matches fits.
assert!(x_bits.len() <= E::Scalar::NUM_BITS as usize);

let C = transcript.read_commitment_primary(cs.namespace(|| "transcript C"))?;

self.deferred.push(AllocatedScalarMulInstance {
A,
B,
x_bits,
C: C.clone(),
});

Ok(C)
}

/// Consume a set of accumulated scalar multiplications, proving each instance by folding a proof
/// into the internal secondary curve accumulator.
pub fn finalize<CS>(
mut self,
mut cs: CS,
mut acc_cf: AllocatedSecondaryRelaxedR1CSInstance<E>,
transcript: &mut AllocatedTranscript<E>,
) -> Result<AllocatedSecondaryRelaxedR1CSInstance<E>, SynthesisError>
where
CS: ConstraintSystem<E::Scalar>,
{
for (i, instance) in self.deferred.drain(..).enumerate() {
let X = instance.into_io(CS::one());

// TODO: In order to avoid computing unnecessary proofs, we can check
// - x = 0 => C = A
acc_cf.fold(
cs.namespace(|| format!("fold cf instance {i}")),
X,
transcript,
)?;
}
Ok(acc_cf)
}
}

impl<E: CurveCycleEquipped> Drop for AllocatedScalarMulAccumulator<E> {
/// Ensures that every scalar multiplication is proved
fn drop(&mut self) {
assert!(self.deferred.is_empty(), "unproved scalar multiplications")
}
}

impl<E: CurveCycleEquipped> AllocatedScalarMulInstance<E> {
fn into_io(self, one: Variable) -> [AllocatedBase<E>; NUM_IO_SECONDARY] {
let Self { A, B, x_bits, C } = self;

// Convert the elements in the instance to a bignum modulo E1::Base.
// Since |E1::Scalar| < |E1::Base|, we can create the limbs without an initial bound-check
// We should check here that the limbs are of the right size, but not-necessarily bound check them.
let x = AllocatedBase::from_bits_le(one, &x_bits);
[A.hash, B.hash, x, C.hash]
}
}
57 changes: 57 additions & 0 deletions src/parafold/cycle_fold/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
use ff::Field;
use neptune::generic_array::typenum::U2;
use neptune::hash_type::HashType;
use neptune::poseidon::PoseidonConstants;
use neptune::{Poseidon, Strength};

use crate::traits::commitment::CommitmentTrait;
use crate::traits::CurveCycleEquipped;
use crate::Commitment;

pub mod circuit;
pub mod prover;

/// Compressed representation of a [Commitment] for a proof over the [Engine]'s scalar field.
///
/// # Details
/// Let F_r be the scalar field over which the circuit is defined, and F_q be the base field of the group G over which
/// the proof is defined, whose scalar field is F_r. We will assume that r < q, which is the case when we instantiate
/// the proof over the BN254/Grumpkin curve cycle.
///
/// A [HashedCommitment] corresponds to a group element C \in G, and would usually be represented by
/// its coordinates (x,y) \in F_q, possibly with a boolean flag indicating whether it is equal to the identity element.
///
/// Representing F_q scalars within a circuit over F_r is expensive since we need to encode these
/// with range-checked limbs, and any operation performed over these non-native scalar require many constraints
/// to properly constrain the modular reduction by q.
///
/// An important observation we can make is that the minimal operation we need to support over [HashedCommitment]s is
/// "multiply-add", and that the internal of the group element are ignored by the recursive verifier.
///
/// We chose to represent the [HashedCommitment] C as the F_q element
/// h_C = H(C) = H((x,y)),
/// where H is a hash function with efficient arithmetization over F_q.
/// If C is the identity, then we define h_C = 0.
///
/// The circuit on the secondary curve has IO (h_C, h_A, h_B, x) \in (F_q, F_q, F_q, F_r),
/// with private inputs A, B \in G, and checks
/// - C <- A + x * B
/// - h_A == H(A), h_B == H(B), h_C == H(C)
///
/// When folding a proof for the above IO on the primary curve, each IO elements leads to a non-native "multiply-add",
/// so this additional hashing that occurs in the secondary circuit ensure we only need to perform this expensive
/// operation 4 times. Moreover, the fact that r<q ensures that the scalar x \in F_r can be trivially embedded into F_q.
pub fn hash_commitment<E: CurveCycleEquipped>(commitment: &Commitment<E>) -> E::Base {
// TODO: Find a way to cache this
let constants = PoseidonConstants::<E::Base, U2>::new_with_strength_and_type(
Strength::Standard,
HashType::ConstantLength(2),
);

let (x, y, infinity) = commitment.to_coordinates();
if infinity {
E::Base::ZERO
} else {
Poseidon::new_with_preimage(&[x, y], &constants).hash()
}
}
Loading
Loading