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

docs/ABI-FFI-BOUNDARY.adoc

@@ -69,8 +69,8 @@ languages link against. The C-ABI-_provider_ role belongs to
 (11 exports, wired to the Idris2 ABI declarations). `+impl/zig/+` is an
 experimental fast-path lib plus a Lean-runtime wrapper, gated on the
 not-yet-built BEAM daemon. Collapsing the two is future work.
-* *The primary Rust CLI (`+impl/rust-cli/+`) does not link the FFI.* Its
-`+build.rs+` is intentionally a no-op; `+vsh+` is a self-contained
+* *The primary Rust CLI (`+impl/rust-cli/+`) does not link the FFI.* It has
+no `+build.rs+` and no link flags; `+vsh+` is a self-contained
 pure-Rust shell today. Wiring it to the Zig FFI is future work.
 
 === Deferred (code-level consolidation — needs owner sign-off)
@@ -80,8 +80,9 @@ the shipping shell:
 
 [arabic]
 . Port `+ffi/rust+` to Zig, or fold it behind the Zig FFI.
-. Wire `+impl/rust-cli+` to the Zig FFI (replace the no-op
-`+build.rs+`).
+. Wire `+impl/rust-cli+` to the Zig FFI (would need a `+build.rs+`
+and link flags; the former no-op `+build.rs+` and broken
+`+.cargo/config.toml+` link path were removed).
 . Collapse `+impl/zig+` into `+ffi/zig+`.
 
 Until then, the spine above is the documented contract, and the three

impl/rust-cli/src/commands.rs

@@ -78,8 +78,7 @@ pub enum CommandError {
 pub fn mkdir(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
     let full_path = state.resolve_path(path);
 
-    // Optional Lean 4 verification (compile-time feature flag)
-    // Provides mathematical guarantee that preconditions are satisfied
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_mkdir(state.root(), path)?;
 
     // Check preconditions (matching Coq)
@@ -146,7 +145,7 @@ pub fn mkdir(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
 pub fn rmdir(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
     let full_path = state.resolve_path(path);
 
-    // Optional Lean 4 verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_rmdir(state.root(), path)?;
 
     // Check preconditions
@@ -210,7 +209,7 @@ pub fn rmdir(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
 pub fn touch(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
     let full_path = state.resolve_path(path);
 
-    // Optional Lean 4 verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_create_file(state.root(), path)?;
 
     if full_path.exists() {
@@ -273,7 +272,7 @@ pub fn touch(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
 pub fn rm(state: &mut ShellState, path: &str, verbose: bool) -> Result<()> {
     let full_path = state.resolve_path(path);
 
-    // Optional Lean 4 verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_delete_file(state.root(), path)?;
 
     if !full_path.exists() {
@@ -341,7 +340,7 @@ pub fn cp(state: &mut ShellState, src: &str, dst: &str, verbose: bool) -> Result
     let src_path = state.resolve_path(src);
     let dst_path = state.resolve_path(dst);
 
-    // Optional verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_copy_file(state.root(), src, dst)?;
 
     // Check preconditions (matching Lean 4 copyFilePrecondition)
@@ -418,7 +417,7 @@ pub fn mv(state: &mut ShellState, src: &str, dst: &str, verbose: bool) -> Result
     let src_path = state.resolve_path(src);
     let dst_path = state.resolve_path(dst);
 
-    // Optional verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_move(state.root(), src, dst)?;
 
     // Check preconditions (matching Lean 4 movePrecondition)
@@ -496,7 +495,7 @@ pub fn mv(state: &mut ShellState, src: &str, dst: &str, verbose: bool) -> Result
 pub fn symlink(state: &mut ShellState, target: &str, link: &str, verbose: bool) -> Result<()> {
     let link_path = state.resolve_path(link);
 
-    // Optional verification
+    // Runtime check of the Lean 4 precondition (see verification.rs)
     verification::verify_symlink(state.root(), target, link)?;
 
     // Check preconditions (matching Lean 4 SymlinkPrecondition)

impl/rust-cli/src/state.rs

@@ -11,7 +11,7 @@ use colored::Colorize;
 use serde::{Deserialize, Serialize};
 use std::collections::{BTreeMap, HashMap, HashSet, VecDeque};
 use std::fs;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use uuid::Uuid;
 
 use crate::functions::FunctionTable;
@@ -561,38 +561,7 @@ impl ShellState {
     /// Resolve a path relative to sandbox root
     /// Prevents path traversal attacks via `..` components
     pub fn resolve_path(&self, path: &str) -> PathBuf {
-        let raw = if let Some(stripped) = path.strip_prefix('/') {
-            self.root.join(stripped)
-        } else {
-            self.root.join(path)
-        };
-
-        // Normalize path components to prevent traversal via ..
-        let mut normalized = PathBuf::new();
-        for component in raw.components() {
-            match component {
-                std::path::Component::ParentDir => {
-                    // Only pop if we're still within the sandbox root
-                    if normalized.starts_with(&self.root) && normalized != self.root {
-                        normalized.pop();
-                    }
-                    // If popping would escape root, silently clamp to root
-                }
-                std::path::Component::CurDir => {
-                    // Skip . components
-                }
-                other => {
-                    normalized.push(other);
-                }
-            }
-        }
-
-        // Final safety check: ensure result is within sandbox
-        if !normalized.starts_with(&self.root) {
-            self.root.clone()
-        } else {
-            normalized
-        }
+        resolve_under_root(&self.root, path)
     }
 
     /// Get root path as string (for Lean FFI)
@@ -949,6 +918,47 @@ struct SerializableState {
     previous_dir: Option<PathBuf>,
 }
 
+/// Resolve `path` against the sandbox `root`, clamping any `..` traversal so
+/// the result never escapes `root`.
+///
+/// A leading `/` is treated as relative to `root`; `.` components are dropped.
+/// This is the single path-resolution rule shared by [`ShellState::resolve_path`]
+/// and the precondition checks in [`crate::verification`].
+pub fn resolve_under_root(root: &Path, path: &str) -> PathBuf {
+    let raw = if let Some(stripped) = path.strip_prefix('/') {
+        root.join(stripped)
+    } else {
+        root.join(path)
+    };
+
+    // Normalize path components to prevent traversal via ..
+    let mut normalized = PathBuf::new();
+    for component in raw.components() {
+        match component {
+            std::path::Component::ParentDir => {
+                // Only pop if we're still within the sandbox root
+                if normalized.starts_with(root) && normalized != root {
+                    normalized.pop();
+                }
+                // If popping would escape root, silently clamp to root
+            }
+            std::path::Component::CurDir => {
+                // Skip . components
+            }
+            other => {
+                normalized.push(other);
+            }
+        }
+    }
+
+    // Final safety check: ensure result is within sandbox
+    if !normalized.starts_with(root) {
+        root.to_path_buf()
+    } else {
+        normalized
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;