Bump Charon

backends/coq/Primitives.v

@@ -875,12 +875,8 @@ Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usi
   | Fail_ e => Fail_ e
   end.
 
-(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
-Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
-
 (* Trait declaration: [core::slice::index::SliceIndex] *)
 Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index_SliceIndex {
-  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_get : Self -> T -> result (option Output);
   core_slice_index_SliceIndex_get_mut :
     Self -> T -> result (option Output * (option Output -> T));
@@ -891,7 +887,6 @@ Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index
     Self -> T -> result (Output * (Output -> T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _ _}.
-Arguments core_slice_index_SliceIndex_sealedInst {_ _ _}.
 Arguments core_slice_index_SliceIndex_get {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _ _}.
@@ -958,14 +953,9 @@ Axiom core_array_Array_index_mut :
   (a : array T N) (i : Idx),
   result (Output * (Output -> array T N)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
-
 (* Trait implementation: [core::slice::index::Range] *)
 Definition core_slice_index_SliceIndexRangeUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_SliceIndexRangeUsizeSlice_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_SliceIndexRangeUsizeSlice_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked;
@@ -1026,14 +1016,9 @@ Axiom core_slice_index_usize_index : forall {T : Type}, usize -> slice T -> resu
 Axiom core_slice_index_usize_index_mut :
   forall {T : Type}, usize -> slice T -> result (T * (T -> slice T)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize := tt.
-
 (* Trait implementation: [core::slice::index::usize] *)
 Definition core_slice_index_SliceIndexUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) T := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked;

backends/fstar/Primitives.fst

@@ -804,12 +804,8 @@ let alloc_vec_Vec_push (#a  : Type0) (v : alloc_vec_Vec a) (x : a) :
 let alloc_vec_Vec_insert (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Ok (list_update v i x) else Fail Failure
 
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
 // Trait declaration: [core::slice::index::SliceIndex]
 noeq type core_slice_index_SliceIndex (self t output : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
   get : self → t → result (option output);
   get_mut : self → t → result (option output & (option output -> t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
@@ -882,14 +878,9 @@ let core_array_Array_index_mut
   result (out & (out -> array t n)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
 // Trait implementation: [core::slice::index::Range]
 let core_slice_index_SliceIndexRangeUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst;
   get = core_slice_index_SliceIndexRangeUsizeSlice_get #t;
   get_mut = core_slice_index_SliceIndexRangeUsizeSlice_get_mut #t;
   get_unchecked = core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked #t;
@@ -957,14 +948,9 @@ let core_slice_index_usize_index_mut (#t : Type0) :
   usize → slice t → result (t & (t -> slice t)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
 // Trait implementation: [core::slice::index::usize]
 let core_slice_index_SliceIndexUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex usize (slice t) t = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
   get = core_slice_index_usize_get #t;
   get_mut = core_slice_index_usize_get_mut #t;
   get_unchecked = core_slice_index_usize_get_unchecked #t;

backends/lean/Aeneas/Std/Slice.lean

@@ -334,12 +334,8 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
 def core.slice.Slice.reverse {T : Type} (s : Slice T) : Slice T :=
   ⟨ s.val.reverse, by scalar_tac ⟩
 
-@[rust_trait "core::slice::index::private_slice_index::Sealed"]
-structure core.slice.index.private_slice_index.Sealed (Self : Type) where
-
-@[rust_trait "core::slice::index::SliceIndex" (parentClauses := ["sealedInst"])]
+@[rust_trait "core::slice::index::SliceIndex"]
 structure core.slice.index.SliceIndex (Self T Output : Type) where
-  sealedInst : core.slice.index.private_slice_index.Sealed Self
   get : Self → T → Result (Option Output)
   get_mut : Self → T → Result (Option Output × (Option Output → T))
   get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output)
@@ -431,14 +427,9 @@ def core.slice.index.Slice.index_mut
   (s : Slice T) (i : I) : Result (Output × (Output → Slice T)) :=
   inst.index_mut i s
 
-@[rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeUsize
-  : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T], [@T]>"]
 def core.slice.index.SliceIndexRangeUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (Range Usize) (Slice T) (Slice T) := {
-  sealedInst := core.slice.index.private_slice_index.SealedRangeUsize
   get := core.slice.index.SliceIndexRangeUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeUsizeSlice.get_mut
   get_unchecked := core.slice.index.SliceIndexRangeUsizeSlice.get_unchecked
@@ -447,11 +438,6 @@ def core.slice.index.SliceIndexRangeUsizeSlice (T : Type) :
   index_mut := core.slice.index.SliceIndexRangeUsizeSlice.index_mut
 }
 
-@[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeTo<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeToUsize :
-  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeTo Usize)
-  := {}
-
 @[rust_fun "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, [@T], [@T]>}::get"]
 def core.slice.index.SliceIndexRangeToUsizeSlice.get
   {T : Type} (r : core.ops.range.RangeTo Usize) (s : Slice T) : Result (Option (Slice T)) :=
@@ -511,7 +497,6 @@ def core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
 def core.slice.index.SliceIndexRangeToUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (core.ops.range.RangeTo Usize) (Slice T) (Slice
   T) := {
-  sealedInst := core.slice.index.private_slice_index.SealedRangeToUsize
   get := core.slice.index.SliceIndexRangeToUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeToUsizeSlice.get_mut
   get_unchecked := core.slice.index.SliceIndexRangeToUsizeSlice.get_unchecked
@@ -566,14 +551,9 @@ abbrev core.slice.index.Usize.index_mut {T : Type}
   (i : Usize) (s : Slice T) : Result (T × (T → (Slice T))) :=
   Slice.index_mut_usize s i
 
-@[rust_trait_impl "core::slice::index::private_slice_index::Sealed<usize>"]
-def core.slice.index.private_slice_index.SealedUsize
-  : core.slice.index.private_slice_index.Sealed Usize := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<usize, [@T], @T>"]
 def core.slice.index.SliceIndexUsizeSlice (T : Type) :
   core.slice.index.SliceIndex Usize (Slice T) T := {
-  sealedInst := core.slice.index.private_slice_index.SealedUsize
   get := core.slice.index.Usize.get
   get_mut := core.slice.index.Usize.get_mut
   get_unchecked := core.slice.index.Usize.get_unchecked
@@ -655,16 +635,9 @@ theorem _SliceIndexRangeFromUsizeSlice.index_mut.test {T} (s : Slice T) (r : cor
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
   simp [h]
 
-@[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeFromUsize :
-  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeFrom Usize)
-  := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, [@T], [@T]>"]
 def core.slice.index.SliceIndexRangeFromUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (core.ops.range.RangeFrom Usize) (Slice T) (Slice T) := {
-  sealedInst :=
-    core.slice.index.private_slice_index.SealedRangeFromUsize
   get := core.slice.index.SliceIndexRangeFromUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeFromUsizeSlice.get_mut
   get_unchecked :=

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.
-f5208b1c4ce287898a1fc015d41a20da3baf0974
+f5a61c8f2cb695213b427ab696f8088f357b5dea

src/extract/ExtractBuiltin.ml

@@ -299,11 +299,8 @@ let builtin_trait_decls_info () =
       (* IndexMut *)
       mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ "indexInst" ]
         ~methods:[ "index_mut" ] ();
-      (* Sealed *)
-      mk_trait "core::slice::index::private_slice_index::Sealed" ();
       (* SliceIndex *)
-      mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ "sealedInst" ]
-        ~types:[ "Output" ]
+      mk_trait "core::slice::index::SliceIndex" ~types:[ "Output" ]
         ~methods:
           [
             "get";
@@ -374,11 +371,6 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
       (* core::ops::index::IndexMut<[T], I> *)
       fmt "core::ops::index::IndexMut<[@T], @I, @O>"
         ~extract_name:(Some "core::ops::index::IndexMutSliceInst") ();
-      (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
-      fmt
-        "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
-        ~extract_name:
-          (Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") ();
       (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
       fmt
         "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T], \
@@ -391,10 +383,6 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
       (* core::ops::index::IndexMut<[T; N], I> *)
       fmt "core::ops::index::IndexMut<[@T; @N], @I, @O>"
         ~extract_name:(Some "core::ops::index::IndexMutArrayInst") ();
-      (* core::slice::index::private_slice_index::Sealed<usize> *)
-      fmt "core::slice::index::private_slice_index::Sealed<usize>"
-        ~extract_name:
-          (Some "core::slice::index::private_slice_index::SealedUsizeInst") ();
       (* core::slice::index::SliceIndex<usize, [T]> *)
       fmt "core::slice::index::SliceIndex<usize, [@T], @T>"
         ~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceInst") ();