Merge branch 'son/clean' into checked-ops

3 files changed, 93 insertions, 92 deletions

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 2469f98c..8e64f43f 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -41,19 +41,19 @@ let betree_store_leaf_node
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
 let betree_fresh_node_id (counter : u64) : result (u64 & u64) =
-  let* counter1 = u64_add counter 1 in Return (counter, counter1)
+  let* counter1 = u64_add counter 1 in Ok (counter, counter1)
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
-  Return { next_node_id = 0 }
+  Ok { next_node_id = 0 }
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
     Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) =
   let* i = u64_add self.next_node_id 1 in
-  Return (self.next_node_id, { next_node_id = i })
+  Ok (self.next_node_id, { next_node_id = i })
 
 (** [betree_main::betree::upsert_update]:
     Source: 'src/betree.rs', lines 234:0-234:70 *)
@@ -62,16 +62,16 @@ let betree_upsert_update
   begin match prev with
   | None ->
     begin match st with
-    | Betree_UpsertFunState_Add v -> Return v
-    | Betree_UpsertFunState_Sub _ -> Return 0
+    | Betree_UpsertFunState_Add v -> Ok v
+    | Betree_UpsertFunState_Sub _ -> Ok 0
     end
   | Some prev1 ->
     begin match st with
     | Betree_UpsertFunState_Add v ->
       let* margin = u64_sub core_u64_max prev1 in
-      if margin >= v then u64_add prev1 v else Return core_u64_max
+      if margin >= v then u64_add prev1 v else Ok core_u64_max
     | Betree_UpsertFunState_Sub v ->
-      if prev1 >= v then u64_sub prev1 v else Return 0
+      if prev1 >= v then u64_sub prev1 v else Ok 0
     end
   end
 
@@ -83,7 +83,7 @@ let rec betree_List_len
   =
   begin match self with
   | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i
-  | Betree_List_Nil -> Return 0
+  | Betree_List_Nil -> Ok 0
   end
 
 (** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
@@ -94,14 +94,14 @@ let rec betree_List_split_at
   (decreases (betree_List_split_at_decreases t self n))
   =
   if n = 0
-  then Return (Betree_List_Nil, self)
+  then Ok (Betree_List_Nil, self)
   else
     begin match self with
     | Betree_List_Cons hd tl ->
       let* i = u64_sub n 1 in
       let* p = betree_List_split_at t tl i in
       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
 
@@ -110,7 +110,7 @@ let rec betree_List_split_at
 let betree_List_push_front
   (t : Type0) (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]:
     Source: 'src/betree.rs', lines 306:4-306:32 *)
@@ -118,7 +118,7 @@ let betree_List_pop_front
   (t : Type0) (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
   begin 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
 
@@ -126,7 +126,7 @@ let betree_List_pop_front
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
-  | Betree_List_Cons hd _ -> Return hd
+  | Betree_List_Cons hd _ -> Ok hd
   | Betree_List_Nil -> Fail Failure
   end
 
@@ -135,8 +135,8 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
 let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
-  | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key)
-  | Betree_List_Nil -> Return false
+  | Betree_List_Cons hd _ -> let (i, _) = hd in Ok (i = key)
+  | Betree_List_Nil -> Ok false
   end
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
@@ -150,12 +150,12 @@ let rec betree_ListPairU64T_partition_at_pivot
   | Betree_List_Cons hd tl ->
     let (i, x) = hd in
     if i >= pivot
-    then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl)
+    then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl)
     else
       let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
       let (ls0, ls1) = p in
-      Return (Betree_List_Cons (i, x) ls0, ls1)
-  | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
+      Ok (Betree_List_Cons (i, x) ls0, ls1)
+  | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil)
   end
 
 (** [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
@@ -176,7 +176,7 @@ let betree_Leaf_split
   let* (st2, _) = betree_store_leaf_node id1 content1 st1 in
   let n = Betree_Node_Leaf { id = id0; size = params.split_size } in
   let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in
-  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
+  Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
     node_id_cnt2))
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
@@ -191,16 +191,16 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Cons x next_msgs ->
     let (i, m) = x in
     if i >= key
-    then Return (Betree_List_Cons (i, m) next_msgs, Return)
+    then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
     else
       let* (l, lookup_first_message_for_key_back) =
         betree_Node_lookup_first_message_for_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_for_key_back ret in
