fix(grpc)+security+test: resuscitate echidna-grpc, bump tonic, add live-prover roundtrip suite

Three coupled changes that leave the platform at 0 cargo-audit findings
with a test suite that actually exercises the Phase-3 backend fix.

### echidna-grpc

Eight pre-existing compile errors (unrelated to the tonic bump but
blocking it) are now fixed:

- `main.rs` was missing the `mod ffi_wrapper;` declaration even though
  `ffi_wrapper.rs` sat next to it.
- Three `echidna::core::ProofState::new(...)` callers were passing
  `String` / `&str`; the signature is now `new(goal: Term)`.  Wrap the
  raw content in `Term::Hole(...)` at every call site.
- `FfiProverBackend` was missing three required trait methods
  (`search_theorems`, `config`, `set_config`); added along with a
  `ProverConfig` field to satisfy the getter/setter pair.
- `TacticResult::Success` takes `ProofState` directly, not
  `Box<ProofState>` — unboxed.
- The local `CoreTacticResult` alias was unused; replaced the remaining
  three call sites with the re-exported `TacticResult`.
- `parse_file` now stashes `source_path` + `ffi_source` in metadata,
  matching the pattern introduced in the rest of `src/rust/provers/`.
- `ffi_wrapper.rs` `CStr::from_ptr(*const u8)` and `CString::as_ptr() →
  extern *const u8` calls were platform-dependent type mismatches;
  added `.cast()` at each boundary.  Dropped the `c_void` and
  `FfiStatus/FfiStringSlice/FfiOwnedString/FfiProverConfig` imports
  that weren't used.

### tonic 0.12 → 0.14 (clears RUSTSEC-2025-0134)

Once echidna-grpc compiles, the tonic bump is mechanical:

- Cargo.toml: `tonic` / `prost` pinned to `0.14`, `tonic-prost` added
  for the new split-out generated-code helper crate.
- Cargo.toml dev deps: `tonic` features `tls` → `tls-ring` (the default
  TLS provider flag rename in 0.14).
- build-dependencies: `tonic-build` → `tonic-prost-build`.
- build.rs: `tonic_build::compile_protos` → `tonic_prost_build::`.

`cargo audit` now reports "0 findings", down from:

- RUSTSEC-2025-0143 (capnp unsound API) — cleared earlier by
  commit c497661.
- RUSTSEC-2025-0134 (rustls-pemfile unmaintained, pulled transitively
  via tonic 0.12.3 → rustls-pemfile 2.2.0) — cleared by this bump.

### Live-prover verify roundtrip suite

`tests/live_prover_verify.rs` runs the real `ProverBackend::parse_file`
→ `verify_proof` pipeline against per-prover fixtures in
`tests/live_goals/`.  The 625-test unit suite stubs solver binaries, so
a regression in the Phase-3 "prefer source_path over lossy IR" fix
would not be caught there — this suite closes that gap by invoking the
actual binaries and asserting both the positive verdict on a valid
proof AND the negative verdict on a deliberately broken one.

Covered: Z3, CVC5, Coq, Agda, Metamath, SPASS (the six apt-installable
MVP provers).  Auto-skip when a binary is absent on PATH (same
convention as `live_prover_suite.rs`) so developers without every
prover installed don't see spurious failures; CI enables the
`live-provers` feature per-tier with the single binary provisioned.

Fixtures:
- `tautology.smt2` / `contradiction.smt2` (shared Z3/CVC5 pair).
- `identity.v` / `broken.v` (Coq).
- `Identity.agda` / `Broken.agda` (Agda).
- `trivial.mm`, `trivial.dfg` (Metamath, SPASS — positive-only).

`.gitignore` in `tests/live_goals/` drops Coq/Agda compilation
artifacts (`*.vo`, `*.vok`, `*.vos`, `*.glob`, `.<base>.aux`, `*.agdai`).

The 625 unit tests remain green.  The live-prover test binary compiles
cleanly; full end-to-end run confirmed via manual CLI invocation
earlier in the session (all six MVP provers return verified=true via
MCP tool-call).

