From 0c814c97dd8e5167f24b0dbb14186d674e4d097b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 11:44:58 +0100
Subject: Update Pure.fun_sig_info

---
 compiler/Translate.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 221d4e73..54e24066 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -216,11 +216,15 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
         (* We need to ignore the forward inputs, and the state input (if there is) *)
         let backward_inputs =
           let sg = backward_sg.sg in
+          (* TODO: *)
+          assert (not !Config.return_back_funs);
           (* We need to ignore the forward state and the backward state *)
           let num_forward_inputs =
-            sg.info.num_fwd_inputs_with_fuel_with_state
+            sg.info.fwd_info.num_inputs_with_fuel_with_state
+          in
+          let num_back_inputs =
+            (Option.get sg.info.back_info).num_inputs_no_fuel_no_state
           in
-          let num_back_inputs = Option.get sg.info.num_back_inputs_no_state in
           Collections.List.subslice sg.inputs num_forward_inputs
             (num_forward_inputs + num_back_inputs)
         in
-- 
cgit v1.3.1


From f1f41818fb14a6c46442ca42a49a3aab0a5b1aaf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Dec 2023 17:48:44 +0100
Subject: Make progress on generated merged fwd/back functions

---
 compiler/SymbolicToPure.ml | 56 ++++++++++++++++++++++++----------------------
 compiler/Translate.ml      |  4 +++-
 2 files changed, 32 insertions(+), 28 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1fd4896e..86c80f87 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -958,19 +958,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   (* Compute the additinal inputs for the current function, if it is a backward
    * function *)
   let back_inputs =
-    match gid with
-    | None -> []
-    | Some gid ->
-        (* For now, we don't allow nested borrows, so the additional inputs to the
-           backward function can only come from borrows that were returned like
-           in (for the backward function we introduce for 'a):
-           {[
-             fn f<'a>(...) -> &'a mut u32;
-           ]}
-           Upon ending the abstraction for 'a, we need to get back the borrow
-           the function returned.
-        *)
-        List.filter_map (translate_back_ty_for_gid gid) [ sg.output ]
+    match gid with None -> [] | Some gid -> translate_back_inputs_for_gid gid
   in
   (* If the function is stateful, the inputs are:
      - forward:  [fwd_ty0, ..., fwd_tyn, state]
@@ -989,11 +977,12 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
        See {!effect_info}. *)
     if effect_info.stateful_group then [ mk_state_ty ] else []
   in
-  let back_state_ty =
+  let mk_back_state_ty_for_gid (gid : RegionGroupId.id option) : ty list =
     (* For the backward state, we check if the function is a backward function,
        and it is stateful *)
     if effect_info.stateful && Option.is_some gid then [ mk_state_ty ] else []
   in
+  let back_state_ty = mk_back_state_ty_for_gid gid in
 
   (* Concatenate the inputs, in the following order:
    * - forward inputs
@@ -1072,22 +1061,35 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
         num_fwd_inputs_with_fuel_no_state + List.length fwd_state_ty;
     }
   in
+  let compute_back_info (back_state_ty : ty list)
+      (num_back_inputs_no_state : int) : inputs_info =
+    let n = num_back_inputs_no_state in
+    (* Note that backward functions never use fuel *)
+    {
+      has_fuel = false;
+      num_inputs_no_fuel_no_state = n;
+      num_inputs_with_fuel_no_state = n;
+      (* Length of [back_state_ty]: similar trick as for [fwd_state_ty] *)
+      num_inputs_with_fuel_with_state = n + List.length back_state_ty;
+    }
+  in
   let back_info : back_inputs_info =
     if !Config.return_back_funs then
+      (* Create the map *)
+      AllBacks
+        (RegionGroupId.Map.of_list
+           (List.map
+              (fun (rg : T.region_var_group) ->
+                ( rg.id,
+                  let back_inputs = translate_back_inputs_for_gid rg.id in
+                  let num_back_inputs = List.length back_inputs in
+                  (* TODO: slightly overkill *)
+                  let back_state_ty = mk_back_state_ty_for_gid (Some rg.id) in
+                  compute_back_info back_state_ty num_back_inputs ))
+              regions_hierarchy))
+    else
       SingleBack
-        (Option.map
-           (fun n ->
-             (* Note that backward functions never use fuel *)
-             {
-               has_fuel = false;
-               num_inputs_no_fuel_no_state = n;
-               num_inputs_with_fuel_no_state = n;
-               (* Length of [back_state_ty]: similar trick as for [fwd_state_ty] *)
-               num_inputs_with_fuel_with_state = n + List.length back_state_ty;
-             })
-           num_back_inputs_no_state)
-    else (* Create the map *)
-      failwith "TODO"
+        (Option.map (compute_back_info back_state_ty) num_back_inputs_no_state)
   in
   let info = { fwd_info; back_info; effect_info } in
   assert (fun_sig_info_is_wf info);
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 54e24066..06d4bd6d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -223,7 +223,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
             sg.info.fwd_info.num_inputs_with_fuel_with_state
           in
           let num_back_inputs =
-            (Option.get sg.info.back_info).num_inputs_no_fuel_no_state
+            match sg.info.back_info with
+            | SingleBack (Some info) -> info.num_inputs_no_fuel_no_state
+            | _ -> raise (Failure "Unexpected")
           in
           Collections.List.subslice sg.inputs num_forward_inputs
             (num_forward_inputs + num_back_inputs)
-- 
cgit v1.3.1


From 884edaa3ee975626f184249d491f343fc02a66e2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 18:54:06 +0100
Subject: Make progress on updating the code

---
 compiler/PureMicroPasses.ml |  48 ++++++----
 compiler/SymbolicToPure.ml  |  79 +++--------------
 compiler/Translate.ml       | 207 ++++++++++++++++++++------------------------
 3 files changed, 134 insertions(+), 200 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 0102b13e..a7c2f154 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -776,9 +776,11 @@ let inline_useless_var_reassignments (ctx : trans_ctx) (inline_named : bool)
       in
       { def with body = Some body }
 
-(** Given a forward or backward function call, is there, for every execution
+(** For the cases where we split the forward/backward functions.
+
+    Given a forward or backward function call, is there, for every execution
     path, a child backward function called later with exactly the same input
-    list prefix? We use this to filter useless function calls: if there are
+    list prefix. We use this to filter useless function calls: if there are
     such child calls, we can remove this one (in case its outputs are not
     used).
     We do this check because we can't simply remove function calls whose
@@ -1008,17 +1010,21 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
                  * under some conditions. *)
                 match (filter_monadic_calls, opt_destruct_function_call re) with
                 | true, Some (Fun (FromLlbc (fid, lp_id, rg_id)), tys, args) ->
-                    (* We need to check if there is a child call - see
-                     * the comments for:
-                     * [expression_contains_child_call_in_all_paths] *)
-                    let has_child_call =
-                      expression_contains_child_call_in_all_paths ctx fid lp_id
-                        rg_id tys args e
-                    in
-                    if has_child_call then (* Filter *)
-                      (e.e, fun _ -> used)
-                    else (* No child call: don't filter *)
-                      dont_filter ()
+                    (* If we split the forward/backward functions.
+
+                       We need to check if there is a child call - see
+                       the comments for:
+                       [expression_contains_child_call_in_all_paths] *)
+                    if not !Config.return_back_funs then
+                      let has_child_call =
+                        expression_contains_child_call_in_all_paths ctx fid
+                          lp_id rg_id tys args e
+                      in
+                      if has_child_call then (* Filter *)
+                        (e.e, fun _ -> used)
+                      else (* No child call: don't filter *)
+                        dont_filter ()
+                    else dont_filter ()
                 | _ ->
                     (* Not an LLBC function call or not allowed to filter: we can't filter *)
                     dont_filter ()
@@ -1509,9 +1515,12 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
     altogether.
   *)
 let keep_forward (fwd : fun_and_loops) (backs : fun_and_loops list) : bool =
-  (* Note that at this point, the output types are no longer seen as tuples:
-   * they should be lists of length 1. *)
-  if
+  (* The question of filtering the forward functions arises only if we split
+     the forward/backward functions *)
+  if !Config.return_back_funs then true
+  else if
+    (* Note that at this point, the output types are no longer seen as tuples:
+     * they should be lists of length 1. *)
     !Config.filter_useless_functions
     && fwd.f.signature.output = mk_result_ty mk_unit_ty
     && backs <> []
@@ -1957,9 +1966,10 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
   log#ldebug (lazy ("remove_meta:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
   (* Remove the backward functions with no outputs.
-   * Note that the calls to those functions should already have been removed,
-   * when translating from symbolic to pure. Here, we remove the definitions
-   * altogether, because they are now useless *)
+
+     Note that the *calls* to those functions should already have been removed,
+     when translating from symbolic to pure. Here, we remove the definitions
+     altogether, because they are now useless *)
   let name = def.name ^ PrintPure.fun_suffix def.loop_id def.back_id in
   let opt_def = filter_if_backward_with_no_outputs def in
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 08f9e950..204fc399 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -45,7 +45,6 @@ type fun_sig_named_outputs = {
 
 type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
-  fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t;  (** *)
   fun_infos : fun_info A.FunDeclId.Map.t;
   regions_hierarchies : T.region_var_groups FunIdMap.t;
 }
@@ -144,7 +143,11 @@ type bs_ctx = {
           a symbolic expansion or upon ending an abstraction, for instance)
           we introduce a new variable (with a let-binding).
        *)
-  var_counter : VarId.generator;
+  var_counter : VarId.generator ref;
+      (** Using a ref to make sure all the variables identifiers are unique.
+          TODO: this is not very clean, and the code was initially written without
+          a reference (and it's shape hasn't changed). We should use DeBruijn indices.
+       *)
   state_var : VarId.id;
       (** The current state variable, in case the function is stateful *)
   back_state_vars : VarId.id RegionGroupId.Map.t;
@@ -1131,13 +1134,14 @@ let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern =
   (* Generate the fresh variable *)
-  let id, var_counter = VarId.fresh ctx.var_counter in
+  let id, var_counter = VarId.fresh !(ctx.var_counter) in
   let state_var =
     { id; basename = Some ConstStrings.state_basename; ty = mk_state_ty }
   in
   let state_pat = mk_typed_pattern_from_var state_var None in
   (* Update the context *)
-  let ctx = { ctx with var_counter; state_var = id } in
+  ctx.var_counter := var_counter;
+  let ctx = { ctx with state_var = id } in
   (* Return *)
   (ctx, state_var, state_pat)
 
@@ -1146,11 +1150,11 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern =
 let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) :
     bs_ctx * var =
   (* Generate the fresh variable *)
-  let id, var_counter = VarId.fresh ctx.var_counter in
+  let id, var_counter = VarId.fresh !(ctx.var_counter) in
   let ty = ctx_translate_fwd_ty ctx ty in
   let var = { id; basename; ty } in
   (* Update the context *)
-  let ctx = { ctx with var_counter } in
+  ctx.var_counter := var_counter;
   (* Return *)
   (ctx, var)
 
@@ -1184,10 +1188,10 @@ let fresh_named_vars_for_symbolic_values
 let fresh_var (basename : string option) (ty : ty) (ctx : bs_ctx) : bs_ctx * var
     =
   (* Generate the fresh variable *)
-  let id, var_counter = VarId.fresh ctx.var_counter in
+  let id, var_counter = VarId.fresh !(ctx.var_counter) in
   let var = { id; basename; ty } in
   (* Update the context *)
-  let ctx = { ctx with var_counter } in
+  ctx.var_counter := var_counter;
   (* Return *)
   (ctx, var)
 
@@ -3303,65 +3307,6 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
   List.map (translate_type_decl ctx)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
-(** Translates function signatures.
-
-    Takes as input a list of function information containing:
-    - the function id
-    - a list of optional names for the inputs
-    - the function signature
-    
-    Returns a map from forward/backward functions identifiers to:
-    - translated function signatures
-    - optional names for the outputs values (we derive them for the backward
-      functions)
- *)
-let translate_fun_signatures (decls_ctx : C.decls_ctx)
-    (functions : (A.fun_id * string option list * A.fun_sig) list) :
-    fun_sig_named_outputs RegularFunIdNotLoopMap.t =
-  (* For every function, translate the signatures of:
-     - the forward function
-     - the backward functions
-  *)
-  let translate_one (fun_id : A.fun_id) (input_names : string option list)
-      (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list
-      =
-    log#ldebug
-      (lazy
-        ("Translating signature of function: "
-        ^ Print.Expressions.fun_id_to_string
-            (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-            fun_id));
-    (* Retrieve the regions hierarchy *)
-    let regions_hierarchy =
-      FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
-    in
-    (* The forward function *)
-    let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in
-    let fwd_id = (fun_id, None) in
-    (* The backward functions *)
-    let back_sgs =
-      if !Config.return_back_funs then []
-      else
-        List.map
-          (fun (rg : T.region_var_group) ->
-            let tsg =
-              translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id)
-            in
-            let id = (fun_id, Some rg.id) in
-            (id, tsg))
-          regions_hierarchy
-    in
-    (* Return *)
-    (fwd_id, fwd_sg) :: back_sgs
-  in
-  let translated =
-    List.concat
-      (List.map (fun (id, names, sg) -> translate_one id names sg) functions)
-  in
-  List.fold_left
-    (fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
-    RegularFunIdNotLoopMap.empty translated
-
 let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     : trait_decl =
   let {
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 06d4bd6d..8b221c93 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -6,7 +6,6 @@ open LlbcAst
 open Contexts
 module SA = SymbolicAst
 module Micro = PureMicroPasses
-open PureUtils
 open TranslateCore
 
 (** The local logger *)
@@ -43,7 +42,6 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
     TODO: maybe we should introduce a record for this.
 *)
 let translate_function_to_pure (trans_ctx : trans_ctx)
-    (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) :
     pure_fun_translation_no_loops =
   (* Debug *)
@@ -58,13 +56,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   (* Convert the symbolic ASTs to pure ASTs: *)
 
   (* Initialize the context *)
-  let forward_sig =
-    RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs
-  in
   let sv_to_var = SymbolicValueId.Map.empty in
   let var_counter = Pure.VarId.generator_zero in
   let state_var, var_counter = Pure.VarId.fresh var_counter in
-  let back_state_var, var_counter = Pure.VarId.fresh var_counter in
   let fuel0, var_counter = Pure.VarId.fresh var_counter in
   let fuel, var_counter = Pure.VarId.fresh var_counter in
   let calls = FunCallId.Map.empty in
@@ -89,7 +83,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   let fun_context =
     {
       SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls;
-      fun_sigs;
       fun_infos = trans_ctx.fun_ctx.fun_infos;
       regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies;
     }
@@ -126,17 +119,45 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
         !m
   in
 
+  let input_names =
+    match fdef.body with
+    | None -> List.map (fun _ -> None) fdef.signature.inputs
+    | Some body ->
+        List.map
+          (fun (v : var) -> v.name)
+          (LlbcAstUtils.fun_body_get_input_vars body)
+  in
+
+  let sg =
+    SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx (FRegular def_id)
+      fdef.signature input_names
+  in
+
+  let regions_hierarchy =
+    LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies
+  in
+
+  let var_counter, back_state_vars =
+    if !Config.return_back_funs then (var_counter, [])
+    else
+      List.fold_left_map
+        (fun var_counter (region_vars : region_var_group) ->
+          let gid = region_vars.id in
+          let var, var_counter = Pure.VarId.fresh var_counter in
+          (var_counter, (gid, var)))
+        var_counter regions_hierarchy
+  in
+  let back_state_vars = RegionGroupId.Map.of_list back_state_vars in
+
   let ctx =
     {
       SymbolicToPure.bid = None;
-      (* Dummy for now *)
-      sg = forward_sig.sg;
-      fwd_sg = forward_sig.sg;
+      sg;
       (* Will need to be updated for the backward functions *)
       sv_to_var;
-      var_counter;
+      var_counter = ref var_counter;
       state_var;
-      back_state_var;
+      back_state_vars;
       fuel0;
       fuel;
       type_context;
@@ -146,9 +167,11 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls;
       fun_decl = fdef;
       forward_inputs = [];
-      (* Empty for now *)
-      backward_inputs = RegionGroupId.Map.empty;
-      (* Empty for now *)
+      (* Initialized just below *)
+      backward_inputs_no_state = RegionGroupId.Map.empty;
+      (* Initialized just below *)
+      backward_inputs_with_state = RegionGroupId.Map.empty;
+      (* Initialized just below *)
       backward_outputs = RegionGroupId.Map.empty;
       loop_backward_outputs = None;
       (* Empty for now *)
@@ -180,6 +203,51 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     | _ -> raise (Failure "Unreachable")
   in
 
+  (* Add the backward inputs *)
+  let ctx, backward_inputs_no_state, backward_inputs_with_state =
+    if !Config.return_back_funs then (ctx, [], [])
+    else
+      let ctx, inputs_no_with_state =
+        List.fold_left_map
+          (fun ctx (region_vars : region_var_group) ->
+            let gid = region_vars.id in
+            let back_sg = RegionGroupId.Map.find gid sg.back_sg in
+            let ctx, no_state =
+              SymbolicToPure.fresh_vars back_sg.inputs_no_state ctx
+            in
+            let ctx, with_state =
+              SymbolicToPure.fresh_vars back_sg.inputs ctx
+            in
+            (ctx, ((gid, no_state), (gid, with_state))))
+          ctx regions_hierarchy
+      in
+      let inputs_no_state, inputs_with_state =
+        List.split inputs_no_with_state
+      in
+      (ctx, inputs_no_state, inputs_with_state)
+  in
+  let backward_inputs_no_state =
+    RegionGroupId.Map.of_list backward_inputs_no_state
+  in
+  let backward_inputs_with_state =
+    RegionGroupId.Map.of_list backward_inputs_with_state
+  in
+  let ctx = { ctx with backward_inputs_no_state; backward_inputs_with_state } in
+
+  (* Add the backward outputs *)
+  let ctx, backward_outputs =
+    List.fold_left_map
+      (fun ctx (region_vars : region_var_group) ->
+        let gid = region_vars.id in
+        let back_sg = RegionGroupId.Map.find gid sg.back_sg in
+        let outputs = List.combine back_sg.output_names back_sg.outputs in
+        let ctx, vars = SymbolicToPure.fresh_vars outputs ctx in
+        (ctx, (gid, vars)))
+      ctx regions_hierarchy
+  in
+  let backward_outputs = RegionGroupId.Map.of_list backward_outputs in
+  let ctx = { ctx with backward_outputs } in
+
   (* Translate the forward function *)
   let pure_forward =
     match symbolic_trans with
@@ -187,7 +255,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast)
   in
 
-  (* Translate the backward functions *)
+  (* Translate the backward functions, if we split the forward and backward functions *)
   let translate_backward (rg : region_var_group) : Pure.fun_decl =
     (* For the backward inputs/outputs initialization: we use the fact that
      * there are no nested borrows for now, and so that the region groups
@@ -197,83 +265,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
     match symbolic_trans with
     | None ->
-        (* Initialize the context - note that the ret_ty is not really
-         * useful as we don't translate a body *)
-        let backward_sg =
-          RegularFunIdNotLoopMap.find (FRegular def_id, Some back_id) fun_sigs
-        in
-        let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in
-
+        (* Initialize the context *)
+        let ctx = { ctx with bid = Some back_id } in
         (* Translate *)
         SymbolicToPure.translate_fun_decl ctx None
     | Some (_, symbolic) ->
-        (* Finish initializing the context by adding the additional input
-           variables required by the backward function.
-        *)
-        let backward_sg =
-          RegularFunIdNotLoopMap.find (FRegular def_id, Some back_id) fun_sigs
-        in
-        (* We need to ignore the forward inputs, and the state input (if there is) *)
-        let backward_inputs =
-          let sg = backward_sg.sg in
-          (* TODO: *)
-          assert (not !Config.return_back_funs);
-          (* We need to ignore the forward state and the backward state *)
-          let num_forward_inputs =
-            sg.info.fwd_info.num_inputs_with_fuel_with_state
-          in
-          let num_back_inputs =
-            match sg.info.back_info with
-            | SingleBack (Some info) -> info.num_inputs_no_fuel_no_state
-            | _ -> raise (Failure "Unexpected")
-          in
-          Collections.List.subslice sg.inputs num_forward_inputs
-            (num_forward_inputs + num_back_inputs)
-        in
-        (* As we forbid nested borrows, the additional inputs for the backward
-         * functions come from the borrows in the return value of the rust function:
-         * we thus use the name "ret" for those inputs *)
-        let backward_inputs =
-          List.map (fun ty -> (Some "ret", ty)) backward_inputs
-        in
-        let ctx, backward_inputs =
-          SymbolicToPure.fresh_vars backward_inputs ctx
-        in
-        (* The outputs for the backward functions, however, come from borrows
-         * present in the input values of the rust function: for those we reuse
-         * the names of the input values. *)
-        let backward_outputs =
-          List.combine backward_sg.output_names backward_sg.sg.doutputs
-        in
-        let ctx, backward_outputs =
-          SymbolicToPure.fresh_vars backward_outputs ctx
-        in
-        let backward_inputs =
-          RegionGroupId.Map.singleton back_id backward_inputs
-        in
-        let backward_outputs =
-          RegionGroupId.Map.singleton back_id backward_outputs
-        in
-
-        (* Put everything in the context *)
-        let ctx =
-          {
-            ctx with
-            bid = Some back_id;
-            sg = backward_sg.sg;
-            backward_inputs;
-            backward_outputs;
-          }
-        in
-
+        (* Initialize the context *)
+        let ctx = { ctx with bid = Some back_id } in
         (* Translate *)
         SymbolicToPure.translate_fun_decl ctx (Some symbolic)
   in
-  let regions_hierarchy =
-    LlbcAstUtils.FunIdMap.find (FRegular fdef.def_id)
-      fun_context.regions_hierarchies
+  let pure_backwards =
+    if !Config.return_back_funs then []
+    else List.map translate_backward regions_hierarchy
   in
-  let pure_backwards = List.map translate_backward regions_hierarchy in
 
   (* Return *)
   (pure_forward, pure_backwards)
@@ -300,36 +305,10 @@ let translate_crate_to_pure (crate : crate) :
       (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
 
-  (* Translate all the function *signatures* *)
-  let assumed_sigs =
-    List.map
-      (fun (info : Assumed.assumed_fun_info) ->
-        ( FAssumed info.fun_id,
-          List.map (fun _ -> None) info.fun_sig.inputs,
-          info.fun_sig ))
-      Assumed.assumed_fun_infos
-  in
-  let local_sigs =
-    List.map
-      (fun (fdef : fun_decl) ->
-        let input_names =
-          match fdef.body with
-          | None -> List.map (fun _ -> None) fdef.signature.inputs
-          | Some body ->
-              List.map
-                (fun (v : var) -> v.name)
-                (LlbcAstUtils.fun_body_get_input_vars body)
-        in
-        (FRegular fdef.def_id, input_names, fdef.signature))
-      (FunDeclId.Map.values crate.fun_decls)
-  in
-  let sigs = List.append assumed_sigs local_sigs in
-  let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in
-
   (* Translate all the *transparent* functions *)
   let pure_translations =
     List.map
-      (translate_function_to_pure trans_ctx fun_sigs type_decls_map)
+      (translate_function_to_pure trans_ctx type_decls_map)
       (FunDeclId.Map.values crate.fun_decls)
   in
 
@@ -1036,7 +1015,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     List.map
       (fun { fwd; _ } ->
         let fwd_f =
-          if fwd.f.Pure.signature.info.effect_info.is_rec then
+          if fwd.f.Pure.signature.fwd_info.effect_info.is_rec then
             [ (fwd.f.def_id, None) ]
           else []
         in
-- 
cgit v1.3.1


From a49754a5b11e4de8793dc7e13c2962d139eb03b1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Dec 2023 10:21:08 +0100
Subject: Rename some definitions

---
 compiler/AssociatedTypes.ml            | 10 ++---
 compiler/Contexts.ml                   | 42 +++++++++---------
 compiler/Interpreter.ml                |  8 ++--
 compiler/InterpreterBorrows.ml         | 12 +++---
 compiler/InterpreterExpansion.ml       |  2 +-
 compiler/InterpreterExpressions.ml     |  5 +--
 compiler/InterpreterLoopsFixedPoint.ml | 18 ++++----
 compiler/InterpreterLoopsJoinCtxs.ml   | 36 ++++++++--------
 compiler/InterpreterLoopsMatchCtxs.ml  |  4 +-
 compiler/InterpreterStatements.ml      | 12 +++---
 compiler/InterpreterUtils.ml           | 26 ++++++------
 compiler/Invariants.ml                 |  2 +-
 compiler/Print.ml                      | 10 ++---
 compiler/SymbolicToPure.ml             | 78 +++++++++++++++++-----------------
 compiler/Translate.ml                  | 14 +++---
 15 files changed, 139 insertions(+), 140 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index e2f687e8..054c8169 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -493,11 +493,11 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
 let mk_norm_ctx (ctx : eval_ctx) : norm_ctx =
   {
     norm_trait_types = ctx.norm_trait_types;
-    type_decls = ctx.type_context.type_decls;
-    fun_decls = ctx.fun_context.fun_decls;
-    global_decls = ctx.global_context.global_decls;
-    trait_decls = ctx.trait_decls_context.trait_decls;
-    trait_impls = ctx.trait_impls_context.trait_impls;
+    type_decls = ctx.type_ctx.type_decls;
+    fun_decls = ctx.fun_ctx.fun_decls;
+    global_decls = ctx.global_ctx.global_decls;
+    trait_decls = ctx.trait_decls_ctx.trait_decls;
+    trait_impls = ctx.trait_impls_ctx.trait_impls;
     type_vars = ctx.type_vars;
     const_generic_vars = ctx.const_generic_vars;
   }
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a30ed0f1..5d646a61 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -180,35 +180,35 @@ type config = {
 
 let mk_config (mode : interpreter_mode) : config = { mode }
 
-type type_context = {
+type type_ctx = {
   type_decls_groups : type_declaration_group TypeDeclId.Map.t;
   type_decls : type_decl TypeDeclId.Map.t;
   type_infos : TypesAnalysis.type_infos;
 }
 [@@deriving show]
 
-type fun_context = {
+type fun_ctx = {
   fun_decls : fun_decl FunDeclId.Map.t;
   fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
   regions_hierarchies : region_var_groups FunIdMap.t;
 }
 [@@deriving show]
 
-type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
+type global_ctx = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
 
-type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t }
+type trait_decls_ctx = { trait_decls : trait_decl TraitDeclId.Map.t }
 [@@deriving show]
 
-type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t }
+type trait_impls_ctx = { trait_impls : trait_impl TraitImplId.Map.t }
 [@@deriving show]
 
 type decls_ctx = {
-  type_ctx : type_context;
-  fun_ctx : fun_context;
-  global_ctx : global_context;
-  trait_decls_ctx : trait_decls_context;
-  trait_impls_ctx : trait_impls_context;
+  type_ctx : type_ctx;
+  fun_ctx : fun_ctx;
+  global_ctx : global_ctx;
+  trait_decls_ctx : trait_decls_ctx;
+  trait_impls_ctx : trait_impls_ctx;
 }
 [@@deriving show]
 
@@ -230,11 +230,11 @@ module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd)
 
 (** Evaluation context *)
 type eval_ctx = {
-  type_context : type_context;
-  fun_context : fun_context;
-  global_context : global_context;
-  trait_decls_context : trait_decls_context;
-  trait_impls_context : trait_impls_context;
+  type_ctx : type_ctx;
+  fun_ctx : fun_ctx;
+  global_ctx : global_ctx;
+  trait_decls_ctx : trait_decls_ctx;
+  trait_impls_ctx : trait_impls_ctx;
   region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
@@ -290,20 +290,20 @@ let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
   fst (env_lookup_var ctx.env vid)
 
 let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
-  TypeDeclId.Map.find tid ctx.type_context.type_decls
+  TypeDeclId.Map.find tid ctx.type_ctx.type_decls
 
 let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
-  FunDeclId.Map.find fid ctx.fun_context.fun_decls
+  FunDeclId.Map.find fid ctx.fun_ctx.fun_decls
 
 let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
     global_decl =
-  GlobalDeclId.Map.find gid ctx.global_context.global_decls
+  GlobalDeclId.Map.find gid ctx.global_ctx.global_decls
 
 let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl =
-  TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls
+  TraitDeclId.Map.find id ctx.trait_decls_ctx.trait_decls
 
 let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
-  TraitImplId.Map.find id ctx.trait_impls_context.trait_impls
+  TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
 
 (** Retrieve a variable's value in the current frame *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
@@ -528,7 +528,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
   fst (ctx_subst_abs ctx abs_id abs)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
-  let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
+  let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
   match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 76432faa..22d176c9 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -195,7 +195,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_context ctx region_groups sg.generics.types
+    initialize_eval_ctx ctx region_groups sg.generics.types
       sg.generics.const_generics
   in
   (* Instantiate the signature. This updates the context because we compute
@@ -277,7 +277,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
    * an instantiation of the signature, so that we use fresh
    * region ids for the return abstractions. *)
   let regions_hierarchy =
-    FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
+    FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let _, ret_inst_sg =
     symbolic_instantiate_fun_sig ctx fdef.signature regions_hierarchy fdef.kind
@@ -466,7 +466,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
   let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
 
   let regions_hierarchy =
-    FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
+    FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
 
   (* Create the continuation to finish the evaluation *)
@@ -615,7 +615,7 @@ module Test = struct
     assert (body.arg_count = 0);
 
     (* Create the evaluation context *)
-    let ctx = initialize_eval_context decls_ctx [] [] [] in
+    let ctx = initialize_eval_ctx decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = ctx_push_uninitialized_vars ctx body.locals in
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e56919fa..a2eb2545 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1628,7 +1628,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
             assert (opt_bid = None);
             (* Simply explore the child *)
             list_avalues false push_fail child_av
@@ -1639,7 +1639,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             { child = child_av; given_back = _; given_back_meta = _ }
         | AIgnoredSharedLoan child_av ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
             (* Simply explore the child *)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
@@ -1659,14 +1659,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             push av
         | AIgnoredMutBorrow (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
             assert (opt_bid = None);
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
             { child = child_av; given_back = _; given_back_meta = _ } ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
@@ -1683,7 +1683,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        assert (not (ty_has_borrows ctx.type_context.type_infos ty))
+        assert (not (ty_has_borrows ctx.type_ctx.type_infos ty))
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1732,7 +1732,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        assert (not (ty_has_borrows ctx.type_context.type_infos ty));
+        assert (not (ty_has_borrows ctx.type_ctx.type_infos ty));
         ([], v)
   in
 
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index bbf4d9d5..e489ddc3 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -627,7 +627,7 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
       inherit [_] iter_eval_ctx
 
       method! visit_VSymbolic _ sv =
-        if ty_has_borrows ctx.type_context.type_infos sv.sv_ty then
+        if ty_has_borrows ctx.type_ctx.type_infos sv.sv_ty then
           raise (FoundSymbolicValue sv)
         else ()
 
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 1b5b79dd..8536b4ab 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -32,8 +32,7 @@ let expand_primitively_copyable_at_place (config : config)
    fun cf ctx ->
     let v = read_place access p ctx in
     match
-      find_first_primitively_copyable_sv_with_borrows
-        ctx.type_context.type_infos v
+      find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v
     with
     | None -> cf ctx
     | Some sv ->
@@ -351,7 +350,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
         assert (
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
-               ctx.type_context.type_infos v));
+               ctx.type_ctx.type_infos v));
         (* Actually perform the copy *)
         let allow_adt_copy = false in
         let ctx, v = copy_value allow_adt_copy config ctx v in
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index c4e180fa..4dabe974 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -300,7 +300,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
   let env = List.append fresh_absl env in
   let ctx = { ctx with env } in
 
-  let _, new_ctx_ids_map = compute_context_ids ctx in
+  let _, new_ctx_ids_map = compute_ctx_ids ctx in
 
   (* Synthesize *)
   match cf ctx with
@@ -385,8 +385,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
       match !fixed_ids with
       | Some _ -> ctx1
       | None ->
-          let old_ids, _ = compute_context_ids ctx1 in
-          let new_ids, _ = compute_contexts_ids !ctxs in
+          let old_ids, _ = compute_ctx_ids ctx1 in
+          let new_ids, _ = compute_ctxs_ids !ctxs in
           let blids = BorrowId.Set.diff old_ids.blids new_ids.blids in
           let aids = AbstractionId.Set.diff old_ids.aids new_ids.aids in
           (* End those borrows and abstractions *)
@@ -409,7 +409,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
           ctxs := List.map (end_borrows_abs blids aids) !ctxs;
           (* Note that the fixed ids are given by the original context, from *before*
              we introduce fresh abstractions/reborrows for the shared values *)
-          fixed_ids := Some (fst (compute_context_ids ctx0));
+          fixed_ids := Some (fst (compute_ctx_ids ctx0));
           ctx1
     in
 
@@ -424,12 +424,12 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
      intersection of ids between the original environment and the list
      of new environments *)
   let compute_fixed_ids (ctxl : eval_ctx list) : ids_sets =
-    let fixed_ids, _ = compute_context_ids ctx0 in
+    let fixed_ids, _ = compute_ctx_ids ctx0 in
     let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in
     let sids = ref sids in
     List.iter
       (fun ctx ->
-        let fixed_ids, _ = compute_context_ids ctx in
+        let fixed_ids, _ = compute_ctx_ids ctx in
         sids := SymbolicValueId.Set.inter !sids fixed_ids.sids)
       ctxl;
     let sids = !sids in
@@ -568,7 +568,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
                   InterpreterBorrows.end_abstraction_no_synth config abs_id ctx
                 in
                 (* Explore the context, and check which abstractions are not there anymore *)
-                let ids, _ = compute_context_ids ctx in
+                let ids, _ = compute_ctx_ids ctx in
                 let ended_ids = AbstractionId.Set.diff !fp_aids ids.aids in
                 add_ended_aids rg_id ended_ids)
               ctx.region_groups
@@ -840,8 +840,8 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
 
 let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) :
     SymbolicValueId.Set.t * symbolic_value list =
-  let old_ids, _ = compute_context_ids ctx in
-  let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
+  let old_ids, _ = compute_ctx_ids ctx in
+  let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in
   let fresh_sids = SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
 
   (* Compute the set of symbolic values which appear in shared values inside
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 8d485483..445e5abf 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
-      assert (not (ty_has_borrows ctx.type_context.type_infos ty1))
+      assert (not (ty_has_borrows ctx.type_ctx.type_infos ty0));
+      assert (not (ty_has_borrows ctx.type_ctx.type_infos ty1))
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -543,11 +543,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (* Construct the joined context - of course, the type, fun, etc. contexts
      * should be the same in the two contexts *)
     let {
-      type_context;
-      fun_context;
-      global_context;
-      trait_decls_context;
-      trait_impls_context;
+      type_ctx;
+      fun_ctx;
+      global_ctx;
+      trait_decls_ctx;
+      trait_impls_ctx;
       region_groups;
       type_vars;
       const_generic_vars;
@@ -559,11 +559,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
       ctx0
     in
     let {
-      type_context = _;
-      fun_context = _;
-      global_context = _;
-      trait_decls_context = _;
-      trait_impls_context = _;
+      type_ctx = _;
+      fun_ctx = _;
+      global_ctx = _;
+      trait_decls_ctx = _;
+      trait_impls_ctx = _;
       region_groups = _;
       type_vars = _;
       const_generic_vars = _;
@@ -577,11 +577,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     let ended_regions = RegionId.Set.union ended_regions0 ended_regions1 in
     Ok
       {
-        type_context;
-        fun_context;
-        global_context;
-        trait_decls_context;
-        trait_impls_context;
+        type_ctx;
+        fun_ctx;
+        global_ctx;
+        trait_decls_ctx;
+        trait_impls_ctx;
         region_groups;
         type_vars;
         const_generic_vars;
@@ -621,7 +621,7 @@ let destructure_new_abs (loop_id : LoopId.id)
     contexts we join don't have non-fixed abstractions with the same ids.
   *)
 let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
-  let ids, _ = compute_context_ids ctx in
+  let ids, _ = compute_ctx_ids ctx in
   let abs_to_refresh = AbstractionId.Set.diff ids.aids old_abs in
   let aids_subst =
     List.map
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 90559c29..2a688fa7 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -658,7 +658,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     else (
       (* The caller should have checked that the symbolic values don't contain
          borrows *)
-      assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty));
+      assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv0.sv_ty));
       (* We simply introduce a fresh symbolic value *)
       mk_fresh_symbolic_value sv0.sv_ty)
 
@@ -669,7 +669,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
        - there are no borrows in the "regular" value
        If there are loans in the regular value, raise an exception.
     *)
-    assert (not (ty_has_borrows S.ctx.type_context.type_infos sv.sv_ty));
+    assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv.sv_ty));
     assert (not (value_has_borrows S.ctx v.value));
     let value_is_left = not left in
     (match InterpreterBorrowsCore.get_first_loan_in_value v with
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 30b7b333..da617c64 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -747,7 +747,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
           let tr_self = UnknownTrait __FUNCTION__ in
           let regions_hierarchy =
             LlbcAstUtils.FunIdMap.find (FRegular fid)
-              ctx.fun_context.regions_hierarchies
+              ctx.fun_ctx.regions_hierarchies
           in
           let inst_sg =
             instantiate_fun_sig ctx func.generics tr_self def.signature
@@ -793,7 +793,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
                   let fid : fun_id = FRegular id in
                   let regions_hierarchy =
                     LlbcAstUtils.FunIdMap.find fid
-                      ctx.fun_context.regions_hierarchies
+                      ctx.fun_ctx.regions_hierarchies
                   in
                   let inst_sg =
                     instantiate_fun_sig ctx generics tr_self
@@ -853,7 +853,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
                           method_def.signature.parent_params_info));
                   let regions_hierarchy =
                     LlbcAstUtils.FunIdMap.find (FRegular method_id)
