Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

28 files changed, 2404 insertions, 1248 deletions

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/Config.ml b/compiler/Config.ml
index b09544ba..2bb1ca34 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -92,6 +92,69 @@ let loop_fixed_point_max_num_iters = 2
 
 (** {1 Translation} *)
 
+(** If true, do not define separate forward/backward functions, but make the
+    forward functions return the backward function.
+
+    Example:
+    {[
+      (* Rust *)
+      pub fn list_nth<'a, T>(l: &'a mut List<T>, i: u32) -> &'a mut T {
+          match l {
+              List::Nil => {
+                  panic!()
+              }
+              List::Cons(x, tl) => {
+                  if i == 0 {
+                      x
+                  } else {
+                      list_nth(tl, i - 1)
+                  }
+              }
+          }
+      }
+
+      (* Translation, if return_back_funs = false *)
+      def list_nth (T : Type) (l : List T) (i : U32) : Result T :=
+        match l with
+        | List.Cons x tl =>
+          if i = 0#u32
+          then Result.ret x
+          else do
+                 let i0 ← i - 1#u32
+                 list_nth T tl i0
+        | List.Nil => Result.fail .panic
+
+      def list_nth_back
+        (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
+        match l with
+        | List.Cons x tl =>
+          if i = 0#u32
+          then Result.ret (List.Cons ret tl)
+          else
+            do
+              let i0 ← i - 1#u32
+              let tl0 ← list_nth_back T tl i0 ret
+              Result.ret (List.Cons x tl0)
+        | List.Nil => Result.fail .panic
+
+      (* Translation, if return_back_funs = true *)
+      def list_nth (T: Type) (ls : List T) (i : U32) :
+        Result (T × (T → Result (List T))) :=
+        match ls with
+        | List.Cons x tl =>
+          if i = 0#u32
+          then Result.ret (x, (λ ret => return (ret :: ls)))
+          else do
+            let i0 ← i - 1#u32
+            let (x, back) ← list_nth ls i0
+            Return.ret (x,
+              (λ ret => do
+               let ls ← back ret
+               return (x :: ls)))
+    ]}
+ *)
+let return_back_funs = ref true
+
 (** Forbids using field projectors for structures.
 
     If we don't use field projectors, whenever we symbolically expand a structure
@@ -307,6 +370,32 @@ let filter_useless_monadic_calls = ref true
  *)
 let filter_useless_functions = ref true
 
+(** Simplify the forward/backward functions, in case we merge them
+    (i.e., the forward functions return the backward functions).
+
+    The simplification occurs as follows:
+    - if a forward function returns the unit type and has non-trivial backward
+      functions, then we remove the returned output.
+    - if a backward function doesn't have inputs, we evaluate it inside the
+      forward function and don't wrap it in a result.
+
+    Example:
+    {[
+      // LLBC:
+      fn incr(x: &mut u32) { *x += 1 }
+
+      // Translation without simplification:
+      let incr (x : u32) : result (unit * result u32) = ...
+                                   ^^^^   ^^^^^^
+                                    |     remove this result
+                                remove the unit
+
+      // Translation with simplification:
+      let incr (x : u32) : result u32 = ...
+    ]}
+ *)
+let simplify_merged_fwd_backs = ref true
+
 (** Use short names for the record fields.
 
     Some backends can't disambiguate records when their field names have collisions.
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/Extract.ml b/compiler/Extract.ml
index 20cdb20b..87dcb1fd 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -43,8 +43,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
                 }
             | _ -> ctx
           in
-          let backs = List.map (fun f -> f.f) def.backs in
-          let funs = if def.keep_fwd then def.fwd.f :: backs else backs in
+          let funs =
+            if !Config.return_back_funs then [ def.fwd.f ]
+            else
+              let backs = List.map (fun f -> f.f) def.backs in
+              if def.keep_fwd then def.fwd.f :: backs else backs
+          in
           List.fold_left
             (fun ctx (f : fun_decl) ->
               let open ExtractBuiltin in
@@ -128,9 +132,15 @@ let extract_adt_g_value
       F.pp_print_string fmt "tt";
       ctx)
     else
-      (* If there is exactly one value, we don't print the parentheses *)
+      (* If there is exactly one value, we don't print the parentheses.
+         Also, for Coq, we need the special syntax ['(...)] if we destruct
+         a tuple pattern in a let-binding and the tuple has > 2 values.
+      *)
       let lb, rb =
-        if List.length field_values = 1 then ("", "") else ("(", ")")
+        if List.length field_values = 1 then ("", "")
+        else if !backend = Coq && is_single_pat && List.length field_values > 2
+        then ("'(", ")")
+        else ("(", ")")
       in
       F.pp_print_string fmt lb;
       let ctx =
@@ -237,30 +247,60 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
         Result.Ok types
 
 (** [inside]: see {!extract_ty}.
+    [with_type]: do we also generate a type annotation? This is necessary for
+    backends like Coq when we write lambdas (Coq is not powerful enough to
+    infer the type).
 
     As a pattern can introduce new variables, we return an extraction context
     updated with new bindings.
  *)
 let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
-    (is_let : bool) (inside : bool) (v : typed_pattern) : extraction_ctx =
-  match v.value with
-  | PatConstant cv ->
-      extract_literal fmt inside cv;
-      ctx
-  | PatVar (v, _) ->
-      let vname = ctx_compute_var_basename ctx v.basename v.ty in
-      let ctx, vname = ctx_add_var vname v.id ctx in
-      F.pp_print_string fmt vname;
-      ctx
-  | PatDummy ->
-      F.pp_print_string fmt "_";
-      ctx
-  | PatAdt av ->
-      let extract_value ctx inside v =
-        extract_typed_pattern ctx fmt is_let inside v
-      in
-      extract_adt_g_value extract_value fmt ctx is_let inside av.variant_id
-        av.field_values v.ty
+    (is_let : bool) (inside : bool) ?(with_type = false) (v : typed_pattern) :
+    extraction_ctx =
+  if with_type then F.pp_print_string fmt "(";
+  let inside = inside && not with_type in
+  let ctx =
+    match v.value with
+    | PatConstant cv ->
+        extract_literal fmt inside cv;
+        ctx
+    | PatVar (v, _) ->
+        let vname = ctx_compute_var_basename ctx v.basename v.ty in
+        let ctx, vname = ctx_add_var vname v.id ctx in
+        F.pp_print_string fmt vname;
+        ctx
+    | PatDummy ->
+        F.pp_print_string fmt "_";
+        ctx
+    | PatAdt av ->
+        let extract_value ctx inside v =
+          extract_typed_pattern ctx fmt is_let inside v
+        in
+        extract_adt_g_value extract_value fmt ctx is_let inside av.variant_id
+          av.field_values v.ty
+  in
+  if with_type then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    extract_ty ctx fmt TypeDeclId.Set.empty false v.ty;
+    F.pp_print_string fmt ")");
+  ctx
+
+(** Return true if we need to wrap a succession of let-bindings in a [do ...]
+    block (because some of them are monadic) *)
+let lets_require_wrap_in_do (lets : (bool * typed_pattern * texpression) list) :
+    bool =
+  match !backend with
+  | Lean ->
+      (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
+      List.exists (fun (m, _, _) -> m) lets
+  | HOL4 ->
+      (* HOL4 is similar to HOL4, but we add a sanity check *)
+      let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
+      if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets);
+      wrap_in_do
+  | FStar | Coq -> false
 
 (** [inside]: controls the introduction of parentheses. See [extract_ty]
 
@@ -285,9 +325,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
   | App _ ->
       let app, args = destruct_apps e in
       extract_App ctx fmt inside app args
-  | Abs _ ->
-      let xl, e = destruct_abs_list e in
-      extract_Abs ctx fmt inside xl e
+  | Lambda _ ->
+      let xl, e = destruct_lambdas e in
+      extract_Lambda ctx fmt inside xl e
   | Qualif _ ->
       (* We use the app case *)
       extract_App ctx fmt inside e []
@@ -574,7 +614,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
       (* No argument: shouldn't happen *)
       raise (Failure "Unreachable")
 
-and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (xl : typed_pattern list) (e : texpression) : unit =
   (* Open a box for the abs expression *)
   F.pp_open_hovbox fmt ctx.indent_incr;
@@ -583,15 +623,16 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   (* Print the lambda - note that there should always be at least one variable *)
   assert (xl <> []);
   F.pp_print_string fmt "fun";
+  let with_type = !backend = Coq in
   let ctx =
     List.fold_left
       (fun ctx x ->
         F.pp_print_space fmt ();
-        extract_typed_pattern ctx fmt true true x)
+        extract_typed_pattern ctx fmt true true ~with_type x)
       ctx xl
   in
   F.pp_print_space fmt ();
-  if !backend = Lean then F.pp_print_string fmt "=>"
+  if !backend = Lean || !backend = Coq then F.pp_print_string fmt "=>"
   else F.pp_print_string fmt "->";
   F.pp_print_space fmt ();
   (* Print the body *)
@@ -630,15 +671,6 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     | HOL4 -> destruct_lets_no_interleave e
     | FStar | Coq | Lean -> destruct_lets e
   in
-  (* Open a box for the whole expression.
-
-     In the case of Lean, we use a vbox so that line breaks are inserted
-     at the end of every let-binding: let-bindings are indeed not ended
-     with an "in" keyword.
-  *)
-  if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
-  (* Open parentheses *)
-  if inside && !backend <> Lean then F.pp_print_string fmt "(";
   (* Extract the let-bindings *)
   let extract_let (ctx : extraction_ctx) (monadic : bool) (lv : typed_pattern)
       (re : texpression) : extraction_ctx =
@@ -711,22 +743,19 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (* Return *)
     ctx
   in
+  (* Open a box for the whole expression.
+
+     In the case of Lean, we use a vbox so that line breaks are inserted
+     at the end of every let-binding: let-bindings are indeed not ended
+     with an "in" keyword.
+  *)
+  if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+  (* Open parentheses *)
+  if inside && !backend <> Lean then F.pp_print_string fmt "(";
   (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
      immediately *)
-  let wrap_in_do_od =
-    match !backend with
-    | Lean ->
-        (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
-        List.exists (fun (m, _, _) -> m) lets
-    | HOL4 ->
-        (* HOL4 is similar to HOL4, but we add a sanity check *)
-        let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
-        if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets);
-        wrap_in_do
-    | FStar | Coq -> false
-  in
+  let wrap_in_do_od = lets_require_wrap_in_do lets in
   if wrap_in_do_od then (
-    F.pp_open_vbox fmt (if !backend = Lean then ctx.indent_incr else 0);
     F.pp_print_string fmt "do";
     F.pp_print_space fmt ());
   let ctx =
@@ -742,11 +771,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   F.pp_close_box fmt ();
 
   (* do-box (Lean and HOL4 only) *)
-  if wrap_in_do_od then (
+  if wrap_in_do_od then
     if !backend = HOL4 then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "od");
-    F.pp_close_box fmt ());
   (* Close parentheses *)
   if inside && !backend <> Lean then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
@@ -1319,16 +1347,16 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
       (Pure.FunId (FRegular def.def_id), def.loop_id, def.back_id)
       ctx.fun_name_info
   in
-  let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]: " in
+  let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]:" in
   let comment =
     let loop_comment =
       match def.loop_id with
       | None -> ""
-      | Some id -> "loop " ^ LoopId.to_string id ^ ": "
+      | Some id -> " loop " ^ LoopId.to_string id ^ ":"
     in
     let fwd_back_comment =
       match def.back_id with
-      | None -> [ "forward function" ]
+      | None -> if !Config.return_back_funs then [] 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
@@ -1340,9 +1368,9 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
           else [ "backward function " ^ T.RegionGroupId.to_string id ]
     in
     match fwd_back_comment with
-    | [] -> raise (Failure "Unreachable")
-    | [ s ] -> [ comment_pre ^ loop_comment ^ s ]
-    | s :: sl -> (comment_pre ^ loop_comment ^ s) :: sl
+    | [] -> [ comment_pre ^ loop_comment ]
+    | [ s ] -> [ comment_pre ^ loop_comment ^ " " ^ s ]
+    | s :: sl -> (comment_pre ^ loop_comment ^ " " ^ s) :: sl
   in
   extract_comment_with_span fmt comment def.meta.span
 
@@ -1470,7 +1498,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
       let inputs_lvs =
         let all_inputs = (Option.get def.body).inputs_lvs in
         let num_fwd_inputs =
-          def.signature.info.num_fwd_inputs_with_fuel_with_state
+          def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state
         in
         Collections.List.prefix num_fwd_inputs all_inputs
       in
@@ -1516,7 +1544,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     let def_body = Option.get def.body in
     let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
     let num_fwd_inputs =
-      def.signature.info.num_fwd_inputs_with_fuel_with_state
+      def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state
     in
     let vars = Collections.List.prefix num_fwd_inputs all_vars in
 
@@ -1794,7 +1822,6 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   assert body.is_global_decl_body;
   assert (Option.is_none body.back_id);
   assert (body.signature.inputs = []);
-  assert (List.length body.signature.doutputs = 1);
   assert (body.signature.generics = empty_generic_params);
 
   (* Add a break then the name of the corresponding LLBC declaration *)
@@ -1813,7 +1840,8 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   let decl_ty, body_ty =
     let ty = body.signature.output in
-    if body.signature.info.effect_info.can_fail then (unwrap_result_ty ty, ty)
+    if body.signature.fwd_info.effect_info.can_fail then
+      (unwrap_result_ty ty, ty)
     else (ty, mk_result_ty ty)
   in
   match body.body with
@@ -1984,7 +2012,8 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
     (* We add one field per required forward/backward function *)
     let get_funs_for_id (id : fun_decl_id) : fun_decl list =
       let trans : pure_fun_translation = FunDeclId.Map.find id ctx.trans_funs in
-      List.map (fun f -> f.f) (trans.fwd :: trans.backs)
+      if !Config.return_back_funs then [ trans.fwd.f ]
+      else List.map (fun f -> f.f) (trans.fwd :: trans.backs)
     in
     match builtin_info with
     | None ->
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index eb2a2ec9..db887539 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -351,7 +351,7 @@ let basename_to_unique (names_set : StringSet.t)
     let s = append basename i in
     if StringSet.mem s names_set then gen (i + 1) else s
   in
-  if StringSet.mem basename names_set then gen 0 else basename
+  if StringSet.mem basename names_set then gen 1 else basename
 
 type fun_name_info = { keep_fwd : bool; num_backs : int }
 