https://claude.ai/code/session_01NaC5RXjTyr5xg9XXUa2FCC

Author: claude

Cargo.lock

@@ -18,8 +18,9 @@ path = "main.rs"
 
 [dependencies]
 # gRPC
-tonic = "0.12"
-prost = "0.13"
+tonic = "0.14"
+tonic-prost = "0.14"
+prost = "0.14"
 tokio = { version = "1.41", features = ["full"] }
 tokio-stream = "0.1"
 
@@ -45,7 +46,7 @@ uuid = { version = "1.11", features = ["v4", "serde"] }
 async-trait = "0.1"
 
 [build-dependencies]
-tonic-build = "0.12"
+tonic-prost-build = "0.14"
 
 [dev-dependencies]
-tonic = { version = "0.12", features = ["tls"] }
+tonic = { version = "0.14", features = ["tls-ring"] }

src/interfaces/grpc/Cargo.toml

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
 
 fn main() -> Result<(), Box<dyn std::error::Error>> {
-    tonic_build::compile_protos("proto/echidna.proto")?;
+    tonic_prost_build::compile_protos("proto/echidna.proto")?;
     Ok(())
 }

src/interfaces/grpc/build.rs

@@ -2,12 +2,9 @@
 // gRPC FFI Wrapper - Connects gRPC 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_int;
 use anyhow::{Result, anyhow};
 
-// Re-export FFI types from core
-pub use echidna::ffi::{FfiStatus, FfiStringSlice, FfiOwnedString, FfiProverConfig};
-
 // External Zig FFI functions (from libechidna_ffi.so)
 extern "C" {
     pub fn echidna_init() -> c_int;
@@ -32,7 +29,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.cast()).to_string_lossy().into_owned()
             };
             return Err(anyhow!("FFI initialization failed: {}", err_msg));
         }
@@ -47,7 +44,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.cast()).to_string_lossy().into_owned();
         Ok(version)
     }
 }
@@ -59,7 +56,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.cast()).to_string_lossy().into_owned();
         Ok(error)
     }
 }
@@ -88,7 +85,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().cast(), content.len());
         if rc != 0 {
             let error = get_last_error()?;
             return Err(anyhow!("Parse failed: {}", error));
@@ -109,7 +106,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().cast(), tactic.len());
         Ok(rc == 0)
     }
 }

src/interfaces/grpc/ffi_wrapper.rs

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
 // ECHIDNA gRPC Server - wired to core
 
-use echidna::core::{Tactic as CoreTactic, TacticResult as CoreTacticResult, Term};
+use echidna::core::{Tactic as CoreTactic, TacticResult, Term};
 use echidna::provers::{ProverBackend, ProverConfig, ProverFactory, ProverKind as CoreProverKind};
 use echidna_proto::v1::proof_service_server::{ProofService, ProofServiceServer};
 use echidna_proto::v1::*;
@@ -10,8 +10,8 @@ use std::sync::Arc;
 use tokio::sync::{Mutex, RwLock};
 use tonic::{transport::Server, Request, Response, Status};
 
-// Import FFI wrapper
-use crate::ffi_wrapper;
+// FFI wrapper module — file lives next to main.rs.
+mod ffi_wrapper;
 
 pub mod echidna_proto {
     pub mod v1 {
@@ -22,11 +22,15 @@ pub mod echidna_proto {
 /// 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,15 +42,29 @@ 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))
+        let mut state = echidna::core::ProofState::new(Term::Hole(content.clone()));
+        state.metadata.insert(
+            "source_path".to_string(),
+            serde_json::Value::String(path.to_string_lossy().into_owned()),
+        );
+        state.metadata.insert(
+            "ffi_source".to_string(),
+            serde_json::Value::String(content),
+        );
+        Ok(state)
     }
 
     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()))
+        let mut state = echidna::core::ProofState::new(Term::Hole(content.to_string()));
+        state.metadata.insert(
+            "ffi_source".to_string(),
+            serde_json::Value::String(content.to_string()),
+        );
+        Ok(state)
     }
 
-    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)
     }
 
