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/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.
+
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),
+{
+}
+
+}
+