Skip to content

docs(proofs): mark the gap-analysis summary superseded; fix the README lib/ count #1046

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Nov 10, 2026
Merged

docs(proofs): mark the gap-analysis summary superseded; fix the README lib/ count #1046

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d9194d3
docs(proofs): mark the gap analysis summary as superseded and state t…
claude Nov 10, 2026
2570967
docs(readme): lib/ holds 155 Elixir source files after #1036
claude Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion EXPLAINME.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

@chatgpt-codex-connector chatgpt-codex-connector Bot Nov 10, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Synchronize the duplicated architecture measurements

After updating this quote, the same Architecture section still says | lib/: 154 | 154 .ex files, 180 defmodule at line 154 and describes those values as gated. The committed tree contains 155 .ex files and 183 defmodule declarations, so EXPLAINME.adoc now contradicts both itself and the repository; update the measured row alongside the quote.

Useful? React with 👍 / 👎.

____

How this is implemented::
Expand Down
2 changes: 1 addition & 1 deletion README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 18 additions & 2 deletions docs/proofs/gap-analysis.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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/+`

Expand Down
Loading