Add an appendix that explains the proof procedures by davidben · Pull Request #150 · ietf-plants-wg/merkle-tree-certs

davidben · 2025-10-06T16:34:12Z

Closes #147

davidben · 2025-10-06T16:34:50Z

+
+* `BIT_WIDTH(n)` refers to the smallest number of bits needed to represent `n`. `BIT_WIDTH(0)` is zero.
+
+* `POPCOUNT(n)` refers to the number of set bits in `n`'s binary representation`.


I used the C++20 names for these operations:
https://en.cppreference.com/w/cpp/header/bit.html

Closes #147

Use the things we've already defined.

nharper

Some suggestions and questions, and I need to keep reading.

nharper · 2025-10-10T20:40:40Z

+
+Iterating from level 0 up, `fn` and `sn` will initially be different. While they are different, step 4.2 hashes on the left or right based on the binary representation, as discussed in {{binary-representations}}.
+
+Once `fn = sn`, the procedure has reached the point where the path diverges from the right edge. At that point, the condition in step 4.2 is always tree. It only incorporates proof entries on the left, once per set bit. Unset bits are skipped.


"the condition in step 4.2 is always tree": should that be "is always true" instead of "is always tree"?

Whoops, yes. Fixed.

nharper · 2025-10-10T20:42:58Z

+
+The procedure in {{evaluating-a-subtree-inclusion-proof}} builds up a subtree hash in `r` by staring from `entry_hash` and iteratively hashing elements of `inclusion_proof` on the left or right. That means this procedure, when successful, must return *some* hash that contains `entry_hash`.
+
+Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.


Possibly add:

fn has the bit pattern that tracks the path from index to the root of the subtree, and sn has the bit pattern that that tracks the right edge of the subtree.

Think that fit slightly better in the next paragraph, but added something to this effect. I added some text in the previous section to make it clear that the right edge and the path to the last element are the same. (It seems to work better to talk about paths.)

nharper · 2025-10-10T20:50:16Z

+
+Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.
+
+Step 4 iterates through `inclusion_proof` and bit positions in parallel. Comparing `sn` to zero ensures that the two iterators stop together, i.e. there aren't extra or missing inclusion proof entries.


Possibly add:

Since sn tracks the path of the right edge to the root of the subtree, the last direction in this path will always be right, which is a 1 bit, hence sn is non-zero exactly when there are additional levels to traverse.

Hmm. I tend to think of every tree as having infinite levels. If zeros on the right edge mean "skip", that just means there are infinitely many "skip" directives at the front of every path. (Subtrees also potentially have infinite levels, but past some point, zeros and ones both mean "skip". Or you subtract start and that removes the ones.) But I think this is probably what equivalent interpretation makes most sense to you.

I added "When sn is zero, the procedure has reached the top of the tree." I think there's lots of ways to see why (including "In this numbering, a node's level can be determined as follows: if the node is a root of subtree [start, end), the node's level is BIT_WIDTH(end - start - 1)") that we can probably just assert that and let the reader justify it to themselves in whatever way makes most sense. This doesn't need to be a rigorous proof, just enough to get the intuition across.

nharper · 2025-10-10T21:06:27Z

+
+Inclusion proofs can also be evaluated by considering these two stages separately. The first stage consumes `l1 = BIT_WIDTH(fn XOR sn)` proof entries. The second stage consumes `l2 = POPCOUNT(fn >> l1)` proof entries. A valid inclusion proof must then have `l1 + l2` entries. The first `l1` entries are hashed based on `fn`'s least significant bits, and the remaining `l2` entries are hashed on the left.
+
+## Consistency Proof Verification {#consistency-proof-bits}


Something that helped me understand this better was when you told me that fn, sn, and tn stand for "first number", "second number", and "third number". Perhaps that would be useful for others and could be mentioned in this section. I think r means "running hash"?

(EDIT 1: Out of scope for this PR, but the naming of fr and sr implies some correlation between those and fn and sn. In RFC 9162 2.1.4.2, there is no tn, and there is direct correlation between the inputs first, first_hash and variables fn and fr (same for second, second_hash, sn, and sr). In this MTC draft, the variables fr and sr seem more closely correlated with sn and tn than they do with fn and sn, which makes me think those variables should be renamed. Maybe sr and tr? Maybe nh (node hash) and rh (root hash)?)

EDIT 2 (also out of scope for this PR): Both verification procedures follow the same pattern: initialize some variables, then loop over the proof array and incorporate hashes. Could the variables be renamed so that fn and r in the inclusion proof procedure have the same names as sn and sr in the consistency proof procedure? AFAICT, once we're in the loop, those are performing the exact same steps (though the initialization is different). (While we're there, maybe give the same name to p in the inclusion proof procedure as c in the consistency proof procedure? I'm assuming p means "proof" and c means "consistency proof", which isn't consistent.)

Added some notes about first, second, and third number. Agreed the variable names are horrid. I'm on board with changing them. Maybe we can do better than first/second/third in the first place, I dunno.

The notes look good. If I think of better names, I'll write up a PR.

nharper · 2025-10-10T22:28:17Z

+
+In the second case, `fn` is less than `sn`. Step 6 will then initialize the hashes to the first value in the consistency proof.
+
+From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.


"From there, step 6 incorporates the consistency proof ..." Step 6 was initializing fr and sr, and is described above. I think that sentence is supposed to say "step 7" instead of "step 6", or I'm misunderstanding something in the verification or this explanation.

Ah yeah, things got jumbled when the steps were renumbered in another PR. Fixed.

nharper · 2025-10-10T23:21:59Z

+
+The procedure in {{verifying-a-subtree-consistency-proof}} iteratively builds two hashes, `fr` and `sr`, which are expected to equal `node_hash` and `root_hash`, respectively. Everything hashed into `fr` is also hashed into `sr`, so success demonstrates that `root_hash` contains `node_hash`.
+
+A subtree consistency proof for `[start, end)` with the tree of `n` elements is a truncated inclusion proof for element `end - 1`. The proof is truncated until the highest common node between the right edge of `[start, end)` and the right edge of the tree.


I think something is missing from this description, but I haven't figured it out yet. I'll take another look next week.

I think in part because it's wrong. :-) (It's not the right edge of the tree) I've rephrased it and elaborated.

nharper · 2025-10-10T23:22:20Z

+From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.
+
+In the case when `fn` is `sn` in step 5, the condition in step 7.2.1 is always false, and `fr` is always equal to `node_hash` in step 8. In this case, steps 6 through 8 are equivalent to verifying an inclusion proof for the truncated subtree `[fn, sn + 1)` and truncated tree `tn + 1`.
+


I'm getting a bit of "and then draw the rest of the owl" vibes from this. I'll take another look on Monday to see if I can offer a suggestion on more words here.

Mostly it's assumed you already read the inclusion proof one. It's really the same function, we're just doing more work along the side. Expanded on it a bit.

Match RFC 9162's styling

davidben

Made a bunch of changes, including to supporting text.

davidben · 2025-10-11T03:11:56Z

+
+Iterating from level 0 up, `fn` and `sn` will initially be different. While they are different, step 4.2 hashes on the left or right based on the binary representation, as discussed in {{binary-representations}}.
+
+Once `fn = sn`, the procedure has reached the point where the path diverges from the right edge. At that point, the condition in step 4.2 is always tree. It only incorporates proof entries on the left, once per set bit. Unset bits are skipped.


Whoops, yes. Fixed.

davidben · 2025-10-11T03:24:04Z

+
+In the second case, `fn` is less than `sn`. Step 6 will then initialize the hashes to the first value in the consistency proof.
+
+From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.


Ah yeah, things got jumbled when the steps were renumbered in another PR. Fixed.

davidben · 2025-10-12T16:50:14Z

+
+The procedure in {{evaluating-a-subtree-inclusion-proof}} builds up a subtree hash in `r` by staring from `entry_hash` and iteratively hashing elements of `inclusion_proof` on the left or right. That means this procedure, when successful, must return *some* hash that contains `entry_hash`.
+
+Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.


Think that fit slightly better in the next paragraph, but added something to this effect. I added some text in the previous section to make it clear that the right edge and the path to the last element are the same. (It seems to work better to talk about paths.)

davidben · 2025-10-12T16:57:40Z

+
+Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.
+
+Step 4 iterates through `inclusion_proof` and bit positions in parallel. Comparing `sn` to zero ensures that the two iterators stop together, i.e. there aren't extra or missing inclusion proof entries.


Hmm. I tend to think of every tree as having infinite levels. If zeros on the right edge mean "skip", that just means there are infinitely many "skip" directives at the front of every path. (Subtrees also potentially have infinite levels, but past some point, zeros and ones both mean "skip". Or you subtract start and that removes the ones.) But I think this is probably what equivalent interpretation makes most sense to you.

I added "When sn is zero, the procedure has reached the top of the tree." I think there's lots of ways to see why (including "In this numbering, a node's level can be determined as follows: if the node is a root of subtree [start, end), the node's level is BIT_WIDTH(end - start - 1)") that we can probably just assert that and let the reader justify it to themselves in whatever way makes most sense. This doesn't need to be a rigorous proof, just enough to get the intuition across.

davidben · 2025-10-12T17:26:52Z

+
+The procedure in {{verifying-a-subtree-consistency-proof}} iteratively builds two hashes, `fr` and `sr`, which are expected to equal `node_hash` and `root_hash`, respectively. Everything hashed into `fr` is also hashed into `sr`, so success demonstrates that `root_hash` contains `node_hash`.
+
+A subtree consistency proof for `[start, end)` with the tree of `n` elements is a truncated inclusion proof for element `end - 1`. The proof is truncated until the highest common node between the right edge of `[start, end)` and the right edge of the tree.


I think in part because it's wrong. :-) (It's not the right edge of the tree) I've rephrased it and elaborated.

davidben · 2025-10-12T17:36:59Z

+
+Inclusion proofs can also be evaluated by considering these two stages separately. The first stage consumes `l1 = BIT_WIDTH(fn XOR sn)` proof entries. The second stage consumes `l2 = POPCOUNT(fn >> l1)` proof entries. A valid inclusion proof must then have `l1 + l2` entries. The first `l1` entries are hashed based on `fn`'s least significant bits, and the remaining `l2` entries are hashed on the left.
+
+## Consistency Proof Verification {#consistency-proof-bits}


Added some notes about first, second, and third number. Agreed the variable names are horrid. I'm on board with changing them. Maybe we can do better than first/second/third in the first place, I dunno.

davidben · 2025-10-12T17:40:30Z

+From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.
+
+In the case when `fn` is `sn` in step 5, the condition in step 7.2.1 is always false, and `fr` is always equal to `node_hash` in step 8. In this case, steps 6 through 8 are equivalent to verifying an inclusion proof for the truncated subtree `[fn, sn + 1)` and truncated tree `tn + 1`.
+


Mostly it's assumed you already read the inclusion proof one. It's really the same function, we're just doing more work along the side. Expanded on it a bit.

nharper · 2025-10-14T20:17:59Z

+
+Inclusion proofs can also be evaluated by considering these two stages separately. The first stage consumes `l1 = BIT_WIDTH(fn XOR sn)` proof entries. The second stage consumes `l2 = POPCOUNT(fn >> l1)` proof entries. A valid inclusion proof must then have `l1 + l2` entries. The first `l1` entries are hashed based on `fn`'s least significant bits, and the remaining `l2` entries are hashed on the left.
+
+## Consistency Proof Verification {#consistency-proof-bits}


The notes look good. If I think of better names, I'll write up a PR.

nharper · 2025-10-14T22:45:36Z

+In the first case, `fn` will equal `sn` after truncation. Step 5 will then initialize the hashes to `node_hash`. The consistency proof does not need to include a separate copy of `node_hash`.
+
+In the second case, `fn` is less than `sn`. Step 6 will then initialize the hashes to the first value in the consistency proof.


It's not clear what cases these are referring to, and they're not the two bullet points above. (fn can equal sn after performing either of those steps.) I'd clarify by changing this to something like the following:

Steps 5 and 6 initialize the hashes fr and sr.

