[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,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<T>` (no restrictions on `T`)
@@ -268,19 +294,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:
 
-    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_.
 
     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 +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**
+<a name="SupportedExprs"></a>
+    * `x` -- local variables, function arguments, actor fields.
+    * `e2 <op> 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:
+<a name="SupportedSpec"></a>
 
     * `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 <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 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<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));
+      }
+      ```
+
+    * **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<T>()` — 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
 -------------------