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.
-42836b36b666a980cbc9d438a8aed340ad3b848b
+65dcdb566e05472a6bca8074318c05f729e30177

scripts/make-charon-companion-pr.sh

@@ -11,6 +11,8 @@ BRANCH_PREFIX="${BRANCH_PREFIX:-update-charon}"
 COMMIT_TITLE="Update charon"
 MERGE_QUEUE_POLL_SECONDS="${MERGE_QUEUE_POLL_SECONDS:-30}"
 MERGE_QUEUE_WAIT_TIMEOUT_SECONDS="${MERGE_QUEUE_WAIT_TIMEOUT_SECONDS:-3600}"
+PR_CHECKS_POLL_SECONDS="${PR_CHECKS_POLL_SECONDS:-30}"
+PR_CHECKS_WAIT_TIMEOUT_SECONDS="${PR_CHECKS_WAIT_TIMEOUT_SECONDS:-1800}"
 
 die() {
     echo "error: $*" >&2
@@ -292,6 +294,59 @@ rerun_pr_job() {
     return 1
 }
 
+wait_for_pr_checks_complete() {
+    local repo="$1"
+    local pr="$2"
+    local waited=0
+    local checks_json pending_count total_count pending_names
+
+    while true; do
+        checks_json="$(gh pr checks "$pr" --repo "$repo" --json name,bucket,state 2>/dev/null || true)"
+
+        if ! jq -e 'type == "array"' >/dev/null <<<"$checks_json"; then
+            die "could not inspect checks for $repo PR #$pr"
+        fi
+
+        total_count="$(jq -r 'length' <<<"$checks_json")" ||
+            die "could not parse checks for $repo PR #$pr"
+        pending_count="$(
+            jq -r '[.[] | select(.bucket == "pending")] | length' <<<"$checks_json"
+        )" || die "could not parse pending checks for $repo PR #$pr"
+
+        if (( pending_count == 0 )); then
+            if (( total_count == 0 )); then
+                echo "No checks found on $repo PR #$pr"
+            else
+                echo "All checks on $repo PR #$pr are complete"
+            fi
+            return 0
+        fi
+
+        if (( waited >= PR_CHECKS_WAIT_TIMEOUT_SECONDS )); then
+            pending_names="$(
+                jq -r '[.[] | select(.bucket == "pending") | .name] | join(", ")' \
+                    <<<"$checks_json"
+            )" || pending_names="unknown"
+            die "timed out waiting for $repo PR #$pr checks to complete: $pending_names"
+        fi
+
+        pending_names="$(
+            jq -r '[.[] | select(.bucket == "pending") | .name] | join(", ")' \
+                <<<"$checks_json"
+        )" || pending_names="unknown"
+        echo "Waiting for $repo PR #$pr checks to complete ($pending_count pending): $pending_names"
+        sleep "$PR_CHECKS_POLL_SECONDS"
+        waited=$((waited + PR_CHECKS_POLL_SECONDS))
+    done
+}
+
+rerun_charon_pin_is_merged_job() {
+    local pr="$1"
+
+    wait_for_pr_checks_complete "$THIS_REPO" "$pr"
+    rerun_pr_job "$THIS_REPO" "$pr" "charon-pin-is-merged"
+}
+
 require_cmd git
 require_cmd gh
 require_cmd jq
@@ -396,16 +451,16 @@ fi
 
 if pr_is_merged "$CHARON_REPO" "$charon_pr"; then
     echo "Charon PR #$charon_pr is merged; rerunning $THIS_REPO_NAME job 'charon-pin-is-merged'"
-    rerun_pr_job "$THIS_REPO" "$this_pr" "charon-pin-is-merged"
+    rerun_charon_pin_is_merged_job "$this_pr"
 elif pr_is_in_merge_queue "$CHARON_REPO" "$charon_pr"; then
     echo "Charon PR #$charon_pr is in the merge queue"
     wait_for_pr_merged "$CHARON_REPO" "$charon_pr"
-    rerun_pr_job "$THIS_REPO" "$this_pr" "charon-pin-is-merged"
+    rerun_charon_pin_is_merged_job "$this_pr"
 else
     ensure_charon_pr_mentions_this_pr "$charon_pr" "$this_pr"
     if ! rerun_pr_job "$CHARON_REPO" "$charon_pr" "select-dep-versions"; then
         echo "Continuing to wait for $CHARON_REPO PR #$charon_pr to merge"
     fi
     wait_for_pr_merged "$CHARON_REPO" "$charon_pr" false
-    rerun_pr_job "$THIS_REPO" "$this_pr" "charon-pin-is-merged"
+    rerun_charon_pin_is_merged_job "$this_pr"
 fi

src/PrePasses.ml

@@ -1313,7 +1313,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl =
                           kind =
                             Assign
                               ( { kind = PlaceLocal local_id; ty = str_ty },
-                                Use (Constant new_cv) );
+                                Use (Constant new_cv, NoRetag) );
                           comments_before = [];
                         }
                       in
