Skip to content

Update charon #562

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
Jul 1, 2025
Merged

Update charon #562

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.
03f6136bea6b2b0f1d6701b0569cc49611d9de4a
17609ac76fb83a5c3cb944fa3ff6121c085c3071
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.

2 changes: 1 addition & 1 deletion src/pure/Pure.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1380,7 +1380,7 @@ type fun_body = {
}
[@@deriving show]

type item_kind = A.item_kind [@@deriving show]
type item_kind = T.item_kind [@@deriving show]

(** Attributes to add to the generated code *)
type backend_attributes = {
Expand Down
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 2025:8-2025:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2037:8-2037: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 2066:8-2066:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2074:8-2074:58
Name pattern: [core::num::{u32}::wrapping_sub] *)
Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.

Expand Down
20 changes: 10 additions & 10 deletions 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.

(** Trait declaration: [core::cmp::PartialEq]
Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
Source: '/rustc/library/core/src/cmp.rs', lines 252:0-252:59
Name pattern: [core::cmp::PartialEq] *)
Record core_cmp_PartialEq_t (Self : Type) (Rhs : Type)
:= mkcore_cmp_PartialEq_t {
Expand All @@ -20,7 +20,7 @@ Arguments mkcore_cmp_PartialEq_t { _ } { _ }.
Arguments core_cmp_PartialEq_t_eq { _ } { _ } _.

(** Trait declaration: [core::cmp::Eq]
Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:44
Name pattern: [core::cmp::Eq] *)
Record core_cmp_Eq_t (Self : Type) := mkcore_cmp_Eq_t {
core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst : core_cmp_PartialEq_t Self Self;
Expand All @@ -30,7 +30,7 @@ Arguments mkcore_cmp_Eq_t { _ }.
Arguments core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst { _ } _.

(** [core::cmp::Ordering]
Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
Source: '/rustc/library/core/src/cmp.rs', lines 391:0-391:17
Name pattern: [core::cmp::Ordering] *)
Inductive core_cmp_Ordering_t :=
| Core_cmp_Ordering_Less : core_cmp_Ordering_t
Expand All @@ -39,7 +39,7 @@ Inductive core_cmp_Ordering_t :=
.

(** Trait declaration: [core::cmp::PartialOrd]
Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
Source: '/rustc/library/core/src/cmp.rs', lines 1344:0-1344:77
Name pattern: [core::cmp::PartialOrd] *)
Record core_cmp_PartialOrd_t (Self : Type) (Rhs : Type)
:= mkcore_cmp_PartialOrd_t {
Expand All @@ -55,7 +55,7 @@ Arguments core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst { _ } { _ }
Arguments core_cmp_PartialOrd_t_partial_cmp { _ } { _ } _.

(** Trait declaration: [core::cmp::Ord]
Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
Source: '/rustc/library/core/src/cmp.rs', lines 960:0-960:51
Name pattern: [core::cmp::Ord] *)
Record core_cmp_Ord_t (Self : Type) := mkcore_cmp_Ord_t {
core_cmp_Ord_tcore_cmp_Ord_t_EqInst : core_cmp_Eq_t Self;
Expand All @@ -72,32 +72,32 @@ Arguments core_cmp_Ord_t_cmp { _ } _.
Arguments core_cmp_Ord_t_min { _ } _.

(** [core::cmp::Ord::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Source: '/rustc/library/core/src/cmp.rs', lines 1051:4-1053:20
Name pattern: [core::cmp::Ord::min] *)
Axiom core_cmp_Ord_min_default :
forall{Self : Type} (ordInst : core_cmp_Ord_t Self),
Self -> Self -> result Self
.

(** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}::eq]:
Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
Source: '/rustc/library/core/src/cmp.rs', lines 1819:16-1819:50
Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
Axiom core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool.

(** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}::partial_cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
Source: '/rustc/library/core/src/cmp.rs', lines 1934:16-1934:71
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
Axiom core_cmp_impls_PartialOrdI32I32_partial_cmp
: i32 -> i32 -> result (option core_cmp_Ordering_t)
.

(** [core::cmp::impls::{core::cmp::Ord for i32}::cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
Source: '/rustc/library/core/src/cmp.rs', lines 1944:16-1944:55
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
Axiom core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t.

(** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1936:12-1936:27
Source: '/rustc/library/core/src/cmp.rs', lines 1942:12-1942:27
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
Axiom core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32.

Expand Down
4 changes: 2 additions & 2 deletions tests/coq/misc/External_FunsExternal_Template.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,15 @@ Include External_Types.
Module External_FunsExternal_Template.

(** [core::cell::{core::cell::Cell<T>}::get]:
Source: '/rustc/library/core/src/cell.rs', lines 541:4-541:32
Source: '/rustc/library/core/src/cell.rs', lines 542:4-542:32
Name pattern: [core::cell::{core::cell::Cell<@T>}::get] *)
Axiom core_cell_Cell_get :
forall{T : Type} (markerCopyInst : core_marker_Copy T),
core_cell_Cell_t T -> state -> result (state * T)
.

(** [core::cell::{core::cell::Cell<T>}::get_mut]:
Source: '/rustc/library/core/src/cell.rs', lines 612:4-612:45
Source: '/rustc/library/core/src/cell.rs', lines 613:4-613:45
Name pattern: [core::cell::{core::cell::Cell<@T>}::get_mut] *)
Axiom core_cell_Cell_get_mut :
forall{T : Type},
Expand Down
2 changes: 1 addition & 1 deletion tests/coq/misc/External_TypesExternal_Template.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Local Open Scope Primitives_scope.
Module External_TypesExternal_Template.

(** [core::cell::Cell]
Source: '/rustc/library/core/src/cell.rs', lines 311:0-311:26
Source: '/rustc/library/core/src/cell.rs', lines 312:0-312:26
Name pattern: [core::cell::Cell] *)
Axiom core_cell_Cell_t : forall (T : Type), Type.

Expand Down
38 changes: 19 additions & 19 deletions tests/coq/misc/Traits.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -421,9 +421,9 @@ Arguments mkParentTrait1_t { _ }.

(** Trait declaration: [traits::ChildTrait]
Source: 'tests/src/traits.rs', lines 208:0-208:52 *)
Record ChildTrait_t (Self : Type) (Self_Clause0_W : Type) := mkChildTrait_t {
Record ChildTrait_t (Self : Type) (Self_Clause1_W : Type) := mkChildTrait_t {
ChildTrait_tChildTrait_t_ParentTrait0Inst : ParentTrait0_t Self
Self_Clause0_W;
Self_Clause1_W;
ChildTrait_tChildTrait_t_ParentTrait1Inst : ParentTrait1_t Self;
}.

Expand All @@ -434,8 +434,8 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1Inst { _ } { _ } _.
(** [traits::test_child_trait1]:
Source: 'tests/src/traits.rs', lines 211:0-213:1 *)
Definition test_child_trait1
{T : Type} {Clause1_Clause0_W : Type} (childTraitInst : ChildTrait_t T
Clause1_Clause0_W) (x : T) :
{T : Type} {Clause1_Clause1_W : Type} (childTraitInst : ChildTrait_t T
Clause1_Clause1_W) (x : T) :
result string
:=
childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_name)
Expand All @@ -445,9 +445,9 @@ Definition test_child_trait1
(** [traits::test_child_trait2]:
Source: 'tests/src/traits.rs', lines 215:0-217:1 *)
Definition test_child_trait2
{T : Type} {Clause1_Clause0_W : Type} (childTraitInst : ChildTrait_t T
Clause1_Clause0_W) (x : T) :
result Clause1_Clause0_W
{T : Type} {Clause1_Clause1_W : Type} (childTraitInst : ChildTrait_t T
Clause1_Clause1_W) (x : T) :
result Clause1_Clause1_W
:=
childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_w)
x
Expand Down Expand Up @@ -524,22 +524,22 @@ Arguments mkWithTarget_t { _ } { _ }.

(** Trait declaration: [traits::ParentTrait2]
Source: 'tests/src/traits.rs', lines 258:0-260:1 *)
Record ParentTrait2_t (Self : Type) (Self_U : Type) (Self_Clause1_Target :
Record ParentTrait2_t (Self : Type) (Self_U : Type) (Self_Clause2_Target :
Type) := mkParentTrait2_t {
ParentTrait2_tParentTrait2_t_WithTargetInst : WithTarget_t Self_U
Self_Clause1_Target;
Self_Clause2_Target;
}.

Arguments mkParentTrait2_t { _ } { _ } { _ }.
Arguments ParentTrait2_tParentTrait2_t_WithTargetInst { _ } { _ } { _ } _.

(** Trait declaration: [traits::ChildTrait2]
Source: 'tests/src/traits.rs', lines 262:0-264:1 *)
Record ChildTrait2_t (Self : Type) (Self_Clause0_U : Type)
(Self_Clause0_Clause1_Target : Type) := mkChildTrait2_t {
Record ChildTrait2_t (Self : Type) (Self_Clause1_U : Type)
(Self_Clause1_Clause2_Target : Type) := mkChildTrait2_t {
ChildTrait2_tChildTrait2_t_ParentTrait2Inst : ParentTrait2_t Self
Self_Clause0_U Self_Clause0_Clause1_Target;
ChildTrait2_t_convert : Self_Clause0_U -> result Self_Clause0_Clause1_Target;
Self_Clause1_U Self_Clause1_Clause2_Target;
ChildTrait2_t_convert : Self_Clause1_U -> result Self_Clause1_Clause2_Target;
}.

Arguments mkChildTrait2_t { _ } { _ } { _ }.
Expand Down Expand Up @@ -580,10 +580,10 @@ Arguments CFnOnce_t_call_once { _ } { _ } { _ } _.

(** Trait declaration: [traits::CFnMut]
Source: 'tests/src/traits.rs', lines 294:0-296:1 *)
Record CFnMut_t (Self : Type) (Args : Type) (Self_Clause0_Output : Type)
Record CFnMut_t (Self : Type) (Args : Type) (Self_Clause1_Output : Type)
:= mkCFnMut_t {
CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args Self_Clause0_Output;
CFnMut_t_call_mut : Self -> Args -> result (Self_Clause0_Output * Self);
CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args Self_Clause1_Output;
CFnMut_t_call_mut : Self -> Args -> result (Self_Clause1_Output * Self);
}.

Arguments mkCFnMut_t { _ } { _ } { _ }.
Expand All @@ -592,10 +592,10 @@ Arguments CFnMut_t_call_mut { _ } { _ } { _ } _.

(** Trait declaration: [traits::CFn]
Source: 'tests/src/traits.rs', lines 298:0-300:1 *)
Record CFn_t (Self : Type) (Args : Type) (Self_Clause0_Clause0_Output : Type)
Record CFn_t (Self : Type) (Args : Type) (Self_Clause1_Clause1_Output : Type)
:= mkCFn_t {
CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args Self_Clause0_Clause0_Output;
CFn_t_call : Self -> Args -> result Self_Clause0_Clause0_Output;
CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args Self_Clause1_Clause1_Output;
CFn_t_call : Self -> Args -> result Self_Clause1_Clause1_Output;
}.

Arguments mkCFn_t { _ } { _ } { _ }.
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 2025:8-2025:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2037:8-2037: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 2066:8-2066:58
Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2074:8-2074:58
Name pattern: [core::num::{u32}::wrapping_sub] *)
assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32

Expand Down
20 changes: 10 additions & 10 deletions tests/fstar/misc/DefaultedMethod.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,37 +6,37 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** Trait declaration: [core::cmp::PartialEq]
Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
Source: '/rustc/library/core/src/cmp.rs', lines 252:0-252:59
Name pattern: [core::cmp::PartialEq] *)
noeq type core_cmp_PartialEq_t (self : Type0) (rhs : Type0) = {
eq : self -> rhs -> result bool;
}

(** Trait declaration: [core::cmp::Eq]
Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:44
Name pattern: [core::cmp::Eq] *)
noeq type core_cmp_Eq_t (self : Type0) = {
partialEqInst : core_cmp_PartialEq_t self self;
}

(** [core::cmp::Ordering]
Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
Source: '/rustc/library/core/src/cmp.rs', lines 391:0-391:17
Name pattern: [core::cmp::Ordering] *)
type core_cmp_Ordering_t =
| Core_cmp_Ordering_Less : core_cmp_Ordering_t
| Core_cmp_Ordering_Equal : core_cmp_Ordering_t
| Core_cmp_Ordering_Greater : core_cmp_Ordering_t

(** Trait declaration: [core::cmp::PartialOrd]
Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
Source: '/rustc/library/core/src/cmp.rs', lines 1344:0-1344:77
Name pattern: [core::cmp::PartialOrd] *)
noeq type core_cmp_PartialOrd_t (self : Type0) (rhs : Type0) = {
partialEqInst : core_cmp_PartialEq_t self rhs;
partial_cmp : self -> rhs -> result (option core_cmp_Ordering_t);
}

(** Trait declaration: [core::cmp::Ord]
Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
Source: '/rustc/library/core/src/cmp.rs', lines 960:0-960:51
Name pattern: [core::cmp::Ord] *)
noeq type core_cmp_Ord_t (self : Type0) = {
eqInst : core_cmp_Eq_t self;
Expand All @@ -46,29 +46,29 @@ noeq type core_cmp_Ord_t (self : Type0) = {
}

(** [core::cmp::Ord::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Source: '/rustc/library/core/src/cmp.rs', lines 1051:4-1053:20
Name pattern: [core::cmp::Ord::min] *)
assume val core_cmp_Ord_min_default
(#self : Type0) (ordInst : core_cmp_Ord_t self) : self -> self -> result self

(** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}::eq]:
Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
Source: '/rustc/library/core/src/cmp.rs', lines 1819:16-1819:50
Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
assume val core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool

(** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}::partial_cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
Source: '/rustc/library/core/src/cmp.rs', lines 1934:16-1934:71
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
assume val core_cmp_impls_PartialOrdI32I32_partial_cmp
: i32 -> i32 -> result (option core_cmp_Ordering_t)

(** [core::cmp::impls::{core::cmp::Ord for i32}::cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
Source: '/rustc/library/core/src/cmp.rs', lines 1944:16-1944:55
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
assume val core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t

(** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1936:12-1936:27
Source: '/rustc/library/core/src/cmp.rs', lines 1942:12-1942:27
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
assume val core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32

Expand Down
4 changes: 2 additions & 2 deletions tests/fstar/misc/External.FunsExternal.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,14 @@ include External.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [core::cell::{core::cell::Cell<T>}::get]:
Source: '/rustc/library/core/src/cell.rs', lines 541:4-541:32
Source: '/rustc/library/core/src/cell.rs', lines 542:4-542:32
Name pattern: [core::cell::{core::cell::Cell<@T>}::get] *)
val core_cell_Cell_get
(#t : Type0) (markerCopyInst : core_marker_Copy t) :
core_cell_Cell_t t -> state -> result (state & t)

(** [core::cell::{core::cell::Cell<T>}::get_mut]:
Source: '/rustc/library/core/src/cell.rs', lines 612:4-612:45
Source: '/rustc/library/core/src/cell.rs', lines 613:4-613:45
Name pattern: [core::cell::{core::cell::Cell<@T>}::get_mut] *)
val core_cell_Cell_get_mut
(#t : Type0) :
Expand Down
2 changes: 1 addition & 1 deletion tests/fstar/misc/External.TypesExternal.fsti
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::cell::Cell]
Source: '/rustc/library/core/src/cell.rs', lines 311:0-311:26
Source: '/rustc/library/core/src/cell.rs', lines 312:0-312:26
Name pattern: [core::cell::Cell] *)
val core_cell_Cell_t (t : Type0) : Type0

Expand Down
Loading