Repository navigation
Delete the six duplicated src/abi/*.idr modules and repoint every reference - #821
Conversation
…erence Closes #815. src/abi/hypatia-abi.ipkg sets `sourcedir = ".."`, which resolves to src/, so the modules it compiles are src/Hypatia/ABI/*.idr. A byte-identical copy of all six sat in src/abi/, compiled by nothing. Divergence between the two was undetectable -- DEBT-REGISTER C-4, now marked RESOLVED. Proven lossless before deleting: five of the six blobs were byte-identical across the two directories, and the dead Types.idr blob 40d2ed6 is a strict ancestor revision of the live 788493e (the live copy carries #120's authority-direction correction on top). Nothing is lost that is not already in the live module's history. Both .ipkg files and README.adoc stay, so src/abi/ still exists and `idris2 --build src/abi/hypatia-abi.ipkg` is unaffected -- verified: it builds all 6 modules from ../Hypatia/ABI/, which is the direct proof the deleted copies were never compiled. The one functional consumer, and the vacuous gate behind it ----------------------------------------------------------- test/zig_ffi_smoke_test.exs asserted File.exists? on five src/abi/*.idr modules, so deleting them turned `mix test` red. Its sibling test listed the directory, filtered for .idr and asserted SPDX headers -- after deletion that list is empty and Enum.each over nothing passes, so it would have gone VACUOUS rather than red. Both are fixed: @abi_dir now points at src/Hypatia/ABI, the required-module list gains RuleEngine.idr and Gen.idr (it named only 5 of 7 -- a pre-existing coverage gap), and the SPDX test gets a non-empty denominator assertion. Mutant-tested: pointing @abi_dir at an empty directory now yields 2 failures including "no .idr files found", where before it would have yielded 1. This consumer was missed by every earlier sweep because it names the directory ("../src/abi") and the basenames (~w(Types.idr ...)) as separate tokens, so grepping the joined path never matched it. Other corrections ----------------- - .hypatia-exemptions.adoc cited an inline marker `hypatia:ignore ...` that does not exist; the real directive is `hypatia: allow ...`. The prose above it claimed the scanner has no directive recognition, which is false -- scanner_suppression.ex file_allowed?/4 implements it. Repoint only, no new row, so the Exemption ratchet sees no growth (6 insertions, 6 deletions). - docs/proofs/HANDOVER-neural-convergence.adoc asserted that src/abi/*.idr "are the real files" and src/Hypatia/ABI/*.idr "are symlinks into them" -- backwards, and they were never symlinks. - .github/CODEOWNERS owned /src/abi/ but nothing owned /src/Hypatia/ABI/, so the normative ABI was unowned. Added. - stapeln.toml [layers.abi-verify] cache-key was "src/abi/*.idr", which would have matched nothing and cached forever. Deliberately untouched ---------------------- - verification/PROOF-STATUS.adoc -- issue #816 ("stale: wrong path, wrong LOC, wrong proofs") owns the path column; two PRs editing the same six rows would conflict. Commented there instead. - test/unified-api-adapter-contract_test.exs:11 -- a past-tense note explaining why the guard was repointed by #120. Still historically true. - verify-proofs.yml paths:, CODEOWNERS /src/abi/, Justfile compile-abi and abi-gen, pack.toml, src/README.adoc -- all reference the directory or the ipkgs, both of which survive. Verification ------------ - mix test: 1593 tests, 2 failures -- both pre-existing, proven by running test/research_extensions_test.exs at stock 86aa936 content (same 2). - just abi-gen: "connectors emitted: 16 / files written: 3 of 3", zero diff against the tracked generated files. - tests.yml dangerous-pattern denominator: 13 -> 7, still non-zero. - The scanner's `-- hypatia: allow code_safety/believe_me structural_drift/SD008` marker survives at line 19 of the live RuleEngine copy, matching what the exemptions ledger cites. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV
|
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 (31)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
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 |
Check results: 22 success, 4 failure, 4 skipped — none of the 4 caused by this PR
The last two did not run on Worth noting positively: 🤖 Generated with Claude Code |
|
❌ Failed to create Coding Agent finishing-touch task. Please try again. |
|
❌ Failed to create Coding Agent finishing-touch task. Please try again. |
…OC drift surface (#835) ## What this is `033193c` (#821) deleted the six duplicated `src/abi/*.idr` modules. Its title says it "repointed every reference"; it did not. Eight references to the deleted files survived on `main`. This PR closes that gap and corrects what the references were saying. **Acceptance test, measured both sides:** ``` git grep -nE 'src/abi/[A-Za-z]+\.idr' -- . ':!data/' ``` | | hits | |---|---| | `origin/main` @ `0aa8972` | **8** | | this branch | **1** | The one remaining hit is `test/unified-api-adapter-contract_test.exs:11`, which names 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 * **Every directory-level `src/abi/` reference stays.** The directory legitimately survives — it holds `hypatia-abi.ipkg`, `hypatia-abi-gen.ipkg` and a README. `verify-proofs.yml`'s `src/abi/**` paths filter is therefore still correct, and **no workflow file is modified by this PR**. * `data/verisim/**` telemetry, which records events about a *different* repo and names files that never existed in hypatia. Rewriting event records would falsify them. * The past-tense sites in `docs/DEBT-REGISTER.adoc`, `test/zig_ffi_smoke_test.exs` and `docs/proofs/HANDOVER-neural-convergence.adoc`. ## The four files **`ffi/zig/src/main.zig:4`** pointed at `src/abi/Foreign.idr` — wrong in *two* ways, since no file of that name has ever existed under either directory. Repointed to `src/Hypatia/ABI/FFI.idr`, where `FFIFunction` and `ffiReturnsApiResponse` actually live. **`verification/PROOF-STATUS.adoc`** — the six ABI rows repointed to `src/Hypatia/ABI/`. Each content claim was re-verified against the live module before being carried across, rather than relocated blind: | Row | Claim | Verdict | |---|---|---| | `Types.idr` | "Confidence refined type" | **true** — `{auto prf : So (value >= 0.0 && value <= 1.0)}` | | `Types.idr` | "Severity ordering" | **FALSE** — replaced | | `RuleEngine.idr` | all six properties | **true** — Sections 1, 2, 4, 5, 7, 8 | | `GraphQL.idr` / `GRPC.idr` / `REST.idr` / `FFI.idr` | as written | **true** | The `Types.idr` "Severity ordering" claim is 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 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: | File | documented | actual | |---|---|---| | `GRPC.idr` | ~150 | **64** | | `GraphQL.idr` | ~200 | **93** | | `REST.idr` | ~150 | **95** | | `FFI.idr` | ~100 | **66** | | `Types.idr` | 140 | **250** | | `VerisimdbConnector.idr` | ~110 | **175** | | `KinGate.tla` | ~130 | **198** | | …and 13 more | | | Nothing consumes them, so they are pure drift surface. A `NOTE` in the document records why the column is gone, so it is not helpfully restored. **`verification/README.adoc`** had two real bugs: a link to `PROOF-STATUS.md`, which does not exist, and a build line `cd src/abi && idris2 --build hypatia-verify.ipkg` that is wrong in both directory *and* mechanism. Replaced with what CI actually runs — the per-file `idris2 --check` loop at `.github/workflows/verify-proofs.yml:100-107` — plus the three real packages. **`.machine_readable/INTENT.contractile:45`** repointed. Checked first that `SD022` in `lib/rules/structural_drift.ex` tests directory *existence* only and never 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. * **AC1** asked for LOC re-derived from `wc -l`. Superseded: measuring proved every figure wrong, so the column is deleted rather than re-derived. Rationale in a comment on the issue. * **AC2** (correct paths) and **AC3** (name `connectorCount = Refl`) land here. * **AC4** demands a live CI check and **AC5** a mutant proving it red. Neither can 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: 1. hypatia's entire ExUnit suite is dead in CI — the repo's only `mix test` sits in a job whose `needs:` points at a permanently failing one, so it resolves to `skipped`. 2. `tests.yml` is `startup_failure` on `main`, and `governance / Actions lockfile verify` is red there, both since the Dependabot pin bumps in #830. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Closes #815. Follow-up to #120, as agreed: #120 repointed the Elixir drift guard onto the live module; this PR deletes the dead copies and corrects every reference.
What was duplicated
src/abi/hypatia-abi.ipkgsetssourcedir = "..", which resolves tosrc/, so the modules it compiles aresrc/Hypatia/ABI/*.idr. A byte-identical copy of all six sat insrc/abi/, compiled by nothing — divergence between them was undetectable. That is DEBT-REGISTER C-4, marked RESOLVED here.Both
.ipkgfiles andREADME.adocstay, sosrc/abi/still exists andidris2 --build src/abi/hypatia-abi.ipkgis unaffected. Verified directly — it builds all 6 modules from../Hypatia/ABI/, which is the proof the deleted copies were never compiled:Proven lossless before deleting
Five of the six blobs were byte-identical across the two directories.
Types.idrdiffered, so I checked rather than assumed: the dead blob40d2ed6cis a strict ancestor revision of the live788493e6— the live copy carries #120's authority-direction correction on top. Nothing is lost that the live module's own history does not already contain.The one functional consumer — and the vacuous gate behind it
test/zig_ffi_smoke_test.exsassertedFile.exists?on fivesrc/abi/*.idrmodules, so deleting them turnedmix testred.Its sibling test was worse. It listed the directory, filtered for
.idr, and asserted SPDX headers — after deletion that list is empty, soEnum.eachover nothing passes. It would have gone vacuous, not red: a deletion silently disarming a gate while the gate next to it screamed.Both are fixed.
@abi_dirnow points atsrc/Hypatia/ABI; the required-module list gainsRuleEngine.idrandGen.idr(it named only 5 of 7 — a pre-existing coverage gap); and the SPDX test gets a non-empty denominator assertion.Mutant-tested. Pointing
@abi_dirat an empty directory now gives 2 failures includingno .idr files found in …, where before it would have given 1:Worth flagging for future sweeps: this consumer was missed by three earlier searches because it holds the directory (
"../src/abi") and the basenames (~w(Types.idr …)) as separate tokens, so grepping the joined path never matches it — and because I had been searching for code that reads those files rather than code that asserts they exist.Other corrections found on the way
.hypatia-exemptions.adoccited an inline marker-- hypatia:ignore …that does not exist (git grep hypatia:ignore→ nothing). The real directive is-- hypatia: allow …. The prose above it claimed the scanner has no directive recognition — also false;scanner_suppression.exfile_allowed?/4implements it. Repoint only, no new row: 6 insertions, 6 deletions, so the Exemption ratchet sees no growth.docs/proofs/HANDOVER-neural-convergence.adocasserted thatsrc/abi/*.idr"are the real files" andsrc/Hypatia/ABI/*.idr"are symlinks into them" — backwards, and they were never symlinks..github/CODEOWNERSowned/src/abi/but nothing owned/src/Hypatia/ABI/, leaving the normative ABI unowned. Added.stapeln.toml[layers.abi-verify]hadcache-key = "src/abi/*.idr", which after deletion would match nothing and cache forever.Deliberately untouched
verification/PROOF-STATUS.adoc— verification/PROOF-STATUS.adoc is stale: wrong path, wrong LOC, wrong proofs #816 ("stale: wrong path, wrong LOC, wrong proofs") owns the path column; two PRs editing the same six rows would collide. Commented on verification/PROOF-STATUS.adoc is stale: wrong path, wrong LOC, wrong proofs #816 instead.test/unified-api-adapter-contract_test.exs:11— a past-tense note explaining why chore(deps): bump thiserror from 1.0.69 to 2.0.18 #120 repointed the guard. Still historically true.verify-proofs.ymlpaths:, CODEOWNERS/src/abi/,Justfilecompile-abi/abi-gen,pack.toml,src/README.adoc— all reference the directory or the ipkgs, both of which survive.Verification
mix test→ 1593 tests, 2 failures. Both pre-existing: proven by runningtest/research_extensions_test.exsat stock86aa936content, which gives the same 2. They are harden-runner rule tests, unrelated to ABI paths.just abi-gen→connectors emitted: 16/files written: 3 of 3, zero diff against the tracked generated files.tests.ymldangerous-pattern denominator: 13 → 7, still non-zero.-- hypatia: allow code_safety/believe_me structural_drift/SD008marker survives at line 19 of the liveRuleEngine.idr, matching what the exemptions ledger cites.🤖 Generated with Claude Code
https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV