From f4b5c5fcbc4fd68eb3854c5112229537f5b11a2f Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 4 Sep 2023 11:14:01 +0200 Subject: [PATCH 1/4] add the hashes module --- examples/cryptography/hashes.qnt | 100 +++++++++++++++++++++++++++ examples/cryptography/hashesTest.qnt | 36 ++++++++++ 2 files changed, 136 insertions(+) create mode 100644 examples/cryptography/hashes.qnt create mode 100644 examples/cryptography/hashesTest.qnt diff --git a/examples/cryptography/hashes.qnt b/examples/cryptography/hashes.qnt new file mode 100644 index 000000000..487186ec7 --- /dev/null +++ b/examples/cryptography/hashes.qnt @@ -0,0 +1,100 @@ +/** + * 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) { + if (p._2) { + // the marker for the end of a hash sequence + (p._1 + HASH_LEN, false) + } else { + // the marker for the start of a hash sequence + (p._1, true) + } + } else { + if (p._2) { + // in hash, keep the length + (p._1, true) + } else { + // in plain text + (p._1 + 1, false) + } + } + )._1 + } +} + +module sha256 { + import hashes(HASH_LEN = 32).* +} \ No newline at end of file diff --git a/examples/cryptography/hashesTest.qnt b/examples/cryptography/hashesTest.qnt new file mode 100644 index 000000000..71b2981b5 --- /dev/null +++ b/examples/cryptography/hashesTest.qnt @@ -0,0 +1,36 @@ +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), + assert(hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ])) != 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) + } +} \ No newline at end of file From be9f5611802933293fe8f4248f11a9d020714816 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 4 Sep 2023 11:22:43 +0200 Subject: [PATCH 2/4] improve the tests a bit --- examples/cryptography/hashesTest.qnt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/examples/cryptography/hashesTest.qnt b/examples/cryptography/hashesTest.qnt index 71b2981b5..2caaca414 100644 --- a/examples/cryptography/hashesTest.qnt +++ b/examples/cryptography/hashesTest.qnt @@ -17,7 +17,8 @@ module hashesTest { 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), - assert(hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ])) != hplain([ 2, 3, 4, 5, 6, 7 ])), + 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 = From 6ca9c737bec2ed6a129e20054ee6dad13055fba5 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 4 Sep 2023 13:02:46 +0200 Subject: [PATCH 3/4] update the dashboard --- examples/README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/README.md b/examples/README.md index 237b811be..86cc5ab78 100644 --- a/examples/README.md +++ b/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:https://github.com/informalsystems/quint/issues/693 | +| [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: | From e0e7aa730226f5ba222ce93ebd80d194906d7e75 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 4 Sep 2023 15:33:09 +0200 Subject: [PATCH 4/4] Apply suggestions from code review Co-authored-by: Kukovec --- examples/cryptography/hashes.qnt | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/examples/cryptography/hashes.qnt b/examples/cryptography/hashes.qnt index 487186ec7..9bb1d90dd 100644 --- a/examples/cryptography/hashes.qnt +++ b/examples/cryptography/hashes.qnt @@ -75,21 +75,11 @@ module hashes { input._bytes.foldl((0, false), (p, b) => if (b == -1) { - if (p._2) { - // the marker for the end of a hash sequence - (p._1 + HASH_LEN, false) - } else { - // the marker for the start of a hash sequence - (p._1, true) - } + 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 { - if (p._2) { - // in hash, keep the length - (p._1, true) - } else { - // in plain text - (p._1 + 1, false) - } + 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 }