Add support for SMT non-membership (exclusion) proofs

[h5law]

Overview

Currently the cosmos/ics23 library has support for the range proofs used to prove non-membership done by Penumbra's JMT [1]. The use of a range proof is common across the other ProofSpec types in cosmos/ics23. However celestiaorg/smt (now unmaintained) does not support this. As we have forked and now maintain and use this SMT in production pokt-network/smt [2] and this implementation achieves non-membership proof verification differently this issue aims to outline the support for this method.

[1] https://github.com/penumbra-zone/jmt/blob/4a96055cbc70f3baef5bd73978d332880c601ded/src/tree.rs#L1036
[2] https://github.com/pokt-network/smt

SMT Proofs

The SMT (pokt-network/smt) does non-membership proofs by proving the existence of 1 of 2 things:

1. A default value (defaultValue []byte = nil) where the key was found
2. An unrelated key-value pair in the place of where the key should be

• Unrelated keys can be found in place of the key we are looking for as they share a common prefix

An example of SMT proofs being used with cosmos/ics23 can be found here [1]

[1] https://github.com/pokt-network/pocket/blob/ibc/module_creation/ibc/stores/proofs_ics23.go

Deliverables

In order to implement this change without breaking support for range proofs a new CommitmentProof type representing a non-membership proof should be implemented along the lines of the following

message ExclusionProof {
    bytes key = 1;
    bytes actual_path = 2;
    bytes actual_valueHash = 3;
    LeafOp leaf = 4;
    repeated InnerOp path = 5;
}

In the above the actual_path field will either contain the unrelated leaf data or the correct path with a null value pairing. In addition to the above the following must also be done:

• Implement verification logic in line with (non-)existence proofs for the ExclusionProof type
• Integrate the ExclusionProof with the CommitmentProof protobuf
• Add a type switch to non-membership proofs to trigger the correct verification logic
• Add test cases to verify the proof works as expected
• Update references to celestiaorg/smt -> pokt-network/smt

Non-Goals

• Change any logic related to (non-)existence proof verification
• Break any backwards compatibility

Owner: @h5law

[Olshansk]

@h5law Thanks for putting this together and just want to publically support and make a request to prioritize it. Leaving a few thoughts/comments/questions below.

---

In the above the actual_path field will either contain the unrelated leaf data or the correct path with a null value pairing

1. Do you mean actual_leaf or path field in place of actual_leaf?
2. I'm not too familiar with the structures in ics23/v1/proofs.proto, but would advocate for some sort of oneof usage so its explicit whether we are proving a null subtree or another leaf w/ the same prefix.
3. Request to rename UnrelatedProof to ExclusionProof in reference to the original JMT whitepaper [1].

4. By integrate the UnrelatedProof with the CommitmentProof protobuf, do you mean making it oneof the proofs available?

[1] https://developers.diem.com/papers/jellyfish-merkle-tree/2021-01-14.pdf

---

Update references to celestiaorg/smt -> pokt-network/smt

💯 as Pocket is the only one supporting it moving forward

[h5law]

Do you mean actual_leaf or path field in place of actual_leaf?

So actual leaf will contain the data of the leaf we find in the SMT after traversing the path until we get to a leaf node. For any key this could be:

var defaultValue []byte = nil

excl := &ExclusionProof{
    ...
    ActualPath: originalPath,
    ActualValueHash: defaultValue,
    ...
}

or

excl := &ExclusionProof{
    ...
    ActualPath: unrelatedLeafPath,
    ActualValueHash: unrelatedLeafValueHash,
    ...
}

This is in line with the proofs generated by the SMT and would represent the NonMembershipLeafData field of the SparseMerkleProof type.

I'm not too familiar with the structures in ics23/v1/proofs.proto, but would advocate for some sort of oneof usage so its explicit whether we are proving a null subtree or another leaf w/ the same prefix.

This is already the way for the proof types and they are switched based on the type found

message CommitmentProof {
  oneof proof {
    ExistenceProof exist = 1;
    NonExistenceProof nonexist = 2;
    BatchProof batch  = 3;
    CompressedBatchProof compressed = 4;
  }
}

I don't think it is needed to switch within the new type itself because the same operations will be made depending on whether we are proving the default value or unrelated key-value pair. This is not decided upon by the user but is generated by the SMT automatically when creating a proof. See [1] and look at how NonMembershipLeafData is populated.

[1] https://github.com/pokt-network/smt/blob/cc555d9078dcd1492032992a76e9ea17303220d4/smt.go#L303

Request to rename UnrelatedProof to ExclusionProof in reference to the original JMT whitepaper

Yeah ExclusionProof is much better updated in the issue ⭐

By integrate the UnrelatedProof with the CommitmentProof protobuf, do you mean making it oneof the proofs available?

Yes see the reply above for this and how the different proof types are already oneof. Integrating it means adding it here and implementing its logic (similar to existence proof) and then adding a switch to the VerifyNonMembership function to check for proof type and execute accordingly

@Olshansk

[crodriguezvega]

@h5law Thanks a lot for opening this issue. Just for my understanding (and forgive me if I am getting something wrong or forgetting anything), your proposal is...

To add in proofs.proto the new commitment proof type:

message ExclusionProof {
  bytes            key         = 1;
  LeafOp           actual_leaf = 2;
  repeated InnerOp path        = 3;
}

/*
CommitmentProof is either an ExistenceProof or a NonExistenceProof, or a Batch of such messages
*/
message CommitmentProof {
  oneof proof {
    ExistenceProof       exist      = 1;
    NonExistenceProof    nonexist   = 2;
    BatchProof           batch      = 3;
    CompressedBatchProof compressed = 4;
    ExclusionProof       exclusion  = 5;
  }
}

To convert the exclusion proof In go/ics23.go into a regular NonExistenceProof:

func getNonExistProofForKey(spec *ProofSpec, proof *CommitmentProof, key []byte) *NonExistenceProof {
	switch p := proof.Proof.(type) {
	case *CommitmentProof_Nonexist:
		np := p.Nonexist
		if isLeft(spec, np.Left, key) && isRight(spec, np.Right, key) {
			return np
		}
	case *CommitmentProof_Batch:
		for _, sub := range p.Batch.Entries {
			if np := sub.GetNonexist(); np != nil && isLeft(spec, np.Left, key) && isRight(spec, np.Right, key) {
				return np
			}
		}
	case *CommitmentProof_Exclusion:
		// convert p.Exclusion proof into NonExistenceProof
	}
	return nil
}

And then implement in NonExistenceProof's Verify function the logic required to do the verification for the exclusion proof.

Is that more or less at a high level?

Do we need to add a new ProofSpec like the one you have here?

[h5law]

@crodriguezvega Appreciate the response

To add in proofs.proto the new commitment proof type:

Yes I plan to change the proto file as you described here

To convert the exclusion proof In go/ics23.go into a regular NonExistenceProof:

The ExclusionProof verification logic is basically identical to the ExistenceProof. Ideally we would convert the ExclusionProof into an ExistenceProof using the actual_leaf field to populate the ExistenceProof this way we can verify either the inclusion of a default nil value at the key provided or the presence of an unrelated key where the key we want should be. This is more in line with how the SMT ExclusionProof works rather than the NonExistenceProof which proves a range. However for this to integrate in this function would require a lot of changes to the NonExistenceProof verification logic to support a non-range based proof. It may be better to do the following:

func VerifyNonMembership(spec *ProofSpec, root CommitmentRoot, proof *CommitmentProof, key []byte) bool {
	// decompress it before running code (no-op if not compressed)
	proof = Decompress(proof)
        if ex, ok := proof.(*CommitmentProof_ExclusionProof); ok {
                // Convert proof to ExistenceProof and VerifyMembership()
        }
	np := getNonExistProofForKey(spec, proof, key)
	if np == nil {
		return false
	}
	err := np.Verify(spec, root, key)
	return err == nil
}

Do we need to add a new ProofSpec like the one you have here?

