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

Parellel NIVC #256

wants to merge 28 commits into from

Conversation

adr1anh
Copy link
Contributor

@adr1anh adr1anh commented Jan 12, 2024

This (draft) PR introduces a new architecture for parallel folding. The goal is to support the current NIVC architecture introduced with SuperNova, while leaving room for generalizing to more complex PCD settings.

  • CycleFold
  • Parallel witness generation
  • NIVC folding and merging
  • More efficient hashing of prover data using Fiat-Shamir transcript abstraction

huitseeker added a commit to huitseeker/arecibo that referenced this pull request Jan 14, 2024
…rk-lang#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 (lurk-lang#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]>
@adr1anh
Copy link
Contributor Author

adr1anh commented Feb 14, 2024

CycleFold CommitmentKey

Let $\mathbb{F}_i, \mathbb{G}_i$ be the scalar field of the circuit, and the commitment group for a circuit proof over the curve with index $i$. For example, the base field of $\mathbb{G}_2$ is $\mathbb{F}_1$ and vice-versa.

The version of CycleFold implemented here makes the assumption that a commitment $C \in \mathbb{G}_1$ of a proof of a circuit over the primary curve, is represented as $h_C = H_2(C.x, C.y) \in \mathbb{F}_2$, where $H_2$ is the Poseidon hash of arity 2 over the secondary curve. Given that $|\mathbb{F}_1| &lt; |\mathbb{F}_2|$, the value $h_C$ does not fit natively as an element in the primary circuit, so we consider it as 4 64-bit limbs. This decomposition is linked to the parameters used for the non-native field arithmetic gadget.

Ideally, we would want a specialized CommitmentKey for the primary curve, with the associated Commitment type

struct CycleFoldCommitment<E: Engine> {
  value: E::GE,
  hash: E::Base,
  limbs: [E::Scalar; NUM_LIMBS],
}

At the moment, this struct is implemented as HashedCommitment, but the conversion from Commitment is done manually.

We do not actually have to make this type homomorphic by implementing the Add, Mul, ... traits, since CycleFold imposes that we prove every single operation on these values.

The CommitmentKey itself would likely own a copy of PoseidonConstants for $H_2$, so that the hash and limb-decomposition can be computed as part of the commitment.

For the CompressedSNARK the verifier will be given value and will need to validate the hash by recomputing it from value.

The main advantage of this approach is that the public IO of the CycleFold circuit is reduced to 4 $\mathbb{F}_2$ elements, instead of 7 (3 points with 2 elements and 1 scalar).

@adr1anh
Copy link
Contributor Author

adr1anh commented Feb 14, 2024

Native NIFS unification

Source: https://github.com/adr1anh/arecibo/blob/para-circuit/src/parafold/nifs/prover.rs

The NIFS module in the native setting should work the same for both curves. However, we currently have two implementations for handling the subtleties on both curves. The main reasons for this are

Different commitment types:
On the primary curve, a Commitment is represented by the limbs of the hash of the x, y coordinates, while on the secondary curve we add the x, y coordinates directly. This would be solved by the above comment if the primary CommitmentKey has the appropriate associated HashedCommitment type. We would need to make sure the Transcript over E1::Scalar can absorb both Commitment<E1> = HashedCommitment<E1> and Commitment<E2> = E2::GE.

If we parametrize the RelaxedR1CS struct with an Engine E, then the Transcript argument needs to be parametrized with a separate field F. On the primary curve, we have E::Scalar=F but on the secondary curve it is E::Base=F.

Scalar multiplication accumulator:
For the primary curve, all group operations need to be proved via the CycleFold circuit. For this, we introduced the ScalarMulAccumulator which

  • Computes the result of C = A + x * B and adds C to the transcript
  • Adds the tuple [A,B,x,C] to a list of deferred claims for the CycleFold circuit, so that all CycleFold invocations can be proved together.

The scalar multiplications required for the folding proof on the secondary curve are computed normally and therefore do not need to be added to the transcript or proved later, so the folding methods specific to the secondary curve do not have a ScalarMulAccumulator input.

We could implement a TrivialScalarMulAccumulator for the secondary curve, which would have the same signature as the corresponding struct on the primary curve, but would be mostly a no-op (except for computing the result C).

It may be useful to make this an associated type of the CommitmentKey, which would make the Add, Mul, ... trait implementations irrelevant.

@adr1anh
Copy link
Contributor Author

adr1anh commented Feb 14, 2024

Expanding RelaxedR1CS

We chose to represent the prover's RelaxedR1CS accumulator as a new struct that includes the underlying instance corresponding to the parts of the accumulator known to the verifier. However, we can simplify some signatures and implement certain allocation optimizations more elegantly if we allow some extra fields.

Arc<R1CSShape<E::Scalar>>:
An accumulator is inherently dependent on a specific R1CSShape which needs to be passed as an argument to each fold or merge call. We can make this relationship clearer by including a pointer to the shape inside the struct. Using Arc should add very little overhead, and makes the construction safer since we do not need to guard against passing the wrong shape as input.

