Remove the meta-value field from AMutBorrow

10 files changed, 144 insertions, 136 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 42fd0122..f870659a 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -143,22 +143,24 @@ let () =
    * command-line arguments *)
   (* By setting a level for the main_logger_handler, we filter everything *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  main_log#set_level EL.Info;
-  llbc_of_json_logger#set_level EL.Info;
-  pre_passes_log#set_level EL.Info;
-  interpreter_log#set_level EL.Info;
-  statements_log#set_level EL.Info;
-  paths_log#set_level EL.Info;
-  expressions_log#set_level EL.Info;
-  expansion_log#set_level EL.Info;
-  projectors_log#set_level EL.Info;
-  borrows_log#set_level EL.Info;
-  invariants_log#set_level EL.Info;
-  pure_utils_log#set_level EL.Info;
-  symbolic_to_pure_log#set_level EL.Info;
-  pure_micro_passes_log#set_level EL.Info;
-  pure_to_extract_log#set_level EL.Info;
-  translate_log#set_level EL.Info;
+  let level = EL.Info in
+  main_log#set_level level;
+  llbc_of_json_logger#set_level level;
+  pre_passes_log#set_level level;
+  interpreter_log#set_level level;
+  statements_log#set_level level;
+  loops_log#set_level level;
+  paths_log#set_level level;
+  expressions_log#set_level level;
+  expansion_log#set_level level;
+  projectors_log#set_level level;
+  borrows_log#set_level level;
+  invariants_log#set_level level;
+  pure_utils_log#set_level level;
+  symbolic_to_pure_log#set_level level;
+  pure_micro_passes_log#set_level level;
+  pure_to_extract_log#set_level level;
+  translate_log#set_level level;
   let log = main_log in
 
   (* Load the module *)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index c71abe25..ab3fb7ea 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -34,13 +34,18 @@ let log = L.borrows_log
 *)
 let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
     (allow_inner_loans : bool) (l : V.BorrowId.id) (ctx : C.eval_ctx) :
-    (C.eval_ctx * g_borrow_content option, priority_borrows_or_abs) result =
+    ( C.eval_ctx * (V.AbstractionId.id option * g_borrow_content) option,
+      priority_borrows_or_abs )
+    result =
   (* We use a reference to communicate the kind of borrow we found, if we
    * find one *)
-  let replaced_bc : g_borrow_content option ref = ref None in
-  let set_replaced_bc (bc : g_borrow_content) =
+  let replaced_bc : (V.AbstractionId.id option * g_borrow_content) option ref =
+    ref None
+  in
+  let set_replaced_bc (abs_id : V.AbstractionId.id option)
+      (bc : g_borrow_content) =
     assert (Option.is_none !replaced_bc);
-    replaced_bc := Some bc
+    replaced_bc := Some (abs_id, bc)
   in
   (* Raise an exception if:
    * - there are outer borrows
@@ -104,7 +109,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
               (* Check if there are outer borrows or if we are inside an abstraction *)
               raise_if_priority outer None;
               (* Register the update *)
-              set_replaced_bc (Concrete bc);
+              set_replaced_bc (fst outer) (Concrete bc);
               (* Update the value *)
               V.Bottom)
             else super#visit_Borrow outer bc
@@ -114,7 +119,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
               (* Check if there are outer borrows or if we are inside an abstraction *)
               raise_if_priority outer (Some bv);
               (* Register the update *)
-              set_replaced_bc (Concrete bc);
+              set_replaced_bc (fst outer) (Concrete bc);
               (* Update the value *)
               V.Bottom)
             else
@@ -155,7 +160,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
 
       method! visit_ABorrow outer bc =
         match bc with
-        | V.AMutBorrow (_, bid, _) ->
+        | V.AMutBorrow (bid, _) ->
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
               (* When ending a mut borrow, there are two cases:
@@ -170,7 +175,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * abstraction *)
               raise_if_priority outer None;
               (* Register the update *)
-              set_replaced_bc (Abstract bc);
+              set_replaced_bc (fst outer) (Abstract bc);
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above.
                * Also note that, as we are moving the borrowed value inside the
@@ -188,7 +193,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * abstraction *)
               raise_if_priority outer None;
               (* Register the update *)
-              set_replaced_bc (Abstract bc);
+              set_replaced_bc (fst outer) (Abstract bc);
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above *)
               V.ABottom)
