Skip to content

Commit 01eee40

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
W1-7: Type-checking Agda proofs + agda --safe CI + honest catalogue (#42)
## What & why `.github/workflows/agda.yml` (added on this branch) type-checks every module under `proofs/` with `agda --safe`. Its **Configure agda-stdlib library** step could never succeed on `ubuntu-latest`: the apt `agda-stdlib` package (Agda 2.6.3 / stdlib 1.7.3) ships the library sources but **no `standard-library.agda-lib` file** anywhere on the filesystem, so the discovery grep ``` dpkg -L agda-stdlib | grep -E '/standard-library\.agda-lib$' ``` returned empty, tripping the step's own guard (`exit 1`) before any proof was checked. The job therefore failed at "Configure agda-stdlib library" and the "Type-check every module" step never ran. ### Fix — `.github/workflows/agda.yml` (only the library-config step changed) - When no packaged `.agda-lib` exists, detect the stdlib source root from the package contents (the directory that contains `Data/Nat/Base.agda`) and synthesise the library file (`name: standard-library` / `include: .`). - `chmod -R a+rwX` that tree so Agda can write its `.agdai` interface build cache as the non-root runner user (the first type-check refreshes interfaces). - A distro that *does* ship a `.agda-lib` still uses it — the original discovery grep is kept as the preferred branch. No `.agda` source changes were required: the three proof modules already type-check under `--safe`. ## Verification - **Local** (dev container, Agda 2.6.4.3 + stdlib 2.1): `agda --safe` passes on every `proofs/**/*.agda`: - `Statistikles/TropicalSemiring.agda` — OK - `Statistikles/RankIdentities.agda` — OK - `Statistikles/Inequalities.agda` — OK - **CI**: opening this PR against `main` fires `agda.yml`'s `pull_request` trigger (base `main`; `paths` match `proofs/**` and `.github/workflows/agda.yml`), so the **Agda Proofs** check runs on the branch for the first time. The `push` trigger is scoped to `[main, master, develop]` by design, which is why it had never executed on the feature branch before. ## Scope / skipped - Requirement (d) — extending the governance grep to reject `postulate` under `proofs/` — was already handled on this branch in `.github/workflows/e2e.yml`. - Requirements (a) type-checking fixes and (b) honest README relabel + ℕ-scope disclaimer were delivered in the branch's first commit; this commit only fixes the CI library-configuration bug flagged in review. - Out of scope per the work order: proofs over ℝ, new theorems, the Julia↔Agda correspondence. Addresses the reviewer must-fix items for branch `fix/agda-proofs-ci`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 29d2f9c commit 01eee40

5 files changed

Lines changed: 219 additions & 38 deletions

File tree

‎.github/workflows/agda.yml‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# agda.yml — Type-check the EXPERIMENTAL Agda proofs under proofs/.
5+
#
6+
# Every proofs/**/*.agda module must pass `agda --safe` (no weakening of --safe),
7+
# no module may go unchecked (a new .agda file that is not registered fails the
8+
# job), and no `postulate` is permitted (the proofs are constructive).
9+
name: Agda Proofs
10+
11+
on:
12+
push:
13+
branches: [main, master, develop]
14+
paths:
15+
- 'proofs/**'
16+
- '.github/workflows/agda.yml'
17+
pull_request:
18+
branches: [main, master]
19+
paths:
20+
- 'proofs/**'
21+
- '.github/workflows/agda.yml'
22+
workflow_dispatch:
23+
24+
permissions:
25+
contents: read
26+
27+
concurrency:
28+
group: agda-${{ github.ref }}
29+
cancel-in-progress: true
30+
31+
jobs:
32+
agda-safe:
33+
name: agda --safe (proofs/)
34+
runs-on: ubuntu-latest
35+
timeout-minutes: 30
36+
37+
steps:
38+
- name: Checkout
39+
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
40+
41+
- name: Install Agda + agda-stdlib (apt)
42+
run: |
43+
sudo apt-get update
44+
sudo apt-get install -y --no-install-recommends agda agda-stdlib
45+
agda --version
46+
47+
- name: Configure agda-stdlib library
48+
run: |
49+
set -euo pipefail
50+
# Some distributions ship a standard-library.agda-lib inside the package;
51+
# prefer it when one is present.
52+
LIB="$(dpkg -L agda-stdlib | grep -E '/standard-library\.agda-lib$' | head -1 || true)"
53+
if [ -z "${LIB:-}" ]; then
54+
# The Debian/Ubuntu agda-stdlib package (apt, ubuntu-latest) ships the
55+
# library sources but NO .agda-lib file anywhere on the filesystem, so
56+
# synthesise one against the installed source root (the directory that
57+
# directly contains Data/, Relation/, ...). Detect that root from the
58+
# package contents rather than hard-coding a path.
59+
SRC="$(dpkg -L agda-stdlib | grep -E '/Data/Nat/Base\.agda$' | head -1 || true)"
60+
if [ -z "${SRC:-}" ]; then
61+
echo "::error::agda-stdlib is installed but neither a packaged .agda-lib nor Data/Nat/Base.agda was found; cannot configure the standard library"
62+
dpkg -L agda-stdlib | sed -n '1,40p'
63+
exit 1
64+
fi
65+
ROOT="${SRC%/Data/Nat/Base.agda}"
66+
LIB="$ROOT/standard-library.agda-lib"
67+
echo "No packaged .agda-lib; synthesising $LIB (source root: $ROOT)"
68+
printf 'name: standard-library\ninclude: .\n' | sudo tee "$LIB" >/dev/null
69+
fi
70+
echo "Using stdlib library file: $LIB"
71+
# Agda writes .agdai interface files next to the sources; the package tree
72+
# is root-owned, so make it writable for the (non-root) runner user before
73+
# the first type-check refreshes the interface build cache.
74+
sudo chmod -R a+rwX "$(dirname "$LIB")"
75+
mkdir -p "$HOME/.agda"
76+
echo "$LIB" > "$HOME/.agda/libraries"
77+
echo "standard-library" > "$HOME/.agda/defaults"
78+
79+
- name: Reject postulates in proofs/
80+
run: |
81+
if grep -rnw --include='*.agda' 'postulate' proofs/; then
82+
echo "::error::proofs/ must contain no 'postulate' — the experimental proofs are constructive"
83+
exit 1
84+
fi
85+
echo "PASS: no postulates under proofs/"
86+
87+
- name: Type-check every module (agda --safe) + guard unchecked files
88+
run: |
89+
set -euo pipefail
90+
# Explicit registry of modules that MUST be type-checked. Adding a new
91+
# proofs/**/*.agda file WITHOUT registering it here fails this job.
92+
EXPECTED_SORTED="$(printf '%s\n' \
93+
'Statistikles/Inequalities.agda' \
94+
'Statistikles/RankIdentities.agda' \
95+
'Statistikles/TropicalSemiring.agda' | sort)"
96+
FOUND_SORTED="$(cd proofs && find . -name '*.agda' -type f | sed 's|^\./||' | sort)"
97+
if [ "$EXPECTED_SORTED" != "$FOUND_SORTED" ]; then
98+
echo "::error::proofs/ module set does not match the registry in agda.yml."
99+
echo "--- registered in workflow ---"; printf '%s\n' "$EXPECTED_SORTED"
100+
echo "--- found under proofs/ ------"; printf '%s\n' "$FOUND_SORTED"
101+
echo "Register any new module in the EXPECTED_SORTED list in .github/workflows/agda.yml."
102+
exit 1
103+
fi
104+
cd proofs
105+
rc=0
106+
while IFS= read -r mod; do
107+
[ -z "$mod" ] && continue
108+
echo "== agda --safe $mod =="
109+
if ! agda --safe "$mod"; then
110+
echo "::error file=proofs/$mod::agda --safe failed for $mod"
111+
rc=1
112+
fi
113+
done <<< "$FOUND_SORTED"
114+
if [ "$rc" -eq 0 ]; then echo "PASS: all proof modules type-check under --safe"; fi
115+
exit $rc

