feat(v2.2): epistemic hardening — Z3 easy fixes, integration wiring, roadmap

Easy fixes (follow-up to 0c94943):
- z3.rs: preamble built once and reused; goal-set inconsistency check added
  (proves P and ¬P simultaneously → InconsistentPremises, not NoProofFound)
- z3.rs: parse_smt_result() now uses last non-empty output line (was whole-output
  contains(), which fired on error messages containing "sat")

Integration wiring:
- server.rs: /api/verify calls check() instead of verify_proof(); VerifyResponse
  gains outcome:String; parse errors → INVALID_INPUT outcome
- echidnabot/dispatcher/mod.rs: ProofStatus extended to full 8-variant taxonomy
  (PROVED/NO_PROOF_FOUND/INVALID_INPUT/UNSUPPORTED_FEATURE/TIMEOUT/
  INCONSISTENT_PREMISES/PROVER_ERROR/SYSTEM_ERROR) + is_verified()/is_retryable()
- echidnabot/dispatcher/echidna_client.rs: parse_proof_status() handles all 8
  taxonomy strings; RestVerifyResponse gains outcome:Option<String> with
  fallback to valid:bool for ECHIDNA <v2.2

Sanity suite:
- tests/sanity_suite.rs: added sanity_goal_set_inconsistency test (contradictory
  goal set); all Z3 integration tests use make_proof_state() direct construction
  instead of lossy parse_string() round-trip

Documentation:
- README.adoc: Outcome Contract section with 8-status table, invariants, commands
- echidnabot/ROADMAP.adoc: full milestone breakdown v0.2→v1.0
- .machine_readable/6a2/STATE.a2ml: session-2026-04-11 entry (v2.2.0)
- contractiles/lust/Intentfile: completed/future/invariant structure

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

README.adoc

@@ -299,9 +299,32 @@ just mvp        # MVP smoke checks (reports missing provers, non-fatal)
 | CI/CD | 17 workflows
 |===
 
-*Planned for v2.0*:
+*Completed in v2.2 (epistemic hardening)*:
+
+* Typed `ProverOutcome` taxonomy — 8 mutually-exclusive statuses replacing `Result<bool>`
+* Z3 `check()` override: inconsistency pre-check before trivial-goal short-circuit
+* Z3 output parsing uses last non-empty line (not whole-output `contains()`)
+* Z3 goal-set inconsistency detection (goals cannot all hold simultaneously)
+* Why3 timeout bug fixed (+5s undocumented slack removed)
+* Pre-colleague sanity suite: 37 tests covering full taxonomy with Z3 integration
+* `/api/verify` REST endpoint now returns typed `outcome` field alongside `valid: bool`
+* echidnabot `ProofStatus` extended to full 8-variant taxonomy, backward compatible
+
+*Roadmap — v2.3 (single-session Z3)*:
+
+* Replace two-process inconsistency check with single Z3 session using `(push)/(pop)` —
+  atomic, halves subprocess overhead
+* `check_raw_smt()` trait method for backends that accept pre-built content directly
+  (bypasses lossy `parse_string()` round-trip)
+
+*Roadmap — v2.4 (typed override coverage)*:
+
+Priority backends for typed `check()` overrides (currently use heuristic fallback):
+CVC5, Lean 4, Coq/Rocq, Isabelle. Each adds accurate `INCONSISTENT_PREMISES` and
+`UNSUPPORTED_FEATURE` detection for that backend.
+
+*Planned for v3.0*:
 
-* Full API-to-prover FFI/IPC integration
 * Deep learning models (Transformers via Flux.jl)
 * Production deployment configuration
 * Tamarin/ProVerif bridge for cipherbot

echidna-playground/contractiles/lust/Intentfile

@@ -1,21 +1,39 @@
-# SPDX-License-Identifier: PLMP-1.0-or-later
-# Intentfile template - declared future intent
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Intentfile — declared future intent for ECHIDNA epistemic hardening
 
 version: 1
 