@@ -207,7 +212,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * abstraction *)
               raise_if_priority outer None;
               (* Register the update *)
-              set_replaced_bc (Abstract bc);
+              set_replaced_bc (fst outer) (Abstract bc);
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above *)
               let asb = remove_borrow_from_asb l asb in
@@ -498,7 +503,7 @@ let give_back_symbolic_value (_config : C.config)
     to convert the {!V.avalue} to a {!type:V.value} by introducing the proper symbolic values.
  *)
 let give_back_avalue_to_same_abstraction (_config : C.config)
-    (bid : V.BorrowId.id) (mv : V.mvalue) (nv : V.typed_avalue)
+    (bid : V.BorrowId.id) (nv : V.typed_avalue) (nsv : V.typed_value)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
@@ -513,7 +518,11 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
       (** This is a bit annoying, but as we need the type of the avalue we
           are exploring, in order to be able to project the value we give
           back, we need to reimplement {!visit_typed_avalue} instead of
-          {!visit_ALoan} *)
+          {!visit_ALoan}.
+
+          TODO: it is possible to do this by remembering the type of the last
+          typed avalue we entered.
+       *)
       method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
           =
         match av.V.value with
@@ -523,7 +532,11 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
         | _ -> super#visit_typed_avalue opt_abs av
 
       (** We are not specializing an already existing method, but adding a
-          new method (for projections, we need type information) *)
+          new method (for projections, we need type information).
+
+          TODO: it is possible to do this by remembering the type of the last
+          typed avalue we entered.
+        *)
       method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
           (lc : V.aloan_content) : V.avalue =
         match lc with
@@ -548,7 +561,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
               (* Return the new value *)
               V.ALoan
                 (V.AEndedMutLoan
-                   { given_back = nv; child; given_back_meta = mv }))
+                   { given_back = nv; child; given_back_meta = nsv }))
             else (* Continue exploring *)
               super#visit_ALoan opt_abs lc
         | V.ASharedLoan (_, _, _)
@@ -569,7 +582,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
               assert (nv.V.ty = ty);
               V.ALoan
                 (V.AEndedIgnoredMutLoan
-                   { given_back = nv; child; given_back_meta = mv }))
+                   { given_back = nv; child; given_back_meta = nsv }))
             else super#visit_ALoan opt_abs lc
         | V.AEndedIgnoredMutLoan
             { given_back = _; child = _; given_back_meta = _ }
@@ -713,9 +726,52 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
   assert !r;
   { ctx with env }
 
-(** Auxiliary function: see {!end_borrow_aux} *)
-let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+(** Convert an {!type:V.avalue} to a {!type:V.value}.
+
+    This function is used when ending abstractions: whenever we end a borrow
+    in an abstraction, we converted the borrowed {!V.avalue} to a fresh symbolic
+    {!type:V.value}, then give back this {!type:V.value} to the context.
+
+    Note that some regions may have ended in the symbolic value we generate.
+    For instance, consider the following function signature:
+    {[
+      fn f<'a>(x : &'a mut &'a mut u32);
+    ]}
+    When ending the abstraction, the value given back for the outer borrow
+    should be ⊥. In practice, we will give back a symbolic value which can't
+    be expanded (because expanding this symbolic value would require expanding
+    a reference whose region has already ended).
+ *)
+let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
+    (av : V.typed_avalue) : V.symbolic_value =
+  let sv_kind =
+    match abs_kind with
+    | V.FunCall _ -> V.FunCallGivenBack
+    | V.SynthRet _ -> V.SynthRetGivenBack
+    | V.SynthInput _ -> V.SynthInputGivenBack
+    | V.Loop _ -> V.LoopGivenBack
+  in
+  mk_fresh_symbolic_value sv_kind av.V.ty
+
+(** Auxiliary function: see {!end_borrow_aux}.
+
+    When we end a mutable borrow, we need to "give back" the value it contained
+    to its original owner by reinserting it at the proper position.
+
+    Rem.: this function is used when we end *one single* borrow (we don't
+    end this borrow as member of the group of borrows belonging to an
+    abstraction).
+    If the borrow is an "abstract" borrow, it means we are ending a borrow
+    inside an abstraction (we end a borrow whose corresponding loan is in
+    the same abstraction - we are allowed to do so without ending the whole
+    abstraction).
+    TODO: we should not treat this case here, and should only consider internal
+    borrows. This kind of internal reshuffling. should be similar to ending
+    abstractions (it is tantamount to ending *sub*-abstractions).
+ *)
+let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option)
+    (l : V.BorrowId.id) (bc : g_borrow_content) (ctx : C.eval_ctx) : C.eval_ctx
+    =
   (* Debug *)
   log#ldebug
     (lazy
@@ -746,13 +802,23 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
       give_back_shared config l ctx
-  | Abstract (V.AMutBorrow (mv, l', av)) ->
+  | Abstract (V.AMutBorrow (l', av)) ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Convert the avalue to a (fresh symbolic) value.
+
+         Rem.: we shouldn't do this here. We should do this in a function
+         which takes care of ending *sub*-abstractions.
+      *)
+      let abs_id = Option.get abs_id_opt in
+      let abs = C.ctx_lookup_abs ctx abs_id in
+      let sv = convert_avalue_to_given_back_value abs.kind av in
       (* Update the context *)
-      give_back_avalue_to_same_abstraction config l mv av ctx
+      give_back_avalue_to_same_abstraction config l av
+        (mk_typed_value_from_symbolic_value sv)
+        ctx
   | Abstract (V.ASharedBorrow l') ->
       (* Sanity check *)
       assert (l' = l);
@@ -770,33 +836,6 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       | V.AEndedSharedBorrow ) ->
       raise (Failure "Unreachable")
 
-(** Convert an {!type:V.avalue} to a {!type:V.value}.
-
-    This function is used when ending abstractions: whenever we end a borrow
-    in an abstraction, we converted the borrowed {!V.avalue} to a fresh symbolic
-    {!type:V.value}, then give back this {!type:V.value} to the context.
- 
-    Note that some regions may have ended in the symbolic value we generate.
-    For instance, consider the following function signature:
-    {[
-      fn f<'a>(x : &'a mut &'a mut u32);
-    ]}
-    When ending the abstraction, the value given back for the outer borrow
-    should be ⊥. In practice, we will give back a symbolic value which can't
-    be expanded (because expanding this symbolic value would require expanding
-    a reference whose region has already ended).
- *)
-let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
-    (av : V.typed_avalue) : V.symbolic_value =
-  let sv_kind =
-    match abs_kind with
-    | V.FunCall _ -> V.FunCallGivenBack
-    | V.SynthRet _ -> V.SynthRetGivenBack
-    | V.SynthInput _ -> V.SynthInputGivenBack
-    | V.Loop _ -> V.LoopGivenBack
-  in
-  mk_fresh_symbolic_value sv_kind av.V.ty
-
 let check_borrow_disappeared (fun_name : string) (l : V.BorrowId.id)
     (ctx0 : C.eval_ctx) : cm_fun =
   let check_disappeared (ctx : C.eval_ctx) : unit =
@@ -921,14 +960,14 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
       cf_check cf ctx
   (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
      the corresponding loan) *)
-  | Ok (ctx, Some bc) ->
+  | Ok (ctx, Some (abs_id_opt, bc)) ->
       (* Sanity check: the borrowed value shouldn't contain loans *)
       (match bc with
       | Concrete (V.MutBorrow (_, bv)) ->
           assert (Option.is_none (get_first_loan_in_value bv))
       | _ -> ());
       (* Give back the value *)
-      let ctx = give_back config l bc ctx in
+      let ctx = give_back config abs_id_opt l bc ctx in
       (* Do a sanity check and continue *)
       cf_check cf ctx
 
@@ -1087,7 +1126,11 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
   (* We explore in-depth and use exceptions. When exploring a borrow, if
    * the exploration didn't trigger an exception, it means there are no
    * inner borrows to end: we can thus trigger an exception for the current
-   * borrow. *)
+   * borrow.
+   *
+   * TODO: there should be a function in InterpreterBorrowsCore which does just
+   * that.
+   *)
   let obj =
     object
       inherit [_] V.iter_abs as super
@@ -1098,7 +1141,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         (* No exception was raise: we can raise an exception for the
          * current borrow *)
         match bc with
-        | V.AMutBorrow (_, _, _) | V.ASharedBorrow _ ->
+        | V.AMutBorrow _ | V.ASharedBorrow _ ->
             (* Raise an exception *)
             raise (FoundABorrowContent bc)
         | V.AProjSharedBorrow asb ->
@@ -1146,7 +1189,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
           ^ aborrow_content_to_string ctx bc));
       let ctx =
         match bc with
-        | V.AMutBorrow (_mv, bid, av) ->
+        | V.AMutBorrow (bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
             let sv = convert_avalue_to_given_back_value abs.kind av in
             (* Replace the mut borrow to register the fact that we ended
@@ -1649,9 +1692,9 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
         assert allow_borrows;
         (* Explore the borrow content *)
         match bc with
-        | V.AMutBorrow (mv, bid, child_av) ->
+        | V.AMutBorrow (bid, child_av) ->
             let ignored = mk_aignored child_av.V.ty in
-            let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+            let value = V.ABorrow (V.AMutBorrow (bid, ignored)) in
             push { V.value; ty };
             (* Explore the child *)
             list_avalues false push_fail child_av
@@ -1833,11 +1876,10 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx bv.V.value));
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
-            let mv = bv in
             let ref_ty = ety_no_regions_to_rty ref_ty in
             let ty = T.Ref (T.Var r_id, ref_ty, kind) in
             let ignored = mk_aignored ref_ty in
-            let av = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+            let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in
             let av = { V.value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
                because we don't support nested borrows for now) *)
@@ -2015,7 +2057,7 @@ let compute_merge_abstractions_info (abs : V.abs) : merge_abstraction_info =
         in
         (* Explore the borrow content *)
         (match bc with
-        | V.AMutBorrow (_, bid, _) -> push_borrow bid (Abstract (ty, bc))
+        | V.AMutBorrow (bid, _) -> push_borrow bid (Abstract (ty, bc))
         | V.ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc))
         | V.AProjSharedBorrow asb ->
             let register asb =
@@ -2053,19 +2095,15 @@ type merge_duplicates_funcs = {
   merge_amut_borrows :
     V.borrow_id ->
     T.rty ->
-    V.mvalue ->
     V.typed_avalue ->
     T.rty ->
-    V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
-          - [mv0]
           - [child0]
           - [ty1]
-          - [mv1]
           - [child1]
 
           The children should be [AIgnored].
@@ -2208,9 +2246,8 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
   let merge_aborrow_contents (ty0 : T.rty) (bc0 : V.aborrow_content)
       (ty1 : T.rty) (bc1 : V.aborrow_content) : V.typed_avalue =
     match (bc0, bc1) with
-    | V.AMutBorrow (mv0, id, child0), V.AMutBorrow (mv1, _, child1) ->
-        (Option.get merge_funs).merge_amut_borrows id ty0 mv0 child0 ty1 mv1
-          child1
+    | V.AMutBorrow (id, child0), V.AMutBorrow (_, child1) ->
+        (Option.get merge_funs).merge_amut_borrows id ty0 child0 ty1 child1
     | ASharedBorrow id, ASharedBorrow _ ->
         (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
     | AProjSharedBorrow _, AProjSharedBorrow _ ->
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 51c6c592..6a8fb87c 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -142,19 +142,15 @@ type merge_duplicates_funcs = {
   merge_amut_borrows :
     V.borrow_id ->
     T.rty ->
-    V.mvalue ->
     V.typed_avalue ->
     T.rty ->
-    V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue;
       (** Parameters:
           - [id]
           - [ty0]
-          - [mv0]
           - [child0]
           - [ty1]
-          - [mv1]
           - [child1]
 
           The children should be [AIgnored].
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6eece4fe..f4116b75 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -186,7 +186,9 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty)
 
     The loan is referred to by a borrow id.
 
-    TODO: group abs_or_var_id and g_loan_content. 
+    Rem.: if the {!g_loan_content} is {!Concrete}, the {!abs_or_var_id} is not
+    necessarily {!VarId} or {!DummyVarId}: there can be concrete loans in
+    abstractions (in the shared values).
  *)
 let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
     (ctx : C.eval_ctx) : (abs_or_var_id * g_loan_content) option =
@@ -434,9 +436,9 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_aborrow_content env bc =
         match bc with
-        | V.AMutBorrow (mv, bid, av) ->
+        | V.AMutBorrow (bid, av) ->
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_AMutBorrow env mv bid av
+            else super#visit_AMutBorrow env bid av
         | V.ASharedBorrow bid ->
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_ASharedBorrow env bid
@@ -551,9 +553,9 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
 
       method! visit_ABorrow env bc =
         match bc with
-        | V.AMutBorrow (mv, bid, av) ->
+        | V.AMutBorrow (bid, av) ->
             if bid = l then update ()
-            else V.ABorrow (super#visit_AMutBorrow env mv bid av)
+            else V.ABorrow (super#visit_AMutBorrow env bid av)
         | V.ASharedBorrow bid ->
             if bid = l then update ()
             else V.ABorrow (super#visit_ASharedBorrow env bid)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index f0a7fdbd..1228ae99 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -476,28 +476,22 @@ module type Matcher = sig
 
   (** Parameters:
       [ty0]
-      [mv0]
       [bid0]
       [av0]
       [ty1]
-      [mv1]
       [bid1]
       [av1]
       [ty]: result of matching ty0 and ty1
-      [mv]: result of matching mv0 and mv1
       [av]: result of matching av0 and av1
    *)
   val match_amut_borrows :
     T.rty ->
-    V.mvalue ->
     V.borrow_id ->
     V.typed_avalue ->
     T.rty ->
-    V.mvalue ->
     V.borrow_id ->
     V.typed_avalue ->
     T.rty ->
-    V.mvalue ->
     V.typed_avalue ->
     V.typed_avalue
 
@@ -692,16 +686,9 @@ module Match (M : Matcher) = struct
         match (bc0, bc1) with
         | ASharedBorrow bid0, ASharedBorrow bid1 ->
             M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty
-        | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) ->
-            (* The meta-value should be the value consumed by the abstracion.
-               This only makes sense if the abstraction was introduced because
-               of a function call (we use it for the translation).
-               TODO: make it optional?
-            *)
-            let mv = mk_bottom mv0.V.ty in
+        | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) ->
             let av = match_arec av0 av1 in
-            M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 ty mv
-              av
+            M.match_amut_borrows v0.V.ty bid0 av0 v1.V.ty bid1 av1 ty av
         | AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
             (* The abstractions are destructured: we shouldn't get there *)
             raise (Failure "Unexpected")
@@ -894,7 +881,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue =
         let bv_ty = ety_no_regions_to_rty bv.V.ty in
-        let value = V.ABorrow (V.AMutBorrow (bv, bid, mk_aignored bv_ty)) in
+        let value = V.ABorrow (V.AMutBorrow (bid, mk_aignored bv_ty)) in
         { V.value; ty = borrow_ty }
       in
       let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in
@@ -1026,7 +1013,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
 
   let match_distinct_aadts _ _ _ _ _ = raise (Failure "Unreachable")
   let match_ashared_borrows _ _ _ _ = raise (Failure "Unreachable")
-  let match_amut_borrows _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
+  let match_amut_borrows _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
   let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
   let match_amut_loans _ _ _ _ _ _ _ _ = raise (Failure "Unreachable")
   let match_avalues _ _ = raise (Failure "Unreachable")
@@ -1053,18 +1040,15 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
   let module M = Match (JM) in
   (* TODO: why not simply call: M.match_type_avalues? (or move this code to
      MakeJoinMatcher?) *)
-  let merge_amut_borrows id ty0 (mv0 : V.typed_value) child0 _ty1
-      (mv1 : V.typed_value) child1 =
+  let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
     assert (is_aignored child0.V.value);
     assert (is_aignored child1.V.value);
-    assert (mv0.V.ty = mv1.V.ty);
 
     (* Same remarks as for [merge_amut_loans] *)
     let ty = ty0 in
     let child = child0 in
-    let mv = mk_bottom mv0.ty in
-    let value = V.ABorrow (V.AMutBorrow (mv, id, child)) in
+    let value = V.ABorrow (V.AMutBorrow (id, child)) in
     { V.value; ty }
   in
 
@@ -1486,9 +1470,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
     let value = V.ABorrow (V.ASharedBorrow bid) in
     { V.value; ty }
 
-  let match_amut_borrows _ty0 _mv0 bid0 _av0 _ty1 _mv1 bid1 _av1 ty mv av =
+  let match_amut_borrows _ty0 bid0 _av0 _ty1 bid1 _av1 ty av =
     let bid = match_bid bid0 bid1 in
-    let value = V.ABorrow (V.AMutBorrow (mv, bid, av)) in
+    let value = V.ABorrow (V.AMutBorrow (bid, av)) in
     { V.value; ty }
 
   let match_ashared_loans _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av =
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index a69052cb..9487df84 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -130,14 +130,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
             let bc =
               match (bc, kind) with
               | V.MutBorrow (bid, bv), T.Mut ->
-                  (* Remember the borrowed value we are about to project as a meta-value *)
-                  let mv = bv in
                   (* Apply the projection on the borrowed value *)
                   let bv =
                     apply_proj_borrows check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
-                  V.AMutBorrow (mv, bid, bv)
+                  V.AMutBorrow (bid, bv)
               | V.SharedBorrow bid, T.Shared ->
                   (* Rem.: we don't need to also apply the projection on the
                      borrowed value, because for as long as the abstraction
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 3fdb963a..5b81cc02 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -253,7 +253,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
       method! visit_aborrow_content env bc =
         let _ =
           match bc with
-          | V.AMutBorrow (_, bid, _) -> register_borrow Mut bid
+          | V.AMutBorrow (bid, _) -> register_borrow Mut bid
           | V.ASharedBorrow bid -> register_borrow Shared bid
           | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
           | V.AIgnoredMutBorrow (None, _)
@@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match bc with
-          | V.AMutBorrow (_, _, _) -> set_outer_mut info
+          | V.AMutBorrow (_, _) -> set_outer_mut info
           | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
           | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
           | V.AEndedIgnoredMutBorrow _ ->
@@ -480,7 +480,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 let glc = lookup_borrow ek_all bid ctx in
                 match glc with
                 | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
-                | Abstract (V.AMutBorrow (_, _, sv)) ->
+                | Abstract (V.AMutBorrow (_, sv)) ->
                     assert (Subst.erase_regions sv.V.ty = ty)
                 | _ -> raise (Failure "Inconsistent context")))
         | V.Symbolic sv, ty ->
@@ -547,7 +547,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.ABottom, _ -> (* Nothing to check *) ()
         | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.AMutBorrow (_, _, av), T.Mut ->
+            | V.AMutBorrow (_, av), T.Mut ->
                 (* Check that the child value has the proper type *)
                 assert (av.V.ty = ref_ty)
             | V.ASharedBorrow bid, T.Shared -> (
@@ -578,7 +578,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 match glc with
                 | Concrete (V.MutBorrow (_, bv)) ->
                     assert (bv.V.ty = Subst.erase_regions borrowed_aty)
-                | Abstract (V.AMutBorrow (_, _, sv)) ->
+                | Abstract (V.AMutBorrow (_, sv)) ->
                     assert (
                       Subst.erase_regions sv.V.ty
                       = Subst.erase_regions borrowed_aty)
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 88d33bce..393f80c2 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -264,7 +264,7 @@ module Values = struct
   and aborrow_content_to_string (fmt : value_formatter) (bc : V.aborrow_content)
       : string =
     match bc with
-    | AMutBorrow (_, bid, av) ->
+    | AMutBorrow (bid, av) ->
         "&mut@" ^ V.BorrowId.to_string bid ^ " ("
         ^ typed_avalue_to_string fmt av
         ^ ")"
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 81cc22e1..6c956fe8 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -949,7 +949,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
 and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
     texpression option =
   match bc with
-  | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+  | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       raise (Failure "Unreachable")
   | AEndedMutBorrow (_, _) ->
       (* We collect consumed values: ignore *)
@@ -1089,7 +1089,7 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
 and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match bc with
-  | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+  | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       raise (Failure "Unreachable")
   | AEndedMutBorrow (msv, _) ->
       (* Return the meta-symbolic-value *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 54575edd..a57c589b 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -638,7 +638,7 @@ and aloan_content =
     ids)?
 *)
 and aborrow_content =
-  | AMutBorrow of mvalue * borrow_id * typed_avalue
+  | AMutBorrow of borrow_id * typed_avalue
       (** A mutable borrow owned by an abstraction.
       
           Is used when an abstraction "consumes" borrows, when giving borrows
@@ -658,17 +658,6 @@ and aborrow_content =
             > px -> ⊥
             > abs0 { a_mut_borrow l0 (U32 0) }
           ]}
-          
-          The meta-value stores the initial value on which the projector was
-          applied, which reduced to this mut borrow. This meta-information
-          is only used for the synthesis.
-          Rem.: we don't use the meta-value for now, but might need it when
-          using nested borrows: if we end an *internal* borrow, this meta
-          value is propagated to the corresponding loan (we need to know
-          what the loan consumed, for the synthesis). We could also generate
-          a fresh symbolic value upon ending the internal borrow (as is
-          done in the regular case), which would allow us to remove the
-          meta-value altogether.
      *)
   | ASharedBorrow of borrow_id
       (** A shared borrow owned by an abstraction.