Non-existence proof verification failed

[yito88]

We can verify the non-existence proof with another proof spec because the left or right leaf's key and value are hashed in Sparse Merkle Tree.

However, we cannot switch the proof spec in the IBC client module. The proof spec is used for both the existence and non-existence proof verification.

[yito88]

The proof and the verification work well, however, sparse-merkle-tree(SMT) isn't compatible with the current IBC integration. We need to replace the Merkle tree implementation.

The problem is that the non-existence proof-verification requires a different proof spec from that of the existence proof verification.
IBC VP couldn't verify the receipt absence on the counterparty chain (when packet-timeout) because IBC VP (ibc-rs and cosmos(ibc-go)) uses the same proof spec for the existence and non-existence proof verification. It is set in an IBC client state.

• Proof spec of the leaf for the existence proof

LeafOp {
    hash: H::hash_op().into(),
    prehash_key: H::hash_op().into(),
    prehash_value: H::hash_op().into(),
    length: LengthOp::NoPrefix.into(),
    prefix: H256::zero().as_slice().to_vec(),
}

• Proof spec of the leaf for the non-existence proof

LeafOp {
    hash: hash_op.into(),
    prehash_key: HashOp::NoHash.into(),
    prehash_value: HashOp::NoHash.into(),
    length: LengthOp::NoPrefix.into(),
    prefix: H256::zero().as_slice().to_vec(),
}

The non-existence proof needs a different proof spec because sparse-merkle-tree (SMT) returns the proof with the hashed key and value of neighbors in SMT.

For the existence proof, we can replace the key and value in the proof generated by SMT with a non-hashed(original) key and value to verify it with ICS23 verification which checks if the key and value are equal to the target key and value. So, the proof spec's LeafOp (it says how to calculate the leaf hash) should set the prehash_key and prehash_value with the hash operation (Sha256 in this case) to calculate their hashes after the comparison.

pub struct ExistenceProof {
    #[prost(bytes = "vec", tag = "1")]
    pub key: ::prost::alloc::vec::Vec<u8>,
    #[prost(bytes = "vec", tag = "2")]
    pub value: ::prost::alloc::vec::Vec<u8>,
    #[prost(message, optional, tag = "3")]
    pub leaf: ::core::option::Option<LeafOp>,
    #[prost(message, repeated, tag = "4")]
    pub path: ::prost::alloc::vec::Vec<InnerOp>,
}

• Replace the hashed key and value
  https://github.com/anoma/anoma/blob/8eeab64ca0765950cef4c8a0c1f5b9de6a672b90/shared/src/ledger/storage/merkle_tree.rs#L251-L261

• ICS23 checks the key and value (called by ibc-rs verification)
  https://github.com/confio/ics23/blob/8ea0b239740068dd004fe4a42a1d861cd607611c/rust/src/verify.rs#L22-L23

We want to replace the hashed key and value for the non-existence proof, but we cannot. That's because they are hashed and we don't know the original key and value of the neighbors (we know only the target key at that time).
The non-existence proof has existence proofs of the neighbors. ICS23 verification checks the existence proofs. These existence proofs have the hashed key and value. We can verify the proof with the spec which sets the prehash_key and prehash_value with NoHash because they have been already hashed. (ICS23 verification doesn't compare that key to the given key in the non-existence proof verification.) However, ibc-rs/cosmos uses the same proof spec for the existence and non-existence proof.

pub struct NonExistenceProof {
    #[prost(bytes = "vec", tag = "1")]
    pub key: ::prost::alloc::vec::Vec<u8>,
    #[prost(message, optional, tag = "2")]
    pub left: ::core::option::Option<ExistenceProof>,
    #[prost(message, optional, tag = "3")]
    pub right: ::core::option::Option<ExistenceProof>,
}

I tried to modify SMT to have the original key and value in each leaf and to get the proof with them. But ICS23 refused the proof. ICS23 verification checks also the key order for the non-existence proof. The original keys order is not the same as hashed keys' order in the tree. That's why it failed.

[cwgoes]

because sparse-merkle-tree (SMT) returns the proof with the hashed key and value of neighbors in SMT.

Returns specifically the non-existence-proof with the hashed key and value of neighbors?

We want to replace the hashed key and value for the non-existence proof, but we cannot. That's because they are hashed and we don't know the original key and value of the neighbors (we know only the target key at that time).

Hmm, we must be storing the key and value of the neighbors in the tree somewhere, right? Can we look them up in order to produce the proofs?

I tried to modify SMT to have the original key and value in each leaf and to get the proof with them. But ICS23 refused the proof. ICS23 verification checks also the key order for the non-existence proof. The original keys order is not the same as hashed keys' order in the tree. That's why it failed.

Hmm, I don't quite follow - if you have the original key and value in each leaf, why would the key order be different? Are some intermediate values still being hashed an extra time, compared to what ICS23 expects?

[yito88]

@cwgoes Thank you for your comments!

because sparse-merkle-tree (SMT) returns the proof with the hashed key and value of neighbors in SMT.

Returns specifically the non-existence-proof with the hashed key and value of neighbors?

non-existence-proof consists of existence-proofs of left and right. The existence-proofs have hashed key and value.

We want to replace the hashed key and value for the non-existence proof, but we cannot. That's because they are hashed and we don't know the original key and value of the neighbors (we know only the target key at that time).

Hmm, we must be storing the key and value of the neighbors in the tree somewhere, right? Can we look them up in order to produce the proofs?

Yes, I could store a non-hashed key-value pair as Value in an SMT leaf node and produce proofs with the original key-value pairs.

I tried to modify SMT to have the original key and value in each leaf and to get the proof with them. But ICS23 refused the proof. ICS23 verification checks also the key order for the non-existence proof. The original keys order is not the same as hashed keys' order in the tree. That's why it failed.

Hmm, I don't quite follow - if you have the original key and value in each leaf, why would the key order be different? Are some intermediate values still being hashed an extra time, compared to what ICS23 expects?

The key order in SMT is arranged with the hashed keys. However, ICS23 checks the order with the given key. When the given key is non-hashed (in the case of IBC), the order isn't the same as hashed keys' order, e.g. the hashed key of the left should be smaller than the hashed given key in SMT, but the non-hashed key of the left might be larger than the given key.
https://github.com/confio/ics23/blob/8ea0b239740068dd004fe4a42a1d861cd607611c/rust/src/verify.rs#L38
https://github.com/confio/ics23/blob/8ea0b239740068dd004fe4a42a1d861cd607611c/rust/src/verify.rs#L42

[yito88]

Note:
Our SMT provides functions to make ICS23 proofs from the tree.
The ICS23 proofs can be verified in our tests.
However, these proofs cannot be used in IBC proof-verification due to the above issue.