From a3585b6ff211e35915acdc43e8e9f1e73c0c17a8 Mon Sep 17 00:00:00 2001 From: Pavel Golovin Date: Sun, 30 Jun 2024 14:57:49 +0200 Subject: [PATCH] [motoko-san] upd README --- src/viper/README.md | 179 +++++++++++++++++++++++++++++++++----------- 1 file changed, 135 insertions(+), 44 deletions(-) diff --git a/src/viper/README.md b/src/viper/README.md index 1f09bb1780b..0d55680eed8 100644 --- a/src/viper/README.md +++ b/src/viper/README.md @@ -26,7 +26,11 @@ _Motoko-san_ is a prototype code-level verifier for Motoko. The project started | [Testing](#Testing) | [File structure](#Struct) -**[Currently supported features](#Subset)** +**[Currently supported features](#Subset) —** + [Types and operations](#SupportedTypes) + | [Declarations](#SupportedDecls) + | [Expressions](#SupportedExprs) + | [Static code specification](#SupportedSpec) **[Further information](#Further)** @@ -147,7 +151,7 @@ The implementation of _Motoko-san_ consists of the following source files: * `src/viper/pretty.ml` — the Viper pretty printer. Used for serializing Viper AST into text. * `src/viper/trans.ml` — the Motoko-to-Viper translation. Implements the logic of _Motoko-san_. * `src/viper/prep.ml` —  the Motoko-to-Motoko pass that prepares the unit for translation. - +* `src/viper/prelude.ml` - the Viper prelude generation. Creates common types and functions. Currently supported language features ------------------------------------- @@ -164,7 +168,7 @@ Below, we summarize the language features that _Motoko-san_ currently supports. Extending to actor classes and modules is _simple_. * **Types and operations** - + * Type `Bool` * Literals: `true`, `false` * Operations: `not`, `or`, `and`, `implies` (short circuiting semantics) @@ -175,15 +179,37 @@ Below, we summarize the language features that _Motoko-san_ currently supports. * Type `Nat` * Supported via translation to `Int` (sound because `Nat` is a - subtype of `Int`) + subtype of `Int` and typechecking precedes verification) + Exploiting positiveness during verification is _simple_. + + * Type `Text` + * Literals: `""`, `"Hello"` + * Operations: `s + "\n"` + + Note: in current translation the verifier does not evaluate text expressions. So only simple symbolic evaluation could be performed. For example: + ```motoko + let x = "Hello"; + let y = ", world!"; + let z = x + y; + assert:system x + y == z; // pass + assert:system x + y == "Hello, world!" // fail + ``` * Relations on `Bool`, `Int`, `Nat` * `==`, `!=`, `<`, `>`, `>=`, `<=` - * Array types `[T]` and `[var T]`, where `T` ∈ {`Bool`, `Int`, `Nat`} + * Array types `[T]` and `[var T]` * Construction: `[]`, `[x]`, `[x, y, z]`, `[var x, y, z]`, etc * Indexing: `a[i]`, can be used on the LHS of an assignment * Operations: `a.size()` + * Functions from `mo:base/Array`: + * `Array.init` + + * **Limitations:** + * `T` cannot be heap-depended value e.g. another array. It requires more complex permissions and has to work around [the receiver injectiveness](https://viper.ethz.ch/tutorial/#receiver-expressions-and-injectivity). + This is _hard_. + * Due to similar reasons array cannot be an inner type e.g. tuple of array. + Difficulty of overcoming this depends on the outer type e.g. for tuples it is _easy_ while to variant probably not so. * Tuple types `(T₁, T₂)`, `(T₁, T₂, T₃)`, etc, where `T` ∈ {`Bool`, `Int`, `Nat`} * Construction: `(a, b)`, `(a, b, c)`, etc @@ -193,7 +219,7 @@ Below, we summarize the language features that _Motoko-san_ currently supports. * `let (a, b) = x` * `switch x { case (a, b) ... }` - Nested matching is _not_ supported, i.e. subpatterns for tuple + Nested matching is _simple_, but it is _not_ supported, i.e. subpatterns for tuple elements `a`, `b`, `c` in `(a, b, c)` must all be variable patterns. * Option types `Option` (no restrictions on `T`) @@ -268,8 +294,20 @@ Below, we summarize the language features that _Motoko-san_ currently supports. let p = (10, true) let x = #Con(p) // not supported ``` + * Record types (immutable) `{ a: T₁; b: T₂}` + * Construction: `let t = {a = x; b = y}` + * Field access: `t.a`, `t.b` + * Pattern matching: - Supporting `Text`, `Int32`, tuples, record, and variants is _simple_. + ```motoko + switch r { + case { a = x; b} + } + ``` + * **Limitations** + * Nominal equality (see variant's limitations) + + Supporting `Int32` is _simple_. Supporting `async` types is _hard_. @@ -277,10 +315,8 @@ Below, we summarize the language features that _Motoko-san_ currently supports. Supporting container types and generic types, e.g. `HashMap`, is _hard_. - Supporting other element types in arrays and tuples is _simple_. - * **Declarations** - + * **Actor fields** * Mutable: `var x = ...` * Immutable: `let y = ...` @@ -350,7 +386,22 @@ Below, we summarize the language features that _Motoko-san_ currently supports. * `if-[else]` statements - Supporting pattern-matching is conceptually _simple_. + * Pattern-matching: `switch(e)` + + ```motoko + switch (x) { + case null { .. }; + case (?a) { + switch(a) { + case 1: { .. }; + case 2: { .. }; + case _: { .. }; + } + }; + }; + ``` + + Nested matching is _not_ supported yet (simplifying Motoko-Motoko pass is missed). * Return statements `return e;` @@ -374,11 +425,28 @@ Below, we summarize the language features that _Motoko-san_ currently supports. ``` The loop invariant assertions must precede all other statements in the - loop body. + loop body. Note that loops are not transparent in the Viper so right after loop execution only loop invariants considered held (even actor's invariant). - Supporting `for` loops is _simple_. + `break` and `continue` is supported. For example: + ```motoko + label l while (cond) { + while (true) { + if (..) break l; + if (..) continue l; + } + } + ``` - Supporting `break` and `continue` is _simple_. + Supporting `for` loops is _simple_. + + * Labeled expressions: + + ```motoko + let x = label exit: Int { + if (..) exit(-1); + ... + }; + ``` * Method calls `f(a,b,c);` @@ -404,7 +472,17 @@ Below, we summarize the language features that _Motoko-san_ currently supports. Supporting async function calls is _simple_. +* **Expressions** + + * `x` -- local variables, function arguments, actor fields. + * `e2 e2` -- binary operations. + * access to elements of an array `a[i]`, tuple `t.0` or record `a.f`. + * method call is _simple_ since could be boiled down to statement via simple Motoko-Motoko pass. + * `if`-expression is _simple_. + * `switch`-expression is _simple_ since boiled down to series of `if`. + * **Static code specifications** — Note that the syntax is provisional: + * `assert:invariant` — Canister-level invariants @@ -417,41 +495,54 @@ Below, we summarize the language features that _Motoko-san_ currently supports. * `assert:func` — Function preconditions * `assert:return` — Function postconditions. - - * These may refer to variables in the _initial_ state of the function call using the syntax `(old )`, for example: - - ```motoko - var x : Int; - private func dec() : () { - x -= 1; - assert:return x < old(x); - }; - ``` - - is equivalent to - - ```motoko - var x : Int; - private func dec() : () { - let old_x = x; - x -= 1; - assert:return x < old_x; - }; - ``` - * To refer to the result value of a function in a postcondition, use the `var:return` syntax: - ```motoko - private func f(): [var Nat] { - assert:return (var:return).size() == xarray.size(); - ... - } - ``` - * `assert:system` — Compile-time assertions * `assert:loop:invariant` — Loop invariants - **Pure functions** — The tool could be easily extended with a keyword, e.g., `@pure`, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., `assert:invariant is_okay()` for some `@pure func is_okay() : Bool`. + **Expressions in assertions** — Note that using the syntax bellow outside of assertions causes undefined behavior. + + * `e1 implies e2` refers to logical implication. + + * `old(e)` — refers to value of the expression `e` in the _initial_ state of the function call. Could be used in postconditions or loop invariants to show changes that are made. For example: + + ```motoko + var x : Int; + private func dec() : () { + x -= 1; + assert:return x < old(x); + }; + ``` + + is equivalent to + + ```motoko + var x : Int; + private func dec() : () { + let old_x = x; + x -= 1; + assert:return x < old_x; + }; + ``` + + * `Prim.Forall(func x ..)` and `Prim.Exists(func x ..)` — refers ∀ and ∃ quantifiers. For example: + + ```motoko + private func fill_array(x: [var Bool], val: Bool): () { + assert:return Prim.Forall(func i = (0 <= i and i < x.size() implies a[i] == val)); + } + ``` + + * **Pure functions** — The tool could be easily extended with a keyword, e.g., `@pure`, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., `assert:invariant is_okay()` for some `@pure func is_okay() : Bool`. + + * `Prim.Ret()` — refers to the result value of a function. It's temporal syntax and requires manually annotate type of the value. Example: + + ```motoko + private func create_array(n: Nat): [var Nat] { + assert:return (Prim.Ret<[var Nat]>).size() == n; + ... + } + ``` Further information -------------------