Update 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.
-8a17efc262ef3af377ab172efc865edcf1bb40ea
+d7737574abf6adbabca3ff45c22d77b9d0bbc5f5

src/Translate.ml

@@ -1126,7 +1126,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       use_dep_ite =
         Config.backend () = Lean && !Config.extract_decreases_clauses;
       trait_decl_id = None (* None by default *);
-      is_provided_method = false (* false by default *);
       trans_trait_decls;
       trans_trait_impls;
       trans_types;

src/extract/Extract.ml

@@ -1300,16 +1300,14 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
      TODO: micro-pass to update what happens when calling trait provided
      functions.
   *)
-  let ctx, trait_decl =
+  let trait_decl =
     match def.kind with
     | TraitDeclItem (trait_ref, _, true) ->
         let trait_decl =
           T.TraitDeclId.Map.find trait_ref.trait_decl_id ctx.trans_trait_decls
         in
-        let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
-        let ctx = { ctx with is_provided_method = true } in
-        (ctx, Some trait_decl)
-    | _ -> (ctx, None)
+        Some trait_decl
+    | _ -> None
   in
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)

src/extract/ExtractBase.ml

@@ -183,41 +183,6 @@ and id =
   | TraitItemId of TraitDeclId.id * string
       (** A trait associated item which is not a method *)
   | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
-  | TraitSelfClauseId
-      (** Specifically for the clause: [Self : Trait].
-
-          For now, we forbid provided methods (methods in trait declarations
-          with a default implementation) from being overriden in trait implementations.
-          We extract trait provided methods such that they take an instance of
-          the trait as input: this instance is given by the trait self clause.
-
-          For instance:
-          {[
-            //
-            // Rust
-            //
-            trait ToU64 {
-              fn to_u64(&self) -> u64;
-
-              // Provided method
-              fn is_pos(&self) -> bool {
-                self.to_u64() > 0
-              }
-            }
-
-            //
-            // Generated code
-            //
-            struct ToU64 (T : Type) {
-              to_u64 : T -> u64;
-            }
-
-            //                    The trait self clause
-            //                    vvvvvvvvvvvvvvvvvvvvvv
-            let is_pos (T : Type) (trait_self : ToU64 T) (self : T) : bool =
-              trait_self.to_u64 self > 0
-          ]}
-       *)
   | UnknownId
       (** Used for stored various strings like keywords, definitions which
           should always be in context, etc. and which can't be linked to one
@@ -592,7 +557,6 @@ type extraction_ctx = {
         *)
   trait_decl_id : trait_decl_id option;
       (** If we are extracting a trait declaration, identifies it *)
-  is_provided_method : bool;
   trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
   trans_funs : pure_fun_translation A.FunDeclId.Map.t;
   trans_globals : Pure.global_decl Pure.GlobalDeclId.Map.t;
@@ -706,7 +670,6 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
       "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
   | TraitMethodId (trait_decl_id, fun_name) ->
       trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name
-  | TraitSelfClauseId -> "trait_self_clause"
 
 let ctx_add (span : Meta.span) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
@@ -750,10 +713,6 @@ let ctx_get_trait_constructor (span : Meta.span) (id : trait_decl_id)
     (ctx : extraction_ctx) : string =
   ctx_get (Some span) (TraitDeclConstructorId id) ctx
 
-let ctx_get_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) : string
-    =
-  ctx_get (Some span) TraitSelfClauseId ctx
-
 let ctx_get_trait_decl (span : Meta.span) (id : trait_decl_id)
     (ctx : extraction_ctx) : string =
   ctx_get (Some span) (TraitDeclId id) ctx
@@ -2018,14 +1977,6 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
   let ctx = ctx_add span (VarId id) name ctx in
   (ctx, name)
 
-(** Generate a unique variable name for the trait self clause and add it to the context *)
-let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
-    extraction_ctx * string =
-  let basename = trait_self_clause_basename in
-  let name = basename_to_unique ctx basename in
-  let ctx = ctx_add span TraitSelfClauseId name ctx in
-  (ctx, name)
-
 (** Generate a unique trait clause name and add it to the context *)
 let ctx_add_local_trait_clause (span : Meta.span) (origin : generic_origin)
     (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) :

