diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2892150..bd90fae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,23 +29,24 @@ jobs: - uses: julia-actions/julia-buildpkg@e3eb439fad4f9aba7da2667e7510e4a46ebc46e1 # v1 - uses: julia-actions/julia-runtest@6e050c8013b833b1195105ff2fce9cd802f53271 # v1 proofs: - name: Agda proofs (2.7.0.1) + name: Agda proofs (Debian 2.6.4.3, stdlib 2.1) runs-on: ubuntu-24.04 timeout-minutes: 30 + # Same recipe as MetaManifold-Evidence and residual-evidence-types: Debian's + # agda and agda-stdlib packages at exact versions inside a digest-pinned + # image. Nothing is fetched from GitHub releases or vendored by SHA; + # proofs/lib.sh refuses any other Agda. + container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132 env: - AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a + LANG: C.UTF-8 + LC_ALL: C.UTF-8 steps: - - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 - - name: Install the pinned Agda release binary + - name: Install the pinned Debian toolchain run: | - set -euo pipefail - curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" \ - https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz - echo "${AGDA_SHA256} $RUNNER_TEMP/agda.tar.xz" | sha256sum --check - tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP" - echo "Agda_datadir=$RUNNER_TEMP/Agda-v2.7.0.1/data" >> "$GITHUB_ENV" - echo "AGDA_BIN=$RUNNER_TEMP/Agda-v2.7.0.1/bin/agda" >> "$GITHUB_ENV" - - name: Type-check and axiom audit - run: proofs/bootstrap.sh - - name: Gate self-test (the gate must reject planted defects) - run: proofs/tests/gate-selftest.sh + apt-get update + apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4 + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 + with: + persist-credentials: false + - name: Proof gate (axiom audit, type-check, reject controls, gate self-test) + run: proofs/check.sh diff --git a/.gitignore b/.gitignore index 6b69765..13099ae 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,3 @@ /Manifest.toml -proofs/.vendor/ -proofs/.agda-libraries *.agdai _build/ diff --git a/README.md b/README.md index 6ef7e33..7570e96 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ q = bh_adjust([0.01, 0.04, 0.2]) # equals R's p.adjust(, "BH") ## Proved and tested are kept apart -`proofs/agda` holds machine-checked proofs (Agda 2.7.0.1, `--safe --without-K`, +`proofs/agda` holds machine-checked proofs (Debian 13's Agda 2.6.4.3 with agda-stdlib 2.1, `--safe --without-K`, no postulates) of the algebraic properties the methods rely on. Each CLR theorem is mirrored by a Julia property test. Each property test is in turn shown to reject a planted mutant (`test/mutants.jl`). The Benjamini–Hochberg step-up (P5: q ≥ p, @@ -54,7 +54,7 @@ criterion; see [`docs/R-SUNSET.md`](docs/R-SUNSET.md). ```sh julia --project -e 'using Pkg; Pkg.test()' -proofs/bootstrap.sh && proofs/tests/gate-selftest.sh # needs Agda 2.7.0.1 +proofs/check.sh # Debian 13: apt install agda agda-stdlib ``` ## Licence diff --git a/proofs/.gitignore b/proofs/.gitignore index 3d1d2a7..c60b420 100644 --- a/proofs/.gitignore +++ b/proofs/.gitignore @@ -1,7 +1,3 @@ -# Vendored Agda standard library (bootstrap.sh fetches it at the pinned SHA). -.vendor/ -# Generated by bootstrap.sh; points at absolute paths on one machine. -.agda-libraries -# Agda interface files. +# Agda interface files and the per-version build cache. _build/ *.agdai diff --git a/proofs/PROOF-STATUS.md b/proofs/PROOF-STATUS.md index 90ae738..f599bb8 100644 --- a/proofs/PROOF-STATUS.md +++ b/proofs/PROOF-STATUS.md @@ -5,8 +5,8 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) **The stdlib pin is a development SHA, not a release.** The branch's own -> library file declares `name: standard-library-3.0` and no `v3.0` tag exists. -> `proofs/bootstrap.sh` normalises the name and refuses any other revision. +> **The toolchain is the Debian 13 pin, not a vendored release.** `proofs/lib.sh` +> resolves `/usr/bin/agda` before anything on `PATH`, checks the version is +> 2.6.4.3 and the library is `standard-library-2.1`, and refuses any other. ## Gates | Gate | Command | Result | | --- | --- | --- | -| Type-check every proof, then audit | `proofs/bootstrap.sh` | PASS — exit 0, no warnings | +| Type-check every proof, audit, then self-test | `proofs/check.sh` | PASS — exit 0, no warnings | | Axiom audit on its own | `proofs/tests/axiom-audit.sh` | PASS — 7/7 modules reachable from `CompositionalDA.All`, 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 — see "Last verified" below for the count | -The CI job `proofs` in `.github/workflows/ci.yml` runs exactly those first and -third commands with `AGDA_BIN` and `Agda_datadir` set to the pinned release -tarball. `bootstrap.sh` vendors the stdlib at the pinned SHA into -`proofs/.vendor` (git-ignored) and writes `proofs/.agda-libraries`; the -self-test reads that file, so the two scripts cannot disagree about which -library they checked against. +The CI job `proofs` in `.github/workflows/ci.yml` runs `proofs/check.sh` in a +digest-pinned `debian:13-slim` container with `agda-bin=2.6.4.3-1+b2` and +`agda-stdlib=2.1-4` installed from apt. `check.sh` type-checks, audits and +then runs the self-test; both scripts resolve the prover and the library +through `proofs/lib.sh`, so they cannot disagree about what they checked +against. The exact commands, exit codes and counts of the most recent run are in "Last verified" at the end of this file. @@ -221,41 +221,42 @@ is one control per check in `axiom-audit.sh` (seven). The controls: ## Reproducing ```sh -proofs/bootstrap.sh # vendor the stdlib at the pin, type-check, audit +proofs/check.sh # type-check, audit, then the gate self-test proofs/tests/gate-selftest.sh # prove the gate rejects planted defects proofs/tests/axiom-audit.sh # the audit alone ``` -`bootstrap.sh` needs exactly `Agda version 2.7.0.1` as `AGDA_BIN` or `agda` -on `PATH`, with `Agda_datadir` pointing at the release tarball's `data/` -directory; it prints the install steps and fails if the version differs. It -does not install Agda (no package manager, no Python) and never writes into -the toolchain's data directory. **An absent prover is a failure, never a +`check.sh` needs Debian 13's `agda-bin` 2.6.4.3 and `agda-stdlib` 2.1 +(`apt install agda agda-stdlib`); `lib.sh` fails, naming the version it saw, +if anything else is found first. Nothing is downloaded and nothing is written +into the toolchain's data directory. **An absent prover is a failure, never a skip** — in CI and locally alike. ## Last verified -2026-10-02, one run of the unmodified CI interface, from an **empty** -`proofs/.vendor` (so the stdlib was fetched at the pin and type-checked from -scratch), with the release binary the CI job downloads: +2026-10-02, after rebasing onto PR #2 (`320513d`, which added `StepUp` and +the 18-control self-test), one run of the CI interface with Debian 13's +packages (`agda-bin 2.6.4.3-1+b2`, `agda-stdlib 2.1-4`), interface files +deleted first so every module was checked from source: ``` -AGDA_BIN=…/Agda-v2.7.0.1/bin/agda Agda_datadir=…/Agda-v2.7.0.1/data -proofs/bootstrap.sh → exit 0 (7 modules reachable from CompositionalDA.All; axiom-audit: clean) +proofs/check.sh → exit 0 (check: Agda version 2.6.4.3, standard-library-2.1; + axiom-audit: 7 module(s) reachable from CompositionalDA.All, clean; + CompositionalDA/All.agda type-checks; + gate-selftest: 18/18 controls behaved correctly) proofs/tests/gate-selftest.sh → exit 0 (gate-selftest: 18/18 controls behaved correctly) proofs/tests/axiom-audit.sh → exit 0 (auditing 7 module(s); axiom-audit: clean) ``` -Wall-clock 14:18:26Z → 14:22:32Z, almost all of it the stdlib. The self-test -was re-run after rebasing onto PR #1, which added the four remaining audit -controls; a planted wrong reason on one of them was reported as a FAIL -(17/18), so the reason check is live. The 18 -controls are the 14 mutations, the 3 `reject/` files and the pristine tree -listed above; each mutation was confirmed to have changed its file before the -gate was run, and each `reject/` file was refused with exit 42 and the error -its `-- EXPECT:` line names. +Wall-clock 14:58:02Z → 15:00:00Z. The only source change the 2.1 library +needed was `_≡?_` → `_≟_` on ℤ in `Prelude.agda`; `StepUp.agda` needed +none. The 18 controls are the 14 mutations, the 3 `reject/` files and the +pristine tree listed above; each mutation is confirmed to have changed its +file before the gate runs, and each `reject/` file is refused with exit 42 +and the error its `-- EXPECT:` line names. The same 18/18 was obtained on +Agda 2.7.0.1 with the stdlib development SHA at PR #2 (14:18Z–14:22Z). -The Julia side, same day: +The Julia side, same run: ``` julia --project -e 'using Pkg; Pkg.test()' → exit 0 (Test Summary: CompositionalDA | Pass 43 | Total 43) diff --git a/proofs/agda/CompositionalDA/Prelude.agda b/proofs/agda/CompositionalDA/Prelude.agda index 6eab6d0..330488e 100644 --- a/proofs/agda/CompositionalDA/Prelude.agda +++ b/proofs/agda/CompositionalDA/Prelude.agda @@ -23,7 +23,7 @@ module CompositionalDA.Prelude where open import Data.Integer as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]; _*_; _+_; _≤_) open import Data.Integer.Properties as ℤₚ - using (pos-*; pos-+; *-comm; *-zeroˡ; _≡?_; *-monoʳ-≤-nonNeg) + using (pos-*; pos-+; *-comm; *-zeroˡ; _≟_; *-monoʳ-≤-nonNeg) renaming (+-*-commutativeRing to +-*-commutativeRingℤ) open import Data.Nat.Base using (z≤n) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) @@ -44,7 +44,7 @@ open import Relation.Nullary.Decidable using (yes; no) infix 4 _≟ℚᵘ_ _≟ℚᵘ_ : Decidable _≃_ -p ≟ℚᵘ q with (↥ p * ↧ q) ≡? (↥ q * ↧ p) +p ≟ℚᵘ q with (↥ p * ↧ q) ≟ (↥ q * ↧ p) ... | yes e = yes (*≡* e) ... | no ¬e = no (λ where (*≡* e) → ¬e e) @@ -67,7 +67,7 @@ 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ℤ) _≡?_ +module ℤ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRingℤ) _≟_ open ℤ-Solver public using () renaming (solve to solve-ℤ; _:=_ to _:=ℤ_; con to conℤ; _:+_ to _:+ℤ_; _:*_ to _:*ℤ_) diff --git a/proofs/agda/compositionalda.agda-lib b/proofs/agda/compositionalda.agda-lib index 3a7e3fd..fc24539 100644 --- a/proofs/agda/compositionalda.agda-lib +++ b/proofs/agda/compositionalda.agda-lib @@ -1,4 +1,4 @@ name: compositionalda include: . -depend: standard-library +depend: standard-library-2.1 flags: --safe --without-K diff --git a/proofs/bootstrap.sh b/proofs/bootstrap.sh deleted file mode 100755 index 7ecd28a..0000000 --- a/proofs/bootstrap.sh +++ /dev/null @@ -1,244 +0,0 @@ -#!/usr/bin/env bash -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# Bootstrap and run the Agda proof gate for CompositionalDA.jl. -# -# 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 vendor the standard library only -# proofs/bootstrap.sh --check check only (fail if not bootstrapped) -# -# Environment: -# AGDA_BIN path to the agda binary to use (default: `agda` on PATH) -# PROOFS_VENDOR directory for the vendored stdlib / Agda source -# (default: proofs/.vendor, which is git-ignored) -# -# This script does NOT install Agda. The estate bans Python, so the PyPI wheel -# the MetaManifold version of this script fell back to is gone; an absent or -# wrong-version Agda is a loud failure with install instructions (see -# `check_agda_version`). -# -# Pinned versions — these are the versions the proofs were developed against. -# Agda 2.7.0.1 with stdlib 3.0-dev. 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_RELEASE_ASSET="Agda-v${AGDA_VERSION}-linux.tar.xz" -AGDA_RELEASE_URL="https://github.com/agda/agda/releases/tag/v${AGDA_VERSION}" - -# 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, `NonNegative` *instances* for `*-monoʳ-≤-nonNeg`, -# `Algebra.Properties.CommutativeMonoid.Sum.sum-permute`) 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. See -# proofs/PROOF-STATUS.md (Open obligations). -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/compositionalda.agda-lib" -ENTRY="CompositionalDA/All.agda" - -# Print a progress line on stdout, prefixed so it is distinguishable from -# Agda's own output. -log() { printf 'proofs: %s\n' "$*"; } - -# Print a fatal error on stderr and exit non-zero. Every failure in this -# script goes through here; there is no soft-fail path. -die() { printf 'proofs: FATAL: %s\n' "$*" >&2; exit 1; } - -[[ -f "$LIB_FILE" ]] || die "missing $LIB_FILE" - -############################################################################## -# Locate Agda and insist on the pinned version -############################################################################## - -# Set AGDA to the binary named by AGDA_BIN, else `agda` on PATH. Returns 1 if -# neither exists; AGDA_BIN naming a non-executable is fatal rather than skipped. -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 - return 1 -} - -# The install instructions printed whenever Agda is absent or the wrong version. -# Written once so the two failure paths cannot drift apart. -install_instructions() { - cat >&2 < -proofs: this unpacks /Agda-v$AGDA_VERSION/{bin/agda,data/} -proofs: 3. the release binary hard-codes a CI build path for its data -proofs: directory, so point it at the bundled one: -proofs: export Agda_datadir=/Agda-v$AGDA_VERSION/data -proofs: 4. run the gate with that binary: -proofs: AGDA_BIN=/Agda-v$AGDA_VERSION/bin/agda proofs/bootstrap.sh -proofs: (or put a wrapper that sets Agda_datadir on PATH as 'agda'). -EOF -} - -# Require `agda --version` to print exactly the pinned version. Anything else — -# a newer Agda, an older one, a binary that cannot run — is fatal. A proof -# checked by a different prover version than the one it was developed against -# is not the same evidence, and this gate does not pretend otherwise. -check_agda_version() { - local reported - reported="$("$AGDA" --version 2>&1 | head -n 1 || true)" - if [[ "$reported" != "Agda version $AGDA_VERSION" ]]; then - install_instructions - die "need 'Agda version $AGDA_VERSION'; '$AGDA --version' printed '${reported:-}'" - fi -} - -############################################################################## -# Vendor the standard library and the Agda primitive libraries -############################################################################## - -# Fetch agda-stdlib at exactly STDLIB_VERSION into $VENDOR/agda-stdlib and -# normalise its library file to `name: standard-library`, which is what the -# `depend:` clause of compositionalda.agda-lib refers to. An existing checkout -# is verified against the pin rather than trusted. -vendor_stdlib() { - if [[ -f "$VENDOR/agda-stdlib/standard-library.agda-lib" ]]; then - local have - have="$(git -C "$VENDOR/agda-stdlib" rev-parse HEAD 2>/dev/null || true)" - [[ "$have" == "$STDLIB_VERSION" ]] \ - || die "$VENDOR/agda-stdlib is at '${have:-}', not the pinned $STDLIB_VERSION; remove it and re-run" - log "stdlib already vendored at $STDLIB_VERSION" - 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" - [[ "$(git -C "$VENDOR/agda-stdlib" rev-parse HEAD)" == "$STDLIB_VERSION" ]] \ - || die "fetched agda-stdlib is not at $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, plain - # `standard-library.agda-lib` at this SHA) and its `name:` does not always read - # `standard-library` (here it reads `standard-library-3.0`), which is what - # `defaults` and every `depend:` clause refer to. Normalise both, whatever the - # revision 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" -} - -# Make sure `Agda.Primitive` and friends are available. The release tarball -# ships them under its data directory (`data/lib/prim`), so with the pinned -# binary this is a no-op. A binary built without them is fatal: the archive -# version of this script copied them into the data directory, but that -# directory belongs to the toolchain install, not to this repo, and a gate -# must not write into it. -vendor_prims() { - local datadir - datadir="$("$AGDA" --print-agda-dir)" - if [[ -d "$datadir/lib/prim/Agda" ]]; then - log "primitive libraries present at $datadir/lib/prim" - return 0 - fi - install_instructions - die "$datadir/lib/prim has no Agda primitive libraries; use the release tarball with Agda_datadir pointed at its bundled data/" -} - -# The in-repo libraries file that check() passes to Agda via --library-file. -# Only this file is written. The MetaManifold version of this script also -# copied it into `$(agda --print-agda-dir)/lib` and `$XDG_CONFIG_HOME/agda`; -# the first writes into the toolchain install (which this repo must not touch) -# and neither is needed, because every Agda invocation in this tree names the -# libraries file explicitly. Interactive users who want `agda` to find the -# libraries without `--library-file` can copy it to `~/.config/agda/libraries` -# themselves. -AGDA_LIBRARIES_FILE="$PROOFS_DIR/.agda-libraries" - -# Write proofs/.agda-libraries listing the project library and the vendored -# stdlib, both as absolute paths. -write_agda_config() { - { - printf '%s\n' "$LIB_FILE" - printf '%s\n' "$VENDOR/agda-stdlib/standard-library.agda-lib" - } > "$AGDA_LIBRARIES_FILE" - log "wrote $AGDA_LIBRARIES_FILE" -} - -############################################################################## -# The gate itself -############################################################################## - -# Type-check the whole tree through its single entry module, then run the -# axiom audit. Both must succeed; the audit is what proves the entry module -# actually reaches every file. -check() { - resolve_agda || { install_instructions; die "agda is not on PATH and no AGDA_BIN was given"; } - check_agda_version - log "using $("$AGDA" --version) at $AGDA" - 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 CompositionalDA.All (this reaches every module in the tree)" - [[ -f "$AGDA_LIBRARIES_FILE" ]] \ - || die "$AGDA_LIBRARIES_FILE is missing; run proofs/bootstrap.sh --bootstrap first" - "$AGDA" --library-file="$AGDA_LIBRARIES_FILE" --safe --without-K "$ENTRY" - log "axiom audit" - "$PROOFS_DIR/tests/axiom-audit.sh" - log "OK" -} - -# The bootstrap half: find the prover, vendor the stdlib, write the libraries -# file. Shared by `--bootstrap` and the no-argument form. -bootstrap() { - resolve_agda || { install_instructions; die "agda is not on PATH and no AGDA_BIN was given"; } - check_agda_version - vendor_stdlib - vendor_prims - write_agda_config -} - -case "${1:-}" in - --bootstrap) - bootstrap - ;; - --check) - check - ;; - "") - bootstrap - check - ;; - *) - die "unknown argument: $1 (expected --bootstrap, --check, or nothing)" - ;; -esac diff --git a/proofs/check.sh b/proofs/check.sh new file mode 100755 index 0000000..e66afb6 --- /dev/null +++ b/proofs/check.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# The whole proof gate, in the order CI runs it: +# 1. axiom audit (--safe on every module, no postulates, FFI, unsound flags, +# trusted primitives or holes; every module reachable from All.agda) +# 2. type-check CompositionalDA/All.agda; any Agda warning is a failure +# 3. gate self-test: the three reject/ controls must fail for their stated +# reason, and each audit check must fire on a planted defect +# +# Toolchain: Debian 13's agda (2.6.4.3) and agda-stdlib (2.1), resolved by +# proofs/lib.sh. Nothing is downloaded or vendored. +# +# Usage: proofs/check.sh + +set -euo pipefail +# shellcheck source=proofs/lib.sh +source "$(dirname "${BASH_SOURCE[0]}")/lib.sh" +resolve_agda +resolve_stdlib +printf 'check: %s, %s\n' "$("$AGDA" --version)" "$STDLIB_PINNED_NAME" + +"$PROOFS_DIR/tests/axiom-audit.sh" + +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT +write_libraries "$WORK/libraries" "$AGDA_DIR" +# --safe and --without-K come from compositionalda.agda-lib, so a module cannot +# opt out of them; they are repeated here so the command line says what it does. +( cd "$AGDA_DIR" && "$AGDA" --library-file="$WORK/libraries" --safe --without-K "$ENTRY" ) 2>&1 | tee "$WORK/typecheck.log" +if grep -qiE '^warning|^[^ ].*: *warning' "$WORK/typecheck.log"; then + die "Agda emitted warnings" +fi +printf 'check: %s type-checks\n' "$ENTRY" + +"$PROOFS_DIR/tests/gate-selftest.sh" +printf 'check: OK\n' diff --git a/proofs/lib.sh b/proofs/lib.sh new file mode 100644 index 0000000..5fc9020 --- /dev/null +++ b/proofs/lib.sh @@ -0,0 +1,58 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# shellcheck shell=bash +# shellcheck disable=SC2034 # the variables set here are consumed by the scripts that source this file +# +# Shared toolchain resolution for the proof scripts. Sourced, not executed. +# +# The proofs are checked against one pinned toolchain: Agda 2.6.4.3 and +# agda-stdlib 2.1, which are exactly Debian 13 (trixie)'s `agda` and +# `agda-stdlib` packages. Any other Agda is refused rather than tried, because +# "it type-checked on something" is not the claim being made. This is the same +# contract as ExactCounts.jl's proofs/lib.sh; the two are kept textually close +# on purpose so a fix to one is a fix to the other. +# +# AGDA_BIN path to an agda binary (default: /usr/bin/agda, then PATH) +# AGDA_STDLIB_LIB path to standard-library.agda-lib +# (default: /usr/share/agda-stdlib/standard-library.agda-lib) +# +# Why /usr/bin/agda is tried BEFORE PATH: a developer machine may carry a newer +# Agda earlier on PATH (this estate does: 2.7.0.1 under tools/provers-solvers). +# Taking "whatever `agda` resolves to" is how these proofs first came to depend +# on an untagged stdlib development SHA. + +PROOFS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +AGDA_DIR="$PROOFS_DIR/agda" +AGDA_PINNED_VERSION="2.6.4.3" +STDLIB_PINNED_NAME="standard-library-2.1" +ENTRY="CompositionalDA/All.agda" + +# Print an error naming the calling script and exit non-zero. +die() { printf '%s: FATAL: %s\n' "$(basename "$0")" "$*" >&2; exit 1; } + +# Set AGDA to the pinned Agda binary, or die naming what was found instead. +resolve_agda() { + local cand found="" + for cand in "${AGDA_BIN:-}" /usr/bin/agda "$(command -v agda 2>/dev/null || true)"; do + [[ -n "$cand" && -x "$cand" ]] || continue + if [[ "$("$cand" --version 2>/dev/null)" == "Agda version $AGDA_PINNED_VERSION" ]]; then + AGDA="$cand" + return 0 + fi + found+=" $cand=($("$cand" --version 2>/dev/null))" + done + die "Agda $AGDA_PINNED_VERSION not found (apt install agda, or set AGDA_BIN); saw:${found:- nothing}" +} + +# Set STDLIB_LIB to the pinned standard library's .agda-lib file, or die. +resolve_stdlib() { + STDLIB_LIB="${AGDA_STDLIB_LIB:-/usr/share/agda-stdlib/standard-library.agda-lib}" + [[ -f "$STDLIB_LIB" ]] || die "standard library not found at $STDLIB_LIB (apt install agda-stdlib, or set AGDA_STDLIB_LIB)" + grep -qx "name: $STDLIB_PINNED_NAME" "$STDLIB_LIB" \ + || die "$STDLIB_LIB is not $STDLIB_PINNED_NAME: $(grep -m1 '^name:' "$STDLIB_LIB")" +} + +# Write an Agda libraries file for the proof tree rooted at $2 into path $1. +write_libraries() { + printf '%s\n%s\n' "$2/compositionalda.agda-lib" "$STDLIB_LIB" > "$1" +} diff --git a/proofs/tests/gate-selftest.sh b/proofs/tests/gate-selftest.sh index 12a73d4..b2bc322 100755 --- a/proofs/tests/gate-selftest.sh +++ b/proofs/tests/gate-selftest.sh @@ -25,55 +25,15 @@ # # Usage: proofs/tests/gate-selftest.sh # -# Environment (same interface as proofs/bootstrap.sh): -# AGDA_BIN path to the agda binary (default: `agda` on PATH) -# PROOFS_VENDOR where bootstrap.sh vendored the stdlib (default: proofs/.vendor) +# Toolchain: Debian 13's Agda 2.6.4.3 and agda-stdlib 2.1, resolved by +# proofs/lib.sh (nothing is vendored; an absent or wrong prover is a failure). set -uo pipefail -PROOFS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +# shellcheck source=proofs/lib.sh +source "$(dirname "${BASH_SOURCE[0]}")/../lib.sh" NAMESPACE="CompositionalDA" LIB_BASENAME="compositionalda.agda-lib" -VENDOR="${PROOFS_VENDOR:-$PROOFS_DIR/.vendor}" - -# Print a fatal error on stderr and exit 1. Every setup failure goes through -# here; a self-test that cannot run must not look like a self-test that passed. -die() { printf 'gate-selftest: FATAL: %s\n' "$*" >&2; exit 1; } - -# Set AGDA from AGDA_BIN or PATH, the same way bootstrap.sh does. There is no -# vendored-binary fallback: the estate installs Agda from the release tarball, -# and an absent prover is a failure here, not a skip. -resolve_agda() { - if [[ -n "${AGDA_BIN:-}" ]]; then - AGDA="$AGDA_BIN" - elif command -v agda >/dev/null 2>&1; then - AGDA="$(command -v agda)" - else - die "agda not found (run proofs/bootstrap.sh, or set AGDA_BIN)" - fi - [[ -x "$AGDA" ]] || die "$AGDA is not executable" -} - -# Set STDLIB_LIBS to the library files the gate depends on, read from the -# `proofs/.agda-libraries` that bootstrap.sh wrote (every line except the -# project's own library file). Falls back to the conventional vendored -# location if that file is absent, and fails if neither exists. -resolve_stdlib() { - STDLIB_LIBS=() - local libs_file="$PROOFS_DIR/.agda-libraries" line - if [[ -f "$libs_file" ]]; then - while IFS= read -r line; do - [[ -z "$line" ]] && continue - [[ "$(basename "$line")" == "$LIB_BASENAME" ]] && continue - [[ -f "$line" ]] || die "$libs_file names $line, which does not exist" - STDLIB_LIBS+=("$line") - done < "$libs_file" - elif [[ -f "$VENDOR/agda-stdlib/standard-library.agda-lib" ]]; then - STDLIB_LIBS+=("$VENDOR/agda-stdlib/standard-library.agda-lib") - fi - [[ ${#STDLIB_LIBS[@]} -gt 0 ]] \ - || die "standard library not found; run proofs/bootstrap.sh first" -} resolve_agda resolve_stdlib @@ -99,10 +59,7 @@ reset_tree # Point Agda at the *copy*: without this the library file would resolve # `CompositionalDA.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' "$WORK/agda/$LIB_BASENAME" - printf '%s\n' "${STDLIB_LIBS[@]}" -} > "$WORK/libraries" +write_libraries "$WORK/libraries" "$WORK/agda" # Type-check the copy's entry module with the gate's exact flags. Output goes # to $WORK/out.txt; the exit status is the verdict.