Auto-commit: Sync changes [2026-02-10]

Author: Jonathan D.A. Jewell

PROVEN-LIBRARIES.md

@@ -1,383 +1,6 @@
-# stapeln Proven Library Integration
+# Proven Libraries (Extracted)
 
-**Date**: 2026-02-05
-**Standard**: ABI/FFI Universal (Idris2 → Zig → ReScript)
+The proven library workstream (Idris2 → Zig → ReScript DOM‑mounter) has been extracted.
+See:
 
----
-
-## 🔐 Overview
-
-stapeln uses **formal verification with Idris2 dependent types** for critical system operations. This document describes the proven library architecture and guarantees.
-
-## ⚡ The Proven Stack
-
-### Architecture: Three Layers
-
-```
-┌─────────────────────────────────────┐
-│  Layer 3: ReScript Bindings         │  Type-safe UI integration
-│  - DomMounter.res                   │  - Option types
-│  - Type-safe API                    │  - Result types
-└─────────────────────────────────────┘  - Pattern matching
-              ↓
-┌─────────────────────────────────────┐
-│  Layer 2: Zig FFI (C ABI)           │  Memory-safe implementation
-│  - ffi/zig/src/dom_mounter.zig     │  - Zero-cost abstractions
-│  - C-compatible interface           │  - No runtime overhead
-└─────────────────────────────────────┘  - Cross-platform
-              ↓
-┌─────────────────────────────────────┐
-│  Layer 1: Idris2 ABI (Proofs)       │  Formal guarantees
-│  - src/abi/DomMounter.idr           │  - Dependent types
-│  - Formal verification              │  - Total functions
-└─────────────────────────────────────┘  - Compile-time proofs
-```
-
----
-
-## 📋 Proven Components
-
-### 1. DOM Mounter (High-Assurance Mounting)
-
-**Files**:
-- **Idris2 ABI**: `frontend/src/abi/DomMounter.idr`
-- **Zig FFI**: `frontend/ffi/zig/src/dom_mounter.zig`
-- **ReScript**: `frontend/src/DomMounter.res`
-
-**Formal Proofs Provided**:
-
-#### Memory Safety
-```idris
-public export
-data NoMemoryLeak : Type where
-  SafeMount : NoMemoryLeak
-```
-**Guarantee**: Mounting operations never leak memory. Proven at compile-time.
-
-#### Thread Safety
-```idris
-public export
-data AtomicMount : Type where
-  Atomic : AtomicMount
-```
-**Guarantee**: All mount operations are atomic. No race conditions possible.
-
-#### Element Validation
-```idris
-public export
-data ValidElementId : String -> Type where
-  MkValidId : (s : String) -> ValidElementId s
-
-public export
-data ElementExists : String -> Type where
-  ElementFound : ValidElementId id -> ElementExists id
-```
-**Guarantee**: Element IDs are validated before use. Element existence checked before mounting.
-
-#### Totality
-```idris
-%default total
-```
-**Guarantee**: All functions provably terminate. No infinite loops or hangs.
-
----
-
-## 🎯 API Usage
-
-### ReScript Layer (Type-Safe)
-
-```rescript
-// Import the proven mounter
-open DomMounter
-
-// Safe mounting with Result type
-let result = mount("app")
-switch result {
-| Ok() => Js.Console.log("✓ Mounted with formal guarantees")
-| Error(msg) => Js.Console.error("Mount failed: " ++ msg)
-}
-
-// Convenience function for default element
-let appMountResult = mountToApp()
-
-// With callbacks
-mountWithCallback(
-  "app",
-  () => Js.Console.log("Success!"),
-  (err) => Js.Console.error(err)
-)
-```
-
-### Idris2 Layer (Formal Proofs)
-
-```idris
--- Full proof with all guarantees
-export
-mountWithProof : (id : String) -> (MountResult, NoMemoryLeak, AtomicMount)
-mountWithProof id = (MountSuccess, SafeMount, Atomic)
-```
-
-### Zig Layer (C ABI Implementation)
-
-```zig
-// C-compatible export
-export fn mount_to_element(element_id: [*:0]const u8) callconv(.C) c_int {
-    // Memory-safe Zig implementation
-    // Matches Idris2 ABI specification
-    return 0; // Success
-}
-```
-
----
-
-## ✅ Verification Status
-
-### Compile-Time Guarantees
-
-| Property | Status | Proof Location |
-|----------|--------|----------------|
-| **Memory Safety** | ✅ Proven | `NoMemoryLeak` in DomMounter.idr |
-| **Thread Safety** | ✅ Proven | `AtomicMount` in DomMounter.idr |
-| **Type Correctness** | ✅ Proven | Idris2 type system |
-| **Non-Empty IDs** | ✅ Proven | `ValidElementId` in DomMounter.idr |
-| **Element Exists** | ✅ Proven | `ElementExists` in DomMounter.idr |
-| **Termination** | ✅ Proven | `%default total` flag |
-
-### Runtime Guarantees
-
-- **Zero crashes** from mounting operations (proven impossible)
-- **Zero memory leaks** from mounting operations (proven impossible)
-- **Zero race conditions** in mount operations (proven impossible)
-- **Zero infinite loops** in mount code (proven impossible)
-
----
-
-## 🏗️ Directory Structure
-
-### Correct Layout (Following ABI/FFI Standard)
-
-```
-frontend/
-├── src/
-│   ├── abi/                    # Layer 1: Idris2 ONLY
-│   │   ├── DomMounter.idr     # ✅ Idris2 formal proofs
-│   │   ├── FileIO.idr         # ✅ Idris2 formal proofs
-│   │   └── build/             # ✅ Idris2 build artifacts (.ttc, .ttm)
-│   │
-│   ├── DomMounter.res         # Layer 3: ReScript bindings
-│   ├── App.res                # Layer 3: Application code
-│   └── IdrisBadge.res         # Layer 3: "Idris² inside" badge
-│
-├── ffi/
-│   └── zig/                    # Layer 2: Zig FFI
-│       ├── src/
-│       │   ├── dom_mounter.zig           # ✅ C ABI implementation
-│       │   ├── dom_mounter_enhanced.zig
-│       │   └── dom_mounter_security.zig
-│       ├── build.zig          # Zig build config
-│       └── libdom_mounter.so  # Compiled shared library
-│
-└── generated/
-    └── abi/                    # Auto-generated C headers (if needed)
-```
-
-### ❌ What NOT to Put in `src/abi/`
-
-- ❌ **NO Zig code** (belongs in `ffi/zig/`)
-- ❌ **NO ReScript code** (belongs in `src/`)
-- ❌ **NO C code** (belongs in `ffi/zig/` or `generated/`)
-- ❌ **NO JavaScript** (belongs in `src/`)
-- ❌ **NO build scripts** (belongs in `ffi/zig/`)
-
-### ✅ What DOES Belong in `src/abi/`
-
-- ✅ **Idris2 source files** (`*.idr`)
-- ✅ **Idris2 build artifacts** (`*.ttc`, `*.ttm`)
-- ✅ **Idris2 documentation** (if inline comments)
-
----
-
-## 🔬 Building the Proven Stack
-
-### Step 1: Compile Idris2 ABI
-
-```bash
-cd frontend/src/abi
-idris2 --build DomMounter.ipkg
-# Generates .ttc and .ttm files
-```
-
-### Step 2: Build Zig FFI
-
-```bash
-cd frontend/ffi/zig
-zig build
-# Generates libdom_mounter.so
-```
-
-### Step 3: Compile ReScript Bindings
-
-```bash
-cd frontend
-rescript build
-# Compiles DomMounter.res → DomMounter.res.js
-```
-
----
-
-## 🎨 UI Integration: Idris² Badge
-
-The "Idris² inside" badge (`IdrisBadge.res`) appears in the UI to indicate formal verification:
-
-### Badge Styles
-
-**Compact** (inline):
-```
-⚡ Idris²
-```
-
-**Standard** (standalone):
-```
-┌──────────────────┐
-│  ⚡  Idris² inside │
-│  Formally Verified│
-└──────────────────┘
-```
-
-**Detailed** (with proof list):
-```
-┌─────────────────────────────┐
-│  ⚡  Idris² inside            │
-│  Dependently-typed proofs    │
-│                              │
-│  🛡️ Memory Safe   ✓ PROVEN  │
-│  🔒 Thread Safe   ✓ PROVEN  │
-│  ✓  Type Correct  ✓ PROVEN  │
-│  📝 Non-Empty     ✓ PROVEN  │
-│  🔍 Element Exists ✓ PROVEN │
-└─────────────────────────────┘
-```
-
-### Usage in Components
-
-```rescript
-// In App.res footer
-<IdrisBadge style=Compact />
-
-// In documentation pages
-<IdrisBadge style=Standard />
-
-// In security inspector
-<IdrisBadge
-  style=Detailed
-  proofs=[MemorySafety, ThreadSafety, TypeCorrectness]
-/>
-```
-
----
-
-## 📊 Benefits of Formal Verification
-
-### Compared to Traditional Testing
-
-| Approach | Coverage | Guarantees |
-|----------|----------|------------|
-| **Unit Tests** | Sample inputs | No guarantees for untested cases |
-| **Property Tests** | Random inputs | High confidence, not certainty |
-| **Formal Proofs** | **ALL inputs** | **Mathematical certainty** |
-
-### Idris2 Advantages
-
-1. **Dependent Types**: Types can depend on values (e.g., `ValidElementId` depends on the string)
-2. **Totality Checking**: Compiler proves all functions terminate
-3. **Erasure**: Proofs disappear at runtime (zero overhead)
-4. **C ABI Export**: Direct FFI to Zig/C without wrapper costs
-
----
-
-## 🔒 Security Implications
-
-### Proven Security Properties
-
-**Memory safety proofs prevent**:
-- Buffer overflows
-- Use-after-free
-- Double-free
-- Memory leaks
-- Null pointer dereferences
-
-**Thread safety proofs prevent**:
-- Race conditions
-- Deadlocks (in proven sections)
-- Data races
-- Atomicity violations
-
-**Type correctness proofs prevent**:
-- Type confusion
-- Invalid casts
-- Uninitialized data
-- Type-based vulnerabilities
-
----
-
-## 📚 References
-
-### Idris2 Documentation
-- [Idris2 Official Docs](https://idris2.readthedocs.io/)
-- [Dependent Types Tutorial](https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html)
-- [FFI Guide](https://idris2.readthedocs.io/en/latest/ffi/ffi.html)
-
-### ABI/FFI Universal Standard
-- **Location**: `~/Documents/hyperpolymath-repos/rsr-template-repo/ABI-FFI-README.md`
-- **Established**: 2026-01-30
-- **Purpose**: Standardize Idris2 → Zig → Language bindings
-
-### Zig Documentation
-- [Zig C ABI](https://ziglang.org/documentation/master/#C)
-- [Zig Memory Safety](https://ziglang.org/documentation/master/#Memory)
-
----
-
-## 🎯 Future Proven Components
-
-### Planned Idris2 Proofs
-
-1. **Network Stack** (`frontend/src/abi/Network.idr`)
-   - Packet validation proofs
-   - Connection safety proofs
-   - Protocol correctness proofs
-
-2. **File I/O** (`frontend/src/abi/FileIO.idr`)
-   - Path traversal prevention proofs
-   - File descriptor safety proofs
-   - Atomic write proofs
-
-3. **Security Policies** (`frontend/src/abi/Security.idr`)
-   - Firewall rule correctness proofs
-   - Access control proofs
-   - Cryptographic protocol proofs
-
-4. **Resource Management** (`frontend/src/abi/Resources.idr`)
-   - Memory limit proofs
-   - CPU limit proofs
-   - No resource starvation proofs
-
----
-
-## ✨ Conclusion
-
-stapeln uses **formal verification with Idris2** to provide **compile-time guarantees** for critical operations. The "Idris² inside" badge indicates components backed by **mathematical proofs**, not just testing.
-
-**Key Takeaways**:
-- ✅ Memory safety is **proven**, not hoped for
-- ✅ Thread safety is **proven**, not tested
-- ✅ Type correctness is **proven** by the compiler
-- ✅ Zero runtime overhead (proofs erase at compile-time)
-- ✅ Clean ABI/FFI separation (Idris2 → Zig → ReScript)
-
----
-
-**Last Updated**: 2026-02-05
-**Verification Status**: ✅ All proofs passing
-**Build Status**: ✅ All layers compiling
-**Integration Status**: ✅ Badge visible in UI
+- `/var/mnt/eclipse/repos/stapeln-dom-mounter/docs/PROVEN-LIBRARIES.md`