Adding a specification of hashes to the examples (#1140)

* add the hashes module

* improve the tests a bit

* update the dashboard

* Apply suggestions from code review

Co-authored-by: Kukovec <[email protected]>

---------

Co-authored-by: Kukovec <[email protected]>

examples/README.md

@@ -68,6 +68,8 @@ listed without any additional command line arguments.
 | [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/tendermint/TendermintTest.qnt](./cosmos/tendermint/TendermintTest.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
+| [cryptography/hashes.qnt](./cryptography/hashes.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [cryptography/hashesTest.qnt](./cryptography/hashesTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/cryptography/hashes.qnt

@@ -0,0 +1,90 @@
+/**
+ * The module `hashes` provides the standard means of hashing byte sequences in
+ * Quint. A direct implementation of a hash (e.g., of SHA256) in Quint would
+ * produce plenty of hard-to-solve arithmetic constraints in a Quint
+ * specification. To this end, we introduce a different specification of a hash
+ * that has the following important properties:
+ *
+ * 1. For two sequences of bytes `bs1` and `bs2`, it holds that `bs1 == bs2` if
+ * and only if `hash(bs1) == hash(bs2)`. That is, our hash is perfect, it does
+ * not produce any collisions.
+ *
+ * 2. Hashes can be nested, e.g., `hash(hash(bs1).hconcat(bs2))`. Nested hashes
+ * preserve the property (1).
+ *
+ * 3. The operator `hlen` computes the length of byte sequences, some of
+ * which may have been computed via `hash`.
+ *
+ * 4. Plain text byte sequences and hashes may be concatenated via `hconcat`.
+ *
+ * Importantly, this modeling does not guarantee that a byte sequence would look
+ * exactly the same, as if it was computed via a real hash implementation.
+ * We will introduce integration with actual hash implementations later.
+ *
+ * Igor Konnov, Informal Systems, 2023.
+ */
+module hashes {
+  /// the length of a hashed sequence in bytes, e.g., 32 for SHA-256.
+  const HASH_LEN: int
+
+  /// A data structure that carries plain texts and hashed texts.
+  /// We could simply use `List[int]`, but a designated type indicates that
+  /// the user should not look inside.
+  type HMessage = {
+    _bytes: List[int]
+  }
+
+  /// Construct HText from plain text, that is, a list of bytes.
+  ///
+  /// @param bytes the input to wrap, all list elements shall be in the range
+  /// of [0, 255].
+  /// @returns the HMessage representation of bytes
+  pure def hplain(bytes: List[int]): HMessage = {
+    { _bytes: bytes }
+  }
+
+  /// Concatenate two messages, possibly hashed.
+  ///
+  /// @param first the first message
+  /// @param second the second message
+  /// @returns new message, in which `second` follows `first`.
+  pure def hconcat(first: HMessage, second: HMessage): HMessage = {
+    { _bytes: first._bytes.concat(second._bytes) }
+  }
+
+  /// Hash a sequence of bytes, some of which may have been hashed already.
+  ///
+  /// @param input the input to hash
+  /// @returns the hashed sequence of bytes
+  pure def hash(input: HMessage): HMessage = {
+    // We simply wrap the whole sequence of bytes with two markers -1.
+    // Since some parts of the input may have been hashed already, we decrease
+    // the hash markers in `input._bytes` first.
+    pure val decreased: List[int] = input._bytes.foldl([],
+      (l, b) => l.append(if (b >= 0) b else (b - 1))
+    )
+    // wrap with the markers -1
+    { _bytes: [-1].concat(decreased).append(-1) }
+  }
+
+  /// Compute the length of a message that may contain hashes or just plain text
+  ///
+  /// @param input the input to calculate the length of
+  /// @returns the length of the sequence
+  pure def hlen(input: HMessage): int = {
+    input._bytes.foldl((0, false),
+      (p, b) =>
+        if (b == -1) {
+          val newLen = p._1 + if (p._2) HASH_LEN else 0 // We add the total hash length at the terminator
+          (newLen, not(p._2)) // toggle the "in hash" flag
+        } else {
+          val newLen = p._1 + if (p._2) 0 else 1 // if in hash, the total hash length gets added in the terminator
+          (newLen, p._2)
+        }
+    )._1
+  }
+}
+
+module sha256 {
+  import hashes(HASH_LEN = 32).*
+}

examples/cryptography/hashesTest.qnt

@@ -0,0 +1,37 @@
+module hashesTest {
+  import hashes(HASH_LEN = 32).* from "./hashes"
+
+  pure def hplainTest = and {
+    assert(hplain([ 2, 3, 4 ]) == hplain([ 2, 3, 4 ])),
+    assert(hplain([ 2, 3, 4 ]) != hplain([ 3, 4, 5 ])),
+  }
+
+  pure def hashTest = and {
+    assert(hash(hplain([ 2, 3, 4 ])) == hash(hplain([ 2, 3, 4 ]))),
+    assert(hash(hplain([ 2, 3, 4 ])) != hash(hplain([ 3, 4, 5 ]))),
+    assert(hash(hplain([ 2, 3, 4 ])) != hplain([ 2, 3, 4 ])),
+    assert(hash(hash(hplain([ 2, 3, 4 ]))) != hash(hplain([ 2, 3, 4 ]))),
+  }
+
+  pure def hconcatTest = and {
+    pure val t234then567 = hplain([ 2, 3, 4 ]).hconcat(hplain([ 5, 6, 7 ]))
+    pure val t234567 = hplain([ 2, 3, 4, 5, 6, 7 ])
+    assert(t234then567 == t234567),
+    pure val h234then567 = hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ]))
+    assert(h234then567 != hplain([ 2, 3, 4, 5, 6, 7 ])),
+    pure def l =
+      (hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ]))).hconcat(hplain([ 8, 9 ]))
+    pure def r =
+      hash(hplain([ 2, 3, 4 ])).hconcat((hplain([ 5, 6, 7 ])).hconcat(hplain([ 8, 9 ])))
+    assert(l == r),
+  }
+
+  pure def hlenTest = and {
+    assert(hlen(hash(hplain([ 2, 3, 4 ]))) == 32),
+    assert(hlen(hash(hash(hplain([ 2, 3, 4 ])))) == 32),
+    assert(hlen(hplain([ 2, 3, 4, 5, 6, 7 ])) == 6),
+    pure def l =
+      (hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ]))).hconcat(hplain([ 8, 9 ]))
+    assert(hlen(l) == 37)
+  }
+}