kverus-strip

Aggressively strip redundant proof code from a Verus codebase while keeping verification passing. Be as aggressive as possible — many proof blocks and assertions exist purely for human readability and are not needed for the SMT solver to succeed.

Preferred invocation:

$kverus-strip verify="<verification command>" target-dirs="<dir1,dir2>"

If verify is missing, ask for it before editing. If target-dirs is missing, first run the proof simplification script for changed files; ask for target-dirs only before doing broader manual proof-code stripping.

Arguments

• verify (required): The full verification command, e.g. cargo verus focus my_crate.
• target-dirs (required for broader manual stripping): Comma-separated source directories or single .rs files to scan, e.g. src/,specs/ or src/model/owners.rs. A path the script would otherwise need to discover can be passed directly here.
• function (optional): Comma-separated function short names to restrict stripping to, e.g. lemma_index_bounds. Only matching functions are processed; all others in the file are left untouched.
• base (optional): Git base ref for changed-file discovery, e.g. origin/main.

Shared Verus References

If understanding Verus proof constructs (proof blocks, ghost/tracked values, spec/proof functions) is needed before deciding deletions, read the relevant reference under ../kverus-common/references/ before editing.

Proof Simplification Script

For routine redundant proof-statement cleanup, prefer the bundled script before manual stripping:

. "$AGENT_DIR/kverus.env"
"$KVERUS_PYTHON" "$AGENT_DIR/skills/kverus-strip/scripts/simplify_proof.py" \
  --base <git-base> \
  --target-dir '<dir1,dir2>' \
  --verify-command '<verification command>' \
  --format-command '<format command>'

The script scans changed .rs files when no --target-dir or --file is provided. It simplifies at function scope, matches the src/refiner/simplifier.py policy, skips runtime assert!(...), never removes assert(false), skips functions containing admit, assume, or #[verifier::external_body] unless --deep-clean is set, removes one proof statement at a time, and keeps the removal only when verification still succeeds. The rlimit perf guard (revert a passing strip when the Z3 rlimit grew by more than --perf-factor, measured via verus --time) applies only to functions carrying an explicit #[verifier::rlimit(...)] budget — those have a real cap a strip could push toward. Every other function strips purely on pass/fail: rlimit growth is not checked and no baseline probe verify is spent. Pass --no-perf-guard to apply that pass/fail-only behavior everywhere. With tree-sitter-verus, candidates include standalone function-call statements in proof fn, proof {}, and assertion proof blocks; executable calls are extracted but never offered for deletion. tree-sitter-verus is required and the script errors out if it is missing. Use --dry-run to list candidates without editing. Each candidate prints one bare outcome line — ✓ removed mod.rs:218 assert(fid != id);, ✗ kept … (verify failed), ~ kept … (rlimit exceeded: N > Kx baseline M) — (DEBUG-level sink, shown by default; --quiet hides them; colored on a tty, symbols only when piped). The tqdm bar postfix carries the live ✓N ✗N tally plus the candidate currently being verified, so there is no separate trying line. Each file first logs stripping <path>: N function(s) so the short filename in outcome lines stays unambiguous; kept … lines end with the bare reason and no more detail than that.