@@ -2008,7 +2008,7 @@ let simplify_trait_calls (crate : crate) : crate =
             if is_blanket_into_iter d.item_meta.name then (
               (* Replace the call by an assignment *)
               [%sanity_check] span (List.length call.args = 1);
-              let arg = Use (List.hd call.args) in
+              let arg = Use (List.hd call.args, NoRetag) in
               Assign (call.dest, arg))
             else if is_blanket_try_into d.item_meta.name then (
               [%ldebug

src/interp/InterpExpressions.ml

@@ -1428,7 +1428,7 @@ let eval_rvalue_not_global (config : config) (span : Meta.span)
   let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> wrap_in_result (eval_operand config span op ctx)
+  | Use (op, _) -> wrap_in_result (eval_operand config span op ctx)
   | RvRef (p, bkind, _) ->
       wrap_in_result (eval_rvalue_ref config span p bkind ctx)
   | UnaryOp (unop, op) -> eval_unary_op config span unop op ctx

src/interp/InterpUtils.ml

@@ -439,8 +439,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut span (ctx : eval_ctx)
     compute span-data, to find pretty names. *)
 let rvalue_get_place (rv : rvalue) : place option =
   match rv with
-  | Use (Copy p | Move p) -> Some p
-  | Use (Constant _) -> None
+  | Use ((Copy p | Move p), _) -> Some p
+  | Use (Constant _, _) -> None
   | Len (p, _, _) | RvRef (p, _, _) | RawPtr (p, _, _) -> Some p
   | NullaryOp _
   | UnaryOp _

src/llbc/FunsAnalysis.ml

@@ -109,7 +109,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) :
 
           method! visit_rvalue env rv =
             match rv with
-            | Use (Constant { kind = CTraitConst _; _ }) ->
+            | Use (Constant { kind = CTraitConst _; _ }, _) ->
                 (* We consider that trait constants can fail, similarly to
                    trait methods. *)
                 self#may_fail true

tests/coq/demo/Demo.v

@@ -9,13 +9,13 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2583:8-2583:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32.
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2620:8-2620:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.

tests/coq/misc/DefaultedMethod.v

@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module DefaultedMethod.
 
 (** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
+    Source: '/rustc/library/core/src/cmp.rs', lines 2008:12-2008:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
     Visibility: public *)
 Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32.

tests/fstar/demo/Demo.fst

@@ -6,13 +6,13 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2583:8-2583:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2620:8-2620:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32

tests/fstar/misc/DefaultedMethod.fst

@@ -6,7 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
+    Source: '/rustc/library/core/src/cmp.rs', lines 2008:12-2008:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
     Visibility: public *)
 assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32

tests/lean/BuiltinAuto.lean

@@ -18,7 +18,7 @@ noncomputable section
 namespace builtin_auto
 
 /-- [core::ptr::null]:
-    Source: '/rustc/library/core/src/ptr/mod.rs', lines 842:0-842:55
+    Source: '/rustc/library/core/src/ptr/mod.rs', lines 854:0-854:55
     Name pattern: [core::ptr::null]
     Visibility: public -/
 @[rust_fun "core::ptr::null"]

tests/lean/Derive.lean

@@ -18,14 +18,14 @@ noncomputable section
 namespace derive
 
 /-- [core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}::ne]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1879:16-1879:50
+    Source: '/rustc/library/core/src/cmp.rs', lines 1880:16-1880:50
     Name pattern: [core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne]
     Visibility: public -/
 @[rust_fun "core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne"]
 axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool
 
 /-- [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<T>> for alloc::boxed::Box<T>}::ne]:
-    Source: '/rustc/library/alloc/src/boxed.rs', lines 2109:4-2109:38
+    Source: '/rustc/library/alloc/src/boxed.rs', lines 2127:4-2127:38
     Name pattern: [alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne]
     Visibility: public -/
 @[rust_fun "alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne"]

tests/lean/DropBug.lean

@@ -18,13 +18,21 @@ noncomputable section
 namespace drop_bug
 
 /-- Trait declaration: [core::ops::drop::Drop]
-    Source: '/rustc/library/core/src/ops/drop.rs', lines 207:0-207:20
+    Source: '/rustc/library/core/src/ops/drop.rs', lines 209:0-209:20
     Name pattern: [core::ops::drop::Drop]
     Visibility: public -/
 @[rust_trait "core::ops::drop::Drop"]
 structure core.ops.drop.Drop (Self : Type) where
   drop : Self → Result Self
 
+/-- [core::ops::drop::Drop::drop]:
+    Source: '/rustc/library/core/src/ops/drop.rs', lines 243:4-243:22
+    Name pattern: [core::ops::drop::Drop::drop]
+    Visibility: public -/
+@[rust_fun "core::ops::drop::Drop::drop"]
+axiom core.ops.drop.Drop.drop.default
+  {Self : Type} (DropInst : core.ops.drop.Drop Self) : Self → Result Self
+
 /-- [drop_bug::wipe_slice]:
     Source: 'tests/src/drop_bug.rs', lines 20:0-24:1 -/
 axiom wipe_slice {T : Type} : Slice T → Result (Slice T)

tests/lean/Issue804ClosureReturnRef.lean

