motoko-san: support forall and exists

src/prelude/prim.mo

@@ -478,3 +478,13 @@ func regionStoreBlob(r : Region, offset : Nat64, val :  Blob) : () =
 let call_raw = @call_raw;
 
 func performanceCounter(counter : Nat32) : Nat64 = (prim "performanceCounter" : (Nat32) -> Nat64) counter;
+
+// predicates for motoko-san
+
+func forall<T>(f: T -> Bool): Bool {
+  (prim "forall" : <T>(T -> Bool) -> Bool) <T>(f);
+};
+
+func exists<T>(f: T -> Bool): Bool {
+  (prim "exists" : <T>(T -> Bool) -> Bool) <T>(f);
+};

src/viper/common.ml

@@ -4,3 +4,23 @@ exception Unsupported of Source.region * string
 let unsupported at sexp =
   raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp)))
 
+let rec zip_with : f:('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list option =
+  fun ~f xs ys ->
+    match xs, ys with
+    | [], [] -> Some []
+    | x :: xs, y :: ys -> Option.bind (zip_with ~f xs ys) (fun xys -> Option.some @@ f x y :: xys)
+    | _ :: _, [] | [], _ :: _ -> None
+
+let zip_with_exn : f:('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list =
+  fun ~f xs ys ->
+    match zip_with ~f xs ys with
+    | Some xys -> xys
+    | None -> failwith "Expected lists to have the same length. %s"
+
+let zip : 'a list -> 'b list -> ('a * 'b) list option =
+  fun xs ys ->
+    zip_with ~f:(fun x y -> x, y) xs ys
+
+let zip_exn : 'a list -> 'b list -> ('a * 'b) list =
+  fun xs ys ->
+    zip_with_exn ~f:(fun x y -> x, y) xs ys

src/viper/pretty.ml

@@ -88,6 +88,9 @@ and pp_decl ppf decl =
     id.it
     pp_typ typ
 
+and pp_binder ppf (id, typ) =
+    fprintf ppf "@[%s : %a@]" id.it pp_typ typ
+
 and pp_pres ppf exps =
    fprintf ppf "@[<v 0>%a@]" (pp_print_list pp_pre) exps
 
@@ -166,6 +169,8 @@ and pp_exp ppf exp =
     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
+  | ForallE (binders, exp) -> fprintf ppf "@[forall %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
+  | ExistsE (binders, exp) -> fprintf ppf "@[exists %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
   | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at)
 
 and pp_perm ppf perm =

src/viper/syntax.ml

@@ -55,6 +55,8 @@ and exp' =
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
   | FldE of string               (* top-level field name, e.g. to be passed as a macro argument *)
   | CallE of string * exp list   (* macro or func call *)
+  | ForallE of (id * typ) list * exp
+  | ExistsE of (id * typ) list * exp
 
 and perm = (perm', info) Source.annotated_phrase
 
@@ -86,7 +88,7 @@ and stmt' =
   | WhileS of exp * invariants * seqn
   | LabelS of id
   | GotoS of id
-  (* TODO: these are temporary helper terms  that should not appear in the final translation 
+  (* TODO: these are temporary helper terms  that should not appear in the final translation
        we should avoid introducing them in the first place if possible, so they can be removed *)
   | PreconditionS of exp
   | PostconditionS of exp

src/viper/trans.ml

@@ -515,7 +515,7 @@ and stmt ctxt (s : M.exp) : seqn =
   | M.WhileE(e, s1) ->
      let (invs, s1') = extract_loop_invariants s1 in
      let invs' = List.map (fun inv -> exp ctxt inv) invs in
-     let invs'' = invs' @ local_access_preds ctxt in
+     let invs'' = local_access_preds ctxt @ invs' in
      let invs''' = invs'' @ [!!(AndE(!!(CallE("$Perm", [self ctxt s.at])),
                                      !!(CallE("$Inv",  [self ctxt s.at]))))] in
      !!([],
@@ -759,9 +759,36 @@ and exp ctxt e =
      !!(match e.it with
         | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es)
         | _ -> CallE (tag.it, [exp ctxt e]))
+  | M.CallE ({ it = M.DotE (_, { it = "forall" | "exists" as predicate_name; _ }); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) ->
+    let binders = extract_binders pattern in
+    let typs =
+      match M.(note.note_typ) with
+      | T.Func (_, _, _, [ T.Tup args ], _) -> args
+      | T.Func (_, _, _, [ arg ], _) -> [ arg ]
+      | _ -> []
+    in
+    let typed_binders = zip_with_exn binders typs ~f:(fun b t ->
+      let b = id b in
+      b, t)
+    in
+    let ctxt = add_locals ctxt typed_binders in
+    let typed_binders = List.map (fun (b, t) -> (b, tr_typ t)) typed_binders in
+    let e = exp ctxt e in
+    (match predicate_name with
+    | "forall" -> !!(ForallE (typed_binders, e))
+    | "exists" -> !!(ExistsE (typed_binders, e))
+    | _ -> assert false)
   | _ ->
      unsupported e.at (Arrange.exp e)
 
+and extract_binders pattern =
+  match pattern.it with
+  | M.AnnotP ({ it = M.VarP binder; _ }, _) | M.VarP binder ->
+    [ binder ]
+  | M.ParP pattern -> extract_binders pattern 
+  | M.TupP pats -> List.concat_map extract_binders pats
+  | _ -> []
+
 and rets t_opt =
   let (!!) p = !!! Source.no_region p in
   match t_opt with

test/fail/ok/no-timer-canc.tc.ok

@@ -97,6 +97,7 @@ no-timer-canc.mo:3.10-3.21: type error [M0119], object field cancelTimer is not
     error : Text -> Error;
     errorCode : Error -> ErrorCode;
     errorMessage : Error -> Text;
+    exists : <T>(T -> Bool) -> Bool;
     exp : Float -> Float;
     floatAbs : Float -> Float;
     floatCeil : Float -> Float;
@@ -111,6 +112,7 @@ no-timer-canc.mo:3.10-3.21: type error [M0119], object field cancelTimer is not
     floatToInt64 : Float -> Int64;
     floatToText : Float -> Text;
     floatTrunc : Float -> Float;
+    forall : <T>(T -> Bool) -> Bool;
     getCertificate : () -> ?Blob;
     hashBlob : Blob -> Nat32;
     idlHash : Text -> Nat32;

test/fail/ok/no-timer-set.tc.ok

@@ -97,6 +97,7 @@ no-timer-set.mo:3.10-3.18: type error [M0119], object field setTimer is not cont
     error : Text -> Error;
     errorCode : Error -> ErrorCode;
     errorMessage : Error -> Text;
+    exists : <T>(T -> Bool) -> Bool;
     exp : Float -> Float;
     floatAbs : Float -> Float;
     floatCeil : Float -> Float;
@@ -111,6 +112,7 @@ no-timer-set.mo:3.10-3.18: type error [M0119], object field setTimer is not cont
     floatToInt64 : Float -> Int64;
     floatToText : Float -> Text;
     floatTrunc : Float -> Float;
+    forall : <T>(T -> Bool) -> Bool;
     getCertificate : () -> ?Blob;
     hashBlob : Blob -> Nat32;
     idlHash : Text -> Nat32;

test/viper/ok/reverse.tc.ok

@@ -1,3 +1,7 @@
-reverse.mo:22.13-22.23: warning [M0155], operator may trap for inferred type
+reverse.mo:27.13-27.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:16.9-16.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)
+reverse.mo:32.35-32.47: warning [M0155], operator may trap for inferred type
+  Nat
+reverse.mo:32.35-32.51: warning [M0155], operator may trap for inferred type
+  Nat
+reverse.mo:21.9-21.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/ok/reverse.vpr.ok

@@ -60,7 +60,9 @@ method reverseArray$Nat($Self: Ref, a: Array)
     requires $array_acc(a, $int, write)
     ensures $Perm($Self)
     ensures $array_acc(a, $int, write)
-    ensures ($size(a) == $size(old(a)))
+    ensures ($size(a) == old($size(a)))
+    ensures forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a, k)).$int == 
+            old(($loc(a, (($size(a) - 1) - k))).$int)))
     { var b: Array
       var length: Int
       var i: Int
@@ -80,10 +82,17 @@ method reverseArray$Nat($Self: Ref, a: Array)
       i := (length - 1);
       j := 0;
       while ((i > j))
-         invariant ((i < length) && (i >= 0))
-         invariant ((j < length) && (j >= 0))
          invariant $array_acc(b, $int, wildcard)
          invariant $array_acc(a, $int, write)
+         invariant ((i < length) && (i >= 0))
+         invariant ((j < length) && (j >= 0))
+         invariant (i == (($size(a) - 1) - j))
+         invariant forall k : Int :: (((j <= k) && (k <= i)) ==> (($loc(a, k)).$int == 
+                   old(($loc(a, k)).$int)))
+         invariant forall k : Int :: (((0 <= k) && (k < j)) ==> (($loc(a, k)).$int == 
+                   old(($loc(a, (($size(a) - 1) - k))).$int)))
+         invariant forall k : Int :: (((i < k) && (k < $size(a))) ==> (
+                   ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int)))
          invariant ($Perm($Self) && $Inv($Self))
          { var tmp: Int
            tmp := ($loc(a, i)).$int;

test/viper/ok/reverse.vpr.stderr.ok

@@ -1,3 +1,7 @@
-reverse.mo:22.13-22.23: warning [M0155], operator may trap for inferred type
+reverse.mo:27.13-27.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:16.9-16.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)
+reverse.mo:32.35-32.47: warning [M0155], operator may trap for inferred type
+  Nat
+reverse.mo:32.35-32.51: warning [M0155], operator may trap for inferred type
+  Nat
+reverse.mo:21.9-21.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/reverse.mo

@@ -1,3 +1,6 @@
+import Prim "mo:⛔";
+
+// @verify
 actor Reverse {
   var xarray : [var Nat] = [var 1, 2, 3, 4, 5];
 
@@ -12,7 +15,9 @@ actor Reverse {
   };
 
   private func reverseArray<T>(a : [var T]) : () {
-    assert:return a.size() == (old a).size();
+    assert:return a.size() == (old (a.size()));
+    assert:return Prim.forall<Nat>(
+      func (k : Nat) = (0 <= k and k < a.size()) implies a[k] == (old (a[a.size() - 1 - k])));
     let b = [1, 2, 4]; // space variable to test loop invariant deducing
     var length = a.size();
     if (length == 0) {
@@ -24,6 +29,13 @@ actor Reverse {
     while (i > j) {
       assert:loop:invariant (i < length and i >= 0);
       assert:loop:invariant (j < length and j >= 0);
+      assert:loop:invariant (i == a.size() - 1 - j);
+      assert:loop:invariant Prim.forall<Nat>(
+        func (k : Nat) = (j <= k and k <= i) implies a[k] == (old (a[k])));
+      assert:loop:invariant Prim.forall<Nat>(
+        func (k : Nat) = (0 <= k and k < j) implies a[k] == (old (a[a.size() - 1 - k])));
+      assert:loop:invariant Prim.forall<Nat>(
+        func (k : Nat) = (i < k and k < a.size()) implies a[k] == (old (a[a.size() - 1 - k])));
       var tmp = a[i];
       a[i] := a[j];
       a[j] := tmp;
@@ -32,7 +44,7 @@ actor Reverse {
     };
     return;
   };
-  
+
   public func reverse() : async () {
     var a = copy_xarray();
     reverseArray(a);