From 9a079cdcf147baa1bcdd5637d8cc770e36abb964 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 16:53:09 +0200 Subject: [PATCH 01/24] refactor the ICS23 spec --- examples/cosmos/ics23/ics23.qnt | 612 +----------------- examples/cosmos/ics23/ics23pbt.qnt | 106 +++ examples/cosmos/ics23/ics23test.qnt | 133 ++++ examples/cosmos/ics23/ics23trees.qnt | 330 ++++++++++ examples/cosmos/ics23/{ => tla}/ics23.tla | 0 examples/cosmos/ics23/{ => tla}/ics23pbt.tla | 0 .../cosmos/ics23/{ => tla}/ics23trees.tla | 0 examples/cosmos/ics23/words.qnt | 26 + 8 files changed, 604 insertions(+), 603 deletions(-) create mode 100644 examples/cosmos/ics23/ics23pbt.qnt create mode 100644 examples/cosmos/ics23/ics23test.qnt create mode 100644 examples/cosmos/ics23/ics23trees.qnt rename examples/cosmos/ics23/{ => tla}/ics23.tla (100%) rename examples/cosmos/ics23/{ => tla}/ics23pbt.tla (100%) rename examples/cosmos/ics23/{ => tla}/ics23trees.tla (100%) create mode 100644 examples/cosmos/ics23/words.qnt diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index e9d3dce03..b6c906fc1 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -1,4 +1,3 @@ -// -*- mode: Bluespec; -*- // This is a protocol specification of ICS23, tuned towards the IAVL case. // // For details of ICS23, see: @@ -12,69 +11,14 @@ // For the moment, the main goal of this spec is to understand the algorithm // and test it with the simulator. // -// 1. To execute the unit tests in REPL, type the following: -// $ quint repl -// >>> .load ics23.qnt -// >>> import ics23test.* -// >>> allTests -// -// REPL should display 'true'. -// -// 2. To execute simple PBT-like tests for 1000 runs of length up to 10 steps -// in REPL, type the following: -// $ quint repl -// >>> .load ics23.qnt -// >>> import ics23pbt.* -// >>> _test(1000, 10, "Init", "Next", "TestVerify") -// >>> _test(1000, 10, "Init", "Next", "TestNonMem") -// -// If REPL displays 'false', it has found an example, -// which can be inspected with q::lastTrace. -// -// 3. To execute advanced PBT-like tests for 1000 runs in REPL, -// type the following: -// $ quint repl -// >>> .load ics23.qnt -// >>> import trees.* -// >>> _test(1000, 1, "Init", "Next", "NonMemInv") -// >>> _test(1000, 1, "Init", "Next", "MemInv") -// -// If REPL displays 'false', it has found an example, -// which can be inspected with q::lastTrace. We expect these tests to -// always return 'true'. Otherwise, this indicates an invariant violation. -// -// Igor Konnov, Informal Systems, 2022 - -module basics { - /// We represent byte sequences as lists of integers - type WORD_T = List[int] - - /// we interpret the empty word as nil - def isNil(word) = length(word) == 0 - - /// compare two integer words lexicographically - def lessThan(w1, w2) = { - val len1 = length(w1) - val len2 = length(w2) - or { - len1 < len2 and w1.indices().forall(i => w1[i] == w2[i]), - and { - len1 == len2, - w1.indices().exists(i => and { - w1[i] < w2[i], - w1.indices().forall(j => j < i implies w1[i] == w2[j]) - }) - } - } - } -} +// Igor Konnov, Informal Systems, 2022-2023 // This is a specification of the membership and non-membership proofs // of ICS23 for IAVL trees: // // https://github.com/confio/ics23/blob/master/go/proof.go module ics23 { - import basics.* + import words.* from "./words" // ICS23 proof checking for IavlSpec. // In contrast to the ICS32 implementation, we specialize it to binary trees: @@ -219,12 +163,12 @@ module ics23 { // Calls getPadding(0) => idx = 0, prefix = 0. // We specialize the constants to IavlSpec. path.indices().forall(i => - val step = path[i] + val pathStep = path[i] or { // the path goes left - hasPadding(step, MinPrefixLen, MaxPrefixLen, ChildSize), + hasPadding(pathStep, MinPrefixLen, MaxPrefixLen, ChildSize), // the path goes right, but the left child is empty (a gap) - leftBranchesAreEmpty(step) + leftBranchesAreEmpty(pathStep) } ) } @@ -249,12 +193,12 @@ module ics23 { // Calls getPadding(1) => minPrefix, maxPrefix, // suffix = ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 path.indices().forall(i => - val step = path[i] + val pathStep = path[i] or { // the path goes right - hasPadding(step, ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0), + hasPadding(pathStep, ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0), // the path goes left, but the right child is empty (a gap) - rightBranchesAreEmpty(step) + rightBranchesAreEmpty(pathStep) } ) } @@ -345,542 +289,4 @@ module ics23 { isLeftNeighbor(np.left.path, np.right.path) } } -} - -// a few unit tests to improve our understanding of the specification -module ics23test { - import ics23.* - - // test data - val a = [5] - val b = [6] - val c = [7] - val d = [8] - val ab = [5, 6] - val ba = [6, 5] - val abc = [5, 6, 7] - val abcd = [5, 6, 7, 8] - - val allStrings = Set([], a, ab, ba, abc, abcd, [1], [2], [3], [4]) - - val test1 = { - existsCalculate({ - key: [5], - value: [5, 6], - leaf: { prefix: [5, 6, 7] }, - path: [ - { prefix: [5, 6], suffix: [8] }, - { prefix: [5], suffix: [7] } - ] - }) == [32, 0, 4] - } - - val test2 = - isLeftMost([ - { prefix: [1], suffix: [3, 4, 5] }, - { prefix: [2], suffix: [3, 4, 5] }, - { prefix: [3], suffix: [3, 4, 5] } - ]) - - val test3 = - isLeftMost([ - { prefix: [1, 0, 0, 0], suffix: [] }, - { prefix: [2], suffix: [3, 4, 5] }, - { prefix: [3], suffix: [3, 4, 5] } - ]) - - val test4 = - isLeftMost([ - { prefix: [1], suffix: [3, 4, 5 ] }, - { prefix: [2, 0, 0, 0], suffix: [] }, - { prefix: [3], suffix: [3, 4, 5] } - ]) - - val test5 = - isRightMost([ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2, 4, 5, 6], suffix: [] }, - { prefix: [3, 3, 4, 5], suffix: [] } - ]) - - val test6 = - isRightMost([ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2], suffix: [0, 0, 0] }, - { prefix: [3, 3, 4, 5], suffix: [] } - ]) - - val test7 = - isLeftStep( - { prefix: [1], suffix: [4, 5, 6] }, - { prefix: [2, 7, 8, 9], suffix: [] } - ) - - val test8 = - isLeftNeighbor( - [ - { prefix: [1], suffix: [4, 5, 6] }, - { prefix: [2, 7, 8, 9], suffix: [] } - ], - [ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2, 7, 8, 9], suffix: [] } - ] - ) - - val test9 = - // * - // / \ - // 2,3 4,5 - val lhash = existsCalculate({ - key:[2], value: [3], leaf: { prefix: [ 0 ] }, path: [] - }) - val rhash = existsCalculate({ - key:[4], value: [5], leaf: { prefix: [ 0 ] }, path: [] - }) - val left = { - key: [ 2 ], - value: [ 3 ], - leaf: { prefix: [ 0 ] }, - path: [{ prefix: [0], suffix: rhash }] - } - val right = { - key: [ 4 ], - value: [ 5 ], - leaf: { prefix: [ 0 ] }, - path: [{ prefix: [0].concat(lhash), suffix: [] }] - } - val root = [32, 0, 2] - val nilProof = { key: [], value: [], leaf: { prefix: [] }, path: [] } - and { - val np1 = { key: [1], left: nilProof, right: left } - verifyNonMembership(root, np1, [ 1 ]), - val np2 = { key: [2], left: left, right: right } - not(verifyNonMembership(root, np2, [ 2 ])), - val np3 = { key: [3], left: left, right: right } - verifyNonMembership(root, np3, [ 3 ]), - val np4 = { key: [2], left: left, right: right } - not(verifyNonMembership(root, np4, [ 4 ])), - val np5 = { key: [5], left: right, right: nilProof } - verifyNonMembership(root, np5, [ 5 ]), - } - - val allTests = and { - test1, test2, test3, test4, test5, test6, test7, test8, test9 - } -} - -// Simple property-based tests for ics23. They happened to be not very useful, -// as random simulation alone cannot produce even simple examples of sound -// non-membership proofs. For more advanced property-based testing, see the -// module 'trees' below. -module ics23pbt { - import basics.* - import ics23.* - - // an non-membership proof - var nonMemProof: NonExistsProof_T - // a key to test - var inputKey: WORD_T - - // We limit the letters to a very small set, - // including '32' for hash headers. - val Byte = 0.to(3).union(Set(32)) - - val toWord(m) = - m.keys().fold([], (l, i) => l.append(m.get(i))) - - action genKey = - nondet i = Byte.oneOf() - inputKey' = [i] - - action Init = all { - genKey, - // we start with leafs in the initial state - nondet lk = Byte.oneOf() - nondet lv = Byte.oneOf() - nondet lp = Byte.oneOf() - nondet rk = Byte.oneOf() - nondet rv = Byte.oneOf() - nondet rp = Byte.oneOf() - nondet pk = Byte.oneOf() - val lproof = { - key: [ lk ], value: [ lv ], - leaf: { prefix: [ lp ] }, path: [] - } - val rproof = { - key: [ rk ], value: [ rv ], leaf: { prefix: [ rp ] }, path: [] - } - nonMemProof' = { key: [ pk ], left: lproof, right: rproof } - } - - def extend(proof, dir, word) = - val node = - if (dir == "turnLeft") { - prefix: word, - suffix: [] - } else { - prefix: word.slice(0, MaxPrefixLen), - suffix: word.slice(MaxPrefixLen, MaxPrefixLen + ChildSize) - } - proof.with("path", proof.path.append(node)) - - /// grow the proof on the left - action growLeft = - nondet dir = Set("turnLeft", "turnRight").oneOf() - nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() - nonMemProof' = - nonMemProof.with("left", nonMemProof.left.extend(dir, toWord(m))) - - /// grow the proof on the right - action growRight = - nondet dir = Set("turnLeft", "turnRight").oneOf() - nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() - nonMemProof' = - nonMemProof.with("right", nonMemProof.right.extend(dir, toWord(m))) - - action Next = all { - genKey, - any { - growLeft, - growRight - }, - } - - /// by checking this invariant, we may produce an example of when - /// verifyMembership succeeds - val TestVerify = { - val root = existsCalculate(nonMemProof.left) - not(verifyMembership(root, - nonMemProof.left, inputKey, nonMemProof.left.value)) - } - - /// by checking this invariant, we may produce an example of when - /// verifyNonMembership succeeds - val TestNonMem = or { - lessThan(inputKey, nonMemProof.left.key), - lessThan(nonMemProof.right.key, inputKey), - val root = existsCalculate(nonMemProof.left) - not(verifyNonMembership(root, nonMemProof, inputKey)) - } -} - -// Advanced randomized simulation (a la PBT) by generating -// random sorted binary trees of small heights over a small set of keys. -// -// We specify arbitrary binary trees, whose keys (in the leafs) are sorted. -// We do not have to specify IAVL+ trees to produce test data for ICS23. -// Note that this module is needed only for testing of ICS23, -// not for the operation of ICS23. -module trees { - import basics.* - import ics23.* - - /// We represent a binary tree as a collection of maps, - /// whose keys are simply integer values 1..n, with 1 being the root. - /// Similar to pointer-based representations of trees (e.g., in C), - /// this data structure requires additional invariants to make sure - /// that it actually defines a binary tree. - /// This is in contrast to the typical data structures in - /// programming languages. - type TREE_T = { - // every leaf has a key and value assigned - leafs: int -> { key: WORD_T, value: WORD_T }, - // intermediate nodes have left and/or right children - left: int -> int, - right: int -> int - } - - /// the tree generated so far - var tree: TREE_T - /// the node nodeHashes - var nodeHashes: int -> WORD_T - /// the keys to use for non-membership proofs - var leftKey: int - var rightKey: int - /// the key whose non-membership or membership we want to prove - var inputKey: int - - /// limit values to a small set - val Byte = 0.to(7).union(Set(32)) - - /// the maximum tree height - val height = 3 - - /// Compute all parents from the binary representation of the index. - /// To simplify random generation of the trees, we are using - /// the binary encoding. For example, if a leaf has the index 4, - /// that is, 100b, then it has the parents 3 = 10b and 1 = 1b. - def parents(i) = 1.to(height).map(h => i / (2^h)).exclude(Set(0)) - - /// is a given key a node (inner or leaf) of a tree - def isNode(t, key) = or { - key == 1, - t.leafs.keys().contains(key), - t.left.keys().contains(key), - t.right.keys().contains(key), - } - - /// Compute nodeHashes of all nodes into a map. - def computeHashes(t) = { - // compute the hash of a single node, assuming that the children's - // nodeHashes have been computed - def putNodeHash(hashMap, key): (int -> List[int], int) => (int -> List[int]) = { - val h = - if (t.leafs.keys().contains(key)) { - // a leaf - val leaf = t.leafs.get(key) - // Hash the leaf as in ics23.existsCalculate. - // In our trees, prefixes are always 0. - hash([0].append(length(leaf.key)) - .concat(hash(leaf.key)) - .append(length(leaf.value)) - .concat(hash(leaf.value))) - } else { - // an inner node, assuming that the children nodeHashes were computed - def hashOrEmpty(childMap) = - if (childMap.keys().contains(key)) { - hashMap.get(childMap.get(key)) - } else { - EmptyChild - } - // hash the prefix ([0]) and the hash of the children - hash([0].concat(hashOrEmpty(t.left)).concat(hashOrEmpty(t.right))) - } - // store the hash - hashMap.put(key, h) - } - // go over the nodes from max to min - val maxNode = 2^height - 0.range(2^height) - .foldl(Map(), - (m, key) => - if (isNode(t, maxNode - key)) putNodeHash(m, maxNode - key) else m - ) - } - - /// It's very easy to produce binary trees by picking an arbitrary graph and - /// restricting it with the predicate isTree. However, this approach produces - /// very sparse sets of states, to be explored by random search. Hence, we - /// use a more algorithmic approach that represents trees with binary words. - action Init = { - // produce an arbitrary tree with leafs in e.g. [2, 8) - nondet idx = 2.to(2^height - 1).powerset().oneOf() - // remove those numbers that should serve as intermediate nodes - val leafKeys = idx.filter(i => idx.forall(j => not(i.in(parents(j))))) - // compute all parents - val allParents = leafKeys.map(i => parents(i)).flatten() - // all intermediate nodes that have a left successor - val leftKeys = allParents.filter(i => - allParents.union(leafKeys).exists(j => 2 * i == j)) - // all intermediate nodes that have a right successor - val rightKeys = allParents.filter(i => - allParents.union(leafKeys).exists(j => 2 * i + 1 == j)) - // left mapping - val left = leftKeys.mapBy(i => 2 * i) - // right mapping - val right = rightKeys.mapBy(i => 2 * i + 1) - all { - // assign values to the keys - nondet vs = leafKeys.setOfMaps(Byte).oneOf() - val leafs = vs.keys().mapBy(k => { key: [k], value: [vs.get(k)] }) - // the resulting tree - val t = { leafs: leafs, left: left, right: right } - all { - tree' = t, - nodeHashes' = computeHashes(t), - }, - // pick arbitrary left and right keys for non-membership proofs - nondet i = leafKeys.oneOf() - leftKey' = i, - nondet i = leafKeys.oneOf() - rightKey' = i, - // pick an arbitrary input key - nondet i = Byte.oneOf() - inputKey' = i - } - } - - /// convert a tree leaf to an exists proof - def leafToExistsProof(key) = - val value = tree.leafs.get(key).value - // encode all intermediate nodes upwards - val path = range(1, height + 1) - .foldl([], - (p, h) => - if (key < 2^h) { - p - } else { - val parent = key / (2^h) - def hashOrChild(childMap) = - if (childMap.keys().contains(parent)) { - nodeHashes.get(childMap.get(parent)) - } else { - EmptyChild - } - // depending on whether the node is going to left or right, - // push the hashes in the prefix and the suffix - if (key == 2 * parent) { - val right = hashOrChild(tree.right) - p.append({ prefix: [0], suffix: right }) - } else { - val left = hashOrChild(tree.left) - p.append({ prefix: [0].concat(left), suffix: [] }) - } - } - ) - // return the exists proof, where the key is the index itself - { - key: [key], - value: tree.leafs.get(key).value, - leaf: { prefix: [0] }, - path: path, - } - - /// The transition does nothing. The state was computed in Init. - action Next = all { - // nothing changes - tree' = tree, - nodeHashes' = nodeHashes, - leftKey' = leftKey, - rightKey' = rightKey, - inputKey' = inputKey, - } - - /// make sure that the proofs are the same for all the leafs - val TreeProofInv = - and { - leftKey.in(tree.leafs.keys()), - rightKey.in(tree.leafs.keys()) - } implies { - val lroot = existsCalculate(leafToExistsProof(leftKey)) - val rroot = existsCalculate(leafToExistsProof(rightKey)) - lroot == rroot - } - - /// The invariant of membership verification: - /// If the input key belongs to the leafs, - /// we should be able to prove its membership. - val MemInv = or { - not(inputKey.in(tree.leafs.keys())), - val proof = leafToExistsProof(inputKey) - val root = existsCalculate(proof) - verifyMembership(root, proof, [inputKey], proof.value) - } - - /// check this property to produce an example of where MemInv is violated - val MemExample = - not(MemInv) - - // A few lemmas for NonMemInv: - // MemberShouldFalsify, NonMemberInTheMiddle, NonMemberLeft, NonMemberRight - - def MemberShouldFalsify(lproof, rproof) = and { - // if the input key belongs to the leafs, - // we should not be able to disprove its membership - inputKey.in(tree.leafs.keys()), - val nproof = { key: [inputKey], left: lproof, right: rproof } - val root = existsCalculate(lproof) - not(verifyNonMembership(root, nproof, [inputKey])) - } - - def NonMemberInTheMiddle(lproof, rproof) = and { - // we should be able to prove its non-membership, - // unless the choice of the keys is bad - not(inputKey.in(tree.leafs.keys())), - val nproof = { key: [inputKey], left: lproof, right: rproof } - val root = existsCalculate(lproof) - val noKeyInTheMiddle = and { - // there is no leaf between leftKey and rightKey - tree.leafs.keys().forall(k => k <= leftKey or k >= rightKey), - // the keys are not misplaced - leftKey < inputKey, - inputKey < rightKey, - } - noKeyInTheMiddle iff verifyNonMembership(root, nproof, [inputKey]) - } - - def NonMemberLeft(lproof, rproof) = and { - // the input key is to the left - isNil(lproof.key), - // non-membership is true when the right key is left-most - and { - tree.leafs.keys().forall(k => rightKey <= k), - inputKey < rightKey, - } iff and { - // or there is a proof - val root = existsCalculate(rproof) - val nproof = { key: [inputKey], left: lproof, right: rproof } - verifyNonMembership(root, nproof, [inputKey]) - } - } - - def NonMemberRight(lproof, rproof) = and { - // the input key is to the right - isNil(rproof.key), - // non-membership is true when the left key is the right-most - and { - tree.leafs.keys().forall(k => (k <= leftKey)), - inputKey > leftKey, - } iff and { - // or there is a proof - val root = existsCalculate(lproof) - val nproof = { key: [inputKey], left: lproof, right: rproof } - verifyNonMembership(root, nproof, [inputKey]) - } - } - - // The invariant of non-membership verification. - // Consider all possible positions of the input key and the left/right keys. - val NonMemInv = - def proofOrNil(key) = { - if (tree.leafs.keys().contains(key)) - leafToExistsProof(key) - else - { key: [], value: [], leaf: { prefix: [] }, path: [] } - } - val lproof = proofOrNil(leftKey) - val rproof = proofOrNil(rightKey) - or { - MemberShouldFalsify(lproof, rproof), - NonMemberInTheMiddle(lproof, rproof), - NonMemberLeft(lproof, rproof), - NonMemberRight(lproof, rproof), - // trivial cases: - inputKey < rightKey and not(isNil(lproof.key)), - inputKey > leftKey and not(isNil(rproof.key)), - } - - /// check this property to produce an example of where NonMemInv is violated - val NonMemExample = - not(NonMemInv) - - /// Predicate isTree(t) is true iff t defines an ordered binary tree starting - /// with 1. It's probably hard to read. However, it is what one has to specify - /// to express that an arbitrary graph is an ordered tree. - def isTree(t: TREE_T): bool = and { - t.leafs.keys().intersect(t.left.keys()) == Set(), - t.leafs.keys().intersect(t.right.keys()) == Set(), - 1.in(t.leafs.keys().union(t.left.keys().union(t.right.keys()))), - // we impose an order on the keys, to break cycles and DAGs - t.left.keys().forall(k => t.left.get(k) > k), - t.right.keys().forall(k => t.right.get(k) > k), - t.left.keys().intersect(t.right.keys()) - .forall(k => t.left.get(k) < t.right.get(k)), - // the leafs are ordered w.r.t. their keys - val leafKeys = t.leafs.keys() - tuples(leafKeys, leafKeys).forall(kk => - kk._1 < kk._2 implies lessThan(t.leafs.get(kk._1).key, t.leafs.get(kk._2).key) - ), - // all nodes have a parent - (t.leafs.keys().union(t.left.keys()).union(t.right.keys())) - .forall(k => or { - // the root - k == 1, - // there is a left parent - t.left.keys().exists(p => t.left.get(p) == k), - // there is a right parent - t.right.keys().exists(p => t.right.get(p) == k), - }), - } -} +} \ No newline at end of file diff --git a/examples/cosmos/ics23/ics23pbt.qnt b/examples/cosmos/ics23/ics23pbt.qnt new file mode 100644 index 000000000..22f7b2db1 --- /dev/null +++ b/examples/cosmos/ics23/ics23pbt.qnt @@ -0,0 +1,106 @@ +/// Simple property-based tests for ics23. They happened to be not very useful, +/// as random simulation alone cannot produce even simple examples of sound +/// non-membership proofs. +/// +/// For more advanced property-based testing, see ics23trees.qnt. +/// +/// To execute simple PBT-like tests for 1000 runs of length up to 10 steps +/// in the simulator, type the following: +/// +/// $ quint run --invariant=TestVerify ics23pbt.qnt +/// $ quint run --invariant=TestNonMem ics23pbt.qnt +/// +/// If the simulator finds an example that violates TestVerify or TestNonMem, +/// it displays this counterexample. +/// +/// Igor Konnov, Informal Systems, 2022-2023 +module ics23pbt { + import words.* from "./words" + import ics23.* from "./ics23" + + // an non-membership proof + var nonMemProof: NonExistsProof_T + // a key to test + var inputKey: WORD_T + + // We limit the letters to a very small set, + // including '32' for hash headers. + val Byte = 0.to(3).union(Set(32)) + + val toWord(m) = + m.keys().fold([], (l, i) => l.append(m.get(i))) + + action genKey = + nondet i = Byte.oneOf() + inputKey' = [i] + + action init = all { + genKey, + // we start with leafs in the initial state + nondet lk = Byte.oneOf() + nondet lv = Byte.oneOf() + nondet lp = Byte.oneOf() + nondet rk = Byte.oneOf() + nondet rv = Byte.oneOf() + nondet rp = Byte.oneOf() + nondet pk = Byte.oneOf() + val lproof = { + key: [ lk ], value: [ lv ], + leaf: { prefix: [ lp ] }, path: [] + } + val rproof = { + key: [ rk ], value: [ rv ], leaf: { prefix: [ rp ] }, path: [] + } + nonMemProof' = { key: [ pk ], left: lproof, right: rproof } + } + + def extend(proof, dir, word) = + val node = + if (dir == "turnLeft") { + prefix: word, + suffix: [] + } else { + prefix: word.slice(0, MaxPrefixLen), + suffix: word.slice(MaxPrefixLen, MaxPrefixLen + ChildSize) + } + proof.with("path", proof.path.append(node)) + + /// grow the proof on the left + action growLeft = + nondet dir = Set("turnLeft", "turnRight").oneOf() + nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() + nonMemProof' = + nonMemProof.with("left", nonMemProof.left.extend(dir, toWord(m))) + + /// grow the proof on the right + action growRight = + nondet dir = Set("turnLeft", "turnRight").oneOf() + nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() + nonMemProof' = + nonMemProof.with("right", nonMemProof.right.extend(dir, toWord(m))) + + action step = all { + genKey, + any { + growLeft, + growRight + }, + } + + /// by checking this invariant, we may produce an example of when + /// verifyMembership succeeds + val TestVerify = { + val root = existsCalculate(nonMemProof.left) + not(verifyMembership(root, + nonMemProof.left, inputKey, nonMemProof.left.value)) + } + + /// by checking this invariant, we may produce an example of when + /// verifyNonMembership succeeds + val TestNonMem = or { + lessThan(inputKey, nonMemProof.left.key), + lessThan(nonMemProof.right.key, inputKey), + val root = existsCalculate(nonMemProof.left) + not(verifyNonMembership(root, nonMemProof, inputKey)) + } +} \ No newline at end of file diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt new file mode 100644 index 000000000..d21477483 --- /dev/null +++ b/examples/cosmos/ics23/ics23test.qnt @@ -0,0 +1,133 @@ +/// A few unit tests to improve our understanding of the specification. +/// +/// +/// +/// To execute the unit tests in REPL, type the following: +/// +/// $ quint repl -r ics23test.qnt::ics23test +/// >>> allTests +/// +/// REPL should display 'true'. +/// +/// Igor Konnov, Informal Systems, 2022-2023 +module ics23test { + import ics23.* from "./ics23" + + // test data + val a = [5] + val b = [6] + val c = [7] + val d = [8] + val ab = [5, 6] + val ba = [6, 5] + val abc = [5, 6, 7] + val abcd = [5, 6, 7, 8] + + val allStrings = Set([], a, ab, ba, abc, abcd, [1], [2], [3], [4]) + + pure val existsCalculateTest = { + pure val result = existsCalculate({ + key: [5], + value: [5, 6], + leaf: { prefix: [5, 6, 7] }, + path: [ + { prefix: [5, 6], suffix: [8] }, + { prefix: [5], suffix: [7] } + ] + }) + assert(result == [32, 0, 4]) + } + + pure val isLeftMost1Test = { + assert(isLeftMost([ + { prefix: [1], suffix: [3, 4, 5] }, + { prefix: [2], suffix: [3, 4, 5] }, + { prefix: [3], suffix: [3, 4, 5] } + ])) + } + + pure val isLeftMost2Test = + assert(isLeftMost([ + { prefix: [1, 0, 0, 0], suffix: [] }, + { prefix: [2], suffix: [3, 4, 5] }, + { prefix: [3], suffix: [3, 4, 5] } + ])) + + pure val isLeftMost3Test = { + assert(isLeftMost([ + { prefix: [1], suffix: [3, 4, 5 ] }, + { prefix: [2, 0, 0, 0], suffix: [] }, + { prefix: [3], suffix: [3, 4, 5] } + ])) + } + + pure val isRightMost1Test = + assert(isRightMost([ + { prefix: [1, 4, 5, 6], suffix: [] }, + { prefix: [2, 4, 5, 6], suffix: [] }, + { prefix: [3, 3, 4, 5], suffix: [] } + ])) + + pure val isRightMost2Test = + assert(isRightMost([ + { prefix: [1, 4, 5, 6], suffix: [] }, + { prefix: [2], suffix: [0, 0, 0] }, + { prefix: [3, 3, 4, 5], suffix: [] } + ])) + + pure val isLeftStep1Test = + assert(isLeftStep( + { prefix: [1], suffix: [4, 5, 6] }, + { prefix: [2, 7, 8, 9], suffix: [] } + )) + + pure val isLeftNeighborTest = + assert(isLeftNeighbor( + [ + { prefix: [1], suffix: [4, 5, 6] }, + { prefix: [2, 7, 8, 9], suffix: [] } + ], + [ + { prefix: [1, 4, 5, 6], suffix: [] }, + { prefix: [2, 7, 8, 9], suffix: [] } + ] + )) + + pure val verifyNonMembershipTest = { + // * + // / \ + // 2,3 4,5 + val lhash = existsCalculate({ + key:[2], value: [3], leaf: { prefix: [ 0 ] }, path: [] + }) + val rhash = existsCalculate({ + key:[4], value: [5], leaf: { prefix: [ 0 ] }, path: [] + }) + val left = { + key: [ 2 ], + value: [ 3 ], + leaf: { prefix: [ 0 ] }, + path: [{ prefix: [0], suffix: rhash }] + } + val right = { + key: [ 4 ], + value: [ 5 ], + leaf: { prefix: [ 0 ] }, + path: [{ prefix: [0].concat(lhash), suffix: [] }] + } + val root = [32, 0, 2] + val nilProof = { key: [], value: [], leaf: { prefix: [] }, path: [] } + and { + val np1 = { key: [1], left: nilProof, right: left } + assert(verifyNonMembership(root, np1, [ 1 ])), + val np2 = { key: [2], left: left, right: right } + assert(not(verifyNonMembership(root, np2, [ 2 ]))), + val np3 = { key: [3], left: left, right: right } + assert(verifyNonMembership(root, np3, [ 3 ])), + val np4 = { key: [2], left: left, right: right } + assert(not(verifyNonMembership(root, np4, [ 4 ]))), + val np5 = { key: [5], left: right, right: nilProof } + assert(verifyNonMembership(root, np5, [ 5 ])), + } + } +} \ No newline at end of file diff --git a/examples/cosmos/ics23/ics23trees.qnt b/examples/cosmos/ics23/ics23trees.qnt new file mode 100644 index 000000000..7f00fe2ae --- /dev/null +++ b/examples/cosmos/ics23/ics23trees.qnt @@ -0,0 +1,330 @@ +/// Advanced randomized simulation (a la PBT) by generating +/// random sorted binary trees of small heights over a small set of keys. +/// +/// We specify arbitrary binary trees, whose keys (in the leafs) are sorted. +/// We do not have to specify IAVL+ trees to produce test data for ICS23. +/// Note that this module is needed only for testing of ICS23, +/// not for the operation of ICS23. +/// +/// To execute advanced PBT-like tests for 1000 runs in the simulator, +/// type the following: +/// +/// $ quint run --invariant=NonMemInv ics23trees.qnt +/// $ quint run --invariant=MemInv ics23trees.qnt +/// +/// We expect these tests to always pass. If you the simulator reports +/// a counterexample, there must be an error somewhere. +/// +/// Igor Konnov, Informal Systems, 2022-2023 +module ics23trees { + import words.* from "./words" + import ics23.* from "./ics23" + + /// We represent a binary tree as a collection of maps, + /// whose keys are simply integer values 1..n, with 1 being the root. + /// Similar to pointer-based representations of trees (e.g., in C), + /// this data structure requires additional invariants to make sure + /// that it actually defines a binary tree. + /// This is in contrast to the typical data structures in + /// programming languages. + type TREE_T = { + // every leaf has a key and value assigned + leafs: int -> { key: WORD_T, value: WORD_T }, + // intermediate nodes have left and/or right children + left: int -> int, + right: int -> int + } + + /// the tree generated so far + var tree: TREE_T + /// the node nodeHashes + var nodeHashes: int -> WORD_T + /// the keys to use for non-membership proofs + var leftKey: int + var rightKey: int + /// the key whose non-membership or membership we want to prove + var inputKey: int + + /// limit values to a small set + val Byte = 0.to(7).union(Set(32)) + + /// the maximum tree height + val height = 3 + + /// Compute all parents from the binary representation of the index. + /// To simplify random generation of the trees, we are using + /// the binary encoding. For example, if a leaf has the index 4, + /// that is, 100b, then it has the parents 3 = 10b and 1 = 1b. + def parents(i) = 1.to(height).map(h => i / (2^h)).exclude(Set(0)) + + /// is a given key a node (inner or leaf) of a tree + def isNode(t, key) = or { + key == 1, + t.leafs.keys().contains(key), + t.left.keys().contains(key), + t.right.keys().contains(key), + } + + /// Compute nodeHashes of all nodes into a map. + def computeHashes(t) = { + // compute the hash of a single node, assuming that the children's + // nodeHashes have been computed + def putNodeHash(hashMap, key): (int -> List[int], int) => (int -> List[int]) = { + val h = + if (t.leafs.keys().contains(key)) { + // a leaf + val leaf = t.leafs.get(key) + // Hash the leaf as in ics23.existsCalculate. + // In our trees, prefixes are always 0. + hash([0].append(length(leaf.key)) + .concat(hash(leaf.key)) + .append(length(leaf.value)) + .concat(hash(leaf.value))) + } else { + // an inner node, assuming that the children nodeHashes were computed + def hashOrEmpty(childMap) = + if (childMap.keys().contains(key)) { + hashMap.get(childMap.get(key)) + } else { + EmptyChild + } + // hash the prefix ([0]) and the hash of the children + hash([0].concat(hashOrEmpty(t.left)).concat(hashOrEmpty(t.right))) + } + // store the hash + hashMap.put(key, h) + } + // go over the nodes from max to min + val maxNode = 2^height + 0.range(2^height) + .foldl(Map(), + (m, key) => + if (isNode(t, maxNode - key)) putNodeHash(m, maxNode - key) else m + ) + } + + /// It's very easy to produce binary trees by picking an arbitrary graph and + /// restricting it with the predicate isTree. However, this approach produces + /// very sparse sets of states, to be explored by random search. Hence, we + /// use a more algorithmic approach that represents trees with binary words. + action init = { + // produce an arbitrary tree with leafs in e.g. [2, 8) + nondet idx = 2.to(2^height - 1).powerset().oneOf() + // remove those numbers that should serve as intermediate nodes + val leafKeys = idx.filter(i => idx.forall(j => not(i.in(parents(j))))) + // compute all parents + val allParents = leafKeys.map(i => parents(i)).flatten() + // all intermediate nodes that have a left successor + val leftKeys = allParents.filter(i => + allParents.union(leafKeys).exists(j => 2 * i == j)) + // all intermediate nodes that have a right successor + val rightKeys = allParents.filter(i => + allParents.union(leafKeys).exists(j => 2 * i + 1 == j)) + // left mapping + val left = leftKeys.mapBy(i => 2 * i) + // right mapping + val right = rightKeys.mapBy(i => 2 * i + 1) + all { + // assign values to the keys + nondet vs = leafKeys.setOfMaps(Byte).oneOf() + val leafs = vs.keys().mapBy(k => { key: [k], value: [vs.get(k)] }) + // the resulting tree + val t = { leafs: leafs, left: left, right: right } + all { + tree' = t, + nodeHashes' = computeHashes(t), + }, + // pick arbitrary left and right keys for non-membership proofs + nondet i = leafKeys.oneOf() + leftKey' = i, + nondet i = leafKeys.oneOf() + rightKey' = i, + // pick an arbitrary input key + nondet i = Byte.oneOf() + inputKey' = i + } + } + + /// convert a tree leaf to an exists proof + def leafToExistsProof(key) = + val value = tree.leafs.get(key).value + // encode all intermediate nodes upwards + val path = range(1, height + 1) + .foldl([], + (p, h) => + if (key < 2^h) { + p + } else { + val parent = key / (2^h) + def hashOrChild(childMap) = + if (childMap.keys().contains(parent)) { + nodeHashes.get(childMap.get(parent)) + } else { + EmptyChild + } + // depending on whether the node is going to left or right, + // push the hashes in the prefix and the suffix + if (key == 2 * parent) { + val right = hashOrChild(tree.right) + p.append({ prefix: [0], suffix: right }) + } else { + val left = hashOrChild(tree.left) + p.append({ prefix: [0].concat(left), suffix: [] }) + } + } + ) + // return the exists proof, where the key is the index itself + { + key: [key], + value: tree.leafs.get(key).value, + leaf: { prefix: [0] }, + path: path, + } + + /// The transition does nothing. The state was computed in Init. + action step = all { + // nothing changes + tree' = tree, + nodeHashes' = nodeHashes, + leftKey' = leftKey, + rightKey' = rightKey, + inputKey' = inputKey, + } + + /// make sure that the proofs are the same for all the leafs + val TreeProofInv = + and { + leftKey.in(tree.leafs.keys()), + rightKey.in(tree.leafs.keys()) + } implies { + val lroot = existsCalculate(leafToExistsProof(leftKey)) + val rroot = existsCalculate(leafToExistsProof(rightKey)) + lroot == rroot + } + + /// The invariant of membership verification: + /// If the input key belongs to the leafs, + /// we should be able to prove its membership. + val MemInv = or { + not(inputKey.in(tree.leafs.keys())), + val proof = leafToExistsProof(inputKey) + val root = existsCalculate(proof) + verifyMembership(root, proof, [inputKey], proof.value) + } + + /// check this property to produce an example of where MemInv is violated + val MemExample = + not(MemInv) + + // A few lemmas for NonMemInv: + // MemberShouldFalsify, NonMemberInTheMiddle, NonMemberLeft, NonMemberRight + + def MemberShouldFalsify(lproof, rproof) = and { + // if the input key belongs to the leafs, + // we should not be able to disprove its membership + inputKey.in(tree.leafs.keys()), + val nproof = { key: [inputKey], left: lproof, right: rproof } + val root = existsCalculate(lproof) + not(verifyNonMembership(root, nproof, [inputKey])) + } + + def NonMemberInTheMiddle(lproof, rproof) = and { + // we should be able to prove its non-membership, + // unless the choice of the keys is bad + not(inputKey.in(tree.leafs.keys())), + val nproof = { key: [inputKey], left: lproof, right: rproof } + val root = existsCalculate(lproof) + val noKeyInTheMiddle = and { + // there is no leaf between leftKey and rightKey + tree.leafs.keys().forall(k => k <= leftKey or k >= rightKey), + // the keys are not misplaced + leftKey < inputKey, + inputKey < rightKey, + } + noKeyInTheMiddle iff verifyNonMembership(root, nproof, [inputKey]) + } + + def NonMemberLeft(lproof, rproof) = and { + // the input key is to the left + isNil(lproof.key), + // non-membership is true when the right key is left-most + and { + tree.leafs.keys().forall(k => rightKey <= k), + inputKey < rightKey, + } iff and { + // or there is a proof + val root = existsCalculate(rproof) + val nproof = { key: [inputKey], left: lproof, right: rproof } + verifyNonMembership(root, nproof, [inputKey]) + } + } + + def NonMemberRight(lproof, rproof) = and { + // the input key is to the right + isNil(rproof.key), + // non-membership is true when the left key is the right-most + and { + tree.leafs.keys().forall(k => (k <= leftKey)), + inputKey > leftKey, + } iff and { + // or there is a proof + val root = existsCalculate(lproof) + val nproof = { key: [inputKey], left: lproof, right: rproof } + verifyNonMembership(root, nproof, [inputKey]) + } + } + + // The invariant of non-membership verification. + // Consider all possible positions of the input key and the left/right keys. + val NonMemInv = + def proofOrNil(key) = { + if (tree.leafs.keys().contains(key)) + leafToExistsProof(key) + else + { key: [], value: [], leaf: { prefix: [] }, path: [] } + } + val lproof = proofOrNil(leftKey) + val rproof = proofOrNil(rightKey) + or { + MemberShouldFalsify(lproof, rproof), + NonMemberInTheMiddle(lproof, rproof), + NonMemberLeft(lproof, rproof), + NonMemberRight(lproof, rproof), + // trivial cases: + inputKey < rightKey and not(isNil(lproof.key)), + inputKey > leftKey and not(isNil(rproof.key)), + } + + /// check this property to produce an example of where NonMemInv is violated + val NonMemExample = + not(NonMemInv) + + /// Predicate isTree(t) is true iff t defines an ordered binary tree starting + /// with 1. It's probably hard to read. However, it is what one has to specify + /// to express that an arbitrary graph is an ordered tree. + def isTree(t: TREE_T): bool = and { + t.leafs.keys().intersect(t.left.keys()) == Set(), + t.leafs.keys().intersect(t.right.keys()) == Set(), + 1.in(t.leafs.keys().union(t.left.keys().union(t.right.keys()))), + // we impose an order on the keys, to break cycles and DAGs + t.left.keys().forall(k => t.left.get(k) > k), + t.right.keys().forall(k => t.right.get(k) > k), + t.left.keys().intersect(t.right.keys()) + .forall(k => t.left.get(k) < t.right.get(k)), + // the leafs are ordered w.r.t. their keys + val leafKeys = t.leafs.keys() + tuples(leafKeys, leafKeys).forall(kk => + kk._1 < kk._2 implies lessThan(t.leafs.get(kk._1).key, t.leafs.get(kk._2).key) + ), + // all nodes have a parent + (t.leafs.keys().union(t.left.keys()).union(t.right.keys())) + .forall(k => or { + // the root + k == 1, + // there is a left parent + t.left.keys().exists(p => t.left.get(p) == k), + // there is a right parent + t.right.keys().exists(p => t.right.get(p) == k), + }), + } +} \ No newline at end of file diff --git a/examples/cosmos/ics23/ics23.tla b/examples/cosmos/ics23/tla/ics23.tla similarity index 100% rename from examples/cosmos/ics23/ics23.tla rename to examples/cosmos/ics23/tla/ics23.tla diff --git a/examples/cosmos/ics23/ics23pbt.tla b/examples/cosmos/ics23/tla/ics23pbt.tla similarity index 100% rename from examples/cosmos/ics23/ics23pbt.tla rename to examples/cosmos/ics23/tla/ics23pbt.tla diff --git a/examples/cosmos/ics23/ics23trees.tla b/examples/cosmos/ics23/tla/ics23trees.tla similarity index 100% rename from examples/cosmos/ics23/ics23trees.tla rename to examples/cosmos/ics23/tla/ics23trees.tla diff --git a/examples/cosmos/ics23/words.qnt b/examples/cosmos/ics23/words.qnt new file mode 100644 index 000000000..4a6490593 --- /dev/null +++ b/examples/cosmos/ics23/words.qnt @@ -0,0 +1,26 @@ +/// A minimal specification of words as lists of integers. +/// +/// Igor Konnov, Informal Systems, 2022-2023 +module words { + /// We represent byte sequences as lists of integers + type WORD_T = List[int] + + /// we interpret the empty word as nil + def isNil(word) = length(word) == 0 + + /// compare two integer words lexicographically + def lessThan(w1, w2) = { + val len1 = length(w1) + val len2 = length(w2) + or { + len1 < len2 and w1.indices().forall(i => w1[i] == w2[i]), + and { + len1 == len2, + w1.indices().exists(i => and { + w1[i] < w2[i], + w1.indices().forall(j => j < i implies w1[i] == w2[j]) + }) + } + } + } +} From 52419f0da4e0ab4d3fcde60f7c0dc1712488e281 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 17:15:49 +0200 Subject: [PATCH 02/24] ignore empty leaf keys --- examples/cosmos/ics23/ics23trees.qnt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/cosmos/ics23/ics23trees.qnt b/examples/cosmos/ics23/ics23trees.qnt index 7f00fe2ae..6a6bde23f 100644 --- a/examples/cosmos/ics23/ics23trees.qnt +++ b/examples/cosmos/ics23/ics23trees.qnt @@ -125,6 +125,8 @@ module ics23trees { // right mapping val right = rightKeys.mapBy(i => 2 * i + 1) all { + // ignore the case of empty trees + leafKeys != Set(), // assign values to the keys nondet vs = leafKeys.setOfMaps(Byte).oneOf() val leafs = vs.keys().mapBy(k => { key: [k], value: [vs.get(k)] }) From aa20aba43618128881dea43cf9742af2ce011c31 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 17:37:28 +0200 Subject: [PATCH 03/24] lowcase definitions and remove isTree --- examples/cosmos/ics23/ics23trees.qnt | 68 +++++++--------------------- 1 file changed, 17 insertions(+), 51 deletions(-) diff --git a/examples/cosmos/ics23/ics23trees.qnt b/examples/cosmos/ics23/ics23trees.qnt index 6a6bde23f..3b97e3dc8 100644 --- a/examples/cosmos/ics23/ics23trees.qnt +++ b/examples/cosmos/ics23/ics23trees.qnt @@ -9,8 +9,8 @@ /// To execute advanced PBT-like tests for 1000 runs in the simulator, /// type the following: /// -/// $ quint run --invariant=NonMemInv ics23trees.qnt -/// $ quint run --invariant=MemInv ics23trees.qnt +/// $ quint run --invariant=nonMemInv ics23trees.qnt +/// $ quint run --invariant=memInv ics23trees.qnt /// /// We expect these tests to always pass. If you the simulator reports /// a counterexample, there must be an error somewhere. @@ -103,10 +103,7 @@ module ics23trees { ) } - /// It's very easy to produce binary trees by picking an arbitrary graph and - /// restricting it with the predicate isTree. However, this approach produces - /// very sparse sets of states, to be explored by random search. Hence, we - /// use a more algorithmic approach that represents trees with binary words. + /// We use an algorithmic approach that represents trees with binary words. action init = { // produce an arbitrary tree with leafs in e.g. [2, 8) nondet idx = 2.to(2^height - 1).powerset().oneOf() @@ -194,7 +191,7 @@ module ics23trees { } /// make sure that the proofs are the same for all the leafs - val TreeProofInv = + val treeProofInv = and { leftKey.in(tree.leafs.keys()), rightKey.in(tree.leafs.keys()) @@ -207,7 +204,7 @@ module ics23trees { /// The invariant of membership verification: /// If the input key belongs to the leafs, /// we should be able to prove its membership. - val MemInv = or { + val memInv = or { not(inputKey.in(tree.leafs.keys())), val proof = leafToExistsProof(inputKey) val root = existsCalculate(proof) @@ -215,13 +212,12 @@ module ics23trees { } /// check this property to produce an example of where MemInv is violated - val MemExample = - not(MemInv) + val memExample = not(memInv) // A few lemmas for NonMemInv: - // MemberShouldFalsify, NonMemberInTheMiddle, NonMemberLeft, NonMemberRight + // memberShouldFalsify, nonMemberInTheMiddle, nonMemberLeft, nonMemberRight - def MemberShouldFalsify(lproof, rproof) = and { + def memberShouldFalsify(lproof, rproof) = and { // if the input key belongs to the leafs, // we should not be able to disprove its membership inputKey.in(tree.leafs.keys()), @@ -230,7 +226,7 @@ module ics23trees { not(verifyNonMembership(root, nproof, [inputKey])) } - def NonMemberInTheMiddle(lproof, rproof) = and { + def nonMemberInTheMiddle(lproof, rproof) = and { // we should be able to prove its non-membership, // unless the choice of the keys is bad not(inputKey.in(tree.leafs.keys())), @@ -246,7 +242,7 @@ module ics23trees { noKeyInTheMiddle iff verifyNonMembership(root, nproof, [inputKey]) } - def NonMemberLeft(lproof, rproof) = and { + def nonMemberLeft(lproof, rproof) = and { // the input key is to the left isNil(lproof.key), // non-membership is true when the right key is left-most @@ -261,7 +257,7 @@ module ics23trees { } } - def NonMemberRight(lproof, rproof) = and { + def nonMemberRight(lproof, rproof) = and { // the input key is to the right isNil(rproof.key), // non-membership is true when the left key is the right-most @@ -278,7 +274,7 @@ module ics23trees { // The invariant of non-membership verification. // Consider all possible positions of the input key and the left/right keys. - val NonMemInv = + val nonMemInv = def proofOrNil(key) = { if (tree.leafs.keys().contains(key)) leafToExistsProof(key) @@ -288,45 +284,15 @@ module ics23trees { val lproof = proofOrNil(leftKey) val rproof = proofOrNil(rightKey) or { - MemberShouldFalsify(lproof, rproof), - NonMemberInTheMiddle(lproof, rproof), - NonMemberLeft(lproof, rproof), - NonMemberRight(lproof, rproof), + memberShouldFalsify(lproof, rproof), + nonMemberInTheMiddle(lproof, rproof), + nonMemberLeft(lproof, rproof), + nonMemberRight(lproof, rproof), // trivial cases: inputKey < rightKey and not(isNil(lproof.key)), inputKey > leftKey and not(isNil(rproof.key)), } /// check this property to produce an example of where NonMemInv is violated - val NonMemExample = - not(NonMemInv) - - /// Predicate isTree(t) is true iff t defines an ordered binary tree starting - /// with 1. It's probably hard to read. However, it is what one has to specify - /// to express that an arbitrary graph is an ordered tree. - def isTree(t: TREE_T): bool = and { - t.leafs.keys().intersect(t.left.keys()) == Set(), - t.leafs.keys().intersect(t.right.keys()) == Set(), - 1.in(t.leafs.keys().union(t.left.keys().union(t.right.keys()))), - // we impose an order on the keys, to break cycles and DAGs - t.left.keys().forall(k => t.left.get(k) > k), - t.right.keys().forall(k => t.right.get(k) > k), - t.left.keys().intersect(t.right.keys()) - .forall(k => t.left.get(k) < t.right.get(k)), - // the leafs are ordered w.r.t. their keys - val leafKeys = t.leafs.keys() - tuples(leafKeys, leafKeys).forall(kk => - kk._1 < kk._2 implies lessThan(t.leafs.get(kk._1).key, t.leafs.get(kk._2).key) - ), - // all nodes have a parent - (t.leafs.keys().union(t.left.keys()).union(t.right.keys())) - .forall(k => or { - // the root - k == 1, - // there is a left parent - t.left.keys().exists(p => t.left.get(p) == k), - // there is a right parent - t.right.keys().exists(p => t.right.get(p) == k), - }), - } + val nonMemExample = not(nonMemInv) } \ No newline at end of file From 446f4d3e91f59ac11cd8dbc94dbc91ae2274dd45 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 17:40:24 +0200 Subject: [PATCH 04/24] clean up the specs --- examples/cosmos/ics23/ics23pbt.qnt | 8 ++++---- examples/cosmos/ics23/ics23test.qnt | 9 ++------- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/examples/cosmos/ics23/ics23pbt.qnt b/examples/cosmos/ics23/ics23pbt.qnt index 22f7b2db1..c6d6de478 100644 --- a/examples/cosmos/ics23/ics23pbt.qnt +++ b/examples/cosmos/ics23/ics23pbt.qnt @@ -7,8 +7,8 @@ /// To execute simple PBT-like tests for 1000 runs of length up to 10 steps /// in the simulator, type the following: /// -/// $ quint run --invariant=TestVerify ics23pbt.qnt -/// $ quint run --invariant=TestNonMem ics23pbt.qnt +/// $ quint run --invariant=noVerifyInv ics23pbt.qnt +/// $ quint run --invariant=noNonMemInv ics23pbt.qnt /// /// If the simulator finds an example that violates TestVerify or TestNonMem, /// it displays this counterexample. @@ -89,7 +89,7 @@ module ics23pbt { /// by checking this invariant, we may produce an example of when /// verifyMembership succeeds - val TestVerify = { + val noVerifyInv = { val root = existsCalculate(nonMemProof.left) not(verifyMembership(root, nonMemProof.left, inputKey, nonMemProof.left.value)) @@ -97,7 +97,7 @@ module ics23pbt { /// by checking this invariant, we may produce an example of when /// verifyNonMembership succeeds - val TestNonMem = or { + val noNonMemInv = or { lessThan(inputKey, nonMemProof.left.key), lessThan(nonMemProof.right.key, inputKey), val root = existsCalculate(nonMemProof.left) diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index d21477483..55b2e235d 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -1,13 +1,8 @@ /// A few unit tests to improve our understanding of the specification. /// +/// To execute the unit tests, type the following: /// -/// -/// To execute the unit tests in REPL, type the following: -/// -/// $ quint repl -r ics23test.qnt::ics23test -/// >>> allTests -/// -/// REPL should display 'true'. +/// $ quint test ics23test.qnt /// /// Igor Konnov, Informal Systems, 2022-2023 module ics23test { From bbf3f440b783425810f83bde836f076a12b2c74d Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 18:42:11 +0200 Subject: [PATCH 05/24] fix the test --- examples/cosmos/ics23/ics23.qnt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index b6c906fc1..2456aeef5 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -76,11 +76,12 @@ module ics23 { /// calculate a hash from an exists proof def existsCalculate(p): (ExistsProof_T) => CommitmentProof_T = { - // this is how the leaf hash is computed + // This is how the leaf hash is computed. + // Notice that the key is not hashed. val leafHash = hash(p.leaf.prefix .append(length(p.key)) - .concat(hash(p.key)) + .concat(p.key) .append(length(p.value)) .concat(hash(p.value))) From c13f25621df56d23d060bb44764f57df022513d2 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Tue, 20 Jun 2023 22:05:42 +0200 Subject: [PATCH 06/24] symbolic hashing --- examples/cosmos/ics23/words.qnt | 107 ++++++++++++++++++++++++++++---- 1 file changed, 96 insertions(+), 11 deletions(-) diff --git a/examples/cosmos/ics23/words.qnt b/examples/cosmos/ics23/words.qnt index 4a6490593..45148b5ae 100644 --- a/examples/cosmos/ics23/words.qnt +++ b/examples/cosmos/ics23/words.qnt @@ -1,17 +1,41 @@ -/// A minimal specification of words as lists of integers. +/// A symbolic specification of a string that is suitable for reasoning about +/// strings and hashes (such as SHA256). The exact hash function is irrelevant. +/// The only assumption is that a hash is irreversible. +/// +/// Similar to symbolic reasoning by Dolev and Yao, we would like to represent: +/// - a raw sequence of bytes, e.g., [ 1, 2, 3 ], +/// - a hashed sequence, e.g., h([ 1, 2, 3 ]), +/// - a concatenation of a raw sequence and a hash (in any order), +/// e.g., [ 1, 2 ] + h([ 3, 4 ])], +/// - nested hashes, e.g., h([ 1, 2 ] + h([ 3, 4 ])). +/// +/// So the idea is basically to represent words as terms, where the atoms are +/// sequences of integers, and terms are constructed as n-ary applications +/// of the symbol "h", which means "hash". Since Quint enforces strict typing +/// and it does not allow for inductive (recursive) algebraic data types, +/// we represent terms as maps that encode trees. For instance, +/// the term h([ 1, 2 ] + h([ 3, 4 ])) + [ 5, 6 ] corresponds to the tree: +/// +/// "h" [ 5, 6 ] +/// / \ +/// [ 1, 2 ] "h" +/// / +/// [ 3, 4 ] +/// +/// The above tree is represented as a map in Quint: +/// +/// Map([ 0 ] -> { t: "h", b: [] }, +/// [ 0, 0 ] -> { t: "r", b: [ 1, 2 ] }, +/// [ 0, 1 ] -> { t: "h", b: [] } ), +/// [ 0, 1, 0 ] -> { t: "r", b: [ 3, 4 ] }, +/// [ 1 ] -> { t: "r", b: [ 5, 6 ] }) /// /// Igor Konnov, Informal Systems, 2022-2023 module words { - /// We represent byte sequences as lists of integers - type WORD_T = List[int] - - /// we interpret the empty word as nil - def isNil(word) = length(word) == 0 - - /// compare two integer words lexicographically - def lessThan(w1, w2) = { - val len1 = length(w1) - val len2 = length(w2) + /// compare two lists of integers (e.g., bytes) lexicographically + pure def lessThan(w1: List[int], w2: List[int]): bool = { + pure val len1 = length(w1) + pure val len2 = length(w2) or { len1 < len2 and w1.indices().forall(i => w1[i] == w2[i]), and { @@ -23,4 +47,65 @@ module words { } } } + + /// A tree node that represents a fragment of a term + type TERM_NODE_T = { + // node type: either "h" (for hash), or "r" (for raw sequence) + t: str, + // the bytes when t = "r", and [] when t = "h" + b: List[int] + } + + /// A word is a map from a path to the term node. + /// The first root's child is [ 0 ], the second root's child is [ 1 ], + /// the first child of [ 0 ] is [ 0, 0], etc. + type TERM_T = List[int] -> TERM_NODE_T + + // Construct the term that encodes a raw sequence of bytes + pure def raw(bytes: List[int]): TERM_T = { + Map([ 0 ] -> { t: "r", b: bytes }) + } + + /// Does the term represent the empty raw sequence of bytes + pure def isNil(term: TERM_T): bool = { + term == Map([ 0 ] -> { t: "r", b: [] }) + } + + // Hash a term + pure def hash(term: TERM_T): TERM_T = { + // add "h" on top, which has the key [ 0 ], and attach term to it + pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) + paths.mapBy(p => + if (p == [ 0 ]) { + { t: "h", b: [] } + } else { + term.get(p.slice(1, length(p))) + } + ) + } + + /// Concatenate two terms. Special attention is paid to the case when the + /// both terms are raw sequences, which requires them to be merged. + pure def plus(left: TERM_T, right: TERM_T): TERM_T = { + pure val l = left.get([0]) + pure val r = right.get([0]) + if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") { + Map([0] -> { t: "r", b: l.b.concat(r.b) }) + } else { + // the number of root's children in the left term + pure val lwidth = size(keys(left).filter(p => length(p) == 1)) + // the paths of the right term shifted to the right by lwidth + pure val rshifted = + keys(right).map(p => [ lwidth + p[0] ].concat(p.slice(1, length(p)))) + // the paths of the concatenation + pure val paths = keys(left).union(rshifted) + paths.mapBy(p => + if (p[0] < lwidth) { + left.get(p) + } else { + right.get( [ p[0] - lwidth ].concat(p.slice(1, length(p)))) + } + ) + } + } } From 33bc57d909de4a222a90c55f90e84a998921df37 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 21 Jun 2023 12:28:44 +0200 Subject: [PATCH 07/24] fix the comments --- examples/cosmos/ics23/words.qnt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/examples/cosmos/ics23/words.qnt b/examples/cosmos/ics23/words.qnt index 45148b5ae..2f1e97da9 100644 --- a/examples/cosmos/ics23/words.qnt +++ b/examples/cosmos/ics23/words.qnt @@ -12,7 +12,7 @@ /// So the idea is basically to represent words as terms, where the atoms are /// sequences of integers, and terms are constructed as n-ary applications /// of the symbol "h", which means "hash". Since Quint enforces strict typing -/// and it does not allow for inductive (recursive) algebraic data types, +/// and it does not allow for inductive/recursive algebraic data types, /// we represent terms as maps that encode trees. For instance, /// the term h([ 1, 2 ] + h([ 3, 4 ])) + [ 5, 6 ] corresponds to the tree: /// @@ -90,15 +90,18 @@ module words { pure val l = left.get([0]) pure val r = right.get([0]) if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") { + // both arguments are raw sequences, produce a single raw sequence Map([0] -> { t: "r", b: l.b.concat(r.b) }) } else { - // the number of root's children in the left term + // Merge the arguments as trees representing terms. + // The number of root's children in the left term: pure val lwidth = size(keys(left).filter(p => length(p) == 1)) // the paths of the right term shifted to the right by lwidth pure val rshifted = keys(right).map(p => [ lwidth + p[0] ].concat(p.slice(1, length(p)))) // the paths of the concatenation pure val paths = keys(left).union(rshifted) + // the resulting term as a map paths.mapBy(p => if (p[0] < lwidth) { left.get(p) From 8534b5e6acfeed6e334132385fbca6c31bb6f4c2 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 21 Jun 2023 12:29:39 +0200 Subject: [PATCH 08/24] rename words to hashes --- examples/cosmos/ics23/{words.qnt => hashes.qnt} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename examples/cosmos/ics23/{words.qnt => hashes.qnt} (100%) diff --git a/examples/cosmos/ics23/words.qnt b/examples/cosmos/ics23/hashes.qnt similarity index 100% rename from examples/cosmos/ics23/words.qnt rename to examples/cosmos/ics23/hashes.qnt From 89f15591b93351c4e30e01378ae569b1673b020c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 21 Jun 2023 15:36:38 +0200 Subject: [PATCH 09/24] refactoring the spec --- examples/cosmos/ics23/hashes.qnt | 37 ++++++++++--- examples/cosmos/ics23/ics23.qnt | 92 ++++++++++++++++---------------- 2 files changed, 76 insertions(+), 53 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 2f1e97da9..3e7565dda 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -31,9 +31,12 @@ /// [ 1 ] -> { t: "r", b: [ 5, 6 ] }) /// /// Igor Konnov, Informal Systems, 2022-2023 -module words { +module hashes { + /// A sequence of bytes is simply a list of integers + type BYTES_T = List[int] + /// compare two lists of integers (e.g., bytes) lexicographically - pure def lessThan(w1: List[int], w2: List[int]): bool = { + pure def lessThan(w1: BYTES_T, w2: BYTES_T): bool = { pure val len1 = length(w1) pure val len2 = length(w2) or { @@ -53,16 +56,25 @@ module words { // node type: either "h" (for hash), or "r" (for raw sequence) t: str, // the bytes when t = "r", and [] when t = "h" - b: List[int] + b: BYTES_T } /// A word is a map from a path to the term node. /// The first root's child is [ 0 ], the second root's child is [ 1 ], /// the first child of [ 0 ] is [ 0, 0], etc. - type TERM_T = List[int] -> TERM_NODE_T + type TERM_T = BYTES_T -> TERM_NODE_T + + /// Compute term length in bytes, + /// assuming that a hash occupies 32 bytes (as SHA256 does) + pure def termLen(term: TERM_T): int = { + // the root's children + pure val top = + keys(term).filter(p => length(p) == 1).map(p => term.get(p)) + top.fold(0, (s, t) => if (t.t == "h") s + 32 else s + length(t.b)) + } // Construct the term that encodes a raw sequence of bytes - pure def raw(bytes: List[int]): TERM_T = { + pure def raw(bytes: BYTES_T): TERM_T = { Map([ 0 ] -> { t: "r", b: bytes }) } @@ -72,7 +84,7 @@ module words { } // Hash a term - pure def hash(term: TERM_T): TERM_T = { + pure def termHash(term: TERM_T): TERM_T = { // add "h" on top, which has the key [ 0 ], and attach term to it pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) paths.mapBy(p => @@ -86,7 +98,7 @@ module words { /// Concatenate two terms. Special attention is paid to the case when the /// both terms are raw sequences, which requires them to be merged. - pure def plus(left: TERM_T, right: TERM_T): TERM_T = { + pure def termConcat(left: TERM_T, right: TERM_T): TERM_T = { pure val l = left.get([0]) pure val r = right.get([0]) if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") { @@ -111,4 +123,15 @@ module words { ) } } + + // Slice the sequence represented by a term. + // We only slice raw sequences. + pure def termSlice(term: TERM_T, start: int, end: int): TERM_T = { + pure val first = term.get([ 0 ]) + if (size(keys(term)) == 1 and first.t == "r") { + raw(first.b.slice(start, end)) + } else { + term + } + } } diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index 2456aeef5..2717c263c 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -18,17 +18,17 @@ // // https://github.com/confio/ics23/blob/master/go/proof.go module ics23 { - import words.* from "./words" + import hashes.* from "./hashes" // ICS23 proof checking for IavlSpec. - // In contrast to the ICS32 implementation, we specialize it to binary trees: + // In contrast to the ICS23 implementation, we specialize it to binary trees: // https://github.com/confio/ics23/tree/master/go // type aliases for readability - type KEY_T = WORD_T - type VALUE_T = WORD_T - type CommitmentRoot_T = WORD_T - type CommitmentProof_T = WORD_T + type KEY_T = TERM_T + type VALUE_T = TERM_T + type CommitmentRoot_T = TERM_T + type CommitmentProof_T = TERM_T // ICS23 IavlSpec has: // MinPrefixLength = 4 @@ -36,31 +36,29 @@ module ics23 { // ChildSize = 33 // // To ease spec testing, we set: - val MinPrefixLen = 1 - val MaxPrefixLen = 2 + pure val MinPrefixLen = 1 + pure val MaxPrefixLen = 2 // It is crucial to make sure that ChildSize > MaxPrefixLen - val ChildSize = 3 // with length byte + pure val ChildSize = 33 // 32 bytes in SHA256 + 1 byte for length // Empty child is a predefined sequence that fills an absent child. - val EmptyChild = [ 0, 0, 0 ] - - /// We need a hash that returns ChildSize elements, - /// with 32 being in the head. - /// For simulation, we are just summing up the word elements modulo 8. - /// For verification, we should use an injective function as a perfect hash. - def hash(word) = [ 32, 0, word.foldl(0, (i, j) => i + j) % 8 ] + // TODO: EmptyChild is set to nil in IavlSpec. We have 33 bytes. + pure val EmptyChild = raw([ + 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 + ]) type LEAF_T = { // The implementation additionally stores hashing and length functions: // hash, prehashKey, prehashValue, len. Since we fix the spec to IAVL, // we do not have to carry them around. - prefix: WORD_T + prefix: TERM_T } type INNER_T = { // The implementation additionally stores the hashing function. // Since we fix the spec to IAVL, we do not have to carry it around. - prefix: WORD_T, - suffix: WORD_T + prefix: TERM_T, + suffix: TERM_T } /// a proof of existence of (key, value) @@ -74,20 +72,21 @@ module ics23 { } /// calculate a hash from an exists proof - def existsCalculate(p): - (ExistsProof_T) => CommitmentProof_T = { + def existsCalculate(p: ExistsProof_T): CommitmentProof_T = { // This is how the leaf hash is computed. // Notice that the key is not hashed. val leafHash = - hash(p.leaf.prefix - .append(length(p.key)) - .concat(p.key) - .append(length(p.value)) - .concat(hash(p.value))) + termHash(p.leaf.prefix + // TODO: use encodeVarintProto + .termConcat(raw([termLen(p.key)])) + .termConcat(p.key) + .termConcat(raw([32])) + .termConcat(termHash(p.value))) // the inner node nodeHashes are concatenated and hashed upwards p.path.foldl(leafHash, - (child, inner) => hash(inner.prefix.concat(child).concat(inner.suffix))) + (child, inner) => + termHash(inner.prefix.termConcat(child).termConcat(inner.suffix))) } /// verify that a proof matches a root @@ -101,8 +100,8 @@ module ics23 { /// proof is an ExistenceProof for the given key and value AND /// calculating the root for the ExistenceProof matches /// the provided CommitmentRoot - def verifyMembership(root, proof, key, value): - (CommitmentRoot_T, ExistsProof_T, KEY_T, VALUE_T) => bool = { + def verifyMembership(root: CommitmentRoot_T, + proof: ExistsProof_T, key: KEY_T, value: VALUE_T): bool = { // TODO: specify Decompress // TODO: specify the case of CommitmentProof_Batch // TODO: CheckAgainstSpec ensures that the proof can be verified @@ -111,20 +110,21 @@ module ics23 { } /// checks if an op has the expected padding - def hasPadding(inner, minPrefixLen, maxPrefixLen, suffixLen) = and { - length(inner.prefix) >= minPrefixLen, - length(inner.prefix) <= maxPrefixLen, + def hasPadding(inner: INNER_T, + minPrefixLen: int, maxPrefixLen: int, suffixLen: int): bool = and { + termLen(inner.prefix) >= minPrefixLen, + termLen(inner.prefix) <= maxPrefixLen, // When inner turns left, suffixLen == ChildSize, // that is, we store the hash of the right child in the suffix. // When inner turns right, suffixLen == 0, // that is, we store the hash of the left child in the prefix. - length(inner.suffix) == suffixLen + termLen(inner.suffix) == suffixLen } /// This will look at the proof and determine which order it is... /// So we can see if it is branch 0, 1, 2 etc... to determine neighbors /// https://github.com/confio/ics23/blob/a4daeb4c24ce1be827829c0841446abc690c4f11/go/proof.go#L400-L411 - def orderFromPadding(inner) = { + def orderFromPadding(inner: INNER_T): (int, bool) = { // Specialize orderFromPadding to IavlSpec: // ChildOrder = { 0, 1 } // branch = 0: minp, maxp, suffix = MinPrefixLen, MaxPrefixLen, ChildSize @@ -146,21 +146,21 @@ module ics23 { /// leftBranchesAreEmpty returns true if the padding bytes correspond to all /// empty siblings on the left side of a branch, ie. it's a valid placeholder /// on a leftmost path - def leftBranchesAreEmpty(inner) = and { + def leftBranchesAreEmpty(inner: INNER_T): bool = and { // the case of leftBranches == 0 returns false val order = orderFromPadding(inner) order._2 and order._1 != 0, // the remaining case is leftBranches == 1, see orderFromPadding // actualPrefix = len(inner.prefix) - 33 - length(inner.prefix) >= ChildSize, + termLen(inner.prefix) >= ChildSize, // getPosition(0) returns 0 - val fromIndex = length(inner.prefix) - ChildSize - inner.prefix.slice(fromIndex, fromIndex + ChildSize) == EmptyChild + val fromIndex = termLen(inner.prefix) - ChildSize + termSlice(inner.prefix, fromIndex, fromIndex + ChildSize) == EmptyChild } /// IsLeftMost returns true if this is the left-most path in the tree, /// excluding placeholder (empty child) nodes - def isLeftMost(path) = { + def isLeftMost(path: List[INNER_T]): bool = { // Calls getPadding(0) => idx = 0, prefix = 0. // We specialize the constants to IavlSpec. path.indices().forall(i => @@ -177,19 +177,19 @@ module ics23 { /// rightBranchesAreEmpty returns true if the padding bytes correspond /// to all empty siblings on the right side of a branch, /// i.e. it's a valid placeholder on a rightmost path - def rightBranchesAreEmpty(inner) = and { + def rightBranchesAreEmpty(inner: INNER_T): bool = and { // the case of rightBranches == 0 returns false val order = orderFromPadding(inner) order._2 and order._1 != 1, // the remaining case is rightBranches == 1, see orderFromPadding - length(inner.suffix) == ChildSize, + termLen(inner.suffix) == ChildSize, // getPosition(0) returns 0, hence, from == 0 inner.suffix == EmptyChild } /// IsRightMost returns true if this is the left-most path in the tree, /// excluding placeholder (empty child) nodes - def isRightMost(path) = { + def isRightMost(path: List[INNER_T]): bool = { // Specialize to IavlSpec // Calls getPadding(1) => minPrefix, maxPrefix, // suffix = ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 @@ -206,7 +206,7 @@ module ics23 { /// isLeftStep assumes left and right have common parents /// checks if left is exactly one slot to the left of right - def isLeftStep(left, right) = { + def isLeftStep(left: INNER_T, right: INNER_T): bool = { // 'left' turns left, and 'right' turns right val lorder = orderFromPadding(left) val rorder = orderFromPadding(right) @@ -225,7 +225,7 @@ module ics23 { /// Validate that LPath[len-1] is the left neighbor of RPath[len-1]. /// For step in LPath[0..len-1], validate step is right-most node. /// For step in RPath[0..len-1], validate step is left-most node. - def isLeftNeighbor(lpath, rpath) = { + def isLeftNeighbor(lpath: List[INNER_T], rpath: List[INNER_T]): bool = { // count common tail (from end, near root) // cut the left and right paths lpath.indices().exists(li => @@ -264,8 +264,8 @@ module ics23 { /// both left and right sub-proofs are valid existence proofs (see above) or nil /// left and right proofs are neighbors (or left/right most if one is nil) /// provided key is between the keys of the two proofs - def verifyNonMembership(root, np, key): - (CommitmentRoot_T, NonExistsProof_T, KEY_T) => bool = and { + def verifyNonMembership(root: CommitmentRoot_T, + np: NonExistsProof_T, key: KEY_T): bool = and { // getNonExistProofForKey isNil(np.left.key) or lessThan(np.left.key, key), isNil(np.right.key) or lessThan(key, np.right.key), From 99c6fe781d53104a83695dcdc04586437a80b134 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 22 Jun 2023 14:46:37 +0200 Subject: [PATCH 10/24] refactored hashes, ics23, and ics23 tests --- examples/cosmos/ics23/hashes.qnt | 29 ++++---- examples/cosmos/ics23/ics23.qnt | 58 +++++++-------- examples/cosmos/ics23/ics23test.qnt | 111 +++++++++++++++++----------- 3 files changed, 110 insertions(+), 88 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 3e7565dda..edf72ea4e 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -33,10 +33,10 @@ /// Igor Konnov, Informal Systems, 2022-2023 module hashes { /// A sequence of bytes is simply a list of integers - type BYTES_T = List[int] + type Bytes_t = List[int] /// compare two lists of integers (e.g., bytes) lexicographically - pure def lessThan(w1: BYTES_T, w2: BYTES_T): bool = { + pure def lessThan(w1: Bytes_t, w2: Bytes_t): bool = { pure val len1 = length(w1) pure val len2 = length(w2) or { @@ -51,22 +51,28 @@ module hashes { } } + /// Does the sequence of bytes have the nil value. + /// In our spec, it is equivalent to empty. + pure def isNil(w: Bytes_t): bool = { + w == [] + } + /// A tree node that represents a fragment of a term type TERM_NODE_T = { // node type: either "h" (for hash), or "r" (for raw sequence) t: str, // the bytes when t = "r", and [] when t = "h" - b: BYTES_T + b: Bytes_t } /// A word is a map from a path to the term node. /// The first root's child is [ 0 ], the second root's child is [ 1 ], /// the first child of [ 0 ] is [ 0, 0], etc. - type TERM_T = BYTES_T -> TERM_NODE_T + type Term_t = Bytes_t -> TERM_NODE_T /// Compute term length in bytes, /// assuming that a hash occupies 32 bytes (as SHA256 does) - pure def termLen(term: TERM_T): int = { + pure def termLen(term: Term_t): int = { // the root's children pure val top = keys(term).filter(p => length(p) == 1).map(p => term.get(p)) @@ -74,17 +80,12 @@ module hashes { } // Construct the term that encodes a raw sequence of bytes - pure def raw(bytes: BYTES_T): TERM_T = { + pure def raw(bytes: Bytes_t): Term_t = { Map([ 0 ] -> { t: "r", b: bytes }) } - /// Does the term represent the empty raw sequence of bytes - pure def isNil(term: TERM_T): bool = { - term == Map([ 0 ] -> { t: "r", b: [] }) - } - // Hash a term - pure def termHash(term: TERM_T): TERM_T = { + pure def termHash(term: Term_t): Term_t = { // add "h" on top, which has the key [ 0 ], and attach term to it pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) paths.mapBy(p => @@ -98,7 +99,7 @@ module hashes { /// Concatenate two terms. Special attention is paid to the case when the /// both terms are raw sequences, which requires them to be merged. - pure def termConcat(left: TERM_T, right: TERM_T): TERM_T = { + pure def termConcat(left: Term_t, right: Term_t): Term_t = { pure val l = left.get([0]) pure val r = right.get([0]) if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") { @@ -126,7 +127,7 @@ module hashes { // Slice the sequence represented by a term. // We only slice raw sequences. - pure def termSlice(term: TERM_T, start: int, end: int): TERM_T = { + pure def termSlice(term: Term_t, start: int, end: int): Term_t = { pure val first = term.get([ 0 ]) if (size(keys(term)) == 1 and first.t == "r") { raw(first.b.slice(start, end)) diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index 2717c263c..07fcd5a6f 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -25,25 +25,25 @@ module ics23 { // https://github.com/confio/ics23/tree/master/go // type aliases for readability - type KEY_T = TERM_T - type VALUE_T = TERM_T - type CommitmentRoot_T = TERM_T - type CommitmentProof_T = TERM_T + type Key_t = Bytes_t + type Value_t = Bytes_t + type CommitmentRoot_t = Term_t + type CommitmentProof_t = Term_t // ICS23 IavlSpec has: - // MinPrefixLength = 4 - // MaxPrefixLength = 12 - // ChildSize = 33 + // MinPrefixLength = 1 + // MaxPrefixLength = 1 + // ChildSize = 32 // // To ease spec testing, we set: pure val MinPrefixLen = 1 - pure val MaxPrefixLen = 2 + pure val MaxPrefixLen = 1 // It is crucial to make sure that ChildSize > MaxPrefixLen - pure val ChildSize = 33 // 32 bytes in SHA256 + 1 byte for length + pure val ChildSize = 32 // 32 bytes in SHA256 // Empty child is a predefined sequence that fills an absent child. - // TODO: EmptyChild is set to nil in IavlSpec. We have 33 bytes. + // TODO: EmptyChild is set to nil in TendermintSpec. We have 32 bytes. pure val EmptyChild = raw([ - 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ]) @@ -51,37 +51,37 @@ module ics23 { // The implementation additionally stores hashing and length functions: // hash, prehashKey, prehashValue, len. Since we fix the spec to IAVL, // we do not have to carry them around. - prefix: TERM_T + prefix: Term_t } type INNER_T = { // The implementation additionally stores the hashing function. // Since we fix the spec to IAVL, we do not have to carry it around. - prefix: TERM_T, - suffix: TERM_T + prefix: Term_t, + suffix: Term_t } /// a proof of existence of (key, value) - type ExistsProof_T = { - key: KEY_T, value: VALUE_T, leaf: LEAF_T, path: List[INNER_T] + type ExistsProof_t = { + key: Key_t, value: Value_t, leaf: LEAF_T, path: List[INNER_T] } /// a proof of non-existence of a key - type NonExistsProof_T = { - key: KEY_T, left: ExistsProof_T, right: ExistsProof_T + type NonExistsProof_t = { + key: Key_t, left: ExistsProof_t, right: ExistsProof_t } /// calculate a hash from an exists proof - def existsCalculate(p: ExistsProof_T): CommitmentProof_T = { + def existsCalculate(p: ExistsProof_t): CommitmentProof_t = { // This is how the leaf hash is computed. // Notice that the key is not hashed. val leafHash = termHash(p.leaf.prefix // TODO: use encodeVarintProto - .termConcat(raw([termLen(p.key)])) - .termConcat(p.key) + .termConcat(raw([length(p.key)])) + .termConcat(raw(p.key)) .termConcat(raw([32])) - .termConcat(termHash(p.value))) + .termConcat(termHash(raw(p.value)))) // the inner node nodeHashes are concatenated and hashed upwards p.path.foldl(leafHash, @@ -100,8 +100,8 @@ module ics23 { /// proof is an ExistenceProof for the given key and value AND /// calculating the root for the ExistenceProof matches /// the provided CommitmentRoot - def verifyMembership(root: CommitmentRoot_T, - proof: ExistsProof_T, key: KEY_T, value: VALUE_T): bool = { + def verifyMembership(root: CommitmentRoot_t, + proof: ExistsProof_t, key: Key_t, value: Value_t): bool = { // TODO: specify Decompress // TODO: specify the case of CommitmentProof_Batch // TODO: CheckAgainstSpec ensures that the proof can be verified @@ -260,12 +260,12 @@ module ics23 { } /// VerifyNonMembership returns true iff - /// proof is (contains) a NonExistenceProof - /// both left and right sub-proofs are valid existence proofs (see above) or nil - /// left and right proofs are neighbors (or left/right most if one is nil) + /// proof is (contains) a NonExistenceProof, + /// both left and right sub-proofs are valid existence proofs (see above) or nil, + /// left and right proofs are neighbors (or left/right most if one is nil), /// provided key is between the keys of the two proofs - def verifyNonMembership(root: CommitmentRoot_T, - np: NonExistsProof_T, key: KEY_T): bool = and { + def verifyNonMembership(root: CommitmentRoot_t, + np: NonExistsProof_t, key: Key_t): bool = and { // getNonExistProofForKey isNil(np.left.key) or lessThan(np.left.key, key), isNil(np.right.key) or lessThan(key, np.right.key), diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 55b2e235d..450280111 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -6,6 +6,7 @@ /// /// Igor Konnov, Informal Systems, 2022-2023 module ics23test { + import hashes.* from "./hashes" import ics23.* from "./ics23" // test data @@ -22,107 +23,127 @@ module ics23test { pure val existsCalculateTest = { pure val result = existsCalculate({ - key: [5], - value: [5, 6], - leaf: { prefix: [5, 6, 7] }, + key: [ 5 ], + value: [ 5, 6 ], + leaf: { + prefix: raw([ 9, 10, 11 ]) + }, path: [ - { prefix: [5, 6], suffix: [8] }, - { prefix: [5], suffix: [7] } + { prefix: raw([5, 6]), suffix: raw([8]) }, + { prefix: raw([5]), suffix: raw([7]) } ] }) - assert(result == [32, 0, 4]) + // a map representation of the term with hashes + pure val expected = Map( + [0, 0] -> { b: [5], t: "r" }, + [0, 1, 0] -> { b: [5, 6], t: "r" }, + [0, 1, 1, 0] -> { b: [9, 10, 11, 1, 5, 32], t: "r" }, + [0, 1, 1, 1, 0] -> { b: [5, 6], t: "r" }, + [0, 1, 1, 1] -> { b: [], t: "h" }, + [0, 1, 1] -> { b: [], t: "h" }, + [0, 1, 2] -> { b: [8], t: "r" }, + [0, 1] -> { b: [], t: "h" }, + [0, 2] -> { b: [7], t: "r" }, + [0] -> { b: [], t: "h" } + ) + assert(expected == result) } pure val isLeftMost1Test = { assert(isLeftMost([ - { prefix: [1], suffix: [3, 4, 5] }, - { prefix: [2], suffix: [3, 4, 5] }, - { prefix: [3], suffix: [3, 4, 5] } + { prefix: raw([1]), suffix: termHash(raw([3, 4, 5])) }, + { prefix: raw([2]), suffix: termHash(raw([3, 4, 5])) }, + { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } ])) } pure val isLeftMost2Test = assert(isLeftMost([ - { prefix: [1, 0, 0, 0], suffix: [] }, - { prefix: [2], suffix: [3, 4, 5] }, - { prefix: [3], suffix: [3, 4, 5] } + { prefix: termConcat(raw([1]), EmptyChild), suffix: raw([]) }, + { prefix: raw([2]), suffix: termHash(raw([3, 4, 5])) }, + { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } ])) pure val isLeftMost3Test = { assert(isLeftMost([ - { prefix: [1], suffix: [3, 4, 5 ] }, - { prefix: [2, 0, 0, 0], suffix: [] }, - { prefix: [3], suffix: [3, 4, 5] } + { prefix: raw([1]), suffix: termHash(raw([3, 4, 5])) }, + { prefix: termConcat(raw([2]), EmptyChild), suffix: raw([]) }, + { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } ])) } pure val isRightMost1Test = assert(isRightMost([ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2, 4, 5, 6], suffix: [] }, - { prefix: [3, 3, 4, 5], suffix: [] } + { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: termConcat(raw([2]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: termConcat(raw([3]), termHash(raw([4, 5, 6]))), suffix: raw([]) } ])) pure val isRightMost2Test = assert(isRightMost([ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2], suffix: [0, 0, 0] }, - { prefix: [3, 3, 4, 5], suffix: [] } + { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: raw([2]), suffix: EmptyChild }, + { prefix: termConcat(raw([2]), termHash(raw([3, 4, 5]))), suffix: raw([]) } ])) pure val isLeftStep1Test = assert(isLeftStep( - { prefix: [1], suffix: [4, 5, 6] }, - { prefix: [2, 7, 8, 9], suffix: [] } + { prefix: raw([1]), suffix: termHash(raw([4, 5, 6])) }, + { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } )) pure val isLeftNeighborTest = assert(isLeftNeighbor( [ - { prefix: [1], suffix: [4, 5, 6] }, - { prefix: [2, 7, 8, 9], suffix: [] } + { prefix: raw([1]), suffix: termHash(raw([4, 5, 6])) }, + { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } ], [ - { prefix: [1, 4, 5, 6], suffix: [] }, - { prefix: [2, 7, 8, 9], suffix: [] } + { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } ] )) pure val verifyNonMembershipTest = { // * // / \ - // 2,3 4,5 - val lhash = existsCalculate({ - key:[2], value: [3], leaf: { prefix: [ 0 ] }, path: [] + // 2:3 4:5 + pure val lhash = existsCalculate({ + key: [2], value: [3], leaf: { prefix: raw([ 0 ]) }, path: [] }) - val rhash = existsCalculate({ - key:[4], value: [5], leaf: { prefix: [ 0 ] }, path: [] + pure val rhash = existsCalculate({ + key:[4], value: [5], leaf: { prefix: raw([ 0 ]) }, path: [] }) - val left = { + // the left proof + pure val lproof: ExistsProof_t = { key: [ 2 ], value: [ 3 ], - leaf: { prefix: [ 0 ] }, - path: [{ prefix: [0], suffix: rhash }] + leaf: { prefix: raw([ 0 ]) }, + path: [{ prefix: raw([0]), suffix: rhash }] } - val right = { + // the right proof + pure val rproof: ExistsProof_t = { key: [ 4 ], value: [ 5 ], - leaf: { prefix: [ 0 ] }, - path: [{ prefix: [0].concat(lhash), suffix: [] }] + leaf: { prefix: raw([ 0 ]) }, + path: [{ prefix: raw([0]).termConcat(lhash), suffix: raw([]) }] } - val root = [32, 0, 2] - val nilProof = { key: [], value: [], leaf: { prefix: [] }, path: [] } + pure val root = termHash(raw([0]).termConcat(lhash).termConcat(rhash)) + pure val nilProof: ExistsProof_t = + { key: [], value: [], leaf: { prefix: raw([]) }, path: [] } and { - val np1 = { key: [1], left: nilProof, right: left } + pure val np1 = { key: [1], left: nilProof, right: lproof } assert(verifyNonMembership(root, np1, [ 1 ])), - val np2 = { key: [2], left: left, right: right } + /* + pure val np2 = { key: [2], left: lproof, right: rproof } assert(not(verifyNonMembership(root, np2, [ 2 ]))), - val np3 = { key: [3], left: left, right: right } + pure val np3 = { key: [3], left: lproof, right: rproof } assert(verifyNonMembership(root, np3, [ 3 ])), - val np4 = { key: [2], left: left, right: right } + pure val np4 = { key: [2], left: lproof, right: rproof } assert(not(verifyNonMembership(root, np4, [ 4 ]))), - val np5 = { key: [5], left: right, right: nilProof } + pure val np5 = { key: [5], left: rproof, right: nilProof } assert(verifyNonMembership(root, np5, [ 5 ])), + */ } } } \ No newline at end of file From c690426be9d4c2c69299f13edbd12b6aec50527c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 22 Jun 2023 14:57:10 +0200 Subject: [PATCH 11/24] uncomment one test --- examples/cosmos/ics23/ics23test.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 450280111..a4ddaf368 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -134,9 +134,9 @@ module ics23test { and { pure val np1 = { key: [1], left: nilProof, right: lproof } assert(verifyNonMembership(root, np1, [ 1 ])), - /* pure val np2 = { key: [2], left: lproof, right: rproof } assert(not(verifyNonMembership(root, np2, [ 2 ]))), + /* pure val np3 = { key: [3], left: lproof, right: rproof } assert(verifyNonMembership(root, np3, [ 3 ])), pure val np4 = { key: [2], left: lproof, right: rproof } From db92c4c3c4b0207b3bd0eeaeba348b738f758939 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 23 Jun 2023 11:01:50 +0200 Subject: [PATCH 12/24] fix all the tests in ics23test --- examples/cosmos/ics23/hashes.qnt | 8 +++++++- examples/cosmos/ics23/ics23test.qnt | 2 -- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index edf72ea4e..430c5613b 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -102,7 +102,13 @@ module hashes { pure def termConcat(left: Term_t, right: Term_t): Term_t = { pure val l = left.get([0]) pure val r = right.get([0]) - if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") { + pure val isLSeq = size(keys(left)) == 1 and l.t == "r" + pure val isRSeq = size(keys(right)) == 1 and r.t == "r" + if (isLSeq and l.b == []) { + right + } else if (isRSeq and r.b == []) { + left + } else if (isLSeq and isRSeq) { // both arguments are raw sequences, produce a single raw sequence Map([0] -> { t: "r", b: l.b.concat(r.b) }) } else { diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index a4ddaf368..7f76e89b5 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -136,14 +136,12 @@ module ics23test { assert(verifyNonMembership(root, np1, [ 1 ])), pure val np2 = { key: [2], left: lproof, right: rproof } assert(not(verifyNonMembership(root, np2, [ 2 ]))), - /* pure val np3 = { key: [3], left: lproof, right: rproof } assert(verifyNonMembership(root, np3, [ 3 ])), pure val np4 = { key: [2], left: lproof, right: rproof } assert(not(verifyNonMembership(root, np4, [ 4 ]))), pure val np5 = { key: [5], left: rproof, right: nilProof } assert(verifyNonMembership(root, np5, [ 5 ])), - */ } } } \ No newline at end of file From b2334dd9a5fb73a80376e047a7ec7113444fe0e7 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 23 Jun 2023 11:28:24 +0200 Subject: [PATCH 13/24] clean unneeded files and update the readme --- examples/cosmos/ics23/README.md | 52 ++-- examples/cosmos/ics23/ics23pbt.qnt | 106 ------- examples/cosmos/ics23/tla/ics23.tla | 265 ---------------- examples/cosmos/ics23/tla/ics23pbt.tla | 102 ------- examples/cosmos/ics23/tla/ics23trees.tla | 285 ------------------ .../ics23/{ics23trees.qnt => treeGen.qnt} | 39 ++- 6 files changed, 39 insertions(+), 810 deletions(-) delete mode 100644 examples/cosmos/ics23/ics23pbt.qnt delete mode 100644 examples/cosmos/ics23/tla/ics23.tla delete mode 100644 examples/cosmos/ics23/tla/ics23pbt.tla delete mode 100644 examples/cosmos/ics23/tla/ics23trees.tla rename examples/cosmos/ics23/{ics23trees.qnt => treeGen.qnt} (91%) diff --git a/examples/cosmos/ics23/README.md b/examples/cosmos/ics23/README.md index 09090a50a..67b031fd4 100644 --- a/examples/cosmos/ics23/README.md +++ b/examples/cosmos/ics23/README.md @@ -1,60 +1,48 @@ -This is a formal specification and invariants of [ICS23 Spec][] in Quint and TLA+: +This is a formal specification and invariants of [ICS23 Spec][] in Quint. +If this is the first Quint specification you see, we recommend checking simpler +specifications first. This one is quite advanced. ## Quint specification Specification [ics23.qnt](./ics23.qnt) is the Quint specification that contains four modules: - - Module `basics` contains basic type definitions and auxiliary definitions. + - Module `hashes` introduces a specification of hashes via a symbolic + representation of irreversible hashes. - - Module `ics23` contains membership and non-membership proofs. + - Module `ics23` contains membership and non-membership proofs, + following the ICS23 code. - - Module `ics23pbt` contains definitions for randomized tests similar to PBT. + - Module `ics23test` contains basic unit tests that demonstrate simple + scenarios of membership and non-membership verification. - - Module `trees` contains advanced randomized tests that use tree generation. + - Module `treeGen` contains advanced randomized tests + that generate randomized tests for ICS23. **Unit tests.** You can use Quint REPL to run basic unit tests as follows: ```sh -$ quint repl ->>> .load ics23.qnt ->>> import ics23test.* ->>> allTests -``` - -**Randomized generation of examples.** You can run randomized tests to produce -examples of successful membership and non-membership verification as follows: - -```sh -$ quint repl ->>> .load ics23.qnt ->>> import ics23pbt.* ->>> _test(1000, 10, "Init", "Next", "TestVerify") ->>> _test(1000, 10, "Init", "Next", "TestNonMem") +$ quint test ics23test.qnt ``` **Randomized invariant checking.** Finally, you can check membership and non-membership invariants with the random simulator: ```sh -$ quint repl ->>> .load ics23.qnt ->>> import trees.* ->>> _test(1000, 1, "Init", "Next", "NonMemInv") ->>> _test(1000, 1, "Init", "Next", "MemInv") +$ quint run --invariant=nonMemInv --max-samples=1000 ics23trees.qnt +$ quint run --invariant=memInv --max-samples=1000 ics23trees.qnt ``` -## TLA+ specification +If the simulator finds a violation to the above invariants, please let us know, +as these invariants should hold true. -Specifications [ics23.tla](./ics23.tla) and [ics23trees.tla](./ics23trees.tla) -is the manual translation from Quint to TLA+. The main value of this -specification is the ability to check the invariants with Apalache: +If you would like to produce several examples of checking membership and +non-membership, run the simulator as follows: ```sh -$ apalache-mc check --inv=MemInv ics23trees.tla -$ apalache-mc check --inv=NonMemInv ics23trees.tla +$ quint run --invariant=memExample --max-samples=1000 treeGen.qnt +$ quint run --invariant=nonMemExample --max-samples=1000 treeGen.qnt ``` - [ICS23 Spec]: https://github.com/cosmos/ibc/tree/main/spec/core/ics-023-vector-commitments [ICS23]: https://github.com/confio/ics23/ diff --git a/examples/cosmos/ics23/ics23pbt.qnt b/examples/cosmos/ics23/ics23pbt.qnt deleted file mode 100644 index c6d6de478..000000000 --- a/examples/cosmos/ics23/ics23pbt.qnt +++ /dev/null @@ -1,106 +0,0 @@ -/// Simple property-based tests for ics23. They happened to be not very useful, -/// as random simulation alone cannot produce even simple examples of sound -/// non-membership proofs. -/// -/// For more advanced property-based testing, see ics23trees.qnt. -/// -/// To execute simple PBT-like tests for 1000 runs of length up to 10 steps -/// in the simulator, type the following: -/// -/// $ quint run --invariant=noVerifyInv ics23pbt.qnt -/// $ quint run --invariant=noNonMemInv ics23pbt.qnt -/// -/// If the simulator finds an example that violates TestVerify or TestNonMem, -/// it displays this counterexample. -/// -/// Igor Konnov, Informal Systems, 2022-2023 -module ics23pbt { - import words.* from "./words" - import ics23.* from "./ics23" - - // an non-membership proof - var nonMemProof: NonExistsProof_T - // a key to test - var inputKey: WORD_T - - // We limit the letters to a very small set, - // including '32' for hash headers. - val Byte = 0.to(3).union(Set(32)) - - val toWord(m) = - m.keys().fold([], (l, i) => l.append(m.get(i))) - - action genKey = - nondet i = Byte.oneOf() - inputKey' = [i] - - action init = all { - genKey, - // we start with leafs in the initial state - nondet lk = Byte.oneOf() - nondet lv = Byte.oneOf() - nondet lp = Byte.oneOf() - nondet rk = Byte.oneOf() - nondet rv = Byte.oneOf() - nondet rp = Byte.oneOf() - nondet pk = Byte.oneOf() - val lproof = { - key: [ lk ], value: [ lv ], - leaf: { prefix: [ lp ] }, path: [] - } - val rproof = { - key: [ rk ], value: [ rv ], leaf: { prefix: [ rp ] }, path: [] - } - nonMemProof' = { key: [ pk ], left: lproof, right: rproof } - } - - def extend(proof, dir, word) = - val node = - if (dir == "turnLeft") { - prefix: word, - suffix: [] - } else { - prefix: word.slice(0, MaxPrefixLen), - suffix: word.slice(MaxPrefixLen, MaxPrefixLen + ChildSize) - } - proof.with("path", proof.path.append(node)) - - /// grow the proof on the left - action growLeft = - nondet dir = Set("turnLeft", "turnRight").oneOf() - nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() - nonMemProof' = - nonMemProof.with("left", nonMemProof.left.extend(dir, toWord(m))) - - /// grow the proof on the right - action growRight = - nondet dir = Set("turnLeft", "turnRight").oneOf() - nondet m = 1.to(MaxPrefixLen + ChildSize).setOfMaps(Byte).oneOf() - nonMemProof' = - nonMemProof.with("right", nonMemProof.right.extend(dir, toWord(m))) - - action step = all { - genKey, - any { - growLeft, - growRight - }, - } - - /// by checking this invariant, we may produce an example of when - /// verifyMembership succeeds - val noVerifyInv = { - val root = existsCalculate(nonMemProof.left) - not(verifyMembership(root, - nonMemProof.left, inputKey, nonMemProof.left.value)) - } - - /// by checking this invariant, we may produce an example of when - /// verifyNonMembership succeeds - val noNonMemInv = or { - lessThan(inputKey, nonMemProof.left.key), - lessThan(nonMemProof.right.key, inputKey), - val root = existsCalculate(nonMemProof.left) - not(verifyNonMembership(root, nonMemProof, inputKey)) - } -} \ No newline at end of file diff --git a/examples/cosmos/ics23/tla/ics23.tla b/examples/cosmos/ics23/tla/ics23.tla deleted file mode 100644 index 5de97e3e0..000000000 --- a/examples/cosmos/ics23/tla/ics23.tla +++ /dev/null @@ -1,265 +0,0 @@ ---------------------------- MODULE ics23 -------------------------------------- -\* A hand-written translation of ics23.qnt -EXTENDS Integers, Sequences, Apalache - -\* basics -\* -\* @typeAlias: word = Seq(Int); -\* @typeAlias: key = $word; -\* @typeAlias: value = $word; -\* @typeAlias: commitmentRoot = $word; -\* @typeAlias: commitmentProof = $word; -\* @typeAlias: leaf = { prefix: $word }; -\* @typeAlias: inner = { prefix: $word, suffix: $word }; -\* @typeAlias: existsProof = { -\* key: $word, value: $word, leaf: $leaf, path: Seq($inner) -\* }; -\* @typeAlias: nonExistsProof = { -\* key: $word, left: $existsProof, right: $existsProof -\* }; -ics23_aliases == TRUE - -\* we interpret the empty word as nil -IsNil(word) == Len(word) = 0 - -\* compare two integer words lexicographically -\* @type: ($word, $word) => Bool; -LessThan(w1, w2) == - LET len1 == Len(w1) IN - LET len2 == Len(w2) IN - \//\ len1 < len2 - /\ \A i \in DOMAIN w1: - w1[i] = w2[i] - \//\ len1 = len2 - /\ \E i \in DOMAIN w1: - /\ w1[i] < w2[i] - /\ \A j \in DOMAIN w1: - (j < i) => w1[i] = w2[i] - - -\* Golang slice lst[start:end] slices in the interval [start, end). -\* Golang indices start with 0. -\* We define this operator for compatibility with the Golang code. -GoSlice(lst, start, end) == SubSeq(lst, start + 1, end) - -\* base spec - -\* TODO: introduce CONSTANTS instead -MinPrefixLen == 1 -MaxPrefixLen == 2 -ChildSize == 3 - -\* @type: $word; -EmptyChild == <<0, 0, 0>> - -\* We need a hash that returns ChildSize - 1 elements. -\* For simulation, we are just summing up the word elements modulo 8. -\* For verification, we should use an injective function as a perfect hash. -\* -\* TODO: introduce Hash as a CONSTANT -\* -\* @type: $word => $word; -Hash(word) == - <<32, 0, ApaFoldSeqLeft(LAMBDA i, j: i + j, 0, word) % 8>> - -\* calculate a hash from an exists proof -\* @type: $existsProof => $commitmentProof; -ExistsCalculate(p) == - \* this is how the leaf hash is computed - LET leafHash == - Hash(Append(Append(p.leaf.prefix, Len(p.key)) \o Hash(p.key), - Len(p.value)) \o Hash(p.value)) - IN - \* the inner node hashes are concatenated and hashed upwards - LET \* @type: ($word, $inner) => $word; - AddHash(child, inner) == - Hash(inner.prefix \o child \o inner.suffix) - IN - ApaFoldSeqLeft(AddHash, leafHash, p.path) - - -\* verify that a proof matches a root -\* @type: ($existsProof, $word, $key, $value) => Bool; -Verify(proof, root, key, value) == - /\ key = proof.key - /\ value = proof.value - /\ root = ExistsCalculate(proof) - -\* VerifyMembership returns true iff -\* proof is an ExistenceProof for the given key and value AND -\* calculating the root for the ExistenceProof matches -\* the provided CommitmentRoot -\* @type: ($word, $existsProof, $key, $value) => Bool; -VerifyMembership(root, proof, key, value) == - \* TODO: specify Decompress - \* TODO: specify the case of CommitmentProof_Batch - \* TODO: CheckAgainstSpec ensures that the proof can be verified - \* by the spec checker - Verify(proof, root, key, value) - - -\* checks if an op has the expected padding -\* @type: ($inner, Int, Int, Int) => Bool; -HasPadding(inner, minPrefixLen, maxPrefixLen, suffixLen) == - /\ Len(inner.prefix) >= minPrefixLen - /\ Len(inner.prefix) <= maxPrefixLen - \* When inner turns left, suffixLen == ChildSize, - \* that is, we store the hash of the right child in the suffix. - \* When inner turns right, suffixLen == 0, - \* that is, we store the hash of the left child in the prefix. - /\ Len(inner.suffix) = suffixLen - -\* This will look at the proof and determine which order it is... -\* So we can see if it is branch 0, 1, 2 etc... to determine neighbors -\* https:\*github.com/confio/ics23/blob/a4daeb4c24ce1be827829c0841446abc690c4f11/go/proof.go#L400-L411 -\* @type: $inner => <>; -OrderFromPadding(inner) == - \* Specialize orderFromPadding to IavlSpec: - \* ChildOrder = { 0, 1 } - \* branch = 0: minp, maxp, suffix = MinPrefixLen, MaxPrefixLen, ChildSize - \* branch = 1: minp, maxp, suffix = - \* ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 - IF HasPadding(inner, MinPrefixLen, MaxPrefixLen, ChildSize) - \* the node turns left - THEN <<0, TRUE>> - ELSE IF HasPadding(inner, ChildSize + MinPrefixLen, - ChildSize + MaxPrefixLen, 0) - \* the node turns right - THEN <<1, TRUE>> - ELSE - \* error - <<0, FALSE>> - -\* leftBranchesAreEmpty returns true if the padding bytes correspond to all -\* empty siblings on the left side of a branch, ie. it's a valid placeholder -\* on a leftmost path -\* @type: $inner => Bool; -LeftBranchesAreEmpty(inner) == - \* the case of leftBranches == 0 returns false - LET order == OrderFromPadding(inner) IN - /\ order[2] /\ order[1] /= 0 - \* the remaining case is leftBranches == 1, see orderFromPadding - \* actualPrefix = len(inner.prefix) - 33 - /\ Len(inner.prefix) >= ChildSize - \* getPosition(0) returns 0 - /\ LET from == Len(inner.prefix) - ChildSize IN - GoSlice(inner.prefix, from, from + ChildSize) = EmptyChild - -\* IsLeftMost returns true if this is the left-most path in the tree, -\* excluding placeholder (empty child) nodes -\* @type: Seq($inner) => Bool; -IsLeftMost(path) == - \* Calls getPadding(0) => idx = 0, prefix = 0. - \* We specialize the constants to IavlSpec. - \A i \in DOMAIN path: - LET step == path[i] IN - \* the path goes left - \/ HasPadding(step, MinPrefixLen, MaxPrefixLen, ChildSize) - \* the path goes right, but the left child is empty (a gap) - \/ LeftBranchesAreEmpty(step) - -\* rightBranchesAreEmpty returns true if the padding bytes correspond -\* to all empty siblings on the right side of a branch, -\* i.e. it's a valid placeholder on a rightmost path -\* @type: $inner => Bool; -RightBranchesAreEmpty(inner) == - \* the case of rightBranches == 0 returns false - LET order == OrderFromPadding(inner) IN - /\ order[2] /\ order[1] /= 1 - \* the remaining case is rightBranches == 1, see orderFromPadding - /\ Len(inner.suffix) = ChildSize - \* getPosition(0) returns 0, hence, from == 0 - /\ inner.suffix = EmptyChild - -\* IsRightMost returns true if this is the left-most path in the tree, -\* excluding placeholder (empty child) nodes -\* @type: Seq($inner) => Bool; -IsRightMost(path) == - \* Specialize to IavlSpec - \* Calls getPadding(1) => minPrefix, maxPrefix, - \* suffix = ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 - \A i \in DOMAIN path: - LET step == path[i] IN - \* the path goes right - \/ HasPadding(step, ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0) - \* the path goes left, but the right child is empty (a gap) - \/ RightBranchesAreEmpty(step) - -\* isLeftStep assumes left and right have common parents -\* checks if left is exactly one slot to the left of right -\* @type: ($inner, $inner) => Bool; -IsLeftStep(left, right) == - \* 'left' turns left, and 'right' turns right - LET lorder == OrderFromPadding(left) IN - LET rorder == OrderFromPadding(right) IN - /\ lorder[2] - /\ rorder[2] - /\ rorder[1] = lorder[1] + 1 - -\* IsLeftNeighbor returns true if `right` is the next possible path -\* right of `left` -\* -\* Find the common suffix from the Left.Path and Right.Path and remove it. -\* We have LPath and RPath now, which must be neighbors. -\* Validate that LPath[len-1] is the left neighbor of RPath[len-1]. -\* For step in LPath[0..len-1], validate step is right-most node. -\* For step in RPath[0..len-1], validate step is left-most node. -IsLeftNeighbor(lpath, rpath) == - \* count common tail (from end, near root) - \* cut the left and right paths - \E li \in DOMAIN lpath, ri \in DOMAIN rpath: - \* they are equidistant from the root - /\ Len(lpath) - li = Len(rpath) - ri - \* The distance to the root (the indices are 0-based). - \* dist == 0 holds for the root. - \* Note: we are compensating for 1-based indices here. - /\ LET dist == Len(lpath) (*- 1*) - li IN - \* The prefixes and suffixes match just above the cut points. - \* Note that we are using a filter over the domain of lpath, - \* as Apalache needs a bounded set, instead of 1..dist. - \A k \in { j \in DOMAIN lpath: j <= dist }: - LET lnode == lpath[li + k] IN - LET rnode == rpath[ri + k] IN - /\ lnode.prefix = rnode.prefix - /\ lnode.suffix = rnode.suffix - \* Now topleft and topright are the first divergent nodes - \* make sure they are left and right of each other. - \* Actually, lpath.nth(li) and rpath.nth(ri) are an abstraction - \* of the same tree node: - \* the left one stores the hash of the right one, whereas - \* the right one stores the hash of the left one. - /\ IsLeftStep(lpath[li], rpath[ri]) - \* Left and right are remaining children below the split, - \* ensure left child is the rightmost path, and visa versa. - \* Note that we are writing `li - 1` and `ri - 1`, - \* as `li` and `ri` are 1-based. - /\ IsRightMost(GoSlice(lpath, 0, li - 1)) - /\ IsLeftMost(GoSlice(rpath, 0, ri - 1)) - -\* VerifyNonMembership returns true iff -\* proof is (contains) a NonExistenceProof -\* both left and right sub-proofs are valid existence proofs (see above) or nil -\* left and right proofs are neighbors (or left/right most if one is nil) -\* provided key is between the keys of the two proofs -\* @type: ($word, $nonExistsProof, $word) => Bool; -VerifyNonMembership(root, np, key) == - \* getNonExistProofForKey - /\ IsNil(np.left.key) \/ LessThan(np.left.key, key) - /\ IsNil(np.right.key) \/ LessThan(key, np.right.key) - \* implicit assumption, missing in the code: - \* https://github.com/informalsystems/ics23-audit/issues/14 - /\ np.key = key - \* Verify - /\ ~IsNil(np.left.key) \/ ~IsNil(np.right.key) - /\ \/ IsNil(np.left.key) - \/ /\ Verify(np.left, root, np.left.key, np.left.value) - /\ LessThan(np.left.key, key) - /\ \/ IsNil(np.right.key) - \/ /\ Verify(np.right, root, np.right.key, np.right.value) - /\ LessThan(key, np.right.key) - /\ IF IsNil(np.left.key) - THEN IsLeftMost(np.right.path) - ELSE IF IsNil(np.right.key) - THEN IsRightMost(np.left.path) - ELSE IsLeftNeighbor(np.left.path, np.right.path) -=============================================================================== diff --git a/examples/cosmos/ics23/tla/ics23pbt.tla b/examples/cosmos/ics23/tla/ics23pbt.tla deleted file mode 100644 index 429ee34ea..000000000 --- a/examples/cosmos/ics23/tla/ics23pbt.tla +++ /dev/null @@ -1,102 +0,0 @@ -------------------------- MODULE ics23pbt -------------------------------------- -\* property-based tests for ICS23 -\* This is a hand-written translation of the module ics23pbt in ics23.qnt -EXTENDS Integers, Sequences, Apalache, ics23 - -VARIABLE - \* @type: $nonExistsProof; - nproof, - \* @type: $word; - inputKey - -\* We limit the letters to a very small set, -\* including '32' for checksums. -Byte == 0..7 \union { 32 } - -\* @type: (Int -> Int) => $word; -ToWord(m) == - LET Add(l, i) == Append(l, m[i]) IN - ApaFoldSet(Add, <<>>, DOMAIN m) - -GenKey == - \E i \in Byte: - inputKey' = <> - -\* @type: Seq({ prefix: $word, suffix: $word }); -EmptyPath == <<>> - -\* @type: $word; -EmptyWord == <<>> - -\* @type: Int => $word; -Single(k) == <> - -Init == - /\ \E i \in Byte: - inputKey = Single(i) - /\ \E lk, lv, lp, rk, rv, rp, pk \in Byte: - LET \* @type: $existsProof; - lproof == [ - key |-> Single(lk), - value |-> Single(lv), - leaf |-> [ prefix |-> Single(lp) ], - path |-> EmptyPath - ] - IN - LET \* @type: $existsProof; - rproof == [ - key |-> Single(rk), - value |-> Single(rv), - leaf |-> [ prefix |-> Single(rp) ], - path |-> EmptyPath - ] - IN - nproof = [ key |-> Single(pk), left |-> lproof, right |-> rproof ] - -\* @type: ($existsProof, Str, $word) => $existsProof; -Extend(proof, dir, word) == - LET node == - IF dir = "turnLeft" - THEN [ prefix |-> word, suffix |-> EmptyWord ] - ELSE [ - prefix |-> GoSlice(word, 0, MaxPrefixLen), - suffix |-> GoSlice(word, MaxPrefixLen, MaxPrefixLen + ChildSize) - ] - IN - [ proof EXCEPT !.path = Append(@, node) ] - -\* grow the proof on the left -GrowLeft == - \E dir \in { "turnLeft", "turnRight" }: - \E m \in [ 1..(MaxPrefixLen + ChildSize) -> Byte ]: - nproof' = [ nproof EXCEPT !.left = Extend(@, dir, ToWord(m)) ] - -\* grow the proof on the right -GrowRight == - \E dir \in { "turnLeft", "turnRight" }: - \E m \in [ 1..(MaxPrefixLen + ChildSize) -> Byte ]: - nproof' = [ nproof EXCEPT !.right = Extend(@, dir, ToWord(m)) ] - -Next == - /\ GenKey - /\ \/ GrowLeft - \/ GrowRight - -\* By checking this invariant, we may produce an example of when -\* verifyNonMembership succeeds -NonMem == - \/ LessThan(inputKey, nproof.left.key) - \/ LessThan(nproof.right.key, inputKey) - \/ ~VerifyNonMembership(ExistsCalculate(nproof.left), nproof, inputKey) - -\* The version of NonMem, where the left path has at least three nodes -NonMem3 == - \/ LessThan(inputKey, nproof.left.key) - \/ LessThan(nproof.right.key, inputKey) - \/ ~VerifyNonMembership(ExistsCalculate(nproof.left), nproof, inputKey) - \/ Len(nproof.left.path) <= 3 - -View == - ExistsCalculate(nproof.left) - -=============================================================================== diff --git a/examples/cosmos/ics23/tla/ics23trees.tla b/examples/cosmos/ics23/tla/ics23trees.tla deleted file mode 100644 index 497853e77..000000000 --- a/examples/cosmos/ics23/tla/ics23trees.tla +++ /dev/null @@ -1,285 +0,0 @@ ----------------------- MODULE ics23trees -------------------------------------- -\* Proving invariants with model checking. -\* This is a hand-written translation of the module trees in ics23.qnt -\* -\* To check the basic invariants of ICS23, run Apalache as follows: -\* -\* apalache-mc check --inv=MemInv ics23trees.tla -\* apalache-mc check --inv=NonMemInv ics23trees.tla -EXTENDS Integers, Sequences, Apalache, ics23 - -(* - @typeAlias: tree = { - leafs: Int -> { key: $word, value: $word }, - left: Int -> Int, - right: Int -> Int - }; - *) -ics23trees_alises == TRUE - -\* the maximum tree height -Height == 4 - -VARIABLE - \* @type: $tree; - tree, - \* @type: Int -> $word; - nodeHashes, - \* @type: Int; - leftKey, - \* @type: Int; - rightKey, - \* @type: Int; - inputKey - -\* We limit the letters to a very small set, -\* including '32' for checksums. -Byte == 0..7 \union { 32 } - -\* @type: (Int -> Int) => $word; -ToWord(m) == - LET Add(l, i) == Append(l, m[i]) IN - ApaFoldSet(Add, <<>>, DOMAIN m) - -Range(start, end) == - MkSeq(end - start, LAMBDA i: start + i) - -\* @type: Seq({ prefix: $word, suffix: $word }); -EmptyPath == <<>> - -\* @type: $word; -EmptyWord == <<>> - -\* @type: Int => $word; -Single(k) == <> - -\* Compute all parents from the binary representation of the index. -\* To simplify random generation of the trees, we are using -\* the binary encoding. For example, if a leaf has the index 4, -\* that is, 100b, then it has the parents 3 = 10b and 1 = 1b. -Parents(key) == - { key \div (2^h): h \in 1..Height } \ { 0 } - -\* Is a given key a node (inner or leaf) of a tree. -\* @type: ($tree, Int) => Bool; -IsNode(t, key) == - \/ key = 1 - \/ key \in DOMAIN t.leafs - \/ key \in DOMAIN t.left - \/ key \in DOMAIN t.right - -\* Compute nodeHashes of all nodes into a map. -\* @type: $tree => (Int -> $word); -ComputeHashes(t) == - \* compute the hash of a single node, assuming that the children's - \* nodeHashes have been computed - LET \* @type: (Int -> $word, Int) => (Int -> $word); - PutNodeHash(hashMap, key) == - LET h == - IF key \in DOMAIN t.leafs - \* a leaf - THEN LET leaf == t.leafs[key] IN - \* Hash the leaf as in ics23.existsCalculate. - \* In our trees, prefixes are always 0. - Hash(Append(Append(Single(0), Len(leaf.key)) \o Hash(leaf.key), - Len(leaf.value)) - \o Hash(leaf.value)) - ELSE - \* an inner node, assuming that the children nodeHashes were computed - LET \* @type: (Int -> Int) => $word; - HashOrEmpty(childMap) == - IF key \in DOMAIN childMap - THEN hashMap[childMap[key]] - ELSE EmptyChild - IN - \* hash the prefix ([0]) and the hash of the children - Hash(Single(0) \o HashOrEmpty(t.left) \o HashOrEmpty(t.right)) - IN - \* store the hash - [ k \in (DOMAIN hashMap) \union { key} |-> - IF k = key THEN h ELSE hashMap[k] ] - IN - \* go over the nodes from 2^Height to 1 - LET seq == MkSeq(2^Height, LAMBDA h: 2^Height - h + 1) IN - LET emptyMap == [ h \in {} |-> Single(0) ] IN - LET Add(m, key) == - IF IsNode(t, key) - THEN PutNodeHash(m, key) - ELSE m - IN - ApaFoldSeqLeft(Add, emptyMap, seq) - -\* It's very easy to produce binary trees by picking an arbitrary graph and -\* restricting it with the predicate isTree. However, this approach produces -\* very sparse sets of states, to be explored by random search. Hence, we -\* use a more algorithmic approach that represents trees with binary words. -Init == - \* produce an arbitrary tree with leafs in e.g. [2, 8) - \E idx \in SUBSET (2..(2^Height - 1)): - \* remove those numbers that should serve as intermediate nodes - LET leafKeys == { i \in idx: \A j \in idx: i \notin Parents(j) } IN - \* compute all parents - LET allParents == UNION { Parents(i): i \in leafKeys } IN - \* all intermediate nodes that have a left successor - LET leftKeys == { - i \in allParents: - \E j \in allParents \union leafKeys: - 2 * i = j - } IN - \* all intermediate nodes that have a right successor - LET rightKeys == { - i \in allParents: - \E j \in allParents \union leafKeys: - 2 * i + 1 = j - } IN - \* left mapping - LET left == [ i \in leftKeys |-> 2 * i ] IN - \* right mapping - LET right == [ i \in rightKeys |-> 2 * i + 1 ] IN - \* assign values to the keys - /\ \E vs \in [ leafKeys -> Byte ]: - LET leafs == [ k \in DOMAIN vs |-> - [ key |-> Single(k), value |-> Single(vs[k]) ] ] IN - LET t == [ leafs |-> leafs, left |-> left, right |-> right ] IN - /\ tree' = t - /\ nodeHashes = ComputeHashes(t) - \* pick arbitrary left and right keys for non-membership proofs - /\ leftKey' \in leafKeys - /\ rightKey' \in leafKeys - \* pick an arbitrary input key - /\ inputKey \in Byte - -\* convert a tree leaf to an exists proof -LeafToExistsProof(key) == - LET value == tree.leafs[key].value IN - \* encode all intermediate nodes upwards - LET \* @type: (Seq($inner), Int) => Seq($inner); - Add(path, h) == - IF key < 2^h - THEN path - ELSE - LET parent == key \div (2^h) IN - LET \* @type: (Int -> Int) => $word; - HashOrChild(childMap) == - IF parent \in DOMAIN childMap - THEN nodeHashes[childMap[parent]] - ELSE EmptyChild - IN - \* depending on whether the node is going to left or right, - \* push the hashes in the prefix and the suffix - IF key = 2 * parent - THEN LET right == HashOrChild(tree.right) IN - Append(path, [ prefix |-> Single(0), suffix |-> right ]) - ELSE LET left == HashOrChild(tree.left) IN - Append(path, [ prefix |-> Single(0) \o left, suffix |-> EmptyWord]) - IN - LET path == ApaFoldSeqLeft(Add, EmptyPath, Range(1, Height + 1)) IN - \* return the exists proof, where the key is the index itself - [ - key |-> Single(key), - value |-> tree.leafs[key].value, - leaf |-> [ prefix |-> Single(0) ], - path |-> path - ] - -\* The transition does nothing. The state was computed in Init. -Next == - UNCHANGED <> - -\* make sure that the proofs are the same for all the leafs -TreeProofInv == - (leftKey \in DOMAIN tree.leafs /\ rightKey \in DOMAIN tree.leafs) - => - LET lroot == ExistsCalculate(LeafToExistsProof(leftKey)) IN - LET rroot == ExistsCalculate(LeafToExistsProof(rightKey)) IN - lroot = rroot - -\* The invariant of membership verification: -\* If the input key belongs to the leafs, -\* we should be able to prove its membership. -MemInv == - \/ inputKey \notin DOMAIN tree.leafs - \/ LET proof == LeafToExistsProof(inputKey) IN - LET root == ExistsCalculate(proof) IN - VerifyMembership(root, proof, Single(inputKey), proof.value) - -\* check this property to produce an example of where MemInv is violated -MemExample == - ~MemInv - -\* A few lemmas for NonMemInv: -\* MemberShouldFalsify, NonMemberInTheMiddle, NonMemberLeft, NonMemberRight - -MemberShouldFalsify(lproof, rproof) == - \* if the input key belongs to the leafs, - \* we should not be able to disprove its membership - /\ inputKey \in DOMAIN tree.leafs - /\ LET nproof == - [ key |-> Single(inputKey), left |-> lproof, right |-> rproof ] - IN - LET root == ExistsCalculate(lproof) IN - ~VerifyNonMembership(root, nproof, Single(inputKey)) - -NonMemberInTheMiddle(lproof, rproof) == - \* we should be able to prove its non-membership, - \* unless the choice of the keys is bad - /\ inputKey \notin DOMAIN tree.leafs - /\ LET nproof == - [ key |-> Single(inputKey), left |-> lproof, right |-> rproof ] - IN - LET root == ExistsCalculate(lproof) IN - LET noKeyInTheMiddle == - \* there is no leaf between leftKey and rightKey - /\ \A k \in DOMAIN tree.leafs: - k <= leftKey \/ k >= rightKey - \* the keys are not misplaced - /\ leftKey < inputKey - /\ inputKey < rightKey - IN - noKeyInTheMiddle <=> VerifyNonMembership(root, nproof, Single(inputKey)) - -NonMemberLeft(lproof, rproof) == - \* the input key is to the left - /\ IsNil(lproof.key) - \* non-membership is true when the right key is left-most - /\ (inputKey < rightKey /\ \A k \in DOMAIN tree.leafs: rightKey <= k) - <=> - \* or there is a proof - LET root == ExistsCalculate(rproof) IN - LET nproof == - [ key |-> Single(inputKey), left |-> lproof, right |-> rproof ] IN - VerifyNonMembership(root, nproof, Single(inputKey)) - -NonMemberRight(lproof, rproof) == - \* the input key is to the right - /\ IsNil(rproof.key) - \* non-membership is true when the left key is the right-most - /\ (inputKey > leftKey /\ \A k \in DOMAIN tree.leafs: k <= leftKey) - <=> - \* or there is a proof - LET root == ExistsCalculate(lproof) IN - LET nproof == - [ key |-> Single(inputKey), left |-> lproof, right |-> rproof ] - IN - VerifyNonMembership(root, nproof, Single(inputKey)) - -\* The invariant of non-membership verification. -\* Consider all possible positions of the input key and the left/right keys. -NonMemInv == - LET ProofOrNil(key) == - IF key \in DOMAIN tree.leafs - THEN LeafToExistsProof(key) - ELSE [ key |-> EmptyWord, value |-> EmptyWord, - leaf |-> [ prefix |-> EmptyWord ], path |-> EmptyPath ] - IN - LET lproof == ProofOrNil(leftKey) IN - LET rproof == ProofOrNil(rightKey) IN - \/ MemberShouldFalsify(lproof, rproof) - \/ NonMemberInTheMiddle(lproof, rproof) - \/ NonMemberLeft(lproof, rproof) - \/ NonMemberRight(lproof, rproof) - \* trivial cases: - \/ inputKey < rightKey /\ ~IsNil(lproof.key) - \/ inputKey > leftKey /\ ~IsNil(rproof.key) - -=============================================================================== diff --git a/examples/cosmos/ics23/ics23trees.qnt b/examples/cosmos/ics23/treeGen.qnt similarity index 91% rename from examples/cosmos/ics23/ics23trees.qnt rename to examples/cosmos/ics23/treeGen.qnt index 3b97e3dc8..711ddc867 100644 --- a/examples/cosmos/ics23/ics23trees.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -16,8 +16,8 @@ /// a counterexample, there must be an error somewhere. /// /// Igor Konnov, Informal Systems, 2022-2023 -module ics23trees { - import words.* from "./words" +module treeGen { + import hashes.* from "./hashes" import ics23.* from "./ics23" /// We represent a binary tree as a collection of maps, @@ -29,7 +29,7 @@ module ics23trees { /// programming languages. type TREE_T = { // every leaf has a key and value assigned - leafs: int -> { key: WORD_T, value: WORD_T }, + leafs: int -> { key: Bytes_t, value: Bytes_t }, // intermediate nodes have left and/or right children left: int -> int, right: int -> int @@ -37,8 +37,8 @@ module ics23trees { /// the tree generated so far var tree: TREE_T - /// the node nodeHashes - var nodeHashes: int -> WORD_T + /// the node hashes + var nodeHashes: int -> Term_t /// the keys to use for non-membership proofs var leftKey: int var rightKey: int @@ -69,18 +69,15 @@ module ics23trees { def computeHashes(t) = { // compute the hash of a single node, assuming that the children's // nodeHashes have been computed - def putNodeHash(hashMap, key): (int -> List[int], int) => (int -> List[int]) = { + def putNodeHash(hashMap: int -> Term_t, key: int): (int -> Term_t) = { val h = if (t.leafs.keys().contains(key)) { - // a leaf + // simply use existsCalculate on the leaf val leaf = t.leafs.get(key) - // Hash the leaf as in ics23.existsCalculate. - // In our trees, prefixes are always 0. - hash([0].append(length(leaf.key)) - .concat(hash(leaf.key)) - .append(length(leaf.value)) - .concat(hash(leaf.value))) - } else { + existsCalculate({ + key: leaf.key, value: leaf.value, leaf: { prefix: raw([0]) }, path: [] + }) + } else { // an inner node, assuming that the children nodeHashes were computed def hashOrEmpty(childMap) = if (childMap.keys().contains(key)) { @@ -89,7 +86,9 @@ module ics23trees { EmptyChild } // hash the prefix ([0]) and the hash of the children - hash([0].concat(hashOrEmpty(t.left)).concat(hashOrEmpty(t.right))) + termHash(raw([0]) + .termConcat(hashOrEmpty(t.left)) + .termConcat(hashOrEmpty(t.right))) } // store the hash hashMap.put(key, h) @@ -145,7 +144,7 @@ module ics23trees { } /// convert a tree leaf to an exists proof - def leafToExistsProof(key) = + def leafToExistsProof(key: int): ExistsProof_t = val value = tree.leafs.get(key).value // encode all intermediate nodes upwards val path = range(1, height + 1) @@ -165,10 +164,10 @@ module ics23trees { // push the hashes in the prefix and the suffix if (key == 2 * parent) { val right = hashOrChild(tree.right) - p.append({ prefix: [0], suffix: right }) + p.append({ prefix: raw([0]), suffix: right }) } else { val left = hashOrChild(tree.left) - p.append({ prefix: [0].concat(left), suffix: [] }) + p.append({ prefix: raw([0]).termConcat(left), suffix: raw([]) }) } } ) @@ -176,7 +175,7 @@ module ics23trees { { key: [key], value: tree.leafs.get(key).value, - leaf: { prefix: [0] }, + leaf: { prefix: raw([0]) }, path: path, } @@ -279,7 +278,7 @@ module ics23trees { if (tree.leafs.keys().contains(key)) leafToExistsProof(key) else - { key: [], value: [], leaf: { prefix: [] }, path: [] } + { key: [], value: [], leaf: { prefix: raw([]) }, path: [] } } val lproof = proofOrNil(leftKey) val rproof = proofOrNil(rightKey) From b81495c390aeb38c3039c13dd36cf7d5d049f35c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 23 Jun 2023 15:08:09 +0200 Subject: [PATCH 14/24] Apply suggestions from code review Co-authored-by: Thomas Pani --- examples/cosmos/ics23/README.md | 2 +- examples/cosmos/ics23/hashes.qnt | 16 ++++++++-------- examples/cosmos/ics23/treeGen.qnt | 8 ++++---- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/examples/cosmos/ics23/README.md b/examples/cosmos/ics23/README.md index 67b031fd4..a10c6ce14 100644 --- a/examples/cosmos/ics23/README.md +++ b/examples/cosmos/ics23/README.md @@ -25,7 +25,7 @@ specifications first. This one is quite advanced. $ quint test ics23test.qnt ``` -**Randomized invariant checking.** Finally, you can check membership and +**Randomized invariant checking.** Also, you can check membership and non-membership invariants with the random simulator: ```sh diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 430c5613b..24c114385 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -22,7 +22,7 @@ /// / /// [ 3, 4 ] /// -/// The above tree is represented as a map in Quint: +/// The above tree is represented as a map in Quint. Each key corresponds to a path in the tree; for example, the first root's child is [ 0 ], the second root's child is [ 1 ], the first child of [ 0 ] is [ 0, 0], etc. /// /// Map([ 0 ] -> { t: "h", b: [] }, /// [ 0, 0 ] -> { t: "r", b: [ 1, 2 ] }, @@ -51,8 +51,8 @@ module hashes { } } - /// Does the sequence of bytes have the nil value. - /// In our spec, it is equivalent to empty. + /// Returns true iff `w` is the nil value. + /// In our spec, nil is equivalent to the empty list. pure def isNil(w: Bytes_t): bool = { w == [] } @@ -73,18 +73,18 @@ module hashes { /// Compute term length in bytes, /// assuming that a hash occupies 32 bytes (as SHA256 does) pure def termLen(term: Term_t): int = { - // the root's children + // the roots' children pure val top = keys(term).filter(p => length(p) == 1).map(p => term.get(p)) top.fold(0, (s, t) => if (t.t == "h") s + 32 else s + length(t.b)) } - // Construct the term that encodes a raw sequence of bytes + /// Construct the term that encodes a raw sequence of bytes pure def raw(bytes: Bytes_t): Term_t = { Map([ 0 ] -> { t: "r", b: bytes }) } - // Hash a term + /// Hash a term pure def termHash(term: Term_t): Term_t = { // add "h" on top, which has the key [ 0 ], and attach term to it pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) @@ -131,8 +131,8 @@ module hashes { } } - // Slice the sequence represented by a term. - // We only slice raw sequences. + /// Slice a raw sequence represented by a term. + /// Non-raw sequences are returned unmodified. pure def termSlice(term: Term_t, start: int, end: int): Term_t = { pure val first = term.get([ 0 ]) if (size(keys(term)) == 1 and first.t == "r") { diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index 711ddc867..6b34f1a25 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -12,7 +12,7 @@ /// $ quint run --invariant=nonMemInv ics23trees.qnt /// $ quint run --invariant=memInv ics23trees.qnt /// -/// We expect these tests to always pass. If you the simulator reports +/// We expect these tests to always pass. If the simulator reports /// a counterexample, there must be an error somewhere. /// /// Igor Konnov, Informal Systems, 2022-2023 @@ -53,12 +53,12 @@ module treeGen { /// Compute all parents from the binary representation of the index. /// To simplify random generation of the trees, we are using - /// the binary encoding. For example, if a leaf has the index 4, + /// a binary encoding. For example, if a leaf has the index 4, /// that is, 100b, then it has the parents 3 = 10b and 1 = 1b. def parents(i) = 1.to(height).map(h => i / (2^h)).exclude(Set(0)) /// is a given key a node (inner or leaf) of a tree - def isNode(t, key) = or { + def isNode(t: TREE_T, key: int) = or { key == 1, t.leafs.keys().contains(key), t.left.keys().contains(key), @@ -179,7 +179,7 @@ module treeGen { path: path, } - /// The transition does nothing. The state was computed in Init. + /// The transition does nothing. The state was computed in `init`. action step = all { // nothing changes tree' = tree, From 60a2df4944beb174a312c28fd5a98cb77e9a0c80 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 23 Jun 2023 15:38:13 +0200 Subject: [PATCH 15/24] apply comments and fix the spec --- examples/cosmos/ics23/hashes.qnt | 23 +++++++++++++++-------- examples/cosmos/ics23/ics23.qnt | 3 ++- examples/cosmos/ics23/treeGen.qnt | 5 +++-- 3 files changed, 20 insertions(+), 11 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 24c114385..23d8cb855 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -16,7 +16,9 @@ /// we represent terms as maps that encode trees. For instance, /// the term h([ 1, 2 ] + h([ 3, 4 ])) + [ 5, 6 ] corresponds to the tree: /// -/// "h" [ 5, 6 ] +/// * +/// / \ +/// "h" [ 5, 6 ] /// / \ /// [ 1, 2 ] "h" /// / @@ -42,7 +44,7 @@ module hashes { or { len1 < len2 and w1.indices().forall(i => w1[i] == w2[i]), and { - len1 == len2, + len1 <= len2, w1.indices().exists(i => and { w1[i] < w2[i], w1.indices().forall(j => j < i implies w1[i] == w2[j]) @@ -84,6 +86,11 @@ module hashes { Map([ 0 ] -> { t: "r", b: bytes }) } + /// Is the term representing a raw term? + pure def isRaw(term: Term_t): bool = { + size(keys(term)) == 1 and term.get([0]).t == "r" + } + /// Hash a term pure def termHash(term: Term_t): Term_t = { // add "h" on top, which has the key [ 0 ], and attach term to it @@ -102,13 +109,13 @@ module hashes { pure def termConcat(left: Term_t, right: Term_t): Term_t = { pure val l = left.get([0]) pure val r = right.get([0]) - pure val isLSeq = size(keys(left)) == 1 and l.t == "r" - pure val isRSeq = size(keys(right)) == 1 and r.t == "r" - if (isLSeq and l.b == []) { + pure val isLeftRaw = isRaw(l) + pure val isRightRaw = isRaw(r) + if (isLeftRaw and l.b == []) { right - } else if (isRSeq and r.b == []) { + } else if (isRightRaw and r.b == []) { left - } else if (isLSeq and isRSeq) { + } else if (isLeftRaw and isRightRaw) { // both arguments are raw sequences, produce a single raw sequence Map([0] -> { t: "r", b: l.b.concat(r.b) }) } else { @@ -135,7 +142,7 @@ module hashes { /// Non-raw sequences are returned unmodified. pure def termSlice(term: Term_t, start: int, end: int): Term_t = { pure val first = term.get([ 0 ]) - if (size(keys(term)) == 1 and first.t == "r") { + if (isRaw(term)) { raw(first.b.slice(start, end)) } else { term diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index 07fcd5a6f..d4c99624b 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -30,7 +30,7 @@ module ics23 { type CommitmentRoot_t = Term_t type CommitmentProof_t = Term_t - // ICS23 IavlSpec has: + // ICS23 TendermintSpec has: // MinPrefixLength = 1 // MaxPrefixLength = 1 // ChildSize = 32 @@ -78,6 +78,7 @@ module ics23 { val leafHash = termHash(p.leaf.prefix // TODO: use encodeVarintProto + // https://github.com/cosmos/ics23/blob/d0edf8e9cd38f7fc1bfc4311b2814e5d2ea966e8/go/proof.go#L67 .termConcat(raw([length(p.key)])) .termConcat(raw(p.key)) .termConcat(raw([32])) diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index 6b34f1a25..ba15d9288 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -55,11 +55,12 @@ module treeGen { /// To simplify random generation of the trees, we are using /// a binary encoding. For example, if a leaf has the index 4, /// that is, 100b, then it has the parents 3 = 10b and 1 = 1b. + /// See the exact definition below. def parents(i) = 1.to(height).map(h => i / (2^h)).exclude(Set(0)) /// is a given key a node (inner or leaf) of a tree - def isNode(t: TREE_T, key: int) = or { - key == 1, + def isNode(t: TREE_T, key: int): bool = or { + key == 1, // the root t.leafs.keys().contains(key), t.left.keys().contains(key), t.right.keys().contains(key), From 4bcb8eb33f93c7d9e9e5229765b190b2b3bd423a Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 23 Jun 2023 15:46:28 +0200 Subject: [PATCH 16/24] fix lessThan --- examples/cosmos/ics23/hashes.qnt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 23d8cb855..914ada3d0 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -42,12 +42,12 @@ module hashes { pure val len1 = length(w1) pure val len2 = length(w2) or { - len1 < len2 and w1.indices().forall(i => w1[i] == w2[i]), + len1 < len2 and indices(w1).forall(i => w1[i] <= w2[i]), and { - len1 <= len2, - w1.indices().exists(i => and { + len1 == len2, + indices(w1).exists(i => and { w1[i] < w2[i], - w1.indices().forall(j => j < i implies w1[i] == w2[j]) + indices(w1).forall(j => j < i implies w1[j] == w2[j]) }) } } From de4cc26fc529f41b736c17635a9b008d817d1c9c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 Jul 2023 12:18:23 +0200 Subject: [PATCH 17/24] fix the type error in termConcat --- examples/cosmos/ics23/hashes.qnt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 914ada3d0..d1c3e8324 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -109,8 +109,8 @@ module hashes { pure def termConcat(left: Term_t, right: Term_t): Term_t = { pure val l = left.get([0]) pure val r = right.get([0]) - pure val isLeftRaw = isRaw(l) - pure val isRightRaw = isRaw(r) + pure val isLeftRaw = isRaw(left) + pure val isRightRaw = isRaw(right) if (isLeftRaw and l.b == []) { right } else if (isRightRaw and r.b == []) { From 2335cf9ff4f853f93cdae3a3e2f80f28647d3f35 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 Jul 2023 13:51:08 +0200 Subject: [PATCH 18/24] fixing tests --- examples/cosmos/ics23/hashes.qnt | 5 +++++ examples/cosmos/ics23/ics23.qnt | 19 ++++++++++--------- examples/cosmos/ics23/ics23test.qnt | 22 +++++++++++----------- 3 files changed, 26 insertions(+), 20 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index d1c3e8324..a47017e12 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -138,6 +138,11 @@ module hashes { } } + // prepend the hash with the length marker + pure def termHashWithLen(term: Term_t): Term_t = { + raw([ 32 ]).termConcat(termHash(term)) + } + /// Slice a raw sequence represented by a term. /// Non-raw sequences are returned unmodified. pure def termSlice(term: Term_t, start: int, end: int): Term_t = { diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index d4c99624b..11fdef49a 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -30,21 +30,22 @@ module ics23 { type CommitmentRoot_t = Term_t type CommitmentProof_t = Term_t - // ICS23 TendermintSpec has: - // MinPrefixLength = 1 - // MaxPrefixLength = 1 - // ChildSize = 32 + // ICS23 IavlSpec has: + // MinPrefixLength = 4 + // MaxPrefixLength = 12 + // ChildSize = 33 // // To ease spec testing, we set: - pure val MinPrefixLen = 1 - pure val MaxPrefixLen = 1 + pure val MinPrefixLen = 4 + pure val MaxPrefixLen = 12 // It is crucial to make sure that ChildSize > MaxPrefixLen - pure val ChildSize = 32 // 32 bytes in SHA256 + pure val ChildSize = 33 // 32 bytes in SHA256 + 1 byte for the length marker // Empty child is a predefined sequence that fills an absent child. - // TODO: EmptyChild is set to nil in TendermintSpec. We have 32 bytes. + // TODO: EmptyChild is set to nil in IavlSpec. We have 33 bytes. pure val EmptyChild = raw([ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, ]) type LEAF_T = { diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 7f76e89b5..10004c6bd 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -26,18 +26,18 @@ module ics23test { key: [ 5 ], value: [ 5, 6 ], leaf: { - prefix: raw([ 9, 10, 11 ]) + prefix: raw([ 9, 10, 11, 12 ]) }, path: [ - { prefix: raw([5, 6]), suffix: raw([8]) }, - { prefix: raw([5]), suffix: raw([7]) } + { prefix: raw([ 5, 6, 7, 8, 9 ]), suffix: raw([ 8 ]) }, + { prefix: raw([ 5, 6, 7, 8 ]), suffix: raw([ 7 ]) } ] }) // a map representation of the term with hashes pure val expected = Map( - [0, 0] -> { b: [5], t: "r" }, - [0, 1, 0] -> { b: [5, 6], t: "r" }, - [0, 1, 1, 0] -> { b: [9, 10, 11, 1, 5, 32], t: "r" }, + [0, 0] -> { b: [5, 6, 7, 8], t: "r" }, + [0, 1, 0] -> { b: [5, 6, 7, 8, 9], t: "r" }, + [0, 1, 1, 0] -> { b: [9, 10, 11, 12, 1, 5, 32], t: "r" }, [0, 1, 1, 1, 0] -> { b: [5, 6], t: "r" }, [0, 1, 1, 1] -> { b: [], t: "h" }, [0, 1, 1] -> { b: [], t: "h" }, @@ -51,17 +51,17 @@ module ics23test { pure val isLeftMost1Test = { assert(isLeftMost([ - { prefix: raw([1]), suffix: termHash(raw([3, 4, 5])) }, - { prefix: raw([2]), suffix: termHash(raw([3, 4, 5])) }, - { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } + { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: raw([2, 3, 4, 5]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: raw([3, 4, 5, 6]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) } pure val isLeftMost2Test = assert(isLeftMost([ { prefix: termConcat(raw([1]), EmptyChild), suffix: raw([]) }, - { prefix: raw([2]), suffix: termHash(raw([3, 4, 5])) }, - { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } + { prefix: raw([2]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: raw([3]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) pure val isLeftMost3Test = { From 3813404739afeebf69a9348364bc9100d10440d9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 Jul 2023 14:34:11 +0200 Subject: [PATCH 19/24] fix all but one test --- examples/cosmos/ics23/ics23test.qnt | 50 ++++++++++++++--------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 10004c6bd..4f161e421 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -59,48 +59,48 @@ module ics23test { pure val isLeftMost2Test = assert(isLeftMost([ - { prefix: termConcat(raw([1]), EmptyChild), suffix: raw([]) }, - { prefix: raw([2]), suffix: termHashWithLen(raw([3, 4, 5])) }, - { prefix: raw([3]), suffix: termHashWithLen(raw([3, 4, 5])) } + { prefix: termConcat(raw([ 1, 2, 3, 4 ]), EmptyChild), suffix: raw([]) }, + { prefix: raw([ 2, 3, 4, 5 ]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: raw([ 3, 4, 5, 6 ]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) pure val isLeftMost3Test = { assert(isLeftMost([ - { prefix: raw([1]), suffix: termHash(raw([3, 4, 5])) }, - { prefix: termConcat(raw([2]), EmptyChild), suffix: raw([]) }, - { prefix: raw([3]), suffix: termHash(raw([3, 4, 5])) } + { prefix: raw([ 1, 2, 3, 4 ]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: termConcat(raw([ 2, 3, 4, 5 ]), EmptyChild), suffix: raw([]) }, + { prefix: raw([3, 4, 5, 6]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) } pure val isRightMost1Test = assert(isRightMost([ - { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, - { prefix: termConcat(raw([2]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, - { prefix: termConcat(raw([3]), termHash(raw([4, 5, 6]))), suffix: raw([]) } + { prefix: termConcat(raw([1, 2, 3, 4 ]), termHashWithLen(raw([ 4, 5, 6 ]))), suffix: raw([]) }, + { prefix: termConcat(raw([2, 3, 4, 5 ]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: termConcat(raw([3, 4, 5, 6 ]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) } ])) pure val isRightMost2Test = assert(isRightMost([ - { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, - { prefix: raw([2]), suffix: EmptyChild }, - { prefix: termConcat(raw([2]), termHash(raw([3, 4, 5]))), suffix: raw([]) } + { prefix: termConcat(raw([1, 2, 3, 4]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: raw([2, 3, 4, 5]), suffix: EmptyChild }, + { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([3, 4, 5]))), suffix: raw([]) } ])) pure val isLeftStep1Test = assert(isLeftStep( - { prefix: raw([1]), suffix: termHash(raw([4, 5, 6])) }, - { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } + { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([4, 5, 6])) }, + { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([7, 8, 9]))), suffix: raw([]) } )) pure val isLeftNeighborTest = assert(isLeftNeighbor( [ - { prefix: raw([1]), suffix: termHash(raw([4, 5, 6])) }, - { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } + { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([4, 5, 6])) }, + { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([7, 8, 9]))), suffix: raw([]) } ], [ - { prefix: termConcat(raw([1]), termHash(raw([4, 5, 6]))), suffix: raw([]) }, - { prefix: termConcat(raw([2]), termHash(raw([7, 8, 9]))), suffix: raw([]) } + { prefix: termConcat(raw([1, 2, 3, 4]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) }, + { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([7, 8, 9]))), suffix: raw([]) } ] )) @@ -109,26 +109,26 @@ module ics23test { // / \ // 2:3 4:5 pure val lhash = existsCalculate({ - key: [2], value: [3], leaf: { prefix: raw([ 0 ]) }, path: [] + key: [2], value: [3], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] }) pure val rhash = existsCalculate({ - key:[4], value: [5], leaf: { prefix: raw([ 0 ]) }, path: [] + key:[4], value: [5], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] }) // the left proof pure val lproof: ExistsProof_t = { key: [ 2 ], value: [ 3 ], - leaf: { prefix: raw([ 0 ]) }, - path: [{ prefix: raw([0]), suffix: rhash }] + leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, + path: [{ prefix: raw([ 0, 1, 2, 3 ]), suffix: raw([32]).termConcat(rhash) }] } // the right proof pure val rproof: ExistsProof_t = { key: [ 4 ], value: [ 5 ], - leaf: { prefix: raw([ 0 ]) }, - path: [{ prefix: raw([0]).termConcat(lhash), suffix: raw([]) }] + leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, + path: [{ prefix: raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash), suffix: raw([ ]) }] } - pure val root = termHash(raw([0]).termConcat(lhash).termConcat(rhash)) + pure val root = termHash(raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash).termConcat(rhash)) pure val nilProof: ExistsProof_t = { key: [], value: [], leaf: { prefix: raw([]) }, path: [] } and { From ac11ff50ba16e23338c36d2516c7d3e3618929b3 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Sep 2024 11:23:59 -0300 Subject: [PATCH 20/24] Fix command on README --- examples/cosmos/ics23/README.md | 4 ++-- examples/cosmos/ics23/ics23test.qnt | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/cosmos/ics23/README.md b/examples/cosmos/ics23/README.md index a10c6ce14..e5e9bfc73 100644 --- a/examples/cosmos/ics23/README.md +++ b/examples/cosmos/ics23/README.md @@ -29,8 +29,8 @@ $ quint test ics23test.qnt non-membership invariants with the random simulator: ```sh -$ quint run --invariant=nonMemInv --max-samples=1000 ics23trees.qnt -$ quint run --invariant=memInv --max-samples=1000 ics23trees.qnt +$ quint run --invariant=nonMemInv --max-samples=1000 treeGen.qnt +$ quint run --invariant=memInv --max-samples=1000 treeGen.qnt ``` If the simulator finds a violation to the above invariants, please let us know, diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 4f161e421..a17f923cd 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -144,4 +144,4 @@ module ics23test { assert(verifyNonMembership(root, np5, [ 5 ])), } } -} \ No newline at end of file +} From c9f8ca04afc3f9a69d46f8423b5b99e6cff25a3c Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Sep 2024 15:11:48 -0300 Subject: [PATCH 21/24] Use a sum type to represent term nodes --- examples/cosmos/ics23/hashes.qnt | 82 ++++++++++++++++------------- examples/cosmos/ics23/ics23test.qnt | 20 +++---- examples/cosmos/ics23/treeGen.qnt | 6 +-- 3 files changed, 57 insertions(+), 51 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index a47017e12..07b4c8c3d 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -16,21 +16,21 @@ /// we represent terms as maps that encode trees. For instance, /// the term h([ 1, 2 ] + h([ 3, 4 ])) + [ 5, 6 ] corresponds to the tree: /// -/// * -/// / \ -/// "h" [ 5, 6 ] -/// / \ -/// [ 1, 2 ] "h" -/// / +/// * +/// / \ +/// Hash [ 5, 6 ] +/// / \ +/// [ 1, 2 ] Hash +/// / /// [ 3, 4 ] /// /// The above tree is represented as a map in Quint. Each key corresponds to a path in the tree; for example, the first root's child is [ 0 ], the second root's child is [ 1 ], the first child of [ 0 ] is [ 0, 0], etc. /// -/// Map([ 0 ] -> { t: "h", b: [] }, -/// [ 0, 0 ] -> { t: "r", b: [ 1, 2 ] }, -/// [ 0, 1 ] -> { t: "h", b: [] } ), -/// [ 0, 1, 0 ] -> { t: "r", b: [ 3, 4 ] }, -/// [ 1 ] -> { t: "r", b: [ 5, 6 ] }) +/// Map([ 0 ] -> Hash, +/// [ 0, 0 ] -> Raw([1, 2]), +/// [ 0, 1 ] -> Hash, +/// [ 0, 1, 0 ] -> Raw([ 3, 4 ]), +/// [ 1 ] -> Raw[ 5, 6 ]) /// /// Igor Konnov, Informal Systems, 2022-2023 module hashes { @@ -60,12 +60,7 @@ module hashes { } /// A tree node that represents a fragment of a term - type TERM_NODE_T = { - // node type: either "h" (for hash), or "r" (for raw sequence) - t: str, - // the bytes when t = "r", and [] when t = "h" - b: Bytes_t - } + type TERM_NODE_T = Hash | Raw(Bytes_t) /// A word is a map from a path to the term node. /// The first root's child is [ 0 ], the second root's child is [ 1 ], @@ -78,26 +73,29 @@ module hashes { // the roots' children pure val top = keys(term).filter(p => length(p) == 1).map(p => term.get(p)) - top.fold(0, (s, t) => if (t.t == "h") s + 32 else s + length(t.b)) + top.fold(0, (s, t) => match(t) { + | Hash => s + 32 + | Raw(bytes) => s + length(bytes) + }) } /// Construct the term that encodes a raw sequence of bytes pure def raw(bytes: Bytes_t): Term_t = { - Map([ 0 ] -> { t: "r", b: bytes }) + Map([ 0 ] -> Raw(bytes)) } /// Is the term representing a raw term? pure def isRaw(term: Term_t): bool = { - size(keys(term)) == 1 and term.get([0]).t == "r" + size(keys(term)) == 1 and term.get([0]) != Hash } /// Hash a term pure def termHash(term: Term_t): Term_t = { - // add "h" on top, which has the key [ 0 ], and attach term to it + // add Hash on top, which has the key [ 0 ], and attach term to it pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) paths.mapBy(p => if (p == [ 0 ]) { - { t: "h", b: [] } + Hash } else { term.get(p.slice(1, length(p))) } @@ -107,18 +105,10 @@ module hashes { /// Concatenate two terms. Special attention is paid to the case when the /// both terms are raw sequences, which requires them to be merged. pure def termConcat(left: Term_t, right: Term_t): Term_t = { - pure val l = left.get([0]) - pure val r = right.get([0]) - pure val isLeftRaw = isRaw(left) - pure val isRightRaw = isRaw(right) - if (isLeftRaw and l.b == []) { - right - } else if (isRightRaw and r.b == []) { - left - } else if (isLeftRaw and isRightRaw) { - // both arguments are raw sequences, produce a single raw sequence - Map([0] -> { t: "r", b: l.b.concat(r.b) }) - } else { + pure val l = if (isRaw(left)) left.get([0]) else Hash + pure val r = if (isRaw(right)) right.get([0]) else Hash + + pure def mergeTerms(left: Term_t, right: Term_t): Term_t = { // Merge the arguments as trees representing terms. // The number of root's children in the left term: pure val lwidth = size(keys(left).filter(p => length(p) == 1)) @@ -136,6 +126,19 @@ module hashes { } ) } + + match(l) { + | Raw(lBytes) => match(r) { + | Raw(rBytes) => + // both arguments are raw sequences, produce a single raw sequence + raw(lBytes.concat(rBytes)) + | Hash => if (lBytes == []) right else mergeTerms(left, right) + } + | Hash => match(r) { + | Raw(rBytes) => if (rBytes == []) left else mergeTerms(left, right) + | Hash => mergeTerms(left, right) + } + } } // prepend the hash with the length marker @@ -146,11 +149,14 @@ module hashes { /// Slice a raw sequence represented by a term. /// Non-raw sequences are returned unmodified. pure def termSlice(term: Term_t, start: int, end: int): Term_t = { - pure val first = term.get([ 0 ]) - if (isRaw(term)) { - raw(first.b.slice(start, end)) - } else { + if (size(keys(term)) != 1) { term + } else { + pure val first = term.get([ 0 ]) + match(first) { + | Raw(bytes) => raw(bytes.slice(start, end)) + | _ => term + } } } } diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index a17f923cd..6f0eca13b 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -35,16 +35,16 @@ module ics23test { }) // a map representation of the term with hashes pure val expected = Map( - [0, 0] -> { b: [5, 6, 7, 8], t: "r" }, - [0, 1, 0] -> { b: [5, 6, 7, 8, 9], t: "r" }, - [0, 1, 1, 0] -> { b: [9, 10, 11, 12, 1, 5, 32], t: "r" }, - [0, 1, 1, 1, 0] -> { b: [5, 6], t: "r" }, - [0, 1, 1, 1] -> { b: [], t: "h" }, - [0, 1, 1] -> { b: [], t: "h" }, - [0, 1, 2] -> { b: [8], t: "r" }, - [0, 1] -> { b: [], t: "h" }, - [0, 2] -> { b: [7], t: "r" }, - [0] -> { b: [], t: "h" } + [0, 0] -> Raw([5, 6, 7, 8]), + [0, 1, 0] -> Raw([5, 6, 7, 8, 9]), + [0, 1, 1, 0] -> Raw([9, 10, 11, 12, 1, 5, 32]), + [0, 1, 1, 1, 0] -> Raw([5, 6]), + [0, 1, 1, 1] -> Hash, + [0, 1, 1] -> Hash, + [0, 1, 2] -> Raw([8]), + [0, 1] -> Hash, + [0, 2] -> Raw([7]), + [0] -> Hash ) assert(expected == result) } diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index ba15d9288..bb4b86be9 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -9,8 +9,8 @@ /// To execute advanced PBT-like tests for 1000 runs in the simulator, /// type the following: /// -/// $ quint run --invariant=nonMemInv ics23trees.qnt -/// $ quint run --invariant=memInv ics23trees.qnt +/// $ quint run --invariant=nonMemInv treeGen.qnt +/// $ quint run --invariant=memInv treeGen.qnt /// /// We expect these tests to always pass. If the simulator reports /// a counterexample, there must be an error somewhere. @@ -295,4 +295,4 @@ module treeGen { /// check this property to produce an example of where NonMemInv is violated val nonMemExample = not(nonMemInv) -} \ No newline at end of file +} From f2f5e2d740023478b8925f63fa56739a0a6c41d9 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 20 Dec 2024 08:59:41 -0300 Subject: [PATCH 22/24] Refactor and generalize to any spec --- examples/cosmos/ics23/hashes.qnt | 35 ++-- examples/cosmos/ics23/ics23.qnt | 289 +++++++++++++++------------- examples/cosmos/ics23/ics23test.qnt | 117 ++++++----- examples/cosmos/ics23/treeGen.qnt | 41 ++-- examples/spells/basicSpells.qnt | 22 +++ 5 files changed, 279 insertions(+), 225 deletions(-) diff --git a/examples/cosmos/ics23/hashes.qnt b/examples/cosmos/ics23/hashes.qnt index 07b4c8c3d..20a2abc3f 100644 --- a/examples/cosmos/ics23/hashes.qnt +++ b/examples/cosmos/ics23/hashes.qnt @@ -35,10 +35,12 @@ /// Igor Konnov, Informal Systems, 2022-2023 module hashes { /// A sequence of bytes is simply a list of integers - type Bytes_t = List[int] + type Bytes = List[int] + pure val Hash256_ZERO = + raw([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) /// compare two lists of integers (e.g., bytes) lexicographically - pure def lessThan(w1: Bytes_t, w2: Bytes_t): bool = { + pure def lessThan(w1: Bytes, w2: Bytes): bool = { pure val len1 = length(w1) pure val len2 = length(w2) or { @@ -53,23 +55,17 @@ module hashes { } } - /// Returns true iff `w` is the nil value. - /// In our spec, nil is equivalent to the empty list. - pure def isNil(w: Bytes_t): bool = { - w == [] - } - /// A tree node that represents a fragment of a term - type TERM_NODE_T = Hash | Raw(Bytes_t) + type TERM_NODE_T = Hash | Raw(Bytes) /// A word is a map from a path to the term node. /// The first root's child is [ 0 ], the second root's child is [ 1 ], /// the first child of [ 0 ] is [ 0, 0], etc. - type Term_t = Bytes_t -> TERM_NODE_T + type Term = Bytes -> TERM_NODE_T /// Compute term length in bytes, /// assuming that a hash occupies 32 bytes (as SHA256 does) - pure def termLen(term: Term_t): int = { + pure def termLen(term: Term): int = { // the roots' children pure val top = keys(term).filter(p => length(p) == 1).map(p => term.get(p)) @@ -80,17 +76,17 @@ module hashes { } /// Construct the term that encodes a raw sequence of bytes - pure def raw(bytes: Bytes_t): Term_t = { + pure def raw(bytes: Bytes): Term = { Map([ 0 ] -> Raw(bytes)) } /// Is the term representing a raw term? - pure def isRaw(term: Term_t): bool = { + pure def isRaw(term: Term): bool = { size(keys(term)) == 1 and term.get([0]) != Hash } /// Hash a term - pure def termHash(term: Term_t): Term_t = { + pure def termHash(term: Term): Term = { // add Hash on top, which has the key [ 0 ], and attach term to it pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p))) paths.mapBy(p => @@ -104,11 +100,11 @@ module hashes { /// Concatenate two terms. Special attention is paid to the case when the /// both terms are raw sequences, which requires them to be merged. - pure def termConcat(left: Term_t, right: Term_t): Term_t = { + pure def termConcat(left: Term, right: Term): Term = { pure val l = if (isRaw(left)) left.get([0]) else Hash pure val r = if (isRaw(right)) right.get([0]) else Hash - pure def mergeTerms(left: Term_t, right: Term_t): Term_t = { + pure def mergeTerms(left: Term, right: Term): Term = { // Merge the arguments as trees representing terms. // The number of root's children in the left term: pure val lwidth = size(keys(left).filter(p => length(p) == 1)) @@ -141,14 +137,9 @@ module hashes { } } - // prepend the hash with the length marker - pure def termHashWithLen(term: Term_t): Term_t = { - raw([ 32 ]).termConcat(termHash(term)) - } - /// Slice a raw sequence represented by a term. /// Non-raw sequences are returned unmodified. - pure def termSlice(term: Term_t, start: int, end: int): Term_t = { + pure def termSlice(term: Term, start: int, end: int): Term = { if (size(keys(term)) != 1) { term } else { diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index 26eafe21a..c6335f75b 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -6,74 +6,70 @@ // For the implementation of ICS23, see: // https://github.com/confio/ics23/ // -// We still have to parameterize the spec with the data structure parameters -// such as MinPrefixLen, MaxPrefixLen, ChildSize, and hash. -// For the moment, the main goal of this spec is to understand the algorithm -// and test it with the simulator. -// // Igor Konnov, Informal Systems, 2022-2023 +// Josef Widder, Informal Systems, 2024 +// Aleksandar Ignjatijevic, Informal Systems, 2024 +// Gabriela Moreira, Informal Systems, 2024 // This is a specification of the membership and non-membership proofs -// of ICS23 for IAVL trees: +// of ICS23: // // https://github.com/confio/ics23/blob/master/go/proof.go module ics23 { + import basicSpells.* from "../../spells/basicSpells" import hashes.* from "./hashes" - // ICS23 proof checking for IavlSpec. + // ICS23 proof checking. // In contrast to the ICS23 implementation, we specialize it to binary trees: // https://github.com/confio/ics23/tree/master/go + type InnerSpec = { + minPrefixLength: int, + maxPrefixLength: int, + childSize: int, + emptyChild: Term, + childOrder: List[int], + } - // type aliases for readability - type Key_t = Bytes_t - type Value_t = Bytes_t - type CommitmentRoot_t = Term_t - type CommitmentProof_t = Term_t + pure val IavlSpec: InnerSpec = { + minPrefixLength: 4, + maxPrefixLength: 12, + childSize: 33, + emptyChild: Hash256_ZERO, + childOrder: [0, 1] + } - // ICS23 IavlSpec has: - // MinPrefixLength = 4 - // MaxPrefixLength = 12 - // ChildSize = 33 - // - // To ease spec testing, we set: - pure val MinPrefixLen = 4 - pure val MaxPrefixLen = 12 - // It is crucial to make sure that ChildSize > MaxPrefixLen - pure val ChildSize = 33 // 32 bytes in SHA256 + 1 byte for the length marker - // Empty child is a predefined sequence that fills an absent child. - // TODO: EmptyChild is set to nil in IavlSpec. We have 33 bytes. - pure val EmptyChild = raw([ - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, - ]) + type Padding = { + minPrefix: int, + maxPrefix: int, + suffix: int, + } - type LEAF_T = { + type LeafOp = { // The implementation additionally stores hashing and length functions: // hash, prehashKey, prehashValue, len. Since we fix the spec to IAVL, // we do not have to carry them around. - prefix: Term_t + prefix: Term } - type INNER_T = { + type InnerOp = { // The implementation additionally stores the hashing function. // Since we fix the spec to IAVL, we do not have to carry it around. - prefix: Term_t, - suffix: Term_t + prefix: Term, + suffix: Term } /// a proof of existence of (key, value) - type ExistsProof_t = { - key: Key_t, value: Value_t, leaf: LEAF_T, path: List[INNER_T] + type ExistenceProof = { + key: Bytes, value: Bytes, leaf: LeafOp, path: List[InnerOp] } /// a proof of non-existence of a key - type NonExistsProof_t = { - key: Key_t, left: ExistsProof_t, right: ExistsProof_t + type NonExistenceProof = { + key: Bytes, left: Option[ExistenceProof], right: Option[ExistenceProof] } /// calculate a hash from an exists proof - def existsCalculate(p: ExistsProof_t): CommitmentProof_t = { + def existsCalculate(p: ExistenceProof): Term = { // This is how the leaf hash is computed. // Notice that the key is not hashed. val leafHash = @@ -102,8 +98,8 @@ module ics23 { /// proof is an ExistenceProof for the given key and value AND /// calculating the root for the ExistenceProof matches /// the provided CommitmentRoot - def verifyMembership(root: CommitmentRoot_t, - proof: ExistsProof_t, key: Key_t, value: Value_t): bool = { + def verifyMembership(root: Term, + proof: ExistenceProof, key: Bytes, value: Bytes): bool = { // TODO: specify Decompress // TODO: specify the case of CommitmentProof_Batch // TODO: CheckAgainstSpec ensures that the proof can be verified @@ -112,110 +108,128 @@ module ics23 { } /// checks if an op has the expected padding - def hasPadding(inner: INNER_T, - minPrefixLen: int, maxPrefixLen: int, suffixLen: int): bool = and { - termLen(inner.prefix) >= minPrefixLen, - termLen(inner.prefix) <= maxPrefixLen, - // When inner turns left, suffixLen == ChildSize, + pure def hasPadding(op: InnerOp, pad: Padding): bool = and { + op.prefix.termLen() >= pad.minPrefix, + op.prefix.termLen() <= pad.maxPrefix, + // When inner turns left, suffixLen == child_size, // that is, we store the hash of the right child in the suffix. // When inner turns right, suffixLen == 0, // that is, we store the hash of the left child in the prefix. - termLen(inner.suffix) == suffixLen + op.suffix.termLen() == pad.suffix, } - /// This will look at the proof and determine which order it is... - /// So we can see if it is branch 0, 1, 2 etc... to determine neighbors - /// https://github.com/confio/ics23/blob/a4daeb4c24ce1be827829c0841446abc690c4f11/go/proof.go#L400-L411 - def orderFromPadding(inner: INNER_T): (int, bool) = { - // Specialize orderFromPadding to IavlSpec: - // ChildOrder = { 0, 1 } - // branch = 0: minp, maxp, suffix = MinPrefixLen, MaxPrefixLen, ChildSize - // branch = 1: minp, maxp, suffix = - // ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 - if (hasPadding(inner, MinPrefixLen, MaxPrefixLen, ChildSize)) { - // the node turns left - (0, true) - } else if (hasPadding(inner, ChildSize + MinPrefixLen, - ChildSize + MaxPrefixLen, 0)) { - // the node turns right - (1, true) - } else { - // error - (0, false) + pure def getPadding(spec: InnerSpec, branch: int): Option[Padding] = { + match spec.childOrder.findFirst(x => x == branch) { + | Some(idx) => { + pure val prefix = idx * spec.childSize + pure val suffix = spec.childSize * (spec.childOrder.length() - 1 - idx) + Some({ + minPrefix: prefix + spec.minPrefixLength, + maxPrefix: prefix + spec.maxPrefixLength, + suffix: suffix, + }) + } + | None => None } } + /// This will look at the proof and determine which order it is. + /// So we can see if it is branch 0, 1, 2 etc... to determine neighbors + pure def orderFromPadding(spec: InnerSpec, op: InnerOp): Option[int] = { + pure val len = spec.childOrder.length() + range(0, len).find_first(branch => { + match getPadding(spec, branch) { + | Some(padding) => hasPadding(op, padding) + | None => false // This should actually early return but this is impossible for our InnerSpec + } + }) + } + /// leftBranchesAreEmpty returns true if the padding bytes correspond to all /// empty siblings on the left side of a branch, ie. it's a valid placeholder /// on a leftmost path - def leftBranchesAreEmpty(inner: INNER_T): bool = and { - // the case of leftBranches == 0 returns false - val order = orderFromPadding(inner) - order._2 and order._1 != 0, - // the remaining case is leftBranches == 1, see orderFromPadding - // actualPrefix = len(inner.prefix) - 33 - termLen(inner.prefix) >= ChildSize, - // getPosition(0) returns 0 - val fromIndex = termLen(inner.prefix) - ChildSize - termSlice(inner.prefix, fromIndex, fromIndex + ChildSize) == EmptyChild + def leftBranchesAreEmpty(spec: InnerSpec, op: InnerOp): bool = { + pure val idx = orderFromPadding(spec, op) + pure val leftBranches = idx.unwrap() + and { + leftBranches != 0, + op.prefix.termLen() >= leftBranches * spec.childSize, + pure val actualPrefix = op.prefix.termLen() - leftBranches * spec.childSize + 0.to(leftBranches - 1).forall(i => { + pure val idx = spec.childOrder.findFirst(x => x == i).unwrap() + val from_index = actualPrefix + idx * spec.childSize + spec.emptyChild == op.prefix.termSlice(from_index, from_index + spec.childSize) + }) + } } /// IsLeftMost returns true if this is the left-most path in the tree, /// excluding placeholder (empty child) nodes - def isLeftMost(path: List[INNER_T]): bool = { - // Calls getPadding(0) => idx = 0, prefix = 0. - // We specialize the constants to IavlSpec. - path.indices().forall(i => - val pathStep = path[i] - or { - // the path goes left - hasPadding(pathStep, MinPrefixLen, MaxPrefixLen, ChildSize), - // the path goes right, but the left child is empty (a gap) - leftBranchesAreEmpty(pathStep) + def isLeftMost(spec: InnerSpec, path: List[InnerOp]): bool = { + match getPadding(spec, 0) { + | Some(pad) => { + path.indices().forall(i => + val step = path[i] + or { + // the path goes left + hasPadding(step, pad), + // the path goes right, but the left child is empty (a gap) + leftBranchesAreEmpty(spec, step) + } + ) } - ) + | None => false + } } /// rightBranchesAreEmpty returns true if the padding bytes correspond /// to all empty siblings on the right side of a branch, /// i.e. it's a valid placeholder on a rightmost path - def rightBranchesAreEmpty(inner: INNER_T): bool = and { - // the case of rightBranches == 0 returns false - val order = orderFromPadding(inner) - order._2 and order._1 != 1, - // the remaining case is rightBranches == 1, see orderFromPadding - termLen(inner.suffix) == ChildSize, - // getPosition(0) returns 0, hence, from == 0 - inner.suffix == EmptyChild + def rightBranchesAreEmpty(spec: InnerSpec, op: InnerOp): bool = and { + val idx = orderFromPadding(spec, op) + pure val rightBranches = spec.childOrder.length() - 1 - idx.unwrap() + and { + idx != None, + rightBranches != 0, + op.suffix.termLen() == spec.childSize, + 0.to(rightBranches - 1).forall(i => { + pure val idx = spec.childOrder.findFirst(x => x == i).unwrap() + val from_index = idx * spec.childSize + spec.emptyChild == op.suffix.termSlice(from_index, from_index + spec.childSize) + }) + } } /// IsRightMost returns true if this is the left-most path in the tree, /// excluding placeholder (empty child) nodes - def isRightMost(path: List[INNER_T]): bool = { - // Specialize to IavlSpec - // Calls getPadding(1) => minPrefix, maxPrefix, - // suffix = ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0 - path.indices().forall(i => - val pathStep = path[i] - or { - // the path goes right - hasPadding(pathStep, ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0), - // the path goes left, but the right child is empty (a gap) - rightBranchesAreEmpty(pathStep) + def isRightMost(spec: InnerSpec, path: List[InnerOp]): bool = { + pure val idx = spec.childOrder.length() - 1 + match getPadding(spec, idx) { + | Some(pad) => { + path.indices().forall(i => + val step = path[i] + or { + // the path goes right + hasPadding(step, pad), + // the path goes left, but the right child is empty (a gap) + rightBranchesAreEmpty(spec, step) + } + ) } - ) + | None => false + } } /// isLeftStep assumes left and right have common parents /// checks if left is exactly one slot to the left of right - def isLeftStep(left: INNER_T, right: INNER_T): bool = { + def isLeftStep(spec: InnerSpec, left: InnerOp, right: InnerOp): bool = { // 'left' turns left, and 'right' turns right - val lorder = orderFromPadding(left) - val rorder = orderFromPadding(right) + val lorder = orderFromPadding(spec, left) + val rorder = orderFromPadding(spec, right) and { - lorder._2, - rorder._2, - rorder._1 == lorder._1 + 1 + lorder != None, + rorder != None, + rorder.unwrap() == lorder.unwrap() + 1 } } @@ -227,7 +241,7 @@ module ics23 { /// Validate that LPath[len-1] is the left neighbor of RPath[len-1]. /// For step in LPath[0..len-1], validate step is right-most node. /// For step in RPath[0..len-1], validate step is left-most node. - def isLeftNeighbor(lpath: List[INNER_T], rpath: List[INNER_T]): bool = { + def isLeftNeighbor(spec: InnerSpec, lpath: List[InnerOp], rpath: List[InnerOp]): bool = { // count common tail (from end, near root) // cut the left and right paths lpath.indices().exists(li => @@ -252,11 +266,11 @@ module ics23 { // of the same tree node: // the left one stores the hash of the right one, whereas // the right one stores the hash of the left one. - isLeftStep(lpath[li], rpath[ri]), + isLeftStep(spec, lpath[li], rpath[ri]), // left and right are remaining children below the split, // ensure left child is the rightmost path, and visa versa - isRightMost(lpath.slice(0, li)), - isLeftMost(rpath.slice(0, ri)), + isRightMost(spec, lpath.slice(0, li)), + isLeftMost(spec, rpath.slice(0, ri)), }) ) } @@ -266,30 +280,37 @@ module ics23 { /// both left and right sub-proofs are valid existence proofs (see above) or nil, /// left and right proofs are neighbors (or left/right most if one is nil), /// provided key is between the keys of the two proofs - def verifyNonMembership(root: CommitmentRoot_t, - np: NonExistsProof_t, key: Key_t): bool = and { - // getNonExistProofForKey - isNil(np.left.key) or lessThan(np.left.key, key), - isNil(np.right.key) or lessThan(key, np.right.key), + def verifyNonMembership(root: Term, + np: NonExistenceProof, key: Bytes): bool = and { // implicit assumption, missing in the code: // https://github.com/informalsystems/ics23-audit/issues/14 np.key == key, // Verify - not(isNil(np.left.key)) or not(isNil(np.right.key)), - isNil(np.left.key) or and { - verify(np.left, root, np.left.key, np.left.value), - lessThan(np.left.key, key), + np.left != None or np.right != None, + np.left != None implies { + pure val left = np.left.unwrap() + and { + lessThan(left.key, key), + verify(left, root, left.key, left.value), + lessThan(left.key, key), + } }, - isNil(np.right.key) or and { - verify(np.right, root, np.right.key, np.right.value), - lessThan(key, np.right.key), + np.right != None implies { + pure val right = np.right.unwrap() + and { + lessThan(key, right.key), + verify(right, root, right.key, right.value), + lessThan(key, right.key), + } }, - if (isNil(np.left.key)) { - isLeftMost(np.right.path) - } else if (isNil(np.right.key)) { - isRightMost(np.left.path) + + pure val spec = IavlSpec + if (np.left == None) { + isLeftMost(spec, np.right.unwrap().path) + } else if (np.right == None) { + isRightMost(spec, np.left.unwrap().path) } else { - isLeftNeighbor(np.left.path, np.right.path) + isLeftNeighbor(spec, np.left.unwrap().path, np.right.unwrap().path) } } } diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 6f0eca13b..076e0caab 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -6,9 +6,15 @@ /// /// Igor Konnov, Informal Systems, 2022-2023 module ics23test { + import basicSpells.* from "../../spells/basicSpells" import hashes.* from "./hashes" import ics23.* from "./ics23" + // prepend the hash with the length marker + pure def termHashWithLen(term: Term): Term = { + raw([ 32 ]).termConcat(termHash(term)) + } + // test data val a = [5] val b = [6] @@ -50,7 +56,7 @@ module ics23test { } pure val isLeftMost1Test = { - assert(isLeftMost([ + assert(isLeftMost(IavlSpec, [ { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([3, 4, 5])) }, { prefix: raw([2, 3, 4, 5]), suffix: termHashWithLen(raw([3, 4, 5])) }, { prefix: raw([3, 4, 5, 6]), suffix: termHashWithLen(raw([3, 4, 5])) } @@ -58,42 +64,44 @@ module ics23test { } pure val isLeftMost2Test = - assert(isLeftMost([ - { prefix: termConcat(raw([ 1, 2, 3, 4 ]), EmptyChild), suffix: raw([]) }, - { prefix: raw([ 2, 3, 4, 5 ]), suffix: termHashWithLen(raw([3, 4, 5])) }, - { prefix: raw([ 3, 4, 5, 6 ]), suffix: termHashWithLen(raw([3, 4, 5])) } + assert(isLeftMost(IavlSpec, [ + { prefix: termConcat(raw([ 1, 2, 3, 4, 5 ]), Hash256_ZERO), suffix: raw([]) }, + { prefix: raw([ 2, 3, 4, 5, 6 ]), suffix: termHashWithLen(raw([3, 4, 5])) }, + { prefix: raw([ 3, 4, 5, 6, 7 ]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) pure val isLeftMost3Test = { - assert(isLeftMost([ + assert(isLeftMost(IavlSpec, [ { prefix: raw([ 1, 2, 3, 4 ]), suffix: termHashWithLen(raw([3, 4, 5])) }, - { prefix: termConcat(raw([ 2, 3, 4, 5 ]), EmptyChild), suffix: raw([]) }, + { prefix: termConcat(raw([ 2, 3, 4, 5 ]), Hash256_ZERO), suffix: raw([]) }, { prefix: raw([3, 4, 5, 6]), suffix: termHashWithLen(raw([3, 4, 5])) } ])) } pure val isRightMost1Test = - assert(isRightMost([ + assert(isRightMost(IavlSpec, [ { prefix: termConcat(raw([1, 2, 3, 4 ]), termHashWithLen(raw([ 4, 5, 6 ]))), suffix: raw([]) }, { prefix: termConcat(raw([2, 3, 4, 5 ]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) }, { prefix: termConcat(raw([3, 4, 5, 6 ]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) } ])) pure val isRightMost2Test = - assert(isRightMost([ + assert(isRightMost(IavlSpec, [ { prefix: termConcat(raw([1, 2, 3, 4]), termHashWithLen(raw([4, 5, 6]))), suffix: raw([]) }, - { prefix: raw([2, 3, 4, 5]), suffix: EmptyChild }, + { prefix: raw([2, 3, 4, 5]), suffix: Hash256_ZERO }, { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([3, 4, 5]))), suffix: raw([]) } ])) pure val isLeftStep1Test = assert(isLeftStep( + IavlSpec, { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([4, 5, 6])) }, { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([7, 8, 9]))), suffix: raw([]) } )) pure val isLeftNeighborTest = assert(isLeftNeighbor( + IavlSpec, [ { prefix: raw([1, 2, 3, 4]), suffix: termHashWithLen(raw([4, 5, 6])) }, { prefix: termConcat(raw([2, 3, 4, 5]), termHashWithLen(raw([7, 8, 9]))), suffix: raw([]) } @@ -104,44 +112,55 @@ module ics23test { ] )) - pure val verifyNonMembershipTest = { - // * - // / \ - // 2:3 4:5 - pure val lhash = existsCalculate({ - key: [2], value: [3], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] - }) - pure val rhash = existsCalculate({ - key:[4], value: [5], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] - }) - // the left proof - pure val lproof: ExistsProof_t = { - key: [ 2 ], - value: [ 3 ], - leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, - path: [{ prefix: raw([ 0, 1, 2, 3 ]), suffix: raw([32]).termConcat(rhash) }] - } - // the right proof - pure val rproof: ExistsProof_t = { - key: [ 4 ], - value: [ 5 ], - leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, - path: [{ prefix: raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash), suffix: raw([ ]) }] - } - pure val root = termHash(raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash).termConcat(rhash)) - pure val nilProof: ExistsProof_t = - { key: [], value: [], leaf: { prefix: raw([]) }, path: [] } - and { - pure val np1 = { key: [1], left: nilProof, right: lproof } - assert(verifyNonMembership(root, np1, [ 1 ])), - pure val np2 = { key: [2], left: lproof, right: rproof } - assert(not(verifyNonMembership(root, np2, [ 2 ]))), - pure val np3 = { key: [3], left: lproof, right: rproof } - assert(verifyNonMembership(root, np3, [ 3 ])), - pure val np4 = { key: [2], left: lproof, right: rproof } - assert(not(verifyNonMembership(root, np4, [ 4 ]))), - pure val np5 = { key: [5], left: rproof, right: nilProof } - assert(verifyNonMembership(root, np5, [ 5 ])), - } + + // Test setup to verify non membership + // * + // / \ + // 2:3 4:5 + pure val lhash = existsCalculate({ + key: [2], value: [3], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] + }) + pure val rhash = existsCalculate({ + key: [4], value: [5], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] + }) + // the left proof + pure val lproof: ExistenceProof = { + key: [ 2 ], + value: [ 3 ], + leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, + path: [{ prefix: raw([ 0, 1, 2, 3 ]), suffix: raw([32]).termConcat(rhash) }] + } + // the right proof + pure val rproof: ExistenceProof = { + key: [ 4 ], + value: [ 5 ], + leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, + path: [{ prefix: raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash), suffix: raw([ ]) }] + } + pure val root = termHash(raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash).termConcat(rhash)) + + run verifyNonMembership1Test = { + pure val np1 = { key: [1], left: None, right: Some(lproof) } + assert(verifyNonMembership(root, np1, [ 1 ])) + } + + run verifyNonMembership2Test = { + pure val np2 = { key: [2], left: Some(lproof), right: Some(rproof) } + assert(not(verifyNonMembership(root, np2, [ 2 ]))) + } + + run verifyNonMembership3Test = { + pure val np3 = { key: [3], left: Some(lproof), right: Some(rproof) } + assert(verifyNonMembership(root, np3, [ 3 ])) + } + + run verifyNonMembership4Test = { + pure val np4 = { key: [2], left: Some(lproof), right: Some(rproof) } + assert(not(verifyNonMembership(root, np4, [ 4 ]))) + } + + run verifyNonMembership5Test = { + pure val np5 = { key: [5], left: Some(rproof), right: None } + assert(verifyNonMembership(root, np5, [ 5 ])) } } diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index bb4b86be9..c9ebdd111 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -17,6 +17,7 @@ /// /// Igor Konnov, Informal Systems, 2022-2023 module treeGen { + import basicSpells.* from "../../spells/basicSpells" import hashes.* from "./hashes" import ics23.* from "./ics23" @@ -27,18 +28,18 @@ module treeGen { /// that it actually defines a binary tree. /// This is in contrast to the typical data structures in /// programming languages. - type TREE_T = { + type Tree = { // every leaf has a key and value assigned - leafs: int -> { key: Bytes_t, value: Bytes_t }, + leafs: int -> { key: Bytes, value: Bytes }, // intermediate nodes have left and/or right children left: int -> int, right: int -> int } /// the tree generated so far - var tree: TREE_T + var tree: Tree /// the node hashes - var nodeHashes: int -> Term_t + var nodeHashes: int -> Term /// the keys to use for non-membership proofs var leftKey: int var rightKey: int @@ -59,7 +60,7 @@ module treeGen { def parents(i) = 1.to(height).map(h => i / (2^h)).exclude(Set(0)) /// is a given key a node (inner or leaf) of a tree - def isNode(t: TREE_T, key: int): bool = or { + def isNode(t: Tree, key: int): bool = or { key == 1, // the root t.leafs.keys().contains(key), t.left.keys().contains(key), @@ -70,7 +71,7 @@ module treeGen { def computeHashes(t) = { // compute the hash of a single node, assuming that the children's // nodeHashes have been computed - def putNodeHash(hashMap: int -> Term_t, key: int): (int -> Term_t) = { + def putNodeHash(hashMap: int -> Term, key: int): (int -> Term) = { val h = if (t.leafs.keys().contains(key)) { // simply use existsCalculate on the leaf @@ -84,7 +85,7 @@ module treeGen { if (childMap.keys().contains(key)) { hashMap.get(childMap.get(key)) } else { - EmptyChild + Hash256_ZERO } // hash the prefix ([0]) and the hash of the children termHash(raw([0]) @@ -145,7 +146,7 @@ module treeGen { } /// convert a tree leaf to an exists proof - def leafToExistsProof(key: int): ExistsProof_t = + def leafToExistsProof(key: int): ExistenceProof = val value = tree.leafs.get(key).value // encode all intermediate nodes upwards val path = range(1, height + 1) @@ -159,7 +160,7 @@ module treeGen { if (childMap.keys().contains(parent)) { nodeHashes.get(childMap.get(parent)) } else { - EmptyChild + Hash256_ZERO } // depending on whether the node is going to left or right, // push the hashes in the prefix and the suffix @@ -221,8 +222,8 @@ module treeGen { // if the input key belongs to the leafs, // we should not be able to disprove its membership inputKey.in(tree.leafs.keys()), - val nproof = { key: [inputKey], left: lproof, right: rproof } - val root = existsCalculate(lproof) + val nproof: NonExistenceProof = { key: [inputKey], left: lproof, right: rproof } + val root = if (lproof != None) existsCalculate(lproof.unwrap()) else existsCalculate(rproof.unwrap()) not(verifyNonMembership(root, nproof, [inputKey])) } @@ -231,7 +232,7 @@ module treeGen { // unless the choice of the keys is bad not(inputKey.in(tree.leafs.keys())), val nproof = { key: [inputKey], left: lproof, right: rproof } - val root = existsCalculate(lproof) + val root = if (lproof != None) existsCalculate(lproof.unwrap()) else existsCalculate(rproof.unwrap()) val noKeyInTheMiddle = and { // there is no leaf between leftKey and rightKey tree.leafs.keys().forall(k => k <= leftKey or k >= rightKey), @@ -244,14 +245,14 @@ module treeGen { def nonMemberLeft(lproof, rproof) = and { // the input key is to the left - isNil(lproof.key), + lproof == None, // non-membership is true when the right key is left-most and { tree.leafs.keys().forall(k => rightKey <= k), inputKey < rightKey, } iff and { // or there is a proof - val root = existsCalculate(rproof) + val root = existsCalculate(rproof.unwrap()) val nproof = { key: [inputKey], left: lproof, right: rproof } verifyNonMembership(root, nproof, [inputKey]) } @@ -259,14 +260,14 @@ module treeGen { def nonMemberRight(lproof, rproof) = and { // the input key is to the right - isNil(rproof.key), + rproof == None, // non-membership is true when the left key is the right-most and { tree.leafs.keys().forall(k => (k <= leftKey)), inputKey > leftKey, } iff and { // or there is a proof - val root = existsCalculate(lproof) + val root = existsCalculate(lproof.unwrap()) val nproof = { key: [inputKey], left: lproof, right: rproof } verifyNonMembership(root, nproof, [inputKey]) } @@ -277,9 +278,9 @@ module treeGen { val nonMemInv = def proofOrNil(key) = { if (tree.leafs.keys().contains(key)) - leafToExistsProof(key) + Some(leafToExistsProof(key)) else - { key: [], value: [], leaf: { prefix: raw([]) }, path: [] } + None } val lproof = proofOrNil(leftKey) val rproof = proofOrNil(rightKey) @@ -289,8 +290,8 @@ module treeGen { nonMemberLeft(lproof, rproof), nonMemberRight(lproof, rproof), // trivial cases: - inputKey < rightKey and not(isNil(lproof.key)), - inputKey > leftKey and not(isNil(rproof.key)), + inputKey < rightKey and lproof != None, + inputKey > leftKey and rproof != None, } /// check this property to produce an example of where NonMemInv is violated diff --git a/examples/spells/basicSpells.qnt b/examples/spells/basicSpells.qnt index 1022b49da..c0e54fe23 100644 --- a/examples/spells/basicSpells.qnt +++ b/examples/spells/basicSpells.qnt @@ -328,9 +328,31 @@ module basicSpells { /// - @param f: a function that takes an element of the list and returns a boolean /// - @returns the first element of `l` that satisfies `f`, or None pure def findFirst(l, f) = l.foldl(None, (a, i) => if (a == None and f(i)) Some(i) else a) + // FIXME: #1560 (remove the copy when fixed) + pure def find_first(l, f) = l.foldl(None, (a, i) => if (a == None and f(i)) Some(i) else a) run findFirstTest = all { assert(findFirst([1, 2, 3], x => x > 1) == Some(2)), assert(findFirst([1, 2, 3], x => x == 4) == None), } + + pure def unwrap(value: Option[a]): a = { + match value { + | None => Map().get(value) + | Some(x) => x + } + } + + pure def safeGet(m: a -> b, k: a): Option[b] = { + if (m.has(k)) Some(m.get(k)) else None + } + + pure def filterMap(s: Set[a], f: (a) => Option[b]): Set[b] = { + s.fold(Set(), (acc, e) => { + match f(e) { + | Some(x) => acc.union(Set(x)) + | None => acc + } + }) + } } From 1115a514391b21d82483ce5078bf64746e72d1da Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 20 Dec 2024 16:12:32 -0300 Subject: [PATCH 23/24] Fix proof generation --- examples/cosmos/ics23/treeGen.qnt | 44 ++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 16 deletions(-) diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index c9ebdd111..9b95844fc 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -81,7 +81,7 @@ module treeGen { }) } else { // an inner node, assuming that the children nodeHashes were computed - def hashOrEmpty(childMap) = + def hashOrZeroes(childMap) = if (childMap.keys().contains(key)) { hashMap.get(childMap.get(key)) } else { @@ -89,8 +89,8 @@ module treeGen { } // hash the prefix ([0]) and the hash of the children termHash(raw([0]) - .termConcat(hashOrEmpty(t.left)) - .termConcat(hashOrEmpty(t.right))) + .termConcat(hashOrZeroes(t.left)) + .termConcat(hashOrZeroes(t.right))) } // store the hash hashMap.put(key, h) @@ -112,12 +112,11 @@ module treeGen { val leafKeys = idx.filter(i => idx.forall(j => not(i.in(parents(j))))) // compute all parents val allParents = leafKeys.map(i => parents(i)).flatten() + val allNodes = allParents.union(leafKeys) // all intermediate nodes that have a left successor - val leftKeys = allParents.filter(i => - allParents.union(leafKeys).exists(j => 2 * i == j)) + val leftKeys = allParents.filter(i => allNodes.contains(2 * i)) // all intermediate nodes that have a right successor - val rightKeys = allParents.filter(i => - allParents.union(leafKeys).exists(j => 2 * i + 1 == j)) + val rightKeys = allParents.filter(i => allNodes.contains(2 * i + 1)) // left mapping val left = leftKeys.mapBy(i => 2 * i) // right mapping @@ -134,7 +133,7 @@ module treeGen { tree' = t, nodeHashes' = computeHashes(t), }, - // pick arbitrary left and right keys for non-membership proofs + // pick arbitrary left and right keys for proofs nondet i = leafKeys.oneOf() leftKey' = i, nondet i = leafKeys.oneOf() @@ -156,7 +155,8 @@ module treeGen { p } else { val parent = key / (2^h) - def hashOrChild(childMap) = + val parentsChild = key / (2^(h - 1)) + def hashOrZeroes(childMap) = if (childMap.keys().contains(parent)) { nodeHashes.get(childMap.get(parent)) } else { @@ -164,19 +164,21 @@ module treeGen { } // depending on whether the node is going to left or right, // push the hashes in the prefix and the suffix - if (key == 2 * parent) { - val right = hashOrChild(tree.right) + if (parentsChild % 2 == 0) { + // going to the left + val right = hashOrZeroes(tree.right) p.append({ prefix: raw([0]), suffix: right }) } else { - val left = hashOrChild(tree.left) - p.append({ prefix: raw([0]).termConcat(left), suffix: raw([]) }) + // going to the right + val left = hashOrZeroes(tree.left) + p.append({ prefix: raw([0]).termConcat(left), suffix: Map() }) } } ) // return the exists proof, where the key is the index itself { key: [key], - value: tree.leafs.get(key).value, + value: value, leaf: { prefix: raw([0]) }, path: path, } @@ -191,7 +193,7 @@ module treeGen { inputKey' = inputKey, } - /// make sure that the proofs are the same for all the leafs + /// make sure that the roots obtained from the proofs are the same for all the leafs val treeProofInv = and { leftKey.in(tree.leafs.keys()), @@ -199,7 +201,11 @@ module treeGen { } implies { val lroot = existsCalculate(leafToExistsProof(leftKey)) val rroot = existsCalculate(leafToExistsProof(rightKey)) - lroot == rroot + val rootHash = nodeHashes.get(1) + and { + lroot == rootHash, + rroot == rootHash, + } } /// The invariant of membership verification: @@ -296,4 +302,10 @@ module treeGen { /// check this property to produce an example of where NonMemInv is violated val nonMemExample = not(nonMemInv) + + val allInvariants = all { + if (treeProofInv) true else q::debug("treeProofInv", false), + if (memInv) true else q::debug("memInv", false), + if (nonMemInv) true else q::debug("nonMemInv", false), + } } From 5734cb417e6bcd8616d469d82b3d6ffd660a52d4 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 20 Dec 2024 18:55:51 -0300 Subject: [PATCH 24/24] Add stronger invariant --- examples/cosmos/ics23/ics23.qnt | 39 +++++++++-------- examples/cosmos/ics23/ics23test.qnt | 68 +++++++++++++++++++---------- examples/cosmos/ics23/treeGen.qnt | 30 +++++++++++-- 3 files changed, 93 insertions(+), 44 deletions(-) diff --git a/examples/cosmos/ics23/ics23.qnt b/examples/cosmos/ics23/ics23.qnt index c6335f75b..40b1f6fd5 100644 --- a/examples/cosmos/ics23/ics23.qnt +++ b/examples/cosmos/ics23/ics23.qnt @@ -68,18 +68,22 @@ module ics23 { key: Bytes, left: Option[ExistenceProof], right: Option[ExistenceProof] } + pure def hashLeaf(key: Bytes, value: Bytes, prefix: Term): Term = { + termHash(prefix + // TODO: use encodeVarintProto + // https://github.com/cosmos/ics23/blob/d0edf8e9cd38f7fc1bfc4311b2814e5d2ea966e8/go/proof.go#L67 + .termConcat(raw([length(key)])) + .termConcat(raw(key)) + .termConcat(raw([32])) + .termConcat(termHash(raw(value)))) + + } + /// calculate a hash from an exists proof def existsCalculate(p: ExistenceProof): Term = { // This is how the leaf hash is computed. // Notice that the key is not hashed. - val leafHash = - termHash(p.leaf.prefix - // TODO: use encodeVarintProto - // https://github.com/cosmos/ics23/blob/d0edf8e9cd38f7fc1bfc4311b2814e5d2ea966e8/go/proof.go#L67 - .termConcat(raw([length(p.key)])) - .termConcat(raw(p.key)) - .termConcat(raw([32])) - .termConcat(termHash(raw(p.value)))) + val leafHash = hashLeaf(p.key, p.value, p.leaf.prefix) // the inner node nodeHashes are concatenated and hashed upwards p.path.foldl(leafHash, @@ -109,13 +113,13 @@ module ics23 { /// checks if an op has the expected padding pure def hasPadding(op: InnerOp, pad: Padding): bool = and { - op.prefix.termLen() >= pad.minPrefix, - op.prefix.termLen() <= pad.maxPrefix, + q::debug("min ok", op.prefix.termLen() >= pad.minPrefix), + q::debug("max ok", op.prefix.termLen() <= pad.maxPrefix), // When inner turns left, suffixLen == child_size, // that is, we store the hash of the right child in the suffix. // When inner turns right, suffixLen == 0, // that is, we store the hash of the left child in the prefix. - op.suffix.termLen() == pad.suffix, + q::debug("ok", op.suffix.termLen() == pad.suffix), } pure def getPadding(spec: InnerSpec, branch: int): Option[Padding] = { @@ -152,6 +156,7 @@ module ics23 { pure val idx = orderFromPadding(spec, op) pure val leftBranches = idx.unwrap() and { + idx != None, leftBranches != 0, op.prefix.termLen() >= leftBranches * spec.childSize, pure val actualPrefix = op.prefix.termLen() - leftBranches * spec.childSize @@ -224,8 +229,8 @@ module ics23 { /// checks if left is exactly one slot to the left of right def isLeftStep(spec: InnerSpec, left: InnerOp, right: InnerOp): bool = { // 'left' turns left, and 'right' turns right - val lorder = orderFromPadding(spec, left) - val rorder = orderFromPadding(spec, right) + val lorder = q::debug("lorder", orderFromPadding(spec, q::debug("l op", left))) + val rorder = q::debug("rorder", orderFromPadding(spec, q::debug("r op", right))) and { lorder != None, rorder != None, @@ -252,21 +257,21 @@ module ics23 { // dist == 0 holds for the root. val dist = length(lpath) - 1 - li // the prefixes and suffixes match just above the cut points - 1.to(dist).forall(k => + q::debug("path match", 1.to(dist).forall(k => val lnode = lpath[li + k] val rnode = rpath[ri + k] and { lnode.prefix == rnode.prefix, lnode.suffix == rnode.suffix } - ), + )), // Now topleft and topright are the first divergent nodes // make sure they are left and right of each other. // Actually, lpath[li] and rpath[ri] are an abstraction // of the same tree node: // the left one stores the hash of the right one, whereas // the right one stores the hash of the left one. - isLeftStep(spec, lpath[li], rpath[ri]), + q::debug("isLeftStep", isLeftStep(spec, lpath[li], rpath[ri])), // left and right are remaining children below the split, // ensure left child is the rightmost path, and visa versa isRightMost(spec, lpath.slice(0, li)), @@ -310,7 +315,7 @@ module ics23 { } else if (np.right == None) { isRightMost(spec, np.left.unwrap().path) } else { - isLeftNeighbor(spec, np.left.unwrap().path, np.right.unwrap().path) + q::debug("isLeftNeighbor", isLeftNeighbor(spec, np.left.unwrap().path, np.right.unwrap().path)) } } } diff --git a/examples/cosmos/ics23/ics23test.qnt b/examples/cosmos/ics23/ics23test.qnt index 076e0caab..5f30bd62b 100644 --- a/examples/cosmos/ics23/ics23test.qnt +++ b/examples/cosmos/ics23/ics23test.qnt @@ -114,30 +114,42 @@ module ics23test { // Test setup to verify non membership - // * - // / \ - // 2:3 4:5 - pure val lhash = existsCalculate({ - key: [2], value: [3], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] - }) - pure val rhash = existsCalculate({ - key: [4], value: [5], leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, path: [] - }) + // 1 + // / \ + // 2 3 + // / / + // 4:3 6:5 + pure val hash4 = hashLeaf([4], [7], raw([0])) + pure val hash6 = hashLeaf([6], [4], raw([0])) + pure val hash2 = termHash(raw([0]).termConcat(hash4).termConcat(Hash256_ZERO)) + pure val hash3 = termHash(raw([0]).termConcat(hash6).termConcat(Hash256_ZERO)) // the left proof pure val lproof: ExistenceProof = { - key: [ 2 ], - value: [ 3 ], - leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, - path: [{ prefix: raw([ 0, 1, 2, 3 ]), suffix: raw([32]).termConcat(rhash) }] + key: [ 4 ], + value: [ 7 ], + leaf: { prefix: raw([ 0 ]) }, + path: [ + { prefix: raw([0]), suffix: Hash256_ZERO }, + { prefix: raw([0]), suffix: hash3 } + ] } // the right proof pure val rproof: ExistenceProof = { - key: [ 4 ], - value: [ 5 ], - leaf: { prefix: raw([ 0, 1, 2, 3 ]) }, - path: [{ prefix: raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash), suffix: raw([ ]) }] + key: [ 6 ], + value: [ 4 ], + leaf: { prefix: raw([ 0 ]) }, + path: [ + { prefix: raw([0]), suffix: Hash256_ZERO }, + { prefix: raw([0]).termConcat(hash2), suffix: Map() }, + ] + } + + pure val root = termHash(raw([0]).termConcat(hash2).termConcat(hash3)) + + run rootTest = and { + assert(root == existsCalculate(lproof)), + assert(root == existsCalculate(rproof)), } - pure val root = termHash(raw([ 0, 1, 2, 3, 32 ]).termConcat(lhash).termConcat(rhash)) run verifyNonMembership1Test = { pure val np1 = { key: [1], left: None, right: Some(lproof) } @@ -145,22 +157,32 @@ module ics23test { } run verifyNonMembership2Test = { - pure val np2 = { key: [2], left: Some(lproof), right: Some(rproof) } - assert(not(verifyNonMembership(root, np2, [ 2 ]))) + pure val np2 = { key: [2], left: None, right: Some(lproof) } + assert(verifyNonMembership(root, np2, [ 2 ])) } run verifyNonMembership3Test = { - pure val np3 = { key: [3], left: Some(lproof), right: Some(rproof) } + pure val np3 = { key: [3], left: None, right: Some(lproof) } assert(verifyNonMembership(root, np3, [ 3 ])) } run verifyNonMembership4Test = { - pure val np4 = { key: [2], left: Some(lproof), right: Some(rproof) } + pure val np4 = { key: [4], left: Some(lproof), right: Some(rproof) } assert(not(verifyNonMembership(root, np4, [ 4 ]))) } run verifyNonMembership5Test = { - pure val np5 = { key: [5], left: Some(rproof), right: None } + pure val np5 = { key: [5], left: Some(lproof), right: Some(rproof) } assert(verifyNonMembership(root, np5, [ 5 ])) } + + run verifyNonMembership6Test = { + pure val np6 = { key: [6], left: Some(lproof), right: Some(rproof) } + assert(not(verifyNonMembership(root, np6, [ 6 ]))) + } + + run verifyNonMembership7Test = { + pure val np7 = { key: [7], left: Some(rproof), right: None } + assert(verifyNonMembership(root, np7, [ 7 ])) + } } diff --git a/examples/cosmos/ics23/treeGen.qnt b/examples/cosmos/ics23/treeGen.qnt index 9b95844fc..8277c8d69 100644 --- a/examples/cosmos/ics23/treeGen.qnt +++ b/examples/cosmos/ics23/treeGen.qnt @@ -74,11 +74,8 @@ module treeGen { def putNodeHash(hashMap: int -> Term, key: int): (int -> Term) = { val h = if (t.leafs.keys().contains(key)) { - // simply use existsCalculate on the leaf val leaf = t.leafs.get(key) - existsCalculate({ - key: leaf.key, value: leaf.value, leaf: { prefix: raw([0]) }, path: [] - }) + hashLeaf(leaf.key, leaf.value, raw([0])) } else { // an inner node, assuming that the children nodeHashes were computed def hashOrZeroes(childMap) = @@ -300,6 +297,31 @@ module treeGen { inputKey > leftKey and rproof != None, } + pure def maxOrNone(s: Set[int]): Option[int] = { + if (s == Set()) None else Some(s.fold(0, (a, b) => if (a > b) a else b)) + } + + pure def minOrNone(s: Set[int]): Option[int] = { + if (s == Set()) None else Some(s.fold(99999, (a, b) => if (a < b) a else b)) + } + + val verifyMembershipInv = { + 2.to(2^height - 1).forall(key => { + if (tree.leafs.has(key)) { + // TODO + true + } else { + val left = q::debug("prev", tree.leafs.keys().filter(k => k < key).maxOrNone()) + val right = q::debug("post", tree.leafs.keys().filter(k => k > key).minOrNone()) + val lproof = if (left != None) Some(leafToExistsProof(left.unwrap())) else None + val rproof = if (right != None) Some(leafToExistsProof(right.unwrap())) else None + val nproof = { key: [key], left: lproof, right: rproof } + val rootHash = nodeHashes.get(1) + verifyNonMembership(rootHash, nproof, [q::debug("key", key)]) + } + }) + } + /// check this property to produce an example of where NonMemInv is violated val nonMemExample = not(nonMemInv)