feat: support for streamed computations and their proofs #1209
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
arthurpaulino
force-pushed
the
ap/stream
branch
8 times, most recently
from
7f5f605 to
a09f04d
Compare
huitseeker
reviewed
Mar 17, 2024
src/proof/mod.rs
Outdated
Comment on lines
167
to
174
| type BaseRecursiveSNARK; | ||
|
|
||
| /// Associated proof type, which must implement `RecursiveSNARKTrait` | ||
| type RecursiveSnark: RecursiveSNARKTrait<F, Self::Frame, PublicParams = Self::PublicParams>; | ||
| type RecursiveSnark: RecursiveSNARKTrait< | ||
| F, | ||
| Self::Frame, | ||
| PublicParams = Self::PublicParams, | ||
| BaseRecursiveSNARK = Self::BaseRecursiveSNARK, |
There was a problem hiding this comment.
I think this can be made simpler by removing the BaseRecursiveSNARK associated type, and constraining the argument of prove instead:
fn prove(
&self,
pp: &Self::PublicParams,
steps: Vec<Self::Frame>,
store: &'a Store<F>,
init: Option<<Self::RecursiveSnark as RecursiveSNARKTrait<F, Self::Frame>>::BaseRecursiveSNARK>,
) -> Result<(Self::RecursiveSnark, Vec<F>, Vec<F>, usize), ProofError> There was a problem hiding this comment.
We need BaseRecursiveSNARK in order to define
/// Associated proof type, which must implement `RecursiveSNARKTrait`
type RecursiveSNARK: RecursiveSNARKTrait<
F,
Self::Frame,
PublicParams = Self::PublicParams,
BaseRecursiveSNARK = Self::BaseRecursiveSNARK,
>;There was a problem hiding this comment.
You can just remove that constraint instead.
| let a = bindings.get_ptr(a)?; | ||
| println!("{}", a.fmt_to_string_simple(&scope.store)); | ||
| } | ||
| Op::Recv(_) => todo!("not supported yet"), |
| @@ -433,6 +436,6 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a> Prover<'a, F> for NovaPr | |||
| let eval_config = self.folding_mode().eval_config(self.lang()); | |||
| let frames = | |||
| C1LEM::<'a, F, C>::build_frames(expr, env, store, limit, &eval_config, ch_terminal)?; | |||
| self.prove_from_frames(pp, &frames, store) | |||
| self.prove_from_frames(pp, &frames, store, None) | |||
There was a problem hiding this comment.
While we're here, we may want to open an issue to hoist
fn lang(&self) -> &Arc<Lang<F, C>>;
fn prove_from_frames(
&self,
pp: &Self::PublicParams,
frames: &[Self::Frame],
store: &'a Store<F>,
init: Option<<Self::RecursiveSnark as RecursiveSNARKTrait<F, Self::Frame>>::BaseRecursiveSNARK>,
) -> Result<(Self::RecursiveSnark, Vec<F>, Vec<F>, usize), ProofError>;Into the Prover trait, that would save us some Nova/SuperNova duplication.
arthurpaulino
force-pushed
the
ap/stream
branch
from
a09f04d to
0dac83e
Compare
Introduce the `Op::Recv` LEM operator, which awaits for data to be received by the channel terminal at LEM interpretation time. This operator is used to implement the logic for the `StreamIn` continuation, which receives the argument to be applied to the (chaining) callable object. The result will be available once the (new) `StreamOut` continuation is reached. When that happens, the computation can be resumed by supplying two pieces of data through the channel: * A flag to tell if the machine should stutter while in `StreamOut` * The next argument to be consumed in the incoming `StreamIn` state Note: the second message should not be be sent if the machine is set to stutter with the first message. There is a test to show that we're now able to construct proofs of computations that grow incrementally by starting from where we had stopped. We don't need to start the folding process from the beginning.
Prepare the next call directly from `StreamOut` without having to go through `StreamIn` again. Since `StreamIn` only occurs in the very first frame after this optimization, it was renamed to `StreamStart`. And `StreamOut`, which now serves as literal point for pause while supporting both input and output, was renamed to `StreamPause`.
arthurpaulino
force-pushed
the
ap/stream
branch
from
0dac83e to
26749d4
Compare
huitseeker
approved these changes
Mar 18, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Introduce the
Op::RecvLEM operator, which awaits for data to be received by the channel terminal at LEM interpretation time.This operator is used to implement the logic for the
StreamIncontinuation, which receives the argument to be applied to the (chaining) callable object.The result will be available once the (new)
StreamOutcontinuation is reached. When that happens, the computation can be resumed by supplying two pieces of data through the channel:StreamOutStreamInstateNote: the second message should not be be sent if the machine is set to stutter with the first message.
There is a test to show that we're now able to construct proofs of computations that grow incrementally by starting from where we had stopped. We don't need to start the folding process from the beginning.
Optimizing
From the second commit in this PR:
This optimization makes starting and resuming streams consume the same number of Lurk iterations.