On duplication in LEM integration

[huitseeker]

I think there are two factors of duplication in #629:

Misuse of genericity

This is essentially explained in a PR comment. That is, the types that depend on a generic C: Coprocessor<F> are redefined in #629 because the LEM logic cannot for now accomodate any coprocessor other than DummyCoproc<F>. However, for any GenericType<Foo, Bar>, there is nothing in Rust that prevents you from defining methods for type GenericType<Foo, usize>.

I have a branch that starts working out the deduplication in https://github.com/huitseeker/lurk-rs/tree/lem-integration-experiment

The reason I think it's important to resolve this is that the methods we'd define today on Foo<F, DummyCoproc<F>> will eventually be able to be defined on Foo<F, C: Coproc<F>>, which is going to be much easier to adapt to if they're not distinct types.

Not abstracting the Multiframe, and failing to define provers in terms of that abstraction

The MultiFrame is the fundamental type that's defined starkly differently in LEM and Lurk:

• in LEM
• in Lurk

This struct appears in the APIs of the prover:
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/mod.rs#L20
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/mod.rs#L33-L34
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/mod.rs#L107-L110
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/nova.rs#L121
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/nova.rs#L131-L141
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/nova.rs#L172-L181
https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/nova.rs#L421-L428

morally speaking, the only thing we need (that is, the only thing Nova requires) in the position of this MultiFrame in the prover is some instance of StepCircuit. I suspect we could implement:

• a trait MultiFrame that abstracts over both types of Multiframe (LEM, non-Lurk). The main APIs to provide there are associated types fixing the local notion of Store and Ptr, blank, from_frames and synthesize_frames (the later being expressed in terms of those associated types:
  https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/proof/nova.rs#L421-L428
  https://github.com/lurk-lab/lurk-rs/blob/9aa8b75247066b70972f2806a1537c359f47c2c6/src/circuit/circuit_frame.rs#L183-L192
  Note the apparent difference between the instances of this backend function are not key, since their only usage is in the
  impl nova::StepCircuit for MultiFrame and impl bellpepper_core::Circuit for MultiFrame. Whatever abstraction that allows implementing those two callsites on top of what the MultiFrame trait offers should be enough.
• an implementation of the Nova prover that works on top of the Multiframe trait, rather than introspecting into the details of the two instances of their implementations above

[huitseeker]

Summarizing the story:

• Lem integration #629 was a meaty PR,
• we worked out how to prove through an interface in MultiFrameTrait #642 and Reduce some noise in Lem integration PR #633
• Isolate some changes from #629 #663 committed isolated changes from Lem integration #629
• the blocker was then a pattern of genericity + mutability of the store which could make interleaving evaluation and proving really hard,
• we moved to an interior mutability store in [PoC] feat: moving to shared store references #680,
• this allowed for the sought after genericity in feat: prove through a Multiframe trait #709
• this paved the way for New LEM integration #717 and Evaluation tests for LEM #718 which offer apples-to-apples guarantees of feature parity for evaluation and proving,

The present should close as soon as #717 and #718 are merged, because while we are indeed taking some duplication with those PRs, this is better than the alternative (worked out in #729) due to a lower complexity.

The missing pieces are NIVC support from #677 and #725, which should also resolve soon.

[huitseeker]

Closed with the merge of #717, #718.