‎.github/workflows/e2e.yml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,13 @@ jobs:
9898
echo "$DANGEROUS"
9999
exit 1
100100
fi
101+
# Experimental Agda proofs must stay constructive — no postulates.
102+
PROOF_POSTULATES=$(grep -rnw --include='*.agda' 'postulate' proofs/ 2>/dev/null || true)
103+
if [ -n "$PROOF_POSTULATES" ]; then
104+
echo "FAIL: postulate found under proofs/"
105+
echo "$PROOF_POSTULATES"
106+
exit 1
107+
fi
101108
echo "PASS: No dangerous patterns"
102109
103110
- name: SPDX headers

‎proofs/README.adoc‎

Lines changed: 89 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2,39 +2,108 @@
22
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
= Statistikles Formal Proofs (Agda)
44

5-
Constructive proofs of core statistical identities used by Statistikles.
6-
Verified by Agda's dependent type checker — no postulates, no holes.
5+
*Status: EXPERIMENTAL.* These modules type-check under `agda --safe` with no
6+
postulates and no holes — but they are *not yet* proofs of the statistical
7+
theorems Statistikles relies on. Every lemma below is stated and proven over
8+
the natural numbers (`ℕ`). The runtime computes over `Float64` (IEEE-754
9+
doubles), so each entry is a *discrete proxy for* — not a proof of — the
10+
statistical target in the right-hand column.
11+
12+
[IMPORTANT]
13+
====
14+
*Scope: current proofs quantify over `ℕ`, not `Float64`.* None of them quantify
15+
over `ℝ` or over the IEEE-754 `Float64` the runtime actually uses. The gap
16+
between the ℕ lemma proven here and the ℝ/`Float64` statement the statistic
17+
needs is real and is tracked below as "target (pending)". Read "Proven (ℕ)" as
18+
"this discrete lemma type-checks", *not* as "the statistic is verified".
19+
Restating these over the reals is deferred future work (production-readiness
20+
reframe W2-4); it is deliberately *not* attempted here.
21+
====
722

