Delete the six duplicated src/abi/*.idr modules and repoint every reference

.claude/CLAUDE.md

@@ -174,9 +174,9 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `RuleEngine.idr` | Rule-evaluation types |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
-The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles**. A byte-identical
-copy of all six modules also sits in `src/abi/*.idr` and is built by nothing — divergence between
-them is undetectable. See DEBT-REGISTER C-4.
+The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the
+normative ABI. `src/abi/` holds only the two `.ipkg` files and a README; the byte-identical
+duplicate modules that used to sit there were deleted 2026-09-22 (issue #815, DEBT-REGISTER C-4).
 
 ### Zig FFI (ffi/zig/src/)
 

.github/CODEOWNERS

@@ -18,6 +18,7 @@
 
 # ABI/FFI layer
 /src/abi/ @hyperpolymath
+/src/Hypatia/ABI/ @hyperpolymath
 /ffi/zig/ @hyperpolymath
 
 # Neural / scanning engine

.github/workflows/tests.yml

@@ -1,3 +1,3 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
@@ -146,7 +146,7 @@
           # strings, not as actual escape hatches).
           # `grep -v '^\s*--'` strips Idris2 / Haskell line comments, which
           # legitimately mention these tokens as documentation
-          # ("Zero believe_me." in src/abi/RuleEngine.idr is the canonical
+          # ("Zero believe_me." in src/Hypatia/ABI/RuleEngine.idr is the canonical
           # example).
           DANGEROUS=$(find lib src \( -name '*.idr' -o -name '*.v' -o -name '*.lean' -o -name '*.hs' \) \
             -not -path 'lib/rules/*' \

.hypatia-exemptions.adoc

@@ -10,19 +10,19 @@ matching its tuple) — the difference: the baseline is a quantitative
 snapshot (regenerable from any scan), this table is the qualitative
 justification (curated by humans).
 
-When the scanner gains support for inline `+hypatia:ignore+` directives
-(see `+lib/rules/+` — currently regex-pattern-based, no directive
-recognition yet), the rows below should map 1:1 to the inline comments
-already placed at each file’s site.
+The scanner recognises inline `+hypatia: allow <module>/<type>+` directives
+(see `+lib/hypatia/scanner_suppression.ex+`, `+file_allowed?/4+`, which scans a
+file's first `+:max_header_lines+` lines). The rows below map 1:1 to the
+inline comments already placed at each file's site.
 
 === Currently accepted findings
 
 [width="100%",cols="20%,20%,20%,20%,20%",options="header",]
 |===
 |File |Rule |Inline marker |Rationale |Revisit when
-|`+src/abi/RuleEngine.idr+` |`+code_safety/believe_me+`,
+|`+src/Hypatia/ABI/RuleEngine.idr+` |`+code_safety/believe_me+`,
 `+structural_drift/SD008+`
-|`+-- hypatia:ignore code_safety/believe_me structural_drift/SD008+`
+|`+-- hypatia: allow code_safety/believe_me structural_drift/SD008+`
 (line 19) |The scanner is counting the literal token `+believe_me+`
 inside an Idris2 comment that asserts there are _no_ such primitives.
 There is no actual `+believe_me+` call site in the module. |The scanner

Justfile

@@ -310,7 +310,7 @@ tour:
     echo "   Rust crates for adapters, CLI tools, data processing, fixes."
     echo ""
     echo "5. ABI/FFI:"
-    echo "     src/abi/   - Idris2 types (GraphQL, gRPC, REST proofs)"
+    echo "     src/abi/   - Idris2 ABI + codegen packages (.ipkg)"
     echo "     ffi/zig/   - 7 exported C functions"
     echo ""
     echo "6. SAFETY SYSTEMS: lib/safety/"

clients/rust/hypatia-client/src/ffi.rs

@@ -22,7 +22,7 @@
 //   2. `lib.get(b"hypatia_*\0")` — symbol lookup is unsafe because the
 //      caller asserts the type signature. Each lookup matches the exact
 //      `extern "C"` signature exported by `main.zig` and pinned by the
-//      Idris2 ABI dependent-type proofs in `src/abi/Types.idr`. Renumbering
+//      Idris2 ABI dependent-type proofs in `src/Hypatia/ABI/Types.idr`. Renumbering
 //      the Connector enum or changing any exported function's signature
 //      breaks the build at the Idris2 layer first.
 //

clients/rust/hypatia-client/src/lib.rs

@@ -20,7 +20,7 @@
 // REST, FlatBuffers, Bebop, JSON-RPC, WebSocket, MQTT, tRPC,
 // Cap'n Proto, SOAP, VeriSimDB-REST, BSP, SCIP, IPFS, Arrow Flight)
 // lives on the Zig side at `hypatia/ffi/zig/src/unified-api-adapter.zig` and is
-// mirrored by the Idris2 ABI in `src/abi/Types.idr`. The Rust client
+// mirrored by the Idris2 ABI in `src/Hypatia/ABI/Types.idr`. The Rust client
 // knows about all sixteen via `Connector` so that future enumeration
 // and dispatch endpoints (`hypatia_connector_count`,
 // `hypatia_connector_name`, `hypatia_unified_api_adapter_start_all`) are

clients/rust/hypatia-client/src/types.rs

@@ -3,7 +3,7 @@
 //
 // Hypatia client types — the typed surface that replaces the
 // V-lang client at the deleted `api/v/hypatia.v`. Mirrors the
-// Idris2 ABI types in `src/abi/Types.idr` and the Zig ABI types
+// Idris2 ABI types in `src/Hypatia/ABI/Types.idr` and the Zig ABI types
 // in `ffi/zig/src/main.zig`.
 
 use serde::{Deserialize, Serialize};

docs/DEBT-REGISTER.adoc

@@ -274,12 +274,15 @@ CI-1). So no human or machine has seen a clippy result recently.
 `+cargo fmt --all --check+` passes and `+Cargo.lock+` is in sync. *To
 verify:* re-run with a warm `+target/+` (~15-20 min).
 
-==== C-4 · MEDIUM · Idris ABI sources duplicated byte-for-byte · UNTRACKED
+==== C-4 · MEDIUM · Idris ABI sources duplicated byte-for-byte · RESOLVED
 
-`+src/Hypatia/ABI/*.idr+` and `+src/abi/*.idr+` — all 6 pairs identical.
+`+src/Hypatia/ABI/*.idr+` and `+src/abi/*.idr+` were all 6 pairs identical.
 `+src/abi/hypatia-abi.ipkg+` sets `+sourcedir = ".."+`, so
-*`+src/Hypatia/ABI/+` is what compiles* and `+src/abi/*.idr+` is a dead
-copy nothing builds. Divergence between them is undetectable today.
+*`+src/Hypatia/ABI/+` is what compiles* and `+src/abi/*.idr+` was a dead
+copy nothing built, whose divergence would have been undetectable.
+*Resolved 2026-09-22 (issue #815):* the six dead modules are deleted; only
+`+hypatia-abi.ipkg+`, `+hypatia-abi-gen.ipkg+` and `+README.adoc+` remain in
+`+src/abi/+`.
 
 ==== C-5 · LOW · One orphaned module · UNTRACKED
 

docs/governance/CRG-AUDIT-2026-04-18.adoc

@@ -133,7 +133,7 @@ hits, contractile trident complete, full mirror fan-out configured.
 |===
 | Item | Count | Notes
 
-| Idris2 ABI modules (`src/abi/*.idr`)
+| Idris2 ABI modules (`src/Hypatia/ABI/*.idr`)
 | 6 files, 1,128 LOC
 | `Types.idr` 240, `REST.idr` 95, `GraphQL.idr` 93, `FFI.idr` 66, `GRPC.idr` 64, `RuleEngine.idr` 570. All declare `%default total` at file head.
 

docs/operations/prover-wars-integration.adoc

@@ -91,7 +91,7 @@ Estimated 400–600 LOC including tests.
 
 === ABI additions
 
-In `src/abi/Types.idr`:
+In `src/Hypatia/ABI/Types.idr`:
 
 [source,idris]
 ----
@@ -113,8 +113,8 @@ record ProofResult where
   timestamp : String
 ----
 
-Add equivalent gRPC + REST endpoint definitions in `src/abi/GRPC.idr`
-and `src/abi/REST.idr`.
+Add equivalent gRPC + REST endpoint definitions in `src/Hypatia/ABI/GRPC.idr`
+and `src/Hypatia/ABI/REST.idr`.
 
 === Telemetry
 

docs/proofs/HANDOVER-neural-convergence.adoc

@@ -57,7 +57,7 @@ assertion; Agda retired) |✅
 
 |parser totality |`+verification/proofs/lean4/ParserTotality.lean+` |✅
 
-|ABI package + verify package |`+src/abi/*.idr+`
+|ABI package + verify package |`+src/Hypatia/ABI/*.idr+`
 (incl. `+RuleEngine.idr+`), `+verify/src/*.idr+` |✅
 
 |*Neural convergence — PageRank*
@@ -185,8 +185,10 @@ cd verification/proofs/tlaplus && java -cp /path/tla2tools.jar tlc2.TLC -config
 instance to lean on).
 * Idris reserved words used as identifiers were the bug class: `+data+`,
 `+record+`, `+partial+`.
-* `+src/abi/*.idr+` are the real files; `+src/Hypatia/ABI/*.idr+` are
-*symlinks* into them (build namespace `+Hypatia.ABI.*+`).
+* `+src/Hypatia/ABI/*.idr+` are the real files (build namespace
+`+Hypatia.ABI.*+`, reached via `+sourcedir = ".."+` in the ipkg). They were
+never symlinks: `+src/abi/*.idr+` held byte-identical duplicate files that
+nothing compiled, deleted 2026-09-22 (issue #815).
 
 === Definition of done
 
@@ -203,5 +205,5 @@ instance to lean on).
 Repo-hygiene PR (173 medium scan findings: `+timeout-minutes+` on
 `+ci.yml+`/`+clusterfuzzlite.yml+`, the `+setup-java+` SHA-pin
 false-positive); `+PipelineState+`→real `+proven+` integration;
-documenting the `+src/abi+` symlink layout; the `+gitbot-fleet+` /
+documenting the `+src/Hypatia/ABI+` layout; the `+gitbot-fleet+` /
 `+.git-private-farm+` repos.

docs/proofs/needs.adoc

@@ -2,7 +2,7 @@
 
 === Current State (Updated 2026-06-05)
 
-* **src/abi/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`,
+* **src/Hypatia/ABI/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`,
 `+GRPC.idr+`, `+REST.idr+`, `+RuleEngine.idr+` — built as the
 `+hypatia-abi+` package under `+--total+`.
 * **verify/src/*.idr**: `+PipelineState.idr+`, `+Verify/Fuel.idr+` —

ffi/README.adoc

@@ -5,7 +5,7 @@ C-compatible FFI bridge between the Idris2 ABI and consuming runtimes.
 
 == zig/
 
-Zig implementation of the 7 documented C ABI functions declared in `src/abi/FFI.idr`.
+Zig implementation of the 7 documented C ABI functions declared in `src/Hypatia/ABI/FFI.idr`.
 Produces a shared library (`libhypatia_ffi.so`) loadable as an Erlang NIF or via `dlopen`.
 
 See link:zig/README.adoc[zig/README.adoc] for build instructions and function reference.

ffi/zig/README.adoc

@@ -74,7 +74,7 @@ renumbered. Port layout is `base + id + 1` (`UnifiedApiAdapter.portFor`).
 The connector set is mirrored in three places that *must agree*:
 
 * Zig — `ffi/zig/src/unified-api-adapter.zig` (`Connector` enum + `comptime` count assertion)
-* Idris2 — `src/abi/Types.idr` (`Connector` + the `connectorCount = Refl` proof)
+* Idris2 — `src/Hypatia/ABI/Types.idr` (`Connector` + the `connectorCount = Refl` proof)
 * Rust — `clients/rust/hypatia-client/src/connector.rs` (`#[repr(u8)]` enum)
 
 `ffi/connectors.json` is the *golden source-of-truth*, and

ffi/zig/src/main.zig

@@ -28,7 +28,7 @@ fn clearError() void {
 }
 
 //==============================================================================
-// Core Types (must match src/abi/Types.idr)
+// Core Types (must match src/Hypatia/ABI/Types.idr)
 //==============================================================================
 
 /// Result codes (must match Idris2 Result type)

lib/hypatia/scanner_suppression.ex

@@ -321,7 +321,7 @@ defmodule Hypatia.ScannerSuppression do
   File-level allow directive: any of the first `:max_header_lines` (default
   20) of the file may include a `hypatia: allow <module>/<type>` directive
   that suppresses *every* matching finding in the file. Used for files like
-  `src/abi/RuleEngine.idr` which contain intentional `believe_me` usage and
+  `src/Hypatia/ABI/RuleEngine.idr` which contain intentional `believe_me` usage and
   want to declare the allowance once at the top.
   """
   def file_allowed?(content, rule_module, rule_type, opts \\ []) do

schema/README.adoc

@@ -9,4 +9,4 @@ Nickel configuration schemas for Hypatia data structures.
 * `generate-findings.ncl` — Generator helpers for findings in tests and tooling
 
 These schemas are used for configuration validation and test fixture generation.
-The authoritative type definitions are in `src/abi/Types.idr`.
+The authoritative type definitions are in `src/Hypatia/ABI/Types.idr`.