@@ -18,7 +18,7 @@ noncomputable section
 namespace issue_804_closure_return_ref
 
 /-- [core::array::from_fn]:
-    Source: '/rustc/library/core/src/array/mod.rs', lines 109:0-111:52
+    Source: '/rustc/library/core/src/array/mod.rs', lines 110:0-112:52
     Name pattern: [core::array::from_fn]
     Visibility: public -/
 @[rust_fun "core::array::from_fn"]

tests/lean/Iterators.lean

@@ -18,14 +18,14 @@ noncomputable section
 namespace iterators
 
 /-- [core::iter::adapters::zip::Zip]
-    Source: '/rustc/library/core/src/iter/adapters/zip.rs', lines 15:0-15:20
+    Source: '/rustc/library/core/src/iter/adapters/zip.rs', lines 13:0-13:20
     Name pattern: [core::iter::adapters::zip::Zip]
     Visibility: public -/
 @[rust_type "core::iter::adapters::zip::Zip"]
 axiom core.iter.adapters.zip.Zip (A : Type) (B : Type) : Type
 
 /-- [core::iter::adapters::zip::{impl core::iter::traits::iterator::Iterator<(Clause0_Item, Clause1_Item)> for core::iter::adapters::zip::Zip<A, B>}::next]:
-    Source: '/rustc/library/core/src/iter/adapters/zip.rs', lines 84:4-84:44
+    Source: '/rustc/library/core/src/iter/adapters/zip.rs', lines 82:4-82:44
     Name pattern: [core::iter::adapters::zip::{core::iter::traits::iterator::Iterator<core::iter::adapters::zip::Zip<@A, @B>, (@Clause0_Item, @Clause1_Item)>}::next]
     Visibility: public -/
 @[rust_fun
@@ -52,7 +52,7 @@ axiom core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.zip
     (core.ops.range.Range A) Clause1_IntoIter)
 
 /-- [core::iter::traits::iterator::Iterator::zip]:
-    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 631:4-634:24
+    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 629:4-632:24
     Name pattern: [core::iter::traits::iterator::Iterator::zip]
     Visibility: public -/
 @[rust_fun "core::iter::traits::iterator::Iterator::zip"]

tests/lean/Order.lean

@@ -77,12 +77,20 @@ def Wrap.Insts.CoreCmpEq : core.cmp.Eq Wrap := {
   assert_fields_are_eq := Wrap.Insts.CoreCmpEq.assert_fields_are_eq
 }
 
+/-- [order::{impl core::cmp::Ord for order::Wrap}::cmp]:
+    Source: 'tests/src/order.rs', lines 21:36-21:39
+    Visibility: public -/
+def Wrap.Insts.CoreCmpOrd.cmp
+  (self : Wrap) (other : Wrap) : Result Ordering := do
+  ok (core.cmp.impls.OrdU64.cmp self other)
+
 /-- [order::{impl core::cmp::PartialOrd<order::Wrap> for order::Wrap}::partial_cmp]:
     Source: 'tests/src/order.rs', lines 21:24-21:34
     Visibility: public -/
 def Wrap.Insts.CoreCmpPartialOrdWrap.partial_cmp
   (self : Wrap) (other : Wrap) : Result (Option Ordering) := do
-  ok (core.cmp.impls.PartialOrdU64.partial_cmp self other)
+  let o ← Wrap.Insts.CoreCmpOrd.cmp self other
+  ok (some o)
 
 /-- Trait implementation: [order::{impl core::cmp::PartialOrd<order::Wrap> for order::Wrap}]
     Source: 'tests/src/order.rs', lines 21:24-21:34 -/
@@ -92,13 +100,6 @@ def Wrap.Insts.CoreCmpPartialOrdWrap : core.cmp.PartialOrd Wrap Wrap := {
   partial_cmp := Wrap.Insts.CoreCmpPartialOrdWrap.partial_cmp
 }
 
-/-- [order::{impl core::cmp::Ord for order::Wrap}::cmp]:
-    Source: 'tests/src/order.rs', lines 21:36-21:39
-    Visibility: public -/
-def Wrap.Insts.CoreCmpOrd.cmp
-  (self : Wrap) (other : Wrap) : Result Ordering := do
-  ok (core.cmp.impls.OrdU64.cmp self other)
-
 /-- Trait implementation: [order::{impl core::cmp::Ord for order::Wrap}]
     Source: 'tests/src/order.rs', lines 21:36-21:39 -/
 @[reducible]

tests/lean/RustBorrowCheckIssues.lean

@@ -25,7 +25,7 @@ namespace rust_borrow_check_issues
 axiom core.mem.drop {T : Type} : T → Result Unit
 
 /-- [core::option::{core::option::Option<T>}::as_mut]:
-    Source: '/rustc/library/core/src/option.rs', lines 766:4-766:52
+    Source: '/rustc/library/core/src/option.rs', lines 763:4-763:52
     Name pattern: [core::option::{core::option::Option<@T>}::as_mut]
     Visibility: public -/
 @[rust_fun "core::option::{core::option::Option<@T>}::as_mut"]