823
== Proof Catalogue
924

10-
[cols="1,2,2,1"]
25+
Each row gives the *exact* lemma the Agda source proves (its type signature),
26+
the module it lives in, and the statistical result it is intended to
27+
approximate. The middle column is *proven over ℕ*; the right-hand target is
28+
*pending*.
29+
30+
[cols="1,5,2,4",options="header"]
1131
|===
12-
| # | Identity | File | Status
13-
14-
| 1 | Tropical addition associative | TropicalSemiring.agda | Proven
15-
| 2 | Tropical addition commutative | TropicalSemiring.agda | Proven
16-
| 3 | Tropical distributivity | TropicalSemiring.agda | Proven
17-
| 4 | Tropical idempotence | TropicalSemiring.agda | Proven
18-
| 5 | Tropical multiplicative identity | TropicalSemiring.agda | Proven
19-
| 6 | Chi-square df identity | RankIdentities.agda | Proven
20-
| 7 | Rank sum (concrete to n=100) | RankIdentities.agda | Proven
21-
| 8 | Bonferroni (elem ≤ sum) | Inequalities.agda | Proven
22-
| 9 | Tie correction bound (sq-mono) | Inequalities.agda | Proven
23-
| 10 | Mean ordering transitivity | Inequalities.agda | Proven
32+
| # | Lemma actually proven (over `ℕ`) | File | Statistical target (pending)
33+
34+
| 1
35+
| `min-assoc : ∀ a b c → min a (min b c) ≡ min (min a b) c` — `min` on `ℕ` is associative
36+
| TropicalSemiring.agda
37+
| Associativity of tropical addition `⊕ = min` on `ℝ ∪ {+∞}`
38+
39+
| 2
40+
| `min-comm : ∀ a b → min a b ≡ min b a` — `min` on `ℕ` is commutative
41+
| TropicalSemiring.agda
42+
| Commutativity of tropical `⊕ = min` on `ℝ ∪ {+∞}`
43+
44+
| 3
45+
| `+-distrib-min : ∀ a b c → a + min b c ≡ min (a + b) (a + c)` — `+` distributes over `min` on `ℕ`
46+
| TropicalSemiring.agda
47+
| Tropical `⊗ = +` distributes over `⊕ = min` on `ℝ ∪ {+∞}`
48+
49+
| 4
50+
| `min-idem : ∀ a → min a a ≡ a` — `min` on `ℕ` is idempotent
51+
| TropicalSemiring.agda
52+
| Idempotence of tropical `⊕` on `ℝ ∪ {+∞}`
53+
54+
| 5
55+
| `tropical-mul-identity : ∀ a → zero + a ≡ a` — `0` is the left identity of `+` on `ℕ` (definitional)
56+
| TropicalSemiring.agda
57+
| `0` is the tropical `⊗`-identity (and `+∞` the `⊕`-identity) on `ℝ ∪ {+∞}`
58+
59+
| 6
60+
| `df-identity : ∀ k → suc k ∸ 1 ≡ k` and `df-nonneg : ∀ k → zero ≤ k` — truncated subtraction on `ℕ`
61+
| RankIdentities.agda
62+
| χ² degrees of freedom `= (categories − 1)` is well-defined and non-negative
63+
64+
| 7
65+
| `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 `ℕ`
66+
| RankIdentities.agda
67+
| Rank/midrank sum identity `Σᵢ₌₁ⁿ i = n(n+1)/2` over `ℝ` (tie handling)
68+
69+
| 8
70+
| `elem-le-sum : ∀ x xs → x ≤ x + list-sum xs` — a list element is `≤` the list sum, on `ℕ`
71+
| Inequalities.agda
72+
| Bonferroni inequality `P(⋃ Aᵢ) ≤ Σ P(Aᵢ)` over `ℝ`
73+
74+
| 9
75+
| `sq-mono : a ≤ b → a * a ≤ b * b` — squaring is monotone on `ℕ`
76+
| Inequalities.agda
77+
| Monotonicity of the tie-correction term `Σ(tᵢ³ − tᵢ)` in `N` over `ℝ`
78+
79+
| 10
80+
| `mean-ordering-transitive : a ≤ b → b ≤ c → a ≤ c` — transitivity of `≤` on `ℕ`
81+
| Inequalities.agda
82+
| Transitivity of the power-mean ordering `M_p ≤ M_q ≤ M_r ⇒ M_p ≤ M_r` over `ℝ`
2483
|===
2584

85+
All ten lemmas are `Proven (ℕ)`; all ten statistical targets remain `pending`.
86+
2687
== Building
2788

28-
Requires Agda 2.6.4+ and agda-stdlib.
89+
Requires Agda 2.6.4+ and agda-stdlib 2.x (library `statistikles-proofs.agda-lib`
90+
depends on `standard-library`). Every module must type-check under `--safe`
91+
(no weakening):
2992

3093
```bash
3194
agda --safe Statistikles/TropicalSemiring.agda
3295
agda --safe Statistikles/RankIdentities.agda
3396
agda --safe Statistikles/Inequalities.agda
3497
```
3598

36-
== Integration with ECHIDNA
99+
CI runs exactly this on every `proofs/**/*.agda` module — see
100+
`.github/workflows/agda.yml`. That workflow also fails if a new `.agda` file is
101+
added under `proofs/` without being type-checked, and rejects any `postulate`.
102+
103+
== Integration with ECHIDNA (aspirational)
37104

38-
These proofs correspond to the `StatProofObligation` entries in
39-
`src/bridge/echidna_adapter.jl`. ECHIDNA dispatches verification
40-
requests to Agda for constructive proofs and Z3 for arithmetic.
105+
The intended design is for these proofs to back the `StatProofObligation`
106+
entries in `src/bridge/echidna_adapter.jl`, with ECHIDNA dispatching
107+
constructive obligations to Agda and arithmetic obligations to Z3. That wiring
108+
is *not yet in place*, and the correspondence between these `ℕ` lemmas and the
109+
runtime's `Float64` statistics is future work — intentionally out of scope here.

‎proofs/Statistikles/Inequalities.agda‎

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
module Statistikles.Inequalities where
88

99
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s)
10-
open import Data.Nat.Properties using (+-mono-≤; m≤m+n; +-comm)
10+
open import Data.Nat.Properties using (m≤m+n; m≤n+m)
1111
open import Data.List using (List; []; _∷_; foldr; map; length)
1212
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
1313

@@ -33,14 +33,7 @@ elem-le-sum x xs = m≤m+n x (list-sum xs)
3333

3434
-- Sum is monotone under cons: list-sum xs ≤ list-sum (y ∷ xs)
3535
sum-mono-cons : ∀ (y : ℕ) (xs : List ℕ) → list-sum xs ≤ y + list-sum xs
36-
sum-mono-cons y xs = m≤m+n y (list-sum xs) |> flip-le
37-
where
38-
flip-le : y ≤ y + list-sum xs → list-sum xs ≤ y + list-sum xs
39-
flip-le _ = subst-le (+-comm (list-sum xs) y)
40-
where
41-
open import Relation.Binary.PropositionalEquality using (subst)
42-
subst-le : list-sum xs + y ≡ y + list-sum xs → list-sum xs ≤ y + list-sum xs
43-
subst-le eq = subst (list-sum xs ≤_) eq (m≤m+n (list-sum xs) y)
36+
sum-mono-cons y xs = m≤n+m (list-sum xs) y
4437

4538
-- ═══════════════════════════════════════════════════════════════════════
4639
-- PROOF 9: Tie correction is bounded

‎proofs/Statistikles/RankIdentities.agda‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
module Statistikles.RankIdentities where
88

99
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s; _∸_)
10+
open import Data.Nat.Properties using (+-mono-≤)
1011
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
1112

1213
-- ═══════════════════════════════════════════════════════════════════════
@@ -66,13 +67,9 @@ _ = refl
6667
-- Rank sum is monotone: n ≤ m → sum-to n ≤ sum-to m
6768
-- ═══════════════════════════════════════════════════════════════════════
6869

70+
-- sum-to (suc n) = suc n + sum-to n, so monotonicity of _+_ on both the
71+
-- successor term (suc n ≤ suc m) and the recursive tail (sum-to n ≤ sum-to m)
72+
-- gives the step directly.
6973
sum-to-mono : ∀ {n m} → n ≤ m → sum-to n ≤ sum-to m
70-
sum-to-mono z≤n = z≤n
71-
sum-to-mono {suc n} {suc m} (s≤s n≤m) = helper n m n≤m
72-
where
73-
-- We need: suc n + sum-to n ≤ suc m + sum-to m
74-
-- This follows from n ≤ m and induction, but the full proof
75-
-- requires +-mono which is complex. State as a consequence.
76-
helper : ∀ n m → n ≤ m → suc n + sum-to n ≤ suc m + sum-to m
77-
helper zero m z≤n = s≤s z≤n
78-
helper (suc n) (suc m) (s≤s p) = s≤s (helper n m p)
74+
sum-to-mono z≤n = z≤n
75+
sum-to-mono (s≤s n≤m) = +-mono-≤ (s≤s n≤m) (sum-to-mono n≤m)

0 commit comments

Comments
 (0)