Support private functions and old expressions in Motoko-to-Viper tr…

…anslation (#3675)

This PR adds support for translating private Motoko functions into Viper. The translation is mostly analogous to that for public `async` functions. However, a private function does not have to be called from a state that satisfies the canister invariant (i.e., it may be called even in intermediate states), and a private function does not have to preserve the canister invariant (i.e., it may result in an intermediate state).

Additionally, we add `old` expressions to enable useful specs in private actor functions, e.g.:

```motoko
private func reward() : () {
  count += 1;
  assert:return count == old count + 1;
};
```

emacs/motoko-mode.el

@@ -79,6 +79,7 @@
                  "while"
                  "prim"
                  "invariant"
+                 "old"
                  "implies"
                  ))
               ;; Braces introduce blocks; it's nice to make them stand

src/ir_def/construct.ml

@@ -327,6 +327,13 @@ let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 ->
   ifE e1 (trueE ()) e2
 let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 ->
   orE (notE e1) e2
+let oldE : Ir.exp -> Ir.exp = fun e ->
+  { it = (primE (CallPrim [typ e]) [e]).it;
+    at = no_region;
+    note = Note.{ def with
+      typ = typ e;
+    }
+  }
 
 let rec conjE : Ir.exp list -> Ir.exp = function
   | [] -> trueE ()

src/ir_def/construct.mli

@@ -98,6 +98,7 @@ val notE : exp -> exp
 val andE : exp -> exp -> exp
 val orE : exp -> exp -> exp
 val impliesE : exp -> exp -> exp
+val oldE : exp -> exp
 val conjE : exp list -> exp
 
 val declare_idE : id -> typ -> exp -> exp

src/lowering/desugar.ml

@@ -202,6 +202,7 @@ and exp' at note = function
   | S.AndE (e1, e2) -> (andE (exp e1) (exp e2)).it
   | S.OrE (e1, e2) -> (orE (exp e1) (exp e2)).it
   | S.ImpliesE (e1, e2) -> (impliesE (exp e1) (exp e2)).it
+  | S.OldE e -> (oldE (exp e)).it
   | S.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3)
   | S.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs)
   | S.TryE (e1, cs) -> I.TryE (exp e1, cases cs)

src/mo_def/arrange.ml

@@ -93,6 +93,7 @@ module Make (Cfg : Config) = struct
     | AndE (e1, e2)       -> "AndE"    $$ [exp e1; exp e2]
     | OrE (e1, e2)        -> "OrE"     $$ [exp e1; exp e2]
     | ImpliesE (e1, e2)   -> "ImpliesE"$$ [exp e1; exp e2]
+    | OldE e              -> "OldE"    $$ [exp e]
     | IfE (e1, e2, e3)    -> "IfE"     $$ [exp e1; exp e2; exp e3]
     | SwitchE (e, cs)     -> "SwitchE" $$ [exp e] @ List.map case cs
     | WhileE (e1, e2)     -> "WhileE"  $$ [exp e1; exp e2]

src/mo_def/syntax.ml

@@ -176,6 +176,7 @@ and exp' =
   | AndE of exp * exp                          (* conjunction *)
   | OrE of exp * exp                           (* disjunction *)
   | ImpliesE of exp * exp                      (* implication *)
+  | OldE of exp                                (* old-expression *)
   | IfE of exp * exp * exp                     (* conditional *)
   | SwitchE of exp * case list                 (* switch *)
   | WhileE of exp * exp                        (* while-do loop *)

src/mo_frontend/assertions.mly

@@ -27,6 +27,7 @@ let is_verification () =
 (*
 %nonassoc IMPLIES  (* see parser.mly *)
 *)
+%token OLD
 
 %%
 
@@ -45,5 +46,7 @@ let is_verification () =
     { is_verification () &&& AssertE(Postcondition, e) @? at $sloc }
   | ASSERT COLON s=NAT COLON ASYNC e=exp_nest
     { is_verification () &&& AssertE(Concurrency s, e) @? at $sloc }
+  | OLD e=exp_nest
+    { is_verification () &&& OldE e @? at $sloc }
 
 %%

src/mo_frontend/definedness.ml

@@ -114,6 +114,7 @@ let rec exp msgs e : f = match e.it with
   | AndE (e1, e2)       -> exps msgs [e1; e2]
   | OrE (e1, e2)        -> exps msgs [e1; e2]
   | ImpliesE (e1, e2)   -> exps msgs [e1; e2]
+  | OldE e              -> exp msgs e
   | IfE (e1, e2, e3)    -> exps msgs [e1; e2; e3]
   | SwitchE (e, cs)     -> exp msgs e ++ cases msgs cs
   | TryE (e, cs)        -> exp msgs e ++ cases msgs cs

src/mo_frontend/effect.ml

