motoko-san: add Prim.Ret primitive that acts like var:return

serokell · Jun 27, 2024 · 7d4e700 · 7d4e700
1 parent 17692ec
commit 7d4e700
Show file tree

Hide file tree

Showing 8 changed files with 27 additions and 17 deletions.
diff --git a/src/prelude/prim.mo b/src/prelude/prim.mo
@@ -488,3 +488,7 @@ func forall<T>(f: T -> Bool): Bool {
 func exists<T>(f: T -> Bool): Bool {
   (prim "exists" : <T>(T -> Bool) -> Bool) <T>(f);
 };
+
+func Ret<T>(): T {
+  (prim "viperRet" : <T>() -> T) ();
+};
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -984,6 +984,8 @@ and exp ctxt e =
     | "forall" -> !!(ForallE (typed_binders, e))
     | "exists" -> !!(ExistsE (typed_binders, e))
     | _ -> assert false)
+  | M.CallE ({ it = M.DotE ({it=M.VarE(m);_}, {it="Ret";_}); _ }, _, _)
+    when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim) -> !!(FldE "$Res")
   | _ ->
      unsupported e.at (Arrange.exp e)
 

diff --git a/test/fail/ok/no-timer-canc.tc.ok b/test/fail/ok/no-timer-canc.tc.ok
@@ -12,6 +12,7 @@ no-timer-canc.mo:3.10-3.21: type error [M0119], object field cancelTimer is not
       };
     Array_init : <T>(Nat, T) -> [var T];
     Array_tabulate : <T>(Nat, Nat -> T) -> [T];
+    Ret : <T>() -> T;
     Types :
       module {
         type Any = Any;

diff --git a/test/fail/ok/no-timer-set.tc.ok b/test/fail/ok/no-timer-set.tc.ok
@@ -12,6 +12,7 @@ no-timer-set.mo:3.10-3.18: type error [M0119], object field setTimer is not cont
       };
     Array_init : <T>(Nat, T) -> [var T];
     Array_tabulate : <T>(Nat, Nat -> T) -> [T];
+    Ret : <T>() -> T;
     Types :
       module {
         type Any = Any;

diff --git a/test/viper/ok/todo_record.vpr.ok b/test/viper/ok/todo_record.vpr.ok
@@ -128,7 +128,10 @@ method getTodo($Self: Ref, id: Int)
     ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> (
             ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
     ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (
-             (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> true)
+             (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> 
+      (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc(
+                                                                    ($Self).todos,
+                                                                    i)).$c_ToDo) == $Res))))
     ensures $Inv($Self)
     { var i: Int
       var res: Option[ToDo]

diff --git a/test/viper/ok/todo_tuple.vpr.ok b/test/viper/ok/todo_tuple.vpr.ok
@@ -139,7 +139,10 @@ method getTodo($Self: Ref, id: Int)
                                                                     ($Self).todos,
                                                                     i)).$tuple3$int$int$c_State))))
     ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (
-             (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))) ==> true)
+             (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))) ==> 
+      (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc(
+                                                                    ($Self).todos,
+                                                                    i)).$tuple3$int$int$c_State) == $Res))))
     ensures $Inv($Self)
     { var i: Int
       var res: Option[Tuple$3[Int, Int, State]]

diff --git a/test/viper/todo_record.mo b/test/viper/todo_record.mo
@@ -52,10 +52,9 @@ actor Assistant {
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
-    // BUG: var:return here have type State
-    // assert:return Prim.forall<Nat>(func i {
-    //   0 <= i and i < (old(todos.size())) implies todos[i] == (var:return)[i])});
     // TODO: is not supported yet, do it manually (as in reverse.mo)
+    // assert:return Prim.forall<Nat>(func i =
+    //   (0 <= i and i < (old(todos.size())) implies todos[i] == Prim.Ret<[ToDo]>()[i]));
     // let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]);
     let new_array : [ToDo] = [ { id = 0; desc = ""; completed = #TODO } ];
     return new_array;
@@ -68,8 +67,7 @@ actor Assistant {
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
     assert:return (Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i].id == id))
                    implies
-                   // BUG: problem with type of the (var:return)
-                   true); // Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i] == (var:return))));
+                   Prim.exists<Nat>(func i = (0 <= i and i < num and ?todos[i] == Prim.Ret<?ToDo>())));
     var i : Nat = 0;
     var res : ?ToDo = null;
     label l while (i < num) {

diff --git a/test/viper/todo_tuple.mo b/test/viper/todo_tuple.mo
@@ -6,7 +6,7 @@ import Array "mo:base/Array";
 actor Assistant {
   // type ToDo = (Nat, Text, State); // (id, desc, completed)
   public type State = { #TODO; #DONE };
-  
+
   var todos : [var (Nat, Text, State)] = [var ];
   var num : Nat = 0;
   var nextId : Nat = 1;
@@ -16,7 +16,7 @@ actor Assistant {
   private func resize(n: Nat) {
     // Actor's invariant is preserved:
     assert:func 0 <= num and num <= todos.size();
-    assert:return 0 <= num and num <= todos.size(); 
+    assert:return 0 <= num and num <= todos.size();
     // unchanged fields:
     assert:return num == (old(num)) and nextId == (old(nextId));
     // functional specification:
@@ -52,10 +52,9 @@ actor Assistant {
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
-    // BUG: var:return here have type State
-    // assert:return Prim.forall<Nat>(func i {
-    //   0 <= i and i < (old(todos.size())) implies todos[i] == (var:return)[i])});
     // TODO: is not supported yet, do it manually (as in reverse.mo)
+    // assert:return Prim.forall<Nat>(func i =
+    //   (0 <= i and i < (old(todos.size())) implies todos[i] == Prim.Ret<[Nat, Text, State]>()[i]));
     // let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]);
     let new_array : [(Nat, Text, State)] = [(0, "", #TODO)];
     return new_array;
@@ -66,10 +65,9 @@ actor Assistant {
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
-    assert:return (Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i].0 == id)) 
+    assert:return (Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i].0 == id))
                    implies
-                   // BUG: problem with type of the (var:return)
-                   true); // Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i] == (var:return))));
+                   Prim.exists<Nat>(func i = (0 <= i and i < num and ?todos[i] == Prim.Ret<?(Nat, Text, State)>())));
     var i : Nat = 0;
     var res : ?(Nat, Text, State) = null;
     label l while (i < num) {
@@ -126,7 +124,7 @@ actor Assistant {
       assert:loop:invariant todos.size() == (old(todos.size()));
       assert:loop:invariant Prim.forall<Nat>(func ii =
         (i <= ii and ii < todos.size() implies todos[ii] == (old(todos[ii]))));
-      
+
       assert:loop:invariant Prim.forall<Nat>(func ii =
         (0 <= ii and ii < i and todos[ii].0 != id implies todos[ii] == (old(todos[ii]))));
       assert:loop:invariant Prim.forall<Nat>(func ii =
@@ -210,4 +208,4 @@ actor Assistant {
     todos := new_array;
     num := j;
   };
-}
+}