Add typed-wasm prover backend + property test regressions

- typed_wasm.rs: new prover backend for typed-wasm integration
- Property test regression file from validation run
- Minor fixes to explanations and prover module registration

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

Author: hyperpolymath

src/rust/agent/explanations.rs

@@ -348,6 +348,7 @@ impl ExplanationGenerator {
             ProverKind::MiniZinc => "MiniZinc is a constraint modelling language compiling to multiple backend solvers.",
             ProverKind::Chuffed => "Chuffed uses lazy clause generation for constraint propagation with SAT-style learning.",
             ProverKind::ORTools => "OR-Tools provides constraint solving, routing, and linear/integer programming.",
+            ProverKind::TypedWasm => "TypedWasm is an internal oracle validating 10-level type safety for typed WASM memory regions.",
         }.to_string()
     }
 

src/rust/main.rs

@@ -557,6 +557,7 @@ fn info_command(prover: ProverKind, formatter: &OutputFormatter) -> Result<()> {
         ProverKind::MiniZinc => "Constraint modelling language with multiple backend solvers.",
         ProverKind::Chuffed => "Lazy clause generation CP solver with SAT-style learning.",
         ProverKind::ORTools => "Google OR-Tools. CP-SAT, routing, linear/integer programming.",
+        ProverKind::TypedWasm => "TypedWasm oracle. 10-level type safety validation for .twasm programs.",
     };
     formatter.info(&format!("  {}", description))?;
     formatter.info("")?;
@@ -592,6 +593,7 @@ fn info_command(prover: ProverKind, formatter: &OutputFormatter) -> Result<()> {
         ProverKind::MiniZinc => ".mzn / .dzn",
         ProverKind::Chuffed => ".fzn",
         ProverKind::ORTools => ".or / .proto",
+        ProverKind::TypedWasm => ".twasm",
     };
     formatter.info(&format!("  {}", extension))?;
     formatter.info("")?;
@@ -695,6 +697,7 @@ fn get_default_executable(kind: ProverKind) -> PathBuf {
         ProverKind::MiniZinc => PathBuf::from("minizinc"),
         ProverKind::Chuffed => PathBuf::from("fzn-chuffed"),
         ProverKind::ORTools => PathBuf::from("ortools_solve"),
+        ProverKind::TypedWasm => PathBuf::from("idris2"),
     }
 }
 

src/rust/provers/mod.rs

@@ -43,6 +43,7 @@ pub mod scip;
 pub mod minizinc;
 pub mod chuffed;
 pub mod ortools;
+pub mod typed_wasm;
 
 /// Enumeration of all supported provers
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
@@ -94,6 +95,9 @@ pub enum ProverKind {
     MiniZinc,
     Chuffed,
     ORTools,
+
+    // Prover oracles (internal structural validators)
+    TypedWasm,
 }
 
 impl std::str::FromStr for ProverKind {
@@ -131,6 +135,7 @@ impl std::str::FromStr for ProverKind {
             "minizinc" | "mzn" => Ok(ProverKind::MiniZinc),
             "chuffed" => Ok(ProverKind::Chuffed),
             "ortools" | "or-tools" => Ok(ProverKind::ORTools),
+            "typedwasm" | "typed-wasm" | "typed_wasm" | "twasm" => Ok(ProverKind::TypedWasm),
             _ => Err(anyhow::anyhow!("Unknown prover: {}", s)),
         }
     }
@@ -183,6 +188,7 @@ impl ProverKind {
             ProverKind::MiniZinc,
             ProverKind::Chuffed,
             ProverKind::ORTools,
+            ProverKind::TypedWasm,
         ]);
         provers
     }
@@ -220,6 +226,7 @@ impl ProverKind {
             ProverKind::MiniZinc => 2, // Constraint modelling
             ProverKind::Chuffed => 2,  // CP solver
             ProverKind::ORTools => 2,  // Constraint/optimization solver
+            ProverKind::TypedWasm => 3, // Internal oracle, structural analysis
         }
     }
 
@@ -262,6 +269,7 @@ impl ProverKind {
             ProverKind::MiniZinc => 5,
             ProverKind::Chuffed => 5,
             ProverKind::ORTools => 5,
+            ProverKind::TypedWasm => 1, // Internal oracle, tier 1 capability
         }
     }
 
@@ -293,6 +301,7 @@ impl ProverKind {
             ProverKind::MiniZinc => 1.0, // Constraint modelling
             ProverKind::Chuffed => 1.0,  // CP solver
             ProverKind::ORTools => 1.5,  // Constraint/optimization
+            ProverKind::TypedWasm => 2.0, // Internal oracle
         }
     }
 
@@ -329,6 +338,7 @@ impl ProverKind {
             ProverKind::MiniZinc => "minizinc",
             ProverKind::Chuffed => "fzn-chuffed",
             ProverKind::ORTools => "ortools_solve",
+            ProverKind::TypedWasm => "idris2", // Validates via Idris2 ABI
         }
     }
 }
@@ -460,6 +470,7 @@ impl ProverFactory {
             ProverKind::MiniZinc => Ok(Box::new(minizinc::MiniZincBackend::new(config))),
             ProverKind::Chuffed => Ok(Box::new(chuffed::ChuffedBackend::new(config))),
             ProverKind::ORTools => Ok(Box::new(ortools::ORToolsBackend::new(config))),
+            ProverKind::TypedWasm => Ok(Box::new(typed_wasm::TypedWasmBackend::new(config))),
         }
     }
 
@@ -493,6 +504,7 @@ impl ProverFactory {
             "pip" | "zpl" => Some(ProverKind::SCIP),  // SCIP/ZIMPL format
             "mzn" | "dzn" => Some(ProverKind::MiniZinc),  // MiniZinc format
             "fzn" => Some(ProverKind::Chuffed),  // FlatZinc (Chuffed input)
+            "twasm" => Some(ProverKind::TypedWasm),  // TypedWasm program
             _ => None,
         })
     }