Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

10 files changed, 265 insertions, 267 deletions

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/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 *)
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index fca80829..acdb09dc 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/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) :
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 7521eecc..0f20125f 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -167,7 +167,7 @@ namespace Fix
     match x1 with
     | div => True
     | fail _ => x2 = x1
-    | ret _ => x2 = x1 -- TODO: generalize
+    | ok _ => x2 = x1 -- TODO: generalize
 
   -- Monotonicity relation over monadic arrows (i.e., Kleisli arrows)
   def karrow_rel (k1 k2 : (x:a) → Result (b x)) : Prop :=
@@ -386,7 +386,7 @@ namespace Fix
       have Hgeq := Hgmono Hffmono
       simp [result_rel] at Hgeq
       cases Heq: g (fix_fuel n k) <;> rename_i y <;> simp_all
-      -- Remains the .ret case
+      -- Remains the .ok case
       -- Use Hdiv to prove that: ∀ n, h y (fix_fuel n f) = div
       -- We do this in two steps: first we prove it for m ≥ n
       have Hhdiv: ∀ m, h y (fix_fuel m k) = .div := by
@@ -507,7 +507,7 @@ namespace FixI
      specific case.
 
      Remark: the index designates the function in the mutually recursive group
-     (it should be a finite type). We make the return type depend on the input
+     (it should be a finite type). We make the output type depend on the input
      type because we group the type parameters in the input type.
    -/
   open Primitives Fix
@@ -943,7 +943,7 @@ namespace Ex1
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k (tl, i - 1)
 
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
@@ -960,7 +960,7 @@ namespace Ex1
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
@@ -981,11 +981,11 @@ namespace Ex2
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else
         do
           let y ← k (tl, i - 1)
-          .ret y
+          .ok y
 
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
     intro k x
@@ -1002,11 +1002,11 @@ namespace Ex2
        match ls with
        | [] => .fail .panic
        | hd :: tl =>
-         if i = 0 then .ret hd
+         if i = 0 then .ok hd
          else
            do
              let y ← list_nth tl (i - 1)
-             .ret y)
+             .ok y)
     := by
     have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
     simp [list_nth]
@@ -1023,9 +1023,9 @@ namespace Ex3
      - inputs: the sum allows to select the function to call in the recursive
        calls (and the functions may not have the same input types)
      - outputs: this case is degenerate because `even` and `odd` have the same
-       return type `Bool`, but generally speaking we need a sum type because
+       output type `Bool`, but generally speaking we need a sum type because
        the functions in the mutually recursive group may have different
-       return types.
+       output types.
    -/
   variable (k : (Int ⊕ Int) → Result (Bool ⊕ Bool))
 
@@ -1034,7 +1034,7 @@ namespace Ex3
     | .inl i =>
       -- Body of `is_even`
       if i = 0
-      then .ret (.inl true) -- We use .inl because this is `is_even`
+      then .ok (.inl true) -- We use .inl because this is `is_even`
       else
         do
           let b ←
@@ -1044,13 +1044,13 @@ namespace Ex3
               let r ← k (.inr (i- 1))
               match r with
               | .inl _ => .fail .panic -- Invalid output
-              | .inr b => .ret b
-          -- Wrap the return value
-          .ret (.inl b)
+              | .inr b => .ok b
+          -- Wrap the output value
+          .ok (.inl b)
     | .inr i =>
       -- Body of `is_odd`
       if i = 0
-      then .ret (.inr false) -- We use .inr because this is `is_odd`
+      then .ok (.inr false) -- We use .inr because this is `is_odd`
       else
         do
           let b ←
@@ -1059,10 +1059,10 @@ namespace Ex3
               -- extract the output value
               let r ← k (.inl (i- 1))
               match r with
-              | .inl b => .ret b
+              | .inl b => .ok b
               | .inr _ => .fail .panic -- Invalid output
-          -- Wrap the return value
-          .ret (.inr b)
+          -- Wrap the output value
+          .ok (.inr b)
 
   theorem is_even_is_odd_body_is_valid:
     ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
@@ -1078,7 +1078,7 @@ namespace Ex3
     do
       let r ← fix is_even_is_odd_body (.inl i)
       match r with
