docs: update CHANGELOG + STATE.a2ml for 2026-04-05 session

VCL rename + V4 certs + prover expansion + RBF recommender + idris2
fixes + /api/verify guard — all tonight's work captured for humans
(CHANGELOG) and machines (STATE.a2ml session history).

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -83,4 +83,6 @@
 
   (session-history
     ("2026-04-04: CRG C blitz - added 55 tests across E2E, contract, aspect, reflexive, property categories")
-    ("2026-04-05: added proof_attempts learning loop (table + MV + /strategy endpoint) and Zig client SDK; closes loop with echidna/hypatia"))))
+    ("2026-04-05: added proof_attempts learning loop (table + MV + /strategy endpoint) and Zig client SDK; closes loop with echidna/hypatia")
+    ("2026-04-05: V4 proof certificates - proof_attempts_cert_policy table, mv_proven_certificates + mv_sanctify_certificates + mv_cert_evidence views, GET /api/v1/proof_attempts/certificates endpoint with window-function evidence pagination; 8 PROVEN + 2 SANCTIFIED certs live against 1156 attempts")
+    ("2026-04-05: VQL->VCL + verisimdb->verisim rename - ClickHouse database renamed (1108 rows migrated via TSV), Prover Enum8 extended to 42 variants, Rust + ReScript identifiers updated, VCL-SPEC.adoc documents 8 proof kinds (was 6), github.com/hyperpolymath/verisimdb URL preserved"))))

CHANGELOG.adoc

@@ -9,8 +9,90 @@ All notable changes to VeriSimDB are documented here. This project uses https://
 
 == [Unreleased]
 
+=== Changed
+
+==== VQL → VCL + VeriSimDB → Verisim Rename (2026-04-05)
+
+*Ecosystem-wide identity migration.* The interaction language and
+engine name have been reframed:
+
+- *VQL → VCL*: VeriSim *Query* Language becomes VeriSim *Consonance* Language.
+  Verisim operations are **propositions to a consonance engine**, not
+  queries against a passive store. Operations split into propositional
+  (`DECLARE`, `ASSERT`, `RETRACT`) and epistemic (`INSPECT`, `VERIFY`).
+- *VeriSimDB → Verisim*: the engine name shortens in discussion, module
+  names, crates, and the ClickHouse database. The GitHub repository URL
+  stays `hyperpolymath/verisimdb` to avoid rename damage.
+
+Changed in this repo:
+
+- ClickHouse database: `verisimdb.*` → `verisim.*`, all 1,108 historical
+  proof_attempts rows migrated via TSV backup/restore
+- Prover enum extended to 42 variants (cadical, kissat, spass, eprover,
+  and all other echidna backends now accepted)
+- Rust workspace crates continue to use the `verisim-*` prefix (already
+  in place before this rename)
+- Prometheus metric names: `verisimdb_*` → `verisim_*`
+- Documentation prose across `docs/`, `*.adoc`, `*.md`, `CHANGELOG`
+- ReScript `.res` VCL modules: mechanical rename of bridge/parser/type-checker
+  identifiers
+- File extension: `.vql` → `.vcl`, directories `src/vql/` → `src/vcl/`,
+  `vql-bridge/` → `vcl-bridge/`, `examples/vql-queries/` → `examples/vcl-queries/`
+- Operation verbs in VCL-context files only: `SELECT` → `INSPECT`,
+  `INSERT`/`UPDATE`/`UPSERT` → `ASSERT`, `DELETE` → `RETRACT`,
+  `CREATE`/`ALTER` (DDL) → `DECLARE`, `CHECK CONSTRAINT` → `VERIFY CONSTRAINT`
+- Query-phrase prose: `query result(s)` → `inspection result(s)`,
+  `query builder` → `statement builder`, `run a query` → `perform an inspection`,
+  etc.
+
+Preserved deliberately: `github.com/hyperpolymath/verisimdb` URLs
+(GitHub repo rename pending), `connectors/test-infra/seed/*.sql` (real
+ClickHouse DDL, left as SQL), `docs/vcl-vs-sql.adoc` (SQL comparison prose),
+generic-English "query language" and "SQL query" references.
+
+The rename cascaded through 18+ dependent repos in the ecosystem
+(hypatia, gitbot-fleet, echidna, vql-ut → vcl-total, nesy-solver,
+typell, panll, gv-clade-index, typedqliser, squeakwell,
+protocol-squisher, nextgen-languages, aerie, typed-wasm,
+metadata-grammar, ambientops, verisimiser) over the same day.
+
 === Added
 
+==== V4: Proof Certificates (2026-04-05)
+
+*PROVEN* and *SANCTIFY* — two new VCL proof types that resolve against
+the learning loop's accumulated evidence:
+
+- `proof_attempts_cert_policy` (ReplacingMergeTree): singleton config
+  table holding `tau_proven`, `n_proven`, `k_sanctify`, `n_sanctify`
+  thresholds. Default seed: τ=0.80, n=20, k=2, n_s=50.
+- `mv_proven_certificates`: view computing PROVEN status per
+  (obligation_class, prover) pair by joining `mv_prover_success_by_class`
+  with current policy.
+- `mv_sanctify_certificates`: view computing SANCTIFY status per class
+  when ≥k_sanctify provers hold PROVEN status with ≥n_sanctify combined
+  attempts.
+- `mv_cert_evidence`: view exposing the backing `proof_attempts` rows
+  for each certificate, enabling falsifiability.
+- `GET /api/v1/proof_attempts/certificates`: returns current PROVEN +
+  SANCTIFY status with optional `class`/`prover` filters, policy echo,
+  and per-cert evidence cursors. N+1 query pattern collapsed into a
+  single window-function query (`row_number() OVER (PARTITION BY ...)`).
+- Validation at API boundary: `obligation_class` rejected with HTTP 400
+  if not in the 11-value allowed set (catches typos before they
+  pollute the strategy MV).
+- 5 new unit tests for the certificate surface (26 total passing).
+
+Live certificate snapshot as of 2026-04-05:
+  8 PROVEN certs (safety/{z3,cvc5,vampire,eprover}, correctness/{z3,cvc5},
+  linearity/idris2, model-check/cadical).
+  2 SANCTIFIED classes (safety: 4 provers × 282 attempts,
+  correctness: 2 provers × 198 attempts).
+
+VCL-SPEC.adoc updated with the eight proof kinds (was six). See
+`docs/design/DESIGN-2026-04-05-V4-proof-attempts-vqldt.adoc` for the
+full design rationale.
+
 ==== Proof-Attempts Learning Loop (2026-04-05)
 - **proof_attempts ClickHouse table**: Records every prover invocation across the estate (attempt_id, obligation_id, repo, file, claim, obligation_class, prover_used, outcome, duration_ms, confidence, strategy_tag, timestamps). 20-prover enum covering the echidna portfolio.
 - **mv_prover_success_by_class materialized view**: SummingMergeTree aggregation of success_count / total_attempts / total_duration_ms per (obligation_class, prover_used) — the source of truth for strategy recommendations.