Support latest Verus, notably new Z3 version

[Jay Lorch (jaylorch)]

This PR makes the projects verify with the latest version of Verus. The most notable change that's happened recently is the switch to a new version of Z3.

[Copilot]

🟡 Human review recommended

It updates core verification toolchains/dependencies and substantially restructures proofs across multiple crates, which warrants a human-run verification check before approval.

Pull request overview

This PR updates multiple crates in the repository to verify against the latest Verus toolchain, including the newer Z3 integration, by switching Verus dependencies to a pinned crates.io release and adjusting proofs/invariants to satisfy the updated verifier/SMT behavior.

Changes:

• Switch vstd (and related Verus crates via Cargo.lock) from a git dependency to a pinned crates.io version (=0.0.0-2026-08-02-0125).
• Bump Rust toolchains (stable to 1.97.1, nightly to nightly-2026-07-12) to align with the updated verification stack.
• Refactor/strengthen several Verus proofs and invariants (notably in pmemlog and capybaraKV) to keep verification tractable under the newer solver behavior.

File summaries

File	Description
unverified/metadata_kv/Cargo.toml	Pins vstd to the new published Verus version instead of git.
unverified/metadata_kv/Cargo.lock	Updates resolved dependency graph to registry-published Verus crates and new transitive deps.
pmemlog/src/logimpl_v.rs	Proof/invariant refactors to maintain verification with the newer Verus/Z3 behavior.
pmemlog/rust-toolchain.toml	Bumps stable toolchain to 1.97.1.
pmemlog/Cargo.toml	Pins vstd to the new published Verus version instead of git.
multilog/pmsafe/rust-toolchain.toml	Bumps stable toolchain to 1.97.1.
multilog/multilog/src/multilog/inv_v.rs	Adjusts proof visibility/structure for updated verifier expectations.
multilog/multilog/rust-toolchain.toml	Bumps nightly toolchain to nightly-2026-07-12.
multilog/multilog/Cargo.toml	Pins vstd to the new published Verus version instead of git.
capybaraKV/pmcopy/rust-toolchain.toml	Bumps stable toolchain to 1.97.1.
capybaraKV/capybarakv/src/kv2/shardkv_v.rs	Extracts/organizes setup loop invariants into named spec/proof helpers.
capybaraKV/capybarakv/src/kv2/setup_v.rs	Adjusts function visibility consistent with updated Verus expectations.
capybaraKV/capybarakv/src/kv2/lists/update_v.rs	Adds lemmas to split/structure update proofs to aid solver performance.
capybaraKV/capybarakv/src/kv2/lists/trim_v.rs	Adds lemmas/spinoff prover usage to keep trimming proofs manageable.
capybaraKV/capybarakv/src/kv2/keys/crud_v.rs	Minor proof/iteration adjustments for compatibility with updated Verus behavior.
capybaraKV/capybarakv/src/common/saturate_v.rs	Adds a proof block to discharge invariants in the `v2==0
capybaraKV/capybarakv/rust-toolchain.toml	Bumps nightly toolchain to nightly-2026-07-12.
capybaraKV/capybarakv/Cargo.toml	Pins vstd to the new published Verus version instead of git.

Review details

• Files reviewed: 17/18 changed files
• Comments generated: 0
• Review effort level: Lite

We're testing this review assessment. Please use 👍 or 👎 to tell us if it's correct.

[Jay Lorch (jaylorch)]

FYI, I've tested this PR on Windows, WSL, and MacOS.