-          Return (Betree_List_Cons (i, m) next_msgs1) in
-      Return (l, back_'a)
-  | 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
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
@@ -214,9 +214,9 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Cons hd tl ->
     let (i, i1) = hd in
     if i = key
-    then Return (Some i1)
-    else if i > key then Return None else betree_Node_lookup_in_bindings key tl
-  | Betree_List_Nil -> Return None
+    then Ok (Some i1)
+    else if i > key then Ok None else betree_Node_lookup_in_bindings key tl
+  | Betree_List_Nil -> Ok None
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
@@ -244,7 +244,7 @@ let rec betree_Node_apply_upserts
     let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Return (st1, (v, msgs1))
+    Ok (st1, (v, msgs1))
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
@@ -256,10 +256,10 @@ let rec betree_Internal_lookup_in_children
   if key < self.pivot
   then
     let* (st1, (o, n)) = betree_Node_lookup self.left key st in
-    Return (st1, (o, { self with left = n }))
+    Ok (st1, (o, { self with left = n }))
   else
     let* (st1, (o, n)) = betree_Node_lookup self.right key st in
-    Return (st1, (o, { self with right = n }))
+    Ok (st1, (o, { self with right = n }))
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
     Source: 'src/betree.rs', lines 709:4-709:58 *)
@@ -282,19 +282,19 @@ and betree_Node_lookup
           betree_Internal_lookup_in_children node key st1 in
         let* _ =
           lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in
-        Return (st2, (o, Betree_Node_Internal node1))
+        Ok (st2, (o, Betree_Node_Internal node1))
       else
         begin match msg with
         | Betree_Message_Insert v ->
           let* _ =
             lookup_first_message_for_key_back (Betree_List_Cons (k,
               Betree_Message_Insert v) l) in
-          Return (st1, (Some v, Betree_Node_Internal node))
+          Ok (st1, (Some v, Betree_Node_Internal node))
         | Betree_Message_Delete ->
           let* _ =
             lookup_first_message_for_key_back (Betree_List_Cons (k,
               Betree_Message_Delete) l) in
-          Return (st1, (None, Betree_Node_Internal node))
+          Ok (st1, (None, Betree_Node_Internal node))
         | Betree_Message_Upsert ufs ->
           let* (st2, (v, node1)) =
             betree_Internal_lookup_in_children node key st1 in
@@ -303,18 +303,18 @@ and betree_Node_lookup
               Betree_Message_Upsert ufs) l) v key st2 in
           let* msgs1 = lookup_first_message_for_key_back pending1 in
           let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in
-          Return (st4, (Some v1, Betree_Node_Internal node1))
+          Ok (st4, (Some v1, Betree_Node_Internal node1))
         end
     | Betree_List_Nil ->
       let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1
         in
       let* _ = lookup_first_message_for_key_back Betree_List_Nil in
-      Return (st2, (o, Betree_Node_Internal node1))
+      Ok (st2, (o, Betree_Node_Internal node1))
     end
   | Betree_Node_Leaf node ->
     let* (st1, bindings) = betree_load_leaf_node node.id st in
     let* o = betree_Node_lookup_in_bindings key bindings in
-    Return (st1, (o, Betree_Node_Leaf node))
+    Ok (st1, (o, Betree_Node_Leaf node))
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
@@ -333,8 +333,8 @@ let rec betree_Node_filter_messages_for_key
         betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
           l) in
       betree_Node_filter_messages_for_key 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
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
@@ -352,13 +352,13 @@ let rec betree_Node_lookup_first_message_after_key
     then
       let* (l, lookup_first_message_after_key_back) =
         betree_Node_lookup_first_message_after_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_after_key_back ret in
