Merge pull request #85 from AeneasVerif/son/fix_loops3

Fix some issues with the loops

28 files changed, 1185 insertions, 350 deletions

diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 3c2ea877..f30148dc 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -510,9 +510,19 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr)
              let i ← mkFinVal grSize id
              -- Check that there are no type parameters
              if type_info.num_params ≠ 0 then throwError "mkUnaryBodies: a recursive call was not eliminated"
-             -- Introduce the call to the continuation
-             let param_args ← mkSigmasVal type_info.params_ty []
-             mkAppM' kk_var #[i, param_args]
+             -- We might be in a degenerate case, if the function takes no arguments
+             -- at all (i.e., the function is a constant).
+             -- For instance:
+             -- ```
+             -- divergent def infinite_loop : Result Unit := infinite_loop
+             -- ``
+             if type_info.total_num_args == 0 then do
+                trace[Diverge.def.genBody.visit] "Degenerate case: total_num_args=0"
+                mkAppM' kk_var #[i, UnitValue, UnitValue]
+             else do
+               -- Introduce the call to the continuation
+               let param_args ← mkSigmasVal type_info.params_ty []
+               mkAppM' kk_var #[i, param_args]
          else pure e
        | _ => pure e
     trace[Diverge.def.genBody.visit] "done with expression (depth: {i}): {e}"
@@ -1571,6 +1581,20 @@ namespace Tests
 
   #check test1.unfold
 
+  -- Testing a degenerate case
+  divergent def infinite_loop : Result Unit :=
+    do
+    let _ ← infinite_loop
+    Result.ret ()
+
+  #check infinite_loop.unfold
+
+  -- Testing a degenerate case
+  divergent def infinite_loop1 : Result Unit :=
+    infinite_loop1
+
+  #check infinite_loop1.unfold
+
   /- Tests with higher-order functions -/
   section HigherOrder
     open Ex8
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 54411fd5..2563bd9d 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -467,8 +467,8 @@ let env_find_abs (env : env) (pred : abs -> bool) : abs option =
   in
   lookup env
 
-let env_lookup_abs (env : env) (abs_id : AbstractionId.id) : abs =
-  Option.get (env_find_abs env (fun abs -> abs.abs_id = abs_id))
+let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
+  env_find_abs env (fun abs -> abs.abs_id = abs_id)
 
 (** Remove an abstraction from the context, as well as all the references to
     this abstraction (for instance, remove the abs id from all the parent sets
@@ -524,8 +524,12 @@ let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
   in
   update env
 
+let ctx_lookup_abs_opt (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs option
+    =
+  env_lookup_abs_opt ctx.env abs_id
+
 let ctx_lookup_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs =
-  env_lookup_abs ctx.env abs_id
+  Option.get (ctx_lookup_abs_opt ctx abs_id)
 
 let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
   env_find_abs ctx.env p
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 22d176c9..fd3e334b 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -301,6 +301,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   let parent_input_abs_ids =
     List.filter_map (fun x -> x) parent_input_abs_ids
   in
+  (* TODO: need to be careful for loops *)
+  assert (parent_input_abs_ids = []);
 
   (* Insert the return value in the return abstractions (by applying
    * borrow projections) *)
@@ -354,8 +356,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       let fun_abs_id =
         (RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
       in
-      if not inside_loop then (fun_abs_id, true)
+      if not inside_loop then (Some fun_abs_id, true)
       else
+        (* We are inside a loop *)
         let pred (abs : abs) =
           match abs.kind with
           | Loop (_, rg_id', kind) ->
@@ -383,14 +386,24 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
              }
            ]}
         *)
-        let abs = Option.get (ctx_find_abs ctx pred) in
-        (abs.abs_id, false)
+        match ctx_find_abs ctx pred with
+        | None ->
+            (* The loop gives back nothing for this region group.
+               Ex.:
+               {[
+                 pub fn ignore_input_mut_borrow(_a: &mut u32) {
+                     loop {}
+                 }
+               ]}
+            *)
+            (None, false)
+        | Some abs -> (Some abs.abs_id, false)
     in
     log#ldebug
       (lazy
         ("evaluate_function_symbolic_synthesize_backward_from_return: ending \
           input abstraction: "
-        ^ AbstractionId.to_string current_abs_id));
+        ^ Print.option_to_string AbstractionId.to_string current_abs_id));
 
     (* Set the proper abstractions as endable *)
     let ctx =
@@ -427,7 +440,10 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       visit_loop_abs#visit_eval_ctx () ctx
     in
 
-    let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
+    let current_abs_id =
+      match current_abs_id with None -> [] | Some id -> [ id ]
+    in
+    let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
     let cf_end_target_abs cf =
       List.fold_left
         (fun cf id -> end_abstraction config id cf)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index a2eb2545..03b2b045 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -963,74 +963,86 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       ^ AbstractionId.to_string abs_id
       ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
 
-  (* Lookup the abstraction *)
-  let abs = ctx_lookup_abs ctx abs_id in
-
-  (* Check that we can end the abstraction *)
-  if abs.can_end then ()
-  else
-    raise
-      (Failure
-         ("Can't end abstraction "
-         ^ AbstractionId.to_string abs.abs_id
-         ^ " as it is set as non-endable"));
-
-  (* End the parent abstractions first *)
-  let cc = end_abstractions_aux config chain abs.parents in
-  let cc =
-    comp_unit cc (fun ctx ->
-        log#ldebug
-          (lazy
-            ("end_abstraction_aux: "
-            ^ AbstractionId.to_string abs_id
-            ^ "\n- context after parent abstractions ended:\n"
-            ^ eval_ctx_to_string ctx)))
-  in
+  (* Lookup the abstraction - note that if we end a list of abstractions,
+     ending one abstraction may lead to the current abstraction having
+     preemptively been ended, so the abstraction might not be in the context
+     anymore. *)
+  match ctx_lookup_abs_opt ctx abs_id with
+  | None ->
+      log#ldebug
+        (lazy
+          ("abs not found (already ended): "
+          ^ AbstractionId.to_string abs_id
+          ^ "\n"));
+      cf ctx
+  | Some abs ->
+      (* Check that we can end the abstraction *)
+      if abs.can_end then ()
+      else
+        raise
+          (Failure
+             ("Can't end abstraction "
+             ^ AbstractionId.to_string abs.abs_id
+             ^ " as it is set as non-endable"));
+
+      (* End the parent abstractions first *)
+      let cc = end_abstractions_aux config chain abs.parents in
+      let cc =
+        comp_unit cc (fun ctx ->
+            log#ldebug
+              (lazy
+                ("end_abstraction_aux: "
+                ^ AbstractionId.to_string abs_id
+                ^ "\n- context after parent abstractions ended:\n"
+                ^ eval_ctx_to_string ctx)))
+      in
 
-  (* End the loans inside the abstraction *)
-  let cc = comp cc (end_abstraction_loans config chain abs_id) in
-  let cc =
-    comp_unit cc (fun ctx ->
-        log#ldebug
-          (lazy
-            ("end_abstraction_aux: "
-            ^ AbstractionId.to_string abs_id
-            ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
-  in
+      (* End the loans inside the abstraction *)
+      let cc = comp cc (end_abstraction_loans config chain abs_id) in
+      let cc =
+        comp_unit cc (fun ctx ->
+            log#ldebug
+              (lazy
+                ("end_abstraction_aux: "
+                ^ AbstractionId.to_string abs_id
+                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
+      in
 
-  (* End the abstraction itself by redistributing the borrows it contains *)
-  let cc = comp cc (end_abstraction_borrows config chain abs_id) in
+      (* End the abstraction itself by redistributing the borrows it contains *)
+      let cc = comp cc (end_abstraction_borrows config chain abs_id) in
 
-  (* End the regions owned by the abstraction - note that we don't need to
-   * relookup the abstraction: the set of regions in an abstraction never
-   * changes... *)
-  let cc =
-    comp_update cc (fun ctx ->
-        let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in
-        { ctx with ended_regions })
-  in
+      (* End the regions owned by the abstraction - note that we don't need to
+       * relookup the abstraction: the set of regions in an abstraction never
+       * changes... *)
+      let cc =
+        comp_update cc (fun ctx ->
+            let ended_regions =
+              RegionId.Set.union ctx.ended_regions abs.regions
+            in
+            { ctx with ended_regions })
+      in
 
-  (* Remove all the references to the id of the current abstraction, and remove
-   * the abstraction itself.
-   * **Rk.**: this is where we synthesize the updated symbolic AST *)
-  let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
+      (* Remove all the references to the id of the current abstraction, and remove
+       * the abstraction itself.
+       * **Rk.**: this is where we synthesize the updated symbolic AST *)
+      let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
 
-  (* Debugging *)
-  let cc =
-    comp_unit cc (fun ctx ->
-        log#ldebug
-          (lazy
-            ("end_abstraction_aux: "
-            ^ AbstractionId.to_string abs_id
-            ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
-            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
-  in
+      (* Debugging *)
+      let cc =
+        comp_unit cc (fun ctx ->
+            log#ldebug
+              (lazy
+                ("end_abstraction_aux: "
+                ^ AbstractionId.to_string abs_id
+                ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
+                ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
+      in
 
-  (* Sanity check: ending an abstraction must preserve the invariants *)
-  let cc = comp cc Invariants.cf_check_invariants in
+      (* Sanity check: ending an abstraction must preserve the invariants *)
+      let cc = comp cc Invariants.cf_check_invariants in
 
-  (* Apply the continuation *)
-  cc cf ctx
+      (* Apply the continuation *)
+      cc cf ctx
 
 and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
     (abs_ids : AbstractionId.Set.t) : cm_fun =
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 6ee08e47..afbe0501 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -30,6 +30,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
      new context (and repeat this an indefinite number of times).
   *)
   let rec reeval_loop_body (res : statement_eval_res) : m_fun =
+    log#ldebug (lazy "eval_loop_concrete: reeval_loop_body");
     match res with
     | Return -> cf (LoopReturn loop_id)
     | Panic -> cf Panic
@@ -90,139 +91,169 @@ let eval_loop_symbolic (config : config) (meta : meta)
      loop entry with the fixed point: in the synthesized code, the function
      will end with a call to the loop translation
   *)
-  let fp_bl_corresp =
-    compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
-  in
-  log#ldebug
-    (lazy
-      ("eval_loop_symbolic: about to match the fixed-point context with the \
-        original context:\n\
-        - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
-     ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
-  let end_expr : SymbolicAst.expression option =
-    match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues
-      fixed_ids fp_ctx cf ctx
-  in
-  log#ldebug
-    (lazy
-      "eval_loop_symbolic: matched the fixed-point context with the original \
-       context");
-
-  (* Synthesize the loop body by evaluating it, with the continuation for
-     after the loop starting at the *fixed point*, but with a special
-     treatment for the [Break] and [Continue] cases *)
-  let cf_loop : st_m_fun =
-   fun res ctx ->
-    match res with
-    | Return ->
-        (* We replace the [Return] with a [LoopReturn] *)
-        cf (LoopReturn loop_id) ctx
-    | Panic -> cf res ctx
-    | Break i ->
-        (* Break out of the loop by calling the continuation *)
-        let res = if i = 0 then Unit else Break (i - 1) in
-        cf res ctx
-    | Continue i ->
-        (* We don't support nested loops for now *)
-        assert (i = 0);
-        log#ldebug
-          (lazy
-            ("eval_loop_symbolic: about to match the fixed-point context with \
-              the context at a continue:\n\
-              - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
-           ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ctx));
-        let cc =
-          match_ctx_with_target config loop_id false fp_bl_corresp
-            fp_input_svalues fixed_ids fp_ctx
-        in
-        cc cf ctx
-    | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
-        (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
-           For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
-        *)
-        raise (Failure "Unreachable")
+  (* First, preemptively end borrows/move values by matching the current
+     context with the target context *)
+  let cf_prepare_ctx cf ctx =
+    log#ldebug
+      (lazy
+        ("eval_loop_symbolic: about to reorganize the original context to \
+          match the fixed-point ctx with it:\n\
+          - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx
+       ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
+
+    prepare_match_ctx_with_target config loop_id fixed_ids fp_ctx cf ctx
   in
-  let loop_expr = eval_loop_body cf_loop fp_ctx in
 
-  log#ldebug
-    (lazy
-      ("eval_loop_symbolic: result:" ^ "\n- src context:\n"
-      ^ eval_ctx_to_string_no_filter ctx
-      ^ "\n- fixed point:\n"
-      ^ eval_ctx_to_string_no_filter fp_ctx
-      ^ "\n- fixed_sids: "
-      ^ SymbolicValueId.Set.show fixed_ids.sids
-      ^ "\n- fresh_sids: "
-      ^ SymbolicValueId.Set.show fresh_sids
-      ^ "\n- input_svalues: "
-      ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
-      ^ "\n\n"));
-
-  (* For every abstraction introduced by the fixed-point, compute the
-     types of the given back values.
-
-     We need to explore the abstractions, looking for the mutable borrows.
-     Moreover, we list the borrows in the same order as the loans (this
-     is important in {!SymbolicToPure}, where we expect the given back
-     values to have a specific order.
-  *)
-  let compute_abs_given_back_tys (abs : abs) : RegionId.Set.t * rty list =
-    let is_borrow (av : typed_avalue) : bool =
-      match av.value with
-      | ABorrow _ -> true
-      | ALoan _ -> false
-      | _ -> raise (Failure "Unreachable")
-    in
-    let borrows, loans = List.partition is_borrow abs.avalues in
-
-    let borrows =
-      List.filter_map
-        (fun (av : typed_avalue) ->
-          match av.value with
-          | ABorrow (AMutBorrow (bid, child_av)) ->
-              assert (is_aignored child_av.value);
-              Some (bid, child_av.ty)
-          | ABorrow (ASharedBorrow _) -> None
-          | _ -> raise (Failure "Unreachable"))
-        borrows
+  (* Actually match *)
+  let cf_match_ctx cf ctx =
+    log#ldebug
+      (lazy
+        ("eval_loop_symbolic: about to compute the id correspondance between \
+          the fixed-point ctx and the original ctx:\n\
+          - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
+       ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
+
+    (* Compute the id correspondance between the contexts *)
+    let fp_bl_corresp =
+      compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
     in
-    let borrows = ref (BorrowId.Map.of_list borrows) in
-
-    let loan_ids =
-      List.filter_map
-        (fun (av : typed_avalue) ->
-          match av.value with
-          | ALoan (AMutLoan (bid, child_av)) ->
-              assert (is_aignored child_av.value);
-              Some bid
-          | ALoan (ASharedLoan _) -> None
-          | _ -> raise (Failure "Unreachable"))
-        loans
+    log#ldebug
+      (lazy
+        ("eval_loop_symbolic: about to match the fixed-point context with the \
+          original context:\n\
+          - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
+       ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
+    let end_expr : SymbolicAst.expression option =
+      match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues
+        fixed_ids fp_ctx cf ctx
     in
+    log#ldebug
+      (lazy
+        "eval_loop_symbolic: matched the fixed-point context with the original \
+         context");
 
-    (* List the given back types, in the order given by the loans *)
-    let given_back_tys =
-      List.map
-        (fun lid ->
-          let bid =
-            BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
+    (* Synthesize the loop body by evaluating it, with the continuation for
+       after the loop starting at the *fixed point*, but with a special
+       treatment for the [Break] and [Continue] cases *)
+    let cf_loop : st_m_fun =
+     fun res ctx ->
+      log#ldebug (lazy "eval_loop_symbolic: cf_loop");
+      match res with
+      | Return ->
+          (* We replace the [Return] with a [LoopReturn] *)
+          cf (LoopReturn loop_id) ctx
+      | Panic -> cf res ctx
+      | Break i ->
+          (* Break out of the loop by calling the continuation *)
+          let res = if i = 0 then Unit else Break (i - 1) in
+          cf res ctx
+      | Continue i ->
+          (* We don't support nested loops for now *)
+          assert (i = 0);
+          log#ldebug
+            (lazy
+              ("eval_loop_symbolic: about to match the fixed-point context \
+                with the context at a continue:\n\
+                - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx
+             ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ctx));
+          let cc =
+            match_ctx_with_target config loop_id false fp_bl_corresp
+              fp_input_svalues fixed_ids fp_ctx
           in
-          let ty = BorrowId.Map.find bid !borrows in
-          borrows := BorrowId.Map.remove bid !borrows;
-          ty)
-        loan_ids
+          cc cf ctx
+      | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
+          (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
+             For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
+          *)
+          raise (Failure "Unreachable")
     in
-    assert (BorrowId.Map.is_empty !borrows);
+    let loop_expr = eval_loop_body cf_loop fp_ctx in
 
-    (abs.regions, given_back_tys)
-  in
-  let rg_to_given_back =
-    RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
-  in
+    log#ldebug
+      (lazy
+        ("eval_loop_symbolic: result:" ^ "\n- src context:\n"
+        ^ eval_ctx_to_string_no_filter ctx
+        ^ "\n- fixed point:\n"
+        ^ eval_ctx_to_string_no_filter fp_ctx
+        ^ "\n- fixed_sids: "
+        ^ SymbolicValueId.Set.show fixed_ids.sids
+        ^ "\n- fresh_sids: "
+        ^ SymbolicValueId.Set.show fresh_sids
+        ^ "\n- input_svalues: "
+        ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
+        ^ "\n\n"));
+
+    (* For every abstraction introduced by the fixed-point, compute the
+       types of the given back values.
+
+       We need to explore the abstractions, looking for the mutable borrows.
+       Moreover, we list the borrows in the same order as the loans (this
+       is important in {!SymbolicToPure}, where we expect the given back
+       values to have a specific order.
+
+       Also, we filter the backward functions which and
+       return nothing.
+    *)
+    let compute_abs_given_back_tys (abs : abs) : rty list =
+      let is_borrow (av : typed_avalue) : bool =
+        match av.value with
+        | ABorrow _ -> true
+        | ALoan _ -> false
+        | _ -> raise (Failure "Unreachable")
+      in
+      let borrows, loans = List.partition is_borrow abs.avalues in
+
+      let borrows =
+        List.filter_map
+          (fun (av : typed_avalue) ->
+            match av.value with
+            | ABorrow (AMutBorrow (bid, child_av)) ->
+                assert (is_aignored child_av.value);
+                Some (bid, child_av.ty)
+            | ABorrow (ASharedBorrow _) -> None
+            | _ -> raise (Failure "Unreachable"))
+          borrows
+      in
+      let borrows = ref (BorrowId.Map.of_list borrows) in
 
-  (* Put together *)
-  S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
-    loop_expr meta
+      let loan_ids =
+        List.filter_map
+          (fun (av : typed_avalue) ->
+            match av.value with
+            | ALoan (AMutLoan (bid, child_av)) ->
+                assert (is_aignored child_av.value);
+                Some bid
+            | ALoan (ASharedLoan _) -> None
+            | _ -> raise (Failure "Unreachable"))
+          loans
+      in
+
+      (* List the given back types, in the order given by the loans *)
+      let given_back_tys =
+        List.map
+          (fun lid ->
+            let bid =
+              BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
+            in
+            let ty = BorrowId.Map.find bid !borrows in
+            borrows := BorrowId.Map.remove bid !borrows;
+            ty)
+          loan_ids
+      in
+      assert (BorrowId.Map.is_empty !borrows);
+
+      given_back_tys
+    in
+    let rg_to_given_back =
+      RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
+    in
+
+    (* Put together *)
+    S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
+      loop_expr meta
+  in
+  (* Compose *)
+  comp cf_prepare_ctx cf_match_ctx cf ctx
 
 let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
     st_cm_fun =
@@ -230,6 +261,10 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
   match config.mode with
   | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
   | SymbolicMode ->
+      (* Simplify the context by ending the unnecessary borrows/loans and getting
+         rid of the useless symbolic values (which are in anonymous variables) *)
+      let cc = cleanup_fresh_values_and_abs config empty_ids_set in
+
       (* We want to make sure the loop will *not* manipulate shared avalues
          containing themselves shared loans (i.e., nested shared loans in
          the abstractions), because it complexifies the matches between values
@@ -248,5 +283,5 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
          introduce *fixed* abstractions, and again later to introduce
          *non-fixed* abstractions.
       *)
-      let cc = prepare_ashared_loans None in
+      let cc = comp cc (prepare_ashared_loans None) in
       comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index e663eb42..0bd57756 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -12,6 +12,7 @@ type updt_env_kind =
   | AbsInRight of AbstractionId.id
   | LoanInRight of BorrowId.id
   | LoansInRight of BorrowId.Set.t
+[@@deriving show]
 
 (** Utility exception *)
 exception ValueMatchFailure of updt_env_kind
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 4dabe974..66c97cde 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -6,6 +6,8 @@ open ValuesUtils
 module S = SynthesizeSymbolic
 open Cps
 open InterpreterUtils
+open InterpreterBorrowsCore
+open InterpreterBorrows
 open InterpreterLoopsCore
 open InterpreterLoopsMatchCtxs
 open InterpreterLoopsJoinCtxs
@@ -13,6 +15,119 @@ open InterpreterLoopsJoinCtxs
 (** The local logger *)
 let log = Logging.loops_fixed_point_log
 
+exception FoundBorrowId of BorrowId.id
+exception FoundAbsId of AbstractionId.id
+
+(* Repeat until we can't simplify the context anymore:
+   - end the borrows which appear in fresh anonymous values and don't contain loans
+   - end the fresh region abstractions which can be ended (no loans)
+*)
+let rec end_useless_fresh_borrows_and_abs (config : config)
+    (fixed_ids : ids_sets) : cm_fun =
+ fun cf ctx ->
+  let rec explore_env (env : env) : unit =
+    match env with
+    | [] -> () (* Done *)
+    | EBinding (BDummy vid, v) :: env
+      when not (DummyVarId.Set.mem vid fixed_ids.dids) ->
+        (* Explore the anonymous value - raises an exception if it finds
+           a borrow to end *)
+        let visitor =
+          object
+            inherit [_] iter_typed_value
+            method! visit_VLoan _ _ = () (* Don't enter inside loans *)
+
+            method! visit_VBorrow _ bc =
+              (* Check if we can end the borrow, do not enter inside if we can't *)
+              match bc with
+              | VSharedBorrow bid | VReservedMutBorrow bid ->
+                  raise (FoundBorrowId bid)
+              | VMutBorrow (bid, v) ->
+                  if not (value_has_loans v.value) then
+                    raise (FoundBorrowId bid)
+                  else (* Stop there *)
+                    ()
+          end
+        in
+        visitor#visit_typed_value () v;
+        (* No exception was raised: continue *)
+        explore_env env
+    | EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)
+      -> (
+        (* Check if it is possible to end the abstraction: if yes, raise an exception *)
+        let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+        match opt_loan with
+        | None ->
+            (* No remaining loans: we can end the abstraction *)
+            raise (FoundAbsId abs.abs_id)
+        | Some _ ->
+            (* There are remaining loans: we can't end the abstraction *)
+            explore_env env)
+    | _ :: env -> explore_env env
+  in
+  let rec_call = end_useless_fresh_borrows_and_abs config fixed_ids in
+  try
+    (* Explore the environment *)
+    explore_env ctx.env;
+    (* No exception raised: call the continuation *)
+    cf ctx
+  with
+  | FoundAbsId abs_id ->
+      let cc = end_abstraction config abs_id in
+      comp cc rec_call cf ctx
+  | FoundBorrowId bid ->
+      let cc = end_borrow config bid in
+      comp cc rec_call cf ctx
+
+(* Explore the fresh anonymous values and replace all the values which are not
+   borrows/loans with ⊥ *)
+let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun =
+ fun cf ctx ->
+  let rec explore_env (env : env) : env =
+    match env with
+    | [] -> [] (* Done *)
+    | EBinding (BDummy vid, v) :: env
+      when not (DummyVarId.Set.mem vid fixed_ids.dids) ->
+        let env = explore_env env in
+        (* Eliminate the value altogether if it doesn't contain loans/borrows *)
+        if not (value_has_loans_or_borrows ctx v.value) then env
+        else
+          (* Explore the anonymous value - raises an exception if it finds
+             a borrow to end *)
+          let visitor =
+            object
+              inherit [_] map_typed_value as super
+              method! visit_VLoan _ v = VLoan v (* Don't enter inside loans *)
+
+              method! visit_VBorrow _ v =
+                VBorrow v (* Don't enter inside borrows *)
+
+              method! visit_value _ v =
+                if not (value_has_loans_or_borrows ctx v) then VBottom
+                else super#visit_value () v
+            end
+          in
+          let v = visitor#visit_typed_value () v in
+          EBinding (BDummy vid, v) :: env
+    | x :: env -> x :: explore_env env
+  in
+  let ctx = { ctx with env = explore_env ctx.env } in
+  cf ctx
+
+(* Repeat until we can't simplify the context anymore:
+   - explore the fresh anonymous values and replace all the values which are not
+     borrows/loans with ⊥
+   - also end the borrows which appear in fresh anonymous values and don't contain loans
+   - end the fresh region abstractions which can be ended (no loans)
+*)
+let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) :
+    cm_fun =
+ fun cf ctx ->
+  comp
+    (end_useless_fresh_borrows_and_abs config fixed_ids)
+    (cleanup_fresh_values fixed_ids)
+    cf ctx
+
 (** Reorder the loans and borrows in the fresh abstractions.
 
     We do this in order to enforce some structure in the environments: this
@@ -352,6 +467,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
 
   let cf_exit_loop_body (res : statement_eval_res) : m_fun =
    fun ctx ->
+    log#ldebug (lazy "compute_loop_entry_fixed_point: cf_exit_loop_body");
     match res with
     | Return | Panic | Break _ -> None
     | Unit ->
@@ -369,7 +485,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
 
   (* The fixed ids. They are the ids of the original ctx, after we ended
      the borrows/loans which end during the first loop iteration (we do
-     one loop iteration, then set it to [Some].
+     one loop iteration, then set it to [Some]).
   *)
   let fixed_ids : ids_sets option ref = ref None in
 
@@ -377,6 +493,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
      context (the context at the loop entry, after we called
      {!prepare_ashared_loans}, if this is the first iteration) *)
   let join_ctxs (ctx1 : eval_ctx) : eval_ctx =
+    log#ldebug (lazy "compute_loop_entry_fixed_point: join_ctxs");
     (* If this is the first iteration, end the borrows/loans/abs which
        appear in ctx1 and not in the other contexts, then compute the
        set of fixed ids. This means those borrows/loans have to end
@@ -400,6 +517,15 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
             ctx
           in
           (* End the borrows/abs in [ctx1] *)
+          log#ldebug
+            (lazy
+              ("compute_loop_entry_fixed_point: join_ctxs: ending \
+                borrows/abstractions before entering the loop:\n\
+                - ending borrow ids: "
+              ^ BorrowId.Set.to_string None blids
+              ^ "\n- ending abstraction ids: "
+              ^ AbstractionId.Set.to_string None aids
+              ^ "\n\n"));
           let ctx1 = end_borrows_abs blids aids ctx1 in
           (* We can also do the same in the contexts [ctxs]: if there are
              several contexts, maybe one of them ended some borrows and some
@@ -414,12 +540,16 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     in
 
     let fixed_ids = Option.get !fixed_ids in
+
+    (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
       loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx1 !ctxs
     in
     ctxs := [];
     ctx2
   in
+  log#ldebug (lazy "compute_loop_entry_fixed_point: after join_ctxs");
+
   (* Compute the set of fixed ids - for the symbolic ids, we compute the
      intersection of ids between the original environment and the list
      of new environments *)
@@ -440,6 +570,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
      existentially quantified borrows/abstractions/symbolic values.
   *)
   let equiv_ctxs (ctx1 : eval_ctx) (ctx2 : eval_ctx) : bool =
+    log#ldebug (lazy "compute_fixed_point: equiv_ctx:");
     let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
     let lookup_shared_value _ = raise (Failure "Unreachable") in
@@ -531,6 +662,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
     in
     let cf_loop : st_m_fun =
      fun res ctx ->
+      log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop");
       match res with
       | Continue _ | Panic ->
           (* We don't want to generate anything *)
@@ -544,6 +676,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
           *)
           raise (Failure "Unreachable")
       | Return ->
+          log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return");
           (* Should we consume the return value and pop the frame?
            * If we check in [Interpreter] that the loop abstraction we end is
            * indeed the correct one, I think it is sound to under-approximate here
@@ -604,12 +737,24 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
           (* Retrieve the first id of the group *)
           match ids with
           | [] ->
-              (* We shouldn't get there: we actually introduce reborrows with
-                 {!prepare_ashared_loans} and in the [match_mut_borrows] function
-                 of {!MakeJoinMatcher} to introduce some fresh abstractions for
-                 this purpose.
+              (* We *can* get there, if the loop doesn't touch the borrowed
+                 values.
+                 For instance:
+                 {[
+                   pub fn iter_slice(a: &mut [u8]) {
+                       let len = a.len();
+                       let mut i = 0;
+                       while i < len {
+                           i += 1;
+                       }
+                   }
+                 ]}
               *)
-              raise (Failure "Unexpected")
+              log#ldebug
+                (lazy
+                  ("No loop region to end for the region group "
+                  ^ RegionGroupId.to_string rg_id));
+              ()
           | id0 :: ids ->
               let id0 = ref id0 in
               (* Add the proper region group into the abstraction *)
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 65a76359..7c3f6199 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -3,6 +3,18 @@ open Contexts
 open InterpreterUtils
 open InterpreterLoopsCore
 
+(** Repeat until we can't simplify the context anymore:
+   - explore the fresh anonymous values and replace all the values which are not
+     borrows/loans with ⊥
+   - also end the borrows which appear in fresh anonymous values and don't contain loans
+   - end the fresh region abstractions which can be ended (no loans)
+
+   Inputs:
+   - config
+   - fixed ids (the fixeds ids are the ids we consider as non-fresh)
+ *)
+val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun
+
 (** Prepare the shared loans in the abstractions by moving them to fresh
     abstractions.
 
@@ -56,6 +68,8 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun
     - the map from region group id to the corresponding abstraction appearing
       in the fixed point (this is useful to compute the return type of the loop
       backward functions for instance).
+      Note that this is a partial map: the loop doesn't necessarily introduce
+      an abstraction for each input region of the function.
 
     Rem.: the list of symbolic values should be computable by simply exploring
     the fixed point environment and listing all the symbolic values we find.
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 4624a1e9..dd7bd7a7 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -11,6 +11,7 @@ open TypesUtils
 open ValuesUtils
 open Cps
 open InterpreterUtils
+open InterpreterBorrowsCore
 open InterpreterBorrows
 open InterpreterLoopsCore
 module S = SynthesizeSymbolic
@@ -450,8 +451,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       (* No borrows, no loans, no bottoms: we can introduce a symbolic value *)
       mk_fresh_symbolic_typed_value_from_no_regions_ty ty
 
-  let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (ty : ety)
-      (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
+  let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec
+      (ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
+    (* Lookup the shared values and match them - we do this mostly
+       to make sure we end loans which might appear on one side
+       and not on the other. *)
+    let sv0 = lookup_shared_value ctx0 bid0 in
+    let sv1 = lookup_shared_value ctx1 bid1 in
+    let sv = match_rec sv0 sv1 in
     if bid0 = bid1 then bid0
     else
       (* We replace bid0 and bid1 with a fresh borrow id, and introduce
@@ -463,10 +470,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let rid = fresh_region_id () in
       let bid2 = fresh_borrow_id () in
 
-      (* Generate a fresh symbolic value for the shared value *)
+      (* Update the type of the shared loan to use the fresh region *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
-
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
@@ -1376,9 +1381,16 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
       }
     in
     Some maps
-  with Distinct msg ->
-    log#ldebug (lazy ("match_ctxs: distinct: " ^ msg));
-    None
+  with
+  | Distinct msg ->
+      log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n"));
+      None
+  | ValueMatchFailure k ->
+      log#ldebug
+        (lazy
+          ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k
+         ^ "\n"));
+      None
 
 let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (ctx1 : eval_ctx) : bool =
@@ -1388,23 +1400,16 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx)
     (match_ctxs check_equivalent fixed_ids lookup_shared_value
        lookup_shared_value ctx0 ctx1)
 
-let match_ctx_with_target (config : config) (loop_id : LoopId.id)
-    (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
-    (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
-    (src_ctx : eval_ctx) : st_cm_fun =
+let prepare_match_ctx_with_target (config : config) (loop_id : LoopId.id)
+    (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun =
  fun cf tgt_ctx ->
   (* Debug *)
   log#ldebug
     (lazy
-      ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
-     ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
-     ^ eval_ctx_to_string tgt_ctx));
-
-  (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by
-     ending loans for instance - remember that the [src_ctx] is the fixed point
-     context, which results from joins during which we ended the loans which
-     were introduced during the loop iterations)
-  *)
+      ("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: "
+     ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
+     ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx
+      ));
   (* End the loans which lead to mismatches when joining *)
   let rec cf_reorganize_join_tgt : cm_fun =
    fun cf tgt_ctx ->
@@ -1530,6 +1535,29 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
       in
       comp cc cf_reorganize_join_tgt cf tgt_ctx
   in
+  (* Apply the reorganization *)
+  cf_reorganize_join_tgt cf tgt_ctx
+
+let match_ctx_with_target (config : config) (loop_id : LoopId.id)
+    (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
+    (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
+    (src_ctx : eval_ctx) : st_cm_fun =
+ fun cf tgt_ctx ->
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
+     ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+     ^ eval_ctx_to_string tgt_ctx));
+
+  (* We first reorganize [tgt_ctx] so that we can match [src_ctx] with it (by
+     ending loans for instance - remember that the [src_ctx] is the fixed point
+     context, which results from joins during which we ended the loans which
+     were introduced during the loop iterations)
+  *)
+  let cf_reorganize_join_tgt =
+    prepare_match_ctx_with_target config loop_id fixed_ids src_ctx
+  in
 
   (* Introduce the "identity" abstractions for the loop re-entry.
 
@@ -1551,6 +1579,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
   let cf_introduce_loop_fp_abs : m_fun =
    fun tgt_ctx ->
     (* Match the source and target contexts *)
+    log#ldebug
+      (lazy
+        ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: "
+       ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
+       ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+       ^ eval_ctx_to_string tgt_ctx));
+
     let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
     let filt_src_env, new_absl, new_dummyl =
       ctx_split_fixed_new fixed_ids src_ctx
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 5f69b8d3..d6f89ed6 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -137,6 +137,21 @@ val match_ctxs :
  *)
 val ctxs_are_equivalent : ids_sets -> eval_ctx -> eval_ctx -> bool
 
+(** Reorganize a target context so that we can match it with a source context
+    (remember that the source context is generally the fixed point context,
+    which results from joins during which we ended the loans which
+    were introduced during the loop iterations).
+
+   **Parameters**:
+   - [config]
+   - [loop_id]
+   - [fixed_ids]
+   - [src_ctx]
+
+ *)
+val prepare_match_ctx_with_target :
+  config -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
+
 (** Match a context with a target context.
 
     This is used to compute application of loop translations: we use this
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 97c8bcd6..0cf8b88a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -933,6 +933,11 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
    fun ctx ->
+    log#ldebug
+      (lazy
+        ("\neval_statement: cf_eval_st: statement:\n"
+        ^ statement_to_string_with_tab ctx st
+        ^ "\n\n"));
     match st.content with
     | Assign (p, rvalue) -> (
         (* We handle global assignments separately *)
@@ -1520,8 +1525,10 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : config) (body : statement) : st_cm_fun =
  fun cf ctx ->
+  log#ldebug (lazy "eval_function_body:");
   let cc = eval_statement config body in
   let cf_finish cf res =
+    log#ldebug (lazy "eval_function_body: cf_finish");
     (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we
      * delegate the check to the caller. *)
     (* Expand the symbolic values if necessary - we need to do that before
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 0817b111..667c5080 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -420,6 +420,8 @@ let compute_ctxs_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
 let compute_ctx_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
   compute_ctxs_ids [ ctx ]
 
+let empty_ids_set = fst (compute_ctxs_ids [])
+
 (** **WARNING**: this function doesn't compute the normalized types
     (for the trait type aliases). This should be computed afterwards.
  *)
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 8999c77d..0c69bd05 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -16,6 +16,10 @@ module Expressions = Charon.PrintExpressions
 let list_to_string (to_string : 'a -> string) (ls : 'a list) : string =
   "[" ^ String.concat "; " (List.map to_string ls) ^ "]"
 
+let pair_to_string (to_string0 : 'a -> string) (to_string1 : 'b -> string)
+    ((x, y) : 'a * 'b) : string =
+  "(" ^ to_string0 x ^ ", " ^ to_string1 y ^ ")"
+
 let bool_to_string (b : bool) : string = if b then "true" else "false"
 
 (** Pretty-printing for values *)
@@ -88,19 +92,19 @@ module Values = struct
 
   and borrow_content_to_string (env : fmt_env) (bc : borrow_content) : string =
     match bc with
-    | VSharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋"
+    | VSharedBorrow bid -> "shared_borrow@" ^ BorrowId.to_string bid
     | VMutBorrow (bid, tv) ->
-        "&mut@" ^ BorrowId.to_string bid ^ " ("
+        "mut_borrow@" ^ BorrowId.to_string bid ^ " ("
         ^ typed_value_to_string env tv
         ^ ")"
-    | VReservedMutBorrow bid -> "⌊reserved_mut@" ^ BorrowId.to_string bid ^ "⌋"
+    | VReservedMutBorrow bid -> "reserved_borrow@" ^ BorrowId.to_string bid
 
   and loan_content_to_string (env : fmt_env) (lc : loan_content) : string =
     match lc with
     | VSharedLoan (loans, v) ->
         let loans = BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string env v ^ ")"
-    | VMutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋"
+    | VMutLoan bid -> "ml@" ^ BorrowId.to_string bid
 
   let abstract_shared_borrow_to_string (env : fmt_env)
       (abs : abstract_shared_borrow) : string =
@@ -184,9 +188,9 @@ module Values = struct
   and aloan_content_to_string (env : fmt_env) (lc : aloan_content) : string =
     match lc with
     | AMutLoan (bid, av) ->
-        "⌊mut@" ^ BorrowId.to_string bid ^ ", "
+        "@mut_loan(" ^ BorrowId.to_string bid ^ ", "
         ^ typed_avalue_to_string env av
-        ^ "⌋"
+        ^ ")"
     | ASharedLoan (loans, v, av) ->
         let loans = BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", "
@@ -225,10 +229,10 @@ module Values = struct
       =
     match bc with
     | AMutBorrow (bid, av) ->
-        "&mut@" ^ BorrowId.to_string bid ^ " ("
+        "mb@" ^ BorrowId.to_string bid ^ " ("
         ^ typed_avalue_to_string env av
         ^ ")"
-    | ASharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋"
+    | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid
     | AIgnoredMutBorrow (opt_bid, av) ->
         "@ignored_mut_borrow("
         ^ option_to_string BorrowId.to_string opt_bid
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 04bc90d7..1820b86a 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -15,6 +15,14 @@ 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
 
+let var_to_string (ctx : trans_ctx) (v : var) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.var_to_string fmt v
+
+let texpression_to_string (ctx : trans_ctx) (x : texpression) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.texpression_to_string fmt false "" "  " x
+
 (** Small utility.
 
     We sometimes have to insert new fresh variables in a function body, in which
@@ -1890,7 +1898,7 @@ end
 module FunLoopIdMap = Collections.MakeMap (FunLoopIdOrderedType)
 
 (** Filter the useless loop input parameters. *)
-let filter_loop_inputs (transl : pure_fun_translation list) :
+let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
     pure_fun_translation list =
   (* We need to explore groups of mutually recursive functions. In order
      to compute which parameters are useless, we need to explore the
@@ -1910,6 +1918,12 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
   in
   let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in
 
+  log#ldebug
+    (lazy
+      ("filter_loop_inputs: all_decls:\n\n"
+      ^ String.concat "\n\n" (List.map (fun_decl_to_string ctx) all_decls)
+      ^ "\n"));
+
   (* Explore the subgroups one by one.
 
      For now, we only filter the parameters of loop functions which are simply
@@ -1918,16 +1932,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
      Rem.: there is a bit of redundancy in computing the useless parameters
      for the loop forward *and* the loop backward functions.
   *)
-  (* The [filtered] map: maps function identifiers to filtering information.
-
-     Note that we ignore the backward id:
-     - we filter the forward inputs only
-     - we want the filtering to be the same for the forward and the backward
-       functions
-     The reason is that for now we want to preserve the fact that a backward
-     function takes the same inputs as its associated forward function, with
-     additional parameters.
-  *)
+  (* The [filtered] map: maps function identifiers to filtering information. *)
   let used_map = ref FunLoopIdMap.empty in
 
   (* We start by computing the filtering information, for each function *)
@@ -1946,6 +1951,11 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
         (fun v -> (var_get_id v, mk_texpression_from_var v))
         inputs_prefix
     in
+    log#ldebug
+      (lazy
+        ("inputs:\n"
+        ^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
+        ^ "\n"));
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
     assert (Option.is_some decl.loop_id);
 
@@ -1985,6 +1995,12 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
                         let beg_args, end_args =
                           Collections.List.split_at args inputs_prefix_length
                         in
+                        log#ldebug
+                          (lazy
+                            ("beg_args:\n"
+                            ^ String.concat ", "
+                                (List.map (texpression_to_string ctx) beg_args)
+                            ^ "\n"));
                         let used_args = List.combine inputs beg_args in
                         List.iter
                           (fun ((vid, var), arg) ->
@@ -2008,8 +2024,17 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
     in
     visitor#visit_texpression () body.body;
 
+    log#ldebug
+      (lazy
+        ("\n- used variables: "
+        ^ String.concat ", "
+            (List.map
+               (Print.pair_to_string VarId.to_string string_of_bool)
+               !used)
+        ^ "\n"));
+
     (* Save the filtering information, if there is anything to filter *)
-    if List.exists snd !used then
+    if List.exists (fun (_, b) -> not b) !used then
       let used = List.map snd !used in
       let used =
         match FunLoopIdMap.find_opt fun_id !used_map with
@@ -2025,6 +2050,11 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
       | [ f ] ->
           (* Group made of one function: check if it is a loop. If it is the
              case, explore it. *)
+          log#ldebug
+            (lazy
+              ("filter_loop_inputs: singleton:\n\n" ^ fun_decl_to_string ctx f
+             ^ "\n"));
+
           if Option.is_some f.loop_id then compute_one_filter_info f else ()
       | _ ->
           (* Group of mutually recursive functions: ignore for now *)
@@ -2234,4 +2264,4 @@ let apply_passes_to_pure_fun_translations (ctx : trans_ctx)
   (* Filter the useless inputs in the loop functions (loops are initially
      parameterized by *all* the symbolic values in the context, because
      they may access any of them). *)
-  filter_loop_inputs transl
+  filter_loop_inputs ctx transl
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 8e8cdec3..7252a020 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -197,16 +197,16 @@ type expression =
           The evaluation context is the context at the moment we introduce the
           [ForwardEnd], and is used to translate the input values (see the
           comments for the {!Return} variant).
+
+          This case also handles the case where we (re-)enter a loop (once
+          we enter a loop in symbolic mode, we don't get out: the loop is
+          responsible for the end of the function).
        *)
   | Loop of loop  (** Loop *)
   | ReturnWithLoop of loop_id * bool
-      (** End the function with a call to a loop function.
-
-          This encompasses the cases when we synthesize a function body
-          and enter a loop for the first time, or when we synthesize a
-          loop body and reach a [Continue].
-
-          The boolean is [is_continue].
+      (** We reach a return while inside a loop.
+          The boolean is [true].
+          TODO: merge this with Return.
        *)
   | Meta of emeta * expression  (** Meta information *)
 
@@ -215,8 +215,7 @@ and loop = {
   input_svalues : symbolic_value list;  (** The input symbolic values *)
   fresh_svalues : symbolic_value_id_set;
       (** The symbolic values introduced by the loop fixed-point *)
-  rg_to_given_back_tys :
-    ((RegionId.Set.t * ty list) RegionGroupId.Map.t[@opaque]);
+  rg_to_given_back_tys : (ty list RegionGroupId.Map.t[@opaque]);
       (** The map from region group ids to the types of the values given back
           by the corresponding loop abstractions.
        *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2db5f66c..922f0375 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -128,6 +128,7 @@ type loop_info = {
   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.
+          This map is partial.
        *)
   back_funs : texpression option RegionGroupId.Map.t option;
       (** Same as {!call_info.back_funs}.
@@ -329,6 +330,10 @@ let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
   PrintPure.ty_to_string env false ty
 
+let pure_var_to_string (ctx : bs_ctx) (v : var) : string =
+  let env = bs_ctx_to_pure_fmt_env ctx in
+  PrintPure.var_to_string env v
+
 let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
   let env = bs_ctx_to_fmt_env ctx in
   Print.Types.ty_to_string env ty
@@ -1251,41 +1256,56 @@ let mk_back_output_ty_from_effect_info (effect_info : fun_effect_info)
 (** Compute the arrow types for all the backward functions.
 
     If a backward function has no inputs/outputs we filter it.
+
+    We may also filter the region group ids (param [keep_rg_ids]).
+    This is useful for the loops: not all the
+    parent function region groups can be linked to a region abstraction
+    introduced by the loop.
  *)
 let compute_back_tys_with_info (dsg : Pure.decomposed_fun_sig)
+    ?(keep_rg_ids : RegionGroupId.Set.t option = None)
     (subst : (generic_args * trait_instance_id) option) :
     (back_sg_info * ty) option list =
+  let keep_rg_id =
+    match keep_rg_ids with
+    | None -> fun _ -> true
+    | Some ids -> fun id -> RegionGroupId.Set.mem id ids
+  in
   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)
+    (fun ((rg_id, back_sg) : RegionGroupId.id * back_sg_info) ->
+      if keep_rg_id rg_id then
+        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)
+      else (* We ignore this region group *)
+        None)
+    (RegionGroupId.Map.bindings dsg.back_sg)
 
 let compute_back_tys (dsg : Pure.decomposed_fun_sig)
+    ?(keep_rg_ids : RegionGroupId.Set.t option = None)
     (subst : (generic_args * trait_instance_id) option) : ty option list =
-  List.map (Option.map snd) (compute_back_tys_with_info dsg subst)
+  List.map (Option.map snd) (compute_back_tys_with_info dsg ~keep_rg_ids subst)
 
 (** Compute the output type of a function, from a decomposed signature
     (the output type contains the type of the value returned by the forward
@@ -1405,8 +1425,14 @@ let fresh_opt_vars (vars : (string option * ty) option list) (ctx : bs_ctx) :
           (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 =
+(* Introduce variables for the backward functions.
+
+   We may filter the region group ids. This is useful for the loops: not all the
+   parent function region groups can be linked to a region abstraction
+   introduced by the loop.
+*)
+let fresh_back_vars_for_current_fun (ctx : bs_ctx)
+    (keep_rg_ids : RegionGroupId.Set.t option) : 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 =
@@ -1436,7 +1462,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) : bs_ctx * var option list =
         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.combine back_var_names (compute_back_tys ctx.sg ~keep_rg_ids None)
+  in
   let back_vars =
     List.map
       (fun (name, ty) ->
@@ -1858,9 +1886,11 @@ 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) ->
-      (* Remark: we can't get there if we are inside a loop *)
+      (* We reached a return.
+         Remark: we can't get there if we are inside a loop. *)
       translate_return ectx opt_v ctx
   | ReturnWithLoop (loop_id, is_continue) ->
+      (* We reached a return and are inside a loop. *)
       translate_return_with_loop loop_id is_continue ctx
   | Panic -> translate_panic ctx
   | FunCall (call, e) -> translate_function_call call e ctx
@@ -1872,6 +1902,10 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       translate_intro_symbolic ectx p sv v e ctx
   | Meta (meta, e) -> translate_emeta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
+      (* Translate the end of a function, or the end of a loop.
+
+         The case where we (re-)enter a loop is handled here.
+      *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
 
@@ -1988,7 +2022,13 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
         (* Backward *)
         (* Group the variables in which we stored the values we need to give back.
          * See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
-        let backward_outputs = Option.get ctx.backward_outputs in
+        (* It can happen that we did not end any output abstraction, because the
+           loop didn't use borrows corresponding to the region we just ended.
+           If this happens, there are no backward outputs.
+        *)
+        let backward_outputs =
+          match ctx.backward_outputs with Some outputs -> outputs | None -> []
+        in
         let field_values = List.map mk_texpression_from_var backward_outputs in
         mk_simpl_tuple_texpression field_values
   in
@@ -2118,7 +2158,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                    | 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
+                          function. Otherwise, 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 =
@@ -2944,12 +2984,9 @@ and translate_forward_end (ectx : C.eval_ctx)
           (* We are translating the forward function - nothing to do *)
           (ctx, fwd_e, fun e -> e)
       | Some bid ->
-          (* 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
+          (* We need to update the state, and 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
@@ -2994,15 +3031,9 @@ and translate_forward_end (ectx : C.eval_ctx)
     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).
+  (* 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.
@@ -3013,11 +3044,31 @@ and translate_forward_end (ectx : C.eval_ctx)
     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. *)
+    (* If we reached a loop: if we are *inside* a loop, we need to ignore the
+       backward functions which are not associated to region abstractions.
+    *)
+    let keep_rg_ids =
+      match ctx.loop_id with
+      | None -> None
+      | Some loop_id ->
+          if ctx.inside_loop then
+            let loop_info = LoopId.Map.find loop_id ctx.loops in
+            Some
+              (RegionGroupId.Set.of_list
+                 (RegionGroupId.Map.keys loop_info.back_outputs))
+          else None
+    in
+    let keep_rg_id =
+      match keep_rg_ids with
+      | None -> fun _ -> true
+      | Some ids -> fun id -> RegionGroupId.Set.mem id ids
+    in
+
     let back_el =
       List.map
         (fun ((gid, _) : RegionGroupId.id * back_sg_info) ->
-          translate_one_end ctx (Some gid))
+          if keep_rg_id gid then Some (translate_one_end ctx (Some gid))
+          else None)
         (RegionGroupId.Map.bindings ctx.sg.back_sg)
     in
 
@@ -3027,17 +3078,20 @@ and translate_forward_end (ectx : C.eval_ctx)
        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)
+        (fun ((rg_id, sg) : RegionGroupId.id * back_sg_info) ->
+          if keep_rg_id rg_id then
+            Some
+              (if !Config.simplify_merged_fwd_backs then
+                 sg.inputs = [] && sg.effect_info.can_fail
+               else false)
+          else None)
+        (RegionGroupId.Map.bindings 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
+    let _, back_vars = fresh_back_vars_for_current_fun ctx keep_rg_ids in
 
     (* Create the return expressions *)
     let vars =
@@ -3072,7 +3126,9 @@ and translate_forward_end (ectx : C.eval_ctx)
     let back_vars_els =
       List.filter_map
         (fun (v, (eval, el)) ->
-          match v with None -> None | Some v -> Some (v, eval, el))
+          match v with
+          | None -> None
+          | Some v -> Some (v, Option.get eval, Option.get el))
         (List.combine back_vars (List.combine evaluate_backs back_el))
     in
     let e =
@@ -3154,7 +3210,16 @@ and translate_forward_end (ectx : C.eval_ctx)
          backward functions of the outer function.
       *)
       let ctx, back_funs_map, back_funs =
-        let ctx, back_vars = fresh_back_vars_for_current_fun ctx in
+        (* We need to filter the region groups which are not linked to region
+           abstractions appearing in the loop, so as not to introduce unnecessary
+           backward functions. *)
+        let keep_rg_ids =
+          RegionGroupId.Set.of_list
+            (RegionGroupId.Map.keys loop_info.back_outputs)
+        in
+        let ctx, back_vars =
+          fresh_back_vars_for_current_fun ctx (Some keep_rg_ids)
+        in
         let back_funs =
           List.filter_map
             (fun v ->
@@ -3266,10 +3331,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl
         ^ "\n- rg_to_abs\n:"
         ^ T.RegionGroupId.Map.show
-            (fun (rids, tys) ->
-              "(" ^ T.RegionId.Set.show rids ^ ", "
-              ^ Print.list_to_string (ty_to_string ctx) tys
-              ^ ")")
+            (Print.list_to_string (ty_to_string ctx))
             loop.rg_to_given_back_tys
         ^ "\n"));
     let ctx, _ = fresh_vars_for_symbolic_values svl ctx in
@@ -3297,7 +3359,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let ctx = ref ctx in
   let rg_to_given_back_tys =
     RegionGroupId.Map.map
-      (fun (_, tys) ->
+      (fun tys ->
         (* The types shouldn't contain borrows - we can translate them as forward types *)
         List.map
           (fun ty ->
@@ -3313,11 +3375,24 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let back_effect_infos, output_ty =
     (* 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
+    log#ldebug
+      (lazy
+        (let back_sgs = RegionGroupId.Map.bindings ctx.sg.back_sg in
+         "translate_loop:" ^ "\n- back_sgs: "
+         ^ (Print.list_to_string
+              (Print.pair_to_string RegionGroupId.to_string show_back_sg_info))
+             back_sgs
+         ^ "\n- given_back_tys: "
+         ^ (RegionGroupId.Map.to_string None
+              (Print.list_to_string (pure_ty_to_string ctx)))
+             rg_to_given_back_tys
+         ^ "\n"));
     let back_info_tys =
       List.map
-        (fun (((id, back_sg), given_back) : (_ * back_sg_info) * ty list) ->
+        (fun ((rg_id, given_back) : RegionGroupId.id * ty list) ->
+          (* Lookup the effect information about the parent function region group
+             associated to this loop region abstraction *)
+          let back_sg = RegionGroupId.Map.find rg_id ctx.sg.back_sg in
           (* 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
@@ -3342,8 +3417,8 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
               let ty = mk_arrows inputs output in
               Some ty
           in
-          ((id, effect_info), ty))
-        (List.combine back_sgs given_back_tys)
+          ((rg_id, effect_info), ty))
+        (RegionGroupId.Map.bindings rg_to_given_back_tys)
     in
     let back_info = List.map fst back_info_tys in
     let back_info = RegionGroupId.Map.of_list back_info in
@@ -3445,9 +3520,6 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         loop_body;
       }
   in
-  (* If we translate forward functions: the return type of a loop body is the
-     same as the parent function *)
-  assert (Option.is_some ctx.bid || fun_end.ty = loop_body.ty);
   let ty = fun_end.ty in
   { e = loop; ty }
 
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 865185a8..20bc107e 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -171,7 +171,7 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx)
 
 let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
     (fresh_svalues : SymbolicValueId.Set.t)
-    (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t)
+    (rg_to_given_back_tys : ty list RegionGroupId.Map.t)
     (end_expr : expression option) (loop_expr : expression option)
     (meta : Meta.meta) : expression option =
   match (end_expr, loop_expr) with
diff --git a/flake.lock b/flake.lock
index b5b7bc3c..b9382775 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1707489322,
-        "narHash": "sha256-fnb4vyW3BxC4+ue4aLxIM0a5WmNdgdpdkSvwir8Zens=",
+        "lastModified": 1709941742,
+        "narHash": "sha256-iSi3HQBac+JSACClXRJBooQbPOtyqA/P//WzwLQH+tQ=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "89cecf5d1074fae7e8007be7f6cdf2f38e9782b1",
+        "rev": "c1b3f94afb32ae0917a2abd09f0c6f8e31bed9d6",
         "type": "github"
       },
       "original": {
@@ -82,11 +82,11 @@
         "systems": "systems_3"
       },
       "locked": {
-        "lastModified": 1705309234,
-        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
+        "lastModified": 1709126324,
+        "narHash": "sha256-q6EQdSeUZOG26WelxqkmR7kArjgWCdw5sfJVHPH/7j8=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
+        "rev": "d465f4819400de7c8d874d50b982301f28a84605",
         "type": "github"
       },
       "original": {
@@ -131,11 +131,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1707271955,
-        "narHash": "sha256-OgPXUBx+sVwiENg4tH3GkdAvX+E67djqE/bTfjqPygU=",
+        "lastModified": 1708956704,
+        "narHash": "sha256-xT0V7oQwR0Zns9g/MvV30ILlAX6tcp92SqWPwej1+sI=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "531185028c4add6ff183ca119ca8415cc2b375db",
+        "rev": "a48722f90e14be69b850f093b41fbbdfee7f6eb9",
         "type": "github"
       },
       "original": {
@@ -164,11 +164,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1707239346,
-        "narHash": "sha256-fCLBOwHv2RqWcDzCqpVzIS1Au5CnfvEqbKHyNUzDEwk=",
+        "lastModified": 1709029146,
+        "narHash": "sha256-xKqBQ1OdLnyng4Kl3XRU//borVLLet+h15mPQ5g0BEI=",
         "owner": "hacl-star",
         "repo": "hacl-star",
-        "rev": "9666f11923844fcdbca6a7af4b4b94fa47b5bb88",
+        "rev": "59723f7dde13bd7b7eb90491f1385b4e3ee2904f",
         "type": "github"
       },
       "original": {
@@ -194,11 +194,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1707354605,
-        "narHash": "sha256-ogIf8OwaCkZCFx3Niayd/zh2LTjNJrRDA6XuY11EqBg=",
+        "lastModified": 1709552015,
+        "narHash": "sha256-zwYbXYRAqKee+OtlWaSX3EhUyD5JLN+xxzcqYxyDnSI=",
         "owner": "hacl-star",
         "repo": "hacl-nix",
-        "rev": "e46ef04ad5120b35bc99eca3c77e039f8ca30a6f",
+        "rev": "96a3c4eaaa65beb0ac9e57fc9aa3e9e34aca12f5",
         "type": "github"
       },
       "original": {
@@ -223,11 +223,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1707198961,
-        "narHash": "sha256-HnOVG+lqfxTJnV+Dmi/UsHfHguWg7WgcC+k5qbBfYxw=",
+        "lastModified": 1709551385,
+        "narHash": "sha256-aryyJy49PlkZeIMO8Jg0qAUCjtre0r+rvmbH6OhH/sk=",
         "owner": "fstarlang",
         "repo": "karamel",
-        "rev": "da1e941b2fcb196aa5d1e34941aa00b4c67ac321",
+        "rev": "a1e1b1f2493ac24f8729f17ebedba7c4571f7c97",
         "type": "github"
       },
       "original": {
@@ -265,11 +265,11 @@
         "nixpkgs": "nixpkgs_4"
       },
       "locked": {
-        "lastModified": 1707482772,
-        "narHash": "sha256-sewRgw1MhmoFJO33rDOyz5KH0CGWEnQmwns4uRkmF0U=",
+        "lastModified": 1709930258,
+        "narHash": "sha256-0oJSuzf3zSRMbfmtZ789sJqhg+pgbBZWo9mATpe/dsE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "488bfe2128a1c5ff0e96c45cf6a382655dc7c703",
+        "rev": "b39042b32c00b6455153f9df26153680b2dc6d6f",
         "type": "github"
       },
       "original": {
@@ -318,11 +318,11 @@
         "nixpkgs": "nixpkgs_7"
       },
       "locked": {
-        "lastModified": 1707482772,
-        "narHash": "sha256-sewRgw1MhmoFJO33rDOyz5KH0CGWEnQmwns4uRkmF0U=",
+        "lastModified": 1709930258,
+        "narHash": "sha256-0oJSuzf3zSRMbfmtZ789sJqhg+pgbBZWo9mATpe/dsE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "488bfe2128a1c5ff0e96c45cf6a382655dc7c703",
+        "rev": "b39042b32c00b6455153f9df26153680b2dc6d6f",
         "type": "github"
       },
       "original": {
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 3a6fb02f..79be3678 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -516,4 +516,73 @@ Definition ite : result unit :=
   Return tt
 .
 
+(** [arrays::zero_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 303:0-310:1 *)
+Fixpoint zero_slice_loop
+  (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s< len
+    then (
+      p <- slice_index_mut_usize u8 a i;
+      let (_, index_mut_back) := p in
+      i1 <- usize_add i 1%usize;
+      a1 <- index_mut_back 0%u8;
+      zero_slice_loop n1 a1 i1 len)
+    else Return a
+  end
+.
+
+(** [arrays::zero_slice]:
+    Source: 'src/arrays.rs', lines 303:0-303:31 *)
+Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
+  let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+.
+
+(** [arrays::iter_mut_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 312:0-318:1 *)
+Fixpoint iter_mut_slice_loop
+  (n : nat) (len : usize) (i : usize) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s< len
+    then (
+      i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+    else Return tt
+  end
+.
+
+(** [arrays::iter_mut_slice]:
+    Source: 'src/arrays.rs', lines 312:0-312:35 *)
+Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
+  let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a
+.
+
+(** [arrays::sum_mut_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 320:0-328:1 *)
+Fixpoint sum_mut_slice_loop
+  (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    let i1 := slice_len u32 a in
+    if i s< i1
+    then (
+      i2 <- slice_index_usize u32 a i;
+      s1 <- u32_add s i2;
+      i3 <- usize_add i 1%usize;
+      sum_mut_slice_loop n1 a i3 s1)
+    else Return s
+  end
+.
+
+(** [arrays::sum_mut_slice]:
+    Source: 'src/arrays.rs', lines 320:0-320:42 *)
+Definition sum_mut_slice
+  (n : nat) (a : slice u32) : result (u32 * (slice u32)) :=
+  i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a)
+.
+
 End Arrays.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8260db02..e235b60d 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge
   Return (p1, back_'a)
 .
 
+(** [loops::ignore_input_mut_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 345:0-349:1 *)
+Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s> 0%u32
+    then (
+      i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+    else Return tt
+  end
+.
+
+(** [loops::ignore_input_mut_borrow]:
+    Source: 'src/loops.rs', lines 345:0-345:56 *)
+Definition ignore_input_mut_borrow
+  (n : nat) (_a : u32) (i : u32) : result u32 :=
+  _ <- ignore_input_mut_borrow_loop n i; Return _a
+.
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 353:0-358:1 *)
+Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s> 0%u32
+    then (
+      i1 <- u32_sub i 1%u32;
+      _ <- incr_ignore_input_mut_borrow_loop n1 i1;
+      Return tt)
+    else Return tt
+  end
+.
+
+(** [loops::incr_ignore_input_mut_borrow]:
+    Source: 'src/loops.rs', lines 353:0-353:60 *)
+Definition incr_ignore_input_mut_borrow
+  (n : nat) (a : u32) (i : u32) : result u32 :=
+  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+.
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 362:0-366:1 *)
+Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s> 0%u32
+    then (
+      i1 <- u32_sub i 1%u32;
+      _ <- ignore_input_shared_borrow_loop n1 i1;
+      Return tt)
+    else Return tt
+  end
+.
+
+(** [loops::ignore_input_shared_borrow]:
+    Source: 'src/loops.rs', lines 362:0-362:59 *)
+Definition ignore_input_shared_borrow
+  (n : nat) (_a : u32) (i : u32) : result u32 :=
+  _ <- ignore_input_shared_borrow_loop n i; Return _a
+.
+
 End Loops.
diff --git a/tests/fstar/arrays/Arrays.Clauses.Template.fst b/tests/fstar/arrays/Arrays.Clauses.Template.fst
index 8cc32583..89654992 100644
--- a/tests/fstar/arrays/Arrays.Clauses.Template.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.Template.fst
@@ -19,3 +19,20 @@ let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
   (i : usize) : nat =
   admit ()
 
+(** [arrays::zero_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 303:0-310:1 *)
+unfold
+let zero_slice_loop_decreases (a : slice u8) (i : usize) (len : usize) : nat =
+  admit ()
+
+(** [arrays::iter_mut_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 312:0-318:1 *)
+unfold
+let iter_mut_slice_loop_decreases (len : usize) (i : usize) : nat = admit ()
+
+(** [arrays::sum_mut_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 320:0-328:1 *)
+unfold
+let sum_mut_slice_loop_decreases (a : slice u32) (i : usize) (s : u32) : nat =
+  admit ()
+
diff --git a/tests/fstar/arrays/Arrays.Clauses.fst b/tests/fstar/arrays/Arrays.Clauses.fst
index aca328c2..f314eabf 100644
--- a/tests/fstar/arrays/Arrays.Clauses.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.fst
@@ -17,3 +17,21 @@ let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
   (i : usize) : nat =
   if i < length s then length s - i else 0
 
+(** [arrays::zero_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 303:0-310:1 *)
+unfold
+let zero_slice_loop_decreases (a : slice u8) (i : usize) (len : usize) : nat =
+  if i < len then len - i else 0
+
+(** [arrays::iter_mut_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 312:0-318:1 *)
+unfold
+let iter_mut_slice_loop_decreases (len : usize) (i : usize) : nat =
+  if i < len then len - i else 0
+
+(** [arrays::sum_mut_slice]: decreases clause
+    Source: 'src/arrays.rs', lines 320:0-328:1 *)
+unfold
+let sum_mut_slice_loop_decreases (a : slice u32) (i : usize) (s : u32) : nat =
+  if i < slice_len u32 a then slice_len u32 a - i else 0
+
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index b0df7fc2..ac57b8fc 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -418,3 +418,58 @@ let ite : result unit =
   let* _ = to_slice_mut_back s1 in
   Return ()
 
+(** [arrays::zero_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 303:0-310:1 *)
+let rec zero_slice_loop
+  (a : slice u8) (i : usize) (len : usize) :
+  Tot (result (slice u8)) (decreases (zero_slice_loop_decreases a i len))
+  =
+  if i < len
+  then
+    let* (_, index_mut_back) = slice_index_mut_usize u8 a i in
+    let* i1 = usize_add i 1 in
+    let* a1 = index_mut_back 0 in
+    zero_slice_loop a1 i1 len
+  else Return a
+
+(** [arrays::zero_slice]:
+    Source: 'src/arrays.rs', lines 303:0-303:31 *)
+let zero_slice (a : slice u8) : result (slice u8) =
+  let len = slice_len u8 a in zero_slice_loop a 0 len
+
+(** [arrays::iter_mut_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 312:0-318:1 *)
+let rec iter_mut_slice_loop
+  (len : usize) (i : usize) :
+  Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i))
+  =
+  if i < len
+  then
+    let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return ()
+  else Return ()
+
+(** [arrays::iter_mut_slice]:
+    Source: 'src/arrays.rs', lines 312:0-312:35 *)
+let iter_mut_slice (a : slice u8) : result (slice u8) =
+  let len = slice_len u8 a in let* _ = iter_mut_slice_loop len 0 in Return a
+
+(** [arrays::sum_mut_slice]: loop 0:
+    Source: 'src/arrays.rs', lines 320:0-328:1 *)
+let rec sum_mut_slice_loop
+  (a : slice u32) (i : usize) (s : u32) :
+  Tot (result u32) (decreases (sum_mut_slice_loop_decreases a i s))
+  =
+  let i1 = slice_len u32 a in
+  if i < i1
+  then
+    let* i2 = slice_index_usize u32 a i in
+    let* s1 = u32_add s i2 in
+    let* i3 = usize_add i 1 in
+    sum_mut_slice_loop a i3 s1
+  else Return s
+
+(** [arrays::sum_mut_slice]:
+    Source: 'src/arrays.rs', lines 320:0-320:42 *)
+let sum_mut_slice (a : slice u32) : result (u32 & (slice u32)) =
+  let* i = sum_mut_slice_loop a 0 0 in Return (i, a)
+
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 244761d3..c8ed16f4 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -136,3 +136,16 @@ let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0)
   (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
+(** [loops::ignore_input_mut_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 345:0-349:1 *)
+unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
+
+(** [loops::incr_ignore_input_mut_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 353:0-358:1 *)
+unfold
+let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
+
+(** [loops::ignore_input_shared_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 362:0-366:1 *)
+unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 13f5513d..7d3c3ae6 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -110,3 +110,17 @@ unfold
 let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
+
+(** [loops::ignore_input_mut_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 345:0-349:1 *)
+unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i
+
+(** [loops::incr_ignore_input_mut_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 353:0-358:1 *)
+unfold
+let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i
+
+(** [loops::ignore_input_shared_borrow]: decreases clause
+    Source: 'src/loops.rs', lines 362:0-366:1 *)
+unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = i
+
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 209c48cd..5f24fe7a 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -548,3 +548,59 @@ let list_nth_shared_mut_loop_pair_merge
   let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in
   Return (p, back_'a)
 
+(** [loops::ignore_input_mut_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 345:0-349:1 *)
+let rec ignore_input_mut_borrow_loop
+  (i : u32) :
+  Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
+  =
+  if i > 0
+  then
+    let* i1 = u32_sub i 1 in
+    let* _ = ignore_input_mut_borrow_loop i1 in
+    Return ()
+  else Return ()
+
+(** [loops::ignore_input_mut_borrow]:
+    Source: 'src/loops.rs', lines 345:0-345:56 *)
+let ignore_input_mut_borrow (_a : u32) (i : u32) : result u32 =
+  let* _ = ignore_input_mut_borrow_loop i in Return _a
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 353:0-358:1 *)
+let rec incr_ignore_input_mut_borrow_loop
+  (i : u32) :
+  Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
+  =
+  if i > 0
+  then
+    let* i1 = u32_sub i 1 in
+    let* _ = incr_ignore_input_mut_borrow_loop i1 in
+    Return ()
+  else Return ()
+
+(** [loops::incr_ignore_input_mut_borrow]:
+    Source: 'src/loops.rs', lines 353:0-353:60 *)
+let incr_ignore_input_mut_borrow (a : u32) (i : u32) : result u32 =
+  let* a1 = u32_add a 1 in
+  let* _ = incr_ignore_input_mut_borrow_loop i in
+  Return a1
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+    Source: 'src/loops.rs', lines 362:0-366:1 *)
+let rec ignore_input_shared_borrow_loop
+  (i : u32) :
+  Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
+  =
+  if i > 0
+  then
+    let* i1 = u32_sub i 1 in
+    let* _ = ignore_input_shared_borrow_loop i1 in
+    Return ()
+  else Return ()
+
+(** [loops::ignore_input_shared_borrow]:
+    Source: 'src/loops.rs', lines 362:0-362:59 *)
+let ignore_input_shared_borrow (_a : u32) (i : u32) : result u32 =
+  let* _ = ignore_input_shared_borrow_loop i in Return _a
+
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d2bb7cf2..59458393 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -473,4 +473,63 @@ def ite : Result Unit :=
   let _ ← to_slice_mut_back s1
   Result.ret ()
 
+/- [arrays::zero_slice]: loop 0:
+   Source: 'src/arrays.rs', lines 303:0-310:1 -/
+divergent def zero_slice_loop
+  (a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
+  if i < len
+  then
+    do
+    let (_, index_mut_back) ← Slice.index_mut_usize U8 a i
+    let i1 ← i + 1#usize
+    let a1 ← index_mut_back 0#u8
+    zero_slice_loop a1 i1 len
+  else Result.ret a
+
+/- [arrays::zero_slice]:
+   Source: 'src/arrays.rs', lines 303:0-303:31 -/
+def zero_slice (a : Slice U8) : Result (Slice U8) :=
+  let len := Slice.len U8 a
+  zero_slice_loop a 0#usize len
+
+/- [arrays::iter_mut_slice]: loop 0:
+   Source: 'src/arrays.rs', lines 312:0-318:1 -/
+divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
+  if i < len
+  then
+    do
+    let i1 ← i + 1#usize
+    let _ ← iter_mut_slice_loop len i1
+    Result.ret ()
+  else Result.ret ()
+
+/- [arrays::iter_mut_slice]:
+   Source: 'src/arrays.rs', lines 312:0-312:35 -/
+def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
+  do
+  let len := Slice.len U8 a
+  let _ ← iter_mut_slice_loop len 0#usize
+  Result.ret a
+
+/- [arrays::sum_mut_slice]: loop 0:
+   Source: 'src/arrays.rs', lines 320:0-328:1 -/
+divergent def sum_mut_slice_loop
+  (a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
+  let i1 := Slice.len U32 a
+  if i < i1
+  then
+    do
+    let i2 ← Slice.index_usize U32 a i
+    let s1 ← s + i2
+    let i3 ← i + 1#usize
+    sum_mut_slice_loop a i3 s1
+  else Result.ret s
+
+/- [arrays::sum_mut_slice]:
+   Source: 'src/arrays.rs', lines 320:0-320:42 -/
+def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
+  do
+  let i ← sum_mut_slice_loop a 0#usize 0#u32
+  Result.ret (i, a)
+
 end arrays
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index f8e1a8cc..433ca8f0 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -557,4 +557,59 @@ def list_nth_shared_mut_loop_pair_merge
   let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
   Result.ret (p, back_'a)
 
+/- [loops::ignore_input_mut_borrow]: loop 0:
+   Source: 'src/loops.rs', lines 345:0-349:1 -/
+divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
+  if i > 0#u32
+  then
+    do
+    let i1 ← i - 1#u32
+    let _ ← ignore_input_mut_borrow_loop i1
+    Result.ret ()
+  else Result.ret ()
+
+/- [loops::ignore_input_mut_borrow]:
+   Source: 'src/loops.rs', lines 345:0-345:56 -/
+def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
+  do
+  let _ ← ignore_input_mut_borrow_loop i
+  Result.ret _a
+
+/- [loops::incr_ignore_input_mut_borrow]: loop 0:
+   Source: 'src/loops.rs', lines 353:0-358:1 -/
+divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
+  if i > 0#u32
+  then
+    do
+    let i1 ← i - 1#u32
+    let _ ← incr_ignore_input_mut_borrow_loop i1
+    Result.ret ()
+  else Result.ret ()
+
+/- [loops::incr_ignore_input_mut_borrow]:
+   Source: 'src/loops.rs', lines 353:0-353:60 -/
+def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
+  do
+  let a1 ← a + 1#u32
+  let _ ← incr_ignore_input_mut_borrow_loop i
+  Result.ret a1
+
+/- [loops::ignore_input_shared_borrow]: loop 0:
+   Source: 'src/loops.rs', lines 362:0-366:1 -/
+divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
+  if i > 0#u32
+  then
+    do
+    let i1 ← i - 1#u32
+    let _ ← ignore_input_shared_borrow_loop i1
+    Result.ret ()
+  else Result.ret ()
+
+/- [loops::ignore_input_shared_borrow]:
+   Source: 'src/loops.rs', lines 362:0-362:59 -/
+def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
+  do
+  let _ ← ignore_input_shared_borrow_loop i
+  Result.ret _a
+
 end loops