-                      ctx.fun_context.regions_hierarchies
+                      ctx.fun_ctx.regions_hierarchies
                   in
                   let tr_self = TraitRef trait_ref in
                   let inst_sg =
@@ -884,7 +884,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
               (* Instantiate *)
               let regions_hierarchy =
                 LlbcAstUtils.FunIdMap.find (FRegular method_id)
-                  ctx.fun_context.regions_hierarchies
+                  ctx.fun_ctx.regions_hierarchies
               in
               let tr_self = TraitRef trait_ref in
               let inst_sg =
@@ -1450,7 +1450,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
    * this is a current limitation of our synthesis *)
   assert (
     List.for_all
-      (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
+      (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty))
       generics.types);
 
   (* There are two cases (and this is extremely annoying):
@@ -1476,7 +1476,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
         | _ ->
             let regions_hierarchy =
               LlbcAstUtils.FunIdMap.find (FAssumed fid)
-                ctx.fun_context.regions_hierarchies
+                ctx.fun_ctx.regions_hierarchies
             in
             (* There shouldn't be any reference to Self *)
             let tr_self = UnknownTrait __FUNCTION__ in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e04a6b90..a1a06ee5 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -265,7 +265,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
       inherit [_] iter_typed_value
 
       method! visit_symbolic_value _ s =
-        if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
+        if ty_has_borrow_under_mut ctx.type_ctx.type_infos s.sv_ty then
           raise Found
         else ()
     end
@@ -288,15 +288,15 @@ let rvalue_get_place (rv : rvalue) : place option =
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
 let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool =
-  ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv
+  ValuesUtils.symbolic_value_has_borrows ctx.type_ctx.type_infos sv
 
 (** See {!ValuesUtils.value_has_borrows}. *)
 let value_has_borrows (ctx : eval_ctx) (v : value) : bool =
-  ValuesUtils.value_has_borrows ctx.type_context.type_infos v
+  ValuesUtils.value_has_borrows ctx.type_ctx.type_infos v
 
 (** See {!ValuesUtils.value_has_loans_or_borrows}. *)
 let value_has_loans_or_borrows (ctx : eval_ctx) (v : value) : bool =
-  ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v
+  ValuesUtils.value_has_loans_or_borrows ctx.type_ctx.type_infos v
 
 (** See {!ValuesUtils.value_has_loans}. *)
 let value_has_loans (v : value) : bool = ValuesUtils.value_has_loans v
@@ -401,19 +401,19 @@ let compute_env_elem_ids (x : env_elem) : ids_sets * ids_to_values =
   compute_env_ids [ x ]
 
 (** Compute the sets of ids found in a list of contexts. *)
-let compute_contexts_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
+let compute_ctxs_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
   List.iter (compute#visit_eval_ctx ()) ctxl;
   (get_ids (), get_ids_to_values ())
 
 (** Compute the sets of ids found in a context. *)
-let compute_context_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
-  compute_contexts_ids [ ctx ]
+let compute_ctx_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
+  compute_ctxs_ids [ ctx ]
 
 (** **WARNING**: this function doesn't compute the normalized types
     (for the trait type aliases). This should be computed afterwards.
  *)
-let initialize_eval_context (ctx : decls_ctx)
+let initialize_eval_ctx (ctx : decls_ctx)
     (region_groups : RegionGroupId.id list) (type_vars : type_var list)
     (const_generic_vars : const_generic_var list) : eval_ctx =
   reset_global_counters ();
@@ -427,11 +427,11 @@ let initialize_eval_context (ctx : decls_ctx)
          const_generic_vars)
   in
   {
-    type_context = ctx.type_ctx;
-    fun_context = ctx.fun_ctx;
-    global_context = ctx.global_ctx;
-    trait_decls_context = ctx.trait_decls_ctx;
-    trait_impls_context = ctx.trait_impls_ctx;
+    type_ctx = ctx.type_ctx;
+    fun_ctx = ctx.fun_ctx;
+    global_ctx = ctx.global_ctx;
+    trait_decls_ctx = ctx.trait_decls_ctx;
+    trait_impls_ctx = ctx.trait_impls_ctx;
     region_groups;
     type_vars;
     const_generic_vars;
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index fa0d7436..b87cdff7 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -768,7 +768,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
     assert (info.env_count = 0 || info.aproj_borrows = []);
     (* A symbolic value containing borrows can't be duplicated (i.e., copied):
      * it must be expanded first *)
-    if ty_has_borrows ctx.type_context.type_infos info.ty then
+    if ty_has_borrows ctx.type_ctx.type_infos info.ty then
       assert (info.env_count <= 1);
     (* A duplicated symbolic value is necessarily primitively copyable *)
     assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty);
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 0e2ec1fc..8999c77d 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -409,11 +409,11 @@ module Contexts = struct
     }
 
   let eval_ctx_to_fmt_env (ctx : eval_ctx) : fmt_env =
-    let type_decls = ctx.type_context.type_decls in
-    let fun_decls = ctx.fun_context.fun_decls in
-    let global_decls = ctx.global_context.global_decls in
-    let trait_decls = ctx.trait_decls_context.trait_decls in
-    let trait_impls = ctx.trait_impls_context.trait_impls in
+    let type_decls = ctx.type_ctx.type_decls in
+    let fun_decls = ctx.fun_ctx.fun_decls in
+    let global_decls = ctx.global_ctx.global_decls in
+    let trait_decls = ctx.trait_decls_ctx.trait_decls in
+    let trait_impls = ctx.trait_impls_ctx.trait_impls in
     (* Below: it is always safe to omit fields - if an id can't be found at
        printing time, we print the id (in raw form) instead of the name it
        designates. *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 204fc399..d8213317 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -15,7 +15,7 @@ module PP = PrintPure
 (** The local logger *)
 let log = Logging.symbolic_to_pure_log
 
-type type_context = {
+type type_ctx = {
   llbc_type_decls : T.type_decl TypeDeclId.Map.t;
   type_decls : type_decl TypeDeclId.Map.t;
       (** We use this for type-checking (for sanity checks) when translating
@@ -43,18 +43,18 @@ type fun_sig_named_outputs = {
 }
 [@@deriving show]
 
-type fun_context = {
+type fun_ctx = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_infos : fun_info A.FunDeclId.Map.t;
   regions_hierarchies : T.region_var_groups FunIdMap.t;
 }
 [@@deriving show]
 
-type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
+type global_ctx = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
 [@@deriving show]
 
-type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
-type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
+type trait_decls_ctx = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
+type trait_impls_ctx = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
 
 (** Whenever we translate a function call or an ended abstraction, we
     store the related information (this is useful when translating ended
@@ -120,11 +120,11 @@ type loop_info = {
 
 (** Body synthesis context *)
 type bs_ctx = {
-  type_context : type_context; (* TODO: rename *)
-  fun_context : fun_context; (* TODO: rename *)
-  global_context : global_context; (* TODO: rename *)
-  trait_decls_ctx : trait_decls_context;
-  trait_impls_ctx : trait_impls_context;
+  type_ctx : type_ctx;
+  fun_ctx : fun_ctx;
+  global_ctx : global_ctx;
+  trait_decls_ctx : trait_decls_ctx;
+  trait_impls_ctx : trait_impls_ctx;
   fun_decl : A.fun_decl;
   bid : RegionGroupId.id option;
       (** TODO: rename
@@ -234,9 +234,9 @@ type bs_ctx = {
 
 (* TODO: move *)
 let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
+  let type_decls = ctx.type_ctx.llbc_type_decls in
+  let fun_decls = ctx.fun_ctx.llbc_fun_decls in
+  let global_decls = ctx.global_ctx.llbc_global_decls in
   let trait_decls = ctx.trait_decls_ctx in
   let trait_impls = ctx.trait_impls_ctx in
   let { regions; types; const_generics; trait_clauses } : T.generic_params =
@@ -258,9 +258,9 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
   }
 
 let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
-  let type_decls = ctx.type_context.llbc_type_decls in
-  let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let global_decls = ctx.global_context.llbc_global_decls in
+  let type_decls = ctx.type_ctx.llbc_type_decls in
+  let fun_decls = ctx.fun_ctx.llbc_fun_decls in
+  let global_decls = ctx.global_ctx.llbc_global_decls in
   let trait_decls = ctx.trait_decls_ctx in
   let trait_impls = ctx.trait_impls_ctx in
   let generics = ctx.sg.generics in
@@ -346,11 +346,11 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
 
 let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
-  TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
+  TypeDeclId.Map.find id ctx.type_ctx.llbc_type_decls
 
 let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
     A.fun_decl =
-  A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
+  A.FunDeclId.Map.find id ctx.fun_ctx.llbc_fun_decls
 
 (* Some generic translation functions (we need to translate different "flavours"
    of types: forward types, backward types, etc.) *)
@@ -617,13 +617,13 @@ and translate_fwd_trait_instance_id (type_infos : type_infos)
 
 (** Simply calls [translate_fwd_ty] *)
 let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
-  let type_infos = ctx.type_context.type_infos in
+  let type_infos = ctx.type_ctx.type_infos in
   translate_fwd_ty type_infos ty
 
 (** Simply calls [translate_fwd_generic_args] *)
 let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     generic_args =
-  let type_infos = ctx.type_context.type_infos in
+  let type_infos = ctx.type_ctx.type_infos in
   translate_fwd_generic_args type_infos generics
 
 (** Translate a type, when some regions may have ended.
@@ -708,7 +708,7 @@ let rec translate_back_ty (type_infos : type_infos)
 (** Simply calls [translate_back_ty] *)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
     (inside_mut : bool) (ty : T.ty) : ty option =
-  let type_infos = ctx.type_context.type_infos in
+  let type_infos = ctx.type_ctx.type_infos in
   translate_back_ty type_infos keep_region inside_mut ty
 
 let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
@@ -721,8 +721,8 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
   in
   let env = VarId.Map.empty in
   {
-    PureTypeCheck.type_decls = ctx.type_context.type_decls;
-    global_decls = ctx.global_context.llbc_global_decls;
+    PureTypeCheck.type_decls = ctx.type_ctx.type_decls;
+    global_decls = ctx.global_ctx.llbc_global_decls;
     env;
     const_generics;
   }
@@ -742,7 +742,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
   match id with
   | FunId fun_id -> FunId fun_id
   | TraitMethod (trait_ref, method_name, fun_decl_id) ->
-      let type_infos = ctx.type_context.type_infos in
+      let type_infos = ctx.type_ctx.type_infos in
       let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
       TraitMethod (trait_ref, method_name, fun_decl_id)
 
@@ -894,7 +894,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
       List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy
     in
     let ctx =
-      InterpreterUtils.initialize_eval_context decls_ctx region_groups
+      InterpreterUtils.initialize_eval_ctx decls_ctx region_groups
         sg.generics.types sg.generics.const_generics
     in
     (* Compute the normalization map for the *sty* types and add it to the context *)
@@ -1786,7 +1786,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         (* Retrieve the effect information about this function (can fail,
          * takes a state as input, etc.) *)
         let effect_info =
-          get_fun_effect_info ctx.fun_context.fun_infos fid None None
+          get_fun_effect_info ctx.fun_ctx.fun_infos fid None None
         in
         (* Depending on the function effects:
            * - add the fuel
@@ -2006,7 +2006,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
         raise (Failure "Unreachable")
   in
   let effect_info =
-    get_fun_effect_info ctx.fun_context.fun_infos fun_id None (Some rg_id)
+    get_fun_effect_info ctx.fun_ctx.fun_infos fun_id None (Some rg_id)
   in
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   (* Retrieve the original call and the parent abstractions *)
@@ -2194,8 +2194,8 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
   | V.LoopCall ->
       let fun_id = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
-          (Some vloop_id) (Some rg_id)
+        get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fun_id) (Some vloop_id)
+          (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
       let generics = loop_info.generics in
@@ -2306,7 +2306,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
 and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
     (e : S.expression) (ctx : bs_ctx) : texpression =
   let ctx, var = fresh_var_for_symbolic_value sval ctx in
-  let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
+  let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in
   let global_expr = { id = Global gid; generics = empty_generic_args } in
   (* We use translate_fwd_ty to translate the global type *)
   let ty = ctx_translate_fwd_ty ctx decl.ty in
@@ -2482,7 +2482,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          - if we forbid using field projectors.
       *)
       let is_rec_def =
-        T.TypeDeclId.Set.mem adt_id ctx.type_context.recursive_decls
+        T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls
       in
       let use_let_with_cons =
         is_enum
@@ -2495,7 +2495,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
            like Coq don't, in which case we have to deconstruct the whole ADT
            at once (`let (a, b, c) = x in`) *)
         || TypesUtils.type_decl_from_type_id_is_tuple_struct
-             ctx.type_context.type_infos type_id
+             ctx.type_ctx.type_infos type_id
            && not (Config.backend_has_tuple_projectors ())
       in
       if use_let_with_cons then
@@ -2588,7 +2588,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
         { e = StructUpdate su; ty = var.ty }
     | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, generics, const_name) ->
-        let type_infos = ctx.type_context.type_infos in
+        let type_infos = ctx.type_ctx.type_infos in
         let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
         let generics = translate_fwd_generic_args type_infos generics in
         let qualif_id = TraitConst (trait_ref, generics, const_name) in
@@ -2722,7 +2722,7 @@ and translate_forward_end (ectx : C.eval_ctx)
         let sg = ctx.fun_decl.signature in
         let regions_hierarchy =
           LlbcAstUtils.FunIdMap.find (FRegular def_id)
-            ctx.fun_context.regions_hierarchies
+            ctx.fun_ctx.regions_hierarchies
         in
         List.map
           (fun (gid, _) ->
@@ -2816,7 +2816,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       (* Lookup the effect info for the loop function *)
       let fid = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
+        get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fid) None ctx.bid
       in
 
       (* Introduce a fresh output value for the forward function *)
@@ -2949,7 +2949,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
           List.map
             (fun ty ->
               assert (
-                not (TypesUtils.ty_has_borrows !ctx.type_context.type_infos ty));
+                not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty));
               (None, ctx_translate_fwd_ty !ctx ty))
             tys
         in
@@ -3173,7 +3173,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* Translate the signature *)
   let signature = translate_fun_sig_from_decomposed ctx.sg ctx.bid in
   let regions_hierarchy =
-    FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies
+    FunIdMap.find (FRegular def_id) ctx.fun_ctx.regions_hierarchies
   in
   (* Translate the body, if there is *)
   let body =
@@ -3181,8 +3181,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     | None -> None
     | Some body ->
         let effect_info =
-          get_fun_effect_info ctx.fun_context.fun_infos
-            (FunId (FRegular def_id)) None bid
+          get_fun_effect_info ctx.fun_ctx.fun_infos (FunId (FRegular def_id))
+            None bid
         in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8b221c93..e153f4f4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -72,7 +72,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
            | RecGroup _ -> Some tid)
          (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
   in
-  let type_context =
+  let type_ctx =
     {
       SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos;
       llbc_type_decls = trans_ctx.type_ctx.type_decls;
@@ -80,14 +80,14 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       recursive_decls = recursive_type_decls;
     }
   in
-  let fun_context =
+  let fun_ctx =
     {
       SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls;
       fun_infos = trans_ctx.fun_ctx.fun_infos;
       regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies;
     }
   in
-  let global_context =
+  let global_ctx =
     { SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls }
   in
 
@@ -134,7 +134,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   in
 
   let regions_hierarchy =
-    LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies
+    LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_ctx.regions_hierarchies
   in
 
   let var_counter, back_state_vars =
@@ -160,9 +160,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       back_state_vars;
       fuel0;
       fuel;
-      type_context;
-      fun_context;
-      global_context;
+      type_ctx;
+      fun_ctx;
+      global_ctx;
       trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls;
       trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls;
       fun_decl = fdef;
-- 
cgit v1.3.1


From 4f7bc41dcbc6187512111a81f968726452024d25 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Dec 2023 12:54:40 +0100
Subject: Simplify SymbolicToPure.bs_ctx.{backward_outputs,
 loop_backward_outputs}

---
 compiler/SymbolicToPure.ml | 153 ++++++++++++++++++++-------------------------
 compiler/Translate.ml      |  17 +----
 2 files changed, 70 insertions(+), 100 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ea2082c7..93e6cb4e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -109,6 +109,10 @@ type loop_info = {
       (** The forward inputs are initialized at [None] *)
   forward_output_no_state_no_result : var option;
       (** The forward outputs are initialized at [None] *)
+  back_outputs : ty list RegionGroupId.Map.t;
+      (** The map from region group ids to the types of the values given back
+          by the corresponding loop abstractions.
+       *)
 }
 [@@deriving show]
 
@@ -187,12 +191,11 @@ type bs_ctx = {
 
           Same remarks as for {!backward_inputs_no_state}.
        *)
-  backward_outputs : var list RegionGroupId.Map.t;
+  backward_outputs : var list option;
       (** The variables that the backward functions will output, corresponding
           to the borrows they give back (don't include the backward state).
 
           The translation is done as follows:
-          - for a given backward function, we choose a set of variables [v_i]
           - when we detect the ended input abstraction which corresponds
             to the backward function of the LLBC function we are translating,
             and which consumed the values [consumed_i] (that we need to give
@@ -201,14 +204,20 @@ type bs_ctx = {
                 let v_i = consumed_i in
                 ...
             ]}
-            Then, upon reaching the [Return] node, we introduce:
+            where the [v_i] are fresh, and are stored in the [backward_output].
+          - Then, upon reaching the [Return] node, we introduce:
             {[
-                (v_i)
+                return (v_i)
             ]}
+
+          The option is [None] before we detect the ended input abstraction,
+          and [Some] afterwards.
        *)
-  loop_backward_outputs : var list RegionGroupId.Map.t option;
+  loop_backward_outputs : var list option;
       (** Same as {!backward_outputs}, but for loops (if we entered a loop).
 
+          TODO: merge with [backward_outputs]?
+
           [None] if we are not inside a loop, [Some] otherwise (and whatever
           the kind of function we are translating: it will be [Some] even
           though we are synthesizing a forward function).
@@ -1607,7 +1616,9 @@ let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
-  | S.Return (ectx, opt_v) -> translate_return ectx opt_v ctx
+  | S.Return (ectx, opt_v) ->
+      (* Remark: we can't get there if we are inside a loop *)
+      translate_return ectx opt_v ctx
   | ReturnWithLoop (loop_id, is_continue) ->
       translate_return_with_loop loop_id is_continue ctx
   | Panic -> translate_panic ctx
@@ -1644,10 +1655,9 @@ and translate_panic (ctx : bs_ctx) : texpression =
   if ctx.inside_loop && Option.is_some ctx.bid then
     (* We are synthesizing the backward function of a loop body *)
     let bid = Option.get ctx.bid in
-    let back_vars =
-      T.RegionGroupId.Map.find bid (Option.get ctx.loop_backward_outputs)
-    in
-    let tys = List.map (fun (v : var) -> v.ty) back_vars in
+    let loop_id = Option.get ctx.loop_id in
+    let loop = LoopId.Map.find loop_id ctx.loops in
+    let tys = RegionGroupId.Map.find bid loop.back_outputs in
     let output = mk_simpl_tuple_ty tys in
     mk_output output
   else
@@ -1667,7 +1677,11 @@ and translate_panic (ctx : bs_ctx) : texpression =
         in
         mk_output output
 
-(** [opt_v]: the value to return, in case we translate a forward body *)
+(** [opt_v]: the value to return, in case we translate a forward body.
+
+    Remark: for now, we can't get there if we are inside a loop.
+    If inside a loop, we use {!translate_return_with_loop}.
+ *)
 and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     (ctx : bs_ctx) : texpression =
   (* There are two cases:
@@ -1676,22 +1690,20 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
      - or we are translating a backward function, in which case it should be [None]
   *)
   (* Compute the values that we should return *without the state and the result
-   * wrapper* *)
+     wrapper* *)
   let output =
     match ctx.bid with
     | None ->
         (* Forward function *)
         let v = Option.get opt_v in
         typed_value_to_texpression ctx ectx v
-    | Some bid ->
+    | Some _ ->
         (* Backward function *)
         (* Sanity check *)
         assert (opt_v = None);
         (* Group the variables in which we stored the values we need to give back.
-         * See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
-        let backward_outputs =
-          T.RegionGroupId.Map.find bid ctx.backward_outputs
-        in
+           See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
+        let backward_outputs = Option.get ctx.backward_outputs in
         let field_values = List.map mk_texpression_from_var backward_outputs in
         mk_simpl_tuple_texpression field_values
   in
@@ -1728,19 +1740,16 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
         (* Forward *)
         mk_texpression_from_var
           (Option.get loop_info.forward_output_no_state_no_result)
-    | Some bid ->
+    | Some _ ->
         (* Backward *)
         (* Group the variables in which we stored the values we need to give back.
          * See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
         let backward_outputs =
-          let map =
-            if ctx.inside_loop then
-              (* We are synthesizing a loop body *)
-              Option.get ctx.loop_backward_outputs
-            else (* Regular function *)
-              ctx.backward_outputs
-          in
-          T.RegionGroupId.Map.find bid map
+          if ctx.inside_loop then
+            (* We are synthesizing a loop body *)
+            Option.get ctx.loop_backward_outputs
+          else (* Regular function *)
+            Option.get ctx.backward_outputs
         in
         let field_values = List.map mk_texpression_from_var backward_outputs in
         mk_simpl_tuple_texpression field_values
@@ -1923,45 +1932,38 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ^ abs_to_string ctx abs ^ "\n"));
 
   (* When we end an input abstraction, this input abstraction gets back
-   * the borrows which it introduced in the context through the input
-   * values: by listing those values, we get the values which are given
-   * back by one of the backward functions we are synthesizing. *)
-  (* Note that we don't support nested borrows for now: if we find
-   * an ended synthesized input abstraction, it must be the one corresponding
-   * to the backward function wer are synthesizing, it can't be the one
-   * for a parent backward function.
-   *)
+     the borrows which it introduced in the context through the input
+     values: by listing those values, we get the values which are given
+     back by one of the backward functions we are synthesizing.
+
+     Note that we don't support nested borrows for now: if we find
+     an ended synthesized input abstraction, it must be the one corresponding
+     to the backward function wer are synthesizing, it can't be the one
+     for a parent backward function.
+  *)
   let bid = Option.get ctx.bid in
   assert (rg_id = bid);
 
-  (* The translation is done as follows:
-     - for a given backward function, we choose a set of variables [v_i]
-     - when we detect the ended input abstraction which corresponds
-       to the backward function, and which consumed the values [consumed_i],
-       we introduce:
-       {[
-           let v_i = consumed_i in
-           ...
-             ]}
-       Then, when we reach the [Return] node, we introduce:
-       {[
-           (v_i)
-       ]}
-  *)
-  (* First, get the given back variables.
+  (* First, introduce the given back variables.
 
      We don't use the same given back variables if we translate a loop or
      the standard body of a function.
   *)
-  let given_back_variables =
-    let map =
-      if ctx.inside_loop then
-        (* We are synthesizing a loop body *)
-        Option.get ctx.loop_backward_outputs
-      else (* Regular function body *)
-        ctx.backward_outputs
-    in
-    T.RegionGroupId.Map.find bid map
+  let ctx, given_back_variables =
+    if ctx.inside_loop then
+      (* We are synthesizing a loop body *)
+      let loop_id = Option.get ctx.loop_id in
+      let loop = LoopId.Map.find loop_id ctx.loops in
+      let tys = RegionGroupId.Map.find bid loop.back_outputs in
+      let vars = List.map (fun ty -> (None, ty)) tys in
+      let ctx, vars = fresh_vars vars ctx in
+      ({ ctx with loop_backward_outputs = Some vars }, vars)
+    else
+      (* Regular function body *)
+      let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in
+      let vars = List.combine back_sg.output_names back_sg.outputs in
+      let ctx, vars = fresh_vars vars ctx in
+      ({ ctx with backward_outputs = Some vars }, vars)
   in
 
   (* Get the list of values consumed by the abstraction upon ending *)
@@ -2943,22 +2945,15 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
 
   (* Compute the backward outputs *)
   let ctx = ref ctx in
-  let loop_backward_outputs =
+  let rg_to_given_back_tys =
     T.RegionGroupId.Map.map
       (fun (_, tys) ->
         (* The types shouldn't contain borrows - we can translate them as forward types *)
-        let vars =
-          List.map
-            (fun ty ->
-              assert (
-                not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty));
-              (None, ctx_translate_fwd_ty !ctx ty))
-            tys
-        in
-        (* Introduce fresh variables *)
-        let ctx', vars = fresh_vars vars !ctx in
-        ctx := ctx';
-        vars)
+        List.map
+          (fun ty ->
+            assert (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty));
+            ctx_translate_fwd_ty !ctx ty)
+          tys)
       loop.rg_to_given_back_tys
   in
   let ctx = !ctx in
@@ -2966,12 +2961,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let back_output_tys =
     match ctx.bid with
     | None -> None
-    | Some rg_id ->
-        let back_outputs =
-          T.RegionGroupId.Map.find rg_id loop_backward_outputs
-        in
-        let back_output_tys = List.map (fun (v : var) -> v.ty) back_outputs in
-        Some back_output_tys
+    | Some rg_id -> Some (T.RegionGroupId.Map.find rg_id rg_to_given_back_tys)
   in
 
   (* Add the loop information in the context *)
@@ -3013,6 +3003,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         generics;
         forward_inputs = None;
         forward_output_no_state_no_result = None;
+        back_outputs = rg_to_given_back_tys;
       }
     in
     let loops = LoopId.Map.add loop_id loop_info ctx.loops in
@@ -3020,13 +3011,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   in
 
   (* Update the context to translate the function end *)
-  let ctx_end =
-    {
-      ctx with
-      loop_id = Some loop_id;
-      loop_backward_outputs = Some loop_backward_outputs;
-    }
-  in
+  let ctx_end = { ctx with loop_id = Some loop_id } in
   let fun_end = translate_expression loop.end_expr ctx_end in
 
   (* Update the context for the loop body *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index e153f4f4..0fa0202b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -171,8 +171,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       backward_inputs_no_state = RegionGroupId.Map.empty;
       (* Initialized just below *)
       backward_inputs_with_state = RegionGroupId.Map.empty;
-      (* Initialized just below *)
-      backward_outputs = RegionGroupId.Map.empty;
+      backward_outputs = None;
       loop_backward_outputs = None;
       (* Empty for now *)
       calls;
@@ -234,20 +233,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   in
   let ctx = { ctx with backward_inputs_no_state; backward_inputs_with_state } in
 
-  (* Add the backward outputs *)
-  let ctx, backward_outputs =
-    List.fold_left_map
-      (fun ctx (region_vars : region_var_group) ->
-        let gid = region_vars.id in
-        let back_sg = RegionGroupId.Map.find gid sg.back_sg in
-        let outputs = List.combine back_sg.output_names back_sg.outputs in
-        let ctx, vars = SymbolicToPure.fresh_vars outputs ctx in
-        (ctx, (gid, vars)))
-      ctx regions_hierarchy
-  in
-  let backward_outputs = RegionGroupId.Map.of_list backward_outputs in
-  let ctx = { ctx with backward_outputs } in
-
   (* Translate the forward function *)
   let pure_forward =
     match symbolic_trans with
-- 
cgit v1.3.1


From 014c0668abf0834342b2b7076cf2f0634460e519 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Dec 2023 13:24:53 +0100
Subject: Remove SymbolicToPure.bs_ctx.loop_backward_outputs

---
 compiler/SymbolicToPure.ml | 47 +++++++++++++++-------------------------------
 compiler/Translate.ml      |  1 -
 2 files changed, 15 insertions(+), 33 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 93e6cb4e..e2787271 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -213,17 +213,6 @@ type bs_ctx = {
           The option is [None] before we detect the ended input abstraction,
           and [Some] afterwards.
        *)
-  loop_backward_outputs : var list option;
-      (** Same as {!backward_outputs}, but for loops (if we entered a loop).
-
-          TODO: merge with [backward_outputs]?
-
-          [None] if we are not inside a loop, [Some] otherwise (and whatever
-          the kind of function we are translating: it will be [Some] even
-          though we are synthesizing a forward function).
-
-          TODO: move to {!loop_info}
-       *)
   calls : call_info V.FunCallId.Map.t;
       (** The function calls we encountered so far *)
   abstractions : (V.abs * texpression list) V.AbstractionId.Map.t;
@@ -1744,13 +1733,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
         (* Backward *)
         (* Group the variables in which we stored the values we need to give back.
          * See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
-        let backward_outputs =
-          if ctx.inside_loop then
-            (* We are synthesizing a loop body *)
-            Option.get ctx.loop_backward_outputs
-          else (* Regular function *)
-            Option.get ctx.backward_outputs
-        in
+        let backward_outputs = Option.get ctx.backward_outputs in
         let field_values = List.map mk_texpression_from_var backward_outputs in
         mk_simpl_tuple_texpression field_values
   in
@@ -1950,20 +1933,20 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
      the standard body of a function.
   *)
   let ctx, given_back_variables =
-    if ctx.inside_loop then
-      (* We are synthesizing a loop body *)
-      let loop_id = Option.get ctx.loop_id in
-      let loop = LoopId.Map.find loop_id ctx.loops in
-      let tys = RegionGroupId.Map.find bid loop.back_outputs in
-      let vars = List.map (fun ty -> (None, ty)) tys in
-      let ctx, vars = fresh_vars vars ctx in
-      ({ ctx with loop_backward_outputs = Some vars }, vars)
-    else
-      (* Regular function body *)
-      let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in
-      let vars = List.combine back_sg.output_names back_sg.outputs in
-      let ctx, vars = fresh_vars vars ctx in
-      ({ ctx with backward_outputs = Some vars }, vars)
+    let vars =
+      if ctx.inside_loop then
+        (* We are synthesizing a loop body *)
+        let loop_id = Option.get ctx.loop_id in
+        let loop = LoopId.Map.find loop_id ctx.loops in
+        let tys = RegionGroupId.Map.find bid loop.back_outputs in
+        List.map (fun ty -> (None, ty)) tys
+      else
+        (* Regular function body *)
+        let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in
+        List.combine back_sg.output_names back_sg.outputs
+    in
+    let ctx, vars = fresh_vars vars ctx in
+    ({ ctx with backward_outputs = Some vars }, vars)
   in
 
   (* Get the list of values consumed by the abstraction upon ending *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0fa0202b..631a5af9 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -172,7 +172,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       (* Initialized just below *)
       backward_inputs_with_state = RegionGroupId.Map.empty;
       backward_outputs = None;
-      loop_backward_outputs = None;
       (* Empty for now *)
       calls;
       abstractions;
-- 
cgit v1.3.1


From 8835d87df111d09122267fadc9a32f16b52d234a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 14:37:43 +0100
Subject: Make good progress on merging the fwd/back functions

---
 compiler/Config.ml                |   2 +-
 compiler/Extract.ml               |   4 +-
 compiler/InterpreterStatements.ml |  47 ++++---
 compiler/PureUtils.ml             |  19 ++-
 compiler/SymbolicAst.ml           |   4 +
 compiler/SymbolicToPure.ml        | 266 ++++++++++++++++++++++++++++++--------
 compiler/SynthesizeSymbolic.ml    |  16 ++-
 compiler/Translate.ml             |   3 +-
 8 files changed, 274 insertions(+), 87 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index c8f3ed58..b8af6c6d 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -153,7 +153,7 @@ let loop_fixed_point_max_num_iters = 2
                return (x :: ls)))
     ]}
  *)
-let return_back_funs = ref false
+let return_back_funs = ref true
 
 (** Forbids using field projectors for structures.
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 3429cd11..46cf8c4a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1332,7 +1332,9 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     in
     let fwd_back_comment =
       match def.back_id with
-      | None -> [ "forward function" ]
+      | None ->
+          if !Config.return_back_funs then [ "function definition" ]
+          else [ "forward function" ]
       | Some id ->
           (* Check if there is only one backward function, and no forward function *)
           if (not keep_fwd) && num_backs = 1 then
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index da617c64..94c65b5c 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -728,7 +728,12 @@ let create_push_abstractions_from_abs_region_groups
     to a trait clause but directly to the method provided in the trait declaration.
  *)
 let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
-    : fun_id_or_trait_method_ref * generic_args * fun_decl * inst_fun_sig =
+    :
+    fun_id_or_trait_method_ref
+    * generic_args
+    * fun_decl
+    * region_var_groups
+    * inst_fun_sig =
   match call.func with
   | FnOpMove _ ->
       (* Closure case: TODO *)
@@ -753,7 +758,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
             instantiate_fun_sig ctx func.generics tr_self def.signature
               regions_hierarchy
           in
-          (func.func, func.generics, def, inst_sg)
+          (func.func, func.generics, def, regions_hierarchy, inst_sg)
       | FunId (FAssumed _) ->
           (* Unreachable: must be a transparent function *)
           raise (Failure "Unreachable")
@@ -806,7 +811,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
                      we also need to update the generics.
                   *)
                   let func = FunId fid in
-                  (func, generics, method_def, inst_sg)
+                  (func, generics, method_def, regions_hierarchy, inst_sg)
               | None ->
                   (* If not found, lookup the methods provided by the trait *declaration*
                      (remember: for now, we forbid overriding provided methods) *)
@@ -860,7 +865,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
                     instantiate_fun_sig ctx all_generics tr_self
                       method_def.signature regions_hierarchy
                   in
-                  (func.func, func.generics, method_def, inst_sg))
+                  ( func.func,
+                    func.generics,
+                    method_def,
+                    regions_hierarchy,
+                    inst_sg ))
           | _ ->
               (* We are using a local clause - we lookup the trait decl *)
               let trait_decl =
