From 6231648c775ceb3c3b6252a4bbb8aa416cf689db Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 09:32:29 +0200 Subject: [PATCH] Update charon --- charon-pin | 2 +- flake.lock | 6 +-- tests/coq/misc/DefaultedMethod.v | 77 ++++++++++++++++++++++++++++ tests/fstar/misc/DefaultedMethod.fst | 52 +++++++++++++++++++ tests/lean/Closures.lean | 15 ++++++ 5 files changed, 148 insertions(+), 4 deletions(-) diff --git a/charon-pin b/charon-pin index fe78caa2b..f980efab0 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. -09043b10a0de68a87e55f8789cb98e1f16fe5b11 +6d0d40d01ecca97a3f064afb6ce346c152ce1cac diff --git a/flake.lock b/flake.lock index 1e139af1a..16f26f012 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1779805263, - "narHash": "sha256-bq9Noz1r4AzKi1BMbkS4xzJA+yyRr+HNm57qPdyeQ+Q=", + "lastModified": 1779866456, + "narHash": "sha256-pke4Dux03fLgnhHq5+N3XpSCyBDIcvvYtyiHUGPIzKI=", "owner": "aeneasverif", "repo": "charon", - "rev": "09043b10a0de68a87e55f8789cb98e1f16fe5b11", + "rev": "6d0d40d01ecca97a3f064afb6ce346c152ce1cac", "type": "github" }, "original": { diff --git a/tests/coq/misc/DefaultedMethod.v b/tests/coq/misc/DefaultedMethod.v index c74b33c17..5ee07b9b1 100644 --- a/tests/coq/misc/DefaultedMethod.v +++ b/tests/coq/misc/DefaultedMethod.v @@ -8,6 +8,83 @@ Import ListNotations. Local Open Scope Primitives_scope. Module DefaultedMethod. +(** Trait declaration: [core::cmp::PartialEq] + Source: '/rustc/library/core/src/cmp.rs', lines 251:0-251:65 + Name pattern: [core::cmp::PartialEq] + Visibility: public *) +Record core_cmp_PartialEq_t (Self : Type) (Rhs : Type) + := mkcore_cmp_PartialEq_t { + core_cmp_PartialEq_t_eq : Self -> Rhs -> result bool; +}. + +Arguments mkcore_cmp_PartialEq_t { _ } { _ }. +Arguments core_cmp_PartialEq_t_eq { _ } { _ } _. + +(** Trait declaration: [core::cmp::Eq] + Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:58 + Name pattern: [core::cmp::Eq] + Visibility: public *) +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; +}. + +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 396:0-396:17 + Name pattern: [core::cmp::Ordering] + Visibility: public *) +Inductive 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 1358:0-1359:41 + Name pattern: [core::cmp::PartialOrd] + Visibility: public *) +Record core_cmp_PartialOrd_t (Self : Type) (Rhs : Type) + := mkcore_cmp_PartialOrd_t { + core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst : + core_cmp_PartialEq_t Self Rhs; + core_cmp_PartialOrd_t_partial_cmp : Self -> Rhs -> result (option + core_cmp_Ordering_t); +}. + +Arguments mkcore_cmp_PartialOrd_t { _ } { _ }. +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 973:0-973:73 + Name pattern: [core::cmp::Ord] + Visibility: public *) +Record core_cmp_Ord_t (Self : Type) := mkcore_cmp_Ord_t { + core_cmp_Ord_tcore_cmp_Ord_t_EqInst : core_cmp_Eq_t Self; + core_cmp_Ord_tcore_cmp_Ord_t_PartialOrdInst : core_cmp_PartialOrd_t Self + Self; + core_cmp_Ord_t_cmp : Self -> Self -> result core_cmp_Ordering_t; + core_cmp_Ord_t_min : Self -> Self -> result Self; +}. + +Arguments mkcore_cmp_Ord_t { _ }. +Arguments core_cmp_Ord_tcore_cmp_Ord_t_EqInst { _ } _. +Arguments core_cmp_Ord_tcore_cmp_Ord_t_PartialOrdInst { _ } _. +Arguments core_cmp_Ord_t_cmp { _ } _. +Arguments core_cmp_Ord_t_min { _ } _. + +(** [core::cmp::Ord::min]: + Source: '/rustc/library/core/src/cmp.rs', lines 1064:4-1066:39 + Name pattern: [core::cmp::Ord::min] + Visibility: public *) +Axiom core_cmp_Ord_min_default : + forall{Self : Type} (ordInst : core_cmp_Ord_t Self), + Self -> Self -> result Self +. + (** [core::cmp::impls::{core::cmp::Ord for i32}::min]: Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33 Name pattern: [core::cmp::impls::{core::cmp::Ord}::min] diff --git a/tests/fstar/misc/DefaultedMethod.fst b/tests/fstar/misc/DefaultedMethod.fst index ae1c85286..9c727935e 100644 --- a/tests/fstar/misc/DefaultedMethod.fst +++ b/tests/fstar/misc/DefaultedMethod.fst @@ -5,6 +5,58 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** Trait declaration: [core::cmp::PartialEq] + Source: '/rustc/library/core/src/cmp.rs', lines 251:0-251:65 + Name pattern: [core::cmp::PartialEq] + Visibility: public *) +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 338:0-338:58 + Name pattern: [core::cmp::Eq] + Visibility: public *) +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 396:0-396:17 + Name pattern: [core::cmp::Ordering] + Visibility: public *) +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 1358:0-1359:41 + Name pattern: [core::cmp::PartialOrd] + Visibility: public *) +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 973:0-973:73 + Name pattern: [core::cmp::Ord] + Visibility: public *) +noeq type core_cmp_Ord_t (self : Type0) = { + eqInst : core_cmp_Eq_t self; + partialOrdInst : core_cmp_PartialOrd_t self self; + cmp : self -> self -> result core_cmp_Ordering_t; + min : self -> self -> result self; +} + +(** [core::cmp::Ord::min]: + Source: '/rustc/library/core/src/cmp.rs', lines 1064:4-1066:39 + Name pattern: [core::cmp::Ord::min] + Visibility: public *) +assume val core_cmp_Ord_min_default + (#self : Type0) (ordInst : core_cmp_Ord_t self) : self -> self -> result self + (** [core::cmp::impls::{core::cmp::Ord for i32}::min]: Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33 Name pattern: [core::cmp::impls::{core::cmp::Ord}::min] diff --git a/tests/lean/Closures.lean b/tests/lean/Closures.lean index d64628aef..a0298664b 100644 --- a/tests/lean/Closures.lean +++ b/tests/lean/Closures.lean @@ -12,8 +12,23 @@ set_option maxHeartbeats 1000000 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ set_option maxRecDepth 2048 +/- You can remove the following line by using the CLI option `-all-computable`: -/ +noncomputable section + namespace closures +/-- [core::iter::traits::iterator::Iterator::map]: + Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 789:4-792:34 + Name pattern: [core::iter::traits::iterator::Iterator::map] + Visibility: public -/ +@[rust_fun "core::iter::traits::iterator::Iterator::map"] +axiom core.iter.traits.iterator.Iterator.map.default + {Self : Type} {B : Type} {F : Type} {Clause0_Item : Type} (IteratorInst : + core.iter.traits.iterator.Iterator Self Clause0_Item) + (opsfunctionFnMutFTupleClause0_ItemBInst : core.ops.function.FnMut F + Clause0_Item B) : + Self → F → Result (core.iter.adapters.map.Map Self F) + /-- [closures::call_fn_no_state::closure] Source: 'tests/src/closures.rs', lines 4:15-4:40 -/ @[reducible]