Merge branch 'main' into proofs/idris2-129-overwrite-irreversible-redesign

Author: hyperpolymath

impl/rust-cli/fuzz/fuzz_targets/fuzz_glob_expansion.rs

@@ -11,6 +11,7 @@
 #![no_main]
 
 use libfuzzer_sys::fuzz_target;
+use tempfile::TempDir;
 use vsh::glob::expand_glob;
 
 fuzz_target!(|data: &[u8]| {
@@ -33,12 +34,18 @@ fuzz_target!(|data: &[u8]| {
             return;
         }
 
+        // Create temporary directory for glob expansion
+        let temp = match TempDir::new() {
+            Ok(t) => t,
+            Err(_) => return,
+        };
+
         // Expand glob (should complete quickly or return error)
         // Should NEVER:
         // - Hang (exponential backtracking)
         // - Panic
         // - Use excessive memory
-        let _ = expand_glob(pattern);
+        let _ = expand_glob(pattern, temp.path());
 
         // Test cases include:
         // - Simple wildcards: *.txt, file?.rs

impl/rust-cli/fuzz/fuzz_targets/fuzz_path_operations.rs

@@ -35,7 +35,7 @@ fuzz_target!(|data: &[u8]| {
             Err(_) => return,
         };
 
-        let mut state = match ShellState::new(temp.path()) {
+        let mut state = match ShellState::new(temp.path().to_str().unwrap()) {
             Ok(s) => s,
             Err(_) => return,
         };

impl/rust-cli/fuzz/fuzz_targets/fuzz_state_machine.rs

@@ -51,7 +51,7 @@ fuzz_target!(|data: &[u8]| {
         Err(_) => return,
     };
 
-    let mut state = match ShellState::new(temp.path()) {
+    let mut state = match ShellState::new(temp.path().to_str().unwrap()) {
         Ok(s) => s,
         Err(_) => return,
     };
@@ -75,7 +75,7 @@ fuzz_target!(|data: &[u8]| {
                 let _ = rm(&mut state, &target, true);
             }
             Action::Undo => {
-                let _ = state.pop_undo();
+                let _ = state.pop_redo();
             }
             Action::Redo => {
                 let _ = state.pop_redo();
@@ -95,7 +95,7 @@ fuzz_target!(|data: &[u8]| {
         .map(|e| e.count())
         .unwrap_or(0);
 
-    while state.pop_undo().is_ok() {
+    while state.pop_redo().is_ok() {
         // Keep undoing
     }
 

proofs/lean4/FilesystemModel.lean

@@ -1,10 +1,10 @@
 /- Valence Shell - Filesystem Model (Lean 4)
 
-   A formal model of POSIX-like filesystem operations for proving
-   MAA (Mutually Assured Accountability) properties.
+    A formal model of POSIX-like filesystem operations for proving
+    MAA (Mutually Assured Accountability) properties.
 
-   This model focuses on directory operations (mkdir/rmdir) with
-   the goal of proving reversibility and correctness properties.
+    This model focuses on directory operations (mkdir/rmdir) with
+    the goal of proving reversibility and correctness properties.
 -/
 
 -- Path Model
@@ -94,6 +94,7 @@ theorem nonempty_path_ne_parent (p : Path) (h : p ≠ []) :
     have hp2 : p.reverse = x :: rest := hp
     rw [heq] at hp2
     simp at hp2
+    contradiction
 
 theorem pathExists_emptyFS_root :
     pathExists rootPath emptyFS := by