fix(rest): unblock /api/v1/consult — 37 pre-existing rest-crate errors

- Add 13 missing variants to models::ProverKind (FStar, Dafny, Why3,
  TLAPS, Twelf, Nuprl, Minlog, Imandra, GLPK, SCIP, MiniZinc, Chuffed,
  ORTools) so the FFI ordinal table 17..29 round-trips through the
  REST schema.
- Wire core_kind_to_rest / rest_kind_to_core for the new variants
  (drops the "_ => Vampire" fallback for everything ≤ ord 29).
- Implement the 3 trait methods ProverBackend now requires on
  FfiProverBackend (search_theorems → empty-vec stub, config /
  set_config → store ProverConfig in the wrapper).
- Use CoreTacticResult (aliased import) consistently in apply_tactic;
  Success now takes ProofState by value, not Box<ProofState>.
- ProofState::new takes Term, not String — wrap parse_string content
  in Term::Var to match the new core API.
- Cast c_char ↔ u8 raw pointers across the Zig FFI boundary (CStr
  expects c_char; Zig declared the args as *const u8).

Reduces rest-crate errors 37 → 0. echidna lib tests still 637 passing.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: hyperpolymath

src/interfaces/rest/ffi_wrapper.rs

@@ -2,7 +2,7 @@
 // REST FFI Wrapper - Connects REST interface to ECHIDNA Rust core via Zig FFI
 
 use std::ffi::{CString, CStr};
-use std::os::raw::{c_int, c_void};
+use std::os::raw::{c_char, c_int, c_void};
 use anyhow::{Result, anyhow};
 
 // Re-export FFI types from core
@@ -32,7 +32,7 @@ pub fn init_ffi() -> Result<()> {
             let err_msg = if err_ptr.is_null() {
                 "Unknown FFI initialization error".to_string()
             } else {
-                CStr::from_ptr(err_ptr).to_string_lossy().into_owned()
+                CStr::from_ptr(err_ptr as *const c_char).to_string_lossy().into_owned()
             };
             return Err(anyhow!("FFI initialization failed: {}", err_msg));
         }
@@ -47,7 +47,7 @@ pub fn get_version() -> Result<String> {
         if ptr.is_null() {
             return Err(anyhow!("FFI version pointer is null"));
         }
-        let version = CStr::from_ptr(ptr).to_string_lossy().into_owned();
+        let version = CStr::from_ptr(ptr as *const c_char).to_string_lossy().into_owned();
         Ok(version)
     }
 }
@@ -59,7 +59,7 @@ pub fn get_last_error() -> Result<String> {
         if ptr.is_null() {
             return Err(anyhow!("No error message available"));
         }
-        let error = CStr::from_ptr(ptr).to_string_lossy().into_owned();
+        let error = CStr::from_ptr(ptr as *const c_char).to_string_lossy().into_owned();
         Ok(error)
     }
 }
