proofs(lean4) + tests: A-12 path-traversal containment

Closes frontier item A-12 from docs/PROOF-OPEN-FRONTIER.adoc: prove
that ShellState::resolve_path always returns a PathBuf within the
sandbox root, regardless of `..` / `.` / normal components in the
input.

Regression-guard for the 2026-02-12 CVE-class audit fix
(resolve_path("../../etc/passwd") previously escaped the sandbox).

Lean 4 — proofs/lean4/PathTraversal.lean
* Models the Rust resolve_path loop as Component → applyComponent.
* Proves applyComponent_preserves_root_prefix per component.
* Lifts to normalizeRaw_within_root via foldl invariant.
* Headline: path_traversal_containment.
* Corollary: normalizePath_eq_normalizeRaw (final clamp never fires).
* Wired into lakefile.lean as lean_lib PathTraversal.
* Verified: lean PathTraversal.lean exit 0.

Rust — impl/rust-cli/tests/security_tests.rs
* property_resolve_path_stays_within_sandbox — proptest with mixed
  ../ + ./ + normal components, optional leading /.
* property_resolve_path_parent_dir_heavy_stays_within_sandbox —
  10:1 weighted toward `..` to specifically target the audit failure
  mode. Each runs 256 random cases (proptest default).
* All 17 security tests pass (existing 15 + 2 new).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

impl/rust-cli/tests/security_tests.rs

@@ -12,6 +12,7 @@
 mod fixtures;
 
 use fixtures::tempfile::TempDir;
+use proptest::prelude::*;
 use std::fs;
 use vsh::parser::parse_command;
 use vsh::state::ShellState;
@@ -114,6 +115,93 @@ fn security_path_traversal_protection() {
     }
 }
 