@@ -49,6 +49,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | TagE (_, exp1)
   | DotE (exp1, _)
   | NotE exp1
+  | OldE (exp1)
   | AssertE (_, exp1)
   | LabelE (_, _, exp1)
   | BreakE (_, exp1)

src/mo_frontend/error_reporting.ml

@@ -119,6 +119,7 @@ let terminal2token (type a) (symbol : a terminal) : token =
       | T_ANDASSIGN -> ANDASSIGN
       | T_AND -> AND
       | T_IMPLIES -> IMPLIES
+      | T_OLD -> OLD
       | T_ADDOP -> ADDOP
       | T_ACTOR -> ACTOR
       | T_INVARIANT -> INVARIANT

src/mo_frontend/printers.ml

@@ -134,6 +134,7 @@ let string_of_symbol = function
   | X (T T_ANDASSIGN) -> binassign "&="
   | X (T T_AND) -> "and"
   | X (T T_IMPLIES) -> "implies"
+  | X (T T_OLD) -> "old"
   | X (T T_ADDOP) -> unop "+"
   | X (T T_ACTOR) -> "actor"
   | X (T T_INVARIANT) -> "invariant"

src/mo_frontend/source_lexer.mll

@@ -219,6 +219,7 @@ rule token mode = parse
   | "in" { IN }
   | "invariant" as s { if mode.verification then INVARIANT else ID s }
   | "implies" as s { if mode.verification then IMPLIES else ID s }
+  | "old" as s { if mode.verification then OLD else ID s }
   | "import" { IMPORT }
   | "module" { MODULE }
   | "not" { NOT }

src/mo_frontend/source_token.ml

@@ -58,6 +58,7 @@ type token =
   | AND
   | OR
   | IMPLIES
+  | OLD
   | NOT
   | IMPORT
   | MODULE
@@ -184,6 +185,7 @@ let to_parser_token :
   | AND -> Ok Parser.AND
   | OR -> Ok Parser.OR
   | IMPLIES -> Ok Parser.IMPLIES
+  | OLD -> Ok Parser.OLD
   | NOT -> Ok Parser.NOT
   | IMPORT -> Ok Parser.IMPORT
   | MODULE -> Ok Parser.MODULE
@@ -373,6 +375,7 @@ let string_of_parser_token = function
   | Parser.UNDERSCORE -> "UNDERSCORE"
   | Parser.INVARIANT -> "INVARIANT"
   | Parser.IMPLIES -> "IMPLIES"
+  | Parser.OLD -> "OLD"
 
 let is_lineless_trivia : token -> void trivia option = function
   | SINGLESPACE -> Some (Space 1)

src/mo_frontend/static.ml

@@ -87,6 +87,7 @@ let rec exp m e = match e.it with
   | TryE _
   | BangE _
   | ImpliesE _
+  | OldE _
   -> err m e.at
 
 and dec_fields m dfs = List.iter (fun df -> dec m df.it.dec) dfs

src/mo_frontend/traversals.ml

@@ -39,6 +39,7 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
      f { exp with it = OrE (over_exp f exp1, over_exp f exp2) }
   | ImpliesE (exp1, exp2) ->
      f { exp with it = ImpliesE (over_exp f exp1, over_exp f exp2) }
+  | OldE exp1 -> f { exp with it = OldE (over_exp f exp1) }
   | WhileE (exp1, exp2) ->
      f { exp with it = WhileE (over_exp f exp1, over_exp f exp2) }
   | LoopE (exp1, exp2_opt) ->

src/mo_frontend/typing.ml

@@ -763,7 +763,7 @@ let rec is_explicit_exp e =
   | BreakE _ | RetE _ | ThrowE _ ->
     false
   | VarE _
-  | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | ShowE _ | ToCandidE _ | FromCandidE _
+  | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | OldE _ | ShowE _ | ToCandidE _ | FromCandidE _
   | AssignE _ | IgnoreE _ | AssertE _ | DebugE _
   | WhileE _ | ForE _
   | AnnotE _ | ImportE _ ->
@@ -1318,6 +1318,8 @@ and infer_exp'' env exp : T.typ =
       check_exp_strong env T.bool exp2
     end;
     T.bool
+  | OldE exp1 ->
+    infer_exp_promote env exp1
   | IfE (exp1, exp2, exp3) ->
     if not env.pre then check_exp_strong env T.bool exp1;
     let t2 = infer_exp env exp2 in

src/mo_interpreter/interpret.ml

@@ -580,6 +580,8 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
         k V.(Bool (as_bool v1 <= as_bool v2))
       )
     )
