lurk-lab / bellpepper Goto Github PK

dev at c0ebcf4 does not include main at 46a3cc4

dev at 9713be6 does not include main at d5953a8

dev at 6b73bc8 does not include main at 029eaad

dev at 31973e1 does not include main at 10e5b56

Examples for the use case

In Lurk
https://github.com/lurk-lab/lurk-rs/blob/e0fab1e2e45f13ba7e4b91e9aa670ec9e9a7ae12/src/circuit/gadgets/constraints.rs#L77-L116

In Arecibo:
https://github.com/lurk-lab/arecibo/pull/48/files#diff-f6708c51fe2bbf307a08ab3f84fd892309b0f4cf87ff55dc2f274e3e46d5c862R600-R618

Is there any way that one could import existing circom templates to use as gadgets in bellpepper?

dev at dfb7973 does not include main at 183be2a

The rust version specified in rust-toolchain.toml (1.75.0) is out of date with the latest stable (1.76.0).

Check the rust version check workflow for details.

This issue was raised by the workflow at https://github.com/lurk-lab/bellpepper/actions/runs/7879590416/workflow.

dev at ad19857 does not include main at 56bbddf

WitnessCS::new pre-populates ONE among the inputs:

But WitnessCS::with_capacity, introduced in #60 does not, which is likely to trip users:

We should fix this before any release of bellpepper.

Issue

The recent PR #88 introduces a new behavior for Num::add, favouring None to Some(v) as a result in (Some(v), None) | (None, Some(v) cases.

This new behavior seems to break the current implementation of PoseidonROCircuit::squeeze in arecibo. In this method we actually call the SpongeCircuit::absorb method with the current state elements, that do not have any values at that stage.

In neptune absorb will call add_rate_element with a Num::add that results on a None variant, transmitted to the set_element method that leverages an unwrap on the value and thus panicking.

I'm not sure about the correct way to fix this, so I'm looking for inputs.

How to reproduce

This bug has been found while leveraging the Bn256EngineKZG engine at PublicParams::setup both for Nova & Supernova. You can reproduce it on your machine by running this test on ethereum-lc/aggpk

I was also able to reproduce it on the aptos-lc if patching both belpepper & bellpepper-core to dev.

dev at 1dd644c does not include main at 8f8c6e3

dev at e8b9acc does not include main at 7422cd4

dev at 9daad54 does not include main at 00f0eac

dev at e1b2132 does not include main at cdff470

When folding an R1CS circuit, the cross-term computation
$$T = AZ_1 ◦ BZ_2 + AZ_2 ◦ BZ_1 − u_1CZ_2 − u_2CZ_1$$
can be computed more efficiently when the circuit takes advantage of linear constraints of the form:
$$0=\sum_i C_{i,j} \cdot z_i.$$
Specifically, this corresponds to a constraint where the linear combinations in the rows $A_j, B_j$ are equal to zero.
If this is the case, then the $j$-th component of $T$ will always be equal to zero, and the computation for the $j$-th constraint can be avoided entirely.
Moreover, the computation of the commitment to $T$ can also be optimized to skip the entries corresponding to linear constraints.

In order to encourage the use of linear constraints, I propose adding the two following methods to the ConstraintSystem trait.

 /// Enforce that `A` = 0. The `annotation` function is invoked in testing contexts
 /// in order to derive a unique name for the constraint in the current namespace.
 fn enforce_eq_zero<A, AR, LA>(&mut self, annotation: A, a: LA)
   where
       A: FnOnce() -> AR,
       AR: Into<String>,
       LA: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar> {
   self.enforce(annotation, |_| LinearCombination::zero(), |_| LinearCombination::zero(), a);
 }

 /// Enforce that `A` = `B`. The `annotation` function is invoked in testing contexts
 /// in order to derive a unique name for the constraint in the current namespace.
 fn enforce_eq<A, AR, LA, LB>(&mut self, annotation: A, a: LA, b: LB)
   where
       A: FnOnce() -> AR,
       AR: Into<String>,
       LA: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar>,
       LB: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar> {
   let zero = a(LinearCombination::zero()) - b(LinearCombination::zero());
   self.enforce_eq_zero(annotation, |_| zero);
 }

Both of these functions can have default implementation defined in terms of the existing enforce function definition, avoiding backwards-compatibility issues. However, it allows folding-specific ConstraintSystems to choose to handle linear constraints differently.

CI equivalent to bellperson and branch protection equivalent to neptune/lurk-rs should be set up.

Some rought spots publishing 0.2.0 with @porcuquine today:

1. check the cargo release version, folks don’t update this one frequently
2. the Makefile publishes all tags, that’s not good if the operator’s local tags include those form a remote of the forked project,
3. the packages are interdependent, so we need to instruct cargo-release on the dependency,
4. and we probably need some massaging with cargo-release so that the path dependency from bellpepper-core to bellpepper doesn’t prevent the operator from publishing.

I'm learning the implementation of bellpepper. The Indexer in lc mod caught my attention, it is mainly used to maintain some (k, v) pairs and is required to be sorted by k. Its insert_or_update method will affect the performance of LinearCombination.

This is the original implementation of Indexer and its insert_or_update:

struct Indexer<T> {
     /// Stores a list of `T` indexed by the number in the first slot of the tuple.
     values: Vec<(usize, T)>,
     /// `(index, key)` of the last insertion operation. Used to optimize consecutive operations
     last_inserted: Option<(usize, usize)>,
}

I think the function can also be achieved with BTreeMap, and the insertion of BTreeMap may be faster than Vector. Because when inserting in the middle of Vector, all remaining elements need to be moved.

Here is the modified one:

struct Indexer<T> {
    values: BTreeMap<usize, T>,
}

https://github.com/zkp-learning/bellpepper/blob/22f81bb64e977cab6a34f26234c56d2f685aec0d/crates/bellpepper-core/src/lc.rs#L70

But the results show that origin implementation is faster in most cases:

detail: https://github.com/zkp-learning/bellpepper-bench#readme

I think this is because the time complexity of the original implementation is O(1) when inserting in order, while BTreeMap is O(log n).

dev at 156f17d does not include main at 964a18b

For example : #8
There may be reasons for this, as I suspect those PRs do not emit events, so as to not create recursive CI runs.

/cc @samuelburnham

dev at 93f2c1e does not include main at 542bf03

dev at 8ada98e does not include main at 133a764

dev at 63b4a4d does not include main at 02cdf17

Completely unconstrained allocations are a common source of programmer error, leading to soundness bugs, when writing circuits. This class of error can be completely detected at circuit-shape-synthesis-time.

Bellpepper already inherits (from bellperson/bellman) an error intended to signal this condition:

We should add support to check synthesized constraint systems for this — either at program run-time, or in tests. Ideally, this would be implemented such that there is no cost if the check is never performed.

Since there are legitimate reasons to allocate unconstrained values, we will need to add a new operation (say, AllocatedNum::alloc_unconstrained(…)), allowing circuit programmers to white-list such allocations. This will greatly improve clarity when this is actually desired, by forcing it to be declared explicitly.

When performing the optional check on a constraint system supporting it, unconstrained allocations that are declared as above should not result in an error. Conversely, declared unconstrained allocations that are in fact constrained should also result in an error. We will need a new error type for this.

The principle suggested here could be taken further, since constrained/unconstrained is a crude binary hammer. Consider that an AllocatedBit will be 'constrained' at the R1CS level, but may still represent a conceptually unconstrained allocation. Ideally, we could similarly catch such unconstrained (except for the booleanity constraint) AllocatedBits — with an equivalent whitelisted-allocation form.

Of course, this could get complicated and expensive. One possibility that might be viable in general is to include metadata during shape synthesis (when opting into a more expensive analysis mode) so that 'partial constraints' of the kind created by AllocatedBit on construction are recorded and can be ignored when attempting to determine whether a given variable has been fully constrained.

These checks should apply both to inputs and aux variables.

If we want this to be shared by many constraint systems, we might need some refactoring and common traits. In that case, Nova's ShapeCS, for example, should be considered.

The most obvious implementation approach would involve a set of all variables (or their indices), with variables removed from the set as they are encountered in (qualifying — if/when we implement that nuance) constraints. A bit field might be a reasonably performant way to instantiate the idea.

For example, a circuit with n constraints might have a field initialized to [0xFFu8; (n + 7) / 8]. Then as each constraint is encountered, the bit at position corresponding to its index is set to 0. If we also explicitly clear the bits corresponding to whitelisted vars, then any remaining non-zero bits correspond to unconstrained allocations which should be reported.

Or maybe that's overkill, and a simpler but heavier data structure will suffice.

As a final note, the existing error (which should be retained for compatibility by consumers who still use Groth16 with bellpepper) doesn't report which var was unconstrained — but it will be much more useful for debugging purposes to include it. So we may need a new error for this, as well as the constrained-but-whitelisted case (which should also report the offending variable).