-      | .inl b => .ret b
+      | .inl b => .ok b
       | .inr _ => .fail .panic
 
   def is_odd (i : Int): Result Bool :=
@@ -1086,11 +1086,11 @@ namespace Ex3
       let r ← fix is_even_is_odd_body (.inr i)
       match r with
       | .inl _ => .fail .panic
-      | .inr b => .ret b
+      | .inr b => .ok b
 
   -- The unfolding equation for `is_even` - diverges if `i < 0`
   theorem is_even_eq (i : Int) :
-    is_even i = (if i = 0 then .ret true else is_odd (i - 1))
+    is_even i = (if i = 0 then .ok true else is_odd (i - 1))
     := by
     have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid
     simp [is_even, is_odd]
@@ -1108,7 +1108,7 @@ namespace Ex3
 
   -- The unfolding equation for `is_odd` - diverges if `i < 0`
   theorem is_odd_eq (i : Int) :
-    is_odd i = (if i = 0 then .ret false else is_even (i - 1))
+    is_odd i = (if i = 0 then .ok false else is_even (i - 1))
     := by
     have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid
     simp [is_even, is_odd]
@@ -1134,17 +1134,17 @@ namespace Ex4
   /- The bodies are more natural -/
   def is_even_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool :=
     if i = 0
-      then .ret true
+      then .ok true
     else do
       let b ← k 1 (i - 1)
-      .ret b
+      .ok b
 
   def is_odd_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool :=
     if i = 0
-      then .ret false
+      then .ok false
     else do
       let b ← k 0 (i - 1)
-      .ret b
+      .ok b
 
   @[simp] def bodies :
     Funs (Fin 2) input_ty output_ty
@@ -1177,19 +1177,19 @@ namespace Ex4
 
   theorem is_even_eq (i : Int) : is_even i =
     (if i = 0
-       then .ret true
+       then .ok true
      else do
        let b ← is_odd (i - 1)
-       .ret b) := by
+       .ok b) := by
     simp [is_even, is_odd];
     conv => lhs; rw [body_fix_eq]
 
   theorem is_odd_eq (i : Int) : is_odd i =
     (if i = 0
-       then .ret false
+       then .ok false
      else do
        let b ← is_even (i - 1)
-       .ret b) := by
+       .ok b) := by
     simp [is_even, is_odd];
     conv => lhs; rw [body_fix_eq]
 end Ex4
@@ -1203,12 +1203,12 @@ namespace Ex5
   /- An auxiliary function, which doesn't require the fixed-point -/
   def map (f : a → Result b) (ls : List a) : Result (List b) :=
     match ls with
-    | [] => .ret []
+    | [] => .ok []
     | hd :: tl =>
       do
         let hd ← f hd
         let tl ← map f tl
-        .ret (hd :: tl)
+        .ok (hd :: tl)
 
   /- The validity theorem for `map`, generic in `f` -/
   theorem map_is_valid
@@ -1229,11 +1229,11 @@ namespace Ex5
 
   def id_body (k : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) :=
     match t with
-    | .leaf x => .ret (.leaf x)
+    | .leaf x => .ok (.leaf x)
     | .node tl =>
       do
         let tl ← map k tl
-        .ret (.node tl)
+        .ok (.node tl)
 
   theorem id_body_is_valid :
     ∀ k x, is_valid_p k (λ k => @id_body a k x) := by
@@ -1254,11 +1254,11 @@ namespace Ex5
   theorem id_eq (t : Tree a) :
     (id t =
        match t with
-       | .leaf x => .ret (.leaf x)
+       | .leaf x => .ok (.leaf x)
        | .node tl =>
        do
          let tl ← map id tl
-         .ret (.node tl))
+         .ok (.node tl))
     := by
     have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a)
     simp [id]
@@ -1283,7 +1283,7 @@ namespace Ex6
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k 0 ⟨ a, tl, i - 1 ⟩
 
   @[simp] def bodies :
@@ -1314,7 +1314,7 @@ namespace Ex6
     match ls with
     | [] => is_valid_p_same k (.fail .panic)
     | hd :: tl =>
-      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩)
+      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩)
 
   theorem body_is_valid' : is_valid body :=
     fun k =>
