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

CycleFold #273

Merged
merged 77 commits into from
Mar 22, 2024
Merged
Show file tree
Hide file tree
Changes from 75 commits
Commits
Show all changes
77 commits
Select commit Hold shift + click to select a range
e63ea22
skeleton
mpenciak Jan 19, 2024
3f1c2bc
(wip) scalar <-> base confusion
mpenciak Jan 19, 2024
24eb599
(wip) fix W_new def
mpenciak Jan 22, 2024
9b0c6a9
(wip) fixed base <-> scalar confusion
mpenciak Jan 23, 2024
49fe8e4
(wip) new gadget scaffolding and allocated witnesses
mpenciak Jan 24, 2024
600e601
(wip) fix prove_step
mpenciak Jan 24, 2024
58c528f
(wip) synthesize_non_base_case
mpenciak Jan 25, 2024
3b373c8
(wip) synthesize
mpenciak Jan 25, 2024
5ec2882
(wip) synthesize_base_case
mpenciak Jan 25, 2024
e1adb35
(wip) fix absorbs
mpenciak Jan 25, 2024
fd5f5b9
(wip) stuck
mpenciak Jan 25, 2024
e324109
(wip) CommitmentKey macro
mpenciak Jan 29, 2024
9b68ff5
(wip) some gadgets filled
mpenciak Jan 31, 2024
dd60109
(wip) some more progress
mpenciak Feb 1, 2024
de9fbbe
(wip) Gadgets done, some cleanup
mpenciak Feb 4, 2024
bdcd68d
(wip) Scalar <-> Base confusion in verify
mpenciak Feb 5, 2024
ea69936
it builds!
mpenciak Feb 5, 2024
56e0b59
make clippy happy
mpenciak Feb 5, 2024
bf01a0b
Delete `RecursiveSNARKTrait` and cleanup
mpenciak Feb 5, 2024
787adda
refactor: Refactor data types and function signatures in Cyclefold mo…
huitseeker Feb 11, 2024
ecdc1c2
refactor: remove uneeded params in PublicParams, RecursiveSNARK
huitseeker Feb 11, 2024
b09059a
refactor: Remove option in CycleFoldInputs, remove a few needless typ…
huitseeker Feb 11, 2024
a169a23
test: use expect_test on brittle test
huitseeker Feb 11, 2024
40952a2
chore: update expect tests
huitseeker Feb 11, 2024
14dc4f1
(wip) addressing comments
mpenciak Feb 13, 2024
72a25cc
(wip) add recursive_snark test
mpenciak Feb 13, 2024
d7e30cf
(wip) add generic bounds for allocatedr1csinstances
mpenciak Feb 15, 2024
7f488bc
make the cyclefold test more **fun**
mpenciak Feb 15, 2024
ca4f46e
fix cyclefold circuit IO
mpenciak Feb 20, 2024
a3a722d
uncomment num_io cyclefold check
mpenciak Feb 20, 2024
6b46449
update constant
mpenciak Feb 20, 2024
eb92e4e
fix link
mpenciak Feb 20, 2024
87d1695
cleanup output
mpenciak Feb 20, 2024
7697e64
last couple circuit pieces
mpenciak Feb 20, 2024
6463bd9
add comm_T to inputs and add cyclefold IO checks
mpenciak Feb 20, 2024
7cb4a10
fix ro absorb numbers
mpenciak Feb 20, 2024
ee8cf69
remove extra unneeded comm_T allocation
mpenciak Feb 21, 2024
315d1ce
properly constrain `always_equal` in `mult_mod` and `red_mod`
mpenciak Feb 21, 2024
42830f5
some allocation fixes
mpenciak Feb 26, 2024
178bb1f
eliminate clone
mpenciak Feb 26, 2024
ceb9c6b
make RO absorb numbers make sense
mpenciak Feb 26, 2024
6a63178
fix cyclefold scalar alloc
mpenciak Feb 27, 2024
734dead
chore: update Bn256Engine -> Bn256EngineKZG
huitseeker Feb 27, 2024
fb85877
chore: run clippy
huitseeker Feb 27, 2024
ab73fa9
update `expect_test`s
mpenciak Feb 28, 2024
d1afdea
fix EmulatedCurveParam allocation
mpenciak Feb 28, 2024
e47d8ae
fix nifs RO absorb count
mpenciak Feb 28, 2024
3a3558c
make `test_augmented_circuit_size` an `expect_test`
mpenciak Feb 28, 2024
8d23795
fix: typo
mpenciak Feb 28, 2024
f630faf
fix: `RecursiveSNARK::new` sets i to 0
mpenciak Feb 28, 2024
695ff0c
fix: Fix RO absorb count in verify
mpenciak Feb 28, 2024
bd3076d
fix: `RecursiveSNARK::new` should set r_*_primary to default values
mpenciak Feb 28, 2024
2aebeb3
u <-> U in folding data Alloc
mpenciak Mar 1, 2024
bccabb6
fix: add trivialization for cyclefold checks in base case
mpenciak Mar 1, 2024
8cdfea3
make prove_verify test more fun
mpenciak Mar 1, 2024
a2d1ed8
fix: fix hashing order
mpenciak Mar 2, 2024
7445a59
fix: r_bools was always None
mpenciak Mar 3, 2024
4fab7cb
make prove_verify test longer
mpenciak Mar 3, 2024
051bab8
clippy
mpenciak Mar 3, 2024
b4dc789
test_augmented_circuit_size should check synthesis works
mpenciak Mar 3, 2024
40abbec
chore: fix rebase
mpenciak Mar 3, 2024
07d92c9
chore: bump msrv
mpenciak Mar 3, 2024
90cc205
chore: cleanup, documentation, and split cyclefold test
mpenciak Mar 6, 2024
13d146f
fix: Fix CycleFold circuit IO to only have arity 4
mpenciak Mar 7, 2024
59577f6
chore: update cyclefold_circuit_size expecttest
mpenciak Mar 7, 2024
e735e9e
fix: fix RO absorb counts and logic
mpenciak Mar 7, 2024
6381ccf
chore: update cyclefold primary circuit size expecttest
mpenciak Mar 7, 2024
0fafbeb
chore: cleanup and docs
mpenciak Mar 7, 2024
f912350
fix: fix rebase
mpenciak Mar 7, 2024
0232b8d
chore: fix clippy lints
mpenciak Mar 7, 2024
a123ba3
fix: constrain `AllocatedEmulPoint::default`
mpenciak Mar 8, 2024
8f0f425
tidy: use `AllocatedNum::add`
mpenciak Mar 8, 2024
67f9a92
chore: fix rebase errors in `src/gadgets`
mpenciak Mar 8, 2024
5d48fc6
fix: fix import
mpenciak Mar 8, 2024
b83d57c
chore: update expecttests
mpenciak Mar 8, 2024
938877b
tidy: add new constant
mpenciak Mar 22, 2024
497aef7
tidy: Cyclefold -> CycleFold
mpenciak Mar 22, 2024
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
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ 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.74.1"

