From d8588670f4ac858ff99241c161abe735d89c2dc1 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 20 Apr 2026 10:57:00 -0700 Subject: [PATCH 1/5] Update to use latest Verus, which uses Rust 1.95.0 --- capybaraKV/capybarakv/Cargo.toml | 2 +- capybaraKV/capybarakv/rust-toolchain.toml | 2 +- capybaraKV/pmcopy/rust-toolchain.toml | 4 ++-- multilog/multilog/Cargo.toml | 2 +- multilog/multilog/rust-toolchain.toml | 2 +- multilog/pmsafe/rust-toolchain.toml | 4 ++-- pmemlog/Cargo.toml | 2 +- pmemlog/rust-toolchain.toml | 4 ++-- unverified/metadata_kv/Cargo.lock | 12 ++++++------ unverified/metadata_kv/Cargo.toml | 2 +- 10 files changed, 18 insertions(+), 18 deletions(-) diff --git a/capybaraKV/capybarakv/Cargo.toml b/capybaraKV/capybarakv/Cargo.toml index d57a2636..41e05cb9 100644 --- a/capybaraKV/capybarakv/Cargo.toml +++ b/capybaraKV/capybarakv/Cargo.toml @@ -19,7 +19,7 @@ default = [ "pmem" ] [dependencies] crc64fast = "1.0.0" rand = "0.8.5" -vstd = "0.0.0-2026-04-12-0118" +vstd = "0.0.0-2026-04-20-1748" pmcopy = { path = "../pmcopy" } [target.'cfg(target_family = "unix")'.dependencies] diff --git a/capybaraKV/capybarakv/rust-toolchain.toml b/capybaraKV/capybarakv/rust-toolchain.toml index 1fe38e8c..c25f9a96 100644 --- a/capybaraKV/capybarakv/rust-toolchain.toml +++ b/capybaraKV/capybarakv/rust-toolchain.toml @@ -5,5 +5,5 @@ # be used with a nightly toolchain. [toolchain] -channel = "nightly-2026-01-01" +channel = "nightly-2026-04-19" diff --git a/capybaraKV/pmcopy/rust-toolchain.toml b/capybaraKV/pmcopy/rust-toolchain.toml index 76a06e6b..a226abfc 100644 --- a/capybaraKV/pmcopy/rust-toolchain.toml +++ b/capybaraKV/pmcopy/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.94.0" +[toolchain] +channel = "1.95.0" diff --git a/multilog/multilog/Cargo.toml b/multilog/multilog/Cargo.toml index e817f9b6..5d5ee382 100644 --- a/multilog/multilog/Cargo.toml +++ b/multilog/multilog/Cargo.toml @@ -19,7 +19,7 @@ default = [ "pmem" ] [dependencies] crc64fast = "1.0.0" rand = "0.8.5" -vstd = "0.0.0-2026-04-12-0118" +vstd = "0.0.0-2026-04-20-1748" pmsafe = { path = "../pmsafe" } [target.'cfg(target_os = "windows")'.dependencies] winapi = { version = "0.3.9", features = ["errhandlingapi", "fileapi", "handleapi", "memoryapi", "winbase", "winerror", "winnt"] } diff --git a/multilog/multilog/rust-toolchain.toml b/multilog/multilog/rust-toolchain.toml index d581eccf..981e8a14 100644 --- a/multilog/multilog/rust-toolchain.toml +++ b/multilog/multilog/rust-toolchain.toml @@ -5,4 +5,4 @@ # be used with a nightly toolchain. [toolchain] -channel = "nightly-2026-01-01" +channel = "nightly-2026-04-16" diff --git a/multilog/pmsafe/rust-toolchain.toml b/multilog/pmsafe/rust-toolchain.toml index 76a06e6b..a226abfc 100644 --- a/multilog/pmsafe/rust-toolchain.toml +++ b/multilog/pmsafe/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.94.0" +[toolchain] +channel = "1.95.0" diff --git a/pmemlog/Cargo.toml b/pmemlog/Cargo.toml index 64be1bd6..912a9ccb 100644 --- a/pmemlog/Cargo.toml +++ b/pmemlog/Cargo.toml @@ -6,7 +6,7 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -vstd = "0.0.0-2026-04-12-0118" +vstd = "0.0.0-2026-04-20-1748" crc64fast = "1.0.0" [lints.rust] diff --git a/pmemlog/rust-toolchain.toml b/pmemlog/rust-toolchain.toml index 76a06e6b..a226abfc 100644 --- a/pmemlog/rust-toolchain.toml +++ b/pmemlog/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.94.0" +[toolchain] +channel = "1.95.0" diff --git a/unverified/metadata_kv/Cargo.lock b/unverified/metadata_kv/Cargo.lock index b6ab3950..891d90a3 100644 --- a/unverified/metadata_kv/Cargo.lock +++ b/unverified/metadata_kv/Cargo.lock @@ -364,9 +364,9 @@ checksum = "a46cb431066009ad2035f6bca936b1c2b7e293bffec93a2090fead0f35ab4276" [[package]] name = "verus_builtin_macros" -version = "0.0.0-2026-04-12-0118" +version = "0.0.0-2026-04-19-0121" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a4db9c476e75215dc079b3b9a740099ae26e318b410a0063b3c97c624bba991" +checksum = "40353590ec73d419cbbae41ceac223b726d93c3db09d577311b3c000fa409017" dependencies = [ "proc-macro2", "quote", @@ -388,9 +388,9 @@ dependencies = [ [[package]] name = "verus_state_machines_macros" -version = "0.0.0-2026-04-05-0114" +version = "0.0.0-2026-04-19-0121" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e799e4fb96bff36ea1356624d8b633887a46b3558f34cc20e8e228d0d7bcac2b" +checksum = "08e3405834c76c48ebe6970b910364547c1fa167880bf6b0ac4025b835068423" dependencies = [ "indexmap", "proc-macro2", @@ -411,9 +411,9 @@ dependencies = [ [[package]] name = "vstd" -version = "0.0.0-2026-04-12-0118" +version = "0.0.0-2026-04-19-0121" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fd22791c5bc9db0227a3be72721e969ac0165028ffa40c9479558b7a73006c5" +checksum = "8c1fd7a88249f8f7fe3e1a7a4b7e40f84e5343e2b664a0e9dcec6da70a53df61" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/unverified/metadata_kv/Cargo.toml b/unverified/metadata_kv/Cargo.toml index 687fab3d..c7f3624b 100644 --- a/unverified/metadata_kv/Cargo.toml +++ b/unverified/metadata_kv/Cargo.toml @@ -7,5 +7,5 @@ edition = "2021" [dependencies] rand = "0.9" -vstd = "0.0.0-2026-04-12-0118" +vstd = "0.0.0-2026-04-19-0121" proptest = "1.4" From 988ebe91bb25282b4f53391499fa3ae8169a25a5 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 20 Apr 2026 11:31:01 -0700 Subject: [PATCH 2/5] Address dependabot concern about rand default features --- capybaraKV/capybarakv/Cargo.toml | 3 +- capybaraKV/capybarakv/src/testkv_v.rs | 4 +- multilog/multilog/Cargo.toml | 3 +- .../multilog/src/multilog/multilogimpl_t.rs | 1118 ++++++++--------- unverified/metadata_kv/Cargo.lock | 354 +++++- unverified/metadata_kv/Cargo.toml | 3 +- .../src/tiering_engine_proptest.rs | 14 +- 7 files changed, 897 insertions(+), 602 deletions(-) diff --git a/capybaraKV/capybarakv/Cargo.toml b/capybaraKV/capybarakv/Cargo.toml index 41e05cb9..cfe7e6c6 100644 --- a/capybaraKV/capybarakv/Cargo.toml +++ b/capybaraKV/capybarakv/Cargo.toml @@ -18,7 +18,8 @@ default = [ "pmem" ] [dependencies] crc64fast = "1.0.0" -rand = "0.8.5" +# Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features +rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] } vstd = "0.0.0-2026-04-20-1748" pmcopy = { path = "../pmcopy" } diff --git a/capybaraKV/capybarakv/src/testkv_v.rs b/capybaraKV/capybarakv/src/testkv_v.rs index 254c948c..b4c74f7c 100644 --- a/capybaraKV/capybarakv/src/testkv_v.rs +++ b/capybaraKV/capybarakv/src/testkv_v.rs @@ -32,7 +32,7 @@ use crate::pmem::pmemutil_v::*; use crate::pmem::traits_t::*; use crate::pmem::power_t::*; use pmcopy::PmCopy; -use rand::Rng; +use rand::RngExt; use std::hash::Hash; use std::collections::VecDeque; use vstd::pcm::*; @@ -44,7 +44,7 @@ verus! { #[verifier::external_body] pub exec fn generate_fresh_id() -> (out: u128) { - rand::thread_rng().gen::() + rand::rng().random::() } // These definitions test PmCopy-generated static assertions for various different types diff --git a/multilog/multilog/Cargo.toml b/multilog/multilog/Cargo.toml index 5d5ee382..e9ec6342 100644 --- a/multilog/multilog/Cargo.toml +++ b/multilog/multilog/Cargo.toml @@ -18,7 +18,8 @@ default = [ "pmem" ] [dependencies] crc64fast = "1.0.0" -rand = "0.8.5" +# Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features +rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] } vstd = "0.0.0-2026-04-20-1748" pmsafe = { path = "../pmsafe" } [target.'cfg(target_os = "windows")'.dependencies] diff --git a/multilog/multilog/src/multilog/multilogimpl_t.rs b/multilog/multilog/src/multilog/multilogimpl_t.rs index bb4052db..019b336f 100644 --- a/multilog/multilog/src/multilog/multilogimpl_t.rs +++ b/multilog/multilog/src/multilog/multilogimpl_t.rs @@ -1,559 +1,559 @@ -//! This file contains the trusted implementation of a `MultiLogImpl`. -//! Although the verifier is run on this file, it needs to be -//! carefully read and audited to be confident of the correctness of -//! this multilog implementation. -//! -//! Fortunately, it delegates most of its work to an untrusted struct -//! `UntrustedMultiLogImpl`, which doesn't need to be read or audited. -//! It forces the `UntrustedMultiLogImpl` to satisfy certain -//! postconditions, and also places restrictions on what -//! `UntrustedMultiLogImpl` can do to persistent memory. These -//! restrictions ensure that even if the system or process crashes in -//! the middle of an operation, the system will still recover to a -//! consistent state. -//! -//! It requires `UntrustedMultiLogImpl` to implement routines that do the -//! various multilog operations like read and commit. -//! -//! It also requires `UntrustedMultiLogImpl` to provide a function -//! `UntrustedMultiLogImpl::recover`, which specifies what its `start` -//! routine will do to recover after a crash. It requires its `start` -//! routine to satisfy that specification. It also uses it to limit -//! how `UntrustedMultiLogImpl` writes to memory: It can only perform -//! updates that, if incompletely performed before a crash, still -//! leave the system in a valid state. The `recover` function takes a -//! second parameter, the `multilog_id` which is passed to the start -//! routine. -//! -//! It also requires `UntrustedMultiLogImpl` to provide a function `view` -//! that converts the current state into an abstract log. It requires that -//! performing a certain operation on the `UntrustedMultiLogImpl` causes a -//! corresponding update to its abstract view. For instance, calling -//! the `u.commit()` method should cause the resulting `u.view()` to -//! become `old(u).view().commit()`. -//! -//! It also permits `UntrustedMultiLogImpl` to provide a function `inv` -//! that encodes any invariants `UntrustedMultiLogImpl` wants maintained -//! across invocations of its functions. This implementation will then -//! guarantee that `inv` holds on any call to an `UntrustedMultiLogImpl` -//! method, and demand that the method preserve that invariant. - -use std::fmt::Write; - -use crate::multilog::multilogimpl_v::UntrustedMultiLogImpl; -use crate::multilog::multilogspec_t::AbstractMultiLogState; -use crate::pmem::pmemspec_t::*; -use crate::pmem::wrpm_t::*; -use vstd::prelude::*; - -use rand::Rng; - -verus! { - - // This is the specification that `MultiLogImpl` provides for data - // bytes it reads. It says that those bytes are correct unless - // there was corruption on the persistent memory between the last - // write and this read. - pub open spec fn read_correct_modulo_corruption(bytes: Seq, true_bytes: Seq, - impervious_to_corruption: bool) -> bool - { - if impervious_to_corruption { - // If the region is impervious to corruption, the bytes read - // must match the true bytes, i.e., the bytes last written. - - bytes == true_bytes - } - else { - // Otherwise, there must exist a sequence of distinct - // addresses `addrs` such that the nth byte of `bytes` is - // a possibly corrupted version of the nth byte of - // `true_bytes` read from the nth address in `addrs`. We - // don't require the sequence of addresses to be - // contiguous because the data might not be contiguous on - // disk (e.g., if it wrapped around the log area). - - exists |addrs: Seq| { - &&& all_elements_unique(addrs) - &&& #[trigger] maybe_corrupted(bytes, true_bytes, addrs) - } - } - } - - // This specification function indicates whether a given view of - // memory can only crash in a way that, after recovery, leads to a - // certain abstract state. - pub open spec fn can_only_crash_as_state( - pm_regions_view: PersistentMemoryRegionsView, - multilog_id: u128, - state: AbstractMultiLogState, - ) -> bool - { - forall |s| #[trigger] pm_regions_view.can_crash_as(s) ==> - UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) - } - - // A `TrustedMultiLogPermission` is the type of a tracked object - // indicating permission to update memory. It restricts updates so - // that if a crash happens, the resulting memory `mem` satisfies - // `is_state_allowable(mem)`. - // - // The struct is defined in this file, and it has a non-public - // field, so the only code that can create one is in this file. - // So untrusted code in other files can't create one, and we can - // rely on it to restrict access to persistent memory. - #[allow(dead_code)] - pub struct TrustedMultiLogPermission { - ghost is_state_allowable: spec_fn(Seq>) -> bool - } - - impl CheckPermission>> for TrustedMultiLogPermission { - closed spec fn check_permission(&self, state: Seq>) -> bool { - (self.is_state_allowable)(state) - } - } - - impl TrustedMultiLogPermission { - - // This is one of two constructors for `TrustedMultiLogPermission`. - // It conveys permission to do any update as long as a - // subsequent crash and recovery can only lead to given - // abstract state `state`. - proof fn new_one_possibility(multilog_id: u128, state: AbstractMultiLogState) -> (tracked perm: Self) - ensures - forall |s| #[trigger] perm.check_permission(s) <==> - UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) - { - Self { - is_state_allowable: |s| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) - } - } - - // This is the second of two constructors for - // `TrustedMultiLogPermission`. It conveys permission to do any - // update as long as a subsequent crash and recovery can only - // lead to one of two given abstract states `state1` and - // `state2`. - proof fn new_two_possibilities( - multilog_id: u128, - state1: AbstractMultiLogState, - state2: AbstractMultiLogState - ) -> (tracked perm: Self) - ensures - forall |s| #[trigger] perm.check_permission(s) <==> { - ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state1) - ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state2) - } - { - Self { - is_state_allowable: |s| { - ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state1) - ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state2) - } - } - } - } - - // This enumeration represents the various errors that can be - // returned from multilog operations. They're self-explanatory. - #[derive(Debug)] - pub enum MultiLogErr { - CantSetupWithFewerThanOneRegion { }, - CantSetupWithMoreThanU32MaxRegions { }, - InsufficientSpaceForSetup { which_log: u32, required_space: u64 }, - StartFailedDueToMultilogIDMismatch { which_log: u32, multilog_id_expected: u128, multilog_id_read: u128 }, - StartFailedDueToRegionSizeMismatch { which_log: u32, region_size_expected: u64, region_size_read: u64 }, - StartFailedDueToProgramVersionNumberUnsupported { which_log: u32, version_number: u64, max_supported: u64 }, - StartFailedDueToInvalidMemoryContents { which_log: u32 }, - CRCMismatch, - InvalidLogIndex { }, - InsufficientSpaceForAppend { available_space: u64 }, - CantReadBeforeHead { head: u128 }, - CantReadPastTail { tail: u128 }, - CantAdvanceHeadPositionBeforeHead { head: u128 }, - CantAdvanceHeadPositionBeyondTail { tail: u128 }, - PmemErr { err: PmemError } - } - - // This executable method can be called to compute a random GUID. - // It uses the external `rand` crate. - #[verifier::external_body] - pub exec fn generate_fresh_multilog_id() -> (out: u128) - { - rand::thread_rng().gen::() - } - - /// A `MultiLogImpl` wraps one `UntrustedMultiLogImpl` and a - /// collection of persistent memory regions to provide the - /// executable interface that turns the persistent memory regions - /// into a set of logs in which any subset of logs can be updated - /// atomically. - /// - /// The `untrusted_log_impl` field is the wrapped - /// `UntrustedMultiLogImpl`. - /// - /// The `multilog_id` field is the multilog ID. It's ghost. - /// - /// The `wrpm_regions` field contains the write-restricted persistent - /// memory. This memory will only allow updates allowed by a - /// tracked `TrustedMultiLogPermission`. So we can pass `wrpm_regions` to an - /// untrusted method, along with a restricting - /// `TrustedMultiLogPermission`, to limit what it's allowed to do. - - pub struct MultiLogImpl { - untrusted_log_impl: UntrustedMultiLogImpl, - multilog_id: Ghost, - wrpm_regions: WriteRestrictedPersistentMemoryRegions - } - - impl MultiLogImpl { - // The view of a `MultiLogImpl` is whatever the - // `UntrustedMultiLogImpl` it wraps says it is. - pub closed spec fn view(self) -> AbstractMultiLogState - { - self.untrusted_log_impl@ - } - - // The constants of a `MultiLogImpl` are whatever the - // persistent memory it wraps says they are. - pub closed spec fn constants(&self) -> PersistentMemoryConstants { - self.wrpm_regions.constants() - } - - // This is the validity condition that is maintained between - // calls to methods on `self`. - // - // That is, each of the trusted wrappers on untrusted methods - // below (e.g., `commit`, `advance_head`) can count on `valid` - // holding because it demands that each untrusted method - // maintains it. - // - // One element of `valid` is that the untrusted `inv` function - // holds. - // - // The other element of `valid` is that the persistent memory, - // if it crashes and recovers, must represent the current - // abstract state with pending tentative appends dropped. - pub closed spec fn valid(self) -> bool { - &&& self.untrusted_log_impl.inv(&self.wrpm_regions, self.multilog_id@) - &&& can_only_crash_as_state(self.wrpm_regions@, self.multilog_id@, self@.drop_pending_appends()) - } - - proof fn lemma_valid_implies_wrpm_inv(self) - requires - self.valid() - ensures - self.wrpm_regions.inv() - { - self.untrusted_log_impl.lemma_inv_implies_wrpm_inv(&self.wrpm_regions, self.multilog_id@); - } - - proof fn lemma_untrusted_log_inv_implies_valid(self) - requires - self.untrusted_log_impl.inv(&self.wrpm_regions, self.multilog_id@) - ensures - self.valid() - { - self.untrusted_log_impl.lemma_inv_implies_can_only_crash_as(&self.wrpm_regions, self.multilog_id@); - } - - // The `setup` method sets up persistent memory regions `pm_regions` - // to store an initial empty multilog. It returns a vector - // listing the capacities of the logs as well as a fresh - // multilog ID to uniquely identify it. See `README.md` for more - // documentation. - pub exec fn setup(pm_regions: &mut PMRegions) -> (result: Result<(Vec, u128), MultiLogErr>) - requires - old(pm_regions).inv(), - ensures - pm_regions.inv(), - pm_regions@.no_outstanding_writes(), - match result { - Ok((log_capacities, multilog_id)) => { - let state = AbstractMultiLogState::initialize(log_capacities@); - &&& pm_regions@.len() == old(pm_regions)@.len() - &&& pm_regions@.len() >= 1 - &&& pm_regions@.len() <= u32::MAX - &&& log_capacities@.len() == pm_regions@.len() - &&& forall |i: int| 0 <= i < pm_regions@.len() ==> - #[trigger] log_capacities@[i] <= pm_regions@[i].len() - &&& forall |i: int| 0 <= i < pm_regions@.len() ==> - #[trigger] pm_regions@[i].len() == old(pm_regions)@[i].len() - &&& can_only_crash_as_state(pm_regions@, multilog_id, state) - &&& UntrustedMultiLogImpl::recover(pm_regions@.committed(), multilog_id) == Some(state) - // Required by the `start` function's precondition. Putting this in the - // postcond of `setup` ensures that the trusted caller doesn't have to prove it - &&& UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id) == Some(state) - &&& state == state.drop_pending_appends() - }, - Err(MultiLogErr::InsufficientSpaceForSetup { which_log, required_space }) => { - let flushed_regions = old(pm_regions)@.flush(); - &&& pm_regions@ == flushed_regions - &&& pm_regions@[which_log as int].len() < required_space - }, - Err(MultiLogErr::CantSetupWithFewerThanOneRegion { }) => { - let flushed_regions = old(pm_regions)@.flush(); - &&& pm_regions@ == flushed_regions - &&& pm_regions@.len() < 1 - }, - Err(MultiLogErr::CantSetupWithMoreThanU32MaxRegions { }) => { - let flushed_regions = old(pm_regions)@.flush(); - &&& pm_regions@ == flushed_regions - &&& pm_regions@.len() > u32::MAX - }, - _ => false - } - { - let multilog_id = generate_fresh_multilog_id(); - let capacities = UntrustedMultiLogImpl::setup(pm_regions, multilog_id)?; - Ok((capacities, multilog_id)) - } - - // The `start` method creates an `UntrustedMultiLogImpl` out - // of a set of persistent memory regions. It's assumed that - // those regions were initialized with `setup` and then only - // multilog operations were allowed to mutate them. See - // `README.md` for more documentation and an example of use. - pub exec fn start(pm_regions: PMRegions, multilog_id: u128) - -> (result: Result, MultiLogErr>) - requires - pm_regions.inv(), - UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id) is Some, - ensures - match result { - Ok(trusted_log_impl) => { - &&& trusted_log_impl.valid() - &&& trusted_log_impl.constants() == pm_regions.constants() - &&& Some(trusted_log_impl@) == UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), - multilog_id) - }, - Err(MultiLogErr::CRCMismatch) => !pm_regions.constants().impervious_to_corruption, - Err(MultiLogErr::InsufficientSpaceForSetup { which_log, required_space }) => { - let flushed_regions = pm_regions@.flush(); - &&& 0 <= which_log < flushed_regions.len() - &&& pm_regions@[which_log as int].len() < required_space - }, - _ => false - } - { - // We allow the untrusted `start` method to update memory - // as part of its initialization. But, to avoid bugs - // stemming from crashes in the middle of this routine, we - // must restrict how it updates memory. We must only let - // it write such that, if a crash happens in the middle, - // it doesn't change the persistent state. - - let ghost state = UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id).unwrap(); - let mut wrpm_regions = WriteRestrictedPersistentMemoryRegions::new(pm_regions); - let tracked perm = TrustedMultiLogPermission::new_one_possibility(multilog_id, state); - let untrusted_log_impl = - UntrustedMultiLogImpl::start(&mut wrpm_regions, multilog_id, Tracked(&perm), Ghost(state))?; - Ok( - MultiLogImpl { - untrusted_log_impl, - multilog_id: Ghost(multilog_id), - wrpm_regions - }, - ) - } - - // The `tentatively_append` method tentatively appends - // `bytes_to_append` to the end of log number `which_log` in - // the multilog. It's tentative in that crashes will undo the - // appends, and reads aren't allowed in the tentative part of - // the log. See `README.md` for more documentation and examples - // of use. - pub exec fn tentatively_append(&mut self, which_log: u32, bytes_to_append: &[u8]) - -> (result: Result) - requires - old(self).valid(), - ensures - self.valid(), - self.constants() == old(self).constants(), - match result { - Ok(offset) => { - let state = old(self)@[which_log as int]; - &&& which_log < old(self)@.num_logs() - &&& offset == state.head + state.log.len() + state.pending.len() - &&& self@ == old(self)@.tentatively_append(which_log as int, bytes_to_append@) - }, - Err(MultiLogErr::InvalidLogIndex { }) => { - &&& which_log >= self@.num_logs() - &&& self@ == old(self)@ - }, - Err(MultiLogErr::InsufficientSpaceForAppend { available_space }) => { - &&& self@ == old(self)@ - &&& which_log < self@.num_logs() - &&& available_space < bytes_to_append@.len() - &&& { - let state = self@[which_log as int]; - ||| available_space == state.capacity - state.log.len() - state.pending.len() - ||| available_space == u128::MAX - state.head - state.log.len() - state.pending.len() - } - }, - _ => false - } - { - // For crash safety, we must restrict the untrusted code's - // writes to persistent memory. We must only let it write - // such that, if a crash happens in the middle of a write, - // the view of the persistent state is the current - // state with pending appends dropped. - let tracked perm = TrustedMultiLogPermission::new_one_possibility(self.multilog_id@, self@.drop_pending_appends()); - self.untrusted_log_impl.tentatively_append(&mut self.wrpm_regions, which_log, bytes_to_append, - self.multilog_id, Tracked(&perm)) - } - - // The `commit` method atomically commits all tentative - // appends that have been done to `self` since the last - // commit. The commit is atomic in that even if there's a - // crash in the middle, the recovered-to state either reflects - // all those tentative appends or none of them. See `README.md` - // for more documentation and examples of use. - pub exec fn commit(&mut self) -> (result: Result<(), MultiLogErr>) - requires - old(self).valid(), - ensures - self.valid(), - self.constants() == old(self).constants(), - match result { - Ok(()) => self@ == old(self)@.commit(), - _ => false, - } - { - // For crash safety, we must restrict the untrusted code's - // writes to persistent memory. We must only let it write - // such that, if a crash happens in the middle of a write, - // the view of the persistent state is either the current - // state with all pending appends dropped or the current - // state with all uncommitted appends committed. - let tracked perm = TrustedMultiLogPermission::new_two_possibilities(self.multilog_id@, self@.drop_pending_appends(), - self@.commit().drop_pending_appends()); - self.untrusted_log_impl.commit(&mut self.wrpm_regions, self.multilog_id, Tracked(&perm)) - } - - // The `advance_head` method advances the head of log number - // `which_log` to virtual new head position `new_head`. It - // doesn't do this tentatively; it completes it durably before - // returning. However, `advance_head` doesn't commit tentative - // appends; to do that, you need a separate call to - // `commit`. See `README.md` for more documentation and examples - // of use. - pub exec fn advance_head(&mut self, which_log: u32, new_head: u128) -> (result: Result<(), MultiLogErr>) - requires - old(self).valid(), - ensures - self.valid(), - self.constants() == old(self).constants(), - match result { - Ok(()) => { - let w = which_log as int; - &&& which_log < self@.num_logs() - &&& old(self)@[w].head <= new_head <= old(self)@[w].head + old(self)@[w].log.len() - &&& self@ == old(self)@.advance_head(w, new_head as int) - }, - Err(MultiLogErr::InvalidLogIndex{ }) => { - &&& which_log >= self@.num_logs() - &&& self@ == old(self)@ - }, - Err(MultiLogErr::CantAdvanceHeadPositionBeforeHead { head }) => { - &&& self@ == old(self)@ - &&& which_log < self@.num_logs() - &&& head == self@[which_log as int].head - &&& new_head < head - }, - Err(MultiLogErr::CantAdvanceHeadPositionBeyondTail { tail }) => { - &&& self@ == old(self)@ - &&& which_log < self@.num_logs() - &&& tail == self@[which_log as int].head + self@[which_log as int].log.len() - &&& new_head > tail - }, - _ => false, - } - { - // For crash safety, we must restrict the untrusted code's - // writes to persistent memory. We must only let it write - // such that, if a crash happens in the middle of a write, - // the view of the persistent state is either the current - // state or the current state with the head advanced. - let tracked perm = TrustedMultiLogPermission::new_two_possibilities( - self.multilog_id@, - self@.drop_pending_appends(), - self@.advance_head(which_log as int, new_head as int).drop_pending_appends() - ); - self.untrusted_log_impl.advance_head(&mut self.wrpm_regions, which_log, new_head, - self.multilog_id, Tracked(&perm)) - } - - // The `read` method reads `len` bytes from log number - // `which_log` starting at virtual position `pos`. It isn't - // allowed to read earlier than the head or past the committed - // tail. See `README.md` for more documentation and examples of - // use. - pub exec fn read(&self, which_log: u32, pos: u128, len: u64) -> (result: Result, MultiLogErr>) - requires - self.valid(), - pos + len <= u128::MAX, - ensures - ({ - let state = self@[which_log as int]; - let head = state.head; - let log = state.log; - match result { - Ok(bytes) => { - let true_bytes = self@.read(which_log as int, pos as int, len as int); - &&& which_log < self@.num_logs() - &&& pos >= head - &&& pos + len <= head + log.len() - &&& read_correct_modulo_corruption(bytes@, true_bytes, - self.constants().impervious_to_corruption) - }, - Err(MultiLogErr::InvalidLogIndex { }) => { - which_log >= self@.num_logs() - }, - Err(MultiLogErr::CantReadBeforeHead{ head: head_pos }) => { - &&& which_log < self@.num_logs() - &&& pos < head - &&& head_pos == head - }, - Err(MultiLogErr::CantReadPastTail{ tail }) => { - &&& which_log < self@.num_logs() - &&& pos + len > tail - &&& tail == head + log.len() - }, - _ => false - } - }) - { - self.untrusted_log_impl.read(&self.wrpm_regions, which_log, pos, len, self.multilog_id) - } - - // The `get_head_tail_and_capacity` method returns three - // pieces of metadata about log number `which_log`: the - // virtual head position, the virtual tail position, and the - // capacity. The capacity is the maximum number of bytes there - // can be in the log past the head, including bytes in - // tentative appends that haven't been committed yet. See - // `README.md` for more documentation and examples of use. - pub exec fn get_head_tail_and_capacity(&self, which_log: u32) -> (result: Result<(u128, u128, u64), MultiLogErr>) - requires - self.valid() - ensures - match result { - Ok((result_head, result_tail, result_capacity)) => { - let inf_log = self@[which_log as int]; - &&& which_log < self@.num_logs() - &&& result_head == inf_log.head - &&& result_tail == inf_log.head + inf_log.log.len() - &&& result_capacity == inf_log.capacity - }, - Err(MultiLogErr::InvalidLogIndex{ }) => { - which_log >= self@.num_logs() - }, - _ => false - } - { - self.untrusted_log_impl.get_head_tail_and_capacity(&self.wrpm_regions, which_log, self.multilog_id) - } - } - -} +//! This file contains the trusted implementation of a `MultiLogImpl`. +//! Although the verifier is run on this file, it needs to be +//! carefully read and audited to be confident of the correctness of +//! this multilog implementation. +//! +//! Fortunately, it delegates most of its work to an untrusted struct +//! `UntrustedMultiLogImpl`, which doesn't need to be read or audited. +//! It forces the `UntrustedMultiLogImpl` to satisfy certain +//! postconditions, and also places restrictions on what +//! `UntrustedMultiLogImpl` can do to persistent memory. These +//! restrictions ensure that even if the system or process crashes in +//! the middle of an operation, the system will still recover to a +//! consistent state. +//! +//! It requires `UntrustedMultiLogImpl` to implement routines that do the +//! various multilog operations like read and commit. +//! +//! It also requires `UntrustedMultiLogImpl` to provide a function +//! `UntrustedMultiLogImpl::recover`, which specifies what its `start` +//! routine will do to recover after a crash. It requires its `start` +//! routine to satisfy that specification. It also uses it to limit +//! how `UntrustedMultiLogImpl` writes to memory: It can only perform +//! updates that, if incompletely performed before a crash, still +//! leave the system in a valid state. The `recover` function takes a +//! second parameter, the `multilog_id` which is passed to the start +//! routine. +//! +//! It also requires `UntrustedMultiLogImpl` to provide a function `view` +//! that converts the current state into an abstract log. It requires that +//! performing a certain operation on the `UntrustedMultiLogImpl` causes a +//! corresponding update to its abstract view. For instance, calling +//! the `u.commit()` method should cause the resulting `u.view()` to +//! become `old(u).view().commit()`. +//! +//! It also permits `UntrustedMultiLogImpl` to provide a function `inv` +//! that encodes any invariants `UntrustedMultiLogImpl` wants maintained +//! across invocations of its functions. This implementation will then +//! guarantee that `inv` holds on any call to an `UntrustedMultiLogImpl` +//! method, and demand that the method preserve that invariant. + +use std::fmt::Write; + +use crate::multilog::multilogimpl_v::UntrustedMultiLogImpl; +use crate::multilog::multilogspec_t::AbstractMultiLogState; +use crate::pmem::pmemspec_t::*; +use crate::pmem::wrpm_t::*; +use vstd::prelude::*; + +use rand::RngExt; + +verus! { + + // This is the specification that `MultiLogImpl` provides for data + // bytes it reads. It says that those bytes are correct unless + // there was corruption on the persistent memory between the last + // write and this read. + pub open spec fn read_correct_modulo_corruption(bytes: Seq, true_bytes: Seq, + impervious_to_corruption: bool) -> bool + { + if impervious_to_corruption { + // If the region is impervious to corruption, the bytes read + // must match the true bytes, i.e., the bytes last written. + + bytes == true_bytes + } + else { + // Otherwise, there must exist a sequence of distinct + // addresses `addrs` such that the nth byte of `bytes` is + // a possibly corrupted version of the nth byte of + // `true_bytes` read from the nth address in `addrs`. We + // don't require the sequence of addresses to be + // contiguous because the data might not be contiguous on + // disk (e.g., if it wrapped around the log area). + + exists |addrs: Seq| { + &&& all_elements_unique(addrs) + &&& #[trigger] maybe_corrupted(bytes, true_bytes, addrs) + } + } + } + + // This specification function indicates whether a given view of + // memory can only crash in a way that, after recovery, leads to a + // certain abstract state. + pub open spec fn can_only_crash_as_state( + pm_regions_view: PersistentMemoryRegionsView, + multilog_id: u128, + state: AbstractMultiLogState, + ) -> bool + { + forall |s| #[trigger] pm_regions_view.can_crash_as(s) ==> + UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) + } + + // A `TrustedMultiLogPermission` is the type of a tracked object + // indicating permission to update memory. It restricts updates so + // that if a crash happens, the resulting memory `mem` satisfies + // `is_state_allowable(mem)`. + // + // The struct is defined in this file, and it has a non-public + // field, so the only code that can create one is in this file. + // So untrusted code in other files can't create one, and we can + // rely on it to restrict access to persistent memory. + #[allow(dead_code)] + pub struct TrustedMultiLogPermission { + ghost is_state_allowable: spec_fn(Seq>) -> bool + } + + impl CheckPermission>> for TrustedMultiLogPermission { + closed spec fn check_permission(&self, state: Seq>) -> bool { + (self.is_state_allowable)(state) + } + } + + impl TrustedMultiLogPermission { + + // This is one of two constructors for `TrustedMultiLogPermission`. + // It conveys permission to do any update as long as a + // subsequent crash and recovery can only lead to given + // abstract state `state`. + proof fn new_one_possibility(multilog_id: u128, state: AbstractMultiLogState) -> (tracked perm: Self) + ensures + forall |s| #[trigger] perm.check_permission(s) <==> + UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) + { + Self { + is_state_allowable: |s| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state) + } + } + + // This is the second of two constructors for + // `TrustedMultiLogPermission`. It conveys permission to do any + // update as long as a subsequent crash and recovery can only + // lead to one of two given abstract states `state1` and + // `state2`. + proof fn new_two_possibilities( + multilog_id: u128, + state1: AbstractMultiLogState, + state2: AbstractMultiLogState + ) -> (tracked perm: Self) + ensures + forall |s| #[trigger] perm.check_permission(s) <==> { + ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state1) + ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state2) + } + { + Self { + is_state_allowable: |s| { + ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state1) + ||| UntrustedMultiLogImpl::recover(s, multilog_id) == Some(state2) + } + } + } + } + + // This enumeration represents the various errors that can be + // returned from multilog operations. They're self-explanatory. + #[derive(Debug)] + pub enum MultiLogErr { + CantSetupWithFewerThanOneRegion { }, + CantSetupWithMoreThanU32MaxRegions { }, + InsufficientSpaceForSetup { which_log: u32, required_space: u64 }, + StartFailedDueToMultilogIDMismatch { which_log: u32, multilog_id_expected: u128, multilog_id_read: u128 }, + StartFailedDueToRegionSizeMismatch { which_log: u32, region_size_expected: u64, region_size_read: u64 }, + StartFailedDueToProgramVersionNumberUnsupported { which_log: u32, version_number: u64, max_supported: u64 }, + StartFailedDueToInvalidMemoryContents { which_log: u32 }, + CRCMismatch, + InvalidLogIndex { }, + InsufficientSpaceForAppend { available_space: u64 }, + CantReadBeforeHead { head: u128 }, + CantReadPastTail { tail: u128 }, + CantAdvanceHeadPositionBeforeHead { head: u128 }, + CantAdvanceHeadPositionBeyondTail { tail: u128 }, + PmemErr { err: PmemError } + } + + // This executable method can be called to compute a random GUID. + // It uses the external `rand` crate. + #[verifier::external_body] + pub exec fn generate_fresh_multilog_id() -> (out: u128) + { + rand::rng().random::() + } + + /// A `MultiLogImpl` wraps one `UntrustedMultiLogImpl` and a + /// collection of persistent memory regions to provide the + /// executable interface that turns the persistent memory regions + /// into a set of logs in which any subset of logs can be updated + /// atomically. + /// + /// The `untrusted_log_impl` field is the wrapped + /// `UntrustedMultiLogImpl`. + /// + /// The `multilog_id` field is the multilog ID. It's ghost. + /// + /// The `wrpm_regions` field contains the write-restricted persistent + /// memory. This memory will only allow updates allowed by a + /// tracked `TrustedMultiLogPermission`. So we can pass `wrpm_regions` to an + /// untrusted method, along with a restricting + /// `TrustedMultiLogPermission`, to limit what it's allowed to do. + + pub struct MultiLogImpl { + untrusted_log_impl: UntrustedMultiLogImpl, + multilog_id: Ghost, + wrpm_regions: WriteRestrictedPersistentMemoryRegions + } + + impl MultiLogImpl { + // The view of a `MultiLogImpl` is whatever the + // `UntrustedMultiLogImpl` it wraps says it is. + pub closed spec fn view(self) -> AbstractMultiLogState + { + self.untrusted_log_impl@ + } + + // The constants of a `MultiLogImpl` are whatever the + // persistent memory it wraps says they are. + pub closed spec fn constants(&self) -> PersistentMemoryConstants { + self.wrpm_regions.constants() + } + + // This is the validity condition that is maintained between + // calls to methods on `self`. + // + // That is, each of the trusted wrappers on untrusted methods + // below (e.g., `commit`, `advance_head`) can count on `valid` + // holding because it demands that each untrusted method + // maintains it. + // + // One element of `valid` is that the untrusted `inv` function + // holds. + // + // The other element of `valid` is that the persistent memory, + // if it crashes and recovers, must represent the current + // abstract state with pending tentative appends dropped. + pub closed spec fn valid(self) -> bool { + &&& self.untrusted_log_impl.inv(&self.wrpm_regions, self.multilog_id@) + &&& can_only_crash_as_state(self.wrpm_regions@, self.multilog_id@, self@.drop_pending_appends()) + } + + proof fn lemma_valid_implies_wrpm_inv(self) + requires + self.valid() + ensures + self.wrpm_regions.inv() + { + self.untrusted_log_impl.lemma_inv_implies_wrpm_inv(&self.wrpm_regions, self.multilog_id@); + } + + proof fn lemma_untrusted_log_inv_implies_valid(self) + requires + self.untrusted_log_impl.inv(&self.wrpm_regions, self.multilog_id@) + ensures + self.valid() + { + self.untrusted_log_impl.lemma_inv_implies_can_only_crash_as(&self.wrpm_regions, self.multilog_id@); + } + + // The `setup` method sets up persistent memory regions `pm_regions` + // to store an initial empty multilog. It returns a vector + // listing the capacities of the logs as well as a fresh + // multilog ID to uniquely identify it. See `README.md` for more + // documentation. + pub exec fn setup(pm_regions: &mut PMRegions) -> (result: Result<(Vec, u128), MultiLogErr>) + requires + old(pm_regions).inv(), + ensures + pm_regions.inv(), + pm_regions@.no_outstanding_writes(), + match result { + Ok((log_capacities, multilog_id)) => { + let state = AbstractMultiLogState::initialize(log_capacities@); + &&& pm_regions@.len() == old(pm_regions)@.len() + &&& pm_regions@.len() >= 1 + &&& pm_regions@.len() <= u32::MAX + &&& log_capacities@.len() == pm_regions@.len() + &&& forall |i: int| 0 <= i < pm_regions@.len() ==> + #[trigger] log_capacities@[i] <= pm_regions@[i].len() + &&& forall |i: int| 0 <= i < pm_regions@.len() ==> + #[trigger] pm_regions@[i].len() == old(pm_regions)@[i].len() + &&& can_only_crash_as_state(pm_regions@, multilog_id, state) + &&& UntrustedMultiLogImpl::recover(pm_regions@.committed(), multilog_id) == Some(state) + // Required by the `start` function's precondition. Putting this in the + // postcond of `setup` ensures that the trusted caller doesn't have to prove it + &&& UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id) == Some(state) + &&& state == state.drop_pending_appends() + }, + Err(MultiLogErr::InsufficientSpaceForSetup { which_log, required_space }) => { + let flushed_regions = old(pm_regions)@.flush(); + &&& pm_regions@ == flushed_regions + &&& pm_regions@[which_log as int].len() < required_space + }, + Err(MultiLogErr::CantSetupWithFewerThanOneRegion { }) => { + let flushed_regions = old(pm_regions)@.flush(); + &&& pm_regions@ == flushed_regions + &&& pm_regions@.len() < 1 + }, + Err(MultiLogErr::CantSetupWithMoreThanU32MaxRegions { }) => { + let flushed_regions = old(pm_regions)@.flush(); + &&& pm_regions@ == flushed_regions + &&& pm_regions@.len() > u32::MAX + }, + _ => false + } + { + let multilog_id = generate_fresh_multilog_id(); + let capacities = UntrustedMultiLogImpl::setup(pm_regions, multilog_id)?; + Ok((capacities, multilog_id)) + } + + // The `start` method creates an `UntrustedMultiLogImpl` out + // of a set of persistent memory regions. It's assumed that + // those regions were initialized with `setup` and then only + // multilog operations were allowed to mutate them. See + // `README.md` for more documentation and an example of use. + pub exec fn start(pm_regions: PMRegions, multilog_id: u128) + -> (result: Result, MultiLogErr>) + requires + pm_regions.inv(), + UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id) is Some, + ensures + match result { + Ok(trusted_log_impl) => { + &&& trusted_log_impl.valid() + &&& trusted_log_impl.constants() == pm_regions.constants() + &&& Some(trusted_log_impl@) == UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), + multilog_id) + }, + Err(MultiLogErr::CRCMismatch) => !pm_regions.constants().impervious_to_corruption, + Err(MultiLogErr::InsufficientSpaceForSetup { which_log, required_space }) => { + let flushed_regions = pm_regions@.flush(); + &&& 0 <= which_log < flushed_regions.len() + &&& pm_regions@[which_log as int].len() < required_space + }, + _ => false + } + { + // We allow the untrusted `start` method to update memory + // as part of its initialization. But, to avoid bugs + // stemming from crashes in the middle of this routine, we + // must restrict how it updates memory. We must only let + // it write such that, if a crash happens in the middle, + // it doesn't change the persistent state. + + let ghost state = UntrustedMultiLogImpl::recover(pm_regions@.flush().committed(), multilog_id).unwrap(); + let mut wrpm_regions = WriteRestrictedPersistentMemoryRegions::new(pm_regions); + let tracked perm = TrustedMultiLogPermission::new_one_possibility(multilog_id, state); + let untrusted_log_impl = + UntrustedMultiLogImpl::start(&mut wrpm_regions, multilog_id, Tracked(&perm), Ghost(state))?; + Ok( + MultiLogImpl { + untrusted_log_impl, + multilog_id: Ghost(multilog_id), + wrpm_regions + }, + ) + } + + // The `tentatively_append` method tentatively appends + // `bytes_to_append` to the end of log number `which_log` in + // the multilog. It's tentative in that crashes will undo the + // appends, and reads aren't allowed in the tentative part of + // the log. See `README.md` for more documentation and examples + // of use. + pub exec fn tentatively_append(&mut self, which_log: u32, bytes_to_append: &[u8]) + -> (result: Result) + requires + old(self).valid(), + ensures + self.valid(), + self.constants() == old(self).constants(), + match result { + Ok(offset) => { + let state = old(self)@[which_log as int]; + &&& which_log < old(self)@.num_logs() + &&& offset == state.head + state.log.len() + state.pending.len() + &&& self@ == old(self)@.tentatively_append(which_log as int, bytes_to_append@) + }, + Err(MultiLogErr::InvalidLogIndex { }) => { + &&& which_log >= self@.num_logs() + &&& self@ == old(self)@ + }, + Err(MultiLogErr::InsufficientSpaceForAppend { available_space }) => { + &&& self@ == old(self)@ + &&& which_log < self@.num_logs() + &&& available_space < bytes_to_append@.len() + &&& { + let state = self@[which_log as int]; + ||| available_space == state.capacity - state.log.len() - state.pending.len() + ||| available_space == u128::MAX - state.head - state.log.len() - state.pending.len() + } + }, + _ => false + } + { + // For crash safety, we must restrict the untrusted code's + // writes to persistent memory. We must only let it write + // such that, if a crash happens in the middle of a write, + // the view of the persistent state is the current + // state with pending appends dropped. + let tracked perm = TrustedMultiLogPermission::new_one_possibility(self.multilog_id@, self@.drop_pending_appends()); + self.untrusted_log_impl.tentatively_append(&mut self.wrpm_regions, which_log, bytes_to_append, + self.multilog_id, Tracked(&perm)) + } + + // The `commit` method atomically commits all tentative + // appends that have been done to `self` since the last + // commit. The commit is atomic in that even if there's a + // crash in the middle, the recovered-to state either reflects + // all those tentative appends or none of them. See `README.md` + // for more documentation and examples of use. + pub exec fn commit(&mut self) -> (result: Result<(), MultiLogErr>) + requires + old(self).valid(), + ensures + self.valid(), + self.constants() == old(self).constants(), + match result { + Ok(()) => self@ == old(self)@.commit(), + _ => false, + } + { + // For crash safety, we must restrict the untrusted code's + // writes to persistent memory. We must only let it write + // such that, if a crash happens in the middle of a write, + // the view of the persistent state is either the current + // state with all pending appends dropped or the current + // state with all uncommitted appends committed. + let tracked perm = TrustedMultiLogPermission::new_two_possibilities(self.multilog_id@, self@.drop_pending_appends(), + self@.commit().drop_pending_appends()); + self.untrusted_log_impl.commit(&mut self.wrpm_regions, self.multilog_id, Tracked(&perm)) + } + + // The `advance_head` method advances the head of log number + // `which_log` to virtual new head position `new_head`. It + // doesn't do this tentatively; it completes it durably before + // returning. However, `advance_head` doesn't commit tentative + // appends; to do that, you need a separate call to + // `commit`. See `README.md` for more documentation and examples + // of use. + pub exec fn advance_head(&mut self, which_log: u32, new_head: u128) -> (result: Result<(), MultiLogErr>) + requires + old(self).valid(), + ensures + self.valid(), + self.constants() == old(self).constants(), + match result { + Ok(()) => { + let w = which_log as int; + &&& which_log < self@.num_logs() + &&& old(self)@[w].head <= new_head <= old(self)@[w].head + old(self)@[w].log.len() + &&& self@ == old(self)@.advance_head(w, new_head as int) + }, + Err(MultiLogErr::InvalidLogIndex{ }) => { + &&& which_log >= self@.num_logs() + &&& self@ == old(self)@ + }, + Err(MultiLogErr::CantAdvanceHeadPositionBeforeHead { head }) => { + &&& self@ == old(self)@ + &&& which_log < self@.num_logs() + &&& head == self@[which_log as int].head + &&& new_head < head + }, + Err(MultiLogErr::CantAdvanceHeadPositionBeyondTail { tail }) => { + &&& self@ == old(self)@ + &&& which_log < self@.num_logs() + &&& tail == self@[which_log as int].head + self@[which_log as int].log.len() + &&& new_head > tail + }, + _ => false, + } + { + // For crash safety, we must restrict the untrusted code's + // writes to persistent memory. We must only let it write + // such that, if a crash happens in the middle of a write, + // the view of the persistent state is either the current + // state or the current state with the head advanced. + let tracked perm = TrustedMultiLogPermission::new_two_possibilities( + self.multilog_id@, + self@.drop_pending_appends(), + self@.advance_head(which_log as int, new_head as int).drop_pending_appends() + ); + self.untrusted_log_impl.advance_head(&mut self.wrpm_regions, which_log, new_head, + self.multilog_id, Tracked(&perm)) + } + + // The `read` method reads `len` bytes from log number + // `which_log` starting at virtual position `pos`. It isn't + // allowed to read earlier than the head or past the committed + // tail. See `README.md` for more documentation and examples of + // use. + pub exec fn read(&self, which_log: u32, pos: u128, len: u64) -> (result: Result, MultiLogErr>) + requires + self.valid(), + pos + len <= u128::MAX, + ensures + ({ + let state = self@[which_log as int]; + let head = state.head; + let log = state.log; + match result { + Ok(bytes) => { + let true_bytes = self@.read(which_log as int, pos as int, len as int); + &&& which_log < self@.num_logs() + &&& pos >= head + &&& pos + len <= head + log.len() + &&& read_correct_modulo_corruption(bytes@, true_bytes, + self.constants().impervious_to_corruption) + }, + Err(MultiLogErr::InvalidLogIndex { }) => { + which_log >= self@.num_logs() + }, + Err(MultiLogErr::CantReadBeforeHead{ head: head_pos }) => { + &&& which_log < self@.num_logs() + &&& pos < head + &&& head_pos == head + }, + Err(MultiLogErr::CantReadPastTail{ tail }) => { + &&& which_log < self@.num_logs() + &&& pos + len > tail + &&& tail == head + log.len() + }, + _ => false + } + }) + { + self.untrusted_log_impl.read(&self.wrpm_regions, which_log, pos, len, self.multilog_id) + } + + // The `get_head_tail_and_capacity` method returns three + // pieces of metadata about log number `which_log`: the + // virtual head position, the virtual tail position, and the + // capacity. The capacity is the maximum number of bytes there + // can be in the log past the head, including bytes in + // tentative appends that haven't been committed yet. See + // `README.md` for more documentation and examples of use. + pub exec fn get_head_tail_and_capacity(&self, which_log: u32) -> (result: Result<(u128, u128, u64), MultiLogErr>) + requires + self.valid() + ensures + match result { + Ok((result_head, result_tail, result_capacity)) => { + let inf_log = self@[which_log as int]; + &&& which_log < self@.num_logs() + &&& result_head == inf_log.head + &&& result_tail == inf_log.head + inf_log.log.len() + &&& result_capacity == inf_log.capacity + }, + Err(MultiLogErr::InvalidLogIndex{ }) => { + which_log >= self@.num_logs() + }, + _ => false + } + { + self.untrusted_log_impl.get_head_tail_and_capacity(&self.wrpm_regions, which_log, self.multilog_id) + } + } + +} diff --git a/unverified/metadata_kv/Cargo.lock b/unverified/metadata_kv/Cargo.lock index 891d90a3..29fad221 100644 --- a/unverified/metadata_kv/Cargo.lock +++ b/unverified/metadata_kv/Cargo.lock @@ -2,6 +2,12 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "anyhow" +version = "1.0.102" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" + [[package]] name = "autocfg" version = "1.1.0" @@ -41,6 +47,32 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "chacha20" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f8d983286843e49675a4b7a2d174efe136dc93a18d69130dd18198a6c167601" +dependencies = [ + "cfg-if", + "cpufeatures", + "rand_core 0.10.1", +] + +[[package]] +name = "cpufeatures" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201" +dependencies = [ + "libc", +] + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + [[package]] name = "errno" version = "0.3.8" @@ -63,6 +95,12 @@ version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" +[[package]] +name = "foldhash" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + [[package]] name = "getrandom" version = "0.2.11" @@ -76,14 +114,16 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.3.4" +version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" +checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555" dependencies = [ "cfg-if", "libc", "r-efi", + "rand_core 0.10.1", "wasip2", + "wasip3", ] [[package]] @@ -92,6 +132,33 @@ version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" +[[package]] +name = "hashbrown" +version = "0.15.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" +dependencies = [ + "foldhash", +] + +[[package]] +name = "hashbrown" +version = "0.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f467dd6dccf739c208452f8014c75c18bb8301b050ad1cfb27153803edb0f51" + +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + +[[package]] +name = "id-arena" +version = "2.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" + [[package]] name = "indexmap" version = "1.9.3" @@ -99,15 +166,39 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" dependencies = [ "autocfg", - "hashbrown", + "hashbrown 0.12.3", ] +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.0", + "serde", + "serde_core", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + [[package]] name = "lazy_static" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" +[[package]] +name = "leb128fmt" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" + [[package]] name = "libc" version = "0.2.185" @@ -126,12 +217,24 @@ version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456" +[[package]] +name = "log" +version = "0.4.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" + +[[package]] +name = "memchr" +version = "2.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" + [[package]] name = "metadata_kv" version = "0.1.0" dependencies = [ "proptest", - "rand 0.9.3", + "rand 0.10.1", "vstd", ] @@ -151,6 +254,16 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn", +] + [[package]] name = "proc-macro2" version = "1.0.103" @@ -172,7 +285,7 @@ dependencies = [ "lazy_static", "num-traits", "rand 0.8.5", - "rand_chacha 0.3.1", + "rand_chacha", "rand_xorshift", "regex-syntax", "rusty-fork", @@ -197,9 +310,9 @@ dependencies = [ [[package]] name = "r-efi" -version = "5.3.0" +version = "6.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" [[package]] name = "rand" @@ -208,18 +321,19 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" dependencies = [ "libc", - "rand_chacha 0.3.1", + "rand_chacha", "rand_core 0.6.4", ] [[package]] name = "rand" -version = "0.9.3" +version = "0.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ec095654a25171c2124e9e3393a930bddbffdc939556c914957a4c3e0a87166" +checksum = "d2e8e8bcc7961af1fdac401278c6a831614941f6164ee3bf4ce61b7edb162207" dependencies = [ - "rand_chacha 0.9.0", - "rand_core 0.9.5", + "chacha20", + "getrandom 0.4.2", + "rand_core 0.10.1", ] [[package]] @@ -232,16 +346,6 @@ dependencies = [ "rand_core 0.6.4", ] -[[package]] -name = "rand_chacha" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" -dependencies = [ - "ppv-lite86", - "rand_core 0.9.5", -] - [[package]] name = "rand_core" version = "0.6.4" @@ -253,12 +357,9 @@ dependencies = [ [[package]] name = "rand_core" -version = "0.9.5" +version = "0.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" -dependencies = [ - "getrandom 0.3.4", -] +checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" [[package]] name = "rand_xorshift" @@ -309,6 +410,54 @@ dependencies = [ "wait-timeout", ] +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.149" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "83fc039473c5595ace860d8c4fafa220ff474b3fc6bfdb4293327f1a37e94d86" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + [[package]] name = "syn" version = "2.0.111" @@ -356,6 +505,12 @@ version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" + [[package]] name = "verus_builtin" version = "0.0.0-2026-04-12-0118" @@ -392,7 +547,7 @@ version = "0.0.0-2026-04-19-0121" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08e3405834c76c48ebe6970b910364547c1fa167880bf6b0ac4025b835068423" dependencies = [ - "indexmap", + "indexmap 1.9.3", "proc-macro2", "quote", "verus_syn", @@ -437,11 +592,54 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasip2" -version = "1.0.2+wasi-0.2.9" +version = "1.0.3+wasi-0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9517f9239f02c069db75e65f174b3da828fe5f5b945c4dd26bd25d89c03ebcf5" +checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6" dependencies = [ - "wit-bindgen", + "wit-bindgen 0.57.1", +] + +[[package]] +name = "wasip3" +version = "0.4.0+wasi-0.3.0-rc-2026-01-06" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5" +dependencies = [ + "wit-bindgen 0.51.0", +] + +[[package]] +name = "wasm-encoder" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319" +dependencies = [ + "leb128fmt", + "wasmparser", +] + +[[package]] +name = "wasm-metadata" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" +dependencies = [ + "anyhow", + "indexmap 2.14.0", + "wasm-encoder", + "wasmparser", +] + +[[package]] +name = "wasmparser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" +dependencies = [ + "bitflags 2.4.1", + "hashbrown 0.15.5", + "indexmap 2.14.0", + "semver", ] [[package]] @@ -581,3 +779,97 @@ name = "wit-bindgen" version = "0.51.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5" +dependencies = [ + "wit-bindgen-rust-macro", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "wit-bindgen-core" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc" +dependencies = [ + "anyhow", + "heck", + "wit-parser", +] + +[[package]] +name = "wit-bindgen-rust" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" +dependencies = [ + "anyhow", + "heck", + "indexmap 2.14.0", + "prettyplease", + "syn", + "wasm-metadata", + "wit-bindgen-core", + "wit-component", +] + +[[package]] +name = "wit-bindgen-rust-macro" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a" +dependencies = [ + "anyhow", + "prettyplease", + "proc-macro2", + "quote", + "syn", + "wit-bindgen-core", + "wit-bindgen-rust", +] + +[[package]] +name = "wit-component" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" +dependencies = [ + "anyhow", + "bitflags 2.4.1", + "indexmap 2.14.0", + "log", + "serde", + "serde_derive", + "serde_json", + "wasm-encoder", + "wasm-metadata", + "wasmparser", + "wit-parser", +] + +[[package]] +name = "wit-parser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" +dependencies = [ + "anyhow", + "id-arena", + "indexmap 2.14.0", + "log", + "semver", + "serde", + "serde_derive", + "serde_json", + "unicode-xid", + "wasmparser", +] + +[[package]] +name = "zmij" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" diff --git a/unverified/metadata_kv/Cargo.toml b/unverified/metadata_kv/Cargo.toml index c7f3624b..164904db 100644 --- a/unverified/metadata_kv/Cargo.toml +++ b/unverified/metadata_kv/Cargo.toml @@ -6,6 +6,7 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -rand = "0.9" +# Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features +rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] } vstd = "0.0.0-2026-04-19-0121" proptest = "1.4" diff --git a/unverified/metadata_kv/src/tiering_engine_proptest.rs b/unverified/metadata_kv/src/tiering_engine_proptest.rs index 9ed3e257..bd6b1693 100644 --- a/unverified/metadata_kv/src/tiering_engine_proptest.rs +++ b/unverified/metadata_kv/src/tiering_engine_proptest.rs @@ -1,14 +1,14 @@ #[cfg(test)] extern crate proptest; use proptest::prelude::*; -use rand::Rng; +use rand::RngExt; use rand::seq::SliceRandom; use crate::metadata_kv::MetadataStore; use crate::tiering_engine::{TieringEngine, ExtentMetadataWithTiering}; use std::collections::HashMap; fn divide_into_random_segments(vec: &Vec, num_segments: usize) -> Vec> { - let mut rng = rand::thread_rng(); + let mut rng = rand::rng(); let mut segments = Vec::new(); let mut start = 0; @@ -81,7 +81,7 @@ proptest! { tiered_store.insert("extent2".to_string(), vec![]); let engine = TieringEngine::::new(); - let mut rng = rand::thread_rng(); + let mut rng = rand::rng(); // Divide data_segments into random segments let segments_extent1 = divide_into_random_segments(&data_segments, num_segments); @@ -90,8 +90,8 @@ proptest! { let mut segments_extent2_iter = segments_extent2.into_iter(); let mut ops = Vec::new(); - for _ in 0..rng.gen_range(1..=num_operations) { - match rng.gen_range(0..4) { + for _ in 0..rng.random_range(1..=num_operations) { + match rng.random_range(0..4) { 0 => { if let Some(segment) = segments_extent1_iter.next() { store.append_index("extent1", &segment); @@ -105,7 +105,7 @@ proptest! { } }, 2 => { - let extent_key = if rng.gen() { "extent1" } else { "extent2" }; + let extent_key = if rng.random() { "extent1" } else { "extent2" }; let is_tiering_in_progress = store.read_metadata(extent_key).unwrap().index_inflight_tiering_length > 0; engine.tier_extent_start(&mut store, extent_key); if !is_tiering_in_progress { @@ -115,7 +115,7 @@ proptest! { } }, _ => { - let extent_key = if rng.gen() { "extent1" } else { "extent2" }; + let extent_key = if rng.random() { "extent1" } else { "extent2" }; engine.tier_extent_end(&mut store, extent_key); ops.push(format!("[4] tier_extent_end({})", extent_key)); } From a9f2e33e5cfd0f261c65a12fbb2bf72c980a2a51 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 20 Apr 2026 11:32:29 -0700 Subject: [PATCH 3/5] Remove extra CRs in rust-toolchain.toml files --- capybaraKV/pmcopy/rust-toolchain.toml | 4 ++-- multilog/pmsafe/rust-toolchain.toml | 4 ++-- pmemlog/rust-toolchain.toml | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/capybaraKV/pmcopy/rust-toolchain.toml b/capybaraKV/pmcopy/rust-toolchain.toml index a226abfc..f25b5b14 100644 --- a/capybaraKV/pmcopy/rust-toolchain.toml +++ b/capybaraKV/pmcopy/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.95.0" +[toolchain] +channel = "1.95.0" diff --git a/multilog/pmsafe/rust-toolchain.toml b/multilog/pmsafe/rust-toolchain.toml index a226abfc..f25b5b14 100644 --- a/multilog/pmsafe/rust-toolchain.toml +++ b/multilog/pmsafe/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.95.0" +[toolchain] +channel = "1.95.0" diff --git a/pmemlog/rust-toolchain.toml b/pmemlog/rust-toolchain.toml index a226abfc..f25b5b14 100644 --- a/pmemlog/rust-toolchain.toml +++ b/pmemlog/rust-toolchain.toml @@ -1,2 +1,2 @@ -[toolchain] -channel = "1.95.0" +[toolchain] +channel = "1.95.0" From 9d62460c1391a0e05e7d278bcd7d292a9fbe1649 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 20 Apr 2026 11:35:20 -0700 Subject: [PATCH 4/5] Use consistent versions --- multilog/multilog/rust-toolchain.toml | 2 +- unverified/metadata_kv/Cargo.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/multilog/multilog/rust-toolchain.toml b/multilog/multilog/rust-toolchain.toml index 981e8a14..8040edc8 100644 --- a/multilog/multilog/rust-toolchain.toml +++ b/multilog/multilog/rust-toolchain.toml @@ -5,4 +5,4 @@ # be used with a nightly toolchain. [toolchain] -channel = "nightly-2026-04-16" +channel = "nightly-2026-04-19" diff --git a/unverified/metadata_kv/Cargo.toml b/unverified/metadata_kv/Cargo.toml index 164904db..bc23943c 100644 --- a/unverified/metadata_kv/Cargo.toml +++ b/unverified/metadata_kv/Cargo.toml @@ -8,5 +8,5 @@ edition = "2021" [dependencies] # Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] } -vstd = "0.0.0-2026-04-19-0121" +vstd = "0.0.0-2026-04-20-1748" proptest = "1.4" From b6dc5cd8515bc4955851efbd8fae8bf5135f140b Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 20 Apr 2026 11:55:10 -0700 Subject: [PATCH 5/5] Fix informational message flagged by Copilot --- unverified/metadata_kv/src/tiering_engine_proptest.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unverified/metadata_kv/src/tiering_engine_proptest.rs b/unverified/metadata_kv/src/tiering_engine_proptest.rs index bd6b1693..7aa3fc9b 100644 --- a/unverified/metadata_kv/src/tiering_engine_proptest.rs +++ b/unverified/metadata_kv/src/tiering_engine_proptest.rs @@ -117,7 +117,7 @@ proptest! { _ => { let extent_key = if rng.random() { "extent1" } else { "extent2" }; engine.tier_extent_end(&mut store, extent_key); - ops.push(format!("[4] tier_extent_end({})", extent_key)); + ops.push(format!("[3] tier_extent_end({})", extent_key)); } } }