Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

2 files changed, 84 insertions, 86 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 9256b149..80518eab 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -49,13 +49,13 @@ Definition betree_store_leaf_node
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
 Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) :=
-  counter1 <- u64_add counter 1%u64; Return (counter, counter1)
+  counter1 <- u64_add counter 1%u64; Ok (counter, counter1)
 .
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
-  Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
+  Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
@@ -63,7 +63,7 @@ Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
 Definition betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) :=
   i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
-  Return (self.(betree_NodeIdCounter_next_node_id),
+  Ok (self.(betree_NodeIdCounter_next_node_id),
     {| betree_NodeIdCounter_next_node_id := i |})
 .
 
@@ -74,16 +74,16 @@ Definition betree_upsert_update
   match prev with
   | None =>
     match st with
-    | Betree_UpsertFunState_Add v => Return v
-    | Betree_UpsertFunState_Sub _ => Return 0%u64
+    | Betree_UpsertFunState_Add v => Ok v
+    | Betree_UpsertFunState_Sub _ => Ok 0%u64
     end
   | Some prev1 =>
     match st with
     | Betree_UpsertFunState_Add v =>
       margin <- u64_sub core_u64_max prev1;
-      if margin s>= v then u64_add prev1 v else Return core_u64_max
+      if margin s>= v then u64_add prev1 v else Ok core_u64_max
     | Betree_UpsertFunState_Sub v =>
-      if prev1 s>= v then u64_sub prev1 v else Return 0%u64
+      if prev1 s>= v then u64_sub prev1 v else Ok 0%u64
     end
   end
 .
@@ -97,7 +97,7 @@ Fixpoint betree_List_len
   | S n1 =>
     match self with
     | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
-    | Betree_List_Nil => Return 0%u64
+    | Betree_List_Nil => Ok 0%u64
     end
   end
 .
@@ -112,14 +112,14 @@ Fixpoint betree_List_split_at
   | O => Fail_ OutOfFuel
   | S n2 =>
     if n1 s= 0%u64
-    then Return (Betree_List_Nil, self)
+    then Ok (Betree_List_Nil, self)
     else
       match self with
       | Betree_List_Cons hd tl =>
         i <- u64_sub n1 1%u64;
         p <- betree_List_split_at T n2 tl i;
         let (ls0, ls1) := p in
-        Return (Betree_List_Cons hd ls0, ls1)
+        Ok (Betree_List_Cons hd ls0, ls1)
       | Betree_List_Nil => Fail_ Failure
       end
   end
@@ -130,7 +130,7 @@ Fixpoint betree_List_split_at
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
   let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
-  Return (Betree_List_Cons x tl)
+  Ok (Betree_List_Cons x tl)
 .
 
 (** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
@@ -139,7 +139,7 @@ Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
   let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
   match ls with
-  | Betree_List_Cons x tl => Return (x, tl)
+  | Betree_List_Cons x tl => Ok (x, tl)
   | Betree_List_Nil => Fail_ Failure
   end
 .
@@ -148,7 +148,7 @@ Definition betree_List_pop_front
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
-  | Betree_List_Cons hd _ => Return hd
+  | Betree_List_Cons hd _ => Ok hd
   | Betree_List_Nil => Fail_ Failure
   end
 .
@@ -158,8 +158,8 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
 Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
-  | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
-  | Betree_List_Nil => Return false
+  | Betree_List_Cons hd _ => let (i, _) := hd in Ok (i s= key)
+  | Betree_List_Nil => Ok false
   end
 .
 
@@ -176,12 +176,12 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
     | Betree_List_Cons hd tl =>
       let (i, t) := hd in
       if i s>= pivot
-      then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
+      then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl)
       else (
         p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
         let (ls0, ls1) := p in
-        Return (Betree_List_Cons (i, t) ls0, ls1))
-    | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
+        Ok (Betree_List_Cons (i, t) ls0, ls1))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
     end
   end
 .
@@ -218,7 +218,7 @@ Definition betree_Leaf_split
       betree_Leaf_id := id1;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+  Ok (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
     node_id_cnt2))
 .
 
@@ -236,16 +236,16 @@ Fixpoint betree_Node_lookup_first_message_for_key
     | Betree_List_Cons x next_msgs =>
       let (i, m) := x in
       if i s>= key
