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.
-5c2ae3744ce702d07920d0f536a272aadd396ed9
+944e91f5fcbed9e6b923c26b12580bf5522f7aee

tests/coq/arrays/Arrays.v

@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'tests/src/arrays.rs', lines 28:0-28:40 *)
 Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T true s1)
 .
 
 (** [arrays::shared_array_len]:
     Source: 'tests/src/arrays.rs', lines 32:0-32:48 *)
 Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T true s1)
 .
 
 (** [arrays::shared_slice_len]:
     Source: 'tests/src/arrays.rs', lines 36:0-36:44 *)
 Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
-  Ok (slice_len T s)
+  Ok (slice_len T true s)
 .
 
 (** [arrays::index_array_shared]:
@@ -382,7 +382,7 @@ Fixpoint sum_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 s in
+    let i1 := slice_len u32 true s in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 s i;
@@ -408,7 +408,7 @@ Fixpoint sum2_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 s in
+    let i1 := slice_len u32 true s in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 s i;
@@ -424,8 +424,8 @@ Fixpoint sum2_loop
 (** [arrays::sum2]:
     Source: 'tests/src/arrays.rs', lines 255:0-255:41 *)
 Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
-  let i := slice_len u32 s in
-  let i1 := slice_len u32 s2 in
+  let i := slice_len u32 true s in
+  let i1 := slice_len u32 true s2 in
   if i s= i1 then sum2_loop n s s2 0%u32 0%usize else Fail_ Failure
 .
 
@@ -528,7 +528,7 @@ Fixpoint zero_slice_loop
 (** [arrays::zero_slice]:
     Source: 'tests/src/arrays.rs', lines 306:0-306:31 *)
 Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+  let len := slice_len u8 true a in zero_slice_loop n a 0%usize len
 .
 
 (** [arrays::iter_mut_slice]: loop 0:
@@ -547,7 +547,9 @@ Fixpoint iter_mut_slice_loop
 (** [arrays::iter_mut_slice]:
     Source: 'tests/src/arrays.rs', lines 315:0-315:35 *)
 Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Ok a
+  let len := slice_len u8 true a in
+  _ <- iter_mut_slice_loop n len 0%usize;
+  Ok a
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
@@ -557,7 +559,7 @@ Fixpoint sum_mut_slice_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 a in
+    let i1 := slice_len u32 true a in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 a i;

tests/coq/betree/Betree_Funs.v

@@ -169,15 +169,17 @@ Definition betree_List_split_at
     Source: 'src/betree.rs', lines 315:4-315:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
-  let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  let (tl, _) := core_mem_replace (betree_List_t T) true self Betree_List_Nil
+    in
   Ok (Betree_List_Cons x tl)
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 322:4-322:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
-  let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  let (ls, _) := core_mem_replace (betree_List_t T) true self Betree_List_Nil
+    in
   match ls with
   | Betree_List_Cons x tl => Ok (x, tl)
   | Betree_List_Nil => Fail_ Failure
@@ -370,7 +372,7 @@ Fixpoint betree_Node_apply_upserts_loop
         betree_Node_apply_upserts_loop n1 msgs1 (Some v) key
       end)
     else (
-      v <- core_option_Option_unwrap u64 prev;
+      v <- core_option_Option_unwrap u64 true prev;
       msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);

tests/coq/hashmap/Hashmap_Funs.v

@@ -229,7 +229,7 @@ Fixpoint hashMap_move_elements_loop
         alloc_vec_Vec_index_mut (AList_t T) usize
           (core_slice_index_SliceIndexUsizeSliceTInst (AList_t T)) slots i;
       let (a, index_mut_back) := p in
-      let (ls, a1) := core_mem_replace (AList_t T) a AList_Nil in
+      let (ls, a1) := core_mem_replace (AList_t T) true a AList_Nil in
       ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back a1;
@@ -467,7 +467,7 @@ Fixpoint hashMap_remove_from_list_loop
       if ckey s= key
       then
         let (mv_ls, _) :=
-          core_mem_replace (AList_t T) (AList_Cons ckey t tl) AList_Nil in
+          core_mem_replace (AList_t T) true (AList_Cons ckey t tl) AList_Nil in
         match mv_ls with
         | AList_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
         | AList_Nil => Fail_ Failure

tests/coq/misc/External_FunsExternal_Template.v

@@ -12,15 +12,15 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::cell::{core::cell::Cell<T>#10}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 510:4-510:26
+    Source: '/rustc/library/core/src/cell.rs', lines 509:4-509:26
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 Axiom core_cell_Cell_get :
   forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
         core_cell_Cell_t T -> state -> result (state * T)
 .
 
 (** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 588:4-588:39
+    Source: '/rustc/library/core/src/cell.rs', lines 587:4-587:39
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 Axiom core_cell_Cell_get_mut :
   forall(T : Type),

tests/coq/misc/NoNestedBorrows.v

@@ -322,7 +322,7 @@ Fixpoint list_rev_aux
 (** [no_nested_borrows::list_rev]:
     Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *)
 Definition list_rev (T : Type) (l : List_t T) : result (List_t T) :=
-  let (li, _) := core_mem_replace (List_t T) l List_Nil in
+  let (li, _) := core_mem_replace (List_t T) true l List_Nil in
   list_rev_aux T li List_Nil
 .
 
@@ -485,7 +485,7 @@ Check (test_weird_borrows1 )%return.
 (** [no_nested_borrows::test_mem_replace]:
     Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *)
 Definition test_mem_replace (px : u32) : result u32 :=
-  let (y, _) := core_mem_replace u32 px 1%u32 in
+  let (y, _) := core_mem_replace u32 true px 1%u32 in
   if y s= 0%u32 then Ok 2%u32 else Fail_ Failure
 .
 

tests/fstar/arrays/Arrays.Funs.fst

@@ -28,17 +28,17 @@ let array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'tests/src/arrays.rs', lines 28:0-28:40 *)
 let array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in Ok (slice_len t s1)
+  let* s1 = array_to_slice t 32 s in Ok (slice_len t true s1)
 
 (** [arrays::shared_array_len]:
     Source: 'tests/src/arrays.rs', lines 32:0-32:48 *)
 let shared_array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in Ok (slice_len t s1)
+  let* s1 = array_to_slice t 32 s in Ok (slice_len t true s1)
 
 (** [arrays::shared_slice_len]:
     Source: 'tests/src/arrays.rs', lines 36:0-36:44 *)
 let shared_slice_len (t : Type0) (s : slice t) : result usize =
-  Ok (slice_len t s)
+  Ok (slice_len t true s)
 
 (** [arrays::index_array_shared]:
     Source: 'tests/src/arrays.rs', lines 40:0-40:57 *)
@@ -312,7 +312,7 @@ let rec sum_loop
   (s : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum_loop_decreases s sum1 i))
   =
-  let i1 = slice_len u32 s in
+  let i1 = slice_len u32 true s in
   if i < i1
   then
     let* i2 = slice_index_usize u32 s i in
@@ -332,7 +332,7 @@ let rec sum2_loop
   (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum2_loop_decreases s s2 sum1 i))
   =
