fix: correct test assertions and version to 1.0.0

- Fixed Levenshtein distance test expectations (gti->git=2, mkdr->mkdir=1)
- Fixed logical AND test (StringNotEmpty for false case)
- Fixed ShellState::new path type in secure_deletion test
- Added enhanced-repl feature to Cargo.toml
- Removed unused import (std::sync::atomic::Ordering)
- Version updated from 0.14.0 to 1.0.0 in Cargo.toml and main.rs

All 198 unit tests + 10 integration tests now passing.

Author: Test

impl/ocaml/Makefile

@@ -0,0 +1,62 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Makefile for Lean 4 → C → OCaml extraction pipeline
+
+LEAN_PREFIX := $(shell lean --print-prefix)
+LEAN_INCLUDE := $(LEAN_PREFIX)/include
+LEAN_LIB := $(LEAN_PREFIX)/lib/lean
+
+# Directories
+LEAN_SRC := ../../proofs/lean4
+LEAN_BUILD := $(LEAN_SRC)/.lake/build
+LEAN_IR_DIR := $(LEAN_BUILD)/ir
+
+# Output library
+TARGET := liblean_vsh.so
+
+# Source files
+C_WRAPPER := lean_wrapper.c
+LEAN_EXTRACTION := Extraction
+
+.PHONY: all clean build-lean build-c test
+
+all: build-lean build-c
+
+# Step 1: Build Lean 4 code and extract to C
+build-lean:
+	@echo "Building Lean 4 extraction..."
+	cd $(LEAN_SRC) && lake build $(LEAN_EXTRACTION)
+	@echo "Lean compilation complete: $(LEAN_IR_DIR)/$(LEAN_EXTRACTION).c"
+
+# Step 2: Compile C wrapper + extracted Lean code to shared library
+build-c: build-lean
+	@echo "Compiling C wrapper to shared library..."
+	gcc -shared -fPIC -o $(TARGET) \
+		$(C_WRAPPER) \
+		$(LEAN_IR_DIR)/$(LEAN_EXTRACTION).c \
+		-I$(LEAN_INCLUDE) \
+		-L$(LEAN_LIB) \
+		-lleanshared \
+		-Wl,-rpath,$(LEAN_LIB)
+	@echo "Shared library created: $(TARGET)"
+
+# Test that the library loads
+test: all
+	@echo "Testing library loading..."
+	@if [ -f $(TARGET) ]; then \
+		echo "✓ $(TARGET) exists"; \
+		ldd $(TARGET) | grep lean || echo "Warning: Lean library not linked"; \
+	else \
+		echo "✗ $(TARGET) not found"; \
+		exit 1; \
+	fi
+
+# Clean build artifacts
+clean:
+	rm -f $(TARGET)
+	cd $(LEAN_SRC) && lake clean
+
+# Install library to system location (optional)
+install: all
+	@echo "Installing $(TARGET) to /usr/local/lib..."
+	sudo cp $(TARGET) /usr/local/lib/
+	sudo ldconfig

impl/ocaml/lean_wrapper.c

@@ -0,0 +1,293 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+/* Valence Shell - C Wrapper for Lean 4 Extracted Code
+ *
+ * This file provides C-callable wrappers around Lean 4 compiled code.
+ * It handles:
+ * - String marshaling between C and Lean
+ * - Filesystem state representation
+ * - Error code conversion
+ *
+ * Compiles to shared library (.so) for OCaml FFI consumption.
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <lean/lean.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/* Error codes matching Lean CErrorCode type */
+typedef enum {
+    VSH_ENOERR = 0,
+    VSH_EEXIST = 17,
+    VSH_ENOENT = 2,
+    VSH_EACCES = 13,
+    VSH_ENOTDIR = 20,
+    VSH_EISDIR = 21,
+    VSH_ENOTEMPTY = 39
+} vsh_error_t;
+
+/* Result type for operations */
+typedef struct {
+    int success;       /* 1 = success, 0 = failure */
+    vsh_error_t error; /* Error code if success = 0 */
+} vsh_result_t;
+
+/* Opaque filesystem handle
+ *
+ * In a full implementation, this would wrap:
+ * - Lean Filesystem value (abstract map)
+ * - Real POSIX filesystem root
+ * - Audit log handle
+ *
+ * For now, placeholder structure.
+ */
+typedef struct vsh_filesystem {
+    void* lean_fs_obj;  /* Lean object representing filesystem state */
+    char* root_path;    /* Root path for sandboxing */
+} vsh_filesystem_t;
+
+/* Create filesystem handle */
+vsh_filesystem_t* vsh_filesystem_create(const char* root) {
+    vsh_filesystem_t* fs = malloc(sizeof(vsh_filesystem_t));
+    if (!fs) return NULL;
+
+    fs->root_path = strdup(root);
+
+    /* Initialize Lean emptyFS object
+     * emptyFS : Filesystem = fun _ => none
+     * This is a constant empty map represented as a closure
+     */
+    fs->lean_fs_obj = lean_box(0);  /* Empty filesystem represented as null pointer */
+    lean_inc_ref(fs->lean_fs_obj);   /* Increment reference count */
+
+    return fs;
+}
+
+/* Destroy filesystem handle */
+void vsh_filesystem_destroy(vsh_filesystem_t* fs) {
+    if (!fs) return;
+    free(fs->root_path);
+
+    /* Decrement Lean object reference count */
+    if (fs->lean_fs_obj) {
+        lean_dec_ref(fs->lean_fs_obj);
+    }
+
+    free(fs);
+}
+
+/* Helper: Convert C string to Lean String
+ *
+ * Lean strings are UTF-8 encoded objects.
+ * This uses Lean runtime API to create them.
+ */
+static lean_object* c_str_to_lean_str(const char* c_str) {
+    return lean_mk_string(c_str);
+}
+
+/* Helper: Convert Lean String to C string
+ *
+ * Returns newly allocated C string (caller must free).
+ */
+static char* lean_str_to_c_str(lean_object* lean_str) {
+    const char* data = lean_string_cstr(lean_str);
+    return strdup(data);
+}
+
+/* Helper: Convert Lean CResult to vsh_result_t */
+static vsh_result_t lean_result_to_c(lean_object* lean_result) {
+    vsh_result_t result;
+
+    /* Extract fields from Lean CResult structure
+     *
+     * Lean structure layout:
+     * CResult.mk : Bool -> CErrorCode -> CResult
+     *
+     * Field 0: success (Bool - unboxed u8)
+     * Field 1: errorCode (CErrorCode enum - unboxed u8)
+     */
+
+    /* Extract success field (Bool) */
+    uint8_t success = lean_unbox(lean_ctor_get(lean_result, 0));
+    result.success = (success != 0) ? 1 : 0;
+
+    /* Extract errorCode field (CErrorCode enum) */
+    uint8_t error_code = lean_unbox(lean_ctor_get(lean_result, 1));
+    result.error = (vsh_error_t)error_code;
+
+    return result;
+}
+
+/* Safe mkdir wrapper
+ *
+ * Calls Lean safeMkdirStr function to check preconditions.
+ * Returns success/error code.
+ * Does NOT perform actual mkdir (that's done by OCaml FFI layer).
+ */
+vsh_result_t vsh_safe_mkdir(vsh_filesystem_t* fs, const char* path) {
+    if (!fs || !path) {
+        vsh_result_t err = {0, VSH_ENOENT};
+        return err;
+    }
+
+    /* Convert C path to Lean String */
+    lean_object* lean_path = c_str_to_lean_str(path);
+
+    /* Get Lean filesystem object */
+    lean_object* lean_fs = (lean_object*)fs->lean_fs_obj;
+    lean_inc_ref(lean_fs);  /* Increment before passing to Lean */
+
+    /* Call Lean safeMkdirStr function
+     * Signature: safeMkdirStr (pathStr : String) (fs : Filesystem) : CResult
+     */
+    extern lean_object* l_ValenceShell_Extraction_safeMkdirStr(lean_object*, lean_object*);
+    lean_object* lean_result = l_ValenceShell_Extraction_safeMkdirStr(lean_path, lean_fs);
+
+    /* Convert Lean CResult to C result */
+    vsh_result_t result = lean_result_to_c(lean_result);
+
+    /* Clean up Lean objects */
+    lean_dec_ref(lean_result);
+
+    return result;
+}
+
+/* Safe rmdir wrapper */
+vsh_result_t vsh_safe_rmdir(vsh_filesystem_t* fs, const char* path) {
+    if (!fs || !path) {
+        vsh_result_t err = {0, VSH_ENOENT};
+        return err;
+    }
+
+    lean_object* lean_path = c_str_to_lean_str(path);
+
+    /* Get Lean filesystem object */
+    lean_object* lean_fs = (lean_object*)fs->lean_fs_obj;
+    lean_inc_ref(lean_fs);
+
+    /* Call Lean safeRmdirStr function */
+    extern lean_object* l_ValenceShell_Extraction_safeRmdirStr(lean_object*, lean_object*);
+    lean_object* lean_result = l_ValenceShell_Extraction_safeRmdirStr(lean_path, lean_fs);
+
+    vsh_result_t result = lean_result_to_c(lean_result);
+
+    lean_dec_ref(lean_result);
+    return result;
+}
+
+/* Safe file creation wrapper */
+vsh_result_t vsh_safe_create_file(vsh_filesystem_t* fs, const char* path) {
+    if (!fs || !path) {
+        vsh_result_t err = {0, VSH_ENOENT};
+        return err;
+    }
+
+    lean_object* lean_path = c_str_to_lean_str(path);
+
+    /* Get Lean filesystem object */
+    lean_object* lean_fs = (lean_object*)fs->lean_fs_obj;
+    lean_inc_ref(lean_fs);
+
+    /* Call Lean safeCreateFileStr function */
+    extern lean_object* l_ValenceShell_Extraction_safeCreateFileStr(lean_object*, lean_object*);
+    lean_object* lean_result = l_ValenceShell_Extraction_safeCreateFileStr(lean_path, lean_fs);
+
+    vsh_result_t result = lean_result_to_c(lean_result);
+
+    lean_dec_ref(lean_result);
+    return result;
+}
+
+/* Safe file deletion wrapper */
+vsh_result_t vsh_safe_delete_file(vsh_filesystem_t* fs, const char* path) {
+    if (!fs || !path) {
+        vsh_result_t err = {0, VSH_ENOENT};
+        return err;
+    }
+
+    lean_object* lean_path = c_str_to_lean_str(path);
+
+    /* Get Lean filesystem object */
+    lean_object* lean_fs = (lean_object*)fs->lean_fs_obj;
+    lean_inc_ref(lean_fs);
+
+    /* Call Lean safeDeleteFileStr function */
+    extern lean_object* l_ValenceShell_Extraction_safeDeleteFileStr(lean_object*, lean_object*);
+    lean_object* lean_result = l_ValenceShell_Extraction_safeDeleteFileStr(lean_path, lean_fs);
+
+    vsh_result_t result = lean_result_to_c(lean_result);
+
+    lean_dec_ref(lean_result);
+    return result;
+}
+
+/* Test function to verify linking */
+const char* vsh_get_version(void) {
+    return "Valence Shell Lean FFI v0.1.0";
+}
+
+#ifdef __cplusplus
+}
+#endif
+
+/*
+ * Implementation Notes
+ * ====================
+ *
+ * Completing this wrapper requires:
+ *
+ * 1. Include Lean-generated header:
+ *    #include "Extraction.h"  // Generated by Lean compiler
+ *
+ * 2. Link against Lean runtime:
+ *    -lleanshared
+ *
+ * 3. Understand Lean object layout:
+ *    - Lean objects are reference-counted
+ *    - Use lean_inc_ref() / lean_dec_ref()
+ *    - Structures accessed via field offsets
+ *
+ * 4. Call Lean functions:
+ *    extern lean_object* ValenceShell_Extraction_safeMkdirStr(
+ *        lean_object* path,
+ *        lean_object* fs
+ *    );
+ *
+ * 5. Handle Lean Sum/Option types:
+ *    - CResult is a structure: { success : Bool, errorCode : CErrorCode }
+ *    - Extract via lean_ctor_get()
+ *
+ * Example complete implementation of vsh_safe_mkdir:
+ *
+ * vsh_result_t vsh_safe_mkdir(vsh_filesystem_t* fs, const char* path) {
+ *     lean_object* lean_path = c_str_to_lean_str(path);
+ *     lean_object* lean_fs = (lean_object*)fs->lean_fs_obj;
+ *
+ *     // Call Lean function
+ *     lean_object* lean_result = ValenceShell_Extraction_safeMkdirStr(
+ *         lean_path, lean_fs
+ *     );
+ *
+ *     // Extract fields from CResult structure
+ *     uint8_t success = lean_unbox(lean_ctor_get(lean_result, 0));
+ *     uint8_t error_code = lean_unbox(lean_ctor_get(lean_result, 1));
+ *
+ *     vsh_result_t result = {
+ *         .success = success,
+ *         .error = (vsh_error_t)error_code
+ *     };
+ *
+ *     // Clean up
+ *     lean_dec_ref(lean_result);
+ *
+ *     return result;
+ * }
+ *
+ * Reference:
+ * - Lean 4 FFI Guide: https://lean-lang.org/lean4/doc/dev/ffi.html
+ * - Lean Runtime API: $(lean --print-prefix)/include/lean/lean.h
+ */