Compare generalized Merkle proof formats

[cwgoes]

cc @jaekwon
cc @mossid

• Key-path based implementation in Tendermint
• Cross-language implementation by Ethan Frey

[cwgoes]

The only documentation I can find for the Tendermint implementation is this ADR. That just defines an interface, not a specification which could be passed to a runtime when a client is created (the likely procedure in IBC), so I think it's a bit less versatile than Ethan Frey's implementation which uses a similar operation-based interface but has more supported operations.

@jaekwon had a concern about that implementation which I don't think I understand (if you could summarize that would be fantastic). What do you think @mossid?

[ethanfrey]

Thank you @cwgoes for opening this up for discussion. I actually don't see them as competing but collaborating specs.

The tendermint ProofOp defines a way to chain various merkle proofs one after another. But leave the implementation of any ProofOp undefined (some interface, dynamic registration). The SDK uses the implementation in iavl, which uses the go-amino encoded range proof. There is no spec for this format, and it would be hopeless to attempt to validate in any language besides go.

My ics23 implementation was designed to form a clear format for any ProofOp. This is well spec'd and there exists tested validation logic in 3 languages. It does not, however, include a spec of how to chain these together. This was an explicit design decision for interoperability with existing code. Also ICS23 should be generic to support non-sdk proof generators and eventually even non-tendermint ones, so I wanted to get consensus on the most generic parts first.

The simplest solution is to create an implementation of ProofOp that uses the ics23 format for now. Mid-term, the ProofOp chain logic should be better specified and support multiple languages. If you wish, it could be added to part of ics23, but I tried to make this as non-invasive as possible, waiting for the core sdk and tendermint teams to decide how they wanted to plug it in.

[mossid]

The ICS23 spec is only the interface so the multiple concrete specs can be used, and I agree with using tendermint ProofOp for layering and general proofs for single merkle proof. In any case we should specify both of them under ICS23 as concrete specs(where Tendermint ProofOp works as "combinator" of other ICS23 proofs, so Op interface itself should be compatible with ICS23).

[ethanfrey]

I'm for adding some spec'd version of Tendermint Proof/ProofOp to ICS23 implementation.

We just need to spec it out first, and then could restrict each ProofOp to be a ics23.CommitmentProof. Importantly, we would need to provide a control format - so we can say this tree should return two CommitmentProofs chained, using Tendermint spec then IAVL spec and combine the keys to form final key. Same what there is an ics23.ProofSpec to remove any wiggle room about which bytes are key and which are value.

[cwgoes]

In addition to the ICS 23 work by @ethanfrey, we need a VerificationSpec or the like which restricts the kinds of LeafOps, HashOps, and LengthOps that can be used with a proof, otherwise we'll open ourselves up to collisions between different hash functions, which violates ICS 23's security properties.

I wonder if it is worth re-assessing how a proof specification format like this compares, in terms of difficulty of implementation, flexibility, and performance, to a generic WASM client or generic WASM state verification functions. I think there may be a case to be made for the latter, since that would give us the same ability to support multiple Merkle trees without upgrading IBC, more flexibility (probably at some cost in performance), and doesn't require multiple compatible implementations.

[ethanfrey]

@cwgoes there is already a spec format required for verification.

The format:
https://github.com/confio/ics23/blob/master/proofs.proto#L143-196

And an example of the spec of iavl proofs:
https://github.com/confio/ics23-iavl/blob/master/create.go#L11

Note child order was added with an eye to supporting merk from nomic, where they encode [left child, right value, node value] and we need to know the lexographical ordering of these children to avoid abuse in neighbor proofs, needed for non-existence (in merk the ordering is [0, 2, 1]