-  let i1 = slice_len u32 s in
+  let i1 = slice_len u32 true s in
   if i < i1
   then
     let* i2 = slice_index_usize u32 s i in
@@ -346,8 +346,8 @@ let rec sum2_loop
 (** [arrays::sum2]:
     Source: 'tests/src/arrays.rs', lines 255:0-255:41 *)
 let sum2 (s : slice u32) (s2 : slice u32) : result u32 =
-  let i = slice_len u32 s in
-  let i1 = slice_len u32 s2 in
+  let i = slice_len u32 true s in
+  let i1 = slice_len u32 true s2 in
   if i = i1 then sum2_loop s s2 0 0 else Fail Failure
 
 (** [arrays::f0]:
@@ -431,7 +431,7 @@ let rec zero_slice_loop
 (** [arrays::zero_slice]:
     Source: 'tests/src/arrays.rs', lines 306:0-306:31 *)
 let zero_slice (a : slice u8) : result (slice u8) =
-  let len = slice_len u8 a in zero_slice_loop a 0 len
+  let len = slice_len u8 true a in zero_slice_loop a 0 len
 
 (** [arrays::iter_mut_slice]: loop 0:
     Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
@@ -446,15 +446,15 @@ let rec iter_mut_slice_loop
 (** [arrays::iter_mut_slice]:
     Source: 'tests/src/arrays.rs', lines 315:0-315:35 *)
 let iter_mut_slice (a : slice u8) : result (slice u8) =
-  let len = slice_len u8 a in let* _ = iter_mut_slice_loop len 0 in Ok a
+  let len = slice_len u8 true a in let* _ = iter_mut_slice_loop len 0 in Ok a
 
 (** [arrays::sum_mut_slice]: loop 0:
     Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
 let rec sum_mut_slice_loop
   (a : slice u32) (i : usize) (s : u32) :
   Tot (result u32) (decreases (sum_mut_slice_loop_decreases a i s))
   =
-  let i1 = slice_len u32 a in
+  let i1 = slice_len u32 true a in
   if i < i1
   then
     let* i2 = slice_index_usize u32 a i in

tests/fstar/betree/Betree.Funs.fst

@@ -140,14 +140,14 @@ let betree_List_split_at
     Source: 'src/betree.rs', lines 315:4-315:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
-  let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+  let (tl, _) = core_mem_replace (betree_List_t t) true self Betree_List_Nil in
   Ok (Betree_List_Cons x tl)
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 322:4-322:32 *)
 let betree_List_pop_front
   (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
-  let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+  let (ls, _) = core_mem_replace (betree_List_t t) true self Betree_List_Nil in
   begin match ls with
   | Betree_List_Cons x tl -> Ok (x, tl)
   | Betree_List_Nil -> Fail Failure
@@ -304,7 +304,7 @@ let rec betree_Node_apply_upserts_loop
       betree_Node_apply_upserts_loop msgs1 (Some v) key
     end
   else
-    let* v = core_option_Option_unwrap u64 prev in
+    let* v = core_option_Option_unwrap u64 true prev in
     let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in

tests/fstar/hashmap/Hashmap.Funs.fst

@@ -169,7 +169,7 @@ let rec hashMap_move_elements_loop
     let* (a, index_mut_back) =
       alloc_vec_Vec_index_mut (aList_t t) usize
         (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) slots i in
-    let (ls, a1) = core_mem_replace (aList_t t) a AList_Nil in
+    let (ls, a1) = core_mem_replace (aList_t t) true a AList_Nil in
     let* ntable1 = hashMap_move_elements_from_list t ntable ls in
     let* i2 = usize_add i 1 in
     let* slots1 = index_mut_back a1 in
@@ -344,7 +344,7 @@ let rec hashMap_remove_from_list_loop
     if ckey = key
     then
       let (mv_ls, _) =
-        core_mem_replace (aList_t t) (AList_Cons ckey x tl) AList_Nil in
+        core_mem_replace (aList_t t) true (AList_Cons ckey x tl) AList_Nil in
       begin match mv_ls with
       | AList_Cons _ cvalue tl1 -> Ok (Some cvalue, tl1)
       | AList_Nil -> Fail Failure

tests/fstar/misc/External.FunsExternal.fsti

@@ -7,14 +7,14 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::{core::cell::Cell<T>#10}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 510:4-510:26
+    Source: '/rustc/library/core/src/cell.rs', lines 509:4-509:26
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 val core_cell_Cell_get
   (t : Type0) (markerCopyInst : core_marker_Copy_t t) :
   core_cell_Cell_t t -> state -> result (state & t)
 
 (** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 588:4-588:39
+    Source: '/rustc/library/core/src/cell.rs', lines 587:4-587:39
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 val core_cell_Cell_get_mut
   (t : Type0) :

tests/fstar/misc/NoNestedBorrows.fst

@@ -271,7 +271,7 @@ let rec list_rev_aux
 (** [no_nested_borrows::list_rev]:
     Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *)
 let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
-  let (li, _) = core_mem_replace (list_t t) l List_Nil in
+  let (li, _) = core_mem_replace (list_t t) true l List_Nil in
   list_rev_aux t li List_Nil
 
 (** [no_nested_borrows::test_list_functions]:
@@ -404,7 +404,7 @@ let _ = assert_norm (test_weird_borrows1 = Ok ())
 (** [no_nested_borrows::test_mem_replace]:
     Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *)
 let test_mem_replace (px : u32) : result u32 =
-  let (y, _) = core_mem_replace u32 px 1 in
+  let (y, _) = core_mem_replace u32 true px 1 in
   if y = 0 then Ok 2 else Fail Failure
 
 (** [no_nested_borrows::test_shared_borrow_bool1]: