docs(verisimdb): clarify ProverKind is proven-domain, not an echidna mirror

Echidna ProverKind drift audit 2026-04-17 (echidna commit 8f573f1 expanded
its own enum from 30 → ~68 variants with 28 new *TypeChecker suffixes).
VeriSimDB's `ProverKind` in `verisim-semantic/src/proven_bridge.rs` is NOT
a mirror of echidna's dispatcher backend list — it is a proven-library
certificate-domain enum with 6 variants (Z3, Lean, Coq, Agda, Idris2,
Custom(String)) recording which prover produced a given `ProvenCertificate`.

No path dep on echidna, no action required. Build + 53/53 verisim-semantic
tests pass post-audit. Added a doc comment on the enum to prevent future
confusion with echidna's upstream list, and a session-history entry in
STATE.a2ml.

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

Author: hyperpolymath

verisimdb/.machine_readable/6a2/STATE.a2ml

@@ -51,6 +51,15 @@ actions = [
 ]
 
 [session-history]
+# 2026-04-17: Echidna ProverKind drift audit (commit 8f573f1 — 28 new
+#             *TypeChecker variants). VeriSimDB's ProverKind (in
+#             rust-core/verisim-semantic/src/proven_bridge.rs) is NOT a
+#             mirror of echidna's: it's a proven-library-domain enum with
+#             6 variants (Z3, Lean, Coq, Agda, Idris2, Custom(String))
+#             documenting the prover that produced a ProvenCertificate —
+#             strictly independent of echidna's dispatcher backend list.
+#             verisim-semantic has no path dep on echidna. No action required.
+#             Build + 53/53 semantic tests pass post-audit.
 # 2026-04-11: Added three proof_attempts routes under /api/v1/:
 #               GET  ?limit=N         — list rows for Julia retraining (ClickHouse SELECT)
 #               POST                  — insert attempt row (ClickHouse INSERT JSONEachRow)

verisimdb/rust-core/verisim-semantic/src/proven_bridge.rs

@@ -39,7 +39,13 @@ use sha2::{Digest, Sha256};
 
 use super::{ProofBlob, ProofType, SemanticError};
 
-/// Supported prover backends from the proven library.
+/// Supported prover backends from the `proven` library (Idris2 ZKP system).
+///
+/// NOTE: This `ProverKind` is NOT a mirror of ECHIDNA's dispatcher backend
+/// enum. It lives in the `proven`-certificate domain and records which prover
+/// produced a given `ProvenCertificate`. Keep it decoupled from echidna —
+/// audited 2026-04-17 against echidna commit `8f573f1` (which expanded its
+/// own ProverKind from 30 → ~68 variants). This enum is deliberately minimal.
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(rename_all = "lowercase")]
 pub enum ProverKind {