From 35c6b1c3c3dbd1b782cb00206c773021f5c74765 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:32:19 +0200
Subject: Add an option to run Aeneas as a borrow checker

---
 compiler/Config.ml          |  22 ++++--
 compiler/Extract.ml         | 185 +++++++++++++++++++++++---------------------
 compiler/ExtractBase.ml     |  72 ++++++++---------
 compiler/ExtractBuiltin.ml  |  24 +++---
 compiler/ExtractTypes.ml    | 173 ++++++++++++++++++++++-------------------
 compiler/Main.ml            |  97 ++++++++++++++++-------
 compiler/PureMicroPasses.ml |   4 +-
 compiler/PureUtils.ml       |   2 +-
 compiler/SymbolicToPure.ml  |   2 +-
 compiler/Translate.ml       |  37 ++++-----
 10 files changed, 342 insertions(+), 276 deletions(-)

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 0b26e2ef..cb2c86ad 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -26,12 +26,22 @@ let set_backend (b : string) : unit =
          belonging to the proper set *)
       raise (Failure "Unexpected")
 
-(** The backend to which to extract.
+(** If [true], we do not generate code and simply borrow-check the program instead.
+    This allows us to relax some sanity checks which are present in the symbolic
+    execution only to make sure we will be able to generate the pure translation.
+
+    Remark: when checking if we are borrow-checking a program, checking this
+    boolean or checking if [opt_backend] is [None] are equivalent. We need to
+    have different variables for the purpose of implementing the parsing of
+    the CI arguments.
+  *)
+let borrow_check = ref false
 
-    We initialize it with a default value, but it always gets overwritten:
-    we check that the user provides a backend argument.
- *)
-let backend = ref FStar
+(** Get the target backend *)
+let backend () : backend = Option.get !opt_backend
+
+let if_backend (f : unit -> 'a) (default : 'a) : 'a =
+  match !opt_backend with None -> default | Some _ -> f ()
 
 (** {1 Interpreter} *)
 
@@ -361,7 +371,7 @@ let variant_concatenate_type_name = ref true
 let use_tuple_structs = ref true
 
 let backend_has_tuple_projectors () =
-  match !backend with Lean -> true | Coq | FStar | HOL4 -> false
+  match backend () with Lean -> true | Coq | FStar | HOL4 -> false
 
 (** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
     we use better projector syntax? *)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 035ea8fe..eab85054 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -58,7 +58,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
               (* Add the termination measure *)
               let ctx = ctx_add_termination_measure def ctx in
               (* Add the decreases proof for Lean only *)
-              match !Config.backend with
+              match backend () with
               | Coq | FStar -> ctx
               | HOL4 -> craise __FILE__ __LINE__ def.span "Unexpected"
               | Lean -> ctx_add_decreases_proof def ctx
@@ -98,7 +98,7 @@ let extract_adt_g_value (span : Meta.span)
   let extract_as_tuple () =
     (* This is very annoying: in Coq, we can't write [()] for the value of
        type [unit], we have to write [tt]. *)
-    if !backend = Coq && field_values = [] then (
+    if backend () = Coq && field_values = [] then (
       F.pp_print_string fmt "tt";
       ctx)
     else
@@ -108,7 +108,8 @@ let extract_adt_g_value (span : Meta.span)
       *)
       let lb, rb =
         if List.length field_values = 1 then ("", "")
-        else if !backend = Coq && is_single_pat && List.length field_values > 2
+        else if
+          backend () = Coq && is_single_pat && List.length field_values > 2
         then ("'(", ")")
         else ("(", ")")
       in
@@ -150,7 +151,7 @@ let extract_adt_g_value (span : Meta.span)
 
            Otherwise, it is: `let Cons x0 ... xn = ...`
         *)
-        is_single_pat && !Config.backend = Lean
+        is_single_pat && backend () = Lean
       then (
         F.pp_print_string fmt "⟨";
         F.pp_print_space fmt ();
@@ -273,7 +274,7 @@ let rec extract_typed_pattern (span : Meta.span) (ctx : extraction_ctx)
     block (because some of them are monadic) *)
 let lets_require_wrap_in_do (span : Meta.span)
     (lets : (bool * typed_pattern * texpression) list) : bool =
-  match !backend with
+  match backend () with
   | Lean ->
       (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
       List.exists (fun (m, _, _) -> m) lets
@@ -299,7 +300,7 @@ let lets_require_wrap_in_do (span : Meta.span)
  *)
 
 let extract_texpression_errors (fmt : F.formatter) =
-  match !Config.backend with
+  match backend () with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
   | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
@@ -360,7 +361,7 @@ and extract_App (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
               const_name ctx
           in
           let add_brackets (s : string) =
-            if !backend = Coq then "(" ^ s ^ ")" else s
+            if backend () = Coq then "(" ^ s ^ ")" else s
           in
           F.pp_print_string fmt ("." ^ add_brackets name))
   | _ ->
@@ -472,7 +473,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
                 method_name ctx
             in
             let add_brackets (s : string) =
-              if !backend = Coq then "(" ^ s ^ ")" else s
+              if backend () = Coq then "(" ^ s ^ ")" else s
             in
             F.pp_print_string fmt ("." ^ add_brackets fun_name))
           else
@@ -496,7 +497,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
 
       (* Sanity check: HOL4 doesn't support const generics *)
       sanity_check __FILE__ __LINE__
-        (generics.const_generics = [] || !backend <> HOL4)
+        (generics.const_generics = [] || backend () <> HOL4)
         span;
       (* Print the generics.
 
@@ -588,7 +589,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
         let field_name =
           (* Check if we need to extract the type as a tuple *)
           if is_tuple_struct then
-            match !backend with
+            match backend () with
             | FStar | HOL4 | Coq -> FieldId.to_string proj.field_id
             | Lean ->
                 (* Tuples in Lean are syntax sugar for nested products/pairs,
@@ -623,7 +624,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
                      Note that the first "." is added below.
                 *)
                 let field_id = FieldId.to_int proj.field_id in
-                if !Config.use_nested_tuple_projectors then
+                if !use_nested_tuple_projectors then
                   (* Nested projection: "2.2.2..."  *)
                   if field_id = 0 then "1"
                   else
@@ -640,10 +641,10 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
         (* Extract the expression *)
         extract_texpression span ctx fmt true arg;
         (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
-        if !backend <> Lean then F.pp_print_break fmt 0 0;
+        if backend () <> Lean then F.pp_print_break fmt 0 0;
         F.pp_print_string fmt ".";
         (* If in Coq, the field projection has to be parenthesized *)
-        (match !backend with
+        (match backend () with
         | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
         | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
         (* Close the box *)
@@ -665,7 +666,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the lambda - note that there should always be at least one variable *)
   sanity_check __FILE__ __LINE__ (xl <> []) span;
   F.pp_print_string fmt "fun";
-  let with_type = !backend = Coq in
+  let with_type = backend () = Coq in
   let ctx =
     List.fold_left
       (fun ctx x ->
@@ -674,7 +675,7 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       ctx xl
   in
   F.pp_print_space fmt ();
-  if !backend = Lean || !backend = Coq then F.pp_print_string fmt "=>"
+  if backend () = Lean || backend () = Coq then F.pp_print_string fmt "=>"
   else F.pp_print_string fmt "->";
   F.pp_print_space fmt ();
   (* Print the body *)
@@ -709,7 +710,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
      ]}
   *)
   let lets, next_e =
-    match !backend with
+    match backend () with
     | HOL4 -> destruct_lets_no_interleave span e
     | FStar | Coq | Lean -> destruct_lets e
   in
@@ -730,11 +731,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
        * ]}
        * TODO: cleanup
        * *)
