refactoring the ics23 spec

[konnov]

This is a refactoring of the ICS23 spec, which took more effort than I expected (about 8hrs in total):

• the spec is now split in multiple files,
• the spec is now using the up-to-date syntax and idioms,
• importantly, hashes are modelled as symbolic terms, see hashes.qnt
• removed TLA+ files, as we do not want to maintain them in the long run,
• removed the simple PBT tests, as they were not useful, in favor of tree generators treeGen.qnt.

Reviewing this specification is probably a big effort. So I would appreciate at least a quick glance, to check that nothing weird stands out.

[thpani]

First set of remarks. I've only made it through hashes.qnt so far.

[thpani]

Wow 🤯
Second set of comments below:

[thpani]

This looks to be the tendermint spec, but the comment says IavlSpec.
Can we confirm which one it is?

[konnov]

True, I always thought it Iavl, but seems to be Tendermint

[thpani]

seems to be Tendermint

Can we ask someone to confirm?

[konnov]

@romac and I had a look at the code this morning. Not easy to see, but both IavlSpec and TendermintSpec should work. Hugs to @romac for figuring that out. That code is beyond my comprehension 🍄

[thpani]

I thought this was good to merge, but something in 60a2df4 broke the verifyNonMembershipTest in ics23test.

[josef-widder]

Looks super useful for testing. I guess now with the sum types, we could turn this spec more readable. I will reach out to the team to see how we can coordinate around merging it.

[josef-widder]

For a binary tree, This would also be encoded today as sum type, e.g., a list of LeftNode, RightNode.

[konnov]

I have to note that Quint sum types are not inductive/recursive, for a reason of not admitting unbounded data structures. So it would not be possible to encode a tree with Quint sum types.

[josef-widder]

But now it is a list of integers, where only 0 and 1 is used. Why cannot it be a list of a sum type instead?

[konnov]

Try to write it in any language that has complete support for sum types, e.g., in OCaml. You will see that you need recursion. Basically, you have to say that a node refers to the children nodes (of the same type). If you use a mathematical function instead, e.g., $f: Paths \rightarrow Nodes$, you do not need an inductive definition.

[konnov]

A list of a sum type would not give you much, as you would not want a leaf to appear in the middle of the list.

[josef-widder]

Root's children is checked with length(p) == 1. If this would be a defined predicate, perhaps it would be more readable.

[josef-widder]

I am not sure I understand what is going on here. Does this only work if left and right don't contain an entry for [1]? Otherwise the expression lwidth + p[0] below would suddenly introduce keys whose value is greater than 1.

[konnov]

As far as I remember, every node is encoded as the path to this node. For instance, [0, 1, 0, 1] in a binary tree would mean that you first go left, then right, then left, then right. So if we count the number of paths of length 1, then we get the number of root's children.

[josef-widder]

I agree, but if we have 2 root's children, we get lwidth = 2, but then two lines below we have

 keys(right).map(p => [ lwidth + p[0] ].concat(p.slice(1, length(p))))

So it seems that I could get a 2 and a 3 as first list entry, and this is what I don't understand.

[konnov]

That definition merges two trees. Say, if you have root's children [0, 1] in tree 1 and root's children [0, 1] in tree 2, then you would like to have root's children [0, 1, 2, 3]. This is what addition does for you: It simply renames the immediate root's children in tree 2, for all paths in that tree.

[josef-widder]

That makes sense. I just thought we would stay with binary trees...

[shonfeder]

Clearing my name from the review requests here.

Hope all is well! <3

[bugarela]

@josef-widder I realize now that the reason why we can't merge this is that a test is failing.

$ quint test ics23test.qnt --verbosity=5

  ics23test
    ok existsCalculateTest passed 1 test(s)
    ok isLeftMost1Test passed 1 test(s)
    ok isLeftMost2Test passed 1 test(s)
    ok isLeftMost3Test passed 1 test(s)
    ok isRightMost1Test passed 1 test(s)
    ok isRightMost2Test passed 1 test(s)
    ok isLeftStep1Test passed 1 test(s)
    ok isLeftNeighborTest passed 1 test(s)
    1) verifyNonMembershipTest failed after 1 test(s)

  8 passing (31ms)
  1 failed

  1) verifyNonMembershipTest:
      /home/gabriela/projects/quint/examples/cosmos/ics23/ics23test.qnt:136:7 - error: [QNT508] Assertion failed
      136:       assert(verifyNonMembership(root, np1, [ 1 ])),

[Frame 0]
verifyNonMembership(
  Map(
    [0, 0] -> { b: [0, 1, 2, 3, 32], t: "r" },
    [0, 1, 0] -> { b: [0, 1, 2, 3, 1, 2, 32], t: "r" },
    [0, 1, 1, 0] -> { b: [3], t: "r" },
    [0, 1, 1] -> { b: [], t: "h" },
    [0, 1] -> { b: [], t: "h" },
    [0, 2, 0] -> { b: [0, 1, 2, 3, 1, 4, 32], t: "r" },
    [0, 2, 1, 0] -> { b: [5], t: "r" },
    [0, 2, 1] -> { b: [], t: "h" },
    [0, 2] -> { b: [], t: "h" },
    [0] -> { b: [], t: "h" }
  ),
  {
    key: [1],
    left: { key: [], leaf: { prefix: Map([0] -> { b: [], t: "r" }) }, path: [], value: [] },
    right:
      {
        key: [2],
        leaf: { prefix: Map([0] -> { b: [0, 1, 2, 3], t: "r" }) },
        path:
          [
            {
              prefix: Map([0] -> { b: [0, 1, 2, 3], t: "r" }),
              suffix: Map([0] -> { b: [32], t: "r" }, [1, 0] -> { b: [0, 1, 2, 3, 1, 4, 32], t: "r" }, [1, 1, 0] -> { b: [5], t: "r" }, [1, 1] -> { b: [], t: "h" }, [1] -> { b: [], t: "h" })
            }
          ],
        value: [3]
      }
  },
  [1]
) => false

I've inspected the commits since the last time it was passing, and I suspect that this is the problematic bit: 2335cf9.

Maybe this test needed to be updated according to the new representation including the length marker byte, but wasn't - I'm not sure, as I don't really understand what is going on here. Do you have a sense of the problem?

[bugarela]

Notes, mostly for my future self: My fix from 1115a51 was enough to make the existing invariants hold on simulations, but even after playing with the verifyNonMembership tests a lot, and checking that the mocked proofs match the generated ones, they were still failing.

I noticed that the invariants had a lot of non-determinism, so I wrote a stronger invariant that checks verifyNonMembership results for all possible keys, and that doesn't hold.

Upon debugging, I found that isLeftStep is returning false for a proof I expected to be verified. It fails on the hasPadding test, but I'm not convinced this is the only issue. At this point, I don't understand where/how we should add prefixes that are longer than the minPrefix from IavlSpec (4).

cc @josef-widder