docs(echidna-bridge): log drift from upstream echidna ProverKind expansion

ECHIDNA commit 8f573f1 (2026-04-17) expanded `ProverKind` from 30 to ~68
variants (28 new `*TypeChecker` suffixes: Ordinary, Phantom, Polymorphic,
Existential, HigherKinded, Row, Subtyping, Intersection, Union, Gradual,
Hoare, Indexed, Linear, Affine, Relevant, Ordered, Uniqueness, Immutable,
Capability, Bunched, Temporal, Provability, Impure, Coeffect, Probabilistic,
Dyadic, Homotopy, Cubical).

`protocol-squisher-echidna-bridge` carries a MIRROR enum (not a path dep),
so compilation is unaffected. Non-exhaustive matches in `goal_generator.rs`
absorb unknown variants via `_ =>` fallback, so the drift is semantic only
(new provers get the generic comment-goal instead of prover-specific syntax).

Build + 21/21 bridge unit tests pass post-audit. Extending the mirror (or
switching to a path dep) is deferred to phase 2 per WIRE-EVERYTHING caveat
on non-breaking drift.

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -25,14 +25,29 @@ milestones = [
 
 [blockers-and-issues]
 issues = [
-  # No blockers recorded
+  # Drift logged 2026-04-17: echidna ProverKind expanded in commit 8f573f1
+  # from 30 to ~68 variants (28 new *TypeChecker suffixes: Ordinary, Phantom,
+  # Polymorphic, Existential, HigherKinded, Row, Subtyping, Intersection,
+  # Union, Gradual, Hoare, Indexed, Linear, Affine, Relevant, Ordered,
+  # Uniqueness, Immutable, Capability, Bunched, Temporal, Provability,
+  # Impure, Coeffect, Probabilistic, Dyadic, Homotopy, Cubical).
+  # protocol-squisher-echidna-bridge carries a MIRROR enum at
+  # crates/protocol-squisher-echidna-bridge/src/types.rs (not a path dep),
+  # so the expansion does not break compilation. Non-exhaustive matches in
+  # goal_generator.rs absorb unknown variants via the _ => fallback arm.
+  # DECISION DEFERRED (phase 2): extend the mirror to parity with echidna.
+  # Until then, any new *TypeChecker prover goals will fall through to the
+  # generic "[Prover:?] Prove:" comment goal rather than producing
+  # prover-specific syntax.
 ]
 
 [critical-next-actions]
 actions = [
-  # No actions recorded
+  # Phase-2 decision: mirror all 68 echidna ProverKind variants (or move to
+  # path dep on echidna proper), and add prover-specific goal rendering
+  # for the 28 new *TypeChecker variants where useful.
 ]
 
 [maintenance-status]
-last-run-utc = "2026-04-04T00:00:00Z"
-last-result = "unknown"  # unknown | pass | warn | fail
+last-run-utc = "2026-04-17T00:00:00Z"
+last-result = "pass"  # 21/21 bridge tests pass post-echidna-expansion drift audit

crates/protocol-squisher-echidna-bridge/src/types.rs

@@ -7,13 +7,24 @@
 //! interface. Each proof goal targets a specific prover backend (one of 30
 //! supported engines) and tracks status through a well-defined lifecycle:
 //! `Pending → InProgress → Success | Failed | Timeout`.
+//!
+//! DRIFT NOTICE (2026-04-17): ECHIDNA commit `8f573f1` expanded its upstream
+//! `ProverKind` from 30 → ~68 variants (28 new `*TypeChecker` suffixes). This
+//! mirror intentionally remains at 30 pending a phase-2 parity decision. See
+//! `.machine_readable/6a2/STATE.a2ml` `[blockers-and-issues]` for rationale.
+//! Non-exhaustive matches (`goal_generator.rs`) absorb unknown variants via
+//! `_ =>` fallback arms, so the mirror staleness does not break compilation.
 
 use serde::{Deserialize, Serialize};
 
-/// Supported prover backends in ECHIDNA (30 engines).
+/// Supported prover backends in ECHIDNA (30 engines mirrored — see DRIFT NOTICE above).
 ///
 /// Each variant represents a distinct theorem proving or verification engine.
 /// The bridge generates prover-specific goal syntax via `ProofGoalGenerator`.
+// TODO(echidna-drift-2026-04-17): upstream ECHIDNA now exposes ~68 variants
+// (28 new `*TypeChecker` suffixes from commit 8f573f1). Decide in phase 2:
+// (a) mirror the full set, or (b) switch this crate to a path dep on echidna
+// proper and drop the mirror.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
 #[serde(rename_all = "snake_case")]
 pub enum ProverKind {