Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Add support for SMT ExclusionProofs #153

Closed
wants to merge 12 commits into from
Closed

feat: Add support for SMT ExclusionProofs #153

wants to merge 12 commits into from

Conversation

h5law
Copy link

@h5law h5law commented Jun 19, 2023

This PR implements the support for SMT ExclusionProofs and verifies them by using converting them into an ExistenceProof and verifying either the existence of a nil value at the key provided or an unrelated key-value pair in place of the key provided.

NOTE: In the LeafOp of the ExclusionProof the reason we set the PrehashKey and PrehashValue to HashOp_NO_HASH is because the ActualPath and ActualValueHash fields should be populated by the NonMembershipLeafData field of the SMT proof and as such should already be hashed in accordance with the TreeSpec meaning hashing them again would result in an incorrect root computation.

@h5law
Copy link
Author

h5law commented Jun 19, 2023

@crodriguezvega @AdityaSripal This is still a WIP and the following must be done:

  • Add unit tests to the go library to cover the new type and any changes made
  • Add support for Rust, and Javascript and add unit tests

@h5law h5law changed the title [WIP] Add support for SMT ExclusionProofs feat: [WIP] Add support for SMT ExclusionProofs Jun 19, 2023
@h5law h5law changed the title feat: [WIP] Add support for SMT ExclusionProofs feat: Add support for SMT ExclusionProofs Jun 28, 2023
@h5law
Copy link
Author

h5law commented Jun 28, 2023

@crodriguezvega @AdityaSripal This PR is now ready for review. Go and rust implementations with test coverage are included. No JS support. This is partially due to me not seeing a usecase currently for JS and having no experience with TS. As it stands this logic will be used in our go project at Pocket and the rust will be used in my implementation of ICS-08 for our WASM client.

@@ -1,5 +1,5 @@
DOCKER := $(shell which docker)
HTTPS_GIT := https://github.com/cosmos/cosmos-sdk.git
HTTPS_GIT := https://github.com/cosmos/ics23.git
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change was made as the current make proto-check-breaking doesn't work it would say something about needing 2 contianers? I will revert this if someone can say how to make it work as intended.

Copy link

@Olshansk Olshansk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Left a couple minor NITS.

Approving because core business logic LGTM but requires review/approval from an owner of the repo as well.

go/vectors_data_test.go Outdated Show resolved Hide resolved
go/vectors_data_test.go Outdated Show resolved Hide resolved
return ep
}
case *CommitmentProof_Batch:
for _, sub := range p.Batch.Entries {

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is this the intended behaviour: for a batch of exclusion proofs we just return the first valid one?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We are checking the batch for the exclusion proof with the correct key. If there are multiple then they are the same proof and we need only return 1.

When we validate a batch in entirety we go through all proofs and execute them individually. This is just that we were given a batch entry and are looking to prove just the one with the matching key.

@@ -43,7 +43,7 @@ var TendermintSpec = &ProofSpec{
},
}

// SmtSpec constrains the format for SMT proofs (as implemented by github.com/celestiaorg/smt)
// SmtSpec constrains the format for SMT proofs (as implemented by github.com/pokt-network/smt)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🙌

Comment on lines +175 to +180
if p.Leaf.PrehashKey != HashOp_NO_HASH {
return nil, errors.New("exclusion proof must have leaf with PrehashKey == NO_HASH")
}
if p.Leaf.PrehashValue != HashOp_NO_HASH {
return nil, errors.New("exclusion proof must have leaf with PrehashValue == NO_HASH")
}

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this a requirement? Consider adding a comment or updating the error message with the reasoning

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I left a comment explaining this in the proto but will add again here

go/proof.go Show resolved Hide resolved
go/proof.go Outdated
}
// check if the actual value was a placeholder and replace with empty hash
// assumes the placeholder value is [32]byte
if bytes.Equal(p.ActualValueHash, make([]byte, 32)) {

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Readability NIT: Move make([]byte, 32) into a constant in this package or a local var and rename to smtPlaceholder

@crodriguezvega
Copy link
Contributor

@crodriguezvega @AdityaSripal This PR is now ready for review. Go and rust implementations with test coverage are included. No JS support. This is partially due to me not seeing a usecase currently for JS and having no experience with TS. As it stands this logic will be used in our go project at Pocket and the rust will be used in my implementation of ICS-08 for our WASM client.

Thank you, @h5law! We have also contacted the Penumbra folks and ask them to take a look at the PR.

Regarding JS support, we have talked in the past to actually stop support for it, so I wouldn't worry about it for now. If we end up still wanting to keep support, I could at some point port your Go implementation into TS.

@Olshansk
Copy link

@crodriguezvega @AdityaSripal This PR is now ready for review. Go and rust implementations with test coverage are included. No JS support. This is partially due to me not seeing a usecase currently for JS and having no experience with TS. As it stands this logic will be used in our go project at Pocket and the rust will be used in my implementation of ICS-08 for our WASM client.

Thank you, @h5law! We have also contacted the Penumbra folks and ask them to take a look at the PR.

Regarding JS support, we have talked in the past to actually stop support for it, so I wouldn't worry about it for now. If we end up still wanting to keep support, I could at some point port your Go implementation into TS.

Would be great to connect with the Penumbra directly. In particular, I believe they might appreciate/adopt the work we're doing at https://github.com/pokt-network/smt

Copy link
Member

@AdityaSripal AdityaSripal left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand the proof here. You're proving the existence of the actualPath and actualValueHash in the tree. But at what point does this prove that the key you provided does not exist?

There's nothing in the proof verification that is constraining the value of p.ActualPath based on p.Key

Perhaps I'm just not understanding how an existence proof of the "unrelated key/value pair" as you say in the PR is a proof of exclusion for the key in question

@h5law
Copy link
Author

h5law commented Jun 29, 2023

I don't understand the proof here. You're proving the existence of the actualPath and actualValueHash in the tree. But at what point does this prove that the key you provided does not exist?

There's nothing in the proof verification that is constraining the value of p.ActualPath based on p.Key

Perhaps I'm just not understanding how an existence proof of the "unrelated key/value pair" as you say in the PR is a proof of exclusion for the key in question

So the actual path / value hash fields are populated by

  1. traverse the tree according to key until we find a leaf
  2. if this leaf's path == hash(key) we have found the right key (inclusion proof)
  3. if this leaf's path != hash(key) we have found an unrelated leaf
  4. as the leaf cannot have children the key we are looking for cannot be in the tree (but it shares a common prefix with the leaf we found which is how we know its definietly not there)
  5. using the leaf we founds data construct an exclusion proof to show the existence of an unrelated key in the place our key should be

@Olshansk
Copy link

Olshansk commented Jun 29, 2023

@AdityaSripal Just wanted to follow up on what @h5law mentioned with a bit of a simplification and some diagrams (see [jmt]).

We can prove exclusion of key by either:

  1. Empty node along path(key)
  2. Different key at path(key)

Screenshot 2023-06-29 at 1 16 53 PM

Screenshot 2023-06-29 at 1 17 32 PM

jmt

@Olshansk
Copy link

I know there was a lengthy offline (slack/discord) discussion with @AdityaSripal @hdevalence and others related to not having ExclusionProofs in ics23, but rather just updating https://github.com/pokt-network/smt to support range proofs.

@h5law could you capture and summarize the key takeaways and next steps?

cc @musalbas for context

@h5law
Copy link
Author

h5law commented Jul 20, 2023

@h5law could you capture and summarize the key takeaways and next steps?

The general sentiment is that instead of supporting newer proof mechanisms, the repo aims to support just a single form of NonMembershipProof using the "range based" (not exactly a range) technique already present. Although this is very specific to the IAVL tree, SMTs such as the JMT by penumbra have modified their implementation of the JMT to use this proof system instead of the intended ExclusionProof (proving the non-existence of a key via a sentinel value due to the sparse nature of the tree).

As a result of this intention it was suggested to have the SMT library instead support the same "range based" non-membership proof as the JMT and IAVL tree. As a result I have opened this issue in the SMT library.

I would like to add that although I will add support for this proof type I think that forcing newer tree types into using the same methods for generating proofs is not the way this library should be moving in. I feel that if we are able to support newer proof types, as long as the changes are backwards compatible we should do so. This enables the innovation to increase, potentially improvements in efficiency as time moves on. IBC is about interoperability not uniformity.

CC: @AdityaSripal @crodriguezvega @hdevalence @plaidfinch

@jackzampolin
Copy link
Member

Strongly agree with @h5law that only supporting a single proof method here is counter to the whole abstraction provided by ics23

@faddat
Copy link
Contributor

faddat commented Aug 24, 2023

@jackzampolin -- I agree.

There's the whole question of dragons and the like re: ics23, will dive in for a bit.

@crodriguezvega
Copy link
Contributor

crodriguezvega commented Aug 28, 2023

Thanks for all the comments here, everyone. Our apologies to @h5law for not providing public feedback on the PR earlier. The reason for that is that discussions happened privately on Slack approximately a month ago, and the understanding of the people involved in them was that Harry would try Penumbra's suggestion of adding support for range-based non-inclusion proofs in Pocket's SMT implementation in the same way that Penumbra did for their JMT implementation, instead of adding support for a new type of exclusion proof to ics23. Penumbra team's arguments were:

  • Changes to ics23 need to be rolled out across the whole ecosystem.
  • Keeping verifier complexity down is an important security goal.
  • ics23 non-inclusion proof style works for sparse and non-sparse trees, at the cost of implementation effort for the sparse merkle tree author.

Even though Penumbra's and Harry's views on how to support non-inclusion proofs for SMT differed, we had the impression that Harry would still try to implement Penumbra's suggestion. Unfortunately that was a misunderstanding from our side, and the consequence was that this PR did not get enough attention since then. Last week @jackzampolin brought this PR again to our attention, and conversations with Harry followed. We agreed that we will pick this up again in approximately one week from now, once @AdityaSripal is back from holidays.

Again, thanks everyone for the feedback and for putting this again in our radar. Whenever anybody notices that an issue of PR is falling through the cracks, feel free to ping us on Slack or Discord, or write a message on the relevant issue/PR. Due to our capacity constraints, we cannot treat everything with high priority, but with a bit of information and context, some rationale for prioritisation, and a pinch of kindness and understanding ❤️ we will do our best to make compromises to fit requests in as soon as possible.

@AdityaSripal
Copy link
Member

So the actual path / value hash fields are populated by

traverse the tree according to key until we find a leaf
if this leaf's path == hash(key) we have found the right key (inclusion proof)
if this leaf's path != hash(key) we have found an unrelated leaf
as the leaf cannot have children the key we are looking for cannot be in the tree (but it shares a common prefix with the > > leaf we found which is how we know its definietly not there)
using the leaf we founds data construct an exclusion proof to show the existence of an unrelated key in the place our key should be

I understand that this is how you are constructing the proof. But I don't see where in the verification logic you are checking that this is what took place. My expectation would be that there are some checks that ensure that p.ActualPath is what you expect given the p.Key.

Namely there should be some check that the path taken is a prefix of the desired key and that the path is not the key itself.

I couldn't find any checks in the ICS23 code to that effect.

Maybe I'm still fundamentally misunderstanding but this is why it took me some time to reply and asked Penumbra for their input since im still a bit confused by the PR.

To illustrate my point I've written up this test case here:

62a057b

Here I took a valid existence proof of the key in question, and malformed it to create an exclusion proof for that same exact key that passes VerifyNonMembership.

In fact as the verification exists right now, I'm pretty sure I could have taken a completely unrelated leaf and stuck it into the exclusion proof with any desired Key and had it pass.

Again its possible I'm missing some very obvious point and maybe made some silly error in my test case writeup. But at the moment I don't see it.

If it is the case that I'm right, then this PR needs to be reworked to add some check of the p.ActualPath using p.Key and I think p.ActualPath will have to contain the preimage and not the hash in order for this to work

@crodriguezvega
Copy link
Contributor

@h5law Did you have time to check out Aditya's comment above and the corresponding PR?

@h5law
Copy link
Author

h5law commented Oct 20, 2023

@crodriguezvega Yes sorry I forgot to update this PR, @AdityaSripal and I synced offline on this. I would like to pick this issue back up and have it in full feature parity to the SMT doing the check itself at a later date. I still believe this is an important feature add to the ics23 repo and will build it in soon, once we have released the next iteration of our protocol.

The issue aditya pointed out is covered in the SMT itself but I looked over it here, although it took a long time Aditya's review will come in very helpful when I pick this up again in the near future.

As a result I will be closing this PR and will open a new one when the time comes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants