Merge pull request #1587 from informalsystems/gabriela/basic-docs

Basic documentation that's missing from the website

docs/pages/docs/_meta.json

@@ -1,25 +1,52 @@
 {
-  "index": "Introduction",
+  "-- Introduction": {
+    "type": "separator",
+    "title": "Introduction"
+  },
+  "why": "Why?",
+  "what-does-quint-do": "What does Quint do?",
   "getting-started": "Getting Started",
-  "lang": "Language Manual",
-  "quint": "CLI Manual",
-  "builtin": "Built-in Operators",
-  "previews": "Tool previews",
   "faq": "FAQ",
-   "-- Learning": {
+  "-- Writing specifications": {
     "type": "separator",
-    "title": "Learning"
+    "title": "Writing specifications"
   },
-  "repl": "Using the REPL",
-  "lessons": "Lessons",
+  "language-basics": "Language Basics",
+  "lessons": "Interactive lessons",
   "blogposts": "Blog Posts",
+  "cheatsheet-link": {
+    "title": "Cheatsheet ↵",
+    "href": "/quint-cheatsheet.pdf"
+  },
+  "examples-link": {
+    "title": "Examples ↵",
+    "href": "https://github.com/informalsystems/quint/tree/main/examples"
+  },
+  "-- Using specifications": {
+    "type": "separator",
+    "title": "Using specifications"
+  },
+  "checking-properties": "Checking properties",
+  "repl": "Interacting with REPL",
   "literate": "Literate Specifications",
-   "-- Development": {
+  "model-based-testing": "Model-Based Testing",
+  "-- How the tools work": {
+    "type": "separator",
+    "title": "How the tools work"
+  },
+  "model-checkers": "Model Checkers",
+  "simulator": "Understanding the Simulator",
+  "-- Reference Documentation": {
+    "type": "separator",
+    "title": "Reference Documentation"
+  },
+  "lang": "Language Manual",
+  "quint": "CLI Manual",
+  "builtin": "Built-in Operators",
+  "-- Development": {
     "type": "separator",
     "title": "Design & Development"
   },
   "design-principles": "",
-  "architecture-decision-records": "Architecture Decision Records (ADRs)",
-  "rfcs": "Requests for Comments (RFCs)",
-  "stories": "User Stories"
+  "development-docs": "Development Docs"
 }

docs/pages/docs/checking-properties.mdx

@@ -0,0 +1,93 @@
+import { Callout } from 'nextra/components'
+
+# Checking Properties
+
+<Callout type="warning" emoji="🚧️">
+  This page is under construction.
+</Callout>
+
+The main way to interact with a Quint model is by checking properties. The [simulator](./simulator) can be used to increase the confidence on a property, and [model checkers](./model-checkers) can be used to formally verify them. Properties can also be used to query the model and understand it better, finding interesting scenarios.
+
+## Actual properties
+
+Thinking about a system's properties is not an easy task, but can often be useful to increase understanding in many ways. Writing those properties in Quint enables using the tools (simulator or model checkers) to check that property, or to find out where it doesn't hold and adjust the model or the expectations about it.
+
+A system might have safety and/or liveness properties.
+- Safety: something *bad* never happens
+  - Examples: balances should never be negative, two different wallets may never hold the same NFT, honest consensus parties may never agree on different values.
+- Liveness: something *good* eventually happens
+  - Examples: eventually all parties decide on a value, eventually termination is detected, eventually a system stabilizes.
+
+It is much easier to write and check safety properties, which can be written as invariants. Liveness properties require temporal formulas, which often rely on assumptions about fairness to be useful, and that may require some hours of study time if you are not familiar already. Also, there are other, more practical, ways to convince ourselves that good things are happening (see below). Safety properties go a long way, start with those. Writing a safety property is as simple as writing a boolean expression:
+
+```quint
+val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0)
+```
+
+`balances` in this expression (considering the model from the [Getting Started](./getting-started) guide) is a state variable. While checking `no_negatives` as an invariant, Quint's tools will check this expression on every state, meaning it will evaluate it for different values of `balances` and expect it to always be true. It needs to be true in the initial state and in every possible state that comes from it - it cannot *vary*, as it is an *invariant*.
+
+## Non-properties to find interesting scenarios
+
+While invariants are things that need to hold on **every** state, sometimes we want to check that something is true in **some** state - a sort of sanity check. For that, we define witness properties.
+
+<Callout type="warning" emoji="🚧️">
+  Quint's built-in support for witness properties is under design. Expect more features in the near future.
+</Callout>
+
+There are currently two ways to define and check witness properties:
+1. Through the `--witnesses` flag of the simulator
+2. Through an invariant (`--invariant`) of the simulator (or the model checker, but you probably won't need it)
+
+### Counting interesting traces with `--witnesses`
+For (1), you define something that you want to be possible:
+
+```quint
+val alice_more_than_bob = balances.get("alice") > balances.get("bob")
+```
+
+The example above states that it should be possible for Alice to have more balance than Bob. This for sure won't be true for every possible state, but it needs to hold for some of them.
+
+Let's ask the simulator to check this witness:
+```sh
+quint run gettingStarted.qnt --witnesses=alice_more_than_bob --max-steps=5
+```
+
+Quint reports:
+```ansi
+[ok] No violation found (599ms).
+You may increase --max-samples and --max-steps.
+Use --verbosity to produce more (or less) output.
+Witnesses:
+alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
+Use --seed=0x1c8a2137939c73 to reproduce.
+```
+
+And that informs us that, in most executions, there is a state where Alice has a larger balance than that of Bob.
+
+<Callout>
+  This is a way to find that "good things are happening" without a liveness property. It is not the same as a liveness property, but it's a practical alternative that is enough in many scenarios. 
+</Callout>
+
+### Inspecting interesting traces with `--invariant`
+
+If we concretely want to see the trace witnessing our property, we can negate that property (add a `not` in front of it) and ask the simulator to check that as an invariant. This is like asking the simulator "is the property false in all states?" to which it may reply "no! Here's a scenario in where it is true".
+
+```sh
+quint run gettingStarted.qnt --invariant="not(alice_more_than_bob)" --max-steps=5
+```
+
+Quint reports:
+```ansi
+An example execution:
+
+[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
+
+[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
+
+[violation] Found an issue (8ms).
+Use --verbosity=3 to show executions.
+Use --seed=0xa0bbf64f2c03 to reproduce.
+error: Invariant violated
+```
+
+Although it says "Invariant violated", this is exactly what we wanted: an example where Alice has more balance than Bob.

docs/pages/docs/development-docs/_meta.json

@@ -0,0 +1,5 @@
+{
+  "architecture-decision-records": "Architecture Decision Records (ADRs)",
+  "rfcs": "Requests for Comments (RFCs)",
+  "stories": "User Stories"
+}

docs/pages/docs/lang.md

@@ -1,9 +1,5 @@
 # Summary of Quint
 
-| Revision | Date       | Author                                                  |
-|:---------|:-----------|:--------------------------------------------------------|
-| 36       | 26.06.2024 | 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). Although we keep it
 up-to-date, this document originated Quint and precedes it's implementation. It

docs/pages/docs/language-basics.mdx

@@ -0,0 +1,143 @@
+# Language basics
+
+Quint mostly resembles a functional programming language, but it has a few key differences that are highlighted on this page.
+- Prime operator (`'`)
+- Non-determinism (`nondet`)
+- Modes (`pure def`, `pure val`, `def`, `val`, `nondet`, `action`, `temporal`, `run`)
+- No recursion
+
+The high-level reasons for this and any other differences are two:
+- Quint is used to define state machines and properties, not regular executable code
+- Quint uses the same logic as TLA+ and can be translated into SMT-constraints by Apalache, which is a very powerful thing and we have to constrain the language in some ways to enable it.
+
+## Prime operator
+
+Quint uses the prime operator (`'`) to define transitions of the state machine. It can be read as "in the next state", that is, 
+
+```quint
+x'
+```
+
+is "x in the next state" and
+
+```quint
+x' = x + 1
+```
+
+is "x in the next state is equal to x (in the present state) plus one".
+
+Although in theory (and in TLA+) you could apply the prime operator to any expression, in Quint it has to always come in the format `<var>' = <expr>` which is called assignment. This prevents us from writing things that are really hard to grasp and potentially not possible to compute with the available tools.
+
+Quint's tooling is equipped to report several different errors if you use `'` in forbidden ways. It won't let you assign a value to a variable more than once in the same transition, or forget to update a variable in some branches of transitions.
+
+
+### Assignments have no order
+
+This assignments are not done as in an imperative language. They are, in fact, only defining a set of state transitions. Consider the example:
+```quint
+all {
+  x' = 1,
+  y' = x,
+}
+```
+
+This could be read as "x in the next state is equal to 1 and y in the next state is equal to x in the **current** state". Someone used to imperative programming assignments will likely expect `y` to be `1` in the next state, but this is not the case here.
+
+### `init` and `step`
+
+Actions named `init` and `step` are special as they define the **state machine**. Action `init` defines the initial states and `step` defines the transitions (you can use different names and specify the on the CLI, but `init` and `step` are the defaults). We use the prime operator to define them. Remember this example from [Quint basics](./quint-basics):
+
+```quint
+var x: int
+
+action init = x' = 1
+
+action step = x' = x + 1
+```
+
+You can see `init` and `step` as the entrypoint for the model, like the `main` function is the entrypoint for many programming language applications. All other defintions don't matter for the model, unless they are referred to by `init` or `step`.
+
+## Non-determinism
+
+If only a single path was possible in our model, it would be easy to table test it manually and Quint tools wouldn't be necessary. In the reality, most systems involve many possibilities through non-deterministic factors: user's input, random factors, processes that can execute in different orders, failures that may or may not happen, etc. In Quint models, we express all of these possibilities using `any` and `oneOf`.
+
+For example, there's non-determinism when a user get's to decide if they want to deposit or withdraw, so we use `any`:
+```quint
+action step = any {
+  deposit,
+  withdraw,
+}
+```
+
+Also, this user can pick the amount they want to deposit or withdraw, which therefore is also non-deterministic:
+```quint
+action step = {
+  nondet amount = 1.to(100).oneOf()
+  any {
+    deposit(amount),
+    withdraw(amount),
+  }
+}
+```
+
+## Modes
+
+Most of Quint code is just functional programming, but a bit of it involves non-determinism and state machines. In order to avoid mixing those up and increasing complexity, Quint provides different *modes*, which help separate specifications into layers: some of them purely functional, some of them which interact with state variables, etc.
+
+Definitions prefixed with `pure` are just like functional programming functions: given the same input (parameters), they will always return the same output. If the `pure` modifier is not present, they can read state variables which can change over time and, therefore, they may return different outputs given the same inputs.
+
+```quint
+pure val PROCESSES = ["p1", "p2", "p3"]
+
+pure def plus_four(p) = p + 4
+```
+
+Definitions that don't take parameters can be of mode `val` (or `pure val`), while definitions that take parameters need to be `def` (or `pure def`).
+
+```quint
+var x: int
+
+val process_at_x = PROCESSES[x]
+
+def plus_x(p) = p + x
+```
+
+Definitions that use the prime operator (`'`) can only be of mode `action`. Actions are defintions that "modify" the state.
+
+```quint
+action increment = x' = x + 1
+
+action reset = x' = 0
+```
+
+Non-determinisc definitions are special ones: you can use them only inside actions, before some assignment(s), in order to pick a value non-determintically.
+
+```quint
+action increase = {
+  nondet amount = 1.to(5).oneOf()
+  x' = x + amount
+}
+```
+
+What is non-deterministically? In theory, we are defining a bunch of transitions: `0 -> 1`, `0 -> 2`, ..., `0 -> 5`, `1 -> 2`, ... In practice: The random simulator will pick a random one and continue, while the model checkers will branch out all possibilities and examine each one of them.
+
+
+## No recursion
+
+Quint doesn't support recursive operators, mutually recursive operators, nor recursive type definitions. Formal verification and recursion have complicated interactions, and on the context of Quint and the available tools, all recursion that it could, in theory, support, is the type of recursion that can be written using folds (a.k.a. reduces). 
+
+For example, although you **can't** write a recursive factorial like this
+
+```quint
+pure def factorial(n) = n * factorial(n - 1)
+```
+
+You **can** rewrite it using a fold:
+
+```quint
+pure def factorial(n) = 1.to(n).fold(1, (acc, i) => acc * i)
+```
+
+{/* TODO: Write page on how to rewrite recursion into folds and link it here */}
+
+The lack of recursion enables powerful analysis tools, and although it can be a burden sometimes, thinking about recursive algorithms in terms of folds can be a good exercise to find problems and optimization oportunities.

docs/pages/docs/model-based-testing.mdx

@@ -0,0 +1,9 @@
+import { Callout } from 'nextra/components'
+
+# Model-based Testing
+
+<Callout type="warning" emoji="🚧️">
+  This page is under construction.
+</Callout>
+
+For now, refer to Informal System's page on Model-Based Techniques: [mbt.informal.systems](https://mbt.informal.systems/)