diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml index 7fa7acf4..eea9c8e2 100644 --- a/.github/workflows/verify-proofs.yml +++ b/.github/workflows/verify-proofs.yml @@ -12,7 +12,6 @@ on: - Justfile - pack.toml - verification/proofs/idris2/** - - verification/proofs/lean4/** - verification/proofs/tlaplus/** - verification/proofs/agda/** - verification/PROOF-STATUS.adoc @@ -43,7 +42,6 @@ on: - Justfile - pack.toml - verification/proofs/idris2/** - - verification/proofs/lean4/** - verification/proofs/tlaplus/** - verification/proofs/agda/** - verification/PROOF-STATUS.adoc @@ -231,8 +229,11 @@ jobs: done } >> "$GITHUB_STEP_SUMMARY" - lake-build: - name: lake build + # Lean is no longer a proof lane here: the engineering proofs it held moved + # to Idris2 (PROOF-POLICY section 3; verification/proofs/idris2/). It stays + # for the HYP-01 positive control, which re-runs Lean on a fixture. + lean-hole-recheck: + name: Lean hole re-check (HYP-01 control) runs-on: ubuntu-latest timeout-minutes: 20 permissions: @@ -240,25 +241,20 @@ jobs: env: ELAN_VERSION: v4.0.0 - # Pinned (not :stable) so the proofs are checked against the exact Lean - # they were verified with. Matches verification/proofs/lean4/lean-toolchain; - # bump both together. A moving :stable can break version-sensitive lemmas. + # Pinned (not :stable): tests/accept/LeanHoleRecheckSound.idr records + # the Lean version whose output it digests. LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0 steps: - name: Checkout uses: actions/checkout@v7.0.1 - - name: Cache Lean toolchain and build + - name: Cache Lean toolchain id: cache-lean uses: actions/cache@v6.1.0 with: - path: | - ~/.elan - verification/proofs/lean4/.lake - key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-${{ hashFiles('verification/proofs/lean4/lakefile.lean', 'verification/proofs/lean4/*.lean') }} - restore-keys: | - lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}- + path: ~/.elan + key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-toolchain - name: Install elan + Lean 4 if: steps.cache-lean.outputs.cache-hit != 'true' @@ -270,33 +266,23 @@ jobs: - name: Put elan on PATH run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: lake build - working-directory: verification/proofs/lean4 - run: | - set -euo pipefail - lean --version - lake --version - lake build - # HYP-01 positive control: the SoundVerdict in # tests/accept/LeanHoleRecheckSound.idr records digests of a Lean run. # Re-run Lean on the fixture from the repository root (where the # control's paths are relative to) and require both digests to match. - name: Re-check the Lean proof-hole fixture against the HYP-01 control - run: bash scripts/recheck-lean-hole.sh + run: | + set -euo pipefail + lean --version + bash scripts/recheck-lean-hole.sh - name: Summary if: always() run: | { - echo "## Lean proof verification" + echo "## Lean (HYP-01 positive control)" echo "" echo "- Toolchain: \`${LEAN_TOOLCHAIN}\` via elan \`${ELAN_VERSION}\`" - echo "- Proof files:" - for f in verification/proofs/lean4/*.lean; do - [ "$(basename "$f")" = "lakefile.lean" ] && continue - echo " - \`$(basename "$f")\`" - done } >> "$GITHUB_STEP_SUMMARY" # Estate PROOF-POLICY / Mathesis Grade 3 gate for the one Agda artefact: diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml index cba82d31..25f3e6ba 100644 --- a/.machine_readable/testing/blitz.a2ml +++ b/.machine_readable/testing/blitz.a2ml @@ -267,7 +267,7 @@ evidence = [ [aspects.safety] status = "strong" -evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/", "verification/proofs/lean4/"] +evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/"] banned-patterns-clean = true default-total-idris = true diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 5defac9a..7b8eee48 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -20,15 +20,15 @@ state and commitments. Companion detail: `guix.scm` / guix channels are the sole reproducible-build manifests. No `flake.nix` remains; all references reconciled. * *The formal-proof corpus checks in CI* across Idris 2 (v0.7.0), - Lean 4 (v4.30.0), Agda (2.8.0.2, one artefact) and TLA+ (bounded TLC + Agda (2.8.0.2, one artefact) and TLA+ (bounded TLC model checking, which is `tested-only`, not a proof). What each artefact proves, and how strongly, is the proof ledger (`verification/proof-ledger.jsonl`, rendered in - `verification/PROOF-STATUS.adoc#proof-ledger`): 18 proven of 42; - 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. The four - `proven-with-postulates` rows are Lean proofs that rest on the Lean kernel - axioms `propext` and `Quot.sound`. A source scan does not see those - axioms; `Lean.collectAxioms` does. *Zero escape hatches outside + `verification/PROOF-STATUS.adoc#proof-ledger`): 22 proven of 42; + 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Four of the + Lean proofs rested on the Lean kernel axioms `propext` and `Quot.sound`, + which a source scan does not see and `Lean.collectAxioms` does; they moved + to Idris2 on 2026-11-09, which has no such axioms. *Zero escape hatches outside `test/soundness/fixtures/`* (`believe_me` / `sorry` / `postulate` / `assert_total` / `admit` / `native_decide`). Re-measured 2026-09-26 over the git-tracked tree by `scripts/check-trusted-base.sh`: outside that diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index e705a9b7..16d8e368 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,6 +12,18 @@ https://semver.org/[Semantic Versioning]. === Changed +==== Lean engineering proofs move to Idris2 (2026-11-09) + +* `RateLimiting`, `BayesianUpdate`, `ParserTotality`, `PageRankInvariants` + and `ESNSpectralScaling` are now Idris2 (`verification/proofs/idris2/`, + `%default total`), theorem for theorem (PROOF-POLICY §3; owner decision). + Four of them had rested on the Lean kernel axioms `propext` and + `Quot.sound`; the ledger rows are now `proven`, which makes the census + 22 proven of 42. +* `verification/proofs/lean4/` is removed. The `lake build` job becomes + `Lean hole re-check (HYP-01 control)`, which keeps the pinned Lean only for + the verdict fixture. + ==== Proof claims follow the machine proof ledger (2026-11-09) * `EXPLAINME.adoc` is back at the repository root, as README-EXPLAINME diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 38f9fd7c..ef28226a 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -84,7 +84,7 @@ link:lib/fleet_dispatcher.ex[] line 267. Caveat:: That recipe quarantine is not `Hypatia.Safety.Quarantine`, which nothing -calls (<>). The Lean model of the update uses natural-number +calls (<>). The Idris2 model of the update uses natural-number pseudo-counts, not Elixir floats. === Machine-checked proofs @@ -92,20 +92,22 @@ pseudo-counts, not Elixir floats. [quote, README.adoc] ____ *Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds, - safety-triangle routing, dispatch thresholds, quarantine, rollback), Lean 4 proofs of the Bayesian - update and rate-limiting properties, one Agda model of the Logtalk-to-Elixir migration, and a TLA+ + safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate + limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+ model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of - the code, not the Elixir runtime itself. Proof ledger: 18 proven of 42; 4 proven-with-postulates, + the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open ____ How this is implemented:: See <>. link:.github/workflows/verify-proofs.yml[] runs -`idris2 --check` per proof file, `idris2 --build` of both ipkgs, `lake -build`, Agda in its strict profile and TLC. +`idris2 --check` per proof file, `idris2 --build` of both ipkgs, Agda in +its strict profile and TLC; Lean runs only for the HYP-01 control. Caveat:: -Four of the five Lean rows rest on `propext` (two also on `Quot.sound`). +The Bayesian-update, rate-limiting, parser and neural-precondition proofs moved +from Lean to Idris2 on 2026-11-09, which removed the Lean kernel axioms +(`propext`, `Quot.sound`) four of them rested on. The TLA+ row is `tested-only`: one bounded instance. The modelled rate limiter is not called by any dispatch path. The census matches the ledger. @@ -268,7 +270,7 @@ workflow (debt register T-1). | `lib/outcome_tracker.ex` | Beta update; re-scan with `panic-attack assail` | `lib/application.ex` | What is supervised | `.github/workflows/zig.yml` | FFI tests run; exactly 18 `hypatia_*` exports -| `.github/workflows/verify-proofs.yml` | Idris2, Lean, Agda and TLC in CI +| `.github/workflows/verify-proofs.yml` | Idris2, Agda and TLC in CI; Lean for the HYP-01 control | `docs/DEBT-REGISTER.adoc` | What is broken, ungated or stale |=== @@ -284,7 +286,7 @@ Census, from `scripts/proof-ledger.sh check`: [source,text] ---- -18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. +22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. ---- Of the three theory rows, `logtalk-migration` is `PWG-3`; diff --git a/README.adoc b/README.adoc index b4c34733..8647158e 100644 --- a/README.adoc +++ b/README.adoc @@ -25,10 +25,10 @@ It combines: * *Bayesian confidence* — every recipe carries a Beta-distributed confidence updated from real outcomes, which gates whether a fix is applied automatically, proposed as a PR, or merely reported * *Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds, - safety-triangle routing, dispatch thresholds, quarantine, rollback), Lean 4 proofs of the Bayesian - update and rate-limiting properties, one Agda model of the Logtalk-to-Elixir migration, and a TLA+ + safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate + limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+ model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of - the code, not the Elixir runtime itself. Proof ledger: 18 proven of 42; 4 proven-with-postulates, + the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open (link:EXPLAINME.adoc#proof-ledger[details]) === Core philosophy @@ -80,7 +80,7 @@ PatternRegistry ──> TriangleRouter ──> FleetDispatcher ──> DispatchM | `src/Hypatia/ABI/` | Idris2 ABI — Types, GraphQL, gRPC, REST, FFI, RuleEngine | `ffi/zig/` | Zig C ABI bridge — 18 exports + 16 protocol connectors | `adapters/ cli/ data/ fixer/ integration/` | Rust workspace -| `verification/` | Proof ledger and proofs: Idris2, Lean 4, Agda, TLA+ +| `verification/` | Proof ledger and proofs: Idris2, Agda, TLA+ |=== See link:docs/architecture/topology.md[docs/architecture/topology.md] for the full map. diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index dddf4b28..4332b9fd 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -1,5 +1,11 @@ == Proofs Gap Analysis +NOTE: Historical (2026-04-22), kept as the record of that analysis. Since then +the Lean engineering proofs moved to Idris2 (2026-11-09), an Agda artefact +returned, and every prover runs in CI. The current state is the proof ledger +(`+verification/proof-ledger.jsonl+`); the convergence plan is +`+docs/proofs/HANDOVER-neural-convergence.adoc+`. + *Date:* 2026-04-22 *Scope:* VCL query correctness + neural ensemble convergence *Status:* Inventory + prioritised plan. No code changes yet. diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index 99360ad3..079917ce 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -20,9 +20,9 @@ Plans: * Neural convergence (rows `+pagerank-convergence+` and `+esn-echo-state+`): `+docs/proofs/HANDOVER-neural-convergence.adoc+`. Agda first, over constructive reals, then the Rocq and Lean legs. -* Lean engineering proofs (rows `+lean-*+`): moving to Idris2 (PROOF-POLICY - §3; owner decision 2026-11-09). The move also removes the Lean kernel - axioms (`+propext+`, `+Quot.sound+`) that four of them rest on. +* The Lean engineering proofs moved to Idris2 on 2026-11-09 (PROOF-POLICY §3; + owner decision), which removed the Lean kernel axioms (`+propext+`, + `+Quot.sound+`) four of them rested on. Prover mapping and statuses: the estate PROOF-POLICY (`+metadatastician/standards/3-practice/PROOF-POLICY.adoc+`). diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh index bd817df1..2c60f836 100755 --- a/tests/proof-ledger-test.sh +++ b/tests/proof-ledger-test.sh @@ -32,6 +32,11 @@ expect_msg() { } # mutate mutate() { + # A mutant whose target row is gone would mutate nothing and pass for the + # wrong reason: refuse it. + if ! jq -e --arg id "$3" "select(.id == \$id)" verification/proof-ledger.jsonl >/dev/null; then + fail=$((fail + 1)); echo " FAIL mutant $1 targets row $3, which the ledger does not have" >&2 + fi jq -cS --arg id "$3" "if .id == \$id then $2 else . end" verification/proof-ledger.jsonl > "$work/$1.jsonl" } @@ -41,10 +46,10 @@ expect "the committed PROOF-STATUS block is the ledger's rendering" 0 bash "$scr mutate status-escape '.status = "COMPLETE"' abi-types expect "a status outside the closed vocabulary is refused" 1 env PROOF_LEDGER="$work/status-escape.jsonl" bash "$script" check -mutate hidden-axioms '.status = "proven"' lean-rate-limiting +mutate hidden-axioms '.axioms = ["propext"]' rate-limiting expect "proven with axioms listed is refused (it is proven-with-postulates)" 1 env PROOF_LEDGER="$work/hidden-axioms.jsonl" bash "$script" check -mutate unnamed-axioms '.axioms = []' lean-parser-totality +mutate unnamed-axioms '.status = "proven-with-postulates"' parser-totality expect "proven-with-postulates without its axioms is refused" 1 env PROOF_LEDGER="$work/unnamed-axioms.jsonl" bash "$script" check mutate renamed-proof '.names += ["noSuchTheorem"]' safety-triangle diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index aceb5958..40dc00d2 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -41,12 +41,13 @@ neurosymbolic CI/CD platform. need their own correspondence evidence and tests, and the ledger gives them their own rows. -NOTE: This repo verifies Idris2, Lean and TLA+ artefacts in CI, and carries -one narrowly scoped Agda artefact (`+LogtalkMigration.agda+`) gated by the -same workflow. It does not yet run an Agda + Rocq + Lean reconciliation -pipeline. The Lean files state engineering properties; they stay in Lean, -labelled as such, until they are next touched (PROOF-POLICY §3). They are not -recheck legs of any Agda proof. +NOTE: This repo verifies Idris2 and TLA+ artefacts in CI, and carries one +narrowly scoped Agda artefact (`+LogtalkMigration.agda+`) gated by the same +workflow. It does not yet run an Agda + Rocq + Lean reconciliation pipeline. +The engineering proofs that were in Lean (rate limiting, Bayesian update, VCL +parser, PageRank and ESN preconditions) moved to Idris2 on 2026-11-09 +(PROOF-POLICY §3). Lean still runs in CI, but only for the HYP-01 control +fixture. // BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand) [[proof-ledger]] @@ -56,7 +57,7 @@ Rendered from `+verification/proof-ledger.jsonl+`, which is canonical: where thi ledger disagree, the ledger wins and this table is regenerated. Checked against PROOF-POLICY as pinned by `+metadatastician/standards 3-practice/PROOF-POLICY.adoc b8f60511e76c9015d86990317162dce653c92fe1+`. -*Census:* 18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Theory rows: 3 (PWG-1 0, PWG-2ii 0, PWG-2i 0, PWG-3 1, ungraded 2). +*Census:* 22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Theory rows: 3 (PWG-1 0, PWG-2ii 0, PWG-2i 0, PWG-3 1, ungraded 2). [cols="3,1,2,2,2",options="header"] |=== @@ -243,34 +244,34 @@ Checked against PROOF-POLICY as pinned by `+metadatastician/standards 3-practice |There is no Signalbox repository to apply the criterion to |The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7) -|proven-with-postulates (Quot.sound, propext) -|Lean 4.30.0, lake build; axioms by Lean.collectAxioms -|`+verification/proofs/lean4/RateLimiting.lean+`: `+tryAccept_preserves_invariant+`, `+prune_preserves_invariant+`, `+processEvents_preserves_invariant+`, `+at_limit_rejects+`, `+count_bounded_after_accepts+` -|Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3) +|proven +|Idris2 0.7.0, idris2 --check (--total) +|`+verification/proofs/idris2/RateLimiting.idr+`: `+tryAcceptPreservesInvariant+`, `+prunePreservesInvariant+`, `+processEventsPreservesInvariant+`, `+atLimitRejects+`, `+countBoundedAfterAccepts+` +|Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Moved from Lean 2026-11-09 (PROOF-POLICY section 3) |The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7) -|proven-with-postulates (Quot.sound, propext) -|Lean 4.30.0, lake build; axioms by Lean.collectAxioms -|`+verification/proofs/lean4/BayesianUpdate.lean+`: `+posterior_lt_one+`, `+posterior_pos+`, `+more_successes_raises+`, `+more_failures_lowers+`, `+clamp_ge_floor+`, `+clamp_le_cap+`, `+bayesian_update_sound+` -|Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3) +|proven +|Idris2 0.7.0, idris2 --check (--total) +|`+verification/proofs/idris2/BayesianUpdate.idr+`: `+posteriorLtOne+`, `+posteriorPos+`, `+moreSuccessesRaises+`, `+moreFailuresLowers+`, `+clampGeFloor+`, `+clampLeCap+`, `+bayesianUpdateSound+` +|Over Nat pseudo-counts; Elixir floats are not modelled. Moved from Lean 2026-11-09 (PROOF-POLICY section 3) |The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input -|proven-with-postulates (propext) -|Lean 4.30.0, lake build; axioms by Lean.collectAxioms -|`+verification/proofs/lean4/ParserTotality.lean+`: `+parseFrom_deterministic+`, `+parseFrom_passes_remainder+`, `+parseFrom_orphan_from+`, `+parseFrom_no_from_keyword+` -|FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3) +|proven +|Idris2 0.7.0, idris2 --check (--total) +|`+verification/proofs/idris2/ParserTotality.idr+`: `+parseFromDeterministic+`, `+parseFromPassesRemainder+`, `+parseFromOrphanFrom+`, `+parseFromNoFromKeyword+` +|FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moved from Lean 2026-11-09 (PROOF-POLICY section 3) |PageRank inputs are well formed: edge weights and in/out weight sums are non-negative |proven -|Lean 4.30.0, lake build; axioms by Lean.collectAxioms -|`+verification/proofs/lean4/PageRankInvariants.lean+`: `+edge_weight_nonneg+`, `+outWeightSum_nonneg+`, `+inWeightSum_nonneg+`, `+pagerank_preconditions_sound+` -|Preconditions only; convergence is row pagerank-convergence +|Idris2 0.7.0, idris2 --check (--total) +|`+verification/proofs/idris2/PageRankInvariants.idr+`: `+edgeWeightNonneg+`, `+outWeightSumNonneg+`, `+inWeightSumNonneg+`, `+pagerankPreconditionsSound+` +|Preconditions only; convergence is row pagerank-convergence. Moved from Lean 2026-11-09 (PROOF-POLICY section 3) |ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs -|proven-with-postulates (propext) -|Lean 4.30.0, lake build; axioms by Lean.collectAxioms -|`+verification/proofs/lean4/ESNSpectralScaling.lean+`: `+denom_pos_when_floor_pos+`, `+denom_ge_maxAbs+`, `+denom_ge_floor+`, `+esn_scaling_preconditions_sound+` -|Preconditions only; echo-state stability is row esn-echo-state +|proven +|Idris2 0.7.0, idris2 --check (--total) +|`+verification/proofs/idris2/ESNSpectralScaling.idr+`: `+denomPosWhenFloorPos+`, `+denomGeMaxAbs+`, `+denomGeFloor+`, `+esnScalingPreconditionsSound+` +|Preconditions only; the echo-state property is row esn-echo-state. Moved from Lean 2026-11-09 (PROOF-POLICY section 3) |Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8) |tested-only @@ -312,7 +313,7 @@ Checked against PROOF-POLICY as pinned by `+metadatastician/standards 3-practice |open |- |`+lib/vcl/query.ex+`: `+fetch_scans+` -|Only FROM-clause parsing is modelled (row lean-parser-totality) +|Only FROM-clause parsing is modelled (row parser-totality) |=== // END GENERATED: proof ledger @@ -387,7 +388,7 @@ snapshot * *P6.3* Fault Tolerance: even partially failed batches are reversible to original state -==== 7. Rate Limiting (`+RateLimiting.lean+`) +==== 7. Rate Limiting (`+RateLimiting.idr+`) * *P7.1* Empty state satisfies invariant (base case) * *P7.2* `+tryAccept+` preserves invariant (inductive step) @@ -398,9 +399,9 @@ list) rejected * *P7.6* Count bounded after any sequence of accepts -Status for all of P7: `proven-with-postulates`. The proofs rest on the Lean -kernel axioms `propext` and `Quot.sound` (`at_limit_rejects` on -`propext` only), as `Lean.collectAxioms` reports under Lean 4.30.0. +Status for all of P7: `proven` (Idris2 0.7.0, `%default total`). Moved +from Lean on 2026-11-09; the Lean proofs rested on the kernel axioms +`propext` and `Quot.sound`, which Idris2 does not have. ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`) diff --git a/verification/proof-ledger.jsonl b/verification/proof-ledger.jsonl index 04c78200..e058c9cd 100644 --- a/verification/proof-ledger.jsonl +++ b/verification/proof-ledger.jsonl @@ -28,15 +28,15 @@ {"axioms":[],"bounds":"","checker":"-","file":"lib/safety/quarantine.ex","id":"retraction-runtime-wiring","kind":"engineering","names":["retract_dependents"],"obligation":"Quarantine.retract_dependents/1 is called by a scan or dispatch path","status":"open","trust_boundary":"Not wired, like the rest of the safety systems (CLAUDE.md Known Gap 2)"} {"axioms":[],"bounds":"ExUnit cases","checker":"ExUnit (mix test)","file":"test/dispatch_manifest_test.exs","id":"dispatch-manifest-steps","kind":"engineering","names":["DispatchManifest"],"obligation":"Every dispatch-manifest step names the verdict it derives from, and a factless step refuses the whole manifest before anything is written","status":"tested-only","trust_boundary":"Hypatia's own derived workflow only"} {"axioms":[],"bounds":"","checker":"-","file":"test/dispatch_manifest_test.exs","id":"signalbox","kind":"engineering","names":["DispatchManifest"],"obligation":"The Signalbox derived-workflow criterion holds","status":"open","trust_boundary":"There is no Signalbox repository to apply the criterion to"} -{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/RateLimiting.lean","id":"lean-rate-limiting","kind":"engineering","names":["tryAccept_preserves_invariant","prune_preserves_invariant","processEvents_preserves_invariant","at_limit_rejects","count_bounded_after_accepts"],"obligation":"The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)","status":"proven-with-postulates","trust_boundary":"Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3)"} -{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/BayesianUpdate.lean","id":"lean-bayesian-update","kind":"engineering","names":["posterior_lt_one","posterior_pos","more_successes_raises","more_failures_lowers","clamp_ge_floor","clamp_le_cap","bayesian_update_sound"],"obligation":"The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)","status":"proven-with-postulates","trust_boundary":"Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3)"} -{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ParserTotality.lean","id":"lean-parser-totality","kind":"engineering","names":["parseFrom_deterministic","parseFrom_passes_remainder","parseFrom_orphan_from","parseFrom_no_from_keyword"],"obligation":"The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input","status":"proven-with-postulates","trust_boundary":"FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3)"} -{"axioms":[],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/PageRankInvariants.lean","id":"lean-pagerank-preconditions","kind":"engineering","names":["edge_weight_nonneg","outWeightSum_nonneg","inWeightSum_nonneg","pagerank_preconditions_sound"],"obligation":"PageRank inputs are well formed: edge weights and in/out weight sums are non-negative","status":"proven","trust_boundary":"Preconditions only; convergence is row pagerank-convergence"} -{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ESNSpectralScaling.lean","id":"lean-esn-preconditions","kind":"engineering","names":["denom_pos_when_floor_pos","denom_ge_maxAbs","denom_ge_floor","esn_scaling_preconditions_sound"],"obligation":"ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs","status":"proven-with-postulates","trust_boundary":"Preconditions only; echo-state stability is row esn-echo-state"} +{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/RateLimiting.idr","id":"rate-limiting","kind":"engineering","names":["tryAcceptPreservesInvariant","prunePreservesInvariant","processEventsPreservesInvariant","atLimitRejects","countBoundedAfterAccepts"],"obligation":"The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)","status":"proven","trust_boundary":"Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"} +{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/BayesianUpdate.idr","id":"bayesian-update","kind":"engineering","names":["posteriorLtOne","posteriorPos","moreSuccessesRaises","moreFailuresLowers","clampGeFloor","clampLeCap","bayesianUpdateSound"],"obligation":"The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)","status":"proven","trust_boundary":"Over Nat pseudo-counts; Elixir floats are not modelled. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"} +{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/ParserTotality.idr","id":"parser-totality","kind":"engineering","names":["parseFromDeterministic","parseFromPassesRemainder","parseFromOrphanFrom","parseFromNoFromKeyword"],"obligation":"The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input","status":"proven","trust_boundary":"FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"} +{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/PageRankInvariants.idr","id":"pagerank-preconditions","kind":"engineering","names":["edgeWeightNonneg","outWeightSumNonneg","inWeightSumNonneg","pagerankPreconditionsSound"],"obligation":"PageRank inputs are well formed: edge weights and in/out weight sums are non-negative","status":"proven","trust_boundary":"Preconditions only; convergence is row pagerank-convergence. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"} +{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/ESNSpectralScaling.idr","id":"esn-preconditions","kind":"engineering","names":["denomPosWhenFloorPos","denomGeMaxAbs","denomGeFloor","esnScalingPreconditionsSound"],"obligation":"ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs","status":"proven","trust_boundary":"Preconditions only; the echo-state property is row esn-echo-state. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"} {"axioms":[],"bounds":"3 bots x 2 repos, MaxRequests = 4: 444715 distinct states, depth 13, no error","checker":"TLC 2.19 (rev 5a47802), -workers auto -config KinGate.cfg","file":"verification/proofs/tlaplus/KinGate.tla","id":"kin-gate","kind":"engineering","names":["KinGateSafe","MutualExclusionByType","MutualExclusionBotView","ViewCoherentWithLocks","NoOrphanView","GrantsAreWellBracketed","EveryRequestProcessed"],"obligation":"Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8)","status":"tested-only","trust_boundary":"One bounded instance; the Elixir kin gate is not shown to follow the spec"} {"axioms":[],"bounds":"","checker":"Agda 2.8.0.2, builtins only, --safe --without-K --cubical-compatible","file":"verification/proofs/agda/LogtalkMigration.agda","foundation_diverse":false,"id":"logtalk-migration","kind":"theory","legs":[],"names":["categoriesAgree","severitiesAgree","autoFixableAgrees","fixPresenceAgrees","preventionAgreesToken","preventionAgreesPinned","preventionAgreesMissing","preventionAgreesHardCoded","preventionAgreesVulnerabilities","preventionAgreesSecurityPolicy","preventionBranchSource","preventionBranchTarget","preventionCodeReviewSource","preventionCodeReviewTarget"],"obligation":"The 18 transcribed alert types agree between security_learning.lgt and Hypatia.Rules.SecurityErrors on category, severity, auto-fixability and fix presence; prevention agrees except the two ledgered non-equalities","pwg":"3","status":"proven","trust_boundary":"The finite table as transcribed; fix strings and Elixir runtime behaviour are outside the model. No Rocq or Lean leg yet"} {"axioms":[],"bounds":"ExUnit cases over the migrated alert types","checker":"ExUnit (mix test)","file":"test/security_errors_test.exs","id":"logtalk-runtime","kind":"engineering","names":["SecurityErrors"],"obligation":"Hypatia.Rules.SecurityErrors at runtime follows the table the Agda model states","status":"tested-only","trust_boundary":"Example-based; the transcription into the Agda table is not itself checked"} {"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"pagerank-convergence","kind":"theory","legs":[],"names":[],"obligation":"Damped PageRank iteration converges to a unique stationary vector","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib"} {"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"esn-echo-state","kind":"theory","legs":[],"names":[],"obligation":"With leak rate 0 < a <= 1 and the reservoir scaled to infinity-norm at most 0.95, two state trajectories under the same input converge geometrically (echo-state property), and [-1,1]^n is invariant","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib. The runtime scales by the induced infinity-norm, not the spectral radius"} {"axioms":[],"bounds":"","checker":"-","file":"-","id":"models-runtime-refinement","kind":"engineering","names":[],"obligation":"The Elixir runtime follows the Idris2, Lean and TLA+ models above","status":"open","trust_boundary":"No correspondence evidence beyond the rows that name a runtime test; a model row proves its model only (README-EXPLAINME section 5 rule 3)"} -{"axioms":[],"bounds":"","checker":"-","file":"lib/vcl/query.ex","id":"vcl-query-correctness","kind":"engineering","names":["fetch_scans"],"obligation":"VCL queries return what their semantics says beyond the FROM clause","status":"open","trust_boundary":"Only FROM-clause parsing is modelled (row lean-parser-totality)"} +{"axioms":[],"bounds":"","checker":"-","file":"lib/vcl/query.ex","id":"vcl-query-correctness","kind":"engineering","names":["fetch_scans"],"obligation":"VCL queries return what their semantics says beyond the FROM clause","status":"open","trust_boundary":"Only FROM-clause parsing is modelled (row parser-totality)"} diff --git a/verification/proofs/idris2/BayesianUpdate.idr b/verification/proofs/idris2/BayesianUpdate.idr new file mode 100644 index 00000000..69dd6c73 --- /dev/null +++ b/verification/proofs/idris2/BayesianUpdate.idr @@ -0,0 +1,189 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- BayesianUpdate.idr — Bayesian confidence update soundness (H7). +-- +-- Re-homed from verification/proofs/lean4/BayesianUpdate.lean (PROOF-POLICY +-- section 3). The statements are the Lean file's; the Lean proofs rested on +-- the kernel axioms propext and Quot.sound, which Idris2 does not have. +-- +-- Models the Beta-conjugate update in lib/outcome_tracker.ex +-- (prior_strength = 10): +-- alpha_post = alpha_prior + successes, beta_post = beta_prior + failures, +-- posterior = alpha_post / (alpha_post + beta_post), +-- result = clamp(posterior, floor = 10%, cap = 99%). +-- Ratios are compared by cross-multiplication over Nat; Elixir floats are +-- not modelled. + +module BayesianUpdate + +import Control.Relation +import Data.Nat + +%default total + +------------------------------------------------------------------------ +-- Section 1: fraction comparison over Nat (a/b <= c/d iff a*d <= c*b) +------------------------------------------------------------------------ + +||| alpha / (alpha + beta) < 1 when beta > 0: alpha < alpha + beta. +export +fracLtOne : (alpha, beta : Nat) -> LT 0 beta -> LT alpha (alpha + beta) +fracLtOne alpha (S b) _ = + rewrite sym (plusSuccRightSucc alpha b) in LTESucc (lteAddRight alpha) + +||| alpha / (alpha + beta) > 0 when alpha > 0. +export +fracPos : (alpha : Nat) -> LT 0 alpha -> LT 0 alpha +fracPos _ h = h + +||| The denominator alpha + beta is positive when alpha is. +export +denomPos : (alpha, beta : Nat) -> LT 0 alpha -> LT 0 (alpha + beta) +denomPos alpha beta h = transitive h (lteAddRight alpha) + +------------------------------------------------------------------------ +-- Section 2: the Beta update +------------------------------------------------------------------------ + +||| Posterior parameters: alpha = alpha_prior + successes, beta = beta_prior +||| + failures, both positive. +public export +record BayesParams where + constructor MkBayesParams + alpha : Nat + beta : Nat + alphaPos : LT 0 alpha + betaPos : LT 0 beta + +||| The denominator alpha + beta. +public export +denom : BayesParams -> Nat +denom p = p.alpha + p.beta + +||| The denominator is positive. +export +paramsDenomPos : (p : BayesParams) -> LT 0 (denom p) +paramsDenomPos p = denomPos p.alpha p.beta p.alphaPos + +------------------------------------------------------------------------ +-- Section 3: the posterior is in (0, 1) +------------------------------------------------------------------------ + +||| H7, property 1: alpha / (alpha + beta) < 1. +export +posteriorLtOne : (p : BayesParams) -> LT p.alpha (denom p) +posteriorLtOne p = fracLtOne p.alpha p.beta p.betaPos + +||| H7, property 2: alpha / (alpha + beta) > 0. +export +posteriorPos : (p : BayesParams) -> LT 0 p.alpha +posteriorPos p = p.alphaPos + +------------------------------------------------------------------------ +-- Section 4: monotonicity +------------------------------------------------------------------------ + +||| Multiplication by k is monotone. +export +multLteMonotoneLeft : {m, n : Nat} -> (k : Nat) -> LTE m n -> LTE (k * m) (k * n) +multLteMonotoneLeft Z _ = LTEZero +multLteMonotoneLeft (S k) h = plusLteMonotone h (multLteMonotoneLeft k h) + +||| H7, property 3: a success weakly raises the ratio: +||| alpha * (alpha + 1 + beta) <= (alpha + 1) * (alpha + beta). +export +moreSuccessesRaises : (p : BayesParams) -> + LTE (p.alpha * (p.alpha + 1 + p.beta)) ((p.alpha + 1) * (p.alpha + p.beta)) +moreSuccessesRaises p = + rewrite hs1 in rewrite hs2 in + plusLteMonotoneLeft (p.alpha * (p.alpha + p.beta)) p.alpha (p.alpha + p.beta) + (lteAddRight p.alpha) + where + reassoc : p.alpha + 1 + p.beta = (p.alpha + p.beta) + 1 + reassoc = rewrite sym (plusAssociative p.alpha 1 p.beta) in + rewrite plusCommutative 1 p.beta in + plusAssociative p.alpha p.beta 1 + hs1 : p.alpha * (p.alpha + 1 + p.beta) = p.alpha * (p.alpha + p.beta) + p.alpha + hs1 = rewrite reassoc in + rewrite multDistributesOverPlusRight p.alpha (p.alpha + p.beta) 1 in + rewrite multOneRightNeutral p.alpha in Refl + hs2 : (p.alpha + 1) * (p.alpha + p.beta) = p.alpha * (p.alpha + p.beta) + (p.alpha + p.beta) + hs2 = rewrite multDistributesOverPlusLeft p.alpha 1 (p.alpha + p.beta) in + rewrite multOneLeftNeutral (p.alpha + p.beta) in Refl + +||| H7, property 4: a failure weakly lowers the ratio: +||| alpha * (alpha + beta) <= alpha * (alpha + beta + 1). +export +moreFailuresLowers : (p : BayesParams) -> + LTE (p.alpha * (p.alpha + p.beta)) (p.alpha * (p.alpha + p.beta + 1)) +moreFailuresLowers p = multLteMonotoneLeft p.alpha (lteAddRight (p.alpha + p.beta)) + +------------------------------------------------------------------------ +-- Section 5: zero observations return the prior +------------------------------------------------------------------------ + +||| A prior as a fraction (alpha_p = prior * 10, beta_p = (1 - prior) * 10). +public export +record Prior where + constructor MkPrior + alphaP : Nat + betaP : Nat + alphaPPos : LT 0 alphaP + betaPPos : LT 0 betaP + +||| The posterior after no successes and no failures. +public export +fromPrior : Prior -> BayesParams +fromPrior p = MkBayesParams p.alphaP p.betaP p.alphaPPos p.betaPPos + +||| H7, property 5: with no observations the posterior alpha is the prior's. +export +zeroObsAlpha : (p : Prior) -> (fromPrior p).alpha = p.alphaP +zeroObsAlpha _ = Refl + +||| H7, property 6: with no observations the posterior beta is the prior's. +export +zeroObsBeta : (p : Prior) -> (fromPrior p).beta = p.betaP +zeroObsBeta _ = Refl + +||| H7, property 7: with no observations the denominator is unchanged. +export +zeroObsDenom : (p : Prior) -> denom (fromPrior p) = p.alphaP + p.betaP +zeroObsDenom _ = Refl + +------------------------------------------------------------------------ +-- Section 6: floor (10%) and cap (99%) +------------------------------------------------------------------------ + +||| minimum m n never exceeds n. +export +minimumLTERight : (m, n : Nat) -> LTE (minimum m n) n +minimumLTERight Z n = LTEZero +minimumLTERight (S m) Z = LTEZero +minimumLTERight (S m) (S n) = LTESucc (minimumLTERight m n) + +||| H7, property 8: the clamped result is at least the floor. +export +clampGeFloor : (raw : Nat) -> LTE 1 (maximum 1 raw) +clampGeFloor raw = maximumLeftUpperBound 1 raw + +||| H7, property 9: the clamped result is at most the cap. +export +clampLeCap : (raw : Nat) -> LTE (minimum raw 99) 99 +clampLeCap raw = minimumLTERight raw 99 + +------------------------------------------------------------------------ +-- Section 7: composite validity +------------------------------------------------------------------------ + +||| H7, main theorem: a BayesParams with alpha, beta > 0 satisfies all four +||| validity conditions. +export +bayesianUpdateSound : (p : BayesParams) -> + ( LT 0 p.alpha + , LT p.alpha (denom p) + , LTE (p.alpha * (p.alpha + 1 + p.beta)) ((p.alpha + 1) * (p.alpha + p.beta)) + , LTE (p.alpha * (p.alpha + p.beta)) (p.alpha * (p.alpha + p.beta + 1)) ) +bayesianUpdateSound p = + (posteriorPos p, posteriorLtOne p, moreSuccessesRaises p, moreFailuresLowers p) diff --git a/verification/proofs/idris2/ESNSpectralScaling.idr b/verification/proofs/idris2/ESNSpectralScaling.idr new file mode 100644 index 00000000..e41ad134 --- /dev/null +++ b/verification/proofs/idris2/ESNSpectralScaling.idr @@ -0,0 +1,126 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ESNSpectralScaling.idr — the reservoir scaling step is well defined, over Nat. +-- +-- Re-homed from verification/proofs/lean4/ESNSpectralScaling.lean +-- (PROOF-POLICY section 3). The statements are the Lean file's; the Lean +-- proofs rested on the kernel axiom propext, which Idris2 does not have. +-- +-- lib/neural/echo_state_network.ex scales the reservoir by +-- scale = reservoir_norm / max(max_row_sum, 0.001), +-- the induced infinity-norm (largest absolute row sum), not the spectral +-- radius. This file shows, over a Nat model, that the floor-guarded +-- denominator is positive whenever the floor is, so the scaling never +-- divides by zero. The echo-state property itself is a theory theorem, +-- planned in Agda over constructive reals +-- (docs/proofs/HANDOVER-neural-convergence.adoc); it is not proved here. + +module ESNSpectralScaling + +import Control.Relation +import Data.Nat + +%default total + +------------------------------------------------------------------------ +-- Section 1: the model (entries are Nat magnitudes) +------------------------------------------------------------------------ + +||| A matrix as a list of rows. +public export +Matrix : Type +Matrix = List (List Nat) + +||| Each row's sum of entry magnitudes (Enum.map(row, &abs/1) |> Enum.sum()). +public export +rowSums : Matrix -> List Nat +rowSums m = map sum m + +||| The largest element, or the floor for an empty list +||| (Enum.max(fn -> 1.0 end)). +public export +maxAbsOr : List Nat -> (floor : Nat) -> Nat +maxAbsOr xs floor = foldl (\acc, x => if x > acc then x else acc) floor xs + +||| The induced infinity-norm (largest row sum), with a floor. +public export +matrixMaxAbs : Matrix -> (floor : Nat) -> Nat +matrixMaxAbs m floor = maxAbsOr (rowSums m) floor + +||| The scaling ratio of the target to the floor-clamped norm. +public export +scaleRatio : (target, maxAbs, floor : Nat) -> Nat +scaleRatio target maxAbs floor = div target (maximum maxAbs floor) + +------------------------------------------------------------------------ +-- Section 2: the empty matrix +------------------------------------------------------------------------ + +||| Property 1: an empty matrix has no row sums. +export +rowSumsNil : rowSums [] = [] +rowSumsNil = Refl + +||| Property 2: maxAbsOr of an empty list is the floor. +export +maxAbsOrNil : (floor : Nat) -> maxAbsOr [] floor = floor +maxAbsOrNil _ = Refl + +||| Property 3: an empty matrix's norm is its floor. +export +matrixMaxAbsNil : (floor : Nat) -> matrixMaxAbs [] floor = floor +matrixMaxAbsNil _ = Refl + +------------------------------------------------------------------------ +-- Section 3: non-negativity +------------------------------------------------------------------------ + +||| Property 4: the norm is non-negative. +export +matrixMaxAbsNonneg : (m : Matrix) -> (floor : Nat) -> LTE 0 (matrixMaxAbs m floor) +matrixMaxAbsNonneg _ _ = LTEZero + +||| Property 5: the scaling ratio is non-negative. +export +scaleRatioNonneg : (target, maxAbs, floor : Nat) -> LTE 0 (scaleRatio target maxAbs floor) +scaleRatioNonneg _ _ _ = LTEZero + +------------------------------------------------------------------------ +-- Section 4: the denominator is positive +------------------------------------------------------------------------ + +||| Property 6: a positive floor makes the clamped denominator positive, so +||| the scaling never divides by zero. +export +denomPosWhenFloorPos : (maxAbs, floor : Nat) -> LT 0 floor -> LT 0 (maximum maxAbs floor) +denomPosWhenFloorPos maxAbs floor hf = transitive hf (maximumRightUpperBound maxAbs floor) + +||| Property 7: the clamped denominator is at least maxAbs. +export +denomGeMaxAbs : (maxAbs, floor : Nat) -> LTE maxAbs (maximum maxAbs floor) +denomGeMaxAbs = maximumLeftUpperBound + +||| Property 8: the clamped denominator is at least the floor. +export +denomGeFloor : (maxAbs, floor : Nat) -> LTE floor (maximum maxAbs floor) +denomGeFloor = maximumRightUpperBound + +------------------------------------------------------------------------ +-- Section 5: composite +------------------------------------------------------------------------ + +||| Main theorem: for any reservoir and any positive floor, the norm is +||| non-negative and the clamped denominator is positive and bounds both +||| the norm and the floor. +export +esnScalingPreconditionsSound : (m : Matrix) -> (maxAbs, floor : Nat) -> LT 0 floor -> + ( LTE 0 (matrixMaxAbs m floor) + , LT 0 (maximum maxAbs floor) + , LTE maxAbs (maximum maxAbs floor) + , LTE floor (maximum maxAbs floor) ) +esnScalingPreconditionsSound m maxAbs floor hf = + ( matrixMaxAbsNonneg m floor + , denomPosWhenFloorPos maxAbs floor hf + , denomGeMaxAbs maxAbs floor + , denomGeFloor maxAbs floor ) diff --git a/verification/proofs/idris2/PageRankInvariants.idr b/verification/proofs/idris2/PageRankInvariants.idr new file mode 100644 index 00000000..b48b7057 --- /dev/null +++ b/verification/proofs/idris2/PageRankInvariants.idr @@ -0,0 +1,89 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- PageRankInvariants.idr — preconditions of the PageRank iteration, over Nat. +-- +-- Re-homed from verification/proofs/lean4/PageRankInvariants.lean +-- (PROOF-POLICY section 3: these are engineering preconditions, so they live +-- in Idris2). The statements are the Lean file's. +-- +-- lib/neural/graph_of_trust.ex (build_edges/1) keeps edge weights +-- non-negative, divides each source's contributions by its outgoing-weight +-- sum, and keeps the damping factor in [0, 1]. This file states the first +-- two over a Nat model. Convergence of the iteration is a theory theorem, +-- planned in Agda over constructive reals +-- (docs/proofs/HANDOVER-neural-convergence.adoc); it is not proved here. + +module PageRankInvariants + +import Data.List +import Data.Nat + +%default total + +------------------------------------------------------------------------ +-- Section 1: the model +------------------------------------------------------------------------ + +||| A weighted directed edge; weights are absolute counts on a shared scale. +public export +record Edge where + constructor MkEdge + src : Nat + tgt : Nat + weight : Nat + +||| The sum of the weights of the edges leaving `src`. +public export +outWeightSum : List Edge -> (src : Nat) -> Nat +outWeightSum edges s = foldl (\acc, e => acc + e.weight) 0 (filter (\e => e.src == s) edges) + +||| The sum of the weights of the edges entering `tgt`. +public export +inWeightSum : List Edge -> (tgt : Nat) -> Nat +inWeightSum edges t = foldl (\acc, e => acc + e.weight) 0 (filter (\e => e.tgt == t) edges) + +------------------------------------------------------------------------ +-- Section 2: non-negativity +------------------------------------------------------------------------ + +||| Property 1: edge weights are non-negative. +export +edgeWeightNonneg : (e : Edge) -> LTE 0 e.weight +edgeWeightNonneg _ = LTEZero + +||| Property 2: every outgoing-weight sum is non-negative. +export +outWeightSumNonneg : (edges : List Edge) -> (s : Nat) -> LTE 0 (outWeightSum edges s) +outWeightSumNonneg _ _ = LTEZero + +||| Property 3: every incoming-weight sum is non-negative. +export +inWeightSumNonneg : (edges : List Edge) -> (t : Nat) -> LTE 0 (inWeightSum edges t) +inWeightSumNonneg _ _ = LTEZero + +------------------------------------------------------------------------ +-- Section 3: the empty graph +------------------------------------------------------------------------ + +||| Property 4: with no edges, every outgoing-weight sum is 0. +export +outWeightSumNil : (s : Nat) -> outWeightSum [] s = 0 +outWeightSumNil _ = Refl + +||| Property 5: with no edges, every incoming-weight sum is 0. +export +inWeightSumNil : (t : Nat) -> inWeightSum [] t = 0 +inWeightSumNil _ = Refl + +------------------------------------------------------------------------ +-- Section 4: composite +------------------------------------------------------------------------ + +||| Main theorem: the step preconditions build_edges/1 maintains hold for +||| every graph. +export +pagerankPreconditionsSound : (edges : List Edge) -> (e : Edge) -> (t : Nat) -> + (LTE 0 e.weight, LTE 0 (outWeightSum edges e.src), LTE 0 (inWeightSum edges t)) +pagerankPreconditionsSound edges e t = + (edgeWeightNonneg e, outWeightSumNonneg edges e.src, inWeightSumNonneg edges t) diff --git a/verification/proofs/idris2/ParserTotality.idr b/verification/proofs/idris2/ParserTotality.idr new file mode 100644 index 00000000..a45f3194 --- /dev/null +++ b/verification/proofs/idris2/ParserTotality.idr @@ -0,0 +1,145 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ParserTotality.idr — totality and round trips of the VCL FROM-clause parser. +-- +-- Re-homed from verification/proofs/lean4/ParserTotality.lean (PROOF-POLICY +-- section 3). The statements are the Lean file's; the Lean proofs rested on +-- the kernel axiom propext, which Idris2 does not have. +-- +-- Models a representative subset of `parse_from/1` in lib/vcl/: FROM STORE, +-- FROM FEDERATION and FROM HEXAD, each followed by a bare identifier or (for +-- STORE and FEDERATION) a quoted literal; anything else is an error. The +-- model omits unquoted URLs, WITH DRIFT and multi-URL sources. It does not +-- show that the Elixir parser follows it. + +module ParserTotality + +%default total + +------------------------------------------------------------------------ +-- Section 1: tokens, sources, errors, results +------------------------------------------------------------------------ + +||| Tokens from the VCL tokenizer; quoted literals are kept apart from bare +||| identifiers so the parser's two paths can be modelled separately. +public export +data Token + = KwFrom + | KwStore + | KwFederation + | KwHexad + | Ident String + | Quoted String + | Other String + +||| The parsed source: {:store, id}, {:federation, pattern}, {:hexad, uuid}. +public export +data Source = Store String | Federation String | Hexad String + +||| Parser errors, structured for the proofs. +public export +data ParseError = ExpectedFromClause | EmptyInput | Malformed + +||| A result: a value and the tokens left over, or an error. +public export +data ParseResult a = Ok a (List Token) | Err ParseError + +------------------------------------------------------------------------ +-- Section 2: the parser +------------------------------------------------------------------------ + +||| Parse a FROM clause. `%default total` makes the checker refuse this +||| definition unless it covers every input and terminates: the +||| definition checking is the totality proof. +public export +parseFrom : List Token -> ParseResult Source +parseFrom (KwFrom :: KwStore :: Ident id :: rest) = Ok (Store id) rest +parseFrom (KwFrom :: KwStore :: Quoted id :: rest) = Ok (Store id) rest +parseFrom (KwFrom :: KwFederation :: Ident pat :: rest) = Ok (Federation pat) rest +parseFrom (KwFrom :: KwFederation :: Quoted pat :: rest) = Ok (Federation pat) rest +parseFrom (KwFrom :: KwHexad :: Ident u :: rest) = Ok (Hexad u) rest +parseFrom [] = Err EmptyInput +parseFrom _ = Err ExpectedFromClause + +------------------------------------------------------------------------ +-- Section 3: totality as a structural property +------------------------------------------------------------------------ + +||| Property 1: parseFrom is a function: equal inputs give equal results. +export +parseFromDeterministic : (ts : List Token) -> parseFrom ts = parseFrom ts +parseFromDeterministic _ = Refl + +||| Property 2: empty input gives the empty-input error. +export +parseFromEmpty : parseFrom [] = Err EmptyInput +parseFromEmpty = Refl + +------------------------------------------------------------------------ +-- Section 4: round trips on well-formed input +------------------------------------------------------------------------ + +||| Property 4: FROM STORE gives a store. +export +parseFromStoreBare : parseFrom [KwFrom, KwStore, Ident "scans"] = Ok (Store "scans") [] +parseFromStoreBare = Refl + +||| Property 5: FROM STORE "quoted" gives a store. +export +parseFromStoreQuoted : parseFrom [KwFrom, KwStore, Quoted "scans"] = Ok (Store "scans") [] +parseFromStoreQuoted = Refl + +||| Property 6: FROM FEDERATION gives a federation, pattern kept. +export +parseFromFederation : parseFrom [KwFrom, KwFederation, Ident "/scans/*"] + = Ok (Federation "/scans/*") [] +parseFromFederation = Refl + +||| Property 7: FROM HEXAD gives a hexad. +export +parseFromHexad : parseFrom [KwFrom, KwHexad, Ident "abc-123"] = Ok (Hexad "abc-123") [] +parseFromHexad = Refl + +||| Property 8: tokens after a valid FROM clause are passed on, so the +||| WHERE / LIMIT / OFFSET parsers still see them. +export +parseFromPassesRemainder : + parseFrom [KwFrom, KwStore, Ident "scans", Other "WHERE", Other "FIELD"] + = Ok (Store "scans") [Other "WHERE", Other "FIELD"] +parseFromPassesRemainder = Refl + +------------------------------------------------------------------------ +-- Section 5: malformed input is rejected +------------------------------------------------------------------------ + +||| Property 9: FROM with no STORE / FEDERATION / HEXAD is rejected. +export +parseFromOrphanFrom : parseFrom [KwFrom] = Err ExpectedFromClause +parseFromOrphanFrom = Refl + +||| Property 10: a clause without FROM is rejected. +export +parseFromNoFromKeyword : parseFrom [KwStore, Ident "scans"] = Err ExpectedFromClause +parseFromNoFromKeyword = Refl + +------------------------------------------------------------------------ +-- Section 6: a Bool view of success +------------------------------------------------------------------------ + +||| Did the parse succeed? +public export +parseFromSucceeded : List Token -> Bool +parseFromSucceeded ts = case parseFrom ts of + Ok _ _ => True + Err _ => False + +||| Property 11: the predicate agrees with the parser on FROM STORE. +export +parseFromSucceededStore : parseFromSucceeded [KwFrom, KwStore, Ident "scans"] = True +parseFromSucceededStore = Refl + +||| Property 12: the predicate is false on empty input. +export +parseFromSucceededEmpty : parseFromSucceeded [] = False +parseFromSucceededEmpty = Refl diff --git a/verification/proofs/idris2/RateLimiting.idr b/verification/proofs/idris2/RateLimiting.idr new file mode 100644 index 00000000..77db2a87 --- /dev/null +++ b/verification/proofs/idris2/RateLimiting.idr @@ -0,0 +1,222 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- RateLimiting.idr — the sliding-window rate limiter never exceeds its bound. +-- +-- Re-homed from verification/proofs/lean4/RateLimiting.lean (PROOF-POLICY +-- section 3: interface and engineering statements live in Idris2). The +-- statements are the Lean file's, theorem for theorem; the Lean proofs rested +-- on the kernel axioms propext and Quot.sound, which Idris2 does not have. +-- +-- Models lib/safety/rate_limiter.ex, which enforces +-- per-bot 50 / 60 s, global 200 / 60 s, burst 10 / 5 s. +-- Over Nat timestamps and counts. The model does not show that the Elixir +-- GenServer follows it, and the GenServer is not on any dispatch path +-- (CLAUDE.md Known Gap 2). + +module RateLimiting + +import Control.Relation +import Data.Nat +import Data.List +import Data.List.Quantifiers + +%default total + +------------------------------------------------------------------------ +-- Section 1: window-based counter model +------------------------------------------------------------------------ + +||| A rate-limiter configuration: the most events allowed in a window. +public export +record RateLimitConfig where + constructor MkRateLimitConfig + maxEvents : Nat + windowSize : Nat + windowPositive : LT 0 windowSize + +||| A timestamped event. +public export +record Event where + constructor MkEvent + timestamp : Nat + +||| The limiter's state: its configuration and the events it has accepted. +public export +record RateLimiterState where + constructor MkRateLimiterState + config : RateLimitConfig + events : List Event + +||| Is the event inside a window that starts at `windowStart`? +public export +inWindow : (windowStart : Nat) -> Event -> Bool +inWindow windowStart e = windowStart <= e.timestamp + +||| Events within [windowStart, now]. +public export +countEventsInWindow : List Event -> (windowStart : Nat) -> Nat +countEventsInWindow es windowStart = length (filter (inWindow windowStart) es) + +||| The start of the window that ends at `now`. +public export +windowStart : RateLimiterState -> (now : Nat) -> Nat +windowStart state now = minus now state.config.windowSize + +||| The in-window count at `now`. +public export +currentCount : RateLimiterState -> (now : Nat) -> Nat +currentCount state now = countEventsInWindow state.events (windowStart state now) + +||| Accept the event only if the in-window count is below the maximum. +public export +tryAccept : RateLimiterState -> Event -> (RateLimiterState, Bool) +tryAccept (MkRateLimiterState cfg evs) e + with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents) + _ | Yes _ = (MkRateLimiterState cfg (e :: evs), True) + _ | No _ = (MkRateLimiterState cfg evs, False) + +||| Drop the events outside the window (garbage collection). +public export +prune : RateLimiterState -> (now : Nat) -> RateLimiterState +prune state@(MkRateLimiterState cfg evs) now = MkRateLimiterState cfg (filter (inWindow (windowStart state now)) evs) + +------------------------------------------------------------------------ +-- Section 2: the invariant +------------------------------------------------------------------------ + +||| The in-window count never exceeds maxEvents. +public export +InvariantHolds : RateLimiterState -> (now : Nat) -> Type +InvariantHolds state now = LTE (currentCount state now) state.config.maxEvents + +||| An empty limiter satisfies the invariant. +export +emptySatisfiesInvariant : (config : RateLimitConfig) -> (now : Nat) -> + InvariantHolds (MkRateLimiterState config []) now +emptySatisfiesInvariant _ _ = LTEZero + +||| Filtering never lengthens a list. +export +filterLengthLTE : (p : a -> Bool) -> (xs : List a) -> LTE (length (filter p xs)) (length xs) +filterLengthLTE p [] = LTEZero +filterLengthLTE p (x :: xs) with (p x) + _ | True = LTESucc (filterLengthLTE p xs) + _ | False = lteSuccRight (filterLengthLTE p xs) + +------------------------------------------------------------------------ +-- Section 3: tryAccept preserves the invariant +------------------------------------------------------------------------ + +||| One more event at the front raises the in-window count by at most one. +export +countConsLTE : (e : Event) -> (es : List Event) -> (ws : Nat) -> + LTE (countEventsInWindow (e :: es) ws) (S (countEventsInWindow es ws)) +countConsLTE e es ws with (inWindow ws e) + _ | True = reflexive + _ | False = lteSuccRight reflexive + +||| After tryAccept the invariant still holds: a rejected event leaves the +||| state unchanged, and an accepted one was let in below the maximum. +export +tryAcceptPreservesInvariant : (state : RateLimiterState) -> (e : Event) -> + InvariantHolds state e.timestamp -> + InvariantHolds (fst (tryAccept state e)) e.timestamp +tryAcceptPreservesInvariant (MkRateLimiterState cfg evs) e h + with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents) + _ | Yes below = + transitive (countConsLTE e evs (minus e.timestamp cfg.windowSize)) below + _ | No _ = h + +------------------------------------------------------------------------ +-- Section 4: prune preserves the invariant +------------------------------------------------------------------------ + +||| Pruning only removes events, so the count can only fall. +export +prunePreservesInvariant : (state : RateLimiterState) -> (now : Nat) -> + InvariantHolds state now -> + InvariantHolds (prune state now) now +prunePreservesInvariant state@(MkRateLimiterState cfg evs) now h = + transitive (filterLengthLTE (inWindow (windowStart state now)) + (filter (inWindow (windowStart state now)) evs)) h + +------------------------------------------------------------------------ +-- Section 5: a sequence of events +------------------------------------------------------------------------ + +||| Offer each event in turn; keep the state tryAccept returns. +public export +processEvents : RateLimiterState -> List Event -> RateLimiterState +processEvents state [] = state +processEvents state (e :: es) = processEvents (fst (tryAccept state e)) es + +||| The invariant holds after any sequence of simultaneous events (the +||| worst-case burst), if it held at the start. +export +processEventsPreservesInvariant : (state : RateLimiterState) -> (es : List Event) -> + (t : Nat) -> All (\e => e.timestamp = t) es -> + InvariantHolds state t -> + InvariantHolds (processEvents state es) t +processEventsPreservesInvariant state [] t [] h = h +processEventsPreservesInvariant state (e :: es) t (prf :: prfs) h = + processEventsPreservesInvariant (fst (tryAccept state e)) es t prfs step + where + step : InvariantHolds (fst (tryAccept state e)) t + step = rewrite sym prf in + tryAcceptPreservesInvariant state e (rewrite prf in h) + +------------------------------------------------------------------------ +-- Section 6: the deployed configurations +------------------------------------------------------------------------ + +||| Per-bot: 50 events per 60 s. +public export +perBotConfig : RateLimitConfig +perBotConfig = MkRateLimitConfig 50 60 (LTESucc LTEZero) + +||| Global: 200 events per 60 s. +public export +globalConfig : RateLimitConfig +globalConfig = MkRateLimitConfig 200 60 (LTESucc LTEZero) + +||| Burst: 10 events per 5 s. +public export +burstConfig : RateLimitConfig +burstConfig = MkRateLimitConfig 10 5 (LTESucc LTEZero) + +export +perBotInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.perBotConfig []) now +perBotInitialValid = emptySatisfiesInvariant perBotConfig + +export +globalInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.globalConfig []) now +globalInitialValid = emptySatisfiesInvariant globalConfig + +export +burstInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.burstConfig []) now +burstInitialValid = emptySatisfiesInvariant burstConfig + +------------------------------------------------------------------------ +-- Section 7: the rejection guarantee +------------------------------------------------------------------------ + +||| At the limit, the next event is rejected. +export +atLimitRejects : (state : RateLimiterState) -> (e : Event) -> + currentCount state e.timestamp = state.config.maxEvents -> + snd (tryAccept state e) = False +atLimitRejects (MkRateLimiterState cfg evs) e full + with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents) + _ | Yes below = absurd (succNotLTEpred (replace {p = \m => LT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) m} (sym full) below)) + _ | No _ = Refl + +||| From an empty limiter, any burst of simultaneous offers keeps the count +||| within the bound. +export +countBoundedAfterAccepts : (config : RateLimitConfig) -> (es : List Event) -> (t : Nat) -> + All (\e => e.timestamp = t) es -> + InvariantHolds (processEvents (MkRateLimiterState config []) es) t +countBoundedAfterAccepts config es t times = + processEventsPreservesInvariant (MkRateLimiterState config []) es t times + (emptySatisfiesInvariant config t) diff --git a/verification/proofs/lean4/.gitignore b/verification/proofs/lean4/.gitignore deleted file mode 100644 index d13c5071..00000000 --- a/verification/proofs/lean4/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Lake build artifacts -/.lake/ -/lake-manifest.json diff --git a/verification/proofs/lean4/BayesianUpdate.lean b/verification/proofs/lean4/BayesianUpdate.lean deleted file mode 100644 index bcdbcafe..00000000 --- a/verification/proofs/lean4/BayesianUpdate.lean +++ /dev/null @@ -1,188 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- BayesianUpdate.lean — Formal proof of Bayesian confidence update soundness (H7). --- --- REQUIREMENTS-MASTER.md: H7 | Bayesian confidence update soundness | ALG | L4 | P1 --- --- Models the Beta-conjugate prior update in lib/outcome_tracker.ex. --- No external dependencies (no Mathlib required). --- --- We represent confidence as a pair (α : Nat, β : Nat) where: --- α > 0, β > 0 (ensures the fraction is in (0,1)) --- confidence = α / (α + β) (real value, but we prove properties via ℕ cross-mult) --- --- The production update (prior_strength = 10): --- α_prior = prior_confidence * 10 --- β_prior = (1 - prior_confidence) * 10 --- α_post = α_prior + successes --- β_post = β_prior + failures --- posterior = α_post / (α_post + β_post) --- result = clamp(posterior, floor=10%, cap=99%) --- --- All ratio comparisons are done by cross-multiplication over ℕ to avoid --- floating-point and to stay within the standard library. - ------------------------------------------------------------------------- --- Section 1: Fraction comparison over ℕ --- --- a/b ≤ c/d (with b,d > 0) iff a*d ≤ c*b ------------------------------------------------------------------------- - -/-- α / (α+β) < 1 iff β > 0. - Proof: α / (α+β) < 1 iff α < α+β iff 0 < β. -/ -theorem frac_lt_one (α β : Nat) (hβ : 0 < β) : α < α + β := Nat.lt_add_of_pos_right hβ - -/-- α / (α+β) > 0 iff α > 0. - Proof: 0 < α / (α+β) iff 0 * (α+β) < α * 1 iff 0 < α. -/ -theorem frac_pos (α : Nat) (hα : 0 < α) : 0 < α := hα - -/-- Denominator α+β > 0 when both α,β ≥ 0 and α > 0. -/ -theorem denom_pos (α β : Nat) (hα : 0 < α) : 0 < α + β := Nat.lt_of_lt_of_le hα (Nat.le_add_right α β) - ------------------------------------------------------------------------- --- Section 2: The beta update ------------------------------------------------------------------------- - -/-- Parameters for the Bayesian update. -/ -structure BayesParams where - α : Nat -- alpha_posterior = alpha_prior + successes - β : Nat -- beta_posterior = beta_prior + failures - hα : 0 < α -- α > 0 - hβ : 0 < β -- β > 0 - -namespace BayesParams - -/-- Denominator α + β. -/ -def denom (p : BayesParams) : Nat := p.α + p.β - -/-- Denominator is positive. -/ -theorem denom_pos (p : BayesParams) : 0 < p.denom := - Nat.lt_of_lt_of_le p.hα (Nat.le_add_right p.α p.β) - ------------------------------------------------------------------------- --- Section 3: Posterior is in (0, 1) --- --- We prove this via the cross-multiplication inequality: --- 0 < α/(α+β) < 1 iff 0 < α and α < α+β ------------------------------------------------------------------------- - -/-- H7 — PROPERTY 1: α/(α+β) is strictly less than 1. - Cross-multiplication: α < α + β iff 0 < β. -/ -theorem posterior_lt_one (p : BayesParams) : p.α < p.denom := - Nat.lt_add_of_pos_right p.hβ - -/-- H7 — PROPERTY 2: α/(α+β) is strictly greater than 0. - (α > 0 by construction.) -/ -theorem posterior_pos (p : BayesParams) : 0 < p.α := p.hα - ------------------------------------------------------------------------- --- Section 4: Monotonicity theorems --- --- We prove via cross-multiplication: --- α/(α+β) ≤ (α+1)/(α+1+β) --- iff α * (α+1+β) ≤ (α+1) * (α+β) --- iff α²+αβ+α ≤ α²+αβ+α+β --- iff 0 ≤ β ✓ ------------------------------------------------------------------------- - -/-- H7 — PROPERTY 3: Adding a success (α+1) weakly increases the ratio. - Cross-multiplication proof: α*(α+1+β) ≤ (α+1)*(α+β). - Key identity: (α+1)*(α+β) = α*(α+β) + (α+β) and α*(α+1+β) = α*(α+β) + α. - Since α ≤ α+β, the claim follows. -/ -theorem more_successes_raises (p : BayesParams) : - p.α * (p.α + 1 + p.β) ≤ (p.α + 1) * (p.α + p.β) := by - -- Step 1: α*(α+1+β) = α*(α+β) + α - have hs1 : p.α * (p.α + 1 + p.β) = p.α * (p.α + p.β) + p.α := by - have : p.α + 1 + p.β = (p.α + p.β) + 1 := by omega - rw [this, Nat.mul_add, Nat.mul_one] - -- Step 2: (α+1)*(α+β) = α*(α+β) + (α+β) - have hs2 : (p.α + 1) * (p.α + p.β) = p.α * (p.α + p.β) + (p.α + p.β) := by - rw [Nat.add_mul, Nat.one_mul] - rw [hs1, hs2] - -- Goal: α*(α+β) + α ≤ α*(α+β) + (α+β) - exact Nat.add_le_add_left (Nat.le_add_right p.α p.β) _ - -/-- H7 — PROPERTY 4: Adding a failure (β+1) weakly decreases the ratio. - α*(α+β) ≤ α*(α+β+1) since α+β ≤ α+β+1. -/ -theorem more_failures_lowers (p : BayesParams) : - p.α * (p.α + p.β) ≤ p.α * (p.α + p.β + 1) := - Nat.mul_le_mul_left p.α (Nat.le_add_right _ 1) - ------------------------------------------------------------------------- --- Section 5: Zero observations returns prior --- --- With no observations: α_post = α_prior, β_post = β_prior. --- So the ratio α_post/(α_post+β_post) = α_prior/(α_prior+β_prior) = prior. --- This is a definitional equality — represented by Refl below. ------------------------------------------------------------------------- - -/-- Represent the prior as a fraction. -/ -structure Prior where - α_p : Nat -- prior alpha (e.g., prior_confidence * 10) - β_p : Nat -- prior beta (e.g., (1 - prior_confidence) * 10) - hα : 0 < α_p - hβ : 0 < β_p - -/-- Construct a BayesParams with zero successes and zero failures. -/ -def fromPrior (p : Prior) : BayesParams where - α := p.α_p - β := p.β_p - hα := p.hα - hβ := p.hβ - -/-- H7 — PROPERTY 5: Zero observations — posterior alpha = prior alpha. -/ -theorem zero_obs_alpha (p : Prior) : - (fromPrior p).α = p.α_p := rfl - -/-- H7 — PROPERTY 6: Zero observations — posterior beta = prior beta. -/ -theorem zero_obs_beta (p : Prior) : - (fromPrior p).β = p.β_p := rfl - -/-- H7 — PROPERTY 7: Zero observations — denominator unchanged. -/ -theorem zero_obs_denom (p : Prior) : - (fromPrior p).denom = p.α_p + p.β_p := rfl - ------------------------------------------------------------------------- --- Section 6: Floor and cap (10% and 99%) --- --- The production clamp is: max(0.10, min(0.99, posterior)). --- We represent: --- floor = 1/10 (10%) ↔ cross-mult: α/(α+β) ≥ 1/10 iff 10α ≥ α+β iff 9α ≥ β --- cap = 99/100 (99%) ↔ cross-mult: α/(α+β) ≤ 99/100 iff 100α ≤ 99(α+β) iff α ≤ 99β --- --- After clamping with max and min, the result is definitionally in [floor, cap]. ------------------------------------------------------------------------- - -/-- H7 — PROPERTY 8: The clamped result is ≥ floor (1/10). - Proof: max(1/10, x) ≥ 1/10 by definition of max. -/ -theorem clamp_ge_floor (raw : Nat) : max 1 raw ≥ 1 := Nat.le_max_left 1 raw - -/-- H7 — PROPERTY 9: The clamped result is ≤ cap (99/100). - Proof: min(99, x) ≤ 99 by definition of min. -/ -theorem clamp_le_cap (raw : Nat) : min raw 99 ≤ 99 := Nat.min_le_right raw 99 - ------------------------------------------------------------------------- --- Section 7: Composite validity theorem --- --- The Bayesian update is valid if: --- 1. α_post > 0 (posterior numerator positive) --- 2. β_post > 0 (posterior denominator positive → ratio < 1) --- 3. Adding successes doesn't decrease the ratio (monotonicity) --- 4. Adding failures doesn't increase the ratio (monotonicity) --- All four hold constructively by the theorems above. ------------------------------------------------------------------------- - -/-- H7 — MAIN THEOREM: Bayesian update soundness. - A BayesParams with α,β > 0 satisfies all validity conditions. -/ -theorem bayesian_update_sound (p : BayesParams) : - 0 < p.α -- numerator positive - ∧ p.α < p.denom -- fraction < 1 - ∧ p.α * (p.α + 1 + p.β) ≤ (p.α + 1) * (p.α + p.β) -- more successes ↑ - ∧ p.α * (p.α + p.β) ≤ p.α * (p.α + p.β + 1) := -- more failures ↓ - ⟨p.posterior_pos, - p.posterior_lt_one, - more_successes_raises p, - more_failures_lowers p⟩ - -end BayesParams diff --git a/verification/proofs/lean4/ESNSpectralScaling.lean b/verification/proofs/lean4/ESNSpectralScaling.lean deleted file mode 100644 index ff65c34d..00000000 --- a/verification/proofs/lean4/ESNSpectralScaling.lean +++ /dev/null @@ -1,148 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ESNSpectralScaling.lean — Structural preconditions for ESN echo-state --- stability, proven over ℕ. --- --- PROOFS-GAP.md: Neural Property 2 — ESN spectral-radius stability. --- --- Context: `lib/neural/echo_state_network.ex` scales the reservoir --- matrix so its induced infinity-norm (the largest absolute row sum) is --- a configured `@reservoir_norm` (default 0.95): --- --- max_row_sum = matrix |> map(row -> sum(map(row, abs))) |> max(1.0) --- scale = @reservoir_norm / max(max_row_sum, 0.001) --- scaled = Enum.map(matrix, fn row -> Enum.map(row, &(&1 * scale)) end) --- --- That scaling is the runtime enforcement of the echo-state property. --- With ‖R‖∞ < 1, leak rate a and tanh (1-Lipschitz), the update --- `x ↦ (1 - a)·x + a·tanh(R·x + w·u)` is a contraction in the sup norm --- with modulus `1 - a + a·‖R‖∞`, so the state trajectory forgets its --- initial state exponentially. (Until 2026-10 the runtime scaled the --- largest single entry instead, which does not bound ‖R‖∞: the 80-node --- reservoir had a spectral radius near 2 and the property failed.) The --- analytical half of that statement needs Mathlib — out of scope for --- the Mathlib-free proof set (see the header note in --- BayesianUpdate.lean). --- --- What this file proves, over ℕ, is that the **scaling operation is --- well-defined**: the floor-guarded `max(max_row_sum, floor)` --- denominator is strictly positive whenever the floor is, which is the --- load-bearing precondition for avoiding divide-by-zero in the --- runtime. The Mathlib follow-up is tracked in --- docs/proofs/HANDOVER-neural-convergence.adoc. - ------------------------------------------------------------------------- --- Section 1: The model --- --- Reservoir entries are ℕ (scaled integer magnitudes; negatives and --- rationals would require Mathlib). The norm is the max over rows of --- each row's sum of entry magnitudes. Scaling is integer division by --- the ratio (norm / target). ------------------------------------------------------------------------- - -/-- Matrix as a list of rows. -/ -def Matrix := List (List Nat) - -/-- Each row's sum of entry magnitudes. Mirrors - `Enum.map(row, &abs/1) |> Enum.sum()` in Elixir. -/ -def rowSums (m : Matrix) : List Nat := m.map List.sum - -/-- Pointwise max of a list of ℕ with a provided floor for the empty - case. Mirrors `Enum.max(fn -> 1.0 end)` in Elixir. -/ -def maxAbsOr (xs : List Nat) (floor : Nat) : Nat := - xs.foldl (fun acc x => if x > acc then x else acc) floor - -/-- Induced infinity-norm (largest row sum) of a matrix, with a floor. -/ -def matrixMaxAbs (m : Matrix) (floor : Nat) : Nat := - maxAbsOr (rowSums m) floor - -/-- Scaling ratio of target to the norm under a positive floor. - Models `scale = reservoir_norm / max(max_row_sum, 0.001)` in Elixir. -/ -def scaleRatio (target maxAbs floor : Nat) : Nat := - target / (max maxAbs floor) - ------------------------------------------------------------------------- --- Section 2: Empty-matrix base cases ------------------------------------------------------------------------- - -/-- ESN — PROPERTY 1: An empty matrix has no row sums. -/ -theorem rowSums_nil : rowSums [] = [] := rfl - -/-- ESN — PROPERTY 2: `maxAbsOr` on an empty list returns the floor. -/ -theorem maxAbsOr_nil (floor : Nat) : maxAbsOr [] floor = floor := rfl - -/-- ESN — PROPERTY 3: An empty matrix has norm equal to its floor. -/ -theorem matrixMaxAbs_nil (floor : Nat) : matrixMaxAbs [] floor = floor := rfl - ------------------------------------------------------------------------- --- Section 3: Non-negativity — ℕ-trivial but load-bearing downstream ------------------------------------------------------------------------- - -/-- ESN — PROPERTY 4: The norm is non-negative for any matrix. -/ -theorem matrixMaxAbs_nonneg (m : Matrix) (floor : Nat) : - 0 ≤ matrixMaxAbs m floor := Nat.zero_le _ - -/-- ESN — PROPERTY 5: The scaling ratio itself is non-negative. -/ -theorem scaleRatio_nonneg (target maxAbs floor : Nat) : - 0 ≤ scaleRatio target maxAbs floor := Nat.zero_le _ - ------------------------------------------------------------------------- --- Section 4: The denominator is strictly positive --- --- The runtime uses `max(max_row_sum, 0.001)` precisely to keep the --- denominator above zero. In ℕ land the positive floor is any --- non-zero constant. This is the load-bearing precondition: without --- it the scaling operation would divide by zero at runtime. ------------------------------------------------------------------------- - -/-- ESN — PROPERTY 6: When the floor is strictly positive, so is the - floor-clamped max. This guarantees the scaling ratio's denominator - is non-zero. -/ -theorem denom_pos_when_floor_pos (maxAbs floor : Nat) (hf : 0 < floor) : - 0 < max maxAbs floor := - Nat.lt_of_lt_of_le hf (Nat.le_max_right maxAbs floor) - -/-- ESN — PROPERTY 7: If the raw `maxAbs` happens to be positive, the - clamped denominator is at least `maxAbs`. Lets downstream proofs - reason about the ratio without relying on the floor. -/ -theorem denom_ge_maxAbs (maxAbs floor : Nat) : - maxAbs ≤ max maxAbs floor := Nat.le_max_left maxAbs floor - -/-- ESN — PROPERTY 8: The clamped denominator is at least the floor. - Symmetric to PROPERTY 7; completes the "max is an upper-bound of - both" lemma. -/ -theorem denom_ge_floor (maxAbs floor : Nat) : - floor ≤ max maxAbs floor := Nat.le_max_right maxAbs floor - ------------------------------------------------------------------------- --- Section 5: Composite soundness theorem ------------------------------------------------------------------------- - -/-- ESN — MAIN THEOREM: The scaling preconditions that - `lib/neural/echo_state_network.ex` `generate_reservoir/1` enforces - are structurally sound. - - For any reservoir matrix and any strictly-positive floor: - - 1. Max-abs is non-negative (ℕ-trivial). - 2. The floor-clamped denominator is strictly positive, so the - scaling ratio is well-defined. - 3. The clamped denominator is bounded below by both `max_row_sum` - and `floor`. - - These are the preconditions a Mathlib-based echo-state-property - proof (trajectory boundedness + exponential forgetting) would - take as hypotheses. The analytical half is deferred until - Mathlib joins the Lean proof set — tracked as PR 5 in - PROOFS-GAP.md. -/ -theorem esn_scaling_preconditions_sound - (m : Matrix) (maxAbs floor : Nat) (hf : 0 < floor) : - (0 ≤ matrixMaxAbs m floor) ∧ - (0 < max maxAbs floor) ∧ - (maxAbs ≤ max maxAbs floor) ∧ - (floor ≤ max maxAbs floor) := - ⟨matrixMaxAbs_nonneg m floor, - denom_pos_when_floor_pos maxAbs floor hf, - denom_ge_maxAbs maxAbs floor, - denom_ge_floor maxAbs floor⟩ diff --git a/verification/proofs/lean4/PageRankInvariants.lean b/verification/proofs/lean4/PageRankInvariants.lean deleted file mode 100644 index 48c258fe..00000000 --- a/verification/proofs/lean4/PageRankInvariants.lean +++ /dev/null @@ -1,120 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- PageRankInvariants.lean — Algebraic preconditions for PageRank --- convergence, proven over ℕ. --- --- PROOFS-GAP.md: Neural Property 1 — PageRank power-iteration convergence. --- --- Context: `lib/neural/graph_of_trust.ex` (after the quality-gates --- fix) enforces: --- --- 1. Every edge weight is non-negative. --- 2. Each source's outgoing contributions are divided by its --- outgoing-weight sum — column-stochastic normalisation. --- 3. The damping factor α lies in [0, 1]. --- --- A full analytical convergence theorem (Banach contraction --- mapping on ℝⁿ with α < 1) requires real analysis, which pulls in --- Mathlib — out of scope for the Mathlib-free proof set (see the --- header note in BayesianUpdate.lean). --- --- What this file proves, over a ℕ model, are the structural --- invariants the Elixir runtime now upholds and an analytical --- proof would take as hypotheses: --- --- • Edge weights are non-negative. --- • Outgoing-weight sums are non-negative. --- • For a graph with no edges, every outgoing-weight sum is 0. --- --- The Mathlib-backed follow-up is tracked as PR 4 in PROOFS-GAP.md. - ------------------------------------------------------------------------- --- Section 1: The model --- --- Scores and weights are ℕ with a shared scale. Weights on edges are --- absolute integer counts; normalisation is handled by dividing by --- the source's outgoing-weight sum. This sidesteps rational --- arithmetic entirely while still capturing the load-bearing --- properties. ------------------------------------------------------------------------- - -/-- A weighted directed edge. -/ -structure Edge where - src : Nat - tgt : Nat - weight : Nat - deriving Repr, DecidableEq - -/-- Sum of outgoing edge weights from a given source. -/ -def outWeightSum (edges : List Edge) (src : Nat) : Nat := - (edges.filter (fun e => e.src = src)).foldl (fun acc e => acc + e.weight) 0 - -/-- Total incoming weight into a given target. -/ -def inWeightSum (edges : List Edge) (tgt : Nat) : Nat := - (edges.filter (fun e => e.tgt = tgt)).foldl (fun acc e => acc + e.weight) 0 - ------------------------------------------------------------------------- --- Section 2: Non-negativity --- --- ℕ has no negative values, so these are definitional. Stating them --- here pins the preconditions the Elixir fix (`build_edges/1`) now --- maintains. ------------------------------------------------------------------------- - -/-- PAGERANK — PROPERTY 1: Edge weights are non-negative. -/ -theorem edge_weight_nonneg (e : Edge) : 0 ≤ e.weight := Nat.zero_le _ - -/-- PAGERANK — PROPERTY 2: The outgoing-weight sum is non-negative - for every source, regardless of graph shape. -/ -theorem outWeightSum_nonneg (edges : List Edge) (src : Nat) : - 0 ≤ outWeightSum edges src := Nat.zero_le _ - -/-- PAGERANK — PROPERTY 3: The incoming-weight sum is non-negative - for every target. -/ -theorem inWeightSum_nonneg (edges : List Edge) (tgt : Nat) : - 0 ≤ inWeightSum edges tgt := Nat.zero_le _ - ------------------------------------------------------------------------- --- Section 3: Empty-graph base cases --- --- An empty graph has zero outgoing and incoming weight at every --- node. The Elixir runtime uses this to short-circuit the iteration --- — a node with no outgoing edges contributes only through the --- teleport term `(1 - α) / n`. ------------------------------------------------------------------------- - -/-- PAGERANK — PROPERTY 4: An empty edge list has zero outgoing - weight at every source. -/ -theorem outWeightSum_nil (src : Nat) : - outWeightSum [] src = 0 := rfl - -/-- PAGERANK — PROPERTY 5: An empty edge list has zero incoming - weight at every target. -/ -theorem inWeightSum_nil (tgt : Nat) : - inWeightSum [] tgt = 0 := rfl - ------------------------------------------------------------------------- --- Section 4: Composite soundness theorem ------------------------------------------------------------------------- - -/-- PAGERANK — MAIN THEOREM: The PageRank iteration-step - preconditions enforced by `build_edges/1` in - `lib/neural/graph_of_trust.ex` are structurally sound. - - For any graph: - 1. Every edge weight is non-negative (ℕ-typed). - 2. Every outgoing-weight sum is non-negative. - 3. Every incoming-weight sum is non-negative. - - These are the load-bearing preconditions for Banach-style - convergence. The analytical half (contraction + unique fixed - point) is deferred until Mathlib joins the Lean proof set. -/ -theorem pagerank_preconditions_sound - (edges : List Edge) (e : Edge) (tgt : Nat) : - (0 ≤ e.weight) ∧ - (0 ≤ outWeightSum edges e.src) ∧ - (0 ≤ inWeightSum edges tgt) := - ⟨edge_weight_nonneg e, - outWeightSum_nonneg edges e.src, - inWeightSum_nonneg edges tgt⟩ diff --git a/verification/proofs/lean4/ParserTotality.lean b/verification/proofs/lean4/ParserTotality.lean deleted file mode 100644 index 3bef09c7..00000000 --- a/verification/proofs/lean4/ParserTotality.lean +++ /dev/null @@ -1,191 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ParserTotality.lean — Parser totality for the VCL `FROM` clause. --- --- REQUIREMENTS-MASTER.md / PROOFS-GAP.md: VCL parser totality | L3 | P1 --- --- Hypatia's VCL query parser lives in `lib/vcl/client.ex` and dispatches on --- pattern match against a token list. Clauses like: --- --- defp parse_from(["FROM", "STORE", store_id | rest]) do ... --- defp parse_from(["FROM", "FEDERATION", pattern | rest]) do ... --- defp parse_from(_), do: {:error, ...} --- --- The catch-all returns `{:error, _}` so the function is total in the --- sense that every token stream produces a result — either a parsed --- source tuple or an error. --- --- This file formalises a representative subset of that dispatch, --- shows it is total (Lean's default — the elaborator refuses --- non-terminating functions without `partial`), and then establishes --- a few concrete round-trip properties against well-formed inputs. --- No external dependencies (no Mathlib required). --- --- The model omits unquoted-URL, WITH-DRIFT, and multi-URL cases; the --- pattern is identical and the shape of the proof scales linearly. - ------------------------------------------------------------------------- --- Section 1: Token / Source datatypes ------------------------------------------------------------------------- - -/-- Tokens produced by `Hypatia.VCL.Client.tokenize/1`. Quoted strings - are distinguished so the parser's two code paths (bare identifier - vs. quoted literal) can be modelled separately. -/ -inductive Token where - | kwFrom - | kwStore - | kwFederation - | kwHexad - | ident (s : String) - | quoted (s : String) - | other (s : String) - deriving Repr, DecidableEq - -/-- Parsed source tuple, mirroring what `parse_from/1` emits in Elixir: - - {:store, store_id} - {:federation, pattern, drift_policy} - {:hexad, uuid} - - `DriftPolicy` is left abstract here (always `none` in the subset - we model). -/ -inductive Source where - | store (id : String) - | federation (pattern : String) - | hexad (uuid : String) - deriving Repr, DecidableEq - -/-- Parser errors. The Elixir side returns a string; we keep it - structured for the proofs. -/ -inductive ParseError where - | expectedFromClause - | emptyInput - | malformed - deriving Repr, DecidableEq - -/-- A parse result either succeeds (with remaining tokens) or fails. -/ -inductive ParseResult (α : Type) where - | ok (value : α) (rest : List Token) - | err (e : ParseError) - deriving Repr - ------------------------------------------------------------------------- --- Section 2: The `parse_from` subset --- --- Mirrors lib/vcl/client.ex `parse_from/1` for the three canonical --- source shapes. Lean refuses non-total functions without `partial`, --- so the very fact that this `def` elaborates is the totality proof. ------------------------------------------------------------------------- - -/-- Parse a FROM clause. Total over every input by construction - (Lean would reject a partial definition without the keyword). -/ -def parseFrom : List Token → ParseResult Source - | Token.kwFrom :: Token.kwStore :: Token.ident id :: rest => - .ok (.store id) rest - | Token.kwFrom :: Token.kwStore :: Token.quoted id :: rest => - .ok (.store id) rest - | Token.kwFrom :: Token.kwFederation :: Token.ident pat :: rest => - .ok (.federation pat) rest - | Token.kwFrom :: Token.kwFederation :: Token.quoted pat :: rest => - .ok (.federation pat) rest - | Token.kwFrom :: Token.kwHexad :: Token.ident u :: rest => - .ok (.hexad u) rest - | [] => .err .emptyInput - | _ => .err .expectedFromClause - ------------------------------------------------------------------------- --- Section 3: Totality as a structural property --- --- Totality is definitionally true — `parseFrom` is a `def`, not a --- `partial def`, so Lean's termination checker has already approved --- it. The theorems below pin concrete reference-transparency and --- base-case properties without leaving tactic safety. ------------------------------------------------------------------------- - -/-- VCL PARSER — PROPERTY 1: `parseFrom` is deterministic. - Pattern matching is confluent; the same input always produces the - same output. -/ -theorem parseFrom_deterministic (ts : List Token) : - parseFrom ts = parseFrom ts := rfl - -/-- VCL PARSER — PROPERTY 2: Empty input produces the canonical - error, never a spurious success. -/ -theorem parseFrom_empty : parseFrom [] = .err .emptyInput := rfl - ------------------------------------------------------------------------- --- Section 4: Round-trip correctness against well-formed inputs --- --- These are end-to-end assertions that the three happy-path clauses --- produce the expected source tuples. If the parser's dispatch order --- were ever reshuffled such that (say) `FROM STORE ident` matched --- the `hexad` clause first, these theorems would fail to type-check. ------------------------------------------------------------------------- - -/-- VCL PARSER — PROPERTY 4: `FROM STORE ` produces `:store`. -/ -theorem parseFrom_store_bare : - parseFrom [Token.kwFrom, Token.kwStore, Token.ident "scans"] - = .ok (.store "scans") [] := rfl - -/-- VCL PARSER — PROPERTY 5: `FROM STORE "quoted"` produces `:store`. -/ -theorem parseFrom_store_quoted : - parseFrom [Token.kwFrom, Token.kwStore, Token.quoted "scans"] - = .ok (.store "scans") [] := rfl - -/-- VCL PARSER — PROPERTY 6: `FROM FEDERATION ` produces - `:federation` with the pattern preserved. -/ -theorem parseFrom_federation : - parseFrom [Token.kwFrom, Token.kwFederation, Token.ident "/scans/*"] - = .ok (.federation "/scans/*") [] := rfl - -/-- VCL PARSER — PROPERTY 7: `FROM HEXAD ` produces `:hexad`. -/ -theorem parseFrom_hexad : - parseFrom [Token.kwFrom, Token.kwHexad, Token.ident "abc-123"] - = .ok (.hexad "abc-123") [] := rfl - -/-- VCL PARSER — PROPERTY 8: Tokens after a valid FROM clause are - passed through as remainder. The downstream WHERE / LIMIT / OFFSET - parsers consume them; dropping the remainder would silently lose - clauses. -/ -theorem parseFrom_passes_remainder : - parseFrom [Token.kwFrom, Token.kwStore, Token.ident "scans", - Token.other "WHERE", Token.other "FIELD"] - = .ok (.store "scans") [Token.other "WHERE", Token.other "FIELD"] := rfl - ------------------------------------------------------------------------- --- Section 5: Malformed-input rejection ------------------------------------------------------------------------- - -/-- VCL PARSER — PROPERTY 9: A FROM token with no following STORE / - FEDERATION / HEXAD keyword is rejected, never silently matched. -/ -theorem parseFrom_orphan_from : - parseFrom [Token.kwFrom] = .err .expectedFromClause := rfl - -/-- VCL PARSER — PROPERTY 10: A bare identifier list without FROM is - rejected. Guards against the token pipeline accidentally skipping - the FROM keyword. -/ -theorem parseFrom_no_from_keyword : - parseFrom [Token.kwStore, Token.ident "scans"] - = .err .expectedFromClause := rfl - ------------------------------------------------------------------------- --- Section 6: A convenience helper ------------------------------------------------------------------------- - -/-- Test whether a parse succeeded. Usable in downstream theorems - that need a Bool-valued predicate. -/ -def parseFrom_succeeded (ts : List Token) : Bool := - match parseFrom ts with - | .ok _ _ => true - | .err _ => false - -/-- VCL PARSER — PROPERTY 11: The `parseFrom_succeeded` predicate - agrees with the `parseFrom` dispatch for the canonical STORE - clause. -/ -theorem parseFrom_succeeded_store : - parseFrom_succeeded [Token.kwFrom, Token.kwStore, Token.ident "scans"] = true := rfl - -/-- VCL PARSER — PROPERTY 12: The `parseFrom_succeeded` predicate - is false on malformed input. -/ -theorem parseFrom_succeeded_empty : - parseFrom_succeeded [] = false := rfl diff --git a/verification/proofs/lean4/RateLimiting.lean b/verification/proofs/lean4/RateLimiting.lean deleted file mode 100644 index fae3ab2d..00000000 --- a/verification/proofs/lean4/RateLimiting.lean +++ /dev/null @@ -1,223 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- RateLimiting.lean — Formal proof that sliding window rate limiter --- never exceeds configured bounds. --- --- Models the Hypatia rate limiter (lib/safety/rate_limiter.ex) which --- enforces: --- - Per-bot limit: 50 dispatches per 60-second window --- - Global limit: 200 dispatches per 60-second window --- - Burst limit: 10 dispatches per 5-second window --- --- The proof shows that the counter can never exceed the configured --- maximum, regardless of the arrival pattern. --- --- Corresponds to: --- - lib/safety/rate_limiter.ex (RateLimiter GenServer) - ------------------------------------------------------------------------- --- Section 1: Window-based counter model ------------------------------------------------------------------------- - -/-- A rate limiter configuration: maximum allowed events in a window. -/ -structure RateLimitConfig where - maxEvents : Nat - windowSize : Nat - windowPositive : windowSize > 0 - -/-- A timestamped event. -/ -structure Event where - timestamp : Nat - -/-- The state of a rate limiter: a list of events within the current window. -/ -structure RateLimiterState where - config : RateLimitConfig - events : List Event - -/-- Count events within a time window [windowStart, now]. -/ -def countEventsInWindow (events : List Event) (windowStart : Nat) : Nat := - events.filter (fun e => e.timestamp >= windowStart) |>.length - -/-- Check whether a new event would be allowed (counter < max). -/ -def isAllowed (state : RateLimiterState) (now : Nat) : Bool := - let windowStart := now - state.config.windowSize - let currentCount := countEventsInWindow state.events windowStart - currentCount < state.config.maxEvents - -/-- Accept an event: add it to the list only if allowed. -/ -def tryAccept (state : RateLimiterState) (event : Event) : RateLimiterState × Bool := - if isAllowed state event.timestamp then - ({ state with events := event :: state.events }, true) - else - (state, false) - -/-- Prune events outside the window (garbage collection). -/ -def prune (state : RateLimiterState) (now : Nat) : RateLimiterState := - let windowStart := now - state.config.windowSize - { state with events := state.events.filter (fun e => e.timestamp >= windowStart) } - ------------------------------------------------------------------------- --- Section 2: Core invariant — counter never exceeds bound ------------------------------------------------------------------------- - -/-- The fundamental invariant: the number of events in any window - never exceeds maxEvents. -/ -def invariantHolds (state : RateLimiterState) (now : Nat) : Prop := - let windowStart := now - state.config.windowSize - countEventsInWindow state.events windowStart ≤ state.config.maxEvents - -/-- An empty rate limiter trivially satisfies the invariant. -/ -theorem empty_satisfies_invariant (config : RateLimitConfig) (now : Nat) : - invariantHolds { config := config, events := [] } now := by - simp [invariantHolds, countEventsInWindow] - -/-- Helper: List.filter never increases length. -/ -theorem filter_length_le {α : Type} (p : α → Bool) (xs : List α) : - (xs.filter p).length ≤ xs.length := by - induction xs with - | nil => simp - | cons x xs ih => - rw [List.filter_cons] - split - · exact Nat.succ_le_succ ih - · exact Nat.le_succ_of_le ih - ------------------------------------------------------------------------- --- Section 3: Proof that tryAccept preserves the invariant ------------------------------------------------------------------------- - -/-- Adding one event to the front raises the in-window count by at most 1. -/ -theorem count_cons_le (e : Event) (es : List Event) (ws : Nat) : - countEventsInWindow (e :: es) ws ≤ countEventsInWindow es ws + 1 := by - unfold countEventsInWindow - rw [List.filter_cons] - split - · rw [List.length_cons] - omega - · omega - -/-- After tryAccept, the invariant is preserved. - If the event is rejected, state is unchanged (trivially preserves). - If the event is accepted, count was < max before, so count+1 <= max. -/ -theorem tryAccept_preserves_invariant - (state : RateLimiterState) (event : Event) - (h : invariantHolds state event.timestamp) : - invariantHolds (tryAccept state event).1 event.timestamp := by - unfold tryAccept - split - · -- accepted: events become event :: state.events; event is in its own window, - -- and isAllowed gave count < maxEvents, so count + 1 ≤ maxEvents. - rename_i hAllowed - simp only [invariantHolds] at h ⊢ - simp only [isAllowed, decide_eq_true_eq] at hAllowed - have hc := count_cons_le event state.events (event.timestamp - state.config.windowSize) - omega - · -- rejected: state unchanged - exact h - ------------------------------------------------------------------------- --- Section 4: Proof that prune preserves the invariant ------------------------------------------------------------------------- - -/-- Pruning only removes events, so it can only decrease the count. -/ -theorem prune_preserves_invariant - (state : RateLimiterState) (now : Nat) - (h : invariantHolds state now) : - invariantHolds (prune state now) now := by - -- prune filters the events; counting re-filters with the same predicate, so the - -- post-prune count is ≤ the pre-prune count, which h bounds by maxEvents. - simp only [invariantHolds, countEventsInWindow, prune] at h ⊢ - exact Nat.le_trans (filter_length_le _ _) h - ------------------------------------------------------------------------- --- Section 5: Sequence of events — invariant holds inductively ------------------------------------------------------------------------- - -/-- Process a sequence of events, accepting only those that don't violate - the rate limit. Returns the final state. -/ -def processEvents (state : RateLimiterState) : List Event → RateLimiterState - | [] => state - | e :: es => - let (state', _) := tryAccept state e - processEvents state' es - -/-- The invariant holds after processing any sequence of events, - provided it held initially and all events have the same timestamp - (worst case: all events arrive simultaneously). -/ -theorem processEvents_preserves_invariant - (state : RateLimiterState) (events : List Event) (t : Nat) - (hTime : ∀ e, e ∈ events → e.timestamp = t) - (h : invariantHolds state t) : - invariantHolds (processEvents state events) t := by - -- Generalize `state`: each step processes one event from a possibly-different - -- state, so the induction hypothesis must hold for any starting state. - induction events generalizing state with - | nil => exact h - | cons e es ih => - simp only [processEvents] - apply ih (tryAccept state e).1 - · intro e' he' - exact hTime e' (List.mem_cons_of_mem e he') - · have hET : e.timestamp = t := hTime e List.mem_cons_self - have hpre : invariantHolds state e.timestamp := by rw [hET]; exact h - have hstep := tryAccept_preserves_invariant state e hpre - rwa [hET] at hstep - ------------------------------------------------------------------------- --- Section 6: Concrete configurations ------------------------------------------------------------------------- - -/-- Per-bot rate limit: 50 events per 60s window. -/ -def perBotConfig : RateLimitConfig := - { maxEvents := 50, windowSize := 60, windowPositive := by omega } - -/-- Global rate limit: 200 events per 60s window. -/ -def globalConfig : RateLimitConfig := - { maxEvents := 200, windowSize := 60, windowPositive := by omega } - -/-- Burst rate limit: 10 events per 5s window. -/ -def burstConfig : RateLimitConfig := - { maxEvents := 10, windowSize := 5, windowPositive := by omega } - -/-- Per-bot limiter starts in a valid state. -/ -theorem perBot_initial_valid (now : Nat) : - invariantHolds { config := perBotConfig, events := [] } now := - empty_satisfies_invariant perBotConfig now - -/-- Global limiter starts in a valid state. -/ -theorem global_initial_valid (now : Nat) : - invariantHolds { config := globalConfig, events := [] } now := - empty_satisfies_invariant globalConfig now - -/-- Burst limiter starts in a valid state. -/ -theorem burst_initial_valid (now : Nat) : - invariantHolds { config := burstConfig, events := [] } now := - empty_satisfies_invariant burstConfig now - ------------------------------------------------------------------------- --- Section 7: Rejection guarantee ------------------------------------------------------------------------- - -/-- When the counter equals maxEvents, the next event is always rejected. -/ -theorem at_limit_rejects - (state : RateLimiterState) (event : Event) - (hFull : countEventsInWindow state.events - (event.timestamp - state.config.windowSize) - = state.config.maxEvents) : - (tryAccept state event).2 = false := by - simp [tryAccept, isAllowed] - rw [hFull] - simp [Nat.lt_irrefl] - -/-- The count after any sequence of simultaneous tryAccept calls is bounded. - All events must share the same timestamp (worst-case burst scenario). -/ -theorem count_bounded_after_accepts - (config : RateLimitConfig) (events : List Event) (t : Nat) - (hTime : ∀ e, e ∈ events → e.timestamp = t) : - let finalState := processEvents { config := config, events := [] } events - invariantHolds finalState t := - processEvents_preserves_invariant - { config := config, events := [] } - events t hTime - (empty_satisfies_invariant config t) diff --git a/verification/proofs/lean4/lakefile.lean b/verification/proofs/lean4/lakefile.lean deleted file mode 100644 index 3b0ac34d..00000000 --- a/verification/proofs/lean4/lakefile.lean +++ /dev/null @@ -1,12 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 -import Lake -open Lake DSL - -package hypatia_proofs - --- @[default_target] so a bare `lake build` actually compiles (and thus --- type-checks) the proof library. Without it, `lake build` reports success --- having built 0 targets — the verify-proofs.yml gate would pass vacuously. -@[default_target] -lean_lib HypatiaProofs where - roots := #[`BayesianUpdate, `RateLimiting, `ParserTotality, `PageRankInvariants, `ESNSpectralScaling] diff --git a/verification/proofs/lean4/lean-toolchain b/verification/proofs/lean4/lean-toolchain deleted file mode 100644 index af9e5d33..00000000 --- a/verification/proofs/lean4/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.30.0