From 0eefa53e776051ac14b6d3bb9b1f6f233e130f6d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 18:51:20 +0100 Subject: [PATCH] docs: repoint the 8 surviving src/abi/*.idr references and drop the LOC drift surface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- .machine_readable/INTENT.contractile | 2 +- ffi/zig/src/main.zig | 2 +- verification/PROOF-STATUS.adoc | 93 +++++++++++++--------------- verification/README.adoc | 30 +++++++-- 4 files changed, 69 insertions(+), 58 deletions(-) diff --git a/.machine_readable/INTENT.contractile b/.machine_readable/INTENT.contractile index 58e579e9..352e5213 100644 --- a/.machine_readable/INTENT.contractile +++ b/.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" diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index f287a7a7..df3e14dd 100644 --- a/ffi/zig/src/main.zig +++ b/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 diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 6b737538..3604b0d5 100644 --- a/verification/PROOF-STATUS.adoc +++ b/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 diff --git a/verification/README.adoc b/verification/README.adoc index f128359b..4cfa6e66 100644 --- a/verification/README.adoc +++ b/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.