@@ -57,15 +75,15 @@ impl ProverBackend for FfiProverBackend {
     ) -> anyhow::Result<TacticResult> {
         let tactic_str = format!("{:?}", tactic);
         if ffi_wrapper::apply_tactic(self.handle, &tactic_str)? {
-            Ok(TacticResult::Success(Box::new(state.clone())))
+            Ok(TacticResult::Success(state.clone()))
         } else {
             Ok(TacticResult::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 +98,13 @@ impl ProverBackend for FfiProverBackend {
         Ok(tactics)
     }
 
-    async fn export(&self, state: &echidna::core::ProofState) -> anyhow::Result<String> {
+    async fn search_theorems(&self, _pattern: &str) -> anyhow::Result<Vec<String>> {
+        // FFI layer doesn't expose theorem search yet; return empty so the
+        // gRPC service can still satisfy the trait contract.
+        Ok(Vec::new())
+    }
+
+    async fn export(&self, _state: &echidna::core::ProofState) -> anyhow::Result<String> {
         ffi_wrapper::export_proof(self.handle)
     }
 
@@ -92,6 +116,14 @@ 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
     }
+
+    fn config(&self) -> &ProverConfig {
+        &self.config
+    }
+
+    fn set_config(&mut self, config: ProverConfig) {
+        self.config = config;
+    }
 }
 
 struct ProofSession {
@@ -167,7 +199,9 @@ impl ProofService for ProofServiceImpl {
                             let session = ProofSession {
                                 prover_kind: core_kind,
                                 prover: Box::new(FfiProverBackend::new(handle)),
-                                state: Some(echidna::core::ProofState::new(req.goal.clone())),
+                                state: Some(echidna::core::ProofState::new(Term::Hole(
+                                    req.goal.clone(),
+                                ))),
                                 goal: req.goal.clone(),
                                 status,
                                 history: vec![],
@@ -377,7 +411,7 @@ impl ProofService for ProofServiceImpl {
             .map_err(|e| Status::internal(e.to_string()))?;
 
         let success = match &result {
-            CoreTacticResult::Success(new_state) => {
+            TacticResult::Success(new_state) => {
                 let complete = new_state.is_complete();
                 session.state = Some(new_state.clone());
                 session.history.push(format!("{:?}", tactic));
@@ -386,14 +420,14 @@ impl ProofService for ProofServiceImpl {
                 }
                 true
             },
-            CoreTacticResult::QED => {
+            TacticResult::QED => {
                 session.status = ProofStatus::Success as i32;
                 if let Some(s) = session.state.as_mut() {
                     s.goals.clear();
                 }
                 true
             },
-            CoreTacticResult::Error(_) => false,
+            TacticResult::Error(_) => false,
         };
 
         let elapsed = session.start_time.elapsed().as_secs_f64();
@@ -413,7 +447,7 @@ impl ProofService for ProofServiceImpl {
                 proof_script: script,
                 time_elapsed: Some(elapsed),
                 error_message: match &result {
-                    CoreTacticResult::Error(msg) => Some(msg.clone()),
+                    TacticResult::Error(msg) => Some(msg.clone()),
                     _ => None,
                 },
             }),

src/interfaces/grpc/main.rs

@@ -0,0 +1,8 @@
+# Coq compilation artifacts — generated when coqc runs on .v fixtures.
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux
+# Agda compilation artifacts
+*.agdai

tests/live_goals/.gitignore

@@ -0,0 +1,5 @@
+-- Type error: claims A → B from no premise.
+module Broken where
+
+bogus : (A : Set) -> (B : Set) -> A -> B
+bogus A B x = x

tests/live_goals/Broken.agda

@@ -0,0 +1,4 @@
+module Identity where
+
+id : (A : Set) -> A -> A
+id A x = x

tests/live_goals/Identity.agda

@@ -0,0 +1,3 @@
+(* Type error: claims `True -> False` and proves with `exact I`. *)
+Theorem broken : True -> False.
+Proof. intro H. exact I. Qed.

tests/live_goals/broken.v

@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(declare-const x Int)
+; Satisfiable assertion — SAT, so verify_proof reports "not verified".
+(assert (= x 1))
+(check-sat)