@@ -891,7 +900,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
                 instantiate_fun_sig ctx generics tr_self method_def.signature
                   regions_hierarchy
               in
-              (func.func, func.generics, method_def, inst_sg)))
+              (func.func, func.generics, method_def, regions_hierarchy, inst_sg)
+          ))
 
 (** Evaluate a statement *)
 let rec eval_statement (config : config) (st : statement) : st_cm_fun =
@@ -1277,14 +1287,14 @@ and eval_transparent_function_call_concrete (config : config)
 and eval_transparent_function_call_symbolic (config : config) (call : call) :
     st_cm_fun =
  fun cf ctx ->
-  let func, generics, def, inst_sg =
+  let func, generics, def, regions_hierarchy, inst_sg =
     eval_transparent_function_call_symbolic_inst call ctx
   in
   (* Sanity check *)
   assert (List.length call.args = List.length def.signature.inputs);
   (* Evaluate the function call *)
-  eval_function_call_symbolic_from_inst_sig config func inst_sg generics
-    call.args call.dest cf ctx
+  eval_function_call_symbolic_from_inst_sig config func def.signature
+    regions_hierarchy inst_sg generics call.args call.dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1298,7 +1308,8 @@ and eval_transparent_function_call_symbolic (config : config) (call : call) :
     trait ref as input.
  *)
 and eval_function_call_symbolic_from_inst_sig (config : config)
