motoko-san: revert var:return syntax

We've introduced a new workaround with `Prim.Ret<T>` primitive. `var:return` syntax became redundant. Let's revert it.
serokell · Jun 27, 2024 · af6e934 · af6e934
1 parent 7d4e700
commit af6e934
Show file tree

Hide file tree

Showing 24 changed files with 75 additions and 80 deletions.
diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml
@@ -228,7 +228,6 @@ and exp' at note = function
   | S.LabelE (l, t, e) -> I.LabelE (l.it, t.Source.note, exp e)
   | S.BreakE (l, e) -> (breakE l.it (exp e)).it
   | S.RetE e -> (retE (exp e)).it
-  | S.ResVarE -> assert false (* var:return syntax only occurs in motoko-san assertions *)
   | S.ThrowE e -> I.PrimE (I.ThrowPrim, [exp e])
   | S.AsyncE (s, tb, e) ->
     I.AsyncE (s, typ_bind tb, exp e,

diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml
@@ -104,7 +104,6 @@ module Make (Cfg : Config) = struct
     | DebugE e            -> "DebugE"  $$ [exp e]
     | BreakE (i, e)       -> "BreakE"  $$ [id i; exp e]
     | RetE e              -> "RetE"    $$ [exp e]
-    | ResVarE             -> Atom "ResVarE"
     | AsyncE (Type.Fut, tb, e) -> "AsyncE"  $$ [typ_bind tb; exp e]
     | AsyncE (Type.Cmp, tb, e) -> "AsyncE*" $$ [typ_bind tb; exp e]
     | AwaitE (Type.Fut, e)     -> "AwaitE"  $$ [exp e]

diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml
@@ -186,7 +186,6 @@ and exp' =
   | LabelE of id * typ * exp                   (* label *)
   | BreakE of id * exp                         (* break *)
   | RetE of exp                                (* return *)
-  | ResVarE                                    (* name of result *)
   | DebugE of exp                              (* debugging *)
   | AsyncE of async_sort * typ_bind * exp      (* future / computation *)
   | AwaitE of async_sort * exp                 (* await *)

diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml
@@ -93,7 +93,6 @@ let rec exp msgs e : f = match e.it with
   (* The rest remaining cases just collect the uses of subexpressions: *)
   | LitE _ | ActorUrlE _
   | PrimE _ | ImportE _ -> M.empty
-  | ResVarE             -> M.empty
   | UnE (_, uo, e)      -> exp msgs e
   | BinE (_, e1, bo, e2)-> exps msgs [e1; e2]
   | RelE (_, e1, ro, e2)-> exps msgs [e1; e2]

diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml
@@ -53,7 +53,6 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
     T.Await
   | PrimE _
   | VarE _
-  | ResVarE
   | LitE _
   | ImportE _
   | FuncE _ ->

diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly
@@ -674,8 +674,6 @@ exp_un(B) :
     { RetE(TupE([]) @? at $sloc) @? at $sloc }
   | RETURN e=exp(ob)
     { RetE(e) @? at $sloc }
-  | VAR COLON RETURN
-    { ResVarE @? at $sloc }
   | ASYNC e=exp_nest
     { AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), e) @? at $sloc }
   | ASYNCSTAR e=exp_nest

diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml
@@ -69,7 +69,6 @@ let rec exp m e = match e.it with
   | LabelE _
   | BreakE _
   | RetE _
-  | ResVarE
   | AsyncE _ (* TBR - Cmp could be static *)
   | AwaitE _
   | LoopE _

diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml
@@ -3,7 +3,7 @@ open Syntax
 open Source
 
 let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
-  | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ | ResVarE -> f exp
+  | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ -> f exp
   | UnE (x, y, exp1) -> f { exp with it = UnE (x, y, over_exp f exp1) }
   | ShowE (x, exp1) -> f { exp with it = ShowE (x, over_exp f exp1) }
   | ToCandidE exps ->  f { exp with it = ToCandidE (List.map (over_exp f) exps) }

diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml
@@ -924,7 +924,7 @@ let rec is_explicit_exp e =
   | TagE _
   | BreakE _ | RetE _ | ThrowE _ ->
     false
-  | VarE _ | ResVarE
+  | VarE _
   | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | OldE _ | ShowE _ | ToCandidE _ | FromCandidE _
   | AssignE _ | IgnoreE _ | AssertE _ | DebugE _
   | WhileE _ | ForE _
@@ -1141,11 +1141,6 @@ and infer_exp'' env exp : T.typ =
     | None ->
       error env id.at "M0057" "unbound variable %s" id.it
     )
