Update Aeneas following changes in Charon

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-82938d10c82d07b24d25de3357c4d3b357382edf
+aec7312164f5f9d68ac432053f35e293de52ef01

compiler/AssociatedTypes.ml

@@ -35,8 +35,8 @@ end
 module TyMap = Collections.MakeMap (TyOrd)
 
 let compute_norm_trait_types_from_preds (span : Meta.span option)
-    (trait_type_constraints : trait_type_constraint list) : ty TraitTypeRefMap.t
-    =
+    (trait_type_constraints : trait_type_constraint region_binder list) :
+    ty TraitTypeRefMap.t =
   (* Compute a union-find structure by recursively exploring the predicates and clauses *)
   let norm : ty UnionFind.elem TyMap.t ref = ref TyMap.empty in
   let get_ref (ty : ty) : ty UnionFind.elem =
@@ -47,10 +47,13 @@ let compute_norm_trait_types_from_preds (span : Meta.span option)
         norm := TyMap.add ty r !norm;
         r
   in
-  let add_trait_type_constraint (c : trait_type_constraint) =
-    (* Sanity check: the type constraint can't make use of regions - Remark
+  let add_trait_type_constraint (c : trait_type_constraint region_binder) =
+    (* Sanity check: there are no bound regions *)
+    sanity_check_opt_span __FILE__ __LINE__ (c.binder_regions = []) span;
+    (* Sanity check: the type constraint can't make use of regions - Note
        that it would be enough to only visit the field [ty] of the trait type
        constraint, but for safety we visit all the fields *)
+    let c = c.binder_value in
     sanity_check_opt_span __FILE__ __LINE__
       (trait_type_constraint_no_regions c)
       span;
@@ -83,7 +86,8 @@ let compute_norm_trait_types_from_preds (span : Meta.span option)
   TraitTypeRefMap.of_list rbindings
 
 let ctx_add_norm_trait_types_from_preds (span : Meta.span option)
-    (ctx : eval_ctx) (trait_type_constraints : trait_type_constraint list) :
+    (ctx : eval_ctx)
+    (trait_type_constraints : trait_type_constraint region_binder list) :
     eval_ctx =
   let norm_trait_types =
     compute_norm_trait_types_from_preds span trait_type_constraints
@@ -397,13 +401,25 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) :
 
   (* Check if the id is an impl, otherwise normalize it *)
   let trait_id = norm_ctx_normalize_trait_instance_id ctx trait_id in
-  let trait_decl_ref = norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref in
+  let trait_decl_ref =
+    norm_ctx_normalize_region_binder norm_ctx_normalize_trait_decl_ref ctx
+      trait_decl_ref
+  in
   log#ldebug
     (lazy
       ("norm_ctx_normalize_trait_ref: no norm: "
       ^ trait_instance_id_to_string ctx trait_id));
   { trait_id; trait_decl_ref }
 
+and norm_ctx_normalize_region_binder :
+      'a.
+      (norm_ctx -> 'a -> 'a) -> norm_ctx -> 'a region_binder -> 'a region_binder
+    =
+ fun norm_value ctx rb ->
+  let { binder_regions; binder_value } = rb in
+  let binder_value = norm_value ctx binder_value in
+  { binder_regions; binder_value }
+
 (* Not sure this one is really necessary *)
 and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx)
     (trait_decl_ref : trait_decl_ref) : trait_decl_ref =
@@ -439,9 +455,12 @@ let ctx_normalize_erase_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
   let ty = ctx_normalize_ty (Some span) ctx ty in
   Subst.erase_regions ty
 
-let ctx_normalize_trait_type_constraint (span : Meta.span) (ctx : eval_ctx)
-    (ttc : trait_type_constraint) : trait_type_constraint =
-  norm_ctx_normalize_trait_type_constraint (mk_norm_ctx (Some span) ctx) ttc
+let ctx_normalize_trait_type_constraint_region_binder (span : Meta.span)
+    (ctx : eval_ctx) (ttc : trait_type_constraint region_binder) :
+    trait_type_constraint region_binder =
+  norm_ctx_normalize_region_binder norm_ctx_normalize_trait_type_constraint
+    (mk_norm_ctx (Some span) ctx)
+    ttc
 
 (** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *)
 let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