As I have merged the lazy loading PR into the SMT this means by default the SMT stores only hashed values. For the purposes of the IBC stores we want the data to be retrievable not just its hash so the custom ProofSpec type simply reflects the SMT not hashing its values at all prior to hashing the node. I dont think changing this in this repo is necissary as it is not the default behaviour of the SMT.

[crodriguezvega]

Thanks for the explanation, @h5law. Ok, so then you would convert the ExclusionProof into an ExistenceProof and verify if the default value or an unrelated value is present at the provided key.

However for this to integrate in this function would require a lot of changes to the NonExistenceProof verification logic to support a non-range based proof.

Could you elaborate a bit more on this? I guess doing this changes would be the cleaner way to do it, right? Maybe it's worth exploring a bit to see if we could achieve it.

Tagging here @AdityaSripal so that he can also give his opinion.

@h5law Would you be interested in opening a draft PR with the changes (doesn't need to be perfect, or complete with all testing, etc)? Having an initial implementation might be also useful for the discussion.

[h5law]

@crodriguezvega I will put up my PR now then. To be clear I have not implemented testing and only done the Go implementation no rust yet. But it works with my SMT code base using replace github.com/cosmos/ics23/go => ../ics23/go to test the changes. I have integrated the new type with Batch Proofs and compression as well in Go.

Could you elaborate a bit more on this? I guess doing this changes would be the cleaner way to do it, right? Maybe it's worth exploring a bit to see if we could achieve it.

So currently the way the NonExistenceProof objects are verified is they prove a range - take a left key and a right key prove they exist and prove they are neighbours and this proves the key is not where it should be (this may be a naive interpretation but this is generally the gist of it). When we do the sanity checks on the NonExistenceProof we first check a few things - do we have 2 existence proofs (left and right) are they actually neighbours etc.

In order to change this type to support non-range based proofs it would mean adding extra fields (similar to the ExistenceProof having the path/steps) or just using a single of the 2 existence proofs embedded within it. This means the verification logic for the NonExistenceProof will become more complicated as we try to support a non-range (exclusion) proof and range based proof in a single type. I think this will be more complicated than simply adding a new type to represent a different kind of proof.

[AdityaSripal]

Would be useful to get @hdevalence or @plaidfinch opinion here as they are using the standard Nonexistence proofs for their own jellyfish tree. Is the pokt SMT tree (forked from celestia) unable to do the same?

[h5law]

Is the pokt SMT tree (forked from celestia) unable to do the same?

@AdityaSripal I read through the rust JMT code and they also do a range proof. SMT proves differently, the ExclusionProof works more like the ExistenceProof. Without changing the SMTs proof verification logic we cannot use the NonExistenceProof as is. The PR I have put up is fully backwards compatible and works proofs_ics23.go with tests passing.

I dont want to change the SMTs proof generation code as it works well. It makes more sense to integrate here and then expand the reach of cosmos/ics23 for non-range based non-membership proofs

[larry0x]

Hey guys, we have the same issue, as we also uses a radix tree as our Merkle commitment scheme.

Our non-membership proof is not compatible with ICS-2, as such we had to create our own custom light client. If the changes suggested here is merged, we won't need the extra work.

Our non-membership proof format is the same as outlined in the JMT whitepaper, referenced in this previous comment.

Would love to see this this feature pushed forward. Happy to make a PR...

[larry0x]

I would suggest renaming the current NonExistenceProof to BSTNonExistenceProof as it's intended for binary search trees, and the new variant we're adding as RadixNonExistenceProof to highlight it's designed for a different type of trees.

[larry0x]

I attempted to implement this today, but realized a problem:

To verify JMT's exclusion proof, ICS-23 needs to know how an internal node is laid out; that is, if the bit is 0, then go to left child; otherwise go to right child:

We need to use this logic to demonstrate that an internal node doesn't have a certain child.

I feel this is against ICS-23's philosophy, which is to be generic and not concern the implementation details of any specific Merkle tree.

For example, if we choose to include this logic, then a Merkle tree that does the opposite (0 = right child, 1 = left child), or has more than 2 children per internal node, will have trouble using this proof format.