kverus-review

Review Verus code changes for exec semantics, =~= usage, and verification quality before committing.

Preferred invocation:

$kverus-review verify="<verification command>"
$kverus-review commit=abc1234 verify="<verification command>"

If verify is missing, ask for it and stop. commit is optional.

Objective

Check uncommitted changes (or changes since a given commit) for three categories of issues and produce a structured report:

1. Exec code modifications and whether they change runtime semantics.
2. New =~= introductions and whether they can be replaced by ==.
3. Deleted comments and whether the deletion is justified.
4. Verification pass/fail and problematic warnings.

Arguments

• commit (optional): A git commit hash. When provided, review changes from that commit to HEAD. When omitted, review all uncommitted changes (unstaged + staged).
• verify (required): The target repository's documented verification command.

Shared Verus References

Locate reference files under the kverus-common skill's references/ directory by topic:

Topic	Reference File
Set / extensional equality / =~= vs ==	set-reasoning.md
Verus syntax / modes / exec-vs-spec-vs-proof	verus-syntax-quickref.md
Ghost / tracked / erasure	ghost-tracked.md
Verification error triage	common-errors.md

When evaluating =~= usage, read the "Set Extensional Equality via Bidirectional Forall" section from the set-reasoning.md reference.

Required Workflow

Step 0: Collect Change Set

Determine the diff scope:

With commit argument:

# List changed .rs files
git diff <commit>..HEAD --name-only -- '*.rs'

# Get diff content for a specific file
git diff <commit>..HEAD -- <file>

Without commit argument:

# List changed .rs files (unstaged + staged)
git diff HEAD --name-only -- '*.rs'
git diff --cached --name-only -- '*.rs'

# Get diff content
git diff HEAD -- <file>
git diff --cached -- <file>