Skip to content

Bump Charon #796

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 1 commit into from
Feb 24, 2026
Merged

Bump Charon #796

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion charon-pin
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
14 changes: 7 additions & 7 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions tests/coq/demo/Demo.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion tests/coq/misc/DefaultedMethod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<i32>}::min] *)
Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32.

Expand Down
4 changes: 2 additions & 2 deletions tests/fstar/demo/Demo.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion tests/fstar/misc/DefaultedMethod.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<i32>}::min] *)
assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32

Expand Down
8 changes: 4 additions & 4 deletions tests/lean/LoopsIssues.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,30 +15,30 @@ 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<i32>}::backward_checked] -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<i32>}::backward_checked"]
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<i32>}::forward_checked] -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<i32>}::forward_checked"]
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<i32>}::steps_between] -/
@[rust_fun "core::iter::range::{core::iter::range::Step<i32>}::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<i32>] -/
@[reducible, rust_trait_impl "core::iter::range::Step<i32>"]
def I32.Insts.CoreIterRangeStep : core.iter.range.Step Std.I32 := {
Expand Down