feat(proofs): Agda formal verification of the numeric core (issue #1) - #79
Conversation
Adds a proof gate for the validated statistics layer: seven Agda modules, 77 top-level definitions, type-checked under --safe --without-K against agda-stdlib 3.0 with Agda 2.7.0.1. What is proved, and why it is not a test: * Prelude -- Outcome A = value A | refused Refusal, with outcome-total saying there is no third arm. A refactor that forgets a refusal case does not type-check. whole-is-one needs no `n =/= 0` hypothesis because Qu's denominator is `suc _`: a zero denominator is unrepresentable by type. * Proportions -- relativeAbundance refuses in the order the Julia layer checks, proportions sum to exactly 1, a returned value is c/t exactly. * ExactCounts -- checkedAdd is exact in both directions: a returned value IS the true sum, and a refusal happens exactly when the sum leaves the range. Plus the fold version, checkedSumOf-is-exact, which is what a table's total rests on. * PermutationTest -- the plus-one estimator never reports zero, for every input, alongside a proved negative control showing the estimator it replaces does. * BenjaminiHochberg -- the q-value scaling is exactly (M/(j+1))*(n/(d+1)), and a bigger family can never make a q-value smaller. * DecimalRounding -- "correctly rounded to s decimals" as a predicate over integers alone, with machine-checked known-answer vectors (0.67 for 2/3, etc.) and the tie-handling contract stated in both directions. Finding, not assumption: relativeAbundance (suc c) 0 refuses as countExceedsTotal, not zeroTotal, because exact_relative_abundance checks count <= total before iszero(total). A test written from the docstring would have asserted the other. The gate cannot pass vacuously: * proofs/bootstrap.sh pins Agda 2.7.0.1 / stdlib v3.0 and exits non-zero if it cannot install them. An absent prover is a failure, never a skip. * proofs/tests/axiom-audit.sh rejects postulates, FFI, unsound flags, holes, missing --safe, and any module not reachable from All.agda. * proofs/tests/gate-selftest.sh breaks the proofs nine ways on purpose and requires each to be rejected. Verified locally: 10/10 controls, exit 0. * .github/workflows/proofs.yml runs all three plus a check that PROOF-STATUS.md matches the tree, and uploads the transcript whether it passed or not. Everything not proved is in proofs/residue/ with an id, a precise statement, and what would close it -- including that no probability theory, no IEEE-754 semantics, and no Julia correspondence is claimed. test/fixtures/agda-known-answers.json carries the Agda-checked vectors into the Julia conformance testset: if the two disagree, the Julia layer is wrong. Verified locally: agda --safe --without-K MetaManifold/All.agda -> exit 0 with empty output; axiom-audit -> clean, 7/7 reachable; gate-selftest -> 10/10; proofs/bootstrap.sh -> OK. Not yet verified: the workflow has not executed on a GitHub runner. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Do not merge as-is —
|
…cient Three defects found by running proofs/bootstrap.sh from an empty proofs/.vendor, which is the only way to find them: 1. The pinned agda-stdlib tag `v3.0` does not exist. `git clone --branch v3.0` fails with "Could not find remote branch v3.0"; the newest tag is v2.4. The tree the proofs were developed against was a development snapshot whose own library file declares `name: standard-library-3.0`. Pinned by SHA instead (2ffa8b7d4e8e818717ad643d184f055a4d1b0447, 2026-09-12) and fetched by `git init` + `fetch --depth 1 origin <sha>`, since `--branch` cannot take one. The proofs do NOT compile against v2.4: the first failure is `Data.Integer.Properties` not exporting `_≡?_`. Recorded as R-TC-1 in proofs/residue/toolchain.residue, with the porting targets in the order they fail. This matters because `main` pins agda-stdlib 2.1 / Agda 2.6.4.3, so landing these modules there requires a port, not a version bump. 2. Agda's library-file location differs between install methods. A fresh PyPI venv reads `$XDG_CONFIG_HOME/agda/libraries`; an earlier venv read the data directory from `--print-agda-dir`. The script wrote only the latter and failed with "Library 'standard-library' not found" while the file it had just written was present and correct. It now writes both AND passes `--library-file` explicitly on every invocation, so the gate does not depend on ambient config. Recorded as R-TC-2 (closed). 3. gate-selftest.sh required `agda` on PATH and died after a successful bootstrap, because bootstrap installs into proofs/.vendor/venv. It now resolves the binary the same way bootstrap.sh does. Also: normalise the stdlib `.agda-lib` filename and `name:` field, which differ between tags (v2.1 ships `standard-library-2.1.agda-lib`). Re-verified from an empty proofs/.vendor: bootstrap.sh -> "proofs: OK" exit 0 (installs Agda from PyPI, fetches the pinned stdlib, fetches Agda source for the primitive libraries, type-checks 7 modules, audits clean); gate-selftest.sh -> 10/10 controls, exit 0. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Correction: the toolchain pin in the first push was wrong, now fixed (
|
Records what a fresh agent has to know before touching this work: that origin/main has been replaced with a single-commit history with no common ancestor to this branch and already carries an Agda suite on a different toolchain; the four concrete collisions that block a naive merge; the three traps that already cost time (stdlib has no v3.0 tag and the proofs do not compile against v2.4 or v2.1, /tmp does not survive between turns, and the self-test's own $0/$1 bug); what is proved, what is explicitly not, and the Agda syntax traps confirmed the hard way. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
1 participant
What this is
A proof gate for the validated statistics layer, as asked for on #1 and in the
follow-up direction to validate the system with Agda (Lean fallback not needed).
Seven Agda modules, 77 top-level definitions, type-checked by Agda 2.7.0.1
against agda-stdlib 3.0 under
--safe --without-K. No postulates, no foreigncode, no proof-irrelevance escape hatch.
Additive only: no existing source file's behaviour changes. The diff is new files
plus appended
Justfilerecipes, one.gitignoreentry, and a new workflow.Verified locally
agda --safe --without-K MetaManifold/All.agda(clean_build)proofs/bootstrap.sh(the repo's own entry point)proofs: OKproofs/tests/axiom-audit.sh7/7 modules reachable,clean, exit 0proofs/tests/gate-selftest.sh10/10 controls behaved correctly, exit 0Not yet verified:
.github/workflows/proofs.ymlhas not executed on a GitHubrunner. The first run of this PR's checks is its first real test. If it goes red
it will be the bootstrap step (PyPI wheel + stdlib clone + primitive libraries),
not the proofs.
What is proved, and why it is not a test
Outcome A = value A ⊎ refused Refusal, withoutcome-totalsaying there is no third arm. A refactor that forgets a refusal case does not
type-check.
whole-is-oneneeds non ≢ 0hypothesis, becauseℚᵘ'sdenominator is
suc _— a zero denominator is unrepresentable by type. That isthe exact sense in which the refusals are total, and the reason Agda was used.
relativeAbundancerefuses in the order the Julia layerchecks; proportions sum to exactly
1ℚᵘ; a returned value isc/t.checkedAddis exact in both directions: a returned valueis the true sum, and a refusal happens exactly when the sum leaves the range.
Proving one direction alone would be worthless, because each alone is satisfied
by an implementation that is useless. Plus
checkedSumOf-is-exact, the foldversion a table's total rests on.
never-reports-zeroholds for everybandB, sop = 0is unprintable by construction rather than by convention. The negativecontrol is proved alongside it:
naive-estimator-can-report-zeroshows theestimator this replaces really does return exactly zero.
(M/(j+1))·(n/(d+1)), and abigger family can never make a q-value smaller (a correction that went the
other way would reward running more tests, silently).
integers alone, no division inside the specification of rounding. Each printed
decimal is a type-checked instance;
0.67for2/3is not a number somebodytyped into two places. Tie handling is stated in both directions
(
IsRoundinghalves go down,IsRoundHalfUpup) and they are proved to agreeeverywhere else.
A finding, not an assumption
relativeAbundance (suc c) 0refuses ascountExceedsTotal, notzeroTotal—exact_relative_abundancecheckscount <= totalbeforeiszero(total). Both orders are defensible; only one is implemented. A testwritten from the docstring would have asserted the other.
The gate cannot pass vacuously
proofs/tests/gate-selftest.shbreaks the proofs nine ways on purpose (wrongknown-answer digit, reversed monotonicity, plus-one removed, zero total silently
zero, overflow no longer refused, module dropped from the gate entry, postulate
injected,
--saferemoved, tie forced the wrong way) and requires each to berejected. On its first run it reported 1/10 — because
bash -c "$mutator" "$file"binds the path to$0, so no mutation applied. The control reported"mutation did not apply" rather than passing. That is the point of having it.
Not proved
proofs/residue/carries every open obligation with an id, a precise statement,and what would close it — including
Checked.refusedinjectivity, BHnon-negativity, the step-down
minenvelope, and explicitly: no probabilitytheory, no IEEE-754 semantics, no proof that
numeric_policy.jlimplements themodel, nothing about the
:ordinarypath.q_i ≥ p_iis false in general andis deliberately absent.
The Agda-to-Julia bridge is
test/fixtures/agda-known-answers.json:Agda-checked vectors, each annotated with the lemma that fixes it, for the Julia
conformance testset to reproduce. If the two disagree, the Julia layer is wrong.
Docs
proofs/PROOF-STATUS.md— full inventory, per-module results, open obligationsdocs/statistics/formal-verification.md— reviewer-facing: what "validatedwith a proof assistant" does and does not mean here
Refs #1. Does not unblock #2 or #4, which stay gated on the full validation of
#1 and owner approval.