-      if monadic && (!backend = Coq || !backend = HOL4) then (
+      if monadic && (backend () = Coq || backend () = HOL4) then (
         let ctx = extract_typed_pattern span ctx fmt true true lv in
         F.pp_print_space fmt ();
         let arrow =
-          match !backend with
+          match backend () with
           | Coq | HOL4 -> "<-"
           | FStar | Lean -> craise __FILE__ __LINE__ span "impossible"
         in
@@ -746,7 +747,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       else (
         (* Print the "let" *)
         if monadic then
-          match !backend with
+          match backend () with
           | FStar ->
               F.pp_print_string fmt "let*";
               F.pp_print_space fmt ()
@@ -760,7 +761,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         let ctx = extract_typed_pattern span ctx fmt true true lv in
         F.pp_print_space fmt ();
         let eq =
-          match !backend with
+          match backend () with
           | FStar -> "="
           | Coq -> ":="
           | Lean -> if monadic then "←" else ":="
@@ -770,7 +771,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         extract_texpression span ctx fmt false re;
         (* End the let-binding *)
-        (match !backend with
+        (match backend () with
         | Lean ->
             (* In Lean, (monadic) let-bindings don't require to end with anything *)
             ()
@@ -791,9 +792,9 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
      at the end of every let-binding: let-bindings are indeed not ended
      with an "in" keyword.
   *)
-  if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+  if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
   (* Open parentheses *)
-  if inside && !backend <> Lean then F.pp_print_string fmt "(";
+  if inside && backend () <> Lean then F.pp_print_string fmt "(";
   (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
      immediately *)
   let wrap_in_do_od = lets_require_wrap_in_do span lets in
@@ -814,11 +815,11 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* do-box (Lean and HOL4 only) *)
   if wrap_in_do_od then
-    if !backend = HOL4 then (
+    if backend () = HOL4 then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "od");
   (* Close parentheses *)
-  if inside && !backend <> Lean then F.pp_print_string fmt ")";
+  if inside && backend () <> Lean then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
   F.pp_close_box fmt ()
 
@@ -832,14 +833,14 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
      In the case of Lean, we rely on indentation to delimit the end of the
      branches, and need to insert line breaks: we thus use a vbox.
   *)
-  if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+  if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
   (* Extract the switch *)
   (match body with
   | If (e_then, e_else) ->
       (* Open a box for the [if e] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       F.pp_print_string fmt "if";
-      if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
+      if backend () = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
       F.pp_print_space fmt ();
       let scrut_inside =
         PureUtils.texpression_requires_parentheses span scrut
@@ -863,7 +864,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         (* Open the parenthesized expression *)
         let print_space_after_parenth =
           if parenth then (
-            match !backend with
+            match backend () with
             | FStar ->
                 F.pp_print_space fmt ();
                 F.pp_print_string fmt "begin";
@@ -885,7 +886,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_close_box fmt ();
         (* Close the parenthesized expression *)
         (if parenth then
-           match !backend with
+           match backend () with
            | FStar ->
                F.pp_print_space fmt ();
                F.pp_print_string fmt "end"
@@ -901,7 +902,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the [match ... with] *)
       let match_begin =
-        match !backend with
+        match backend () with
         | FStar -> "begin match"
         | Coq -> "match"
         | Lean -> if ctx.use_dep_ite then "match h:" else "match"
@@ -917,7 +918,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       extract_texpression span ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
       let match_scrut_end =
-        match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+        match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of"
       in
       F.pp_print_string fmt match_scrut_end;
       (* Close the box for the [match ... with] *)
@@ -936,7 +937,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         let ctx = extract_typed_pattern span ctx fmt false false br.pat in
         F.pp_print_space fmt ();
         let arrow =
-          match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+          match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
         in
         F.pp_print_string fmt arrow;
         (* Close the box for the pattern *)
@@ -955,7 +956,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       List.iter extract_branch branches;
 
       (* End the match *)
-      match !backend with
+      match backend () with
       | Lean -> (*We rely on indentation in Lean *) ()
       | FStar | Coq ->
           F.pp_print_space fmt ();
@@ -969,11 +970,11 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
     unit =
   (* We can't update a subset of the fields in Coq (i.e., we can do
      [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
-  sanity_check __FILE__ __LINE__ (!backend <> Coq || supd.init = None) span;
+  sanity_check __FILE__ __LINE__ (backend () <> Coq || supd.init = None) span;
   (* In the case of HOL4, records with no fields are not supported and are
      thus extracted to unit. We need to check that by looking up the definition *)
   let extract_as_unit =
-    match (!backend, supd.struct_id) with
+    match (backend (), supd.struct_id) with
     | HOL4, TAdtId adt_id ->
         let d = TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls in
         d.kind = Struct []
@@ -1009,14 +1010,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         *)
         (* Outer brackets *)
         let olb, orb =
-          match !backend with
+          match backend () with
           | Lean | FStar -> (Some "{", Some "}")
           | Coq -> (Some "{|", Some "|}")
           | HOL4 -> (None, None)
         in
         (* Inner brackets *)
         let ilb, irb =
-          match !backend with
+          match backend () with
           | Lean | FStar | Coq -> (None, None)
           | HOL4 -> (Some "<|", Some "|>")
         in
@@ -1030,7 +1031,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
           | None -> ()
         in
         print_bracket true olb;
-        let need_paren = inside && !backend = HOL4 in
+        let need_paren = inside && backend () = HOL4 in
         if need_paren then F.pp_print_string fmt "(";
         F.pp_open_hvbox fmt ctx.indent_incr;
         if supd.init <> None then (
@@ -1042,10 +1043,10 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         print_bracket true ilb;
         F.pp_open_hvbox fmt 0;
         let delimiter =
-          match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
         in
         let assign =
-          match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+          match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "="
         in
         Collections.List.iter_link
           (fun () ->
@@ -1093,7 +1094,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         F.pp_close_box fmt ();
         (* Print the values *)
         let delimiter =
-          match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
         in
         F.pp_print_space fmt ();
         F.pp_open_hovbox fmt 0;
@@ -1209,7 +1210,7 @@ let extract_fun_inputs_output_parameters_types (ctx : extraction_ctx)
   extract_ty def.span ctx fmt TypeDeclId.Set.empty false def.signature.output
 
 let assert_backend_supports_decreases_clauses (span : Meta.span) =
-  match !backend with
+  match backend () with
   | FStar | Lean -> ()
   | _ ->
       craise __FILE__ __LINE__ span
@@ -1233,7 +1234,9 @@ let assert_backend_supports_decreases_clauses (span : Meta.span) =
  *)
 let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) : unit =
-  cassert __FILE__ __LINE__ (!backend = FStar) def.span
+  cassert __FILE__ __LINE__
+    (backend () = FStar)
+    def.span
     "The generation of template decrease clauses is only supported for the F* \
      backend";
 
@@ -1245,7 +1248,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
-     if !Config.extract_external_name_patterns && not def.is_local then
+     if !extract_external_name_patterns && not def.is_local then
        Some def.llbc_name
      else None
    in
@@ -1302,7 +1305,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
 *)
 let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) : unit =
-  cassert __FILE__ __LINE__ (!backend = Lean) def.span
+  cassert __FILE__ __LINE__
+    (backend () = Lean)
+    def.span
     "The generation of template termination and decreasing clauses is only \
      supported for the Lean backend";
   (*
@@ -1414,7 +1419,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     [ comment_pre ^ loop_comment ]
   in
   let name =
-    if !Config.extract_external_name_patterns && not def.is_local then
+    if !extract_external_name_patterns && not def.is_local then
       Some def.llbc_name
     else None
   in
@@ -1433,7 +1438,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.span def.def_id def.loop_id ctx in
   (* Add a break before *)
-  if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+  if backend () <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted definition to its original rust definition *)
   extract_fun_comment ctx fmt def;
@@ -1443,7 +1448,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hvbox fmt 0;
   F.pp_open_vbox fmt ctx.indent_incr;
   (* For HOL4: we may need to put parentheses around the definition *)
-  let parenthesize = !backend = HOL4 && decl_is_not_last_from_group kind in
+  let parenthesize = backend () = HOL4 && decl_is_not_last_from_group kind in
   if parenthesize then F.pp_print_string fmt "(";
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1454,7 +1459,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
 
      The boolean [is_opaque_coq] is used to detect this case.
   *)
-  let is_opaque_coq = !backend = Coq && is_opaque in
+  let is_opaque_coq = backend () = Coq && is_opaque in
   let use_forall =
     is_opaque_coq && def.signature.generics <> empty_generic_params
   in
@@ -1502,7 +1507,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (* [Tot] *)
     if has_decreases_clause then (
       assert_backend_supports_decreases_clauses def.span;
-      if !backend = FStar then (
+      if backend () = FStar then (
         F.pp_print_string fmt "Tot";
         F.pp_print_space fmt ()));
     extract_ty def.span ctx fmt TypeDeclId.Set.empty has_decreases_clause
@@ -1511,7 +1516,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ();
     (* Print the decrease clause - rk.: a function with a decreases clause
      * is necessarily a transparent function *)
-    if has_decreases_clause && !backend = FStar then (
+    if has_decreases_clause && backend () = FStar then (
       assert_backend_supports_decreases_clauses def.span;
       F.pp_print_space fmt ();
       (* Open a box for the decreases clause *)
@@ -1569,7 +1574,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the "=" *)
   if not is_opaque then (
     F.pp_print_space fmt ();
-    let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
@@ -1588,7 +1593,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the inner box for the definition *)
   F.pp_close_box fmt ();
   (* Termination clause and proof for Lean *)
-  if has_decreases_clause && !backend = Lean then (
+  if has_decreases_clause && backend () = Lean then (
     let def_body = Option.get def.body in
     let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
     let num_fwd_inputs =
@@ -1659,10 +1664,10 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the parentheses *)
   if parenthesize then F.pp_print_string fmt ")";
   (* Add the definition end delimiter *)
-  if !backend = HOL4 && decl_is_not_last_from_group kind then (
+  if backend () = HOL4 && decl_is_not_last_from_group kind then (
     F.pp_print_space fmt ();
     F.pp_print_string fmt "/\\")
-  else if !backend = Coq && decl_is_last_from_group kind then (
+  else if backend () = Coq && decl_is_last_from_group kind then (
     (* This is actually an end of group delimiter. For aesthetic reasons
        we print it here instead of in {!end_fun_decl_group}. *)
     F.pp_print_cut fmt ();
@@ -1670,7 +1675,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the outer box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-  if !backend <> HOL4 || decl_is_not_last_from_group kind then
+  if backend () <> HOL4 || decl_is_not_last_from_group kind then
     F.pp_print_break fmt 0 0
 
 (** Extract an opaque function declaration to HOL4.
@@ -1733,7 +1738,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
   sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
   (* We treat HOL4 opaque functions in a specific manner *)
-  if !backend = HOL4 && Option.is_none def.body then
+  if backend () = HOL4 && Option.is_none def.body then
     extract_fun_decl_hol4_opaque ctx fmt def
   else extract_fun_decl_gen ctx fmt kind has_decreases_clause def
 
@@ -1752,7 +1757,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   let is_opaque = Option.is_none extract_body in
 
   (* HOL4: Definition wrapper *)
-  if !backend = HOL4 then (
+  if backend () = HOL4 then (
     (* Open a vertical box: we *must* break lines *)
     F.pp_open_vbox fmt 0;
     F.pp_print_string fmt ("Definition " ^ name ^ "_def:");
@@ -1797,7 +1802,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
@@ -1817,7 +1822,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   F.pp_close_box fmt ();
 
   (* Coq: add a "." *)
-  if !backend = Coq then (
+  if backend () = Coq then (
     F.pp_print_cut fmt ();
     F.pp_print_string fmt ".");
 
@@ -1825,7 +1830,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   F.pp_close_box fmt ();
 
   (* HOL4: Definition wrapper *)
-  if !backend = HOL4 then (
+  if backend () = HOL4 then (
     F.pp_close_box fmt ();
     F.pp_print_space fmt ();
     F.pp_print_string fmt "End";
@@ -1888,7 +1893,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
   let name =
-    if !Config.extract_external_name_patterns && not global.is_local then
+    if !extract_external_name_patterns && not global.is_local then
       Some global.llbc_name
     else None
   in
@@ -1918,7 +1923,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   | None ->
       (* No body: only generate a [val x_c : u32] declaration *)
       let kind = if interface then Declared else Assumed in
-      if !backend = HOL4 then
+      if backend () = HOL4 then
         extract_global_decl_hol4_opaque span ctx fmt decl_name global.generics
           decl_ty
       else
@@ -1949,7 +1954,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
              let use_brackets = all_params <> [] in
              (* Extract the name *)
              let before, after =
-               match !backend with
+               match backend () with
                | FStar | Lean ->
                    ( (fun () ->
                        F.pp_print_string fmt "eval_global";
@@ -1994,7 +1999,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
             let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in
             (* Add a prefix if necessary *)
             let name =
-              if !Config.record_fields_short_names then name
+              if !record_fields_short_names then name
               else ctx_compute_trait_decl_name ctx trait_decl ^ name
             in
             (c.clause_id, name))
@@ -2027,7 +2032,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
             let name = ctx_compute_trait_const_name ctx trait_decl item_name in
             (* Add a prefix if necessary *)
             let name =
-              if !Config.record_fields_short_names then name
+              if !record_fields_short_names then name
               else ctx_compute_trait_decl_name ctx trait_decl ^ name
             in
             (item_name, name))
@@ -2061,7 +2066,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
           let type_name =
             ctx_compute_trait_type_name ctx trait_decl item_name
           in
-          if !Config.record_fields_short_names then type_name
+          if !record_fields_short_names then type_name
           else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
         in
         let compute_clause_name (item_name : string) (clause : trait_clause) :
@@ -2071,7 +2076,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
           in
           (* Add a prefix if necessary *)
           let name =
-            if !Config.record_fields_short_names then name
+            if !record_fields_short_names then name
             else ctx_compute_trait_decl_name ctx trait_decl ^ name
           in
           (clause.clause_id, name)
@@ -2141,7 +2146,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
           let name = ctx_compute_fun_name f ctx in
           (* Add a prefix if necessary *)
           let name =
-            if !Config.record_fields_short_names then name
+            if !record_fields_short_names then name
             else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name
           in
           (item_name, name)
@@ -2271,7 +2276,7 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter)
   (* ":" or "=" *)
   F.pp_print_string fmt separator;
   ty ();
-  (match !Config.backend with Lean -> () | _ -> F.pp_print_string fmt ";");
+  (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";");
   F.pp_close_box fmt ()
 
 let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
@@ -2280,7 +2285,7 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
 
 let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter)
     (item_name : string) (ty : unit -> unit) : unit =
-  let assign = match !Config.backend with Lean | Coq -> ":=" | _ -> "=" in
+  let assign = match backend () with Lean | Coq -> ":=" | _ -> "=" in
   extract_trait_item ctx fmt item_name assign ty
 
 (** Small helper - TODO: move *)
@@ -2325,7 +2330,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
         generics ctx
     in
     let backend_uses_forall =
-      match !backend with Coq | Lean -> true | FStar | HOL4 -> false
+      match backend () with Coq | Lean -> true | FStar | HOL4 -> false
     in
     let generics_not_empty = generics <> empty_generic_params in
     let use_forall = generics_not_empty && backend_uses_forall in
@@ -2350,7 +2355,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
-     if !Config.extract_external_name_patterns && not decl.is_local then
+     if !extract_external_name_patterns && not decl.is_local then
        Some decl.llbc_name
      else None
    in
@@ -2364,7 +2369,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
      There is just an exception with Lean: in this backend, line breaks are important
      for the parsing, so we always open a vertical box.
   *)
-  if !Config.backend = Lean then F.pp_open_vbox fmt ctx.indent_incr
+  if backend () = Lean then F.pp_open_vbox fmt ctx.indent_incr
   else (
     F.pp_open_hvbox fmt 0;
     F.pp_open_hvbox fmt ctx.indent_incr);
@@ -2378,7 +2383,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* When checking if the trait declaration is empty: we ignore the provided
      methods, because for now they are extracted separately *)
   let is_empty = trait_decl_is_empty { decl with provided_methods = [] } in
-  if !backend = FStar && not is_empty then (
+  if backend () = FStar && not is_empty then (
     F.pp_print_string fmt "noeq";
     F.pp_print_space fmt ());
   F.pp_print_string fmt qualif;
@@ -2396,18 +2401,18 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     type_params cg_params trait_clauses;
 
   F.pp_print_space fmt ();
-  if is_empty && !backend = FStar then (
+  if is_empty && backend () = FStar then (
     F.pp_print_string fmt "= unit";
     (* Outer box *)
     F.pp_close_box fmt ())
-  else if is_empty && !backend = Coq then (
+  else if is_empty && backend () = Coq then (
     (* Coq is not very good at infering constructors *)
     let cons = ctx_get_trait_constructor decl.span decl.def_id ctx in
     F.pp_print_string fmt (":= " ^ cons ^ "{}.");
     (* Outer box *)
     F.pp_close_box fmt ())
   else (
-    (match !backend with
+    (match backend () with
     | Lean -> F.pp_print_string fmt "where"
     | FStar -> F.pp_print_string fmt "= {"
     | Coq ->
@@ -2481,9 +2486,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
       decl.required_methods;
 
     (* Close the outer boxes for the definition *)
-    if !Config.backend <> Lean then F.pp_close_box fmt ();
+    if backend () <> Lean then F.pp_close_box fmt ();
     (* Close the brackets *)
-    match !Config.backend with
+    match backend () with
     | Lean -> ()
     | Coq ->
         F.pp_print_space fmt ();
@@ -2554,7 +2559,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
 (** See {!extract_trait_decl_coq_arguments} *)
 let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (trait_decl : trait_decl) : unit =
-  match !backend with
+  match backend () with
   | Coq -> extract_trait_decl_coq_arguments ctx fmt trait_decl
   | _ -> ()
 
@@ -2645,7 +2650,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name, generics =
-     if !Config.extract_external_name_patterns && not impl.is_local then
+     if !extract_external_name_patterns && not impl.is_local then
        let decl_id = impl.impl_trait.trait_decl_id in
        let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
        let decl_ref = impl.llbc_impl_trait in
@@ -2665,7 +2670,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
      There is just an exception with Lean: in this backend, line breaks are important
      for the parsing, so we always open a vertical box.
   *)
-  if !Config.backend = Lean then (
+  if backend () = Lean then (
     F.pp_open_vbox fmt 0;
     F.pp_open_vbox fmt ctx.indent_incr)
   else (
@@ -2705,11 +2710,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in
 
   F.pp_print_space fmt ();
-  if is_empty && !Config.backend = FStar then (
+  if is_empty && backend () = FStar then (
     F.pp_print_string fmt "= ()";
     (* Outer box *)
     F.pp_close_box fmt ())
-  else if is_empty && !Config.backend = Coq then (
+  else if is_empty && backend () = Coq then (
     (* Coq is not very good at infering constructors *)
     let cons =
       ctx_get_trait_constructor impl.span impl.impl_trait.trait_decl_id ctx
@@ -2718,8 +2723,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (* Outer box *)
     F.pp_close_box fmt ())
   else (
-    if !Config.backend = Lean then F.pp_print_string fmt ":= {"
-    else if !Config.backend = Coq then F.pp_print_string fmt ":= {|"
+    if backend () = Lean then F.pp_print_string fmt ":= {"
+    else if backend () = Coq then F.pp_print_string fmt ":= {|"
     else F.pp_print_string fmt "= {";
 
     (* Close the box for the name + generics *)
@@ -2811,10 +2816,10 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* Close the outer boxes for the definition, as well as the brackets *)
     F.pp_close_box fmt ();
-    if !backend = Coq then (
+    if backend () = Coq then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "|}.")
-    else if (not (!backend = FStar)) || not is_empty then (
+    else if (not (backend () = FStar)) || not is_empty then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "}"));
   F.pp_close_box fmt ();
@@ -2854,7 +2859,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     (* Open a box for the test *)
     F.pp_open_hovbox fmt ctx.indent_incr;
     (* Print the test *)
-    (match !backend with
+    (match backend () with
     | FStar ->
         F.pp_print_string fmt "let _ =";
         F.pp_print_space fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 815e228f..3346c328 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -495,14 +495,14 @@ let names_maps_add_function (id_to_string : id -> string)
     names_maps =
   names_maps_add id_to_string (FunId fid) span name nm
 
-let bool_name () = if !backend = Lean then "Bool" else "bool"
-let char_name () = if !backend = Lean then "Char" else "char"
-let str_name () = if !backend = Lean then "String" else "string"
+let bool_name () = if backend () = Lean then "Bool" else "bool"
+let char_name () = if backend () = Lean then "Char" else "char"
+let str_name () = if backend () = Lean then "String" else "string"
 
 (** Small helper to compute the name of an int type *)
 let int_name (int_ty : integer_type) : string =
   let isize, usize, i_format, u_format =
-    match !backend with
+    match backend () with
     | FStar | Coq | HOL4 ->
         ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
     | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
@@ -525,9 +525,9 @@ let scalar_name (ty : literal_type) : string =
   match ty with
   | TInteger ty -> int_name ty
   | TBool -> (
-      match !backend with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+      match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
   | TChar -> (
-      match !backend with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+      match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
 
 (** Extraction context.
 
@@ -786,13 +786,13 @@ let ctx_get_termination_measure (span : Meta.span) (def_id : A.FunDeclId.id)
 let unop_name (unop : unop) : string =
   match unop with
   | Not -> (
-      match !backend with
+      match backend () with
       | FStar -> "not"
       | Lean -> "¬"
       | Coq -> "negb"
       | HOL4 -> "~")
   | Neg (int_ty : integer_type) -> (
-      match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
+      match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
   | Cast _ ->
       (* We never directly use the unop name in this case *)
       raise (Failure "Unsupported")
@@ -821,7 +821,7 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
-  match !backend with
+  match backend () with
   | Lean -> int_name int_ty ^ "." ^ binop_s
   | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
 
@@ -843,7 +843,7 @@ let keywords () =
       named_binops
   in
   let misc =
-    match !backend with
+    match backend () with
     | FStar ->
         [
           "assert";
@@ -1042,7 +1042,7 @@ let keywords () =
 let assumed_adts () : (assumed_ty * string) list =
   let state =
     if !use_state then
-      match !backend with
+      match backend () with
       | Lean -> [ (TState, "State") ]
       | Coq | FStar | HOL4 -> [ (TState, "state") ]
     else []
@@ -1051,7 +1051,7 @@ let assumed_adts () : (assumed_ty * string) list =
      referenced in the generated translation, and easily collides
      with user-defined types *)
   let adts =
-    match !backend with
+    match backend () with
     | Lean ->
         [
           (TResult, "Result");
@@ -1065,7 +1065,7 @@ let assumed_adts () : (assumed_ty * string) list =
     | Coq | FStar | HOL4 ->
         [
           (TResult, "result");
-          (TFuel, if !backend = HOL4 then "num" else "nat");
+          (TFuel, if backend () = HOL4 then "num" else "nat");
           (TArray, "array");
           (TSlice, "slice");
           (TStr, "str");
@@ -1076,14 +1076,14 @@ let assumed_adts () : (assumed_ty * string) list =
   state @ adts
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
-  match !backend with
+  match backend () with
   | Lean -> [ (TArray, "Array.make") ]
   | Coq -> [ (TArray, "mk_array") ]
   | FStar -> [ (TArray, "mk_array") ]
   | HOL4 -> [ (TArray, "mk_array") ]
 
 let assumed_variants () : (assumed_ty * VariantId.id * string) list =
-  match !backend with
+  match backend () with
   | FStar ->
       [
         (TResult, result_ok_id, "Ok");
@@ -1123,7 +1123,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
 
 let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
-  match !backend with
+  match backend () with
   | FStar | Coq | HOL4 ->
       [
         (ArrayIndexShared, "array_index_usize");
@@ -1146,7 +1146,7 @@ let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
       ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
-  match !backend with
+  match backend () with
   | FStar ->
       [
         (Return, "return");
@@ -1258,7 +1258,7 @@ let initialize_names_maps () : names_maps =
  *)
 let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
     (type_kind : type_decl_kind option) : string option =
-  match !backend with
+  match backend () with
   | FStar -> (
       match kind with
       | SingleNonRec -> Some "type"
@@ -1307,7 +1307,7 @@ let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
     Remark: can return [None] for some backends like HOL4.
  *)
 let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
-  match !backend with
+  match backend () with
   | FStar -> (
       match kind with
       | SingleNonRec -> Some "let"
@@ -1342,7 +1342,7 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
     TODO: move inside the formatter?
  *)
 let type_keyword (span : Meta.span) =
-  match !backend with
+  match backend () with
   | FStar -> "Type0"
   | Coq | Lean -> "Type"
   | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
@@ -1391,7 +1391,7 @@ let ctx_compute_type_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
 let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) =
   let name = ctx_compute_type_name_no_suffix span ctx name in
-  match !backend with
+  match backend () with
   | FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
   | Coq | HOL4 -> name ^ "_t"
   | Lean -> name
@@ -1425,7 +1425,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
     let def_name =
       ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ field_name_s
     in
-    match !backend with
+    match backend () with
     | Lean | HOL4 -> def_name
     | Coq | FStar -> StringUtils.lowercase_first_letter def_name
 
@@ -1435,7 +1435,7 @@ let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
  *)
 let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx)
     (def_name : llbc_name) (variant : string) : string =
-  match !backend with
+  match backend () with
   | FStar | Coq | HOL4 ->
       let variant = to_camel_case variant in
       if !variant_concatenate_type_name then
@@ -1465,14 +1465,14 @@ let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
   let fname = ctx_compute_simple_name span ctx fname in
   (* TODO: don't convert to snake case for Coq, HOL4, F* *)
   let fname = flatten_name fname in
-  match !backend with
+  match backend () with
   | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
   | Lean -> fname
 
 (** Provided a basename, compute the name of a global declaration. *)
 let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
     (name : llbc_name) : string =
-  match !Config.backend with
+  match Config.backend () with
   | Coq | FStar | HOL4 ->
       let parts =
         List.map to_snake_case (ctx_compute_simple_name span ctx name)
@@ -1537,7 +1537,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
   in
   let name = flatten_name name in
-  match !backend with
+  match backend () with
   | FStar -> StringUtils.lowercase_first_letter name
   | Coq | HOL4 | Lean -> name
 
@@ -1614,7 +1614,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
   in
   let clause = clause ^ "Inst" in
-  match !backend with
+  match backend () with
   | FStar -> StringUtils.lowercase_first_letter clause
   | Coq | HOL4 | Lean -> clause
 
@@ -1633,7 +1633,7 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
      can't disambiguate fields coming from different ADTs if they have the same
      names), and thus don't need to add a prefix starting with a lowercase.
   *)
-  match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
 
 let ctx_compute_trait_const_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1642,7 +1642,7 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx)
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
   in
   (* See [trait_type_name] *)
-  match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
 
 let ctx_compute_trait_method_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1677,7 +1677,7 @@ let ctx_compute_termination_measure_name (span : Meta.span)
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> "_decreases"
     | Lean -> "_terminates"
     | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
@@ -1706,7 +1706,7 @@ let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
-    match !Config.backend with
+    match Config.backend () with
     | Lean -> "_decreases"
     | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
   in
@@ -1747,7 +1747,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
   match basename with
   | Some basename -> (
       (* This should be a no-op *)
-      match !Config.backend with
+      match Config.backend () with
       | Lean -> basename
       | FStar | Coq | HOL4 -> to_snake_case basename)
   | None -> (
@@ -1779,7 +1779,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
               name_from_type_ident (TypesUtils.as_ident cl))
       | TVar _ -> (
           (* TODO: use "t" also for F* *)
-          match !backend with
+          match backend () with
           | FStar -> "x" (* lacking inspiration here... *)
           | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
       | TLiteral lty -> (
@@ -1792,7 +1792,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
     string =
   (* Rust type variables are snake-case and start with a capital letter *)
-  match !backend with
+  match backend () with
   | FStar ->
       (* This is *not* a no-op: this removes the capital letter *)
       to_snake_case basename
@@ -1805,7 +1805,7 @@ let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
 let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
     (basename : string) : string =
   (* Rust type variables are snake-case and start with a capital letter *)
-  match !backend with
+  match backend () with
   | FStar | HOL4 ->
       (* This is *not* a no-op: this removes the capital letter *)
       to_snake_case basename
@@ -1827,7 +1827,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
       params.trait_clauses clause_id
   in
   let clause = clause ^ "Inst" in
-  match !backend with
+  match backend () with
   | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
   | Lean -> clause
 
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index ff936d2f..37b676bb 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -43,13 +43,13 @@ let split_on_separator (s : string) : string list =
   Str.split (Str.regexp "\\(::\\|\\.\\)") s
 
 let flatten_name (name : string list) : string =
-  match !backend with
+  match backend () with
   | FStar | Coq | HOL4 -> String.concat "_" name
   | Lean -> String.concat "." name
 
 (** Utility for Lean-only definitions **)
 let mk_lean_only (funs : 'a list) : 'a list =
-  match !backend with Lean -> funs | _ -> []
+  match backend () with Lean -> funs | _ -> []
 
 let () =
   assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
@@ -61,7 +61,7 @@ let () =
     is F*, Coq or HOL4, and a different value if the target is Lean.
  *)
 let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
-  match !backend with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+  match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
 
 let builtin_globals : (string * string) list =
   [
@@ -135,9 +135,11 @@ type type_variant_kind =
 
 let mk_struct_constructor (type_name : string) : string =
   let prefix =
-    match !backend with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+    match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+  in
+  let suffix =
+    match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk"
   in
-  let suffix = match !backend with FStar | Coq | HOL4 -> "" | Lean -> ".mk" in
   prefix ^ type_name ^ suffix
 
 (** The assumed types.
@@ -164,7 +166,7 @@ let builtin_types () : builtin_type_info list =
             List.map
               (fun (rname, name) ->
                 ( rname,
-                  match !backend with
+                  match backend () with
                   | FStar | Lean -> name
                   | Coq | HOL4 -> extract_name ^ "_" ^ name ))
               fields
@@ -197,7 +199,7 @@ let builtin_types () : builtin_type_info list =
     {
       rust_name = parse_pattern "core::option::Option";
       extract_name =
-        (match !backend with
+        (match backend () with
         | Lean -> "Option"
         | Coq | FStar | HOL4 -> "option");
       keep_params = None;
@@ -208,7 +210,7 @@ let builtin_types () : builtin_type_info list =
                {
                  rust_variant_name = "None";
                  extract_variant_name =
-                   (match !backend with
+                   (match backend () with
                    | FStar | Coq -> "None"
                    | Lean -> "none"
                    | HOL4 -> "NONE");
@@ -217,7 +219,7 @@ let builtin_types () : builtin_type_info list =
                {
                  rust_variant_name = "Some";
                  extract_variant_name =
-                   (match !backend with
+                   (match backend () with
                    | FStar | Coq -> "Some"
                    | Lean -> "some"
                    | HOL4 -> "SOME");
@@ -529,7 +531,7 @@ let mk_builtin_fun_effects () : (pattern * effect_info) list =
     builtin_funs
 
 let mk_builtin_fun_effects_map () =
-  NameMatcherMap.of_list (mk_builtin_fun_effects ())
+  NameMatcherMap.of_list (if_backend mk_builtin_fun_effects [])
 
 let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map
 
@@ -571,7 +573,7 @@ let builtin_trait_decls_info () =
           else extract_name ^ "_" ^ item_name
         in
         let type_name =
-          match !backend with
+          match backend () with
           | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
           | Lean -> type_name
         in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index cc0c351d..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -19,12 +19,12 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
     (cv : literal) : unit =
   match cv with
   | VScalar sv -> (
-      match !backend with
+      match backend () with
       | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
       | Coq | HOL4 | Lean ->
-          let print_brackets = inside && !backend = HOL4 in
+          let print_brackets = inside && backend () = HOL4 in
           if print_brackets then F.pp_print_string fmt "(";
-          (match !backend with
+          (match backend () with
           | Coq | Lean -> ()
           | HOL4 ->
               F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
@@ -34,7 +34,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
           if sv.value >= Z.of_int 0 then
             F.pp_print_string fmt (Z.to_string sv.value)
           else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
-          (match !backend with
+          (match backend () with
           | Coq ->
               let iname = int_name sv.int_ty in
               F.pp_print_string fmt ("%" ^ iname)
@@ -46,13 +46,13 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
           if print_brackets then F.pp_print_string fmt ")")
   | VBool b ->
       let b =
-        match !backend with
+        match backend () with
         | HOL4 -> if b then "T" else "F"
         | Coq | FStar | Lean -> if b then "true" else "false"
       in
       F.pp_print_string fmt b
   | VChar c -> (
-      match !backend with
+      match backend () with
       | HOL4 ->
           (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
           F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
@@ -99,7 +99,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
   | Cast (src, tgt) -> (
       (* HOL4 has a special treatment: because it doesn't support dependent
          types, we don't have a specific operator for the cast *)
-      match !backend with
+      match backend () with
       | HOL4 ->
           (* Casting, say, an u32 to an i32 would be done as follows:
              {[
@@ -121,7 +121,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
           (* Different cases depending on the conversion *)
           (let cast_str, src, tgt =
              let integer_type_to_string (ty : integer_type) : string =
-               if !backend = Lean then "." ^ int_name ty
+               if backend () = Lean then "." ^ int_name ty
                else
                  StringUtils.capitalize_first_letter
                    (PrintPure.integer_type_to_string ty)
@@ -129,20 +129,20 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
              match (src, tgt) with
              | TInteger src, TInteger tgt ->
                  let cast_str =
-                   match !backend with
+                   match backend () with
                    | Coq | FStar -> "scalar_cast"
                    | Lean -> "Scalar.cast"
                    | HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
                  in
                  let src =
-                   if !backend <> Lean then Some (integer_type_to_string src)
+                   if backend () <> Lean then Some (integer_type_to_string src)
                    else None
                  in
                  let tgt = integer_type_to_string tgt in
                  (cast_str, src, Some tgt)
              | TBool, TInteger tgt ->
                  let cast_str =
-                   match !backend with
+                   match backend () with
                    | Coq | FStar -> "scalar_cast_bool"
                    | Lean -> "Scalar.cast_bool"
                    | HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
@@ -198,7 +198,7 @@ let extract_binop (span : Meta.span)
     (arg0 : texpression) (arg1 : texpression) : unit =
   if inside then F.pp_print_string fmt "(";
   (* Some binary operations have a special notation depending on the backend *)
-  (match (!backend, binop) with
+  (match (backend (), binop) with
   | HOL4, (Eq | Ne)
   | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
   | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
@@ -207,7 +207,7 @@ let extract_binop (span : Meta.span)
         | Eq -> "="
         | Lt -> "<"
         | Le -> "<="
-        | Ne -> if !backend = Lean then "!=" else "<>"
+        | Ne -> if backend () = Lean then "!=" else "<>"
         | Ge -> ">="
         | Gt -> ">"
         | Div -> "/"
@@ -225,7 +225,9 @@ let extract_binop (span : Meta.span)
         | BitAnd -> "&&&"
       in
       let binop =
-        match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop
+        match backend () with
+        | FStar | Lean | HOL4 -> binop
+        | Coq -> "s" ^ binop
       in
       extract_expr false arg0;
       F.pp_print_space fmt ();
@@ -239,7 +241,7 @@ let extract_binop (span : Meta.span)
       (* In the case of F*, for shift operations, because machine integers
          are simply integers with a refinement, if the second argument is a
          constant we need to provide the second implicit type argument *)
-      if binop_is_shift && !backend = FStar && is_const arg1 then (
+      if binop_is_shift && backend () = FStar && is_const arg1 then (
         F.pp_print_space fmt ();
         let ty = ty_as_integer span arg1.ty in
         F.pp_print_string fmt
@@ -275,7 +277,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
  *)
 let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
     (is_rec : bool) (dg : Pure.fun_decl list) =
-  match !backend with
+  match backend () with
   | FStar | Coq | Lean -> ()
   | HOL4 ->
       (* In HOL4, opaque functions have a special treatment *)
@@ -304,7 +306,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
 (** See {!start_fun_decl_group}. *)
 let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
     (dg : Pure.fun_decl list) =
-  match !backend with
+  match backend () with
   | FStar -> ()
   | Coq ->
       (* For aesthetic reasons, we print the Coq end group delimiter directly
@@ -335,7 +337,7 @@ let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
 (** See {!start_fun_decl_group}: similar usage, but for the type declarations. *)
 let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
     (is_rec : bool) (dg : Pure.type_decl list) =
-  match !backend with
+  match backend () with
   | FStar | Coq -> ()
   | Lean ->
       if is_rec && List.length dg > 1 then (
@@ -362,7 +364,7 @@ let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
 (** See {!start_fun_decl_group}. *)
 let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
     (dg : Pure.type_decl list) =
-  match !backend with
+  match backend () with
   | FStar -> ()
   | Coq ->
       (* For aesthetic reasons, we print the Coq end group delimiter directly
@@ -394,11 +396,11 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
         F.pp_print_break fmt 0 0)
 
 let unit_name () =
-  match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
+  match backend () with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
 
 (** Small helper *)
 let extract_arrow (fmt : F.formatter) () : unit =
-  if !Config.backend = Lean then F.pp_print_string fmt "→"
+  if Config.backend () = Lean then F.pp_print_string fmt "→"
   else F.pp_print_string fmt "->"
 
 let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
@@ -441,7 +443,7 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
  *)
 
 let extract_ty_errors (fmt : F.formatter) : unit =
-  match !Config.backend with
+  match Config.backend () with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
   | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
@@ -463,7 +465,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
               (fun () ->
                 F.pp_print_space fmt ();
                 let product =
-                  match !backend with
+                  match backend () with
                   | FStar -> "&"
                   | Coq -> "*"
                   | Lean -> "×"
@@ -480,7 +482,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
              In HOL4 we would write:
              `('a, 'b) tree`
           *)
-          match !backend with
+          match backend () with
           | FStar | Coq | Lean ->
               let print_paren = inside && has_params in
               if print_paren then F.pp_print_string fmt "(";
@@ -556,7 +558,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
             type_name ctx
         in
         let add_brackets (s : string) =
-          if !backend = Coq then "(" ^ s ^ ")" else s
+          if backend () = Coq then "(" ^ s ^ ")" else s
         in
         (* There may be a special treatment depending on the instance id.
            See the comments for {!extract_trait_instance_id_with_dot}.
@@ -575,7 +577,9 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
             F.pp_print_string fmt type_name
         | _ ->
             (* HOL4 doesn't have 1st class types *)
-            cassert __FILE__ __LINE__ (!backend <> HOL4) span
+            cassert __FILE__ __LINE__
+              (backend () <> HOL4)
+              span
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref span ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
@@ -624,14 +628,16 @@ and extract_generic_args (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t)
     (generics : generic_args) : unit =
   let { types; const_generics; trait_refs } = generics in
-  if !backend <> HOL4 then (
+  if backend () <> HOL4 then (
     if types <> [] then (
       F.pp_print_space fmt ();
       Collections.List.iter_link (F.pp_print_space fmt)
         (extract_ty span ctx fmt no_params_tys true)
         types);
     if const_generics <> [] then (
-      cassert __FILE__ __LINE__ (!backend <> HOL4) span
+      cassert __FILE__ __LINE__
+        (backend () <> HOL4)
+        span
         "Constant generics are not supported yet when generating code for HOL4";
       F.pp_print_space fmt ();
       Collections.List.iter_link (F.pp_print_space fmt)
@@ -682,7 +688,9 @@ and extract_trait_instance_id_with_dot (span : Meta.span) (ctx : extraction_ctx)
 and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
     (id : trait_instance_id) : unit =
-  let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in
+  let add_brackets (s : string) =
+    if backend () = Coq then "(" ^ s ^ ")" else s
+  in
   match id with
   | Self ->
       (* This has a specific treatment depending on the item we're extracting
@@ -812,7 +820,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
                     in
                     (* Add the type name prefix for Lean *)
                     let name =
-                      if !Config.backend = Lean then
+                      if Config.backend () = Lean then
                         let type_name =
                           ctx_compute_type_name def.span ctx def.llbc_name
                         in
@@ -859,7 +867,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
   (* [| Cons :]
    * Note that we really don't want any break above so we print everything
    * at once. *)
-  let opt_colon = if !backend <> HOL4 then " :" else "" in
+  let opt_colon = if backend () <> HOL4 then " :" else "" in
   F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon);
   let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
       extraction_ctx =
@@ -871,7 +879,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
      * Note that when printing fields, we register the field names as
      * *variables*: they don't need to be unique at the top level. *)
     let ctx =
-      match !backend with
+      match backend () with
       | FStar -> (
           match f.field_name with
           | None -> ctx
@@ -887,10 +895,10 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
       | Coq | Lean | HOL4 -> ctx
     in
     (* Print the field type *)
-    let inside = !backend = HOL4 in
+    let inside = backend () = HOL4 in
     extract_ty span ctx fmt type_decl_group inside f.field_ty;
     (* Print the arrow [->] *)
-    if !backend <> HOL4 then (
+    if backend () <> HOL4 then (
       F.pp_print_space fmt ();
       extract_arrow fmt ());
     (* Close the field box *)
@@ -904,9 +912,9 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
     List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
   in
   (* Sanity check: HOL4 doesn't support const generics *)
-  sanity_check __FILE__ __LINE__ (cg_params = [] || !backend <> HOL4) span;
+  sanity_check __FILE__ __LINE__ (cg_params = [] || backend () <> HOL4) span;
   (* Print the final type *)
-  if !backend <> HOL4 then (
+  if backend () <> HOL4 then (
     F.pp_print_space fmt ();
     F.pp_open_hovbox fmt 0;
     F.pp_print_string fmt type_name;
@@ -978,7 +986,7 @@ let extract_type_decl_tuple_struct_body (span : Meta.span)
     F.pp_print_space fmt ();
     F.pp_print_string fmt (unit_name ()))
   else
-    let sep = match !backend with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
+    let sep = match backend () with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
     Collections.List.iter_link
       (fun () ->
         F.pp_print_space fmt ();
@@ -1049,28 +1057,28 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
   (* Note that we already printed: [type t =] *)
   let is_rec = decl_is_from_rec_group kind in
   let _ =
-    if !backend = FStar && fields = [] then (
+    if backend () = FStar && fields = [] then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt (unit_name ()))
-    else if !backend = Lean && fields = [] then ()
+    else if backend () = Lean && fields = [] then ()
       (* If the definition is recursive, we may need to extract it as an inductive
          (instead of a record). We start with the "normal" case: we extract it
          as a record. *)
-    else if (not is_rec) || (!backend <> Coq && !backend <> Lean) then (
-      if !backend <> Lean then F.pp_print_space fmt ();
+    else if (not is_rec) || (backend () <> Coq && backend () <> Lean) then (
+      if backend () <> Lean then F.pp_print_space fmt ();
       (* If Coq: print the constructor name *)
       (* TODO: remove superfluous test not is_rec below *)
-      if !backend = Coq && not is_rec then (
+      if backend () = Coq && not is_rec then (
         F.pp_print_string fmt (ctx_get_struct def.span (TAdtId def.def_id) ctx);
         F.pp_print_string fmt " ");
-      (match !backend with
+      (match backend () with
       | Lean -> ()
       | FStar | Coq -> F.pp_print_string fmt "{"
       | HOL4 -> F.pp_print_string fmt "<|");
       F.pp_print_break fmt 1 ctx.indent_incr;
       (* The body itself *)
       (* Open a box for the body *)
-      (match !backend with
+      (match backend () with
       | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
       | Lean -> F.pp_open_vbox fmt 0);
       (* Print the fields *)
@@ -1085,7 +1093,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt ":";
         F.pp_print_space fmt ();
         extract_ty def.span ctx fmt type_decl_group false f.field_ty;
-        if !backend <> Lean then F.pp_print_string fmt ";";
+        if backend () <> Lean then F.pp_print_string fmt ";";
         (* Close the box for the field *)
         F.pp_close_box fmt ()
       in
@@ -1095,7 +1103,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         fields;
       (* Close the box for the body *)
       F.pp_close_box fmt ();
-      match !backend with
+      match backend () with
       | Lean -> ()
       | FStar | Coq ->
           F.pp_print_space fmt ();
@@ -1107,7 +1115,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* We extract for Coq or Lean, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type *)
       cassert __FILE__ __LINE__
-        (is_rec && (!backend = Coq || !backend = Lean))
+        (is_rec && (backend () = Coq || backend () = Lean))
         def.span
         "Constant generics are not supported yet when generating code for HOL4";
       (* Small trick: in Lean we use namespaces, meaning we don't need to prefix
@@ -1115,7 +1123,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
          i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
          we generate `inductive Foo := | mk ... *)
       let cons_name =
-        if !backend = Lean then "mk"
+        if backend () = Lean then "mk"
         else ctx_get_struct def.span (TAdtId def.def_id) ctx
       in
       let def_name = ctx_get_local_type def.span def.def_id ctx in
@@ -1128,7 +1136,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   (* Delimiters, space after we break a line *)
   let ld, space, rd =
-    match !backend with
+    match backend () with
     | Coq | FStar | HOL4 -> ("(** ", 4, " *)")
     | Lean -> ("/- ", 3, " -/")
   in
@@ -1223,18 +1231,18 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
   let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
   (* HOL4 doesn't support const generics *)
   cassert __FILE__ __LINE__
-    (cg_params = [] || !backend <> HOL4)
+    (cg_params = [] || backend () <> HOL4)
     span "Constant generics are not supported yet when generating code for HOL4";
   let left_bracket (implicit : bool) =
-    if implicit && !backend <> FStar then F.pp_print_string fmt "{"
+    if implicit && backend () <> FStar then F.pp_print_string fmt "{"
     else F.pp_print_string fmt "("
   in
   let right_bracket (implicit : bool) =
-    if implicit && !backend <> FStar then F.pp_print_string fmt "}"
+    if implicit && backend () <> FStar then F.pp_print_string fmt "}"
     else F.pp_print_string fmt ")"
   in
   let print_implicit_symbol (implicit : bool) =
-    if implicit && !backend = FStar then F.pp_print_string fmt "#" else ()
+    if implicit && backend () = FStar then F.pp_print_string fmt "#" else ()
   in
   let insert_req_space () =
     match space with
@@ -1254,7 +1262,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
         (const_generics : const_generic_var list)
         (trait_clauses : trait_clause list) : unit =
       (* Note that in HOL4 we don't print the type parameters. *)
-      if !backend <> HOL4 then (
+      if backend () <> HOL4 then (
         (* Print the type parameters *)
         if type_params <> [] then (
           insert_req_space ();
@@ -1372,7 +1380,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
     (extract_body : bool) : unit =
   (* Sanity check *)
-  sanity_check __FILE__ __LINE__ (extract_body || !backend <> HOL4) def.span;
+  sanity_check __FILE__ __LINE__ (extract_body || backend () <> HOL4) def.span;
   let is_tuple_struct =
     TypesUtils.type_decl_from_decl_id_is_tuple_struct
       ctx.trans_ctx.type_ctx.type_infos def.def_id
@@ -1397,7 +1405,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
      The boolean [is_opaque_coq] is used to detect this case.
   *)
   let is_opaque = type_kind = None in
-  let is_opaque_coq = !backend = Coq && is_opaque in
+  let is_opaque_coq = backend () = Coq && is_opaque in
   let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.span def.def_id ctx in
@@ -1408,7 +1416,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
       ctx
   in
   (* Add a break before *)
-  if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+  if backend () <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
@@ -1423,7 +1431,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line. Note however that in the case of Lean line breaks are important
    * for parsing: we thus use a hovbox. *)
-  (match !backend with
+  (match backend () with
   | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
   | Lean ->
       if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
@@ -1433,7 +1441,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
      We need this annotation, otherwise Lean sometimes doesn't manage to typecheck
      the expressions when it needs to coerce the type.
   *)
-  if is_tuple_struct_one_or_zero_field && !backend = Lean then (
+  if is_tuple_struct_one_or_zero_field && backend () = Lean then (
     F.pp_print_string fmt "@[reducible]";
     F.pp_print_space fmt ())
   else ();
@@ -1445,7 +1453,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* HOL4 doesn't support const generics, and type definitions in HOL4 don't
      support trait clauses *)
   cassert __FILE__ __LINE__
-    ((cg_params = [] && trait_clauses = []) || !backend <> HOL4)
+    ((cg_params = [] && trait_clauses = []) || backend () <> HOL4)
     def.span
     "Constant generics and type definitions with trait clauses are not \
      supported yet when generating code for HOL4";
@@ -1456,7 +1464,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if extract_body then (
     F.pp_print_space fmt ();
     let eq =
-      match !backend with
+      match backend () with
       | FStar -> "="
       | Coq ->
           (* For Coq, the `*` is overloaded. If we want to extract a product
@@ -1493,10 +1501,10 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
            type_params cg_params variants
      | Opaque -> craise __FILE__ __LINE__ def.span "Unreachable");
   (* Add the definition end delimiter *)
-  if !backend = HOL4 && decl_is_not_last_from_group kind then (
+  if backend () = HOL4 && decl_is_not_last_from_group kind then (
     F.pp_print_space fmt ();
     F.pp_print_string fmt ";")
-  else if !backend = Coq && decl_is_last_from_group kind then (
+  else if backend () = Coq && decl_is_last_from_group kind then (
     (* This is actually an end of group delimiter. For aesthetic reasons
        we print it here instead of in {!end_type_decl_group}. *)
     F.pp_print_cut fmt ();
@@ -1504,7 +1512,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-  if !backend <> HOL4 || decl_is_not_last_from_group kind then
+  if backend () <> HOL4 || decl_is_not_last_from_group kind then
     F.pp_print_break fmt 0 0
 
 (** Extract an opaque type declaration to HOL4.
@@ -1572,11 +1580,11 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
     | Assumed | Declared -> false
   in
   if extract_body then
-    if !backend = HOL4 && is_empty_record_type_decl def then
+    if backend () = HOL4 && is_empty_record_type_decl def then
       extract_type_decl_hol4_empty_record ctx fmt def
     else extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
   else
-    match !backend with
+    match backend () with
     | FStar | Coq | Lean ->
         extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
     | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def
@@ -1625,7 +1633,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
-  sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span;
+  sanity_check __FILE__ __LINE__ (backend () = Coq) decl.span;
   (* Generating the [Arguments] instructions is useful only if there are parameters *)
   let num_params =
     List.length decl.generics.types
@@ -1674,7 +1682,9 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
-  sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span;
+  sanity_check __FILE__ __LINE__
+    (backend () = Coq || backend () = Lean)
+    decl.span;
   match decl.kind with
   | Opaque | Enum _ -> ()
   | Struct fields ->
@@ -1704,7 +1714,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           F.pp_open_hvbox fmt ctx.indent_incr;
 
           (* For Lean: add some attributes *)
-          if !backend = Lean then (
+          if backend () = Lean then (
             (* Box for the attributes *)
             F.pp_open_vbox fmt 0;
             (* Annotate the projectors with both simp and reducible.
@@ -1717,7 +1727,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
 
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
-          (match !backend with
+          (match backend () with
           | Lean -> F.pp_print_string fmt "def"
           | Coq -> F.pp_print_string fmt "Definition"
           | _ -> internal_error __FILE__ __LINE__ decl.span);
@@ -1729,7 +1739,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           let field_name =
             ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
           in
-          if !backend = Lean then (
+          if backend () = Lean then (
             F.pp_print_string fmt def_name;
             F.pp_print_string fmt ".");
           F.pp_print_string fmt field_name;
@@ -1795,7 +1805,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           F.pp_close_box fmt ();
 
           (* Print the [end] *)
-          if !backend = Coq then (
+          if backend () = Coq then (
             F.pp_print_space fmt ();
             F.pp_print_string fmt "end");
 
@@ -1804,7 +1814,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Close the inner box projector *)
           F.pp_close_box fmt ();
           (* If Coq: end the definition with a "." *)
-          if !backend = Coq then (
+          if backend () = Coq then (
             F.pp_print_cut fmt ();
             F.pp_print_string fmt ".");
           (* Close the outer box for projector definition *)
@@ -1842,7 +1852,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Close the inner box projector *)
           F.pp_close_box fmt ();
           (* If Coq: end the definition with a "." *)
-          if !backend = Coq then (
+          if backend () = Coq then (
             F.pp_print_cut fmt ();
             F.pp_print_string fmt ".");
           (* Close the outer box projector  *)
@@ -1854,7 +1864,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
         let extract_field_proj_and_notation (field_id : FieldId.id)
             (field : field) : unit =
           extract_field_proj field_id field;
-          if !backend = Coq then extract_proj_notation field_id field
+          if backend () = Coq then extract_proj_notation field_id field
         in
 
         FieldId.iteri extract_field_proj_and_notation fields
@@ -1866,7 +1876,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
  *)
 let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
-  match !backend with
+  match backend () with
   | FStar | HOL4 -> ()
   | Lean | Coq ->
       if
@@ -1874,7 +1884,8 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
           (TypesUtils.type_decl_from_decl_id_is_tuple_struct
              ctx.trans_ctx.type_ctx.type_infos decl.def_id)
       then (
-        if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl;
+        if backend () = Coq then
+          extract_type_decl_coq_arguments ctx fmt kind decl;
         extract_type_decl_record_field_projectors ctx fmt kind decl)
 
 (** Extract the state type declaration. *)
@@ -1893,7 +1904,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
   (* The syntax for Lean and Coq is almost identical. *)
   let print_axiom () =
     let axiom =
-      match !backend with
+      match backend () with
       | Coq -> "Axiom"
       | Lean -> "axiom"
       | FStar | HOL4 -> raise (Failure "Unexpected")
@@ -1905,14 +1916,14 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
     F.pp_print_string fmt "Type";
-    if !backend = Coq then F.pp_print_string fmt "."
+    if backend () = Coq then F.pp_print_string fmt "."
   in
   (* The kind should be [Assumed] or [Declared] *)
   (match kind with
   | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast ->
       raise (Failure "Unexpected")
   | Assumed -> (
-      match !backend with
+      match backend () with
       | FStar ->
           F.pp_print_string fmt "assume";
           F.pp_print_space fmt ();
@@ -1927,7 +1938,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
       | Coq | Lean -> print_axiom ())
   | Declared -> (
-      match !backend with
+      match backend () with
       | FStar ->
           F.pp_print_string fmt "val";
           F.pp_print_space fmt ();
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 29322049..557a3993 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -68,9 +68,13 @@ let () =
 
   let spec_ls =
     [
+      ( "-borrow-check",
+        Arg.Set borrow_check,
+        " Only borrow-check the program and do not generate any translation" );
       ( "-backend",
         Arg.Symbol (backend_names, set_backend),
-        " Specify the target backend" );
+        " Specify the target backend (" ^ String.concat ", " backend_names ^ ")"
+      );
       ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
       ( "-test-units",
         Arg.Set test_unit_functions,
@@ -137,6 +141,12 @@ let () =
   let check_arg_name name =
     assert (List.exists (fun (n, _, _) -> n = name) spec_ls)
   in
+
+  let fail_with_error (msg : string) =
+    log#serror msg;
+    fail ()
+  in
+
   let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool)
       (name1 : string) : unit =
     check_arg_name name0;
@@ -160,6 +170,14 @@ let () =
       fail ())
   in
 
+  let check (cond : bool) (msg : string) =
+    if not cond then fail_with_error msg
+  in
+
+  let check_not (cond : bool) (msg : string) =
+    if cond then fail_with_error msg
+  in
+
   if !print_llbc then main_log#set_level EL.Debug;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
@@ -176,44 +194,63 @@ let () =
   check_arg_implies
     (not !generate_lib_entry_point)
     "-no-gen-lib-entry" !split_files "-split-files";
-  if !lean_gen_lakefile && not (!backend = Lean) then
-    log#error
+  if !lean_gen_lakefile && not (backend () = Lean) then
+    fail_with_error
       "The -lean-default-lakefile option is valid only for the Lean backend";
 
+  if !borrow_check then (
+    check (!dest_dir = "") "Options -borrow-check and -dest are not compatible";
+    check_not !split_files
+      "Options -borrow-check and -split-files are not compatible";
+    check_not !test_unit_functions
+      "Options -borrow-check and -test-unit-functions are not compatible";
+    check_not !test_trans_unit_functions
+      "Options -borrow-check and -test-trans-units are not compatible";
+    check_not !extract_decreases_clauses
+      "Options -borrow-check and -decreases-clauses are not compatible";
+    check_not !use_state
+      "Options -borrow-check and -use-state are not compatible";
+    check_not !use_fuel "Options -borrow-check and -use-fuel are not compatible";
+    check_not !split_files
+      "Options -borrow-check and -split-files are not compatible");
+
   (* Check that the user specified a backend *)
   let _ =
     match !opt_backend with
-    | Some b -> backend := b
+    | Some _ ->
+        check_not !borrow_check
+          "Arguments `-backend` and `-borrow-check` are not compatible"
     | None ->
-        log#error "Backend not specified (use the `-backend` argument)";
-        fail ()
+        check !borrow_check "Missing `-backend` or `-borrow-check` argument"
   in
 
   (* Set some options depending on the backend *)
   let _ =
-    match !backend with
-    | FStar ->
-        (* F* can disambiguate the field names *)
-        record_fields_short_names := true
-    | Coq ->
-        (* Some patterns are not supported *)
-        decompose_monadic_let_bindings := true;
-        decompose_nested_let_patterns := true
-    | Lean ->
-        (* We don't support fuel for the Lean backend *)
-        if !use_fuel then (
-          log#error "The Lean backend doesn't support the -use-fuel option";
-          fail ());
-        (* Lean can disambiguate the field names *)
-        record_fields_short_names := true;
-        (* We exploit the fact that the variant name should always be
-           prefixed with the type name to prevent collisions *)
-        variant_concatenate_type_name := false
-    | HOL4 ->
-        (* We don't support fuel for the HOL4 backend *)
-        if !use_fuel then (
-          log#error "The HOL4 backend doesn't support the -use-fuel option";
-          fail ())
+    match !opt_backend with
+    | None -> ()
+    | Some backend -> (
+        match backend with
+        | FStar ->
+            (* F* can disambiguate the field names *)
+            record_fields_short_names := true
+        | Coq ->
+            (* Some patterns are not supported *)
+            decompose_monadic_let_bindings := true;
+            decompose_nested_let_patterns := true
+        | Lean ->
+            (* We don't support fuel for the Lean backend *)
+            check_not !use_fuel
+              "The Lean backend doesn't support the -use-fuel option";
+            (* Lean can disambiguate the field names *)
+            record_fields_short_names := true;
+            (* We exploit the fact that the variant name should always be
+               prefixed with the type name to prevent collisions *)
+            variant_concatenate_type_name := false
+        | HOL4 ->
+            (* We don't support fuel for the HOL4 backend *)
+            if !use_fuel then (
+              log#error "The HOL4 backend doesn't support the -use-fuel option";
+              fail ()))
   in
 
   (* Retrieve and check the filename *)
@@ -251,7 +288,7 @@ let () =
 
       (* We don't support mutually recursive definitions with decreases clauses in Lean *)
       if
-        !backend = Lean && !extract_decreases_clauses
+        !opt_backend = Some Lean && !extract_decreases_clauses
         && List.exists
              (function
                | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a4319b28..a22a39ab 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -649,7 +649,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     (* Convert, if possible - note that for now for Lean and Coq
                        we don't support the structure syntax on recursive structures *)
                     if
-                      (!Config.backend <> Lean && !Config.backend <> Coq)
+                      (Config.backend () <> Lean && Config.backend () <> Coq)
                       || not is_rec
                     then
                       let struct_id = TAdtId adt_id in
@@ -1295,7 +1295,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                    the shape [{ x with f := v }]).
 
                    This is not supported by Coq *)
-                !Config.backend <> Coq
+                Config.backend () <> Coq
               then (
                 (* Compute the number of occurrences of each variable *)
                 let occurs = ref VarId.Map.empty in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e7dcd933..fe5d3414 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -241,7 +241,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
         msg (* TODO : check if true should'nt be returned instead ? *)
 
 let texpression_requires_parentheses span e =
-  match !Config.backend with
+  match Config.backend () with
   | FStar | Lean -> false
   | Coq | HOL4 -> let_group_requires_parentheses span e
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 848bfe50..ba6bba68 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3693,7 +3693,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
   let fail_branch =
     mk_result_fail_texpression_with_error_id span error_out_of_fuel_id body.ty
   in
-  match !Config.backend with
+  match Config.backend () with
   | FStar ->
       (* Generate an expression:
          {[
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0f887ec8..690bff5c 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -665,7 +665,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
           let extract_decrease decl =
             let has_decr_clause = has_decreases_clause decl in
             if has_decr_clause then
-              match !Config.backend with
+              match Config.backend () with
               | Lean ->
                   Extract.extract_template_lean_termination_and_decreasing ctx
                     fmt decl
@@ -864,7 +864,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
    * internal count is consistent with the state of the file.
    *)
   (* Create the header *)
-  (match !Config.backend with
+  (match Config.backend () with
   | Lean ->
       Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
       Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
@@ -873,7 +873,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
         "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
       Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
   (* Generate the imports *)
-  (match !Config.backend with
+  (match Config.backend () with
   | FStar ->
       Printf.fprintf out "module %s\n" fi.module_name;
       Printf.fprintf out "open Primitives\n";
@@ -957,7 +957,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   Format.pp_print_newline fmt ();
 
   (* Close the module *)
-  (match !Config.backend with
+  (match Config.backend () with
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
@@ -1039,7 +1039,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       trans_ctx;
       names_maps;
       indent_incr = 2;
-      use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
+      use_dep_ite =
+        Config.backend () = Lean && !Config.extract_decreases_clauses;
       trait_decl_id = None (* None by default *);
       is_provided_method = false (* false by default *);
       trans_trait_decls;
@@ -1113,13 +1114,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         (* Convert the case *)
         let crate_name = StringUtils.to_camel_case basename in
         let crate_name =
-          if !Config.backend = HOL4 then
+          if Config.backend () = HOL4 then
             StringUtils.lowercase_first_letter crate_name
           else crate_name
         in
         (* We use the raw crate name for the namespaces *)
         let namespace =
-          match !Config.backend with
+          match Config.backend () with
           | FStar | Coq | HOL4 -> crate.name
           | Lean -> crate.name
         in
@@ -1144,7 +1145,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Lean reflects the module hierarchy within the filesystem, so we need to
      create more directories *)
-  if !Config.backend = Lean then (
+  if Config.backend () = Lean then (
     let ( ^^ ) = Filename.concat in
     if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
     if needs_clauses_module then (
@@ -1156,7 +1157,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     (* Retrieve the executable's directory *)
     let exe_dir = Filename.dirname Sys.argv.(0) in
     let primitives_src_dest =
-      match !Config.backend with
+      match Config.backend () with
       | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
@@ -1190,18 +1191,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Extract the file(s) *)
   let module_delimiter =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> "."
     | Coq -> "_"
     | Lean -> "."
     | HOL4 -> "_"
   in
   let file_delimiter =
-    if !Config.backend = Lean then "/" else module_delimiter
+    if Config.backend () = Lean then "/" else module_delimiter
   in
   (* File extension for the "regular" modules *)
   let ext =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> ".fst"
     | Coq -> ".v"
     | Lean -> ".lean"
@@ -1209,7 +1210,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
   in
   (* File extension for the opaque module *)
   let opaque_ext =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> ".fsti"
     | Coq -> ".v"
     | Lean -> ".lean"
@@ -1253,7 +1254,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             For the other backends, we generate a template file as a model
             for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
-           match !Config.backend with
+           match Config.backend () with
            | FStar ->
                ("TypesExternal", "TypesExternal", ": external type declarations")
            | HOL4 | Coq | Lean ->
@@ -1306,7 +1307,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
      (* Extract the non opaque types *)
      let types_filename_ext =
-       match !Config.backend with
+       match Config.backend () with
        | FStar -> ".fst"
        | Coq -> ".v"
        | Lean -> ".lean"
@@ -1377,7 +1378,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             For the other backends, we generate a template file as a model
             for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
-           match !Config.backend with
+           match Config.backend () with
            | FStar ->
                ( "FunsExternal",
                  "FunsExternal",
@@ -1445,7 +1446,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      let clauses_module =
        if needs_clauses_module then
          let clauses_submodule =
-           if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+           if Config.backend () = Lean then module_delimiter ^ "Clauses" else ""
          in
          [ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
        else []
@@ -1501,7 +1502,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      extract_file gen_config ctx file_info);
 
   (* Generate the build file *)
-  match !Config.backend with
+  match Config.backend () with
   | Coq | FStar | HOL4 ->
       ()
       (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.
-- 
cgit v1.2.3


From 49c8e42ec3bcfc323e61c5ba0345abeb41372ac4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:50:21 +0200
Subject: Implement a BorrowCheck.borrow_check_crate

---
 compiler/BorrowCheck.ml | 28 ++++++++++++++++++++++++++++
 compiler/Interpreter.ml | 18 +++++++++++++-----
 compiler/Logging.ml     |  3 +++
 compiler/Main.ml        |  9 ++++++---
 compiler/Translate.ml   |  5 +++--
 compiler/dune           |  1 +
 6 files changed, 54 insertions(+), 10 deletions(-)
 create mode 100644 compiler/BorrowCheck.ml

diff --git a/compiler/BorrowCheck.ml b/compiler/BorrowCheck.ml
new file mode 100644
index 00000000..52f42c37
--- /dev/null
+++ b/compiler/BorrowCheck.ml
@@ -0,0 +1,28 @@
+open Interpreter
+open LlbcAst
+
+(** The local logger *)
+let log = Logging.borrow_check_log
+
+(** Borrow-check a crate.
+
+    Note that we don't return anything: if we find borrow-checking errors,
+    we register them and print them later.
+ *)
+let borrow_check_crate (crate : crate) : unit =
+  (* Debug *)
+  log#ldebug (lazy "translate_crate_to_pure");
+
+  (* Compute the translation context *)
+  let trans_ctx = compute_contexts crate in
+
+  (* Borrow-check *)
+  let borrow_check_fun (fdef : fun_decl) : unit =
+    match fdef.body with
+    | None -> ()
+    | Some _ ->
+        let synthesize = false in
+        let _ = evaluate_function_symbolic synthesize trans_ctx fdef in
+        ()
+  in
+  List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fb3701f3..81d6ff72 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -489,9 +489,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     - the list of symbolic values introduced for the input values (this is
       useful for the synthesis)
     - the symbolic AST generated by the symbolic execution
+
+   If [synthesize] is [true]: we synthesize the symbolic AST that is used for
+   the translation. Otherwise, we do not (the symbolic execution then simply
+   borrow-checks the function).
  *)
-let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
-    symbolic_value list * SA.expression =
+let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+    (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
     Print.Types.name_to_string
@@ -615,9 +619,13 @@ let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
       let ctx_resl, cc =
         eval_function_body config (Option.get fdef.body).body ctx
       in
-      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
-      cc el
-    with CFailure (span, msg) -> Error (span, msg)
+      if synthesize then
+        (* Finish synthesizing *)
+        let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+        Some (cc el)
+      else None
+    with CFailure (span, msg) ->
+      if synthesize then Some (Error (span, msg)) else None
   in
   (* Return *)
   (input_svs, symbolic)
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 9b8019b2..620c5fb5 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -15,6 +15,9 @@ let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy"
 (** Logger for Translate *)
 let translate_log = L.get_logger "MainLogger.Translate"
 
+(** Logger for BorrowCheck *)
+let borrow_check_log = L.get_logger "MainLogger.BorrowCheck"
+
 (** Logger for Contexts *)
 let contexts_log = L.get_logger "MainLogger.Contexts"
 
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 557a3993..1bf9196a 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -309,8 +309,9 @@ let () =
          (* Test the unit functions with the concrete interpreter *)
          if !test_unit_functions then Test.test_unit_functions m;
 
-         (* Translate the functions *)
-         Aeneas.Translate.translate_crate filename dest_dir m
+         (* Translate or borrow-check the crate *)
+         if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m
+         else Aeneas.Translate.translate_crate filename dest_dir m
        with Errors.CFailure (_, _) ->
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
@@ -323,7 +324,9 @@ let () =
           (* Reverse the list of error messages so that we print them from the
              earliest to the latest. *)
           (List.rev !Errors.error_list);
-        exit 1);
+        exit 1)
+      else if !borrow_check then
+        log#linfo (lazy "Crate successfully borrow-checked");
 
       (* Print total elapsed time *)
       log#linfo
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 690bff5c..2bc9bb25 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,8 +31,9 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   | None -> None
   | Some _ ->
       (* Evaluate *)
-      let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
-      Some (inputs, symb)
+      let synthesize = true in
+      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+      Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
 
diff --git a/compiler/dune b/compiler/dune
index 6bdfd153..f987faec 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -14,6 +14,7 @@
  (modules
   AssociatedTypes
   Assumed
+  BorrowCheck
   Collections
   Config
   ConstStrings
-- 
cgit v1.2.3


From bb1caf9a8efdadd599560b3ff7a12d275a12f696 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 15:03:01 +0200
Subject: Update the test runner to allow the syntax [!lean] and [borrow-check]

---
 tests/src/betree/aeneas-test-options         |  2 +-
 tests/src/bitwise.rs                         |  2 +-
 tests/src/constants.rs                       |  2 +-
 tests/src/external.rs                        |  4 ++--
 tests/src/hashmap.rs                         |  2 +-
 tests/src/mutually-recursive-traits.lean.out | 14 +++++++-------
 tests/src/mutually-recursive-traits.rs       |  4 ++--
 tests/src/no_nested_borrows.rs               |  2 +-
 tests/src/paper.rs                           |  2 +-
 tests/src/polonius_list.rs                   |  2 +-
 tests/src/string-chars.rs                    |  2 +-
 tests/test_runner/Backend.ml                 | 18 ++++++++++++++++--
 tests/test_runner/Input.ml                   | 28 +++++++++++++++++++---------
 tests/test_runner/run_test.ml                | 15 +++++++++++----
 14 files changed, 65 insertions(+), 34 deletions(-)

diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
index c71e01df..5a1e4180 100644
--- a/tests/src/betree/aeneas-test-options
+++ b/tests/src/betree/aeneas-test-options
@@ -1,4 +1,4 @@
 charon-args=--polonius --opaque=betree_utils
-aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
 [coq] aeneas-args=-use-fuel
 [fstar] aeneas-args=-decreases-clauses -template-clauses
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index fda8eff3..be12cea0 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,4 +1,4 @@
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Exercise the bitwise operations
 
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index ac24dcd4..71d7c557 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Tests with constants
 
diff --git a/tests/src/external.rs b/tests/src/external.rs
index baea76e4..00acdb0b 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,6 +1,6 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-state -split-files
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module uses external types and functions
 
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 19832a84..7dda2404 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--opaque=utils
-//@ aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index 6d638644..e2ed3abc 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
 [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 812:
+[Error] In file Translate.ml, line 813:
 Mutually recursive trait declarations are not supported
 
 Uncaught exception:
   
   (Failure
-    "In file Translate.ml, line 812:\
-   \nIn file Translate.ml, line 812:\
+    "In file Translate.ml, line 813:\
+   \nIn file Translate.ml, line 813:\
    \nMutually recursive trait declarations are not supported")
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42
+Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66
diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs
index 351763b2..9bc4ca63 100644
--- a/tests/src/mutually-recursive-traits.rs
+++ b/tests/src/mutually-recursive-traits.rs
@@ -1,6 +1,6 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
-//@ subdir=misc
+//@ [!lean] skip
+//@ [lean] subdir=misc
 pub trait Trait1 {
     type T: Trait2;
 }
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 6d3074ef..11c4a695 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 6a4a7c31..d9fb1032 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! The examples from the ICFP submission, all in one place.
 
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index b029ad02..084441aa 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--polonius
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
index f8490e76..9fd91752 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,5 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
+//@ [!lean] skip
 //@ no-check-output
 fn main() {
     let s = "hello";
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
index d21a46fc..819081a2 100644
--- a/tests/test_runner/Backend.ml
+++ b/tests/test_runner/Backend.ml
@@ -1,15 +1,24 @@
 (*** Define the backends we support as an enum *)
 
-type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
+type t =
+  | Coq
+  | Lean
+  | FStar
+  | HOL4
+  | BorrowCheck
+      (** Borrow check: no backend.
+          We use this when we only want to borrow-check the program *)
+[@@deriving ord, sexp]
 
 (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-let all = [ Coq; Lean; FStar ]
+let all = [ Coq; Lean; FStar; BorrowCheck ]
 
 let of_string = function
   | "coq" -> Coq
   | "lean" -> Lean
   | "fstar" -> FStar
   | "hol4" -> HOL4
+  | "borrow-check" -> BorrowCheck
   | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
 
 let to_string = function
@@ -17,6 +26,11 @@ let to_string = function
   | Lean -> "lean"
   | FStar -> "fstar"
   | HOL4 -> "hol4"
+  | BorrowCheck -> "borrow-check"
+
+let to_command = function
+  | BorrowCheck -> [ "-borrow-check" ]
+  | x -> [ "-backend"; to_string x ]
 
 module Map = struct
   (* Hack to be able to include things from the parent module with the same names *)
diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
index 960ffe8d..e35be96f 100644
--- a/tests/test_runner/Input.ml
+++ b/tests/test_runner/Input.ml
@@ -7,7 +7,7 @@ type action = Normal | Skip | KnownFailure
 type per_backend = {
   action : action;
   aeneas_options : string list;
-  subdir : string;
+  subdir : string option;
   (* Whether to store the command output to a file. Only available for known-failure tests. *)
   check_output : bool;
 }
@@ -22,8 +22,11 @@ type t = {
 }
 
 (* The default subdirectory in which to store the outputs. *)
-let default_subdir backend test_name =
-  match backend with Backend.Lean -> "." | _ -> test_name
+let default_subdir backend test_name : string option =
+  match backend with
+  | Backend.Lean -> Some "."
+  | Backend.BorrowCheck -> None
+  | _ -> Some test_name
 
 (* Parse lines that start `//@`. Each of them modifies the options we use for the test.
    Supported comments:
@@ -39,14 +42,21 @@ let default_subdir backend test_name =
 let apply_special_comment comment input =
   let comment = String.trim comment in
   (* Parse the backends if any *)
-  let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in
+  let re = Re.compile (Re.Pcre.re "^\\[(!)?([a-zA-Z,-]+)\\](.*)$") in
   let comment, (backends : Backend.t list) =
     match Re.exec_opt re comment with
     | Some groups ->
-        let backends = Re.Group.get groups 1 in
+        let exclude = Re.Group.get_opt groups 1 <> None in
+        let backends = Re.Group.get groups 2 in
         let backends = String.split_on_char ',' backends in
         let backends = List.map Backend.of_string backends in
-        let rest = Re.Group.get groups 2 in
+        let rest = Re.Group.get groups 3 in
+        (* If [exclude]: we take all the backends *but* the list provided. *)
+        let backends =
+          if exclude then
+            List.filter (fun x -> not (List.mem x backends)) Backend.all
+          else backends
+        in
         (String.trim rest, backends)
     | None -> (comment, Backend.all)
   in
@@ -83,9 +93,9 @@ let apply_special_comment comment input =
     let args = String.split_on_char ' ' args in
     per_backend (fun x ->
         { x with aeneas_options = List.append x.aeneas_options args })
-  else if Option.is_some subdir then
-    let subdir = Option.get subdir in
-    per_backend (fun x -> { x with subdir })
+  else if Option.is_some subdir then (
+    assert (not (List.mem Backend.BorrowCheck backends));
+    per_backend (fun x -> { x with subdir }))
   else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
 
 (* Given a path to a rust file or crate, gather the details and options about how to build the test. *)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index c17c17be..9bdfe81d 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -50,21 +50,28 @@ end
 (* Run Aeneas on a specific input with the given options *)
 let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let backend_str = Backend.to_string backend in
+  let backend_command = Backend.to_command backend in
   let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
+
   let per_backend = Backend.Map.find backend case.per_backend in
   let subdir = per_backend.subdir in
   let check_output = per_backend.check_output in
   let aeneas_options = per_backend.aeneas_options in
   let action = per_backend.action in
-  let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
+  (* No destination directory if we borrow-check *)
+  let dest_command =
+    match backend with
+    | Backend.BorrowCheck -> []
+    | _ ->
+        let subdir = match subdir with None -> [] | Some x -> [ x ] in
+        [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ]
+  in
 
   (* Build the command *)
-  let args =
-    [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
-  in
+  let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
   let abort_on_error =
     match action with
     | Skip | Normal -> []
-- 
cgit v1.2.3


From a6c9ab139977982f610f3d46e2e2f4c141880c3c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:12:15 +0200
Subject: Relax some constraints in the symbolic execution when borrow-checking

---
 compiler/Interpreter.ml                | 36 ++++++++++++++++++++++++++++------
 compiler/InterpreterLoopsFixedPoint.ml | 26 ++++++++++++++++--------
 compiler/InterpreterLoopsMatchCtxs.ml  |  5 ++++-
 compiler/Print.ml                      |  3 ++-
 4 files changed, 54 insertions(+), 16 deletions(-)

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 81d6ff72..b2e55841 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -362,6 +362,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       ctx)
     else ctx
   in
+  log#ldebug
+    (lazy
+      ("evaluate_function_symbolic_synthesize_backward_from_return: (after \
+        putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n"
+      ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx));
 
   (* We now need to end the proper *input* abstractions - pay attention
    * to the fact that we end the *input* abstractions, not the *return*
@@ -418,7 +423,28 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                }
              ]}
           *)
-          (None, false)
+          (* If we are borrow-checking: end the synth input abstraction to
+             check there is no borrow-checking issue.
+             Otherwise, do nothing.
+
+             We need this check because of the following:
+             {[
+               fn loop_reborrow_mut1<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+                   let mut x = 0;
+                   while x > 0 {
+                       x += 1;
+                   }
+                   if x > 0 {
+                       a
+                   } else {
+                       b // Failure
+                   }
+               }
+             ]}
+             (remark: this is slightly ad-hoc, and we won't need to do that
+              once we make the handling of loops more general).
+          *)
+          if !Config.borrow_check then (Some fun_abs_id, true) else (None, false)
       | Some abs -> (Some abs.abs_id, false)
   in
   log#ldebug
@@ -619,11 +645,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
       let ctx_resl, cc =
         eval_function_body config (Option.get fdef.body).body ctx
       in
-      if synthesize then
-        (* Finish synthesizing *)
-        let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
-        Some (cc el)
-      else None
+      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+      (* Finish synthesizing *)
+      if synthesize then Some (cc el) else None
     with CFailure (span, msg) ->
       if synthesize then Some (Error (span, msg)) else None
   in
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 735f3743..0d770e80 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -665,8 +665,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     in
     List.iter end_at_return (fst (eval_loop_body fp));
 
-    (* Check that the sets of abstractions we need to end per region group are pairwise
-     * disjoint *)
+    (* Check that the sets of abstractions we need to end per region group are
+       pairwise disjoint *)
     let aids_union = ref AbstractionId.Set.empty in
     let _ =
       RegionGroupId.Map.iter
@@ -680,8 +680,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
         !fp_ended_aids
     in
 
-    (* We also check that all the regions need to end - this is not necessary per
-       se, but if it doesn't happen it is bizarre and worth investigating... *)
+    (* If we generate a translation, we check that all the regions need to end
+       - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
+       We need this check for now for technical reasons to make the translation work.
+    *)
     sanity_check __FILE__ __LINE__
       (AbstractionId.Set.equal !aids_union !fp_aids)
       span;
@@ -779,9 +781,11 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
        no region group, and we set them as endable just above).
 
        If [remove_rg_id] is [false], we simply set the abstractions as non-endable
-       to freeze them (we will use the fixed point as starting point for the
-       symbolic execution of the loop body, and we have to make sure the input
-       abstractions are frozen).
+       **when generating a pure translation** to freeze them (we will use the
+       fixed point as starting point for the symbolic execution of the loop body,
+       and we have to make sure the input abstractions are frozen).
+       If we are simply borrow-checking the program, we can set the abstraction
+       as endable.
     *)
     let update_loop_abstractions (remove_rg_id : bool) =
       object
@@ -796,7 +800,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
               in
-              { abs with can_end = remove_rg_id; kind }
+              (* If we borrow check we can always set the abstraction as
+                 endable. If we generate a pure translation we have a few
+                 more constraints. *)
+              let can_end =
+                if !Config.borrow_check then true else remove_rg_id
+              in
+              { abs with can_end; kind }
           | _ -> abs
       end
     in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 3f7c023e..a1c0841a 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span)
         | Loop (loop_id', rg_id, kind) ->
             sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
             sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
-            let can_end = false in
+            (* If we borrow-check: we can set the abstractions as endable.
+               If we synthesize we have to constrain the region abstractions
+               a bit. *)
+            let can_end = !Config.borrow_check in
             let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
             let abs = { abs with kind; can_end } in
             super#visit_abs env abs
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7495d6bf..8bd709d0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -309,13 +309,14 @@ module Values = struct
     let kind =
       if verbose then "[kind:" ^ abs_kind_to_string abs.kind ^ "]" else ""
     in
+    let can_end = if abs.can_end then "{endable}" else "{frozen}" in
     indent ^ "abs@"
     ^ AbstractionId.to_string abs.abs_id
     ^ kind ^ "{parents="
     ^ AbstractionId.Set.to_string None abs.parents
     ^ "}" ^ "{regions="
     ^ RegionId.Set.to_string None abs.regions
-    ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
+    ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
 
   let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) :
       string =
-- 
cgit v1.2.3


From 0a0ab7c0e159e736a3187b8121d106ee76651f57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:47:52 +0200
Subject: Relax more checks for borrow-checking

---
 compiler/InterpreterLoopsFixedPoint.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 0d770e80..3760d15a 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -683,9 +683,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     (* If we generate a translation, we check that all the regions need to end
        - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
        We need this check for now for technical reasons to make the translation work.
+       If we only borrow-check, we can ignore this.
     *)
     sanity_check __FILE__ __LINE__
-      (AbstractionId.Set.equal !aids_union !fp_aids)
+      (!Config.borrow_check || AbstractionId.Set.equal !aids_union !fp_aids)
       span;
 
     (* Merge the abstractions which need to be merged, and compute the map from
-- 
cgit v1.2.3


From c6ba96bf0723fd46432d73e52eaf6b0859c75fa8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:48:08 +0200
Subject: Update the test runner

---
 tests/test_runner/run_test.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 9bdfe81d..0c3426c5 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -72,10 +72,13 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
 
   (* Build the command *)
   let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
+  (* If we target a specific backend and the test is known to fail, we abort
+     on error so as not to generate any files *)
   let abort_on_error =
     match action with
     | Skip | Normal -> []
-    | KnownFailure -> [ "-abort-on-error" ]
+    | KnownFailure ->
+        if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ]
   in
   let args = List.concat [ args; aeneas_options; abort_on_error ] in
   let cmd = Command.make args in
-- 
cgit v1.2.3


From 31c749247b30c1f88c0842a26f4f9956c92404be Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:48:22 +0200
Subject: Add more tests

---
 tests/src/loops-borrow-check-fail.borrow-check.out | 17 +++++++++++++
 tests/src/loops-borrow-check-fail.rs               | 21 ++++++++++++++++
 .../loops-borrow-check-negative.borrow-check.out   |  3 +++
 tests/src/loops-borrow-check-negative.rs           | 28 ++++++++++++++++++++++
 tests/src/loops-borrow-check.rs                    | 10 ++++++++
 5 files changed, 79 insertions(+)
 create mode 100644 tests/src/loops-borrow-check-fail.borrow-check.out
 create mode 100644 tests/src/loops-borrow-check-fail.rs
 create mode 100644 tests/src/loops-borrow-check-negative.borrow-check.out
 create mode 100644 tests/src/loops-borrow-check-negative.rs
 create mode 100644 tests/src/loops-borrow-check.rs

diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
new file mode 100644
index 00000000..54bb2102
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -0,0 +1,17 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_fail.llbc
+[Error] Inconsistent projection:
+- pe: Expressions.Deref
+- v:
+Values.VBottom
+- ty:
+(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
+   Types.RMut))
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1
+[Error] Inconsistent projection:
+- pe: Expressions.Deref
+- v:
+Values.VBottom
+- ty:
+(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
+   Types.RShared))
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs
new file mode 100644
index 00000000..24be052c
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.rs
@@ -0,0 +1,21 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// We need to use the general rules for joining the loans
+fn loop_reborrow_mut() {
+    let mut x = 0;
+    let mut px = &mut x;
+    while *px > 0 {
+        x += 1;
+        px = &mut x;
+    }
+}
+
+// We need to imrpove [prepare_ashared_loans]
+fn iter_local_shared_borrow() {
+    let mut x = 0;
+    let mut p = &x;
+    loop {
+        p = &(*p);
+    }
+}
diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..093d8b8a
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.borrow-check.out
@@ -0,0 +1,3 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_negative.llbc
+[Error] Can't end abstraction 16 as it is set as non-endable
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66
diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs
new file mode 100644
index 00000000..3386d581
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.rs
@@ -0,0 +1,28 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// This succeeds
+fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b
+    }
+}
+
+// This fails
+fn loop_a_b<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b // Expect lifetime 'a
+    }
+}
diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs
new file mode 100644
index 00000000..ab300b37
--- /dev/null
+++ b/tests/src/loops-borrow-check.rs
@@ -0,0 +1,10 @@
+//@ [!borrow-check] skip
+
+fn iter_local_mut_borrow() {
+    let mut x = 0;
+    let mut p = &mut x;
+    loop {
+        p = &mut (*p);
+        *p += 1;
+    }
+}
-- 
cgit v1.2.3


From 7cb0914c68a055a308539ccc781fea8f30ef27bb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:03:57 +0200
Subject: Update an error message

---
 compiler/InterpreterPaths.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 8a924a0a..992146de 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -250,12 +250,16 @@ let rec access_projection (span : Meta.span) (access : projection_access)
                     Ok (ctx, { res with updated = nv })
               else Error (FailSharedLoan bids))
       | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r ->
-          let pe, v, ty = r in
-          let pe = "- pe: " ^ show_projection_elem pe in
-          let v = "- v:\n" ^ show_value v in
-          let ty = "- ty:\n" ^ show_ety ty in
-          craise __FILE__ __LINE__ span
-            ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
+          if v.value = VBottom then
+            craise __FILE__ __LINE__ span
+              "Can not apply a projection to the ⊥ value"
+          else
+            let pe, v, ty = r in
+            let pe = "- pe: " ^ show_projection_elem pe in
+            let v = "- v:\n" ^ show_value v in
+            let ty = "- ty:\n" ^ show_ety ty in
+            craise __FILE__ __LINE__ span
+              ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
 
 (** Generic function to access (read/write) the value at a given place.
 
-- 
cgit v1.2.3


From afe15cc3208b16b95109f056656c1c3d312841cc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:04:05 +0200
Subject: Add some negative tests for the borrow checker

---
 tests/src/borrow-check-negative.borrow-check.out | 15 ++++
 tests/src/borrow-check-negative.rs               | 90 ++++++++++++++++++++++++
 2 files changed, 105 insertions(+)
 create mode 100644 tests/src/borrow-check-negative.borrow-check.out
 create mode 100644 tests/src/borrow-check-negative.rs

diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..dc9dd5a7
--- /dev/null
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -0,0 +1,15 @@
+[Info ] Imported: tests/llbc/borrow_check_negative.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1
+[Error] Can't end abstraction 8 as it is set as non-endable
+Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1
diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs
new file mode 100644
index 00000000..697546dd
--- /dev/null
+++ b/tests/src/borrow-check-negative.rs
@@ -0,0 +1,90 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+// Some negative tests for borrow checking
+
+// This succeeds
+fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn choose_test() {
+    let mut x = 0;
+    let mut y = 0;
+    let z = choose(true, &mut x, &mut y);
+    *z += 1;
+    assert!(*z == 1);
+    // drop(z)
+    assert!(x == 1);
+    assert!(y == 0);
+    assert!(*z == 1); // z is not valid anymore
+}
+
+fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y // Expected lifetime 'a
+    }
+}
+
+fn test_mut1(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &mut x } else { &mut y };
+    *z += 1;
+    assert!(x >= 0);
+    *z += 1; // z is not valid anymore
+}
+
+#[allow(unused_assignments)]
+fn test_mut2(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &x } else { &y };
+    x += 1;
+    assert!(*z == 0); // z is not valid anymore
+}
+
+fn test_move1<T>(x: T) -> T {
+    let _ = x;
+    return x; // x has been moved
+}
+
+pub fn refs_test1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    **ppx = 1;
+    assert!(x == 1);
+    assert!(**ppx == 1); // ppx has ended
+}
+
+pub fn refs_test2() {
+    let mut x = 0;
+    let mut y = 1;
+    let mut px = &mut x;
+    let py = &mut y;
+    let ppx = &mut px;
+    *ppx = py;
+    **ppx = 2;
+    assert!(*px == 2);
+    assert!(x == 0);
+    assert!(*py == 2);
+    assert!(y == 2);
+    assert!(**ppx == 2); // ppx has ended
+}
+
+pub fn test_box1() {
+    use std::ops::Deref;
+    use std::ops::DerefMut;
+    let mut b: Box<i32> = Box::new(0);
+    let x0 = b.deref_mut();
+    *x0 = 1;
+    let x1 = b.deref();
+    assert!(*x1 == 1);
+    assert!(*x0 == 1); // x0 has ended
+}
-- 
cgit v1.2.3


From c4eb37f33259fe2c58de43c36fe3457644c7d9df Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:13:24 +0200
Subject: Regenerate some tests

---
 tests/src/loops-borrow-check-fail.borrow-check.out | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
index 54bb2102..34eb75f8 100644
--- a/tests/src/loops-borrow-check-fail.borrow-check.out
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -1,17 +1,5 @@
 [Info ] Imported: tests/llbc/loops_borrow_check_fail.llbc
-[Error] Inconsistent projection:
-- pe: Expressions.Deref
-- v:
-Values.VBottom
-- ty:
-(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
-   Types.RMut))
+[Error] Can not apply a projection to the ⊥ value
 Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1
-[Error] Inconsistent projection:
-- pe: Expressions.Deref
-- v:
-Values.VBottom
-- ty:
-(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
-   Types.RShared))
+[Error] Can not apply a projection to the ⊥ value
 Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
-- 
cgit v1.2.3


From 9e18eb774c78bd2344bff45cb689f742c91470d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:48:08 +0200
Subject: Update the betree

---
 tests/src/betree/src/betree.rs | 197 ++++++++++++++++++++---------------------
 1 file changed, 98 insertions(+), 99 deletions(-)

diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs
index 12f2847d..8ba07824 100644
--- a/tests/src/betree/src/betree.rs
+++ b/tests/src/betree/src/betree.rs
@@ -274,25 +274,41 @@ pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value {
 
 impl<T> List<T> {
     fn len(&self) -> u64 {
-        match self {
-            List::Nil => 0,
-            List::Cons(_, tl) => 1 + tl.len(),
+        let mut l = self;
+        let mut len = 0;
+        while let List::Cons(_, tl) = l {
+            len += 1;
+            l = tl;
         }
+        len
     }
 
     /// Split a list at a given length
-    fn split_at(self, n: u64) -> (List<T>, List<T>) {
-        if n == 0 {
-            (List::Nil, self)
-        } else {
-            match self {
+    fn split_at(self, mut n: u64) -> (List<T>, List<T>) {
+        let mut beg = List::Nil;
+        let mut end = self;
+        while n > 0 {
+            match end {
                 List::Nil => unreachable!(),
-                List::Cons(hd, tl) => {
-                    let (ls0, ls1) = tl.split_at(n - 1);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
+                List::Cons(hd, mut tl) => {
+                    n -= 1;
+                    end = *tl;
+                    *tl = beg;
+                    beg = List::Cons(hd, tl);
                 }
             }
         }
+        (beg.reverse(), end)
+    }
+
+    fn reverse(mut self) -> Self {
+        let mut out = List::Nil;
+        while let List::Cons(hd, mut tl) = self {
+            self = *tl;
+            *tl = out;
+            out = List::Cons(hd, tl);
+        }
+        out
     }
 
     /// Push an element at the front of the list.
@@ -337,17 +353,20 @@ impl<T> Map<Key, T> {
     /// Note that the bindings in the map are supposed to be sorted in
     /// order of increasing keys.
     fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) {
-        match self {
-            List::Nil => (List::Nil, List::Nil),
-            List::Cons(hd, tl) => {
-                if hd.0 >= pivot {
-                    (List::Nil, List::Cons(hd, tl))
-                } else {
-                    let (ls0, ls1) = tl.partition_at_pivot(pivot);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
-                }
+        let mut beg = List::Nil;
+        let mut end = List::Nil;
+        let mut curr = self;
+        while let List::Cons(hd, mut tl) = curr {
+            curr = *tl;
+            if hd.0 >= pivot {
+                *tl = end;
+                end = List::Cons(hd, tl);
+            } else {
+                *tl = beg;
+                beg = List::Cons(hd, tl);
             }
         }
+        (beg.reverse(), end.reverse())
     }
 }
 
@@ -443,14 +462,11 @@ impl Node {
     /// Apply a list of message to ourselves: leaf node case
     fn apply_messages_to_leaf<'a>(
         bindings: &'a mut Map<Key, Value>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
-                Node::apply_messages_to_leaf(bindings, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -501,14 +517,11 @@ impl Node {
     /// Apply a list of message to ourselves: internal node case
     fn apply_messages_to_internal<'a>(
         msgs: &'a mut Map<Key, Message>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
-                Node::apply_messages_to_internal(msgs, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -633,38 +646,34 @@ impl Node {
 
     /// Lookup a value in a list of bindings.
     /// Note that the values should be stored in order of increasing key.
-    fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> {
-        match bindings {
-            List::Nil => Option::None,
-            List::Cons(hd, tl) => {
-                if hd.0 == key {
-                    Option::Some(hd.1)
-                } else if hd.0 > key {
-                    Option::None
-                } else {
-                    Node::lookup_in_bindings(key, tl)
-                }
+    fn lookup_in_bindings(key: Key, mut bindings: &Map<Key, Value>) -> Option<Value> {
+        while let List::Cons(hd, tl) = bindings {
+            if hd.0 == key {
+                return Option::Some(hd.1);
+            } else if hd.0 > key {
+                return Option::None;
+            } else {
+                bindings = tl;
             }
         }
+        Option::None
     }
 
     /// Lookup a value in a list of bindings, and return a borrow to the position
     /// where the value is (or should be inserted, if the key is not in the bindings).
     fn lookup_mut_in_bindings<'a>(
         key: Key,
-        bindings: &'a mut Map<Key, Value>,
+        mut bindings: &'a mut Map<Key, Value>,
     ) -> &'a mut Map<Key, Value> {
-        match bindings {
-            List::Nil => bindings,
-            List::Cons(hd, tl) => {
-                // This requires Polonius
-                if hd.0 >= key {
-                    bindings
-                } else {
-                    Node::lookup_mut_in_bindings(key, tl)
-                }
+        while let List::Cons(hd, tl) = bindings {
+            // This requires Polonius
+            if hd.0 >= key {
+                break;
+            } else {
+                bindings = tl;
             }
         }
+        bindings
     }
 
     /// Filter all the messages which concern [key].
@@ -672,34 +681,28 @@ impl Node {
     /// Note that the stack of messages must start with a message for [key]:
     /// we stop filtering at the first message which is not about [key].
     fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) {
-        match msgs {
-            List::Nil => (),
-            List::Cons((k, _), _) => {
-                if *k == key {
-                    msgs.pop_front();
-                    Node::filter_messages_for_key(key, msgs);
-                } else {
-                    // Stop
-                    ()
-                }
+        while let List::Cons((k, _), _) = msgs {
+            if *k == key {
+                msgs.pop_front();
+            } else {
+                // Stop
+                break;
             }
         }
     }
 
     fn lookup_first_message_after_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons((k, _), next_msgs) => {
-                if *k == key {
-                    Node::lookup_first_message_after_key(key, next_msgs)
-                } else {
-                    msgs
-                }
+        while let List::Cons((k, _), next_msgs) = msgs {
+            if *k == key {
+                msgs = next_msgs;
+            } else {
+                break;
             }
         }
+        return msgs;
     }
 
     /// Returns the value bound to a key.
@@ -788,24 +791,22 @@ impl Node {
     /// of the list).
     fn lookup_first_message_for_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons(x, next_msgs) => {
-                // Rk.: we need Polonius here
-                // We wouldn't need Polonius if directly called the proper
-                // function to make the modifications here (because we wouldn't
-                // need to return anything). However, it would not be very
-                // idiomatic, especially with regards to the fact that we will
-                // rewrite everything with loops at some point.
-                if x.0 >= key {
-                    msgs
-                } else {
-                    Node::lookup_first_message_for_key(key, next_msgs)
-                }
+        while let List::Cons(x, next_msgs) = msgs {
+            // Rk.: we need Polonius here
+            // We wouldn't need Polonius if directly called the proper
+            // function to make the modifications here (because we wouldn't
+            // need to return anything). However, it would not be very
+            // idiomatic, especially with regards to the fact that we will
+            // rewrite everything with loops at some point.
+            if x.0 >= key {
+                return msgs;
+            } else {
+                msgs = next_msgs;
             }
         }
+        msgs
     }
 
     /// Apply the upserts from the current messages stack to a looked up value.
@@ -816,8 +817,8 @@ impl Node {
     /// Note that if there are no more upserts to apply, then the value must be
     /// `Some`. Also note that we use the invariant that in the message stack,
     /// upsert messages are sorted from the first to the last to apply.
-    fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value {
-        if msgs.head_has_key(key) {
+    fn apply_upserts(msgs: &mut Map<Key, Message>, mut prev: Option<Value>, key: Key) -> Value {
+        while msgs.head_has_key(key) {
             // Pop the front message.
             // Note that it *must* be an upsert.
             let msg = msgs.pop_front();
@@ -825,9 +826,8 @@ impl Node {
                 Message::Upsert(s) => {
                     // Apply the update
                     let v = upsert_update(prev, s);
-                    let prev = Option::Some(v);
+                    prev = Option::Some(v);
                     // Continue
-                    Node::apply_upserts(msgs, prev, key)
                 }
                 _ => {
                     // Unreachable: we can only have [Upsert] messages
@@ -835,13 +835,12 @@ impl Node {
                     unreachable!();
                 }
             }
-        } else {
-            // We applied all the upsert messages: simply put an [Insert]
-            // message and return the value.
-            let v = prev.unwrap();
-            msgs.push_front((key, Message::Insert(v)));
-            return v;
         }
+        // We applied all the upsert messages: simply put an [Insert]
+        // message and return the value.
+        let v = prev.unwrap();
+        msgs.push_front((key, Message::Insert(v)));
+        v
     }
 }
 
-- 
cgit v1.2.3


From 0892b943de4de5e34372b91b40580e5bdfe50016 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:48:46 +0200
Subject: Fix a minor issue

---
 compiler/ExtractBase.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 3346c328..bc56dd28 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -850,6 +850,7 @@ let keywords () =
           "assert_norm";
           "assume";
           "else";
+          "end";
           "fun";
           "fn";
           "FStar";
-- 
cgit v1.2.3


From bf3f474ed65fd6ad7a7ca3d5851c990231a857e7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:48:59 +0200
Subject: Update the F* betree

---
 tests/fstar/betree/Betree.Clauses.Template.fst |  65 ++---
 tests/fstar/betree/Betree.Clauses.fst          |  40 ++--
 tests/fstar/betree/Betree.Funs.fst             | 319 +++++++++++++++++--------
 3 files changed, 280 insertions(+), 144 deletions(-)

diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index fad8c5ba..d3e07c7e 100644
--- a/tests/fstar/betree/Betree.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -7,100 +7,109 @@ open Betree.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause
-    Source: 'src/betree.rs', lines 276:4-276:24 *)
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
 unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t)
+  (len : u64) : nat =
+  admit ()
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+unfold
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+  (out : betree_List_t t) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
 unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
-  (n : u64) : nat =
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+  (beg : betree_List_t t) (self : betree_List_t t) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
 unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
-  (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+  (pivot : u64) (beg : betree_List_t (u64 & t))
+  (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
 unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
 unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
 unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 unfold
 let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
 unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
 unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
 unfold
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
 unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
 unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -108,7 +117,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t)
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 unfold
 let betree_Node_apply_messages_decreases (self : betree_Node_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
diff --git a/tests/fstar/betree/Betree.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst
index ae201cee..c50bf421 100644
--- a/tests/fstar/betree/Betree.Clauses.fst
+++ b/tests/fstar/betree/Betree.Clauses.fst
@@ -103,36 +103,46 @@ let wf_nat_pair_lem (p0 p1 : nat_pair) :
 
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) (len : u64) : betree_List_t t =
   self
 
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
 unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
-  (n : u64) : nat =
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+  (out : betree_List_t t) =
+  self
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+unfold
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+  (beg : betree_List_t t) (self : betree_List_t t) : nat =
   n
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
 unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
-  (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+  (pivot : u64) (beg : betree_List_t (u64 & t)) (end0 : betree_List_t (u64 & t))
+  (self : betree_List_t (u64 & t)) =
   self
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : betree_List_t (u64 & betree_Message_t) =
   msgs
@@ -151,29 +161,29 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
 unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index 07f561f5..de3ac13c 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -75,45 +75,76 @@ let betree_upsert_update
     end
   end
 
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
+let rec betree_List_len_loop
+  (t : Type0) (self : betree_List_t t) (len : u64) :
+  Tot (result u64) (decreases (betree_List_len_loop_decreases t self len))
+  =
+  begin match self with
+  | Betree_List_Cons _ tl ->
+    let* len1 = u64_add len 1 in betree_List_len_loop t tl len1
+  | Betree_List_Nil -> Ok len
+  end
+
 (** [betree::betree::{betree::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
-let rec betree_List_len
-  (t : Type0) (self : betree_List_t t) :
-  Tot (result u64) (decreases (betree_List_len_decreases t self))
+let betree_List_len (t : Type0) (self : betree_List_t t) : result u64 =
+  betree_List_len_loop t self 0
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+let rec betree_List_reverse_loop
+  (t : Type0) (self : betree_List_t t) (out : betree_List_t t) :
+  Tot (result (betree_List_t t))
+  (decreases (betree_List_reverse_loop_decreases t self out))
   =
   begin match self with
-  | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i
-  | Betree_List_Nil -> Ok 0
+  | Betree_List_Cons hd tl ->
+    betree_List_reverse_loop t tl (Betree_List_Cons hd out)
+  | Betree_List_Nil -> Ok out
   end
 
-(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
-let rec betree_List_split_at
-  (t : Type0) (self : betree_List_t t) (n : u64) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+    Source: 'src/betree.rs', lines 304:4-304:32 *)
+let betree_List_reverse
+  (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
+  betree_List_reverse_loop t self Betree_List_Nil
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+let rec betree_List_split_at_loop
+  (t : Type0) (n : u64) (beg : betree_List_t t) (self : betree_List_t t) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
-  (decreases (betree_List_split_at_decreases t self n))
+  (decreases (betree_List_split_at_loop_decreases t n beg self))
   =
-  if n = 0
-  then Ok (Betree_List_Nil, self)
-  else
+  if n > 0
+  then
     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
-      Ok (Betree_List_Cons hd ls0, ls1)
+      let* n1 = u64_sub n 1 in
+      betree_List_split_at_loop t n1 (Betree_List_Cons hd beg) tl
     | Betree_List_Nil -> Fail Failure
     end
+  else let* l = betree_List_reverse t beg in Ok (l, self)
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+    Source: 'src/betree.rs', lines 287:4-287:55 *)
+let betree_List_split_at
+  (t : Type0) (self : betree_List_t t) (n : u64) :
+  result ((betree_List_t t) & (betree_List_t t))
+  =
+  betree_List_split_at_loop t n Betree_List_Nil self
 
 (** [betree::betree::{betree::betree::List<T>#1}::push_front]:
-    Source: 'src/betree.rs', lines 299:4-299:34 *)
+    Source: 'src/betree.rs', lines 315:4-315:34 *)
 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
   Ok (Betree_List_Cons x tl)
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
+    Source: 'src/betree.rs', lines 322:4-322:32 *)
 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
@@ -123,7 +154,7 @@ let betree_List_pop_front
   end
 
 (** [betree::betree::{betree::betree::List<T>#1}::hd]:
-    Source: 'src/betree.rs', lines 318:4-318:22 *)
+    Source: 'src/betree.rs', lines 334:4-334:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd _ -> Ok hd
@@ -131,7 +162,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   end
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-    Source: 'src/betree.rs', lines 327:4-327:44 *)
+    Source: 'src/betree.rs', lines 343:4-343:44 *)
 let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
@@ -139,27 +170,43 @@ let betree_ListPairU64T_head_has_key
   | Betree_List_Nil -> Ok false
   end
 
-(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
-let rec betree_ListPairU64T_partition_at_pivot
-  (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
+let rec betree_ListPairU64T_partition_at_pivot_loop
+  (t : Type0) (pivot : u64) (beg : betree_List_t (u64 & t))
+  (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
-  (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot))
+  (decreases (
+    betree_ListPairU64T_partition_at_pivot_loop_decreases t pivot beg end1
+      self))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
     let (i, x) = hd in
     if i >= pivot
-    then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl)
+    then
+      betree_ListPairU64T_partition_at_pivot_loop t pivot beg (Betree_List_Cons
+        (i, x) end1) tl
     else
-      let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
-      let (ls0, ls1) = p in
-      Ok (Betree_List_Cons (i, x) ls0, ls1)
-  | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil)
+      betree_ListPairU64T_partition_at_pivot_loop t pivot (Betree_List_Cons (i,
+        x) beg) end1 tl
+  | Betree_List_Nil ->
+    let* l = betree_List_reverse (u64 & t) beg in
+    let* l1 = betree_List_reverse (u64 & t) end1 in
+    Ok (l, l1)
   end
 
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+    Source: 'src/betree.rs', lines 355:4-355:73 *)
+let betree_ListPairU64T_partition_at_pivot
+  (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
+  result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))
+  =
+  betree_ListPairU64T_partition_at_pivot_loop t pivot Betree_List_Nil
+    Betree_List_Nil self
+
 (** [betree::betree::{betree::betree::Leaf#3}::split]:
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
+    Source: 'src/betree.rs', lines 378:4-383:17 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -179,13 +226,14 @@ let betree_Leaf_split
   Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
     node_id_cnt2))
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-let rec betree_Node_lookup_first_message_for_key
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
+let rec betree_Node_lookup_first_message_for_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
     betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs))
+  (decreases (
+    betree_Node_lookup_first_message_for_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons x next_msgs ->
@@ -193,39 +241,55 @@ let rec betree_Node_lookup_first_message_for_key
     if i >= key
     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 =
+      let* (l, back) =
+        betree_Node_lookup_first_message_for_key_loop key next_msgs in
+      let back1 =
         fun ret ->
-          let* next_msgs1 = lookup_first_message_for_key_back ret in
-          Ok (Betree_List_Cons (i, m) next_msgs1) in
-      Ok (l, back)
+          let* next_msgs1 = back ret in Ok (Betree_List_Cons (i, m) next_msgs1)
+        in
+      Ok (l, back1)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-let rec betree_Node_lookup_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+    Source: 'src/betree.rs', lines 792:4-795:34 *)
+let betree_Node_lookup_first_message_for_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+  =
+  betree_Node_lookup_first_message_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+let rec betree_Node_lookup_in_bindings_loop
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
-  (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
+  (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings))
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
     let (i, i1) = hd in
     if i = key
     then Ok (Some i1)
-    else if i > key then Ok None else betree_Node_lookup_in_bindings key tl
+    else
+      if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl
   | Betree_List_Nil -> Ok None
   end
 
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-let rec betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-649:84 *)
+let betree_Node_lookup_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) =
+  betree_Node_lookup_in_bindings_loop key bindings
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
+let rec betree_Node_apply_upserts_loop
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) :
   Tot (result (u64 & (betree_List_t (u64 & betree_Message_t))))
-  (decreases (betree_Node_apply_upserts_decreases msgs prev key))
+  (decreases (betree_Node_apply_upserts_loop_decreases msgs prev key))
   =
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
@@ -237,7 +301,7 @@ let rec betree_Node_apply_upserts
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts msgs1 (Some v) key
+      betree_Node_apply_upserts_loop msgs1 (Some v) key
     end
   else
     let* v = core_option_Option_unwrap u64 prev in
@@ -246,8 +310,17 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Ok (v, msgs1)
 
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+    Source: 'src/betree.rs', lines 820:4-820:94 *)
+let betree_Node_apply_upserts
+  (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
+  (key : u64) :
+  result (u64 & (betree_List_t (u64 & betree_Message_t)))
+  =
+  betree_Node_apply_upserts_loop msgs prev key
+
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & ((option u64) & betree_Internal_t)))
@@ -262,7 +335,7 @@ let rec betree_Internal_lookup_in_children
     Ok (st1, (o, { self with right = n }))
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]:
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & ((option u64) & betree_Node_t)))
@@ -317,12 +390,12 @@ and betree_Node_lookup
     Ok (st1, (o, Betree_Node_Leaf node))
   end
 
-(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
-let rec betree_Node_filter_messages_for_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
+let rec betree_Node_filter_messages_for_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_filter_messages_for_key_decreases key msgs))
+  (decreases (betree_Node_filter_messages_for_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons p l ->
@@ -332,37 +405,55 @@ let rec betree_Node_filter_messages_for_key
       let* (_, msgs1) =
         betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
           l) in
-      betree_Node_filter_messages_for_key key msgs1
+      betree_Node_filter_messages_for_key_loop key msgs1
     else Ok (Betree_List_Cons (k, m) l)
   | Betree_List_Nil -> Ok Betree_List_Nil
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-let rec betree_Node_lookup_first_message_after_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+    Source: 'src/betree.rs', lines 683:4-683:77 *)
+let betree_Node_filter_messages_for_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & betree_Message_t))
+  =
+  betree_Node_filter_messages_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
+let rec betree_Node_lookup_first_message_after_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
     betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs))
+  (decreases (
+    betree_Node_lookup_first_message_after_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons p next_msgs ->
     let (k, m) = p in
     if k = key
     then
-      let* (l, lookup_first_message_after_key_back) =
-        betree_Node_lookup_first_message_after_key key next_msgs in
-      let back =
+      let* (l, back) =
+        betree_Node_lookup_first_message_after_key_loop key next_msgs in
+      let back1 =
         fun ret ->
-          let* next_msgs1 = lookup_first_message_after_key_back ret in
-          Ok (Betree_List_Cons (k, m) next_msgs1) in
-      Ok (l, back)
+          let* next_msgs1 = back ret in Ok (Betree_List_Cons (k, m) next_msgs1)
+        in
+      Ok (l, back1)
     else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+    Source: 'src/betree.rs', lines 694:4-697:34 *)
+let betree_Node_lookup_first_message_after_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+  =
+  betree_Node_lookup_first_message_after_key_loop key msgs
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-    Source: 'src/betree.rs', lines 521:4-521:89 *)
+    Source: 'src/betree.rs', lines 534:4-534:89 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -421,29 +512,39 @@ let betree_Node_apply_to_internal
       betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
     lookup_first_message_for_key_back msgs2
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
-let rec betree_Node_apply_messages_to_internal
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
+let rec betree_Node_apply_messages_to_internal_loop
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs))
+  (decreases (
+    betree_Node_apply_messages_to_internal_loop_decreases msgs new_msgs))
   =
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     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_Node_apply_messages_to_internal_loop msgs1 new_msgs_tl
   | Betree_List_Nil -> Ok msgs
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-let rec betree_Node_lookup_mut_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+    Source: 'src/betree.rs', lines 518:4-521:5 *)
+let betree_Node_apply_messages_to_internal
+  (msgs : betree_List_t (u64 & betree_Message_t))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & betree_Message_t))
+  =
+  betree_Node_apply_messages_to_internal_loop msgs new_msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
+let rec betree_Node_lookup_mut_in_bindings_loop
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) ->
     result (betree_List_t (u64 & u64)))))
-  (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings))
+  (decreases (betree_Node_lookup_mut_in_bindings_loop_decreases key bindings))
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
@@ -451,18 +552,24 @@ let rec betree_Node_lookup_mut_in_bindings
     if i >= key
     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 =
-        fun ret ->
-          let* tl1 = lookup_mut_in_bindings_back ret in
-          Ok (Betree_List_Cons (i, i1) tl1) in
-      Ok (l, back)
+      let* (l, back) = betree_Node_lookup_mut_in_bindings_loop key tl in
+      let back1 =
+        fun ret -> let* tl1 = back ret in Ok (Betree_List_Cons (i, i1) tl1) in
+      Ok (l, back1)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+    Source: 'src/betree.rs', lines 664:4-667:32 *)
+let betree_Node_lookup_mut_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) :
+  result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> result
+    (betree_List_t (u64 & u64))))
+  =
+  betree_Node_lookup_mut_in_bindings_loop key bindings
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-    Source: 'src/betree.rs', lines 460:4-460:87 *)
+    Source: 'src/betree.rs', lines 476:4-476:87 *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -497,24 +604,34 @@ let betree_Node_apply_to_leaf
       lookup_mut_in_bindings_back bindings2
     end
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
-let rec betree_Node_apply_messages_to_leaf
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
+let rec betree_Node_apply_messages_to_leaf_loop
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & u64)))
-  (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs))
+  (decreases (
+    betree_Node_apply_messages_to_leaf_loop_decreases bindings new_msgs))
   =
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     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_Node_apply_messages_to_leaf_loop bindings1 new_msgs_tl
   | Betree_List_Nil -> Ok bindings
   end
 
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+    Source: 'src/betree.rs', lines 463:4-466:5 *)
+let betree_Node_apply_messages_to_leaf
+  (bindings : betree_List_t (u64 & u64))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & u64))
+  =
+  betree_Node_apply_messages_to_leaf_loop bindings new_msgs
+
 (** [betree::betree::{betree::betree::Internal#4}::flush]:
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -551,7 +668,7 @@ let rec betree_Internal_flush
     Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]:
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -592,7 +709,7 @@ and betree_Node_apply_messages
   end
 
 (** [betree::betree::{betree::betree::Node#5}::apply]:
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
+    Source: 'src/betree.rs', lines 589:4-595:5 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -606,7 +723,7 @@ let betree_Node_apply
   Ok (st1, (self1, node_id_cnt1))
 
 (** [betree::betree::{betree::betree::BeTree#6}::new]:
-    Source: 'src/betree.rs', lines 849:4-849:60 *)
+    Source: 'src/betree.rs', lines 848:4-848:60 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -622,7 +739,7 @@ let betree_BeTree_new
     })
 
 (** [betree::betree::{betree::betree::BeTree#6}::apply]:
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
+    Source: 'src/betree.rs', lines 867:4-867:47 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & betree_BeTree_t)
@@ -633,7 +750,7 @@ let betree_BeTree_apply
   Ok (st1, { self with node_id_cnt = nic; root = n })
 
 (** [betree::betree::{betree::betree::BeTree#6}::insert]:
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
+    Source: 'src/betree.rs', lines 873:4-873:52 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -641,7 +758,7 @@ let betree_BeTree_insert
   betree_BeTree_apply self key (Betree_Message_Insert value) st
 
 (** [betree::betree::{betree::betree::BeTree#6}::delete]:
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
+    Source: 'src/betree.rs', lines 879:4-879:38 *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -649,7 +766,7 @@ let betree_BeTree_delete
   betree_BeTree_apply self key Betree_Message_Delete st
 
 (** [betree::betree::{betree::betree::BeTree#6}::upsert]:
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
+    Source: 'src/betree.rs', lines 885:4-885:59 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -658,7 +775,7 @@ let betree_BeTree_upsert
   betree_BeTree_apply self key (Betree_Message_Upsert upd) st
 
 (** [betree::betree::{betree::betree::BeTree#6}::lookup]:
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
+    Source: 'src/betree.rs', lines 894:4-894:62 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & ((option u64) & betree_BeTree_t))
-- 
cgit v1.2.3


From e6d04cf1a73533ae80a68d9ef5f34a9e832e77a3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:51:24 +0200
Subject: Fix a minor issue

---
 compiler/ExtractBase.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index bc56dd28..4aac270f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -883,6 +883,7 @@ let keywords () =
           "Declare";
           "Definition";
           "else";
+          "end";
           "End";
           "fun";
           "Fixpoint";
-- 
cgit v1.2.3


From a4dd9fe0598328976862868097f59207846d865c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 17:51:36 +0200
Subject: Regenerate the Coq and Lean betrees

---
 tests/coq/betree/Betree_Funs.v | 310 +++++++++++++++++++++++++++++------------
 tests/lean/Betree/Funs.lean    | 291 ++++++++++++++++++++++++++------------
 2 files changed, 423 insertions(+), 178 deletions(-)

diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index b965d423..1c6092ba 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -88,45 +88,85 @@ Definition betree_upsert_update
   end
 .
 
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
+Fixpoint betree_List_len_loop
+  (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match self with
+    | Betree_List_Cons _ tl =>
+      len1 <- u64_add len 1%u64; betree_List_len_loop T n1 tl len1
+    | Betree_List_Nil => Ok len
+    end
+  end
+.
+
 (** [betree::betree::{betree::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
-Fixpoint betree_List_len
+Definition betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
+  betree_List_len_loop T n self 0%u64
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+Fixpoint betree_List_reverse_loop
+  (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
+  result (betree_List_t T)
+  :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
     match self with
-    | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
-    | Betree_List_Nil => Ok 0%u64
+    | Betree_List_Cons hd tl =>
+      betree_List_reverse_loop T n1 tl (Betree_List_Cons hd out)
+    | Betree_List_Nil => Ok out
     end
   end
 .
 
-(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
-Fixpoint betree_List_split_at
-  (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+    Source: 'src/betree.rs', lines 304:4-304:32 *)
+Definition betree_List_reverse
+  (T : Type) (n : nat) (self : betree_List_t T) : result (betree_List_t T) :=
+  betree_List_reverse_loop T n self Betree_List_Nil
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+Fixpoint betree_List_split_at_loop
+  (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T)
+  (self : betree_List_t T) :
   result ((betree_List_t T) * (betree_List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n2 =>
-    if n1 s= 0%u64
-    then Ok (Betree_List_Nil, self)
-    else
+    if n1 s> 0%u64
+    then
       match self with
       | Betree_List_Cons hd tl =>
-        i <- u64_sub n1 1%u64;
-        p <- betree_List_split_at T n2 tl i;
-        let (ls0, ls1) := p in
-        Ok (Betree_List_Cons hd ls0, ls1)
+        n3 <- u64_sub n1 1%u64;
+        betree_List_split_at_loop T n2 n3 (Betree_List_Cons hd beg) tl
       | Betree_List_Nil => Fail_ Failure
       end
+    else (l <- betree_List_reverse T n2 beg; Ok (l, self))
   end
 .
 
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+    Source: 'src/betree.rs', lines 287:4-287:55 *)
+Definition betree_List_split_at
+  (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+  result ((betree_List_t T) * (betree_List_t T))
+  :=
+  betree_List_split_at_loop T n n1 Betree_List_Nil self
+.
+
 (** [betree::betree::{betree::betree::List<T>#1}::push_front]:
-    Source: 'src/betree.rs', lines 299:4-299:34 *)
+    Source: 'src/betree.rs', lines 315:4-315:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
   let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -134,7 +174,7 @@ Definition betree_List_push_front
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
+    Source: 'src/betree.rs', lines 322:4-322:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
   let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -145,7 +185,7 @@ Definition betree_List_pop_front
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::hd]:
-    Source: 'src/betree.rs', lines 318:4-318:22 *)
+    Source: 'src/betree.rs', lines 334:4-334:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
   | Betree_List_Cons hd _ => Ok hd
@@ -154,7 +194,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
 .
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-    Source: 'src/betree.rs', lines 327:4-327:44 *)
+    Source: 'src/betree.rs', lines 343:4-343:44 *)
 Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
@@ -163,10 +203,11 @@ Definition betree_ListPairU64T_head_has_key
   end
 .
 
-(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
-Fixpoint betree_ListPairU64T_partition_at_pivot
-  (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
+Fixpoint betree_ListPairU64T_partition_at_pivot_loop
+  (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T))
+  (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) :
   result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
   :=
   match n with
@@ -176,18 +217,32 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
     | Betree_List_Cons hd tl =>
       let (i, t) := hd in
       if i s>= pivot
-      then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl)
-      else (
-        p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
-        let (ls0, ls1) := p in
-        Ok (Betree_List_Cons (i, t) ls0, ls1))
-    | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
+      then
+        betree_ListPairU64T_partition_at_pivot_loop T n1 pivot beg
+          (Betree_List_Cons (i, t) end1) tl
+      else
+        betree_ListPairU64T_partition_at_pivot_loop T n1 pivot
+          (Betree_List_Cons (i, t) beg) end1 tl
+    | Betree_List_Nil =>
+      l <- betree_List_reverse (u64 * T) n1 beg;
+      l1 <- betree_List_reverse (u64 * T) n1 end1;
+      Ok (l, l1)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+    Source: 'src/betree.rs', lines 355:4-355:73 *)
+Definition betree_ListPairU64T_partition_at_pivot
+  (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+  result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
+  :=
+  betree_ListPairU64T_partition_at_pivot_loop T n pivot Betree_List_Nil
+    Betree_List_Nil self
+.
+
 (** [betree::betree::{betree::betree::Leaf#3}::split]:
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
+    Source: 'src/betree.rs', lines 378:4-383:17 *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -222,9 +277,9 @@ Definition betree_Leaf_split
     node_id_cnt2))
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-Fixpoint betree_Node_lookup_first_message_for_key
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
+Fixpoint betree_Node_lookup_first_message_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
     betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -238,21 +293,30 @@ Fixpoint betree_Node_lookup_first_message_for_key
       if i s>= key
       then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
       else (
-        p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
-        let (l, lookup_first_message_for_key_back) := p in
-        let back :=
+        p <- betree_Node_lookup_first_message_for_key_loop n1 key next_msgs;
+        let (l, back) := p in
+        let back1 :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
-            next_msgs1 <- lookup_first_message_for_key_back ret;
-            Ok (Betree_List_Cons (i, m) next_msgs1) in
-        Ok (l, back))
+            next_msgs1 <- back ret; Ok (Betree_List_Cons (i, m) next_msgs1) in
+        Ok (l, back1))
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-Fixpoint betree_Node_lookup_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+    Source: 'src/betree.rs', lines 792:4-795:34 *)
+Definition betree_Node_lookup_first_message_for_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+  :=
+  betree_Node_lookup_first_message_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+Fixpoint betree_Node_lookup_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
   :=
@@ -265,15 +329,26 @@ Fixpoint betree_Node_lookup_in_bindings
       if i s= key
       then Ok (Some i1)
       else
-        if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+        if i s> key
+        then Ok None
+        else betree_Node_lookup_in_bindings_loop n1 key tl
     | Betree_List_Nil => Ok None
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-Fixpoint betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-649:84 *)
+Definition betree_Node_lookup_in_bindings
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result (option u64)
+  :=
+  betree_Node_lookup_in_bindings_loop n key bindings
+.
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
+Fixpoint betree_Node_apply_upserts_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) :
   result (u64 * (betree_List_t (u64 * betree_Message_t)))
@@ -292,7 +367,7 @@ Fixpoint betree_Node_apply_upserts
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        betree_Node_apply_upserts n1 msgs1 (Some v) key
+        betree_Node_apply_upserts_loop n1 msgs1 (Some v) key
       end)
     else (
       v <- core_option_Option_unwrap u64 prev;
@@ -303,8 +378,18 @@ Fixpoint betree_Node_apply_upserts
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+    Source: 'src/betree.rs', lines 820:4-820:94 *)
+Definition betree_Node_apply_upserts
+  (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
+  (key : u64) :
+  result (u64 * (betree_List_t (u64 * betree_Message_t)))
+  :=
+  betree_Node_apply_upserts_loop n msgs prev key
+.
+
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_Internal_t))
@@ -328,7 +413,7 @@ Fixpoint betree_Internal_lookup_in_children
   end
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]:
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_Node_t))
@@ -394,9 +479,9 @@ with betree_Node_lookup
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
-Fixpoint betree_Node_filter_messages_for_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
+Fixpoint betree_Node_filter_messages_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
   :=
@@ -412,16 +497,25 @@ Fixpoint betree_Node_filter_messages_for_key
           betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
             m) l);
         let (_, msgs1) := p1 in
-        betree_Node_filter_messages_for_key n1 key msgs1)
+        betree_Node_filter_messages_for_key_loop n1 key msgs1)
       else Ok (Betree_List_Cons (k, m) l)
     | Betree_List_Nil => Ok Betree_List_Nil
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-Fixpoint betree_Node_lookup_first_message_after_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+    Source: 'src/betree.rs', lines 683:4-683:77 *)
+Definition betree_Node_filter_messages_for_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * betree_Message_t))
+  :=
+  betree_Node_filter_messages_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
+Fixpoint betree_Node_lookup_first_message_after_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
     betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -434,21 +528,30 @@ Fixpoint betree_Node_lookup_first_message_after_key
       let (k, m) := p in
       if k s= key
       then (
-        p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
-        let (l, lookup_first_message_after_key_back) := p1 in
-        let back :=
+        p1 <- betree_Node_lookup_first_message_after_key_loop n1 key next_msgs;
+        let (l, back) := p1 in
+        let back1 :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
-            next_msgs1 <- lookup_first_message_after_key_back ret;
-            Ok (Betree_List_Cons (k, m) next_msgs1) in
-        Ok (l, back))
+            next_msgs1 <- back ret; Ok (Betree_List_Cons (k, m) next_msgs1) in
+        Ok (l, back1))
       else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+    Source: 'src/betree.rs', lines 694:4-697:34 *)
+Definition betree_Node_lookup_first_message_after_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+  :=
+  betree_Node_lookup_first_message_after_key_loop n key msgs
+.
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-    Source: 'src/betree.rs', lines 521:4-521:89 *)
+    Source: 'src/betree.rs', lines 534:4-534:89 *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -508,9 +611,9 @@ Definition betree_Node_apply_to_internal
     lookup_first_message_for_key_back msgs2)
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
-Fixpoint betree_Node_apply_messages_to_internal
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
+Fixpoint betree_Node_apply_messages_to_internal_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -522,15 +625,25 @@ Fixpoint betree_Node_apply_messages_to_internal
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
-      betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
+      betree_Node_apply_messages_to_internal_loop n1 msgs1 new_msgs_tl
     | Betree_List_Nil => Ok msgs
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-Fixpoint betree_Node_lookup_mut_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+    Source: 'src/betree.rs', lines 518:4-521:5 *)
+Definition betree_Node_apply_messages_to_internal
+  (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
+  (new_msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * betree_Message_t))
+  :=
+  betree_Node_apply_messages_to_internal_loop n msgs new_msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
+Fixpoint betree_Node_lookup_mut_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
     (betree_List_t (u64 * u64))))
@@ -544,20 +657,29 @@ Fixpoint betree_Node_lookup_mut_in_bindings
       if i s>= key
       then Ok (Betree_List_Cons (i, i1) tl, Ok)
       else (
-        p <- betree_Node_lookup_mut_in_bindings n1 key tl;
-        let (l, lookup_mut_in_bindings_back) := p in
-        let back :=
+        p <- betree_Node_lookup_mut_in_bindings_loop n1 key tl;
+        let (l, back) := p in
+        let back1 :=
           fun (ret : betree_List_t (u64 * u64)) =>
-            tl1 <- lookup_mut_in_bindings_back ret;
-            Ok (Betree_List_Cons (i, i1) tl1) in
-        Ok (l, back))
+            tl1 <- back ret; Ok (Betree_List_Cons (i, i1) tl1) in
+        Ok (l, back1))
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+    Source: 'src/betree.rs', lines 664:4-667:32 *)
+Definition betree_Node_lookup_mut_in_bindings
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
+    (betree_List_t (u64 * u64))))
+  :=
+  betree_Node_lookup_mut_in_bindings_loop n key bindings
+.
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-    Source: 'src/betree.rs', lines 460:4-460:87 *)
+    Source: 'src/betree.rs', lines 476:4-476:87 *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -594,9 +716,9 @@ Definition betree_Node_apply_to_leaf
     end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
-Fixpoint betree_Node_apply_messages_to_leaf
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
+Fixpoint betree_Node_apply_messages_to_leaf_loop
   (n : nat) (bindings : betree_List_t (u64 * u64))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * u64))
@@ -608,14 +730,24 @@ Fixpoint betree_Node_apply_messages_to_leaf
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
-      betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
+      betree_Node_apply_messages_to_leaf_loop n1 bindings1 new_msgs_tl
     | Betree_List_Nil => Ok bindings
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+    Source: 'src/betree.rs', lines 463:4-466:5 *)
+Definition betree_Node_apply_messages_to_leaf
+  (n : nat) (bindings : betree_List_t (u64 * u64))
+  (new_msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * u64))
+  :=
+  betree_Node_apply_messages_to_leaf_loop n bindings new_msgs
+.
+
 (** [betree::betree::{betree::betree::Internal#4}::flush]:
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -665,7 +797,7 @@ Fixpoint betree_Internal_flush
   end
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]:
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -721,7 +853,7 @@ with betree_Node_apply_messages
 .
 
 (** [betree::betree::{betree::betree::Node#5}::apply]:
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
+    Source: 'src/betree.rs', lines 589:4-595:5 *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -737,7 +869,7 @@ Definition betree_Node_apply
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::new]:
-    Source: 'src/betree.rs', lines 849:4-849:60 *)
+    Source: 'src/betree.rs', lines 848:4-848:60 *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -762,7 +894,7 @@ Definition betree_BeTree_new
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::apply]:
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
+    Source: 'src/betree.rs', lines 867:4-867:47 *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -782,7 +914,7 @@ Definition betree_BeTree_apply
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::insert]:
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
+    Source: 'src/betree.rs', lines 873:4-873:52 *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -791,7 +923,7 @@ Definition betree_BeTree_insert
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::delete]:
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
+    Source: 'src/betree.rs', lines 879:4-879:38 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -800,7 +932,7 @@ Definition betree_BeTree_delete
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::upsert]:
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
+    Source: 'src/betree.rs', lines 885:4-885:59 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -810,7 +942,7 @@ Definition betree_BeTree_upsert
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::lookup]:
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
+    Source: 'src/betree.rs', lines 894:4-894:62 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_BeTree_t))
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 8612ccbc..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -79,42 +79,74 @@ def betree.upsert_update
       then prev1 - v
       else Result.ok 0#u64
 
+/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+   Source: 'src/betree.rs', lines 276:4-284:5 -/
+divergent def betree.List.len_loop
+  (T : Type) (self : betree.List T) (len : U64) : Result U64 :=
+  match self with
+  | betree.List.Cons _ tl =>
+    do
+    let len1 ← len + 1#u64
+    betree.List.len_loop T tl len1
+  | betree.List.Nil => Result.ok len
+
 /- [betree::betree::{betree::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
-divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+  betree.List.len_loop T self 0#u64
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+   Source: 'src/betree.rs', lines 304:4-312:5 -/
+divergent def betree.List.reverse_loop
+  (T : Type) (self : betree.List T) (out : betree.List T) :
+  Result (betree.List T)
+  :=
   match self with
-  | betree.List.Cons _ tl => do
-                             let i ← betree.List.len T tl
-                             1#u64 + i
-  | betree.List.Nil => Result.ok 0#u64
-
-/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
-   Source: 'src/betree.rs', lines 284:4-284:51 -/
-divergent def betree.List.split_at
-  (T : Type) (self : betree.List T) (n : U64) :
+  | betree.List.Cons hd tl =>
+    betree.List.reverse_loop T tl (betree.List.Cons hd out)
+  | betree.List.Nil => Result.ok out
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]:
+   Source: 'src/betree.rs', lines 304:4-304:32 -/
+def betree.List.reverse
+  (T : Type) (self : betree.List T) : Result (betree.List T) :=
+  betree.List.reverse_loop T self betree.List.Nil
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+   Source: 'src/betree.rs', lines 287:4-302:5 -/
+divergent def betree.List.split_at_loop
+  (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n = 0#u64
-  then Result.ok (betree.List.Nil, self)
-  else
+  if n > 0#u64
+  then
     match self with
     | betree.List.Cons hd tl =>
       do
-      let i ← n - 1#u64
-      let p ← betree.List.split_at T tl i
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons hd ls0, ls1)
+      let n1 ← n - 1#u64
+      betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
     | betree.List.Nil => Result.fail .panic
+  else do
+       let l ← betree.List.reverse T beg
+       Result.ok (l, self)
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
+   Source: 'src/betree.rs', lines 287:4-287:55 -/
+def betree.List.split_at
+  (T : Type) (self : betree.List T) (n : U64) :
+  Result ((betree.List T) × (betree.List T))
+  :=
+  betree.List.split_at_loop T n betree.List.Nil self
 
 /- [betree::betree::{betree::betree::List<T>#1}::push_front]:
-   Source: 'src/betree.rs', lines 299:4-299:34 -/
+   Source: 'src/betree.rs', lines 315:4-315:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
   Result.ok (betree.List.Cons x tl)
 
 /- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-   Source: 'src/betree.rs', lines 306:4-306:32 -/
+   Source: 'src/betree.rs', lines 322:4-322:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
   let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
@@ -123,14 +155,14 @@ def betree.List.pop_front
   | betree.List.Nil => Result.fail .panic
 
 /- [betree::betree::{betree::betree::List<T>#1}::hd]:
-   Source: 'src/betree.rs', lines 318:4-318:22 -/
+   Source: 'src/betree.rs', lines 334:4-334:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
 /- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-   Source: 'src/betree.rs', lines 327:4-327:44 -/
+   Source: 'src/betree.rs', lines 343:4-343:44 -/
 def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
@@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key
                              Result.ok (i = key)
   | betree.List.Nil => Result.ok false
 
-/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-   Source: 'src/betree.rs', lines 339:4-339:73 -/
-divergent def betree.ListPairU64T.partition_at_pivot
-  (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+   Source: 'src/betree.rs', lines 355:4-370:5 -/
+divergent def betree.ListPairU64T.partition_at_pivot_loop
+  (T : Type) (pivot : U64) (beg : betree.List (U64 × T))
+  (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
   match self with
   | betree.List.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
-    then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
+    then
+      betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons
+        (i, t) end1) tl
     else
-      do
-      let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons (i, t) ls0, ls1)
-  | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
+      betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i,
+        t) beg) end1 tl
+  | betree.List.Nil =>
+    do
+    let l ← betree.List.reverse (U64 × T) beg
+    let l1 ← betree.List.reverse (U64 × T) end1
+    Result.ok (l, l1)
+
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+   Source: 'src/betree.rs', lines 355:4-355:73 -/
+def betree.ListPairU64T.partition_at_pivot
+  (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+  Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
+  :=
+  betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil
+    betree.List.Nil self
 
 /- [betree::betree::{betree::betree::Leaf#3}::split]:
-   Source: 'src/betree.rs', lines 359:4-364:17 -/
+   Source: 'src/betree.rs', lines 378:4-383:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -176,9 +222,9 @@ def betree.Leaf.split
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
   Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-   Source: 'src/betree.rs', lines 789:4-792:34 -/
-divergent def betree.Node.lookup_first_message_for_key
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 792:4-810:5 -/
+divergent def betree.Node.lookup_first_message_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key
     then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
     else
       do
-      let (l, lookup_first_message_for_key_back) ←
-        betree.Node.lookup_first_message_for_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_for_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_for_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (i, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-   Source: 'src/betree.rs', lines 636:4-636:80 -/
-divergent def betree.Node.lookup_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+   Source: 'src/betree.rs', lines 792:4-795:34 -/
+def betree.Node.lookup_first_message_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 649:4-660:5 -/
+divergent def betree.Node.lookup_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   match bindings with
   | betree.List.Cons hd tl =>
@@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings
     else
       if i > key
       then Result.ok none
-      else betree.Node.lookup_in_bindings key tl
+      else betree.Node.lookup_in_bindings_loop key tl
   | betree.List.Nil => Result.ok none
 
-/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-   Source: 'src/betree.rs', lines 819:4-819:90 -/
-divergent def betree.Node.apply_upserts
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+   Source: 'src/betree.rs', lines 649:4-649:84 -/
+def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  betree.Node.lookup_in_bindings_loop key bindings
+
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+   Source: 'src/betree.rs', lines 820:4-844:5 -/
+divergent def betree.Node.apply_upserts_loop
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   :
   Result (U64 × (betree.List (U64 × betree.Message)))
@@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts msgs1 (some v) key
+      betree.Node.apply_upserts_loop msgs1 (some v) key
   else
     do
     let v ← core.option.Option.unwrap U64 prev
@@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts
         betree.Message.Insert v)
     Result.ok (v, msgs1)
 
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+   Source: 'src/betree.rs', lines 820:4-820:94 -/
+def betree.Node.apply_upserts
+  (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
+  :
+  Result (U64 × (betree.List (U64 × betree.Message)))
+  :=
+  betree.Node.apply_upserts_loop msgs prev key
+
 /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-   Source: 'src/betree.rs', lines 395:4-395:63 -/
+   Source: 'src/betree.rs', lines 414:4-414:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
@@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children
     Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
 /- [betree::betree::{betree::betree::Node#5}::lookup]:
-   Source: 'src/betree.rs', lines 709:4-709:58 -/
+   Source: 'src/betree.rs', lines 712:4-712:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Node))
@@ -320,9 +390,9 @@ divergent def betree.Node.lookup
 
 end
 
-/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-   Source: 'src/betree.rs', lines 674:4-674:77 -/
-divergent def betree.Node.filter_messages_for_key
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 683:4-692:5 -/
+divergent def betree.Node.filter_messages_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
@@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key
       let (_, msgs1) ←
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
-      betree.Node.filter_messages_for_key key msgs1
+      betree.Node.filter_messages_for_key_loop key msgs1
     else Result.ok (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ok betree.List.Nil
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-   Source: 'src/betree.rs', lines 689:4-692:34 -/
-divergent def betree.Node.lookup_first_message_after_key
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+   Source: 'src/betree.rs', lines 683:4-683:77 -/
+def betree.Node.filter_messages_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.filter_messages_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+   Source: 'src/betree.rs', lines 694:4-706:5 -/
+divergent def betree.Node.lookup_first_message_after_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key
     if k = key
     then
       do
-      let (l, lookup_first_message_after_key_back) ←
-        betree.Node.lookup_first_message_after_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_after_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_after_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (k, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
     else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+   Source: 'src/betree.rs', lines 694:4-697:34 -/
+def betree.Node.lookup_first_message_after_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_after_key_loop key msgs
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-   Source: 'src/betree.rs', lines 521:4-521:89 -/
+   Source: 'src/betree.rs', lines 534:4-534:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
   (new_msg : betree.Message) :
@@ -427,9 +514,9 @@ def betree.Node.apply_to_internal
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
     lookup_first_message_for_key_back msgs2
 
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-   Source: 'src/betree.rs', lines 502:4-505:5 -/
-divergent def betree.Node.apply_messages_to_internal
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+   Source: 'src/betree.rs', lines 518:4-526:5 -/
+divergent def betree.Node.apply_messages_to_internal_loop
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal
     do
     let (i, m) := new_msg
     let msgs1 ← betree.Node.apply_to_internal msgs i m
-    betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
+    betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl
   | betree.List.Nil => Result.ok msgs
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-   Source: 'src/betree.rs', lines 653:4-656:32 -/
-divergent def betree.Node.lookup_mut_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+   Source: 'src/betree.rs', lines 518:4-521:5 -/
+def betree.Node.apply_messages_to_internal
+  (msgs : betree.List (U64 × betree.Message))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.apply_messages_to_internal_loop msgs new_msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 664:4-677:5 -/
+divergent def betree.Node.lookup_mut_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
     (betree.List (U64 × U64))))
@@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings
     then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
     else
       do
-      let (l, lookup_mut_in_bindings_back) ←
-        betree.Node.lookup_mut_in_bindings key tl
-      let back :=
+      let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← lookup_mut_in_bindings_back ret
+          let tl1 ← back ret
           Result.ok (betree.List.Cons (i, i1) tl1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+   Source: 'src/betree.rs', lines 664:4-667:32 -/
+def betree.Node.lookup_mut_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) :
+  Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
+    (betree.List (U64 × U64))))
+  :=
+  betree.Node.lookup_mut_in_bindings_loop key bindings
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-   Source: 'src/betree.rs', lines 460:4-460:87 -/
+   Source: 'src/betree.rs', lines 476:4-476:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
   :
@@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf
       let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
       lookup_mut_in_bindings_back bindings2
 
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-   Source: 'src/betree.rs', lines 444:4-447:5 -/
-divergent def betree.Node.apply_messages_to_leaf
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+   Source: 'src/betree.rs', lines 463:4-471:5 -/
+divergent def betree.Node.apply_messages_to_leaf_loop
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × U64))
@@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf
     do
     let (i, m) := new_msg
     let bindings1 ← betree.Node.apply_to_leaf bindings i m
-    betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
+    betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl
   | betree.List.Nil => Result.ok bindings
 
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+   Source: 'src/betree.rs', lines 463:4-466:5 -/
+def betree.Node.apply_messages_to_leaf
+  (bindings : betree.List (U64 × U64))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × U64))
+  :=
+  betree.Node.apply_messages_to_leaf_loop bindings new_msgs
+
 /- [betree::betree::{betree::betree::Internal#4}::flush]:
-   Source: 'src/betree.rs', lines 410:4-415:26 -/
+   Source: 'src/betree.rs', lines 429:4-434:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush
       self.left n, node_id_cnt1)))
 
 /- [betree::betree::{betree::betree::Node#5}::apply_messages]:
-   Source: 'src/betree.rs', lines 588:4-593:5 -/
+   Source: 'src/betree.rs', lines 601:4-606:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages
 end
 
 /- [betree::betree::{betree::betree::Node#5}::apply]:
-   Source: 'src/betree.rs', lines 576:4-582:5 -/
+   Source: 'src/betree.rs', lines 589:4-595:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -625,7 +738,7 @@ def betree.Node.apply
   Result.ok (st1, (self1, node_id_cnt1))
 
 /- [betree::betree::{betree::betree::BeTree#6}::new]:
-   Source: 'src/betree.rs', lines 849:4-849:60 -/
+   Source: 'src/betree.rs', lines 848:4-848:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -642,7 +755,7 @@ def betree.BeTree.new
     })
 
 /- [betree::betree::{betree::betree::BeTree#6}::apply]:
-   Source: 'src/betree.rs', lines 868:4-868:47 -/
+   Source: 'src/betree.rs', lines 867:4-867:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × betree.BeTree)
@@ -654,7 +767,7 @@ def betree.BeTree.apply
   Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
 /- [betree::betree::{betree::betree::BeTree#6}::insert]:
-   Source: 'src/betree.rs', lines 874:4-874:52 -/
+   Source: 'src/betree.rs', lines 873:4-873:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -662,7 +775,7 @@ def betree.BeTree.insert
   betree.BeTree.apply self key (betree.Message.Insert value) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::delete]:
-   Source: 'src/betree.rs', lines 880:4-880:38 -/
+   Source: 'src/betree.rs', lines 879:4-879:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -670,7 +783,7 @@ def betree.BeTree.delete
   betree.BeTree.apply self key betree.Message.Delete st
 
 /- [betree::betree::{betree::betree::BeTree#6}::upsert]:
-   Source: 'src/betree.rs', lines 886:4-886:59 -/
+   Source: 'src/betree.rs', lines 885:4-885:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -679,7 +792,7 @@ def betree.BeTree.upsert
   betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::lookup]:
-   Source: 'src/betree.rs', lines 895:4-895:62 -/
+   Source: 'src/betree.rs', lines 894:4-894:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.BeTree))
-- 
cgit v1.2.3