kverus-run

Run the complete Rust-to-Verus pipeline for one file or a directory of .rs files.

Preferred invocation:

$kverus-run target=path/to/file_or_dir verify="<verification command>"

If either target or verify is missing, ask for the missing value and stop.

If out_dir is missing, default to .kverus-run-output/ under the workspace root.

Pipeline Overview

Phase 0  Pre-flight ─────── validate inputs, snapshot originals
Phase 1  Migrate ─────────── Rust → Verus compatible code
Phase 2  Stage ──────────── git add migrated files
Phase 3  Spec ───────────── add requires/ensures/invariants
Phase 4  Fix ────────────── repair verification failures from spec
Phase 5  Eval ───────────── score spec quality (unstaged changes)
Phase 6  Semantic Audit ──── verify migration preserved runtime behavior
         ── QUALITY GATE ──  pause if critical semantic changes found
Phase 7  Postprocess ────── final review rules, assert simplification, fmt
Phase 8  Report ─────────── final summary

Shared Verus References

All phases that edit Verus code should consult ../kverus-common/references/ when encountering unfamiliar Verus syntax, modes, ghost/tracked values, loop invariants, quantifiers, or tokenized state-machine rules.

Phase 0: Pre-flight

1. Verify target exists.
2. Detect input type:
   • If target is a single .rs file: single-file mode. Set FILE_LIST = [target].
   • If target is a directory: directory mode. Discover all .rs files recursively. Sort by dependency order when possible (leaf modules first), otherwise alphabetical. Set FILE_LIST accordingly.
3. Verify the git workspace is clean for the files in FILE_LIST (no uncommitted changes). If dirty, warn the user and ask whether to continue.
4. Snapshot originals for audit:
   • Create a temporary directory: ORIG_DIR=$(mktemp -d).
   • Copy each file from FILE_LIST into ORIG_DIR preserving relative path structure.
   • Example: if target=src/lib.rs, copy to $ORIG_DIR/src/lib.rs.
5. Create out_dir if it does not exist.
6. Set AGENT_DIR to the installed agent directory for script calls. Skills are read from $AGENT_DIR/skills.
7. If KVERUS_POSTPROCESS_RULE_REPO is configured, run the postprocess checker with --cache-status. When the cache is stale or missing and subagents are available, delegate one --refresh-only command to a subagent. The subagent must make no source edits and preserve the old cache on failure. Continue the pipeline immediately; never perform or wait for a GitHub request in the main agent. If no subagent is available, proceed with cached or static rules.
8. Print a summary: mode (single/directory), file count, target path, verify command.