refactoring the ics23 spec

[konnov]

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

• [x] the spec is now split in multiple files,
• [x] the spec is now using the up-to-date syntax and idioms,
• [x] importantly, hashes are modelled as symbolic terms, see hashes.qnt
• [x] removed TLA+ files, as we do not want to maintain them in the long run,
• [x] 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]

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

[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: https://github.com/informalsystems/quint/pull/975/commits/2335cf9ff4f853f93cdae3a3e2f80f28647d3f35.

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?