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.
-09043b10a0de68a87e55f8789cb98e1f16fe5b11
+6d0d40d01ecca97a3f064afb6ce346c152ce1cac

tests/coq/misc/DefaultedMethod.v

@@ -8,6 +8,83 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module DefaultedMethod.
 
+(** Trait declaration: [core::cmp::PartialEq]
+    Source: '/rustc/library/core/src/cmp.rs', lines 251:0-251:65
+    Name pattern: [core::cmp::PartialEq]
+    Visibility: public *)
+Record core_cmp_PartialEq_t (Self : Type) (Rhs : Type)
+  := mkcore_cmp_PartialEq_t {
+  core_cmp_PartialEq_t_eq : Self -> Rhs -> result bool;
+}.
+
+Arguments mkcore_cmp_PartialEq_t { _ } { _ }.
+Arguments core_cmp_PartialEq_t_eq { _ } { _ } _.
+
+(** Trait declaration: [core::cmp::Eq]
+    Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:58
+    Name pattern: [core::cmp::Eq]
+    Visibility: public *)
+Record core_cmp_Eq_t (Self : Type) := mkcore_cmp_Eq_t {
+  core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst : core_cmp_PartialEq_t Self Self;
+}.
+
+Arguments mkcore_cmp_Eq_t { _ }.
+Arguments core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst { _ } _.
+
+(** [core::cmp::Ordering]
+    Source: '/rustc/library/core/src/cmp.rs', lines 396:0-396:17
+    Name pattern: [core::cmp::Ordering]
+    Visibility: public *)
+Inductive core_cmp_Ordering_t :=
+| Core_cmp_Ordering_Less : core_cmp_Ordering_t
+| Core_cmp_Ordering_Equal : core_cmp_Ordering_t
+| Core_cmp_Ordering_Greater : core_cmp_Ordering_t
+.
+
+(** Trait declaration: [core::cmp::PartialOrd]
+    Source: '/rustc/library/core/src/cmp.rs', lines 1358:0-1359:41
+    Name pattern: [core::cmp::PartialOrd]
+    Visibility: public *)
+Record core_cmp_PartialOrd_t (Self : Type) (Rhs : Type)
+  := mkcore_cmp_PartialOrd_t {
+  core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst :
+    core_cmp_PartialEq_t Self Rhs;
+  core_cmp_PartialOrd_t_partial_cmp : Self -> Rhs -> result (option
+    core_cmp_Ordering_t);
+}.
+
+Arguments mkcore_cmp_PartialOrd_t { _ } { _ }.
+Arguments core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst { _ } { _ }
+  _.
+Arguments core_cmp_PartialOrd_t_partial_cmp { _ } { _ } _.
+
+(** Trait declaration: [core::cmp::Ord]
+    Source: '/rustc/library/core/src/cmp.rs', lines 973:0-973:73
+    Name pattern: [core::cmp::Ord]
+    Visibility: public *)
+Record core_cmp_Ord_t (Self : Type) := mkcore_cmp_Ord_t {
+  core_cmp_Ord_tcore_cmp_Ord_t_EqInst : core_cmp_Eq_t Self;
+  core_cmp_Ord_tcore_cmp_Ord_t_PartialOrdInst : core_cmp_PartialOrd_t Self
+    Self;
+  core_cmp_Ord_t_cmp : Self -> Self -> result core_cmp_Ordering_t;
+  core_cmp_Ord_t_min : Self -> Self -> result Self;
+}.
+
+Arguments mkcore_cmp_Ord_t { _ }.
+Arguments core_cmp_Ord_tcore_cmp_Ord_t_EqInst { _ } _.
+Arguments core_cmp_Ord_tcore_cmp_Ord_t_PartialOrdInst { _ } _.
+Arguments core_cmp_Ord_t_cmp { _ } _.
+Arguments core_cmp_Ord_t_min { _ } _.
+
+(** [core::cmp::Ord::min]:
+    Source: '/rustc/library/core/src/cmp.rs', lines 1064:4-1066:39
+    Name pattern: [core::cmp::Ord::min]
+    Visibility: public *)
+Axiom core_cmp_Ord_min_default :
+  forall{Self : Type} (ordInst : core_cmp_Ord_t Self),
+        Self -> Self -> result Self
+.
+
 (** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
     Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]