+# Completed in v2.2 (2026-04-11)
+completed:
+  epistemic-taxonomy:
+    - "8-variant ProverOutcome taxonomy replacing Result<bool>."
+    - "Z3 check() override with three-phase consistency detection."
+    - "Z3 last-line output parsing replacing whole-output contains()."
+    - "Why3 timeout bug fixed; parse_outcome() preserves all distinctions."
+    - "37-test sanity suite covering full taxonomy with Z3 integration."
+    - "/api/verify REST endpoint exposes typed outcome field."
+    - "echidnabot ProofStatus extended to full 8-variant taxonomy."
+
 future:
-  trust-engine:
-    - "Integrate hardware-backed key management."
-    - "Support node attestation for deployments."
+  v2.3-single-session-z3:
+    - "Replace two-process inconsistency check with single Z3 session (push/pop)."
+    - "Add check_raw_smt() trait method to bypass parse_string round-trip."
+    - "Halves subprocess overhead; makes inconsistency+validity check atomic."
 
-  control-plane:
-    - "Move to GitOps-backed configuration promotion."
-    - "Add canary and staged rollout support."
+  v2.4-typed-override-coverage:
+    - "CVC5 typed check() override — same SMT-LIB surface as Z3."
+    - "Lean 4 typed check() override — most common interactive backend."
+    - "Coq/Rocq typed check() override — InconsistentPremises via tauto+exfalso."
+    - "Isabelle typed check() override — INCONSISTENT_PREMISES from simp pattern."
 
-  pipeline:
-    - "Adopt Nickel (or your DSL) as the primary policy language."
-    - "Automate policy promotion from dev to prod with signed artifacts."
+  v3.0-integration:
+    - "gitbot-fleet submodule pinned so echidnabot builds independently."
+    - "Deep learning models (Transformers via Flux.jl)."
+    - "Tamarin/ProVerif bridge for cipherbot."
+    - "Production deployment configuration."
 
-  introspection:
-    - "Expose decision latency and policy evaluation metrics."
-    - "Add tracing for end-to-end request decisions."
+  invariant:
+    - "Every failure surfaced by the system carries enough information for the
+       proof author to act on it without reading logs."
+    - "InconsistentPremises is never silently treated as a valid proof."
+    - "Timeout is never collapsed into NoProofFound."

echidnabot/.machine_readable/6a2/STATE.a2ml

@@ -2,63 +2,37 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # STATE.a2ml — Echidnabot project state
-
 [metadata]
 project = "echidnabot"
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "0.0.1"
+last-updated = "2026-01-03"
 status = "active"
-session = "VeriSimDB coupling + dogfood run — 2026-04-11"
+session = "converted from scheme — 2026-04-11"
 
 [project-context]
 name = "Echidnabot"
-purpose = """
-Proof-aware CI bot for theorem prover repositories. Calls ECHIDNA Core
-to verify proof files, records every attempt (success + failure) to
-VeriSimDB via the VeriSimWriter adapter, and feeds the Hypatia learning
-loop through the proof_attempts ClickHouse table.
-"""
-completion-percentage = 72
+purpose = """"""
+completion-percentage = 0
 
 [position]