[dependencies]
bellpepper-core = { version = "0.4.0", default-features = false }
Expand Down
2 changes: 2 additions & 0 deletions src/constants.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ pub(crate) const BN_N_LIMBS: usize = 4;
pub(crate) const NUM_FE_WITHOUT_IO_FOR_CRHF: usize = 9 + NIO_NOVA_FOLD * BN_N_LIMBS;
pub(crate) const NUM_FE_FOR_RO: usize = 9;
pub(crate) const NIO_NOVA_FOLD: usize = 2;
pub(crate) const NUM_FE_IN_EMULATED_POINT: usize = 2 * BN_N_LIMBS + 1;
pub(crate) const NIO_CYCLE_FOLD: usize = 4; // 1 per point (3) + scalar

/// Bit size of Nova field element hashes
pub const NUM_HASH_BITS: usize = 250;
288 changes: 288 additions & 0 deletions src/cyclefold/circuit.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,288 @@
//! This module defines Cyclefold circuit

use bellpepper_core::{
boolean::{AllocatedBit, Boolean},
ConstraintSystem, SynthesisError,
};
use ff::Field;
use neptune::{circuit2::poseidon_hash_allocated, poseidon::PoseidonConstants};

use crate::{
constants::NUM_CHALLENGE_BITS,
gadgets::{alloc_zero, le_bits_to_num, AllocatedPoint},
traits::{commitment::CommitmentTrait, Engine},
Commitment,
};
use bellpepper::gadgets::boolean_utils::conditionally_select;

/// A structure containing the CycleFold circuit inputs and implementing the synthesize function
pub struct CyclefoldCircuit<E: Engine> {
commit_1: Option<Commitment<E>>,
commit_2: Option<Commitment<E>>,
scalar: Option<[bool; NUM_CHALLENGE_BITS]>,
mpenciak marked this conversation as resolved.
Show resolved Hide resolved
poseidon_constants: PoseidonConstants<E::Base, generic_array::typenum::U2>,
}