Caching buffers:
The computation of the T cross-term vector requires several temporary buffers for storing intermediary computations. These buffers could be stored in RelaxedR1CS directly to avoid relying on the caller to create and keep track of them.

@adr1anh
Copy link
Contributor Author

adr1anh commented Feb 14, 2024

Public Parameter digest

For security, the public parameter digest of the different circuits needs to be included in the transcript in some form. This is not currently handled in this branch, but needs to be addressed differently from the existing SuperNova implementation.

In the NIVC setting, the recursive verifier needs to store a representation of the accumulator instances for each circuit. In SuperNova, these are stored as their "raw representation" which means that at every iteration, the entire list of accumulators needs to be hashed. Instead, we noted that the verifier only needs to store a list of hashes of each accumulator. During the folding verification, the verifier must prove knowledge of the pre-image of the hash corresponding to the accumulator being folded. This simplifies the recursion circuit since we no longer need to conditionally select a vector of accumulator, but only a vector of hashes.

The pre-image of the accumulator should include the public parameter digest of the circuit it corresponds to. This provides a strong link between the accumulator values (u, X, W, E) and the actual circuit. During the CompressedSNARK verification, the verifier will be given the list of hashes of the accumulators and the corresponding pre-images which contains the verification key digest, hence tying the accumulator to a specific circuit.

@adr1anh
Copy link
Contributor Author

adr1anh commented Feb 26, 2024

New thoughts on unifying NIFS for both curves

Trying to unify the implementations of the nifs module to work over both primary and secondary curves no longer seems like the right approach at this time. The original goal was to minimize code duplication between the two implementations, this seems to be more complex and may not actually help in the long-run.

After some discussions, it seems likely we will want a different folding argument for the primary curve, whether that is HyperNova or an extension of Nova that supports more features. However, due to the tight constraints around the verifiability of secondary curve circuits, it does not seem likely we will replace Nova on the secondary curve with another arguments. Even if that did happen, we will likely end up with two arguments to maintain anyway.

Even at this point, the two implementation diverge significantly enough that the only thing they really have in common is the RelaxedR1CS struct.

  • We have separate folding/merging methods that have different signatures
  • Serialization is becoming a head-ache and making us resort to some fancy trait-fu to support serializing the same types in two different ways.

It is also almost certain that the secondary circuit will only be used to perform a single scalar multiplication of primary curve commitments. For this reason, I'd like to refactor the current PR as follows:

  • Move the logic for folding the secondary circuit into the cyclefold module. The only thing we'll want to expose is the ScalarMulAccumulator
  • Move the SecondaryRelaxedR1CSInstance into the ScalarMulAccumulator.
  • Create a cyclefold/gadgets module that contains the gadgets that are only relevant to the folding over the secondary curve
    • This includes a small wrapper around bellpepper-emulated which is specific to the E::Base field .
    • For now, it would also include the ecc gadget that provides efficient group operations over curves whose base field is equal to the field the constraint system is defined over. Later on, this gadget should also be moved to bellpepper-gadgets since it would also be used by an upcoming ECMH gadget.
  • Define a custom SecondaryR1CS struct is specialized over E: CurveCycleEquipped, and whose elements can be serialized in a way that makes sense for E. This will make the serialization work in feat: Introduce a proof-of-concept field Writer for writing to "native field" as well as "foreign field" transcripts #340 simpler and avoid making it too generic.

- replace nivc merge with merge_many
- add alloc for circuit types
- define nivc state hasher
- Rework fold API
- add ECC copy with Engine->Group
- Replace E::TE with own transcript
- placeholder NIFS secondary
- make accumulator fold mutate self
- add engine type constraint
- add `to_native` for converting back to the normal type
- Wrap ECC and EmulatedFieldElement
- Make all structs CurveCycleEquipped
- Specialize R1CS for both curves
- Update Transcript
adr1anh added 6 commits March 1, 2024 10:54
- remove unused/commented out functions
- revert to 128-bit limb hashing due to security concern
- make ScalarMulAccumulator take ownership of R1CS accumulator
- add ability to generate dummy input proof for circuit
- use sponge for hashing the NIVC instance due to problems with variable-sized hashing
- add test for `from_proof`
- comment out merge-related code
- ensure namespaces have unique names
- remove wrong mersenne prime parameters
- add emulatedbase tests
- add cycle fold circuit
- add inputize_hashed methods in allocated point for cyclefold circuit
- Rework primary IO.
  - Return transcript and state hash
- Use correct Poseidon for sponge
- Impl `eq_native` methods for comparing allocated types
- Add ability to generate dummy proofs as initial input to the circuit
- Fix `AllocatedPoint::enforce_trivial`
- Impl CycleFold circuit
  - Ensure IO matches
  - Add Poseidon hashing of points
- Fix AllocatedBase
  - fix `big_int_to_limbs`
  - fix other limb issues
  - add test
- Fix `enforce_trivial` for `AllocatedBase` elements
- Fix r_bits to r conversion
- add recursive snark verification
- use sponge for hashing state due to variable size
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant