Prove inclusion of subtree into another tree

[HarryTmetic]

This discussion continues from #115, where the topic of subtree inclusion has been started.
To keep the original thread focused, let's use this discussion here on the subtree inclusion!

Prove that a particular node is a frontier node in LER_A at index k by showing that the right-adjacent leaf has a value of zero in LER_A.

I don't think we need this step as the first step in the proof would be to use the leaf_count and frontier of the respective trees to recompute the root hashes in both trees against which the Merkle proofs for the same leaf will be generated, and if the root of tree_A can be properly derived from its leaf_count and frontier, it means that the leaf at index k = leaf_count - 1 we are trying to prove inclusion of is the last element of tree_A
The rest follows nicely as briefly discussed face to face with @bpfarmer and @hadjiszs earlier this week.
Below is the pseudo code:

# Generate the proof that the tree structures are preserved up to the same leaf
def generate_proof(leaf_count_A, frontier_A, leaf_count_B, frontier_B):
    # Reconstruct the root hashes of both trees
    root_A = reconstruct_root(frontier_A, leaf_count_A)
    root_B = reconstruct_root(frontier_B, leaf_count_B)

    # Calculate the position of the last leaf in tree A
    position = leaf_count_A - 1

    # Generate Merkle proofs for the same position in both trees
    merkleProofA = generate_merkle_proof(tree_A, position)
    merkleProofB = generate_merkle_proof(tree_B, position)

    return merkleProofA, merkleProofB

proof_A, proof_B = generate_proof(leaf_count_A, frontier_A, leaf_count_B, frontier_B)

# Verify the proof
def verify_proof(proof_A, proof_B, leaf_count_A, root_A, root_B, leaf):
    position = leaf_count_A - 1

    # Verify individual Merkle proofs
    if not verify_merkle_proof(proof_A, leaf, root_A):
        return False
    if not verify_merkle_proof(proof_B, leaf, root_B):
        return False

    # Verify invariants based on the binary address of the leaf
    for i in range(len(proof_A)):
        if get_bit_at(position, i) == 0 and proof_A[i] != proof_B[i]:
            return False
    return True

[bpfarmer]

I don't think we need this step as the first step in the proof would be to use the leaf_count and frontier of the respective trees

Do we have this data? I was under the impression that chains were signing the LER but not the leaf_count and frontier.

root_A = reconstruct_root(frontier_A, leaf_count_A)

What does reconstruct_root do here? I'm not sure that we can derive the root from a single node and a leaf count.

In the pseudo-code, I think there's a missing check that the two nodes at position are equal.

if get_bit_at(position, i) == 0 and proof_A[i] != proof_B[i]:

As @invocamanman noted - we don't need to binary-decompose the index given that we already have the pivots in proof_B. Need to look at where the pivot bit is set to zero in the path and then ensure that the entry at the same index in proof_A is equal.

[bpfarmer]

Just to follow up on this - I think it's important to verify leaf_count of A. I don't think it's sufficient for a chain to sign the leaf_count and frontier. I think there's an attack where a chain could import an invalid LER by lying about the leaf count, and the inclusion proof would still pass.

Consider LET_A, a valid LET with leaf_count k. Now an attacker can add a bunch of nodes to LET_A to form LET_Malicious, but not update leaf_count. Meanwhile, Chain A also adds new nodes to LET_A to form LET_A'. I think that the inclusion check for LET_Malicious should still pass, even though LET_Malicious has nodes that conflict with LET_A'.

As an alternative to verifying a separate inclusion proof for the right-most node we could always precompute roots for empty subtrees and then verify in proof_A that any entry in the path on the right is the root of an empty subtree. I'm not sure that's simpler or more efficient.

Could also pass leaf_count as a public input and increment with each PP but that seems more complicated to me.

[HarryTmetic]

Do we have this data? I was under the impression that chains were signing the LER but not the leaf_count and frontier.

The bridge service provides the Merkle proofs for all claims/exits so it has access to all the leaves and to the LET (defined as the leaf_count and frontier).

What does reconstruct_root do here?

reconstruct_root is used for instance by the bridge service in order to compute the LER.
The pseudo code is very general (as in describing a general method to prove "subtree" inclusion) so it tries to take everything needed to compute and verify the final proof, so that's why I included the root computation since it is eventually needed for the verification.

I'm not sure that we can derive the root from a single node and a leaf count.

The frontier is a set (of size max TREE_DEPTH) nodes and given the leaf_count you can reconstruct the root of the tree since the leaf count informs you about what to merge and with what up to the last level of the tree.

In the pseudo-code, I think there's a missing check that the two nodes at position are equal.

I'm not sure this is needed because if the prover takes 2 different position, then the verification of the final proof would fail, which should be what is expected.

As @invocamanman noted - we don't need to binary-decompose the index given that we already have the pivots in proof_B. Need to look at where the pivot bit is set to zero in the path and then ensure that the entry at the same index in proof_A is equal.

Could you explain what you mean by pivots?

I don't think it's sufficient for a chain to sign the leaf_count and frontier. I think there's an attack where a chain could import an invalid LER by lying about the leaf count, and the inclusion proof would still pass.
Consider LET_A, a valid LET with leaf_count k. Now an attacker can add a bunch of nodes to LET_A to form LET_Malicious, but not update leaf_count. Meanwhile, Chain A also adds new nodes to LET_A to form LET_A'. I think that the inclusion check for LET_Malicious should still pass, even though LET_Malicious has nodes that conflict with LET_A'.

I'm probably misunderstanding what you mean, but since the leaf_count_A and frontier_A completely define the LET_A (resp. leaf_count_A' and frontier_A' completely define the LET_A') and so the root as well. If it is signed, and even if an adversary appends some new leaves (unrelated to what is on-chain) this shouldn't have any effect. The leaf at leaf_count_Malicious would be different form the leaf at leaf_count_A' so the inclusion proof of the leaf at leaf_count_Malicious into the final LET would fail.

[bpfarmer]

The bridge service provides the Merkle proofs for all claims/exits so it has access to all the leaves and to the LET (defined as the leaf_count and frontier).

Right - my concern was around verifying this data.

The frontier is a set (of size max TREE_DEPTH) nodes and given the leaf_count you can reconstruct the root of the tree since the leaf count informs you about what to merge and with what up to the last level of the tree.

I see what you mean - I had thought that frontier referred to the right-most leaf. What you're doing is computing the roots of empty subtrees and using the set of right-most non-empty nodes to regenerate the root. Calling this regenerate_root is maybe a bit confusing, as it's not necessary to regenerate the root (we already have it signed/authenticated by a PP), but it is necessary to prove that a certain node is the right-most node and the rest of the tree is empty.

Just thinking out loud, we can precompute the roots for empty powers-of-two subtrees of sizes 2^0 -> 2^31 and use these to efficiently verify the right-most leaf (and that the remainder of the tree is empty). The disadvantage of this approach vs proving that the adjacent leaf is empty is that it is more complex and possibly more expensive (though in theory you should save on a couple of hashes), but the advantage is that while it should suffice to prove that the adjacent leaf is empty to prove that every leaf to the right of the right-most leaf is empty, given the PP, we might mess up somewhere and it might be good to have some redundancy.

Note it's not necessary to perform this check for LET_B - we already have the LER from the PP.

I'm not sure this is needed because if the prover takes 2 different position, then the verification of the final proof would fail

No, the case is that two leaves have the same position, but are different. Remember that the subtree inclusion check takes the inclusion proofs for the node at position k in LET_A and LET_B. It checks that for every left pivot in the merkle proof, the provided node in the path is identical to the provided node in the path in LET_A (technically, I think that your pseudo-code is incorrect, as I think - though it's late here - that it should be taking bits from 2^DEPTH - position).

Take the case where we have 4 leaves (positions 0,1,2,3) and the right-most element in LET_A is at position 2. The only check is that the second element in the inclusion proof is identical in both proofs (this shows that the subtree containing leaves 0, 1 is identical in both trees). Unless we explicitly check that the node at position 2 is identical in both trees, it's possible to pass the check with different nodes at the same position.

Could you explain what you mean by pivots?

The inclusion path in the tree should look something like Vec<(node, bit)> where the "pivot" bit defines whether the node is hashed on the left or right of the calculated intermediate root.

I'm probably misunderstanding what you mean

No, it wasn't clear to me how you were verifying the right-most node in your scheme, because it was unclear what reconstruct_root was doing. In my comment, I noted that:

As an alternative to verifying a separate inclusion proof for the right-most node we could always precompute roots for empty subtrees and then verify in proof_A that any entry in the path on the right is the root of an empty subtree.

This is in fact what you're doing!

[bpfarmer]

Want to close the loop here - fixing the above pseudo-code:

# Formerly: Generate the proof that the tree structures are preserved up to the same leaf
# This method didn't have sufficient information to compute the merkle proof of the leaf at index leaf_count_a - 1 in B
# The frontier already serves as the Merkle path for the right-most leaf in A, so it doesn't make sense to compute it
# Instead, let's just delete
# def generate_proof(leaf_count_A, frontier_A, leaf_count_B, frontier_B):

# Verifies that A is a subtree of B
# Note that merkle_proof_B is the inclusion proof of the node at position leaf_count_A in B
def verify_subtree(leaf_count_A, frontier_A, root_A, merkle_proof_B, root_B):
    
    # Only reconstruct the root for A, verifying that all leaves with index >= leaf_count_A are empty
    # Reference the from_parts and get_root methods in the Rust implementation of the LET
    if root_A != get_root(frontier_A, leaf_count_A):
        return False

    # Verify individual Merkle proof for B
    # Leaf should be included in the proof, don't need a separate var
    if not verify_merkle_proof(proof_B, root_B):
        return False


    # We don't technically need the merkle path from A - I think that we just need to verify that every element of
    # frontier_A shows up in the merkle proof for the leaf at position leaf_count_A in B. 
    # Remove position = leaf_count_a - 1 ---- should be the 1-indexed position of the leaf, not the 0-indexed position.
    # If we're following the Rust implementation of the LET, then the bit was backward.
    # The nice thing is that this version will enforce that the nodes at position are identical in both trees
    # Too lazy to look up python range syntax - I know that 0..TREE_DEPTH is not correct, but it'll be in rust anyway
    # Note that I didn't find a definition of the Merkle Path in the Rust implementation, so indices may need to be adjusted.
    for i in 0..TREE_DEPTH:
        if get_bit_at(leaf_count_A, i) == 1 and frontier_A[i] != proof_B[i]:
            return False
    return True

[HarryTmetic]

The frontier (after appending the leaf at leaf_count) – although it provides a proof that not only the leaf at leaf_count is included in tree A but also that it's the last non-zero leaf – is not the same as the Merkle path of the leaf into tree A (sometimes the leaf itself can be part of the frontier cf see example below with h_4). The frontier is just to store the minimal amount of information in order to be able to append new leaves and reconstruct the root.

if get_bit_at(leaf_count_A, i) == 1 and frontier_A[i] != proof_B[i]:

I don't think this works, I think we need to compare frontier_A (or equivalently proof_A) and proof_B not at leaf_count_A but rather at leaf_count_A - 1
As a couple concrete examples for a tree with 8 leaves max:

• For leaf h_4 with leaf_count_A = 5 (101)
  Frontier: [h_4, h_01, h_0123]
  Merkle path in tree B: [h_5, h_67, h_0123]
• For leaf h_5 with leaf_count_A = 6 (110)
  Frontier: [h_4, h_45, h_0123]
  Merkle path in tree B: [h_4, h_67, h_0123]

In both cases the frontier and Merkle path are not the same at the 1-indices and so the check would fail.

That's why we need to compare the frontier given the address of the leaf in the tree and not the leaf count i.e., leaf_count_A - 1 in binary (starting with LSB), this gives us:

• For leaf h_4 with leaf_count_A - 1 = 4 (100)
  Frontier: [h_4, h_01, h_0123]
  Merkle path in tree B: [h_5, h_67, h_0123]
• For leaf h_5 with leaf_count_A - 1 = 5 (101)
  Frontier: [h_4, h_45, h_0123]
  Merkle path in tree B: [h_4, h_67, h_0123]

Now we have the check that passes at the 1-indices.

[bpfarmer]

The frontier is just to store the minimal amount of information in order to be able to append new leaves and reconstruct the root.

Indeed - it consists of the roots of all maximal power-of-2-sized subtrees. But you don't construct it properly in your examples. For instance, the frontier for the tree of max 8 leaves consisting of 5 leaves has the following structure:

frontier_5 = [h_4, 0, h_0123, 0]

This might be a source of the confusion. I linked the code in my last comment, but it's here.

For subtree inclusion, it suffices to show that every non-zero entry in the frontier of A is contained in B. Your proposal to bit-decompose leaf_count_A - 1 doesn't work because it doesn't map to non-zero entries of the frontier of A. An easy counterexample to show why we don't want to bit-decompose leaf_count_a - 1 is to take the tree with 1 leaf - we would perform zero checks.

To your example, for the 5th leaf (h_4) that you provide, we need to check that h_4 is identical in B and that h_0123 (the root of the subtree consisting of the first four leaves) is identical in B. Your "corrected" version doesn't do this - it takes the bit-decomposition of 4, 0010, and only checks h_0123, but not h_4. Instead, if we bit-decompose 5, we get 1010, and we're checking at the correct indices of the frontier of A.

For the 6th leaf (h_5), the frontier of A is actually this:

frontier_6 = [0, h_45, h_0123, 0]

We want to check h_45 and h_0123. So, we bit-decompose 6 to 0110 and we're checking in the appropriate indices of the frontier of A.

Your example (bit-decomposing 5) checks h_4 (though your frontier is wrong - h_4 isn't included) and h_0123, but it actually isn't sound to check h4 and h_0123. The attacker can change h_5 in B.

We can see in simpler examples, ex n=8, why bit-decomposing leaf_count_A - 1 doesn't work.

frontier_8 = [0, 0, 0, h_012345678] - we bit-decompose 8, 0001, which points us to the index of the frontier that we want to check.

In a comment on my last post, I did handwave the indexing of the path in B a bit as it wasn't defined, but when we implement we can make sure that it's indexed properly. The important point is that bit-decomposing leaf_count_A points us to non-zero entries of the frontier, and we can reconstruct the matching node from the path in B.