If fn equals sn (possibly after truncation), step 5 initializes the hashes to node_hash because the subtree [start, end) is directly contained in the tree, so the consistency proof did not need to include a separate copy of node_hash.

Otherwise, fn is less than sn, and step 6 initializes the hashes to the first value in the consistency proof.

They should be the same as the two bullet points, I think. Rather, the two bullets don't quite match step 3 and step 4. I added some parentheses to make that clear. (I found these two cases to be more natural, but they didn't quite line up with code.)

meacer · 2025-10-15T23:42:07Z

+~~~
+{: #fig-subtree-consistency-example-1 title="An example subtree consistency proof for a subtree that is directly contained in the full tree"}
+
+The subtree consistency proof for `[8, 13)` and a tree of size 14 contains `MTH({d[12]})`, `MTH({d[12]})`, `MTH(D[8:12])`, and `MTH(D[0:8])`, depicted in {{fig-subtree-consistency-example-2}}. `[8, 13)` is not directly contained in the tree, so the proof must include sufficient nodes to reconstruct both hashes.


MTH({d[12]}), MTH({d[12]}) --> should be MTH({d[12]}), MTH({d[13]})?

Whoops, yes. Fixed.

nharper

one nit, otherwise looks good

nharper · 2025-10-15T23:55:04Z

+
+A subtree consistency proof for `[start, end)` and the tree of `n` elements is similar to an inclusion proof for element `end - 1`. If one starts from `end - 1`'s hash, incorporating the whole inclusion proof should reconstruct `root_hash` and incorporating a subset of the inclusion proof should reconstruct `node_hash`. Thus `end - 1`'s hash and this inclusion proof can prove consistency. A subtree consistency proof in this document applies two optimizations over this construction:
+
+1. Instead of starting at level 0 with `end - 1`, the proof can start at a higher level. Any ancestor of `end - 1` shared by both the subtree and the overall tree will `node_hash` and `root_hash`. Use the highest level with a commmon ancestor. This truncates the inclusion proof portion of the consistency proof.


nit: missing a word in "the overall tree will node_hash and root_hash"?

Whoops, fixed.

davidben requested a review from lukevalenta October 6, 2025 16:34

davidben commented Oct 6, 2025

View reviewed changes

davidben added 2 commits October 6, 2025 18:27

Add an appendix that explains the proof procedures

cfc9cc4

Closes #147

Use BIT_WIDTH instead of log2

3ffb3a1

Use the things we've already defined.

davidben force-pushed the proof-explain branch from c0ef457 to 3ffb3a1 Compare October 6, 2025 22:27

nharper reviewed Oct 10, 2025

View reviewed changes

davidben added 8 commits October 12, 2025 12:41

Consistently capitalize Merkle Tree

f9ba9de

Match RFC 9162's styling

Add example subtree consistency and inclusion proofs

7afc5bd

Fix typos

d3020e0

Clarify that the rightmost edge is the path to the last element

d57ccce

Clarify how we iterate by bit

a970be7

Clarify the starting node business

818dfec

Explain fn/sn/tn

83bc984

Expand on consistency proof evaluation

86d39b8

davidben commented Oct 12, 2025

View reviewed changes

Merge remote-tracking branch 'origin/main' into proof-explain

f7da5bc

nharper reviewed Oct 14, 2025

View reviewed changes

davidben added 5 commits October 15, 2025 10:32

Tweak description of the consistency proof

81ef41b

Make two diagrams

0f492f4

Split structure and verification into different sections

bc3b3b3

Consistency proof verification tweaks

f200c20

Path directions are too hard

07988d2

meacer reviewed Oct 15, 2025

View reviewed changes

nharper approved these changes Oct 16, 2025

View reviewed changes

davidben added 2 commits October 15, 2025 22:39

Fix typo

03dd65d

Missing words

c595971

davidben merged commit 923c83b into main Oct 17, 2025
2 checks passed

davidben deleted the proof-explain branch October 17, 2025 20:06


		* `BIT_WIDTH(n)` refers to the smallest number of bits needed to represent `n`. `BIT_WIDTH(0)` is zero.

		* `POPCOUNT(n)` refers to the number of set bits in `n`'s binary representation`.


		Iterating from level 0 up, `fn` and `sn` will initially be different. While they are different, step 4.2 hashes on the left or right based on the binary representation, as discussed in {{binary-representations}}.

		Once `fn = sn`, the procedure has reached the point where the path diverges from the right edge. At that point, the condition in step 4.2 is always tree. It only incorporates proof entries on the left, once per set bit. Unset bits are skipped.


		The procedure in {{evaluating-a-subtree-inclusion-proof}} builds up a subtree hash in `r` by staring from `entry_hash` and iteratively hashing elements of `inclusion_proof` on the left or right. That means this procedure, when successful, must return some hash that contains `entry_hash`.

		Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.


		Treating `[start, end)` as a Merkle Tree of size `end - start`, the procedure hashes by based on the path to `index`. Within this smaller Merkle Tree, it has index `fn = index - start`. The procedure additionally follows `sn = end - start - 1`, the path to the last element.

		Step 4 iterates through `inclusion_proof` and bit positions in parallel. Comparing `sn` to zero ensures that the two iterators stop together, i.e. there aren't extra or missing inclusion proof entries.


		Inclusion proofs can also be evaluated by considering these two stages separately. The first stage consumes `l1 = BIT_WIDTH(fn XOR sn)` proof entries. The second stage consumes `l2 = POPCOUNT(fn >> l1)` proof entries. A valid inclusion proof must then have `l1 + l2` entries. The first `l1` entries are hashed based on `fn`'s least significant bits, and the remaining `l2` entries are hashed on the left.

		## Consistency Proof Verification {#consistency-proof-bits}


		In the second case, `fn` is less than `sn`. Step 6 will then initialize the hashes to the first value in the consistency proof.

		From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.


		The procedure in {{verifying-a-subtree-consistency-proof}} iteratively builds two hashes, `fr` and `sr`, which are expected to equal `node_hash` and `root_hash`, respectively. Everything hashed into `fr` is also hashed into `sr`, so success demonstrates that `root_hash` contains `node_hash`.

		A subtree consistency proof for `[start, end)` with the tree of `n` elements is a truncated inclusion proof for element `end - 1`. The proof is truncated until the highest common node between the right edge of `[start, end)` and the right edge of the tree.

		From there, step 6 incorporates the consistency proof into `sr` as in inclusion proof evaluation. In parallel, step 7.2.1 incorporates a subset of the hashes into `fr`, ony of those subtrees are contained within `[start, end)`. Specifically, it incorporates only those hashes to the left of the path, and stops incorporating when `fn` and `sn` have no longer diverged.

		In the case when `fn` is `sn` in step 5, the condition in step 7.2.1 is always false, and `fr` is always equal to `node_hash` in step 8. In this case, steps 6 through 8 are equivalent to verifying an inclusion proof for the truncated subtree `[fn, sn + 1)` and truncated tree `tn + 1`.

		In the first case, `fn` will equal `sn` after truncation. Step 5 will then initialize the hashes to `node_hash`. The consistency proof does not need to include a separate copy of `node_hash`.

		In the second case, `fn` is less than `sn`. Step 6 will then initialize the hashes to the first value in the consistency proof.


		A subtree consistency proof for `[start, end)` and the tree of `n` elements is similar to an inclusion proof for element `end - 1`. If one starts from `end - 1`'s hash, incorporating the whole inclusion proof should reconstruct `root_hash` and incorporating a subset of the inclusion proof should reconstruct `node_hash`. Thus `end - 1`'s hash and this inclusion proof can prove consistency. A subtree consistency proof in this document applies two optimizations over this construction:

		1. Instead of starting at level 0 with `end - 1`, the proof can start at a higher level. Any ancestor of `end - 1` shared by both the subtree and the overall tree will `node_hash` and `root_hash`. Use the highest level with a commmon ancestor. This truncates the inclusion proof portion of the consistency proof.

Uh oh!

Conversation

davidben commented Oct 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nharper left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

davidben left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nharper left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

davidben commented Oct 6, 2025 •

edited

Loading