@@ -512,7 +531,7 @@ let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
   let output = ctx_normalize_ty (Some span) ctx output in
   let trait_type_constraints =
     List.map
-      (ctx_normalize_trait_type_constraint span ctx)
+      (ctx_normalize_trait_type_constraint_region_binder span ctx)
       trait_type_constraints
   in
   { regions_hierarchy; inputs; output; trait_type_constraints }

compiler/ExtractBase.ml

@@ -1656,9 +1656,12 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
         (fun (c : Types.trait_clause) -> c.clause_id = clause_id)
         clauses
     in
-    let trait_id = clause.trait.trait_decl_id in
+    (* Note that we ignore the binder *)
+    let clause_trait = clause.trait.binder_value in
+    (* *)
+    let trait_id = clause_trait.trait_decl_id in
     let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
-    let args = clause.trait.decl_generics in
+    let args = clause_trait.decl_generics in
     trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
       impl_trait_decl.item_meta.name params args
   in

compiler/Interpreter.ml

@@ -133,15 +133,27 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
       List.fold_left_map
         (fun tr_map (c : trait_clause) ->
           let subst = mk_subst tr_map in
-          let { trait_decl_id; decl_generics; _ } = c.trait in
+          (* *)
+          sanity_check __FILE__ __LINE__ (c.trait.binder_regions = []) span;
+          let { trait_decl_id; decl_generics; _ } = c.trait.binder_value in
           let generics =
             Substitute.generic_args_substitute subst decl_generics
           in
           let trait_decl_ref = { trait_decl_id; decl_generics = generics } in
           (* Note that because we directly refer to the clause, we give it
              empty generics *)
           let trait_id = Clause c.clause_id in
-          let trait_ref = { trait_id; trait_decl_ref } in
+          let trait_ref =
+            {
+              trait_id;
+              trait_decl_ref =
+                {
+                  (* Empty list of bound regions: we don't support the other cases for now *)
+                  binder_regions = [];
+                  binder_value = trait_decl_ref;
+                };
+            }
+          in
           (* Update the traits map *)
           let tr_map = TraitClauseId.Map.add c.clause_id trait_id tr_map in
           (tr_map, trait_ref))

compiler/InterpreterStatements.ml

@@ -683,7 +683,13 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
              ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
               ^ generic_args_to_string ctx func.generics
               ^ "\n- trait_ref.trait_decl_ref: "
-              ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref));
+              ^ trait_decl_ref_region_binder_to_string ctx
+                  trait_ref.trait_decl_ref));
+          (* Check that there are no bound regions *)
+          cassert __FILE__ __LINE__
+            (trait_ref.trait_decl_ref.binder_regions = [])
+            span "Unexpected bound regions";
+          let trait_decl_ref = trait_ref.trait_decl_ref.binder_value in
           (* Lookup the trait method signature - there are several possibilities
              depending on whethere we call a top-level trait method impl or the
              method from a local clause *)
@@ -737,8 +743,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                     (trait_impl.provided_methods = [])
                     span "Overriding provided methods is currently forbidden";
                   let trait_decl =
-                    ctx_lookup_trait_decl ctx
-                      trait_ref.trait_decl_ref.trait_decl_id
+                    ctx_lookup_trait_decl ctx trait_decl_ref.trait_decl_id
                   in
                   let _, method_id =
                     List.find
@@ -764,8 +769,8 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                      ]}
                   *)
                   let all_generics =
