From bfb6b808891296f3c89fb97f81735ad5f142b1f1 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 19:02:23 +0100 Subject: [PATCH] docs: correct 8 prose sites claiming src/abi/ holds the Idris2 modules PR #835 fixed every reference naming a specific `src/abi/*.idr` FILE, but a `.idr`-filename regex cannot see the other half of the same defect: prose that names the DIRECTORY and asserts it contains the Idris2 ABI. Those claims are equally false and were left standing. `src/abi/` holds exactly three files -- `README.adoc`, `hypatia-abi.ipkg` and `hypatia-abi-gen.ipkg`. The modules live in `src/Hypatia/ABI/`; the ipkg sets `sourcedir = ".."`, which is why the build line still names `src/abi/`. Corrected (8 sites, all verified in context before editing): docs/EXPLAINME.adoc:76,119 docs/operations/prover-wars-integration.adoc:39 docs/proofs/gap-analysis.adoc:79 docs/quickstart/llm-warmup-dev.adoc:117 docs/quickstart/llm-warmup-user.adoc:47 docs/quickstart/user.adoc:43 docs/wiki-pages/Architecture.md:102 Two stated module counts were also wrong and are fixed with them: the dev warmup said "5 modules" and EXPLAINME/Architecture listed five, against seven live modules (RuleEngine.idr and Gen.idr were both missing). Also corrects an overclaim this PR's predecessor introduced. The NOTE in `verification/PROOF-STATUS.adoc` said "every one of the twenty" LOC figures had gone wrong. Sixteen were wrong; four tilde-approximations (PageRankInvariants 120/~120, ESNSpectralScaling 144/~145, BayesianUpdate 188/~190, ParserTotality 191/~190) landed within two lines. A false count inside a note about false counts is not acceptable, whichever direction it errs in. Deliberately NOT changed, each verified correct as written: - `verify-proofs.yml` paths filters, Justfile, stapeln.toml, the ipkg build lines -- `src/abi/` is genuinely where the packages live - DEBT-REGISTER.adoc, HANDOVER-neural-convergence.adoc and unified-api-adapter-contract_test.exs -- past-tense records of the deleted duplicates, correct precisely because they name the old path - lib/rules/structural_drift.ex:1130 -- quotes gitbot-fleet's INTENT file as measured evidence for an SD022 defect, not a claim about this repo - .claude/CLAUDE.md's "the two .ipkg files" -- accurate; there are two in `src/abi/`, the third Idris2 package is `verify/hypatia-verify.ipkg` Acceptance: `git grep -n 'src/abi/' -- . ':!data/' | grep -iE 'idris|proof|\.idr|module'` returns 20 hits, every one an ipkg reference, past-tense history, or the `src/abi/README.adoc` title. No false claim survives. All edited AsciiDoc re-rendered clean with `asciidoctor --failure-level=WARN`. Refs #816 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- docs/EXPLAINME.adoc | 4 ++-- docs/operations/prover-wars-integration.adoc | 2 +- docs/proofs/gap-analysis.adoc | 2 +- docs/quickstart/llm-warmup-dev.adoc | 11 ++++++++--- docs/quickstart/llm-warmup-user.adoc | 2 +- docs/quickstart/user.adoc | 2 +- docs/wiki-pages/Architecture.md | 2 +- verification/PROOF-STATUS.adoc | 6 ++++-- 8 files changed, 19 insertions(+), 12 deletions(-) diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 43e63e5a..45cdcaec 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -73,7 +73,7 @@ This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), a | Technology | Role in Hypatia | Also Used In | *Idris2 ABI* (hyperpolymath standard) -| `src/abi/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr` +| `src/Hypatia/ABI/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr` | gossamer (`gossamer/src/interface/abi/`), burble (`burble/src/Burble/ABI/`), verisimdb, proven, typed-wasm — every repo with an FFI layer | *Zig FFI* (hyperpolymath standard) @@ -116,7 +116,7 @@ This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), a | `lib/self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery | `lib/neural/` | 5 networks (graph-of-trust, moe, lsm, esn, rbf) + coordinator | `lib/vcl/` | VCL client, file executor, query functions -| `src/abi/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI) +| `src/Hypatia/ABI/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI, RuleEngine, Gen) | `ffi/zig/src/` | 7 C-compatible exported functions | `adapters/ cli/ data/ fixer/ integration/` | Rust workspace (root crates) | `proofs/agda/` | Formal verification of safety triangle correctness diff --git a/docs/operations/prover-wars-integration.adoc b/docs/operations/prover-wars-integration.adoc index 82dfc9cd..5e9bcb3c 100644 --- a/docs/operations/prover-wars-integration.adoc +++ b/docs/operations/prover-wars-integration.adoc @@ -36,7 +36,7 @@ the head-to-head statistics from each prover's results corpus. `data/prover-wars/{challenge,result,winner}/*.jsonl` (proposed layout — needs confirmation with the VeriSimDB owner). - * *ABI* — Idris2 ABI definitions in `src/abi/` already export + * *ABI* — Idris2 ABI definitions in `src/Hypatia/ABI/` already export `ProofObligation` types. Prover Wars integration adds `ProofChallenge` + `ProofResult` to the ABI so cross-language consumers see consistent shapes. diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index eab72e3e..dddf4b28 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -76,7 +76,7 @@ CI invocation does not. This is the one proof currently gated on every push to main and on a weekly Monday 04:00 UTC schedule. Pattern to replicate. -==== Idris 2 type library (not proofs) — `+src/abi/+`, `+verify/src/+` +==== Idris 2 type library (not proofs) — `+src/Hypatia/ABI/+`, `+verify/src/+` `+Types.idr+`, `+RuleEngine.idr+`, `+PipelineState.idr+` — dependent-type library code used by the ABI. Type-checked locally; not diff --git a/docs/quickstart/llm-warmup-dev.adoc b/docs/quickstart/llm-warmup-dev.adoc index 49adccac..4af9f66d 100644 --- a/docs/quickstart/llm-warmup-dev.adoc +++ b/docs/quickstart/llm-warmup-dev.adoc @@ -114,9 +114,10 @@ revert |`+tools/cii-registrar+` |CII Best Practices registration |=== -==== Idris2 ABI (src/abi/) +==== Idris2 ABI (src/Hypatia/ABI/) -5 modules with dependent type proofs: +7 modules with dependent type proofs. The `+.ipkg+` files that build them +live in `+src/abi/+` and set `+sourcedir = ".."+`: [width="100%",cols="40%,60%",options="header",] |=== @@ -132,7 +133,11 @@ health) |`+FFI.idr+` |GADT constructors for C ABI functions -|`+hypatia-abi.ipkg+` |Package definition +|`+RuleEngine.idr+` |Rule-evaluation types, safety triangle, dispatch proofs + +|`+Gen.idr+` |Wire-enum generator for the Zig and Rust connector enums + +|`+src/abi/hypatia-abi.ipkg+` |Package definition |=== ==== Zig FFI (ffi/zig/) diff --git a/docs/quickstart/llm-warmup-user.adoc b/docs/quickstart/llm-warmup-user.adoc index f4fa2c03..677e255f 100644 --- a/docs/quickstart/llm-warmup-user.adoc +++ b/docs/quickstart/llm-warmup-user.adoc @@ -44,7 +44,7 @@ OutcomeTracker (Bayesian feedback loop) |`+lib/safety/+` |Rate limiter, quarantine, batch rollback |`+adapters/+` |Rust adapter crate |`+cli/+` |Rust CLI crate -|`+src/abi/+` |Idris2 ABI definitions +|`+src/Hypatia/ABI/+` |Idris2 ABI definitions (built by `+src/abi/*.ipkg+`) |`+ffi/zig/+` |Zig FFI bridge (7 functions) |`+mix.exs+` |Elixir project config |`+Cargo.toml+` |Rust workspace config diff --git a/docs/quickstart/user.adoc b/docs/quickstart/user.adoc index 1035eeb4..4d228d03 100644 --- a/docs/quickstart/user.adoc +++ b/docs/quickstart/user.adoc @@ -40,7 +40,7 @@ toc::[] Optional (for ABI/FFI layers): -* Idris2 >= 0.7.0 (for ABI definitions in `src/abi/`) +* Idris2 >= 0.7.0 (for the ABI definitions in `src/Hypatia/ABI/`) * Zig >= 0.13.0 (for FFI bridge in `ffi/zig/`) == Clone and build diff --git a/docs/wiki-pages/Architecture.md b/docs/wiki-pages/Architecture.md index f9db4efb..3ca7424b 100644 --- a/docs/wiki-pages/Architecture.md +++ b/docs/wiki-pages/Architecture.md @@ -99,7 +99,7 @@ All `/api/*` endpoints are loopback-only by default; set `HYPATIA_API_BEARER_TOK Foreign callers reach Hypatia through: -- **Idris2 ABI** (`src/abi/`) — `Types.idr`, `GraphQL.idr`, `GRPC.idr`, `REST.idr`, `FFI.idr` (with dependent-type proofs) +- **Idris2 ABI** (`src/Hypatia/ABI/`) — `Types.idr`, `GraphQL.idr`, `GRPC.idr`, `REST.idr`, `FFI.idr`, `RuleEngine.idr` (with dependent-type proofs) - **Zig FFI** (`ffi/zig/`) — 7 exported C functions (`hypatia_health_check`, `hypatia_scan_repo`, `hypatia_dispatch`, `hypatia_record_outcome`, `hypatia_force_learning_cycle`, `hypatia_get_confidence`, `hypatia_dispatch_strategy`) ## Component table diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 3604b0d5..e99e2e47 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -18,8 +18,10 @@ convenient ==== Existing Proofs (pre-2026-04-04) NOTE: These tables deliberately carry no line-count column. Hand-maintained LOC -figures drift silently, nothing consumes them, and every one of the twenty -previously recorded here had gone wrong. Use `+wc -l+` on the paths below. +figures drift silently, nothing consumes them, and sixteen of the twenty +previously recorded here were wrong — some by more than double. Use `+wc -l+` +on the paths below. (The four that were right were all tilde-approximations +that happened to land within two lines; the column was still not worth keeping.) [width="100%",cols="28%,14%,42%,16%",options="header",] |===