+  | OldE exp1 ->
+    interpret_exp env exp1 (fun v1 -> k v1)
   | IfE (exp1, exp2, exp3) ->
     interpret_exp env exp1 (fun v1 ->
       if V.as_bool v1

src/viper/README.md

@@ -111,7 +111,7 @@ Contributing to _Motoko-san_
 <a name="Running"></a>
 
 ```bash
-[nix-shell:motoko] moc -viper input.mo > output.vpr
+[nix-shell:motoko] moc --viper input.mo > output.vpr
 ```
 
 You may then verify the `output.vpr` file using [Viper](https://viper.ethz.ch/). Soon, there will be an interactive IDE integration for VS Code, s.t. the outputs do not need to be verified by manually invoking Viper.
@@ -185,13 +185,13 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
         * Immutable: `let y = ...`
         * Fields may _not_ be initialized via block expressions: `let z = { ... };`
 
-    * **Public functions** — Only functions of `async ()` type with no arguments are supported:
+    * **Functions** — Only functions of `()` and `async ()` type with no arguments are supported:
 
-        `public func claim() : async () = { ... };`
+        `public shared func claim() : async () = { ... };`
 
-        Supporting function arguments and return values is _simple_.
+        `private func reward() : () = { ... };`
 
-    * **Private functions** — Currently not supported (extension is _simple_).
+        Supporting function arguments and return values is _simple_.
 
     * **Local declarations** — Only local variable declarations with trivial left-hand side are supported:
 
@@ -239,13 +239,34 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
 
     * `assert:func` — Function preconditions
 
-    * `assert:return` — Function postconditions
+    * `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;
+            };
+            ```
 
     * `assert:system` — Compile-time assertions
 
     **Loop invariants** — Extension is _simple_.
 
-    **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`. This feature requires private functions.
+    **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
 -------------------

src/viper/pretty.ml

@@ -11,7 +11,12 @@ let comma ppf () = fprintf ppf ",@ "
 
 let semi ppf () = fprintf ppf ";@ "
 
-let pp_info ppf NoInfo = ()
+let pp_info ppf info =
+  match info with
+  | NoInfo -> ()
+  | ActorInit -> fprintf ppf "@[// translation of actor initializers @]"
+  | PublicFunction x -> fprintf ppf "@[// translation of PUBLIC function %s@]" x
+  | PrivateFunction x -> fprintf ppf "@[// translation of _private_ function %s@]" x
 
 let rec pp_prog ppf p =
   match p.it with
@@ -118,6 +123,8 @@ and pp_exp ppf exp =
        | Implies _ -> "==>" | OrE _ -> "||" | AndE _ -> "&&"
        | _ -> failwith "not a binary operator" in
      fprintf ppf "(%a %s %a)" pp_exp e1 op pp_exp e2
+  | Old e ->
+    fprintf ppf "@[old(%a)@]" pp_exp e
   | PermE p -> pp_perm ppf p
   | AccE (fldacc, perm) -> fprintf ppf "@[acc(%a,%a)@]" pp_fldacc fldacc pp_exp perm
   | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at)
@@ -179,8 +186,27 @@ and pp_stmt' ppf = function
     fprintf ppf "@[<v 2>/*concurrency max %s, cond: s %a*/@]"
       max
       pp_exp exp
-  | MethodCallS (_, _, _)
-  | LabelS (_, _) -> failwith "MethodCallS or LabelS?"
+  | MethodCallS (rs, m, args) ->
+    let () = match rs with
+    | [] -> ()
+    | r :: rs ->
+      let () = fprintf ppf "@[%s@]" r.it in
+      List.iter (fun r ->
+        fprintf ppf ", @[%s@]" r.it
+      ) rs
+    in
+    let () = if rs != [] then
+      fprintf ppf " := "
+    in
+    let () = fprintf ppf "@[%s(@]" m.it in
+    let () = match args with
+    | [] -> ()
+    | arg :: args ->
+      let () = fprintf ppf "@[%a@]" pp_exp arg in
+      fprintf ppf "@[%a@]" (pp_print_list ~pp_sep:comma pp_exp) args
+    in
+    fprintf ppf ")"
+  | LabelS (_, _) -> failwith "LabelS?"
 
 and pp_fldacc ppf fldacc =
   match fldacc with

src/viper/syntax.ml

@@ -1,4 +1,8 @@
-type info = NoInfo
+type info =
+  | NoInfo
+  | ActorInit
+  | PublicFunction of string
+  | PrivateFunction of string
 
 type id = (string, info) Source.annotated_phrase
 
@@ -41,6 +45,7 @@ and exp' =
   | AndE of exp * exp
   | OrE of exp * exp
   | Implies of exp * exp
+  | Old of exp
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
@@ -64,7 +69,7 @@ and tmpl' = (Mo_def.Syntax.exp -> exp) -> exp
 and fldacc = exp * id
 
 and stmt' =
-  | MethodCallS of id * exp list * id list
+  | MethodCallS of id list * id * exp list
   | ExhaleS of exp
   | InhaleS of exp
   | AssertS of exp