Implement MemoSet. #1004
Implement MemoSet. #1004
Conversation
porcuquine
force-pushed
the
memoset
branch
10 times, most recently
from
d8e4937 to
8965f96
Compare
porcuquine
force-pushed
the
memoset
branch
2 times, most recently
from
ca59e25 to
32ed056
Compare
porcuquine
force-pushed
the
memoset
branch
3 times, most recently
from
da7f9f4 to
27a7a5d
Compare
| //! Whenever a computation being proved needs the result of a query, the prover non-deterministically supplies the | ||
| //! correct response. The resulting key-value pair is then added to a multiset representing deferred proofs. The | ||
| //! dependent proof now must not be accepted until every element in the deferred-proof multiset has been proved. | ||
| //! |
There was a problem hiding this comment.
While this module documentation is useful to document the building blocks, I would love to see some use-case level doc: what can I find in this module, what can I use it for, and what can I not use it for?
The core piece of information that we may want to volunteer at the top-level, is that this particular coprocessor takes assumptions about Lurk data structures (and their hash-consing), because it is meant to represent Lurk evaluation proofs. That's not a thing that all coprocessors do (e.g sha256) and laying that out in a couple sentences at the top should help the reader interpret the meaning of a struct named "Transcript" at the top of the file (i.e. this is not a garden-variety RO).
| } | ||
| } | ||
|
|
||
| fn build_transcript(&self, s: &Store<F>) -> (Transcript<F>, Vec<Ptr>) { |
There was a problem hiding this comment.
We should have access to std::slice::group_by in a future version of Rust, and already have those through itertools. Does that change some of the algorithmic costs incurred by .sort() here?
There was a problem hiding this comment.
I don't think it helps with this. We can avoid the sort by just assembling insertions as a hash table of vectors, though.
| //! `Scope`. This allows us to accumulate queries and the subqueries on which they depend, along with the memoized query | ||
| //! results computed 'naturally' during evaluation. We then separate and sort in an order matching that which the NIVC | ||
| //! prover will follow when provably maintaining the multiset accumulator and Fiat-Shamir transcript in the circuit. | ||
|
|
There was a problem hiding this comment.
We may also want to add some context for how this is in the coprocessor module but does not implement the Coprocessor traits. This is fine for now, but a TODO to find a "home" for this module would help.
| @@ -0,0 +1,850 @@ | |||
| //! The `memoset` module implements a `MemoSet`. | |||
There was a problem hiding this comment.
Nit: you've made the public API of this module quite sparse by making few members public, which is great.
It also means that if you were to annotate the top of this module with #![deny(missing_docs)] the amount of work you'd have to do to fix would be small.
github-merge-queue
bot
removed this pull request from the merge queue due to no response for status checks
This PR implements a MemoSet proof-of-concept, sufficient to implement mutually recursive coprocessors ('coroutines') using Lurk calling conventions. It does not integrate this ability into the Lurk reduction, nor provide concrete coprocessors sufficient to package this work into existing NIVC proofs.
The transcript is produced in the most straightforward way that can work, using literal Lurk data. It is worth noting that this dramatically simplified the already difficult task of getting an evaluation-time and proof-time transcript to match. There are undoubtedly optimization opportunities via reducing hashing costs. Because of the debugging benefit of the current approach, it is likely worth refactoring to something less legible only carefully. Ideally, it would be a simple configuration change to recover legible hashing for debugging purposes.
Please reserve most discussion of this PR until after the holidays, since I intend not to engage in the meantime, and this will make that easier.