-          Return (Betree_List_Cons (k, m) next_msgs1) in
-      Return (l, back_'a)
-    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
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
@@ -434,7 +434,7 @@ let rec betree_Node_apply_messages_to_internal
     let (i, m) = new_msg in
     let* msgs1 = betree_Node_apply_to_internal msgs i m in
     betree_Node_apply_messages_to_internal msgs1 new_msgs_tl
-  | Betree_List_Nil -> Return msgs
+  | Betree_List_Nil -> Ok msgs
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
@@ -449,16 +449,16 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Cons hd tl ->
     let (i, i1) = hd in
     if i >= key
-    then Return (Betree_List_Cons (i, i1) tl, Return)
+    then Ok (Betree_List_Cons (i, i1) tl, Ok)
     else
       let* (l, lookup_mut_in_bindings_back) =
         betree_Node_lookup_mut_in_bindings key tl in
-      let back_'a =
+      let back =
         fun ret ->
           let* tl1 = lookup_mut_in_bindings_back ret in
-          Return (Betree_List_Cons (i, i1) tl1) in
-      Return (l, back_'a)
-  | 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
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
@@ -510,7 +510,7 @@ let rec betree_Node_apply_messages_to_leaf
     let (i, m) = new_msg in
     let* bindings1 = betree_Node_apply_to_leaf bindings i m in
     betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl
-  | Betree_List_Nil -> Return bindings
+  | Betree_List_Nil -> Ok bindings
   end
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
@@ -541,14 +541,14 @@ let rec betree_Internal_flush
         betree_Node_apply_messages self.right params node_id_cnt1 msgs_right
           st1 in
       let (n1, node_id_cnt2) = p2 in
-      Return (st2, (Betree_List_Nil, ({ self with left = n; right = n1 },
+      Ok (st2, (Betree_List_Nil, ({ self with left = n; right = n1 },
         node_id_cnt2)))
-    else Return (st1, (msgs_right, ({ self with left = n }, node_id_cnt1)))
+    else Ok (st1, (msgs_right, ({ self with left = n }, node_id_cnt1)))
   else
     let* (st1, p1) =
       betree_Node_apply_messages self.right params node_id_cnt msgs_right st in
     let (n, node_id_cnt1) = p1 in
-    Return (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
+    Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
     Source: 'src/betree.rs', lines 588:4-593:5 *)
@@ -571,10 +571,10 @@ and betree_Node_apply_messages
         betree_Internal_flush node params node_id_cnt content1 st1 in
       let (node1, node_id_cnt1) = p in
       let* (st3, _) = betree_store_internal_node node1.id content2 st2 in
-      Return (st3, (Betree_Node_Internal node1, node_id_cnt1))
+      Ok (st3, (Betree_Node_Internal node1, node_id_cnt1))
     else
       let* (st2, _) = betree_store_internal_node node.id content1 st1 in
-      Return (st2, (Betree_Node_Internal node, node_id_cnt))
+      Ok (st2, (Betree_Node_Internal node, node_id_cnt))
   | Betree_Node_Leaf node ->
     let* (st1, content) = betree_load_leaf_node node.id st in
     let* content1 = betree_Node_apply_messages_to_leaf content msgs in
@@ -585,10 +585,10 @@ and betree_Node_apply_messages
       let* (st2, (new_node, node_id_cnt1)) =
         betree_Leaf_split node content1 params node_id_cnt st1 in
       let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in
-      Return (st3, (Betree_Node_Internal new_node, node_id_cnt1))
+      Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1))
     else
       let* (st2, _) = betree_store_leaf_node node.id content1 st1 in
-      Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
+      Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply]:
@@ -603,7 +603,7 @@ let betree_Node_apply
     betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
       new_msg) Betree_List_Nil) st in
   let (self1, node_id_cnt1) = p in
-  Return (st1, (self1, node_id_cnt1))
+  Ok (st1, (self1, node_id_cnt1))
 
 (** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
     Source: 'src/betree.rs', lines 849:4-849:60 *)
@@ -614,7 +614,7 @@ let betree_BeTree_new
   let* node_id_cnt = betree_NodeIdCounter_new in
   let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in
   let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in
