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.
-df3b7fd4c1277827c92b4a2cb84347f1f54d92a6
+9d7c40aced38074cf874a0cff869442ecb067724

scripts/update-charon-pin.sh

@@ -12,9 +12,6 @@ else
     echo 'Pinning the latest commit from Charon `main`'
     nix flake lock --update-input charon
 fi
-# In both cases we also update the rust overlay to make sure we can get the
-# latest rust nightlies.
-nix flake lock --update-input charon/rust-overlay
 
 # Keep the commit revision in `./charon-pin` as well so that non-nix users can know which commit to use.
 echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin

tests/coq/hashmap/Hashmap_FunsExternal_Template.v

@@ -19,12 +19,4 @@ Axiom utils_deserialize : state -> result (state * (HashMap_t u64)).
     Source: 'tests/src/hashmap.rs', lines 326:4-328:5 *)
 Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit).
 
-(** [core::clone::Clone::clone_from]:
-    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),
-        Self -> Self -> state -> result (state * Self)
-.
-
 End Hashmap_FunsExternal_Template.

tests/coq/misc/External_FunsExternal_Template.v

@@ -28,12 +28,4 @@ Axiom core_cell_Cell_get_mut :
           (state * (core_cell_Cell_t T)))))
 .
 
-(** [core::clone::Clone::clone_from]:
-    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),
-        Self -> Self -> state -> result (state * Self)
-.
-
 End External_FunsExternal_Template.

tests/coq/traits/Traits.v

@@ -713,4 +713,10 @@ Definition TestType_test_TestTraittraitsTestTypetestTestType1 :
     testType_test_TestTraittraitsTestTypetestTestType1_test;
 |}.
 
+(** [traits::WithConstTy::LEN1]
+    Source: 'tests/src/traits.rs', lines 164:4-164:22 *)
+Axiom with_const_ty_len1 (Self : Type) (LEN : usize) : usize.
+(** [traits::Trait::LEN]
+    Source: 'tests/src/traits.rs', lines 313:4-313:21 *)
+Axiom trait_len (Self : Type) : usize.
 End Traits.

tests/fstar/hashmap/Hashmap.FunsExternal.fsti

@@ -14,10 +14,3 @@ val utils_deserialize : state -> result (state & (hashMap_t u64))
     Source: 'tests/src/hashmap.rs', lines 326:4-328:5 *)
 val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
 
-(** [core::clone::Clone::clone_from]:
-    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 -> self -> state -> result (state & self)
-

tests/fstar/misc/External.FunsExternal.fsti

@@ -21,10 +21,3 @@ val core_cell_Cell_get_mut
   core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> (state &
     (core_cell_Cell_t t)))))
 
-(** [core::clone::Clone::clone_from]:
-    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 -> self -> state -> result (state & self)
-

tests/fstar/traits/Traits.fst

@@ -535,3 +535,9 @@ let testType_test_TestTraittraitsTestTypetestTestType1 :
   test = testType_test_TestTraittraitsTestTypetestTestType1_test;
 }
 
+(** [traits::WithConstTy::LEN1]
+    Source: 'tests/src/traits.rs', lines 164:4-164:22 *)
+assume val with_const_ty_len1 (self : Type0) (len : usize) : usize
+(** [traits::Trait::LEN]
+    Source: 'tests/src/traits.rs', lines 313:4-313:21 *)
+assume val trait_len (self : Type0) : usize

tests/lean/Traits.lean

@@ -556,4 +556,10 @@ def TestType.test.TestTraittraitsTestTypetestTestType1 :
   test := TestType.test.TestTraittraitsTestTypetestTestType1.test
 }
 
+/- [traits::WithConstTy::LEN1]
+   Source: 'tests/src/traits.rs', lines 164:4-164:22 -/
+axiom WithConstTy.LEN1 (Self : Type) (LEN : Usize) : Usize
+/- [traits::Trait::LEN]
+   Source: 'tests/src/traits.rs', lines 313:4-313:21 -/
+axiom Trait.LEN (Self : Type) : Usize
 end traits