diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml new file mode 100644 index 0000000..6cd841e --- /dev/null +++ b/.github/workflows/agda.yml @@ -0,0 +1,115 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# agda.yml — Type-check the EXPERIMENTAL Agda proofs under proofs/. +# +# Every proofs/**/*.agda module must pass `agda --safe` (no weakening of --safe), +# no module may go unchecked (a new .agda file that is not registered fails the +# job), and no `postulate` is permitted (the proofs are constructive). +name: Agda Proofs + +on: + push: + branches: [main, master, develop] + paths: + - 'proofs/**' + - '.github/workflows/agda.yml' + pull_request: + branches: [main, master] + paths: + - 'proofs/**' + - '.github/workflows/agda.yml' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: agda-${{ github.ref }} + cancel-in-progress: true + +jobs: + agda-safe: + name: agda --safe (proofs/) + runs-on: ubuntu-latest + timeout-minutes: 30 + + steps: + - name: Checkout + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + + - name: Install Agda + agda-stdlib (apt) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends agda agda-stdlib + agda --version + + - name: Configure agda-stdlib library + run: | + set -euo pipefail + # Some distributions ship a standard-library.agda-lib inside the package; + # prefer it when one is present. + LIB="$(dpkg -L agda-stdlib | grep -E '/standard-library\.agda-lib$' | head -1 || true)" + if [ -z "${LIB:-}" ]; then + # The Debian/Ubuntu agda-stdlib package (apt, ubuntu-latest) ships the + # library sources but NO .agda-lib file anywhere on the filesystem, so + # synthesise one against the installed source root (the directory that + # directly contains Data/, Relation/, ...). Detect that root from the + # package contents rather than hard-coding a path. + SRC="$(dpkg -L agda-stdlib | grep -E '/Data/Nat/Base\.agda$' | head -1 || true)" + if [ -z "${SRC:-}" ]; then + echo "::error::agda-stdlib is installed but neither a packaged .agda-lib nor Data/Nat/Base.agda was found; cannot configure the standard library" + dpkg -L agda-stdlib | sed -n '1,40p' + exit 1 + fi + ROOT="${SRC%/Data/Nat/Base.agda}" + LIB="$ROOT/standard-library.agda-lib" + echo "No packaged .agda-lib; synthesising $LIB (source root: $ROOT)" + printf 'name: standard-library\ninclude: .\n' | sudo tee "$LIB" >/dev/null + fi + echo "Using stdlib library file: $LIB" + # Agda writes .agdai interface files next to the sources; the package tree + # is root-owned, so make it writable for the (non-root) runner user before + # the first type-check refreshes the interface build cache. + sudo chmod -R a+rwX "$(dirname "$LIB")" + mkdir -p "$HOME/.agda" + echo "$LIB" > "$HOME/.agda/libraries" + echo "standard-library" > "$HOME/.agda/defaults" + + - name: Reject postulates in proofs/ + run: | + if grep -rnw --include='*.agda' 'postulate' proofs/; then + echo "::error::proofs/ must contain no 'postulate' — the experimental proofs are constructive" + exit 1 + fi + echo "PASS: no postulates under proofs/" + + - name: Type-check every module (agda --safe) + guard unchecked files + run: | + set -euo pipefail + # Explicit registry of modules that MUST be type-checked. Adding a new + # proofs/**/*.agda file WITHOUT registering it here fails this job. + EXPECTED_SORTED="$(printf '%s\n' \ + 'Statistikles/Inequalities.agda' \ + 'Statistikles/RankIdentities.agda' \ + 'Statistikles/TropicalSemiring.agda' | sort)" + FOUND_SORTED="$(cd proofs && find . -name '*.agda' -type f | sed 's|^\./||' | sort)" + if [ "$EXPECTED_SORTED" != "$FOUND_SORTED" ]; then + echo "::error::proofs/ module set does not match the registry in agda.yml." + echo "--- registered in workflow ---"; printf '%s\n' "$EXPECTED_SORTED" + echo "--- found under proofs/ ------"; printf '%s\n' "$FOUND_SORTED" + echo "Register any new module in the EXPECTED_SORTED list in .github/workflows/agda.yml." + exit 1 + fi + cd proofs + rc=0 + while IFS= read -r mod; do + [ -z "$mod" ] && continue + echo "== agda --safe $mod ==" + if ! agda --safe "$mod"; then + echo "::error file=proofs/$mod::agda --safe failed for $mod" + rc=1 + fi + done <<< "$FOUND_SORTED" + if [ "$rc" -eq 0 ]; then echo "PASS: all proof modules type-check under --safe"; fi + exit $rc diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index 8a49649..e0b2ff5 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -98,6 +98,13 @@ jobs: echo "$DANGEROUS" exit 1 fi + # Experimental Agda proofs must stay constructive — no postulates. + PROOF_POSTULATES=$(grep -rnw --include='*.agda' 'postulate' proofs/ 2>/dev/null || true) + if [ -n "$PROOF_POSTULATES" ]; then + echo "FAIL: postulate found under proofs/" + echo "$PROOF_POSTULATES" + exit 1 + fi echo "PASS: No dangerous patterns" - name: SPDX headers diff --git a/proofs/README.adoc b/proofs/README.adoc index 653aca8..bd3f9b1 100644 --- a/proofs/README.adoc +++ b/proofs/README.adoc @@ -2,30 +2,93 @@ // Copyright (c) Jonathan D.A. Jewell = Statistikles Formal Proofs (Agda) -Constructive proofs of core statistical identities used by Statistikles. -Verified by Agda's dependent type checker — no postulates, no holes. +*Status: EXPERIMENTAL.* These modules type-check under `agda --safe` with no +postulates and no holes — but they are *not yet* proofs of the statistical +theorems Statistikles relies on. Every lemma below is stated and proven over +the natural numbers (`ℕ`). The runtime computes over `Float64` (IEEE-754 +doubles), so each entry is a *discrete proxy for* — not a proof of — the +statistical target in the right-hand column. + +[IMPORTANT] +==== +*Scope: current proofs quantify over `ℕ`, not `Float64`.* None of them quantify +over `ℝ` or over the IEEE-754 `Float64` the runtime actually uses. The gap +between the ℕ lemma proven here and the ℝ/`Float64` statement the statistic +needs is real and is tracked below as "target (pending)". Read "Proven (ℕ)" as +"this discrete lemma type-checks", *not* as "the statistic is verified". +Restating these over the reals is deferred future work (production-readiness +reframe W2-4); it is deliberately *not* attempted here. +==== == Proof Catalogue -[cols="1,2,2,1"] +Each row gives the *exact* lemma the Agda source proves (its type signature), +the module it lives in, and the statistical result it is intended to +approximate. The middle column is *proven over ℕ*; the right-hand target is +*pending*. + +[cols="1,5,2,4",options="header"] |=== -| # | Identity | File | Status - -| 1 | Tropical addition associative | TropicalSemiring.agda | Proven -| 2 | Tropical addition commutative | TropicalSemiring.agda | Proven -| 3 | Tropical distributivity | TropicalSemiring.agda | Proven -| 4 | Tropical idempotence | TropicalSemiring.agda | Proven -| 5 | Tropical multiplicative identity | TropicalSemiring.agda | Proven -| 6 | Chi-square df identity | RankIdentities.agda | Proven -| 7 | Rank sum (concrete to n=100) | RankIdentities.agda | Proven -| 8 | Bonferroni (elem ≤ sum) | Inequalities.agda | Proven -| 9 | Tie correction bound (sq-mono) | Inequalities.agda | Proven -| 10 | Mean ordering transitivity | Inequalities.agda | Proven +| # | Lemma actually proven (over `ℕ`) | File | Statistical target (pending) + +| 1 +| `min-assoc : ∀ a b c → min a (min b c) ≡ min (min a b) c` — `min` on `ℕ` is associative +| TropicalSemiring.agda +| Associativity of tropical addition `⊕ = min` on `ℝ ∪ {+∞}` + +| 2 +| `min-comm : ∀ a b → min a b ≡ min b a` — `min` on `ℕ` is commutative +| TropicalSemiring.agda +| Commutativity of tropical `⊕ = min` on `ℝ ∪ {+∞}` + +| 3 +| `+-distrib-min : ∀ a b c → a + min b c ≡ min (a + b) (a + c)` — `+` distributes over `min` on `ℕ` +| TropicalSemiring.agda +| Tropical `⊗ = +` distributes over `⊕ = min` on `ℝ ∪ {+∞}` + +| 4 +| `min-idem : ∀ a → min a a ≡ a` — `min` on `ℕ` is idempotent +| TropicalSemiring.agda +| Idempotence of tropical `⊕` on `ℝ ∪ {+∞}` + +| 5 +| `tropical-mul-identity : ∀ a → zero + a ≡ a` — `0` is the left identity of `+` on `ℕ` (definitional) +| TropicalSemiring.agda +| `0` is the tropical `⊗`-identity (and `+∞` the `⊕`-identity) on `ℝ ∪ {+∞}` + +| 6 +| `df-identity : ∀ k → suc k ∸ 1 ≡ k` and `df-nonneg : ∀ k → zero ≤ k` — truncated subtraction on `ℕ` +| RankIdentities.agda +| χ² degrees of freedom `= (categories − 1)` is well-defined and non-negative + +| 7 +| `sum-to` running-sum recursion with concrete checks (`sum-to 5 ≡ 15`, …, `sum-to 100 ≡ 5050`) and `sum-to-mono : n ≤ m → sum-to n ≤ sum-to m` on `ℕ` +| RankIdentities.agda +| Rank/midrank sum identity `Σᵢ₌₁ⁿ i = n(n+1)/2` over `ℝ` (tie handling) + +| 8 +| `elem-le-sum : ∀ x xs → x ≤ x + list-sum xs` — a list element is `≤` the list sum, on `ℕ` +| Inequalities.agda +| Bonferroni inequality `P(⋃ Aᵢ) ≤ Σ P(Aᵢ)` over `ℝ` + +| 9 +| `sq-mono : a ≤ b → a * a ≤ b * b` — squaring is monotone on `ℕ` +| Inequalities.agda +| Monotonicity of the tie-correction term `Σ(tᵢ³ − tᵢ)` in `N` over `ℝ` + +| 10 +| `mean-ordering-transitive : a ≤ b → b ≤ c → a ≤ c` — transitivity of `≤` on `ℕ` +| Inequalities.agda +| Transitivity of the power-mean ordering `M_p ≤ M_q ≤ M_r ⇒ M_p ≤ M_r` over `ℝ` |=== +All ten lemmas are `Proven (ℕ)`; all ten statistical targets remain `pending`. + == Building -Requires Agda 2.6.4+ and agda-stdlib. +Requires Agda 2.6.4+ and agda-stdlib 2.x (library `statistikles-proofs.agda-lib` +depends on `standard-library`). Every module must type-check under `--safe` +(no weakening): ```bash agda --safe Statistikles/TropicalSemiring.agda @@ -33,8 +96,14 @@ agda --safe Statistikles/RankIdentities.agda agda --safe Statistikles/Inequalities.agda ``` -== Integration with ECHIDNA +CI runs exactly this on every `proofs/**/*.agda` module — see +`.github/workflows/agda.yml`. That workflow also fails if a new `.agda` file is +added under `proofs/` without being type-checked, and rejects any `postulate`. + +== Integration with ECHIDNA (aspirational) -These proofs correspond to the `StatProofObligation` entries in -`src/bridge/echidna_adapter.jl`. ECHIDNA dispatches verification -requests to Agda for constructive proofs and Z3 for arithmetic. +The intended design is for these proofs to back the `StatProofObligation` +entries in `src/bridge/echidna_adapter.jl`, with ECHIDNA dispatching +constructive obligations to Agda and arithmetic obligations to Z3. That wiring +is *not yet in place*, and the correspondence between these `ℕ` lemmas and the +runtime's `Float64` statistics is future work — intentionally out of scope here. diff --git a/proofs/Statistikles/Inequalities.agda b/proofs/Statistikles/Inequalities.agda index 2e9ded9..533db93 100644 --- a/proofs/Statistikles/Inequalities.agda +++ b/proofs/Statistikles/Inequalities.agda @@ -7,7 +7,7 @@ module Statistikles.Inequalities where open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s) -open import Data.Nat.Properties using (+-mono-≤; m≤m+n; +-comm) +open import Data.Nat.Properties using (m≤m+n; m≤n+m) open import Data.List using (List; []; _∷_; foldr; map; length) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) @@ -33,14 +33,7 @@ elem-le-sum x xs = m≤m+n x (list-sum xs) -- Sum is monotone under cons: list-sum xs ≤ list-sum (y ∷ xs) sum-mono-cons : ∀ (y : ℕ) (xs : List ℕ) → list-sum xs ≤ y + list-sum xs -sum-mono-cons y xs = m≤m+n y (list-sum xs) |> flip-le - where - flip-le : y ≤ y + list-sum xs → list-sum xs ≤ y + list-sum xs - flip-le _ = subst-le (+-comm (list-sum xs) y) - where - open import Relation.Binary.PropositionalEquality using (subst) - subst-le : list-sum xs + y ≡ y + list-sum xs → list-sum xs ≤ y + list-sum xs - subst-le eq = subst (list-sum xs ≤_) eq (m≤m+n (list-sum xs) y) +sum-mono-cons y xs = m≤n+m (list-sum xs) y -- ═══════════════════════════════════════════════════════════════════════ -- PROOF 9: Tie correction is bounded diff --git a/proofs/Statistikles/RankIdentities.agda b/proofs/Statistikles/RankIdentities.agda index 192cf8d..1b1af04 100644 --- a/proofs/Statistikles/RankIdentities.agda +++ b/proofs/Statistikles/RankIdentities.agda @@ -7,6 +7,7 @@ module Statistikles.RankIdentities where open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s; _∸_) +open import Data.Nat.Properties using (+-mono-≤) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) -- ═══════════════════════════════════════════════════════════════════════ @@ -66,13 +67,9 @@ _ = refl -- Rank sum is monotone: n ≤ m → sum-to n ≤ sum-to m -- ═══════════════════════════════════════════════════════════════════════ +-- sum-to (suc n) = suc n + sum-to n, so monotonicity of _+_ on both the +-- successor term (suc n ≤ suc m) and the recursive tail (sum-to n ≤ sum-to m) +-- gives the step directly. sum-to-mono : ∀ {n m} → n ≤ m → sum-to n ≤ sum-to m -sum-to-mono z≤n = z≤n -sum-to-mono {suc n} {suc m} (s≤s n≤m) = helper n m n≤m - where - -- We need: suc n + sum-to n ≤ suc m + sum-to m - -- This follows from n ≤ m and induction, but the full proof - -- requires +-mono which is complex. State as a consequence. - helper : ∀ n m → n ≤ m → suc n + sum-to n ≤ suc m + sum-to m - helper zero m z≤n = s≤s z≤n - helper (suc n) (suc m) (s≤s p) = s≤s (helper n m p) +sum-to-mono z≤n = z≤n +sum-to-mono (s≤s n≤m) = +-mono-≤ (s≤s n≤m) (sum-to-mono n≤m)