Merge branch 'main' into claude/pin-toolchain-clippy

Author: hyperpolymath

docs/proofs/verification/AUDIT.md

@@ -185,8 +185,13 @@ treatment as the Lean file.
   - Coq models floats as `ℝ` ⇒ `value_eq_dec` is fully decidable (`Req_EM_T`),
     at the cost of the classical-reals axioms above. (Lean models `Float` as
     opaque IEEE and decides equality classically via `by_cases`.)
-  - Coq is **behind on binops**: only `add`/`eq`/`and` have rules — none of
-    `sub/mul/div/mod` or the comparisons/`or` the Lean file now has.
+  - Coq is now **at parity on integer binops** (landed 2026-06-15): on top of
+    `add`/`eq`/`and` it gains `or`, `sub`, `mul`, `div`/`mod` (which panic to
+    `VOops` on a zero divisor, mirroring the proven unwrap-of-oops fragment) and
+    the comparisons `lt`/`gt`/`le`/`ge` (`Z` → `bool`) — each with a `has_type`
+    rule, a `step` rule, and full `progress`/`preservation` coverage, axiom-free.
+    Float arithmetic variants remain unmodelled on both sides, and `BNeq` is a
+    symmetric gap (neither Lean nor Coq has it).
 
 - **`cap_subsumes` bug fixed.** Its catch-all was `TODO: false`, so the relation
   was **not even reflexive** (`cap_subsumes CapProcess CapProcess = false`).
@@ -199,7 +204,10 @@ treatment as the Lean file.
   large brute-force `try solve [...]` pile ending in a literal *"Nuclear
   option"* — it compiles and is axiom-honest, but is fragile and unreviewable.
   A clean per-case rewrite (in the style of the Lean `preservation`) is worth
-  doing. Also: bring the Coq binops up to parity with the extended Lean set.
+  doing — the binop-parity work (2026-06-15) extended its `first [...]`
+  reconstruction block and added an early literal-result closer rather than
+  rewriting it. (That cascade also scales badly: the new ops had to be closed
+  early and deterministically to avoid a multi-minute typecheck.)
 
 ## Status
 

docs/proofs/verification/WokeLang.v

@@ -151,7 +151,13 @@ fn main() -> Result<()> {
 }
 
 fn run_program(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {
@@ -189,7 +195,13 @@ fn run_program(file: &PathBuf) -> Result<()> {
 }
 
 fn compile_program(file: &PathBuf, _output: Option<PathBuf>) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {
@@ -245,7 +257,13 @@ fn compile_program(file: &PathBuf, _output: Option<PathBuf>) -> Result<()> {
 }
 
 fn run_vm(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
 
     // Use the vm::run_vm helper which compiles and runs
     match wokelang::vm::run_vm(&source) {
@@ -261,7 +279,13 @@ fn run_vm(file: &PathBuf) -> Result<()> {
 }
 
 fn disassemble(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
 
     // Compile to bytecode
     let compiled = match wokelang::vm::compile(&source) {
@@ -280,7 +304,13 @@ fn disassemble(file: &PathBuf) -> Result<()> {
 }
 
 fn typecheck_program(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {
@@ -314,7 +344,13 @@ fn typecheck_program(file: &PathBuf) -> Result<()> {
 }
 
 fn lint_program(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {
@@ -355,7 +391,13 @@ fn lint_program(file: &PathBuf) -> Result<()> {
 }
 
 fn tokenize_file(file: &PathBuf) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {
@@ -381,7 +423,13 @@ fn tokenize_file(file: &PathBuf) -> Result<()> {
 /// - `sexpr` / `sexp`: S-expression representation
 /// - `json`: JSON serialization via serde_json
 fn parse_file(file: &PathBuf, format: &str) -> Result<()> {
-    let source = fs::read_to_string(file).expect("Failed to read file");
+    let source = {
+        use std::io::Read;
+        let mut file_handle = std::fs::File::open(file).expect("Failed to open file");
+        let mut buf = String::new();
+        file_handle.take(10 * 1024 * 1024).read_to_string(&mut buf).expect("Failed to read file");
+        buf
+    };
     let lexer = Lexer::new(&source);
 
     let tokens = match lexer.tokenize() {

src/main.rs

@@ -138,8 +138,15 @@ impl ModuleLoader {
         self.loading.insert(path.clone());
 
         // Load and parse the file
-        let source = fs::read_to_string(&path)
-            .map_err(|e| ModuleError::IoError(format!("Failed to read {}: {}", path.display(), e)))?;
+        let source = {
+            use std::io::Read;
+            let mut file = std::fs::File::open(&path)
+                .map_err(|e| ModuleError::IoError(format!("Failed to open {}: {}", path.display(), e)))?;
+            let mut buf = String::new();
+            file.take(5 * 1024 * 1024).read_to_string(&mut buf)
+                .map_err(|e| ModuleError::IoError(format!("Failed to read {}: {}", path.display(), e)))?;
+            buf
+        };
 
         let lexer = Lexer::new(&source);
         let tokens = lexer
@@ -186,8 +193,15 @@ impl ModuleLoader {
         }
 
         // Load and parse
-        let source = fs::read_to_string(&path)
-            .map_err(|e| ModuleError::IoError(format!("Failed to read {}: {}", path.display(), e)))?;
+        let source = {
+            use std::io::Read;
+            let mut file = std::fs::File::open(&path)
+                .map_err(|e| ModuleError::IoError(format!("Failed to open {}: {}", path.display(), e)))?;
+            let mut buf = String::new();
+            file.take(5 * 1024 * 1024).read_to_string(&mut buf)
+                .map_err(|e| ModuleError::IoError(format!("Failed to read {}: {}", path.display(), e)))?;
+            buf
+        };
 
         let lexer = Lexer::new(&source);
         let tokens = lexer

src/modules.rs

@@ -99,7 +99,13 @@ impl ConsentStore {
             return Ok(());
         }
 
-        let content = fs::read_to_string(&self.path)?;
+        let content = {
+            use std::io::Read;
+            let mut file = std::fs::File::open(&self.path)?;
+            let mut buf = String::new();
+            file.take(1024 * 1024).read_to_string(&mut buf)?;
+            buf
+        };
 
         for line in content.lines() {
             if line.trim().is_empty() || line.starts_with('#') {

src/security/consent.rs

@@ -95,7 +95,14 @@ pub fn read_file(args: &[Value], caps: &mut CapabilityRegistry) -> Result<Value,
     // Check file size to prevent memory exhaustion
     check_file_size(&validated_path)?;
 
-    match fs::read_to_string(&validated_path) {
+    match {
+        use std::io::Read;
+        std::fs::File::open(&validated_path).and_then(|mut f| {
+            let mut buf = String::new();
+            f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
+            Ok(buf)
+        })
+    } {
         Ok(contents) => Ok(Value::String(contents)),
         Err(e) => Err(StdlibError::IoError(e.to_string())),
     }

src/stdlib/io.rs

@@ -364,9 +364,10 @@ fn http_request_binary_with_body(
             .map_err(|e| StdlibError::NetworkError(format!("Read body failed: {}", e)))?;
         buf
     } else {
-        // Read until connection closes
+        // Read until connection closes (limit to 5MB)
         let mut buf = Vec::new();
         reader
+            .take(5 * 1024 * 1024)
             .read_to_end(&mut buf)
             .map_err(|e| StdlibError::NetworkError(format!("Read body failed: {}", e)))?;
         buf