AeneasVerif · Nadrieril · Jul 16, 2024 · Jul 16, 2024
diff --git a/charon-pin b/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.
-cccc38353eec92c32c0f7a755fcef4ab5b1ae863
+65a82e39d87f019eb2d83b7e5a9f6ee4026db696
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
@@ -90,12 +90,11 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
   { ctx with norm_trait_types }
 
 (** A trait instance id refers to a local clause if it only uses the variants:
-    [Self], [Clause], [ParentClause], [ItemClause] *)
+    [Self], [Clause], [ParentClause] *)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
-  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
-      trait_instance_id_is_local_clause id
+  | ParentClause (id, _, _) -> trait_instance_id_is_local_clause id
   | TraitImpl _
   | BuiltinOrAuto _
   | UnknownTrait _
@@ -185,7 +184,7 @@ let norm_ctx_lookup_trait_impl_ty (ctx : norm_ctx) (impl_id : TraitImplId.id)
   (* Lookup the implementation *)
   let trait_impl, subst = norm_ctx_lookup_trait_impl ctx impl_id generics in
   (* Lookup the type *)
-  let ty = snd (List.assoc type_name trait_impl.types) in
+  let ty = List.assoc type_name trait_impl.types in
   (* Substitute *)
   Subst.ty_substitute subst ty
 
@@ -201,19 +200,6 @@ let norm_ctx_lookup_trait_impl_parent_clause (ctx : norm_ctx)
   (* Substitute *)
   Subst.trait_ref_substitute subst clause
 