@@ -88,7 +88,7 @@ pub fn destroy_prover(handle: i32) -> Result<()> {
 pub fn parse_string(handle: i32, content: &str) -> Result<()> {
     unsafe {
         let c_content = CString::new(content)?;
-        let rc = echidna_parse_string(handle, c_content.as_ptr(), content.len());
+        let rc = echidna_parse_string(handle, c_content.as_ptr() as *const u8, content.len());
         if rc != 0 {
             let error = get_last_error()?;
             return Err(anyhow!("Parse failed: {}", error));
@@ -109,7 +109,7 @@ pub fn verify_proof(handle: i32) -> Result<bool> {
 pub fn apply_tactic(handle: i32, tactic: &str) -> Result<bool> {
     unsafe {
         let c_tactic = CString::new(tactic)?;
-        let rc = echidna_apply_tactic(handle, c_tactic.as_ptr(), tactic.len());
+        let rc = echidna_apply_tactic(handle, c_tactic.as_ptr() as *const u8, tactic.len());
         Ok(rc == 0)
     }
 }

src/interfaces/rest/handlers.rs

@@ -22,11 +22,15 @@ use crate::{models::*, AppState, ProofSession};
 /// Wrapper for FFI-based prover backend
 struct FfiProverBackend {
     handle: i32,
+    config: ProverConfig,
 }
 
 impl FfiProverBackend {
     pub fn new(handle: i32) -> Self {
-        FfiProverBackend { handle }
+        FfiProverBackend {
+            handle,
+            config: ProverConfig::default(),
+        }
     }
 }
 
@@ -38,34 +42,34 @@ impl ProverBackend for FfiProverBackend {
     ) -> anyhow::Result<echidna::core::ProofState> {
         let content = std::fs::read_to_string(&path)?;
         ffi_wrapper::parse_string(self.handle, &content)?;
-        Ok(echidna::core::ProofState::new(content))
+        Ok(echidna::core::ProofState::new(Term::Var(content)))
     }
 
     async fn parse_string(&self, content: &str) -> anyhow::Result<echidna::core::ProofState> {
         ffi_wrapper::parse_string(self.handle, content)?;
-        Ok(echidna::core::ProofState::new(content.to_string()))
+        Ok(echidna::core::ProofState::new(Term::Var(content.to_string())))
     }
 
-    async fn verify_proof(&self, state: &echidna::core::ProofState) -> anyhow::Result<bool> {
+    async fn verify_proof(&self, _state: &echidna::core::ProofState) -> anyhow::Result<bool> {
         ffi_wrapper::verify_proof(self.handle)
     }
 
     async fn apply_tactic(
         &self,
         state: &echidna::core::ProofState,
         tactic: &CoreTactic,
-    ) -> anyhow::Result<TacticResult> {
+    ) -> anyhow::Result<CoreTacticResult> {
         let tactic_str = format!("{:?}", tactic);
         if ffi_wrapper::apply_tactic(self.handle, &tactic_str)? {
-            Ok(TacticResult::Success(Box::new(state.clone())))
+            Ok(CoreTacticResult::Success(state.clone()))
         } else {
-            Ok(TacticResult::Error("Tactic failed".to_string()))
+            Ok(CoreTacticResult::Error("Tactic failed".to_string()))
         }
     }
 
     async fn suggest_tactics(
         &self,
-        state: &echidna::core::ProofState,
+        _state: &echidna::core::ProofState,
         limit: usize,
     ) -> anyhow::Result<Vec<CoreTactic>> {
         let tactic_names = ffi_wrapper::suggest_tactics(self.handle, limit)?;
@@ -80,7 +84,7 @@ impl ProverBackend for FfiProverBackend {
         Ok(tactics)
     }
 
-    async fn export(&self, state: &echidna::core::ProofState) -> anyhow::Result<String> {
+    async fn export(&self, _state: &echidna::core::ProofState) -> anyhow::Result<String> {
         ffi_wrapper::export_proof(self.handle)
     }
 
@@ -92,6 +96,20 @@ impl ProverBackend for FfiProverBackend {
         // This is a bit simplified - in a real implementation we'd track the kind
         CoreProverKind::Lean // Default, would need to be set during creation
     }
+
+    async fn search_theorems(&self, _pattern: &str) -> anyhow::Result<Vec<String>> {
+        // FFI shim doesn't expose theorem search yet. Return empty list rather
+        // than failing so portfolio/search callers degrade gracefully.
+        Ok(Vec::new())
+    }
+
+    fn config(&self) -> &ProverConfig {
+        &self.config
+    }
+
+    fn set_config(&mut self, config: ProverConfig) {
+        self.config = config;
+    }
 }
 
 /// List all available provers (all 30)
@@ -558,7 +576,20 @@ fn core_kind_to_rest(kind: &CoreProverKind) -> ProverKind {
         CoreProverKind::EProver => ProverKind::EProver,
         CoreProverKind::SPASS => ProverKind::Spass,
         CoreProverKind::AltErgo => ProverKind::AltErgo,
-        _ => ProverKind::Vampire, // fallback for remaining provers
+        CoreProverKind::FStar => ProverKind::FStar,
+        CoreProverKind::Dafny => ProverKind::Dafny,
+        CoreProverKind::Why3 => ProverKind::Why3,
+        CoreProverKind::TLAPS => ProverKind::TLAPS,
+        CoreProverKind::Twelf => ProverKind::Twelf,
+        CoreProverKind::Nuprl => ProverKind::Nuprl,
+        CoreProverKind::Minlog => ProverKind::Minlog,
+        CoreProverKind::Imandra => ProverKind::Imandra,
+        CoreProverKind::GLPK => ProverKind::GLPK,
+        CoreProverKind::SCIP => ProverKind::SCIP,
+        CoreProverKind::MiniZinc => ProverKind::MiniZinc,
+        CoreProverKind::Chuffed => ProverKind::Chuffed,
+        CoreProverKind::ORTools => ProverKind::ORTools,
+        _ => ProverKind::Vampire, // fallback for remaining provers (>30 in core)
     }
 }
 
@@ -581,6 +612,19 @@ fn rest_kind_to_core(kind: &ProverKind) -> CoreProverKind {
         ProverKind::EProver => CoreProverKind::EProver,
         ProverKind::Spass => CoreProverKind::SPASS,
         ProverKind::AltErgo => CoreProverKind::AltErgo,
+        ProverKind::FStar => CoreProverKind::FStar,
+        ProverKind::Dafny => CoreProverKind::Dafny,
+        ProverKind::Why3 => CoreProverKind::Why3,
+        ProverKind::TLAPS => CoreProverKind::TLAPS,
+        ProverKind::Twelf => CoreProverKind::Twelf,
+        ProverKind::Nuprl => CoreProverKind::Nuprl,
+        ProverKind::Minlog => CoreProverKind::Minlog,
+        ProverKind::Imandra => CoreProverKind::Imandra,
+        ProverKind::GLPK => CoreProverKind::GLPK,
+        ProverKind::SCIP => CoreProverKind::SCIP,
+        ProverKind::MiniZinc => CoreProverKind::MiniZinc,
+        ProverKind::Chuffed => CoreProverKind::Chuffed,
+        ProverKind::ORTools => CoreProverKind::ORTools,
     }
 }
 

src/interfaces/rest/models.rs

@@ -24,6 +24,22 @@ pub enum ProverKind {
     EProver,
     Spass,
     AltErgo,
+    FStar,
+    Dafny,
+    Why3,
+    #[serde(rename = "tlaps")]
+    TLAPS,
+    Twelf,
+    Nuprl,
+    Minlog,
+    Imandra,
+    #[serde(rename = "glpk")]
+    GLPK,
+    #[serde(rename = "scip")]
+    SCIP,
+    MiniZinc,
+    Chuffed,
+    ORTools,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, ToSchema)]