lurk-lab / lurk-rs

Lurk is a Turing-complete programming language for recursive zk-SNARKs. It is a statically scoped dialect of Lisp, influenced by Scheme and Common Lisp.
https://lurk-lang.org/
Apache License 2.0
418 stars 54 forks source link

feat: support for streamed computations and their proofs #1209

Closed arthurpaulino closed 3 months ago

arthurpaulino commented 3 months ago

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:

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.

Optimizing

From the second commit in this PR:

optimize: skip new `StreamIn` ocurrences

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`.

This optimization makes starting and resuming streams consume the same number of Lurk iterations.