[motoko-san] upd README

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**
-
+<a name="SupportedTypes"></a>
     * Type `Bool`
         * Literals: `true`, `false`
         * Operations: `not`, `or`, `and`, `implies` (short circuiting semantics)
@@ -175,28 +179,68 @@ 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: `+`
+
+        Note: in current translation the verifier does not evaluate text expressions. So only simple symbolic reductions 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`
+          * `Array.freeze` is _trivial_
+          * `Array.tabulate` is _easy_ in limited forms.
+
+        * **Limitations:**
+          * Arrays should not coincide. For example if you want to pass an array field into a private function it cause an error:
+            ```motoko
+            actor A {
+              var x: [Int];
+              private func foo(y: [Int]): () {
+                // reason of the error is that two arrays refering same memory:
+                // 1. y -- argument
+                // 2. x -- actor field
+              }
+
+              public func bar(): async () {
+                 foo(x); // error
+              }
+            }
+            ```
+            There are workarounds that are _easy_ but the general problem is _hard_.
+          * `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).
+            Overcoming is _hard_ and may require change permission encoding (to set-based model).
+          * Due to similar reasons array cannot be an inner type e.g. tuple of array.
+            Difficulty of overcoming of this depends on the outer type e.g. for tuples it is _easy_ while for variants probably it is not so.
 
-    * Tuple types `(T₁, T₂)`, `(T₁, T₂, T₃)`, etc, where `T` ∈ {`Bool`, `Int`, `Nat`}
+    * Tuple types `(T₁, T₂)`, `(T₁, T₂, T₃)`, etc
         * 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
+          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<T>` (no restrictions on `T`)
+    * Option types `Option<T>`
         * Construction: `null`, `?a`
         * Deconstruction by pattern matching:
 
@@ -268,19 +312,29 @@ 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:
+
+        ```motoko
+        switch r {
+            case { a = x; b}
+        }
+        ```
+      * **Limitations**
+        * Nominal equality (see variant's limitations)
 
-    Supporting `Text`, `Int32`, tuples, record, and variants is _simple_.
+    Supporting `Int32` 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. `HashMap<K, V>`, is _hard_.
 
-    Supporting other element types in arrays and tuples is _simple_.
-
 * **Declarations**
-  
+<a name="SupportedDecls"></a>
     * **Actor fields**
         * Mutable: `var x = ...`
         * Immutable: `let y = ...`
@@ -350,7 +404,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 +443,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. That's why even actor invariant should be repeated for now.
 
-        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 +490,17 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
 
         Supporting async function calls is _simple_.
 
+* **Expressions**
+<a name="SupportedExprs"></a>
+    * `x` — local variables, function arguments, actor fields.
+    * `e2 <op> e2` — binary operations (see [types](#SupportedTypes) for details).
+    * 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:
+<a name="SupportedSpec"></a>
 
     * `assert:invariant` — Canister-level invariants
     
@@ -417,41 +513,53 @@ 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 <exp>)`, 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 verify 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<T>(func x ..)` and `Prim.Exists<T>(func x ..)` — refers ∀ and ∃ quantifiers. For example:
+
+      ```motoko
+      private func fill_array(x: [var Bool], val: Bool): () {
+         assert:return Prim.Forall<Nat>(func i = (0 <= i and i < x.size() implies a[i] == val));
+      }
+      ```
+    * `Prim.Ret<T>()` — refers to the result value of a function. It's temporal syntax and requires to manually annotate type of the value. Example:
+
+      ```motoko
+      private func create_array(n: Nat): [var Nat] {
+         assert:return (Prim.Ret<[var Nat]>).size() == n;
+         ...
+      }
+      ```
+    * **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`.
+
 
 Further information
 -------------------