++ Installation • + Documentation • + Community +
+ + + +
++ Installation • + Documentation • + Community +
+ + + +
](https://viennabusinessagency.at/).
-
-[Design Principles]: ./doc/design-principles.md
-[Apalache]: https://github.com/informalsystems/apalache
-[Lessons from Writing a Compiler]: https://borretti.me/article/lessons-writing-compiler
-[Imports]: ./doc/lang.md#imports-1
-[Module definitions]: ./doc/lang.md#module-definition
-[Constant declarations]: ./doc/lang.md#constant-declarations
-[Assumptions]: ./doc/lang.md#assumptions
-[Variable definitions]: ./doc/lang.md#variable-definitions
-[Operator definitions]: ./doc/lang.md#variable-definitions
-[Module instances]: ./doc/lang.md#module-instances
-[Lambdas]: ./doc/lang.md#lambdas-aka-anonymous-operators
-[Booleans]: ./doc/lang.md#boolean-operators-and-equality
-[Integers]: ./doc/lang.md#integers
-[Sets]: ./doc/lang.md#sets
-[Lists]: ./doc/lang.md#lists-aka-sequences
-[Multiline disjunctions]: ./doc/lang.md#multiline-disjunctions
-[Multiline conjunctions]: ./doc/lang.md#multiline-conjunctions
-[if-then-else]: ./doc/lang.md#condition
-[nondet]: ./doc/lang.md#existential-quantifier-and-non-deterministic-choice
-[Maps]: ./doc/lang.md#maps-aka-functions
-[Records]: ./doc/lang.md#records
-[Tuples]: ./doc/lang.md#tuples
-[Sum types]: ./doc/lang.md#sum-types
-[Delayed assignment]: ./doc/lang.md#delayed-assignment
-[Runs]: ./doc/lang.md#runs
-[Temporal operators]: ./doc/lang.md#temporal-operators
-[Fairness]: ./doc/lang.md#fairness
-[Unbounded quantifiers]: ./doc/lang.md#unbounded-quantifiers
-[Modes]: ./doc/lang.md#modes
-[Spells]: ./examples/spells/README.md
-[Contribute your spell]: ./examples/spells/contribute-your-spell.md
-[539]: https://github.com/informalsystems/quint/issues/539
-[221]: https://github.com/informalsystems/quint/issues/221
-[235]: https://github.com/informalsystems/quint/issues/235
-[8]: https://github.com/informalsystems/quint/issues/8
-[1034]: https://github.com/informalsystems/quint/issues/1034
-[Higher-order definitions]: https://github.com/informalsystems/quint/blob/main/doc/lang.md#operator-definitions
-[String literals]: https://github.com/informalsystems/quint/blob/main/doc/lang.md#identifiers-and-strings
-[TLA+]: https://lamport.azurewebsites.net/tla/tla.html
-[TLA]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions
-[Visual Studio Code Marketplace]: https://marketplace.visualstudio.com/items?itemName=informal.quint-vscode
-[Tutorials]: ./tutorials/README.md
-[Quint zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/378959-quint
-[Quint discussions]: https://github.com/informalsystems/quint/discussions
-[ITF traces]: https://apalache.informal.systems/docs/adr/015adr-trace.html
-[ITF Trace Viewer]: https://marketplace.visualstudio.com/items?itemName=informal.itf-trace-viewer
-[15 minute intro to Quint]: https://youtu.be/OZIX8rs-kOA
+Supported by the Vienna Business Agency.
](https://viennabusinessagency.at/)
diff --git a/Wirtschaftsagentur_Wien_logo.jpg b/Wirtschaftsagentur_Wien_logo.jpg
deleted file mode 100644
index 5598fbece..000000000
Binary files a/Wirtschaftsagentur_Wien_logo.jpg and /dev/null differ
diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 000000000..97e4ef5cf
--- /dev/null
+++ b/doc/README.md
@@ -0,0 +1,20 @@
+# Documentation
+
+## Language
+
+- [Language tutorials](../tutorials/README.md)
+- [Syntax specification](./lang.md)
+- [Cheatsheet](./quint-cheatsheet.pdf)
+- [API documentation for built-in operators](./builtin.md)
+
+## Tooling
+
+- [REPL tutorial](../tutorials/repl/repl.md)
+- [CLI manual](./quint.md)
+- [Literate executable specifications](./literate.md)
+
+## Design and Development
+
+- [Design Principles](./design-principles.md)
+- [Roadmap](./roadmap.md)
+- [Frequently asked questions](./faq.md)
diff --git a/doc/builtin.md b/doc/builtin.md
index 4ed2c6eec..2ccb49c70 100644
--- a/doc/builtin.md
+++ b/doc/builtin.md
@@ -239,15 +239,16 @@ assert(Set(Set(1, 2), Set(3, 4)).flatten() == Set(1, 2, 3, 4))
## `pure def allLists: (Set[a]) => Set[List[a]]`
-`s.allLists()` is the set of all lists containing all the elements in `s`.
+`s.allLists()` is the set of all lists containing elements in `s`.
+This is an infinite set unless `s` is the empty set.
+
+Like other inifite sets, this is not supported in the simulator.
### Examples
```
-assert(Set(1, 2).allLists() == Set(
- List(1, 2),
- List(2, 1),
-))
+assert(Set(1, 2).allLists().contains([]))
+assert(Set(1, 2).allLists().contains([1, 1, 1, 1, 2, 1]))
```
## `pure def chooseSome: (Set[a]) => a`
@@ -851,7 +852,9 @@ run test = (x' = 0).then(a).then(assert(x == 3))
`a` is true for a step from `s1` to `t` and `b` is true for a step from `t` to `s2`.
-This is the action composition operator.
+This is the action composition operator. If `a` evaluates to `false`, then
+`a.then(b)` reports an error. If `b` evaluates to `false` after `a`, then
+`a.then(b)` returns `false`.
### Examples
@@ -860,6 +863,26 @@ var x: int
run test = (x' = 1).then(x' = 2).then(x' = 3).then(assert(x == 3))
```
+## `action expect: (bool, bool) => bool`
+
+`a.expect(b)` is true for a step from `s1` to `s2` if
+
+ - `a` is true for a step from `s1` to `s2`, and
+ - `b` holds true in `s2`.
+
+If `a` evaluates to `false`, evaluation of `a.expect(b)`
+fails with an error message. If `b` evaluates to `false`,
+evaluation of `a.expect(b)` fails with an error message.
+
+### Examples
+
+```
+var n: int
+run expectConditionOkTest = (n' = 0).then(n' = 3).expect(n == 3)
+run expectConditionFailsTest = (n' = 0).then(n' = 3).expect(n == 4)
+run expectRunFailsTest = (n' = 0).then(all { n == 2, n' = 3 }).expect(n == 4)
+```
+
## `action reps: (int, (int) => bool) => bool`
`n.reps(i => A(i))` or `n.reps(A)` the action `A`, `n` times.
@@ -897,7 +920,7 @@ It does not change the state.
```
var x: int
-run test = (x' = 0).then(3.times(x' = x + 1)).then(assert(x == 3))
+run test = (x' = 0).then(3.reps(x' = x + 1)).then(assert(x == 3))
```
```
@@ -907,3 +930,22 @@ action Next = x' = x + 1
run test = Init.then(all { Next, assert(x > 0) })
```
+
+## `pure def q::debug: (str, a) => a`
+
+`q::debug(msg, value)` prints the given message and value to the console,
+separated by a space.
+
+It also returns the given value unchanged,
+so that it can be used directly within expressions.
+
+### Examples
+
+```
+var x: int
+>>> (x' = 0).then(3.reps(i => x' = q::debug("new x:", x + 1)))
+> new x: 1
+> new x: 2
+> new x: 3
+true
+```
diff --git a/doc/lang.md b/doc/lang.md
index 9dec39e9a..a598c6146 100644
--- a/doc/lang.md
+++ b/doc/lang.md
@@ -2,7 +2,7 @@
| Revision | Date | Author |
|:---------|:-----------|:--------------------------------------------------------|
-| 34 | 09.10.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
+| 35 | 12.12.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
This document presents language constructs in the same order as the [summary of
TLA+](https://lamport.azurewebsites.net/tla/summary.pdf).
@@ -64,6 +64,7 @@ Table of Contents
* [Then](#then)
* [Reps](#reps)
* [Example](#example)
+ * [Expect](#expect)
* [Fail](#fail)
* [Temporal operators](#temporal-operators)
* [Always](#always)
@@ -146,31 +147,34 @@ This is the same type system as in Apalache:
A type is one of the following:
- - Basic type: `bool`, `int`, `str`.
+- Basic type: `bool`, `int`, `str`.
- - Uninterpreted type or type name: `IDENTIFIER_IN_CAPS`.
+- Uninterpreted type or type name: `IDENTIFIER_IN_CAPS`.
- - Type variable (parameter): `a`, ..., `z`.
+- Type variable (parameter): `a`, ..., `z`.
- - Set: `Set[T]` for a type `T`.
+- Set: `Set[T]` for a type `T`.
- - List: `List[T]` for a type `T`.
+- List: `List[T]` for a type `T`.
- - Tuple: `(T_1, T_2, ..., T_n)` for `n >= 2` types `T_1`, ..., `T_n`.
+- Tuple: `(T_1, T_2, ..., T_n)` for `n >= 2` types `T_1`, ..., `T_n`.
- - Record: `{ name_1: T_1, name_2: T_2, ..., name_n: T_n }`
- for `n >= 1` types `T_1`, ..., `T_n`.
+- Record: `{ name_1: T_1, name_2: T_2, ..., name_n: T_n }`
+ for `n >= 1` types `T_1`, ..., `T_n`.
- - Function: `T1 -> T2` for types `T1` and `T2`.
+- Function: `T1 -> T2` for types `T1` and `T2`.
- - Operator: `(T_1, ..., T_n) => R` for `n >= 0` argument types `T_1, ..., T_n`
- and result type `R`.
+- Operator: `(T_1, ..., T_n) => R` for `n >= 0` argument types `T_1, ..., T_n`
+ and result type `R`.
- - Sum Types: `type T = L_1(T_1) | ... | L_n(T_n) ` for `n >= 1`, argument types
- `T_1`, ..., `T_n`, and a type alais `T`.
+- Sum Types: `type T = L_1(T_1) | ... | L_n(T_n) ` for `n >= 1`, argument types
+ `T_1`, ..., `T_n`, and a type alais `T`.
- - Type in parentheses: `(T)` for a type `T`.
+- Type in parentheses: `(T)` for a type `T`.
+- An instance of a defined polymorphic type `T[T_1, ..., T_n]` for a defined type
+ constructor with type parameters `T[p_1, ..., p_n]` and types `T_1, ...,
+ T_n`.
It is often convenient to declare a type alias. You can use `type` to define
an alias inside a module definition. For instance:
@@ -179,6 +183,18 @@ an alias inside a module definition. For instance:
type Temperature = int
```
+A type alias specified with type parameters defines a polymorphic type
+constructor for instances of the defined type. For instance, given
+
+```bluespec
+type Option[a] =
+ | Some(a)
+ | None
+```
+
+You can then construct concrete types such as `Option[int]` or
+`Option[List[int]]`.
+
A type identifier can also introduce an uninterpreted type by defining a type without any constructors for values of that type:
```bluespec
@@ -498,7 +514,7 @@ module Top {
Note that in the above example, `Inner::x2` is treated as a qualified identifier, that is, it consists of the prefix `Inner` and the name `x2`.
-*No collisions.* There must be no name collisions between names. Shadowing of a name is not allowed. For example:
+Shadowing names is allowed. For example:
```bluespec
module OS {
@@ -508,13 +524,7 @@ module OS {
}
```
-The Quint parser produces the following error message:
-
-```
-error: [QNT101] Conflicting definitions found for name 'clock' in module 'OS'
-4: def increase(clock) = clock + 1
- ^^^^^
-```
+PS: Let us know if you are bothered by this. We are considering making it a togglable feature.
*No order.* In contrast to TLA+, namespaces are not ordered. It is perfectly
fine to write out-of-order definitions, like in many programming languages:
@@ -1290,14 +1300,14 @@ sets of records: (1) It often confuses beginners, (2) It can be expressed with
### Tuples
-In contrast to TLA+, Quint tuples have length of at least 2.
-If you need lists, use lists.
-
```scala
// Tuple constructor: << e_1, ..., e_n >>
-// Warning: n >= 2
(e_1, ..., e_n)
Tup(e_1, ..., e_n)
+// The empty tuple is also the canonical unit type
+// <<>>
+()
+Tup()
// t[1], t[2], t[3], t[4], ... , t[50]
t._1
t._2
@@ -1657,13 +1667,19 @@ then(A, B)
The semantics of this operator is as follows. When `A.then(B)` is applied to a
state `s_1`, the operator computes a next state `s_2` of `s_1` by applying
-action `A`, if such a state exists. If `A` returns `true`, then the operator
-`A.then(B)` computes a next state `s_3` of `s_2` by applying action `B`, if
-such a state exists. If `B` returns true, then the operator `A.then(B)` returns
-`true`, the old state is equal to `s_1`, and the new state is equal to `s_3`.
-In all other cases, the operator returns `false`.
+action `A`, if such a state exists. Depending on the result of `A`, two scenarios
+are possible:
-This operator is equivalent to `A \cdot B` of TLA+.
+ - When `A` returns `true`, then the operator `A.then(B)` computes a next state
+ `s_3` of `s_2` by applying action `B`, if such a state exists.
+ If `B` returns true, then the operator `A.then(B)` returns
+ `true`, the old state is equal to `s_1`, and the new state is equal to `s_3`.
+ Otherwise, the operator `A.then(B)` returns `false`.
+
+ - If `A` returns `false`, then it is impossible to continue. A runtime error
+ should be reported.
+
+This operator is equivalent to `A \cdot B` of TLA+ (except for the runtime errors).
**Example.** Consider the specification `counters`:
@@ -1754,6 +1770,40 @@ to be disabled.
*Mode:* Run.
+#### Expect
+
+The operator `expect` has the following syntax:
+
+```scala
+A.expect(P)
+expect(A, P)
+```
+
+The left-hand side `A` must be an action or a run. The right-hand side `P` must
+be a non-action Boolean expression.
+
+The semantics of this operator is as follows:
+
+- Evaluate action `A`:
+ - When `A`'s result is `false`, emit a runtime error.
+ - When `A`'s result is `true`:
+ - Commit the variable updates.
+ - Evaluate `P`:
+ - If `P` evaluates to `false`, emit a runtime error (similar to `assert`).
+ - If `P` evaluates to `true`, undo the updates back to the state where we
+ were after `A` was applied.
+
+##### Example
+
+```bluespec
+var n: int
+run expectConditionOkTest = (n' = 0).then(n' = 3).expect(n == 3)
+run expectConditionFailsTest = (n' = 0).then(n' = 3).expect(n == 4)
+run expectRunFailsTest = (n' = 0).then(all { n == 2, n' = 3 }).expect(n == 4)
+```
+
+*Mode:* Run.
+
### Temporal operators
Temporal operators describe infinite executions.
diff --git a/doc/quint.md b/doc/quint.md
index e455f2e4a..e3c3c079f 100644
--- a/doc/quint.md
+++ b/doc/quint.md
@@ -14,6 +14,8 @@ and integration with other tools.
The main commands of `quint` are as follows:
- [x] `repl` starts the REPL (Read-Eval-Print loop) for Quint
+ - [x] `compile` parses, typechecks, and processes a quint specification
+ into the `--target` format, writing the results to stdout
- [x] `parse` parses a Quint specification and resolves names
- [x] `typecheck` infers types in a Quint specification
- [x] `run` executes a Quint specification via random simulation
@@ -65,13 +67,58 @@ The REPL is especially useful for learning the language. See the
The verbosity levels 3 and 4 are used to show execution details. They are
especially useful for debugging complex specifications.
+## Command `compile`
+
+```sh
+$ quint compile --help
+quint compile
+
+compile a Quint specification into the target, the output is written to stdout
+
+Options:
+ --help Show help [boolean]
+ --version Show version number [boolean]
+ --out output file (suppresses all console output) [string]
+ --main name of the main module (by default, computed from filename)
+ [string]
+ --init name of the initializer action [string] [default: "init"]
+ --step name of the step action [string] [default: "step"]
+ --invariant the invariants to check, separated by commas (e.g.) [string]
+ --temporal the temporal properties to check, separated by commas [string]
+ --target the compilation target. Supported values: tlaplus, json
+ [string] [default: "json"]
+ --verbosity control how much output is produced (0 to 5)[number] [default: 2]
+```
+
+Given a quint specification as input, this command parses, resolves imports,
+typechecks, and then "flattens" the specification into on module containing just
+the needed definitions.
+
+The main module is determined as follows: If a module name is specified by
+`--main`, that takes precedence. Otherwise, if there is only one module in the
+input file, that is the main module. Otherwise, the module with the same name as
+the file is taken to be the main module.
+
+The main module must specify a state machine. This means it must either define
+actions named `init` and `step`, specifying the initial state and the
+transition action respectively, or suitable actions defined in the main module
+must be indicated using the `--init` and `--step` options.
+
+The following compilation targets are supported
+
+- `json`: The default target, this produces a json representation, in the same
+ format which is described under [`parse`](#command-parse) and
+ [`typecheck`](#command-typecheck), below.
+- `tlaplus`: Quint uses its integration with Apalache to compile the
+ specification into TLA+.
+
## Command `parse`
*Warning: The language is still in active development, and breaking changes are
to be expected.*
```sh
-$ quint parse --help
+$ quint parse --help
quint parse
parse a Quint specification
@@ -184,6 +231,8 @@ Options:
--invariant invariant to check: a definition name or an expression
[string] [default: ["true"]]
--seed random seed to use for non-deterministic choice [string]
+ --mbt (experimental) whether to produce metadata to be used by
+ model-based testing [boolean] [default: false]
```
- If there are no critical errors (e.g., in parsing, typechecking, etc.), the
@@ -208,6 +257,19 @@ Options:
The errors and warnings are written in the format of [ADR002][].
+### The `--mbt` flag
+When this flag is given, the Quint simulator will keep track of two additional
+variables on the traces it produces:
+- `action_taken`: The first action executed by the simulator on each step, reset
+ at every `any` evaluation. That is, if the spec has nested `any` statements,
+ `action_taken` will correspond to the action picked in the innermost `any`.
+- `nondet_picks`: A record with all `nondet` values that were picked since the
+ last `any` was called (or since the start, if there were no `any` calls in the
+ step).
+
+Keep in mind that this is an experimental flag and it is specially subject to
+changes in its behavior.
+
## Command test
```sh
@@ -258,30 +320,32 @@ Options:
## Command verify
```sh
-$ quint verify
+$ quint verify --help
+quint verify
Verify a Quint specification via Apalache
Options:
- --help Show help [boolean]
- --version Show version number [boolean]
- --main name of the main module (by default, computed from
- filename) [string]
- --out output file (suppresses all console output) [string]
- --out-itf output the trace in the Informal Trace Format to file
- (suppresses all console output) [string]
- --max-steps the maximum number of steps in every trace
- [number] [default: 10]
- --init name of the initializer action [string] [default: "init"]
- --step name of the step action [string] [default: "step"]
- --invariant the invariants to check, separated by a comma [string]
- --temporal the temporal properties to check, separated by a comma
+ --help Show help [boolean]
+ --version Show version number [boolean]
+ --out output file (suppresses all console output) [string]
+ --main name of the main module (by default, computed from
+ filename) [string]
+ --init name of the initializer action[string] [default: "init"]
+ --step name of the step action [string] [default: "step"]
+ --invariant the invariants to check, separated by commas (e.g.)
[string]
+ --temporal the temporal properties to check, separated by commas
+ [string]
+ --out-itf output the trace in the Informal Trace Format to file
+ (suppresses all console output) [string]
+ --max-steps the maximum number of steps in every trace
+ [number] [default: 10]
--random-transitions choose transitions at random (= use symbolic simulation)
[boolean] [default: false]
--apalache-config path to an additional Apalache configuration file (in
JSON) [string]
- --verbosity control how much output is produced (0 to 5)
+ --verbosity control how much output is produced (0 to 5)
[number] [default: 2]
```
@@ -298,7 +362,7 @@ steps:
Apalache uses bounded model checking. This technique checks *all runs* up to
`--max-steps` steps via [z3][]. Apalache is highly configurable. See [Apalache
configuration](https://apalache.informal.systems/docs/apalache/config.html?highlight=configuration#apalache-configuration)
-for guidance.
+for guidance.
- If there are no critical errors (e.g., in parsing, typechecking, etc.), this
command sends the Quint specification to the [Apalache][] model checker, which
diff --git a/doc/rfc007-foreign-calls.md b/doc/rfc007-foreign-calls.md
new file mode 100644
index 000000000..2b4d7470d
--- /dev/null
+++ b/doc/rfc007-foreign-calls.md
@@ -0,0 +1,220 @@
+# RFC007: Design space of foreign calls in Quint
+
+| Revision | Date | Author |
+| :------- | :--------- | :--------------- |
+| 1 | 2023-04-05 | Igor Konnov |
+
+## 1. Summary
+
+In this RFC, we discuss potential solutions for integrating the Quint simulator
+with other execution environments. This would enrich the simulator with
+computations that cannot be expressed in Quint itself, e.g., rich string
+manipulation and parsing. Additionally, it would give us another path for more
+interactive integration of the Quint simulator with systems under test.
+
+## 2. Context
+
+Quint is a specification language with the following features that are important
+in the context of this RFC:
+
+ - Quint has a relatively small standard library, and
+ - Quint has formal semantics, thanks to its transpilation to TLA+.
+
+Thanks to these features, Quint is an easier target for static analysis and
+verification tools than general-purpose programming languages. At the same time,
+these nice features are somewhat in conflict with the expressivity and usability
+of the language, from the systems engineer's point of view. Even though Quint is
+obviously Turing-complete (for example, quantifiers over integers and integer
+arithmetic make many properties undecidable), this does not mean that all of the
+typical engineering tasks are easy to do in Quint.
+
+In the following, we introduce several examples that motivate the need for this
+RFC.
+
+### Example 1: Strings
+
+From the systems engineer's point of view, the most glaring omission in the
+language is the absence of string manipulation. From the verification engineer's
+point of view strings are nothing else but lists of constants, which are
+normally represented with bytes or sequences of bytes in programming languages.
+While this is true, it is simply hard for humans to read expressions in this
+representation. Compare the two expressions:
+
+```js
+["I", " ", "a", "m", " ", "a" , " ", "s", "t", "r", "i", "n", "g"]
+"I am a string"
+```
+
+Although, string operations are typically used to format the output and process
+the input, they open a room for hard verification problems. We should not
+introduce hard problems, if they are caused by non-functional features such as
+the user interface.
+
+Yet, it would be nice to have a nice user interface in REPL, while keeping the
+specifications amenable for verification. This shows a need for a clear
+boundary between the "essential" computations and "non-essential" computations.
+
+One concrete example of this usability issue is the string representation of
+[IBC denominations][]. For instance, IBC operates over strings such as
+`transfer/channelToA/denom`. In a Quint specification, we would prefer to
+operate over lists such as `["transfer", "channelToA", "denom"]`. How can we
+make Quint consume and produce the human-readable form of denominations, while
+operating over lists? This problem calls for a serialization solution, which
+would be typically done via a standard interface such as `toString` and
+`parseFrom` in programming languages. For instance, it would be quite easy to
+write such functions in JavaScript.
+
+*Desired state: We would to input and output strings in a human-readable
+form without impairing the verification tools.*
+
+### Example 2: Hashing and encryption
+
+Related to Example 1, blockchain projects heavily rely on the standard hashing
+and encryption functions such as [SHA-2][] and ed25519, see [Cosmos Accounts][].
+Not only it would be hard to express these algorithms in Quint, it would also
+introduce enormous complexity to the verification tasks. To perform functional
+verification, we would usually need high-level properties of these algorithms.
+Actually, assuming perfect hashing and perfect encryption is often sufficient to
+reason about non-cryptographic properties of distributed algorithms.
+
+Again, while this is mostly irrelevant for verification, systems engineers
+would like to call the actual hashing and encryption functions at some point,
+for instance, to generate realistic data.
+
+*Desired state: We should be able to use the standard hashing/encryption
+functions in the simulator. We do not have to verify these functions, assuming
+that they are in the trusted core of our system.*
+
+### Example 3: Testing
+
+Testing is probably the most obvious example that would require an integration
+between the simulator and the system under test. Our current approach to this
+problem is to produce traces in the [ITF Format][]. For instance, the following
+command would save a trace found by the simulator into `foo.itf.json`, see
+the [Quint manual][] for details:
+
+```sh
+quint run --out-itf=foo.itf.json foo.qnt
+```
+
+This approach assumes that the simulator (or a verification tool) is called
+once, and its output is consumed by the system under test. However, this makes
+it hard to integrate the simulator/verifier and the system under test into a
+feedback loop. For example, see [Issue 2453][].
+
+*Desired state: We should be able to call a system under test from a Quint
+specification, in order to get interactive feedback from the system under test.*
+
+### Example 4: Interactive trace visualization
+
+Visualization is another example of where we could benefit from an integration
+with non-Quint code. Whereas it should be easy to visualize ITF traces, we could
+go further and visualize interactive computations, e.g., in Quint REPL. We have
+discussed this approach once, and it was not clear to us, why should we call
+foreign code from Quint to do that, see [Issue 143][]. So this is probably not
+the strongest motivator for this RFC.
+
+*Desired state: We should be able to inform an external visualization tool
+about a change in the system state, while running the simulator, or doing
+interactive exploration in REPL. Visualization should not compromise the
+formal specification.*
+
+## 3. Options
+
+We are discussing the choice of a good technology, given the following
+constraints:
+
+ - Ideally, the simulator should be able to integration with codebases
+ written in Rust and Golang, as these are the implementation languages
+ of the Cosmos ecosystem.
+
+ - We emphasize ease of use over performance.
+
+### Option 1: Dynamic integration with JavaScript via eval
+
+The most obvious solution that first came to my mind is to introduce a special
+Quint operator such as `unsafe { ... }` and place JavaScript code inside. We
+could evaluate the JavaScript code with `eval`.
+
+Although this solution is quite simple, it has a very bad security smell:
+
+ - Many execution environments disable `eval`, see [eval][].
+
+ - Security analysis tools may complain about Quint, if we place `eval` in its
+ code.
+
+ - Ironically, placing `eval` into a formal spec may lead to vulnerabilities.
+
+It looks like poisoning formal specs with `eval` is a very bad idea.
+Additionally, it limits the integration point to JavaScript.
+
+### Option 2: Node vm sandbox
+
+A slightly better option would be to use [NodeJS VM][].
+
+Pros:
+
+ - It would still interpret JavaScript code, but in a sandboxed environment.
+
+Cons:
+
+ - We would depend on NodeJS, so transferring REPL to the web will be harder.
+
+ - It limits the integration point to JavaScript and NodeJS.
+
+### Option 3: JSON-RPC
+
+We would like to execute the non-Quint code outside of the Quint tooling itself.
+[JSON-RPC][] would allow us to implement such a loosely-coupled integration.
+
+Pros:
+
+ - Quint is written in TypeScript and submitting JSON is no brainer, especially
+ given that we are using [ITF Format][] for serialization.
+
+ - Language agnostic. Non-Quint code may be writte in JavaScript, Golang, and
+ Rust.
+
+ - Relatively easy to implement in Quint.
+
+ - Does not require `.proto` files, in contrast to gRPC.
+
+Cons:
+
+ - Not the best performance. If we aim at high-performance integration loops,
+ e.g., when doing fuzzing, JSON-RPC may become a bottleneck.
+
+### Option 4: Compile-time integration
+
+Another option to explore is to link against dynamic libraries that are written
+in other languages, e.g., Rust and Golang.
+
+Pros:
+
+ - This would probably give us the best performance.
+
+ - This may give us bonus points from the people who like low-level languages.
+
+Cons:
+
+ - Serialization would be painful.
+
+ - External libraries would have compilation-time dependencies. It would not
+ pose serious problems to use, but it would make integration harder.
+
+## 4. Solution
+
+We have to figure out a good solution, or maybe several solutions. The problem
+space outlined by the four examples is quite large.
+
+
+[IBC denominations]: https://github.com/cosmos/ibc/blob/main/spec/app/ics-020-fungible-token-transfer/README.md#data-structures
+[SHA-2]: https://en.wikipedia.org/wiki/SHA-2
+[Cosmos Accounts]: https://docs.cosmos.network/v0.45/basics/accounts.html#signatures
+[ITF Format]: https://apalache.informal.systems/docs/adr/015adr-trace.html
+[Quint manual]: https://github.com/informalsystems/quint/blob/main/doc/quint.md
+[Issue 2453]: https://github.com/informalsystems/apalache/issues/2453
+[Issue 143]: https://github.com/informalsystems/quint/issues/143
+[eval]: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/eval
+[NodeJS VM]: https://nodejs.org/api/vm.html
+[JSON-RPC]: https://en.wikipedia.org/wiki/JSON-RPC#Implementations
\ No newline at end of file
diff --git a/doc/roadmap.md b/doc/roadmap.md
new file mode 100644
index 000000000..253c2b3fe
--- /dev/null
+++ b/doc/roadmap.md
@@ -0,0 +1,92 @@
+# Roadmap
+
+In the spirit of [Lessons from Writing a Compiler][], we have a roadmap, where
+we are implementing various transpiler passes feature-by-feature, instead of
+completely implementing every pass.
+
+- :white_check_mark: Completed
+- :green_circle: Won't get in your way, but there's still work to be done
+- :x: Not implemented yet
+
+| Language feature | Parser | Name resolution | Effects | Type checker | Simulator | To-Apalache | Tutorials |
+|:----------------------------------|:------------------:|:------------------:|:------------------:|:------------------:|:------------------:|:------------------:|:------------------:|
+| [Booleans][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Integers][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [if-then-else][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Operator definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Modes][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Sets][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [nondet][] | :white_check_mark: | :white_check_mark: | :green_circle: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Maps][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Lists][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Records][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Tuples][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Sum types][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Imports][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Module definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Module instances][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Multiple files][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Constant declarations][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Variable definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Assumptions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [235][] | :white_check_mark: | :x: |
+| [Lambdas][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Multiline disjunctions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Multiline conjunctions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Delayed assignment][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| Invariant checking | - | - | - | - | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [Higher-order definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [Runs][] | :white_check_mark: | :white_check_mark: | :green_circle: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: |
+| [Temporal operators][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: | :x: |
+| [Fairness][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: | :x: |
+| [Unbounded quantifiers][] | :white_check_mark: | :white_check_mark: | :x: | :x: | *non-goal* | :x: | :x: |
+| [String literals][], see #118 | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| ~~uninterpreted types~~, see #118 | :white_check_mark: | :white_check_mark: | :x: | :x: | :x: | :x: | :x: |
+
+
+[Design Principles]: ./design-principles.md
+[Apalache]: https://github.com/informalsystems/apalache
+[Lessons from Writing a Compiler]: https://borretti.me/article/lessons-writing-compiler
+[Imports]: ./lang.md#imports-1
+[Module definitions]: ./lang.md#module-definition
+[Constant declarations]: ./lang.md#constant-declarations
+[Assumptions]: ./lang.md#assumptions
+[Variable definitions]: ./lang.md#variable-definitions
+[Operator definitions]: ./lang.md#variable-definitions
+[Module instances]: ./lang.md#module-instances
+[Lambdas]: ./lang.md#lambdas-aka-anonymous-operators
+[Booleans]: ./lang.md#boolean-operators-and-equality
+[Integers]: ./lang.md#integers
+[Sets]: ./lang.md#sets
+[Lists]: ./lang.md#lists-aka-sequences
+[Multiline disjunctions]: ./lang.md#multiline-disjunctions
+[Multiline conjunctions]: ./lang.md#multiline-conjunctions
+[if-then-else]: ./lang.md#condition
+[nondet]: ./lang.md#existential-quantifier-and-non-deterministic-choice
+[Maps]: ./lang.md#maps-aka-functions
+[Records]: ./lang.md#records
+[Tuples]: ./lang.md#tuples
+[Sum types]: ./lang.md#sum-types
+[Delayed assignment]: ./lang.md#delayed-assignment
+[Runs]: ./lang.md#runs
+[Temporal operators]: ./lang.md#temporal-operators
+[Fairness]: ./lang.md#fairness
+[Unbounded quantifiers]: ./lang.md#unbounded-quantifiers
+[Modes]: ./lang.md#modes
+[Spells]: ./examples/spells/README.md
+[Contribute your spell]: ./examples/spells/contribute-your-spell.md
+[539]: https://github.com/informalsystems/quint/issues/539
+[221]: https://github.com/informalsystems/quint/issues/221
+[235]: https://github.com/informalsystems/quint/issues/235
+[8]: https://github.com/informalsystems/quint/issues/8
+[1034]: https://github.com/informalsystems/quint/issues/1034
+[Higher-order definitions]: https://github.com/informalsystems/quint/blob/main/doc/lang.md#operator-definitions
+[String literals]: https://github.com/informalsystems/quint/blob/main/doc/lang.md#identifiers-and-strings
+[TLA+]: https://lamport.azurewebsites.net/tla/tla.html
+[TLA]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions
+[Visual Studio Code Marketplace]: https://marketplace.visualstudio.com/items?itemName=informal.quint-vscode
+[Tutorials]: ./tutorials/README.md
+[Quint zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/378959-quint
+[Quint discussions]: https://github.com/informalsystems/quint/discussions
+[ITF traces]: https://apalache.informal.systems/docs/adr/015adr-trace.html
+[ITF Trace Viewer]: https://marketplace.visualstudio.com/items?itemName=informal.itf-trace-viewer
+[15 minute intro to Quint]: https://youtu.be/OZIX8rs-kOA
diff --git a/doc/story008-repl-traces.md b/doc/story008-repl-traces.md
new file mode 100644
index 000000000..840a5a2e0
--- /dev/null
+++ b/doc/story008-repl-traces.md
@@ -0,0 +1,262 @@
+# Story008: Simulator Traces in REPL
+
+| Revision | Date | Author |
+|---------:|:----------:|:------------------------|
+| 1 | 2023-05-05 | Igor Konnov |
+
+This is a UX design document for the interaction with states and traces in REPL.
+This document helps us to understand the user stories before implementing them.
+
+Over the last months, we had several requests that could be unified under a
+common theme that is related to state and trace inspection.
+
+ - [#446][]
+ - [#795][]
+ - [#347][]
+ - [#303][]
+ - [#288][]
+
+This document is using [kettle][] as a running example. We assume that
+a Quint REPL session is run in the directory of the example:
+
+```sh
+$ cd ./tutorials/repl
+$ quint
+Quint REPL 0.9.1
+Type ".exit" to exit, or ".help" for more information
+>>> import kettle.* from "./kettle"
+
+```
+
+## Story 1: Inspect the current state
+
+*As a protocol reader, I want to print the protocol state without remembering
+the names of the state variables, so I can discover which state variables are
+around and which values they carry.*
+
+Assume that we have initialized the protocol state with `init`:
+
+```bluespec
+>>> init
+true
+```
+
+**Current interface**. Currently, we can inspect the state, by evaluating
+the variable names:
+
+```bluespec
+>>> temperature
+20
+>>> heatingOn
+false
+>>> beeping
+false
+```
+
+However, it is often more convenient to see the value of all the state variables
+at once, e.g., when we do not remember them. The issues [#446][] and [#795][]
+highlight this idea.
+
+A workaround is to introduce a definition like the following one:
+
+```bluespec
+// a handy definition that captures the state in a record
+val kettleState = {
+ heatingOn: heatingOn,
+ beeping: beeping,
+ temperature: temperature
+}
+```
+
+**Proposed interface**. The simplest yet powerful interface is to introduce the
+system state as a record that is accessible via a standard name. We decided to
+use the name `q::state`. Here is an example:
+
+```bluespec
+>>> q::state
+{
+ beeping: false,
+ heatingOn: false,
+ temperature: 20,
+}
+```
+
+Since `q::state` is simply a `val`, we would be do all kinds of programmatic things with it:
+
+```bluespec
+>>> q::state.fieldNames()
+Set("beeping", "heatingOn", "temperature")
+
+>>> q::state.temperature
+20
+```
+
+**Shortcut.** Since typing `q::state` often may be tedious, we offer a shortcut
+*`q::s` for `q::state`.
+
+## Story 2: Inspect the trace
+
+*As a protocol reader, I want to print the sequence of states that were visited
+on the way to the current protocol state, so I can see how the system was
+progressing.*
+
+Assume that we have executed a few steps:
+
+```bluespec
+>>> init
+true
+>>> pressButton
+true
+>>> heat
+true
+>>> depressButton
+true
+```
+
+**Current interface**. After executing a few steps, we can inspect the reached
+state. However, we would not be able to inspect the intermediate states, e.g.,
+the states reached by executing `init`, then `pressButton`, then `heat`.
+
+As mentioned in [#446][], it would be great to observe the sequence of visited
+states. Currently, the only way to do that is by replaying the actions from the
+start and printing the intermediate states after executing every action.
+
+**Proposed interface**. Similar to Story 1, we are proposing to use a standard
+name such as `q::trace`.
+
+For the sequence `init.then(pressButton).then(heat).then(depressButton)`, we
+expect `q::trace` to evaluate as follows:
+
+```bluespec
+>>> q::trace
+[
+ // 0
+ { beeping: false, heatingOn: false, temperature: 20 },
+ // 1
+ { beeping: false, heatingOn: true, temperature: 20 },
+ // 2
+ { beeping: false, heatingOn: true, temperature: 21 },
+ // 3*
+ { beeping: false, heatingOn: false, temperature: 21 },
+]
+```
+
+As we can see, `q::trace` is simply a value, which is printed as a
+syntactically correct Quint expression. We expect REPL to decorate it a bit with
+helpful comments: It should print the state numbers and highlight the active
+state (with a `*`). However, the fact that `q::trace` is a value, lets us to
+access it programmatically:
+
+```bluespec
+>>> q::trace.length()
+4
+>>> q::trace[3].temperature - q::trace[0].temperature
+1
+```
+
+**Shortcut.** Since typing `q::trace` may be tedious, we offer a shortcut
+`q::t` for `q::trace`.
+
+## Story 3: Navigate the trace
+
+*As a protocol reader, I want to jump between the visited states in the trace,
+so I can evaluate invariants against them and explore different paths.*
+
+As in Story 2, assume that we have executed a few steps:
+
+```bluespec
+>>> init
+true
+>>> pressButton
+true
+>>> heat
+true
+>>> depressButton
+true
+```
+
+**Current interface**. Assuming that `q::trace` from Story 2 is implemented,
+we should be able to see the intermediate states that are produced by the above
+sequence of actions. However, if we want to evaluate state invariants against
+the intermediate states, we have to replay the actions from start, e.g., by
+executing `init`, then `pressButton`, then `heat`.
+
+**Proposed interface**. We introduce several actions for navigating the trace.
+
+### 3.1. Jump
+
+The following REPL session highlights the expected interface:
+
+```bluespec
+>>> init.then(pressButton).then(heat).then(depressButton)
+true
+>>> q::jump(2)
+true
+>>> q::state
+{ beeping: false, heatingOn: true, temperature: 21 }
+>>> // we can evaluate expressions against the state
+>>> q::state.temperature > 20
+true
+>>> // the trace does not change
+>>> // the star is pointing to the active state
+>>> q::trace
+[
+ // 0
+ { beeping: false, heatingOn: false, temperature: 20 },
+ // 1
+ { beeping: false, heatingOn: true, temperature: 20 },
+ // 2*
+ { beeping: false, heatingOn: true, temperature: 21 },
+ // 3
+ { beeping: false, heatingOn: false, temperature: 21 },
+]
+```
+
+Importantly, `q::jump` does not modify the trace `q::trace`. Hence, we can jump
+forth and back in the current trace, without recomputing it. This is especially
+important, since some of the actions may be non-deterministic.
+
+### 3.2. Continue trace from the active state
+
+```bluespec
+>>> // ...continue the above session
+>>> heat
+true
+>>> // the trace continues from the active state
+>>> q::hist
+[
+ // 0
+ { beeping: false, heatingOn: false, temperature: 20 },
+ // 1
+ { beeping: false, heatingOn: true, temperature: 20 },
+ // 2
+ { beeping: false, heatingOn: true, temperature: 21 },
+ // 3*
+ { beeping: false, heatingOn: true, temperature: 22 },
+]
+```
+
+Note that when an action is evaluated, the trace beyond the active state is
+cleared, and the new state is added after the active state.
+
+### 3.3. Clear the trace
+
+The trace is accumulating the states, even when `init` is executed. Hence, at
+some point, we have to clear the trace:
+
+```bluespec
+>>> // ...continue the above session
+>>> q::reset
+true
+>>> q::trace
+[]
+```
+
+
+
+[#446]: https://github.com/informalsystems/quint/issues/446
+[#795]: https://github.com/informalsystems/quint/issues/795
+[#347]: https://github.com/informalsystems/quint/issues/347
+[#303]: https://github.com/informalsystems/quint/issues/303
+[#288]: https://github.com/informalsystems/quint/issues/288
+[kettle]: https://github.com/informalsystems/quint/blob/main/tutorials/repl/kettle.qnt
\ No newline at end of file
diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
index 50458eeee..e64273133 100755
--- a/examples/.scripts/run-example.sh
+++ b/examples/.scripts/run-example.sh
@@ -34,26 +34,35 @@ result () {
"$file" =~ ^cryptography/ ||
"$file" =~ ^spells/ ||
"$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
- "$file" == "cosmos/ics20/base.qnt" ) ]] ; then
+ "$file" == "cosmos/ics20/base.qnt" ||
+ "$file" == "cosmos/bank/bank.qnt" ) ]] ; then
printf "N/A[^nostatemachine]"; return
fi
# Run the command and record success / failure
local quint_cmd="quint $cmd $args $file"
+ local succeeded=false
if ($quint_cmd &> /dev/null)
then
printf ":white_check_mark:"
+ succeeded=true
else
printf ":x:"
+ succeeded=false
fi
- # Print additional explanations
- if [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && "$cmd" == "verify" ]] ; then
- printf "https://github.com/informalsystems/quint/issues/1034"
- elif [[ "$file" == "language-features/option.qnt" && "$cmd" == verify ]] ; then
- printf "https://github.com/informalsystems/quint/issues/1034"
- elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
- printf "https://github.com/informalsystems/quint/issues/1019"
+ # We only want to print additional info to annotate failing results
+ if [[ $succeeded == false ]]; then
+ # Print additional explanations
+ if [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
+ printf "https://github.com/informalsystems/quint/issues/1285"
+ elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && "$cmd" == "verify" ]] ; then
+ printf "https://github.com/informalsystems/quint/issues/1284"
+ elif [[ "$file" == "classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt" && "$cmd" =~ (test|verify) ]] ; then
+ printf "https://github.com/informalsystems/quint/issues/1299"
+ elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then
+ printf "https://github.com/informalsystems/quint/issues/1393"
+ fi
fi
}
@@ -66,6 +75,8 @@ get_main () {
main="--main=ReadersWriters_5"
elif [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" ]] ; then
main="--main=ewd840_3"
+ elif [[ "$file" == "classic/distributed/TwoPhaseCommit/two_phase_commit.qnt" ]] ; then
+ main="--main=two_phase_commit_3"
elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" ]] ; then
main="--main=Paxos_val2_accept3_quorum2"
elif [[ "$file" == "classic/sequential/BinSearch/BinSearch.qnt" ]] ; then
@@ -82,6 +93,8 @@ get_main () {
main="--main=Lightclient_4_3_correct"
elif [[ "$file" == "puzzles/prisoners/prisoners.qnt" ]] ; then
main="--main=prisoners3"
+ elif [[ "$file" == "games/secret-santa/secret_santa.qnt" ]] ; then
+ main="--main=quint_team_secret_santa"
elif [[ "$file" == "solidity/ERC20/erc20.qnt" ]] ; then
main="--main=erc20Tests"
elif [[ "$file" == "solidity/SimplePonzi/simplePonzi.qnt" ]] ; then
@@ -118,6 +131,8 @@ get_verify_args () {
args="--init=n4_f1::Init --step=n4_f1::Next --invariant=n4_f1::Agreement"
elif [[ "$file" == "cosmos/ics23/ics23.qnt" ]] ; then
args="--init=Init --step=Next"
+ elif [[ "$file" == "games/tictactoe/tictactoe.qnt" ]] ; then
+ args="--max-steps=1" # pretty slow, and we just want to check that verification can run
fi
echo "${args}"
}
diff --git a/examples/README.md b/examples/README.md
index 2e536ee2b..0abecf829 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -51,10 +51,14 @@ listed without any additional command line arguments.
| [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1034 |
+| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1284 |
| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1299 | :x:https://github.com/informalsystems/quint/issues/1299 |
| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/bank/bank.qnt](./cosmos/bank/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
| [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -62,7 +66,7 @@ listed without any additional command line arguments.
| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
| [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -70,6 +74,8 @@ listed without any additional command line arguments.
| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cryptography/hashes.qnt](./cryptography/hashes.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [cryptography/hashesTest.qnt](./cryptography/hashesTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [games/secret-santa/secret_santa.qnt](./games/secret-santa/secret_santa.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [games/tictactoe/tictactoe.qnt](./games/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [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: |
@@ -80,17 +86,16 @@ listed without any additional command line arguments.
| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1034 |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1393 |
| [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [puzzles/tictactoe/tictactoe.qnt](./puzzles/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [solidity/Coin/coin.qnt](./solidity/Coin/coin.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1019 |
+| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1285 |
| [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
| [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
diff --git a/examples/classic/distributed/TwoPhaseCommit/two_phase_commit.qnt b/examples/classic/distributed/TwoPhaseCommit/two_phase_commit.qnt
new file mode 100644
index 000000000..48410ce24
--- /dev/null
+++ b/examples/classic/distributed/TwoPhaseCommit/two_phase_commit.qnt
@@ -0,0 +1,158 @@
+// -*- mode: Bluespec; -*-
+
+/* This specification stems from the specification of the two phase protocol
+ by Leslie Lamport:
+
+ https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla */
+
+module two_phase_commit {
+ const resourceManagers: Set[str]
+
+ type ResourceManagerState = Working | Prepared | Committed | Aborted
+ type TransactionManagerState = Init | TMCommitted | TMAborted
+ type Message =
+ | Abort
+ | Commit
+ | RMPrepared(str)
+
+ var RM::states: str -> ResourceManagerState
+ var TM::state: TransactionManagerState
+ /// The set of resource managers from which the transaction manager has
+ /// received RMPrepared messages
+ var TM::preparedRMs: Set[str]
+ var messages: Set[Message]
+
+ action init = all {
+ RM::states' = resourceManagers.mapBy(r => Working),
+ TM::state' = Init,
+ TM::preparedRMs' = Set(),
+ messages' = Set(),
+ }
+
+ /* Transaction Manager (TM) actions */
+
+ /// The transaction manager receives a RMPrepared(rm) message from the resource manager rm
+ action TM::addPreparedResourceManager(resourceManager: str): bool = all {
+ TM::state == Init,
+ messages.contains(RMPrepared(resourceManager)),
+ TM::preparedRMs' = TM::preparedRMs.union(Set(resourceManager))
+ }
+
+ /// The transaction manager commits the transaction; enabled iff the
+ /// transaction manager is in its initial state and every resource manager has
+ /// sent an RMPrepared message.
+ action TM::decideOnCommit = all {
+ TM::state == Init,
+ TM::preparedRMs == resourceManagers,
+ TM::state' = TMCommitted,
+ messages' = messages.union(Set(Commit))
+ }
+
+ /// The transaction manager spontaneously aborts the transaction
+ action TM::decideOnAbort = all {
+ TM::state == Init,
+ TM::state' = TMAborted,
+ messages' = messages.union(Set(Abort))
+ }
+
+ /* Resource Manager (RM) actions */
+
+ /// A resource manager prepares
+ action RM::prepare(resourceManager: str): bool = all {
+ RM::states.get(resourceManager) == Working,
+ RM::states' = RM::states.set(resourceManager, Prepared),
+ messages' = messages.union(Set(RMPrepared(resourceManager)))
+ }
+
+ /// A resource manager aborts, either spontaneously or because of an Abort message
+ action RM::abort(resourceManager: str): bool = all {
+ or {
+ // Resource manager chooses to abort
+ RM::states.get(resourceManager) == Working,
+ // Resource manager receives an abort message from the transaction manager
+ messages.contains(Abort),
+ },
+ RM::states' = RM::states.set(resourceManager, Aborted),
+ // There is no need to let others know that this resource manager aborted
+ messages' = messages
+ }
+
+ // A resource manager commits due to a Commit message
+ action RM::commit(resourceManager: str): bool = all {
+ messages.contains(Commit),
+ RM::states' = RM::states.set(resourceManager, Committed),
+ messages' = messages
+ }
+
+ action step = any {
+ // Resource manager actions
+ all {
+ nondet rm = resourceManagers.oneOf()
+ any { RM::prepare(rm), RM::abort(rm), RM::commit(rm) },
+ TM::state' = TM::state,
+ TM::preparedRMs' = TM::preparedRMs,
+ },
+ // Transaction manager decisions (commit or abort)
+ all {
+ any { TM::decideOnCommit, TM::decideOnAbort },
+ TM::preparedRMs' = TM::preparedRMs,
+ RM::states' = RM::states,
+ },
+ // Transaction managers message consumption
+ all {
+ nondet rm = resourceManagers.oneOf()
+ TM::addPreparedResourceManager(rm),
+ TM::state' = TM::state,
+ RM::states' = RM::states,
+ messages' = messages,
+ }
+ }
+
+ /// Two resource managers have not arrived at conflicting decisions
+ val consistencyInv = tuples(resourceManagers, resourceManagers).forall(((r1, r2)) =>
+ not(RM::states.get(r1) == Committed and RM::states.get(r2) == Aborted)
+ )
+}
+
+module two_phase_commit_3 {
+ import two_phase_commit(resourceManagers = Set("rm1", "rm2", "rm3")).*
+
+ /// Compose two actions: send an RMPrepare message and consume it in the
+ /// transaction manager
+ run preparation(rm) = (all {
+ RM::prepare(rm),
+ TM::state' = TM::state,
+ TM::preparedRMs' = TM::preparedRMs,
+ }).then(all {
+ TM::addPreparedResourceManager(rm),
+ TM::state' = TM::state,
+ RM::states' = RM::states,
+ messages' = messages,
+ })
+
+ /// Compose several actions: The transaction manager decides to commit and
+ /// each resource manager consumes its Commit message
+ run commitment = (all {
+ TM::decideOnCommit,
+ TM::preparedRMs' = TM::preparedRMs,
+ RM::states' = RM::states,
+ }).then(all {
+ RM::commit("rm1"),
+ TM::state' = TM::state,
+ TM::preparedRMs' = TM::preparedRMs,
+ }).then(all {
+ RM::commit("rm2"),
+ TM::state' = TM::state,
+ TM::preparedRMs' = TM::preparedRMs,
+ }).then(all {
+ RM::commit("rm3"),
+ TM::state' = TM::state,
+ TM::preparedRMs' = TM::preparedRMs,
+ })
+
+ run successTest = init
+ .then(preparation("rm1"))
+ .then(preparation("rm2"))
+ .then(preparation("rm3"))
+ .then(commitment)
+}
diff --git a/examples/classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt b/examples/classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt
new file mode 100644
index 000000000..3bc33c343
--- /dev/null
+++ b/examples/classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt
@@ -0,0 +1,208 @@
+// -*- mode: Bluespec; -*-
+
+/* This specification is a variation on ./two_phase_commit.qnt that experiments with
+ using modules to divides the state spaces to reflect possible state access in the
+ system.
+*/
+
+module message {
+ type T =
+ | Abort
+ | Commit
+ | Prepared(str)
+
+ var channel: Set[T]
+
+ action init: bool = {
+ channel' = Set()
+ }
+
+ action stutter = all {
+ channel' = channel
+ }
+
+ action send(m: T): bool = {
+ channel' = channel.union(Set(m))
+ }
+
+}
+
+module resource_managers {
+ import message as msg
+
+ type Status = | Working | Prepared | Committed | Aborted
+ var statuses : str -> Status
+
+ action init(rms: Set[str]): bool = {
+ statuses' = rms.mapBy(r => Working)
+ }
+
+ action stutter = all {
+ statuses' = statuses
+ }
+
+ action prepare(resourceManager: str): bool = all {
+ statuses.get(resourceManager) == Working,
+ statuses' = statuses.set(resourceManager, Prepared),
+ msg::send(msg::Prepared(resourceManager))
+ }
+
+ action abort(resourceManager: str): bool = all {
+ or {
+ // Resource manager is working, and chooses to abort spontaneously
+ statuses.get(resourceManager) == Working,
+ // Resource manager receives an abort message from the transaction manager
+ msg::channel.contains(msg::Abort),
+ },
+ statuses' = statuses.set(resourceManager, Aborted),
+ // There is no need to let others know that this resource manager aborted
+ msg::stutter,
+ }
+
+
+ // A resource manager commits due to a Commit message
+ action commit(resourceManager: str): bool = all {
+ msg::channel.contains(msg::Commit),
+ statuses' = statuses.set(resourceManager, Committed),
+ msg::stutter,
+ }
+
+
+ def consistencyInv(resourceManagers) =
+ tuples(resourceManagers, resourceManagers)
+ .forall(((r1, r2)) =>
+ not( statuses.get(r1) == Committed
+ and
+ statuses.get(r2) == Aborted))
+}
+
+module transaction_manager {
+ import message as msg
+
+ type Status = | TMInitiated | TMCommitted | TMAborted
+
+ var status : Status
+ /// The set of resource managers from which the transaction manager has
+ /// received msg::Prepared messages
+ var preparedRMs : Set[str]
+
+ action init: bool = all {
+ status' = TMInitiated,
+ preparedRMs' = Set(),
+ }
+
+ action stutter = all {
+ status' = status,
+ preparedRMs' = preparedRMs,
+ }
+
+ /// The transaction manager receives a RMPrepared(rm) message from the resource manager rm
+ action addPreparedResourceManager(resourceManager: str): bool = all {
+ status == TMInitiated,
+ msg::channel.contains(msg::Prepared(resourceManager)),
+ preparedRMs' = preparedRMs.union(Set(resourceManager)),
+ status' = status,
+ }
+
+ /// The transaction manager commits the transaction; enabled iff the
+ /// transaction manager is in its initial state and every resource manager has
+ /// sent an RMPrepared message.
+ action decideOnCommit(resourceManagers) = all {
+ status == TMInitiated,
+ preparedRMs == resourceManagers,
+ status' = TMCommitted,
+ preparedRMs' = preparedRMs,
+ msg::send(msg::Commit)
+ }
+
+ /// The transaction manager spontaneously aborts the transaction
+ action decideOnAbort = all {
+ status == TMInitiated,
+ status' = TMAborted,
+ preparedRMs' = preparedRMs,
+ msg::send(msg::Abort)
+ }
+}
+
+module two_phase_commit {
+ const resourceManagers: Set[str]
+
+ import resource_managers as RM
+ import transaction_manager as TM
+ import message as msg
+
+ action step = any {
+ // Resource manager actions
+ all {
+ nondet rm = resourceManagers.oneOf()
+ any { RM::prepare(rm),
+ RM::abort(rm),
+ RM::commit(rm) },
+ TM::stutter
+ },
+ // Transaction manager decisions (commit or abort)
+ all {
+ any { TM::decideOnCommit(resourceManagers),
+ TM::decideOnAbort },
+ RM::stutter,
+ },
+ // Transaction managers message consumption
+ all {
+ nondet rm = resourceManagers.oneOf()
+ TM::addPreparedResourceManager(rm),
+ RM::stutter,
+ msg::stutter
+ }
+ }
+
+ action init = all {
+ msg::init,
+ TM::init,
+ RM::init(resourceManagers),
+ }
+
+ /// Two resource managers have not arrived at conflicting decisions
+ val inv = RM::consistencyInv(resourceManagers)
+}
+
+module two_phase_commit_tests {
+ import two_phase_commit(resourceManagers = Set("rm1", "rm2", "rm3")).*
+
+ import resource_managers as RM
+ import transaction_manager as TM
+ import message as msg
+
+ /// Compose two actions: send an RMPrepare message and consume it in the
+ /// transaction manager
+ run preparation(rm) = (all {
+ RM::prepare(rm),
+ TM::stutter,
+ }).then(all {
+ TM::addPreparedResourceManager(rm),
+ RM::stutter,
+ msg::stutter,
+ })
+
+ /// Compose several actions: The transaction manager decides to commit and
+ /// each resource manager consumes its Commit message
+ run commitment = (all {
+ TM::decideOnCommit(resourceManagers),
+ RM::stutter
+ }).then(all {
+ RM::commit("rm1"),
+ TM::stutter
+ }).then(all {
+ RM::commit("rm2"),
+ TM::stutter
+ }).then(all {
+ RM::commit("rm3"),
+ TM::stutter
+ })
+
+ run successTest = init.then(step).then(step)
+ // run successTest = init
+ // .then(preparation("rm1"))
+ // .then(preparation("rm2"))
+ // .then(preparation("rm3"))
+ // .then(commitment)
+}
diff --git a/examples/cosmos/bank/bank.qnt b/examples/cosmos/bank/bank.qnt
new file mode 100644
index 000000000..73353dec8
--- /dev/null
+++ b/examples/cosmos/bank/bank.qnt
@@ -0,0 +1,202 @@
+// -*- mode: Bluespec; -*-
+// An executable specification of the bank module
+module bank {
+ //----------------------- type declarations -------------------------
+ // Addresses are simply strings
+ type Addr = str
+ // Denominations are simply strings too
+ type Denom = str
+ // 64-bit and 256-bit integers are a special case of big integers.
+ // We have to take care of the bit width where it matters.
+ type Int64 = int
+ type Int256 = int
+
+ // the maximum value for Int256 in Golang
+ pure val MAX_INT256 = 2^256 - 1
+
+ // the range of 256-bit integers in the SDK
+ pure def isInt256(i: int): bool = -2^256 < i and i < 2^256
+
+ // A coin is a record that contains a denomination and an amount
+ type Coin = { denom: Denom, amount: Int256 }
+ // Coins is a map from denominations to amounts
+ type Coins = Denom -> Int256
+ // Account balances
+ type Balance = { address: Addr, coins: Coins }
+
+ // A result that is produced by the functions that update the context
+ type BankResult =
+ | BankErr(str)
+ | BankOk(BankCtx)
+
+ // A result that is produced by the functions that return a coin or panic
+ type CoinResult =
+ | CoinErr(str)
+ | CoinOk(Coin)
+
+ // A result that is produced by the functions that return a Boolean or panic
+ type BoolResult =
+ | BoolErr(str)
+ | BoolOk(bool)
+
+ // An input of a multiparty transfer
+ type Input = {
+ address: str,
+ coins: Coins,
+ }
+ // An output of a multiparty transfer
+ type Output = {
+ address: str,
+ coins: Coins,
+ }
+ // the portion of the context that is accessed by the bank module
+ type BankCtx = {
+ // block time (needed by vesting accounts)
+ blockTime: Int64,
+ // accessed via AccountKeeper
+ accounts: Set[Addr],
+ // the balances are the essential part of the bank module
+ balances: Addr -> Coins,
+ // module parameters
+ params: Params,
+ }
+
+ // Parameters of the bank module
+ type Params = {
+ // whether coin send is enabled for specific denominations
+ sendEnabled: Set[{ denom: str, enabled: bool }],
+ // whether coin send is enabled by default
+ defaultSendEnabled: bool,
+ }
+
+ //------- the module logic, that is, the logic of keepers -----------
+
+ /// `GetAllBalances` returns all the account balances for the given account address.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L61
+ pure def ViewKeeper::GetAllBalances(ctx: BankCtx, addr: Addr): Coins = {
+ if (ctx.balances.keys().contains(addr)) {
+ ctx.balances.get(addr)
+ } else {
+ Map()
+ }
+ }
+
+ /// `ValidateBalance` should only be called upon genesis state.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L202
+ pure def ViewKeeper::ValidateBalance(ctx: BankCtx, addr: Addr): bool = and {
+ ctx.accounts.contains(addr),
+ val coins = ViewKeeper::GetAllBalances(ctx, addr)
+ // Implementation: Coins.IsValid also validates denominations
+ coins.keys().forall(denom => coins.get(denom) > 0),
+ // TODO: add validation logic for the vesting accounts
+ }
+
+ /// GetBalance returns the balance of a specific denomination for a given account by address.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L98
+ pure def ViewKeeper::GetBalance(ctx: BankCtx, addr: Addr, denom: str): CoinResult = {
+ if (ctx.balances.keys().contains(addr)) {
+ val accountBal = ctx.balances.get(addr)
+ if (accountBal.keys().contains(denom)) {
+ CoinOk({ denom: denom, amount: accountBal.get(denom) })
+ } else {
+ CoinErr("Unmarshal error")
+ }
+ } else {
+ CoinErr("Unmarshal error")
+ }
+ }
+
+ /// HasBalance returns whether or not an account has at least amt balance.\
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L56
+ pure def ViewKeeper::HasBalance(ctx: BankCtx, addr: Addr, coin: Coin): BoolResult = {
+ // Implementation: panic if the address or denomination are not stored?
+ match ViewKeeper::GetBalance(ctx, addr, coin.denom) {
+ | CoinOk(c) => BoolOk(c.amount >= coin.amount)
+ | CoinErr(msg) => BoolErr(msg)
+ }
+ }
+
+ /// GetAccountsBalances returns all the accounts balances from the store.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L72
+ pure def ViewKeeper::GetAccountsBalances(ctx: BankCtx): Set[Balance] = {
+ // The implementation may panic due to unmarshalling errors.
+ // Since these errors are not related to the parameters, we do not propagate them.
+ ctx.balances.keys().map(a => { address: a, coins: ctx.balances.get(a) })
+ }
+
+ /// SendCoins transfers amt coins from a sending account to a receiving account.
+ /// An error is returned upon failure.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L135
+ pure def SendKeeper::SendCoins(ctx: BankCtx,
+ fromAddr: Addr, toAddr: Addr, amt: Coins): BankResult = {
+ // Implementation: if Coins are constructed with NewCoins, they must be positive.
+ // However, if they are constructed another way, there is no precondition.
+ // TODO: checking LockedCoins that deal with vested coins.
+ // Safely subtract the coins from fromAddr and add them to toAddr.
+ val fromCoins = ViewKeeper::GetAllBalances(ctx, fromAddr)
+ if (amt.keys().exists(d =>
+ not(d.in(fromCoins.keys())) or fromCoins.get(d) < amt.get(d))) {
+ // some denominations do not exist on fromAddr, or there is not enough funds
+ BankErr("invalid coins or insufficient funds")
+ } else {
+ // x/bank invariants prohibit persistence of zero balances
+ // clean zero balances
+ def getOr0(coins: Coins, d: str): int = if (d.in(coins.keys())) coins.get(d) else 0
+ val positiveDenoms = fromCoins.keys().filter(d => fromCoins.get(d) > getOr0(amt, d))
+ val subCoins = positiveDenoms.mapBy(d => fromCoins.get(d) - getOr0(amt, d))
+ // add coins to toAddr: the tricky part is that the denominations may differ
+ val toCoins = ViewKeeper::GetAllBalances(ctx, toAddr)
+ // extend the toCoins and amt with zeroes over the joint denominations
+ val jointDenoms = toCoins.keys().union(amt.keys())
+ // since toCoins and amt held positive values, their sums must be positive too
+ val addCoins = jointDenoms.mapBy(d => getOr0(toCoins, d) + getOr0(amt, d))
+ if (addCoins.keys().exists(d => addCoins.get(d) > MAX_INT256)) {
+ BankErr("overflow")
+ } else {
+ // add toAddr to the accounts, if it did not exist
+ val newAccounts = ctx.accounts.union(Set(toAddr))
+ val newBalances =
+ if (fromAddr == toAddr) {
+ ctx.balances
+ } else {
+ // Update the balance of fromAddr with subCoins.
+ val newBalancesSub = ctx.balances.set(fromAddr, subCoins)
+ // Since toAddr may be a new account, extend the map, if needed
+ newBalancesSub.put(toAddr, addCoins)
+ }
+ // succeed with a new balance
+ BankOk({ ...ctx, balances: newBalances, accounts: newAccounts })
+ }
+ }
+ }
+
+ /// GetParams returns the total set of bank parameters.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L61
+ pure def SendKeeper::GetParams(ctx: BankCtx): Params = ctx.params
+
+ /// SetParams sets the total set of bank parameters.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L67
+ pure def SendKeeper::SetParams(ctx: BankCtx, params: Params): BankCtx = {
+ { ...ctx, params: params }
+ }
+
+ /// IsSendEnabledCoin returns the current SendEnabled status of the provided coin's denom.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L315
+ pure def SendKeeper::IsSendEnabledCoin(ctx: BankCtx, coin: Coin): bool = {
+ val found = ctx.params.sendEnabled.filter(p => coin.denom == p.denom)
+ if (found != Set()) {
+ found.exists(p => p.enabled)
+ } else {
+ ctx.params.defaultSendEnabled
+ }
+ }
+
+ /// IsSendEnabledCoins checks the coins provide and returns an ErrSendDisabled if
+ /// any of the coins are not configured for sending. Returns nil if sending is enabled
+ /// for all provided coin.
+ /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L306C28-L306C28
+ pure def SendKeeper::IsSendEnabledCoins(ctx: BankCtx, coins: Set[Coin]): bool = {
+ // Implementation: return the error ErrSendDisabled on false
+ coins.forall(c => SendKeeper::IsSendEnabledCoin(ctx, c))
+ }
+}
diff --git a/examples/cosmos/bank/bankTest.qnt b/examples/cosmos/bank/bankTest.qnt
new file mode 100644
index 000000000..d721d54d0
--- /dev/null
+++ b/examples/cosmos/bank/bankTest.qnt
@@ -0,0 +1,117 @@
+// -*- mode: Bluespec; -*-
+module bankTest {
+ import bank.* from "./bank"
+
+ // the state of the machine that tests the logic
+ // Total supply of coins per denomination
+ var supply: Denom -> Int256
+ // Balances for each address
+ var balances: Addr -> Coins
+ // if non-empty, then it stores the last error message
+ var _lastError: str
+ // all addresses we would like to work with
+ pure val ADDR = Set("king", "donkeykong", "peaches", "mario")
+ // all denominations
+ pure val DENOM = Set("banana", "burger")
+
+ // state transitions of the machine
+ // initialize the state machine
+ action init = all {
+ // limit the total supply of burgers and bananas to 10_000
+ supply' = Set("banana", "burger").mapBy(d => 10_000),
+ // the king has it all
+ balances' = Map("king" -> Set("banana", "burger").mapBy(d => 10_000)),
+ _lastError' = "",
+ }
+
+ action send(fromAddr: Addr, toAddr: Addr, coins: Coins): bool = all {
+ val ctx = stateToCtx(0)
+ val result = SendKeeper::SendCoins(ctx, fromAddr, toAddr, coins)
+ match result {
+ | BankOk(newCtx) => all {
+ balances' = newCtx.balances,
+ supply' = supply,
+ _lastError' = "",
+ }
+ | BankErr(msg) => all {
+ // We could simply return 'false' here.
+ // But we prefer to store the error message instead.
+ _lastError' = msg,
+ balances' = balances,
+ supply' = supply,
+ }
+ }
+ }
+
+ action step = any {
+ nondet fromAddr = oneOf(ADDR)
+ nondet toAddr = oneOf(ADDR)
+ nondet denom = oneOf(DENOM)
+ nondet amt = (-10).to(supply.get(denom)).oneOf()
+ send(fromAddr, toAddr, Set(denom).mapBy(d => amt))
+ }
+
+ // protocol invariants
+ // sum up amounts over all balances for a given denomination
+ def sumForDenom(denom: Denom): Int256 = {
+ balances.keys().fold(0, (sum, addr) => {
+ val coins = balances.get(addr)
+ if (denom.in(coins.keys())) {
+ sum + coins.get(denom)
+ } else {
+ sum
+ }
+ })
+ }
+
+ // The total Supply of the network is equal to the sum of all coins from the account
+ val totalSupplyInv = {
+ supply.keys().forall(denom => (sumForDenom(denom) == supply.get(denom)))
+ }
+
+ // tests
+ run getAllBalancesTest = {
+ init
+ .expect(
+ val ctx = stateToCtx(0)
+ val kings = ViewKeeper::GetAllBalances(ctx, "king")
+ val donkeys = ViewKeeper::GetAllBalances(ctx, "donkeykong")
+ and {
+ assert(kings.keys() == Set("banana", "burger")),
+ assert(kings.get("banana") == 10_000),
+ assert(kings.get("burger") == 10_000),
+ assert(donkeys.keys() == Set()),
+ }
+ )
+ }
+
+ // a helper operator that produces a context from a state
+ def stateToCtx(time: int): BankCtx = {
+ {
+ blockTime: time,
+ accounts: balances.keys(),
+ balances: balances,
+ params: {
+ sendEnabled: Set(),
+ defaultSendEnabled: true
+ }
+ }
+ }
+
+ run sendTest = {
+ init
+ // the King has bananas and he can send it
+ .then(send("king",
+ "donkeykong",
+ Map("banana" -> 2_000)))
+ .expect(and {
+ balances.get("king").get("banana") == 8_000,
+ balances.get("donkeykong").get("banana") == 2_000,
+ balances.get("king").get("burger") == 10_000,
+ balances.get("donkeykong").keys() == Set("banana"),
+ })
+ // Donkeykong does not have any burgers, so this action must fail
+ .then(send("donkeykong", "peaches", Set("burger").mapBy(d => 1_000)))
+ .expect(_lastError == "invalid coins or insufficient funds")
+ }
+}
diff --git a/examples/cosmos/bank/cosmos-bank.md b/examples/cosmos/bank/cosmos-bank.md
new file mode 100644
index 000000000..c8ddcabf8
--- /dev/null
+++ b/examples/cosmos/bank/cosmos-bank.md
@@ -0,0 +1,739 @@
+# Onboarding to the module `x/bank` of Cosmos SDK
+
+**Author**: Igor Konnov, Informal Systems, 2023
+
+**Version**: Cosmos SDK [v0.46.10](https://github.com/cosmos/cosmos-sdk/blob/v0.46.10/).
+
+**This page is still experimental. We believe that Cosmos documentation will
+become executable one day.**
+
+## Abstract
+
+This document shows how we could turn an inanimate piece of documentation into
+an executable specification. We are using the [bank module][] of Cosmos SDK as
+an example. In the following, all of the quoted text belongs to the original
+description on the [bank module][] page, unless specified otherwise. To obtain
+a Quint module, run [lmt][] against this document. Check the executable
+specification in [bank.qnt](./bank.qnt) and [bankTest.qnt](./bankTest.qnt).
+We follow the same order of exposition, as in the original document.
+
+Importantly, this description is tuned towards ease of exposition, not for
+implementation or verification. Remember that we do not want to make protocols
+as complex as their implementation! These are the most illuminating differences:
+
+ - We use abstract data types whenever possible, e.g., big integers, sets, and maps.
+
+ - We abstract error codes to `true` (no error) and `false` (error). The actual
+ error codes belong to the implementation details. They are written in comments.
+
+> The bank module is responsible for handling multi-asset coin transfers
+> between accounts and tracking special-case pseudo-transfers which must work
+> differently with particular kinds of accounts (notably
+> delegating/undelegating for vesting accounts). It exposes several interfaces
+> with varying capabilities for secure interaction with other modules which
+> must alter user balances.
+>
+> In addition, the bank module tracks and provides query support for the total
+> supply of all assets used in the application.
+
+From the engineer's perspective, the bank module looks as follows:
+
+```bluespec bank.qnt +=
+// -*- mode: Bluespec; -*-
+// An executable specification of the bank module
+module bank {
+ //----------------------- type declarations -------------------------
+ <<
+ 
+ 
+ 
+