From 6a29e485dcceb9fd4a73922cc1a5bc88e398d7be Mon Sep 17 00:00:00 2001 From: Dragosh <39906742+0dragosh@users.noreply.github.com> Date: Thu, 23 Apr 2026 17:37:23 +0300 Subject: [PATCH 1/2] Add Verus workflow verification sidecar --- Cargo.lock | 139 ++++++++++++- Cargo.toml | 1 + flake.nix | 83 +++++++- scripts/verify-verus.sh | 56 +++++ src/worktree/handoff.rs | 72 +++++++ src/worktree/manager.rs | 111 +++++++++- tests/workflow_conformance.rs | 380 ++++++++++++++++++++++++++++++++++ verification/ASSUMPTIONS.md | 32 +++ verification/workflow.rs | 282 +++++++++++++++++++++++++ 9 files changed, 1151 insertions(+), 5 deletions(-) create mode 100755 scripts/verify-verus.sh create mode 100644 tests/workflow_conformance.rs create mode 100644 verification/ASSUMPTIONS.md create mode 100644 verification/workflow.rs diff --git a/Cargo.lock b/Cargo.lock index 5002272..eb046f7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -109,7 +109,16 @@ version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0700ddab506f33b20a03b13996eccd309a48e5ff77d0d95926aa0210fb4e95f1" dependencies = [ - "bit-vec", + "bit-vec 0.6.3", +] + +[[package]] +name = "bit-set" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08807e080ed7f9d5433fa9b275196cfc35414f66a0c79d864dc51a0d825231a3" +dependencies = [ + "bit-vec 0.8.0", ] [[package]] @@ -118,6 +127,12 @@ version = "0.6.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "349f9b6a179ed607305526ca489b34ad0a41aed5f7980fa90eb03160b69598fb" +[[package]] +name = "bit-vec" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7" + [[package]] name = "bitflags" version = "1.3.2" @@ -362,6 +377,7 @@ dependencies = [ "clap", "crossterm", "dirs", + "proptest", "rand 0.10.1", "ratatui", "serde", @@ -522,7 +538,7 @@ version = "0.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b95f7c0680e4142284cf8b22c14a476e87d61b004a3a0861872b32ef7ead40a2" dependencies = [ - "bit-set", + "bit-set 0.5.3", "regex", ] @@ -1118,6 +1134,15 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + [[package]] name = "prettyplease" version = "0.2.37" @@ -1137,6 +1162,31 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "proptest" +version = "1.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744" +dependencies = [ + "bit-set 0.8.0", + "bit-vec 0.8.0", + "bitflags 2.11.0", + "num-traits", + "rand 0.9.4", + "rand_chacha", + "rand_xorshift", + "regex-syntax", + "rusty-fork", + "tempfile", + "unarray", +] + +[[package]] +name = "quick-error" +version = "1.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0" + [[package]] name = "quote" version = "1.0.45" @@ -1167,6 +1217,16 @@ dependencies = [ "rand_core 0.6.4", ] +[[package]] +name = "rand" +version = "0.9.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" +dependencies = [ + "rand_chacha", + "rand_core 0.9.5", +] + [[package]] name = "rand" version = "0.10.1" @@ -1178,18 +1238,46 @@ dependencies = [ "rand_core 0.10.0", ] +[[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" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +[[package]] +name = "rand_core" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" +dependencies = [ + "getrandom 0.3.4", +] + [[package]] name = "rand_core" version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0c8d0fd677905edcbeedbf2edb6494d676f0e98d54d5cf9bda0b061cb8fb8aba" +[[package]] +name = "rand_xorshift" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a" +dependencies = [ + "rand_core 0.9.5", +] + [[package]] name = "ratatui" version = "0.30.0" @@ -1352,6 +1440,18 @@ version = "1.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" +[[package]] +name = "rusty-fork" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc6bf79ff24e648f6da1f8d1f011e9cac26491b619e6b9280f2b47f1774e6ee2" +dependencies = [ + "fnv", + "quick-error", + "tempfile", + "wait-timeout", +] + [[package]] name = "ryu" version = "1.0.23" @@ -1763,6 +1863,12 @@ version = "0.1.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2896d95c02a80c6d6a5d6e953d479f5ddf2dfdb6a244441010e373ac0fb88971" +[[package]] +name = "unarray" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94" + [[package]] name = "unicode-ident" version = "1.0.24" @@ -1831,6 +1937,15 @@ dependencies = [ "utf8parse", ] +[[package]] +name = "wait-timeout" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11" +dependencies = [ + "libc", +] + [[package]] name = "wasi" version = "0.11.1+wasi-snapshot-preview1" @@ -2199,6 +2314,26 @@ dependencies = [ "wasmparser", ] +[[package]] +name = "zerocopy" +version = "0.8.48" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eed437bf9d6692032087e337407a86f04cd8d6a16a37199ed57949d415bd68e9" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.48" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70e3cd084b1788766f53af483dd21f93881ff30d7320490ec3ef7526d203bad4" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.117", +] + [[package]] name = "zmij" version = "1.0.21" diff --git a/Cargo.toml b/Cargo.toml index fa4cac6..0ac2665 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -34,6 +34,7 @@ anyhow = "1" thiserror = "2" [dev-dependencies] +proptest = "1" tempfile = "3" [profile.release] diff --git a/flake.nix b/flake.nix index cd6e449..dff7072 100644 --- a/flake.nix +++ b/flake.nix @@ -14,6 +14,24 @@ let supportedSystems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; forAllSystems = nixpkgs.lib.genAttrs supportedSystems; + verusVersion = "0.2026.04.19.6f7d4de"; + verusSources = { + aarch64-darwin = { + asset = "verus-${verusVersion}-arm64-macos.zip"; + hash = "sha256-RMv+8CiyJ66XFN2nJ8QZnuYLakIQXJ8PIH47BQbRCxY="; + rustToolchain = "1.95.0-aarch64-apple-darwin"; + }; + x86_64-darwin = { + asset = "verus-${verusVersion}-x86-macos.zip"; + hash = "sha256-Dfw54tQcwfmkZpJHgy5Hry/hL3TM9oRK/wKyJ+ZaAvc="; + rustToolchain = "1.95.0-x86_64-apple-darwin"; + }; + x86_64-linux = { + asset = "verus-${verusVersion}-x86-linux.zip"; + hash = "sha256-cChaGWIBB9HYez/Ef1DFshhP5AVDe5hqPzEGuE/rdKU="; + rustToolchain = "1.95.0-x86_64-unknown-linux-gnu"; + }; + }; in { packages = forAllSystems (system: @@ -75,7 +93,68 @@ overlays = [ rust-overlay.overlays.default ]; }; rustToolchain = pkgs.rust-bin.stable.latest.default.override { - extensions = [ "rust-src" "rust-analyzer" ]; + extensions = [ "rust-src" "rust-analyzer" "clippy" ]; + }; + verusMeta = verusSources.${system} or null; + verus = if verusMeta == null then null else pkgs.stdenvNoCC.mkDerivation { + pname = "verus"; + version = verusVersion; + + src = pkgs.fetchurl { + url = "https://github.com/verus-lang/verus/releases/download/release/${verusVersion}/${verusMeta.asset}"; + hash = verusMeta.hash; + }; + + nativeBuildInputs = with pkgs; [ unzip makeWrapper ]; + dontBuild = true; + unpackPhase = '' + runHook preUnpack + mkdir source + unzip -q "$src" -d source + cd source + runHook postUnpack + ''; + + installPhase = '' + runHook preInstall + + mkdir -p "$out/lib/verus" "$out/bin" + release_root= + for dir in */; do + release_root="$dir" + break + done + if [ -z "$release_root" ]; then + echo "Verus release zip did not contain a top-level directory" >&2 + exit 1 + fi + cp -R "$release_root"/. "$out/lib/verus" + chmod -R u+w "$out/lib/verus" + chmod +x "$out/lib/verus/verus" "$out/lib/verus/cargo-verus" \ + "$out/lib/verus/rust_verify" "$out/lib/verus/z3" + makeWrapper "$out/lib/verus/verus" "$out/bin/verus" \ + --run "cd $out/lib/verus" + makeWrapper "$out/lib/verus/cargo-verus" "$out/bin/cargo-verus" \ + --run "cd $out/lib/verus" + + runHook postInstall + ''; + }; + verusShell = pkgs.mkShell { + buildInputs = with pkgs; [ + rustup + unzip + verus + ]; + + shellHook = '' + echo "cwt Verus shell - Verus ${verusVersion}" + echo " verify: ./scripts/verify-verus.sh" + if ! rustup run ${verusMeta.rustToolchain} rustc --version >/dev/null 2>&1; then + echo "Verus requires Rust toolchain ${verusMeta.rustToolchain}" + echo "Install it with: rustup install ${verusMeta.rustToolchain}" + fi + ''; }; in { @@ -97,6 +176,8 @@ echo " cargo run -- tui # launch TUI" ''; }; + } // pkgs.lib.optionalAttrs (verusMeta != null) { + verus = verusShell; } ); diff --git a/scripts/verify-verus.sh b/scripts/verify-verus.sh new file mode 100755 index 0000000..eaf0c67 --- /dev/null +++ b/scripts/verify-verus.sh @@ -0,0 +1,56 @@ +#!/usr/bin/env bash +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +verification_dir="$repo_root/verification" + +required_rust_toolchain() { + case "$(uname -s):$(uname -m)" in + Darwin:arm64|Darwin:aarch64) + echo "1.95.0-aarch64-apple-darwin" + ;; + Darwin:x86_64) + echo "1.95.0-x86_64-apple-darwin" + ;; + Linux:x86_64) + echo "1.95.0-x86_64-unknown-linux-gnu" + ;; + *) + echo "error: unsupported host for pinned Verus release: $(uname -s) $(uname -m)" >&2 + exit 1 + ;; + esac +} + +if ! command -v verus >/dev/null 2>&1; then + echo "error: verus is not on PATH" >&2 + echo "hint: run via nix develop .#verus -c ./scripts/verify-verus.sh" >&2 + exit 127 +fi + +if ! command -v rustup >/dev/null 2>&1; then + toolchain="$(required_rust_toolchain)" + echo "error: rustup is not on PATH" >&2 + echo "Verus requires Rust toolchain $toolchain" >&2 + echo "install it with: rustup install $toolchain" >&2 + exit 127 +fi + +toolchain="$(required_rust_toolchain)" +if ! rustup run "$toolchain" rustc --version >/dev/null 2>&1; then + echo "error: required Rust toolchain is not installed: $toolchain" >&2 + echo "install it with: rustup install $toolchain" >&2 + exit 1 +fi + +found=0 +while IFS= read -r file; do + found=1 + echo "verus ${file#$repo_root/}" + verus "$file" +done < <(find "$verification_dir" -type f -name '*.rs' | LC_ALL=C sort) + +if [[ "$found" -eq 0 ]]; then + echo "error: no Verus files found under ${verification_dir#$repo_root/}" >&2 + exit 1 +fi diff --git a/src/worktree/handoff.rs b/src/worktree/handoff.rs index 146c7be..e6288e0 100644 --- a/src/worktree/handoff.rs +++ b/src/worktree/handoff.rs @@ -215,3 +215,75 @@ pub fn execute( Ok(()) } + +#[cfg(test)] +mod tests { + use super::*; + use tempfile::TempDir; + + fn run_git(dir: &Path, args: &[&str]) { + let out = Command::new("git") + .args(args) + .current_dir(dir) + .output() + .unwrap_or_else(|e| panic!("git {} failed to start: {e}", args.join(" "))); + assert!( + out.status.success(), + "git {} failed in {}:\n{}", + args.join(" "), + dir.display(), + String::from_utf8_lossy(&out.stderr) + ); + } + + fn make_repo() -> (TempDir, std::path::PathBuf) { + let temp = TempDir::new().expect("create temp repo"); + let root = temp.path().to_path_buf(); + run_git(&root, &["init", "--initial-branch=main"]); + run_git(&root, &["config", "user.email", "test@cwt.dev"]); + run_git(&root, &["config", "user.name", "cwt-test"]); + std::fs::write(root.join("README.md"), "# handoff repo\n").expect("write README"); + run_git(&root, &["add", "."]); + run_git(&root, &["commit", "-m", "initial commit"]); + (temp, root) + } + + #[test] + fn local_to_worktree_handoff_preserves_source_and_only_mutates_target() { + let (_temp, root) = make_repo(); + let wt_path = root.join("wt-target"); + run_git( + &root, + &[ + "worktree", + "add", + wt_path.to_str().expect("utf-8 path"), + "-b", + "wt/handoff-target", + "main", + ], + ); + + let changed_readme = "# handoff repo\nlocal change\n"; + std::fs::write(root.join("README.md"), changed_readme).expect("write local change"); + + execute(HandoffDirection::LocalToWorktree, &wt_path, &root, None) + .expect("handoff should apply local patch to worktree"); + + let local_readme = std::fs::read_to_string(root.join("README.md")).expect("read local"); + let target_readme = + std::fs::read_to_string(wt_path.join("README.md")).expect("read target"); + assert_eq!(local_readme, changed_readme); + assert_eq!(target_readme, changed_readme); + + let local_status = Command::new("git") + .args(["status", "--porcelain"]) + .current_dir(&root) + .output() + .expect("git status"); + assert!( + String::from_utf8_lossy(&local_status.stdout).contains("README.md"), + "source repo should still hold its uncommitted change" + ); + } +} diff --git a/src/worktree/manager.rs b/src/worktree/manager.rs index 32b16e7..af0556e 100644 --- a/src/worktree/manager.rs +++ b/src/worktree/manager.rs @@ -337,13 +337,13 @@ impl Manager { // Apply committed changes first if !committed_patch.trim().is_empty() { - git::commands::apply_patch(&wt_abs_path, committed_patch.trim()) + git::commands::apply_patch(&wt_abs_path, &committed_patch) .context("failed to apply committed changes from snapshot")?; } // Apply uncommitted changes if !uncommitted_patch.trim().is_empty() { - git::commands::apply_patch(&wt_abs_path, uncommitted_patch.trim()) + git::commands::apply_patch(&wt_abs_path, &uncommitted_patch) .context("failed to apply uncommitted changes from snapshot")?; } @@ -420,3 +420,110 @@ impl Manager { } } } + +#[cfg(test)] +mod tests { + use super::*; + use std::path::Path; + use std::sync::{Mutex, OnceLock}; + use tempfile::TempDir; + + static ENV_LOCK: OnceLock> = OnceLock::new(); + + struct HomeGuard { + previous_home: Option, + _lock: std::sync::MutexGuard<'static, ()>, + } + + impl HomeGuard { + fn set(home: &Path) -> Self { + let lock = ENV_LOCK + .get_or_init(|| Mutex::new(())) + .lock() + .expect("env lock should not be poisoned"); + let previous_home = std::env::var_os("HOME"); + std::env::set_var("HOME", home); + Self { + previous_home, + _lock: lock, + } + } + } + + impl Drop for HomeGuard { + fn drop(&mut self) { + if let Some(previous_home) = &self.previous_home { + std::env::set_var("HOME", previous_home); + } else { + std::env::remove_var("HOME"); + } + } + } + + fn run_git(dir: &Path, args: &[&str]) { + let out = std::process::Command::new("git") + .args(args) + .current_dir(dir) + .output() + .unwrap_or_else(|e| panic!("git {} failed to start: {e}", args.join(" "))); + assert!( + out.status.success(), + "git {} failed in {}:\n{}", + args.join(" "), + dir.display(), + String::from_utf8_lossy(&out.stderr) + ); + } + + fn make_repo() -> (TempDir, PathBuf) { + let temp = TempDir::new().expect("create temp repo"); + let root = std::fs::canonicalize(temp.path()).expect("canonical repo path"); + run_git(&root, &["init", "--initial-branch=main"]); + run_git(&root, &["config", "user.email", "test@cwt.dev"]); + run_git(&root, &["config", "user.name", "cwt-test"]); + std::fs::write(root.join("README.md"), "# restore repo\n").expect("write README"); + run_git(&root, &["add", "."]); + run_git(&root, &["commit", "-m", "initial commit"]); + (temp, root) + } + + #[test] + fn restore_snapshot_preserves_snapshot_metadata_and_recreates_worktree() { + let home = TempDir::new().expect("create home"); + let _home_guard = HomeGuard::set(home.path()); + let (_temp, root) = make_repo(); + let manager = Manager::new(root.clone(), Config::default()); + + let worktree = manager + .create(Some("restore-wt"), "main", false) + .expect("create worktree"); + let wt_path = manager.worktree_abs_path(&worktree); + std::fs::write( + wt_path.join("README.md"), + "# restore repo\nrestored change\n", + ) + .expect("write worktree change"); + + manager.delete("restore-wt").expect("delete worktree"); + let snapshots_before = manager.list_snapshots().expect("list snapshots"); + assert_eq!(snapshots_before.len(), 1); + let snapshot = snapshots_before[0].clone(); + assert!(snapshot.patch_file.exists()); + + let restored = manager + .restore_snapshot(&snapshot) + .expect("restore snapshot"); + + assert_eq!(restored.name, "restore-wt"); + let state = manager.load_state().expect("load state"); + assert!(state.worktrees.contains_key("restore-wt")); + assert_eq!(state.snapshots.len(), snapshots_before.len()); + assert_eq!(state.snapshots[0].name, "restore-wt"); + assert!(snapshot.patch_file.exists()); + + let restored_path = manager.worktree_abs_path(&restored); + let restored_readme = + std::fs::read_to_string(restored_path.join("README.md")).expect("read restored file"); + assert!(restored_readme.contains("restored change")); + } +} diff --git a/tests/workflow_conformance.rs b/tests/workflow_conformance.rs new file mode 100644 index 0000000..047a029 --- /dev/null +++ b/tests/workflow_conformance.rs @@ -0,0 +1,380 @@ +//! Conformance checks for the sidecar workflow model. +//! +//! These tests exercise real temporary git repositories through the cwt binary +//! and compare the observable state against the same invariants the Verus +//! sidecar models abstractly. + +use proptest::prelude::*; +use std::collections::BTreeMap; +use std::path::{Path, PathBuf}; +use std::process::Command; +use tempfile::TempDir; + +struct TestRepo { + _repo_dir: TempDir, + home_dir: TempDir, + root: PathBuf, +} + +impl TestRepo { + fn new() -> Self { + let repo_dir = TempDir::new().expect("create repo dir"); + let home_dir = TempDir::new().expect("create home dir"); + configure_git(home_dir.path()); + + let root = repo_dir.path().to_path_buf(); + run_git(home_dir.path(), &root, &["init"]); + std::fs::write(root.join("README.md"), "# conformance repo\n").expect("write README"); + run_git(home_dir.path(), &root, &["add", "."]); + run_git(home_dir.path(), &root, &["commit", "-m", "initial commit"]); + + Self { + _repo_dir: repo_dir, + home_dir, + root, + } + } + + fn run_cwt(&self, args: &[&str]) -> (String, String, bool) { + let out = Command::new(cwt_binary()) + .args(args) + .current_dir(&self.root) + .env("HOME", self.home_dir.path()) + .env("XDG_CONFIG_HOME", self.home_dir.path().join(".config")) + .output() + .unwrap_or_else(|e| panic!("failed to run cwt {}: {e}", args.join(" "))); + + ( + String::from_utf8_lossy(&out.stdout).to_string(), + String::from_utf8_lossy(&out.stderr).to_string(), + out.status.success(), + ) + } + + fn run_cwt_ok(&self, args: &[&str]) -> String { + let (stdout, stderr, ok) = self.run_cwt(args); + assert!( + ok, + "cwt {} failed in {}:\n{}", + args.join(" "), + self.root.display(), + stderr + ); + stdout + } + + fn git(&self, dir: &Path, args: &[&str]) { + run_git(self.home_dir.path(), dir, args); + } + + fn worktree_path(&self, name: &str) -> PathBuf { + self.root.join(".claude/worktrees").join(name) + } +} + +#[derive(Clone, Debug)] +enum WorkflowOp { + Create(usize), + Promote(usize), + Delete(usize), +} + +fn workflow_op() -> impl Strategy { + prop_oneof![ + (0usize..3).prop_map(WorkflowOp::Create), + (0usize..3).prop_map(WorkflowOp::Promote), + (0usize..3).prop_map(WorkflowOp::Delete), + ] +} + +fn workflow_name(index: usize) -> &'static str { + ["alpha", "beta", "gamma"][index] +} + +proptest! { + #![proptest_config(ProptestConfig { + cases: 4, + max_shrink_iters: 0, + .. ProptestConfig::default() + })] + + #[test] + fn create_delete_promote_round_trips_follow_model( + ops in proptest::collection::vec(workflow_op(), 1..8) + ) { + let repo = TestRepo::new(); + let mut model = BTreeMap::::new(); + + for op in ops { + match op { + WorkflowOp::Create(index) => { + let name = workflow_name(index); + let (_stdout, stderr, ok) = repo.run_cwt(&["create", name, "--base", "main"]); + if model.contains_key(name) { + prop_assert!(!ok, "duplicate create for {name} should fail"); + prop_assert!( + stderr.contains("already exists") || stderr.contains("failed"), + "duplicate create should explain the conflict, got: {stderr}" + ); + } else { + prop_assert!(ok, "create {name} should succeed: {stderr}"); + model.insert(name.to_string(), "ephemeral".to_string()); + } + } + WorkflowOp::Promote(index) => { + let name = workflow_name(index); + let (_stdout, _stderr, ok) = repo.run_cwt(&["promote", name]); + if let Some(lifecycle) = model.get_mut(name) { + prop_assert!(ok, "promote {name} should succeed"); + *lifecycle = "permanent".to_string(); + } else { + prop_assert!(!ok, "promote of absent {name} should fail"); + } + } + WorkflowOp::Delete(index) => { + let name = workflow_name(index); + let (_stdout, _stderr, ok) = repo.run_cwt(&["delete", name]); + if model.remove(name).is_some() { + prop_assert!(ok, "delete {name} should succeed"); + prop_assert!( + !repo.worktree_path(name).exists(), + "delete should remove worktree directory for {name}" + ); + prop_assert!( + snapshot_names(&repo.root).iter().any(|snapshot| snapshot == name), + "delete should retain snapshot metadata for {name}" + ); + } else { + prop_assert!(!ok, "delete of absent {name} should fail"); + } + } + } + + prop_assert_eq!(worktree_lifecycles(&repo.root), model.clone()); + } + } +} + +#[test] +fn gc_preview_skips_permanent_running_dirty_and_unpushed_worktrees() { + let repo = TestRepo::new(); + std::fs::create_dir_all(repo.root.join(".cwt")).expect("create .cwt"); + std::fs::write( + repo.root.join(".cwt/config.toml"), + "[worktree]\nmax_ephemeral = 1\n", + ) + .expect("write config"); + + repo.git( + &repo.root, + &["remote", "add", "origin", repo.root.to_str().unwrap()], + ); + repo.git(&repo.root, &["fetch", "origin"]); + repo.git(&repo.root, &["push", "origin", "main"]); + + for name in [ + "gc-clean-old", + "gc-permanent", + "gc-running", + "gc-dirty", + "gc-unpushed", + "gc-clean-new", + ] { + repo.run_cwt_ok(&["create", name, "--base", "main"]); + } + + for name in [ + "gc-clean-old", + "gc-permanent", + "gc-running", + "gc-dirty", + "gc-clean-new", + ] { + let branch = format!("wt/{name}"); + repo.git(&repo.root, &["push", "origin", &branch]); + repo.git( + &repo.worktree_path(name), + &["branch", "--set-upstream-to", &format!("origin/{branch}")], + ); + } + + repo.run_cwt_ok(&["promote", "gc-permanent"]); + set_worktree_status(&repo.root, "gc-running", "running"); + std::fs::write(repo.worktree_path("gc-dirty").join("dirty.txt"), "dirty\n") + .expect("dirty worktree"); + + let stdout = repo.run_cwt_ok(&["gc"]); + + assert!(stdout.contains("gc-clean-old")); + assert!(stdout.contains("gc-clean-new")); + for protected in ["gc-permanent", "gc-running", "gc-dirty", "gc-unpushed"] { + assert!( + !stdout.contains(protected), + "GC preview must not select protected worktree {protected}; stdout was:\n{stdout}" + ); + } +} + +#[test] +fn verification_sidecar_files_are_present_and_document_trusted_boundaries() { + let root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + + let assumptions = std::fs::read_to_string(root.join("verification/ASSUMPTIONS.md")) + .expect("verification assumptions doc should exist"); + for boundary in [ + "git command truth", + "patch application semantics", + "filesystem atomicity", + "tmux/session facts", + "wall-clock timestamps", + "Verus/Rust compiler trust", + ] { + assert!( + assumptions.contains(boundary), + "ASSUMPTIONS.md should document trusted boundary: {boundary}" + ); + } + + let workflow = std::fs::read_to_string(root.join("verification/workflow.rs")) + .expect("Verus workflow model should exist"); + for proof_name in [ + "lemma_create_adds_fresh_idle_ephemeral", + "lemma_delete_removes_exactly_one_after_snapshot", + "lemma_promote_is_idempotent", + "lemma_gc_preview_selects_only_safe_excess", + "lemma_restore_preserves_snapshot_metadata", + "lemma_handoff_success_only_mutates_target", + ] { + assert!( + workflow.contains(proof_name), + "Verus workflow model should contain proof {proof_name}" + ); + } + + let script_path = root.join("scripts/verify-verus.sh"); + let script = std::fs::read_to_string(&script_path).expect("Verus runner should exist"); + assert!( + script.contains("verification"), + "runner should scan verification/" + ); + assert!(script.contains("verus"), "runner should invoke verus"); + + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mode = std::fs::metadata(script_path) + .expect("stat Verus runner") + .permissions() + .mode(); + assert!(mode & 0o111 != 0, "Verus runner should be executable"); + } +} + +fn configure_git(home: &Path) { + for args in [ + &["config", "--global", "user.email", "test@cwt.dev"][..], + &["config", "--global", "user.name", "cwt-test"], + &["config", "--global", "init.defaultBranch", "main"], + ] { + let out = Command::new("git") + .args(args) + .env("HOME", home) + .output() + .expect("git config should start"); + assert!( + out.status.success(), + "git {} failed: {}", + args.join(" "), + String::from_utf8_lossy(&out.stderr) + ); + } +} + +fn run_git(home: &Path, dir: &Path, args: &[&str]) { + let out = Command::new("git") + .args(args) + .current_dir(dir) + .env("HOME", home) + .output() + .unwrap_or_else(|e| panic!("git {} failed to start: {e}", args.join(" "))); + assert!( + out.status.success(), + "git {} failed in {}:\n{}", + args.join(" "), + dir.display(), + String::from_utf8_lossy(&out.stderr) + ); +} + +fn cwt_binary() -> PathBuf { + if let Ok(path) = std::env::var("CARGO_BIN_EXE_cwt") { + return PathBuf::from(path); + } + + let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let target_debug = manifest_dir.join("target/debug/cwt"); + if target_debug.exists() { + return target_debug; + } + + panic!("cwt binary not found. Run `cargo build` first."); +} + +fn read_state(root: &Path) -> serde_json::Value { + let path = root.join(".cwt/state.json"); + if !path.exists() { + return serde_json::json!({ + "worktrees": {}, + "snapshots": [], + }); + } + + let content = std::fs::read_to_string(&path) + .unwrap_or_else(|e| panic!("failed to read {}: {e}", path.display())); + serde_json::from_str(&content).expect("state should be valid JSON") +} + +fn worktree_lifecycles(root: &Path) -> BTreeMap { + let state = read_state(root); + state["worktrees"] + .as_object() + .unwrap_or_else(|| panic!("state worktrees should be an object")) + .iter() + .map(|(name, wt)| { + ( + name.clone(), + wt["lifecycle"] + .as_str() + .unwrap_or_else(|| panic!("worktree {name} should have lifecycle")) + .to_string(), + ) + }) + .collect() +} + +fn snapshot_names(root: &Path) -> Vec { + let state = read_state(root); + state["snapshots"] + .as_array() + .unwrap_or_else(|| panic!("state snapshots should be an array")) + .iter() + .map(|snapshot| { + snapshot["name"] + .as_str() + .expect("snapshot should have name") + .to_string() + }) + .collect() +} + +fn set_worktree_status(root: &Path, name: &str, status: &str) { + let state_path = root.join(".cwt/state.json"); + let content = std::fs::read_to_string(&state_path).expect("read state"); + let mut state: serde_json::Value = serde_json::from_str(&content).expect("parse state"); + state["worktrees"][name]["status"] = serde_json::Value::String(status.to_string()); + std::fs::write( + &state_path, + serde_json::to_string_pretty(&state).expect("serialize state"), + ) + .expect("write state"); +} diff --git a/verification/ASSUMPTIONS.md b/verification/ASSUMPTIONS.md new file mode 100644 index 0000000..9872699 --- /dev/null +++ b/verification/ASSUMPTIONS.md @@ -0,0 +1,32 @@ +# Verus Sidecar Assumptions + +This verification suite models cwt workflow state transitions. It does not +prove git, tmux, filesystem, terminal UI, or operating system behavior. + +Trusted boundaries: + +- git command truth: git command wrappers report the actual repository, + worktree, branch, dirty, and upstream state. +- patch application semantics: `git apply --3way` and `git am --3way` apply + exactly the patch or mailbox content supplied to the target repository. +- filesystem atomicity: snapshot temp-file writes followed by rename either + leave a complete snapshot entry or surface an error before state deletion. +- tmux/session facts: session status recorded in cwt state correctly reflects + whether a worktree is running and should be protected from GC. +- wall-clock timestamps: creation and deletion timestamps are trusted for + ordering, auditing, and display, but not for safety-critical proof steps. +- Verus/Rust compiler trust: the Verus verifier, Rust compiler, standard + libraries, and platform toolchain are part of the trusted computing base. + +The sidecar model verifies workflow invariants over abstract state: + +- create adds only a fresh idle ephemeral worktree; +- delete removes exactly one worktree after snapshot success; +- promote is idempotent and never demotes permanent worktrees; +- GC preview selects only safe ephemeral worktrees and never exceeds the + requested excess; +- restore recreates a worktree from snapshot metadata without consuming the + snapshot; +- handoff preserves source changes and only mutates the intended target on + successful apply. + diff --git a/verification/workflow.rs b/verification/workflow.rs new file mode 100644 index 0000000..14d00ef --- /dev/null +++ b/verification/workflow.rs @@ -0,0 +1,282 @@ +use vstd::prelude::*; +use vstd::set::*; + +verus! { + +/// Abstract lifecycle for a managed worktree. +pub enum Lifecycle { + Ephemeral, + Permanent, +} + +/// Abstract runtime status for a managed worktree. +pub enum Status { + Idle, + Running, + Waiting, + Done, + Shipping, +} + +/// Abstract cwt workflow state. +/// +/// A worktree is present when its id is in `worktrees`. Marker sets encode the +/// lifecycle/status/git facts that matter for workflow correctness. Entries +/// absent from a marker set use the safe/default value: ephemeral, idle, clean, +/// pushed, and no source changes. +pub struct State { + pub worktrees: Set, + pub permanent: Set, + pub running: Set, + pub dirty: Set, + pub unpushed: Set, + pub snapshots: Set, + pub changes: Set, +} + +pub open spec fn wf(s: State) -> bool { + &&& forall|id: int| #[trigger] s.permanent.contains(id) ==> s.worktrees.contains(id) + &&& forall|id: int| #[trigger] s.running.contains(id) ==> s.worktrees.contains(id) + &&& forall|id: int| #[trigger] s.dirty.contains(id) ==> s.worktrees.contains(id) + &&& forall|id: int| #[trigger] s.unpushed.contains(id) ==> s.worktrees.contains(id) + &&& forall|id: int| #[trigger] s.changes.contains(id) ==> s.worktrees.contains(id) +} + +pub open spec fn is_ephemeral(s: State, id: int) -> bool { + s.worktrees.contains(id) && !s.permanent.contains(id) +} + +pub open spec fn is_gc_safe(s: State, id: int) -> bool { + &&& is_ephemeral(s, id) + &&& !s.running.contains(id) + &&& !s.dirty.contains(id) + &&& !s.unpushed.contains(id) +} + +pub open spec fn gc_preview_valid(s: State, selected: Set, excess: nat) -> bool { + &&& selected.finite() + &&& selected.len() <= excess + &&& forall|id: int| #[trigger] selected.contains(id) ==> is_gc_safe(s, id) +} + +pub open spec fn create(s: State, id: int) -> State + recommends + wf(s), + !s.worktrees.contains(id), +{ + State { + worktrees: s.worktrees.insert(id), + permanent: s.permanent.remove(id), + running: s.running.remove(id), + dirty: s.dirty.remove(id), + unpushed: s.unpushed.remove(id), + snapshots: s.snapshots, + changes: s.changes.remove(id), + } +} + +pub open spec fn snapshot_success(s: State, id: int) -> State + recommends + wf(s), + s.worktrees.contains(id), +{ + State { + worktrees: s.worktrees, + permanent: s.permanent, + running: s.running, + dirty: s.dirty, + unpushed: s.unpushed, + snapshots: s.snapshots.insert(id), + changes: s.changes, + } +} + +pub open spec fn delete_after_snapshot(s: State, id: int) -> State + recommends + wf(s), + s.worktrees.contains(id), +{ + let snap = snapshot_success(s, id); + State { + worktrees: snap.worktrees.remove(id), + permanent: snap.permanent.remove(id), + running: snap.running.remove(id), + dirty: snap.dirty.remove(id), + unpushed: snap.unpushed.remove(id), + snapshots: snap.snapshots, + changes: snap.changes.remove(id), + } +} + +pub open spec fn promote(s: State, id: int) -> State + recommends + wf(s), + s.worktrees.contains(id), +{ + State { + worktrees: s.worktrees, + permanent: s.permanent.insert(id), + running: s.running, + dirty: s.dirty, + unpushed: s.unpushed, + snapshots: s.snapshots, + changes: s.changes, + } +} + +pub open spec fn restore(s: State, id: int) -> State + recommends + wf(s), + s.snapshots.contains(id), + !s.worktrees.contains(id), +{ + State { + worktrees: s.worktrees.insert(id), + permanent: s.permanent.remove(id), + running: s.running.remove(id), + dirty: s.dirty.remove(id), + unpushed: s.unpushed.remove(id), + snapshots: s.snapshots, + changes: s.changes.insert(id), + } +} + +pub open spec fn handoff_success(s: State, source: int, target: int) -> State + recommends + wf(s), + source != target, + s.worktrees.contains(source), + s.worktrees.contains(target), + s.changes.contains(source), +{ + State { + worktrees: s.worktrees, + permanent: s.permanent, + running: s.running, + dirty: s.dirty, + unpushed: s.unpushed, + snapshots: s.snapshots, + changes: s.changes.insert(target), + } +} + +pub proof fn lemma_create_adds_fresh_idle_ephemeral(s: State, id: int) + requires + wf(s), + !s.worktrees.contains(id), + ensures + wf(create(s, id)), + create(s, id).worktrees.contains(id), + !create(s, id).permanent.contains(id), + !create(s, id).running.contains(id), + !create(s, id).dirty.contains(id), + !create(s, id).unpushed.contains(id), + !create(s, id).changes.contains(id), + forall|other: int| other != id ==> ( + #[trigger] create(s, id).worktrees.contains(other) <==> s.worktrees.contains(other) + ), + forall|other: int| other != id ==> ( + #[trigger] create(s, id).snapshots.contains(other) <==> s.snapshots.contains(other) + ), +{ +} + +pub proof fn lemma_delete_removes_exactly_one_after_snapshot(s: State, id: int) + requires + wf(s), + s.worktrees.contains(id), + ensures + wf(delete_after_snapshot(s, id)), + !delete_after_snapshot(s, id).worktrees.contains(id), + delete_after_snapshot(s, id).snapshots.contains(id), + !delete_after_snapshot(s, id).permanent.contains(id), + !delete_after_snapshot(s, id).running.contains(id), + !delete_after_snapshot(s, id).dirty.contains(id), + !delete_after_snapshot(s, id).unpushed.contains(id), + forall|other: int| other != id ==> ( + #[trigger] delete_after_snapshot(s, id).worktrees.contains(other) + <==> s.worktrees.contains(other) + ), + forall|other: int| other != id ==> ( + #[trigger] delete_after_snapshot(s, id).snapshots.contains(other) + <==> s.snapshots.contains(other) + ), +{ +} + +pub proof fn lemma_promote_is_idempotent(s: State, id: int) + requires + wf(s), + s.worktrees.contains(id), + ensures + wf(promote(s, id)), + promote(s, id).permanent.contains(id), + forall|other: int| #[trigger] promote(s, id).worktrees.contains(other) + <==> promote(promote(s, id), id).worktrees.contains(other), + forall|other: int| #[trigger] promote(s, id).permanent.contains(other) + <==> promote(promote(s, id), id).permanent.contains(other), + forall|other: int| #[trigger] s.permanent.contains(other) + ==> promote(s, id).permanent.contains(other), +{ +} + +pub proof fn lemma_gc_preview_selects_only_safe_excess( + s: State, + selected: Set, + excess: nat, +) + requires + wf(s), + gc_preview_valid(s, selected, excess), + ensures + selected.len() <= excess, + forall|id: int| #[trigger] selected.contains(id) ==> s.worktrees.contains(id), + forall|id: int| #[trigger] selected.contains(id) ==> !s.permanent.contains(id), + forall|id: int| #[trigger] selected.contains(id) ==> !s.running.contains(id), + forall|id: int| #[trigger] selected.contains(id) ==> !s.dirty.contains(id), + forall|id: int| #[trigger] selected.contains(id) ==> !s.unpushed.contains(id), +{ +} + +pub proof fn lemma_restore_preserves_snapshot_metadata(s: State, id: int) + requires + wf(s), + s.snapshots.contains(id), + !s.worktrees.contains(id), + ensures + wf(restore(s, id)), + restore(s, id).worktrees.contains(id), + restore(s, id).snapshots.contains(id), + !restore(s, id).permanent.contains(id), + !restore(s, id).running.contains(id), + !restore(s, id).dirty.contains(id), + !restore(s, id).unpushed.contains(id), + forall|snapshot: int| #[trigger] restore(s, id).snapshots.contains(snapshot) + <==> s.snapshots.contains(snapshot), +{ +} + +pub proof fn lemma_handoff_success_only_mutates_target(s: State, source: int, target: int) + requires + wf(s), + source != target, + s.worktrees.contains(source), + s.worktrees.contains(target), + s.changes.contains(source), + ensures + wf(handoff_success(s, source, target)), + handoff_success(s, source, target).changes.contains(source), + handoff_success(s, source, target).changes.contains(target), + forall|id: int| id != target ==> ( + #[trigger] handoff_success(s, source, target).changes.contains(id) + <==> s.changes.contains(id) + ), + forall|id: int| #[trigger] handoff_success(s, source, target).worktrees.contains(id) + <==> s.worktrees.contains(id), + forall|id: int| #[trigger] handoff_success(s, source, target).snapshots.contains(id) + <==> s.snapshots.contains(id), +{ +} + +} + From 280f261ba91915f83c9d6f5f05a244da8695a22e Mon Sep 17 00:00:00 2001 From: Dragosh <39906742+0dragosh@users.noreply.github.com> Date: Thu, 23 Apr 2026 17:48:48 +0300 Subject: [PATCH 2/2] Document the verification sidecar for agents --- docs/verification.md | 236 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 236 insertions(+) create mode 100644 docs/verification.md diff --git a/docs/verification.md b/docs/verification.md new file mode 100644 index 0000000..8f2f1d0 --- /dev/null +++ b/docs/verification.md @@ -0,0 +1,236 @@ +# Verification Guide for Agents + +This document explains why `cwt` has a Verus sidecar verification layer, what +it is useful for, and what an agent should update when changing workflow +behavior in this repository. + +## Purpose + +The verification layer exists to keep a small set of workflow guarantees +explicit and hard to regress. + +`cwt` manages mutable state across git worktrees, snapshots, session state, and +handoff operations. Those flows are easy to break with local changes that look +reasonable in isolation. The sidecar model gives agents a place to state the +intended invariants directly, while Rust tests check that the real code still +behaves consistently with those invariants. + +This is intentionally not a proof of all production code. It is a proof of the +workflow rules we care about most. + +## Why This Is Useful + +For agents modifying this repo, the sidecar helps in three ways: + +1. It makes the intended behavior of create, delete, promote, GC, restore, and + handoff concrete instead of implicit. +2. It forces trusted boundaries to be named, rather than hand-waved. +3. It gives a second line of defense beyond ordinary Rust tests: an abstract + model plus conformance tests against real temporary repos. + +In practice, this is most useful when you are: + +- changing worktree lifecycle rules +- changing what GC is allowed to prune +- changing snapshot / restore behavior +- changing handoff semantics +- adding a new workflow transition that should preserve existing invariants + +## Verus Principles We Rely On + +The sidecar follows a few core principles from the Verus guide: + +- Verus is for static verification. The goal is to prove properties ahead of + time rather than adding runtime checks to production code. +- Verus separates `spec`, `proof`, and `exec` concerns. In `cwt`, we keep the + verified model in sidecar `spec` / `proof` code and leave production Rust as + ordinary executable code. +- Verification always depends on a trusted computing base. If some behavior is + outside the proof boundary, it must be called out explicitly as an assumption. + +Useful references: + +- +- +- + +## Why A Sidecar Instead Of Annotating `src/` + +For this repo, the sidecar approach is deliberate. + +We want the first pass to verify workflow correctness without refactoring the +production code into verifier-friendly shapes. `cwt` depends on git commands, +filesystem effects, tmux state, and CLI behavior. Treating those as fully +verified implementation details would expand scope sharply and slow iteration. + +The sidecar model keeps the proof target narrow: + +- model the workflow state transitions abstractly +- prove invariants over those transitions +- validate the real implementation with Rust tests on real git repos + +That gives useful assurance without pretending we have verified git, tmux, or +the operating system. + +## What Is Verified + +The current sidecar model in [verification/workflow.rs](../verification/workflow.rs) +covers: + +- create adds a fresh idle ephemeral worktree +- delete removes exactly one worktree after snapshot success +- promote is idempotent and never demotes permanent worktrees +- GC preview only selects safe ephemeral worktrees and never exceeds the + required excess +- restore recreates a worktree from snapshot metadata without consuming the + snapshot +- handoff preserves source changes and only mutates the intended target on + successful apply + +The matching conformance coverage lives in +[tests/workflow_conformance.rs](../tests/workflow_conformance.rs), with a few +targeted production-path tests in +[src/worktree/manager.rs](../src/worktree/manager.rs) and +[src/worktree/handoff.rs](../src/worktree/handoff.rs). + +## What Is Not Verified + +The sidecar does not prove: + +- git itself +- patch application internals +- tmux or zellij behavior +- filesystem atomicity beyond the assumptions we document +- wall-clock correctness +- TUI rendering or interaction logic +- the Verus toolchain, Rust compiler, or solver + +Those are trusted boundaries and must stay documented in +[verification/ASSUMPTIONS.md](../verification/ASSUMPTIONS.md). + +## Files You Must Update + +When you change workflow behavior, check these files deliberately: + +### `verification/workflow.rs` + +Update this when the abstract workflow rules change. + +Examples: + +- a new lifecycle state changes whether something is GC-safe +- restore semantics change +- handoff changes what counts as source preservation +- a new transition should preserve existing invariants + +If production behavior changes and this file does not, that is usually a smell. + +### `verification/ASSUMPTIONS.md` + +Update this when the trust boundary changes. + +Examples: + +- new dependence on external command truth +- new filesystem assumption +- new runtime fact relied on by the workflow model + +If you rely on something outside the proof boundary, write it down here. + +### `tests/workflow_conformance.rs` + +Update this when the real implementation should be checked against a changed or +new invariant. + +The rule is simple: if the Verus model says some behavior matters, there should +usually be a Rust test that exercises the real code path too. + +### `scripts/verify-verus.sh` + +Update this if the verification entrypoint changes. + +Right now it is intentionally simple: run all Verus files under +`verification/`, and fail early with the exact `rustup install` command when +the required toolchain is missing. + +## How To Extend The Verification Layer + +When adding a new workflow rule: + +1. Decide whether it belongs in the abstract model or only in production tests. +2. If it is a workflow invariant, encode it in `verification/workflow.rs`. +3. Document any new trust boundary in `verification/ASSUMPTIONS.md`. +4. Add or extend Rust conformance tests. +5. Keep the model narrow. Do not pull unrelated implementation detail into the + proof just because it exists. + +Good candidates: + +- selection rules +- preservation properties +- idempotence properties +- “only mutates X” style guarantees +- “never chooses Y” style safety rules + +Bad candidates for this layer: + +- UI details +- subprocess output formatting +- low-level git behavior that is better treated as trusted command truth + +## How To Run It + +For normal repo validation: + +```sh +cargo test +nix build +``` + +For the Verus environment: + +```sh +nix develop .#verus +./scripts/verify-verus.sh +``` + +Or in one command: + +```sh +nix develop .#verus -c ./scripts/verify-verus.sh +``` + +The pinned Verus release currently requires an exact Rust toolchain via +`rustup`. The script does not install that toolchain for you; it prints the +exact `rustup install ...` command instead. + +## How To Read Failures + +If a Verus run fails: + +- first ask whether the workflow model is stale +- then ask whether the production behavior is wrong +- then ask whether a new assumption has been introduced but not documented + +If Rust conformance tests fail while Verus still passes: + +- the abstract model is likely still true, but the real implementation drifted +- fix the implementation, or change the model and tests together if the behavior + change is intended + +If production code changes but neither the model nor the tests need updates, +that is fine only if the change is outside the modeled workflow surface. + +## Agent Checklist + +Before finishing a workflow-related change, check: + +- Did I change a modeled transition? +- Did I change a trusted boundary? +- Did I update the conformance tests? +- Did I keep the proof target narrow? +- Did I rerun the relevant Rust and Verus commands? + +If the answer to the first two questions is yes and the docs/model stayed +unchanged, revisit the change before you call it done. +