tests/fstar/misc/DefaultedMethod.fst

@@ -5,6 +5,58 @@ open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
+(** Trait declaration: [core::cmp::PartialEq]
+    Source: '/rustc/library/core/src/cmp.rs', lines 251:0-251:65
+    Name pattern: [core::cmp::PartialEq]
+    Visibility: public *)
+noeq type core_cmp_PartialEq_t (self : Type0) (rhs : Type0) = {
+  eq : self -> rhs -> result bool;
+}
+
+(** Trait declaration: [core::cmp::Eq]
+    Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:58
+    Name pattern: [core::cmp::Eq]
+    Visibility: public *)
+noeq type core_cmp_Eq_t (self : Type0) = {
+  partialEqInst : core_cmp_PartialEq_t self self;
+}
+
+(** [core::cmp::Ordering]
+    Source: '/rustc/library/core/src/cmp.rs', lines 396:0-396:17
+    Name pattern: [core::cmp::Ordering]
+    Visibility: public *)
+type core_cmp_Ordering_t =
+| Core_cmp_Ordering_Less : core_cmp_Ordering_t
+| Core_cmp_Ordering_Equal : core_cmp_Ordering_t
+| Core_cmp_Ordering_Greater : core_cmp_Ordering_t
+
+(** Trait declaration: [core::cmp::PartialOrd]
+    Source: '/rustc/library/core/src/cmp.rs', lines 1358:0-1359:41
+    Name pattern: [core::cmp::PartialOrd]
+    Visibility: public *)
+noeq type core_cmp_PartialOrd_t (self : Type0) (rhs : Type0) = {
+  partialEqInst : core_cmp_PartialEq_t self rhs;
+  partial_cmp : self -> rhs -> result (option core_cmp_Ordering_t);
+}
+
+(** Trait declaration: [core::cmp::Ord]
+    Source: '/rustc/library/core/src/cmp.rs', lines 973:0-973:73
+    Name pattern: [core::cmp::Ord]
+    Visibility: public *)
+noeq type core_cmp_Ord_t (self : Type0) = {
+  eqInst : core_cmp_Eq_t self;
+  partialOrdInst : core_cmp_PartialOrd_t self self;
+  cmp : self -> self -> result core_cmp_Ordering_t;
+  min : self -> self -> result self;
+}
+
+(** [core::cmp::Ord::min]:
+    Source: '/rustc/library/core/src/cmp.rs', lines 1064:4-1066:39
+    Name pattern: [core::cmp::Ord::min]
+    Visibility: public *)
+assume val core_cmp_Ord_min_default
+  (#self : Type0) (ordInst : core_cmp_Ord_t self) : self -> self -> result self
+
 (** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
     Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]

tests/lean/Closures.lean

@@ -12,8 +12,23 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace closures
 
+/-- [core::iter::traits::iterator::Iterator::map]:
+    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 789:4-792:34
+    Name pattern: [core::iter::traits::iterator::Iterator::map]
+    Visibility: public -/
+@[rust_fun "core::iter::traits::iterator::Iterator::map"]
+axiom core.iter.traits.iterator.Iterator.map.default
+  {Self : Type} {B : Type} {F : Type} {Clause0_Item : Type} (IteratorInst :
+  core.iter.traits.iterator.Iterator Self Clause0_Item)
+  (opsfunctionFnMutFTupleClause0_ItemBInst : core.ops.function.FnMut F
+  Clause0_Item B) :
+  Self → F → Result (core.iter.adapters.map.Map Self F)
+
 /-- [closures::call_fn_no_state::closure]
     Source: 'tests/src/closures.rs', lines 4:15-4:40 -/
 @[reducible]