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

Lem integration #629

Closed
wants to merge 147 commits into from
Closed

Lem integration #629

wants to merge 147 commits into from

Conversation

arthurpaulino
Copy link
Contributor

@arthurpaulino arthurpaulino commented Aug 23, 2023

This PR implements the first iteration on the integration of LEM with the rest of the codebase.

It offers an experimental interface via a --lem flag, which enters a REPL that uses the LEM engine. This REPL is not feature complete.

The bulk of this contribution is in the tests from nova_lem.rs, which is a proof of concept that attests that LEM can generate well-formed circuits that can be used to make proofs with Nova.

As a collateral effect, the hashing of symbols in the main infra was fixed. The error was found because of a mismatch between the main infra and LEM.

In terms of benchmarks, the key point is that LEM evaluation is 35x slower than the one implemented directly with Rust functions. This will be addressed in the future.

arthurpaulino added a commit that referenced this pull request Sep 12, 2023
arthurpaulino added a commit that referenced this pull request Sep 12, 2023
arthurpaulino added a commit that referenced this pull request Sep 13, 2023
* chore: replace circuits

* refactor: Refactor lifetime parameters and enhance MultiFrameTrait

- Refactored the `MultiFrameTrait` by removing the lifetime parameter, which enhances flexibility and usability in more contexts.
- Updated function signatures across several files by changing lifetime-bound references to borrowed references, improving flexibility and reducing clone necessities for multiframes.
- Updated `MultiFrameTrait` implementation for `MultiFrame` and `NovaProver` with new types, methods and enhancements to frame handling, allowing better processing of hash functions and creation of witness circuit systems.
- Modified the `Groth16Prover` and `NovaProver` to handle the `MultiFrameTrait` without being lifetime-bound, potentially improving flexibility and usability.
- Renamed `NovaProver._p` to `NovaProver._phantom`.
- Refactored several `Store` references to become generic thereby moving away from lifetime annotation.
- Updated `LurkProof` enum in `lurk_proof.rs` to include a new `MultiFrameTrait` generic parameter and updated its verification methods to accommodate the new `nova::Proof` parameters.

* WIP MultiFrame

* translate some test types

* * Rename `FramePtr` to `FrameIO`
* Remove unused implementation of `FrameLike` for LEM's `MultiFrame`
* Add interface `MultiFrameTrait::output` and implement it for both instances

* progress on generalization

* invert C1 alias, correct Serialize reqs

* adjust lifetimes

* chore: more lifetimes adjustments

* fix: more adjustments, doc

* refactor: Refactor frame handling and evaluation in prover modules

- Removed `Prover` import and replaced its usage with a `padding_predicate` in `get_evaluation_frames` method of `src/circuit/circuit_frame.rs`.
- Modified `src/proof/mod.rs` and `src/lem/multiframe.rs` to pass a `padding_predicate` function to `get_evaluation_frames` to determine if the prover needs padding.

* replace a loop with a macro, performing a sequence of calls from the original owner of the mutable reference to the store

* fix: adapt to latest Nova

---------

Co-authored-by: Arthur Paulino <[email protected]>
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 27, 2023
- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,
huitseeker added a commit that referenced this pull request Sep 28, 2023
* feat: Introduce MultiFrame trait

Mutability leftovers (see #680)

- Updated benchmarking scripts to no longer mutate the `store` variable during evaluation frames retrieval.
- Reformed `get_evaluation_frames` method across several files to use immutable references to `store` instead of mutable references.

Multiframe definition

- Introduced several new traits - `CEKState`, `FrameLike`, `EvaluationStore` and `MultiFrameTrait` to manage complex evaluation and circuit proof operations in the `proof/mod.rs` file.
- Detailed implementations of the above traits introduced in `circuit/circuit_frame.rs`, providing methods for handling evaluation frames, synthesizing data from multiple frames and more.

* refactor: make nova proofs use the generic trait

- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova,
- For references on the latest work defining this trait, see #629 (and its history, incl. #642, #707) and #677.

- make the benches use the generic trait, so LEM can bench similarly,
- make the examples use the generic trait, so LEM can example similarly,
- make Supernova use the generic trait, so LEM can NIVC similarly,

* use a type alias to simplify test calls

---------

Co-authored-by: Arthur Paulino <[email protected]>
@arthurpaulino arthurpaulino deleted the lem-integration branch October 13, 2023 21:22
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.

On duplication in LEM integration
5 participants