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.

Sign up for GitHub

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

Mark variables with segment numbers #341

Open
wants to merge 10 commits into
base: main
Choose a base branch
from
Open

Mark variables with segment numbers #341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
2112360
Squashed commit of the following:
Forpee Nov 6, 2024
9df429a
chore: delete dead code, attribute original sources
Forpee Nov 7, 2024
93e3b62
chore: rm precommitted var
Forpee Nov 7, 2024
3baeef8
chore: rm unused var
Forpee Nov 7, 2024
c06bd03
chore: cleanup deadcode and clippy warnings
Forpee Nov 12, 2024
54cfd7d
chore: cleanup up dead comment
Forpee Nov 26, 2024
35284ef
Add segment number to namespace
Acentelles Dec 4, 2024
b2e749f
chore: cleanup
Acentelles Dec 17, 2024
ff12f2d
feat: update newer code with segments
Acentelles Dec 17, 2024
822d6d1
chore: merge conflicts
Acentelles Dec 17, 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
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ name = "ppsnark"
harness = false

[features]
default = ["halo2curves/asm"]
# default = ["halo2curves/asm"]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: bring this back?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can bring it back. The reason is that I get the following error when I compile the code with this default enabled:

Currently feature `asm` can only be enabled on x86_64 arch.

This means that the assembly optimizations feature in halo2curves is only compatible with x86_64 architecture processors, and I am running an ARM processor (Apple M3 in particular).

Maybe I can open an issue with it. What do you think?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For non-x86 platforms, one could use --no-default-features. See for example:

https://github.com/microsoft/Nova?tab=readme-ov-file#tests-and-examples

# Compiles in portable mode, w/o ISA extensions => binary can be executed on all systems.
portable = ["pasta-msm/portable"]
flamegraph = ["pprof/flamegraph", "pprof/criterion"]
30 changes: 15 additions & 15 deletions examples/and.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ pub fn u64_into_bit_vec_le<Scalar: PrimeField, CS: ConstraintSystem<Scalar>>(
let bits = values
.into_iter()
.enumerate()
.map(|(i, b)| AllocatedBit::alloc(cs.namespace(|| format!("bit {}", i)), b))
.map(|(i, b)| AllocatedBit::alloc(cs.namespace(|| (i, format!("bit {}", i))), b))
.collect::<Result<Vec<_>, SynthesisError>>()?;

Ok(bits)
Expand Down Expand Up @@ -114,11 +114,11 @@ where
});
coeff = coeff.double();
}
let num = AllocatedNum::alloc(cs.namespace(|| "Field element"), || {
let num = AllocatedNum::alloc(cs.namespace(|| (0, "Field element")), || {
fe.ok_or(SynthesisError::AssignmentMissing)
})?;
lc = lc - num.get_variable();
cs.enforce(|| "compute number from bits", |lc| lc, |lc| lc, |_| lc);
cs.enforce(|| (1, "compute number from bits"), |lc| lc, |lc| lc, |_| lc);
Ok(num)
}

Expand All @@ -134,35 +134,35 @@ impl<G: Group> StepCircuit<G::Scalar> for AndCircuit<G> {
) -> Result<Vec<AllocatedNum<G::Scalar>>, SynthesisError> {
for i in 0..self.batch.len() {
// allocate a and b as field elements
let a = AllocatedNum::alloc(cs.namespace(|| format!("a_{}", i)), || {
let a = AllocatedNum::alloc(cs.namespace(|| (i, format!("a_{}", i))), || {
Ok(G::Scalar::from(self.batch[i].a))
})?;
let b = AllocatedNum::alloc(cs.namespace(|| format!("b_{}", i)), || {
let b = AllocatedNum::alloc(cs.namespace(|| (i, format!("b_{}", i))), || {
Ok(G::Scalar::from(self.batch[i].b))
})?;

// obtain bit representations of a and b
let a_bits = u64_into_bit_vec_le(
cs.namespace(|| format!("a_bits_{}", i)),
cs.namespace(|| (i, format!("a_bits_{}", i))),
Some(self.batch[i].a),
)?; // little endian
let b_bits = u64_into_bit_vec_le(
cs.namespace(|| format!("b_bits_{}", i)),
cs.namespace(|| (i, format!("b_bits_{}", i))),
Some(self.batch[i].b),
)?; // little endian

// enforce that bits of a and b are correct
let a_from_bits = le_bits_to_num(cs.namespace(|| format!("a_{}", i)), &a_bits)?;
let b_from_bits = le_bits_to_num(cs.namespace(|| format!("b_{}", i)), &b_bits)?;
let a_from_bits = le_bits_to_num(cs.namespace(|| (i, format!("a_{}", i))), &a_bits)?;
let b_from_bits = le_bits_to_num(cs.namespace(|| (i, format!("b_{}", i))), &b_bits)?;

cs.enforce(
|| format!("a_{} == a_from_bits", i),
|| (i, format!("a_{} == a_from_bits", i)),
|lc| lc + a.get_variable(),
|lc| lc + CS::one(),
|lc| lc + a_from_bits.get_variable(),
);
cs.enforce(
|| format!("b_{} == b_from_bits", i),
|| (i, format!("b_{} == b_from_bits", i)),
|lc| lc + b.get_variable(),
|lc| lc + CS::one(),
|lc| lc + b_from_bits.get_variable(),
Expand All @@ -173,23 +173,23 @@ impl<G: Group> StepCircuit<G::Scalar> for AndCircuit<G> {
// perform bitwise AND
for i in 0..64 {
let c_bit = AllocatedBit::and(
cs.namespace(|| format!("and_bit_{}", i)),
cs.namespace(|| (i, format!("and_bit_{}", i))),
&a_bits[i],
&b_bits[i],
)?;
c_bits.push(c_bit);
}

// convert back to an allocated num
let c_from_bits = le_bits_to_num(cs.namespace(|| format!("c_{}", i)), &c_bits)?;
let c_from_bits = le_bits_to_num(cs.namespace(|| (i, format!("c_{}", i))), &c_bits)?;

let c = AllocatedNum::alloc(cs.namespace(|| format!("c_{}", i)), || {
let c = AllocatedNum::alloc(cs.namespace(|| (i, format!("c_{}", i))), || {
Ok(G::Scalar::from(self.batch[i].a & self.batch[i].b))
})?;

// enforce that c is correct
cs.enforce(
|| format!("c_{} == c_from_bits", i),
|| (i, format!("c_{} == c_from_bits", i)),
|lc| lc + c.get_variable(),
|lc| lc + CS::one(),
|lc| lc + c_from_bits.get_variable(),
Expand Down
6 changes: 3 additions & 3 deletions examples/hashchain.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ impl<G: Group> StepCircuit<G::Scalar> for HashChainCircuit<G> {

// allocate x_i
let x_i = (0..self.num_elts_per_step)
.map(|i| AllocatedNum::alloc(cs.namespace(|| format!("x_{}", i)), || Ok(self.x_i[i])))
.map(|i| AllocatedNum::alloc(cs.namespace(|| (i, format!("x_{}", i))), || Ok(self.x_i[i])))
.collect::<Result<Vec<_>, _>>()?;

// concatenate z_in and x_i
Expand All @@ -80,7 +80,7 @@ impl<G: Group> StepCircuit<G::Scalar> for HashChainCircuit<G> {
let parameter = IOPattern(vec![SpongeOp::Absorb(num_absorbs), SpongeOp::Squeeze(1u32)]);

let pc = Sponge::<G::Scalar, U24>::api_constants(Strength::Standard);
let mut ns = cs.namespace(|| "ns");
let mut ns = cs.namespace(|| (0, "ns"));

let z_out = {
let mut sponge = SpongeCircuit::new_with_constants(&pc, Simplex);
Expand All @@ -91,7 +91,7 @@ impl<G: Group> StepCircuit<G::Scalar> for HashChainCircuit<G> {

let output = SpongeAPI::squeeze(&mut sponge, 1, acc);
sponge.finish(acc).unwrap();
Elt::ensure_allocated(&output[0], &mut ns.namespace(|| "ensure allocated"), true)?
Elt::ensure_allocated(&output[0], &mut ns.namespace(|| (1, "ensure allocated")), true)?
};

Ok(vec![z_out])
Expand Down
8 changes: 4 additions & 4 deletions examples/minroot.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ impl<G: Group> StepCircuit<G::Scalar> for MinRootCircuit<G> {
for i in 0..self.seq.len() {
// non deterministic advice
let x_i_plus_1 =
AllocatedNum::alloc(cs.namespace(|| format!("x_i_plus_1_iter_{i}")), || {
AllocatedNum::alloc(cs.namespace(|| (i, format!("x_i_plus_1_iter_{i}"))), || {
Ok(self.seq[i].x_i_plus_1)
})?;

Expand All @@ -115,11 +115,11 @@ impl<G: Group> StepCircuit<G::Scalar> for MinRootCircuit<G> {
// (ii) y_i_plus_1 = x_i
// (1) constraints for condition (i) are below
// (2) constraints for condition (ii) is avoided because we just used x_i wherever y_i_plus_1 is used
let x_i_plus_1_sq = x_i_plus_1.square(cs.namespace(|| format!("x_i_plus_1_sq_iter_{i}")))?;
let x_i_plus_1_sq = x_i_plus_1.square(cs.namespace(|| (i, format!("x_i_plus_1_sq_iter_{i}"))))?;
let x_i_plus_1_quad =
x_i_plus_1_sq.square(cs.namespace(|| format!("x_i_plus_1_quad_{i}")))?;
x_i_plus_1_sq.square(cs.namespace(|| (i, format!("x_i_plus_1_quad_{i}"))))?;
cs.enforce(
|| format!("x_i_plus_1_quad * x_i_plus_1 = x_i + y_i_iter_{i}"),
|| (i, format!("x_i_plus_1_quad * x_i_plus_1 = x_i + y_i_iter_{i}")),
|lc| lc + x_i_plus_1_quad.get_variable(),
|lc| lc + x_i_plus_1.get_variable(),
|lc| lc + x_i.get_variable() + y_i.get_variable(),
Expand Down
68 changes: 34 additions & 34 deletions src/circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,17 +129,17 @@ impl<'a, E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'a, E, SC> {
> {
// Allocate the params
let params = alloc_scalar_as_base::<E, _>(
cs.namespace(|| "params"),
cs.namespace(|| (0, "params")),
self.inputs.as_ref().map(|inputs| inputs.params),
)?;

// Allocate i
let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
let i = AllocatedNum::alloc(cs.namespace(|| (1, "i")), || Ok(self.inputs.get()?.i))?;

// Allocate z0
let z_0 = (0..arity)
.map(|i| {
AllocatedNum::alloc(cs.namespace(|| format!("z0_{i}")), || {
AllocatedNum::alloc(cs.namespace(|| (i, format!("z0_{i}"))), || {
Ok(self.inputs.get()?.z0[i])
})
})
Expand All @@ -149,43 +149,43 @@ impl<'a, E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'a, E, SC> {
let zero = vec![E::Base::ZERO; arity];
let z_i = (0..arity)
.map(|i| {
AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
AllocatedNum::alloc(cs.namespace(|| (i, format!("zi_{i}"))), || {
Ok(self.inputs.get()?.zi.as_ref().unwrap_or(&zero)[i])
})
})
.collect::<Result<Vec<AllocatedNum<E::Base>>, _>>()?;

// Allocate the running instance
let U: AllocatedRelaxedR1CSInstance<E> = AllocatedRelaxedR1CSInstance::alloc(
cs.namespace(|| "Allocate U"),
cs.namespace(|| (2, "Allocate U")),
self.inputs.as_ref().and_then(|inputs| inputs.U.as_ref()),
self.params.limb_width,
self.params.n_limbs,
)?;

// Allocate ri
let r_i = AllocatedNum::alloc(cs.namespace(|| "ri"), || {
let r_i = AllocatedNum::alloc(cs.namespace(|| (3, "ri")), || {
Ok(self.inputs.get()?.ri.unwrap_or(E::Base::ZERO))
})?;

// Allocate r_i+1
let r_next = AllocatedNum::alloc(cs.namespace(|| "r_i+1"), || Ok(self.inputs.get()?.r_next))?;
let r_next = AllocatedNum::alloc(cs.namespace(|| (4, "r_i+1")), || Ok(self.inputs.get()?.r_next))?;

// Allocate the instance to be folded in
let u = AllocatedR1CSInstance::alloc(
cs.namespace(|| "allocate instance u to fold"),
cs.namespace(|| (5, "allocate instance u to fold")),
self.inputs.as_ref().and_then(|inputs| inputs.u.as_ref()),
)?;

// Allocate T
let T = AllocatedPoint::alloc(
cs.namespace(|| "allocate T"),
cs.namespace(|| (6, "allocate T")),
self
.inputs
.as_ref()
.and_then(|inputs| inputs.T.map(|T| T.to_coordinates())),
)?;
T.check_on_curve(cs.namespace(|| "check T on curve"))?;
T.check_on_curve(cs.namespace(|| (7, "check T on curve")))?;

Ok((params, i, z_0, z_i, U, r_i, r_next, u, T))
}
Expand All @@ -199,14 +199,14 @@ impl<'a, E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'a, E, SC> {
let U_default: AllocatedRelaxedR1CSInstance<E> = if self.params.is_primary_circuit {
// The primary circuit just returns the default R1CS instance
AllocatedRelaxedR1CSInstance::default(
cs.namespace(|| "Allocate U_default"),
cs.namespace(|| (0, "Allocate U_default")),
self.params.limb_width,
self.params.n_limbs,
)?
} else {
// The secondary circuit returns the incoming R1CS instance
AllocatedRelaxedR1CSInstance::from_r1cs_instance(
cs.namespace(|| "Allocate U_default"),
cs.namespace(|| (1, "Allocate U_default")),
u,
self.params.limb_width,
self.params.n_limbs,
Expand Down Expand Up @@ -243,20 +243,20 @@ impl<'a, E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'a, E, SC> {
for e in z_i {
ro.absorb(e);
}
U.absorb_in_ro(cs.namespace(|| "absorb U"), &mut ro)?;
U.absorb_in_ro(cs.namespace(|| (0, "absorb U")), &mut ro)?;
ro.absorb(r_i);

let hash_bits = ro.squeeze(cs.namespace(|| "Input hash"), NUM_HASH_BITS)?;
let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), &hash_bits)?;
let hash_bits = ro.squeeze(cs.namespace( || (1, "Input hash")), NUM_HASH_BITS)?;
let hash = le_bits_to_num(cs.namespace(|| (2, "bits to hash")), &hash_bits)?;
let check_pass = alloc_num_equals(
cs.namespace(|| "check consistency of u.X[0] with H(params, U, i, z0, zi)"),
cs.namespace(|| (3, "check consistency of u.X[0] with H(params, U, i, z0, zi)")),
&u.X0,
&hash,
)?;

// Run NIFS Verifier
let U_fold = U.fold_with_r1cs(
cs.namespace(|| "compute fold of U and u"),
cs.namespace(|| (4, "compute fold of U and u")),
params,
u,
T,
Expand All @@ -279,19 +279,19 @@ impl<E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'_, E, SC> {

// Allocate all witnesses
let (params, i, z_0, z_i, U, r_i, r_next, u, T) =
self.alloc_witness(cs.namespace(|| "allocate the circuit witness"), arity)?;
self.alloc_witness(cs.namespace(|| (0, "allocate the circuit witness")), arity)?;

// Compute variable indicating if this is the base case
let zero = alloc_zero(cs.namespace(|| "zero"));
let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?;
let zero = alloc_zero(cs.namespace(|| (1, "zero")));
let is_base_case = alloc_num_equals(cs.namespace(|| (2, "Check if base case")), &i.clone(), &zero)?;

// Synthesize the circuit for the base case and get the new running instance
let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"), u.clone())?;
let Unew_base = self.synthesize_base_case(cs.namespace(|| (3, "base case") ), u.clone())?;

// Synthesize the circuit for the non-base case and get the new running
// instance along with a boolean indicating if all checks have passed
let (Unew_non_base, check_non_base_pass) = self.synthesize_non_base_case(
cs.namespace(|| "synthesize non base case"),
cs.namespace(|| (4, "synthesize non base case")),
&params,
&i,
&z_0,
Expand All @@ -305,46 +305,46 @@ impl<E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'_, E, SC> {

// Either check_non_base_pass=true or we are in the base case
let should_be_false = AllocatedBit::nor(
cs.namespace(|| "check_non_base_pass nor base_case"),
cs.namespace(|| (5, "check_non_base_pass nor base_case")),
&check_non_base_pass,
&is_base_case,
)?;
cs.enforce(
|| "check_non_base_pass nor base_case = false",
|| (6, "check_non_base_pass nor base_case = false"),
|lc| lc + should_be_false.get_variable(),
|lc| lc + CS::one(),
|lc| lc,
);

// Compute the U_new
let Unew = Unew_base.conditionally_select(
cs.namespace(|| "compute U_new"),
cs.namespace(|| (7, "compute U_new")),
&Unew_non_base,
&Boolean::from(is_base_case.clone()),
)?;

// Compute i + 1
let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
let i_new = AllocatedNum::alloc(cs.namespace(|| (8, "i + 1")), || {
Ok(*i.get_value().get()? + E::Base::ONE)
})?;
cs.enforce(
|| "check i + 1",
|| (9, "check i + 1"),
|lc| lc,
|lc| lc,
|lc| lc + i_new.get_variable() - CS::one() - i.get_variable(),
);

// Compute z_{i+1}
let z_input = conditionally_select_vec(
cs.namespace(|| "select input to F"),
cs.namespace(|| (10, "select input to F")),
&z_0,
&z_i,
&Boolean::from(is_base_case),
)?;

let z_next = self
.step_circuit
.synthesize(&mut cs.namespace(|| "F"), &z_input)?;
.synthesize(&mut cs.namespace(|| (11, "F")), &z_input)?;

if z_next.len() != arity {
return Err(SynthesisError::IncompatibleLengthVector(
Expand All @@ -362,15 +362,15 @@ impl<E: Engine, SC: StepCircuit<E::Base>> NovaAugmentedCircuit<'_, E, SC> {
for e in &z_next {
ro.absorb(e);
}
Unew.absorb_in_ro(cs.namespace(|| "absorb U_new"), &mut ro)?;
Unew.absorb_in_ro(cs.namespace(|| (12, "absorb U_new") ), &mut ro)?;
ro.absorb(&r_next);
let hash_bits = ro.squeeze(cs.namespace(|| "output hash bits"), NUM_HASH_BITS)?;
let hash = le_bits_to_num(cs.namespace(|| "convert hash to num"), &hash_bits)?;
let hash_bits = ro.squeeze(cs.namespace(|| (13, "output hash bits")), NUM_HASH_BITS)?;
let hash = le_bits_to_num(cs.namespace(|| (14, "convert hash to num")), &hash_bits)?;

// Outputs the computed hash and u.X[1] that corresponds to the hash of the other circuit
u.X1
.inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
.inputize(cs.namespace(|| (15, "Output unmodified hash of the other circuit")))?;
hash.inputize(cs.namespace(|| (16, "output new hash of this circuit")))?;

Ok(z_next)
}
Expand Down
Loading
Loading