From 55f320366d136ac49b1c3aa28d6bacea9d63ee23 Mon Sep 17 00:00:00 2001 From: N1ark Date: Tue, 24 Feb 2026 15:53:06 +0000 Subject: [PATCH] Bump Charon --- charon-pin | 2 +- flake.lock | 14 +++++++------- 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/LoopsIssues.lean | 8 ++++---- 7 files changed, 18 insertions(+), 18 deletions(-) diff --git a/charon-pin b/charon-pin index 5414f0e78..24885e25d 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. -eb7e0fb79a20d1ee338c3d47fe16243d6ab81f66 +5096e3636113c1e4da8a27c8d90b88dbadf87150 diff --git a/flake.lock b/flake.lock index 2415a1271..688ccb2cb 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1771437768, - "narHash": "sha256-krVwC21DtygsLTM7RUYcZJCwQVoOEnxy/aupelGi9s8=", + "lastModified": 1771947499, + "narHash": "sha256-69FxDQdwZNpI66nRYa2C6ITb+G8BNqeyJ3xT3WDvGts=", "owner": "aeneasverif", "repo": "charon", - "rev": "eb7e0fb79a20d1ee338c3d47fe16243d6ab81f66", + "rev": "5096e3636113c1e4da8a27c8d90b88dbadf87150", "type": "github" }, "original": { @@ -158,17 +158,17 @@ ] }, "locked": { - "lastModified": 1763952169, - "narHash": "sha256-+PeDBD8P+NKauH+w7eO/QWCIp8Cx4mCfWnh9sJmy9CM=", + "lastModified": 1771902481, + "narHash": "sha256-svI5ivzggtu4KhCdoab3xR5+Btop24o7yLFtIPXrsPM=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "ab726555a9a72e6dc80649809147823a813fa95b", + "rev": "5177426d9f8f7f1827001c9749b9a9c5570d456b", "type": "github" }, "original": { "owner": "oxalica", "repo": "rust-overlay", - "rev": "ab726555a9a72e6dc80649809147823a813fa95b", + "rev": "5177426d9f8f7f1827001c9749b9a9c5570d456b", "type": "github" } }, diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index f320f1567..66a1358a0 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -9,12 +9,12 @@ Local Open Scope Primitives_scope. Module Demo. (** [core::num::{u32}::wrapping_add]: - Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2315:8-2315:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58 Name pattern: [core::num::{u32}::wrapping_add] *) 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 2352:8-2352:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58 Name pattern: [core::num::{u32}::wrapping_sub] *) 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 92e4ea81e..3bed72bfa 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::{core::cmp::Ord for i32}::min]: - Source: '/rustc/library/core/src/cmp.rs', lines 1995:12-1995:33 + Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33 Name pattern: [core::cmp::impls::{core::cmp::Ord}::min] *) Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32. diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index c39d687b0..54cb69fa5 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -6,12 +6,12 @@ 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 2315:8-2315:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58 Name pattern: [core::num::{u32}::wrapping_add] *) 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 2352:8-2352:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58 Name pattern: [core::num::{u32}::wrapping_sub] *) 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 e6a9d63a8..960605e05 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::{core::cmp::Ord for i32}::min]: - Source: '/rustc/library/core/src/cmp.rs', lines 1995:12-1995:33 + Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33 Name pattern: [core::cmp::impls::{core::cmp::Ord}::min] *) assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32 diff --git a/tests/lean/LoopsIssues.lean b/tests/lean/LoopsIssues.lean index 05a2ef02b..9b5ac46e8 100644 --- a/tests/lean/LoopsIssues.lean +++ b/tests/lean/LoopsIssues.lean @@ -15,7 +15,7 @@ noncomputable section namespace loops_issues /- [core::iter::range::{core::iter::range::Step for i32}::backward_checked]: - Source: '/rustc/library/core/src/iter/range.rs', lines 333:16-333:74 + Source: '/rustc/library/core/src/iter/range.rs', lines 340:16-340:74 Name pattern: [core::iter::range::{core::iter::range::Step}::backward_checked] -/ @[rust_fun "core::iter::range::{core::iter::range::Step}::backward_checked"] @@ -23,7 +23,7 @@ axiom I32.Insts.CoreIterRangeStep.backward_checked : Std.I32 → Std.Usize → Result (Option Std.I32) /- [core::iter::range::{core::iter::range::Step for i32}::forward_checked]: - Source: '/rustc/library/core/src/iter/range.rs', lines 312:16-312:73 + Source: '/rustc/library/core/src/iter/range.rs', lines 319:16-319:73 Name pattern: [core::iter::range::{core::iter::range::Step}::forward_checked] -/ @[rust_fun "core::iter::range::{core::iter::range::Step}::forward_checked"] @@ -31,14 +31,14 @@ axiom I32.Insts.CoreIterRangeStep.forward_checked : Std.I32 → Std.Usize → Result (Option Std.I32) /- [core::iter::range::{core::iter::range::Step for i32}::steps_between]: - Source: '/rustc/library/core/src/iter/range.rs', lines 297:16-297:84 + Source: '/rustc/library/core/src/iter/range.rs', lines 304:16-304:84 Name pattern: [core::iter::range::{core::iter::range::Step}::steps_between] -/ @[rust_fun "core::iter::range::{core::iter::range::Step}::steps_between"] axiom I32.Insts.CoreIterRangeStep.steps_between : Std.I32 → Std.I32 → Result (Std.Usize × (Option Std.Usize)) /- Trait implementation: [core::iter::range::{core::iter::range::Step for i32}] - Source: '/rustc/library/core/src/iter/range.rs', lines 292:12-292:37 + Source: '/rustc/library/core/src/iter/range.rs', lines 299:12-299:37 Name pattern: [core::iter::range::Step] -/ @[reducible, rust_trait_impl "core::iter::range::Step"] def I32.Insts.CoreIterRangeStep : core.iter.range.Step Std.I32 := {