+// ============================================================
+// Path traversal containment — property test for frontier A-12
+// ============================================================
+//
+// The headline theorem `PathTraversal.path_traversal_containment` in
+// `proofs/lean4/PathTraversal.lean` proves that the Rust normaliser's
+// loop-body invariant holds for arbitrary component sequences. This
+// property test is the Rust-side validation that the implementation
+// matches the Lean model: regardless of how many `..` / `.` / normal
+// components appear (or in what order), `resolve_path` always returns
+// a `PathBuf` that starts with the sandbox root.
+//
+// Regression-guard for the 2026-02-12 CVE-class audit fix
+// (`resolve_path("../../etc/passwd")` previously escaped the sandbox).
+
+/// Generate a single path component as a string fragment.
+/// Mix of `..`, `.`, and short normal names to exercise every branch
+/// of the normaliser loop.
+fn component_strategy() -> impl Strategy<Value = String> {
+    prop_oneof![
+        Just("..".to_string()),
+        Just(".".to_string()),
+        "[a-zA-Z0-9_-]{1,8}".prop_map(|s| s),
+    ]
+}
+
+/// Build a path string from a sequence of components, with optional
+/// leading slash to exercise the absolute-path strip.
+fn path_strategy() -> impl Strategy<Value = String> {
+    (any::<bool>(), prop::collection::vec(component_strategy(), 0..20))
+        .prop_map(|(absolute, parts)| {
+            let joined = parts.join("/");
+            if absolute {
+                format!("/{}", joined)
+            } else {
+                joined
+            }
+        })
+}
+
+proptest! {
+    /// `resolve_path(p)` is always a descendant of the sandbox root, for
+    /// any input `p` (any mix of `..`, `.`, normal components, with or
+    /// without leading slash). Mirrors `PathTraversal.path_traversal_containment`.
+    #[test]
+    fn property_resolve_path_stays_within_sandbox(path in path_strategy()) {
+        let temp = TempDir::new().unwrap();
+        let state = ShellState::new(temp.path().to_str().unwrap()).unwrap();
+        let resolved = state.resolve_path(&path);
+
+        // The sandbox root as the implementation sees it. We compare
+        // path-prefix (not canonical-realpath) because the resolved
+        // path may not physically exist; the Lean theorem is about
+        // structural prefix, not filesystem realpath.
+        let root = temp.path();
+        prop_assert!(
+            resolved.starts_with(root),
+            "resolve_path({:?}) returned {:?}, which does not start with sandbox root {:?}",
+            path, resolved, root
+        );
+    }
+
+    /// Stronger variant: paths heavily stocked with `..` (10× more
+    /// likely than normal components) still stay contained. Targets
+    /// the specific 2026-02-12 audit failure mode.
+    #[test]
+    fn property_resolve_path_parent_dir_heavy_stays_within_sandbox(
+        path in prop::collection::vec(
+            prop_oneof![
+                10 => Just("..".to_string()),
+                1  => "[a-z]{1,4}".prop_map(|s| s),
+            ],
+            1..30,
+        ).prop_map(|parts| parts.join("/"))
+    ) {
+        let temp = TempDir::new().unwrap();
+        let state = ShellState::new(temp.path().to_str().unwrap()).unwrap();
+        let resolved = state.resolve_path(&path);
+        let root = temp.path();
+        prop_assert!(
+            resolved.starts_with(root),
+            "..-heavy path {:?} escaped sandbox: resolved={:?}, root={:?}",
+            path, resolved, root
+        );
+    }
+}
+
 #[test]
 fn security_absolute_path_handling() {
     let temp = TempDir::new().unwrap();

proofs/lean4/PathTraversal.lean

@@ -0,0 +1,182 @@
+/- SPDX-License-Identifier: MPL-2.0
+   Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+   Valence Shell — Path-traversal containment proof (frontier item A-12)
+
+   Formalises the path-normalisation discipline implemented by
+   `vsh::state::ShellState::resolve_path` in `impl/rust-cli/src/state.rs`
+   and proves that the result is always within the sandbox root,
+   regardless of `..` components in the input.
+
+   The 2026-02-12 audit caught a real CVE-class bug here
+   (`resolve_path("../../etc/passwd")` escaped the sandbox before the
+   `normalized.starts_with(root)` check + `..`-pop guard landed). This
+   module is the regression-guard.
+
+   Companion property test:
+   `impl/rust-cli/tests/security_tests.rs::property_resolve_path_stays_within_sandbox`
+-/
+
+namespace PathTraversal
+
+-- Path representation matches `FilesystemModel.Path` (List String of
+-- components). Kept local to avoid coupling: this module is about
+-- containment of a path-string normalisation, not about the
+-- filesystem semantics.
+abbrev Path := List String
+
+-- A raw path component as parsed from a user-supplied string.
+-- Mirrors `std::path::Component` in Rust (the three variants
+-- `resolve_path` switches on; we elide RootDir/Prefix since the
+-- Rust code strips them before normalisation).
+inductive Component where
+  | parentDir : Component
+  | curDir    : Component
+  | normal    : String → Component
+  deriving DecidableEq, Repr
+
+-- Step the normaliser by one component. Matches the Rust loop body:
+--   `..` → pop if normalized strictly extends root (still within root
+--          AND not at root); silently clamp at root otherwise
+--   `.`  → skip
+--   name → append
+def applyComponent (root normalized : Path) (c : Component) : Path :=
+  match c with
+  | Component.parentDir =>
+      if root <+: normalized ∧ normalized ≠ root then
+        normalized.dropLast
+      else
+        normalized
+  | Component.curDir    => normalized
+  | Component.normal s  => normalized ++ [s]
+
+-- Drive the normaliser over a list of components, starting from
+-- `root` as the initial accumulator (matches the Rust implementation,
+-- which starts `normalized` empty and pre-joins with root).
+def normalizeRaw (root : Path) (raw : List Component) : Path :=
+  raw.foldl (applyComponent root) root
+
+-- The final safety check (Rust line 589-593 in `state.rs`): if the
+-- accumulated result somehow does not start with root, clamp to root.
+-- This is defensive; the foldl invariant we prove below means the
+-- check never fires, but the clamp is what makes the theorem closed-
+-- form regardless of `applyComponent` correctness.
+def normalizePath (root : Path) (raw : List Component) : Path :=
+  let n := normalizeRaw root raw
+  if root <+: n then n else root
+
+-- ---------------------------------------------------------------------
+-- Helper lemmas
+-- ---------------------------------------------------------------------
+
+-- Appending on the right preserves prefix (`xs <+: ys → xs <+: ys ++ zs`).
+-- This is the key compositional step used by the `Component.normal`
+-- case. Uses `List.prefix_append` (every list is a prefix of itself
+-- appended) plus transitivity of `<+:`.
+theorem isPrefix_append_right
+    (xs ys zs : Path) (h : xs <+: ys) :
+    xs <+: ys ++ zs :=
+  h.trans (List.prefix_append ys zs)
+
+-- Dropping the last element preserves a prefix, provided the prefix
+-- itself wasn't the whole list (otherwise dropping erases an element
+-- of the prefix and breaks containment).
+theorem isPrefix_dropLast
+    (xs ys : Path)
+    (hp : xs <+: ys) (hne : ys ≠ xs) :
+    xs <+: ys.dropLast := by
+  -- Obtain the witness suffix: ys = xs ++ tail
+  obtain ⟨tail, htail⟩ := hp
+  -- tail must be non-empty (if it were [], then ys = xs ++ [] = xs,
+  -- contradicting hne).
+  cases tail with
+  | nil =>
+      exfalso; apply hne
+      simpa using htail.symm
+  | cons t ts =>
+      -- ys = xs ++ (t :: ts); dropLast strips the trailing element.
+      -- ys.dropLast = (xs ++ (t :: ts)).dropLast = xs ++ (t :: ts).dropLast
+      -- (since t :: ts is non-empty), so xs is still a prefix.
+      refine ⟨(t :: ts).dropLast, ?_⟩
+      subst htail
+      rw [List.dropLast_append_of_ne_nil _ (List.cons_ne_nil t ts)]
+
+-- ---------------------------------------------------------------------
+-- Per-step invariant
+-- ---------------------------------------------------------------------
+
+-- Applying one component preserves the root-prefix invariant.
+theorem applyComponent_preserves_root_prefix
+    (root normalized : Path) (c : Component)
+    (h : root <+: normalized) :
+    root <+: applyComponent root normalized c := by
+  cases c with
+  | curDir =>
+      unfold applyComponent
+      exact h
+  | normal s =>
+      unfold applyComponent
+      exact isPrefix_append_right root normalized [s] h
+  | parentDir =>
+      unfold applyComponent
+      by_cases hcond : root <+: normalized ∧ normalized ≠ root
+      · simp [hcond]
+        obtain ⟨hpre, hne⟩ := hcond
+        exact isPrefix_dropLast root normalized hpre hne
+      · simp [hcond]; exact h
+
+-- ---------------------------------------------------------------------
+-- foldl invariant
+-- ---------------------------------------------------------------------
+
+-- foldl preserves the root-prefix invariant for any initial accumulator
+-- that already starts with root.
+theorem normalizeRaw_acc_preserves_root_prefix
+    (root : Path) :
+    ∀ (raw : List Component) (acc : Path),
+      root <+: acc →
+      root <+: raw.foldl (applyComponent root) acc := by
+  intro raw
+  induction raw with
+  | nil =>
+      intro acc h; exact h
+  | cons c rest ih =>
+      intro acc h
+      simp only [List.foldl]
+      apply ih
+      exact applyComponent_preserves_root_prefix root acc c h
+
+-- The intermediate result is always within root.
+theorem normalizeRaw_within_root (root : Path) (raw : List Component) :
+    root <+: normalizeRaw root raw := by
+  unfold normalizeRaw
+  exact normalizeRaw_acc_preserves_root_prefix root raw root (List.prefix_refl root)
+
+-- ---------------------------------------------------------------------
+-- Headline theorem (frontier A-12)
+-- ---------------------------------------------------------------------
+
+-- Path-traversal containment: `normalizePath root raw` is always a
+-- descendant of `root`, regardless of `..` / `.` / normal components
+-- in `raw`. This is the regression-guard for the 2026-02-12 CVE-class
+-- audit fix.
+theorem path_traversal_containment
+    (root : Path) (raw : List Component) :
+    root <+: normalizePath root raw := by
+  unfold normalizePath
+  by_cases h : root <+: normalizeRaw root raw
+  · simp [h]
+  · simp [h]
+
+-- Corollary: the final clamp never fires (the unfolded definition
+-- always lands on `normalizeRaw root raw`, never on the fallback
+-- `root`). Useful as a regression-guard against changes to
+-- `applyComponent` that would silently break the invariant.
+theorem normalizePath_eq_normalizeRaw
+    (root : Path) (raw : List Component) :
+    normalizePath root raw = normalizeRaw root raw := by
+  unfold normalizePath
+  have h : root <+: normalizeRaw root raw := normalizeRaw_within_root root raw
+  simp [h]
+
+end PathTraversal

proofs/lean4/lakefile.lean

@@ -48,3 +48,6 @@ lean_lib PermissionOperations where
 
 lean_lib CrashConsistency where
   srcDir := "."
+
+lean_lib PathTraversal where
+  srcDir := "."