docs: repoint the 8 surviving src/abi/*.idr references and drop the LOC drift surface

.machine_readable/INTENT.contractile

@@ -42,7 +42,7 @@
   ; === Sensitive Areas (if in doubt, ask) ===
   (ask-before-touching
     "lib/ — Elixir pipeline modules; incorrect routing can cause fleet misdispatch"
-    "src/abi/ — Idris2 formal proofs; changes require re-verification"
+    "src/Hypatia/ABI/ — Idris2 formal proofs; changes require re-verification"
     "ffi/zig/ — C ABI boundary; changes affect all language consumers"
     "config/ — dispatch thresholds and neural network parameters"
     ".machine_readable/ — checkpoint files, format is specified"

ffi/zig/src/main.zig

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 // HYPATIA FFI Implementation
 //
-// This module implements the C-compatible FFI declared in src/abi/Foreign.idr
+// This module implements the C-compatible FFI declared in src/Hypatia/ABI/FFI.idr
 // All types and layouts must match the Idris2 ABI definitions.
 //
 // SPDX-License-Identifier: MPL-2.0

verification/PROOF-STATUS.adoc

@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
 == Proof Status — Hypatia
 
 Tracking status of formal verification proofs for the Hypatia
@@ -16,92 +17,96 @@ convenient
 
 ==== Existing Proofs (pre-2026-04-04)
 
-[width="100%",cols="15%,20%,10%,39%,16%",options="header",]
+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.
+
+[width="100%",cols="28%,14%,42%,16%",options="header",]
 |===
-|File |Language |LOC |Properties Proven |Status
-|`+src/abi/Types.idr+` |Idris2 |140 |Confidence refined type, Severity
-ordering, core data types |COMPLETE
+|File |Language |Properties Proven |Status
+|`+src/Hypatia/ABI/Types.idr+` |Idris2 |Confidence refined type
+(`+So (value >= 0.0 && value <= 1.0)+` auto-proof), core data types,
+and the wire-contract pin `+connectorCount : length allConnectors = 16+`
+|COMPLETE
 
-|`+src/abi/RuleEngine.idr+` |Idris2 |571 |Safety triangle ordering,
+|`+src/Hypatia/ABI/RuleEngine.idr+` |Idris2 |Safety triangle ordering,
 route totality, dispatch correctness, Bayesian monotonicity, annealing
 caps, end-to-end composition |COMPLETE
 
-|`+src/abi/GraphQL.idr+` |Idris2 |~200 |Query/Mutation/Subscription type
-safety |COMPLETE
+|`+src/Hypatia/ABI/GraphQL.idr+` |Idris2 |Query/Mutation/Subscription
+type safety |COMPLETE
 
-|`+src/abi/GRPC.idr+` |Idris2 |~150 |gRPC service type definitions
+|`+src/Hypatia/ABI/GRPC.idr+` |Idris2 |gRPC service type definitions
 |COMPLETE
 
-|`+src/abi/REST.idr+` |Idris2 |~150 |REST endpoint type definitions
+|`+src/Hypatia/ABI/REST.idr+` |Idris2 |REST endpoint type definitions
 |COMPLETE
 
-|`+src/abi/FFI.idr+` |Idris2 |~100 |GADT constructors,
-ffiReturnsApiResponse proof |COMPLETE
+|`+src/Hypatia/ABI/FFI.idr+` |Idris2 |GADT constructors,
+`+ffiReturnsApiResponse+` proof |COMPLETE
 
-|`+verify/src/PipelineState.idr+` |Idris2 |175 |Pipeline state machine
+|`+verify/src/PipelineState.idr+` |Idris2 |Pipeline state machine
 (ValidTransition GADT), terminal/active classification |COMPLETE
 |===
 
-*Existing total: ~1,486 LOC of proven code*
-
 ==== New Proofs (2026-04-04)
 
-[width="100%",cols="15%,20%,10%,39%,16%",options="header",]
+[width="100%",cols="28%,14%,42%,16%",options="header",]
 |===
-|File |Language |LOC |Properties Proven |Status
-|`+verification/proofs/idris2/ConfidenceBounds.idr+` |Idris2 |~220
+|File |Language |Properties Proven |Status
+|`+verification/proofs/idris2/ConfidenceBounds.idr+` |Idris2
 |[0,1] bounds preserved by construction, Bayesian update,
 success/failure monotonicity, clamping, weighted average |COMPLETE
 
-|`+verification/proofs/idris2/SafetyTriangle.idr+` |Idris2 |~195 |Strict
+|`+verification/proofs/idris2/SafetyTriangle.idr+` |Idris2 |Strict
 total order (irreflexive, asymmetric, transitive), trichotomy, routing
 respects hierarchy, optimality (highest available), completeness (all
 tiers reachable) |COMPLETE
 
-|`+verification/proofs/idris2/DispatchStrategy.idr+` |Idris2 |~230
+|`+verification/proofs/idris2/DispatchStrategy.idr+` |Idris2
 |Confidence-to-strategy monotonicity, boundary proofs (high/mid/low),
 annealing clamp bounds, nascent-never-auto, veteran-unrestricted
 |COMPLETE
 
-|`+verification/proofs/idris2/VerisimdbConnector.idr+` |Idris2 |~110
+|`+verification/proofs/idris2/VerisimdbConnector.idr+` |Idris2
 |Completeness (mandatory fields), Soundness (no "`unknown`" fallbacks),
 Preservation (transit to Logtalk facts) |COMPLETE
 
-|`+verification/proofs/idris2/Quarantine.idr+` |Idris2 |~95 |State
+|`+verification/proofs/idris2/Quarantine.idr+` |Idris2 |State
 transitions (ok/soft/hard/permanent), Auto-quarantine triggers, Release
 restoration, Routing blockage |COMPLETE
 
-|`+verification/proofs/idris2/BatchRollback.idr+` |Idris2 |~85
+|`+verification/proofs/idris2/BatchRollback.idr+` |Idris2
 |Transactionality (all-or-nothing), Reversibility (snapshot
 restoration), Fault tolerance (failure handling) |COMPLETE
 
-|`+verification/proofs/lean4/RateLimiting.lean+` |Lean 4 |~175 |Counter
+|`+verification/proofs/lean4/RateLimiting.lean+` |Lean 4 |Counter
 never exceeds configured bound, tryAccept preserves invariant, prune
 preserves invariant, inductive sequence processing, rejection guarantee,
 concrete configs (per-bot/global/burst) |COMPLETE
 
-|`+verification/proofs/lean4/BayesianUpdate.lean+` |Lean 4 |~190 |H7:
+|`+verification/proofs/lean4/BayesianUpdate.lean+` |Lean 4 |H7:
 posterior in (0,1), monotone in successes/failures, zero-observation
 identity, floor/cap clamp |COMPLETE
 
-|`+verification/proofs/lean4/ParserTotality.lean+` |Lean 4 |~190 |VCL
+|`+verification/proofs/lean4/ParserTotality.lean+` |Lean 4 |VCL
 `+FROM+`-clause parser totality, determinism, round-trip,
 malformed-input rejection |COMPLETE
 
-|`+verification/proofs/lean4/PageRankInvariants.lean+` |Lean 4 |~120
+|`+verification/proofs/lean4/PageRankInvariants.lean+` |Lean 4
 |PageRank preconditions (edge-weight / out-degree non-negativity).
 *Convergence theorem in progress (Mathlib).* |PARTIAL
 
-|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |Lean 4 |~145
+|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |Lean 4
 |ESN scaling preconditions (floor-clamped denominator positive).
 *Echo-state stability in progress (Mathlib).* |PARTIAL
 
-|`+verification/proofs/idris2/NeuralConsensus.idr+` |Idris2 |~170 |H9:
+|`+verification/proofs/idris2/NeuralConsensus.idr+` |Idris2 |H9:
 uniform-mean aggregation of Vect n Prediction is in [0,1], bounded below
 by n * min(inputs), denominator > 0 for non-empty ensembles, 8-network
 specialization |COMPLETE
 
-|`+verification/proofs/tlaplus/KinGate.tla+` |TLA+ |~130 |H8: Kin gate
+|`+verification/proofs/tlaplus/KinGate.tla+` |TLA+ |H8: Kin gate
 atomicity. Acquire/Release/Expire transitions + MutualExclusionByType +
 MutualExclusionBotView + ViewCoherentWithLocks + NoOrphanView +
 GrantsAreWellBracketed + EveryRequestProcessed (liveness) |COMPLETE —
@@ -110,16 +115,13 @@ TLC model-check 2026-04-17 passed on 3 bots × 2 repos × MaxRequests=4:
 21 JRE, tla2tools 2.19)
 
 |[line-through]#`+verification/proofs/agda/OutcomeLog.agda+`#
-|[line-through]#Agda# |~[line-through]#220# |[line-through]#H6: outcome
+|[line-through]#Agda# |[line-through]#H6: outcome
 log monotonicity (strictly increasing timestamps)# |RETIRED 2026-04-22 —
 downgraded to a runtime assertion in
 `+lib/outcome_tracker.ex:assert_h6_monotone/2+`. Echidnabot audits the
 JSONL for violations. See commit history.
 |===
 
-*New total: ~1,400 LOC of proven code (all TLC-verified or
-Idris2/Lean4-typechecked)*
-
 === Properties Proven
 
 ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`)
@@ -261,26 +263,15 @@ convergence/stability in progress (Lean + Mathlib)
 
 === File Locations
 
+Formal-verification sources live under three roots. The two inventory tables
+above carry the full path of every file; this section names only the roots, so
+that adding a proof does not require editing a third hand-maintained list.
+
 ....
 hypatia/
-├── src/abi/                              # Idris2 ABI definitions + proofs (1027 LOC)
-│   ├── Types.idr
-│   ├── RuleEngine.idr
-│   ├── GraphQL.idr
-│   ├── GRPC.idr
-│   ├── REST.idr
-│   └── FFI.idr
-├── verify/src/                           # Pipeline state machine proofs
-│   └── PipelineState.idr
-└── verification/proofs/                  # Standalone property proofs (NEW)
-    ├── idris2/
-    │   ├── ConfidenceBounds.idr          # [0,1] invariant
-    │   ├── SafetyTriangle.idr            # Ordering + routing correctness
-    │   └── DispatchStrategy.idr          # Monotonicity
-    ├── lean4/
-    │   └── RateLimiting.lean             # Counter bounds
-    └── tlaplus/
-        └── KinGate.tla                   # Mutex under interleaved bot requests
+├── src/Hypatia/ABI/        # Idris2 ABI definitions + proofs (normative wire contract)
+├── verify/src/             # Pipeline state machine proofs
+└── verification/proofs/    # Standalone property proofs (idris2/, lean4/, tlaplus/)
 ....
 
 === Retired proofs

verification/README.adoc

@@ -1,20 +1,40 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = verification/ — Formal Proofs
 
-Idris2 proof verification for Hypatia's type-level guarantees.
+Idris2, Lean 4 and TLA+ proof sources for Hypatia's type-level guarantees.
 
 == Contents
 
-* `proofs/` — Idris2 proof files (`.idr`) asserting invariants from `src/abi/`
-* `PROOF-STATUS.md` — Current proof completion status
+* `proofs/idris2/` — Idris2 proof files (`.idr`) asserting invariants over the
+  normative ABI in `src/Hypatia/ABI/`
+* `proofs/lean4/`, `proofs/tlaplus/` — Lean 4 and TLA+ proofs
+* `PROOF-STATUS.adoc` — Current proof completion status
 
 == Building Proofs
 
+The `proofs/` tree is not an Idris2 package; each file is type-checked
+independently, exactly as `.github/workflows/verify-proofs.yml` does it:
+
 [source,bash]
 ----
-cd src/abi && idris2 --build hypatia-verify.ipkg
+cd verification/proofs/idris2
+for f in *.idr; do idris2 --check "$f"; done
 ----
 
+The Idris2 *packages* in the repository are built separately:
+
+[source,bash]
+----
+idris2 --build src/abi/hypatia-abi.ipkg      # the normative ABI (src/Hypatia/ABI/)
+idris2 --build verify/hypatia-verify.ipkg    # verify/src/PipelineState.idr
+idris2 --build src/abi/hypatia-abi-gen.ipkg  # the wire-enum generator (just abi-gen)
+----
+
+NOTE: `src/abi/hypatia-abi.ipkg` sets `sourcedir = ".."`, so it compiles the
+modules under `src/Hypatia/ABI/`. The `.ipkg` files live in `src/abi/`; the
+Idris2 sources they build do not.
+
 == Status
 
-See link:PROOF-STATUS.md[PROOF-STATUS.md] for current proof completion per module.
+See link:PROOF-STATUS.adoc[PROOF-STATUS.adoc] for current proof completion per
+module.