docs: repoint the 8 surviving src/abi/*.idr references and drop the LOC drift surface - #835
Merged
Merged
Conversation
…OC drift surface PR #821 deleted the six duplicated `src/abi/*.idr` modules but, despite its title, did not repoint every reference: 8 survived on main. git grep -nE 'src/abi/[A-Za-z]+\.idr' -- . ':!data/' before: 8 hits after: 1 hit The single remaining hit is `test/unified-api-adapter-contract_test.exs:11`, which names the dead path in the past tense as history. That is correct and is left alone, as are every directory-level `src/abi/` reference: the directory legitimately survives, holding `hypatia-abi.ipkg`, `hypatia-abi-gen.ipkg` and a README. `verify-proofs.yml`'s `src/abi/**` paths filter is therefore still right and no workflow is touched. Changes: * `ffi/zig/src/main.zig:4` named `src/abi/Foreign.idr` — wrong in two ways, as no file of that name ever existed under either directory. Repointed to `src/Hypatia/ABI/FFI.idr`, which is where `FFIFunction` and `ffiReturnsApiResponse` actually live. * `verification/PROOF-STATUS.adoc`: the six ABI rows repointed to `src/Hypatia/ABI/`. Every content claim was re-verified against the live modules before being carried across; five of six were accurate and are kept verbatim. One was false — `Types.idr`'s "Severity ordering", contradicted by that module's own comment at lines 157-159 ("has never existed in this module; connectorCount is the real pin"). Replaced with the claim the module does prove, `connectorCount : length allConnectors = 16`. The hand-written LOC column is deleted from both inventory tables, along with the two derived total lines and the duplicate "File Locations" file tree. All twenty LOC figures were wrong, several by more than 100% (GRPC.idr recorded ~150, actual 64), and nothing consumes them. A NOTE records why, so the column is not helpfully restored. * `verification/README.adoc`: `PROOF-STATUS.md` does not exist and the link was broken — corrected to `.adoc`. The build line `cd src/abi && idris2 --build hypatia-verify.ipkg` was wrong in both directory and mechanism; replaced with what CI actually runs, the per-file `idris2 --check` loop from `.github/workflows/verify-proofs.yml:100-107`, plus the three real packages. * `.machine_readable/INTENT.contractile:45` repointed. Checked first that SD022 tests directory existence only and never content, so this edit has no consumer and breaks no test. Advances #816 on acceptance criteria 1-3. AC1's literal "re-derive LOC from wc -l" is superseded by deleting the column; ACs 4-5 need a live CI check and a mutant and cannot be satisfied here - see the issue comment. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV
Contributor
|
Navigate logical layers of code changes, visualize relationships, and explore their blast radius. Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (4)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
This was referenced Sep 22, 2026
Closed
Closed
hyperpolymath
added a commit
that referenced
this pull request
Sep 22, 2026
#839) ## The half of the defect a filename regex cannot see PR #835 corrected every reference naming a specific `src/abi/*.idr` **file** — 8 hits, driven down to 1 (past-tense history). But a `.idr`-filename regex is blind to the other half of the same defect: **prose that names the directory and asserts it contains the Idris2 ABI**. Those claims are just as false, and #835 left all eight standing. `src/abi/` holds exactly three files: ``` src/abi/README.adoc src/abi/hypatia-abi-gen.ipkg src/abi/hypatia-abi.ipkg ``` The modules live in `src/Hypatia/ABI/`. The ipkg sets `sourcedir = ".."`, which is why build lines legitimately still name `src/abi/` — and why a naive search-and-replace across the path would have broken the build documentation. ## Corrected — 8 sites, each read in context first | File | Was | |---|---| | `docs/EXPLAINME.adoc:76` | ``src/abi/` — formal specs for GraphQL, gRPC, REST with dependent type proofs` | | `docs/EXPLAINME.adoc:119` | `` `src/abi/` \| Idris2 specs (Types, GraphQL, gRPC, REST, FFI)`` | | `docs/operations/prover-wars-integration.adoc:39` | `Idris2 ABI definitions in `src/abi/` already export` | | `docs/proofs/gap-analysis.adoc:79` | ``+src/abi/+`, `+verify/src/+`` | | `docs/quickstart/llm-warmup-dev.adoc:117` | `==== Idris2 ABI (src/abi/)` | | `docs/quickstart/llm-warmup-user.adoc:47` | `` `+src/abi/+` \| Idris2 ABI definitions`` | | `docs/quickstart/user.adoc:43` | `Idris2 >= 0.7.0 (for ABI definitions in `src/abi/`)` | | `docs/wiki-pages/Architecture.md:102` | `**Idris2 ABI** (`src/abi/`) — `Types.idr`, `GraphQL.idr`, …` | Two **stated counts** were wrong in the same sentences and are fixed with them. The dev warmup said "5 modules" and EXPLAINME/Architecture enumerated five; there are **seven** live modules — `RuleEngine.idr` and `Gen.idr` (added by #120) were missing from every list. ## Correcting an overclaim #835 introduced The `NOTE` #835 added to `verification/PROOF-STATUS.adoc` read *"every one of the twenty previously recorded here had gone wrong."* That is itself false. **Sixteen** were wrong; four tilde-approximations landed within two lines: | File | documented | actual | |---|---|---| | `PageRankInvariants` | ~120 | 120 | | `ESNSpectralScaling` | ~145 | 144 | | `BayesianUpdate` | ~190 | 188 | | `ParserTotality` | ~190 | 191 | The conclusion is unchanged — 16/20 wrong, several by more than double, and nothing consumed the column — but a false count inside a note about false counts is not acceptable in either direction. The NOTE now says sixteen and states what the other four were. ## Deliberately NOT changed — each verified correct as written - **`verify-proofs.yml` paths filters, `Justfile`, `stapeln.toml`, every `idris2 --build src/abi/*.ipkg` line** — `src/abi/` is genuinely where the packages live. - **`docs/DEBT-REGISTER.adoc`, `docs/proofs/HANDOVER-neural-convergence.adoc`, `test/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`, elsewhere. ## Acceptance ``` git grep -n 'src/abi/' -- . ':!data/' | grep -iE 'idris|proof|\.idr|module' ``` → 20 hits, every one an ipkg/build reference, past-tense history, or the `src/abi/README.adoc` title. **No false claim survives.** All seven edited AsciiDoc files re-render clean under `asciidoctor --failure-level=WARN`. Refs #816. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
033193c(#821) deleted the six duplicatedsrc/abi/*.idrmodules. Its titlesays it "repointed every reference"; it did not. Eight references to the deleted
files survived on
main. This PR closes that gap and corrects what thereferences were saying.
Acceptance test, measured both sides:
origin/main@0aa8972The one remaining hit is
test/unified-api-adapter-contract_test.exs:11, whichnames the dead path in the past tense as a comment explaining why the guard
was repointed in #120. That is history and is correct.
What is deliberately not touched
src/abi/reference stays. The directory legitimatelysurvives — it holds
hypatia-abi.ipkg,hypatia-abi-gen.ipkgand a README.verify-proofs.yml'ssrc/abi/**paths filter is therefore still correct, andno workflow file is modified by this PR.
data/verisim/**telemetry, which records events about a different repo andnames files that never existed in hypatia. Rewriting event records would falsify
them.
docs/DEBT-REGISTER.adoc,test/zig_ffi_smoke_test.exsand
docs/proofs/HANDOVER-neural-convergence.adoc.The four files
ffi/zig/src/main.zig:4pointed atsrc/abi/Foreign.idr— wrong in twoways, since no file of that name has ever existed under either directory.
Repointed to
src/Hypatia/ABI/FFI.idr, whereFFIFunctionandffiReturnsApiResponseactually live.verification/PROOF-STATUS.adoc— the six ABI rows repointed tosrc/Hypatia/ABI/. Each content claim was re-verified against the live modulebefore being carried across, rather than relocated blind:
Types.idr{auto prf : So (value >= 0.0 && value <= 1.0)}Types.idrRuleEngine.idrGraphQL.idr/GRPC.idr/REST.idr/FFI.idrThe
Types.idr"Severity ordering" claim is contradicted by that module's owncomment at lines 157-159: "has never existed in this module;
connectorCountis the real pin." Replaced with the property the module does prove,
connectorCount : length allConnectors = 16.The hand-written LOC column is deleted from both inventory tables, with the
two derived total lines and the duplicate "File Locations" file tree. Every one
of the twenty figures was wrong:
GRPC.idrGraphQL.idrREST.idrFFI.idrTypes.idrVerisimdbConnector.idrKinGate.tlaNothing consumes them, so they are pure drift surface. A
NOTEin the documentrecords why the column is gone, so it is not helpfully restored.
verification/README.adochad two real bugs: a link toPROOF-STATUS.md,which does not exist, and a build line
cd src/abi && idris2 --build hypatia-verify.ipkgthat is wrong in both directory and mechanism. Replacedwith what CI actually runs — the per-file
idris2 --checkloop at.github/workflows/verify-proofs.yml:100-107— plus the three real packages..machine_readable/INTENT.contractile:45repointed. Checked first thatSD022inlib/rules/structural_drift.extests directory existence only andnever a content claim, so this edit has no consumer and breaks no test.
On #816
This advances #816 on ACs 1-3 and does not close it.
wc -l. Superseded: measuring provedevery figure wrong, so the column is deleted rather than re-derived. Rationale
in a comment on the issue.
connectorCount = Refl) land here.be satisfied in this PR — see the issue comment for the measurement.
Related findings, filed as issues rather than folded in
Per the standing rule that a new finding is an issue, not a merge blocker:
mix testsitsin a job whose
needs:points at a permanently failing one, so it resolves toskipped.tests.ymlisstartup_failureonmain, andgovernance / Actions lockfile verifyis red there, both since the Dependabot pin bumps in chore(deps): bump the actions group across 1 directory with 4 updates #830.🤖 Generated with Claude Code
https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV