From d9194d39d176e21def20c39de1ee2c1c6f284192 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:54:38 +0000 Subject: [PATCH 1/2] docs(proofs): mark the gap analysis summary as superseded and state today's proof lanes The TL;DR and inventory still described 2026-04-22: Agda retired, only TLA+ gated, the Lean and Idris proofs ungated. Date both headings as superseded and list the three lanes verify-proofs.yml gates today (Idris2, Agda, TLC), as the Codex review on #1025 asked. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4 --- docs/proofs/gap-analysis.adoc | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index 2e65d223..5e680a91 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -6,10 +6,26 @@ returned, and every prover runs in CI. The current state is the proof ledger (`+verification/proof-ledger.jsonl+`); the convergence plan is `+docs/proofs/HANDOVER-neural-convergence.adoc+`. +The TL;DR and the inventory below describe 2026-04-22 and are superseded. +Today `+.github/workflows/verify-proofs.yml+` gates three proof lanes, each +recording a receipt that `+scripts/proof-ledger.sh derive+` checks against the +ledger: + +* *Idris2:* `+idris2 --check+` on every file in + `+verification/proofs/idris2/+`, and builds of `+src/abi/hypatia-abi.ipkg+` + and `+verify/hypatia-verify.ipkg+`. +* *Agda:* `+verification/proofs/agda/LogtalkMigration.agda+` under + `+--safe --without-K --cubical-compatible+`. +* *TLA+:* TLC on `+verification/proofs/tlaplus/KinGate.tla+`, a bounded model + check (`+tested-only+`, not a proof). + +There is no Lean proof directory any more. The Lean job left in the workflow +is the HYP-01 hole re-check control, not a proof lane. + *Date:* 2026-04-22 *Scope:* VCL query correctness + neural ensemble convergence *Status:* Inventory + prioritised plan. No code changes yet. -=== TL;DR +=== TL;DR (2026-04-22, superseded) Hypatia has 14 proof-adjacent files across three active provers (Lean 4, Idris 2, TLA+) and zero remaining Agda (retired 2026-04 via H6). Only @@ -35,7 +51,7 @@ scoped to exclude the lazy window. Everything else in this document is forward-looking. -=== Current proof inventory +=== Proof inventory (2026-04-22, superseded) ==== Lean 4 — `+verification/proofs/lean4/+` From 25709671f885d75d0b8c369f36546c089cb3ba91 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:55:27 +0000 Subject: [PATCH 2/2] docs(readme): lib/ holds 155 Elixir source files after #1036 check-readme-claims.sh fails on main: #1036 added a lib/ source file and left the README and EXPLAINME count at 154. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4 --- EXPLAINME.adoc | 2 +- README.adoc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d992dc13..5a8ec5ab 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -142,7 +142,7 @@ an action is capped at review, not report-only (line 67). [quote, README.adoc] ____ -154 Elixir source files — pipeline, rules, VCL, neural, safety, web, merge orchestration +155 Elixir source files — pipeline, rules, VCL, neural, safety, web, merge orchestration ____ How this is implemented:: diff --git a/README.adoc b/README.adoc index d952043c..db4b0eb3 100644 --- a/README.adoc +++ b/README.adoc @@ -76,7 +76,7 @@ PatternRegistry ──> TriangleRouter ──> FleetDispatcher ──> DispatchM [cols="1,3"] |=== -| `lib/` | 154 Elixir source files — pipeline, rules, VCL, neural, safety, web, merge orchestration +| `lib/` | 155 Elixir source files — pipeline, rules, VCL, neural, safety, web, merge orchestration | `lib/rules/` | 42 source files: rule modules and their helpers; see link:docs/rules/catalogue.adoc[the catalogue] | `lib/neural/` | 8 networks + blackboard, coordinator, persistence, rebalancer | `lib/vcl/` | VCL query layer over verisim-data: parser, file executor, cache, federation