-let norm_ctx_lookup_trait_impl_item_clause (ctx : norm_ctx)
-    (impl_id : TraitImplId.id) (generics : generic_args) (item_name : string)
-    (clause_id : TraitClauseId.id) : trait_ref =
-  (* Lookup the implementation *)
-  let trait_impl, subst = norm_ctx_lookup_trait_impl ctx impl_id generics in
-  (* Lookup the item then its clause *)
-  let item = List.assoc item_name trait_impl.types in
-  let clause = TraitClauseId.nth (fst item) clause_id in
-  (* Sanity check: the clause necessarily refers to an impl *)
-  let _ = TypesUtils.trait_instance_id_as_trait_impl clause.trait_id in
-  (* Substitute *)
-  Subst.trait_ref_substitute subst clause
-
 (** Normalize a type by simplifying the references to trait associated types
     and choosing a representative when there are equalities between types
     enforced by local clauses (i.e., `where Trait1::T = Trait2::U`.
@@ -325,7 +311,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       the normalization is in particular to eliminate it. Inside a [TraitRef]
       there is necessarily:
       - an id referencing a local (sub-)clause, that is an id using the variants
-        [Self], [Clause], [ItemClause] and [ParentClause] exclusively. We can't
+        [Self], [Clause], and [ParentClause] exclusively. We can't
         simplify those cases: all we can do is remove the [TraitRef] wrapper
         by leveraging the fact that the generic arguments must be empty.
       - a [TraitImpl]. Note that the [TraitImpl] is necessarily just a [TraitImpl],
@@ -377,36 +363,6 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
             ctx.span;
           ParentClause (inst_id, decl_id, clause_id)
     end
-  | ItemClause (inst_id, decl_id, item_name, clause_id) -> begin
-      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
-      (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match inst_id with
-      | TraitImpl (impl_id, generics) ->
-          (* We figure out the item clause by doing the following:
-             {[
-               // The implementation we are looking at
-               impl Impl1 : Trait1<R> {
-                  type S = ...
-                     with Impl2 : Trait2 ... // Instances satisfying the declared bounds
-                          ^^^^^^^^^^^^^^^^^^
-                      Lookup the clause from here
-               }
-             ]}
-          *)
-          (* Lookup the impl *)
-          let clause =
-            norm_ctx_lookup_trait_impl_item_clause ctx impl_id generics
-              item_name clause_id
-          in
-          (* Normalize the clause *)
-          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
-      | _ ->
-          (* This is actually a local clause *)
-          sanity_check_opt_span __FILE__ __LINE__
-            (trait_instance_id_is_local_clause inst_id)
-            ctx.span;
-          ItemClause (inst_id, decl_id, item_name, clause_id)
-    end
   | FnPointer ty ->
       let ty = norm_ctx_normalize_ty ctx ty in
       (* TODO: we might want to return the ref to the function pointer,

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
@@ -2120,55 +2120,26 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
           if !record_fields_short_names then type_name
           else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
         in
-        let compute_clause_name (item_name : string) (clause : trait_clause) :
-            TraitClauseId.id * string =
-          let name =
-            ctx_compute_trait_type_clause_name ctx trait_decl item_name clause
-          in
-          (* Add a prefix if necessary *)
-          let name =
-            if !record_fields_short_names then name
-            else ctx_compute_trait_decl_name ctx trait_decl ^ name
-          in
-          (clause.clause_id, name)
-        in
         List.map
-          (fun (item_name, (item_clauses, _)) ->
+          (fun (item_name, _) ->
             (* Type name *)
             let type_name = compute_type_name item_name in
-            (* Clause names *)
-            let clauses =
-              List.map (compute_clause_name item_name) item_clauses
-            in
-            (item_name, (type_name, clauses)))
+            (item_name, type_name))
           types
     | Some info ->
         let type_map = StringMap.of_list info.types in
         List.map
-          (fun (item_name, (item_clauses, _)) ->
-            let type_name, clauses_info = StringMap.find item_name type_map in
-            let clauses =
-              List.map
-                (fun (clause, clause_name) -> (clause.clause_id, clause_name))
-                (List.combine item_clauses clauses_info)
-            in
-            (item_name, (type_name, clauses)))
+          (fun (item_name, _) ->
+            let type_name = StringMap.find item_name type_map in
+            (item_name, type_name))
           types
   in
   (* Register the names *)
   List.fold_left
-    (fun ctx (item_name, (type_name, clauses)) ->
-      let ctx =
-        ctx_add trait_decl.item_meta.span
-          (TraitItemId (trait_decl.def_id, item_name))
-          type_name ctx
-      in
-      List.fold_left
-        (fun ctx (clause_id, clause_name) ->
-          ctx_add trait_decl.item_meta.span
-            (TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
-            clause_name ctx)
-        ctx clauses)
+    (fun ctx (item_name, type_name) ->
+      ctx_add trait_decl.item_meta.span
+        (TraitItemId (trait_decl.def_id, item_name))
+        type_name ctx)
     ctx type_names
 
 (** Similar to {!extract_trait_decl_register_names} *)
@@ -2510,7 +2481,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* The types *)
     List.iter
-      (fun (name, (clauses, _)) ->
+      (fun (name, _) ->
         (* Extract the type *)
         let item_name =
           ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
@@ -2519,21 +2490,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_space fmt ();
           F.pp_print_string fmt (type_keyword decl.item_meta.span)
         in
-        extract_trait_decl_item ctx fmt item_name ty;
-        (* Extract the clauses *)
-        List.iter
-          (fun clause ->
-            let item_name =
-              ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
-                clause.clause_id ctx
-            in
-            let ty () =
-              F.pp_print_space fmt ();
-              extract_trait_clause_type decl.item_meta.span ctx fmt
-                TypeDeclId.Set.empty clause
-            in
-            extract_trait_decl_item ctx fmt item_name ty)
-          clauses)
+        extract_trait_decl_item ctx fmt item_name ty)
       decl.types;
 
     (* The parent clauses - note that the parent clauses may refer to the types
@@ -2598,21 +2555,12 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
       decl.consts;
     (* The types *)
     List.iter
-      (fun (name, (clauses, _)) ->
+      (fun (name, _) ->
         (* The type *)
         let item_name =
           ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
         in
-        extract_coq_arguments_instruction ctx fmt item_name num_params;
-        (* The type clauses *)
-        List.iter
-          (fun clause ->
-            let item_name =
-              ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
-                clause.clause_id ctx
-            in
-            extract_coq_arguments_instruction ctx fmt item_name num_params)
-          clauses)
+        extract_coq_arguments_instruction ctx fmt item_name num_params)
       decl.types;
     (* The parent clauses *)
     List.iter
@@ -2859,7 +2807,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* The types *)
     List.iter
-      (fun (name, (trait_refs, ty)) ->
+      (fun (name, ty) ->
         (* Extract the type *)
         let item_name =
           ctx_get_trait_type impl.item_meta.span trait_decl_id name ctx
@@ -2868,21 +2816,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_space fmt ();
           extract_ty impl.item_meta.span ctx fmt TypeDeclId.Set.empty false ty
         in
-        extract_trait_impl_item ctx fmt item_name ty;
-        (* Extract the clauses *)
-        TraitClauseId.iteri
-          (fun clause_id trait_ref ->
-            let item_name =
-              ctx_get_trait_item_clause impl.item_meta.span trait_decl_id name
-                clause_id ctx
-            in
-            let ty () =
-              F.pp_print_space fmt ();
-              extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
-                false trait_ref
-            in
-            extract_trait_impl_item ctx fmt item_name ty)
-          trait_refs)
+        extract_trait_impl_item ctx fmt item_name ty)
       impl.types;
 
     (* The parent clauses *)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
@@ -172,7 +172,6 @@ type id =
   | TraitItemId of TraitDeclId.id * string
       (** A trait associated item which is not a method *)
   | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
-  | TraitItemClauseId of TraitDeclId.id * string * TraitClauseId.id
   | TraitSelfClauseId
       (** Specifically for the clause: [Self : Trait].
 
@@ -396,11 +395,8 @@ let strict_collisions (id : id) : bool =
 (** We might not check for collisions for some specific ids (ex.: field names) *)
 let allow_collisions (id : id) : bool =
   match id with
-  | FieldId _
-  | TraitItemClauseId _
-  | TraitParentClauseId _
-  | TraitItemId _
-  | TraitMethodId _ -> !Config.record_fields_short_names
+  | FieldId _ | TraitParentClauseId _ | TraitItemId _ | TraitMethodId _ ->
+      !Config.record_fields_short_names
   | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) ->
       (* We map several assumed functions to the same id *)
       true
@@ -675,10 +671,6 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
   | TraitParentClauseId (id, clause_id) ->
       "trait_parent_clause_id: " ^ trait_decl_id_to_string id ^ ", clause_id: "
       ^ TraitClauseId.to_string clause_id
-  | TraitItemClauseId (id, item_name, clause_id) ->
-      "trait_item_clause_id: " ^ trait_decl_id_to_string id ^ ", item name: "
-      ^ item_name ^ ", clause_id: "
-      ^ TraitClauseId.to_string clause_id
   | TraitItemId (id, name) ->
       "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
   | TraitMethodId (trait_decl_id, fun_name) ->
@@ -759,10 +751,6 @@ let ctx_get_trait_parent_clause (span : Meta.span) (id : trait_decl_id)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
   ctx_get (Some span) (TraitParentClauseId (id, clause)) ctx
 
-let ctx_get_trait_item_clause (span : Meta.span) (id : trait_decl_id)
-    (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-  ctx_get (Some span) (TraitItemClauseId (id, item, clause)) ctx
-
 let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) :
     string =
   ctx_get (Some span) (VarId id) ctx

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
@@ -550,11 +550,10 @@ type builtin_trait_decl_info = {
   constructor : string;
   parent_clauses : string list;
   consts : (string * string) list;
-  types : (string * (string * string list)) list;
+  types : (string * string) list;
       (** Every type has:
           - a Rust name
-          - an extraction name
-          - a list of clauses *)
+          - an extraction name *)
   methods : (string * builtin_fun_info) list;
 }
 [@@deriving show]
@@ -586,8 +585,7 @@ let builtin_trait_decls_info () =
           | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
           | Lean -> type_name
         in
-        let clauses = [] in
-        (item_name, (type_name, clauses))
+        (item_name, type_name)
       in
       List.map mk_type types
     in

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
@@ -720,13 +720,6 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
       let name = ctx_get_trait_parent_clause span decl_id clause_id ctx in
       extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
-  | ItemClause (inst_id, decl_id, item_name, clause_id) ->
-      (* Use the trait decl id to lookup the name *)
-      let name =
-        ctx_get_trait_item_clause span decl_id item_name clause_id ctx
-      in
-      extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
-      F.pp_print_string fmt (add_brackets name)
   | UnknownTrait _ ->
       (* This is an error case *)
       craise __FILE__ __LINE__ span "Unexpected"

diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
@@ -198,10 +198,6 @@ and trait_instance_id_to_string (env : fmt_env) (id : trait_instance_id) :
       let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
       "parent(" ^ inst_id ^ ")::" ^ clause_id
-  | ItemClause (inst_id, _decl_id, item_name, clause_id) ->
-      let inst_id = trait_instance_id_to_string env inst_id in
-      let clause_id = trait_clause_id_to_string env clause_id in
-      "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
   | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
 
 let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
@@ -309,8 +309,6 @@ and trait_instance_id =
   | TraitImpl of trait_impl_id * generic_args
   | Clause of trait_clause_id
   | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
-  | ItemClause of
-      trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id
   | UnknownTrait of string
 [@@deriving
   show,
@@ -1147,7 +1145,7 @@ type trait_decl = {
   parent_clauses : trait_clause list;
   llbc_parent_clauses : Types.trait_clause list;
   consts : (trait_item_name * (ty * global_decl_id option)) list;
-  types : (trait_item_name * (trait_clause list * ty option)) list;
+  types : (trait_item_name * ty option) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id option) list;
 }
@@ -1170,7 +1168,7 @@ type trait_impl = {
   preds : predicates;
   parent_trait_refs : trait_ref list;
   consts : (trait_item_name * (ty * global_decl_id)) list;
-  types : (trait_item_name * (trait_ref list * ty)) list;
+  types : (trait_item_name * ty) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id) list;
 }