impl<E: Engine> Default for CyclefoldCircuit<E> {
fn default() -> Self {
let poseidon_constants = PoseidonConstants::new();
Self {
commit_1: None,
commit_2: None,
scalar: None,
poseidon_constants,
}
}
}
impl<E: Engine> CyclefoldCircuit<E> {
/// Create a new CycleFold circuit with the given inputs
pub fn new(
commit_1: Option<Commitment<E>>,
commit_2: Option<Commitment<E>>,
scalar: Option<[bool; NUM_CHALLENGE_BITS]>,
) -> Self {
let poseidon_constants = PoseidonConstants::new();
Self {
commit_1,
commit_2,
scalar,
poseidon_constants,
}
}

fn alloc_witness<CS: ConstraintSystem<<E as Engine>::Base>>(
&self,
mut cs: CS,
) -> Result<
(
AllocatedPoint<E::GE>, // commit_1
AllocatedPoint<E::GE>, // commit_2
Vec<AllocatedBit>, // scalar
),
SynthesisError,
> {
let commit_1 = AllocatedPoint::alloc(
cs.namespace(|| "allocate C_1"),
self.commit_1.map(|C_1| C_1.to_coordinates()),
)?;
commit_1.check_on_curve(cs.namespace(|| "commit_1 on curve"))?;

let commit_2 = AllocatedPoint::alloc(
cs.namespace(|| "allocate C_2"),
self.commit_2.map(|C_2| C_2.to_coordinates()),
)?;
commit_2.check_on_curve(cs.namespace(|| "commit_2 on curve"))?;

let scalar: Vec<AllocatedBit> = self
.scalar
.unwrap_or([false; NUM_CHALLENGE_BITS])
.into_iter()
.enumerate()
.map(|(idx, bit)| {
AllocatedBit::alloc(cs.namespace(|| format!("scalar bit {idx}")), Some(bit))
})
.collect::<Result<Vec<_>, _>>()?;

Ok((commit_1, commit_2, scalar))
}

/// Synthesize the CycleFold circuit
pub fn synthesize<CS: ConstraintSystem<<E as Engine>::Base>>(
mpenciak marked this conversation as resolved.
Show resolved Hide resolved
&self,
mut cs: CS,
) -> Result<(), SynthesisError> {
let (C_1, C_2, r) = self.alloc_witness(cs.namespace(|| "allocate circuit witness"))?;

// Calculate C_final
let r_C_2 = C_2.scalar_mul(cs.namespace(|| "r * C_2"), &r)?;

let C_final = C_1.add(cs.namespace(|| "C_1 + r * C_2"), &r_C_2)?;

self.inputize_point(&C_1, cs.namespace(|| "inputize C_1"))?;
self.inputize_point(&C_2, cs.namespace(|| "inputize C_2"))?;
self.inputize_point(&C_final, cs.namespace(|| "inputize C_final"))?;

let scalar = le_bits_to_num(cs.namespace(|| "get scalar"), &r)?;

scalar.inputize(cs.namespace(|| "scalar"))?;

Ok(())
}

// Represent the point in the public IO as its 2-ary Poseidon hash
fn inputize_point<CS>(
&self,
point: &AllocatedPoint<E::GE>,
mut cs: CS,
) -> Result<(), SynthesisError>
where
E: Engine,
CS: ConstraintSystem<E::Base>,
{
let (x, y, is_infinity) = point.get_coordinates();
let preimage = vec![x.clone(), y.clone()];
let val = poseidon_hash_allocated(
cs.namespace(|| "hash point"),
preimage,
&self.poseidon_constants,
)?;

let zero = alloc_zero(cs.namespace(|| "zero"));

let is_infinity_bit = AllocatedBit::alloc(
cs.namespace(|| "is_infinity"),
Some(is_infinity.get_value().unwrap_or(E::Base::ONE) == E::Base::ONE),
)?;

cs.enforce(
|| "infinity_bit matches",
|lc| lc,
|lc| lc,
|lc| lc + is_infinity_bit.get_variable() - is_infinity.get_variable(),
);

// Output 0 when it is the point at infinity
let output = conditionally_select(
cs.namespace(|| "select output"),
&zero,
&val,
&Boolean::from(is_infinity_bit),
)?;

output.inputize(cs.namespace(|| "inputize hash"))?;

Ok(())
}
}