-    (fid : fun_id_or_trait_method_ref) (inst_sg : inst_fun_sig)
+    (fid : fun_id_or_trait_method_ref) (sg : fun_sig)
+    (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig)
     (generics : generic_args) (args : operand list) (dest : place) : st_cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -1378,8 +1389,8 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
     let expr = cf ctx in
 
     (* Synthesize the symbolic AST *)
-    S.synthesize_regular_function_call fid call_id ctx abs_ids generics args
-      args_places ret_spc dest_place expr
+    S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy
+      abs_ids generics args args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
 
@@ -1468,7 +1479,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
       (* In symbolic mode, the behaviour of a function call is completely defined
        * by the signature of the function: we thus simply generate correctly
        * instantiated signatures, and delegate the work to an auxiliary function *)
-      let inst_sig =
+      let sg, regions_hierarchy, inst_sig =
         match fid with
         | BoxFree ->
             (* Should have been treated above *)
@@ -1480,14 +1491,16 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
             in
             (* There shouldn't be any reference to Self *)
             let tr_self = UnknownTrait __FUNCTION__ in
-            instantiate_fun_sig ctx generics tr_self
-              (Assumed.get_assumed_fun_sig fid)
-              regions_hierarchy
+            let sg = Assumed.get_assumed_fun_sig fid in
+            let inst_sg =
+              instantiate_fun_sig ctx generics tr_self sg regions_hierarchy
+            in
+            (sg, regions_hierarchy, inst_sg)
       in
 
       (* Evaluate the function call *)
-      eval_function_call_symbolic_from_inst_sig config (FunId (FAssumed fid))
-        inst_sig generics args dest cf ctx
+      eval_function_call_symbolic_from_inst_sig config (FunId (FAssumed fid)) sg
+        regions_hierarchy inst_sig generics args dest cf ctx
 
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : config) (body : statement) : st_cm_fun =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6e86578c..6579e84c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -321,14 +321,23 @@ let destruct_apps (e : texpression) : texpression * texpression list =
 
 (** Make an [App (app, arg)] expression *)
 let mk_app (app : texpression) (arg : texpression) : texpression =
+  let raise_or_return msg =
+    if !Config.fail_hard then raise (Failure msg)
+    else
+      let e = App (app, arg) in
+      (* Dummy type - TODO: introduce an error type *)
+      let ty = app.ty in
+      { e; ty }
+  in
   match app.ty with
   | TArrow (ty0, ty1) ->
       (* Sanity check *)
-      assert (ty0 = arg.ty);
-      let e = App (app, arg) in
-      let ty = ty1 in
-      { e; ty }
-  | _ -> raise (Failure "Expected an arrow type")
+      if ty0 <> arg.ty then raise_or_return "App: wrong input type"
+      else
+        let e = App (app, arg) in
+        let ty = ty1 in
+        { e; ty }
+  | _ -> raise_or_return "Expected an arrow type"
 
 (** The reverse of {!destruct_apps} *)
 let mk_apps (app : texpression) (args : texpression list) : texpression =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 53f99b7f..54d207d9 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -42,7 +42,11 @@ type call = {
           evaluated). We need it to compute the translated values for shared
           borrows (we need to perform lookups).
        *)
+  sg : fun_sig option;
+      (** The uninstantiated function signature, if this is not a unop/binop *)
+  regions_hierarchy : region_var_groups;
   abstractions : AbstractionId.id list;
+      (** The region abstractions introduced upon calling the function *)
   generics : generic_args;
   args : typed_value list;
   args_places : mplace option list;  (** Meta information *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e2787271..1ce6c698 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -67,6 +67,18 @@ type call_info = {
 
           Those inputs include the fuel and the state, if pertinent.
        *)
+  back_funs : texpression RegionGroupId.Map.t option;
+      (** If we do not split between the forward/backward functions: the
+          variables we introduced for the backward functions.
+
+          Example:
+          {[
+            let x, back = Vec.index_mut n v in
+                   ^^^^
+                   here
+            ...
+          ]}
+       *)
 }
 [@@deriving show]
 
@@ -118,6 +130,8 @@ type loop_info = {
 
 (** Body synthesis context *)
 type bs_ctx = {
+  (* TODO: there are a lot of duplications with the various decls ctx *)
+  decls_ctx : C.decls_ctx;
   type_ctx : type_ctx;
   fun_ctx : fun_ctx;
   global_ctx : global_ctx;
@@ -757,17 +771,27 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
       TraitMethod (trait_ref, method_name, fun_decl_id)
 
 let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
-    (args : texpression list) (ctx : bs_ctx) : bs_ctx =
+    (args : texpression list)
+    (back_funs : texpression RegionGroupId.Map.t option) (ctx : bs_ctx) : bs_ctx
+    =
   let calls = ctx.calls in
   assert (not (V.FunCallId.Map.mem call_id calls));
-  let info = { forward; forward_inputs = args } in
+  let info = { forward; forward_inputs = args; back_funs } in
   let calls = V.FunCallId.Map.add call_id info calls in
   { ctx with calls }
 
-(** [back_args]: the *additional* list of inputs received by the backward function *)
-let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
-    (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx)
-    : bs_ctx * fun_or_op_id =
+(** [inherit_args]: the list of inputs inherited from the forward function and
+    the ancestors backward functions, if pertinent.
+    [back_args]: the *additional* list of inputs received by the backward function,
+    including the state.
+
+    Returns the updated context and the expression corresponding to the function.
+ *)
+let bs_ctx_register_backward_call (abs : V.abs) (effect_info : fun_effect_info)
+    (call_id : V.FunCallId.id) (back_id : T.RegionGroupId.id)
+    (inherited_args : texpression list) (back_args : texpression list)
+    (generics : generic_args) (output_ty : ty) (ctx : bs_ctx) :
+    bs_ctx * texpression =
   (* Insert the abstraction in the call informations *)
   let info = V.FunCallId.Map.find call_id ctx.calls in
   let calls = V.FunCallId.Map.add call_id info ctx.calls in
@@ -777,16 +801,31 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
   let abstractions =
     V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
   in
-  (* Retrieve the fun_id *)
-  let fun_id =
-    match info.forward.call_id with
-    | S.Fun (fid, _) ->
-        let fid = translate_fun_id_or_trait_method_ref ctx fid in
-        Fun (FromLlbc (fid, None, Some back_id))
-    | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
+  (* Compute the expression corresponding to the function *)
+  let func =
+    if !Config.return_back_funs then
+      (* Lookup the variable introduced for the backward function *)
+      RegionGroupId.Map.find back_id (Option.get info.back_funs)
+    else
+      (* Retrieve the fun_id *)
+      let fun_id =
+        match info.forward.call_id with
+        | S.Fun (fid, _) ->
+            let fid = translate_fun_id_or_trait_method_ref ctx fid in
+            Fun (FromLlbc (fid, None, Some back_id))
+        | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
+      in
+      let args = List.append inherited_args back_args in
+      let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
+      let ret_ty =
+        if effect_info.can_fail then mk_result_ty output_ty else output_ty
+      in
+      let func_ty = mk_arrows input_tys ret_ty in
+      let func = { id = FunOrOp fun_id; generics } in
+      { e = Qualif func; ty = func_ty }
   in
   (* Update the context and return *)
-  ({ ctx with calls; abstractions }, fun_id)
+  ({ ctx with calls; abstractions }, func)
 
 (** List the ancestors of an abstraction *)
 let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
@@ -878,15 +917,12 @@ let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
     We use [bid] ("backward function id") only if we split the forward
     and the backward functions.
  *)
-let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
-    (fun_id : A.fun_id) (sg : A.fun_sig) (input_names : string option list) :
-    decomposed_fun_sig =
+let translate_fun_sig_with_regions_hierarchy_to_decomposed
+    (decls_ctx : C.decls_ctx) (fun_id : A.fun_id_or_trait_method_ref)
+    (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig)
+    (input_names : string option list) : decomposed_fun_sig =
   let fun_infos = decls_ctx.fun_ctx.fun_infos in
   let type_infos = decls_ctx.type_ctx.type_infos in
-  (* Retrieve the list of parent backward functions *)
-  let regions_hierarchy =
-    FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
-  in
   (* We need an evaluation context to normalize the types (to normalize the
      associated types, etc. - for instance it may happen that the types
      refer to the types associated to a trait ref, but where the trait ref
@@ -915,9 +951,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
   in
 
   (* Is the forward function stateful, and can it fail? *)
-  let fwd_effect_info =
-    get_fun_effect_info fun_infos (FunId fun_id) None None
-  in
+  let fwd_effect_info = get_fun_effect_info fun_infos fun_id None None in
   (* Compute the forward inputs *)
   let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in
   let fwd_inputs_no_fuel_no_state =
@@ -1030,7 +1064,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
       RegionGroupId.id * back_sg_info =
     let gid = rg.id in
     let back_effect_info =
-      get_fun_effect_info fun_infos (FunId fun_id) None (Some gid)
+      get_fun_effect_info fun_infos fun_id None (Some gid)
     in
     let inputs_no_state = translate_back_inputs_for_gid gid in
     let inputs_no_state =
@@ -1072,6 +1106,16 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
     fwd_info;
   }
 
+let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
+    (fun_id : FunDeclId.id) (sg : A.fun_sig) (input_names : string option list)
+    : decomposed_fun_sig =
+  (* Retrieve the list of parent backward functions *)
+  let regions_hierarchy =
+    FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies
+  in
+  translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx
+    (FunId (FRegular fun_id)) regions_hierarchy sg input_names
+
 let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty
     =
   let output =
@@ -1090,6 +1134,40 @@ let compute_back_tys (dsg : Pure.decomposed_fun_sig) : ty list =
       mk_arrows inputs output)
     (RegionGroupId.Map.values dsg.back_sg)
 
+(** Return the pure signature of a backward function, in the case the
+    forward/backward functions are merged (i.e., the forward functions
+    return the backward functions).
+
+    TODO: merge with {!translate_fun_sig_from_decomposed}
+ *)
+let translate_ret_back_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
+    (gid : RegionGroupId.id) : fun_sig =
+  assert !Config.return_back_funs;
+
+  let generics = dsg.generics in
+  let llbc_generics = dsg.llbc_generics in
+  let preds = dsg.preds in
+  (* Compute the effects info *)
+  let fwd_info = dsg.fwd_info in
+  let back_effect_info =
+    RegionGroupId.Map.of_list
+      (List.map
+         (fun ((gid, info) : RegionGroupId.id * back_sg_info) ->
+           (gid, info.effect_info))
+         (RegionGroupId.Map.bindings dsg.back_sg))
+  in
+  (* Two cases depending on whether we split the forward/backward functions
+     or not *)
+  let mk_output_ty = mk_output_ty_from_effect_info in
+
+  let back_sg = RegionGroupId.Map.find gid dsg.back_sg in
+  let effect_info = back_sg.effect_info in
+  (* Do not prepend the forward inputs *)
+  let inputs = List.map snd back_sg.inputs in
+  let output = mk_simpl_tuple_ty back_sg.outputs in
+  let output = mk_output_ty effect_info output in
+  { generics; llbc_generics; preds; inputs; output; fwd_info; back_effect_info }
+
 let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
     (gid : RegionGroupId.id option) : fun_sig =
   let generics = dsg.generics in
@@ -1774,7 +1852,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
   (* Retrieve the function id, and register the function call in the context
    * if necessary. *)
-  let ctx, fun_id, effect_info, args, out_state =
+  let ctx, fun_id, effect_info, args, back_funs, out_state =
     match call.call_id with
     | S.Fun (fid, call_id) ->
         (* Regular function call *)
@@ -1798,9 +1876,80 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             (List.concat [ fuel; args; [ state_var ] ], ctx, Some nstate_var)
           else (List.concat [ fuel; args ], ctx, None)
         in
+        (* If we do not split the forward/backward functions: generate the
+           variables for the backward functions returned by the forward
+           function. *)
+        let ctx, back_funs_map, back_funs =
+          if !Config.return_back_funs then
+            (* We need to compute the signatures of the backward functions. *)
+            let sg = Option.get call.sg in
+            let decls_ctx = ctx.decls_ctx in
+            let dsg =
+              translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx
+                fid call.regions_hierarchy sg
+                (List.map (fun _ -> None) sg.inputs)
+            in
+            let gids =
+              List.map
+                (fun (g : T.region_var_group) -> g.id)
+                call.regions_hierarchy
+            in
+            let back_sgs =
+              List.map (translate_ret_back_fun_sig_from_decomposed dsg) gids
+            in
+            (* Introduce variables for the backward functions *)
+            let back_tys =
+              List.map
+                (fun (sg : fun_sig) -> mk_arrows sg.inputs sg.output)
+                back_sgs
+            in
+            (* Compute a proper basename for the variables *)
+            let back_fun_name =
+              let name =
+                match fid with
+                | FunId (FAssumed fid) -> (
+                    match fid with
+                    | BoxNew -> "box_new"
+                    | BoxFree -> "box_free"
+                    | ArrayRepeat -> "array_repeat"
+                    | ArrayIndexShared -> "index_shared"
+                    | ArrayIndexMut -> "index_mut"
+                    | ArrayToSliceShared -> "to_slice_shared"
+                    | ArrayToSliceMut -> "to_slice_mut"
+                    | SliceIndexShared -> "index_shared"
+                    | SliceIndexMut -> "index_mut")
+                | FunId (FRegular fid) | TraitMethod (_, _, fid) -> (
+                    let decl =
+                      FunDeclId.Map.find fid ctx.fun_ctx.llbc_fun_decls
+                    in
+                    match Collections.List.last decl.name with
+                    | PeIdent (s, _) -> s
+                    | PeImpl _ ->
+                        (* We shouldn't get there *)
+                        raise (Failure "Unexpected"))
+              in
+              name ^ "_back"
+            in
+            let ctx, back_vars =
+              fresh_vars
+                (List.map (fun ty -> (Some back_fun_name, ty)) back_tys)
+                ctx
+            in
+            let back_funs =
+              List.map (fun v -> mk_typed_pattern_from_var v None) back_vars
+            in
+            let back_funs_map =
+              RegionGroupId.Map.of_list
+                (List.combine gids (List.map mk_texpression_from_var back_vars))
+            in
+            (ctx, Some back_funs_map, back_funs)
+          else (ctx, None, [])
+        in
         (* Register the function call *)
-        let ctx = bs_ctx_register_forward_call call_id call args ctx in
-        (ctx, func, effect_info, args, out_state)
+        let ctx =
+          bs_ctx_register_forward_call call_id call args back_funs_map ctx
+        in
+        (ctx, func, effect_info, args, back_funs, out_state)
     | S.Unop E.Not ->
         let effect_info =
           {
@@ -1811,7 +1960,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             is_rec = false;
           }
         in
-        (ctx, Unop Not, effect_info, args, None)
+        (ctx, Unop Not, effect_info, args, [], None)
     | S.Unop E.Neg -> (
         match args with
         | [ arg ] ->
@@ -1827,7 +1976,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Unop (Neg int_ty), effect_info, args, None)
+            (ctx, Unop (Neg int_ty), effect_info, args, [], None)
         | _ -> raise (Failure "Unreachable"))
     | S.Unop (E.Cast cast_kind) -> (
         match cast_kind with
@@ -1842,7 +1991,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
+            (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, [], None)
         | CastFnPtr _ -> raise (Failure "TODO: function casts"))
     | S.Binop binop -> (
         match args with
@@ -1862,11 +2011,12 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Binop (binop, int_ty0), effect_info, args, None)
+            (ctx, Binop (binop, int_ty0), effect_info, args, [], None)
         | _ -> raise (Failure "Unreachable"))
   in
   let dest_v =
     let dest = mk_typed_pattern_from_var dest dest_mplace in
+    let dest = mk_simpl_tuple_pattern (dest :: back_funs) in
     match out_state with
     | None -> dest
     | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
@@ -2026,9 +2176,11 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     else ([], ctx, None)
   in
   (* Concatenate all the inpus *)
-  let inputs =
-    List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs; back_state ]
+  let inherited_inputs =
+    if !Config.return_back_funs then []
+    else List.concat [ fwd_inputs; back_ancestors_inputs ]
   in
+  let back_inputs = List.append back_inputs back_state in
   (* Retrieve the values given back by this function: those are the output
    * values. We rely on the fact that there are no nested borrows to use the
    * meta-place information from the input values given to the forward function
@@ -2046,43 +2198,43 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ]
   in
   (* Retrieve the function id, and register the function call in the context
-   * if necessary *)
+     if necessary.Arith_status *)
   let ctx, func =
-    bs_ctx_register_backward_call abs call_id rg_id back_inputs ctx
+    bs_ctx_register_backward_call abs effect_info call_id rg_id inherited_inputs
+      back_inputs generics output.ty ctx
   in
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
   (* Put everything together *)