-phase = "implementation"   # design | implementation | testing | maintenance | archived
-maturity = "alpha"         # experimental | alpha | beta | production | lts
+phase = "initial"   # design | implementation | testing | maintenance | archived
+maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
-  { id = "M1", title = "Core prover dispatch (48 provers)", status = "done" },
-  { id = "M2", title = "VeriSimWriter — proof_attempts recording", status = "done" },
-  { id = "M3", title = "check --slug for ad-hoc dogfood runs", status = "done" },
-  { id = "M4", title = "Webhook server + scheduler", status = "done" },
-  { id = "M5", title = "Register/check/status CLI commands", status = "done" },
-  { id = "M6", title = "GitHub / GitLab / Bitbucket adapters", status = "in-progress" },
-  { id = "M7", title = "Production hardening (retry, backoff, circuit-break)", status = "planned" },
-  { id = "M8", title = "Prover availability detection (not just status)", status = "planned" },
+  # No milestones recorded
 ]
 
 [blockers-and-issues]
 issues = [
-  { id = "B1", description = "Agda/Coq/Isabelle provers report status=unavailable when not installed locally; proof attempts write failure rows correctly but classification could be improved", severity = "low" },
-  { id = "B2", description = "GitHub adapter not yet wired with real webhook signing validation", severity = "medium" },
+  # No blockers recorded
 ]
 
 [critical-next-actions]
 actions = [
-  "Wire GitHub PAT for production webhook dispatch",
-  "Add prover-not-installed vs proof-failed distinction in outcome classification",
-  "Test process_job path end-to-end with a real GitHub webhook",
+  # No actions recorded
 ]
 
-[session-history]
-# 2026-04-11: VeriSimDB coupling complete. VeriSimWriter records every verify_proof
-#             result to POST /api/v1/proof_attempts (ClickHouse via verisim-api).
-#             Fixed timestamp format to DateTime64(3) without Z suffix.
-#             Added --slug flag to check command so ad-hoc file checks also populate
-#             proof_attempts. Dogfood run: 4 echidna proof files verified, all rows
-#             landed in ClickHouse (lean=success, agda/coq=failure, correct timestamps).
-# 2026-04-05: V4 coupling: VeriSimWriter stub present but not wired into process_job.
-#             echidnabot compiles, 0 clippy warnings.
-
 [maintenance-status]
-last-run-utc = "2026-04-11T17:11:17Z"
-last-result = "pass"
+last-run-utc = "2026-01-03T00:00:00Z"
+last-result = "unknown"  # unknown | pass | warn | fail

echidnabot/ROADMAP.adoc

@@ -1,22 +1,75 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
 = Echidnabot Roadmap
 
-== Current Status
+== Current Status (v0.1.x)
 
-Initial development phase.
+Core dispatch, trust pipeline integration, and GitOps proof-verification flow
+operational. Communicates with ECHIDNA over REST and GraphQL.
+
+=== Done
+* [x] `EchidnaClient` — REST + GraphQL with `Auto` fallback
+* [x] `ProofStatus` extended to full 8-variant taxonomy matching ECHIDNA's
+      `ProverOutcome` (PROVED / NO_PROOF_FOUND / INVALID_INPUT /
+      UNSUPPORTED_FEATURE / TIMEOUT / INCONSISTENT_PREMISES / PROVER_ERROR /
+      SYSTEM_ERROR)
+* [x] `parse_proof_status()` handles both new taxonomy strings and legacy strings
+* [x] REST response deserialization upgraded: reads `outcome` field when present
+      (ECHIDNA v2.2+), falls back to `valid: bool` for older servers
+* [x] `ProofStatus::is_verified()` and `is_retryable()` helpers
 
 == Milestones
 
