feat: prove through a Multiframe trait#709
Conversation
Mutability leftovers (see lurk-lab#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.
7cb9ad2 to
b239e95
Compare
223a363 to
90e1dfd
Compare
- 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,
90e1dfd to
6b5f11f
Compare
|
!benchmark |
arthurpaulino
left a comment
There was a problem hiding this comment.
✨ 🎉
Let's just see the benchmarks to make sure that nothing weird happened.
src/proof/nova.rs
Outdated
| @@ -866,7 +928,7 @@ pub mod tests { | |||
| let s = &mut Store::<Fr>::default(); | |||
| let expected = s.num(3); | |||
| let terminal = s.get_cont_terminal(); | |||
| test_aux::<Coproc<Fr>>( | |||
| test_aux::<_, _, C1<'_, _, Coproc<_>>>( | |||
There was a problem hiding this comment.
Can we abbreviate this type with a local type definition? It will probably avoid a bunch of line additions.
It would also setup an organized pattern for when we introduce the LEM tests.
There was a problem hiding this comment.
I'm not quite sure what local type definition you have in mind, but I'm of course in favor of the PR re-organizing the proof tests to put LEM & Lurk side-by-side doing some heavy refactoring to do so.
The line changes made here are such that those generic methods that need annotation now bear the exact same annotation on each line, syntactically - this makes them ripe for mechanized refactoring. So I'm not too worried about that.
|
I ran the benchmarks locally and everything is okay |
use a type alias to simplify test calls
|
This will be blocked on @porcuquine 's review because of the removal of the |
Nest steps :
src/proof/nova.rsso that it tests each expression with LEM and Lurk,