Skip to content

Commit

Permalink
motoko-san: Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
@int-index
int-index committed May 28, 2024
1 parent 09f926d commit 9057948
Showing 1 changed file with 208 additions and 24 deletions.
232 changes: 208 additions & 24 deletions src/viper/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ Formal code specifications are written as part of the Motoko source code. These
* specify that the property `exp` is _intended_ to hold when this block execution begins.
* require that the tool actually _checks_ whether this assumption holds (given this actor's entire source code)
* `assert:system (exp : Bool);` — a _static assertion_ that asks the verifier to prove that the property `exp` holds. Useful while designing code-level canister specifications.
* `assert:loop:invariant (exp : Bool);` — a _loop invariant_ specifies that the property `exp` is intended to hold at the start and at the end of each iteration of a loop

Note: the above syntax is provisional. It has been used so far to avoid introducing breaking changes to the Motoko grammar. In the future, _Motoko-san_ may switch to bespoke syntax for code specifications.

Expand Down Expand Up @@ -124,8 +125,9 @@ After modifying the code and recompiling `moc`, don't forget to test the changes
[nix-shell:motoko]$ make -C test/viper
```
Each test case consists of a (formally specified) Motoko source file, say, `$TEST` (e.g., `invariant.mo`) and the expected test results, represented via a triplet of files:
Each test case consists of a (formally specified) Motoko source file, say, `$TEST` (e.g., `invariant.mo`) and the expected test results, represented via a set of files:
* `test/viper/ok/$TEST.vpr.ok` — what the Motoko compiler is expected to generate; this should be a Viper program.
* `test/viper/ok/$TEST.vpr.stderr.ok` — diagnostic messages (warnings) emitted by the Motoko compiler. No file if stderr is empty.
* `test/viper/ok/$TEST.silicon.ok` — verification errors reported by the Viper tool. For example:
```
[0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. ([email protected])
Expand Down Expand Up @@ -161,23 +163,121 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
Extending to actor classes and modules is _simple_.
* **Primitive types** — Only integer and Boolean types are supported (including literals of these types):
* `Bool`: `not`, `or`, `and`, `implies` (short circuiting semantics)
* **Types and operations**
* Type `Bool`
* Literals: `true`, `false`
* Operations: `not`, `or`, `and`, `implies` (short circuiting semantics)
* Type `Int`
* Literals: `0`, `23`, `-5`, etc
* Operations: `+`, `/`, `*`, `-`, `%`
* Type `Nat`
* Supported via translation to `Int` (sound because `Nat` is a
subtype of `Int`)
* Relations on `Bool`, `Int`, `Nat`
* `==`, `!=`, `<`, `>`, `>=`, `<=`
* Array types `[T]` and `[var T]`, where `T` ∈ {`Bool`, `Int`, `Nat`}
* 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()`
* Tuple types `(T₁, T₂)`, `(T₁, T₂, T₃)`, etc, where `T` ∈ {`Bool`, `Int`, `Nat`}
* Construction: `(a, b)`, `(a, b, c)`, etc
* Projections: `x.1`, `x.2`, etc
* Deconstruction by pattern matching:
* `let (a, b) = x`
* `switch x { case (a, b) ... }`
Nested matching is _not_ supported, i.e. subpatterns for tuple
elements `a`, `b`, `c` in `(a, b, c)` must all be variable patterns.
* Option types `Option<T>` (no restrictions on `T`)
* Construction: `null`, `?a`
* Deconstruction by pattern matching:
```motoko
switch x {
case null ...;
case (?a) ...;
}
```
Nested matching is _not_ supported, i.e. the subpattern `a` in `?a`
must be a variable pattern.
* Variant types `{ #A; #B : T₁; #C : (T₂, T₃) }` (with limitations)
* Construction: `#A`, `#B(x)`, `#C(x, y)`
* Deconstruction by pattern matching:
* `Int`: `+`, `/`, `*`, `-`, `%`
```motoko
switch x {
case #A ...;
case #B(x) ...;
case #C(x, y) ...;
}
```
* Relations: `==`, `!=`, `<`, `>`, `>=`, `<=`
Nested matching is _not_ supported, i.e. the subpatterns `x`, `y` in
`#B(x)` and `#C(x, y)` must all be variable patterns.
Supporting `Text`, `Nat`, `Int32`, tuples, record, and variants is _simple_.
* Generic and recursive variants are supported, e.g.
Supporting `Option<T>` types is _trivial_.
```motoko
type List<T> = { #Nil; #Cons : (T, List<T>) }
```
* Limitation 1: Nominal equality. In the Viper translation, equality
of variant types is not _structural_ (as in normal Motoko programs)
but _nominal_.
* One consequence of this is that a variant type may not be used
directly but must be bound to a name:
```motoko
type N = { #A; #B }
```
Instead of using `{ #A; #B }` in type signatures, one must always
refer to this variant by its name `N`.
* Furthermore, given two identical variant declarations, they are
treated as distinct in the translation:
```motoko
type N = { #A; #B }
type M = { #A; #B } // M ≠ N
```
* Motoko's type checker has not been modified to account for
nominal equality of variants, so type inference is not reliable:
if a variant is bound to a variable in `let`, `var`, or `case`, the
bound variable must be explicitly annotated with the named type of
the variant.
* Limitation 2: Tuple components. If the type associated with a
constructor is a tuple, its components must be specified individually.
That is:

```motoko
type N = { #Con: (Int, Bool) }
let x = #Con(10, true) // supported
let p = (10, true)
let x = #Con(p) // not supported
```
Supporting `Text`, `Int32`, tuples, record, and variants is _simple_.
Supporting `async` types is _hard_.
Supporting `Float`, function types, co-inductive, mutually recursive, and sub-typing is _hard_.
Supporting container types and generic types, e.g., arrays (`[var T]`) and `HashMap<K, V>`, is _hard_.
Supporting container types and generic types, e.g. `HashMap<K, V>`, is _hard_.
Supporting other element types in arrays and tuples is _simple_.
* **Declarations**
Expand All @@ -186,42 +286,118 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
* Immutable: `let y = ...`
* Fields may _not_ be initialized via block expressions: `let z = { ... };`
* **Functions** — Only functions of `()` and `async ()` type with no arguments are supported:
* **Functions** — Functions of multiple arguments are supported:
`public shared func claim() : async () = { ... };`
```motoko
// public func, the result is async
public func f(a: Int, b: Bool) : async [Bool] { ... };
`private func reward() : () = { ... };`
// private func, no async
func g(a: Int, b: Bool) : [Bool] { ... };
```
Supporting function arguments and return values is _simple_.
If a function result type is non-`()`, it must be returned using the
`return` statement.
* **Local declarations** — Only local variable declarations with trivial left-hand side are supported:
Polymorphism is supported in private functions only:
`var x = ...;` and `let y = ...;`
```motoko
func firstValue<T, U>(a : T, _b : U) : T { ... };
```
Supporting pattern matching declarations (e.g., `let (a, b) = ...;`) is _simple_.
In the Viper translation, a polymorphic function is treated as a
template: each instantiation of its type parameters creates a new copy
of the function definition, where the parameters have been instantiated
to concrete types. The call sites are modified to use the monomorphised
version. The instantiations are found by traversing the static call
graph within the actor.
* **Local declarations** — Local variables are declared with `var` or `let`:
```motoko
var x = ...;
let y = ...;
```
Furthermore, `let`-declarations may pattern match on a tuple:
```motoko
let (a, b) = ...;
```
* **Statements**
* `()`-typed block statements and sequential composition:
`{ var x = 0 : Int; x := x + 1; }`
```motoko
{
var x = 0 : Int;
x := x + 1;
}
```
Supporting `let y = do { let y = 1 : Int; y + y };` is _simple_.
* Runtime assertions: `assert i <= MAX;`
* Assignments (to local variables and actor fields): `x := x + 1`
* Assignments (to local variables, actor fields, and array elements):
```motoko
x := x + 1; // x is a local variable
fld := fld + 1; // fld is an actor field
a[i] := a[i] + 1; // a is an array
```
* `if-[else]` statements
Supporting pattern-matching is conceptually _simple_.
* `while` loops (loop invariants are not currently supported)
* Return statements `return e;`
Early exit from a function is also supported:
```motoko
if (length == 0) {
return a; // conditional early exit
};
return a; // normal exit
```
* `while` loops and loop invariants
```motoko
while (cond) {
assert:loop:invariant (e1);
assert:loop:invariant (e2);
...
};
```
The loop invariant assertions must precede all other statements in the
loop body.
Supporting `for` loops is _simple_.
Supporting `break` and `continue` is _simple_.
* Method calls `f(a,b,c);`
```motoko
f1(e); // standalone method call
let c1 = f2(e); // method call in let-declaration
var c2 = f3(e); // method call in var-declaration
c2 := f4(e); // method call in assignment
return f5(e); // method call in return statement
```
Limitiation: at the moment, only one method call per statement is allowed. Nested calls `f(g(x), h(y)))` must be rewritten using temporary variables:
```motoko
let a = g(x);
let b = h(y);
f(a, b);
```
* `await async { ... }` — Asynchronous code blocks that are immediately awaited on.
Supporting general `await`s and `async`s is _hard_.
Expand Down Expand Up @@ -262,10 +438,18 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
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
**Loop invariants** — Extension is _simple_.
* `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`.
Expand Down

0 comments on commit 9057948

Please sign in to comment.