#[cfg(test)]
mod tests {
use expect_test::{expect, Expect};
use ff::{Field, PrimeField, PrimeFieldBits};
use neptune::Poseidon;
use rand_core::OsRng;

use crate::{
bellpepper::{
r1cs::{NovaShape, NovaWitness},
shape_cs::ShapeCS,
solver::SatisfyingAssignment,
},
constants::NIO_CYCLE_FOLD,
gadgets::scalar_as_base,
provider::{Bn256EngineKZG, PallasEngine, Secp256k1Engine},
traits::{commitment::CommitmentEngineTrait, snark::default_ck_hint, CurveCycleEquipped, Dual},
};

use super::*;

fn test_cyclefold_circuit_size_with<E1>(expected_constraints: &Expect, expected_vars: &Expect)
where
E1: CurveCycleEquipped,
{
// Instantiate the circuit with trivial inputs
let circuit: CyclefoldCircuit<Dual<E1>> = CyclefoldCircuit::default();

// Synthesize the R1CS shape
let mut cs: ShapeCS<E1> = ShapeCS::new();
let _ = circuit.synthesize(cs.namespace(|| "synthesizing shape"));

// Extract the number of constraints and variables
let num_constraints = cs.num_constraints();
let num_variables = cs.num_aux();
let num_io = cs.num_inputs();

// Check the number of constraints and variables match the expected values
expected_constraints.assert_eq(&num_constraints.to_string());
expected_vars.assert_eq(&num_variables.to_string());
assert_eq!(num_io, NIO_CYCLE_FOLD + 1); // includes 1
}

#[test]
fn test_cyclefold_circuit_size() {
test_cyclefold_circuit_size_with::<PallasEngine>(&expect!("2090"), &expect!("2081"));
test_cyclefold_circuit_size_with::<Bn256EngineKZG>(&expect!("2090"), &expect!("2081"));
test_cyclefold_circuit_size_with::<Secp256k1Engine>(&expect!("2090"), &expect!("2081"));
}

fn test_cyclefold_circuit_sat_with<E: CurveCycleEquipped>() {
let rng = OsRng;

let ck = <<Dual<E> as Engine>::CE as CommitmentEngineTrait<Dual<E>>>::setup(b"test", 5);

// Generate random vectors to commit to
let v1 = (0..5)
.map(|_| <<Dual<E> as Engine>::Scalar as Field>::random(rng))
.collect::<Vec<_>>();
let v2 = (0..5)
.map(|_| <<Dual<E> as Engine>::Scalar as Field>::random(rng))
.collect::<Vec<_>>();

// Calculate the random commitments
let C_1 = <<Dual<E> as Engine>::CE as CommitmentEngineTrait<Dual<E>>>::commit(&ck, &v1);
let C_2 = <<Dual<E> as Engine>::CE as CommitmentEngineTrait<Dual<E>>>::commit(&ck, &v2);

// Generate a random scalar
let val: u128 = rand::random();
let r = <<Dual<E> as Engine>::Scalar as PrimeField>::from_u128(val);
let r_bits = r
.to_le_bits()
.into_iter()
.map(Some)
.collect::<Option<Vec<_>>>()
.map(|mut vec| {
vec.resize_with(128, || false);
vec.try_into().unwrap()
});

let circuit: CyclefoldCircuit<Dual<E>> = CyclefoldCircuit::new(Some(C_1), Some(C_2), r_bits);

// Calculate the result out of circuit
let native_result = C_1 + C_2 * r;

// Generate the R1CS shape and commitment key
let mut cs: ShapeCS<E> = ShapeCS::new();
let _ = circuit.synthesize(cs.namespace(|| "synthesizing shape"));
let (shape, ck) = cs.r1cs_shape_and_key(&*default_ck_hint());

// Synthesize the R1CS circuit on the random inputs
let mut cs = SatisfyingAssignment::<E>::new();
circuit
.synthesize(cs.namespace(|| "synthesizing witness"))
.unwrap();

let (instance, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();
let X = &instance.X;

// Helper functio to calculate the hash
let compute_hash = |P: Commitment<Dual<E>>| -> E::Scalar {
let (x, y, is_infinity) = P.to_coordinates();
if is_infinity {
return E::Scalar::ZERO;
}

let mut hasher = Poseidon::new_with_preimage(&[x, y], &circuit.poseidon_constants);

hasher.hash()
};

// Check the circuit calculates the right thing
let hash_1 = compute_hash(C_1);
assert_eq!(hash_1, X[0]);
let hash_2 = compute_hash(C_2);
assert_eq!(hash_2, X[1]);
let hash_res = compute_hash(native_result);
assert_eq!(hash_res, X[2]);
assert_eq!(r, scalar_as_base::<E>(X[3]));

// Check the R1CS equation is satisfied
shape.is_sat(&ck, &instance, &witness).unwrap();
}
mpenciak marked this conversation as resolved.
Show resolved Hide resolved

#[test]
fn test_cyclefold_circuit_sat() {
test_cyclefold_circuit_sat_with::<PallasEngine>();
test_cyclefold_circuit_sat_with::<Bn256EngineKZG>();
test_cyclefold_circuit_sat_with::<Secp256k1Engine>();
}
}
Loading
Loading