@@ -1051,33 +1051,60 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
 let assumed_llbc_functions () :
     (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
   let rg0 = Some T.RegionGroupId.zero in
-  match !backend with
-  | FStar | Coq | HOL4 ->
-      [
-        (ArrayIndexShared, None, "array_index_usize");
-        (ArrayIndexMut, None, "array_index_usize");
-        (ArrayIndexMut, rg0, "array_update_usize");
-        (ArrayToSliceShared, None, "array_to_slice");
-        (ArrayToSliceMut, None, "array_to_slice");
-        (ArrayToSliceMut, rg0, "array_from_slice");
-        (ArrayRepeat, None, "array_repeat");
-        (SliceIndexShared, None, "slice_index_usize");
-        (SliceIndexMut, None, "slice_index_usize");
-        (SliceIndexMut, rg0, "slice_update_usize");
-      ]
-  | Lean ->
-      [
-        (ArrayIndexShared, None, "Array.index_usize");
-        (ArrayIndexMut, None, "Array.index_usize");
-        (ArrayIndexMut, rg0, "Array.update_usize");
-        (ArrayToSliceShared, None, "Array.to_slice");
-        (ArrayToSliceMut, None, "Array.to_slice");
-        (ArrayToSliceMut, rg0, "Array.from_slice");
-        (ArrayRepeat, None, "Array.repeat");
-        (SliceIndexShared, None, "Slice.index_usize");
-        (SliceIndexMut, None, "Slice.index_usize");
-        (SliceIndexMut, rg0, "Slice.update_usize");
-      ]
+  let regular : (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+    match !backend with
+    | FStar | Coq | HOL4 ->
+        [
+          (ArrayIndexShared, None, "array_index_usize");
+          (ArrayToSliceShared, None, "array_to_slice");
+          (ArrayRepeat, None, "array_repeat");
+          (SliceIndexShared, None, "slice_index_usize");
+        ]
+    | Lean ->
+        [
+          (ArrayIndexShared, None, "Array.index_usize");
+          (ArrayToSliceShared, None, "Array.to_slice");
+          (ArrayRepeat, None, "Array.repeat");
+          (SliceIndexShared, None, "Slice.index_usize");
+        ]
+  in
+  let mut_funs : (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+    if !Config.return_back_funs then
+      match !backend with
+      | FStar | Coq | HOL4 ->
+          [
+            (ArrayIndexMut, None, "array_index_mut_usize");
+            (ArrayToSliceMut, None, "array_to_slice_mut");
+            (SliceIndexMut, None, "slice_index_mut_usize");
+          ]
+      | Lean ->
+          [
+            (ArrayIndexMut, None, "Array.index_mut_usize");
+            (ArrayToSliceMut, None, "Array.to_slice_mut");
+            (SliceIndexMut, None, "Slice.index_mut_usize");
+          ]
+    else
+      match !backend with
+      | FStar | Coq | HOL4 ->
+          [
+            (ArrayIndexMut, None, "array_index_usize");
+            (ArrayIndexMut, rg0, "array_update_usize");
+            (ArrayToSliceMut, None, "array_to_slice");
+            (ArrayToSliceMut, rg0, "array_from_slice");
+            (SliceIndexMut, None, "slice_index_usize");
+            (SliceIndexMut, rg0, "slice_update_usize");
+          ]
+      | Lean ->
+          [
+            (ArrayIndexMut, None, "Array.index_usize");
+            (ArrayIndexMut, rg0, "Array.update_usize");
+            (ArrayToSliceMut, None, "Array.to_slice");
+            (ArrayToSliceMut, rg0, "Array.from_slice");
+            (SliceIndexMut, None, "Slice.index_usize");
+            (SliceIndexMut, rg0, "Slice.update_usize");
+          ]
+  in
+  regular @ mut_funs
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
   match !backend with
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/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/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index f8d979f4..b975371c 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -52,7 +52,7 @@ val eval_operands :
 
     Transmits the computed rvalue to the received continuation.
 
-    Note that this function fails on {!constructor:Aeneas.Expressions.rvalue.Discriminant}: discriminant
+    Note that this function fails on {!Aeneas.Expressions.rvalue.Discriminant}: discriminant
     reads should have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
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..97c8bcd6 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -728,7 +728,13 @@ 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
+    * (generic_args * trait_instance_id) option
+    * fun_decl
+    * region_var_groups
+    * inst_fun_sig =
   match call.func with
   | FnOpMove _ ->
       (* Closure case: TODO *)
@@ -747,13 +753,13 @@ 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
               regions_hierarchy
           in
-          (func.func, func.generics, def, inst_sg)
+          (func.func, func.generics, None, def, regions_hierarchy, inst_sg)
       | FunId (FAssumed _) ->
           (* Unreachable: must be a transparent function *)
           raise (Failure "Unreachable")
@@ -793,7 +799,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
@@ -806,7 +812,12 @@ 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,
+                    Some (generics, tr_self),
+                    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) *)
@@ -853,14 +864,19 @@ 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 =
                     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,
+                    Some (all_generics, tr_self),
+                    method_def,
+                    regions_hierarchy,
+                    inst_sg ))
           | _ ->
               (* We are using a local clause - we lookup the trait decl *)
               let trait_decl =
@@ -884,14 +900,19 @@ 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 =
                 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,
+                Some (generics, tr_self),
+                method_def,
+                regions_hierarchy,
+                inst_sg )))
 
 (** Evaluate a statement *)
 let rec eval_statement (config : config) (st : statement) : st_cm_fun =
@@ -1277,14 +1298,15 @@ 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, trait_method_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 trait_method_generics call.args call.dest
+    cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1298,8 +1320,11 @@ 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)
-    (generics : generic_args) (args : operand list) (dest : place) : st_cm_fun =
+    (fid : fun_id_or_trait_method_ref) (sg : fun_sig)
+    (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig)
+    (generics : generic_args)
+    (trait_method_generics : (generic_args * trait_instance_id) option)
+    (args : operand list) (dest : place) : st_cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -1378,8 +1403,9 @@ 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 trait_method_generics args args_places ret_spc dest_place
+      expr
   in
   let cc = comp cc cf_call in
 
@@ -1450,7 +1476,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):
@@ -1468,7 +1494,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 *)
@@ -1476,18 +1502,20 @@ 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
-            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 None 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/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/Main.ml b/compiler/Main.ml
index 835b9088..0b8ec439 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -120,6 +120,9 @@ let () =
         " Generate a default lakefile.lean (Lean only)" );
       ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
       ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error");
+      ( "-split-fwd-back",
+        Arg.Clear return_back_funs,
+        " Split the forward and backward functions." );
     ]
   in
 
@@ -193,9 +196,6 @@ let () =
   let _ =
     match !backend with
     | FStar ->
-        (* Some patterns are not supported *)
-        decompose_monadic_let_bindings := false;
-        decompose_nested_let_patterns := false;
         (* F* can disambiguate the field names *)
         record_fields_short_names := true
     | Coq ->
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/PrintPure.ml b/compiler/PrintPure.ml
index 2fe5843e..66475d02 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -103,10 +103,13 @@ let adt_field_names (env : fmt_env) =
   Print.Types.adt_field_names (fmt_env_to_llbc_fmt_env env)
 
 let option_to_string = Print.option_to_string
-let type_var_to_string = Print.Types.type_var_to_string
-let const_generic_var_to_string = Print.Types.const_generic_var_to_string
-let integer_type_to_string = Print.Values.integer_type_to_string
 let literal_type_to_string = Print.Values.literal_type_to_string
+let type_var_to_string (v : type_var) = "(" ^ v.name ^ ": Type)"
+
+let const_generic_var_to_string (v : const_generic_var) =
+  "(" ^ v.name ^ " : " ^ literal_type_to_string v.ty ^ ")"
+
+let integer_type_to_string = Print.Values.integer_type_to_string
 let scalar_value_to_string = Print.Values.scalar_value_to_string
 let literal_to_string = Print.Values.literal_to_string
 
@@ -203,13 +206,12 @@ and trait_instance_id_to_string (env : fmt_env) (inside : bool)
   | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
 
 let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =
-  let clause_id = trait_clause_id_to_string env clause.clause_id in
   let trait_id = trait_decl_id_to_string env clause.trait_id in
   let generics = generic_args_to_strings env true clause.generics in
   let generics =
     if generics = [] then "" else " " ^ String.concat " " generics
   in
-  "[" ^ clause_id ^ "]: " ^ trait_id ^ generics
+  trait_id ^ generics
 
 let generic_params_to_strings (env : fmt_env) (generics : generic_params) :
     string list =
@@ -543,9 +545,9 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string)
       let app, args = destruct_apps e in
       (* Convert to string *)
       app_to_string env inside indent indent_incr app args
-  | Abs _ ->
-      let xl, e = destruct_abs_list e in
-      let e = abs_to_string env indent indent_incr xl e in
+  | Lambda _ ->
+      let xl, e = destruct_lambdas e in
+      let e = lambda_to_string env indent indent_incr xl e in
       if inside then "(" ^ e ^ ")" else e
   | Qualif _ ->
       (* Qualifier without arguments *)
@@ -609,35 +611,36 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string)
    * expression *)
   let app, generics =
     match app.e with
-    | Qualif qualif ->
+    | Qualif qualif -> (
         (* Qualifier case *)
-        (* Convert the qualifier identifier *)
-        let qualif_s =
-          match qualif.id with
-          | FunOrOp fun_id -> fun_or_op_id_to_string env fun_id
-          | Global global_id -> global_decl_id_to_string env global_id
-          | AdtCons adt_cons_id ->
-              let variant_s =
-                adt_variant_to_string env adt_cons_id.adt_id
-                  adt_cons_id.variant_id
-              in
-              ConstStrings.constructor_prefix ^ variant_s
-          | Proj { adt_id; field_id } ->
-              let adt_s = adt_variant_to_string env adt_id None in
-              let field_s = adt_field_to_string env adt_id field_id in
-              (* Adopting an F*-like syntax *)
-              ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s
-          | TraitConst (trait_ref, generics, const_name) ->
-              let trait_ref = trait_ref_to_string env true trait_ref in
-              let generics_s = generic_args_to_string env generics in
+        match qualif.id with
+        | FunOrOp fun_id ->
+            let generics = generic_args_to_strings env true qualif.generics in
+            let qualif_s = fun_or_op_id_to_string env fun_id in
+            (qualif_s, generics)
+        | Global global_id ->
+            let generics = generic_args_to_strings env true qualif.generics in
+            (global_decl_id_to_string env global_id, generics)
+        | AdtCons adt_cons_id ->
+            let variant_s =
+              adt_variant_to_string env adt_cons_id.adt_id
+                adt_cons_id.variant_id
+            in
+            (ConstStrings.constructor_prefix ^ variant_s, [])
+        | Proj { adt_id; field_id } ->
+            let adt_s = adt_variant_to_string env adt_id None in
+            let field_s = adt_field_to_string env adt_id field_id in
+            (* Adopting an F*-like syntax *)
+            (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, [])
+        | TraitConst (trait_ref, generics, const_name) ->
+            let trait_ref = trait_ref_to_string env true trait_ref in
+            let generics_s = generic_args_to_string env generics in
+            let qualif =
               if generics <> empty_generic_args then
                 "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name
               else trait_ref ^ "." ^ const_name
-        in
-        (* Convert the type instantiation *)
-        let generics = generic_args_to_strings env true qualif.generics in
-        (* *)
-        (qualif_s, generics)
+            in
+            (qualif, []))
     | _ ->
         (* "Regular" expression case *)
         let inside = args <> [] || (args = [] && inside) in
@@ -660,7 +663,7 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string)
   (* Add parentheses *)
   if all_args <> [] && inside then "(" ^ e ^ ")" else e
 
-and abs_to_string (env : fmt_env) (indent : string) (indent_incr : string)
+and lambda_to_string (env : fmt_env) (indent : string) (indent_incr : string)
     (xl : typed_pattern list) (e : texpression) : string =
   let xl = List.map (typed_pattern_to_string env) xl in
   let e = texpression_to_string env false indent indent_incr e in
@@ -708,21 +711,14 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string)
     ^ String.concat "; " (List.map (var_to_string env) loop.inputs)
     ^ "]"
   in
-  let back_output_tys =
-    let tys =
-      match loop.back_output_tys with
-      | None -> ""
-      | Some tys -> String.concat "; " (List.map (ty_to_string env false) tys)
-    in
-    "back_output_tys: [" ^ tys ^ "]"
-  in
+  let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in
   let fun_end =
     texpression_to_string env false indent2 indent_incr loop.fun_end
   in
   let loop_body =
     texpression_to_string env false indent2 indent_incr loop.loop_body
   in
-  "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ back_output_tys ^ "\n"
+  "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n"
   ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n"
   ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n"
   ^ indent ^ "}"
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 8d39cc69..a879ba37 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -561,7 +561,7 @@ type fun_id_or_trait_method_ref =
 
 (** A function id for a non-assumed function *)
 type regular_fun_id =
-  fun_id_or_trait_method_ref * LoopId.id option * T.RegionGroupId.id option
+  fun_id_or_trait_method_ref * LoopId.id option * RegionGroupId.id option
 [@@deriving show, ord]
 
 (** A function identifier *)
@@ -684,7 +684,7 @@ type expression =
           field accesses with calls to projectors over fields (when there
           are clashes of field names, some provers like F* get pretty bad...)
        *)