-                    TypesUtils.merge_generic_args
-                      trait_ref.trait_decl_ref.decl_generics func.generics
+                    TypesUtils.merge_generic_args trait_decl_ref.decl_generics
+                      func.generics
                   in
                   log#ldebug
                     (lazy
@@ -793,7 +798,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
           | _ ->
               (* We are using a local clause - we lookup the trait decl *)
               let trait_decl =
-                ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id
+                ctx_lookup_trait_decl ctx trait_decl_ref.trait_decl_id
               in
               (* Lookup the method decl in the required *and* the provided methods *)
               let _, method_id =
@@ -809,8 +814,8 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
               (* When instantiating, we need to group the generics for the
                  trait ref and the generics for the method *)
               let generics =
-                TypesUtils.merge_generic_args
-                  trait_ref.trait_decl_ref.decl_generics func.generics
+                TypesUtils.merge_generic_args trait_decl_ref.decl_generics
+                  func.generics
               in
               let regions_hierarchy =
                 LlbcAstUtils.FunIdMap.find (FRegular method_id)

compiler/InterpreterUtils.ml

@@ -34,6 +34,9 @@ let generic_args_to_string = Print.EvalCtx.generic_args_to_string
 let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string
 let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string
 
+let trait_decl_ref_region_binder_to_string =
+  Print.EvalCtx.trait_decl_ref_region_binder_to_string
+
 let fun_id_or_trait_method_ref_to_string =
   Print.EvalCtx.fun_id_or_trait_method_ref_to_string
 

compiler/LlbcAst.ml

@@ -10,7 +10,7 @@ type abs_region_groups = abs_region_group list [@@deriving show]
 (** A function signature, after instantiation *)
 type inst_fun_sig = {
   regions_hierarchy : abs_region_groups;
-  trait_type_constraints : trait_type_constraint list;
+  trait_type_constraints : trait_type_constraint region_binder list;
   inputs : rty list;
   output : rty;
 }

compiler/Print.ml

@@ -558,6 +558,11 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     trait_ref_to_string env x
 
+  let trait_decl_ref_region_binder_to_string (ctx : eval_ctx)
+      (x : trait_decl_ref region_binder) : string =
+    let env = eval_ctx_to_fmt_env ctx in
+    region_binder_to_string trait_decl_ref_to_string env x
+
   let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string =
     let env = eval_ctx_to_fmt_env ctx in
     trait_decl_ref_to_string env x

compiler/RegionsHierarchy.ml

@@ -120,6 +120,13 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
         g := RegionMap.add short s m
   in
 
+  let add_edges_from_region_binder :
+        'a. ('a -> unit) -> 'a region_binder -> unit =
+   fun visit c ->
+    sanity_check_opt_span __FILE__ __LINE__ (c.binder_regions = []) span;
+    visit c.binder_value
+  in
+
   let add_edge_from_region_constraint ((long, short) : region_outlives) =
     add_edge ~short ~long
   in
@@ -130,7 +137,9 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
 
   (* Explore the clauses - we only explore the "region outlives" clause,
      not the "type outlives" clauses *)
-  List.iter add_edge_from_region_constraint sg.generics.regions_outlive;
+  List.iter
+    (add_edges_from_region_binder add_edge_from_region_constraint)
+    sg.generics.regions_outlive;
 
   (* Explore the types in the signature to add the edges *)
   let rec explore_ty (outer : region list) (ty : ty) =
@@ -151,11 +160,17 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
             let predicates = Subst.predicates_substitute subst decl.generics in
             (* Note that because we also explore the generics below, we may
                explore several times the same type - this is ok *)
+            let add_edges_from_regions_outlive (long, short) =
+              add_edges ~long ~shorts:(short :: outer)
+            in
             List.iter
-              (fun (long, short) -> add_edges ~long ~shorts:(short :: outer))
+              (add_edges_from_region_binder add_edges_from_regions_outlive)
               predicates.regions_outlive;
+            let add_edges_from_types_outlive (ty, short) =
+              explore_ty (short :: outer) ty
+            in
             List.iter