dev at bf65ad8 does not include main at a05deaa

dev at 309fb9d does not include main at 3eef5c8

The rust version specified in rust-toolchain.toml (1.76.0) is out of date with the latest stable (1.78.0).

Check the rust version check workflow for details.

This issue was raised by the workflow at https://github.com/lurk-lab/bellpepper/actions/runs/8977420345/workflow.

dev at cc14447 does not include main at 4deb9d0

dev at 5bb775e does not include main at 5e2268a

From #55 (comment):

If we are establishing a new set of gadgets, it may be worth taking a moment to consider unification of similar alternate approaches for two reasons:

• This may lead to the most coherent/efficient foundation.
• This may simplify achieving the goal of migrating downstream projects to use a common base.

To that end, let's take a moment to make an active decision. The current function (alloc_num_is_zero) can be implemented in terms of the (also important) alloc_equal_const (https://github.com/lurk-lab/lurk-rs/blob/dae0d6c478a83c80e3b3753c29f89e4ecd2a6313/src/circuit/gadgets/constraints.rs#L495) [UPDATE: actually alloc_num_is_zero operates on a Num — so my points here are not quite germane to this work. The general point stands as something we should sort out as part of a 'base gadgets' project, though.].

Arecibo, for path-dependent reasons associated with its own internal consistency has the slightly-differently-named alloc_num_equals_const: https://github.com/lurk-lab/arecibo/blob/6a9e8707e868068abf8c6b8da999443c3f3d0895/src/gadgets/utils.rs#L200-L237.

In addition to the slight naming difference, that function has a more concise (arguably simpler — if also less didactic) definition, itself derived from its alloc_num_equals (https://github.com/lurk-lab/arecibo/blob/6a9e8707e868068abf8c6b8da999443c3f3d0895/src/gadgets/utils.rs#L156-L197), which has a similar relationship to Lurk's equivalent alloc_num_equal (https://github.com/lurk-lab/lurk-rs/blob/dae0d6c478a83c80e3b3753c29f89e4ecd2a6313/src/circuit/gadgets/constraints.rs#L440-L492C2).

The point of this comment is to suggest we take a moment to actively decide:

• About names, do we want to use:
  • the lurk-rs names;
  • the nova/arecibo names;
  • some (potentially) more lexically-consistent names considered from the ground up to solve the larger design problem now faced.
• About implementations, do we want to use:
  • the lurk-rs implementations;
  • the nova/arecibo implementations;
  • fresh implementations [note: probably not a good idea in this work]

The reason this is worth considering is that any refactoring of both arecibo (which implies the hope for an eventual change in nova) and lurk-rs will have audit/correctness implications for at least one of those projects. We should seek to minimize global cost and maximize eventual global confidence in correctness with whatever we do here.

I don't think we need to overthink this, just make an active decision. I suggest there are only four reasonable choices, and all are more-or-less acceptable with the right argument:

• lurk-rs names and implementations (status quo of this PR)
• arecibo names and implementations (status quo if we had started from the premise of refactoring arecibo)
• lurk-rs names and arecibo implementations (possible lessening of the lower-level crypto's auditing burden as a matter of policy, or in deference to the lowest-level's cryptographic weight).
• arecibo names and lurk-rs implementations (in deference to lurk-rs and many of the gadgets in question more broadly than just this PR having undergone one round of audit).

I would say that the last option probably makes little sense. If the logic for lurk-rs implementations is strong, we should probably also use lurk-rs names. This is because lurk-rs names are probably the better choice anyway, and changes of naming for purpose of gadget standardization should be non-threatening to arecibo/nova.

In the end, I think my vote is for lurk-rs names and either implementation. If we know we will prefer one implementation over the other, it's probably best to initialize this work with that choice so we can follow a policy of not gratuitously changing implementations of gadgets — since this has a substantive effect on any circuit depending on them; making it a deeply breaking change in ways that are not instantly obvious.

cc: @adr1anh @gabriel-barrett @huitseeker

Originally posted by @porcuquine in #55 (comment)

dev at d90eee7 does not include main at 88d8af2

dev at 0357ebf does not include main at 4bde01b

dev at 039ac97 does not include main at 81a69fd

dev at 99b4d46 does not include main at cd30233

dev at 99f5293 does not include main at 6264c8b

dev at ae07eb4 does not include main at d967146

See lurk-lab/neptune#250 (comment)

We want to not update bellpepper-core versions unless absolutely necessary.

• 0.2.0 -> 0.3.0 was breaking,
• 0.3.0 -> 0.4.0 was not.