-      then Return (Betree_List_Cons (i, m) next_msgs, Return)
+      then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
       else (
         p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
         let (l, lookup_first_message_for_key_back) := p in
         let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_for_key_back ret;
-            Return (Betree_List_Cons (i, m) next_msgs1) in
-        Return (l, back))
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (i, m) next_msgs1) in
+        Ok (l, back))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -263,12 +263,10 @@ Fixpoint betree_Node_lookup_in_bindings
     | Betree_List_Cons hd tl =>
       let (i, i1) := hd in
       if i s= key
-      then Return (Some i1)
+      then Ok (Some i1)
       else
-        if i s> key
-        then Return None
-        else betree_Node_lookup_in_bindings n1 key tl
-    | Betree_List_Nil => Return None
+        if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+    | Betree_List_Nil => Ok None
     end
   end
 .
@@ -302,7 +300,7 @@ Fixpoint betree_Node_apply_upserts
       msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Return (st1, (v, msgs1)))
+      Ok (st1, (v, msgs1)))
   end
 .
 
@@ -320,13 +318,13 @@ Fixpoint betree_Internal_lookup_in_children
       p <- betree_Node_lookup n1 self.(betree_Internal_left) key st;
       let (st1, p1) := p in
       let (o, n2) := p1 in
-      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) n2 self.(betree_Internal_right))))
     else (
       p <- betree_Node_lookup n1 self.(betree_Internal_right) key st;
       let (st1, p1) := p in
       let (o, n2) := p1 in
-      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) self.(betree_Internal_left) n2)))
   end
 
@@ -354,19 +352,19 @@ with betree_Node_lookup
           let (st2, p4) := p3 in
           let (o, node1) := p4 in
           _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
-          Return (st2, (o, Betree_Node_Internal node1)))
+          Ok (st2, (o, Betree_Node_Internal node1)))
         else
           match msg with
           | Betree_Message_Insert v =>
             _ <-
               lookup_first_message_for_key_back (Betree_List_Cons (k,
                 Betree_Message_Insert v) l);
-            Return (st1, (Some v, Betree_Node_Internal node))
+            Ok (st1, (Some v, Betree_Node_Internal node))
           | Betree_Message_Delete =>
             _ <-
               lookup_first_message_for_key_back (Betree_List_Cons (k,
                 Betree_Message_Delete) l);
-            Return (st1, (None, Betree_Node_Internal node))
+            Ok (st1, (None, Betree_Node_Internal node))
           | Betree_Message_Upsert ufs =>
             p3 <- betree_Internal_lookup_in_children n1 node key st1;
             let (st2, p4) := p3 in
@@ -380,20 +378,20 @@ with betree_Node_lookup
             p7 <-
               betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
             let (st4, _) := p7 in
-            Return (st4, (Some v1, Betree_Node_Internal node1))
+            Ok (st4, (Some v1, Betree_Node_Internal node1))
           end
       | Betree_List_Nil =>
         p2 <- betree_Internal_lookup_in_children n1 node key st1;
         let (st2, p3) := p2 in
         let (o, node1) := p3 in
         _ <- lookup_first_message_for_key_back Betree_List_Nil;
-        Return (st2, (o, Betree_Node_Internal node1))
+        Ok (st2, (o, Betree_Node_Internal node1))
       end
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, bindings) := p in
       o <- betree_Node_lookup_in_bindings n1 key bindings;
-      Return (st1, (o, Betree_Node_Leaf node))
+      Ok (st1, (o, Betree_Node_Leaf node))
     end
   end
 .
@@ -417,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
             m) l);
         let (_, msgs1) := p1 in
         betree_Node_filter_messages_for_key n1 key msgs1)
-      else Return (Betree_List_Cons (k, m) l)
-    | Betree_List_Nil => Return Betree_List_Nil
+      else Ok (Betree_List_Cons (k, m) l)
+    | Betree_List_Nil => Ok Betree_List_Nil
     end
   end
 .
@@ -443,10 +441,10 @@ Fixpoint betree_Node_lookup_first_message_after_key
         let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_after_key_back ret;
-            Return (Betree_List_Cons (k, m) next_msgs1) in
-        Return (l, back))
-      else Return (Betree_List_Cons (k, m) next_msgs, Return)
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (k, m) next_msgs1) in
+        Ok (l, back))
+      else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -527,7 +525,7 @@ Fixpoint betree_Node_apply_messages_to_internal
       let (i, m) := new_msg in
       msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
       betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
-    | Betree_List_Nil => Return msgs
+    | Betree_List_Nil => Ok msgs
     end
   end
 .
@@ -546,16 +544,16 @@ Fixpoint betree_Node_lookup_mut_in_bindings
     | Betree_List_Cons hd tl =>
       let (i, i1) := hd in
       if i s>= key
