From 8a0bdc7177ce6dc0a04a63d8966a31a9cd7a6b94 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 1 Jun 2026 13:10:42 +0200 Subject: [PATCH 1/2] Update charon --- charon-pin | 2 +- flake.lock | 14 +++++++------- src/PrePasses.ml | 4 ++-- src/interp/InterpExpressions.ml | 2 +- src/interp/InterpUtils.ml | 4 ++-- src/llbc/FunsAnalysis.ml | 2 +- tests/coq/demo/Demo.v | 4 ++-- tests/coq/misc/DefaultedMethod.v | 2 +- tests/fstar/demo/Demo.fst | 4 ++-- tests/fstar/misc/DefaultedMethod.fst | 2 +- tests/lean/BuiltinAuto.lean | 2 +- tests/lean/Derive.lean | 4 ++-- tests/lean/DropBug.lean | 10 +++++++++- tests/lean/Issue804ClosureReturnRef.lean | 2 +- tests/lean/Iterators.lean | 6 +++--- tests/lean/Order.lean | 17 +++++++++-------- tests/lean/RustBorrowCheckIssues.lean | 2 +- 17 files changed, 46 insertions(+), 37 deletions(-) diff --git a/charon-pin b/charon-pin index ca309b005..6f20ce68d 100644 --- a/charon-pin +++ b/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 diff --git a/flake.lock b/flake.lock index 37ae0ed51..c45ac1661 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1780248582, - "narHash": "sha256-zzh6JL6Boun4OFBSndfSM+5aZJUXfVNaYgePxIszBOA=", + "lastModified": 1780311953, + "narHash": "sha256-YEbUYbgdW1BddC9xxqOF0W2kaWLRrA/5IjxUn0sVJ04=", "owner": "aeneasverif", "repo": "charon", - "rev": "42836b36b666a980cbc9d438a8aed340ad3b848b", + "rev": "65dcdb566e05472a6bca8074318c05f729e30177", "type": "github" }, "original": { @@ -158,17 +158,17 @@ ] }, "locked": { - "lastModified": 1780024773, - "narHash": "sha256-aU9nlrS9S+IJ2EiCzsaxzOXUhggogqTrJojBicE6Oeg=", + "lastModified": 1780284119, + "narHash": "sha256-y2wR4Mk6D/N1ID4FZa2oUMStCUxyIoRzmgOOpLzoWmo=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63", + "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e", "type": "github" }, "original": { "owner": "oxalica", "repo": "rust-overlay", - "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63", + "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e", "type": "github" } }, diff --git a/src/PrePasses.ml b/src/PrePasses.ml index 0115ab64e..dc0ab803c 100644 --- a/src/PrePasses.ml +++ b/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 diff --git a/src/interp/InterpExpressions.ml b/src/interp/InterpExpressions.ml index b4c4b0042..45fddae6e 100644 --- a/src/interp/InterpExpressions.ml +++ b/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 diff --git a/src/interp/InterpUtils.ml b/src/interp/InterpUtils.ml index cff80b1fc..764af6eba 100644 --- a/src/interp/InterpUtils.ml +++ b/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 _ diff --git a/src/llbc/FunsAnalysis.ml b/src/llbc/FunsAnalysis.ml index 657e15862..a2678ba12 100644 --- a/src/llbc/FunsAnalysis.ml +++ b/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 diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index 5b19636e0..ac8debe2c 100644 --- a/tests/coq/demo/Demo.v +++ b/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. diff --git a/tests/coq/misc/DefaultedMethod.v b/tests/coq/misc/DefaultedMethod.v index e8e57dad6..2bff5e941 100644 --- a/tests/coq/misc/DefaultedMethod.v +++ b/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}::min] Visibility: public *) Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32. diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index b9a40dbcf..b9c77846f 100644 --- a/tests/fstar/demo/Demo.fst +++ b/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 diff --git a/tests/fstar/misc/DefaultedMethod.fst b/tests/fstar/misc/DefaultedMethod.fst index ed722d32e..1c46a357a 100644 --- a/tests/fstar/misc/DefaultedMethod.fst +++ b/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}::min] Visibility: public *) assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32 diff --git a/tests/lean/BuiltinAuto.lean b/tests/lean/BuiltinAuto.lean index 7b2e5da9a..674dd52f2 100644 --- a/tests/lean/BuiltinAuto.lean +++ b/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"] diff --git a/tests/lean/Derive.lean b/tests/lean/Derive.lean index 3fb96ffac..cdca874f7 100644 --- a/tests/lean/Derive.lean +++ b/tests/lean/Derive.lean @@ -18,14 +18,14 @@ noncomputable section namespace derive /-- [core::cmp::impls::{impl core::cmp::PartialEq 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}::ne] Visibility: public -/ @[rust_fun "core::cmp::impls::{core::cmp::PartialEq}::ne"] axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool /-- [alloc::boxed::{impl core::cmp::PartialEq> for alloc::boxed::Box}::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>>}::ne] Visibility: public -/ @[rust_fun "alloc::boxed::{core::cmp::PartialEq, Box<@T>>}::ne"] diff --git a/tests/lean/DropBug.lean b/tests/lean/DropBug.lean index 45da5f3ca..450aeadaf 100644 --- a/tests/lean/DropBug.lean +++ b/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) diff --git a/tests/lean/Issue804ClosureReturnRef.lean b/tests/lean/Issue804ClosureReturnRef.lean index ef9ef24bb..023c657f9 100644 --- a/tests/lean/Issue804ClosureReturnRef.lean +++ b/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"] diff --git a/tests/lean/Iterators.lean b/tests/lean/Iterators.lean index 3d0f64099..ccf8b3ac5 100644 --- a/tests/lean/Iterators.lean +++ b/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}::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, (@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"] diff --git a/tests/lean/Order.lean b/tests/lean/Order.lean index 4040455b6..ad3a94ea2 100644 --- a/tests/lean/Order.lean +++ b/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 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 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] diff --git a/tests/lean/RustBorrowCheckIssues.lean b/tests/lean/RustBorrowCheckIssues.lean index 2bd16c6f5..c2d0c0cc1 100644 --- a/tests/lean/RustBorrowCheckIssues.lean +++ b/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}::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"] From daf8a2fd36a9e9bf3defefdb924ece3a34445597 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 1 Jun 2026 13:27:10 +0200 Subject: [PATCH 2/2] Tweak PR script --- scripts/make-charon-companion-pr.sh | 61 +++++++++++++++++++++++++++-- 1 file changed, 58 insertions(+), 3 deletions(-) diff --git a/scripts/make-charon-companion-pr.sh b/scripts/make-charon-companion-pr.sh index 76c4381a0..9c5a76a5d 100755 --- a/scripts/make-charon-companion-pr.sh +++ b/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