@@ -1330,7 +1330,7 @@ namespace Ex6
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq body_is_valid
@@ -1345,7 +1345,7 @@ namespace Ex6
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     :=
     -- Use the fixed-point equation
@@ -1376,7 +1376,7 @@ namespace Ex7
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k 0 a ⟨ tl, i - 1 ⟩
 
   @[simp] def bodies :
@@ -1407,7 +1407,7 @@ namespace Ex7
     match ls with
     | [] => is_valid_p_same k (.fail .panic)
     | hd :: tl =>
-      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩)
+      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩)
 
   theorem body_is_valid' : is_valid body :=
     fun k =>
@@ -1423,7 +1423,7 @@ namespace Ex7
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq body_is_valid
@@ -1438,7 +1438,7 @@ namespace Ex7
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     :=
     -- Use the fixed-point equation
@@ -1464,12 +1464,12 @@ namespace Ex8
   /- An auxiliary function, which doesn't require the fixed-point -/
   def map {a : Type y} {b : Type z} (f : a → Result b) (ls : List a) : Result (List b) :=
     match ls with
-    | [] => .ret []
+    | [] => .ok []
     | hd :: tl =>
       do
         let hd ← f hd
         let tl ← map f tl
-        .ret (hd :: tl)
+        .ok (hd :: tl)
 
   /- The validity theorems for `map`, generic in `f` -/
 
@@ -1518,11 +1518,11 @@ namespace Ex9
   def id_body.{u} (k : (i:Fin 1) → (t:ty i) →  input_ty i t → Result (output_ty i t))
     (a : Type u) (t : Tree a) : Result (Tree a) :=
     match t with
-    | .leaf x => .ret (.leaf x)
+    | .leaf x => .ok (.leaf x)
     | .node tl =>
       do
         let tl ← map (k 0 a) tl
-        .ret (.node tl)
+        .ok (.node tl)
 
   @[simp] def bodies :
     Funs (Fin 1) ty input_ty output_ty tys :=
@@ -1556,11 +1556,11 @@ namespace Ex9
   theorem id_eq' {a : Type u} (t : Tree a) :
     id t =
       (match t with
-       | .leaf x => .ret (.leaf x)
+       | .leaf x => .ok (.leaf x)
        | .node tl =>
          do
            let tl ← map id tl
-           .ret (.node tl))
+           .ok (.node tl))
     :=
     -- The unfolding equation
     have Heq := is_valid_fix_fixed_eq body_is_valid.{u}
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 71eaba10..5db8ffed 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -35,7 +35,7 @@ def mkProd (x y : Expr) : MetaM Expr :=
 def mkInOutTy (x y z : Expr) : MetaM Expr := do
   mkAppM ``FixII.mk_in_out_ty #[x, y, z]
 
--- Return the `a` in `Return a`
+-- Return the `a` in `Result a`
 def getResultTy (ty : Expr) : MetaM Expr :=
   ty.withApp fun f args => do
   if ¬ f.isConstOf ``Result ∨ args.size ≠ 1 then
@@ -411,7 +411,7 @@ structure TypeInfo where
      For `list_nth`: `λ a => List a × Int`
    -/
   in_ty : Expr
-  /- The output type, without the `Return`. This is a function taking
+  /- The output type, without the `Result`. This is a function taking
      as input a value of type `params_ty`.
 
      For `list_nth`: `λ a => a`
@@ -1479,9 +1479,9 @@ namespace Tests
   divergent def list_nth {a: Type u} (ls : List a) (i : Int) : Result a :=
     match ls with
     | [] => .fail .panic
-    | x :: ls =>
-      if i = 0 then return x
-      else return (← list_nth ls (i - 1))
+    | x :: ls => do
+      if i = 0 then pure x
+      else pure (← list_nth ls (i - 1))
 
   --set_option trace.Diverge false
 
@@ -1490,7 +1490,7 @@ namespace Tests
   example {a: Type} (ls : List a) :
     ∀ (i : Int),
     0 ≤ i → i < ls.length →
-    ∃ x, list_nth ls i = .ret x := by
+    ∃ x, list_nth ls i = .ok x := by
     induction ls
     . intro i hpos h; simp at h; linarith
     . rename_i hd tl ih
@@ -1538,7 +1538,7 @@ namespace Tests
       if i > 10 then return (← foo (i / 10)) + (← bar i) else bar 10
 
     divergent def bar (i : Int) : Result Nat :=
-      if i > 20 then foo (i / 20) else .ret 42
+      if i > 20 then foo (i / 20) else .ok 42
   end
 
   #check foo.unfold
@@ -1557,8 +1557,8 @@ namespace Tests
   divergent def iInBounds {a : Type} (ls : List a) (i : Int) : Result Bool :=
     let i0 := ls.length
     if i < i0
-    then Result.ret True
-    else Result.ret False
+    then Result.ok True
+    else Result.ok False
 
   #check iInBounds.unfold
 
@@ -1566,8 +1566,8 @@ namespace Tests
     {a : Type} (ls : List a) : Result Bool :=
     let ls1 := ls
     match ls1 with
-    | [] => Result.ret False
-    | _ :: _ => Result.ret True
+    | [] => Result.ok False
+    | _ :: _ => Result.ok True
 
   #check isCons.unfold
 
@@ -1584,7 +1584,7 @@ namespace Tests
   divergent def infinite_loop : Result Unit :=
     do
     let _ ← infinite_loop
-    Result.ret ()
+    Result.ok ()
 
   #check infinite_loop.unfold
 