-      then Return (Betree_List_Cons (i, i1) tl, Return)
+      then Ok (Betree_List_Cons (i, i1) tl, Ok)
       else (
         p <- betree_Node_lookup_mut_in_bindings n1 key tl;
         let (l, lookup_mut_in_bindings_back) := p in
         let back :=
           fun (ret : betree_List_t (u64 * u64)) =>
             tl1 <- lookup_mut_in_bindings_back ret;
-            Return (Betree_List_Cons (i, i1) tl1) in
-        Return (l, back))
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (i, i1) tl1) in
+        Ok (l, back))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -613,7 +611,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
       let (i, m) := new_msg in
       bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
       betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
-    | Betree_List_Nil => Return bindings
+    | Betree_List_Nil => Ok bindings
     end
   end
 .
@@ -650,20 +648,20 @@ Fixpoint betree_Internal_flush
             node_id_cnt1 msgs_right st1;
         let (st2, p4) := p3 in
         let (n3, node_id_cnt2) := p4 in
-        Return (st2, (Betree_List_Nil, (mkbetree_Internal_t
+        Ok (st2, (Betree_List_Nil, (mkbetree_Internal_t
           self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3,
           node_id_cnt2))))
       else
-        Return (st1, (msgs_right, (mkbetree_Internal_t
-          self.(betree_Internal_id) self.(betree_Internal_pivot) n2
-          self.(betree_Internal_right), node_id_cnt1))))
+        Ok (st1, (msgs_right, (mkbetree_Internal_t self.(betree_Internal_id)
+          self.(betree_Internal_pivot) n2 self.(betree_Internal_right),
+          node_id_cnt1))))
     else (
       p1 <-
         betree_Node_apply_messages n1 self.(betree_Internal_right) params
           node_id_cnt msgs_right st;
       let (st1, p2) := p1 in
       let (n2, node_id_cnt1) := p2 in
-      Return (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) self.(betree_Internal_left) n2,
         node_id_cnt1))))
   end
@@ -694,12 +692,12 @@ with betree_Node_apply_messages
         p4 <-
           betree_store_internal_node node1.(betree_Internal_id) content2 st2;
         let (st3, _) := p4 in
-        Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
+        Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)))
       else (
         p1 <-
           betree_store_internal_node node.(betree_Internal_id) content1 st1;
         let (st2, _) := p1 in
-        Return (st2, (Betree_Node_Internal node, node_id_cnt)))
+        Ok (st2, (Betree_Node_Internal node, node_id_cnt)))
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, content) := p in
@@ -713,11 +711,11 @@ with betree_Node_apply_messages
         let (new_node, node_id_cnt1) := p2 in
         p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
         let (st3, _) := p3 in
-        Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
+        Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
       else (
         p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
         let (st2, _) := p1 in
-        Return (st2, (Betree_Node_Leaf
+        Ok (st2, (Betree_Node_Leaf
           {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
           |}, node_id_cnt)))
     end
@@ -737,7 +735,7 @@ Definition betree_Node_apply
       (key, new_msg) Betree_List_Nil) st;
   let (st1, p1) := p in
   let (self1, node_id_cnt1) := p1 in
-  Return (st1, (self1, node_id_cnt1))
+  Ok (st1, (self1, node_id_cnt1))
 .
 
 (** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
@@ -751,7 +749,7 @@ Definition betree_BeTree_new
   let (id, node_id_cnt1) := p in
   p1 <- betree_store_leaf_node id Betree_List_Nil st;
   let (st1, _) := p1 in
-  Return (st1,
+  Ok (st1,
     {|
       betree_BeTree_params :=
         {|
@@ -777,7 +775,7 @@ Definition betree_BeTree_apply
       self.(betree_BeTree_node_id_cnt) key msg st;
   let (st1, p1) := p in
   let (n1, nic) := p1 in
-  Return (st1,
+  Ok (st1,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := nic;
@@ -822,7 +820,7 @@ Definition betree_BeTree_lookup
   p <- betree_Node_lookup n self.(betree_BeTree_root) key st;
   let (st1, p1) := p in
   let (o, n1) := p1 in
-  Return (st1, (o,
+  Ok (st1, (o,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt);
@@ -833,7 +831,7 @@ Definition betree_BeTree_lookup
 (** [betree_main::main]:
     Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 Definition main : result unit :=
-  Return tt.
+  Ok tt.
 
 (** Unit test for [betree_main::main] *)
 Check (main )%return.
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)