Use a sum type to represent term nodes

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
+      }
     }
   }
 }

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)
   }

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)
-}
+}