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.