@@ -1604,51 +1604,51 @@ namespace Tests
 
     divergent def id {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map id tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id.unfold
 
     divergent def id1 {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map (fun x => id1 x) tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id1.unfold
 
     divergent def id2 {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map (fun x => do let _ ← id2 x; id2 x) tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id2.unfold
 
     divergent def incr (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
           let tl ← map incr tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     -- We handle this by inlining the let-binding
     divergent def id3 (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
           let f := id3
           let tl ← map f tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id3.unfold
 
@@ -1658,12 +1658,12 @@ namespace Tests
     -- be parameterized by something).
     divergent def id4 (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
-          let f ← .ret id4
+          let f ← .ok id4
           let tl ← map f tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id4.unfold
     -/
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 1f470fe1..15fe1ff9 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -11,8 +11,8 @@ namespace boxed -- alloc.boxed
 
 namespace Box -- alloc.boxed.Box
 
-def deref (T : Type) (x : T) : Result T := ret x
-def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x)
+def deref (T : Type) (x : T) : Result T := ok x
+def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
 
 /-- Trait instance -/
 def coreopsDerefInst (Self : Type) :
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 3bd2aebb..91ca7284 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -49,7 +49,7 @@ abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i
 def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 -- For initialization
 def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
@@ -68,7 +68,7 @@ theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
 @[pspec]
 theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize α n i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -78,12 +78,12 @@ def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x:
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α n i x = ret nv ∧
+  ∃ nv, v.update_usize α n i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -95,12 +95,12 @@ theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Us
 def Array.index_mut_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) :
   Result (α × (α -> Result (Array α n))) := do
   let x ← index_usize α n v i
-  ret (x, update_usize α n v i)
+  ok (x, update_usize α n v i)
 
 @[pspec]
 theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize α n i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize α n i = ok (x, back) ∧
   x = v.val.index i.val ∧
   back = update_usize α n v i := by
   simp only [index_mut_usize, Bind.bind, bind]
@@ -147,7 +147,7 @@ abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : Lis
 def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 /- In the theorems below: we don't always need the `∃ ..`, but we use one
    so that `progress` introduces an opaque variable and an equality. This
@@ -157,7 +157,7 @@ def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
 @[pspec]
 theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize α i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -167,12 +167,12 @@ def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α i x = ret nv ∧
+  ∃ nv, v.update_usize α i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -184,12 +184,12 @@ theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
 def Slice.index_mut_usize (α : Type u) (v: Slice α) (i: Usize) :
   Result (α × (α → Result (Slice α))) := do
   let x ← Slice.index_usize α v i
-  ret (x, Slice.update_usize α v i)
+  ok (x, Slice.update_usize α v i)
 
 @[pspec]
 theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize α i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize α i = ok (x, back) ∧
   x = v.val.index i.val ∧
   back = Slice.update_usize α v i := by
   simp only [index_mut_usize, Bind.bind, bind]
@@ -203,30 +203,30 @@ theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i
    `progress` tactic), meaning `Array.to_slice` should be considered as opaque.
    All what the spec theorem reveals is that the "representative" lists are the same. -/
 def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
-  ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
+  ok ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
 
 @[pspec]
 theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+  ∃ s, to_slice α n v = ok s ∧ v.val = s.val := by simp [to_slice]
 
 def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
   if h: s.val.len = n.val then
-    ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+    ok ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
   else fail panic
 
 @[pspec]
 theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
-  ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+  ∃ na, from_slice α n a ns = ok na ∧ na.val = ns.val
   := by simp [from_slice, *]
 
 def Array.to_slice_mut (α : Type u) (n : Usize) (a : Array α n) :
   Result (Slice α × (Slice α → Result (Array α n))) := do
   let s ← Array.to_slice α n a
-  ret (s, Array.from_slice α n a)
+  ok (s, Array.from_slice α n a)
 
 @[pspec]
 theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s back, to_slice_mut α n v = ret (s, back) ∧
+  ∃ s back, to_slice_mut α n v = ok (s, back) ∧
   v.val = s.val ∧
   back = Array.from_slice α n v
   := by simp [to_slice_mut, to_slice]
@@ -234,7 +234,7 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
 def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
-    ret ⟨ a.val.slice r.start.val r.end_.val,
+    ok ⟨ a.val.slice r.start.val r.end_.val,
           by
             simp [← List.len_eq_length]
             have := a.val.slice_len_le r.start.val r.end_.val
@@ -245,7 +245,7 @@ def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize)
 @[pspec]
 theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
-  ∃ s, subslice α n a r = ret s ∧
+  ∃ s, subslice α n a r = ok s ∧
   s.val = a.val.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
   := by
@@ -269,7 +269,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
       . scalar_tac
     let na := s_beg.append (s.val.append s_end)
     have : na.len = a.val.len := by simp [na, *]
-    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+    ok ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
 
@@ -281,7 +281,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
 @[pspec]
 theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
-  ∃ na, update_subslice α n a r s = ret na ∧
+  ∃ na, update_subslice α n a r s = ok na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
@@ -305,7 +305,7 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a :
 def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
-    ret ⟨ s.val.slice r.start.val r.end_.val,
+    ok ⟨ s.val.slice r.start.val r.end_.val,
           by
             simp [← List.len_eq_length]
             have := s.val.slice_len_le r.start.val r.end_.val
@@ -316,7 +316,7 @@ def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slic
 @[pspec]
 theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
-  ∃ ns, subslice α s r = ret ns ∧
+  ∃ ns, subslice α s r = ok ns ∧
   ns.val = s.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i))
   := by
@@ -343,14 +343,14 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
       . scalar_tac
     let ns := s_beg.append (ss.val.append s_end)
     have : ns.len = s.val.len := by simp [ns, *]
-    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+    ok ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
 
 @[pspec]
 theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
-  ∃ na, update_subslice α a r ss = ret na ∧
+  ∃ na, update_subslice α a r ss = ok na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
@@ -392,7 +392,7 @@ def core.slice.index.Slice.index
   let x ← inst.get i slice
   match x with
   | none => fail panic
-  | some x => ret x
+  | some x => ok x
 
 /- [core::slice::index::Range:::get]: forward function -/
 def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0c64eca1..4c5b2795 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -41,7 +41,7 @@ deriving Repr, BEq
 open Error
 
 inductive Result (α : Type u) where
-  | ret (v: α): Result α
+  | ok (v: α): Result α
   | fail (e: Error): Result α
   | div
 deriving Repr, BEq
@@ -56,31 +56,31 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
 
 /- HELPERS -/
 
-def ret? {α: Type u} (r: Result α): Bool :=
+def ok? {α: Type u} (r: Result α): Bool :=
   match r with
-  | ret _ => true
+  | ok _ => true
   | fail _ | div => false
 
 def div? {α: Type u} (r: Result α): Bool :=
   match r with
   | div => true
-  | ret _ | fail _ => false
+  | ok _ | fail _ => false
 
 def massert (b:Bool) : Result Unit :=
-  if b then ret () else fail assertionFailure
+  if b then ok () else fail assertionFailure
 
 macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
 
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
+def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : α :=
   match x with
   | fail _ | div => by contradiction
-  | ret x => x
+  | ok x => x
 
 /- DO-DSL SUPPORT -/
 
 def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
   match x with
-  | ret v  => f v
+  | ok v  => f v
   | fail v => fail v
   | div => div
 
@@ -88,11 +88,11 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu
 instance : Bind Result where
   bind := bind
 
--- Allows using return x in do-blocks
+-- Allows using pure x in do-blocks
 instance : Pure Result where
-  pure := fun x => ret x
+  pure := fun x => ok x
 
-@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok x) f = f x := by simp [bind]
 @[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
 @[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
 
@@ -103,14 +103,14 @@ instance : Pure Result where
 -- rely on subtype, and a custom let-binding operator, in effect recreating our
 -- own variant of the do-dsl
 
-def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
+def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
   match o with
-  | ret x => ret ⟨x, rfl⟩
+  | ok x => ok ⟨x, rfl⟩
   | fail e => fail e
   | div => div
 
-@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
-  (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+@[simp] theorem bind_tc_ok (x : α) (f : α → Result β) :
+  (do let y ← .ok x; f y) = f x := by simp [Bind.bind, bind]
 
 @[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
   (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 7668bc59..98d695a4 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -350,7 +350,7 @@ def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
     -- ```
     -- then normalization blocks (for instance, some proofs which use reflexivity fail).
     -- However, the version below doesn't block reduction (TODO: investigate):
-    return Scalar.ofIntCore x (Scalar.check_bounds_prop h)
+    ok (Scalar.ofIntCore x (Scalar.check_bounds_prop h))
   else fail integerOverflow
 
 def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
@@ -584,7 +584,7 @@ instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where
 theorem Scalar.add_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x + y.val)
   (hmax : ↑x + ↑y ≤ Scalar.max ty) :
-  (∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y) := by
+  (∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
   -- Applying the unfoldings only on the left
   conv => congr; ext; lhs; unfold HAdd.hAdd instHAddScalarResult; simp [add, tryMk]
   split
@@ -593,7 +593,7 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   (hmax : ↑x + ↑y ≤ Scalar.max ty) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   have hmin : Scalar.min ty ≤ ↑x + ↑y := by
     have hx := x.hmin
     have hy := y.hmin
@@ -602,57 +602,57 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem Isize.add_spec {x y : Isize}
   (hmin : Isize.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ Isize.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I8.add_spec {x y : I8}
   (hmin : I8.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I8.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I16.add_spec {x y : I16}
   (hmin : I16.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I16.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I32.add_spec {x y : I32}
   (hmin : I32.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I32.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I64.add_spec {x y : I64}
   (hmin : I64.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I64.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I128.add_spec {x y : I128}
   (hmin : I128.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I128.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -660,7 +660,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 theorem Scalar.sub_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ Scalar.max ty) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub]
   split
   . simp [pure]
@@ -669,7 +669,7 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
   {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   have : ↑x - ↑y ≤ Scalar.max ty := by
     have hx := x.hmin
     have hxm := x.hmax
@@ -680,64 +680,64 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ Isize.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I8.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I16.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I32.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I64.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I128.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
 theorem Scalar.mul_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ Scalar.max ty) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   conv => congr; ext; lhs; simp [HMul.hMul]
   simp [mul, tryMk]
   split
@@ -747,7 +747,7 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   (hmax : ↑x * ↑y ≤ Scalar.max ty) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   have : Scalar.min ty ≤ ↑x * ↑y := by
     have hx := x.hmin
     have hy := y.hmin
@@ -756,57 +756,57 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ Isize.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I8.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I16.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I32.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I64.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I128.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -815,15 +815,14 @@ theorem Scalar.div_spec {ty} {x y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Scalar.min ty ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
   simp [HDiv.hDiv, div, Div.div]
   simp [tryMk, *]
-  simp [pure]
   rfl
 
 theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
   have hx := x.hmin
   have hy := y.hmin
@@ -839,69 +838,69 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem Isize.div_spec (x : Isize) {y : Isize}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Isize.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ Isize.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I8.div_spec (x : I8) {y : I8}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I8.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I8.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I16.div_spec (x : I16) {y : I16}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I16.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I16.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I32.div_spec (x : I32) {y : I32}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I32.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I32.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I64.div_spec (x : I64) {y : I64}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I64.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I64.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I128.div_spec (x : I128) {y : I128}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I128.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I128.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -910,15 +909,14 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Scalar.min ty ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
   simp [HMod.hMod, rem]
   simp [tryMk, *]
-  simp [pure]
   rfl
 
 theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
   have hx := x.hmin
   have hy := y.hmin
@@ -934,62 +932,62 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   simp [*]
 
 @[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem I8.rem_spec (x : I8) {y : I8}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I8.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I8.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I16.rem_spec (x : I16) {y : I16}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I16.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I16.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I32.rem_spec (x : I32) {y : I32}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I32.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I32.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I64.rem_spec (x : I64) {y : I64}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I64.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I64.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I128.rem_spec (x : I128) {y : I128}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I128.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I128.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 -- ofIntCore
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 2b8425d8..8e2d65a8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -60,34 +60,34 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
       simp [Usize.max] at *
       have hm := Usize.refined_max.property
       cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
-    return ⟨ List.concat v.val x, by simp at *; assumption ⟩
+    ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
   else
     fail maximumSizeExceeded
 
 -- This shouldn't be used
 def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < v.length then
-    .ret ()
+    ok ()
   else
-    .fail arrayOutOfBounds
+    fail arrayOutOfBounds
 
 -- This is actually the backward function
 def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   if i.val < v.length then
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
   else
-    .fail arrayOutOfBounds
+    fail arrayOutOfBounds
 
 @[pspec]
 theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+  ∃ nv, v.insert α i x = ok nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
 def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 /- In the theorems below: we don't always need the `∃ ..`, but we use one
    so that `progress` introduces an opaque variable and an equality. This
@@ -97,7 +97,7 @@ def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
 @[pspec]
 theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -107,12 +107,12 @@ def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize i x = ret nv ∧
+  ∃ nv, v.update_usize i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -124,15 +124,15 @@ theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
 def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) :
   Result (α × (α → Result (Vec α))) :=
   match Vec.index_usize v i with
-  | ret x =>
-    ret (x, Vec.update_usize v i)
+  | ok x =>
+    ok (x, Vec.update_usize v i)
   | fail e => fail e
   | div => div
 
 @[pspec]
 theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize i = ok (x, back) ∧
   x = v.val.index i.val ∧
   -- Backward function
   back = v.update_usize i
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index dc30c441..ea38c630 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -136,7 +136,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     let _ ←
       tryTac
         (simpAt true []
-               [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+               [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
                [hEq.fvarId!] (.targets #[] true))
     -- It may happen that at this point the goal is already solved (though this is rare)
     -- TODO: not sure this is the best way of checking it
@@ -397,33 +397,33 @@ namespace Test
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep _ as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep h with Scalar.add_spec as ⟨ z ⟩
     simp [*, h]
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     -- This spec theorem is suboptimal, but it is good to check that it works
     progress with Scalar.add_spec as ⟨ z, h1 .. ⟩
     simp [*, h1]
  
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress with U32.add_spec as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep _ as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
@@ -431,7 +431,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.update_usize i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ok nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
@@ -443,8 +443,8 @@ namespace Test
       (do
          (do
             let _ ← v.update_usize i x
-            .ret ())
-         .ret ()) = ret nv
+            .ok ())
+         .ok ()) = ok nv
       := by
     progress
     simp [*]
@@ -454,8 +454,8 @@ namespace Test
      not a constant. We also test the case where the function under scrutinee
      is not a constant. -/
   example {x : U32}
-    (f : U32 → Result Unit) (h : ∀ x, f x = .ret ()) :
-    f x = ret () := by
+    (f : U32 → Result Unit) (h : ∀ x, f x = .ok ()) :
+    f x = ok () := by
     progress
 
 end Test