fix(rust-cli): real Lean precondition checks in verification.rs (P0-5)

[hyperpolymath]

ULTRAPLAN P0-5. Until now the seven verify_* functions in impl/rust-cli/src/verification.rs returned Ok(()). Each one now checks, against the real filesystem, the Lean precondition its operation is proved under.

Rust	Lean	Checks, in order
verify_mkdir	MkdirPrecondition (FilesystemModel.lean:119)	target absent (lstat) → parent exists → parent is dir → parent writable
verify_rmdir	RmdirPrecondition (FilesystemModel.lean:129)	exists (lstat) → real dir → no entries → not sandbox root → parent writable
verify_create_file	CreateFilePrecondition (FileOperations.lean:11)	as mkdir
verify_delete_file	DeleteFilePrecondition (FileOperations.lean:20)	exists (lstat) → not dir → regular file or symlink → parent writable
verify_copy_file	copyFilePrecondition	src exists → src not dir → dst absent → dst parent exists → src regular file → dst parent dir → src readable → dst parent writable
verify_move	movePrecondition	src exists → dst absent → src ≠ dst → not into itself → dst parent exists → src/dst parents writable
verify_symlink	SymlinkPrecondition	link absent (lstat) → parent exists → parent dir → parent writable (the target is deliberately not checked)

Status, in the plan's taxonomy: each mapping is TESTED, not PROVEN. The Rust checks are written by hand to mirror the Lean Props, not extracted from them. Correspondence is checked by review plus 41 new positive and negative unit tests. The module doc says so.

Commits

1. fix(rust-cli): implement real Lean precondition checks
   • Path resolution moves to state::resolve_under_root, so the verifiers and ShellState::resolve_path use one rule. The body is moved, not changed.
   • Each verifier first repeats the checks the command already makes, in the same order and with byte-identical messages, then applies the conditions only Lean has. User-visible errors therefore stay the same.
2. chore(rust-cli): remove broken .cargo/config.toml and no-op build.rs
   • The config's only content was rustflags with a literal $REPOS_DIR link path, for a lean-runtime-checks feature that nothing defines. There is no extern "C" and no #[link] in src/.
   • docs/ABI-FFI-BOUNDARY.adoc is updated to match.
3. fix(rust-cli): keep rmdir read_dir error text identical to the command

Behaviour changes (all from conditions the stub skipped)

• Dangling symlink at a mkdir/touch/cp destination: now already exists. Before, mkdir and touch failed with an OS error, and cp wrote through the link.
• rm on a FIFO, socket or device: refused (Path is not a regular file). The model has no such node.
• New messages, reached only through the Lean-only conditions: Parent is not a directory (ENOTDIR), … is not writable (EACCES), Source is not readable (EACCES), Cannot remove the sandbox root.
• mv follows Lean in not requiring the destination parent to be a directory, so the rename itself reports that case.

Evidence (rebased on main 3440d69)

cargo test                          suites=23 passed=827 failed=0 ignored=15
cargo clippy --all-targets -D warnings   clean
cargo fmt --check                   clean

• Before the change, on 4401867: 787 passed / 14 ignored.
• This PR adds 41 tests, all in verification.rs.
• One test moved from passed to ignored because fix(test): model oracle test fails instead of skipping as a pass (P0-4) #214 (P0-4) made the oracle test #[ignore].
• Mutant: putting the Ok(()) stub back into verify_mkdir fails all 5 mkdir negative tests, including the unwritable-parent test. That shows the permission tests really run as uid 1000.
• The permission tests skip themselves when run as root.

⚠ Finding: RmdirPrecondition is unsatisfiable (PROVEN)

isEmptyDir p fs (FilesystemModel.lean:69-71) quantifies over child.isPrefixOf p, which ranges over p's ancestors, not its children. So it requires p's parent not to exist, while parentWritable requires the parent to exist. This typechecks against this repo's FilesystemModel on Lean v4.34.1:

theorem rmdir_precondition_vacuous (p : Path) (fs : Filesystem)
    (h : RmdirPrecondition p fs) : False

The file was checked with lake env lean. As a control, adding example : (1:Nat) = 2 := by decide to the same file produces an error, so the file is really checked.

Consequence: every theorem that takes hpre : RmdirPrecondition p fs (in FilesystemModel, FilesystemEquivalence, FilesystemComposition) holds vacuously, including the mkdir/rmdir reversibility results.

The Rust here implements the evident intent ("the directory has no entries"), and its docstring records the gap. The Lean fix (p.isPrefixOf child, i.e. no descendant exists) belongs to the V1 proof phase, not this PR. It has been logged for the owner in dev-notes/inbox/findings.md.

Not in scope

• ffi/rust/src/verification.rs is a separate copy and is untouched.
• The ShellState::root() fallback to / for a non-UTF-8 root already existed and is unchanged.
• The CLAUDE.md test-count table (736) is stale; this PR does not update it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: dbc02ce9-bd36-4f16-b63c-b9766345ca27

📥 Commits

Reviewing files that changed from the base of the PR and between 3440d69 and 7cac31f.

📒 Files selected for processing (6)

• docs/ABI-FFI-BOUNDARY.adoc
• impl/rust-cli/.cargo/config.toml
• impl/rust-cli/build.rs
• impl/rust-cli/src/commands.rs
• impl/rust-cli/src/state.rs
• impl/rust-cli/src/verification.rs

 _______________________________________
< CI/CD: Carrots In / Defects Canceled. >
 ---------------------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

✨ Finishing Touches 💡 1

📝 Generate docstrings 💡

• 🔴 Error committing to branch - (🔄 Check to retry)
• Create a new PR

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[coderabbitai]

Autopilot could not be updated. Open Coding to check access and billing.

[coderabbitai]

❌ Failed to create Coding Agent finishing-touch task. Please try again.

[github-actions]

🔍 Hypatia Security Scan

Findings: 120 issues detected

Severity	Count
🔴 Critical	9
🟠 High	27
🟡 Medium	84

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "line": 38,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/cflite_batch.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_batch.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 45,
    "reason": "job in .github/workflows/cflite_pr.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/cflite_pr.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 20,
    "reason": "job in .github/workflows/instant-sync.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/instant-sync.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 83,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 52,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 88,
    "reason": "workflow .github/workflows/compilation_tests.yml:88 step `Run ignored tests (stress)` swallows non-zero exit via `continue-on-error: true` — failures will be masked",
    "type": "RE005",
    "file": ".github/workflows/compilation_tests.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence