wip short-circuiting proof composition #164
Draft
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
Doesn't compile, unfinished. The idea is to make an abstraction over "statements", such that they are either done by a recursive proof verification or by doing some minor logic in-circuit. For the action state extension statement, it would be short-circuiting if source and target are only N actions from each other (for e.g. N = 8), but more than that could use a recursive proof (and reusing the portion of the circuit to verify the last N ones). Then, we can define short-circuiting proof composition, currently called WrapTwo dumbly, such that if either of the two wrapped statements can be short-circuited, then we avoid an extra proof. This is very useful for reducing proofs to deal with the 2 recursive proof verifications per circuit limit, since you can stack WrapTwos on top of WrapTwos, and only proving when necessary, short-circuiting the rest. Closes #162
|
I've currently unprioritized this since it's non-trivial and hard to audit. |
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.
Doesn't compile, unfinished.
The idea is to make an abstraction over "statements", such that they are either done by a recursive proof verification or by doing some minor logic in-circuit.
For the action state extension statement, it would be short-circuiting if source and target are only N actions from each other (for e.g. N = 8), but more than that could use a recursive proof (and reusing the portion of the circuit to verify the last N ones).
Then, we can define short-circuiting proof composition, currently called WrapTwo dumbly,
such that if either of the two wrapped statements can be short-circuited, then we avoid an extra proof.
This is very useful for reducing proofs to deal with the 2 recursive proof verifications per circuit limit, since you can stack WrapTwos on top of WrapTwos, and only proving when necessary, short-circuiting the rest.
Closes #162