-  | ResVarE ->
-    (match env.rets with
-    | Some t -> t
-    | None ->
-      error env exp.at "M0085" "misplaced var:return")
   | LitE lit ->
     T.Prim (infer_lit env lit exp.at)
   | ActorUrlE exp' ->
@@ -2549,7 +2544,7 @@ and infer_dec env dec : T.typ =
   let t =
   match dec.it with
   | ExpD exp -> infer_exp env exp
-  | LetD (pat, exp, None) -> 
+  | LetD (pat, exp, None) ->
     (* For developer convenience, ignore top-level actor and module identifiers in unused detection. *)
     (if env.in_prog && (CompUnit.is_actor_def exp || CompUnit.is_module_def exp) then
       match pat.it with

diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml
@@ -672,7 +672,6 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
     if !Mo_config.Flags.release_mode then k V.unit else interpret_exp env exp1 k
   | RetE exp1 ->
     interpret_exp env exp1 (Option.get env.rets)
-  | ResVarE -> assert false (* var:return syntax only occurs in motoko-san assertions *)
   | ThrowE exp1 ->
     interpret_exp env exp1 (Option.get env.throws)
   | AsyncE (T.Fut, _, exp1) ->

diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -877,7 +877,6 @@ and exp ctxt e =
      | _ ->
         unsupported e.at (Arrange.exp e)
     end
-  | M.ResVarE -> !!(FldE "$Res")
   | M.AnnotE(a, b) ->
     exp ctxt a
   | M.CallE ({it=M.DotE (e1, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_})

diff --git a/src/viper/traversals.ml b/src/viper/traversals.ml
@@ -12,7 +12,7 @@ type visitor =
 
 let rec over_exp (v : visitor) (exp : exp) : exp =
   v.visit_exp (match exp.it with
-  | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ | ResVarE -> exp
+  | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ -> exp
   | UnE (x, y, exp1) -> { exp with it = UnE (x, y, over_exp v exp1) }
   | ShowE (x, exp1) -> { exp with it = ShowE (x, over_exp v exp1) }
   | ToCandidE exps ->  { exp with it = ToCandidE (List.map (over_exp v) exps) }

diff --git a/test/viper/ok/record.tc.ok b/test/viper/ok/record.tc.ok
@@ -1,10 +1,10 @@
-record.mo:7.7-7.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
-record.mo:8.7-8.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
-record.mo:12.7-12.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
-record.mo:14.8-14.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
-record.mo:22.8-22.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
-record.mo:33.8-33.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
-record.mo:44.8-44.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
-record.mo:49.8-49.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
-record.mo:55.13-55.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
-record.mo:61.8-61.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`)
+record.mo:9.7-9.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
+record.mo:10.7-10.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
+record.mo:14.7-14.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
+record.mo:16.8-16.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
+record.mo:24.8-24.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
+record.mo:35.8-35.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
+record.mo:46.8-46.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
+record.mo:51.8-51.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:57.13-57.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
+record.mo:63.8-63.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`)
diff --git a/test/viper/ok/record.vpr.stderr.ok b/test/viper/ok/record.vpr.stderr.ok
@@ -1,10 +1,10 @@
-record.mo:7.7-7.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
-record.mo:8.7-8.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
-record.mo:12.7-12.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
-record.mo:14.8-14.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
-record.mo:22.8-22.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
-record.mo:33.8-33.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
-record.mo:44.8-44.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
-record.mo:49.8-49.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
-record.mo:55.13-55.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
-record.mo:61.8-61.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`)
+record.mo:9.7-9.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
+record.mo:10.7-10.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
+record.mo:14.7-14.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
+record.mo:16.8-16.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
+record.mo:24.8-24.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
+record.mo:35.8-35.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
+record.mo:46.8-46.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
+record.mo:51.8-51.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:57.13-57.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
+record.mo:63.8-63.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`)
diff --git a/test/viper/ok/text.tc.ok b/test/viper/ok/text.tc.ok
@@ -1,8 +1,8 @@
-text.mo:5.8-5.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
-text.mo:13.8-13.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
-text.mo:21.8-21.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
-text.mo:32.8-32.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
-text.mo:37.8-37.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
-text.mo:38.9-38.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
-text.mo:48.8-48.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
-text.mo:53.8-53.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
+text.mo:9.8-9.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
+text.mo:17.8-17.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
+text.mo:25.8-25.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
+text.mo:36.8-36.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
+text.mo:41.8-41.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
+text.mo:42.9-42.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+text.mo:52.8-52.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
+text.mo:57.8-57.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
diff --git a/test/viper/ok/text.vpr.stderr.ok b/test/viper/ok/text.vpr.stderr.ok
@@ -1,8 +1,8 @@
-text.mo:5.8-5.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
-text.mo:13.8-13.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
-text.mo:21.8-21.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
-text.mo:32.8-32.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
-text.mo:37.8-37.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
-text.mo:38.9-38.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
-text.mo:48.8-48.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
-text.mo:53.8-53.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
+text.mo:9.8-9.19: warning [M0194], unused identifier concat_text (delete or rename to wildcard `_` or `_concat_text`)
+text.mo:17.8-17.18: warning [M0194], unused identifier array_text (delete or rename to wildcard `_` or `_array_text`)
+text.mo:25.8-25.18: warning [M0194], unused identifier tuple_text (delete or rename to wildcard `_` or `_tuple_text`)
+text.mo:36.8-36.17: warning [M0194], unused identifier call_text (delete or rename to wildcard `_` or `_call_text`)
+text.mo:41.8-41.20: warning [M0194], unused identifier change_field (delete or rename to wildcard `_` or `_change_field`)
+text.mo:42.9-42.10: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+text.mo:52.8-52.17: warning [M0194], unused identifier pass_text (delete or rename to wildcard `_` or `_pass_text`)
+text.mo:57.8-57.21: warning [M0194], unused identifier match_on_text (delete or rename to wildcard `_` or `_match_on_text`)
diff --git a/test/viper/ok/tuple.tc.ok b/test/viper/ok/tuple.tc.ok
@@ -1,6 +1,6 @@
-tuple.mo:25.18-25.31: warning [M0194], unused identifier getLargeTuple (delete or rename to wildcard `_` or `_getLargeTuple`)
-tuple.mo:42.18-42.27: warning [M0194], unused identifier passTuple (delete or rename to wildcard `_` or `_passTuple`)
-tuple.mo:45.13-45.14: warning [M0194], unused identifier r (delete or rename to wildcard `_` or `_r`)
-tuple.mo:49.13-49.15: warning [M0194], unused identifier r2 (delete or rename to wildcard `_` or `_r2`)
-tuple.mo:52.18-52.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)
-tuple.mo:60.13-60.14: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+tuple.mo:29.18-29.31: warning [M0194], unused identifier getLargeTuple (delete or rename to wildcard `_` or `_getLargeTuple`)
+tuple.mo:46.18-46.27: warning [M0194], unused identifier passTuple (delete or rename to wildcard `_` or `_passTuple`)
+tuple.mo:49.13-49.14: warning [M0194], unused identifier r (delete or rename to wildcard `_` or `_r`)
+tuple.mo:53.13-53.15: warning [M0194], unused identifier r2 (delete or rename to wildcard `_` or `_r2`)
+tuple.mo:56.18-56.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)
+tuple.mo:64.13-64.14: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
diff --git a/test/viper/ok/tuple.vpr.stderr.ok b/test/viper/ok/tuple.vpr.stderr.ok
@@ -1,6 +1,6 @@
-tuple.mo:25.18-25.31: warning [M0194], unused identifier getLargeTuple (delete or rename to wildcard `_` or `_getLargeTuple`)
-tuple.mo:42.18-42.27: warning [M0194], unused identifier passTuple (delete or rename to wildcard `_` or `_passTuple`)
-tuple.mo:45.13-45.14: warning [M0194], unused identifier r (delete or rename to wildcard `_` or `_r`)
-tuple.mo:49.13-49.15: warning [M0194], unused identifier r2 (delete or rename to wildcard `_` or `_r2`)
-tuple.mo:52.18-52.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)
-tuple.mo:60.13-60.14: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
+tuple.mo:29.18-29.31: warning [M0194], unused identifier getLargeTuple (delete or rename to wildcard `_` or `_getLargeTuple`)
+tuple.mo:46.18-46.27: warning [M0194], unused identifier passTuple (delete or rename to wildcard `_` or `_passTuple`)
+tuple.mo:49.13-49.14: warning [M0194], unused identifier r (delete or rename to wildcard `_` or `_r`)
+tuple.mo:53.13-53.15: warning [M0194], unused identifier r2 (delete or rename to wildcard `_` or `_r2`)
+tuple.mo:56.18-56.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)
+tuple.mo:64.13-64.14: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
diff --git a/test/viper/record.mo b/test/viper/record.mo
@@ -1,5 +1,7 @@
 // @verify
 