+  let inputs = List.append inherited_inputs back_inputs in
   let args_mplaces = List.map (fun _ -> None) inputs in
   let args =
     List.map
       (fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
       (List.combine inputs args_mplaces)
   in
-  let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
-  let ret_ty =
-    if effect_info.can_fail then mk_result_ty output.ty else output.ty
-  in
-  let func_ty = mk_arrows input_tys ret_ty in
-  let func = { id = FunOrOp func; generics } in
-  let func = { e = Qualif func; ty = func_ty } in
   let call = mk_apps func args in
   (* **Optimization**:
-   * =================
-   * We do a small optimization here: if the backward function doesn't
-   * have any output, we don't introduce any function call.
-   * See the comment in {!Config.filter_useless_monadic_calls}.
-   *
-   * TODO: use an option to disallow backward functions from updating the state.
-   * TODO: a backward function which only gives back shared borrows shouldn't
-   * update the state (state updates should only be used for mutable borrows,
-   * with objects like Rc for instance).
-   *)
-  if !Config.filter_useless_monadic_calls && outputs = [] && nstate = None then (
+     =================
+     We do a small optimization here if we split the forward/backward functions.
+     If the backward function doesn't have any output, we don't introduce any function
+     call.
+     See the comment in {!Config.filter_useless_monadic_calls}.
+
+     TODO: use an option to disallow backward functions from updating the state.
+     TODO: a backward function which only gives back shared borrows shouldn't
+     update the state (state updates should only be used for mutable borrows,
+     with objects like Rc for instance).
+  *)
+  if
+    (not !Config.return_back_funs)
+    && !Config.filter_useless_monadic_calls
+    && outputs = [] && nstate = None
+  then (
     (* No outputs - we do a small sanity check: the backward function
-     * should have exactly the same number of inputs as the forward:
-     * this number can be different only if the forward function returned
-     * a value containing mutable borrows, which can't be the case... *)
+       should have exactly the same number of inputs as the forward:
+       this number can be different only if the forward function returned
+       a value containing mutable borrows, which can't be the case... *)
     assert (List.length inputs = List.length fwd_inputs);
     next_e)
   else mk_let effect_info.can_fail output call next_e
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index efcf001a..4ec7524b 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -2,6 +2,7 @@ open Types
 open TypesUtils
 open Expressions
 open Values
+open LlbcAst
 open SymbolicAst
 
 let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace =
@@ -92,6 +93,7 @@ let synthesize_symbolic_expansion_no_branching (sv : symbolic_value)
   synthesize_symbolic_expansion sv place [ Some see ] el
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
+    (sg : fun_sig option) (regions_hierarchy : region_var_groups)
     (abstractions : AbstractionId.id list) (generics : generic_args)
     (args : typed_value list) (args_places : mplace option list)
     (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
@@ -102,6 +104,8 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
         {
           call_id;
           ctx;
+          sg;
+          regions_hierarchy;
           abstractions;
           generics;
           args;
@@ -118,28 +122,30 @@ let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value)
   Option.map (fun e -> EvalGlobal (gid, dest, e)) e
 
 let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
-    (call_id : FunCallId.id) (ctx : Contexts.eval_ctx)
+    (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig)
+    (regions_hierarchy : region_var_groups)
     (abstractions : AbstractionId.id list) (generics : generic_args)
     (args : typed_value list) (args_places : mplace option list)
     (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
     : expression option =
   synthesize_function_call
     (Fun (fun_id, call_id))
-    ctx abstractions generics args args_places dest dest_place e
+    ctx (Some sg) regions_hierarchy abstractions generics args args_places dest
+    dest_place e
 
 let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop)
     (arg : typed_value) (arg_place : mplace option) (dest : symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
   let generics = empty_generic_args in
-  synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ]
-    dest dest_place e
+  synthesize_function_call (Unop unop) ctx None [] [] generics [ arg ]
+    [ arg_place ] dest dest_place e
 
 let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : binop)
     (arg0 : typed_value) (arg0_place : mplace option) (arg1 : typed_value)
     (arg1_place : mplace option) (dest : symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
   let generics = empty_generic_args in
-  synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ]
+  synthesize_function_call (Binop binop) ctx None [] [] generics [ arg0; arg1 ]
     [ arg0_place; arg1_place ] dest dest_place e
 
 let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : abs)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 631a5af9..5584fb9a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -129,7 +129,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   in
 
   let sg =
-    SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx (FRegular def_id)
+    SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx def_id
       fdef.signature input_names
   in
 
@@ -151,6 +151,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
   let ctx =
     {
+      decls_ctx = trans_ctx;
       SymbolicToPure.bid = None;
       sg;
       (* Will need to be updated for the backward functions *)
-- 
cgit v1.3.1


From 266db04e97778911c93cfd1aac251de04bb25f53 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 22:17:11 +0100
Subject: Fix several issues

---
 compiler/Pure.ml           |  17 -----
 compiler/SymbolicToPure.ml | 186 ++++++++++++++++++++++++++++++++-------------
 compiler/Translate.ml      |  29 +++----
 3 files changed, 151 insertions(+), 81 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 05cdbd70..71531688 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -886,23 +886,6 @@ type inputs_info = {
 }
 [@@deriving show]
 
-type ('a, 'b) back_info =
-  | SingleBack of 'a
-      (** Information about a single backward function, if pertinent.
-
-          We use this variant if we split the forward and the backward functions.
-       *)
-  | AllBacks of 'b RegionGroupId.Map.t
-      (** Information about the various backward functions.
-
-          We use this if we *do not* split the forward and the backward functions.
-          All the information is then carried by the forward function.
-       *)
-[@@deriving show]
-
-type back_inputs_info = (inputs_info option, inputs_info) back_info
-[@@deriving show]
-
 (** Meta information about a function signature *)
 type fun_sig_info = {
   fwd_info : inputs_info;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 70a4e18d..37f621e4 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -146,6 +146,7 @@ type bs_ctx = {
   global_ctx : global_ctx;
   trait_decls_ctx : trait_decls_ctx;
   trait_impls_ctx : trait_impls_ctx;
+  fun_dsigs : decomposed_fun_sig FunDeclId.Map.t;
   fun_decl : A.fun_decl;
   bid : RegionGroupId.id option;
       (** TODO: rename
@@ -890,7 +891,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
   if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
 
 (** Small utility. *)
-let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
+let compute_raw_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
@@ -917,6 +918,22 @@ let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
         is_rec = false;
       }
 
+(** TODO: not very clean. *)
+let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
+    (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) :
+    fun_effect_info =
+  match fun_id with
+  | TraitMethod (_, _, fid) | FunId (FRegular fid) ->
+      let dsg = A.FunDeclId.Map.find fid ctx.fun_dsigs in
+      let info =
+        match gid with
+        | None -> dsg.fwd_info.effect_info
+        | Some gid -> (RegionGroupId.Map.find gid dsg.back_sg).effect_info
+      in
+      { info with is_rec = info.is_rec || Option.is_some lid }
+  | FunId (FAssumed _) ->
+      compute_raw_fun_effect_info ctx.fun_ctx.fun_infos fun_id lid gid
+
 (** Translate a function signature to a decomposed function signature.
 
     Note that the function also takes a list of names for the inputs, and
@@ -962,7 +979,9 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
   in
 
   (* Is the forward function stateful, and can it fail? *)
-  let fwd_effect_info = get_fun_effect_info fun_infos fun_id None None in
+  let fwd_effect_info =
+    compute_raw_fun_effect_info fun_infos fun_id None None
+  in
   (* Compute the forward inputs *)
   let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in
   let fwd_inputs_no_fuel_no_state =
@@ -1051,12 +1070,23 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
       RegionGroupId.id * back_sg_info =
     let gid = rg.id in
     let back_effect_info =
-      get_fun_effect_info fun_infos fun_id None (Some gid)
+      compute_raw_fun_effect_info fun_infos fun_id None (Some gid)
     in
     let inputs_no_state = translate_back_inputs_for_gid gid in
     let inputs_no_state =
       List.map (fun ty -> (Some "ret", ty)) inputs_no_state
     in
+    (* We consider the backward function as stateful and potentially failing
+       **only if it has inputs** (for the "potentially failing": if it has
+       not inputs, we directly evaluate it in the body of the forward function).
+    *)
+    let back_effect_info =
+      {
+        back_effect_info with
+        stateful = back_effect_info.stateful && inputs_no_state <> [];
+        can_fail = back_effect_info.can_fail && inputs_no_state <> [];
+      }
+    in
     let state =
       if back_effect_info.stateful then [ (None, mk_state_ty) ] else []
     in
@@ -1140,6 +1170,19 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
   translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx
     (FunId (FRegular fun_id)) regions_hierarchy sg input_names
 
+let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx)
+    (fdef : LlbcAst.fun_decl) : decomposed_fun_sig =
+  let input_names =
+    match fdef.body with
+    | None -> List.map (fun _ -> None) fdef.signature.inputs
+    | Some body ->
+        List.map
+          (fun (v : LlbcAst.var) -> v.name)
+          (LlbcAstUtils.fun_body_get_input_vars body)
+  in
+  translate_fun_sig_to_decomposed decls_ctx fdef.def_id fdef.signature
+    input_names
+
 let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty
     =
   let output =
@@ -1158,8 +1201,9 @@ let mk_back_output_ty_from_effect_info (effect_info : fun_effect_info)
 
     If a backward function has no inputs/outputs we filter it.
  *)
-let compute_back_tys (dsg : Pure.decomposed_fun_sig)
-    (subst : (generic_args * trait_instance_id) option) : ty option list =
+let compute_back_tys_with_info (dsg : Pure.decomposed_fun_sig)
+    (subst : (generic_args * trait_instance_id) option) :
+    (back_sg_info * ty) option list =
   List.map
     (fun (back_sg : back_sg_info) ->
       let effect_info = back_sg.effect_info in
@@ -1185,9 +1229,13 @@ let compute_back_tys (dsg : Pure.decomposed_fun_sig)
               in
               ty_substitute subst ty
         in
-        Some ty)
+        Some (back_sg, ty))
     (RegionGroupId.Map.values dsg.back_sg)
 
+let compute_back_tys (dsg : Pure.decomposed_fun_sig)
+    (subst : (generic_args * trait_instance_id) option) : ty option list =
+  List.map (Option.map snd) (compute_back_tys_with_info dsg subst)
+
 (** In case we merge the fwd/back functions: compute the output type of
     a function, from a decomposed signature. *)
 let compute_output_ty_from_decomposed (dsg : Pure.decomposed_fun_sig) : ty =
@@ -1363,6 +1411,7 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) : bs_ctx * var option list =
   in
   fresh_opt_vars back_vars ctx
 
+(** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *)
 let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
   match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with
   | Some v -> v
@@ -1381,12 +1430,22 @@ let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
       | _ -> raise (Failure "Unreachable"))
   | _ -> v
 
-(** Translate a symbolic value *)
+(** Translate a symbolic value.
+
+    Because we do not necessarily introduce variables for the symbolic values
+    of (translated) type unit, it is important that we do not lookup variables
+    in case the symbolic value has type unit.
+ *)
 let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) :
     texpression =
   (* Translate the type *)
-  let var = lookup_var_for_symbolic_value sv ctx in
-  mk_texpression_from_var var
+  let ty = ctx_translate_fwd_ty ctx sv.sv_ty in
+  (* If the type is unit, directly return unit *)
+  if ty_is_unit ty then mk_unit_rvalue
+  else
+    (* Otherwise lookup the variable *)
+    let var = lookup_var_for_symbolic_value sv ctx in
+    mk_texpression_from_var var
 
 (** Translate a typed value.
 
@@ -1565,13 +1624,11 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
   match aproj with
   | V.AEndedProjLoans (msv, []) ->
       (* The symbolic value was left unchanged *)
-      let var = lookup_var_for_symbolic_value msv ctx in
-      Some (mk_texpression_from_var var)
+      Some (symbolic_value_to_texpression ctx msv)
   | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
       assert (child_aproj = AIgnoredProjBorrows);
       (* The symbolic value was updated *)
-      let var = lookup_var_for_symbolic_value mnv ctx in
-      Some (mk_texpression_from_var var)
+      Some (symbolic_value_to_texpression ctx mnv)
   | V.AEndedProjLoans (_, _) ->
       (* The symbolic value was updated, and the given back values come from sevearl
        * abstractions *)
@@ -1940,10 +1997,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
       (List.combine args args_mplaces)
   in
   let dest_mplace = translate_opt_mplace call.dest_place in
-  let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
   (* Retrieve the function id, and register the function call in the context
    * if necessary. *)
-  let ctx, fun_id, effect_info, args, back_funs, out_state =
+  let ctx, fun_id, effect_info, args, dest_v =
     match call.call_id with
     | S.Fun (fid, call_id) ->
         (* Regular function call *)
@@ -1951,13 +2007,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         let func = Fun (FromLlbc (fid_t, None, None)) in
         (* Retrieve the effect information about this function (can fail,
          * takes a state as input, etc.) *)
-        let effect_info =
-          get_fun_effect_info ctx.fun_ctx.fun_infos fid None None
-        in
+        let effect_info = get_fun_effect_info ctx fid None None in
         (* Depending on the function effects:
-           * - add the fuel
-           * - add the state input argument
-           * - generate a fresh state variable for the returned state
+           - add the fuel
+           - add the state input argument
+           - generate a fresh state variable for the returned state
         *)
         let args, ctx, out_state =
           let fuel = mk_fuel_input_as_list ctx effect_info in
@@ -1970,7 +2024,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         (* If we do not split the forward/backward functions: generate the
            variables for the backward functions returned by the forward
            function. *)
-        let ctx, back_funs_map, back_funs =
+        let ctx, ignore_fwd_output, back_funs_map, back_funs =
           if !Config.return_back_funs then
             (* We need to compute the signatures of the backward functions. *)
             let sg = Option.get call.sg in
@@ -1981,7 +2035,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 (List.map (fun _ -> None) sg.inputs)
             in
             let tr_self = UnknownTrait __FUNCTION__ in
-            let back_tys = compute_back_tys dsg (Some (generics, tr_self)) in
+            let back_tys =
+              compute_back_tys_with_info dsg (Some (generics, tr_self))
+            in
             (* Introduce variables for the backward functions *)
             (* Compute a proper basename for the variables *)
             let back_fun_name =
@@ -2016,7 +2072,18 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                    (fun ty ->
                      match ty with
                      | None -> None
-                     | Some ty -> Some (Some back_fun_name, ty))
+                     | Some (back_sg, ty) ->
+                         (* We insert a name for the variable only if the function
+                            can fail: if it can fail, it means the call returns a backward
+                            function. Otherwise, we it directly returns the value given
+                            back by the backward function, which means we shouldn't
+                            give it a name like "back..." (it doesn't make sense) *)
+                         let name =
+                           if back_sg.effect_info.can_fail then
+                             Some back_fun_name
+                           else None
+                         in
+                         Some (name, ty))
                    back_tys)
                 ctx
             in
@@ -2039,14 +2106,37 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let back_funs_map =
               RegionGroupId.Map.of_list (List.combine gids back_vars)
             in
-            (ctx, Some back_funs_map, back_funs)
-          else (ctx, None, [])
+            (ctx, dsg.fwd_info.ignore_output, Some back_funs_map, back_funs)
+          else (ctx, false, None, [])
+        in
+        (* Compute the pattern for the destination *)
+        let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+        let dest = mk_typed_pattern_from_var dest dest_mplace in
+        let dest =
+          (* Here there is something subtle: as we might ignore the output
+             of the forward function (because it translates to unit) we doNOT
+             necessarily introduce in the let-binding the variable to which we
+             map the symbolic value which was introduced for the output of the
+             function call. This would be problematic if later we need to
+             translate this symbolic value, but we implemented
+             {!symbolic_value_to_texpression} so that it doesn't perform any
+             lookups if the symbolic value has type unit.
+          *)
+          let vars =
+            if ignore_fwd_output then back_funs else dest :: back_funs
+          in
+          mk_simpl_tuple_pattern vars
+        in
+        let dest =
+          match out_state with
+          | None -> dest
+          | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
         in
         (* Register the function call *)
         let ctx =
           bs_ctx_register_forward_call call_id call args back_funs_map ctx
         in
-        (ctx, func, effect_info, args, back_funs, out_state)
+        (ctx, func, effect_info, args, dest)
     | S.Unop E.Not ->
         let effect_info =
           {
@@ -2057,7 +2147,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             is_rec = false;
           }
         in
-        (ctx, Unop Not, effect_info, args, [], None)
+        let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+        let dest = mk_typed_pattern_from_var dest dest_mplace in
+        (ctx, Unop Not, effect_info, args, dest)
     | S.Unop E.Neg -> (
         match args with
         | [ arg ] ->
@@ -2073,7 +2165,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Unop (Neg int_ty), effect_info, args, [], None)
+            let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+            let dest = mk_typed_pattern_from_var dest dest_mplace in
+            (ctx, Unop (Neg int_ty), effect_info, args, dest)
         | _ -> raise (Failure "Unreachable"))
     | S.Unop (E.Cast cast_kind) -> (
         match cast_kind with
@@ -2088,7 +2182,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, [], None)
+            let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+            let dest = mk_typed_pattern_from_var dest dest_mplace in
+            (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest)
         | CastFnPtr _ -> raise (Failure "TODO: function casts"))
     | S.Binop binop -> (
         match args with
@@ -2108,16 +2204,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 is_rec = false;
               }
             in
-            (ctx, Binop (binop, int_ty0), effect_info, args, [], None)
+            let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+            let dest = mk_typed_pattern_from_var dest dest_mplace in
+            (ctx, Binop (binop, int_ty0), effect_info, args, dest)
         | _ -> raise (Failure "Unreachable"))
   in
-  let dest_v =
-    let dest = mk_typed_pattern_from_var dest dest_mplace in
-    let dest = mk_simpl_tuple_pattern (dest :: back_funs) in
-    match out_state with
-    | None -> dest
-    | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
-  in
   let func = { id = FunOrOp fun_id; generics } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
   let ret_ty =
@@ -2242,9 +2333,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
         (* Those don't have backward functions *)
         raise (Failure "Unreachable")
   in
-  let effect_info =
-    get_fun_effect_info ctx.fun_ctx.fun_infos fun_id None (Some rg_id)
-  in
+  let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
   (* Retrieve the original call and the parent abstractions *)
   let _forward, backwards = get_abs_ancestors ctx abs call_id in
@@ -2449,8 +2538,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
          to a forward call which happened earlier *)
       let fun_id = E.FRegular ctx.fun_decl.def_id in
       let effect_info =
-        get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fun_id) (Some vloop_id)
-          (Some rg_id)
+        get_fun_effect_info ctx (FunId fun_id) (Some vloop_id) (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
       let generics = loop_info.generics in
@@ -2609,8 +2697,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
 and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
     (exp : S.expansion) (ctx : bs_ctx) : texpression =
   (* Translate the scrutinee *)
-  let scrutinee_var = lookup_var_for_symbolic_value sv ctx in
-  let scrutinee = mk_texpression_from_var scrutinee_var in
+  let scrutinee = symbolic_value_to_texpression ctx sv in
   let scrutinee_mplace = translate_opt_mplace p in
   (* Translate the branches *)
   match exp with
@@ -2999,7 +3086,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       (* Compute whether the backward expressions should be evaluated straight
          away or not (i.e., if we should bind them with monadic let-bindings
          or not). We evaluate them straight away if they can fail and have no
-         inputs *)
+         inputs. *)
       let evaluate_backs =
         List.map
           (fun (sg : back_sg_info) ->
@@ -3098,9 +3185,7 @@ and translate_forward_end (ectx : C.eval_ctx)
 
       (* Lookup the effect info for the loop function *)
       let fid = E.FRegular ctx.fun_decl.def_id in
-      let effect_info =
-        get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fid) None ctx.bid
-      in
+      let effect_info = get_fun_effect_info ctx (FunId fid) None ctx.bid in
 
       (* Introduce a fresh output value for the forward function *)
       let ctx, output_var = fresh_var None ctx.sg.fwd_output ctx in
@@ -3479,8 +3564,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     | None -> None
     | Some body ->
         let effect_info =
-          get_fun_effect_info ctx.fun_ctx.fun_infos (FunId (FRegular def_id))
-            None bid
+          get_fun_effect_info ctx (FunId (FRegular def_id)) None bid
         in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 5584fb9a..ccc46420 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -42,7 +42,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
     TODO: maybe we should introduce a record for this.
 *)
 let translate_function_to_pure (trans_ctx : trans_ctx)
