subtree update positive security exercise (#387)

* add positive security annotations to subtree update circuit

* changelog

* add comment to _computeAccumulatorHashe

* clarify wording

* add comment tying together subtreeupdate circuit & OffchainMerkle

* snap manifest

packages/circuits/CHANGELOG.md

@@ -2,6 +2,7 @@
 
 ### Unreleased
 
+- add positive security annotations to subtreeupdate circuit
 - add positive security annotations to `joinsplit.circom`
 - add on-curve and order check to `spendPubkey`
 - change `IsOrderGreaterThan8` to `IsOrderL`, which is a stricter condition that leaves less room for error

packages/circuits/circuits/lib.circom

@@ -255,6 +255,8 @@ template Encrypt(n) {
 
 // takes `2n` bits and outputs n 2-bit limbs
 // interpreted in little-endian order
+//@requires(1) n < 127
+//@ensures(1) for all i in 0..n: limbs[i] == bits[i*2] + 2*bits[i*2 + 1]
 template BitsToTwoBitLimbs(n) {
     signal input bits[2*n];
     signal output limbs[n];
@@ -266,6 +268,8 @@ template BitsToTwoBitLimbs(n) {
 
 // slices first k elements out of an array of n elements
 // why doesn't circom support this????
+//@requires(1) k <= n
+//@ensures(1) forall i in 0..k: slice[i] == arr[i]
 template SliceFirstK(n, k) {
     signal input arr[n];
     signal output slice[k];
@@ -275,6 +279,9 @@ template SliceFirstK(n, k) {
     }
 }
 
+//@requires(1) k <= n
+//@ensures(1) slice.length == k
+//@ensures(1) forall i in 0..k: slice[i] == arr[n - k + i]
 template SliceLastK(n, k) {
     signal input arr[n];
     signal output slice[k];

packages/circuits/circuits/subtreeupdate.circom

@@ -8,6 +8,14 @@ include "lib.circom";
 include "tree.circom";
 
 // Update a quaternary subtree of depth 2, where overall tree is of depth r + 2
+//@requires(1) encodedPathAndHash is a 2*r + 3 bit number, where (in little-endian order) the first 2*r bits are the path indices
+//   represented as a series of two-byit numbers indicating which child to traverse, in order from leaf to root,
+//   and the last 3 bits are the high bits of the accumulator hash
+//@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) `oldRoot` is the current commitment tree root
+//@ensures(1) `accumulatorHash` is the correct accumulator hash over the batch of notes to be inserted
+//@ensures(2) `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`
 template SubtreeUpdate4(r) {
     var s = 2;
     // public inputs
@@ -35,9 +43,13 @@ template SubtreeUpdate4(r) {
     signal input encodedAssetIds[4**s];
     signal input values[4**s];
 
+    //@satisfies(1, 2)
+    //@argument SubtreeUpdate.requires(1, 2, 3) are satisfied by @requires(...),
+    //   SubtreeUpdate.requires(4) is satisfied by the assignment below,
+    //   and SubtreeUpdate.ensures(1, 2) is identical to (1, 2)
     component inner = SubtreeUpdate(r, s);
 
-    // root of the depth-2 subtree
+    // root of the depth-2 subtree filled with `ZERO_VALUE = KECCAK256("nocturne") % p`
     inner.emptySubtreeRoot <== 6810774033780416412415162199345403563615586099663557224316660575326988281139;
 
     for (var i = 0; i < r; i++) {
@@ -64,6 +76,9 @@ template SubtreeUpdate4(r) {
 }
 
 // computes both poseidon and sha256 hash of a "concrete" note as defined in notion
+//@ensures(1) noteCommitment is the correct note commitment for the note with fields given as inputs
+//@ensures(2) sha256HashBits is the correct sha256 hash of the note with fields given as inputs, represented as a big-endian bitstring
+//  where the "sha256 hash of a note" is as defined by `sha256Note` in `TreeUtils.sol`
 template NoteCommitmentHash() {
     // ! NOTE: This assumes ristretto compression for addresses has been implemented
     signal input ownerH1X;
@@ -80,12 +95,22 @@ template NoteCommitmentHash() {
     signal output noteCommitment;
 
     // compress owner address points
+    //@lemma(1) h1CompressedY is the y-coordinate of the compressed point
+    //@argument easy to see from implementation of CompressPoint (see `lib.circom`)
+    //@lemma(2) h1Sign is the sign of the compressed point, where the x coordinate is considered
+    //   "negative" (sign == 1) if it's greater than (p-1)/2, and "positive" (sign == 0) otherwise
+    //@argument easy to see from implementation of CompressPoint (see `lib.circom`)
     component compressorH1 = CompressPoint();
     compressorH1.in[0] <== ownerH1X;
     compressorH1.in[1] <== ownerH1Y;
     signal h1Sign <== compressorH1.sign;
     signal h1CompressedY <== compressorH1.y;
 
+    //@lemma(3) h2CompressedY is the y-coordinate of the compressed point
+    //@argument same as lemma(1)
+    //@lemma(4) h2Sign is the sign of the compressed point, where the x coordinate is considered
+    //   "negative" (sign == 1) if it's greater than (p-1)/2, and "positive" (sign == 0) otherwise
+    //@argument same as lemma(2) 
     component compressorH2 = CompressPoint();
     compressorH2.in[0] <== ownerH2X;
     compressorH2.in[1] <== ownerH2Y;
@@ -138,10 +163,20 @@ template NoteCommitmentHash() {
         }
     }
 
+    //@satisfies(2)
+    //@argument elemBits[i].out is the big-endian bitstring representation of the ith field of the note, except for
+    // elemBits[0] and elemBits[1], which are the big-endian bitstring representation of the y-coordinates of the compressed
+    // for the first two 256-bit words, we pack the owner points in as 0 || xSign || yBits. This matches the behavior of `sha256Note`,
+    // as this is the same way compressed points are encoded on-chain, and this is checked before the note is queued for insertion.
+    // the rest of the fields are packed in as 0 || 0 || fieldBits, which is the same as the behavior of `sha256Note`, as, on-chain,
+    // field elements are represented as uint256s, the first two 256-bit words are always 0 if the value is a valid field element,
+    // and thisis checked before the note is queued for insertion
     for (var i = 0; i < 256; i++) {
         sha256HashBits[i] <== sha256Hasher.out[i];
     }
 
+    //@satsifes(1)
+    //@argument easy to see NoteCommit.requires(1) is true (exactly what code does), and (1) follows from NoteCommit.ensures(1)
     noteCommitment <== NoteCommit()(
         Poseidon(4)([ownerH1X, ownerH1Y, ownerH2X, ownerH2Y]),
         nonce,
@@ -152,6 +187,15 @@ template NoteCommitmentHash() {
 }
 
 // Update a quaternary subtree of depth s, where overall tree is of depth r + s
+//@requires(1) encodedPathAndHash is a 2*r + 3 bit number, where (in little-endian order) the first 2*r bits are the path indices
+//   represented as a series of two-byit numbers indicating which child to traverse, in order from leaf to root,
+//   and the last 3 bits are the high bits of the accumulator hash
+//@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(5) `oldRoot` is the current commitment tree root
+//@ensures(1) `accumulatorHash` is the correct accumulator hash over the batch of notes to be inserted
+//@ensures(2) `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`
 template SubtreeUpdate(r, s) {
 
     // Public signals
@@ -210,6 +254,14 @@ template SubtreeUpdate(r, s) {
         noteHashers[i].encodedAssetId <== encodedAssetIds[i];
         noteHashers[i].value <== values[i];
 
+        //@lemma(0) `leaves[i]` is the note commitment for the ith note enqueued in the batch on-chain
+        // 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
+        //     not match that which was queued for insertion on-chain (which includes bitmap)
+        //   - since @lemma(1) guarantees that, in the case where bitmap[i] is 0, `accumulatorInnerHashes[i]` is set to `leaves[i]`, then
+        //     that means `leaves[i]` must be match the note commitment enqueued on-chain
         bitmap[i] * (noteHashers[i].noteCommitment - leaves[i]) === 0;
 
         leafBits[i] = Num2BitsBE_strict();
@@ -220,9 +272,15 @@ template SubtreeUpdate(r, s) {
         tmp2[i][0] <== 0;
         tmp2[i][1] <== 0;
 
+        //@lemma(1) if `bitmap` matches the bitmap on-chain, then, for all i..4**s: `accumulatorInnerHashes[i]` contains...
+        // 1) the sha256 hash of the ith note in the batch (according to `sha256Note` in `TreeUtils.sol`) if bitmap[i] is 1
+        // 2) leaves[i] if bitmap[i] is 0
+        //@argument `bitmap` matches what was committed to on-chain, then:
+        //   1) if `bitmap[i] == 1` `tmp1[i]` is assigned to 0 (due to for loop above) and `tmp2[i]` is assigned to the correct sha256 hash of the note due to selection logic below and NoteCommitmentHash.ensures(2)
+        //   2) if `bitmap[i] == 0` `tmp1[i]` is assigned to `leaves[i]` (due to for loop above) and `tmp2[i]` is assigned to 0 (due to note selection logic below)
         for (var j = 0; j < 256; j++) {
             // For some reason circcom complains if I combine these into a single (still quadratic) constraint
-            // if I don't split it up with a temp signal
+            // so I split it up with a temp signal
             tmp1[i][j] <== bitmap[i] * noteHashers[i].sha256HashBits[j];
             accumulatorInnerHashes[i][j] <== tmp1[i][j] + tmp2[i][j];
         }
@@ -231,6 +289,12 @@ template SubtreeUpdate(r, s) {
     // decode pathIndices from encodedPathAndHash
     // note that we decode in LE order here - this is because `BitsToTwoBitLimbs` assumes LE.
     // this is equivalent to the BE way of describing it in the spec
+    //@lemma(2) there exists a valid membership proof of an empty depth-s subtree at the location encoded by `encodedPathAndHash` in the tree with root `oldRoot`
+    //@argument `pathAndHashBits` is the unique, little-endian bit decomp of `encodedPathAndHash` because @requires(1) gaurantees `Num2Bits` to be safe.
+    // => `pathBits` contains the 2*r path bits due to SliceFirstK.ensures(1) since SliceFirstK.requires(1) is satisfied by @requires(3).
+    // => `pathIndices` contains pathIndices for path from empty subtree root the commitment tree root since BitsToTwoBitLimbs.ensures(1) matches encoding guaranteed by @requires(1)
+    //     and BitsToTwoBitLimbs.requires(1) is guaranteed by @requires(3)
+    // =>  @lemma(2) due to MerkleTreeInclusionProof.ensures(1) since MerkleTreeInclusionProof.requires(1) is guaranteed by @requires(3)
     signal pathAndHashBits[2*r+3] <== Num2Bits(2*r+3)(encodedPathAndHash);
     signal pathBits[2*r] <== SliceFirstK(2*r+3, 2*r)(pathAndHashBits);
     signal accumulatorHashTop3Bits[3] <== SliceLastK(2*r+3, 3)(pathAndHashBits);
@@ -246,6 +310,13 @@ template SubtreeUpdate(r, s) {
     // followed by a 256-bit number with the bitmap packed into the upper bits
     // i.e. the ith bit of the bitmap is the ith bit of the last 256-bits of the input
     // i.e. the ith bit of the bitmap is the bit of the number with value 2^(255-i)
+    //@satisifies(1) `hasher.out` is the correct accumulator hash for the batch of notes.
+    //@argument `accumulatorhash` is defined as sha256(...innerHashes || bitmap) where each element of `innerHashes` is a 256-bit word
+    // and `bitmap` is encoded as big-endian number with the ith bit of the bitmap being the ith bit of the number with value 2^(255-i)
+    // (i.e. it's padded out to 256 bits, shifted all the way to the most-significant position) 
+    // the assigments below match this definition since @lemma(1) guarantees that `accumulatorInnerHashes` are correct`
+    // due to collision resistance of sha256 and the fact that bitmap is included in the hash, this is the only possible
+    // accumulator hash for this batch
 
     // set accumulatorInnerHash part of input
     for (var i = 0; i < 4**s; i++) {
@@ -261,9 +332,8 @@ template SubtreeUpdate(r, s) {
     for (var i = 4**s; i < 256; i++) {
         hasher.in[256 * (4**s) + i] <== 0;
     }
-
 
-    // Assert that the accumulatorHash is correct
+    // assert that the accumulatorHash matches what we computed
     signal computedHashBits[253] <== Num2BitsBE(253)(accumulatorHash);
     for (var i = 0; i < 256; i++) {
         if (i < 3) {
@@ -274,6 +344,13 @@ template SubtreeUpdate(r, s) {
         }
     }
 
+    //@satisfies(2)
+    //@argument due to (1), `hasher.out` is the correct accumulator hash, and due to @requires(2), it will match the `accumulatorHash` PI
+    //   (checks above) IFF the batch supplied as witness in this circuit matches the batch queued for insertion on-chain
+    //   => that the circuit is satisfiable IFF `newRoot` is the correct root that results from inserting `leaves` into the tree.
+    //   due to @lemma(0), `leaves[i]` is the "correct" sequence of leaves to be inserted into the tree, so the circuit is satisfiable
+    //   IFF `newRoot` is the correct root that results from inserting the batch of notes committed to by `accumulatorhash` into the tree
+
     // Compute subtree root
     signal nodes[s+1][4**s];
     for (var i = 0; i < 4**s; i++) {

packages/contracts/contracts/libs/OffchainMerkleTree.sol

@@ -86,6 +86,14 @@ library LibOffchainMerkleTree {
     ) internal {
         uint256[] memory pis = _calculatePublicInputs(self, newRoot);
 
+        // 1) this library computes accumulatorHash on its own,
+        // the definition of accumulatorHash prevents collisions (different batch with same hash),
+        // and the subtree update circuit guarantees `accumulatorHash` is re-computed correctly,
+        // so if the circuit accepts, the only possible batch the updater could be inserting is precisely
+        // the batch we've enqueued here on-chain
+        // 2) the subtree update circuit guarantees that the new root is computed correctly,
+        //    so due to (1), the only possible newRoot is the newRoot that results from inserting
+        //    the batch we've enqueued here on-chain
         require(
             self.subtreeUpdateVerifier.verifyProof(proof, pis),
             "subtree update proof invalid"
@@ -163,6 +171,12 @@ library LibOffchainMerkleTree {
     }
 
     // H(updates || bitmap)
+    // claim: it's impossible to have a collision between two different sets of updates
+    // argument: order matters because of hash function. The only way two different sequences of note commitments
+    // could result in the same accumulatorHash would be if the inner hashes - either note commitments or note sha256 hashes -
+    // were the same, but the insertion kinds were mismatched. That is, there's a sha256 hash "masquerading" as a note commitment
+    // in the batch. But this is impossible because we also include the bitmap in the hash - which this library ensures is consistent with the
+    // order and kind of insertinos in the batch.
     function _computeAccumulatorHash(
         OffchainMerkleTree storage self
     ) internal view returns (uint256) {

packages/snap/snap.manifest.json

@@ -3,7 +3,7 @@
   "description": "Nocturne Snap",
   "proposedName": "Nocturne Snap",
   "source": {
-    "shasum": "FRTL+9bOs5el7kYH9qi8EvQEfuldWWM3K+8MtlQXTW4=",
+    "shasum": "zunlrXuvR+70b6qX9LQ+WGxxEnBoUgHqDeBxCFFN2f0=",
     "location": {
       "npm": {
         "filePath": "dist/bundle.js",