+import Prim "mo:⛔";
+
 actor Record {
   type R  = { aa: Int; b: Text; };
   type R1 = { aa: Int; b: Text; };
@@ -26,7 +28,7 @@ actor Record {
   };
 
   func get_record(): R {
-    assert:return (var:return) == { aa = 100; b = "aaa" };
+    assert:return Prim.Ret<R>() == { aa = 100; b = "aaa" };
     return { aa = 100; b = "aaa" };
   };
 
@@ -37,7 +39,7 @@ actor Record {
 
   func record_arg(r: R): R {
     assert:func r.aa == 100;
-    assert:return (var:return).aa == 100;
+    assert:return Prim.Ret<R>().aa == 100;
     return { aa = 100; b = "aaa" };
   };
 
@@ -47,7 +49,7 @@ actor Record {
   };
 
   func match_on_record(): Int {
-    assert:return (var:return) == 42;
+    assert:return Prim.Ret<Int>() == 42;
 
     let r = get_record();
     switch r {

diff --git a/test/viper/reverse.mo b/test/viper/reverse.mo
@@ -11,8 +11,8 @@ actor Reverse {
     // actor invariant is preserved:
     assert:func xarray.size() == 5;
     assert:return xarray.size() == 5;
-    
-    assert:return (var:return).size() == xarray.size();
+
+    assert:return Prim.Ret<[var Nat]>().size() == xarray.size();
     let length = xarray.size();
     let t = Array.init<Nat>(length, 0);
     var i = 0;

diff --git a/test/viper/text.mo b/test/viper/text.mo
@@ -1,3 +1,7 @@
+// @verify
+
+import Prim "mo:⛔";
+
 actor Text {
   let fld1 = "42";
   var fld2 = "42";
@@ -25,7 +29,7 @@ actor Text {
   };
 
   func get_text(): Text {
-    assert:return (var:return) == "foo";
+    assert:return Prim.Ret<Text>() == "foo";
     return "foo";
   };
 
@@ -41,7 +45,7 @@ actor Text {
 
   func text_arg(txt: Text): Text {
     assert:func txt == "abc";
-    assert:return (var:return) == "abc" # "42";
+    assert:return Prim.Ret<Text>() == "abc" # "42";
     return txt # "42";
   };
 
@@ -51,7 +55,7 @@ actor Text {
   };
 
   func match_on_text(): Int {
-    assert:return (var:return) == 42;
+    assert:return Prim.Ret<Int>() == 42;
 
     let txt = get_text();
     switch txt {

diff --git a/test/viper/todo_record.mo b/test/viper/todo_record.mo
@@ -93,8 +93,8 @@ actor Assistant {
     assert:return 0 <= num and num <= todos.size(); // actor invariant (rise it earler)
     assert:return num == (old(num)) + 1;
     assert:return nextId == (old(nextId)) + 1;
-    assert:return (var:return) == (old(nextId));
-    assert:return todos[num-1] == ({ id = var:return; desc = description; completed = #TODO });
+    assert:return Prim.Ret<Nat>() == (old(nextId));
+    assert:return todos[num-1] == ({ id = Prim.Ret<Nat>(); desc = description; completed = #TODO });
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i+1 < num implies todos[i] == (old(todos[i]))));
     let id = nextId;

diff --git a/test/viper/todo_tuple.mo b/test/viper/todo_tuple.mo
@@ -93,8 +93,8 @@ actor Assistant {
     assert:return 0 <= num and num <= todos.size(); // actor invariant (rise it earler)
     assert:return num == (old(num)) + 1;
     assert:return nextId == (old(nextId)) + 1;
-    assert:return (var:return) == (old(nextId));
-    assert:return todos[num-1] == (var:return, description, #TODO);
+    assert:return Prim.Ret<Nat>() == (old(nextId));
+    assert:return todos[num-1] == (Prim.Ret<Nat>(), description, #TODO);
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i+1 < num implies todos[i] == (old(todos[i]))));
     let id = nextId;

diff --git a/test/viper/tuple.mo b/test/viper/tuple.mo
@@ -1,3 +1,7 @@
+// @verify
+
+import Prim "mo:⛔";
+
 actor Tuple {
 
     let fld1 = (1, false);
@@ -18,7 +22,7 @@ actor Tuple {
     };
 
     private func getTuple(): (Int, Bool) {
-        assert:return (var:return).0 == 42 and (var:return).1 == false;
+        assert:return Prim.Ret<(Int, Bool)>().0 == 42 and Prim.Ret<(Int, Bool)>().1 == false;
         return (42, false);
     };