src/extract/ExtractTypes.ml

@@ -699,26 +699,9 @@ and extract_trait_instance_id_with_dot (span : Meta.span) (ctx : extraction_ctx)
     (id : trait_instance_id) : unit =
   match id with
   | Self ->
-      (* There are two situations:
-         - we are extracting a declared item and need to refer to another
-           item (for instance, we are extracting a method signature and
-           need to refer to an associated type).
-           We directly refer to the other item (we extract trait declarations
-           as structures, so we can refer to their fields)
-         - we are extracting a provided method for a trait declaration. We
-           refer to the item in the self trait clause (see {!SelfTraitClauseId}).
-
-         Remark: we can't get there for trait *implementations* because then the
-         types should have been normalized.
-      *)
-      if ctx.is_provided_method then
-        (* Provided method: use the trait self clause *)
-        let self_clause = ctx_get_trait_self_clause span ctx in
-        F.pp_print_string fmt (self_clause ^ ".")
-      else
-        (* Declaration: nothing to print, we will directly refer to
-           the item. *)
-        ()
+      (* This can only happen inside a trait (not inside its methods) so there
+         is nothing to print, we will directly refer to the item.*)
+      ()
   | _ ->
       (* Other cases *)
       extract_trait_instance_id span ctx fmt no_params_tys inside id;
@@ -1263,31 +1246,6 @@ let extract_trait_clause_type (span : Meta.span) (ctx : extraction_ctx)
 let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
   if !space then space := false else F.pp_print_space fmt ()
 
-(** Extract the trait self clause.
-
-    We add the trait self clause for provided methods (see {!TraitSelfClauseId}).
- *)
-let extract_trait_self_clause (insert_req_space : unit -> unit)
-    (ctx : extraction_ctx) (fmt : F.formatter) (trait_decl : trait_decl)
-    (params : string list) : unit =
-  insert_req_space ();
-  F.pp_print_string fmt "(";
-  let self_clause = ctx_get_trait_self_clause trait_decl.item_meta.span ctx in
-  F.pp_print_string fmt self_clause;
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt ":";
-  F.pp_print_space fmt ();
-  let trait_id =
-    ctx_get_trait_decl trait_decl.item_meta.span trait_decl.def_id ctx
-  in
-  F.pp_print_string fmt trait_id;
-  List.iter
-    (fun p ->
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt p)
-    params;
-  F.pp_print_string fmt ")"
-
 (**
  - [trait_decl]: if [Some], it means we are extracting the generics for a provided
    method and need to insert a trait self clause (see {!TraitSelfClauseId}).
@@ -1442,24 +1400,6 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
           List.map (fun (_, x) -> (Implicit, x)) dtrait_clauses
         in
         print_generics dtype_params dcgs dtrait_clauses;
-        (* Extract the trait self clause *)
-        let params =
-          concat
-            [
-              map snd dtype_params;
-              map
-                (fun ((_, cg) : _ * const_generic_var) ->
-                  ctx_get_const_generic_var trait_decl.item_meta.span origin
-                    cg.index ctx)
-                dcgs;
-              map
-                (fun (_, c) ->
-                  ctx_get_local_trait_clause trait_decl.item_meta.span origin
-                    c.clause_id ctx)
-                dtrait_clauses;
-            ]
-        in
-        extract_trait_self_clause insert_req_space ctx fmt trait_decl params;
         (* Extract the method generics *)
         print_generics mtype_params mcgs mtrait_clauses)
 

tests/coq/hashmap/Hashmap_FunsExternal_Template.v

@@ -23,7 +23,7 @@ Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit).
     Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
     Name pattern: core::clone::Clone::clone_from *)
 Axiom core_clone_Clone_clone_from :
-  forall{Self : Type} (self_clause : core_clone_Clone Self),
+  forall{Self : Type} (cloneInst1 : core_clone_Clone Self),
         Self -> Self -> state -> result (state * Self)
 .
 

tests/coq/misc/External_FunsExternal_Template.v

@@ -32,7 +32,7 @@ Axiom core_cell_Cell_get_mut :
     Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
     Name pattern: core::clone::Clone::clone_from *)
 Axiom core_clone_Clone_clone_from :
-  forall{Self : Type} (self_clause : core_clone_Clone Self),
+  forall{Self : Type} (cloneInst1 : core_clone_Clone Self),
         Self -> Self -> state -> result (state * Self)
 .
 

tests/coq/rename_attribute/RenameAttribute.v

@@ -30,8 +30,7 @@ Definition BoolImpl : BoolTest_t bool := {|
 
 (** [rename_attribute::BoolTrait::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-Definition boolTrait_retTest
-  {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
+Definition boolTrait_retTest {Self : Type} (self : Self) : result bool :=
   Ok true
 .
 

tests/coq/traits/Traits.v

@@ -30,8 +30,7 @@ Definition BoolTraitBool : BoolTrait_t bool := {|
 
 (** [traits::BoolTrait::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-Definition boolTrait_ret_true
-  {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
+Definition boolTrait_ret_true {Self : Type} (self : Self) : result bool :=
   Ok true
 .
 

tests/fstar/hashmap/Hashmap.FunsExternal.fsti

@@ -18,6 +18,6 @@ val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
     Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
     Name pattern: core::clone::Clone::clone_from *)
 val core_clone_Clone_clone_from
-  (#self : Type0) (self_clause : core_clone_Clone self) :
+  (#self : Type0) (cloneInst : core_clone_Clone self) :
   self -> self -> state -> result (state & self)
 

tests/fstar/misc/External.FunsExternal.fsti

@@ -25,6 +25,6 @@ val core_cell_Cell_get_mut
     Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
     Name pattern: core::clone::Clone::clone_from *)
 val core_clone_Clone_clone_from
-  (#self : Type0) (self_clause : core_clone_Clone self) :
+  (#self : Type0) (cloneInst : core_clone_Clone self) :
   self -> self -> state -> result (state & self)
 

tests/fstar/rename_attribute/RenameAttribute.Funs.fst

@@ -18,10 +18,7 @@ let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; }
 
 (** [rename_attribute::BoolTrait::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-let boolTrait_retTest
-  (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
-  result bool
-  =
+let boolTrait_retTest (#self : Type0) (self1 : self) : result bool =
   Ok true
 
 (** [rename_attribute::test_bool_trait]:

tests/fstar/traits/Traits.fst

@@ -20,10 +20,7 @@ let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; }
 
 (** [traits::BoolTrait::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-let boolTrait_ret_true
-  (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
-  result bool
-  =
+let boolTrait_ret_true (#self : Type0) (self1 : self) : result bool =
   Ok true
 
 (** [traits::test_bool_trait_bool]:

tests/lean/RenameAttribute.lean

@@ -27,8 +27,7 @@ def BoolImpl : BoolTest Bool := {
 
 /- [rename_attribute::BoolTrait::ret_true]:
    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/
-def BoolTrait.retTest
-  {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool :=
+def BoolTrait.retTest {Self : Type} (self : Self) : Result Bool :=
   Result.ok true
 
 /- [rename_attribute::test_bool_trait]:

tests/lean/Traits.lean

@@ -27,8 +27,7 @@ def BoolTraitBool : BoolTrait Bool := {
 
 /- [traits::BoolTrait::ret_true]:
    Source: 'tests/src/traits.rs', lines 8:4-10:5 -/
-def BoolTrait.ret_true
-  {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
+def BoolTrait.ret_true {Self : Type} (self : Self) : Result Bool :=
   Result.ok true
 
 /- [traits::test_bool_trait_bool]:

tests/src/mutually-recursive-traits.lean.out

@@ -13,5 +13,5 @@ Called from Aeneas__Translate.extract_definitions.export_decl_group in file "Tra
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 886, characters 2-177
 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1018, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1652, characters 5-42
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1651, characters 5-42
 Called from Dune__exe__Main in file "Main.ml", line 493, characters 11-63