fix(server): guard against empty-ProofState false positives in verify/prove

Partial fix for the parse+export round-trip bug documented in
TEST-NEEDS.md: when the selected prover's parse_string returns an
empty ProofState for unrecognised input, the subsequent verify_proof
regenerated an empty prover source file that the real backend accepted
vacuously — producing valid=true for garbage input to Coq/Lean/Agda.

Added `is_empty_state` helper that checks goals, theorems, definitions,
axioms, and variables. If all are empty AND the request content is
non-empty, both handlers now return valid=false / success=false with
a clear message instead of round-tripping.

Verified live:
  garbage @#$ to Coq           → valid=false (was valid=true)
  empty to Coq                  → valid=true  (legitimately vacuous)
  'Theorem t : True. ...' Coq   → valid=true  (unchanged — real proof)
  unsat SMT to Z3               → valid=false (real Z3 result)

The deeper fix (making each prover preserve original content) still
outstanding — this guard catches the worst false-positive class and
makes /api/verify usable for training-signal collection without
bypassing it via the batch_driver's direct-binary approach.

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

Author: hyperpolymath

TEST-NEEDS.md

@@ -242,6 +242,16 @@ Idris2 has the mirror-image bug (false-negative): `parse_string` parses
 - Add regression tests: `verify` on garbage, empty, cross-prover content
   must all return `valid: false`.
 
+**Partial fix (2026-04-05):** server-level guard in `prove_handler` and
+`verify_handler` now returns `valid: false` when `parse_string` produces
+an empty `ProofState` (no goals, theorems, definitions, axioms, or variables)
+on non-empty input. Verified live:
+  - garbage to Coq/Lean: `valid: false` (was `true`)
+  - cross-prover (SMT to Coq): `valid: false`
+  - real Coq/Z3 proofs: still work correctly
+The deeper fix — making each prover backend preserve original content
+instead of round-tripping through ProofState — remains outstanding.
+
 ## Priority
 - **CRG C COMPLETE** as of 2026-04-04
 - Next priority: Fix 5 shell issues found by validation

src/rust/server.rs

@@ -238,6 +238,19 @@ async fn prove_handler(Json(req): Json<ProveRequest>) -> Result<Json<ProveRespon
         .await
         .map_err(|e| AppError::ParseError(e.to_string()))?;
 
+    // Fail-fast on empty parse results (fixes false-positive: unrecognised
+    // content produced an empty ProofState that re-exported to an empty file
+    // which the backend prover then happily accepted). Require at least one
+    // goal, theorem, definition, or axiom before we claim "parse succeeded".
+    if is_empty_state(&state) && !req.content.trim().is_empty() {
+        return Ok(Json(ProveResponse {
+            success: false,
+            goals: 0,
+            message: "Parse produced no goals, theorems, definitions, or axioms — \
+                     content not recognised by the selected prover backend".to_string(),
+        }));
+    }
+
     // Verify proof
     let valid = prover
         .verify_proof(&state)
@@ -270,6 +283,15 @@ async fn verify_handler(Json(req): Json<VerifyRequest>) -> Result<Json<VerifyRes
         .await
         .map_err(|e| AppError::ParseError(e.to_string()))?;
 
+    // Fail-fast on empty parse results (see prove_handler comment).
+    if is_empty_state(&state) && !req.content.trim().is_empty() {
+        return Ok(Json(VerifyResponse {
+            valid: false,
+            goals_remaining: 0,
+            tactics_used: 0,
+        }));
+    }
+
     // Verify
     let valid = prover
         .verify_proof(&state)
@@ -283,6 +305,19 @@ async fn verify_handler(Json(req): Json<VerifyRequest>) -> Result<Json<VerifyRes
     }))
 }
 
+/// Return true if the parsed ProofState contains no meaningful structure.
+/// Used to detect the parse+export round-trip bug: a prover backend's
+/// `parse_string` returns an empty state on unrecognised input, then
+/// `verify_proof` regenerates an empty file which the real backend binary
+/// then accepts vacuously (false positive).
+fn is_empty_state(state: &echidna::core::ProofState) -> bool {
+    state.goals.is_empty()
+        && state.context.theorems.is_empty()
+        && state.context.axioms.is_empty()
+        && state.context.definitions.is_empty()
+        && state.context.variables.is_empty()
+}
+
 /// Get tactic suggestions
 async fn suggest_handler(
     State(state): State<AppState>,