-  | Abs of typed_pattern * texpression  (** Lambda abstraction: [fun x -> e] *)
+  | Lambda of typed_pattern * texpression  (** Lambda abstraction: [λ x => e] *)
   | Qualif of qualif  (** A top-level qualifier *)
   | Let of bool * typed_pattern * texpression * texpression
       (** Let binding.
@@ -754,9 +754,7 @@ and loop = {
   inputs : var list;
   inputs_lvs : typed_pattern list;
       (** The inputs seen as patterns. See {!fun_body}. *)
-  back_output_tys : ty list option;
-      (** The types of the given back values, if we ar esynthesizing a backward
-          function *)
+  output_ty : ty;  (** The output type of the loop *)
   loop_body : texpression;
 }
 
@@ -860,8 +858,8 @@ type fun_effect_info = {
           the set [{ forward function } U { backward functions }].
 
           We need this because of the option {!val:Config.backward_no_state_update}:
-          if it is [true], then in case of a backward function {!stateful} is [false],
-          but we might need to know whether the corresponding forward function
+          if it is [true], then in case of a backward function {!stateful} might be
+          [false], but we might need to know whether the corresponding forward function
           is stateful or not.
        *)
   stateful : bool;  (** [true] if the function is stateful (updates a state) *)
@@ -873,22 +871,108 @@ type fun_effect_info = {
 }
 [@@deriving show]
 
-(** Meta information about a function signature *)
-type fun_sig_info = {
+type inputs_info = {
   has_fuel : bool;
-  (* TODO: add [num_fwd_inputs_no_fuel_no_state] *)
-  num_fwd_inputs_with_fuel_no_state : int;
-      (** The number of input types for forward computation, with the fuel (if used)
+  num_inputs_no_fuel_no_state : int;
+      (** The number of input types ignoring the fuel (if used)
+          and ignoring the state (if used) *)
+  num_inputs_with_fuel_no_state : int;
+      (** The number of input types, with the fuel (if used)
           and ignoring the state (if used) *)
-  num_fwd_inputs_with_fuel_with_state : int;
-      (** The number of input types for forward computation, with fuel and state (if used) *)
-  num_back_inputs_no_state : int option;
-      (** The number of additional inputs for the backward computation (if pertinent),
-          ignoring the state (if there is one) *)
-  num_back_inputs_with_state : int option;
-      (** The number of additional inputs for the backward computation (if pertinent),
-          with the state (if there is one) *)
+  num_inputs_with_fuel_with_state : int;
+      (** The number of input types, with fuel and state (if used) *)
+}
+[@@deriving show]
+
+(** Meta information about a function signature *)
+type fun_sig_info = {
+  fwd_info : inputs_info;
+      (** Information about the inputs of the forward function *)
   effect_info : fun_effect_info;
+  ignore_output : bool;
+      (** In case we merge the forward/backward functions: should we ignore
+          the output (happens for forward functions if the output type is
+          [unit] and there are non-filtered backward functions)?
+       *)
+}
+[@@deriving show]
+
+type back_sg_info = {
+  inputs : (string option * ty) list;
+      (** The additional inputs of the backward function *)
+  inputs_no_state : (string option * ty) list;
+  outputs : ty list;
+      (** The "decomposed" list of outputs.
+
+          The list contains all the types of
+          all the given back values (there is at most one type per forward
+          input argument).
+
+          Ex.:
+          {[
+            fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
+          ]}
+          Decomposed outputs:
+          - forward function:  [[T]]
+          - backward function: [[T; T]] (for "x" and "y")
+
+          Non-decomposed ouputs (if the function can fail, but is not stateful):
+          - [result T]
+          - [[result (T * T)]]
+       *)
+  output_names : string option list;
+      (** The optional names for the backward outputs.
+          We derive those from the names of the inputs of the original LLBC
+          function. *)
+  effect_info : fun_effect_info;
+  filter : bool;  (** Should we filter this backward function? *)
+}
+[@@deriving show]
+
+(** A *decomposed* function signature. *)
+type decomposed_fun_sig = {
+  generics : generic_params;
+      (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
+  llbc_generics : Types.generic_params;
+      (** We use the LLBC generics to generate "pretty" names, for instance
+          for the variables we introduce for the trait clauses: we derive
+          those names from the types, and when doing so it is more meaningful
+          to derive them from the original LLBC types from before the
+          simplification of types like boxes and references. *)
+  preds : predicates;
+  fwd_inputs : ty list;
+      (** The types of the inputs of the forward function.
+
+          Note that those input types take include the [fuel] parameter,
+          if the function uses fuel for termination, and the [state] parameter,
+          if the function is stateful.
+
+          For instance, if we have the following Rust function:
+          {[
+            fn f(x : int);
+          ]}
+
+          If we translate it to a stateful function which uses fuel we get:
+          {[
+            val f : nat -> int -> state -> result (state * unit);
+          ]}
+
+          In particular, the list of input types is: [[nat; int; state]].
+       *)
+  fwd_output : ty;
+      (** The "pure" output type of the forward function.
+
+          Note that this type doesn't contain the "effect" of the function (i.e.,
+          we haven't added the [state] if it is a stateful function and haven't
+          wrapped the type in a [result]). Also, this output type is only about
+          the forward function (it doesn't contain the type of the closures we
+          return for the backward functions, in case we merge the forward and
+          backward functions).
+       *)
+  back_sg : back_sg_info RegionGroupId.Map.t;
+      (** Information about the backward functions *)
+  fwd_info : fun_sig_info;
+      (** Additional information about the forward function *)
 }
 [@@deriving show]
 
@@ -906,15 +990,15 @@ type fun_sig_info = {
       [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
        result (state & (back_out0 & ... & back_outp))] (* state-error *)
 
-       Note that a stateful backward function may take two states as inputs: the
-       state received by the associated forward function, and the state at which
-       the backward is called. This leads to code of the following shape:
+      Note that a stateful backward function may take two states as inputs: the
+      state received by the associated forward function, and the state at which
+      the backward is called. This leads to code of the following shape:
 
-       {[
-         (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
-         ... // the state may be updated
-         (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
-       ]}
+      {[
+        (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
+        ... // the state may be updated
+        (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
+      ]}
 
     The function's type should be given by [mk_arrows sig.inputs sig.output].
     We provide additional meta-information with {!fun_sig.info}:
@@ -962,40 +1046,14 @@ type fun_sig = {
           be a tuple with a [state] if the function is stateful, and will be wrapped
           in a [result] if the function can fail.
        *)
-  doutputs : ty list;
-      (** The "decomposed" list of outputs.
-
-          In case of a forward function, the list has length = 1, for the
-          type of the returned value.
-
-          In case of backward function, the list contains all the types of
-          all the given back values (there is at most one type per forward
-          input argument).
-
-          Ex.:
-          {[
-            fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
-          ]}
-          Decomposed outputs:
-          - forward function:  [[T]]
-          - backward function: [[T; T]] (for "x" and "y")
-
-          Non-decomposed ouputs (if the function can fail, but is not stateful):
-          - [result T]
-          - [[result (T * T)]]
-       *)
-  info : fun_sig_info;  (** Additional information *)
+  fwd_info : fun_sig_info;
+      (** Additional information about the forward function. *)
+  back_effect_info : fun_effect_info RegionGroupId.Map.t;
 }
 [@@deriving show]
 
 (** An instantiated function signature. See {!fun_sig} *)
-type inst_fun_sig = {
-  inputs : ty list;
-  output : ty;
-  doutputs : ty list;
-  info : fun_sig_info;
-}
-[@@deriving show]
+type inst_fun_sig = { inputs : ty list; output : ty } [@@deriving show]
 
 type fun_body = {
   inputs : var list;
@@ -1020,7 +1078,7 @@ type fun_decl = {
        *)
   loop_id : LoopId.id option;
       (** [Some] if this definition was generated for a loop *)
-  back_id : T.RegionGroupId.id option;
+  back_id : RegionGroupId.id option;
   llbc_name : llbc_name;  (** The original LLBC name. *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 959ec1c8..ec64df21 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -11,6 +11,10 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let fmt = trans_ctx_to_pure_fmt_env ctx in
   PrintPure.fun_decl_to_string fmt def
 
+let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_sig_to_string fmt sg
+
 (** Small utility.
 
     We sometimes have to insert new fresh variables in a function body, in which
@@ -385,17 +389,17 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
           let ctx, arg = update_texpression arg ctx in
           let e = App (app, arg) in
           (ctx, e)
-      | Abs (x, e) -> update_abs x e ctx
       | Qualif _ -> (* nothing to do *) (ctx, e.e)
       | Let (monadic, lb, re, e) -> update_let monadic lb re e ctx
       | Switch (scrut, body) -> update_switch_body scrut body ctx
       | Loop loop -> update_loop loop ctx
       | StructUpdate supd -> update_struct_update supd ctx
+      | Lambda (lb, e) -> update_lambda lb e ctx
       | Meta (meta, e) -> update_emeta meta e ctx
     in
     (ctx, { e; ty })
   (* *)
-  and update_abs (x : typed_pattern) (e : texpression) (ctx : pn_ctx) :
+  and update_lambda (x : typed_pattern) (e : texpression) (ctx : pn_ctx) :
       pn_ctx * expression =
     (* We first add the left-constraint *)
     let ctx = add_left_constraint x ctx in
@@ -404,7 +408,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     (* Update the abstracted value *)
     let x = update_typed_pattern ctx x in
     (* Put together *)
-    (ctx, Abs (x, e))
+    (ctx, Lambda (x, e))
   (* *)
   and update_let (monadic : bool) (lv : typed_pattern) (re : texpression)
       (e : texpression) (ctx : pn_ctx) : pn_ctx * expression =
@@ -455,7 +459,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       input_state;
       inputs;
       inputs_lvs;
-      back_output_tys;
+      output_ty;
       loop_body;
     } =
       loop
@@ -474,7 +478,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         input_state;
         inputs;
         inputs_lvs;
-        back_output_tys;
+        output_ty;
         loop_body;
       }
     in
@@ -641,6 +645,135 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
       let body = { body with body = obj#visit_texpression () body.body } in
       { def with body = Some body }
 
+(** Simplify the let-bindings by performing the following rewritings:
+
+    Move inner let-bindings outside. This is especially useful to simplify
+    the backward expressions, when we merge the forward/backward functions.
+    Note that the rule is also applied with monadic let-bindings.
+    {[
+      let x :=
+        let y := ... in
+        e
+
+        ~~>
+
+      let y := ... in
+      let x := e
+    ]}
+
+    Simplify panics and returns:
+    {[
+      let x ← fail
+      ...
+        ~~>
+      fail
+
+      let x ← return y
+      ...
+        ~~>
+      let x := y
+      ...
+    ]}
+
+    Simplify tuples:
+    {[
+      let (y0, y1) := (x0, x1) in
+      ...
+        ~~>
+      let y0 = x0 in
+      let y1 = x1 in
+      ...
+    ]}
+
+    Simplify arrows:
+    {[
+      let f := fun x => g x in
+      ...
+        ~~>
+      let f := g in
+      ...
+    ]}
+ *)
+let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
+  let obj =
+    object (self)
+      inherit [_] map_expression as super
+
+      method! visit_Let env monadic lv rv next =
+        match rv.e with
+        | Let (rmonadic, rlv, rrv, rnext) ->
+            (* Case 1: move the inner let outside then re-visit *)
+            let rnext1 = Let (monadic, lv, rnext, next) in
+            let rnext1 = { ty = next.ty; e = rnext1 } in
+            self#visit_Let env rmonadic rlv rrv rnext1
+        | App
+            ( {
+                e =
+                  Qualif
+                    {
+                      id =
+                        AdtCons
+                          {
+                            adt_id = TAssumed TResult;
+                            variant_id = Some variant_id;
+                          };
+                      generics = _;
+                    };
+                ty = _;
+              },
+              x ) ->
+            (* return/fail case *)
+            if variant_id = result_return_id then
+              (* Return case - note that the simplification we just perform
+                 might have unlocked the tuple simplification below *)
+              self#visit_Let env false lv x next
+            else if variant_id = result_fail_id then
+              (* Fail case *)
+              self#visit_expression env rv.e
+            else raise (Failure "Unexpected")
+        | App _ ->
+            (* This might be the tuple case *)
+            if not monadic then
+              match
+                (opt_dest_struct_pattern lv, opt_dest_tuple_texpression rv)
+              with
+              | Some pats, Some vals ->
+                  (* Tuple case *)
+                  let pat_vals = List.combine pats vals in
+                  let e =
+                    List.fold_right
+                      (fun (pat, v) next -> mk_let false pat v next)
+                      pat_vals next
+                  in
+                  super#visit_expression env e.e
+              | _ -> super#visit_Let env monadic lv rv next
+            else super#visit_Let env monadic lv rv next
+        | Lambda _ ->
+            if not monadic then
+              (* Arrow case *)
+              let pats, e = destruct_lambdas rv in
+              let g, args = destruct_apps e in
+              if List.length pats = List.length args then
+                (* Check if the arguments are exactly the lambdas *)
+                let check_pat_arg ((pat, arg) : typed_pattern * texpression) =
+                  match (pat.value, arg.e) with
+                  | PatVar (v, _), Var vid -> v.id = vid
+                  | _ -> false
+                in
+                if List.for_all check_pat_arg (List.combine pats args) then
+                  self#visit_Let env monadic lv g next
+                else super#visit_Let env monadic lv rv next
+              else super#visit_Let env monadic lv rv next
+            else super#visit_Let env monadic lv rv next
+        | _ -> super#visit_Let env monadic lv rv next
+    end
+  in
+  match def.body with
+  | None -> def
+  | Some body ->
+      let body = { body with body = obj#visit_texpression () body.body } in
+      { def with body = Some body }
+
 (** Inline the useless variable (re-)assignments:
 
     A lot of intermediate variable assignments are introduced through the
@@ -667,8 +800,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
     leave the let-bindings where they are, and eliminated them in a subsequent
     pass (if they are useless).
  *)
-let inline_useless_var_reassignments (ctx : trans_ctx) (inline_named : bool)
-    (inline_pure : bool) (def : fun_decl) : fun_decl =
+let inline_useless_var_reassignments (ctx : trans_ctx) ~(inline_named : bool)
+    ~(inline_const : bool) ~(inline_pure : bool) (def : fun_decl) : fun_decl =
   let obj =
     object (self)
       inherit [_] map_expression as super
@@ -693,15 +826,31 @@ let inline_useless_var_reassignments (ctx : trans_ctx) (inline_named : bool)
               | _ -> false
             in
             (* And either:
-             * 2.1 the right-expression is a variable, a global or a const generic var *)
+               2.1 the right-expression is a variable, a global or a const generic var *)
             let var_or_global = is_var re || is_cvar re || is_global re in
             (* Or:
-             * 2.2 the right-expression is a constant value, an ADT value,
-             *     a projection or a primitive function call *and* the flag
-             *     [inline_pure] is set *)
+               2.2 the right-expression is a constant-value and we inline constant values,
+                   *or* it is a qualif with no arguments (we consider this as a const) *)
+            let const_re =
+              inline_const
+              &&
+              let is_const_adt =
+                let app, args = destruct_apps re in
+                if args = [] then
+                  match app.e with
+                  | Qualif _ -> true
+                  | StructUpdate upd -> upd.updates = []
+                  | _ -> false
+                else false
+              in
+              is_const re || is_const_adt
+            in
+            (* Or:
+               2.3 the right-expression is an ADT value, a projection or a
+                   primitive function call *and* the flag [inline_pure] is set *)
             let pure_re =
-              is_const re
-              ||
+              inline_pure
+              &&
               let app, _ = destruct_apps re in
               match app.e with
               | Qualif qualif -> (
@@ -716,7 +865,7 @@ let inline_useless_var_reassignments (ctx : trans_ctx) (inline_named : bool)
               | _ -> false
             in
             let filter =
-              filter_left && (var_or_global || (inline_pure && pure_re))
+              filter_left && (var_or_global || const_re || pure_re)
             in
 
             (* Update the rhs (we may perform substitutions inside, and it is
@@ -776,9 +925,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
@@ -890,12 +1041,12 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                 let call_is_child = check_call func1 generics1 args1 in
                 if call_is_child then fun () -> true
                 else fun () -> self#visit_texpression env e ())
+        | Lambda (_, e) -> self#visit_texpression env e
         | App _ -> (
             fun () ->
               match opt_destruct_function_call e with
               | Some (func1, tys1, args1) -> check_call func1 tys1 args1
               | None -> false)
-        | Abs (_, e) -> self#visit_texpression env e
         | Qualif _ ->
             (* Note that this case includes functions without arguments *)
             fun () -> false
@@ -973,10 +1124,23 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
       method! visit_expression env e =
         match e with
         | Var _ | CVar _ | Const _ | App _ | Qualif _
-        | Switch (_, _)
         | Meta (_, _)
-        | StructUpdate _ | Abs _ ->
+        | StructUpdate _ | Lambda _ ->
             super#visit_expression env e
+        | Switch (scrut, switch) -> (
+            match switch with
+            | If (_, _) -> super#visit_expression env e
+            | Match branches ->
+                (* Simplify the branches *)
+                let simplify_branch (br : match_branch) =
+                  (* Compute the set of values used inside the branch *)
+                  let branch, used = self#visit_texpression env br.branch in
+                  (* Simplify the pattern *)
+                  let pat, _ = filter_typed_pattern (used ()) br.pat in
+                  { pat; branch }
+                in
+                super#visit_expression env
+                  (Switch (scrut, Match (List.map simplify_branch branches))))
         | Let (monadic, lv, re, e) ->
             (* Compute the set of values used in the next expression *)
             let e, used = self#visit_texpression env e in
@@ -1008,17 +1172,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 ()
@@ -1297,7 +1465,8 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option =
     those function bodies into independent definitions while removing
     occurrences of the {!Pure.Loop} node.
  *)
-let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
+let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
+    fun_decl * fun_decl list =
   match def.body with
   | None -> (def, [])
   | Some body ->
@@ -1323,77 +1492,55 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
 
           method! visit_Loop env loop =
             let fun_sig = def.signature in
-            let fun_sig_info = fun_sig.info in
-            let fun_effect_info = fun_sig_info.effect_info in
+            let fwd_info = fun_sig.fwd_info in
+            let fwd_effect_info = fwd_info.effect_info in
+            let ignore_output = fwd_info.ignore_output in
 
             (* Generate the loop definition *)
-            let loop_effect_info =
-              {
-                stateful_group = fun_effect_info.stateful_group;
-                stateful = fun_effect_info.stateful;
-                can_fail = fun_effect_info.can_fail;
-                can_diverge = fun_effect_info.can_diverge;
-                is_rec = fun_effect_info.is_rec;
-              }
-            in
+            let loop_fwd_effect_info = fwd_effect_info in
 
-            let loop_sig_info =
+            let loop_fwd_sig_info : fun_sig_info =
               let fuel = if !Config.use_fuel then 1 else 0 in
               let num_inputs = List.length loop.inputs in
-              let num_fwd_inputs_with_fuel_no_state = fuel + num_inputs in
-              let fwd_state =
-                fun_sig_info.num_fwd_inputs_with_fuel_with_state
-                - fun_sig_info.num_fwd_inputs_with_fuel_no_state
-              in
-              let num_fwd_inputs_with_fuel_with_state =
-                num_fwd_inputs_with_fuel_no_state + fwd_state
+              let fwd_info : inputs_info =
+                let info = fwd_info.fwd_info in
+                let fwd_state =
+                  info.num_inputs_with_fuel_with_state
+                  - info.num_inputs_with_fuel_no_state
+                in
+                {
+                  has_fuel = !Config.use_fuel;
+                  num_inputs_no_fuel_no_state = num_inputs;
+                  num_inputs_with_fuel_no_state = num_inputs + fuel;
+                  num_inputs_with_fuel_with_state =
+                    num_inputs + fuel + fwd_state;
+                }
               in
-              {
-                has_fuel = !Config.use_fuel;
-                num_fwd_inputs_with_fuel_no_state;
-                num_fwd_inputs_with_fuel_with_state;
-                num_back_inputs_no_state = fun_sig_info.num_back_inputs_no_state;
-                num_back_inputs_with_state =
-                  fun_sig_info.num_back_inputs_with_state;
-                effect_info = loop_effect_info;
-              }
+
+              { fwd_info; effect_info = loop_fwd_effect_info; ignore_output }
             in
+            assert (fun_sig_info_is_wf loop_fwd_sig_info);
 
             let inputs_tys =
               let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
               let fwd_inputs = List.map (fun (v : var) -> v.ty) loop.inputs in
-              let state =
+              let info = fwd_info.fwd_info in
+              let fwd_state =
                 Collections.List.subslice fun_sig.inputs
-                  fun_sig_info.num_fwd_inputs_with_fuel_no_state
-                  fun_sig_info.num_fwd_inputs_with_fuel_with_state
+                  info.num_inputs_with_fuel_no_state
+                  info.num_inputs_with_fuel_with_state
               in
-              let _, back_inputs =
-                Collections.List.split_at fun_sig.inputs
-                  fun_sig_info.num_fwd_inputs_with_fuel_with_state
+              let back_inputs =
+                if !Config.return_back_funs then []
+                else
+                  snd
+                    (Collections.List.split_at fun_sig.inputs
+                       info.num_inputs_with_fuel_with_state)
               in
-              List.concat [ fuel; fwd_inputs; state; back_inputs ]
+              List.concat [ fuel; fwd_inputs; fwd_state; back_inputs ]
             in
 
-            let output, doutputs =
-              match loop.back_output_tys with
-              | None ->
-                  (* Forward function: the return type is the same as the
-                     parent function *)
-                  (fun_sig.output, fun_sig.doutputs)
-              | Some doutputs ->
-                  (* Backward function: custom return type *)
-                  let output = mk_simpl_tuple_ty doutputs in
-                  let output =
-                    if loop_effect_info.stateful then
-                      mk_simpl_tuple_ty [ mk_state_ty; output ]
-                    else output
-                  in
-                  let output =
-                    if loop_effect_info.can_fail then mk_result_ty output
-                    else output
-                  in
-                  (output, doutputs)
-            in
+            let output = loop.output_ty in
 
             let loop_sig =
               {
@@ -1402,8 +1549,8 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
                 preds = fun_sig.preds;
                 inputs = inputs_tys;
                 output;
-                doutputs;
-                info = loop_sig_info;
+                fwd_info = loop_fwd_sig_info;
+                back_effect_info = fun_sig.back_effect_info;
               }
             in
 
@@ -1420,7 +1567,8 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
               (* Introduce the forward input state *)
               let fwd_state_var, fwd_state_lvs =
                 assert (
-                  loop_effect_info.stateful = Option.is_some loop.input_state);
+                  loop_fwd_effect_info.stateful
+                  = Option.is_some loop.input_state);
                 match loop.input_state with
                 | None -> ([], [])
                 | Some input_state ->
@@ -1429,15 +1577,16 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
                     ([ state_var ], [ state_lvs ])
               in
 
-              (* Introduce the additional backward inputs *)
+              (* Introduce the additional backward inputs, if necessary *)
               let fun_body = Option.get def.body in
+              let info = fwd_info.fwd_info in
               let _, back_inputs =
                 Collections.List.split_at fun_body.inputs
-                  fun_sig_info.num_fwd_inputs_with_fuel_with_state
+                  info.num_inputs_with_fuel_with_state
               in
               let _, back_inputs_lvs =
                 Collections.List.split_at fun_body.inputs_lvs
-                  fun_sig_info.num_fwd_inputs_with_fuel_with_state
+                  info.num_inputs_with_fuel_with_state
               in
 
               let inputs =
@@ -1508,9 +1657,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 <> []
@@ -1816,11 +1968,15 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   log#ldebug
     (lazy ("intro_struct_updates:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
+  (* Simplify the let-bindings *)
+  let def = simplify_let_bindings ctx def in
+  log#ldebug
+    (lazy ("simplify_let_bindings:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+
   (* Inline the useless variable reassignments *)
-  let inline_named_vars = true in
-  let inline_pure = true in
   let def =
-    inline_useless_var_reassignments ctx inline_named_vars inline_pure def
+    inline_useless_var_reassignments ctx ~inline_named:true ~inline_const:true
+      ~inline_pure:true def
   in
   log#ldebug
     (lazy
@@ -1867,6 +2023,23 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   log#ldebug
     (lazy ("simplify_aggregates:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
+  (* Simplify the let-bindings - some simplifications may have been unlocked by
+     the pass above (for instance, the lambda simplification) *)
+  let def = simplify_let_bindings ctx def in
+  log#ldebug
+    (lazy
+      ("simplify_let_bindings (pass 2):\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+
+  (* Inline the useless vars again *)
+  let def =
+    inline_useless_var_reassignments ctx ~inline_named:true ~inline_const:true
+      ~inline_pure:false def
+  in
+  log#ldebug
+    (lazy
+      ("inline_useless_var_assignments (pass 2):\n\n"
+     ^ fun_decl_to_string ctx def ^ "\n"));
+
   (* Decompose the monadic let-bindings - used by Coq *)
   let def =
     if !Config.decompose_monadic_let_bindings then (
@@ -1917,67 +2090,6 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   (* We are done *)
   def
 
-(** Apply all the micro-passes to a function.
-
-    As loops are initially directly integrated into the function definition,
-    {!apply_passes_to_def} extracts those loops definitions from the body;
-    it thus returns the pair: (function def, loop defs). See {!decompose_loops}
-    for more information.
-
-    Will return [None] if the function is a backward function with no outputs.
-
-    [ctx]: used only for printing.
- *)
-let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
-    fun_and_loops option =
-  (* Debug *)
-  log#ldebug
-    (lazy
-      ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " ("
-      ^ Print.option_to_string T.RegionGroupId.to_string def.back_id
-      ^ ")"));
-
-  log#ldebug (lazy ("original decl:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
-
-  (* First, find names for the variables which are unnamed *)
-  let def = compute_pretty_names def in
-  log#ldebug
-    (lazy ("compute_pretty_name:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
-
-  (* TODO: we might want to leverage more the assignment meta-data, for
-   * aggregates for instance. *)
-
-  (* TODO: reorder the branches of the matches/switches *)
-
-  (* The meta-information is now useless: remove it.
-   * Rk.: some passes below use the fact that we removed the meta-data
-   * (otherwise we would have to "unmeta" expressions before matching) *)
-  let def = remove_meta def in
-  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 *)
-  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
-
-  match opt_def with
-  | None ->
-      log#ldebug (lazy ("filtered (backward with no outputs): " ^ name ^ "\n"));
-      None
-  | Some def ->
-      log#ldebug
-        (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n"));
-
-      (* Extract the loop definitions by removing the {!Loop} node *)
-      let def, loops = decompose_loops def in
-
-      (* Apply the remaining passes *)
-      let f = apply_end_passes_to_def ctx def in
-      let loops = List.map (apply_end_passes_to_def ctx) loops in
-      Some { f; loops }
-
 (** Small utility for {!filter_loop_inputs} *)
 let filter_prefix (keep : bool list) (ls : 'a list) : 'a list =
   let ls0, ls1 = Collections.List.split_at ls (List.length keep) in
@@ -2058,7 +2170,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
     (* We only look at the forward inputs, without the state *)
     let inputs_prefix, _ =
       Collections.List.split_at body.inputs
-        decl.signature.info.num_fwd_inputs_with_fuel_no_state
+        decl.signature.fwd_info.fwd_info.num_inputs_with_fuel_no_state
     in
     let used = ref (List.map (fun v -> (var_get_id v, false)) inputs_prefix) in
     let inputs_prefix_length = List.length inputs_prefix in
@@ -2077,8 +2189,9 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
     in
 
     (* Set the fuel as used *)
-    let sg_info = decl.signature.info in
-    if sg_info.has_fuel then set_used (fst (Collections.List.nth inputs 0));
+    let sg_info = decl.signature.fwd_info in
+    if sg_info.fwd_info.has_fuel then
+      set_used (fst (Collections.List.nth inputs 0));
 
     let visitor =
       object (self : 'self)
@@ -2162,37 +2275,54 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
           let num_filtered =
             List.length (List.filter (fun b -> not b) used_info)
           in
-          let { generics; llbc_generics; preds; inputs; output; doutputs; info }
-              =
+          let {
+            generics;
+            llbc_generics;
+            preds;
+            inputs;
+            output;
+            fwd_info;
+            back_effect_info;
+          } =
             decl.signature
           in
+          let { fwd_info; effect_info; ignore_output } = fwd_info in
+
           let {
             has_fuel;
-            num_fwd_inputs_with_fuel_no_state;
-            num_fwd_inputs_with_fuel_with_state;
-            num_back_inputs_no_state;
-            num_back_inputs_with_state;
-            effect_info;
+            num_inputs_no_fuel_no_state;
+            num_inputs_with_fuel_no_state;
+            num_inputs_with_fuel_with_state;
           } =
-            info
+            fwd_info
           in
 
           let inputs = filter_prefix used_info inputs in
 
-          let info =
+          let fwd_info =
             {
               has_fuel;
-              num_fwd_inputs_with_fuel_no_state =
-                num_fwd_inputs_with_fuel_no_state - num_filtered;
-              num_fwd_inputs_with_fuel_with_state =
-                num_fwd_inputs_with_fuel_with_state - num_filtered;
-              num_back_inputs_no_state;
-              num_back_inputs_with_state;
-              effect_info;
+              num_inputs_no_fuel_no_state =
+                num_inputs_no_fuel_no_state - num_filtered;
+              num_inputs_with_fuel_no_state =
+                num_inputs_with_fuel_no_state - num_filtered;
+              num_inputs_with_fuel_with_state =
+                num_inputs_with_fuel_with_state - num_filtered;
             }
           in
+
+          let fwd_info = { fwd_info; effect_info; ignore_output } in
+          assert (fun_sig_info_is_wf fwd_info);
           let signature =
-            { generics; llbc_generics; preds; inputs; output; doutputs; info }
+            {
+              generics;
+              llbc_generics;
+              preds;
+              inputs;
+              output;
+              fwd_info;
+              back_effect_info;
+            }
           in
 
           { decl with signature }
@@ -2283,6 +2413,68 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
   (* Return *)
   transl
 
+(** Apply all the micro-passes to a function.
+
+    As loops are initially directly integrated into the function definition,
+    {!apply_passes_to_def} extracts those loops definitions from the body;
+    it thus returns the pair: (function def, loop defs). See {!decompose_loops}
+    for more information.
+
+    Will return [None] if the function is a backward function with no outputs.
+
+    [ctx]: used only for printing.
+ *)
+let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
+    fun_and_loops option =
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " ("
+      ^ Print.option_to_string T.RegionGroupId.to_string def.back_id
+      ^ ")"));
+
+  log#ldebug (lazy ("original decl:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+
+  (* First, find names for the variables which are unnamed *)
+  let def = compute_pretty_names def in
+  log#ldebug
+    (lazy ("compute_pretty_name:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+
+  (* TODO: we might want to leverage more the assignment meta-data, for
+   * aggregates for instance. *)
+
+  (* TODO: reorder the branches of the matches/switches *)
+
+  (* The meta-information is now useless: remove it.
+   * Rk.: some passes below use the fact that we removed the meta-data
+   * (otherwise we would have to "unmeta" expressions before matching) *)
+  let def = remove_meta def in
+  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 *)
+  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
+
+  match opt_def with
+  | None ->
+      log#ldebug (lazy ("filtered (backward with no outputs): " ^ name ^ "\n"));
+      None
+  | Some def ->
+      log#ldebug
+        (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n"));
+
+      (* Extract the loop definitions by removing the {!Loop} node *)
+      let def, loops = decompose_loops ctx def in
+
+      (* Apply the remaining passes *)
+      let f = apply_end_passes_to_def ctx def in
+      let loops = List.map (apply_end_passes_to_def ctx) loops in
+      Some { f; loops }
+
 (** Apply the micro-passes to a list of forward/backward translations.
 
     This function also extracts the loop definitions from the function body
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index a62a2361..a989fd3b 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -120,7 +120,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       assert (output_ty = e.ty);
       check_texpression ctx app;
       check_texpression ctx arg
-  | Abs (pat, body) ->
+  | Lambda (pat, body) ->
       let pat_ty, body_ty = destruct_arrow e.ty in
       assert (pat.ty = pat_ty);
       assert (body.ty = body_ty);
@@ -188,12 +188,6 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
           List.iter check_branch branches)
   | Loop loop ->
       assert (loop.fun_end.ty = e.ty);
-      (* If we translate forward functions, the type of the loop is the same
-         as the type of the parent expression - in case of backward functions,
-         the loop doesn't necessarily give back the same values as the parent
-         function
-      *)
-      assert (Option.is_some loop.back_output_tys || loop.loop_body.ty = e.ty);
       check_texpression ctx loop.fun_end;
       check_texpression ctx loop.loop_body
   | StructUpdate supd -> (
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 39dcd52d..80bf3c42 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -57,6 +57,23 @@ end
 module FunLoopIdMap = Collections.MakeMap (FunLoopIdOrderedType)
 module FunLoopIdSet = Collections.MakeSet (FunLoopIdOrderedType)
 
+let inputs_info_is_wf (info : inputs_info) : bool =
+  let {
+    has_fuel;
+    num_inputs_no_fuel_no_state;
+    num_inputs_with_fuel_no_state;
+    num_inputs_with_fuel_with_state;
+  } =
+    info
+  in
+  let fuel = if has_fuel then 1 else 0 in
+  num_inputs_no_fuel_no_state >= 0
+  && num_inputs_with_fuel_no_state = num_inputs_no_fuel_no_state + fuel
+  && num_inputs_with_fuel_with_state >= num_inputs_with_fuel_no_state
+
+let fun_sig_info_is_wf (info : fun_sig_info) : bool =
+  inputs_info_is_wf info.fwd_info
+
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
   | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
@@ -187,9 +204,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
   let subst = ty_substitute subst in
   let inputs = List.map subst sg.inputs in
   let output = subst sg.output in
-  let doutputs = List.map subst sg.doutputs in
-  let info = sg.info in
-  { inputs; output; doutputs; info }
+  { inputs; output }
 
 (** We use this to check whether we need to add parentheses around expressions.
     We only look for outer monadic let-bindings.
@@ -200,12 +215,14 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
-  | Var _ | CVar _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ ->
-      false
+  | Var _ | CVar _ | Const _ | App _ | Qualif _ | StructUpdate _ -> false
   | Let (monadic, _, _, next_e) ->
       if monadic then true else let_group_requires_parentheses next_e
   | Switch (_, _) -> false
   | Meta (_, next_e) -> let_group_requires_parentheses next_e
+  | Lambda (_, _) ->
+      (* Being conservative here *)
+      true
   | Loop _ ->
       (* Should have been eliminated *)
       raise (Failure "Unreachable")
@@ -304,14 +321,26 @@ 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
+        (* TODO: we need to normalize the types *)
+        !Config.type_check_pure_code && 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 =
@@ -356,18 +385,6 @@ let opt_destruct_tuple (ty : ty) : ty list option =
       Some generics.types
   | _ -> None
 
-let mk_abs (x : typed_pattern) (e : texpression) : texpression =
-  let ty = TArrow (x.ty, e.ty) in
-  let e = Abs (x, e) in
-  { e; ty }
-
-let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
-  match e.e with
-  | Abs (x, e') ->
-      let xl, e'' = destruct_abs_list e' in
-      (x :: xl, e'')
-  | _ -> ([], e)
-
 let destruct_arrow (ty : ty) : ty * ty =
   match ty with
   | TArrow (ty0, ty1) -> (ty0, ty1)
@@ -431,6 +448,7 @@ let mk_simpl_tuple_ty (tys : ty list) : ty =
 
 let mk_bool_ty : ty = TLiteral TBool
 let mk_unit_ty : ty = TAdt (TTuple, empty_generic_args)
+let ty_is_unit ty : bool = ty = mk_unit_ty
 
 let mk_unit_rvalue : texpression =
   let id = AdtCons { adt_id = TTuple; variant_id = None } in
@@ -698,3 +716,39 @@ let type_decl_from_type_id_is_tuple_struct (ctx : TypesAnalysis.type_infos)
       let info = TypeDeclId.Map.find id ctx in
       info.is_tuple_struct
   | TAssumed _ -> false
+
+let mk_lambda (x : typed_pattern) (e : texpression) : texpression =
+  let ty = TArrow (x.ty, e.ty) in
+  let e = Lambda (x, e) in
+  { e; ty }
+
+let mk_lambda_from_var (var : var) (mp : mplace option) (e : texpression) :
+    texpression =
+  let pat = PatVar (var, mp) in
+  let pat = { value = pat; ty = var.ty } in
+  mk_lambda pat e
+
+let mk_lambdas_from_vars (vars : var list) (mps : mplace option list)
+    (e : texpression) : texpression =
+  let vars = List.combine vars mps in
+  List.fold_right (fun (v, mp) e -> mk_lambda_from_var v mp e) vars e
+
+let rec destruct_lambdas (e : texpression) : typed_pattern list * texpression =
+  match e.e with
+  | Lambda (pat, e) ->
+      let pats, e = destruct_lambdas e in
+      (pat :: pats, e)
+  | _ -> ([], e)
+
+let opt_dest_tuple_texpression (e : texpression) : texpression list option =
+  let app, args = destruct_apps e in
+  match app.e with
+  | Qualif { id = AdtCons { adt_id = TTuple; variant_id = None }; generics = _ }
+    ->
+      Some args
+  | _ -> None
+
+let opt_dest_struct_pattern (pat : typed_pattern) : typed_pattern list option =
+  match pat.value with
+  | PatAdt { variant_id = None; field_values } -> Some field_values
+  | _ -> None
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 53f99b7f..8e8cdec3 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -42,8 +42,16 @@ 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;
+  trait_method_generics : (generic_args * trait_instance_id) option;
+      (** In case the call is to a trait method, we may need an additional type
+          parameter ([Self]) and the self trait clause to instantiate the
+          function signature. *)
   args : typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : symbolic_value;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 84f09280..3a50e495 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,19 +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_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.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
@@ -68,11 +67,21 @@ type call_info = {
 
           Those inputs include the fuel and the state, if pertinent.
        *)
-  backwards : (V.abs * texpression list) T.RegionGroupId.Map.t;
-      (** A map from region group id (i.e., backward function id) to
-          pairs (abstraction, additional arguments received by the backward function)
-       
-          TODO: remove? it is also in the bs_ctx ("abstractions" field)
+  back_funs : texpression option 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
+            ...
+          ]}
+
+          The expression might be [None] in case the backward function
+          has to be filtered (because it does nothing - the backward
+          functions for shared borrows for instance).
        *)
 }
 [@@deriving show]
@@ -114,33 +123,61 @@ type loop_info = {
   generics : generic_args;
   forward_inputs : texpression list option;
       (** The forward inputs are initialized at [None] *)
-  forward_output_no_state_no_result : var option;
+  forward_output_no_state_no_result : texpression 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.
+       *)
+  back_funs : texpression option RegionGroupId.Map.t option;
+      (** Same as {!call_info.back_funs}.
+          Initialized with [None], gets updated to [Some] only if we merge
+          the fwd/back functions.
+       *)
+  fwd_effect_info : fun_effect_info;
+  back_effect_infos : fun_effect_info RegionGroupId.Map.t;
 }
 [@@deriving show]
 
 (** Body synthesis context *)
 type bs_ctx = {
-  type_context : type_context;
-  fun_context : fun_context;
-  global_context : global_context;
-  trait_decls_ctx : trait_decls_context;
-  trait_impls_ctx : trait_impls_context;
+  (* 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;
+  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 : T.RegionGroupId.id option;  (** TODO: rename *)
-  sg : fun_sig;
-      (** The function signature - useful in particular to translate [Panic] *)
-  fwd_sg : fun_sig;  (** The signature of the forward function *)
+  bid : RegionGroupId.id option;
+      (** TODO: rename
+
+        The id of the group region we are currently translating.
+        If we split the forward/backward functions, we set this id at the
+        very beginning of the translation.
+        If we don't split, we set it to `None`, then update it when we enter
+        an expression which is specific to a backward function.
+     *)
+  sg : decomposed_fun_sig;
+      (** Information about the function signature - useful in particular to
+          translate [Panic] *)
   sv_to_var : var V.SymbolicValueId.Map.t;
       (** Whenever we encounter a new symbolic value (introduced because of
           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_var : VarId.id;
-      (** The additional input state variable received by a stateful backward function.
+  back_state_vars : VarId.id RegionGroupId.Map.t;
+      (** The additional input state variable received by a stateful backward
+          function, **in case we are splitting the forward/backward functions**.
+
           When generating stateful functions, we generate code of the following
           form:
 
@@ -153,7 +190,9 @@ type bs_ctx = {
           When translating a backward function, we need at some point to update
           [state_var] with [back_state_var], to account for the fact that the
           state may have been updated by the caller between the call to the
-          forward function and the call to the backward function.
+          forward function and the call to the backward function. We also need
+          to make sure we use the same variable in all the branches (because
+          this variable is quantified at the definition level).
        *)
   fuel0 : VarId.id;
       (** The original fuel taken as input by the function (if we use fuel) *)
@@ -163,28 +202,50 @@ type bs_ctx = {
       (** The input parameters for the forward function corresponding to the
           translated Rust inputs (no fuel, no state).
        *)
-  backward_inputs : var list T.RegionGroupId.Map.t;
+  backward_inputs_no_state : var list RegionGroupId.Map.t;
       (** The additional input parameters for the backward functions coming
           from the borrows consumed upon ending the lifetime (as a consequence
           those don't include the backward state, if there is one).
-       *)
-  backward_outputs : var list T.RegionGroupId.Map.t;
-      (** The variables that the backward functions will output, corresponding
-          to the borrows they give back (don't include the backward state)
-       *)
-  loop_backward_outputs : var list T.RegionGroupId.Map.t option;
-      (** Same as {!backward_outputs}, but for loops (if we entered a loop).
 
-          [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).
+          If we split the forward/backward functions: we initialize this map
+          when initializing the bs_ctx, because those variables are quantified
+          at the definition level. Otherwise, we initialize it upon diving
+          into the expressions which are specific to the backward functions.
+       *)
+  backward_inputs_with_state : var list RegionGroupId.Map.t;
+      (** All the additional input parameters for the backward functions.
 
-          TODO: move to {!loop_info}
+          Same remarks as for {!backward_inputs_no_state}.
+       *)
+  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:
+          - 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
+            back to the caller), we introduce:
+            {[
+                let v_i = consumed_i in
+                ...
+            ]}
+            where the [v_i] are fresh, and are stored in the [backward_output].
+          - Then, upon reaching the [Return] node, we introduce:
+            {[
+                return (v_i)
+            ]}
+
+          The option is [None] before we detect the ended input abstraction,
+          and [Some] afterwards.
        *)
   calls : call_info V.FunCallId.Map.t;
       (** The function calls we encountered so far *)
   abstractions : (V.abs * texpression list) V.AbstractionId.Map.t;
-      (** The ended abstractions we encountered so far, with their additional input arguments  *)
+      (** The ended abstractions we encountered so far, with their additional
+          input arguments. We store it here and not in {!call_info} because
+          we need a map from abstraction id to abstraction (and not
+          from call id + region group id to abstraction). *)
   loop_ids_map : LoopId.id V.LoopId.Map.t;  (** Ids to use for the loops *)
   loops : loop_info LoopId.Map.t;
       (** The loops we encountered so far.
@@ -209,9 +270,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 =
@@ -233,9 +294,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
@@ -300,6 +361,17 @@ let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
   PrintPure.typed_pattern_to_string env p
 
+let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) :
+    fun_effect_info =
+  match bid with
+  | None -> ctx.sg.fwd_info.effect_info
+  | Some bid ->
+      let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in
+      back_sg.effect_info
+
+let ctx_get_effect_info (ctx : bs_ctx) : fun_effect_info =
+  ctx_get_effect_info_for_bid ctx ctx.bid
+
 (* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let env = bs_ctx_to_fmt_env ctx in
@@ -308,33 +380,13 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let indent_incr = "  " in
   Print.Values.abs_to_string env verbose indent indent_incr abs
 
-let get_instantiated_fun_sig (fun_id : A.fun_id)
-    (back_id : T.RegionGroupId.id option) (generics : generic_args)
-    (ctx : bs_ctx) : inst_fun_sig =
-  (* Lookup the non-instantiated function signature *)
-  let sg =
-    (RegularFunIdNotLoopMap.find (fun_id, back_id) ctx.fun_context.fun_sigs).sg
-  in
-  (* Create the substitution *)
-  (* There shouldn't be any reference to Self *)
-  let tr_self = UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics sg.generics generics tr_self in
-  (* Apply *)
-  fun_sig_substitute subst sg
-
 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
-
-(* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
-    (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
-  let id = (E.FRegular def_id, back_id) in
-  (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
+  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.) *)
@@ -601,13 +653,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.
@@ -682,17 +734,21 @@ let rec translate_back_ty (type_infos : type_infos)
       None
   | TTraitType (trait_ref, generics, type_name) ->
       assert (generics.regions = []);
-      (* Translate the trait ref and the generics as "forward" generics -
-         we do not want to filter any type *)
-      let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
-      let generics = translate_fwd_generic_args type_infos generics in
-      Some (TTraitType (trait_ref, generics, type_name))
+      assert (
+        AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id);
+      if inside_mut then
+        (* Translate the trait ref and the generics as "forward" generics -
+           we do not want to filter any type *)
+        let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
+        let generics = translate_fwd_generic_args type_infos generics in
+        Some (TTraitType (trait_ref, generics, type_name))
+      else None
   | TArrow _ -> raise (Failure "TODO")
 
 (** 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 =
@@ -705,8 +761,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;
   }
@@ -726,31 +782,36 @@ 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)
 
 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 option 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; backwards = T.RegionGroupId.Map.empty }
-  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
+    that we need to call. This function may be [None] if it has to be ignored
+    (because it does nothing).
+ *)
+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 option =
   (* Insert the abstraction in the call informations *)
   let info = V.FunCallId.Map.find call_id ctx.calls in
-  assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
-  let backwards =
-    T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards
-  in
-  let info = { info with backwards } in
   let calls = V.FunCallId.Map.add call_id info ctx.calls in
   (* Insert the abstraction in the abstractions map *)
   let abstractions = ctx.abstractions in
@@ -758,16 +819,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
+      Some { 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)
@@ -821,7 +897,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
@@ -848,33 +924,53 @@ let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
         is_rec = false;
       }
 
-(** Translate a function signature.
+(** 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 lid with
+  | None -> (
+      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)
+  | Some lid -> (
+      (* This is necessarily for the current function *)
+      match fun_id with
+      | FunId (FRegular fid) -> (
+          assert (fid = ctx.fun_decl.def_id);
+          (* Lookup the loop *)
+          let lid = V.LoopId.Map.find lid ctx.loop_ids_map in
+          let loop_info = LoopId.Map.find lid ctx.loops in
+          match gid with
+          | None -> loop_info.fwd_effect_info
+          | Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos)
+      | _ -> raise (Failure "Unreachable"))
+
+(** Translate a function signature to a decomposed function signature.
 
     Note that the function also takes a list of names for the inputs, and
     computes, for every output for the backward functions, a corresponding
     name (outputs for backward functions come from borrows in the inputs
     of the forward function) which we use as hints to generate pretty names
     in the extracted code.
+
+    We use [bid] ("backward function id") only if we split the forward
+    and the backward functions.
  *)
-let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
-    (sg : A.fun_sig) (input_names : string option list)
-    (bid : T.RegionGroupId.id option) : fun_sig_named_outputs =
+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
-  let gid, parents =
-    match bid with
-    | None -> (None, T.RegionGroupId.Set.empty)
-    | Some bid ->
-        let parents = list_ancestor_region_groups regions_hierarchy bid in
-        (Some bid, parents)
-  in
-  (* Is the function stateful, and can it fail? *)
-  let lid = None in
-  let effect_info = get_fun_effect_info fun_infos (FunId fun_id) lid bid 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
@@ -885,7 +981,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
       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 *)
@@ -902,17 +998,28 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
     { sg with A.inputs; output }
   in
 
-  (* List the inputs for:
-   * - the fuel
-   * - the forward function
-   * - the parent backward functions, in proper order
-   * - the current backward function (if it is a backward function)
-   *)
-  let fuel = mk_fuel_input_ty_as_list effect_info in
-  let fwd_inputs = List.map (translate_fwd_ty type_infos) sg.inputs in
-  (* For the backward functions: for now we don't supported nested borrows,
-   * so just check that there aren't parent regions *)
-  assert (T.RegionGroupId.Set.is_empty parents);
+  (* Is the forward function stateful, and can it fail? *)
+  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 =
+    List.map (translate_fwd_ty type_infos) sg.inputs
+  in
+  (* State input for the forward function *)
+  let fwd_state_ty =
+    (* For the forward state, we check if the *whole group* is stateful.
+       See {!effect_info}. *)
+    if fwd_effect_info.stateful_group then [ mk_state_ty ] else []
+  in
+  let fwd_inputs =
+    List.concat [ fwd_fuel; fwd_inputs_no_fuel_no_state; fwd_state_ty ]
+  in
+  (* Compute the backward output, without the effect information *)
+  let fwd_output = translate_fwd_ty type_infos sg.output in
+
+  (* Compute the type information for the backward function *)
   (* Small helper to translate types for backward functions *)
   let translate_back_ty_for_gid (gid : T.RegionGroupId.id) (ty : T.ty) :
       ty option =
@@ -939,163 +1046,336 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
     let inside_mut = false in
     translate_back_ty type_infos keep_region inside_mut ty
   in
-  (* 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 ]
-  in
-  (* If the function is stateful, the inputs are:
-     - forward:  [fwd_ty0, ..., fwd_tyn, state]
-     - backward:
-       - if {!Config.backward_no_state_update}: [fwd_ty0, ..., fwd_tyn, state, back_ty, state]
-       - otherwise: [fwd_ty0, ..., fwd_tyn, state, back_ty]
-
-       The backward takes the same state as input as the forward function,
-       together with the state at the point where it gets called, if it is
-       stateful.
-
-       See the comments for {!Config.backward_no_state_update}
-  *)
-  let fwd_state_ty =
-    (* For the forward state, we check if the *whole group* is stateful.
-       See {!effect_info}. *)
-    if effect_info.stateful_group then [ mk_state_ty ] else []
+  let translate_back_inputs_for_gid (gid : T.RegionGroupId.id) : ty list =
+    (* For now we don't supported nested borrows, so we check that there
+       aren't parent regions *)
+    let parents = list_ancestor_region_groups regions_hierarchy gid in
+    assert (T.RegionGroupId.Set.is_empty parents);
+    (* 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.
+    *)
+    let inputs =
+      List.filter_map (translate_back_ty_for_gid gid) [ sg.output ]
+    in
+    log#ldebug
+      (lazy
+        (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in
+         let pctx = PrintPure.decls_ctx_to_fmt_env decls_ctx in
+         let output = Print.Types.ty_to_string ctx sg.output in
+         let inputs =
+           Print.list_to_string (PrintPure.ty_to_string pctx false) inputs
+         in
+         "translate_back_inputs_for_gid:" ^ "\n- gid: "
+         ^ RegionGroupId.to_string gid
+         ^ "\n- output: " ^ output ^ "\n- back inputs: " ^ inputs ^ "\n"));
+    inputs
+  in
+  let compute_back_outputs_for_gid (gid : RegionGroupId.id) :
+      string option list * ty list =
+    (* The outputs are the borrows inside the regions of the abstractions
+       and which are present in the input values. For instance, see:
+       {[
+         fn f<'a>(x : &'a mut u32) -> ...;
+       ]}
+       Upon ending the abstraction for 'a, we give back the borrow which
+       was consumed through the [x] parameter.
+    *)
+    let outputs =
+      List.map
+        (fun (name, input_ty) -> (name, translate_back_ty_for_gid gid input_ty))
+        (List.combine input_names sg.inputs)
+    in
+    (* Filter *)
+    let outputs =
+      List.filter (fun (_, opt_ty) -> Option.is_some opt_ty) outputs
+    in
+    let outputs =
+      List.map (fun (name, opt_ty) -> (name, Option.get opt_ty)) outputs
+    in
+    let names, outputs = List.split outputs in
+    log#ldebug
+      (lazy
+        (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in
+         let pctx = PrintPure.decls_ctx_to_fmt_env decls_ctx in
+         let inputs =
+           Print.list_to_string (Print.Types.ty_to_string ctx) sg.inputs
+         in
+         let outputs =
+           Print.list_to_string (PrintPure.ty_to_string pctx false) outputs
+         in
+         "compute_back_outputs_for_gid:" ^ "\n- gid: "
+         ^ RegionGroupId.to_string gid
+         ^ "\n- inputs: " ^ inputs ^ "\n- back outputs: " ^ outputs ^ "\n"));
+    (names, outputs)
+  in
+  let compute_back_info_for_group (rg : T.region_var_group) :
+      RegionGroupId.id * back_sg_info =
+    let gid = rg.id in
+    let back_effect_info =
+      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
+    (* In case we merge the forward/backward functions:
+       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 =
+      if !Config.return_back_funs then
+        let b = inputs_no_state <> [] in
+        {
+          back_effect_info with
+          stateful = back_effect_info.stateful && b;
+          can_fail = back_effect_info.can_fail && b;
+        }
+      else back_effect_info
+    in
+    let state =
+      if back_effect_info.stateful then [ (None, mk_state_ty) ] else []
+    in
+    let inputs = inputs_no_state @ state in
+    let output_names, outputs = compute_back_outputs_for_gid gid in
+    let filter =
+      !Config.simplify_merged_fwd_backs
+      && !Config.return_back_funs && inputs = [] && outputs = []
+    in
+    let info =
+      {
+        inputs;
+        inputs_no_state;
+        outputs;
+        output_names;
+        effect_info = back_effect_info;
+        filter;
+      }
+    in
+    (gid, info)
   in
-  let back_state_ty =
-    (* 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 []
+  let back_sg =
+    RegionGroupId.Map.of_list
+      (List.map compute_back_info_for_group regions_hierarchy)
   in
 
-  (* Concatenate the inputs, in the following order:
-   * - forward inputs
-   * - forward state input
-   * - backward inputs
-   * - backward state input
-   *)
-  let inputs =
-    List.concat [ fuel; fwd_inputs; fwd_state_ty; back_inputs; back_state_ty ]
-  in
-  (* Outputs *)
-  let output_names, doutputs =
-    match gid with
-    | None ->
-        (* This is a forward function: there is one (unnamed) output *)
-        ([ None ], [ translate_fwd_ty type_infos sg.output ])
-    | Some gid ->
-        (* This is a backward function: there might be several outputs.
-           The outputs are the borrows inside the regions of the abstractions
-           and which are present in the input values. For instance, see:
-           {[
-             fn f<'a>(x : &'a mut u32) -> ...;
-           ]}
-           Upon ending the abstraction for 'a, we give back the borrow which
-           was consumed through the [x] parameter.
-        *)
-        let outputs =
-          List.map
-            (fun (name, input_ty) ->
-              (name, translate_back_ty_for_gid gid input_ty))
-            (List.combine input_names sg.inputs)
-        in
-        (* Filter *)
-        let outputs =
-          List.filter (fun (_, opt_ty) -> Option.is_some opt_ty) outputs
-        in
-        let outputs =
-          List.map (fun (name, opt_ty) -> (name, Option.get opt_ty)) outputs
-        in
-        List.split outputs
-  in
-  (* Create the return type *)
-  let output =
-    (* Group the outputs together *)
-    let output = mk_simpl_tuple_ty doutputs in
-    (* Add the output state *)
-    let output =
-      if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ]
-      else output
+  (* The additional information about the forward function *)
+  let fwd_info =
+    (* *)
+    let has_fuel = fwd_fuel <> [] in
+    let num_inputs_no_fuel_no_state = List.length fwd_inputs_no_fuel_no_state in
+    let num_inputs_with_fuel_no_state =
+      (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *)
+      List.length fwd_fuel + num_inputs_no_fuel_no_state
+    in
+    let fwd_info : inputs_info =
+      {
+        has_fuel;
+        num_inputs_no_fuel_no_state;
+        num_inputs_with_fuel_no_state;
+        num_inputs_with_fuel_with_state =
+          (* We use the fact that [fwd_state_ty] has length 1 if there is a state,
+             and 0 otherwise *)
+          num_inputs_with_fuel_no_state + List.length fwd_state_ty;
+      }
+    in
+    let ignore_output =
+      if !Config.return_back_funs && !Config.simplify_merged_fwd_backs then
+        ty_is_unit fwd_output
+        && List.exists
+             (fun (info : back_sg_info) -> not info.filter)
+             (RegionGroupId.Map.values back_sg)
+      else false
     in
-    (* Wrap in a result type *)
-    if effect_info.can_fail then mk_result_ty output else output
+    let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in
+    assert (fun_sig_info_is_wf info);
+    info
   in
+
   (* Generic parameters *)
   let generics = translate_generic_params sg.generics in
+
   (* Return *)
-  let has_fuel = fuel <> [] in
-  let num_fwd_inputs_no_state = List.length fwd_inputs in
-  let num_fwd_inputs_with_fuel_no_state =
-    (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *)
-    List.length fuel + num_fwd_inputs_no_state
-  in
-  let num_back_inputs_no_state =
-    if bid = None then None else Some (List.length back_inputs)
+  let preds = translate_predicates sg.preds in
+  {
+    generics;
+    llbc_generics = sg.generics;
+    preds;
+    fwd_inputs;
+    fwd_output;
+    back_sg;
+    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
-  let info =
-    {
-      has_fuel;
-      num_fwd_inputs_with_fuel_no_state;
-      num_fwd_inputs_with_fuel_with_state =
-        (* We use the fact that [fwd_state_ty] has length 1 if there is a state,
-           and 0 otherwise *)
-        num_fwd_inputs_with_fuel_no_state + List.length fwd_state_ty;
-      num_back_inputs_no_state;
-      num_back_inputs_with_state =
-        (* Length of [back_state_ty]: similar trick as for [fwd_state_ty] *)
-        Option.map
-          (fun n -> n + List.length back_state_ty)
-          num_back_inputs_no_state;
-      effect_info;
-    }
+  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
-  let preds = translate_predicates sg.preds in
   let sg =
-    {
-      generics;
-      llbc_generics = sg.generics;
-      preds;
-      inputs;
-      output;
-      doutputs;
-      info;
-    }
+    translate_fun_sig_to_decomposed decls_ctx fdef.def_id fdef.signature
+      input_names
+  in
+  log#ldebug
+    (lazy
+      ("translate_fun_sig_from_decl_to_decomposed:" ^ "\n- name: "
+     ^ T.show_name fdef.name ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n"));
+  sg
+
+let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty
+    =
+  let output =
+    if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; ty ] else ty
   in
-  { sg; output_names }
+  if effect_info.can_fail then mk_result_ty output else output
 
-let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
+let mk_back_output_ty_from_effect_info (effect_info : fun_effect_info)
+    (inputs : ty list) (ty : ty) : ty =
+  let output =
+    if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; ty ] else ty
+  in
+  if effect_info.can_fail && inputs <> [] then mk_result_ty output else output
+
+(** Compute the arrow types for all the backward functions.
+
+    If a backward function has no inputs/outputs we filter it.
+ *)
+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
+      (* Compute the input/output types *)
+      let inputs = List.map snd back_sg.inputs in
+      let outputs = back_sg.outputs in
+      (* Filter if necessary *)
+      if !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] then
+        None
+      else
+        let output = mk_simpl_tuple_ty outputs in
+        let output =
+          mk_back_output_ty_from_effect_info effect_info inputs output
+        in
+        let ty = mk_arrows inputs output in
+        (* Substitute - TODO: normalize *)
+        let ty =
+          match subst with
+          | None -> ty
+          | Some (generics, tr_self) ->
+              let subst =
+                make_subst_from_generics dsg.generics generics tr_self
+              in
+              ty_substitute subst ty
+        in
+        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 =
+  assert !Config.return_back_funs;
+  (* Compute the arrow types for all the backward functions *)
+  let back_tys = List.filter_map (fun x -> x) (compute_back_tys dsg None) in
+  (* Group the forward output and the types of the backward functions *)
+  let effect_info = dsg.fwd_info.effect_info in
+  let output =
+    (* We might need to ignore the output of the forward function
+       (if it is unit for instance) *)
+    let tys =
+      if dsg.fwd_info.ignore_output then back_tys
+      else dsg.fwd_output :: back_tys
+    in
+    mk_simpl_tuple_ty tys
+  in
+  mk_output_ty_from_effect_info effect_info output
+
+let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig)
+    (gid : RegionGroupId.id option) : fun_sig =
+  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
+  let mk_output_ty = mk_output_ty_from_effect_info in
+  let inputs, output =
+    (* Two cases depending on whether we split the forward/backward functions or not *)
+    if !Config.return_back_funs then (
+      assert (gid = None);
+      let output = compute_output_ty_from_decomposed dsg in
+      let inputs = dsg.fwd_inputs in
+      (inputs, output))
+    else
+      match gid with
+      | None ->
+          let effect_info = dsg.fwd_info.effect_info in
+          let output = mk_output_ty effect_info dsg.fwd_output in
+          (dsg.fwd_inputs, output)
+      | Some gid ->
+          let back_sg = RegionGroupId.Map.find gid dsg.back_sg in
+          let effect_info = back_sg.effect_info in
+          let inputs = dsg.fwd_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
+          (inputs, output)
+  in
+  { generics; llbc_generics; preds; inputs; output; fwd_info; back_effect_info }
+
+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_pat)
+  (ctx, state_var, state_pat)
 
 (** WARNING: do not call this function directly.
     Call [fresh_named_var_for_symbolic_value] instead. *)
 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)
 
@@ -1129,10 +1409,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)
 
@@ -1140,6 +1420,58 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) :
     bs_ctx * var list =
   List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars
 
+let fresh_opt_vars (vars : (string option * ty) option list) (ctx : bs_ctx) :
+    bs_ctx * var option list =
+  List.fold_left_map
+    (fun ctx var ->
+      match var with
+      | None -> (ctx, None)
+      | Some (name, ty) ->
+          let ctx, var = fresh_var name ty ctx in
+          (ctx, Some var))
+    ctx vars
+
+(* Introduce variables for the backward functions *)
+let fresh_back_vars_for_current_fun (ctx : bs_ctx) : bs_ctx * var option list =
+  (* We lookup the LLBC definition in an attempt to derive pretty names
+     for the backward functions. *)
+  let back_var_names =
+    let def_id = ctx.fun_decl.def_id in
+    let sg = ctx.fun_decl.signature in
+    let regions_hierarchy =
+      LlbcAstUtils.FunIdMap.find (FRegular def_id)
+        ctx.fun_ctx.regions_hierarchies
+    in
+    List.map
+      (fun (gid, _) ->
+        let rg = RegionGroupId.nth regions_hierarchy gid in
+        let region_names =
+          List.map
+            (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
+            rg.regions
+        in
+        let name =
+          match region_names with
+          | [] -> "back"
+          | [ Some r ] -> "back" ^ r
+          | _ ->
+              (* Concatenate all the region names *)
+              "back"
+              ^ String.concat "" (List.filter_map (fun x -> x) region_names)
+        in
+        Some name)
+      (RegionGroupId.Map.bindings ctx.sg.back_sg)
+  in
+  let back_vars = List.combine back_var_names (compute_back_tys ctx.sg None) in
+  let back_vars =
+    List.map
+      (fun (name, ty) ->
+        match ty with None -> None | Some ty -> Some (name, ty))
+      back_vars
+  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
@@ -1158,12 +1490,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.
 
@@ -1342,13 +1684,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 *)
@@ -1543,7 +1883,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
@@ -1565,32 +1907,56 @@ and translate_panic (ctx : bs_ctx) : texpression =
    * but it won't be true anymore once we translate individual blocks *)
   (* If we use a state monad, we need to add a lambda for the state variable *)
   (* Note that only forward functions return a state *)
-  let output_ty =
-    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
-      mk_simpl_tuple_ty tys
-    else
-      (* Regular function, or forward function (the forward translation for
-         a loop has the same return type as the parent function)
-      *)
-      mk_simpl_tuple_ty ctx.sg.doutputs
-  in
+  let effect_info = ctx_get_effect_info ctx in
   (* TODO: we should use a [Fail] function *)
-  if ctx.sg.info.effect_info.stateful then
-    (* Create the [Fail] value *)
-    let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
-    let ret_v =
-      mk_result_fail_texpression_with_error_id error_failure_id ret_ty
-    in
-    ret_v
-  else mk_result_fail_texpression_with_error_id error_failure_id output_ty
+  let mk_output output_ty =
+    if effect_info.stateful then
+      (* Create the [Fail] value *)
+      let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+      let ret_v =
+        mk_result_fail_texpression_with_error_id error_failure_id ret_ty
+      in
+      ret_v
+    else mk_result_fail_texpression_with_error_id error_failure_id output_ty
+  in
+  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 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
+    (* Regular function, or forward function (the forward translation for
+       a loop has the same return type as the parent function)
+    *)
+    match ctx.bid with
+    | None ->
+        if !Config.return_back_funs then
+          let back_tys = compute_back_tys ctx.sg None in
+          let back_tys = List.filter_map (fun x -> x) back_tys in
+          let tys =
+            if ctx.sg.fwd_info.ignore_output then back_tys
+            else ctx.sg.fwd_output :: back_tys
+          in
+          let output = mk_simpl_tuple_ty tys in
+          mk_output output
+        else mk_output ctx.sg.fwd_output
+    | Some bid ->
+        let output =
+          mk_simpl_tuple_ty (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs
+        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}.
+
+    Remark: in case we merge the forward/backward functions, we introduce
+    those in [translate_forward_end].
+*)
 and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     (ctx : bs_ctx) : texpression =
   (* There are two cases:
@@ -1599,22 +1965,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
@@ -1622,7 +1986,7 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
    * - error-monad: Return x
    * - state-error: Return (state, x)
    * *)
-  let effect_info = ctx.sg.info.effect_info in
+  let effect_info = ctx_get_effect_info ctx in
   let output =
     if effect_info.stateful then
       let state_rvalue = mk_state_texpression ctx.state_var in
@@ -1647,24 +2011,12 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
   *)
   let output =
     match ctx.bid with
-    | None ->
-        (* Forward *)
-        mk_texpression_from_var
-          (Option.get loop_info.forward_output_no_state_no_result)
-    | Some bid ->
+    | None -> Option.get loop_info.forward_output_no_state_no_result
+    | 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
-        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
@@ -1676,7 +2028,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
    * effect - in particular, one manipulates a state iff the other does
    * the same.
    * *)
-  let effect_info = ctx.sg.info.effect_info in
+  let effect_info = ctx_get_effect_info ctx in
   let output =
     if effect_info.stateful then
       let state_rvalue = mk_state_texpression ctx.state_var in
@@ -1684,13 +2036,15 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     else output
   in
   (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
-  mk_result_return_texpression output
+  mk_emeta (Tag "return_with_loop") (mk_result_return_texpression output)
 
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   log#ldebug
     (lazy
-      ("translate_function_call:\n"
+      ("translate_function_call:\n" ^ "\n- call.call_id:"
+      ^ S.show_call_id call.call_id
+      ^ "\n\n- call.generics:\n"
       ^ ctx_generic_args_to_string ctx call.generics));
   (* Translate the function call *)
   let generics = ctx_translate_fwd_generic_args ctx call.generics in
@@ -1702,10 +2056,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, out_state =
+  let ctx, fun_id, effect_info, args, dest_v =
     match call.call_id with
     | S.Fun (fid, call_id) ->
         (* Regular function call *)
@@ -1713,25 +2066,150 @@ 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_context.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
           if effect_info.stateful then
             let state_var = mk_state_texpression ctx.state_var in
-            let ctx, nstate_var = bs_ctx_fresh_state_var ctx in
+            let ctx, _, nstate_var = bs_ctx_fresh_state_var ctx in
             (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, 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
+            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
+            log#ldebug
+              (lazy ("dsg.generics:\n" ^ show_generic_params dsg.generics));
+            let tr_self, all_generics =
+              match call.trait_method_generics with
+              | None -> (UnknownTrait __FUNCTION__, generics)
+              | Some (all_generics, tr_self) ->
+                  let all_generics =
+                    ctx_translate_fwd_generic_args ctx all_generics
+                  in
+                  let tr_self =
+                    translate_fwd_trait_instance_id ctx.type_ctx.type_infos
+                      tr_self
+                  in
+                  (tr_self, all_generics)
+            in
+            let back_tys =
+              compute_back_tys_with_info dsg (Some (all_generics, tr_self))
+            in
+            (* Introduce variables for the backward functions *)
+            (* 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_opt_vars
+                (List.map
+                   (fun ty ->
+                     match ty with
+                     | None -> None
+                     | 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
+            let back_funs =
+              List.filter_map
+                (fun v ->
+                  match v with
+                  | None -> None
+                  | Some v -> Some (mk_typed_pattern_from_var v None))
+                back_vars
+            in
+            let gids =
+              List.map
+                (fun (g : T.region_var_group) -> g.id)
+                call.regions_hierarchy
+            in
+            let back_vars =
+              List.map (Option.map mk_texpression_from_var) back_vars
+            in
+            let back_funs_map =
+              RegionGroupId.Map.of_list (List.combine gids back_vars)
+            in
+            (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 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, dest)
     | S.Unop E.Not ->
         let effect_info =
           {
@@ -1742,7 +2220,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 ] ->
@@ -1758,7 +2238,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
@@ -1773,7 +2255,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
@@ -1793,15 +2277,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
-    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 =
@@ -1846,45 +2326,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 =
+  let ctx, given_back_variables =
+    let vars =
       if ctx.inside_loop then
         (* We are synthesizing a loop body *)
-        Option.get ctx.loop_backward_outputs
-      else (* Regular function body *)
-        ctx.backward_outputs
+        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
-    T.RegionGroupId.Map.find bid map
+    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 *)
@@ -1933,9 +2406,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_context.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
@@ -1959,14 +2430,16 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   let back_state, ctx, nstate =
     if effect_info.stateful then
       let back_state = mk_state_texpression ctx.state_var in
-      let ctx, nstate = bs_ctx_fresh_state_var ctx in
+      let ctx, _, nstate = bs_ctx_fresh_state_var ctx in
       ([ back_state ], ctx, Some nstate)
     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
@@ -1983,78 +2456,61 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | None -> output
     | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ]
   in
-  (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
-  (if (* TODO: normalize the types *) !Config.type_check_pure_code then
-     match fun_id with
-     | FunId fun_id ->
-         let inst_sg =
-           get_instantiated_fun_sig fun_id (Some rg_id) generics ctx
-         in
-         log#ldebug
-           (lazy
-             ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
-             ^ string_of_int (List.length inputs)
-             ^ "): "
-             ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
-             ^ "\n- inst_sg.inputs ("
-             ^ string_of_int (List.length inst_sg.inputs)
-             ^ "): "
-             ^ String.concat ", "
-                 (List.map (pure_ty_to_string ctx) inst_sg.inputs)));
-         List.iter
-           (fun (x, ty) -> assert ((x : texpression).ty = ty))
-           (List.combine inputs inst_sg.inputs);
-         log#ldebug
-           (lazy
-             ("\n- outputs: "
-             ^ string_of_int (List.length outputs)
-             ^ "\n- expected outputs: "
-             ^ string_of_int (List.length inst_sg.doutputs)));
-         List.iter
-           (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
-           (List.combine outputs inst_sg.doutputs)
-     | _ -> (* TODO: trait methods *) ());
   (* 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
+  else
+    (* The backward function might also have been filtered if we do not
+       split the forward/backward functions *)
+    match func with
+    | None -> next_e
+    | Some func ->
+        log#ldebug
+          (lazy
+            (let args = List.map (texpression_to_string ctx) args in
+             "func: "
+             ^ texpression_to_string ctx func
+             ^ "\nfunc type: "
+             ^ pure_ty_to_string ctx func.ty
+             ^ "\n\nargs:\n" ^ String.concat "\n" args));
+        let call = mk_apps func args in
+        mk_let effect_info.can_fail output call next_e
 
 and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
     (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -2095,15 +2551,15 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
      let-binding:
      {[
        let id_back x nx =
-         let s = nx in // the name [s] is not important (only collision matters)
-                                                        ...
+       let s = nx in // the name [s] is not important (only collision matters)
+       ...
      ]}
 
      This let-binding later gets inlined, during a micro-pass.
   *)
   (* First, retrieve the list of variables used for the inputs for the
    * backward function *)
-  let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs in
+  let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state in
   (* Retrieve the values consumed upon ending the loans inside this
    * abstraction: as there are no nested borrows, there should be none. *)
   let consumed = abs_to_consumed ctx ectx abs in
@@ -2150,11 +2606,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
   | V.LoopSynthInput ->
       (* Actually the same case as [SynthInput] *)
       translate_end_abstraction_synth_input ectx abs e ctx rg_id
-  | V.LoopCall ->
+  | V.LoopCall -> (
+      (* We need to introduce a call to the backward function corresponding
+         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_context.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
@@ -2165,7 +2622,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
          values consumed upon ending the abstraction (i.e., we don't use
          [abs_to_consumed]) *)
       let back_inputs_vars =
-        T.RegionGroupId.Map.find rg_id ctx.backward_inputs
+        T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state
       in
       let back_inputs = List.map mk_texpression_from_var back_inputs_vars in
       (* If the function is stateful:
@@ -2175,12 +2632,15 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       let back_state, ctx, nstate =
         if effect_info.stateful then
           let back_state = mk_state_texpression ctx.state_var in
-          let ctx, nstate = bs_ctx_fresh_state_var ctx in
+          let ctx, _, nstate = bs_ctx_fresh_state_var ctx in
           ([ back_state ], ctx, Some nstate)
         else ([], ctx, None)
       in
       (* Concatenate all the inputs *)
-      let inputs = List.concat [ fwd_inputs; back_inputs; back_state ] in
+      let inputs =
+        if !Config.return_back_funs then List.concat [ back_inputs; back_state ]
+        else List.concat [ fwd_inputs; back_inputs; back_state ]
+      in
       (* Retrieve the values given back by this function *)
       let ctx, outputs = abs_to_given_back None abs ctx in
       (* Group the output values together: first the updated inputs *)
@@ -2204,68 +2664,88 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       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 = Fun (FromLlbc (FunId fun_id, Some loop_id, Some rg_id)) in
-      let func = { id = FunOrOp func; generics } in
-      let func = { e = Qualif func; ty = func_ty } in
-      let call = mk_apps func args in
+      (* Create the expression for the function:
+         - it is either a call to a top-level function, if we split the
+           forward/backward functions
+         - or a call to the variable we introduced for the backward function,
+           if we merge the forward/backward functions *)
+      let func =
+        if !Config.return_back_funs then
+          RegionGroupId.Map.find rg_id (Option.get loop_info.back_funs)
+        else
+          let func_ty = mk_arrows input_tys ret_ty in
+          let func = Fun (FromLlbc (FunId fun_id, Some loop_id, Some rg_id)) in
+          let func = { id = FunOrOp func; generics } in
+          Some { e = Qualif func; ty = func_ty }
+      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
+         =================
+         We do a small optimization here in case 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
-        (* Add meta-information - this is slightly hacky: we look at the
-           values consumed by the abstraction (note that those come from
-           *before* we applied the fixed-point context) and use them to
-           guide the naming of the output vars.
-
-           Also, we need to convert the backward outputs from patterns to
-           variables.
-
-           Finally, in practice, this works well only for loop bodies:
-           we do this only in this case.
-           TODO: improve the heuristics, to give weight to the hints for
-           instance.
-        *)
-        let next_e =
-          if ctx.inside_loop then
-            let consumed_values = abs_to_consumed ctx ectx abs in
-            let var_values = List.combine outputs consumed_values in
-            let var_values =
-              List.filter_map
-                (fun (var, v) ->
-                  match var.Pure.value with
-                  | PatVar (var, _) -> Some (var, v)
-                  | _ -> None)
-                var_values
+        (* In case we merge the fwd/back functions we filter the backward
+           functions elsewhere *)
+        match func with
+        | None -> next_e
+        | Some func ->
+            let call = mk_apps func args in
+            (* Add meta-information - this is slightly hacky: we look at the
+               values consumed by the abstraction (note that those come from
+               *before* we applied the fixed-point context) and use them to
+               guide the naming of the output vars.
+
+               Also, we need to convert the backward outputs from patterns to
+               variables.
+
+               Finally, in practice, this works well only for loop bodies:
+               we do this only in this case.
+               TODO: improve the heuristics, to give weight to the hints for
+               instance.
+            *)
+            let next_e =
+              if ctx.inside_loop then
+                let consumed_values = abs_to_consumed ctx ectx abs in
+                let var_values = List.combine outputs consumed_values in
+                let var_values =
+                  List.filter_map
+                    (fun (var, v) ->
+                      match var.Pure.value with
+                      | PatVar (var, _) -> Some (var, v)
+                      | _ -> None)
+                    var_values
+                in
+                let vars, values = List.split var_values in
+                mk_emeta_symbolic_assignments vars values next_e
+              else next_e
             in
-            let vars, values = List.split var_values in
-            mk_emeta_symbolic_assignments vars values next_e
-          else next_e
-        in
 
-        (* Create the let-binding *)
-        mk_let effect_info.can_fail output call next_e
+            (* Create the let-binding *)
+            mk_let effect_info.can_fail output call next_e)
 
 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
@@ -2290,8 +2770,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
@@ -2370,7 +2849,13 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
             If (true_e, false_e) )
       in
       let ty = true_e.ty in
-      assert (ty = false_e.ty);
+      log#ldebug
+        (lazy
+          ("true_e.ty: "
+          ^ pure_ty_to_string ctx true_e.ty
+          ^ "\n\nfalse_e.ty: "
+          ^ pure_ty_to_string ctx false_e.ty));
+      if !Config.fail_hard then assert (ty = false_e.ty);
       { e; ty }
   | ExpandInt (int_ty, branches, otherwise) ->
       let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
@@ -2441,7 +2926,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
@@ -2454,7 +2939,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
@@ -2547,7 +3032,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
@@ -2562,22 +3047,169 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
 
 and translate_forward_end (ectx : C.eval_ctx)
     (loop_input_values : V.typed_value S.symbolic_value_id_map option)
-    (e : S.expression) (back_e : S.expression S.region_group_id_map)
+    (fwd_e : S.expression) (back_e : S.expression S.region_group_id_map)
     (ctx : bs_ctx) : texpression =
-  (* Update the current state with the additional state received by the backward
-     function, if needs be, and lookup the proper expression *)
-  let translate_end ctx =
+  let translate_one_end ctx (bid : RegionGroupId.id option) =
+    let ctx = { ctx with bid } in
     (* Update the current state with the additional state received by the backward
        function, if needs be, and lookup the proper expression *)
-    let ctx, e =
-      match ctx.bid with
-      | None -> (ctx, e)
+    let ctx, e, finish =
+      match bid with
+      | None ->
+          (* We are translating the forward function - nothing to do *)
+          (ctx, fwd_e, fun e -> e)
       | Some bid ->
-          let ctx = { ctx with state_var = ctx.back_state_var } in
+          (* There are two cases here:
+             - if we split the fwd/backward functions, we simply need to update
+               the state.
+             - if we don't split, we also need to wrap the expression in a
+               lambda, which introduces the additional inputs of the backward
+               function
+          *)
+          let ctx =
+            (* Introduce variables for the inputs and the state variable
+               and update the context. *)
+            if !Config.return_back_funs then
+              (* If the forward/backward functions are not split, we need
+                 to introduce fresh variables for the additional inputs,
+                 because they are locally introduced in a lambda *)
+              let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in
+              let ctx, backward_inputs_no_state =
+                fresh_vars back_sg.inputs_no_state ctx
+              in
+              let ctx, backward_inputs_with_state =
+                if back_sg.effect_info.stateful then
+                  let ctx, var, _ = bs_ctx_fresh_state_var ctx in
+                  (ctx, backward_inputs_no_state @ [ var ])
+                else (ctx, backward_inputs_no_state)
+              in
+              {
+                ctx with
+                backward_inputs_no_state =
+                  RegionGroupId.Map.add bid backward_inputs_no_state
+                    ctx.backward_inputs_no_state;
+                backward_inputs_with_state =
+                  RegionGroupId.Map.add bid backward_inputs_with_state
+                    ctx.backward_inputs_with_state;
+              }
+            else
+              (* Update the state variable *)
+              let back_state_var =
+                RegionGroupId.Map.find bid ctx.back_state_vars
+              in
+              { ctx with state_var = back_state_var }
+          in
+
           let e = T.RegionGroupId.Map.find bid back_e in
-          (ctx, e)
+          let finish e =
+            (* Wrap in lambdas if necessary *)
+            if !Config.return_back_funs then
+              let inputs =
+                RegionGroupId.Map.find bid ctx.backward_inputs_with_state
+              in
+              let places = List.map (fun _ -> None) inputs in
+              mk_lambdas_from_vars inputs places e
+            else e
+          in
+          (ctx, e, finish)
     in
-    translate_expression e ctx
+    let e = translate_expression e ctx in
+    finish e
+  in
+
+  (* There are two cases, depending on whether we are splitting the forward/backward
+     functions or not.
+
+     - if we split, then we simply need to translate the proper "end" expression,
+       that is the end of the forward function, or of the backward function we
+       are currently translating.
+     - if we don't split, then we need to translate the end of the forward
+       function (this is the value we will return) and generate the bodies
+       of the backward functions (which we will also return).
+
+     Update the current state with the additional state received by the backward
+     function, if needs be, and lookup the proper expression.
+  *)
+  let translate_end ctx =
+    if !Config.return_back_funs then
+      (* Compute the output of the forward function *)
+      let fwd_effect_info = ctx.sg.fwd_info.effect_info in
+      let ctx, pure_fwd_var = fresh_var None ctx.sg.fwd_output ctx in
+      let fwd_e = translate_one_end ctx None in
+
+      (* Introduce the backward functions. *)
+      let back_el =
+        List.map
+          (fun ((gid, _) : RegionGroupId.id * back_sg_info) ->
+            translate_one_end ctx (Some gid))
+          (RegionGroupId.Map.bindings ctx.sg.back_sg)
+      in
+
+      (* 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. *)
+      let evaluate_backs =
+        List.map
+          (fun (sg : back_sg_info) ->
+            if !Config.simplify_merged_fwd_backs then
+              sg.inputs = [] && sg.effect_info.can_fail
+            else false)
+          (RegionGroupId.Map.values ctx.sg.back_sg)
+      in
+
+      (* Introduce variables for the backward functions.
+         We lookup the LLBC definition in an attempt to derive pretty names
+         for those functions. *)
+      let _, back_vars = fresh_back_vars_for_current_fun ctx in
+
+      (* Create the return expressions *)
+      let vars =
+        let back_vars = List.filter_map (fun x -> x) back_vars in
+        if ctx.sg.fwd_info.ignore_output then back_vars
+        else pure_fwd_var :: back_vars
+      in
+      let vars = List.map mk_texpression_from_var vars in
+      let ret = mk_simpl_tuple_texpression vars in
+
+      (* Introduce a fresh input state variable for the forward expression *)
+      let _ctx, state_var, state_pat =
+        if fwd_effect_info.stateful then
+          let ctx, var, pat = bs_ctx_fresh_state_var ctx in
+          (ctx, [ var ], [ pat ])
+        else (ctx, [], [])
+      in
+
+      let state_var = List.map mk_texpression_from_var state_var in
+      let ret = mk_simpl_tuple_texpression (state_var @ [ ret ]) in
+      let ret = mk_result_return_texpression ret in
+
+      (* Introduce all the let-bindings *)
+
+      (* Combine:
+         - the backward variables
+         - whether we should evaluate the expression for the backward function
+           (i.e., should we use a monadic let-binding or not - we do if the
+           backward functions don't have inputs and can fail)
+         - the expressions for the backward functions
+      *)
+      let back_vars_els =
+        List.filter_map
+          (fun (v, (eval, el)) ->
+            match v with None -> None | Some v -> Some (v, eval, el))
+          (List.combine back_vars (List.combine evaluate_backs back_el))
+      in
+      let e =
+        List.fold_right
+          (fun (var, evaluate, back_e) e ->
+            mk_let evaluate (mk_typed_pattern_from_var var None) back_e e)
+          back_vars_els ret
+      in
+      (* Bind the expression for the forward output *)
+      let fwd_var = mk_typed_pattern_from_var pure_fwd_var None in
+      let pat = mk_simpl_tuple_pattern (state_pat @ [ fwd_var ]) in
+      mk_let fwd_effect_info.can_fail pat fwd_e e
+    else translate_one_end ctx ctx.bid
   in
 
   (* If we are (re-)entering a loop, we need to introduce a call to the
@@ -2624,17 +3256,53 @@ 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
-      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 =
-        let output_ty = mk_simpl_tuple_ty ctx.fwd_sg.doutputs in
-        fresh_var None output_ty ctx
+      let ctx, fwd_output, output_pat =
+        if ctx.sg.fwd_info.ignore_output then
+          (* Note that we still need the forward output (which is unit),
+             because even though the loop function will ignore the forward output,
+             the forward expression will still compute an output (which
+             will have type unit - otherwise we can't ignore it). *)
+          (ctx, mk_unit_rvalue, [])
+        else
+          let ctx, output_var = fresh_var None ctx.sg.fwd_output ctx in
+          ( ctx,
+            mk_texpression_from_var output_var,
+            [ mk_typed_pattern_from_var output_var None ] )
+      in
+
+      (* Introduce fresh variables for the backward functions of the loop.
+
+         For now, the backward functions of the loop are the same as the
+         backward functions of the outer function.
+      *)
+      let ctx, back_funs_map, back_funs =
+        if !Config.return_back_funs then
+          let ctx, back_vars = fresh_back_vars_for_current_fun ctx in
+          let back_funs =
+            List.filter_map
+              (fun v ->
+                match v with
+                | None -> None
+                | Some v -> Some (mk_typed_pattern_from_var v None))
+              back_vars
+          in
+          let gids = RegionGroupId.Map.keys ctx.sg.back_sg in
+          let back_funs_map =
+            RegionGroupId.Map.of_list
+              (List.combine gids
+                 (List.map (Option.map mk_texpression_from_var) back_vars))
+          in
+          (ctx, Some back_funs_map, back_funs)
+        else (ctx, None, [])
       in
+
+      (* Introduce patterns *)
       let args, ctx, out_pats =
-        let output_pat = mk_typed_pattern_from_var output_var None in
+        (* Add the returned backward functions (they might be empty) *)
+        let output_pat = mk_simpl_tuple_pattern (output_pat @ back_funs) in
 
         (* Depending on the function effects:
          * - add the fuel
@@ -2644,7 +3312,7 @@ and translate_forward_end (ectx : C.eval_ctx)
         let fuel = mk_fuel_input_as_list ctx effect_info in
         if effect_info.stateful then
           let state_var = mk_state_texpression ctx.state_var in
-          let ctx, nstate_pat = bs_ctx_fresh_state_var ctx in
+          let ctx, _, nstate_pat = bs_ctx_fresh_state_var ctx in
           ( List.concat [ fuel; args; [ state_var ] ],
             ctx,
             [ nstate_pat; output_pat ] )
@@ -2656,7 +3324,8 @@ and translate_forward_end (ectx : C.eval_ctx)
         {
           loop_info with
           forward_inputs = Some args;
-          forward_output_no_state_no_result = Some output_var;
+          forward_output_no_state_no_result = Some fwd_output;
+          back_funs = back_funs_map;
         }
       in
       let ctx =
@@ -2753,35 +3422,107 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
 
   (* Compute the backward outputs *)
   let ctx = ref ctx in
-  let loop_backward_outputs =
-    T.RegionGroupId.Map.map
+  let rg_to_given_back_tys =
+    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_context.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
 
-  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
+  (* The output type of the loop function *)
+  let fwd_effect_info = { ctx.sg.fwd_info.effect_info with is_rec = true } in
+  let back_effect_infos, output_ty =
+    if !Config.return_back_funs then
+      (* The loop backward functions consume the same additional inputs as the parent
+         function, but have custom outputs *)
+      let back_sgs = RegionGroupId.Map.bindings ctx.sg.back_sg in
+      let given_back_tys = RegionGroupId.Map.values rg_to_given_back_tys in
+      let back_info_tys =
+        List.map
+          (fun (((id, back_sg), given_back) : (_ * back_sg_info) * ty list) ->
+            (* Remark: the effect info of the backward function for the loop
+               is almost the same as for the backward function of the parent function.
+               Quite importantly, the fact that the function is stateful and/or can fail
+               mostly depends on whether it has inputs or not, and the backward functions
+               for the loops have the same inputs as the backward functions for the parent
+               function.
+            *)
+            let effect_info = back_sg.effect_info in
+            let effect_info = { effect_info with is_rec = true } in
+            (* Compute the input/output types *)
+            let inputs = List.map snd back_sg.inputs in
+            let outputs = given_back in
+            (* Filter if necessary *)
+            let ty =
+              if
+                !Config.simplify_merged_fwd_backs && inputs = [] && outputs = []
+              then None
+              else
+                let output = mk_simpl_tuple_ty outputs in
+                let output =
+                  mk_back_output_ty_from_effect_info effect_info inputs output
+                in
+                let ty = mk_arrows inputs output in
+                Some ty
+            in
+            ((id, effect_info), ty))
+          (List.combine back_sgs given_back_tys)
+      in
+      let back_info = List.map fst back_info_tys in
+      let back_info = RegionGroupId.Map.of_list back_info in
+      let back_tys = List.filter_map snd back_info_tys in
+      let output =
+        if ctx.sg.fwd_info.ignore_output then back_tys
+        else ctx.sg.fwd_output :: back_tys
+      in
+      let output = mk_simpl_tuple_ty output in
+      let effect_info = ctx.sg.fwd_info.effect_info in
+      let output =
+        if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ]
+        else output
+      in
+      let output =
+        if effect_info.can_fail && inputs <> [] then mk_result_ty output
+        else output
+      in
+      (back_info, output)
+    else
+      let back_info =
+        RegionGroupId.Map.of_list
+          (List.map
+             (fun ((id, back_sg) : _ * back_sg_info) ->
+               (id, { back_sg.effect_info with is_rec = true }))
+             (RegionGroupId.Map.bindings ctx.sg.back_sg))
+      in
+      let output =
+        match ctx.bid with
+        | None ->
+            (* Forward function: same type as the parent function *)
+            (translate_fun_sig_from_decomposed ctx.sg None).output
+        | Some rg_id ->
+            (* Backward function: custom return type *)
+            let doutputs =
+              T.RegionGroupId.Map.find rg_id rg_to_given_back_tys
+            in
+            let output = mk_simpl_tuple_ty doutputs in
+            let fwd_effect_info = ctx.sg.fwd_info.effect_info in
+            let output =
+              if fwd_effect_info.stateful then
+                mk_simpl_tuple_ty [ mk_state_ty; output ]
+              else output
+            in
+            let output =
+              if fwd_effect_info.can_fail then mk_result_ty output else output
+            in
+            output
+      in
+      (back_info, output)
   in
 
   (* Add the loop information in the context *)
@@ -2823,6 +3564,10 @@ 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;
+        back_funs = None;
+        fwd_effect_info;
+        back_effect_infos;
       }
     in
     let loops = LoopId.Map.add loop_id loop_info ctx.loops in
@@ -2830,13 +3575,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 *)
@@ -2844,7 +3583,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
 
   (* Add the input state *)
   let input_state =
-    if ctx.sg.info.effect_info.stateful then Some ctx.state_var else None
+    if (ctx_get_effect_info ctx).stateful then Some ctx.state_var else None
   in
 
   (* Translate the loop body *)
@@ -2862,7 +3601,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         input_state;
         inputs;
         inputs_lvs;
-        back_output_tys;
+        output_ty;
         loop_body;
       }
   in
@@ -2982,10 +3721,10 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let def_id = def.def_id in
   let llbc_name = def.name in
   let name = name_to_string ctx llbc_name in
-  (* Retrieve the signature *)
-  let signature = ctx.sg in
+  (* 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 =
@@ -2993,8 +3732,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_context.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 *)
@@ -3027,20 +3765,25 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
           match bid with
           | None -> []
           | Some back_id ->
+              assert (not !Config.return_back_funs);
               let parents_ids =
                 list_ordered_ancestor_region_groups regions_hierarchy back_id
               in
               let backward_ids = List.append parents_ids [ back_id ] in
               List.concat
                 (List.map
-                   (fun id -> T.RegionGroupId.Map.find id ctx.backward_inputs)
+                   (fun id ->
+                     T.RegionGroupId.Map.find id ctx.backward_inputs_no_state)
                    backward_ids)
         in
         (* Introduce the backward input state (the state at call site of the
          * *backward* function), if necessary *)
         let back_state =
           if effect_info.stateful && Option.is_some bid then
-            [ mk_state_var ctx.back_state_var ]
+            let state_var =
+              RegionGroupId.Map.find (Option.get bid) ctx.back_state_vars
+            in
+            [ mk_state_var state_var ]
           else []
         in
         (* Group the inputs together *)
@@ -3114,63 +3857,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 =
-      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/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index efcf001a..865185a8 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,7 +93,9 @@ 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)
+    (trait_method_generics : (generic_args * trait_instance_id) option)
     (args : typed_value list) (args_places : mplace option list)
     (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
     : expression option =
@@ -102,8 +105,11 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
         {
           call_id;
           ctx;
+          sg;
+          regions_hierarchy;
           abstractions;
           generics;
+          trait_method_generics;
           args;
           dest;
           args_places;
@@ -118,29 +124,32 @@ 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)
+    (trait_method_generics : (generic_args * trait_instance_id) option)
     (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 trait_method_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 None [ 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 ]
-    [ arg0_place; arg1_place ] dest dest_place e
+  synthesize_function_call (Binop binop) ctx None [] [] generics None
+    [ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e
 
 let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : abs)
     (e : expression option) : expression option =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 221d4e73..55a94302 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,8 +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)
-    (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t)
-    (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
@@ -58,13 +57,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
@@ -78,7 +73,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;
@@ -86,15 +81,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_sigs;
       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
 
@@ -126,31 +120,51 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
         !m
   in
 
+  let sg =
+    SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef
+  in
+
+  let regions_hierarchy =
+    LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_ctx.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 =
     {
+      decls_ctx = trans_ctx;
       SymbolicToPure.bid = None;
-      (* Dummy for now *)
-      sg = forward_sig.sg;
-      fwd_sg = forward_sig.sg;
+      sg;
+      fun_dsigs;
       (* 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;
-      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;
       forward_inputs = [];
-      (* Empty for now *)
-      backward_inputs = RegionGroupId.Map.empty;
-      (* Empty for now *)
-      backward_outputs = RegionGroupId.Map.empty;
-      loop_backward_outputs = None;
+      (* Initialized just below *)
+      backward_inputs_no_state = RegionGroupId.Map.empty;
+      (* Initialized just below *)
+      backward_inputs_with_state = RegionGroupId.Map.empty;
+      backward_outputs = None;
       (* Empty for now *)
       calls;
       abstractions;
@@ -180,6 +194,37 @@ 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
+
   (* Translate the forward function *)
   let pure_forward =
     match symbolic_trans with
@@ -187,7 +232,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,77 +242,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
-          (* We need to ignore the forward state and the backward state *)
-          let num_forward_inputs =
-            sg.info.num_fwd_inputs_with_fuel_with_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
-        (* 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)
@@ -294,36 +282,21 @@ 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)
+  (* 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
-  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 fun_dsigs)
       (FunDeclId.Map.values crate.fun_decls)
   in
 
@@ -1030,7 +1003,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
@@ -1198,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