-              (fun (ty, short) -> explore_ty (short :: outer) ty)
+              (add_edges_from_region_binder add_edges_from_types_outlive)
               predicates.types_outlive
         | TTuple -> (* No clauses for tuples *) ()
         | TAssumed aid -> (

compiler/Substitute.ml

@@ -116,9 +116,27 @@ let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
     ({ id; regions; parents } : abs_region_group)
   in
   let regions_hierarchy = List.map subst_region_group regions_hierarchy in
+  let push_region_group (subst : subst) : subst =
+    let r_subst (r : region) : region =
+      match r with
+      | RStatic | RErased | RFVar _ -> r
+      | RBVar (bdid, rid) ->
+          if bdid = 0 then r else subst.r_subst (RBVar (bdid - 1, rid))
+    in
+    { subst with r_subst }
+  in
+  let subst_region_binder :
+        'a. (subst -> 'a -> 'a) -> subst -> 'a region_binder -> 'a region_binder
+      =
+   fun subst_value subst rb ->
+    let subst = push_region_group subst in
+    let { binder_regions; binder_value } = rb in
+    let binder_value = subst_value subst binder_value in
+    { binder_regions; binder_value }
+  in
   let trait_type_constraints =
     List.map
-      (trait_type_constraint_substitute subst)
+      (subst_region_binder trait_type_constraint_substitute subst)
       sg.generics.trait_type_constraints
   in
   { inputs; output; regions_hierarchy; trait_type_constraints }

compiler/SymbolicToPure.ml

@@ -405,6 +405,11 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
     A.fun_decl =
   A.FunDeclId.Map.find id ctx.fun_ctx.llbc_fun_decls
 
+(* We simply ignore the bound regions *)
+let translate_region_binder (translate_value : 'a -> 'b)
+    (rb : 'a T.region_binder) : 'b =
+  translate_value rb.binder_value
+
 (* Some generic translation functions (we need to translate different "flavours"
    of types: forward types, backward types, etc.) *)
 let rec translate_generic_args (span : Meta.span option)
@@ -422,7 +427,9 @@ and translate_trait_ref (span : Meta.span option) (translate_ty : T.ty -> ty)
     (tr : T.trait_ref) : trait_ref =
   let trait_id = translate_trait_instance_id span translate_ty tr.trait_id in
   let trait_decl_ref =
-    translate_trait_decl_ref span translate_ty tr.trait_decl_ref
+    translate_region_binder
+      (translate_trait_decl_ref span translate_ty)
+      tr.trait_decl_ref
   in
   { trait_id; trait_decl_ref }
 
@@ -526,11 +533,15 @@ and translate_strait_instance_id (span : Meta.span option)
     (id : T.trait_instance_id) : trait_instance_id =
   translate_trait_instance_id span (translate_sty span) id
 
+let translate_strait_decl_ref (span : Meta.span option) (tr : T.trait_decl_ref)
+    : trait_decl_ref =
+  translate_trait_decl_ref span (translate_sty span) tr
+
 let translate_trait_clause (span : Meta.span option) (clause : T.trait_clause) :
     trait_clause =
   let { T.clause_id; span = _; trait } = clause in
-  let generics = translate_sgeneric_args span trait.decl_generics in
-  { clause_id; trait_id = trait.trait_decl_id; generics }
+  let trait = translate_region_binder (translate_strait_decl_ref span) trait in
+  { clause_id; trait_id = trait.trait_decl_id; generics = trait.decl_generics }
 
 let translate_strait_type_constraint (span : Meta.span option)
     (ttc : T.trait_type_constraint) : trait_type_constraint =
@@ -553,7 +564,9 @@ let translate_generic_params (span : Meta.span option)
   in
   let trait_clauses = List.map (translate_trait_clause span) trait_clauses in
   let trait_type_constraints =
-    List.map (translate_strait_type_constraint span) trait_type_constraints
+    List.map
+      (translate_region_binder (translate_strait_type_constraint span))
+      trait_type_constraints
   in
   ({ types; const_generics; trait_clauses }, { trait_type_constraints })
 
@@ -4135,8 +4148,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   let span = item_meta.span in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
-    translate_trait_decl_ref (Some span)
-      (translate_fwd_ty (Some span) type_infos)
+    (translate_trait_decl_ref (Some span)
+       (translate_fwd_ty (Some span) type_infos))
       llbc_impl_trait
   in
   let name =