subtree update positive security exercise #387
Conversation
Sladuca
changed the title
| //@requires(2) `accumulatorHash` is the low-253 bits of the batch `accumulatorHash` from the commitment tree in `OffchainMerkleTree.sol` | ||
| //@requires(3) `2*r + 3` is less than 254 and `r > 0` | ||
| //@requires(3) `oldRoot` is the current commitment tree root | ||
| //@ensures(1) `newRoot` is the commitment tree root that results from inserting the batch with accumulator hash `accumulatorHash` (+ 3 hi-bits form `encodedPathAndHash`) into the commitment tree with root `oldRoot` |
There was a problem hiding this comment.
We don't need any requires for siblings, leaves, bitmap, etc (all the fields committed to be accumulator hash)?
There was a problem hiding this comment.
One big requires is that the bitmap, owner fields, nonces, etc are in the exact order they occurred on chain. Idk the best way to frame this but you could mention how each field is committed to
There was a problem hiding this comment.
The circuit doesn't require this - this all comes from accumulatorHash. They're also all private witness values so we can't make any assumptions on them at all.
There was a problem hiding this comment.
added a comment to OffchainMerkleTree.sol explaining this.
| @@ -35,9 +42,13 @@ template SubtreeUpdate4(r) { | |||
| signal input encodedAssetIds[4**s]; | |||
| signal input values[4**s]; | |||
|
|
|||
| //@satisfies(1) | |||
| //@argument Subtreeupdate.requires(1, 2, 3) are satisfied by @requires(...), | |||
There was a problem hiding this comment.
inner's require statements are satisfied by this template's require statements
| //@requires(2) `accumulatorHash` is the low-253 bits of the batch `accumulatorHash` from the commitment tree in `OffchainMerkleTree.sol` | ||
| //@requires(3) `2*r + 3` is less than 254 and `r > 0` | ||
| //@requires(4) `emptySubtreeRoot` is the correct root of a depth-s subtree full of "zeros", where the "zero value" is up to the caller | ||
| //@requires(3) `oldRoot` is the current commitment tree root |
There was a problem hiding this comment.
requires 5 you mean not 3?
| // this is clearly the case from this constaint in the case where bitmap[i] == 1 | ||
| // in the case where it's 0, the argument goes like this: | ||
| // - due to @lemma(3), `hasher.out` is the unique, correct accumulator hash for the batch of notes, | ||
| // so, due to @requires(2), the circuit will be unsatisfiable if the batch supplied as witness to this circuit does |
There was a problem hiding this comment.
REVISIT: accumulator hash is not guaranteed to be unique (e.g. accumulator hash for 2 empty batches, though fully zero batches is not possible)? are non unique accumulator hashes a problem?
There was a problem hiding this comment.
unique probably isn't the right word - I meant it's the only possible accumulator hash we could get from the given batch. clarified wording in newest revision.
Sladuca
force-pushed
the
seb/subtree-update-positive-sec
branch
from
a3bf881 to
b68fc7b
Compare
Sladuca
force-pushed
the
seb/subtree-update-positive-sec
branch
from
b68fc7b to
44dafd2
Compare
Motivation
Want to enumerate subtree update circuit assumptions and argue subtree update circuit is "correct" given those assumptions to gain more surety that it's "correct"
Solution
Add annotations in comments listing out assumptions and arguing they're correct
Proof
unnecessary, as there are no code changes
PR Checklist