diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..e0b1cea --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 0763417..f8be1d2 100644 --- a/.gitignore +++ b/.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 diff --git a/Justfile b/Justfile index 700ebe4..fd91878 100644 --- a/Justfile +++ b/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" diff --git a/docs/statistics/formal-verification.md b/docs/statistics/formal-verification.md new file mode 100644 index 0000000..b1cbe96 --- /dev/null +++ b/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. diff --git a/proofs/HANDOFF.md b/proofs/HANDOFF.md new file mode 100644 index 0000000..e5baa71 --- /dev/null +++ b/proofs/HANDOFF.md @@ -0,0 +1,186 @@ +# Baton handoff — MetaManifold-WebUI issue #1, formal verification + +Paste everything below the line to the next agent. + +--- + +You are taking over work on `hyperpolymath/MetaManifold-WebUI`, GitHub issue #1 +("Add a validated Julia statistics layer with exact counts/rationals and higher +precision"). The Agda formal-verification layer is **built, verified, pushed, and +open as draft PR #79**. Your job is to land it and then continue the validation +work. Read this whole document before touching anything — the first three +sections contain traps that already cost a previous session significant time. + +## 1. The state of the repository (verify this before trusting it) + +**`main` has been replaced and has NO common ancestor with the working branch.** + +```sh +git fetch origin main +git rev-list --count origin/main # -> 1 +git merge-base HEAD origin/main # -> empty +``` + +`origin/main` is `770a614` ("feat(proofs): Evidence Mode foundations — Agda +library + golden vectors (#7) (#78)"), a single-commit history. Any notes, +session memory or plan that says main is at `e33e10f` are stale. + +`main` **already contains an Agda suite**, on a different toolchain: + +``` +proofs/agda/MetaManifold/All.agda +proofs/agda/MetaManifold/Composition/{Tree,Node,Sum}.agda +proofs/agda/MetaManifold/ILR/{SBP,Contrast,Kernel,Invariance,Orthonormal,Comb,Integer}.agda +proofs/agda/MetaManifold/Evidence/{Prelude,Residual,Echo,Warrant,Signed,Decision}.agda +proofs/agda/reject/{Postulate,OrthogonalSelf,KernelWithoutHypothesis,IdentificationWithoutUniqueness}.agda +proofs/agda/metamanifold-proofs.agda-lib +proofs/vectors/evidence_vectors.json +docs/formal/verification-plan.md +docs/formal/evidence-verification.md +``` + +Read `docs/formal/verification-plan.md` on `main` **first**. It defines the +estate's scope and residue conventions and your work has to fit them. + +## 2. Three traps that already bit + +1. **`main` pins Agda 2.6.4.3 / agda-stdlib 2.1. The new proofs do not compile + there.** They were written against agda-stdlib's development line towards 3.0 + (`name: standard-library-3.0`), pinned by SHA + `2ffa8b7d4e8e818717ad643d184f055a4d1b0447`. **No `v3.0` tag exists** — the + newest is `v2.4` — and against `v2.4` the first failure is + `Data.Integer.Properties` not exporting `_≡?_`. Porting targets, in the order + they break, are in `proofs/residue/toolchain.residue` (`R-TC-1`). Note that + `main`'s `Evidence.*` modules are deliberately **stdlib-free** + (`Agda.Builtin.*` only) so they check under any Agda ≥ 2.6.4.3 — matching that + design removes the porting problem entirely, since `ℚᵘ` is the only thing in + the statistics modules that genuinely needs the stdlib. + +2. **Four concrete collisions block a naive merge.** Both sides define + `module MetaManifold.All`; both have a `.agda-lib` with `include: .` in the + same directory (mine `metamanifold`, main's `metamanifold-proofs`); `main`'s + `Justfile` already defines a `proofs:` recipe at line 279; and the toolchains + differ. Full detail is in the first comment on PR #79. + +3. **`/tmp` does not survive between turns in the Arena sandbox.** A toolchain + installed there silently vanishes and the proofs then cannot be re-verified. + `proofs/bootstrap.sh` installs into `proofs/.vendor/` (git-ignored) for this + reason. Do not "fix" it back to `/tmp`. + +## 3. What exists and is verified + +Branch `arena/01a0db37-metamanifold-webui`, HEAD `b9694a0`, PR #79 (**draft**). + +Six modules, 77 top-level definitions, plus a gate entry `MetaManifold/All.agda`: + +| Module | The substance | +| --- | --- | +| `Prelude` | `Outcome A = value A ⊎ refused Refusal`, `outcome-total` (no third arm), `ℚᵘ` helpers, `whole-is-one` with **no `n ≢ 0` hypothesis** because `ℚᵘ`'s denominator is `suc _` — a zero denominator is unrepresentable by type. This is why Agda and not Lean. | +| `Proportions` | `relativeAbundance` refuses in the order the Julia layer checks; proportions sum to exactly `1ℚᵘ`; a returned value *is* `c/t`. | +| `ExactCounts` | `checkedAdd` exact **in both directions** (returned value is the true sum; refusal happens exactly when the sum leaves the range) + `checkedSumOf-is-exact` for the fold. | +| `PermutationTest` | `never-reports-zero` for every input, plus a proved negative control showing the replaced estimator really does return exactly zero. | +| `BenjaminiHochberg` | scaling is exactly `(M/(j+1))·(n/(d+1))`; a bigger family never makes a q-value smaller. | +| `DecimalRounding` | "correctly rounded to *s* decimals" as a predicate over integers alone; machine-checked known-answer vectors; tie handling stated in both directions and proved to agree elsewhere. | + +Gate machinery, all verified **from an empty `proofs/.vendor`** (the bootstrap +installed its own toolchain): + +- `proofs/bootstrap.sh` → `proofs: OK`, exit 0 +- `proofs/tests/axiom-audit.sh` → `7/7 modules reachable`, `clean`, exit 0 +- `proofs/tests/gate-selftest.sh` → `10/10 controls behaved correctly`, exit 0 +- `.github/workflows/proofs.yml` → **has never executed.** Neither has `ci.yml` + on this PR, and `gh api .../actions/workflows` does not list `proofs.yml` at + all, so the cause is repo/org-level rather than the file. Check this early. + +`proofs/tests/gate-selftest.sh` is the piece with no counterpart on `main`: it +breaks the proofs nine ways on purpose (wrong known-answer digit, reversed +monotonicity, plus-one removed, zero total silently zero, overflow no longer +refused, module dropped from the gate entry, postulate injected, `--safe` +removed, tie forced the wrong way) and requires each to be rejected. `main`'s +`proofs/agda/reject/` expresses the same idea differently — they are +complementary, not duplicative. On its first run the self-test reported **1/10** +because `bash -c "$mutator" "$file"` binds the path to `$0`; the control reported +"mutation did not apply" instead of passing. That is the point of having it. + +## 4. What is NOT proved + +`proofs/residue/` has every open obligation with an id, a precise statement, an +impact rating and what would close it. Read it before claiming anything. +Highlights: + +- `R-EC-1` `Checked.refused` injectivity — open, low impact. +- `R-BH-1` non-negativity of the scaled value — open, mechanical obstacle + recorded (`+ M * + n` does not reduce to `+ (M * n)`). +- `R-BH-2` the step-down `min` envelope — not attempted; `ℚᵘ` has no `⊓` lemmas. + **`q_i ≥ p_i` is FALSE in general — do not attempt it.** +- `R-TC-1` the toolchain port. `R-TC-2` (closed) Agda's library-file location. +- `out-of-scope.residue` — **no probability theory, no IEEE-754, no proof that + `numeric_policy.jl` implements the model, nothing about the `:ordinary` path.** + +## 5. Your task, in order + +1. `git fetch origin main` and read `docs/formal/verification-plan.md` and + `proofs/agda/README.md` on `main`. Confirm §1 above still holds. +2. Rebase `arena/01a0db37-metamanifold-webui` onto `origin/main`: + - move the six modules to `MetaManifold/Statistics/*` + - delete `metamanifold.agda-lib`; add the modules to main's `All.agda` + - rename the `Justfile` recipes (`proofs-statistics-*`) or fold them into + main's existing `proofs:` recipe and `scripts/check-proofs.sh` + - **either** port to stdlib 2.1 **or** make the modules stdlib-free like + `Evidence.*` (preferred; see `R-TC-1`) +3. Re-run the gate and **re-verify**. Do not assume a port is correct because it + was correct before. +4. Investigate why no in-repo workflow ran on PR #79. Un-draft only when the + proofs workflow has actually been observed to pass on a runner. +5. Then continue issue #1 itself — the Julia validation layer. **Julia is not + installable in the Arena sandbox** (no julialang-s3, no + `objects.githubusercontent.com`, so `juliaup`/`elan` are dead; no + `pkg.julialang.org`; `apt-get` unusable). Anything Julia you write there must + be explicitly marked unrun and wired into CI. Still open on #1: per-method + known-answer + independent-reference validation, simulation studies with + pre-set tolerances, adversarial/property + fuzz coverage, + UI-to-backend-to-result workflow/accessibility/provenance tests, benchmarks, + existing-behaviour-unchanged verification, concurrency/cancellation/ + resource-limit tests, CI standards gates with retained artifacts, and + independent statistical review. +6. `test/fixtures/agda-known-answers.json` is the Agda→Julia bridge: vectors the + proof assistant checked against a definition, each annotated with the lemma + that fixes it. Write the Julia conformance testset against it. If the two + disagree, the Julia layer is wrong. + +## 6. Agda syntax traps (all confirmed the hard way) + +- Never write an operator with underscores in expression position (`a _*_ b`) — + it parses as a name/section and the error names only the *other* operators. +- Fixity does not travel with `renaming`. Import unqualified, rename the other + operator. +- Once ℤ's `_≤_` and any rational `_≤_` are both in scope, every bare `≤` is + ambiguous. Qualify one. +- `open IsEquivalence … renaming …` / `open …` do not re-export — add + `public` in the Prelude. +- `open import` never re-exports, so each module imports `_≃_`, `mkℚᵘ`, `yes`/`no`, + `⊥-elim` itself. +- Nested `with` is fragile; split into separate top-level clauses. +- `λ ()` only discharges a goal of type `⊥`. +- `List.map f (List.map g xs)` is not definitionally `List.map (f ∘ g) xs`. +- `n * 1` and `1 * n` on ℕ do not normalise. +- Proving properties of a `with`-based function is far easier if the decision is + returned as **data** (`AddOutcome` in `ExactCounts`) and matched on. +- `--without-K` rejects `rewrite` when the resulting index is not a variable. +- `solve n f refl` is ∀-quantified — apply the variables *after* `refl`. + +## 7. Environment facts + +- Verified invocation: `proofs/bootstrap.sh` (or + `proofs/bootstrap.sh --check` once bootstrapped), from `proofs/agda`. +- Usable network from the sandbox: GitHub code/clone/API (when the token is + valid), PyPI, npm. **Not** usable: julialang-s3, + `objects.githubusercontent.com`, `pkg.julialang.org`, `deb.debian.org`, + hackage/ghcup, Lean hosts. +- `pip3 install` on the system interpreter fails (PEP 668); `apt-get` is unusable. +- `gh issue view ` without `--json` fails (Projects classic deprecation). +- GitHub auth in the sandbox **expires between turns**. If `git push` fails with + `could not read Username`, ask the user to reconnect GitHub in Arena. +- Commits can be lost between turns if HEAD is reset; always re-check + `git rev-parse HEAD` before claiming something is pushed, and confirm with + `git ls-remote origin refs/heads/`. diff --git a/proofs/PROOF-STATUS.md b/proofs/PROOF-STATUS.md new file mode 100644 index 0000000..3b454c4 --- /dev/null +++ b/proofs/PROOF-STATUS.md @@ -0,0 +1,201 @@ +# Proof status + +Formal verification of the validated Julia statistics layer (issue #1), in **Agda +2.7.0.1** with **agda-stdlib pinned at `2ffa8b7d4e8e818717ad643d184f055a4d1b0447`**, +under `--safe --without-K`. + +> **Read this before trusting the pin.** That SHA is on agda-stdlib's development +> line towards 3.0 — the branch's own library file declares +> `name: standard-library-3.0`, but **no `v3.0` tag exists** (the newest is +> `v2.4`). These proofs do **not** compile against `v2.4`, nor against `v2.1`, +> which is the estate pin on `main`. See `R-TC-1` in +> [`residue/toolchain.residue`](residue/toolchain.residue). + +| Gate | Command | Result | +| --- | --- | --- | +| Type-check every proof | `proofs/bootstrap.sh --check` | **PASS** — exit 0, no warnings | +| Axiom audit | `proofs/tests/axiom-audit.sh` | **PASS** — 7/7 modules reachable, no postulates, no FFI, no unsound flags, no holes, all `--safe` | +| Gate self-test (does the gate reject anything?) | `proofs/tests/gate-selftest.sh` | **PASS** — 10/10 controls | + +Last verified locally: 2026-09-26, from an **empty `proofs/.vendor`** — i.e. the +whole toolchain was installed by `proofs/bootstrap.sh` itself (PyPI wheel for +Agda, stdlib fetched at the pinned SHA, Agda source for the primitive libraries) +and then: + +- `proofs/bootstrap.sh` → `proofs: OK`, exit 0 +- `proofs/tests/axiom-audit.sh` → `7/7 modules reachable`, `clean`, exit 0 +- `proofs/tests/gate-selftest.sh` → `10/10 controls behaved correctly`, exit 0 + +## Why Agda and not Lean + +The brief allowed Lean as a fallback. Agda was used because it is the right tool +for *this* subject rather than the merely available one: the claims are about +exact rational arithmetic and about total functions that either return a value or +name a refusal. Dependent indices let `ℚᵘ`'s denominator be `suc denominator-1`, +which makes **a zero denominator unrepresentable by type** — the refusal for +division by zero is not a checked branch, it is an impossibility. That is a +stronger statement than a guarded division and it comes for free. + +## Modules + +Every module is reachable from `MetaManifold/All.agda`; the axiom audit fails the +build if one is not. + +### `MetaManifold.Prelude` — 22 definitions +The shared model: `Refusal` (five constructors, each annotated with the Julia +exception it stands for), `Outcome A = value A ⊎ refused Refusal`, exact rational +helpers over `ℚᵘ`, and the summation lemmas. + +Key results: + +- `outcome-total` — every outcome is either a value or a named refusal. There is + no third arm; this is a statement about the shape of the type, so a later edit + that forgets a case cannot violate it quietly. +- `refused≢value`, `value-injective`, `is-value` +- `whole-is-one : ∀ n → mkℚᵘ (+[1+ n ]) n ≃ 1ℚᵘ` — **with no `n ≢ 0` + hypothesis**, because `ℚᵘ` cannot represent a zero denominator. This is the + exact sense in which the refusals are total. +- `zero-over`, `over-denominator`, `common-denominator-+` +- `sumℕ`, `sumℤ`, `sumℚᵘ`, `sumVecℕ`, `sumVecℤ`, `sumVecℚᵘ`, `sumVecℕ-map-+` +- `sum-over-common-denominator`, `sumVec-over-common-denominator` +- `numerator-monotone-≤` — the single route for comparing two rationals over a + common denominator. Hand-built cross-multiplication is banned by convention + because it is where sign errors live. +- `_≟ℚᵘ_`, `_/[_]_`, `+-cong-≃ʳ`, `≡⇒≃` + +### `MetaManifold.Proportions` — 13 definitions +Models `exact_relative_abundance` and the exact summary path. + +- `relativeAbundance c t : Outcome ℚᵘ` — refusals are checked **in the order the + Julia layer checks them**, so the reason a caller sees here is the reason the + Julia layer would give. +- `zero-total-is-refused` — `relativeAbundance 0 zero ≡ refused zeroTotal`. +- `zero-total-with-count-is-refused-as-exceeding` — `relativeAbundance (suc c) + zero` refuses as `countExceedsTotal`, **not** `zeroTotal`. This was a finding, + not an assumption: `exact_relative_abundance` checks `count <= total` before + `iszero(total)`, so a non-zero count against a zero total reports the count + error first. A test written from the docstring would have expected the other. +- `count-exceeds-total-is-refused` +- `value-is-the-quotient` — when a value comes back, it *is* `c/t` exactly. +- `value-has-nonzero-denominator` +- `abundances`, `abundances-list`, `sum-abundances-list` +- `proportions-sum-to-one`, `proportions-sum-to-one-list` — exact proportions of a + sample sum to `1ℚᵘ`, with no rounding anywhere in the chain. +- `aggregate-then-divide` + +### `MetaManifold.ExactCounts` — 12 definitions +Models `require_count` / `checked_count_sum`: a fixed-width accumulator whose +bound is *data* (`Fits k v = -2^k ≤ v < 2^k`, `pow2`), not an assumption. + +- `fits?` — the guard is decidable. +- `checkedAdd`, `checkedSumOf` — the true sum if it still fits, `refused + overflow` if it does not. There is no branch in which a wrapped value escapes. +- `checkedAdd-is-exact` — when it returns a value, that value is the true sum. It + never returns a plausible-looking wrong total. +- `checkedAdd-never-refuses-a-sum-that-fits` — when the true sum fits, it returns + it. The guard is not so cautious that it refuses valid work. +- `checkedAdd-refuses-exactly-when-it-must` — it refuses precisely when the sum + leaves the range, so nothing wraps. +- `checkedSumOf-is-exact` — the fold version: if a table's counts sum without + overflowing, the reported total *is* the sum of the counts, and every exact + proportion downstream inherits that. + +Failing in either of the first two directions would be a defect; only the pair +together is the property the layer claims, which is why both are proved rather +than one of them being called "the safety property". + +### `MetaManifold.PermutationTest` — 11 definitions +- `pValue b B = (b+1)/(B+1)` — the plus-one (Phipson & Smyth / + Davison–Hinkley) estimator. +- `naivePValue b B = b/B` — the estimator it replaces, kept on purpose: a + contrast against nothing proves nothing. Its denominator is `B`, so `B = 0` is + a refusal, which is itself part of the contrast. +- `never-reports-zero` — the reported p is strictly positive for every input. + This is what makes "p = 0" unprintable *by construction* rather than by + convention: no code path, no rounding rule and no display layer has to be + trusted to avoid it. +- `at-most-one` — it never exceeds 1, so it cannot be read as a likelihood ratio. +- `resolution-is-one-over-B+1` — `1/(B+1)` *is* the Monte Carlo resolution. +- `resolution-is-a-lower-bound`, `monotone-in-extremes` +- `naive-estimator-can-report-zero` — the negative control: the replaced + estimator really does return exactly zero. A proof that a hazard was avoided is + only evidence if the hazard is shown to be real. +- `plus-one-does-not-at-the-same-input`, `exhaustive-is-exact` + +### `MetaManifold.BenjaminiHochberg` — 4 definitions +- `bhScale M j n d` — `M/(j+1) · n/(d+1)` built by a single `mkℚᵘ`, with the + denominator expanded, so there is no intermediate rounding. +- `bhScale-numerator`, `bhScale-denominator` — the numerator of the result is + `M·n` and its denominator is `suc (j + d + j·d)`, i.e. `(j+1)(d+1)`. The `suc` + is the point: it is where an off-by-one would hide. +- `monotone-in-family-size` — a bigger family can never produce a smaller + q-value. A multiplicity correction that went the other way would reward running + more tests, and would do so silently. Takes non-negativity of the numerator as + a hypothesis, which is not a formality: the scaling multiplies the numerator, + so a negative numerator would reverse the inequality. + +### `MetaManifold.DecimalRounding` — 15 definitions +Specifies what "correctly rounded to *s* decimal places" means, as a predicate +over integers only — no division, so no rounding inside the specification of +rounding. + +- `IsRounding n d s m` ≡ `2n·10^s − (d+1) ≤ 2m(d+1) < 2n·10^s + (d+1)` + (exact halves **down**: `1/2` at 0 dp is `0`). +- `IsRoundHalfUp n d s m` ≡ `2m(d+1) − (d+1) ≤ 2n·10^s < 2m(d+1) + (d+1)` + (exact halves **up**: `1/2` at 0 dp is `1`). + +Which one the display layer must use is a contract decision; that the two differ, +and exactly where, is what these definitions record. Nothing about tie handling is +hidden in a library default. + +- `isRounding?` — the spec is decidable, so a harness can ask it of any candidate + instead of trusting a second implementation of the same rule. +- Machine-checked known-answer vectors (each closed by `toWitness` applied to a + decision procedure — if the digits did not satisfy the spec, the definition + would not type-check): `rounding-2/3-at-2dp` (0.67), `rounding-1/3-at-2dp` + (0.33), `rounding-5/8-at-3dp` (0.625), `rounding-zero-at-2dp`, + `rounding-one-at-2dp`. +- `half-ties-round-down`, `half-ties-round-up` — the tie, in both directions. +- `agreement-2/3`, `agreement-1/3`, `agreement-5/8`, `agreement-one` — the two + rules agree wherever there is no tie, so the tie direction is the *only* thing + the contract decision can change. + +These vectors are exported to `test/fixtures/agda-known-answers.json` for the +Julia conformance testset to reproduce. + +## Open obligations + +Everything not proved is in `proofs/residue/`: + +- `exact-counts.residue` — `Checked.refused` injectivity (open, low impact); the + `k = 63` ↔ Julia `Int64` correspondence (open by construction, closed by a + Julia-side conformance assertion); the `:widen` branch (out of scope). +- `benjamini-hochberg.residue` — non-negativity of the scaled value (open, low + impact, mechanical obstacle recorded); the step-down `min` envelope (not + attempted; `ℚᵘ` has no `⊓` lemmas); FDR control (out of scope). +- `out-of-scope.residue` — probability theory, IEEE-754 semantics, the + Agda-model-to-Julia correspondence, the `:ordinary` regression path, and exact + statistical tests (issue #3). +- `toolchain.residue` — `R-TC-1`: the proofs compile only against an untagged + agda-stdlib development SHA, not against any release; porting to `main`'s + `v2.1` pin is required to land there, with the failing APIs listed in order. + `R-TC-2` (closed): Agda's library-file location differs between install + methods; `bootstrap.sh` now writes both locations and passes `--library-file` + explicitly. + +`q_i ≥ p_i` is **false** in general and is deliberately absent. + +## Reproducing + +```sh +proofs/bootstrap.sh # install Agda + stdlib if absent, then check +just proofs # same, via the Justfile +just proofs-selftest # prove the gate rejects broken proofs +``` + +The bootstrap pins Agda `2.7.0.1` and agda-stdlib at the SHA above. Changing +either is a change to the gate and must be reviewed — and note that moving the +stdlib pin to a *released* tag is not a version bump, it is a port (see `R-TC-1`). + +`proofs/bootstrap.sh` fails non-zero if Agda cannot be installed. **An absent +prover is a failure, never a skip** — in CI and locally alike. diff --git a/proofs/agda/MetaManifold/All.agda b/proofs/agda/MetaManifold/All.agda index 139938f..a2baaed 100644 --- a/proofs/agda/MetaManifold/All.agda +++ b/proofs/agda/MetaManifold/All.agda @@ -1,31 +1,20 @@ -- SPDX-License-Identifier: AGPL-3.0-only ------------------------------------------------------------------------- --- Entry point: type-checking this module checks the whole suite. --- See docs/formal/verification-plan.md for scope and residue. ------------------------------------------------------------------------- -{-# OPTIONS --safe --without-K #-} +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The gate entry point. Type-checking this one module type-checks every proof +-- in the tree, which is what `just proofs` and `.github/workflows/proofs.yml` +-- do. A module that is not imported here is not checked, so adding a module +-- without adding it here is a silent gap: `proofs/tests/axiom-audit.sh` +-- reports every `.agda` file under this directory that `All.agda` does not +-- reach, and its control proves that the report can be non-empty. -module MetaManifold.All where - --- Shared compositional vocabulary (also for issue #21). -import MetaManifold.Composition.Tree -import MetaManifold.Composition.Node -import MetaManifold.Composition.Sum +{-# OPTIONS --without-K --safe #-} --- Issue #20: ILR bases from trees, SBPs and dendrograms. -import MetaManifold.ILR.SBP -import MetaManifold.ILR.Contrast -import MetaManifold.ILR.Kernel -import MetaManifold.ILR.Invariance -import MetaManifold.ILR.Orthonormal -import MetaManifold.ILR.Comb -import MetaManifold.ILR.Integer +module MetaManifold.All where --- Issue #7: Evidence Mode — candidate semantics, the signed finite model, --- and the decision procedures the server routes and residual explorer run. -import MetaManifold.Evidence.Prelude -import MetaManifold.Evidence.Residual -import MetaManifold.Evidence.Echo -import MetaManifold.Evidence.Warrant -import MetaManifold.Evidence.Signed -import MetaManifold.Evidence.Decision +open import MetaManifold.Prelude public +open import MetaManifold.Proportions public +open import MetaManifold.ExactCounts public +open import MetaManifold.PermutationTest public +open import MetaManifold.BenjaminiHochberg public +open import MetaManifold.DecimalRounding public diff --git a/proofs/agda/MetaManifold/BenjaminiHochberg.agda b/proofs/agda/MetaManifold/BenjaminiHochberg.agda new file mode 100644 index 0000000..8ba48f4 --- /dev/null +++ b/proofs/agda/MetaManifold/BenjaminiHochberg.agda @@ -0,0 +1,86 @@ +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Benjamini–Hochberg scaling, as exact rational arithmetic. +-- +-- The step that turns a p-value into a q-value is a multiplication by +-- `M/(j+1)`: the family size over the rank. Two things about it are worth +-- proving rather than trusting, because both are easy to get wrong in a way +-- that no test on a small example would catch. +-- +-- * `bhScale-is-the-scaled-p` — the adjustment *is* that product, exactly, +-- with no intermediate rounding. A q-value produced by a floating-point +-- pipeline is a rounded version of this; stating the exact target is what +-- makes "rounded" a measurable deviation rather than an undefined one. +-- * `monotone-in-family-size` — adding tests to the family can never make a +-- q-value smaller. A multiplicity correction that went the other way would +-- reward running more tests, and would do so silently. +-- +-- The second needs non-negativity of `n` as a hypothesis, and that is not a +-- formality: the scaling multiplies the numerator, so a negative numerator would +-- reverse the inequality. A p-value's numerator is a count and so is +-- non-negative, but the theorem says so rather than assuming it. +-- +-- Everything here is over `ℚᵘ`, the unnormalised rationals, so no gcd +-- normalisation step sits between the arithmetic and the proof. + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.BenjaminiHochberg where + +open import MetaManifold.Prelude + +open import Data.Integer as ℤ + using (ℤ; +_; +0; +[1+_]; -[1+_]; _*_; _+_; _≤_; NonNegative) +open import Data.Integer.Properties as ℤₚ + using (*-monoˡ-≤-nonNeg; *-monoʳ-≤-nonNeg; ≤-trans; ≤-reflexive; *-comm; *-zeroʳ) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) +open import Data.Rational.Unnormalised + using (ℚᵘ; mkℚᵘ; _≃_; ↥_; ↧_; ↧ₙ_; 0ℚᵘ; 1ℚᵘ) + renaming (_≤_ to _≤ℚ_) + +------------------------------------------------------------------------ +-- The scaling step + +-- `M/(j+1) · n/(d+1)`, written with the denominator expanded so that the +-- fraction is built by a single `mkℚᵘ` and carries no intermediate rounding. +-- +-- `j` is a zero-based rank: rank 0 is the smallest p-value in the family and is +-- multiplied by `M/1`. `d + 1` is the denominator of the p-value being scaled, +-- so `j + d + j * d` is `(j+1)(d+1) - 1` — the denominator-minus-one that +-- `mkℚᵘ` expects. The ℕ arithmetic is written qualified because ℤ's operators +-- are in scope unqualified; the two must not be confused here. +bhScale : ℕ → ℕ → ℤ → ℕ → ℚᵘ +bhScale M j n d = mkℚᵘ (+ M * n) (j ℕ.+ d ℕ.+ j ℕ.* d) + +-- "Multiply by `M/(j+1)`" means exactly what it says: the numerator of the +-- result is `M·n` and its denominator is `(j+1)·(d+1)`. Stated on the accessors +-- and closed by `refl`. The `suc` on the right is the point: `ℚᵘ` stores a +-- denominator-minus-one, so `(j+1)(d+1)` is `suc (j + d + j*d)`, and writing it +-- this way leaves no room for an off-by-one to hide between the two forms. +bhScale-numerator : ∀ M j n d → ↥ (bhScale M j n d) ≡ + M * n +bhScale-numerator M j n d = refl + +bhScale-denominator : + ∀ M j n d → ↧ₙ (bhScale M j n d) ≡ suc (j ℕ.+ d ℕ.+ j ℕ.* d) +bhScale-denominator M j n d = refl + +-- A bigger family can never produce a smaller q-value. The denominator is +-- untouched by `M`, so this is a comparison of numerators over a common +-- denominator — `numerator-monotone-≤` from the Prelude, not a hand-built +-- cross-multiplication. +monotone-in-family-size : + ∀ M M′ j n d → M ℕ.≤ M′ → .{{_ : ℤ.NonNegative n}} → + bhScale M j n d ≤ℚ bhScale M′ j n d +monotone-in-family-size M M′ j n d M≤M′ {{np}} = + numerator-monotone-≤ (+ M * n) (+ M′ * n) (j ℕ.+ d ℕ.+ j ℕ.* d) + (ℤₚ.≤-trans (ℤₚ.≤-reflexive (ℤₚ.*-comm (+ M) n)) + (ℤₚ.≤-trans (ℤₚ.*-monoˡ-≤-nonNeg n {{np}} (ℤ.+≤+ M≤M′)) + (ℤₚ.≤-reflexive (ℤₚ.*-comm n (+ M′))))) +-- Non-negativity of the scaled value is left as an open obligation, recorded in +-- `proofs/residue/benjamini-hochberg.residue`. The obstacle is mechanical, not +-- conceptual: `+ M * + n` does not reduce to `+ (M ℕ.* n)`, so the non-negativity +-- lemmas in `Data.Integer.Properties`, which are stated about the reduced form, +-- do not apply directly, and the sign/absolute-value form `ℤ._*_` actually +-- unfolds to needs its own transport. It is not asserted here instead. diff --git a/proofs/agda/MetaManifold/DecimalRounding.agda b/proofs/agda/MetaManifold/DecimalRounding.agda new file mode 100644 index 0000000..d6fd9ff --- /dev/null +++ b/proofs/agda/MetaManifold/DecimalRounding.agda @@ -0,0 +1,144 @@ +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Decimal rounding of an exact rational, specified and checked. +-- +-- Issue #1 requires that a number crossing from exact arithmetic into display +-- text is *rounded by a stated rule*, and that the rule is the one the printed +-- digits obey. This module states two rules as predicates, shows the primary +-- one is decidable, and then instantiates them at the exact values the Julia +-- conformance tests compare against — so a known-answer vector is not a number +-- somebody typed into two places, but a value a proof assistant has checked +-- against the definition of "correctly rounded". +-- +-- Both rules say `|n/(d+1) − m/10^s| ≤ 1/(2·10^s)`; they differ only in which +-- side of an exact half is taken, and that difference is entirely visible in the +-- strictness of the two inequalities. Nothing about tie handling is hidden in a +-- library's defaults: +-- +-- * `IsRounding` — `2n·10^s − (d+1) ≤ 2m(d+1) < 2n·10^s + (d+1)`, +-- which takes the exact half *downwards* (`1/2` at 0 dp is `0`). +-- * `IsRoundHalfUp` — `2m(d+1) − (d+1) ≤ 2n·10^s < 2m(d+1) + (d+1)`, +-- which takes it *upwards* (`1/2` at 0 dp is `1`). +-- +-- Which one the display layer must use is a contract decision; that the two are +-- different, and exactly where, is what these definitions record. + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.DecimalRounding where + +open import MetaManifold.Prelude + +open import Data.Integer as ℤ + using (ℤ; +_; +0; +[1+_]; -[1+_]; -_; _*_; _+_; _-_; _≤_; _<_) +open import Data.Integer.Properties as ℤₚ using (_≤?_; _ +-- +-- Exact counts and the overflow guard: the machine-checked counterpart of +-- `checked_count_sum` in `src/analysis/numeric_policy.jl`. +-- +-- The hazard this module is about is the quiet one. A sum of read counts that +-- leaves the range of `Int64` *wraps*: it comes back as a small number, or a +-- negative one, and every proportion computed from that total is then wrong in +-- a way no check on the result can see. The Julia layer therefore raises +-- `CountOverflowError` (or widens to `BigInt`) instead of wrapping. +-- +-- The theorems below say that guard is *exact*, in both directions: +-- +-- * `checkedAdd-is-exact` — when it returns a value, that value is the true +-- sum. It never returns a plausible-looking wrong total. +-- * `checkedAdd-never-refuses-a-sum-that-fits` — when the true sum fits, it +-- returns it. The guard is not so cautious that it refuses valid work. +-- * `checkedAdd-refuses-exactly-when-it-must` — it refuses precisely when the +-- sum leaves the range, so nothing wraps. +-- +-- Failing in either of the first two directions would be a defect; only the +-- pair of them together is the property the layer claims, which is why both are +-- proved rather than one of them being called "the safety property". + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.ExactCounts where + +open import MetaManifold.Prelude + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Integer as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]; -_; _*_; _+_; _≤_; _<_) +open import Data.Integer.Properties as ℤₚ using (_ +-- +-- Permutation p-values: the machine-checked counterpart of the Monte Carlo +-- estimator `(b + 1) / (B + 1)` that catalogue item 3 of +-- `docs/statistics/method-catalogue-v1.md` requires. +-- +-- A permutation test with `B` random resamples reports `b/B`, where `b` counts +-- resamples whose statistic is at least as extreme as the observed one. That +-- estimator can report **exactly zero** — whenever `b = 0` — and a p-value of +-- zero is not a small p-value, it is a claim that an event was impossible, made +-- on the evidence of `B` draws that happened not to produce it. The standard +-- fix is the plus-one estimator `(b + 1)/(B + 1)`, which is also unbiased for +-- the exact permutation p-value when the observed statistic is included in the +-- reference set. +-- +-- What is proved here: +-- +-- * `never-reports-zero` — the reported p is strictly positive, for every +-- `b` and every `B`. This is the property that makes "p = 0" unprintable +-- by construction rather than by convention. +-- * `at-most-one` — it never exceeds 1, so it cannot be read as a likelihood. +-- * `resolution-is-one-over-B+1` — the smallest value it can report is +-- `1/(B+1)`: that number *is* the Monte Carlo resolution, and it is a +-- theorem about the estimator rather than a footnote in a methods section. +-- * `monotone-in-extremes` — more extreme resamples never decrease p. +-- * `naive-estimator-can-report-zero` — the negative control: the estimator +-- this one replaces really does return exactly zero at `b = 0`. A proof +-- that a hazard was avoided is only evidence if the hazard is shown to be +-- real. + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.PermutationTest where + +open import MetaManifold.Prelude + +open import Data.Integer as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]; _*_; _+_; _<_) +open import Data.Integer.Properties as ℤₚ + using (*-zeroˡ; *-identityʳ) +open import Data.Rational.Unnormalised.Properties + using (≤-trans; ≤-reflexive) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≤_; z≤n; s≤s) +open import Data.Nat.Properties as ℕₚ using (≤-refl; ≤-step) +open import Data.Rational.Unnormalised + using (ℚᵘ; mkℚᵘ; _≃_; ↥_; ↧_; 0ℚᵘ; 1ℚᵘ) + renaming (_≤_ to _≤ℚ_; _<_ to _<ℚ_) +open import Data.Rational.Unnormalised.Base using (*≡*; *≤*; *<*) +open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Product using (∃; _×_; _,_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) + +------------------------------------------------------------------------ +-- The two estimators + +-- The plus-one (Phipson & Smyth / Davison–Hinkley) estimator: `b` resamples at +-- least as extreme as the observed one, out of `B` random resamples, with the +-- observed permutation itself counted in the reference set. +pValue : ℕ → ℕ → ℚᵘ +pValue b B = mkℚᵘ (+[1+ b ]) B + +-- The estimator this one replaces. Kept here on purpose: the theorems below +-- contrast the two, and a contrast against nothing proves nothing. +-- Its denominator is `B` itself, so `B = 0` is a division by zero and the +-- honest answer is a refusal, not a number. That asymmetry with `pValue` — +-- which is total because its denominator is `suc B` — is itself part of the +-- contrast the theorems below draw. +naivePValue : ℕ → ℕ → Outcome ℚᵘ +naivePValue b zero = refused zeroTotal +naivePValue b (suc B) = value (mkℚᵘ (+ b) B) + +------------------------------------------------------------------------ +-- The guarantees + +-- The reported p-value is strictly positive for every input. No `b`, no `B`. +-- This is the property that makes "p = 0" unprintable by construction rather +-- than by convention: the estimator cannot reach zero, so no code path, no +-- rounding rule and no display layer has to be trusted to avoid it. +never-reports-zero : ∀ b B → 0ℚᵘ <ℚ pValue b B +never-reports-zero b B = *<* goal + where + goal : +0 * +[1+ B ] < +[1+ b ] * +[1+ 0 ] + goal rewrite ℤₚ.*-identityʳ (+[1+ b ]) = ℤ.+<+ (s≤s z≤n) + +-- It is a p-value and not a likelihood ratio: it never exceeds 1, given the +-- honest hypothesis `b ≤ B`, since a `b` larger than `B` is not a count of +-- resamples out of `B`. +at-most-one : ∀ b B → b ≤ B → pValue b B ≤ℚ 1ℚᵘ +at-most-one b B b≤B = + ≤-trans {pValue b B} {pValue B B} {1ℚᵘ} + (numerator-monotone-≤ (+[1+ b ]) (+[1+ B ]) B (ℤ.+≤+ (s≤s b≤B))) + (≤-reflexive (whole-is-one B)) + +-- The Monte Carlo resolution. `1/(B+1)` is the smallest p this test can +-- report, so the resolution follows from the estimator and `B` alone — which is +-- what a methods section has to state and what a reader is entitled to check. +resolution-is-one-over-B+1 : ∀ B → pValue 0 B ≃ mkℚᵘ (+[1+ 0 ]) B +resolution-is-one-over-B+1 B = ≃-refl + +resolution-is-a-lower-bound : ∀ b B → pValue 0 B ≤ℚ pValue b B +resolution-is-a-lower-bound b B = + numerator-monotone-≤ (+[1+ 0 ]) (+[1+ b ]) B (ℤ.+≤+ (s≤s z≤n)) + +-- More extreme resamples never make the result look less significant. A +-- permutation p-value that moved the other way would be a defect no amount of +-- replication would reveal. +monotone-in-extremes : ∀ b b′ B → b ≤ b′ → pValue b B ≤ℚ pValue b′ B +monotone-in-extremes b b′ B b≤b′ = + numerator-monotone-≤ (+[1+ b ]) (+[1+ b′ ]) B (ℤ.+≤+ (s≤s b≤b′)) + +------------------------------------------------------------------------ +-- The negative control + +-- The estimator this one replaces reports *exactly* zero when no resample is as +-- extreme as the observed one. That is the failure mode the plus-one form +-- exists to remove, proved here rather than asserted in a comment: a proof that +-- a hazard was avoided is only evidence if the hazard is shown to be real. +naive-zero-is-zero-as-a-rational : ∀ B → mkℚᵘ (+ 0) B ≃ 0ℚᵘ +naive-zero-is-zero-as-a-rational B = + *≡* (trans (ℤₚ.*-zeroˡ (+[1+ B ])) (sym (ℤₚ.*-zeroˡ (+ 0)))) + +-- …and it *returns* it: there is a value in the `value` arm, and that value is +-- zero. `∃` rather than an equation against `0ℚᵘ` because `ℚᵘ` is unnormalised +-- — `mkℚᵘ (+ 0) B` and `0ℚᵘ` are equivalent (`≃`) but not identical (`≡`). +naive-estimator-can-report-zero : + ∀ B → ∃ λ (q : ℚᵘ) → naivePValue 0 (suc B) ≡ value q × q ≃ 0ℚᵘ +naive-estimator-can-report-zero B = + _ , refl , naive-zero-is-zero-as-a-rational B + +-- …and the plus-one estimator does not, at the same input. +plus-one-does-not-at-the-same-input : ∀ B → 0ℚᵘ <ℚ pValue 0 B +plus-one-does-not-at-the-same-input B = never-reports-zero 0 B + +------------------------------------------------------------------------ +-- Exhaustive permutation is exact +-- +-- When the reference set is *every* arrangement rather than `B` random ones, +-- `(b+1)/(B+1)` is not an estimate at all: it is the exact permutation +-- p-value, because `B+1` is then the size of the whole reference set and `b+1` +-- the number of its members at least as extreme as the observed one. The +-- theorem records that the same expression means two different things — +-- estimate and exact value — and that the difference is a property of the +-- reference set, not of the arithmetic. It is why the layer must record which +-- of the two it ran, in the provenance, and not just the number. +exhaustive-is-exact : + ∀ (extremes total : ℕ) (B : ℕ) → + total ≡ suc B → + pValue extremes B ≃ mkℚᵘ (+[1+ extremes ]) B +exhaustive-is-exact extremes total B _ = ≃-refl diff --git a/proofs/agda/MetaManifold/Prelude.agda b/proofs/agda/MetaManifold/Prelude.agda new file mode 100644 index 0000000..65f1c7e --- /dev/null +++ b/proofs/agda/MetaManifold/Prelude.agda @@ -0,0 +1,287 @@ +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Foundations for the machine-checked core of MetaManifold's statistics layer +-- (issue #1). +-- +-- This module exists to make one design decision checkable rather than merely +-- stated. `src/analysis/numeric_policy.jl` refuses to produce a proportion +-- whose denominator is zero, because Julia's own `//` will happily answer `1//0` +-- and that non-finite Rational goes on to render in a chart as if it were a +-- number. Here the same fact is a property of the *type*: the denominator of a +-- `ℚᵘ` is `suc denominator-1`, so zero is not a denominator this type can hold +-- at all. Every refusal below therefore has somewhere to go that is not a +-- number, and every value that does come back is provably a real quotient. +-- +-- Everything in `proofs/agda` is built on this file plus the Agda standard +-- library and nothing else. There are no `postulate`s anywhere in the tree; +-- `proofs/tests/axiom-audit.sh` checks that, and checks its own control. + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.Prelude where + +open import Data.Bool.Base using (Bool; true; false) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Integer as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]; _*_; _+_; _≤_; _<_; nonNegative) +open import Data.Integer.Properties as ℤₚ + using (pos-*; pos-+; *-comm; *-zeroˡ; _≡?_; *-monoʳ-≤-nonNeg) + renaming (+-*-commutativeRing to +-*-commutativeRingℤ) +open import Data.Nat.Base using (z≤n; s≤s) +open import Data.List.Base as List using (List; []; _∷_; map) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; ≢-nonZero) +open import Data.Product using (Σ; Σ-syntax; ∃; ∃-syntax; _×_; _,_) +open import Data.Rational.Unnormalised + using (ℚᵘ; mkℚᵘ; _≃_; ↥_; ↧_; ↧ₙ_; 0ℚᵘ; 1ℚᵘ) + renaming (_+_ to _+ℚ_; _*_ to _*ℚ_; _/_ to _/ℚ_; _≤_ to _≤ℚ_; _<_ to _<ℚ_) +open import Data.Rational.Unnormalised.Base using (*≡*; *≤*; *<*) +open import Data.Rational.Unnormalised.Properties + using (+-*-commutativeRing; ≃-isEquivalence; +-isMagma; *-isMagma) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Function.Base using (_∘′_; const) +open import Relation.Binary using (Decidable) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst) +open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Negation using (¬_) + +------------------------------------------------------------------------ +-- Refusals +-- +-- The statistics layer's job is not to always produce a number. It is to +-- produce a number *or* name the reason it cannot. These constructors are the +-- reasons; the comment on each names the exception it stands for in +-- `src/analysis/`. A refusal is not an error path bolted on afterwards: it is +-- one arm of the same sum type as the answer, which is what makes +-- `outcome-total` below a theorem rather than a convention. + +data Refusal : Set where + -- UnsupportedRepresentationError("a proportion", "n/0", …) + zeroTotal : Refusal + -- ArgumentError("count (c) exceeds total (t)") + countExceedsTotal : Refusal + -- ResourceLimitError("denominator", limit, observed) + budgetExhausted : Refusal + -- CountOverflowError(left, right) + overflow : Refusal + -- UnsupportedRepresentationError("an exactly-known count", …): a Float64 + -- past 2^53 cannot say which integer it holds. + unprovenCount : Refusal + +data Outcome (A : Set) : Set where + value : A → Outcome A + refused : Refusal → Outcome A + +-- There is no third arm. This looks trivial and it is the point: "the answer is +-- either the exact value or a named refusal" is a statement about the shape of +-- the type, so a later edit that forgets a case cannot violate it quietly. +outcome-total : ∀ {A} (o : Outcome A) → + (∃ λ a → o ≡ value a) ⊎ (∃ λ r → o ≡ refused r) +outcome-total (value a) = inj₁ (a , refl) +outcome-total (refused r) = inj₂ (r , refl) + +-- A refusal is never a value. Stated because the whole layer's safety story +-- rests on the two arms not being confused downstream: a `nothing` that reaches +-- a chart as `0.0` is exactly the failure mode the refusals exist to prevent. +refused≢value : ∀ {A} {a : A} {r : Refusal} → value a ≢ refused r +refused≢value () + +is-value : ∀ {A} → Outcome A → Bool +is-value (value _) = true +is-value (refused _) = false + +------------------------------------------------------------------------ +-- Exact rationals +-- +-- `ℚᵘ` is the *unnormalised* rationals: an integer numerator and a positive +-- denominator, with equality `_≃_` by cross-multiplication. Two reasons this +-- models `Rational{BigInt}` faithfully rather than approximately: +-- +-- 1. `Rational{BigInt}(n, d)` normalises by gcd, but normalising changes the +-- representation and never the value. Every theorem here is about values +-- (`_≃_`), so each one transfers to the normalised form unchanged. +-- 2. The denominator is `suc _` by construction, so the zero-denominator case +-- is unrepresentable rather than checked-and-hoped-for. + +infix 4 _≟ℚᵘ_ + +_≟ℚᵘ_ : Decidable _≃_ +p ≟ℚᵘ q with (↥ p * ↧ q) ≡? (↥ q * ↧ p) +... | yes e = yes (*≡* e) +... | no ¬e = no (λ where (*≡* e) → ¬e e) + +-- Setoid structure over `_≃_`, so `≃-Reasoning` chains are available. +open import Algebra.Structures using (IsMagma) +open import Relation.Binary.Structures using (IsEquivalence) +open IsEquivalence ≃-isEquivalence public + using () renaming (refl to ≃-refl; sym to ≃-sym; trans to ≃-trans) + +-- Congruence of the two operations, taken from the library's own structures +-- rather than re-proved. +open IsMagma +-isMagma public using () renaming (∙-cong to +-cong-≃) +open IsMagma *-isMagma public using () renaming (∙-cong to *-cong-≃) + +-- Ring solvers, so that rational and integer identities are discharged by +-- computation rather than by hand-written chains. The ℚᵘ one is what makes +-- "the proportions of a sample sum to exactly one" a one-line proof instead of +-- a page of `*-assoc`. +open import Algebra.Solver.Ring.AlmostCommutativeRing using (fromCommutativeRing) +import Algebra.Solver.Ring.Simple as RingSolver + +module ℚᵘ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRing) _≟ℚᵘ_ +open ℚᵘ-Solver public using (con; _:+_; _:*_; _:=_) renaming (solve to solve-ℚ) + +module ℤ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRingℤ) _≡?_ +open ℤ-Solver public using () + renaming (solve to solve-ℤ; _:=_ to _:=ℤ_; con to conℤ; _:+_ to _:+ℤ_; _:*_ to _:*ℤ_) + +-- `n/d` with the positivity proof made explicit. `_/ℚ_` wants a `NonZero` +-- instance; this turns the proof a caller already holds into one. +_/[_]_ : (n : ℤ) (d : ℕ) → d ≢ 0 → ℚᵘ +n /[ d ] p = _/ℚ_ n d {{ℕ.≢-nonZero p}} + +infixl 7 _/[_]_ + +-- The two facts about quotients that everything else is built from. + +-- `a/d + b/d ≃ (a + b)/d`: proportions over a common total add by adding their +-- counts. This single lemma is why the exact relative abundances of one sample +-- sum to exactly one, with no rounding anywhere in the chain. +common-denominator-+ : ∀ (a b : ℤ) (d : ℕ) → + mkℚᵘ a d +ℚ mkℚᵘ b d ≃ mkℚᵘ (a + b) d +common-denominator-+ a b d = *≡* cross + where + -- ↥(p+q) · ↧r ≡ ↥r · ↧(p+q), where p = a/d, q = b/d, r = (a+b)/d: + -- (a·(1+d) + b·(1+d)) · (1+d) ≡ (a+b) · ((1+d)·(1+d)) + cross : (a * +[1+ d ] + b * +[1+ d ]) * +[1+ d ] + ≡ (a + b) * +[1+ d ℕ.+ d ℕ.* suc d ] + cross = trans + (solve-ℤ 3 (λ a b d → (a :*ℤ d :+ℤ b :*ℤ d) :*ℤ d :=ℤ (a :+ℤ b) :*ℤ (d :*ℤ d)) + refl a b (+[1+ d ])) + (cong ((a + b) *_) (sym (ℤₚ.pos-* (suc d) (suc d)))) + +-- `n/n ≃ 1`: the whole of a sample is the whole. +-- +-- Note what is *absent* from this statement: no side condition that `n` is +-- non-zero. In `ℚᵘ` the denominator is `suc _`, so `n/n` here means +-- `(n+1)/(n+1)` and the zero-denominator case is not a case this type has. The +-- Julia layer has to *check* for it at runtime, because `Rational{BigInt}` and +-- `//` both admit `1//0`; here there is nothing to check. That is the precise +-- sense in which the refusals in this development are total. +whole-is-one : ∀ (n : ℕ) → mkℚᵘ (+[1+ n ]) n ≃ 1ℚᵘ +whole-is-one n = *≡* (*-comm (+[1+ n ]) (+[1+ 0 ])) + +-- `0/n ≃ 0`: a feature absent from a sample that has reads at all is exactly +-- zero. That is a different claim from the sample having no reads, which is +-- refused rather than reported as zero. +zero-over : ∀ (d : ℕ) → mkℚᵘ (+ 0) d ≃ 0ℚᵘ +zero-over d = *≡* (trans (ℤₚ.*-zeroˡ (+[1+ 0 ])) (sym (ℤₚ.*-zeroˡ (+[1+ d ])))) + +------------------------------------------------------------------------ +-- Sums +-- +-- The Julia layer sums counts with `checked_count_sum` and rationals with +-- `exact_rational_sum`, and the two do not share an identity element on the +-- empty collection: an empty count sum is `0` (nothing was read) but an empty +-- rational sum is `nothing`, because "the values add up to none" is not the same +-- claim as "the values add up to zero". Keeping those apart is why the sums +-- below are separate definitions. + +-- Written out rather than taken from a library fold, so that the identity +-- element each sum starts from is visible in the definition: `+0` for counts, +-- `0ℚᵘ` for rationals. Neither is available for an empty collection of +-- *proportions*, which is why the analysis layer returns `nothing` there. +sumℤ : List ℤ → ℤ +sumℤ [] = +0 +sumℤ (x ∷ xs) = x + sumℤ xs + +sumℕ : List ℕ → ℕ +sumℕ [] = zero +sumℕ (x ∷ xs) = x ℕ.+ sumℕ xs + +sumℚᵘ : List ℚᵘ → ℚᵘ +sumℚᵘ [] = 0ℚᵘ +sumℚᵘ (x ∷ xs) = x +ℚ sumℚᵘ xs + +sumVecℤ : ∀ {n} → Vec ℤ n → ℤ +sumVecℤ [] = +0 +sumVecℤ (x ∷ xs) = x + sumVecℤ xs + +sumVecℕ : ∀ {n} → Vec ℕ n → ℕ +sumVecℕ [] = zero +sumVecℕ (x ∷ xs) = x ℕ.+ sumVecℕ xs + +sumVecℚᵘ : ∀ {n} → Vec ℚᵘ n → ℚᵘ +sumVecℚᵘ [] = 0ℚᵘ +sumVecℚᵘ (x ∷ xs) = x +ℚ sumVecℚᵘ xs + +-- Every count of a sample over the same denominator, as a vector of rationals. +-- This is the exact relative abundance of each feature before any rounding. +over-denominator : ∀ {n} (cs : Vec ℤ n) (d : ℕ) → Vec ℚᵘ n +over-denominator [] d = [] +over-denominator (c ∷ cs) d = mkℚᵘ c d ∷ over-denominator cs d + +-- Congruence of addition in its right argument, with the left one pinned. The +-- library's `∙-cong` needs both arguments' endpoints named; naming the left pair +-- explicitly is what lets `≃-refl` infer which value is unchanged. ++-cong-≃ʳ : ∀ {u v w : ℚᵘ} → u ≃ v → (w +ℚ u) ≃ (w +ℚ v) ++-cong-≃ʳ {u} {v} {w} p = +-cong-≃ {w} {w} {u} {v} ≃-refl p + +-- Summing with a common denominator distributes over the sum of the numerators. +-- This is the algebraic content of "aggregate counts, never average +-- proportions" (`src/analysis/exact_summaries.jl`), proved rather than asserted. +sum-over-common-denominator : ∀ (ns : List ℤ) (d : ℕ) → + sumℚᵘ (List.map (λ n → mkℚᵘ n d) ns) + ≃ mkℚᵘ (sumℤ ns) d +sum-over-common-denominator [] d = ≃-sym (zero-over d) +sum-over-common-denominator (n ∷ ns) d = + ≃-trans {mkℚᵘ n d +ℚ sumℚᵘ (List.map (λ m → mkℚᵘ m d) ns)} + {mkℚᵘ n d +ℚ mkℚᵘ (sumℤ ns) d} + {mkℚᵘ (n + sumℤ ns) d} + (+-cong-≃ʳ {sumℚᵘ (List.map (λ m → mkℚᵘ m d) ns)} {mkℚᵘ (sumℤ ns) d} {mkℚᵘ n d} + (sum-over-common-denominator ns d)) + (common-denominator-+ n (sumℤ ns) d) + +-- The same statement for the vector of counts in one sample, which is the shape +-- the analysis layer actually holds. +sumVec-over-common-denominator : ∀ {k} (cs : Vec ℤ k) (d : ℕ) → + sumVecℚᵘ (over-denominator cs d) + ≃ mkℚᵘ (sumVecℤ cs) d +sumVec-over-common-denominator [] d = ≃-sym (zero-over d) +sumVec-over-common-denominator (c ∷ cs) d = + ≃-trans {mkℚᵘ c d +ℚ sumVecℚᵘ (over-denominator cs d)} + {mkℚᵘ c d +ℚ mkℚᵘ (sumVecℤ cs) d} + {mkℚᵘ (c + sumVecℤ cs) d} + (+-cong-≃ʳ {sumVecℚᵘ (over-denominator cs d)} {mkℚᵘ (sumVecℤ cs) d} {mkℚᵘ c d} + (sumVec-over-common-denominator cs d)) + (common-denominator-+ c (sumVecℤ cs) d) + +-- Propositional equality implies value equality. Used whenever a numerator is +-- rewritten by an ℕ or ℤ computation: the quotient changes representation, never +-- value, and this is the one step that carries that across. +≡⇒≃ : ∀ {p q : ℚᵘ} → p ≡ q → p ≃ q +≡⇒≃ {p} pq = subst (λ x → p ≃ x) pq ≃-refl + +-- `+` preserves ℕ sums: the integer sum of the counts of a sample is the +-- integer image of their ℕ sum. Without this, "the counts add up to the depth" +-- (an ℕ fact) could not be used where the rationals need an ℤ numerator. +sumVecℕ-map-+ : ∀ {n} (cs : Vec ℕ n) → sumVecℤ (Vec.map +_ cs) ≡ + sumVecℕ cs +sumVecℕ-map-+ [] = refl +sumVecℕ-map-+ (c ∷ cs) = trans (cong (λ x → + c + x) (sumVecℕ-map-+ cs)) (sym (ℤₚ.pos-+ c (sumVecℕ cs))) + + +-- Monotonicity of a quotient in its numerator: over a common denominator, the +-- order of the values *is* the order of the counts. Used by the permutation +-- and multiple-testing modules, where every comparison is between quantities +-- that share a denominator by construction. +numerator-monotone-≤ : + ∀ (n m : ℤ) (d : ℕ) → n ≤ m → mkℚᵘ n d ≤ℚ mkℚᵘ m d +numerator-monotone-≤ n m d n≤m = + *≤* (ℤₚ.*-monoʳ-≤-nonNeg +[1+ d ] {{nonNegative (ℤ.+≤+ z≤n)}} n≤m) + + +-- Injectivity of the value arm, so a proof that two outcomes are the same +-- `value` yields a proof that the two numbers are the same number. +value-injective : ∀ {A} {a b : A} → value a ≡ value b → a ≡ b +value-injective refl = refl diff --git a/proofs/agda/MetaManifold/Proportions.agda b/proofs/agda/MetaManifold/Proportions.agda new file mode 100644 index 0000000..b06edb7 --- /dev/null +++ b/proofs/agda/MetaManifold/Proportions.agda @@ -0,0 +1,197 @@ +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Exact proportions: the machine-checked counterpart of +-- `src/analysis/numeric_policy.jl` (`exact_fraction`, `exact_relative_abundance`) +-- and `src/analysis/exact_summaries.jl`. +-- +-- The headline result is `proportions-sum-to-one`: the exact relative abundances +-- of one sample sum to *exactly* one, as a rational value, with no rounding +-- anywhere in the chain. That is a property compositional analysis quietly +-- assumes and almost never checks; here it is a theorem, and a theorem about +-- *values*, so it transfers to `Rational{BigInt}` and not only to the +-- unnormalised model used to prove it. +-- +-- The second group of results is about refusals. A sample with no reads has no +-- composition, so `exact_relative_abundance` returns `nothing` rather than `0`. +-- `zero-total-is-refused` pins that, and `value-is-the-quotient` pins the +-- converse: whenever this layer does hand back a number, that number is the +-- quotient it claims to be. + +{-# OPTIONS --without-K --safe #-} + +module MetaManifold.Proportions where + +open import MetaManifold.Prelude + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Integer using (ℤ; +_; +0; +[1+_]; _*_; _+_) +open import Data.Integer.Properties as ℤₚ using (pos-+) +open import Data.List.Base as List using (List; []; _∷_; map) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc) +open import Data.Nat.Properties as ℕₚ using (_≤?_; <-irrefl; ≤-trans) +open import Data.Product using (∃; _×_; _,_) +open import Data.Rational.Unnormalised + using (ℚᵘ; mkℚᵘ; _≃_; ↥_; ↧_; 0ℚᵘ; 1ℚᵘ) + renaming (_+_ to _+ℚ_) +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; sym; trans; cong) + +------------------------------------------------------------------------ +-- The operation itself +-- +-- `relativeAbundance c t` is `c/t` exactly, or a named refusal. The refusals +-- are checked in the order the Julia layer checks them, so the reason a caller +-- sees here is the reason the Julia layer would give. + +relativeAbundance : ℕ → ℕ → Outcome ℚᵘ +relativeAbundance c zero with c ℕₚ.≤? zero +... | no _ = refused countExceedsTotal +... | yes _ = refused zeroTotal +relativeAbundance c (suc m) with c ℕₚ.≤? suc m +... | no _ = refused countExceedsTotal +... | yes _ = value (+ c /[ suc m ] (λ ())) + +-- The exact relative abundance of every feature of a sample, given the +-- denominator (depth − 1, in ℚᵘ's encoding). Every entry shares one +-- denominator, which is what makes `proportions-sum-to-one` a one-step +-- consequence of `sumVec-over-common-denominator`. +abundances : ∀ {n} → Vec ℕ n → ℕ → Vec ℚᵘ n +abundances cs m = over-denominator (Vec.map +_ cs) m + +------------------------------------------------------------------------ +-- The refusals are what they say they are + +-- A sample of zero reads has no composition. `nothing`, not `0`: a proportion +-- of zero claims the feature is absent from a sample that was sequenced, which +-- a sample that was not sequenced cannot support. +zero-total-is-refused : relativeAbundance 0 zero ≡ refused zeroTotal +zero-total-is-refused = refl + +-- A sample with no reads, asked about a feature that claims reads, is refused +-- for the *count* reason and not the total one, because +-- `exact_relative_abundance` checks `count <= total` before `iszero(total)`. +-- The order is not arbitrary: the two reasons tell a user different things +-- about which of the two numbers is wrong, and this theorem pins the order +-- rather than leaving it to a reader of the source. +zero-total-with-count-is-refused-as-exceeding : + ∀ c → relativeAbundance (suc c) zero ≡ refused countExceedsTotal +zero-total-with-count-is-refused-as-exceeding c = refl + +-- A count larger than its own total is not a count of that table. Refused +-- rather than clamped, because clamping would silently invent a composition +-- that sums to one. +count-exceeds-total-is-refused : + ∀ c t → suc t ℕ.≤ c → relativeAbundance c t ≡ refused countExceedsTotal +count-exceeds-total-is-refused c zero t +# +# Bootstrap and run the Agda proof gate. +# +# This script exists because the proofs must be checkable by anyone, on a clean +# machine, with one command — and because a proof gate that silently passes when +# the prover is absent is worse than no gate at all. Every failure mode below +# exits non-zero. There is no `|| true`, no `command -v agda || exit 0`, and no +# path in which "prover not installed" is reported as success. +# +# Usage: +# proofs/bootstrap.sh bootstrap if needed, then check +# proofs/bootstrap.sh --bootstrap install toolchain only +# proofs/bootstrap.sh --check check only (fail if not bootstrapped) +# +# Environment: +# AGDA_BIN path to an agda binary to use instead of bootstrapping one +# PROOFS_VENDOR directory for the vendored stdlib / Agda source +# (default: proofs/.vendor, which is git-ignored) +# +# Pinned versions — these are the versions the proofs were developed against. +# Agda 2.7.0.1 with stdlib 3.0. Changing either is a real change to the gate and +# must be reviewed, not a maintenance chore to be done silently. + +set -euo pipefail + +AGDA_VERSION="2.7.0.1" + +# agda-stdlib revision. Pinned by SHA, not by tag, and the reason matters: +# these proofs use stdlib APIs (`Data.Integer.Properties._≡?_`, the `Dec` record +# shape, `toWitness {a? = …}`, `NonNegative` *instances* for +# `*-monoʳ-≤-nonNeg`) that exist only on the development line towards 3.0 — the +# branch self-identifies as `standard-library-3.0` but no `v3.0` tag has been cut. +# They do NOT compile against the latest release (v2.4) or against v2.1, which is +# the estate pin on `main`. See proofs/residue/toolchain.residue. +STDLIB_VERSION="2ffa8b7d4e8e818717ad643d184f055a4d1b0447" + +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +PROOFS_DIR="$REPO_ROOT/proofs" +AGDA_DIR_SRC="$PROOFS_DIR/agda" +VENDOR="${PROOFS_VENDOR:-$PROOFS_DIR/.vendor}" +LIB_FILE="$AGDA_DIR_SRC/metamanifold.agda-lib" + +log() { printf 'proofs: %s\n' "$*"; } +die() { printf 'proofs: FATAL: %s\n' "$*" >&2; exit 1; } + +[[ -f "$LIB_FILE" ]] || die "missing $LIB_FILE" + +############################################################################## +# Locate or install Agda +############################################################################## + +resolve_agda() { + if [[ -n "${AGDA_BIN:-}" ]]; then + [[ -x "$AGDA_BIN" ]] || die "AGDA_BIN=$AGDA_BIN is not executable" + AGDA="$AGDA_BIN" + return 0 + fi + if command -v agda >/dev/null 2>&1; then + AGDA="$(command -v agda)" + return 0 + fi + if [[ -x "$VENDOR/venv/bin/agda" ]]; then + AGDA="$VENDOR/venv/bin/agda" + return 0 + fi + return 1 +} + +install_agda() { + log "no agda on PATH; installing agda $AGDA_VERSION from PyPI into $VENDOR/venv" + command -v python3 >/dev/null 2>&1 || die "python3 is required to bootstrap agda" + mkdir -p "$VENDOR" + python3 -m venv "$VENDOR/venv" + "$VENDOR/venv/bin/pip" install --quiet --disable-pip-version-check "agda==$AGDA_VERSION" \ + || die "pip install agda==$AGDA_VERSION failed" + AGDA="$VENDOR/venv/bin/agda" + [[ -x "$AGDA" ]] || die "agda was not installed at $AGDA" +} + +############################################################################## +# Vendor the standard library and the Agda primitive libraries +############################################################################## + +vendor_stdlib() { + if [[ -f "$VENDOR/agda-stdlib/standard-library.agda-lib" ]]; then + return 0 + fi + log "cloning agda-stdlib at $STDLIB_VERSION" + mkdir -p "$VENDOR" + rm -rf "$VENDOR/agda-stdlib" + # A tag would allow `--branch`; a SHA does not, so fetch the exact revision. + git init -q "$VENDOR/agda-stdlib" + git -C "$VENDOR/agda-stdlib" remote add origin https://github.com/agda/agda-stdlib + git -C "$VENDOR/agda-stdlib" fetch -q --depth 1 origin "$STDLIB_VERSION" \ + && git -C "$VENDOR/agda-stdlib" checkout -q FETCH_HEAD \ + || die "could not fetch agda-stdlib $STDLIB_VERSION" + # The upstream `.agda-lib` file is named after the tag (`agda-stdlib.agda-lib` + # on some tags, `standard-library-2.1.agda-lib` on others) and its `name:` does + # not always read `standard-library`, which is what `defaults` and every + # `depend:` clause refer to. Normalise both, whatever the tag ships. + local lib + lib="$(find "$VENDOR/agda-stdlib" -maxdepth 1 -name '*.agda-lib' | head -1)" + [[ -n "$lib" ]] || die "the agda-stdlib checkout at $STDLIB_VERSION has no .agda-lib file" + sed -i 's/^name: .*/name: standard-library/' "$lib" + if [[ "$(basename "$lib")" != "standard-library.agda-lib" ]]; then + cp "$lib" "$VENDOR/agda-stdlib/standard-library.agda-lib" + fi + log "stdlib library file: $lib" +} + +vendor_prims() { + # The PyPI wheel ships the Agda executable but not `Agda.Primitive` and + # friends, which every module transitively needs. They come from the source + # tree at the matching tag. A wheel installed from a system package manager + # normally has them already, in which case this is a no-op. + local datadir + datadir="$("$AGDA" --print-agda-dir)" + if [[ -d "$datadir/lib/prim/Agda" ]]; then + log "primitive libraries already present at $datadir/lib/prim" + PRIM_SRC="" + return 0 + fi + log "fetching Agda v$AGDA_VERSION source for the primitive libraries" + mkdir -p "$VENDOR" + if [[ ! -d "$VENDOR/agda-src/src/data/lib/prim/Agda" ]]; then + rm -rf "$VENDOR/agda-src" + git clone --quiet --depth 1 --branch "v$AGDA_VERSION" \ + https://github.com/agda/agda "$VENDOR/agda-src" \ + || die "could not clone agda v$AGDA_VERSION (needed for the primitive libraries)" + fi + mkdir -p "$datadir/lib" + cp -r "$VENDOR/agda-src/src/data/lib/prim" "$datadir/lib/prim" \ + || die "could not install the primitive libraries into $datadir/lib/prim" +} + +# Agda looks for the library list in two places, and which one wins depends on +# how Agda was installed: the user config directory (`~/.config/agda/`, i.e. +# $XDG_CONFIG_HOME/agda/) and the data directory reported by --print-agda-dir. +# A PyPI wheel reads one, a distro package the other. Write both, so the gate +# does not depend on how the toolchain happens to have been installed. +AGDA_LIBRARIES_FILE="$PROOFS_DIR/.agda-libraries" + +write_agda_config() { + # A stable, in-repo libraries file. check() passes this to Agda explicitly via + # --library-file, so the gate works even if neither config location is read. + { + printf '%s\n' "$LIB_FILE" + printf '%s\n' "$VENDOR/agda-stdlib/standard-library.agda-lib" + } > "$AGDA_LIBRARIES_FILE" + + local datadir userdir + datadir="$("$AGDA" --print-agda-dir)" + userdir="${XDG_CONFIG_HOME:-$HOME/.config}/agda" + for d in "$datadir/lib" "$userdir"; do + mkdir -p "$d" + cp "$AGDA_LIBRARIES_FILE" "$d/libraries" + printf 'standard-library\n' > "$d/defaults" + log "wrote $d/{libraries,defaults}" + done +} + +############################################################################## +# The gate itself +############################################################################## + +check() { + resolve_agda || die "agda is not installed and no AGDA_BIN was given; run proofs/bootstrap.sh" + log "using $("$AGDA" --version)" + cd "$AGDA_DIR_SRC" + # --safe: no postulates, no foreign code, no `--type-in-type`. A proof that + # needs an escape hatch is not a proof. + # --without-K: no proof-irrelevance-by-fiat for equality. + log "type-checking MetaManifold.All (this reaches every module in the tree)" + if [[ -f "$AGDA_LIBRARIES_FILE" ]]; then + "$AGDA" --library-file="$AGDA_LIBRARIES_FILE" --safe --without-K MetaManifold/All.agda + else + die "$AGDA_LIBRARIES_FILE is missing; run proofs/bootstrap.sh --bootstrap first" + fi + log "axiom audit" + "$PROOFS_DIR/tests/axiom-audit.sh" + log "OK" +} + +case "${1:-}" in + --bootstrap) + resolve_agda || install_agda + vendor_stdlib + vendor_prims + write_agda_config + ;; + --check) + check + ;; + "") + resolve_agda || install_agda + vendor_stdlib + vendor_prims + write_agda_config + check + ;; + *) + die "unknown argument: $1 (expected --bootstrap, --check, or nothing)" + ;; +esac diff --git a/proofs/residue/benjamini-hochberg.residue b/proofs/residue/benjamini-hochberg.residue new file mode 100644 index 0000000..ec301dd --- /dev/null +++ b/proofs/residue/benjamini-hochberg.residue @@ -0,0 +1,52 @@ +# Residue — Benjamini–Hochberg scaling +# +# See exact-counts.residue for the format and for what this file is for. + +R-BH-1 + statement: | + ∀ M j n d → 0ℚᵘ ≤ℚ bhScale M j (+ n) d + (the scaled value of a non-negative p-value is non-negative) + status: OPEN + why: | + `+ M * + n` does not reduce to `+ (M ℕ.* n)`; `ℤ._*_` unfolds to a + sign-times-absolute-value form, and the non-negativity lemmas in + `Data.Integer.Properties` (`*-monoʳ-≤-nonNeg`, `*-monoˡ-≤-nonNeg`) are stated + about the reduced form. Two attempts were made — one via + `ℤ.+≤+ z≤n` directly, one via `*-zeroʳ` plus `*-monoʳ-≤-nonNeg` — and both + failed on exactly that mismatch. + impact: LOW. A negative q-value would need a negative p-value numerator, and + p-value numerators are counts. + closes-with: | + A transport through `ℤₚ.◃-+`/`sign` lemmas, or restating the goal with the + numerator written as `+ (M ℕ.* n)` and transporting the `bhScale` definition. + +R-BH-2 + statement: | + The BH step-down envelope: `q_i = min over j ≥ i of bhScale M j p_j`, + monotone-enforced so that adjusted values are non-decreasing in rank. + status: NOT ATTEMPTED + why: | + `ℚᵘ` has no `⊓` lemmas in the standard library — there is no `x⊓y≤x` for the + unnormalised rationals — so a minimum has to be built from `≤-total` and then + have its two projection properties proved by hand. That is a real chunk of + work and it was cut to keep this change reviewable. + impact: | + MEDIUM. What IS proved is the per-rank scaling step, which is the part that + can silently go wrong through floating-point drift. The envelope is a + `min` over proved-correct values. + closes-with: | + `minℚ : ℚᵘ → ℚᵘ → ℚᵘ` defined by case analysis on `≤-total`, with + `minℚ-≤ˡ`/`minℚ-≤ʳ` proved from it, then a fold with a monotonicity + invariant. Also note: `q_i ≥ p_i` is FALSE in general and must not be + attempted — it holds only when `M/(j+1) ≥ 1`. + +R-BH-3 + statement: | + That the q-values produced by this scaling control the false discovery rate + at the nominal level. + status: OUT OF SCOPE (see out-of-scope.residue) + why: | + FDR control is a theorem about a probability measure over a sampling model. + This development is about exact rational arithmetic, not about measure + theory. Claiming FDR control from these lemmas would be the single worst + thing this directory could assert. diff --git a/proofs/residue/exact-counts.residue b/proofs/residue/exact-counts.residue new file mode 100644 index 0000000..89848e2 --- /dev/null +++ b/proofs/residue/exact-counts.residue @@ -0,0 +1,63 @@ +# Residue — exact counts +# +# What this file is: obligations that the Agda development does *not* discharge, +# stated precisely enough that somebody could pick one up cold. Residue is not a +# backlog of nice-to-haves. Each entry is something a reader of PROOF-STATUS.md +# might reasonably assume is proved, and is not. +# +# Format: `id | statement | status | why it is open | what would close it` + +R-EC-1 + statement: + ∀ {A} {r s : Refusal} → Checked.refused r ≡ Checked.refused s → r ≡ s + (injectivity of the `refused` constructor of `MetaManifold.ExactCounts.Checked`) + status: OPEN + why: | + Agda's pattern matcher will not discharge `refl` on `refused r ≡ refused s` + here, even with the carrier `A` pinned on both sides; the unification stays + blocked on the implicit carrier. This was attempted three ways (dotted + pattern, `{A = A}` on both sides, and a `where`-scoped helper) and all three + reported the same blocked meta. + impact: | + LOW. The statement that a caller actually depends on is + `checkedAdd-refuses-exactly-when-it-must` — a refusal happens exactly when + the sum leaves the representable range — and that IS proved. Injectivity + would additionally pin down *which* constructor is used, which no call site + currently branches on. + closes-with: | + Either a five-clause case analysis over `Refusal`'s constructors (each arm + closed by `refl`, since both sides are then closed constructor applications), + or moving `Checked` into the Prelude next to `Outcome` so the two share one + carrier discipline. + +R-EC-2 + statement: | + The bound `k` in `Bounded k` models `Int64` as `Fits 63`, i.e. + -2^63 ≤ v < 2^63. The connection between this `k = 63` and the width of + Julia's `Int64` is not proved, because Julia's integer width is not in scope + for an Agda module. + status: OPEN BY CONSTRUCTION + why: | + Proving it would require a model of Julia's `Int` inside Agda. What the + development does instead is make the bound *data* — `pow2 63` — so the + arithmetic is checked for whatever `k` the caller supplies. + impact: | + MEDIUM but bounded. A wrong `k` would make the guard wrong in a way the + proofs would still accept. + closes-with: | + A conformance test in the Julia testset that asserts the constant the + statistics layer passes as the bit width equals `sizeof(Int) * 8 - 1`. That + is a one-line test, not a proof, and it has to live on the Julia side because + `sizeof(Int)` is a fact about the running Julia, not about the model. + +R-EC-3 + statement: | + `checked_count_sum` with `on_overflow = :widen` promotes to `BigInt` instead + of refusing. The Agda model covers only the refusing branch. + status: OUT OF SCOPE (see out-of-scope.residue) + why: | + Widening has no bound, so there is no `k` to state `Fits k` about. Modelling + it would mean modelling unbounded integers, which is what `sumℤ` in the + Prelude already does — and `checkedSumOf-is-exact` is the exactness statement + for the *refusing* path that the analysis layer actually uses. + impact: LOW. diff --git a/proofs/residue/out-of-scope.residue b/proofs/residue/out-of-scope.residue new file mode 100644 index 0000000..70705ad --- /dev/null +++ b/proofs/residue/out-of-scope.residue @@ -0,0 +1,41 @@ +# Residue — out of scope for the Agda development +# +# Statements that the formalisation deliberately does not make. They are listed +# here rather than left unsaid because the alternative is a reader inferring them +# from the presence of a proof directory, which would be worse than not having +# one. + +R-OOS-1 Probability theory + This development reasons about exact rational arithmetic: what a proportion is, + when a count overflows, what a p-value estimator can and cannot return, what a + rounded decimal means. It does not model randomness. No statement here is a + statement about coverage, bias, type I error, or FDR control. Those are + simulation-study questions and are addressed (with pre-set tolerances) in the + Julia validation layer, not here. + +R-OOS-2 Floating point + No IEEE-754 semantics are modelled. Every theorem is over `ℚᵘ`, the exact + unnormalised rationals. Claims of the form "Float64 arithmetic gives the same + answer" are not made and cannot be read off this directory. Where the shipped + code uses Float64 — `:ordinary` mode, which is unchanged — its correctness is + an empirical question answered by tests, not a proved one. + +R-OOS-3 Correspondence between the Agda model and the Julia implementation + The Agda modules model the *semantics* the Julia layer is required to have. + Nothing here proves that `src/analysis/numeric_policy.jl` implements them. The + bridge is `test/fixtures/agda-known-answers.json`: values computed by the + proof assistant that the Julia conformance testset must reproduce. If the + Julia layer and the model disagree, the fixture test fails — that is the + mechanism, and it is a test, not a proof. + +R-OOS-4 The `:ordinary` path + Existing behaviour with the new layer not selected is required to be + byte-for-byte unchanged. That is a regression property over a large existing + test suite, not a theorem about a small model, and it is verified by running + that suite, not by Agda. + +R-OOS-5 Exact statistical tests + Deferred to issue #3 by the approved method catalogue + (docs/statistics/method-catalogue-v1.md, item 4). `PermutationTest.agda` + proves properties of the *estimator* used when a permutation test is run, and + says nothing about exact tests as a method. diff --git a/proofs/residue/toolchain.residue b/proofs/residue/toolchain.residue new file mode 100644 index 0000000..74459cf --- /dev/null +++ b/proofs/residue/toolchain.residue @@ -0,0 +1,46 @@ +# Residue — toolchain +# +# The one entry in this directory that is not a mathematical obligation but a +# reproducibility defect. It is recorded here rather than buried in a script +# comment because it changes what "the proofs are verified" means. + +R-TC-1 + statement: | + The proofs compile against agda-stdlib's development line towards 3.0, pinned + by SHA `2ffa8b7d4e8e818717ad643d184f055a4d1b0447` (2026-09-12, "Remove fixity + declarations for closed operators (#3115)"). That branch's own library file + declares `name: standard-library-3.0`, but **no `v3.0` tag has been cut**. + status: OPEN + why: | + Verified this session: `git clone --branch v3.0` fails with "Could not find + remote branch v3.0"; the newest tag is `v2.4`. Against `v2.4` the proofs do + NOT compile — the first failure is `Data.Integer.Properties` not exporting + `_≡?_`. Pinning an untagged SHA is reproducible but fragile: it is a moving + target's frozen point, not a supported release. + impact: | + HIGH for portability, nil for correctness. The theorems are unaffected; only + the API surface they are written against is. + closes-with: | + Either (a) wait for an agda-stdlib `v3.0` tag and re-pin to it, or (b) port + the six modules to a released stdlib. Option (b) is required anyway to land + on `main`, which pins agda-stdlib 2.1 / Agda 2.6.4.3. Known porting targets, + in the order they fail: `Data.Integer.Properties._≡?_` (use `_≟_`), the `Dec` + record shape and `toWitness {a? = …}`, `NonNegative` as an *instance* argument + to `*-monoˡ-≤-nonNeg` / `*-monoʳ-≤-nonNeg`, and `Data.Rational.Unnormalised` + module layout. `main`'s `Evidence.*` modules avoid all of this by being + stdlib-free (`Agda.Builtin.*` only), which is the better target if the estate + wants the statistics modules to check without the stdlib at all. + +R-TC-2 + statement: | + Agda's library-file location differs between install methods. + status: CLOSED (worked around) + why: | + A PyPI wheel and a distro package disagree about whether the library list is + read from `$XDG_CONFIG_HOME/agda/libraries` or from the data directory + reported by `--print-agda-dir`. `proofs/bootstrap.sh` now writes both AND + passes `--library-file` explicitly on every invocation, so the gate no longer + depends on ambient configuration. Recorded because an earlier version of the + script wrote only the data directory and silently failed on a fresh venv with + "Library 'standard-library' not found" — despite the file being present and + correct. diff --git a/proofs/tests/axiom-audit.sh b/proofs/tests/axiom-audit.sh new file mode 100755 index 0000000..5b09789 --- /dev/null +++ b/proofs/tests/axiom-audit.sh @@ -0,0 +1,107 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: AGPL-3.0-only +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Audit the proof tree for anything that would let a "proof" pass without +# proving anything. +# +# A type-checker only guarantees what its rules allow. Every check here is a +# rule we refuse to allow. Each one exits non-zero on a finding, and each one is +# exercised by `proofs/tests/gate-selftest.sh`, so this script cannot rot into a +# no-op unnoticed. +# +# Checks: +# 1. every module declares `--safe` +# 2. no `postulate` blocks +# 3. no FFI, no `{-# COMPILE`, no `{-# BUILTIN` +# 4. no unsound flags (`--type-in-type`, `--no-positivity-check`, +# `--no-termination-check`, `--no-universe-polymorphism` off-switches) +# 5. no `trustMe` / `primTrust` / `{-# NO_POSITIVITY_CHECK` pragmas +# 6. no holes (`{!!}`, `?`) left in a checked module +# 7. every `.agda` file is reachable from `All.agda` — a module that is not +# imported by the gate entry point is not checked at all, which is the +# easiest way to have a "proved" theorem that nobody ever type-checked + +set -euo pipefail + +PROOFS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +AGDA_DIR="$PROOFS_DIR/agda" +ENTRY="$AGDA_DIR/MetaManifold/All.agda" + +failures=0 +fail() { printf 'axiom-audit: FAIL: %s\n' "$*" >&2; failures=$((failures + 1)); } +note() { printf 'axiom-audit: %s\n' "$*"; } + +[[ -f "$ENTRY" ]] || { printf 'axiom-audit: FATAL: missing %s\n' "$ENTRY" >&2; exit 1; } + +mapfile -t FILES < <(find "$AGDA_DIR" -name '*.agda' -type f | sort) +[[ ${#FILES[@]} -gt 0 ]] || { printf 'axiom-audit: FATAL: no .agda files found\n' >&2; exit 1; } +note "auditing ${#FILES[@]} module(s)" + +for f in "${FILES[@]}"; do + rel="${f#"$AGDA_DIR"/}" + + # 1. --safe + if ! grep -q '^{-# OPTIONS .*--safe' "$f"; then + fail "$rel does not declare --safe" + fi + + # 2. postulates + if grep -nE '^[[:space:]]*postulate\b' "$f" >/dev/null; then + fail "$rel contains a postulate block: $(grep -nE '^[[:space:]]*postulate\b' "$f" | head -3 | tr '\n' ' ')" + fi + + # 3. FFI + if grep -nE '\{-#[[:space:]]*(FOREIGN|COMPILE|BUILTIN)' "$f" >/dev/null; then + fail "$rel uses FOREIGN/COMPILE/BUILTIN" + fi + + # 4. unsound flags + if grep -nE '\{-#[[:space:]]*OPTIONS.*(--type-in-type|--no-positivity-check|--no-termination-check|--no-guardedness)' "$f" >/dev/null; then + fail "$rel enables an unsound flag" + fi + + # 5. trusted primitives + if grep -nE '\b(trustMe|primTrust|NO_POSITIVITY_CHECK|NO_TERMINATION_CHECK)\b' "$f" >/dev/null; then + fail "$rel uses trustMe/primTrust or a check-disabling pragma" + fi + + # 6. holes + if grep -nE '\{\![^!]*\!\}|^[^[:space:]].*[[:space:]]\?[[:space:]]*$' "$f" >/dev/null; then + fail "$rel contains a hole" + fi +done + +# 7. reachability from the gate entry point +# +# Walk the import graph starting at All.agda. Anything not reached is a module +# the gate never type-checks. +declare -A SEEN=() +queue=("MetaManifold.All") +while [[ ${#queue[@]} -gt 0 ]]; do + mod="${queue[0]}" + queue=("${queue[@]:1}") + [[ -n "${SEEN[$mod]:-}" ]] && continue + SEEN[$mod]=1 + path="$AGDA_DIR/$(echo "$mod" | tr '.' '/').agda" + [[ -f "$path" ]] || { fail "imported module $mod has no file at $path"; continue; } + while read -r dep; do + queue+=("$dep") + done < <(grep -oE '^[[:space:]]*open[[:space:]]+import[[:space:]]+[A-Za-z0-9_.]+' "$path" \ + | awk '{print $NF}' | grep '^MetaManifold\.') +done + +for f in "${FILES[@]}"; do + rel="${f#"$AGDA_DIR"/}" + mod="$(echo "${rel%.agda}" | tr '/' '.')" + if [[ -z "${SEEN[$mod]:-}" ]]; then + fail "$rel is not reachable from MetaManifold/All.agda — it is never type-checked" + fi +done +note "reachability: ${#SEEN[@]} module(s) reachable from MetaManifold.All" + +if [[ $failures -gt 0 ]]; then + printf 'axiom-audit: %d finding(s)\n' "$failures" >&2 + exit 1 +fi +note "clean" diff --git a/proofs/tests/gate-selftest.sh b/proofs/tests/gate-selftest.sh new file mode 100755 index 0000000..f380dc7 --- /dev/null +++ b/proofs/tests/gate-selftest.sh @@ -0,0 +1,137 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: AGPL-3.0-only +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Prove that the proof gate can fail. +# +# A gate that has never been observed to reject anything is not evidence. This +# script takes a throwaway copy of the proof tree, breaks it in one specific way +# at a time, and requires the gate to reject it. If any mutation is *accepted*, +# or if a mutation failed to apply at all, this script exits non-zero. +# +# It runs in CI. A gate whose self-test is skipped is a gate nobody can trust, +# so there is no flag to turn this off. +# +# Usage: proofs/tests/gate-selftest.sh + +set -uo pipefail + +PROOFS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +# Resolve Agda the same way bootstrap.sh does, so `just proofs-selftest` works +# after `just proofs-bootstrap` with nothing else on PATH. +VENDOR="${PROOFS_VENDOR:-$PROOFS_DIR/.vendor}" +if [[ -n "${AGDA_BIN:-}" ]]; then + AGDA="$AGDA_BIN" +elif command -v agda >/dev/null 2>&1; then + AGDA="$(command -v agda)" +elif [[ -x "$VENDOR/venv/bin/agda" ]]; then + AGDA="$VENDOR/venv/bin/agda" +else + printf 'gate-selftest: FATAL: agda not found (run proofs/bootstrap.sh --bootstrap, or set AGDA_BIN)\n' >&2 + exit 1 +fi +[[ -x "$AGDA" ]] || { printf 'gate-selftest: FATAL: %s is not executable\n' "$AGDA" >&2; exit 1; } + +STDLIB_LIB="" +for cand in "$VENDOR/agda-stdlib/standard-library.agda-lib"; do + [[ -f "$cand" ]] && { STDLIB_LIB="$cand"; break; } +done +[[ -n "$STDLIB_LIB" ]] || { printf 'gate-selftest: FATAL: standard library not found\n' >&2; exit 1; } + +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT +cp -r "$PROOFS_DIR/agda" "$WORK/agda" +cp -r "$PROOFS_DIR/tests" "$WORK/tests" +cp "$PROOFS_DIR/agda/metamanifold.agda-lib" "$WORK/agda/" 2>/dev/null || true + +# Point Agda at the *copy*: without this the library file would resolve +# `MetaManifold.All` back to the pristine tree and every mutation below would be +# checked against unmutated sources — a self-test that tests nothing. +printf '%s\n%s\n' "$WORK/agda/metamanifold.agda-lib" "$STDLIB_LIB" > "$WORK/libraries" + +run_gate() { + ( cd "$WORK/agda" && "$AGDA" --library-file="$WORK/libraries" --safe --without-K MetaManifold/All.agda ) \ + >"$WORK/out.txt" 2>&1 +} +run_audit() { "$WORK/tests/axiom-audit.sh" >"$WORK/out.txt" 2>&1; } + +total=0 +failed=0 + +# expect_reject +expect_reject() { + local name="$1" runner="$2" target="$3" mutator="$4" + local file="$WORK/agda/$target" + total=$((total + 1)) + + # Restore a pristine copy of the target before mutating. + cp "$PROOFS_DIR/agda/$target" "$file" + local before after + before="$(sha256sum "$file" | awk '{print $1}')" + bash -c "$mutator" mutator "$file" + after="$(sha256sum "$file" | awk '{print $1}')" + if [[ "$before" == "$after" ]]; then + printf 'gate-selftest: FAIL %-42s mutation did not apply (stale pattern?)\n' "$name" + failed=$((failed + 1)) + return + fi + + if $runner; then + printf 'gate-selftest: FAIL %-42s gate ACCEPTED a broken proof\n' "$name" + sed 's/^/ | /' "$WORK/out.txt" | head -6 + failed=$((failed + 1)) + else + printf 'gate-selftest: ok %-42s rejected\n' "$name" + fi + cp "$PROOFS_DIR/agda/$target" "$file" +} + +# --- the type-checker must reject wrong mathematics ------------------------- +# +# Each mutator is a shell snippet receiving the target file as $1. If a snippet +# stops matching (because the proof was rewritten), `expect_reject` reports the +# mutation as unapplied rather than silently passing. + +expect_reject "rounding: wrong known-answer digit" run_gate "MetaManifold/DecimalRounding.agda" \ + 'sed -i "s|+ 402 ℤ.> "$1"' + +expect_reject "audit: --safe removed" run_audit "MetaManifold/Proportions.agda" \ + 'sed -i "s|--without-K --safe|--without-K|" "$1"' + +# --- the gate must still accept the pristine tree -------------------------- + +total=$((total + 1)) +cp "$PROOFS_DIR/agda/MetaManifold/All.agda" "$WORK/agda/MetaManifold/All.agda" +if run_gate && run_audit; then + printf 'gate-selftest: ok %-42s accepted\n' "pristine tree" +else + printf 'gate-selftest: FAIL %-42s gate REJECTED the real proofs\n' "pristine tree" + sed 's/^/ | /' "$WORK/out.txt" | head -12 + failed=$((failed + 1)) +fi + +printf 'gate-selftest: %d/%d controls behaved correctly\n' "$((total - failed))" "$total" +[[ $failed -eq 0 ]] || exit 1 diff --git a/test/fixtures/agda-known-answers.json b/test/fixtures/agda-known-answers.json new file mode 100644 index 0000000..9d4e345 --- /dev/null +++ b/test/fixtures/agda-known-answers.json @@ -0,0 +1,128 @@ +{ + "_provenance": { + "generator": "proofs/agda/MetaManifold/DecimalRounding.agda, BenjaminiHochberg.agda, PermutationTest.agda", + "checked_by": "agda 2.7.0.1 --safe --without-K, agda-stdlib v3.0", + "gate": "proofs/bootstrap.sh --check", + "generated": "2026-09-26", + "contract": "Every value in this file is a value a proof assistant has checked against a definition, not a number somebody typed into two places. The Julia conformance testset MUST reproduce these exactly. If the Julia layer and this file disagree, the Julia layer is wrong: these are the specification, and each entry names the lemma that fixes it.", + "do_not_edit_by_hand": "Edit the Agda module and re-run the gate. A hand-edited value here is an unchecked value." + }, + + "decimal_rounding": { + "_spec": "IsRounding n d s m == 2*n*10^s - (d+1) <= 2*m*(d+1) < 2*n*10^s + (d+1); the rational being rounded is n/(d+1), so d is denominator-minus-one. Exact halves go DOWN under this rule.", + "_alt_spec": "IsRoundHalfUp n d s m == 2*m*(d+1) - (d+1) <= 2*n*10^s < 2*m*(d+1) + (d+1); same tolerance, exact halves go UP.", + "vectors": [ + { + "rational": "2/3", + "n": 2, "d": 2, "decimals": 2, + "scaled_integer": 67, + "printed": "0.67", + "rule": "IsRounding", + "lemma": "rounding-2/3-at-2dp" + }, + { + "rational": "1/3", + "n": 1, "d": 2, "decimals": 2, + "scaled_integer": 33, + "printed": "0.33", + "rule": "IsRounding", + "lemma": "rounding-1/3-at-2dp" + }, + { + "rational": "5/8", + "n": 5, "d": 7, "decimals": 3, + "scaled_integer": 625, + "printed": "0.625", + "rule": "IsRounding", + "lemma": "rounding-5/8-at-3dp" + }, + { + "rational": "0/1", + "n": 0, "d": 0, "decimals": 2, + "scaled_integer": 0, + "printed": "0.00", + "rule": "IsRounding", + "lemma": "rounding-zero-at-2dp", + "note": "An exact zero rounds to zero, not to a small number that merely prints as zero." + }, + { + "rational": "1/1", + "n": 1, "d": 0, "decimals": 2, + "scaled_integer": 100, + "printed": "1.00", + "rule": "IsRounding", + "lemma": "rounding-one-at-2dp", + "note": "Rounding must not introduce error where there is none." + } + ], + "tie": { + "_note": "The two rules differ ONLY at an exact half. Everywhere else they agree, which is what the agreement_* lemmas record.", + "half_at_zero_decimals": { + "rational": "1/2", + "n": 1, "d": 1, "decimals": 0, + "IsRounding": { "scaled_integer": 0, "printed": "0", "lemma": "half-ties-round-down" }, + "IsRoundHalfUp": { "scaled_integer": 1, "printed": "1", "lemma": "half-ties-round-up" } + }, + "agreement": [ + { "rational": "2/3", "scaled_integer": 67, "lemma": "agreement-2/3" }, + { "rational": "1/3", "scaled_integer": 33, "lemma": "agreement-1/3" }, + { "rational": "5/8", "scaled_integer": 625, "lemma": "agreement-5/8" }, + { "rational": "1/1", "scaled_integer": 100, "lemma": "agreement-one" } + ] + } + }, + + "benjamini_hochberg": { + "_spec": "bhScale M j n d = mkQ (+ M * n) (j + d + j*d), i.e. (M/(j+1)) * (n/(d+1)). Numerator and denominator are fixed by bhScale-numerator and bhScale-denominator; the denominator stored is (j+1)(d+1) - 1.", + "vectors": [ + { + "family_size": 10, "rank0": 0, "p_numerator": 1, "p_denominator_minus_one": 99, + "q_numerator": 10, "q_denominator": 100, "q": "1/10", + "note": "Rank 0 of 10 tests scales p=0.01 by 10/1." + }, + { + "family_size": 10, "rank0": 9, "p_numerator": 5, "p_denominator_minus_one": 19, + "q_numerator": 50, "q_denominator": 200, "q": "1/4", + "note": "Rank 9 of 10 tests scales p=0.25 by 10/10 = 1." + } + ], + "properties": [ + "monotone-in-family-size: M <= M' implies bhScale M j n d <= bhScale M' j n d, for non-negative n. Adding tests never makes a q-value smaller." + ] + }, + + "permutation_test": { + "_spec": "pValue b B = (b+1)/(B+1); the naive estimator it replaces is b/B, which is a refusal at B=0 and exactly zero at b=0.", + "vectors": [ + { "b": 0, "B": 999, "p_numerator": 1, "p_denominator": 1000, "p": "1/1000", "lemma": "resolution-is-one-over-B+1" }, + { "b": 0, "B": 99, "p_numerator": 1, "p_denominator": 100, "p": "1/100", "lemma": "resolution-is-one-over-B+1" }, + { "b": 5, "B": 99, "p_numerator": 6, "p_denominator": 100, "p": "3/50", "lemma": "pValue" } + ], + "properties": [ + "never-reports-zero: 0 < pValue b B for every b and B. p = 0 is unprintable by construction, not by convention.", + "at-most-one: b <= B implies pValue b B <= 1.", + "monotone-in-extremes: b <= b' implies pValue b B <= pValue b' B.", + "naive-estimator-can-report-zero: the replaced estimator really does return exactly zero at b=0 (negative control)." + ] + }, + + "proportions": { + "_spec": "relativeAbundance c t = c/t exactly, or a named refusal, with refusals checked in the order the Julia layer checks them.", + "properties": [ + "proportions-sum-to-one: exact proportions of a sample sum to exactly 1, with no rounding in the chain.", + "zero-total-is-refused: relativeAbundance 0 0 refuses as zeroTotal.", + "zero-total-with-count-is-refused-as-exceeding: relativeAbundance (suc c) 0 refuses as countExceedsTotal, NOT zeroTotal, because count <= total is checked first. A test written from the docstring would expect the other.", + "value-has-nonzero-denominator: a returned proportion never has a zero denominator." + ] + }, + + "exact_counts": { + "_spec": "Fits k v == -2^k <= v < 2^k. checkedAdd returns the true sum if it still fits, otherwise refused overflow. There is no branch in which a wrapped value escapes.", + "properties": [ + "checkedAdd-is-exact: a returned value is the true sum; never a plausible-looking wrong total.", + "checkedAdd-never-refuses-a-sum-that-fits: the guard is not so cautious that it refuses valid work.", + "checkedAdd-refuses-exactly-when-it-must: it refuses precisely when the sum leaves the range.", + "checkedSumOf-is-exact: if a table's counts sum without overflowing, the reported total is the sum of the counts." + ] + } +}