-    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) :
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+    (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
     pure_fun_translation_no_loops =
   (* Debug *)
   log#ldebug
@@ -119,18 +120,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
         !m
   in
 
-  let input_names =
-    match fdef.body with
-    | None -> List.map (fun _ -> None) fdef.signature.inputs
-    | Some body ->
-        List.map
-          (fun (v : var) -> v.name)
-          (LlbcAstUtils.fun_body_get_input_vars body)
-  in
-
   let sg =
-    SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx def_id
-      fdef.signature input_names
+    SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef
   in
 
   let regions_hierarchy =
@@ -154,6 +145,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       decls_ctx = trans_ctx;
       SymbolicToPure.bid = None;
       sg;
+      fun_dsigs;
       (* Will need to be updated for the backward functions *)
       sv_to_var;
       var_counter = ref var_counter;
@@ -290,10 +282,21 @@ let translate_crate_to_pure (crate : crate) :
       (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
 
+  (* Compute the decomposed fun sigs for the whole crate *)
+  let fun_dsigs =
+    FunDeclId.Map.of_list
+      (List.map
+         (fun (fdef : LlbcAst.fun_decl) ->
+           ( fdef.def_id,
+             SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx
+               fdef ))
+         (FunDeclId.Map.values crate.fun_decls))
+  in
+
   (* Translate all the *transparent* functions *)
   let pure_translations =
     List.map
-      (translate_function_to_pure trans_ctx type_decls_map)
+      (translate_function_to_pure trans_ctx type_decls_map fun_dsigs)
       (FunDeclId.Map.values crate.fun_decls)
   in
 
-- 
cgit v1.3.1


From 455ba366f9c8d07a1f1848ec0960b1f2d161e7cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 18:47:50 +0100
Subject: Update the library for F*

---
 Makefile                            |   6 +-
 backends/fstar/Makefile             |  47 --
 backends/fstar/Primitives.fst       | 884 ------------------------------------
 backends/fstar/merge/Makefile       |  47 ++
 backends/fstar/merge/Primitives.fst | 829 +++++++++++++++++++++++++++++++++
 backends/fstar/split/Makefile       |  47 ++
 backends/fstar/split/Primitives.fst | 884 ++++++++++++++++++++++++++++++++++++
 compiler/ExtractBuiltin.ml          |   8 +
 compiler/Translate.ml               |   8 +-
 9 files changed, 1826 insertions(+), 934 deletions(-)
 delete mode 100644 backends/fstar/Makefile
 delete mode 100644 backends/fstar/Primitives.fst
 create mode 100644 backends/fstar/merge/Makefile
 create mode 100644 backends/fstar/merge/Primitives.fst
 create mode 100644 backends/fstar/split/Makefile
 create mode 100644 backends/fstar/split/Primitives.fst

(limited to 'compiler/Translate.ml')

diff --git a/Makefile b/Makefile
index 2cce30d9..37408554 100644
--- a/Makefile
+++ b/Makefile
@@ -70,9 +70,11 @@ build-bin-dir: build-bin build-lib
 	mkdir -p bin
 	cp -f compiler/_build/default/main.exe bin/aeneas
 	cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
-	mkdir -p bin/backends/fstar
+	mkdir -p bin/backends/fstar/split
+	mkdir -p bin/backends/fstar/merge
 	mkdir -p bin/backends/coq
-	cp -rf backends/fstar/*.fst* bin/backends/fstar/
+	cp -rf backends/fstar/split/*.fst* bin/backends/fstar/split/
+	cp -rf backends/fstar/merge/*.fst* bin/backends/fstar/merge/
 	cp -rf backends/coq/*.v bin/backends/coq/
 
 .PHONY: doc
diff --git a/backends/fstar/Makefile b/backends/fstar/Makefile
deleted file mode 100644
index a16b0edb..00000000
--- a/backends/fstar/Makefile
+++ /dev/null
@@ -1,47 +0,0 @@
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
-  --warn_error '+241@247+285-274' \
-
-FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
-	@echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
-	$(FSTAR) $(FSTAR_OPTIONS) $< && \
-	touch -c $@
-
-.PHONY: clean
-clean:
-	rm -f obj/*
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
deleted file mode 100644
index a3ffbde4..00000000
--- a/backends/fstar/Primitives.fst
+++ /dev/null
@@ -1,884 +0,0 @@
-/// This file lists primitive and assumed functions and types
-module Primitives
-open FStar.Mul
-open FStar.List.Tot
-
-#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
-
-(*** Utilities *)
-val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
-  ls':list a{
-    length ls' = length ls /\
-    index ls' i == x
-  }
-#push-options "--fuel 1"
-let rec list_update #a ls i x =
-  match ls with
-  | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
-#pop-options
-
-(*** Result *)
-type error : Type0 =
-| Failure
-| OutOfFuel
-
-type result (a : Type0) : Type0 =
-| Return : v:a -> result a
-| Fail : e:error -> result a
-
-// Monadic return operator
-unfold let return (#a : Type0) (x : a) : result a = Return x
-
-// Monadic bind operator.
-// Allows to use the notation:
-// ```
-// let* x = y in
-// ...
-// ```
-unfold let (let*) (#a #b : Type0) (m: result a)
-  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
-  result b =
-  match m with
-  | Return x -> f x
-  | Fail e   -> Fail e
-
-// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail Failure
-
-// Normalize and unwrap a successful result (used for globals).
-let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
-
-(*** Misc *)
-type char = FStar.Char.char
-type string = string
-
-let is_zero (n: nat) : bool = n = 0
-let decrease (n: nat{n > 0}) : nat = n - 1
-
-let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
-let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
-
-// We don't really use raw pointers for now
-type mut_raw_ptr (t : Type0) = { v : t }
-type const_raw_ptr (t : Type0) = { v : t }
-
-(*** Scalars *)
-/// Rem.: most of the following code was partially generated
-
-assume val size_numbits : pos
-
-// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t
-
-let isize_min : int = -9223372036854775808 // TODO: should be opaque
-let isize_max : int = 9223372036854775807 // TODO: should be opaque
-let i8_min : int = -128
-let i8_max : int = 127
-let i16_min : int = -32768
-let i16_max : int = 32767
-let i32_min : int = -2147483648
-let i32_max : int = 2147483647
-let i64_min : int = -9223372036854775808
-let i64_max : int = 9223372036854775807
-let i128_min : int = -170141183460469231731687303715884105728
-let i128_max : int = 170141183460469231731687303715884105727
-let usize_min : int = 0
-let usize_max : int = 4294967295 // TODO: should be opaque
-let u8_min : int = 0
-let u8_max : int = 255
-let u16_min : int = 0
-let u16_max : int = 65535
-let u32_min : int = 0
-let u32_max : int = 4294967295
-let u64_min : int = 0
-let u64_max : int = 18446744073709551615
-let u128_min : int = 0
-let u128_max : int = 340282366920938463463374607431768211455
-
-type scalar_ty =
-| Isize
-| I8
-| I16
-| I32
-| I64
-| I128
-| Usize
-| U8
-| U16
-| U32
-| U64
-| U128
-
-let is_unsigned = function
-  | Isize | I8 | I16 | I32 | I64 | I128 -> false
-  | Usize | U8 | U16 | U32 | U64 | U128 -> true
-
-let scalar_min (ty : scalar_ty) : int =
-  match ty with
-  | Isize -> isize_min
-  | I8 -> i8_min
-  | I16 -> i16_min
-  | I32 -> i32_min
-  | I64 -> i64_min
-  | I128 -> i128_min
-  | Usize -> usize_min
-  | U8 -> u8_min
-  | U16 -> u16_min
-  | U32 -> u32_min
-  | U64 -> u64_min
-  | U128 -> u128_min
-
-let scalar_max (ty : scalar_ty) : int =
-  match ty with
-  | Isize -> isize_max
-  | I8 -> i8_max
-  | I16 -> i16_max
-  | I32 -> i32_max
-  | I64 -> i64_max
-  | I128 -> i128_max
-  | Usize -> usize_max
-  | U8 -> u8_max
-  | U16 -> u16_max
-  | U32 -> u32_max
-  | U64 -> u64_max
-  | U128 -> u128_max
-
-type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
-
-let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
-
-let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
-
-let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
-
-/// The remainder operation
-let int_rem (x : int) (y : int{y <> 0}) : int =
-  if x >= 0 then (x % y) else -(x % y)
-
-(* Checking consistency with Rust *)
-let _ = assert_norm(int_rem 1 2 = 1)
-let _ = assert_norm(int_rem (-1) 2 = -1)
-let _ = assert_norm(int_rem 1 (-2) = 1)
-let _ = assert_norm(int_rem (-1) (-2) = -1)
-
-let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
-
-let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x + y)
-
-let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x - y)
-
-let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x * y)
-
-let scalar_xor (#ty : scalar_ty)
-    (x : scalar ty) (y : scalar ty) : scalar ty =
-  match ty with
-  | U8 -> FStar.UInt.logxor #8 x y
-  | U16 -> FStar.UInt.logxor #16 x y
-  | U32 -> FStar.UInt.logxor #32 x y
-  | U64 -> FStar.UInt.logxor #64 x y
-  | U128 -> FStar.UInt.logxor #128 x y
-  | Usize -> admit() // TODO
-  | I8 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 8);
-    normalize_spec (scalar I8);
-    FStar.Int.logxor #8 x y
-  | I16 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 16);
-    normalize_spec (scalar I16);
-    FStar.Int.logxor #16 x y
-  | I32 -> FStar.Int.logxor #32 x y
-  | I64 -> FStar.Int.logxor #64 x y
-  | I128 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 128);
-    normalize_spec (scalar I128);
-    FStar.Int.logxor #128 x y
-  | Isize -> admit() // TODO
-
-let scalar_or (#ty : scalar_ty)
-    (x : scalar ty) (y : scalar ty) : scalar ty =
-  match ty with
-  | U8 -> FStar.UInt.logor #8 x y
-  | U16 -> FStar.UInt.logor #16 x y
-  | U32 -> FStar.UInt.logor #32 x y
-  | U64 -> FStar.UInt.logor #64 x y
-  | U128 -> FStar.UInt.logor #128 x y
-  | Usize -> admit() // TODO
-  | I8 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 8);
-    normalize_spec (scalar I8);
-    FStar.Int.logor #8 x y
-  | I16 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 16);
-    normalize_spec (scalar I16);
-    FStar.Int.logor #16 x y
-  | I32 -> FStar.Int.logor #32 x y
-  | I64 -> FStar.Int.logor #64 x y
-  | I128 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 128);
-    normalize_spec (scalar I128);
-    FStar.Int.logor #128 x y
-  | Isize -> admit() // TODO
-
-let scalar_and (#ty : scalar_ty)
-    (x : scalar ty) (y : scalar ty) : scalar ty =
-  match ty with
-  | U8 -> FStar.UInt.logand #8 x y
-  | U16 -> FStar.UInt.logand #16 x y
-  | U32 -> FStar.UInt.logand #32 x y
-  | U64 -> FStar.UInt.logand #64 x y
-  | U128 -> FStar.UInt.logand #128 x y
-  | Usize -> admit() // TODO
-  | I8 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 8);
-    normalize_spec (scalar I8);
-    FStar.Int.logand #8 x y
-  | I16 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 16);
-    normalize_spec (scalar I16);
-    FStar.Int.logand #16 x y
-  | I32 -> FStar.Int.logand #32 x y
-  | I64 -> FStar.Int.logand #64 x y
-  | I128 ->
-    // Encoding issues...
-    normalize_spec (FStar.Int.int_t 128);
-    normalize_spec (scalar I128);
-    FStar.Int.logand #128 x y
-  | Isize -> admit() // TODO
-
-// Shift left
-let scalar_shl (#ty0 #ty1 : scalar_ty)
-    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
-  admit()
-
-// Shift right
-let scalar_shr (#ty0 #ty1 : scalar_ty)
-    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
-  admit()
-
-(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-// TODO: check the semantics of casts in Rust
-let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
-  mk_scalar tgt_ty x
-
-// This can't fail, but for now we make all casts faillible (easier for the translation)
-let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
-  mk_scalar tgt_ty (if x then 1 else 0)
-
-/// The scalar types
-type isize : eqtype = scalar Isize
-type i8    : eqtype = scalar I8
-type i16   : eqtype = scalar I16
-type i32   : eqtype = scalar I32
-type i64   : eqtype = scalar I64
-type i128  : eqtype = scalar I128
-type usize : eqtype = scalar Usize
-type u8    : eqtype = scalar U8
-type u16   : eqtype = scalar U16
-type u32   : eqtype = scalar U32
-type u64   : eqtype = scalar U64
-type u128  : eqtype = scalar U128
-
-
-let core_isize_min : isize = isize_min
-let core_isize_max : isize = isize_max
-let core_i8_min    : i8 = i8_min
-let core_i8_max    : i8 = i8_max
-let core_i16_min   : i16 = i16_min
-let core_i16_max   : i16 = i16_max
-let core_i32_min   : i32 = i32_min
-let core_i32_max   : i32 = i32_max
-let core_i64_min   : i64 = i64_min
-let core_i64_max   : i64 = i64_max
-let core_i128_min  : i128 = i128_min
-let core_i128_max  : i128 = i128_max
-
-let core_usize_min : usize = usize_min
-let core_usize_max : usize = usize_max
-let core_u8_min    : u8 = u8_min
-let core_u8_max    : u8 = u8_max
-let core_u16_min   : u16 = u16_min
-let core_u16_max   : u16 = u16_max
-let core_u32_min   : u32 = u32_min
-let core_u32_max   : u32 = u32_max
-let core_u64_min   : u64 = u64_min
-let core_u64_max   : u64 = u64_max
-let core_u128_min  : u128 = u128_min
-let core_u128_max  : u128 = u128_max
-
-/// Negation
-let isize_neg = scalar_neg #Isize
-let i8_neg = scalar_neg #I8
-let i16_neg = scalar_neg #I16
-let i32_neg = scalar_neg #I32
-let i64_neg = scalar_neg #I64
-let i128_neg = scalar_neg #I128
-
-/// Division
-let isize_div = scalar_div #Isize
-let i8_div = scalar_div #I8
-let i16_div = scalar_div #I16
-let i32_div = scalar_div #I32
-let i64_div = scalar_div #I64
-let i128_div = scalar_div #I128
-let usize_div = scalar_div #Usize
-let u8_div = scalar_div #U8
-let u16_div = scalar_div #U16
-let u32_div = scalar_div #U32
-let u64_div = scalar_div #U64
-let u128_div = scalar_div #U128
-
-/// Remainder
-let isize_rem = scalar_rem #Isize
-let i8_rem = scalar_rem #I8
-let i16_rem = scalar_rem #I16
-let i32_rem = scalar_rem #I32
-let i64_rem = scalar_rem #I64
-let i128_rem = scalar_rem #I128
-let usize_rem = scalar_rem #Usize
-let u8_rem = scalar_rem #U8
-let u16_rem = scalar_rem #U16
-let u32_rem = scalar_rem #U32
-let u64_rem = scalar_rem #U64
-let u128_rem = scalar_rem #U128
-
-/// Addition
-let isize_add = scalar_add #Isize
-let i8_add = scalar_add #I8
-let i16_add = scalar_add #I16
-let i32_add = scalar_add #I32
-let i64_add = scalar_add #I64
-let i128_add = scalar_add #I128
-let usize_add = scalar_add #Usize
-let u8_add = scalar_add #U8
-let u16_add = scalar_add #U16
-let u32_add = scalar_add #U32
-let u64_add = scalar_add #U64
-let u128_add = scalar_add #U128
-
-/// Subtraction
-let isize_sub = scalar_sub #Isize
-let i8_sub = scalar_sub #I8
-let i16_sub = scalar_sub #I16
-let i32_sub = scalar_sub #I32
-let i64_sub = scalar_sub #I64
-let i128_sub = scalar_sub #I128
-let usize_sub = scalar_sub #Usize
-let u8_sub = scalar_sub #U8
-let u16_sub = scalar_sub #U16
-let u32_sub = scalar_sub #U32
-let u64_sub = scalar_sub #U64
-let u128_sub = scalar_sub #U128
-
-/// Multiplication
-let isize_mul = scalar_mul #Isize
-let i8_mul = scalar_mul #I8
-let i16_mul = scalar_mul #I16
-let i32_mul = scalar_mul #I32
-let i64_mul = scalar_mul #I64
-let i128_mul = scalar_mul #I128
-let usize_mul = scalar_mul #Usize
-let u8_mul = scalar_mul #U8
-let u16_mul = scalar_mul #U16
-let u32_mul = scalar_mul #U32
-let u64_mul = scalar_mul #U64
-let u128_mul = scalar_mul #U128
-
-/// Xor
-let u8_xor = scalar_xor #U8
-let u16_xor = scalar_xor #U16
-let u32_xor = scalar_xor #U32
-let u64_xor = scalar_xor #U64
-let u128_xor = scalar_xor #U128
-let usize_xor = scalar_xor #Usize
-let i8_xor = scalar_xor #I8
-let i16_xor = scalar_xor #I16
-let i32_xor = scalar_xor #I32
-let i64_xor = scalar_xor #I64
-let i128_xor = scalar_xor #I128
-let isize_xor = scalar_xor #Isize
-
-/// Or
-let u8_or = scalar_or #U8
-let u16_or = scalar_or #U16
-let u32_or = scalar_or #U32
-let u64_or = scalar_or #U64
-let u128_or = scalar_or #U128
-let usize_or = scalar_or #Usize
-let i8_or = scalar_or #I8
-let i16_or = scalar_or #I16
-let i32_or = scalar_or #I32
-let i64_or = scalar_or #I64
-let i128_or = scalar_or #I128
-let isize_or = scalar_or #Isize
-
-/// And
-let u8_and = scalar_and #U8
-let u16_and = scalar_and #U16
-let u32_and = scalar_and #U32
-let u64_and = scalar_and #U64
-let u128_and = scalar_and #U128
-let usize_and = scalar_and #Usize
-let i8_and = scalar_and #I8
-let i16_and = scalar_and #I16
-let i32_and = scalar_and #I32
-let i64_and = scalar_and #I64
-let i128_and = scalar_and #I128
-let isize_and = scalar_and #Isize
-
-/// Shift left
-let u8_shl #ty = scalar_shl #U8 #ty
-let u16_shl #ty = scalar_shl #U16 #ty
-let u32_shl #ty = scalar_shl #U32 #ty
-let u64_shl #ty = scalar_shl #U64 #ty
-let u128_shl #ty = scalar_shl #U128 #ty
-let usize_shl #ty = scalar_shl #Usize #ty
-let i8_shl #ty = scalar_shl #I8 #ty
-let i16_shl #ty = scalar_shl #I16 #ty
-let i32_shl #ty = scalar_shl #I32 #ty
-let i64_shl #ty = scalar_shl #I64 #ty
-let i128_shl #ty = scalar_shl #I128 #ty
-let isize_shl #ty = scalar_shl #Isize #ty
-
-/// Shift right
-let u8_shr #ty = scalar_shr #U8 #ty
-let u16_shr #ty = scalar_shr #U16 #ty
-let u32_shr #ty = scalar_shr #U32 #ty
-let u64_shr #ty = scalar_shr #U64 #ty
-let u128_shr #ty = scalar_shr #U128 #ty
-let usize_shr #ty = scalar_shr #Usize #ty
-let i8_shr #ty = scalar_shr #I8 #ty
-let i16_shr #ty = scalar_shr #I16 #ty
-let i32_shr #ty = scalar_shr #I32 #ty
-let i64_shr #ty = scalar_shr #I64 #ty
-let i128_shr #ty = scalar_shr #I128 #ty
-let isize_shr #ty = scalar_shr #Isize #ty
-
-(*** core::ops *)
-
-// Trait declaration: [core::ops::index::Index]
-noeq type core_ops_index_Index (self idx : Type0) = {
-  output : Type0;
-  index : self → idx → result output
-}
-
-// Trait declaration: [core::ops::index::IndexMut]
-noeq type core_ops_index_IndexMut (self idx : Type0) = {
-  indexInst : core_ops_index_Index self idx;
-  index_mut : self → idx → result indexInst.output;
-  index_mut_back : self → idx → indexInst.output → result self;
-}
-
-// Trait declaration [core::ops::deref::Deref]
-noeq type core_ops_deref_Deref (self : Type0) = {
-  target : Type0;
-  deref : self → result target;
-}
-
-// Trait declaration [core::ops::deref::DerefMut]
-noeq type core_ops_deref_DerefMut (self : Type0) = {
-  derefInst : core_ops_deref_Deref self;
-  deref_mut : self → result derefInst.target;
-  deref_mut_back : self → derefInst.target → result self;
-}
-
-type core_ops_range_Range (a : Type0) = {
-  start : a;
-  end_ : a;
-}
-
-(*** [alloc] *)
-
-let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
-
-// Trait instance
-let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
-  target = self;
-  deref = alloc_boxed_Box_deref self;
-}
-
-// Trait instance
-let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
-  derefInst = alloc_boxed_Box_coreopsDerefInst self;
-  deref_mut = alloc_boxed_Box_deref_mut self;
-  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
-}
-
-(*** Array *)
-type array (a : Type0) (n : usize) = s:list a{length s = n}
-
-// We tried putting the normalize_term condition as a refinement on the list
-// but it didn't work. It works with the requires clause.
-let mk_array (a : Type0) (n : usize)
-  (l : list a) :
-  Pure (array a n)
-  (requires (normalize_term(FStar.List.Tot.length l) = n))
-  (ensures (fun _ -> True)) =
-  normalize_term_spec (FStar.List.Tot.length l);
-  l
-
-let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
-  if i < length x then Return (index x i)
-  else Fail Failure
-
-let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
-  if i < length x then Return (list_update x i nx)
-  else Fail Failure
-
-(*** Slice *)
-type slice (a : Type0) = s:list a{length s <= usize_max}
-
-let slice_len (a : Type0) (s : slice a) : usize = length s
-
-let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
-  if i < length x then Return (index x i)
-  else Fail Failure
-
-let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
-  if i < length x then Return (list_update x i nx)
-  else Fail Failure
-
-(*** Subslices *)
-
-let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
-let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
-  if length s = n then Return s
-  else Fail Failure
-
-// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
-let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
-  admit()
-
-let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) =
-  admit()
-
-let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
-  admit()
-
-let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
-  admit()
-
-let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
-  admit()
-
-(*** Vector *)
-type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max}
-
-let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
-let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
-
-// Helper
-let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail Failure
-// Helper
-let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
-  if i < length v then Return (list_update v i x) else Fail Failure
-
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
-let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
-  Pure (result (alloc_vec_Vec a))
-  (requires True)
-  (ensures (fun res ->
-    match res with
-    | Fail e -> e == Failure
-    | Return v' -> length v' = length v + 1)) =
-  if length v < usize_max then begin
-    (**) assert_norm(length [x] == 1);
-    (**) append_length v [x];
-    (**) assert(length (append v [x]) = length v + 1);
-    Return (append v [x])
-    end
-  else Fail Failure
-
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail Failure
-let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
-  if i < length v then Return (list_update v i x) else Fail Failure
-
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
-// Trait declaration: [core::slice::index::SliceIndex]
-noeq type core_slice_index_SliceIndex (self t : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
-  output : Type0;
-  get : self → t → result (option output);
-  get_mut : self → t → result (option output);
-  get_mut_back : self → t → option output → result t;
-  get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
-  get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
-  index : self → t → result output;
-  index_mut : self → t → result output;
-  index_mut_back : self → t → output → result t;
-}
-
-// [core::slice::index::[T]::index]: forward function
-let core_slice_index_Slice_index
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (s : slice t) (i : idx) : result inst.output =
-  let* x = inst.get i s in
-  match x with
-  | None -> Fail Failure
-  | Some x -> Return x
-
-// [core::slice::index::Range:::get]: forward function
-let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
-  result (option (slice t)) =
-  admit () // TODO
-
-// [core::slice::index::Range::get_mut]: forward function
-let core_slice_index_RangeUsize_get_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
-  admit () // TODO
-
-// [core::slice::index::Range::get_mut]: backward function 0
-let core_slice_index_RangeUsize_get_mut_back
-  (t : Type0) :
-  core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::Range::get_unchecked]: forward function
-let core_slice_index_RangeUsize_get_unchecked
-  (t : Type0) :
-  core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) =
-  // Don't know what the model should be - for now we always fail to make
-  // sure code which uses it fails
-  fun _ _ -> Fail Failure
-
-// [core::slice::index::Range::get_unchecked_mut]: forward function
-let core_slice_index_RangeUsize_get_unchecked_mut
-  (t : Type0) :
-  core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) =
-  // Don't know what the model should be - for now we always fail to make
-  // sure code which uses it fails
-  fun _ _ -> Fail Failure
-
-// [core::slice::index::Range::index]: forward function
-let core_slice_index_RangeUsize_index
-  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::Range::index_mut]: forward function
-let core_slice_index_RangeUsize_index_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::Range::index_mut]: backward function 0
-let core_slice_index_RangeUsize_index_mut_back
-  (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::[T]::index_mut]: forward function
-let core_slice_index_Slice_index_mut
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → result inst.output =
-  admit () // 
-
-// [core::slice::index::[T]::index_mut]: backward function 0
-let core_slice_index_Slice_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → inst.output → result (slice t) =
-  admit () // TODO
-
-// [core::array::[T; N]::index]: forward function
-let core_array_Array_index
-  (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
-  (a : array t n) (i : idx) : result inst.output =
-  admit () // TODO
-
-// [core::array::[T; N]::index_mut]: forward function
-let core_array_Array_index_mut
-  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) : result inst.indexInst.output =
-  admit () // TODO
-
-// [core::array::[T; N]::index_mut]: backward function 0
-let core_array_Array_index_mut_back
-  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
-  admit () // TODO
-
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
-// Trait implementation: [core::slice::index::Range]
-let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
-  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
-  output = slice t;
-  get = core_slice_index_RangeUsize_get t;
-  get_mut = core_slice_index_RangeUsize_get_mut t;
-  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
-  get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
-  get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
-  index = core_slice_index_RangeUsize_index t;
-  index_mut = core_slice_index_RangeUsize_index_mut t;
-  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
-}
-
-// Trait implementation: [core::slice::index::[T]]
-let core_ops_index_IndexSliceTIInst (t idx : Type0)
-  (inst : core_slice_index_SliceIndex idx (slice t)) :
-  core_ops_index_Index (slice t) idx = {
-  output = inst.output;
-  index = core_slice_index_Slice_index t idx inst;
-}
-
-// Trait implementation: [core::slice::index::[T]]
-let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
-  (inst : core_slice_index_SliceIndex idx (slice t)) :
-  core_ops_index_IndexMut (slice t) idx = {
-  indexInst = core_ops_index_IndexSliceTIInst t idx inst;
-  index_mut = core_slice_index_Slice_index_mut t idx inst;
-  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
-}
-
-// Trait implementation: [core::array::[T; N]]
-let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
-  (inst : core_ops_index_Index (slice t) idx) :
-  core_ops_index_Index (array t n) idx = {
-  output = inst.output;
-  index = core_array_Array_index t idx n inst;
-}
-
-// Trait implementation: [core::array::[T; N]]
-let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
-  (inst : core_ops_index_IndexMut (slice t) idx) :
-  core_ops_index_IndexMut (array t n) idx = {
-  indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
-  index_mut = core_array_Array_index_mut t idx n inst;
-  index_mut_back = core_array_Array_index_mut_back t idx n inst;
-}
-
-// [core::slice::index::usize::get]: forward function
-let core_slice_index_usize_get
-  (t : Type0) : usize → slice t → result (option t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_mut]: forward function
-let core_slice_index_usize_get_mut
-  (t : Type0) : usize → slice t → result (option t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_mut]: backward function 0
-let core_slice_index_usize_get_mut_back
-  (t : Type0) : usize → slice t → option t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_unchecked]: forward function
-let core_slice_index_usize_get_unchecked
-  (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_unchecked_mut]: forward function
-let core_slice_index_usize_get_unchecked_mut
-  (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) =
-  admit () // TODO
-
-// [core::slice::index::usize::index]: forward function
-let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
-  admit () // TODO
-
-// [core::slice::index::usize::index_mut]: forward function
-let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
-  admit () // TODO
-
-// [core::slice::index::usize::index_mut]: backward function 0
-let core_slice_index_usize_index_mut_back
-  (t : Type0) : usize → slice t → t → result (slice t) =
-  admit () // TODO
-
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
-// Trait implementation: [core::slice::index::usize]
-let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
-  core_slice_index_SliceIndex usize (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
-  output = t;
-  get = core_slice_index_usize_get t;
-  get_mut = core_slice_index_usize_get_mut t;
-  get_mut_back = core_slice_index_usize_get_mut_back t;
-  get_unchecked = core_slice_index_usize_get_unchecked t;
-  get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
-  index = core_slice_index_usize_index t;
-  index_mut = core_slice_index_usize_index_mut t;
-  index_mut_back = core_slice_index_usize_index_mut_back t;
-}
-
-// [alloc::vec::Vec::index]: forward function
-let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
-  admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: forward function
-let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
-  admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: backward function 0
-let alloc_vec_Vec_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
-  admit () // TODO
-
-// Trait implementation: [alloc::vec::Vec]
-let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
-  (inst : core_slice_index_SliceIndex idx (slice t)) :
-  core_ops_index_Index (alloc_vec_Vec t) idx = {
-  output = inst.output;
-  index = alloc_vec_Vec_index t idx inst;
-}
-
-// Trait implementation: [alloc::vec::Vec]
-let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
-  (inst : core_slice_index_SliceIndex idx (slice t)) :
-  core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
-  indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
-  index_mut = alloc_vec_Vec_index_mut t idx inst;
-  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
-}
-
-(*** Theorems *)
-
-let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
-  Lemma (
-    alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
-      alloc_vec_Vec_index_usize v i)
-  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
-  =
-  admit()
-
-let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
-  Lemma (
-    alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
-      alloc_vec_Vec_index_usize v i)
-  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
-  =
-  admit()
-
-let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
-  Lemma (
-    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
-      alloc_vec_Vec_update_usize v i x)
-  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
-  =
-  admit()
diff --git a/backends/fstar/merge/Makefile b/backends/fstar/merge/Makefile
new file mode 100644
index 00000000..a16b0edb
--- /dev/null
+++ b/backends/fstar/merge/Makefile
@@ -0,0 +1,47 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+# Generete the .checked files in batch mode
+%.checked:
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/backends/fstar/merge/Primitives.fst b/backends/fstar/merge/Primitives.fst
new file mode 100644
index 00000000..6b8dbeb7
--- /dev/null
+++ b/backends/fstar/merge/Primitives.fst
@@ -0,0 +1,829 @@
+/// This file lists primitive and assumed functions and types
+module Primitives
+open FStar.Mul
+open FStar.List.Tot
+
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+
+(*** Utilities *)
+val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
+  ls':list a{
+    length ls' = length ls /\
+    index ls' i == x
+  }
+#push-options "--fuel 1"
+let rec list_update #a ls i x =
+  match ls with
+  | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
+#pop-options
+
+(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
+type result (a : Type0) : Type0 =
+| Return : v:a -> result a
+| Fail : e:error -> result a
+
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a)
+  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
+  result b =
+  match m with
+  | Return x -> f x
+  | Fail e   -> Fail e
+
+// Monadic assert(...)
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
+
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
+(*** Misc *)
+type char = FStar.Char.char
+type string = string
+
+let is_zero (n: nat) : bool = n = 0
+let decrease (n: nat{n > 0}) : nat = n - 1
+
+let core_mem_replace (a : Type0) (x : a) (y : a) : a & (a -> a) = (x, (fun x -> x))
+
+// We don't really use raw pointers for now
+type mut_raw_ptr (t : Type0) = { v : t }
+type const_raw_ptr (t : Type0) = { v : t }
+
+(*** Scalars *)
+/// Rem.: most of the following code was partially generated
+
+assume val size_numbits : pos
+
+// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t
+
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
+let i8_min : int = -128
+let i8_max : int = 127
+let i16_min : int = -32768
+let i16_max : int = 32767
+let i32_min : int = -2147483648
+let i32_max : int = 2147483647
+let i64_min : int = -9223372036854775808
+let i64_max : int = 9223372036854775807
+let i128_min : int = -170141183460469231731687303715884105728
+let i128_max : int = 170141183460469231731687303715884105727
+let usize_min : int = 0
+let usize_max : int = 4294967295 // TODO: should be opaque
+let u8_min : int = 0
+let u8_max : int = 255
+let u16_min : int = 0
+let u16_max : int = 65535
+let u32_min : int = 0
+let u32_max : int = 4294967295
+let u64_min : int = 0
+let u64_max : int = 18446744073709551615
+let u128_min : int = 0
+let u128_max : int = 340282366920938463463374607431768211455
+
+type scalar_ty =
+| Isize
+| I8
+| I16
+| I32
+| I64
+| I128
+| Usize
+| U8
+| U16
+| U32
+| U64
+| U128
+
+let is_unsigned = function
+  | Isize | I8 | I16 | I32 | I64 | I128 -> false
+  | Usize | U8 | U16 | U32 | U64 | U128 -> true
+
+let scalar_min (ty : scalar_ty) : int =
+  match ty with
+  | Isize -> isize_min
+  | I8 -> i8_min
+  | I16 -> i16_min
+  | I32 -> i32_min
+  | I64 -> i64_min
+  | I128 -> i128_min
+  | Usize -> usize_min
+  | U8 -> u8_min
+  | U16 -> u16_min
+  | U32 -> u32_min
+  | U64 -> u64_min
+  | U128 -> u128_min
+
+let scalar_max (ty : scalar_ty) : int =
+  match ty with
+  | Isize -> isize_max
+  | I8 -> i8_max
+  | I16 -> i16_max
+  | I32 -> i32_max
+  | I64 -> i64_max
+  | I128 -> i128_max
+  | Usize -> usize_max
+  | U8 -> u8_max
+  | U16 -> u16_max
+  | U32 -> u32_max
+  | U64 -> u64_max
+  | U128 -> u128_max
+
+type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
+
+let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
+
+let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
+
+let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
+
+/// The remainder operation
+let int_rem (x : int) (y : int{y <> 0}) : int =
+  if x >= 0 then (x % y) else -(x % y)
+
+(* Checking consistency with Rust *)
+let _ = assert_norm(int_rem 1 2 = 1)
+let _ = assert_norm(int_rem (-1) 2 = -1)
+let _ = assert_norm(int_rem 1 (-2) = 1)
+let _ = assert_norm(int_rem (-1) (-2) = -1)
+
+let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
+
+let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x + y)
+
+let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x - y)
+
+let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x * y)
+
+let scalar_xor (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logxor #8 x y
+  | U16 -> FStar.UInt.logxor #16 x y
+  | U32 -> FStar.UInt.logxor #32 x y
+  | U64 -> FStar.UInt.logxor #64 x y
+  | U128 -> FStar.UInt.logxor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logxor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logxor #16 x y
+  | I32 -> FStar.Int.logxor #32 x y
+  | I64 -> FStar.Int.logxor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logxor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_or (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logor #8 x y
+  | U16 -> FStar.UInt.logor #16 x y
+  | U32 -> FStar.UInt.logor #32 x y
+  | U64 -> FStar.UInt.logor #64 x y
+  | U128 -> FStar.UInt.logor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logor #16 x y
+  | I32 -> FStar.Int.logor #32 x y
+  | I64 -> FStar.Int.logor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_and (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logand #8 x y
+  | U16 -> FStar.UInt.logand #16 x y
+  | U32 -> FStar.UInt.logand #32 x y
+  | U64 -> FStar.UInt.logand #64 x y
+  | U128 -> FStar.UInt.logand #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logand #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logand #16 x y
+  | I32 -> FStar.Int.logand #32 x y
+  | I64 -> FStar.Int.logand #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logand #128 x y
+  | Isize -> admit() // TODO
+
+// Shift left
+let scalar_shl (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
+
+// Shift right
+let scalar_shr (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
+
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty x
+
+// This can't fail, but for now we make all casts faillible (easier for the translation)
+let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty (if x then 1 else 0)
+
+/// The scalar types
+type isize : eqtype = scalar Isize
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
+type usize : eqtype = scalar Usize
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
+
+/// Negation
+let isize_neg = scalar_neg #Isize
+let i8_neg = scalar_neg #I8
+let i16_neg = scalar_neg #I16
+let i32_neg = scalar_neg #I32
+let i64_neg = scalar_neg #I64
+let i128_neg = scalar_neg #I128
+
+/// Division
+let isize_div = scalar_div #Isize
+let i8_div = scalar_div #I8
+let i16_div = scalar_div #I16
+let i32_div = scalar_div #I32
+let i64_div = scalar_div #I64
+let i128_div = scalar_div #I128
+let usize_div = scalar_div #Usize
+let u8_div = scalar_div #U8
+let u16_div = scalar_div #U16
+let u32_div = scalar_div #U32
+let u64_div = scalar_div #U64
+let u128_div = scalar_div #U128
+
+/// Remainder
+let isize_rem = scalar_rem #Isize
+let i8_rem = scalar_rem #I8
+let i16_rem = scalar_rem #I16
+let i32_rem = scalar_rem #I32
+let i64_rem = scalar_rem #I64
+let i128_rem = scalar_rem #I128
+let usize_rem = scalar_rem #Usize
+let u8_rem = scalar_rem #U8
+let u16_rem = scalar_rem #U16
+let u32_rem = scalar_rem #U32
+let u64_rem = scalar_rem #U64
+let u128_rem = scalar_rem #U128
+
+/// Addition
+let isize_add = scalar_add #Isize
+let i8_add = scalar_add #I8
+let i16_add = scalar_add #I16
+let i32_add = scalar_add #I32
+let i64_add = scalar_add #I64
+let i128_add = scalar_add #I128
+let usize_add = scalar_add #Usize
+let u8_add = scalar_add #U8
+let u16_add = scalar_add #U16
+let u32_add = scalar_add #U32
+let u64_add = scalar_add #U64
+let u128_add = scalar_add #U128
+
+/// Subtraction
+let isize_sub = scalar_sub #Isize
+let i8_sub = scalar_sub #I8
+let i16_sub = scalar_sub #I16
+let i32_sub = scalar_sub #I32
+let i64_sub = scalar_sub #I64
+let i128_sub = scalar_sub #I128
+let usize_sub = scalar_sub #Usize
+let u8_sub = scalar_sub #U8
+let u16_sub = scalar_sub #U16
+let u32_sub = scalar_sub #U32
+let u64_sub = scalar_sub #U64
+let u128_sub = scalar_sub #U128
+
+/// Multiplication
+let isize_mul = scalar_mul #Isize
+let i8_mul = scalar_mul #I8
+let i16_mul = scalar_mul #I16
+let i32_mul = scalar_mul #I32
+let i64_mul = scalar_mul #I64
+let i128_mul = scalar_mul #I128
+let usize_mul = scalar_mul #Usize
+let u8_mul = scalar_mul #U8
+let u16_mul = scalar_mul #U16
+let u32_mul = scalar_mul #U32
+let u64_mul = scalar_mul #U64
+let u128_mul = scalar_mul #U128
+
+/// Xor
+let u8_xor = scalar_xor #U8
+let u16_xor = scalar_xor #U16
+let u32_xor = scalar_xor #U32
+let u64_xor = scalar_xor #U64
+let u128_xor = scalar_xor #U128
+let usize_xor = scalar_xor #Usize
+let i8_xor = scalar_xor #I8
+let i16_xor = scalar_xor #I16
+let i32_xor = scalar_xor #I32
+let i64_xor = scalar_xor #I64
+let i128_xor = scalar_xor #I128
+let isize_xor = scalar_xor #Isize
+
+/// Or
+let u8_or = scalar_or #U8
+let u16_or = scalar_or #U16
+let u32_or = scalar_or #U32
+let u64_or = scalar_or #U64
+let u128_or = scalar_or #U128
+let usize_or = scalar_or #Usize
+let i8_or = scalar_or #I8
+let i16_or = scalar_or #I16
+let i32_or = scalar_or #I32
+let i64_or = scalar_or #I64
+let i128_or = scalar_or #I128
+let isize_or = scalar_or #Isize
+
+/// And
+let u8_and = scalar_and #U8
+let u16_and = scalar_and #U16
+let u32_and = scalar_and #U32
+let u64_and = scalar_and #U64
+let u128_and = scalar_and #U128
+let usize_and = scalar_and #Usize
+let i8_and = scalar_and #I8
+let i16_and = scalar_and #I16
+let i32_and = scalar_and #I32
+let i64_and = scalar_and #I64
+let i128_and = scalar_and #I128
+let isize_and = scalar_and #Isize
+
+/// Shift left
+let u8_shl #ty = scalar_shl #U8 #ty
+let u16_shl #ty = scalar_shl #U16 #ty
+let u32_shl #ty = scalar_shl #U32 #ty
+let u64_shl #ty = scalar_shl #U64 #ty
+let u128_shl #ty = scalar_shl #U128 #ty
+let usize_shl #ty = scalar_shl #Usize #ty
+let i8_shl #ty = scalar_shl #I8 #ty
+let i16_shl #ty = scalar_shl #I16 #ty
+let i32_shl #ty = scalar_shl #I32 #ty
+let i64_shl #ty = scalar_shl #I64 #ty
+let i128_shl #ty = scalar_shl #I128 #ty
+let isize_shl #ty = scalar_shl #Isize #ty
+
+/// Shift right
+let u8_shr #ty = scalar_shr #U8 #ty
+let u16_shr #ty = scalar_shr #U16 #ty
+let u32_shr #ty = scalar_shr #U32 #ty
+let u64_shr #ty = scalar_shr #U64 #ty
+let u128_shr #ty = scalar_shr #U128 #ty
+let usize_shr #ty = scalar_shr #Usize #ty
+let i8_shr #ty = scalar_shr #I8 #ty
+let i16_shr #ty = scalar_shr #I16 #ty
+let i32_shr #ty = scalar_shr #I32 #ty
+let i64_shr #ty = scalar_shr #I64 #ty
+let i128_shr #ty = scalar_shr #I128 #ty
+let isize_shr #ty = scalar_shr #Isize #ty
+
+(*** core::ops *)
+
+// Trait declaration: [core::ops::index::Index]
+noeq type core_ops_index_Index (self idx : Type0) = {
+  output : Type0;
+  index : self → idx → result output
+}
+
+// Trait declaration: [core::ops::index::IndexMut]
+noeq type core_ops_index_IndexMut (self idx : Type0) = {
+  indexInst : core_ops_index_Index self idx;
+  index_mut : self → idx → result (indexInst.output & (indexInst.output → result self));
+}
+
+// Trait declaration [core::ops::deref::Deref]
+noeq type core_ops_deref_Deref (self : Type0) = {
+  target : Type0;
+  deref : self → result target;
+}
+
+// Trait declaration [core::ops::deref::DerefMut]
+noeq type core_ops_deref_DerefMut (self : Type0) = {
+  derefInst : core_ops_deref_Deref self;
+  deref_mut : self → result (derefInst.target & (derefInst.target → result self));
+}
+
+type core_ops_range_Range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** [alloc] *)
+
+let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) =
+  Return (x, (fun x -> Return x))
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
+  target = self;
+  deref = alloc_boxed_Box_deref self;
+}
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
+  derefInst = alloc_boxed_Box_coreopsDerefInst self;
+  deref_mut = alloc_boxed_Box_deref_mut self;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  normalize_term_spec (FStar.List.Tot.length l);
+  l
+
+let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
+  if i < length x then Return (index x i)
+  else Fail Failure
+
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+type slice (a : Type0) = s:list a{length s <= usize_max}
+
+let slice_len (a : Type0) (s : slice a) : usize = length s
+
+let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
+  if i < length x then Return (index x i)
+  else Fail Failure
+
+let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Subslices *)
+
+let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
+let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
+  if length s = n then Return s
+  else Fail Failure
+
+// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
+let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
+  admit()
+
+let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) =
+  admit()
+
+let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
+  admit()
+
+let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
+  admit()
+
+let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
+  admit()
+
+(*** Vector *)
+type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max}
+
+let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
+let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
+
+// Helper
+let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
+  if i < length v then Return (index v i) else Fail Failure
+// Helper
+let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
+  if i < length v then Return (list_update v i x) else Fail Failure
+
+let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) :
+  result (a & (a → result (alloc_vec_Vec a))) =
+  match alloc_vec_Vec_index_usize v i with
+  | Return x ->
+    Return (x, alloc_vec_Vec_update_usize v i)
+  | Fail e -> Fail e
+
+let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
+  Pure (result (alloc_vec_Vec a))
+  (requires True)
+  (ensures (fun res ->
+    match res with
+    | Fail e -> e == Failure
+    | Return v' -> length v' = length v + 1)) =
+  if length v < usize_max then begin
+    (**) assert_norm(length [x] == 1);
+    (**) append_length v [x];
+    (**) assert(length (append v [x]) = length v + 1);
+    Return (append v [x])
+    end
+  else Fail Failure
+
+let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
+  if i < length v then Return (list_update v i x) else Fail Failure
+
+// Trait declaration: [core::slice::index::private_slice_index::Sealed]
+type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
+
+// Trait declaration: [core::slice::index::SliceIndex]
+noeq type core_slice_index_SliceIndex (self t : Type0) = {
+  sealedInst : core_slice_index_private_slice_index_Sealed self;
+  output : Type0;
+  get : self → t → result (option output);
+  get_mut : self → t → result (option output & (option output -> result t));
+  get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
+  get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
+  index : self → t → result output;
+  index_mut : self → t → result (output & (output -> result t));
+}
+
+// [core::slice::index::[T]::index]: forward function
+let core_slice_index_Slice_index
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (s : slice t) (i : idx) : result inst.output =
+  let* x = inst.get i s in
+  match x with
+  | None -> Fail Failure
+  | Some x -> Return x
+
+// [core::slice::index::Range:::get]: forward function
+let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
+  result (option (slice t)) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_mut]: forward function
+let core_slice_index_RangeUsize_get_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (option (slice t) & (option (slice t) -> result (slice t))) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_unchecked]: forward function
+let core_slice_index_RangeUsize_get_unchecked
+  (t : Type0) :
+  core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::get_unchecked_mut]: forward function
+let core_slice_index_RangeUsize_get_unchecked_mut
+  (t : Type0) :
+  core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::index]: forward function
+let core_slice_index_RangeUsize_index
+  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::index_mut]: forward function
+let core_slice_index_RangeUsize_index_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (slice t & (slice t -> result (slice t))) =
+  admit () // TODO
+
+// [core::slice::index::[T]::index_mut]: forward function
+let core_slice_index_Slice_index_mut
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
+  slice t → idx → result (inst.output & (inst.output -> result (slice t))) =
+  admit () // 
+
+// [core::array::[T; N]::index]: forward function
+let core_array_Array_index
+  (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
+  (a : array t n) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [core::array::[T; N]::index_mut]: forward function
+let core_array_Array_index_mut
+  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
+  (a : array t n) (i : idx) :
+  result (inst.indexInst.output & (inst.indexInst.output -> result (array t n))) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::Range]
+let core_slice_index_private_slice_index_SealedRangeUsizeInst
+  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
+
+// Trait implementation: [core::slice::index::Range]
+let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
+  output = slice t;
+  get = core_slice_index_RangeUsize_get t;
+  get_mut = core_slice_index_RangeUsize_get_mut t;
+  get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
+  index = core_slice_index_RangeUsize_index t;
+  index_mut = core_slice_index_RangeUsize_index_mut t;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (slice t) idx = {
+  output = inst.output;
+  index = core_slice_index_Slice_index t idx inst;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (slice t) idx = {
+  indexInst = core_ops_index_IndexSliceTIInst t idx inst;
+  index_mut = core_slice_index_Slice_index_mut t idx inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_Index (slice t) idx) :
+  core_ops_index_Index (array t n) idx = {
+  output = inst.output;
+  index = core_array_Array_index t idx n inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_IndexMut (slice t) idx) :
+  core_ops_index_IndexMut (array t n) idx = {
+  indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
+  index_mut = core_array_Array_index_mut t idx n inst;
+}
+
+// [core::slice::index::usize::get]: forward function
+let core_slice_index_usize_get
+  (t : Type0) : usize → slice t → result (option t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_mut]: forward function
+let core_slice_index_usize_get_mut (t : Type0) :
+  usize → slice t → result (option t & (option t -> result (slice t))) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked]: forward function
+let core_slice_index_usize_get_unchecked
+  (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked_mut]: forward function
+let core_slice_index_usize_get_unchecked_mut
+  (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::index]: forward function
+let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
+  admit () // TODO
+
+// [core::slice::index::usize::index_mut]: forward function
+let core_slice_index_usize_index_mut (t : Type0) :
+  usize → slice t → result (t & (t -> result (slice t))) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::usize]
+let core_slice_index_private_slice_index_SealedUsizeInst
+  : core_slice_index_private_slice_index_Sealed usize = ()
+
+// Trait implementation: [core::slice::index::usize]
+let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex usize (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
+  output = t;
+  get = core_slice_index_usize_get t;
+  get_mut = core_slice_index_usize_get_mut t;
+  get_unchecked = core_slice_index_usize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
+  index = core_slice_index_usize_index t;
+  index_mut = core_slice_index_usize_index_mut t;
+}
+
+// [alloc::vec::Vec::index]: forward function
+let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [alloc::vec::Vec::index_mut]: forward function
+let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) :
+  result (inst.output & (inst.output -> result (alloc_vec_Vec t))) =
+  admit () // TODO
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (alloc_vec_Vec t) idx = {
+  output = inst.output;
+  index = alloc_vec_Vec_index t idx inst;
+}
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
+  indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
+  index_mut = alloc_vec_Vec_index_mut t idx inst;
+}
+
+(*** Theorems *)
+
+let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_mut_usize v i)
+  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
diff --git a/backends/fstar/split/Makefile b/backends/fstar/split/Makefile
new file mode 100644
index 00000000..a16b0edb
--- /dev/null
+++ b/backends/fstar/split/Makefile
@@ -0,0 +1,47 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+# Generete the .checked files in batch mode
+%.checked:
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/backends/fstar/split/Primitives.fst b/backends/fstar/split/Primitives.fst
new file mode 100644
index 00000000..a3ffbde4
--- /dev/null
+++ b/backends/fstar/split/Primitives.fst
@@ -0,0 +1,884 @@
+/// This file lists primitive and assumed functions and types
+module Primitives
+open FStar.Mul
+open FStar.List.Tot
+
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+
+(*** Utilities *)
+val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
+  ls':list a{
+    length ls' = length ls /\
+    index ls' i == x
+  }
+#push-options "--fuel 1"
+let rec list_update #a ls i x =
+  match ls with
+  | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
+#pop-options
+
+(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
+type result (a : Type0) : Type0 =
+| Return : v:a -> result a
+| Fail : e:error -> result a
+
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a)
+  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
+  result b =
+  match m with
+  | Return x -> f x
+  | Fail e   -> Fail e
+
+// Monadic assert(...)
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
+
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
+(*** Misc *)
+type char = FStar.Char.char
+type string = string
+
+let is_zero (n: nat) : bool = n = 0
+let decrease (n: nat{n > 0}) : nat = n - 1
+
+let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
+let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+
+// We don't really use raw pointers for now
+type mut_raw_ptr (t : Type0) = { v : t }
+type const_raw_ptr (t : Type0) = { v : t }
+
+(*** Scalars *)
+/// Rem.: most of the following code was partially generated
+
+assume val size_numbits : pos
+
+// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t
+
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
+let i8_min : int = -128
+let i8_max : int = 127
+let i16_min : int = -32768
+let i16_max : int = 32767
+let i32_min : int = -2147483648
+let i32_max : int = 2147483647
+let i64_min : int = -9223372036854775808
+let i64_max : int = 9223372036854775807
+let i128_min : int = -170141183460469231731687303715884105728
+let i128_max : int = 170141183460469231731687303715884105727
+let usize_min : int = 0
+let usize_max : int = 4294967295 // TODO: should be opaque
+let u8_min : int = 0
+let u8_max : int = 255
+let u16_min : int = 0
+let u16_max : int = 65535
+let u32_min : int = 0
+let u32_max : int = 4294967295
+let u64_min : int = 0
+let u64_max : int = 18446744073709551615
+let u128_min : int = 0
+let u128_max : int = 340282366920938463463374607431768211455
+
+type scalar_ty =
+| Isize
+| I8
+| I16
+| I32
+| I64
+| I128
+| Usize
+| U8
+| U16
+| U32
+| U64
+| U128
+
+let is_unsigned = function
+  | Isize | I8 | I16 | I32 | I64 | I128 -> false
+  | Usize | U8 | U16 | U32 | U64 | U128 -> true
+
+let scalar_min (ty : scalar_ty) : int =
+  match ty with
+  | Isize -> isize_min
+  | I8 -> i8_min
+  | I16 -> i16_min
+  | I32 -> i32_min
+  | I64 -> i64_min
+  | I128 -> i128_min
+  | Usize -> usize_min
+  | U8 -> u8_min
+  | U16 -> u16_min
+  | U32 -> u32_min
+  | U64 -> u64_min
+  | U128 -> u128_min
+
+let scalar_max (ty : scalar_ty) : int =
+  match ty with
+  | Isize -> isize_max
+  | I8 -> i8_max
+  | I16 -> i16_max
+  | I32 -> i32_max
+  | I64 -> i64_max
+  | I128 -> i128_max
+  | Usize -> usize_max
+  | U8 -> u8_max
+  | U16 -> u16_max
+  | U32 -> u32_max
+  | U64 -> u64_max
+  | U128 -> u128_max
+
+type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
+
+let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
+
+let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
+
+let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
+
+/// The remainder operation
+let int_rem (x : int) (y : int{y <> 0}) : int =
+  if x >= 0 then (x % y) else -(x % y)
+
+(* Checking consistency with Rust *)
+let _ = assert_norm(int_rem 1 2 = 1)
+let _ = assert_norm(int_rem (-1) 2 = -1)
+let _ = assert_norm(int_rem 1 (-2) = 1)
+let _ = assert_norm(int_rem (-1) (-2) = -1)
+
+let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
+
+let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x + y)
+
+let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x - y)
+
+let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
+  mk_scalar ty (x * y)
+
+let scalar_xor (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logxor #8 x y
+  | U16 -> FStar.UInt.logxor #16 x y
+  | U32 -> FStar.UInt.logxor #32 x y
+  | U64 -> FStar.UInt.logxor #64 x y
+  | U128 -> FStar.UInt.logxor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logxor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logxor #16 x y
+  | I32 -> FStar.Int.logxor #32 x y
+  | I64 -> FStar.Int.logxor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logxor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_or (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logor #8 x y
+  | U16 -> FStar.UInt.logor #16 x y
+  | U32 -> FStar.UInt.logor #32 x y
+  | U64 -> FStar.UInt.logor #64 x y
+  | U128 -> FStar.UInt.logor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logor #16 x y
+  | I32 -> FStar.Int.logor #32 x y
+  | I64 -> FStar.Int.logor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_and (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logand #8 x y
+  | U16 -> FStar.UInt.logand #16 x y
+  | U32 -> FStar.UInt.logand #32 x y
+  | U64 -> FStar.UInt.logand #64 x y
+  | U128 -> FStar.UInt.logand #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logand #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logand #16 x y
+  | I32 -> FStar.Int.logand #32 x y
+  | I64 -> FStar.Int.logand #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logand #128 x y
+  | Isize -> admit() // TODO
+
+// Shift left
+let scalar_shl (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
+
+// Shift right
+let scalar_shr (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
+
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty x
+
+// This can't fail, but for now we make all casts faillible (easier for the translation)
+let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty (if x then 1 else 0)
+
+/// The scalar types
+type isize : eqtype = scalar Isize
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
+type usize : eqtype = scalar Usize
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
+
+/// Negation
+let isize_neg = scalar_neg #Isize
+let i8_neg = scalar_neg #I8
+let i16_neg = scalar_neg #I16
+let i32_neg = scalar_neg #I32
+let i64_neg = scalar_neg #I64
+let i128_neg = scalar_neg #I128
+
+/// Division
+let isize_div = scalar_div #Isize
+let i8_div = scalar_div #I8
+let i16_div = scalar_div #I16
+let i32_div = scalar_div #I32
+let i64_div = scalar_div #I64
+let i128_div = scalar_div #I128
+let usize_div = scalar_div #Usize
+let u8_div = scalar_div #U8
+let u16_div = scalar_div #U16
+let u32_div = scalar_div #U32
+let u64_div = scalar_div #U64
+let u128_div = scalar_div #U128
+
+/// Remainder
+let isize_rem = scalar_rem #Isize
+let i8_rem = scalar_rem #I8
+let i16_rem = scalar_rem #I16
+let i32_rem = scalar_rem #I32
+let i64_rem = scalar_rem #I64
+let i128_rem = scalar_rem #I128
+let usize_rem = scalar_rem #Usize
+let u8_rem = scalar_rem #U8
+let u16_rem = scalar_rem #U16
+let u32_rem = scalar_rem #U32
+let u64_rem = scalar_rem #U64
+let u128_rem = scalar_rem #U128
+
+/// Addition
+let isize_add = scalar_add #Isize
+let i8_add = scalar_add #I8
+let i16_add = scalar_add #I16
+let i32_add = scalar_add #I32
+let i64_add = scalar_add #I64
+let i128_add = scalar_add #I128
+let usize_add = scalar_add #Usize
+let u8_add = scalar_add #U8
+let u16_add = scalar_add #U16
+let u32_add = scalar_add #U32
+let u64_add = scalar_add #U64
+let u128_add = scalar_add #U128
+
+/// Subtraction
+let isize_sub = scalar_sub #Isize
+let i8_sub = scalar_sub #I8
+let i16_sub = scalar_sub #I16
+let i32_sub = scalar_sub #I32
+let i64_sub = scalar_sub #I64
+let i128_sub = scalar_sub #I128
+let usize_sub = scalar_sub #Usize
+let u8_sub = scalar_sub #U8
+let u16_sub = scalar_sub #U16
+let u32_sub = scalar_sub #U32
+let u64_sub = scalar_sub #U64
+let u128_sub = scalar_sub #U128
+
+/// Multiplication
+let isize_mul = scalar_mul #Isize
+let i8_mul = scalar_mul #I8
+let i16_mul = scalar_mul #I16
+let i32_mul = scalar_mul #I32
+let i64_mul = scalar_mul #I64
+let i128_mul = scalar_mul #I128
+let usize_mul = scalar_mul #Usize
+let u8_mul = scalar_mul #U8
+let u16_mul = scalar_mul #U16
+let u32_mul = scalar_mul #U32
+let u64_mul = scalar_mul #U64
+let u128_mul = scalar_mul #U128
+
+/// Xor
+let u8_xor = scalar_xor #U8
+let u16_xor = scalar_xor #U16
+let u32_xor = scalar_xor #U32
+let u64_xor = scalar_xor #U64
+let u128_xor = scalar_xor #U128
+let usize_xor = scalar_xor #Usize
+let i8_xor = scalar_xor #I8
+let i16_xor = scalar_xor #I16
+let i32_xor = scalar_xor #I32
+let i64_xor = scalar_xor #I64
+let i128_xor = scalar_xor #I128
+let isize_xor = scalar_xor #Isize
+
+/// Or
+let u8_or = scalar_or #U8
+let u16_or = scalar_or #U16
+let u32_or = scalar_or #U32
+let u64_or = scalar_or #U64
+let u128_or = scalar_or #U128
+let usize_or = scalar_or #Usize
+let i8_or = scalar_or #I8
+let i16_or = scalar_or #I16
+let i32_or = scalar_or #I32
+let i64_or = scalar_or #I64
+let i128_or = scalar_or #I128
+let isize_or = scalar_or #Isize
+
+/// And
+let u8_and = scalar_and #U8
+let u16_and = scalar_and #U16
+let u32_and = scalar_and #U32
+let u64_and = scalar_and #U64
+let u128_and = scalar_and #U128
+let usize_and = scalar_and #Usize
+let i8_and = scalar_and #I8
+let i16_and = scalar_and #I16
+let i32_and = scalar_and #I32
+let i64_and = scalar_and #I64
+let i128_and = scalar_and #I128
+let isize_and = scalar_and #Isize
+
+/// Shift left
+let u8_shl #ty = scalar_shl #U8 #ty
+let u16_shl #ty = scalar_shl #U16 #ty
+let u32_shl #ty = scalar_shl #U32 #ty
+let u64_shl #ty = scalar_shl #U64 #ty
+let u128_shl #ty = scalar_shl #U128 #ty
+let usize_shl #ty = scalar_shl #Usize #ty
+let i8_shl #ty = scalar_shl #I8 #ty
+let i16_shl #ty = scalar_shl #I16 #ty
+let i32_shl #ty = scalar_shl #I32 #ty
+let i64_shl #ty = scalar_shl #I64 #ty
+let i128_shl #ty = scalar_shl #I128 #ty
+let isize_shl #ty = scalar_shl #Isize #ty
+
+/// Shift right
+let u8_shr #ty = scalar_shr #U8 #ty
+let u16_shr #ty = scalar_shr #U16 #ty
+let u32_shr #ty = scalar_shr #U32 #ty
+let u64_shr #ty = scalar_shr #U64 #ty
+let u128_shr #ty = scalar_shr #U128 #ty
+let usize_shr #ty = scalar_shr #Usize #ty
+let i8_shr #ty = scalar_shr #I8 #ty
+let i16_shr #ty = scalar_shr #I16 #ty
+let i32_shr #ty = scalar_shr #I32 #ty
+let i64_shr #ty = scalar_shr #I64 #ty
+let i128_shr #ty = scalar_shr #I128 #ty
+let isize_shr #ty = scalar_shr #Isize #ty
+
+(*** core::ops *)
+
+// Trait declaration: [core::ops::index::Index]
+noeq type core_ops_index_Index (self idx : Type0) = {
+  output : Type0;
+  index : self → idx → result output
+}
+
+// Trait declaration: [core::ops::index::IndexMut]
+noeq type core_ops_index_IndexMut (self idx : Type0) = {
+  indexInst : core_ops_index_Index self idx;
+  index_mut : self → idx → result indexInst.output;
+  index_mut_back : self → idx → indexInst.output → result self;
+}
+
+// Trait declaration [core::ops::deref::Deref]
+noeq type core_ops_deref_Deref (self : Type0) = {
+  target : Type0;
+  deref : self → result target;
+}
+
+// Trait declaration [core::ops::deref::DerefMut]
+noeq type core_ops_deref_DerefMut (self : Type0) = {
+  derefInst : core_ops_deref_Deref self;
+  deref_mut : self → result derefInst.target;
+  deref_mut_back : self → derefInst.target → result self;
+}
+
+type core_ops_range_Range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** [alloc] *)
+
+let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
+  target = self;
+  deref = alloc_boxed_Box_deref self;
+}
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
+  derefInst = alloc_boxed_Box_coreopsDerefInst self;
+  deref_mut = alloc_boxed_Box_deref_mut self;
+  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  normalize_term_spec (FStar.List.Tot.length l);
+  l
+
+let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
+  if i < length x then Return (index x i)
+  else Fail Failure
+
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+type slice (a : Type0) = s:list a{length s <= usize_max}
+
+let slice_len (a : Type0) (s : slice a) : usize = length s
+
+let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
+  if i < length x then Return (index x i)
+  else Fail Failure
+
+let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Subslices *)
+
+let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
+let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
+  if length s = n then Return s
+  else Fail Failure
+
+// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
+let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
+  admit()
+
+let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) =
+  admit()
+
+let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
+  admit()
+
+let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
+  admit()
+
+let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
+  admit()
+
+(*** Vector *)
+type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max}
+
+let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
+let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
+
+// Helper
+let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
+  if i < length v then Return (index v i) else Fail Failure
+// Helper
+let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
+  if i < length v then Return (list_update v i x) else Fail Failure
+
+// The **forward** function shouldn't be used
+let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
+let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
+  Pure (result (alloc_vec_Vec a))
+  (requires True)
+  (ensures (fun res ->
+    match res with
+    | Fail e -> e == Failure
+    | Return v' -> length v' = length v + 1)) =
+  if length v < usize_max then begin
+    (**) assert_norm(length [x] == 1);
+    (**) append_length v [x];
+    (**) assert(length (append v [x]) = length v + 1);
+    Return (append v [x])
+    end
+  else Fail Failure
+
+// The **forward** function shouldn't be used
+let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
+  if i < length v then Return () else Fail Failure
+let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
+  if i < length v then Return (list_update v i x) else Fail Failure
+
+// Trait declaration: [core::slice::index::private_slice_index::Sealed]
+type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
+
+// Trait declaration: [core::slice::index::SliceIndex]
+noeq type core_slice_index_SliceIndex (self t : Type0) = {
+  sealedInst : core_slice_index_private_slice_index_Sealed self;
+  output : Type0;
+  get : self → t → result (option output);
+  get_mut : self → t → result (option output);
+  get_mut_back : self → t → option output → result t;
+  get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
+  get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
+  index : self → t → result output;
+  index_mut : self → t → result output;
+  index_mut_back : self → t → output → result t;
+}
+
+// [core::slice::index::[T]::index]: forward function
+let core_slice_index_Slice_index
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (s : slice t) (i : idx) : result inst.output =
+  let* x = inst.get i s in
+  match x with
+  | None -> Fail Failure
+  | Some x -> Return x
+
+// [core::slice::index::Range:::get]: forward function
+let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
+  result (option (slice t)) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_mut]: forward function
+let core_slice_index_RangeUsize_get_mut
+  (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_mut]: backward function 0
+let core_slice_index_RangeUsize_get_mut_back
+  (t : Type0) :
+  core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_unchecked]: forward function
+let core_slice_index_RangeUsize_get_unchecked
+  (t : Type0) :
+  core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::get_unchecked_mut]: forward function
+let core_slice_index_RangeUsize_get_unchecked_mut
+  (t : Type0) :
+  core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::index]: forward function
+let core_slice_index_RangeUsize_index
+  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::index_mut]: forward function
+let core_slice_index_RangeUsize_index_mut
+  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::index_mut]: backward function 0
+let core_slice_index_RangeUsize_index_mut_back
+  (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::[T]::index_mut]: forward function
+let core_slice_index_Slice_index_mut
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
+  slice t → idx → result inst.output =
+  admit () // 
+
+// [core::slice::index::[T]::index_mut]: backward function 0
+let core_slice_index_Slice_index_mut_back
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
+  slice t → idx → inst.output → result (slice t) =
+  admit () // TODO
+
+// [core::array::[T; N]::index]: forward function
+let core_array_Array_index
+  (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
+  (a : array t n) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [core::array::[T; N]::index_mut]: forward function
+let core_array_Array_index_mut
+  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
+  (a : array t n) (i : idx) : result inst.indexInst.output =
+  admit () // TODO
+
+// [core::array::[T; N]::index_mut]: backward function 0
+let core_array_Array_index_mut_back
+  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
+  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::Range]
+let core_slice_index_private_slice_index_SealedRangeUsizeInst
+  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
+
+// Trait implementation: [core::slice::index::Range]
+let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
+  output = slice t;
+  get = core_slice_index_RangeUsize_get t;
+  get_mut = core_slice_index_RangeUsize_get_mut t;
+  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
+  get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
+  index = core_slice_index_RangeUsize_index t;
+  index_mut = core_slice_index_RangeUsize_index_mut t;
+  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (slice t) idx = {
+  output = inst.output;
+  index = core_slice_index_Slice_index t idx inst;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (slice t) idx = {
+  indexInst = core_ops_index_IndexSliceTIInst t idx inst;
+  index_mut = core_slice_index_Slice_index_mut t idx inst;
+  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_Index (slice t) idx) :
+  core_ops_index_Index (array t n) idx = {
+  output = inst.output;
+  index = core_array_Array_index t idx n inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_IndexMut (slice t) idx) :
+  core_ops_index_IndexMut (array t n) idx = {
+  indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
+  index_mut = core_array_Array_index_mut t idx n inst;
+  index_mut_back = core_array_Array_index_mut_back t idx n inst;
+}
+
+// [core::slice::index::usize::get]: forward function
+let core_slice_index_usize_get
+  (t : Type0) : usize → slice t → result (option t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_mut]: forward function
+let core_slice_index_usize_get_mut
+  (t : Type0) : usize → slice t → result (option t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_mut]: backward function 0
+let core_slice_index_usize_get_mut_back
+  (t : Type0) : usize → slice t → option t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked]: forward function
+let core_slice_index_usize_get_unchecked
+  (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked_mut]: forward function
+let core_slice_index_usize_get_unchecked_mut
+  (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::index]: forward function
+let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
+  admit () // TODO
+
+// [core::slice::index::usize::index_mut]: forward function
+let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
+  admit () // TODO
+
+// [core::slice::index::usize::index_mut]: backward function 0
+let core_slice_index_usize_index_mut_back
+  (t : Type0) : usize → slice t → t → result (slice t) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::usize]
+let core_slice_index_private_slice_index_SealedUsizeInst
+  : core_slice_index_private_slice_index_Sealed usize = ()
+
+// Trait implementation: [core::slice::index::usize]
+let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex usize (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
+  output = t;
+  get = core_slice_index_usize_get t;
+  get_mut = core_slice_index_usize_get_mut t;
+  get_mut_back = core_slice_index_usize_get_mut_back t;
+  get_unchecked = core_slice_index_usize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
+  index = core_slice_index_usize_index t;
+  index_mut = core_slice_index_usize_index_mut t;
+  index_mut_back = core_slice_index_usize_index_mut_back t;
+}
+
+// [alloc::vec::Vec::index]: forward function
+let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [alloc::vec::Vec::index_mut]: forward function
+let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [alloc::vec::Vec::index_mut]: backward function 0
+let alloc_vec_Vec_index_mut_back
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
+  admit () // TODO
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (alloc_vec_Vec t) idx = {
+  output = inst.output;
+  index = alloc_vec_Vec_index t idx inst;
+}
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
+  indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
+  index_mut = alloc_vec_Vec_index_mut t idx inst;
+  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
+}
+
+(*** Theorems *)
+
+let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
+  Lemma (
+    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
+      alloc_vec_Vec_update_usize v i x)
+  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
+  =
+  admit()
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 24d16dca..ee8d4831 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -232,6 +232,14 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
   let mk_fun (rust_name : string) (extract_name : string option)
       (filter : bool list option) (with_back : bool) (back_no_suffix : bool) :
       pattern * bool list option * builtin_fun_info list =
+    (* [back_no_suffix] is used to control whether the backward function should
+       have the suffix "_back" or not (if not, then the forward function has the
+       prefix "_fwd", and is filtered anyway). This is pertinent only if we split
+       the fwd/back functions. *)
+    let back_no_suffix = back_no_suffix && not !Config.return_back_funs in
+    (* Same for the [with_back] option: this is pertinent only if we split
+       the fwd/back functions *)
+    let with_back = with_back && not !Config.return_back_funs in
     let rust_name =
       try parse_pattern rust_name
       with Failure _ ->
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index ccc46420..55a94302 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1171,7 +1171,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     let exe_dir = Filename.dirname Sys.argv.(0) in
     let primitives_src_dest =
       match !Config.backend with
-      | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
+      | FStar ->
+          let src =
+            if !Config.return_back_funs then
+              "/backends/fstar/merge/Primitives.fst"
+            else "/backends/fstar/split/Primitives.fst"
+          in
+          Some (src, "Primitives.fst")
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
       | HOL4 -> None
-- 
cgit v1.3.1