-=== v0.1.0 - Foundation
-* [ ] Core functionality
-* [ ] Basic documentation
-* [ ] CI/CD pipeline
+=== v0.2.0 — Session-based Z3 (single-process round-trip)
+
+Replace the two-process `execute_command()` pattern in ECHIDNA Z3 backend with
+a single Z3 session using `(push)/(pop)`. This makes the inconsistency pre-check
+and validity check atomic (one process, no races) and halves subprocess overhead.
+
+Echidnabot impact: faster response times for Z3-backed proofs; TIMEOUT outcome
+more reliable (single process, single wall-clock budget).
+
+* [ ] ECHIDNA: session-based `Z3Backend::execute_session()` with push/pop
+* [ ] ECHIDNA: retire two-call pattern in `check()`
+* [ ] echidnabot: no code change needed — outcome taxonomy unchanged
+
+=== v0.3.0 — Typed override coverage for priority backends
+
+ECHIDNA's `check()` default falls back to heuristic string matching for 46 of 48
+backends. Priority overrides (each surfaces full taxonomy without guessing):
+
+* [ ] CVC5 — heavily used alongside Z3, same SMT-LIB surface
+* [ ] Lean 4 — most common interactive backend
+* [ ] Coq/Rocq — second most common; `InconsistentPremises` detection via
+      `tauto` + `exfalso`
+* [ ] Isabelle — `INCONSISTENT_PREMISES` from `simp` failure pattern
+
+Echidnabot impact: `INCONSISTENT_PREMISES` and `UNSUPPORTED_FEATURE` reported
+accurately instead of `NO_PROOF_FOUND` for these backends.
+
+=== v0.4.0 — `check_raw_smt()` API surface
+
+Add a `check_raw_smt(raw: &str) -> ProverOutcome` method to `ProverBackend` for
+backends that accept pre-built content directly (Z3, CVC5, Why3). Avoids the
+lossy `parse_string()` → ProofState → reconstruct round-trip.
+
+ECHIDNA's `/api/verify` REST handler uses this path when the content is raw
+SMT-LIB (already detected via `should_passthrough_smt_eval`), making the
+`outcome` field accurate for raw-mode requests.
+
+Echidnabot impact: `verify_proof_rest()` receives meaningful `outcome` even
+for SMT-LIB passthroughs (currently gets a synthesised PROVED/NO_PROOF_FOUND).
+
+=== v1.0.0 — Production stable
+
+* [ ] `gitbot-fleet/shared-context` submodule pinned and shipped
+* [ ] All above milestones complete
+* [ ] Comprehensive integration tests against live ECHIDNA instance
+* [ ] Deployment documentation
 
-=== v1.0.0 - Stable Release
-* [ ] Full feature set
-* [ ] Comprehensive tests
-* [ ] Production ready
+== Architectural direction
 
-== Future Directions
+The long-term direction is: **every failure surfaced by echidnabot carries enough
+information for the proof author to act on it without reading logs.**
 
-_To be determined based on community feedback._
+The taxonomy established in ECHIDNA v2.2 is the foundation. Each subsequent
+milestone makes more of that taxonomy reachable through the bot's output.

echidnabot/src/dispatcher/echidna_client.rs

@@ -319,17 +319,16 @@ impl EchidnaClient {
         }
 
         let data: RestVerifyResponse = response.json().await.map_err(Error::Http)?;
