feat(proofs): Agda formal verification of the numeric core (issue #1)

.github/workflows/proofs.yml

@@ -0,0 +1,122 @@
+# SPDX-License-Identifier: AGPL-3.0-only
+name: Proofs
+
+# The formal-verification gate for issue #1.
+#
+# Design rules, all of which are here because the alternative is a gate that lies:
+#
+#   * An absent prover is a FAILURE, never a skip.  `proofs/bootstrap.sh` exits
+#     non-zero if it cannot install Agda.  There is no `if: always()` escape and
+#     no `continue-on-error`.
+#   * The self-test runs on every push.  A gate that has never been observed to
+#     reject anything is not evidence, so `proofs/tests/gate-selftest.sh` breaks
+#     the proofs on purpose in nine ways and requires each to be rejected.
+#   * The axiom audit runs as its own step, so a failure says which check failed
+#     rather than "the proofs job failed".
+#   * The type-check output is uploaded as an artifact whether it passed or not,
+#     because "it passed" and "it printed warnings nobody read" look identical in
+#     a green tick.
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: proofs-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  agda:
+    name: Agda proofs (2.7.0.1 / stdlib 2ffa8b7d)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Cache the vendored toolchain
+        uses: actions/cache@v4
+        with:
+          path: |
+            proofs/.vendor
+            ~/.config/agda
+          key: agda-2.7.0.1-stdlib-2ffa8b7d-${{ hashFiles('proofs/agda/**/*.agda', 'proofs/agda/*.agda-lib') }}
+          restore-keys: agda-2.7.0.1-stdlib-2ffa8b7d-
+
+      - name: Bootstrap the prover
+        run: proofs/bootstrap.sh --bootstrap
+
+      - name: Axiom audit (postulates, FFI, unsound flags, holes, reachability)
+        run: proofs/tests/axiom-audit.sh
+
+      - name: Type-check every proof module
+        run: |
+          set -o pipefail
+          proofs/bootstrap.sh --check 2>&1 | tee proofs-typecheck.log
+          # A clean run prints nothing but the harness lines.  Any Agda warning
+          # is treated as a failure here rather than being left in the log.
+          if grep -qE '^(warning|Warning)' proofs-typecheck.log; then
+            echo "::error::Agda emitted warnings"
+            grep -nE '^(warning|Warning)' proofs-typecheck.log
+            exit 1
+          fi
+
+      - name: Gate self-test (nine deliberate breakages must be rejected)
+        run: proofs/tests/gate-selftest.sh
+
+      - name: Upload the type-check transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: agda-typecheck-transcript
+          path: proofs-typecheck.log
+          if-no-files-found: error
+
+  # The proof status document is a claim about the tree.  This job checks the
+  # claims that are mechanically checkable, so PROOF-STATUS.md cannot drift away
+  # from what the modules actually contain.
+  status-consistency:
+    name: PROOF-STATUS.md matches the tree
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Every module is listed, and every listed module exists
+        run: |
+          set -euo pipefail
+          fail=0
+          # Every .agda module under proofs/agda/MetaManifold must appear in the
+          # status document, and every `MetaManifold.X` named in the document
+          # must exist on disk.
+          for f in proofs/agda/MetaManifold/*.agda; do
+            mod="$(basename "$f" .agda)"
+            if ! grep -q "MetaManifold.$mod" proofs/PROOF-STATUS.md; then
+              echo "::error::PROOF-STATUS.md does not mention MetaManifold.$mod"
+              fail=1
+            fi
+          done
+          for named in $(grep -oE 'MetaManifold\.[A-Za-z]+' proofs/PROOF-STATUS.md | sort -u); do
+            path="proofs/agda/${named//./\/}.agda"
+            if [[ ! -f "$path" ]]; then
+              echo "::error::PROOF-STATUS.md names $named but $path does not exist"
+              fail=1
+            fi
+          done
+          # Residue files referenced by the document must exist.
+          for r in $(grep -oE '[a-z-]+\.residue' proofs/PROOF-STATUS.md | sort -u); do
+            if [[ ! -f "proofs/residue/$r" ]]; then
+              echo "::error::PROOF-STATUS.md references proofs/residue/$r, which is missing"
+              fail=1
+            fi
+          done
+          exit $fail

.gitignore

@@ -372,7 +372,8 @@ archive/
 !docs/migration/
 !docs/migration/**
 
-### Agda ###
-# Interface files (regenerated by scripts/check-proofs.sh)
+# Agda interface cache — build output, regenerated by `proofs/bootstrap.sh`.
 proofs/agda/_build/
-*.agdai
+
+# Agda libraries file generated by proofs/bootstrap.sh
+proofs/.agda-libraries

Justfile

@@ -596,3 +596,41 @@ reanchor:
 # Re-anchor but STOP at every conflict for hands-on resolution.
 reanchor-manual:
     @{{REANCHOR}} run --policy manual --keep
+
+# ----------------------------------------------------------------------- #
+# Formal verification — Agda proofs for the validated statistics layer
+#
+# Issue #1 requires the numeric core to be validated, not merely tested.  These
+# recipes wrap `proofs/bootstrap.sh`, which pins Agda 2.7.0.1 and agda-stdlib
+# 3.0 and refuses to pass when the prover is missing.  `just proofs` is the whole
+# gate: install if needed, audit for escape hatches, type-check every module.
+# See proofs/PROOF-STATUS.md for what is proved and proofs/residue/ for what is
+# explicitly not.
+# ----------------------------------------------------------------------- #
+
+# Bootstrap the pinned Agda toolchain into proofs/.vendor (no checking).
+proofs-bootstrap:
+    @proofs/bootstrap.sh --bootstrap
+
+# The whole proof gate: axiom audit + type-check of MetaManifold.All.
+proofs:
+    @proofs/bootstrap.sh
+
+# Type-check only; fails loudly if the toolchain has not been bootstrapped.
+proofs-check:
+    @proofs/bootstrap.sh --check
+
+# Audit for postulates, FFI, unsound flags, holes, and unreachable modules.
+proofs-audit:
+    @proofs/tests/axiom-audit.sh
+
+# Prove the gate can fail: nine deliberate breakages, each must be rejected.
+# A gate whose self-test is skipped is a gate nobody can trust, so `just ci`
+# runs this too.
+proofs-selftest:
+    @proofs/tests/gate-selftest.sh
+
+# Remove the vendored toolchain (proofs/.vendor) and Agda's interface cache.
+proofs-clean:
+    @rm -rf proofs/.vendor proofs/agda/_build proofs/agda/MetaManifold/*.agdai
+    @echo "proofs: cleaned"

docs/statistics/formal-verification.md

@@ -0,0 +1,131 @@
+# Formal verification of the validated statistics layer
+
+Status: **the Agda gate is green**. See [`proofs/PROOF-STATUS.md`](../../proofs/PROOF-STATUS.md)
+for the full inventory and [`proofs/residue/`](../../proofs/residue/) for what is
+explicitly *not* proved.
+
+This page is for a reviewer who needs to know what "validated with a proof
+assistant" does and does not mean for issue #1, without reading Agda.
+
+## The one-line version
+
+Seven modules, 77 top-level definitions, type-checked by Agda 2.7.0.1 with
+agda-stdlib (pinned by SHA — see the caveat below) under `--safe --without-K`: no
+postulates, no foreign code, no proof-irrelevance escape hatch, no universe-level
+cheating. A separate audit script enforces those four facts on every build, and a
+self-test script proves the audit and the type-checker can actually fail.
+
+One caveat that changes what "verified" means here, stated up front rather than
+in a footnote: the stdlib pin is `2ffa8b7d`, which is on the development line
+towards agda-stdlib 3.0. **No `v3.0` tag exists** — the newest is `v2.4` — and
+these proofs do not compile against `v2.4` or against the `v2.1` estate pin on
+`main`. Reproducible, but not portable. `proofs/residue/toolchain.residue` lists
+the exact APIs that have to change to port it.
+
+## Why a proof assistant at all
+
+Issue #1 asks for a numeric layer that never silently produces a plausible wrong
+number. Tests sample the input space; they cannot cover it. Three of the claims
+this layer makes are exactly the kind that survive every test anybody thinks to
+write and fail in production:
+
+1. **"An exact proportion of an empty sample is refused, not zero."** A test can
+   check `c = 0, t = 0`. It cannot check that no future refactor turns the
+   refusal into a default. In the model, the refusal is one arm of a sum type and
+   `outcome-total` says there is no third arm — an edit that forgets a case does
+   not type-check.
+
+2. **"A count sum that overflows is refused, not wrapped."** `checkedAdd-is-exact`
+   and `checkedAdd-refuses-exactly-when-it-must` are a two-sided statement: a
+   returned value *is* the true sum, and a refusal happens *exactly* when the sum
+   leaves the range. Proving one direction alone would be worthless, because each
+   direction alone is satisfied by an implementation that is useless.
+
+3. **"A permutation p-value cannot be zero."** `never-reports-zero` holds for
+   *every* `b` and `B`. No rounding rule, display layer or downstream filter has
+   to be trusted, because the estimator cannot reach zero. The negative control
+   is proved alongside it: `naive-estimator-can-report-zero` shows the estimator
+   this one replaces really does return exactly zero. A proof that a hazard was
+   avoided is only evidence if the hazard is shown to be real.
+
+## The design decision that made this tractable
+
+`ℚᵘ` — Agda's unnormalised rationals — stores its denominator as
+`suc denominator-1`. **A zero denominator is therefore unrepresentable by type.**
+
+Consequences that fall out rather than being proved:
+
+- `whole-is-one : ∀ n → mkℚᵘ (+[1+ n ]) n ≃ 1ℚᵘ` needs **no** `n ≢ 0` hypothesis.
+- `value-has-nonzero-denominator` is a statement about a value that could not
+  have been constructed otherwise.
+- The refusal for division by zero is not a checked branch that could be
+  reordered by a refactor; it is an impossibility in the representation.
+
+This is the exact sense in which the refusals are total, and it is why Agda was
+used rather than the Lean fallback the brief permitted.
+
+## What a finding looked like
+
+`relativeAbundance (suc c) 0` refuses as **`countExceedsTotal`**, not
+`zeroTotal`. That is not a modelling choice: `exact_relative_abundance` checks
+`count <= total` *before* `iszero(total)`, so a non-zero count against a zero
+total reports the count error first. Both orders are defensible; only one is
+implemented. `zero-total-with-count-is-refused-as-exceeding` records which, and a
+test written from the docstring would have asserted the other.
+
+## The bridge to Julia
+
+A proof about a model proves nothing about an implementation unless something
+ties them together. The tie is
+[`test/fixtures/agda-known-answers.json`](../../test/fixtures/agda-known-answers.json):
+values the proof assistant has *checked against a definition*, each annotated
+with the lemma that fixes it. The Julia conformance testset must reproduce them
+exactly. If the two disagree, the Julia layer is wrong.
+
+The rounding vectors are the clearest case. "Correctly rounded to *s* decimals"
+is specified as a predicate over integers alone — no division, so no rounding
+inside the specification of rounding — and each printed decimal is then a
+type-checked instance of it. `0.67` for `2/3` at two decimals is not a number
+somebody typed into two places.
+
+The same file records the tie-handling contract: at an exact half,
+`IsRounding` goes down (`1/2` at 0 dp is `0`) and `IsRoundHalfUp` goes up
+(`1/2` at 0 dp is `1`). The two agree everywhere else, which is itself proved, so
+the tie direction is the *only* thing the contract decision can change.
+
+## What this does not prove
+
+Stated here because the alternative is a reader inferring it from the presence of
+a `proofs/` directory:
+
+- **No probability theory.** Nothing about coverage, bias, type I error or FDR
+  control. Those are simulation-study questions with pre-set tolerances, and they
+  live in the Julia validation layer.
+- **No IEEE-754.** Every theorem is over exact rationals. No claim of the form
+  "Float64 gives the same answer" is made anywhere.
+- **No proof that `numeric_policy.jl` implements the model.** The bridge is the
+  fixture file and the conformance testset — a test, not a proof.
+- **Nothing about the `:ordinary` path.** Unchanged existing behaviour is a
+  regression property over the existing suite.
+- **`q_i ≥ p_i` is false** in general and is deliberately absent.
+
+Each of these has an entry in `proofs/residue/` with an id, a precise statement,
+and what would close it.
+
+## Running it
+
+```sh
+just proofs          # bootstrap if needed, audit, type-check everything
+just proofs-audit    # escape-hatch audit only
+just proofs-selftest # prove the gate rejects broken proofs (nine breakages)
+just proofs-clean    # remove the vendored toolchain and interface cache
+```
+
+`proofs/bootstrap.sh` pins Agda `2.7.0.1` and agda-stdlib at `2ffa8b7d`, and
+exits non-zero if it cannot install them. **An absent prover is a failure, never
+a skip**, in CI and locally alike. CI runs the audit, the type-check, the
+self-test, and a consistency check that `PROOF-STATUS.md` matches the tree, and
+uploads the type-check transcript as an artifact whether it passed or not.
+
+Verified from an empty `proofs/.vendor`, so the numbers above are the bootstrap
+script installing its own toolchain, not a pre-existing one being reused.