From 827d63a7d92cda2fcd899b6c26d3384dcc34c6c4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Oct 2024 18:30:48 +0200 Subject: [PATCH] Update charon --- charon-pin | 2 +- flake.lock | 12 ++++++------ tests/coq/misc/External_FunsExternal_Template.v | 6 +++--- tests/coq/misc/External_Types.v | 2 +- tests/coq/misc/External_TypesExternal_Template.v | 2 +- tests/fstar/misc/External.FunsExternal.fsti | 6 +++--- tests/fstar/misc/External.Types.fst | 2 +- tests/fstar/misc/External.TypesExternal.fsti | 2 +- tests/lean/External/FunsExternal_Template.lean | 4 ++-- tests/lean/External/Types.lean | 2 +- tests/lean/External/TypesExternal_Template.lean | 2 +- 11 files changed, 21 insertions(+), 21 deletions(-) diff --git a/charon-pin b/charon-pin index b1c94ac21..8e34e4387 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. -aec7312164f5f9d68ac432053f35e293de52ef01 +5642ea4f0e40ad4890f4e9dc69a500737ec08940 diff --git a/flake.lock b/flake.lock index 2cccbcb0f..fb6352535 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1727774841, - "narHash": "sha256-T7OtlgWVkN74UxNSncAPHrJbyhvatFvVCcLUXreEZYI=", + "lastModified": 1729785533, + "narHash": "sha256-Hc8UDsJ3NWTNIrkvtBRDLxpSRiXANfizBTNbz05qD7Y=", "owner": "aeneasverif", "repo": "charon", - "rev": "aec7312164f5f9d68ac432053f35e293de52ef01", + "rev": "5642ea4f0e40ad4890f4e9dc69a500737ec08940", "type": "github" }, "original": { @@ -285,11 +285,11 @@ ] }, "locked": { - "lastModified": 1727749966, - "narHash": "sha256-DUS8ehzqB1DQzfZ4bRXVSollJhu+y7cvh1DJ9mbWebE=", + "lastModified": 1729736953, + "narHash": "sha256-Rb6JUop7NRklg0uzcre+A+Ebrn/ZiQPkm4QdKg6/3pw=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "00decf1b4f9886d25030b9ee4aed7bfddccb5f66", + "rev": "29b1275740d9283467b8117499ec8cbb35250584", "type": "github" }, "original": { diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index ff1eb9f6f..67f989cdc 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -12,7 +12,7 @@ Include External_Types. Module External_FunsExternal_Template. (** [core::cell::{core::cell::Cell}#10::get]: - Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26 + Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) Axiom core_cell_Cell_get : forall{T : Type} (markerCopyInst : core_marker_Copy_t T), @@ -20,7 +20,7 @@ Axiom core_cell_Cell_get : . (** [core::cell::{core::cell::Cell}#11::get_mut]: - Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39 + Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45 Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *) Axiom core_cell_Cell_get_mut : forall{T : Type}, @@ -29,7 +29,7 @@ Axiom core_cell_Cell_get_mut : . (** [core::clone::Clone::clone_from]: - Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) Axiom core_clone_Clone_clone_from : forall{Self : Type} (self_clause : core_clone_Clone Self), diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v index eedb88077..7601795ac 100644 --- a/tests/coq/misc/External_Types.v +++ b/tests/coq/misc/External_Types.v @@ -11,7 +11,7 @@ Include External_TypesExternal. Module External_Types. (** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21 + Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 Name pattern: core::marker::Copy *) Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t { core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self; diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v index 17aab7361..88fce9d4b 100644 --- a/tests/coq/misc/External_TypesExternal_Template.v +++ b/tests/coq/misc/External_TypesExternal_Template.v @@ -10,7 +10,7 @@ Local Open Scope Primitives_scope. Module External_TypesExternal_Template. (** [core::cell::Cell] - Source: '/rustc/library/core/src/cell.rs', lines 309:0-309:26 + Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26 Name pattern: core::cell::Cell *) Axiom core_cell_Cell_t : forall (T : Type), Type. diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index ddfd55386..462b41f62 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -7,14 +7,14 @@ include External.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [core::cell::{core::cell::Cell}#10::get]: - Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26 + Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) val core_cell_Cell_get (#t : Type0) (markerCopyInst : core_marker_Copy_t t) : core_cell_Cell_t t -> state -> result (state & t) (** [core::cell::{core::cell::Cell}#11::get_mut]: - Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39 + Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45 Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *) val core_cell_Cell_get_mut (#t : Type0) : @@ -22,7 +22,7 @@ val core_cell_Cell_get_mut (state & (core_cell_Cell_t t))))) (** [core::clone::Clone::clone_from]: - Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) val core_clone_Clone_clone_from (#self : Type0) (self_clause : core_clone_Clone self) : diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst index 80ac40c81..cb4fa57bf 100644 --- a/tests/fstar/misc/External.Types.fst +++ b/tests/fstar/misc/External.Types.fst @@ -7,7 +7,7 @@ include External.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21 + Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 Name pattern: core::marker::Copy *) noeq type core_marker_Copy_t (self : Type0) = { cloneCloneInst : core_clone_Clone self; diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti index 5b1c44544..871a8b55b 100644 --- a/tests/fstar/misc/External.TypesExternal.fsti +++ b/tests/fstar/misc/External.TypesExternal.fsti @@ -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 309:0-309:26 + Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26 Name pattern: core::cell::Cell *) val core_cell_Cell_t (t : Type0) : Type0 diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index ea4dd4857..dd6db7663 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -10,14 +10,14 @@ set_option linter.unusedVariables false open external /- [core::cell::{core::cell::Cell}#10::get]: - Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26 + Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get -/ axiom core.cell.Cell.get {T : Type} (markerCopyInst : core.marker.Copy T) : core.cell.Cell T → State → Result (State × T) /- [core::cell::{core::cell::Cell}#11::get_mut]: - Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39 + Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45 Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/ axiom core.cell.Cell.get_mut {T : Type} : diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 5ad4d3b17..5e64121ed 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -10,7 +10,7 @@ set_option linter.unusedVariables false namespace external /- Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21 + Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 Name pattern: core::marker::Copy -/ structure core.marker.Copy (Self : Type) where cloneCloneInst : core.clone.Clone Self diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean index 38024d696..46808e78d 100644 --- a/tests/lean/External/TypesExternal_Template.lean +++ b/tests/lean/External/TypesExternal_Template.lean @@ -8,7 +8,7 @@ set_option linter.hashCommand false set_option linter.unusedVariables false /- [core::cell::Cell] - Source: '/rustc/library/core/src/cell.rs', lines 309:0-309:26 + Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26 Name pattern: core::cell::Cell -/ axiom core.cell.Cell (T : Type) : Type