+        // Use typed outcome when ECHIDNA v2.2+ sends it; fall back to bool for
+        // older servers.
+        let status = match data.outcome.as_deref() {
+            Some(s) => parse_proof_status(s),
+            None => if data.valid { ProofStatus::Verified } else { ProofStatus::Failed },
+        };
+        let message = format!("{:?}", status);
         Ok(ProofResult {
-            status: if data.valid {
-                ProofStatus::Verified
-            } else {
-                ProofStatus::Failed
-            },
-            message: if data.valid {
-                "Proof verified successfully".to_string()
-            } else {
-                "Proof verification failed".to_string()
-            },
+            status,
+            message,
             prover_output: String::new(),
             duration_ms: 0,
             artifacts: Vec::new(),
@@ -437,6 +436,10 @@ struct RestVerifyRequest {
 #[derive(Deserialize)]
 struct RestVerifyResponse {
     valid: bool,
+    /// Typed outcome string from ProverOutcome::status_str() (added in v2.2).
+    /// Absent in older ECHIDNA versions — fall back to `valid` boolean when None.
+    #[serde(default)]
+    outcome: Option<String>,
     #[allow(dead_code)]
     goals_remaining: usize,
     #[allow(dead_code)]
@@ -560,12 +563,24 @@ pub enum ProverStatus {
     Unknown,
 }
 
+/// Map an ECHIDNA status string (from `ProverOutcome::status_str()`) to
+/// `ProofStatus`. Handles both the new 8-variant taxonomy and legacy strings
+/// for backward compatibility.
 fn parse_proof_status(s: &str) -> ProofStatus {
     match s.to_uppercase().as_str() {
+        // New taxonomy (ProverOutcome::status_str())
+        "PROVED" => ProofStatus::Proved,
+        "NO_PROOF_FOUND" => ProofStatus::NoProofFound,
+        "INVALID_INPUT" => ProofStatus::InvalidInput,
+        "UNSUPPORTED_FEATURE" => ProofStatus::UnsupportedFeature,
+        "TIMEOUT" => ProofStatus::Timeout,
+        "INCONSISTENT_PREMISES" => ProofStatus::InconsistentPremises,
+        "PROVER_ERROR" => ProofStatus::ProverError,
+        "SYSTEM_ERROR" => ProofStatus::SystemError,
+        // Legacy strings (older ECHIDNA versions / other API consumers)
         "VERIFIED" | "PASS" | "SUCCESS" => ProofStatus::Verified,
         "FAILED" | "FAIL" => ProofStatus::Failed,
-        "TIMEOUT" => ProofStatus::Timeout,
-        "ERROR" => ProofStatus::Error,
+        "ERROR" => ProofStatus::ProverError,
         _ => ProofStatus::Unknown,
     }
 }

echidnabot/src/dispatcher/mod.rs

@@ -18,17 +18,57 @@ pub struct ProofResult {
     pub artifacts: Vec<String>,
 }
 
-/// Proof verification status
+/// Proof verification status — mirrors ECHIDNA's ProverOutcome taxonomy.
+///
+/// The full 8-variant set maps directly to `ProverOutcome::status_str()` on
+/// the ECHIDNA side. `Verified`/`Failed` are backward-compatible aliases
+/// kept for callers that only care about the boolean outcome.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(rename_all = "SCREAMING_SNAKE_CASE")]
 pub enum ProofStatus {
+    /// ECHIDNA `PROVED` — goal valid, hypotheses consistent.
+    Proved,
+    /// Backward-compatible alias for `Proved` (used by GraphQL/REST responses
+    /// that still emit "VERIFIED" or "SUCCESS").
     Verified,
+    /// ECHIDNA `NO_PROOF_FOUND` — prover could not establish validity.
+    NoProofFound,
+    /// Backward-compatible alias for `NoProofFound`.
     Failed,
+    /// ECHIDNA `INVALID_INPUT` — parse or syntax error in the submitted content.
+    InvalidInput,
+    /// ECHIDNA `UNSUPPORTED_FEATURE` — syntactically valid but logic/feature
+    /// not supported by the selected prover.
+    UnsupportedFeature,
+    /// ECHIDNA `TIMEOUT` — prover hit its configured time limit.
     Timeout,
-    Error,
+    /// ECHIDNA `INCONSISTENT_PREMISES` — axiom/hypothesis set is unsatisfiable;
+    /// any goal follows trivially. Result is epistemically worthless.
+    InconsistentPremises,
+    /// ECHIDNA `PROVER_ERROR` — prover binary ran but reported an internal error.
+    ProverError,
+    /// ECHIDNA `SYSTEM_ERROR` — ECHIDNA could not communicate with the prover.
+    SystemError,
+    /// Status string was not recognised (future-proofing).
     Unknown,
 }
 
+impl ProofStatus {
+    /// Returns true if this status represents a successful, trustworthy proof.
+    ///
+    /// Specifically, `Proved` and `Verified` return true. `InconsistentPremises`
+    /// intentionally returns false even though a prover may have returned "proved" —
+    /// the result is not epistemically meaningful.
+    pub fn is_verified(self) -> bool {
+        matches!(self, ProofStatus::Proved | ProofStatus::Verified)
+    }
+
+    /// Returns true if the failure was transient and the request may be retried.
+    pub fn is_retryable(self) -> bool {
+        matches!(self, ProofStatus::Timeout | ProofStatus::SystemError)
+    }
+}
+
 /// Prover kind matching ECHIDNA's supported backends
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
 #[serde(rename_all = "lowercase")]