-  Return (st1,
+  Ok (st1,
     {
       params = { min_flush_size = min_flush_size; split_size = split_size };
       node_id_cnt = node_id_cnt1;
@@ -630,7 +630,7 @@ let betree_BeTree_apply
   let* (st1, p) =
     betree_Node_apply self.root self.params self.node_id_cnt key msg st in
   let (n, nic) = p in
-  Return (st1, { self with node_id_cnt = nic; root = n })
+  Ok (st1, { self with node_id_cnt = nic; root = n })
 
 (** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
     Source: 'src/betree.rs', lines 874:4-874:52 *)
@@ -664,13 +664,13 @@ let betree_BeTree_lookup
   result (state & ((option u64) & betree_BeTree_t))
   =
   let* (st1, (o, n)) = betree_Node_lookup self.root key st in
-  Return (st1, (o, { self with root = n }))
+  Ok (st1, (o, { self with root = n }))
 
 (** [betree_main::main]:
     Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 let main : result unit =
-  Return ()
+  Ok ()
 
 (** Unit test for [betree_main::main] *)
-let _ = assert_norm (main = Return ())
+let _ = assert_norm (main = Ok ())
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index de9b96fd..3aad9390 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -29,7 +29,8 @@ val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index fca80829..acdb09dc 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -23,11 +23,11 @@ type error : Type0 =
 | OutOfFuel
 
 type result (a : Type0) : Type0 =
-| Return : v:a -> result a
+| Ok : v:a -> result a
 | Fail : e:error -> result a
 
 // Monadic return operator
-unfold let return (#a : Type0) (x : a) : result a = Return x
+unfold let return (#a : Type0) (x : a) : result a = Ok x
 
 // Monadic bind operator.
 // Allows to use the notation:
@@ -36,17 +36,17 @@ unfold let return (#a : Type0) (x : a) : result a = Return x
 // ...
 // ```
 unfold let (let*) (#a #b : Type0) (m: result a)
-  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
+  (f: (x:a) -> Pure (result b) (requires (m == Ok x)) (ensures fun _ -> True)) :
   result b =
   match m with
-  | Return x -> f x
+  | Ok x -> f x
   | Fail e   -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail Failure
+let massert (b:bool) : result unit = if b then Ok () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
-let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+let eval_global (#a : Type0) (x : result a{Ok? (normalize_term x)}) : a = Ok?.v x
 
 (*** Misc *)
 type char = FStar.Char.char
@@ -144,7 +144,7 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
+  if scalar_min ty <= x && scalar_max ty >= x then Ok x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
@@ -498,9 +498,9 @@ type core_ops_range_Range (a : Type0) = {
 
 (*** [alloc] *)
 
-let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Ok x
 let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) =
-  Return (x, (fun x -> Return x))
+  Ok (x, (fun x -> Ok x))
 
 // Trait instance
 let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
@@ -528,20 +528,20 @@ let mk_array (a : Type0) (n : usize)
   l
 
 let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
-  if i < length x then Return (index x i)
+  if i < length x then Ok (index x i)
   else Fail Failure
 
 let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) :
   result (array a n) =
-  if i < length x then Return (list_update x i nx)
+  if i < length x then Ok (list_update x i nx)
   else Fail Failure
 
 let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) :
   result (a & (a -> result (array a n))) =
   match array_index_usize a n x i with
   | Fail e -> Fail e
-  | Return v ->
-    Return (v, array_update_usize a n x i)
+  | Ok v ->
+    Ok (v, array_update_usize a n x i)
 
 (*** Slice *)
 type slice (a : Type0) = s:list a{length s <= usize_max}
@@ -549,30 +549,30 @@ type slice (a : Type0) = s:list a{length s <= usize_max}
 let slice_len (a : Type0) (s : slice a) : usize = length s
 
 let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
-  if i < length x then Return (index x i)
+  if i < length x then Ok (index x i)
   else Fail Failure
 
 let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
-  if i < length x then Return (list_update x i nx)
+  if i < length x then Ok (list_update x i nx)
   else Fail Failure
 
 let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) :
   result (a & (a -> result (slice a))) =
   match slice_index_usize a s i with
   | Fail e -> Fail e
-  | Return x ->
-    Return (x, slice_update_usize a s i)
+  | Ok x ->
+    Ok (x, slice_update_usize a s i)
 
 (*** Subslices *)
 
-let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
+let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Ok x
 let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
-  if length s = n then Return s
+  if length s = n then Ok s
   else Fail Failure
 
 let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) :
   result (slice a & (slice a -> result (array a n))) =
-  Return (x, array_from_slice a n x)
+  Ok (x, array_from_slice a n x)
 
 // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
 let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
@@ -598,16 +598,16 @@ let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
 
 // Helper
 let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail Failure
+  if i < length v then Ok (index v i) else Fail Failure
 // Helper
 let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
-  if i < length v then Return (list_update v i x) else Fail Failure
+  if i < length v then Ok (list_update v i x) else Fail Failure
 
 let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) :
   result (a & (a → result (alloc_vec_Vec a))) =
   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
 
 let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
@@ -616,17 +616,17 @@ let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
   (ensures (fun res ->
     match res with
     | Fail e -> e == Failure
-    | Return v' -> length v' = length v + 1)) =
+    | Ok v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
     (**) append_length v [x];
     (**) assert(length (append v [x]) = length v + 1);
-    Return (append v [x])
+    Ok (append v [x])
     end
   else Fail Failure
 
 let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
-  if i < length v then Return (list_update v i x) else Fail Failure
+  if i < length v then Ok (list_update v i x) else Fail Failure
 
 // Trait declaration: [core::slice::index::private_slice_index::Sealed]
 type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
@@ -650,7 +650,7 @@ let core_slice_index_Slice_index
   let* x = inst.get i s in
   match x with
   | None -> Fail Failure
-  | Some x -> Return x
+  | Some x -> Ok x
 
 // [core::slice::index::Range:::get]: forward function
 let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :