diff --git a/.github/workflows/echidna-verify.yml b/.github/workflows/echidna-verify.yml index d5376c4..665be19 100644 --- a/.github/workflows/echidna-verify.yml +++ b/.github/workflows/echidna-verify.yml @@ -11,7 +11,11 @@ # That copy there is now a presence-guard no-op because the corpus was # evicted here; this workflow is the authoritative gate, so unlike the # standards original — which downgraded failures to ::warning:: — a failed -# type-check is a HARD failure here. +# type-check is a HARD failure here. The first run of this port proved why +# that matters: Ubuntu's apt agda-stdlib ships no .agda-lib manifest at all, +# so the standards-style "find *.agda-lib" registration silently finds +# nothing; scripts/prove-agda.sh detects both layouts and FAILS when it +# can't see the stdlib instead of proceeding vacuously. # # Design notes carried from issue #4 deliberately: # 1. No workflow-level `paths:` filter on pull_request. If this context is @@ -22,6 +26,12 @@ # 2. Never exit 0 on a missing corpus: the file count is asserted before # anything is reported, so this repo cannot inherit the fail-open gate # that hid the strand in standards. +# +# Runner is pinned to ubuntu-24.04 rather than ubuntu-latest: the gate pins +# its toolchain to apt agda 2.6.4.x + agda-stdlib 1.7.2 semantics (see +# proofs/echidna.toml), and ubuntu-latest moves to Ubuntu 26 on 2026-10-19 +# (runner-images #14748). Upgrading means deliberately re-verifying the +# corpus against the newer stdlib, not getting it in via a label rename. name: Echidna Proof Verification @@ -30,7 +40,8 @@ on: branches: [main] paths: - 'proofs/**' - - 'scripts/audit-trust-base.py' + - 'scripts/prove-agda.sh' + - 'scripts/audit-trust-base.sh' - '.github/workflows/echidna-verify.yml' # NO path filter on pull_request — see design note 1 above. pull_request: @@ -55,7 +66,7 @@ jobs: detect-proof-changes: timeout-minutes: 5 name: Detect proof changes - runs-on: ubuntu-latest + runs-on: ubuntu-24.04 outputs: proofs: ${{ steps.check.outputs.proofs }} steps: @@ -77,7 +88,7 @@ jobs: echo "::warning::diff failed; verifying conservatively" echo "proofs=true" >> "$GITHUB_OUTPUT"; exit 0 fi - if printf '%s\n' "$changed" | grep -qE '^(proofs/|scripts/audit-trust-base\.py$|\.github/workflows/echidna-verify\.yml$)'; then + if printf '%s\n' "$changed" | grep -qE '^(proofs/|scripts/(prove-agda|audit-trust-base)\.sh$|\.github/workflows/echidna-verify\.yml$)'; then echo "proofs=true" >> "$GITHUB_OUTPUT" else echo "proofs=false" >> "$GITHUB_OUTPUT" @@ -87,8 +98,8 @@ jobs: name: Agda — proofs/theories needs: detect-proof-changes if: needs.detect-proof-changes.outputs.proofs == 'true' - runs-on: ubuntu-latest - timeout-minutes: 20 + runs-on: ubuntu-24.04 + timeout-minutes: 30 steps: - name: Checkout uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 @@ -100,80 +111,12 @@ jobs: sudo apt-get install -y --no-install-recommends agda agda-stdlib agda --version - - name: Register stdlib for Agda - run: | - set -euo pipefail - mkdir -p "$HOME/.agda/libraries" - touch "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults" - found=0 - while IFS= read -r lib; do - [ -n "$lib" ] || continue - grep -qxF "$lib" "$HOME/.agda/libraries/estate-stdlib" \ - || echo "$lib" >> "$HOME/.agda/libraries/estate-stdlib" - name=$(awk '$1=="name:"{print $2; exit}' "$lib") - if [ -n "$name" ] && ! grep -qxF "$name" "$HOME/.agda/defaults"; then - echo "$name" >> "$HOME/.agda/defaults" - fi - found=1 - done < <(find /usr/share/agda-stdlib -maxdepth 2 -name '*.agda-lib' 2>/dev/null | sort) - if [ "$found" != 1 ]; then - echo "::error::no *.agda-lib found under /usr/share/agda-stdlib — the agda-stdlib package layout changed; fix this step before trusting the gate" - exit 1 - fi - echo "--- registered ---" - cat "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults" - - - name: Probe stdlib visibility - run: | - set -euo pipefail - probe=$(mktemp -d) - cat > "$probe/Probe.agda" <<'EOF' - module Probe where - open import Data.Nat using (ℕ) - open import Data.Vec using (Vec) - open import Data.Float using (Float) - EOF - agda --safe "$probe/Probe.agda" >/dev/null - echo "stdlib probe OK (Data.Nat / Data.Vec / Data.Float resolve under --safe)" - - - name: "Corpus presence (fail-closed, issue #4 note 2)" - run: | - set -euo pipefail - mapfile -t FILES < <(find proofs/theories -name '*.agda' | sort) - echo "Agda corpus files: ${#FILES[@]}" - printf ' %s\n' "${FILES[@]}" - if [ "${#FILES[@]}" -lt 1 ]; then - echo "::error::proofs/theories contains no .agda files — refusing to report success with an empty corpus" - exit 1 - fi - - - name: Type-check proofs - run: | - set -eo pipefail - failed="" - : > agda-verify.log - while IFS= read -r f; do - if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then - flags="--safe --without-K" - else - flags="--without-K" - echo "note: $f is the quarantined trust base (compiled without --safe by design)" - fi - echo "--- checking $f ($flags) ---" - if ! agda $flags -i proofs/theories "$f" >> agda-verify.log 2>&1; then - echo "::error::agda type-check FAILED for $f" - failed="$failed$f"$'\n' - tail -n 40 agda-verify.log - fi - done < <(find proofs/theories -name '*.agda' | sort) - if [ -n "$failed" ]; then - printf 'Failed files:\n%s' "$failed" - exit 1 - fi - echo "All Agda proofs type-checked cleanly under the enforced flags." + - name: Type-check proofs (stdlib probe + fail-closed corpus + per-module flags) + shell: bash + run: sh scripts/prove-agda.sh 2>&1 | tee agda-verify.log - name: Trust-base audit - run: python3 scripts/audit-trust-base.py + run: sh scripts/audit-trust-base.sh - name: Postulate census (advisory listing for the run log) run: | diff --git a/.gitignore b/.gitignore index 46d6186..d213a10 100644 --- a/.gitignore +++ b/.gitignore @@ -68,7 +68,9 @@ build/ # Agda (interfaces + MAlta/compile artifacts emitted by `agda --safe` checks) *.ai +*.agdai *.agda-ir/ +/agda-compile-dir/ /proofs/verification-results.json /proofs/reports/ diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1d0973d..bd26e99 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -176,37 +176,15 @@ proof-verification: DEBIAN_FRONTEND: "noninteractive" script: - apt-get update -qq - - apt-get install -y -qq --no-install-recommends agda agda-stdlib python3 findutils - - | - set -eu - mkdir -p "$HOME/.agda/libraries" - touch "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults" - found=0 - for lib in $(find /usr/share/agda-stdlib -maxdepth 2 -name '*.agda-lib' | sort); do - echo "$lib" >> "$HOME/.agda/libraries/estate-stdlib" - name=$(awk '$1=="name:"{print $2; exit}' "$lib") - [ -n "$name" ] && echo "$name" >> "$HOME/.agda/defaults" - found=1 - done - [ "$found" = 1 ] || { echo "ERROR: no agda-stdlib .agda-lib found"; exit 1; } - - | - set -eu - FILES=$(find proofs/theories -name '*.agda' | sort) - [ -n "$FILES" ] || { echo "ERROR: empty Agda corpus under proofs/theories"; exit 1; } - failed="" - for f in $FILES; do - if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then flags="--safe --without-K"; else flags="--without-K"; fi - echo "--- checking $f ($flags) ---" - agda $flags -i proofs/theories "$f" || failed="$failed $f" - done - [ -z "$failed" ] || { echo "FAILED:$failed"; exit 1; } - - python3 scripts/audit-trust-base.py + - apt-get install -y -qq --no-install-recommends agda agda-stdlib + - sh scripts/prove-agda.sh + - sh scripts/audit-trust-base.sh allow_failure: true rules: - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH changes: - proofs/** - - scripts/audit-trust-base.py + - scripts/audit-trust-base.sh - .gitlab-ci.yml # ============================================================================= diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 8ddb168..a088677 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 == [Unreleased] === Added +- Trust-base redesign after PR #18 review: `plogp`/`klTerm` now carry a + strict positivity guard (`0.0 <ᵇ v`) internally, making them NaN-safe by + construction; the refutable `mul-sign`/`log₂-nonpos` pair is replaced by a + single honest per-entry axiom `plogp-nonneg` (trust base 6 → 5 postulates) +- `docs/proof-debt.md` — estate Trusted-Base Reduction Policy ledger for the + corpus (§(a) discharged, §(c) necessary axioms, §(d) dated conjectures), + satisfying the governance `Trusted-base reduction policy` job (was red on + main since the pre-2026 corpus) via `AXIOM:`/`TRUSTED:` leading comments on + each `postulate` block - Agda proof verification CI (`.github/workflows/echidna-verify.yml`, resolving issue #4): hard-failing `agda --safe` type-check over `proofs/theories`, fail-closed corpus assertion, and a trust-base audit @@ -32,6 +41,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - AsciiDoc documentation === Changed +- CI gate scripts are now POSIX shell (`scripts/prove-agda.sh`, + `scripts/audit-trust-base.sh`) — Python is banned in estate repos by the + language policy; the gate flags `::error::` annotations per failing file, + probes the apt `agda-stdlib` layout (which ships no `.agda-lib` manifest), + pins correctness jobs to `ubuntu-24.04` (not floating `ubuntu-latest`), + and treats a failed diff as "verify" conservatively - `Distribution` now carries range and normalisation hypotheses with a computational float order `_≤ᶠ_` (fixes the vacuous where-clause relations identified in POSTULATE-AUDIT; refutable-as-stated versions removed) diff --git a/Justfile b/Justfile index b96cc21..caa034d 100644 --- a/Justfile +++ b/Justfile @@ -157,31 +157,11 @@ prove: # Type-check the Agda corpus exactly like CI (.github/workflows/echidna-verify.yml). # Needs: apt install agda agda-stdlib (or nix-shell -p agda agdaPackages.stdlib) prove-agda: - #!/usr/bin/env bash - set -euo pipefail - command -v agda >/dev/null 2>&1 || { echo "agda not found — install it (apt install agda agda-stdlib) first"; exit 1; } - failed="" - while IFS= read -r f; do - if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then - flags="--safe --without-K" - else - flags="--without-K" - echo "note: $f is the quarantined trust base (compiled without --safe by design)" - fi - echo "--- checking $f ($flags) ---" - if ! agda $flags -i proofs/theories "$f"; then - failed="$failed$f"$'\n' - fi - done < <(find proofs/theories -name '*.agda' | sort) - if [ -n "$failed" ]; then - printf 'FAILED:\n%s' "$failed" - exit 1 - fi - echo "All Agda proofs type-checked cleanly." + sh scripts/prove-agda.sh # Audit the trust base (postulate quarantine vs proofs/trust-base.json) prove-audit: - python3 scripts/audit-trust-base.py + sh scripts/audit-trust-base.sh # Local mirror of the CI gate: type-check + trust-base audit prove-check-all: prove-agda prove-audit diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..3c553a2 --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,92 @@ + + +# Proof debt + +Corpus: `proofs/theories/` (Agda). Single quarantined trust base: +`proofs/theories/InformationTheory/Axioms.agda`. All other modules compile +with `agda --safe`, which itself rejects `postulate` — so this ledger and +the file it describes can never silently diverge from what the checker +accepts (the CI job in `.github/workflows/echidna-verify.yml` enforces +set-equality against `proofs/trust-base.json` in both directions). + +## (a) Discharged in this repo + +- `entropy-nonnegative` (pre-2026 `information_theory.agda`, 2026-04 audit + Phase 2 #2) — **discharged 2026-10-04** as `InformationTheory.entropy-nonneg`: + proven by induction over the vector sum from the guarded entry function; + see PR #18. +- `js-symmetric` (audit Phase 2 #1) — **discharged 2026-10-04** as + `InformationTheory.js-symmetric`: midpoint swap via `add-comm`, no + associativity required; see PR #18. +- `log₂`, `_*f_`, `_+f_`, `negateF`, `_/f_` (the 2024 baseline's five "FFI + axiom" float ops) — **discharged 2026-10-04** by definition: they are + re-exports of `Agda.Builtin.Float` primitives through `Data.Float`, not + postulates. A re-export is not a trust assumption. + +## (b) Budgeted — tested with refutation budget + +- (none) + +## (c) Necessary axiom + +- `proofs/theories/InformationTheory/Axioms.agda` — `plogp-nonneg` + - **Kind**: IEEE-754 property of the guarded entropy term (post-log + multiplication non-negativity on [0,1]); not derivable in intensional + type theory over opaque float primitives. + - **Justification**: true of correctly-rounded IEEE `log`, `*`, `-`; the + guard (`0.0 <ᵇ v` in `Foundations.plogp`) makes the out-of-domain side + evaluate to exactly `0.0`, so the statement is non-refutable by + evaluation (no `0·(−∞) = NaN` witness — see PR #18 review, where an + earlier unguarded formulation was caught refutable at v = 0). + - **Citation**: equivalent real-analysis statement in + `agda-real`/Coq stdlibs; float-side sign law: IEEE-754 §6.3 exact + rounding of operations preserving operand sign. +- `proofs/theories/InformationTheory/Axioms.agda` — `add-nonneg` + - **Kind**: closure of non-negative floats (including +∞) under + correctly-rounded addition; NaN excluded by the hypotheses themselves. + - **Justification / Citation**: IEEE-754 §6.3 + §7.2; no associativity + is assumed anywhere (only the binary law is postulated). +- `proofs/theories/InformationTheory/Axioms.agda` — `add-comm` + - **Kind**: bitwise commutativity of correctly-rounded float addition. + - **Justification**: holds for every IEEE-754 operand pair including + NaN payload propagation and the ±0 corners under round-to-nearest; + used by `js-symmetric` only. + - **Citation**: IEEE-754-2019 §6.3 (each operation returns the rounded + exact result, which is symmetric in its two operands for `+`). + +## (d) DEBT — actively to be closed + +- `proofs/theories/InformationTheory/Axioms.agda` — `kl-nonneg` (class + `conjecture`) + - **Owner**: @hyperpolymath + - **Plan**: discharge over a reals model (agda-real or an internal ℝ + formalisation): Gibbs via the log-sum inequality, then bridge to float + with explicit rounding-tolerance lemmas against `Distribution`'s + `normalised : sumF values ≡ 1.0` (the bridge is where the corpus + should get *stronger*: as stated it is true modulo ≤ 1 ulp of slack; + an exact-float version would need compensated summation in `Foundations.sumF`). + - **Deadline**: 2027-03-31 (estate proof-debt epic + hyperpolymath/standards#124 sweep boundary) +- `proofs/theories/InformationTheory/Axioms.agda` — `js-bounded` (class + `conjecture`) + - **Owner**: @hyperpolymath + - **Plan**: Lin (1991) upper bound 1 bit + non-negativity via + `kl-nonneg` after that discharges (JSD is an average of two KLs); the + upper-bound half additionally needs the monotonicity bridge, same + rounding machinery as `kl-nonneg`. + - **Deadline**: 2027-03-31 (inherits from `kl-nonneg` above) diff --git a/proofs/POSTULATE-AUDIT.adoc b/proofs/POSTULATE-AUDIT.adoc index 58abeaf..c75b927 100644 --- a/proofs/POSTULATE-AUDIT.adoc +++ b/proofs/POSTULATE-AUDIT.adoc @@ -11,42 +11,66 @@ The corpus was rebuilt around a quarantined trust base. All postulates now live in exactly one module — `InformationTheory/Axioms.agda`, compiled without `--safe` because Agda's `--safe` rejects `postulate` (Agda test `SafeFlagPostulate`) — and every one of them is tagged, named, classified, -and budget-enforced against `{manifest}` by `scripts/audit-trust-base.py` in +and budget-enforced against `{manifest}` by `scripts/audit-trust-base.sh` in CI (`.github/workflows/echidna-verify.yml`, issue #4). -The audit now contains **6 postulates**: +The audit now contains **5 postulates**: -- **4 legitimate IEEE-754 `ffi-fact` axioms** (true facts about +- **3 legitimate IEEE-754 `ffi-fact` axioms** (true facts about correctly-rounded float ops that Agda cannot derive from opaque primitives) - **2 `conjecture` axioms** (Gibbs' inequality and Lin's JSD bound lifted to floats — honest open debt, never used by the proven theorems) - **0 uninterpreted where-clause relations** — the 2026-04 correctness bug is structurally impossible now (see below) +Every axiom is also mirrored with a full ledger entry in +`docs/proof-debt.md` in the estate Trusted-Base Reduction Policy +schema, and each `postulate` keyword in the quarantine carries the +policy-mandated `AXIOM:`/`TRUSTED:` leading comment — `standards`' +`check-trusted-base.sh` (the governance `Trusted-Base reduction policy` job) +walks those blocks, so the two enforcement regimes (local budget audit + +estate ledger) fail closed on the same atoms. + [cols="3,2,3,2",options="header"] |=== | Axiom | Class | Statement (roughly) | Why axiom -| `log₂-nonpos` | ffi-fact | 0 ≤ v ≤ 1 → log₂ v ≤ 0 (IEEE, incl. v = 0 → −∞) -| Float `log` is a runtime primitive; no real-analysis model in scope -| `mul-sign` | ffi-fact | a ≥ 0 ∧ b ≤ 0 → −(a·b) ≥ 0 (correctly-rounded ×) -| Sign/rounding law of IEEE multiplication +| `plogp-nonneg` | ffi-fact | v ∈ [0,1] → 0 ≤ −(v·log₂ v) for the *guarded* + `Foundations.plogp` (out-of-guard side computes exactly 0.0) +| Sign/rounding law of IEEE `log`, `÷`, `*`, `-` composition; Agda has no + real-analysis model over the opaque float builtins | `add-nonneg` | ffi-fact | a ≥ 0 ∧ b ≥ 0 → a + b ≥ 0 | Same, for addition (no associativity is ever claimed) | `add-comm` | ffi-fact | a + b ≡ b + a (bitwise) | IEEE addition is commutative even under rounding; NaN payload propagation is symmetric | `kl-nonneg` | conjecture | Σ p·log₂(p/q) ≥ 0 for [0,1] entries summing to 1 -| Gibbs over reals; float rounding bridge is real proof work (Phase 2 open) +| Gibbs over reals; float rounding bridge is real proof work (docs/proof-debt.md §(d)) | `js-bounded` | conjecture | 0 ≤ JSD ≤ 1 (bits) | Lin (1991); same rounding bridge plus log-sum inequality |=== +⚠️ **The NaN trap this design closed (PR #18 review, 2026-10-04).** An +earlier revision postulated `mul-sign : 0 ≤ a → b ≤ 0 → 0 ≤ −(a·b)` and +defined `plogp 0.0` via a non-strict zero test. Refutation: `log₂ 0 = −∞`, +`0·(−∞) = NaN`, and `T (0 ≤ᵇ NaN)` is inhabited — the "axiom" was FALSE, +so the corpus would have proven `⊥`. The fix is structural, not +hypothesis-tightening: the guard `0.0 <ᵇ v` is *inside* `plogp`, so no +caller or axiom can ever observe an unguarded product, and every axiom in +the table above is now non-refutable by evaluation (each side of each +conditional is checked: see the `klTerm-zero-left`, `plogp-zero`, +`plogp-one-boundary` refl/T lemmas in `InformationTheory`). Lesson recorded +here because it generalises: *an axiom about a partially-defined FFI term is +a ⊥-generator waiting for one corner case; axiomatise guarded, total +combinators instead.* + **Discharged since the 2026-04 audit** (were postulates, now theorems proven -in `InformationTheory` using only the four `ffi-fact` axioms): +in `InformationTheory` using only the three `ffi-fact` axioms): -* `entropy-nonneg` — per-entry guard `plogpB` + `sumF` induction + - `lookup-map` transport. +* `entropy-nonneg` — guarded entry term `plogp` + `sumF` induction + + `lookup-map` transport; the top-level theorem is genuinely *proven*, only + its per-entry fact is postulated (the split POSTULATE-AUDIT Phase 2 + prescribed in 2026-04). * `js-symmetric` — `zipWith-comm` on the midpoint construction + `add-comm`; the swap never needs associativity. * The five float-arithmetic postulates from the 2024 baseline @@ -82,7 +106,7 @@ layers of gate now prevent this class: `normalised` hypotheses expressed through the *computational* order `_≤ᶠ_ := T (… ≤ᵇ …)`, so each claim evaluates against the real IEEE comparison. -2. `scripts/audit-trust-base.py` fails on any `where _≥_/_≤_ :` shape inside +2. `scripts/audit-trust-base.sh` fails on any `where _≥_/_≤_ :` shape inside the trust base, and on any untagged or off-manifest postulate. == License note (unchanged) @@ -97,12 +121,16 @@ newer PMPL-1.0-or-later), reflecting attributed third-party origin `_≤ᶠ_`/`_<ᶠ_`/`_≥ᶠ_` module-wide in `Foundations`; where-clause relations eliminated and regression-gated. -*Phase 2 — prove the 4 theorems*: **PARTIAL 2026-10-04.** `js-symmetric` and -`entropy-nonneg` are proven. `kl-nonneg` and `js-bounded` remain tagged -`conjecture` axioms — each requires real-analysis lemmas (log-sum/Jensen) -over a reals model plus a rounding bridge; `Probability`-style range + -normalisation hypotheses now make their statements *true-as-stated modulo -rounding* rather than vacuous. +*Phase 2 — prove the 4 theorems*: **2/4 PROVEN, 2/4 budgeted debt +2026-10-04.** `js-symmetric` and `entropy-nonneg` are proven top-level +theorems (entropy: induction + `lookup-map` transport over the single +per-entry `plogp-nonneg` ffi-fact — the "float lemma as auxiliary +postulate, top-level theorem proven" split this audit prescribed in 2026-04). +`kl-nonneg` and `js-bounded` remain tagged `conjecture` axioms with owner and +deadline in `docs/proof-debt.md` §(d) — each requires +real-analysis lemmas (log-sum/Jensen) over a reals model plus a rounding +bridge; `Distribution`'s range + normalisation hypotheses now make their +statements *true-as-stated modulo rounding* rather than vacuous. *Phase 3 — convert FFI postulates to trust-tagged axioms*: **DONE.** The audit asked for `@trust(level=axiom, prover=ffi, since=...)` annotations; @@ -111,7 +139,12 @@ Agda has no annotation syntax, so the mechanism is the `ECHIDNA:trust manifest equality (`{manifest}`), which is strictly stronger than comments: the tag set and the source are checked for exact bi-directional match. -*Phase 4 (new, from issue #4) — CI that type-checks this tree*: **DONE.** +*Phase 4 (new, from issue #4) — CI that type-checks this tree*: **DONE, +first green 2026-10-04** (PR #19, job `Agda — proofs/theories`: apt Agda +2.6.4 + agda-stdlib 1.7 mirror, Foundations/Axioms/theorems all type-checked; +two proof-level fixes were needed en route — the NaN-guard axiom redesign +above, and `jsdF` losing its `where` binding because Agda's unifier cannot +peel a local module, recorded in the PR #19 commit trail). Workflow ported from the stranded `standards` job with its two structural notes applied (no workflow-level `paths:` filter on `pull_request`; fail-closed corpus assertion), and with the type-check made a hard failure diff --git a/proofs/README.adoc b/proofs/README.adoc index 63cbc93..ca3be40 100644 --- a/proofs/README.adoc +++ b/proofs/README.adoc @@ -13,14 +13,18 @@ type-checked in CI by == Verified Tree and Trust Layering -The corpus is split so that everything load-bearing checks under Agda's -`--safe` flag, and the irreducible trust base is quarantined and audited: +The corpus is split so that all definitions check under Agda's `--safe` +flag, and the irreducible trust base is quarantined and audited. Theorems +live in a registered *derived* header: Agda's flag inheritance forbids a +`--safe` module from importing the quarantine, so a `--safe` claim there +would mean "no FFI axiom used" — and the audit enforces the honesty of +every file's claim in both directions: [source] ---- proofs/ ├── theories/ -│ ├── InformationTheory.agda # public module: theorems (agda --safe) +│ ├── InformationTheory.agda # public module: theorems (derived: no postulate, imports Axioms) │ ├── InformationTheory/ │ │ ├── Foundations.agda # total, postulate-free definitions (agda --safe) │ │ └── Axioms.agda # THE ONLY quarantine holding `postulate` @@ -33,14 +37,22 @@ proofs/ └── echidna.toml # multi-prover pipeline config ---- -Rules enforced by CI (`scripts/audit-trust-base.py`, one of the workflow steps): +Rules enforced by CI (`scripts/audit-trust-base.sh`, one of the workflow steps): * `postulate` may only appear in `InformationTheory/Axioms.agda`; * every axiom carries an `ECHIDNA:trust :: ` tag and must match `trust-base.json` exactly — adding, removing, renaming, or reclassifying an axiom without updating the manifest and this audit fails the build; -* every safe module must keep `{-# OPTIONS --safe ... #-}`; -* the corpus must be non-empty (a gate with nothing to check is no gate). +* every safe module must keep `{-# OPTIONS --safe ... #-}`, and every + `derived_modules` entry must *not* claim it (claiming it while importing + axioms is Agda-illegal; dropping the claim after discharging the axioms is + how a module graduates into `safe_modules`); +* the corpus must be non-empty (a gate with nothing to check is no gate); +* separately from the local audit, the estate `Trusted-Base reduction policy` + job (`standards/scripts/check-trusted-base.sh`) walks the comment block + directly above each `postulate` keyword for an `AXIOM:`/`TRUSTED:` marker — + keep those leading blocks (no blank line between marker and keyword) and + mirror every entry in `docs/proof-debt.md`. `--safe` is not decoration: since Agda 2.6.1 it rejects `postulate` outright, which is why the trust base is a separate non-safe module rather than @@ -52,8 +64,9 @@ see POSTULATE-AUDIT.adoc). *Proven in `InformationTheory`* (from IEEE-754 `ffi-fact` axioms only): -* `entropy-nonneg` — H ≥ 0 for entries in [0, 1], via per-entry - `0·log 0 = 0` guarding and a `sumF` induction. +* `entropy-nonneg` — H ≥ 0 for entries in [0, 1], via the guarded, NaN-safe + entry term `plogp` (its non-negativity on [0,1] is the one `ffi-fact` + consumed) and a `sumF` induction transporting through `lookup-map`. * `js-symmetric` — JSD(P,Q) ≡ JSD(Q,P), from commutativity of float addition and the symmetric midpoint construction. * Vector plumbing (`lookup-map`, `sumF-nonneg`, `zipWith-cong₂`, diff --git a/proofs/echidna.toml b/proofs/echidna.toml index 30ff4c6..db4717c 100644 --- a/proofs/echidna.toml +++ b/proofs/echidna.toml @@ -24,7 +24,7 @@ stdlib = true # `--safe` applies to every module EXCEPT the quarantined trust base # (theories/InformationTheory/Axioms.agda, which holds the ECHIDNA:trust # postulates and is checked with --without-K only). The split is enforced by -# scripts/audit-trust-base.py; see proofs/README.adoc. +# scripts/audit-trust-base.sh; see proofs/README.adoc. flags = ["--safe", "--without-K"] [provers.coq] diff --git a/proofs/theories/InformationTheory.agda b/proofs/theories/InformationTheory.agda index b4b0cdb..82f54ed 100644 --- a/proofs/theories/InformationTheory.agda +++ b/proofs/theories/InformationTheory.agda @@ -3,59 +3,72 @@ -- -- Information Theory — theorems -- ============================= --- The public module of the LOL information-theory formalisation --- (1000Langs/ReScript side keeps its own property tests; this tree is the --- machine-checked companion). +-- The public module of the LOL information-theory formalisation. The +-- ReScript crawler side keeps its property tests; this tree is the +-- machine-checked companion. -- -- Layering (enforced by .github/workflows/echidna-verify.yml, issue #4): -- --- InformationTheory.Foundations --safe total, postulate-free definitions +-- InformationTheory.Foundations --safe total, postulate-free definitions -- InformationTheory.Axioms not safe the only quarantine holding `postulate` --- InformationTheory (this module) --safe theorems + public surface +-- InformationTheory (this module) not safe theorems + public surface -- --- The two theorems POSTULATE-AUDIT classified as "provable" (`entropy-nonneg`, --- `js-symmetric`) are proven here — from the four IEEE-754 `ffi-fact` axioms, --- never from the `conjecture` class. `kl-nonneg` and `js-bounded` remain --- tagged conjectures (Phase 2 open), re-exported so dependents see the --- trust level. -{-# OPTIONS --safe --without-K #-} +-- This header cannot claim `--safe` even though it contains no postulates: +-- Agda's flag-inheritance rule rejects safe modules importing anything that +-- is not safe ("Importing module ... not using the --safe flag from a module +-- which does") — which is itself the proof that a `--safe` claim here would +-- mean "no FFI axioms used at all". The postulate-free property this file +-- can claim, and does, is enforced by the trust-base census (a `postulate` +-- outside Axioms.agda is a hard CI failure), and Foundations carries the +-- genuine `--safe` certificate for every definition, guard and relation the +-- theorems consume. The audit registers this file under +-- `derived_modules` in proofs/trust-base.json (registered, flagged, and +-- forbidden from silently claiming --safe without discharging its axioms). +-- +-- Both POSTULATE-AUDIT "provable" obligations are discharged here: +-- `entropy-nonneg` by induction over the vector sum from the per-entry +-- `plogp-nonneg` ffi-fact, and `js-symmetric` by rewriting the midpoint +-- with `add-comm`. Neither proof touches the `conjecture` class — +-- `kl-nonneg`/`js-bounded` stay open and are only re-exported as-is so +-- consumers see their trust level. +{-# OPTIONS --without-K #-} module InformationTheory where -open import Data.Bool.Base using (Bool; true; false; T) -open import Data.Float using (Float; _+_; _÷_; _≤ᵇ_; _≡ᵇ_) -open import Data.Fin using (Fin; zero; suc) -open import Data.Nat using (ℕ) -open import Data.Product using (_×_; _,_) -open import Data.Vec using (Vec; []; _∷_; map; zipWith; lookup) +open import Data.Float using (Float; _+_; _÷_; _≤ᵇ_; _<ᵇ_) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Vec.Base using (Vec; []; _∷_; map; zipWith; lookup) open import Data.Unit.Base using (tt) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst) open import InformationTheory.Foundations public open import InformationTheory.Axioms - using (log₂-nonpos; mul-sign; add-nonneg; add-comm; kl-nonneg; js-bounded) + using (plogp-nonneg; add-nonneg; add-comm; kl-nonneg; js-bounded) public -- ============================================================================ --- Vector plumbing +-- Vector plumbing (no axioms used in this section) -- ============================================================================ +-- `map` and `lookup` commute pointwise, definitionally. lookup-map : ∀ {n} (f : Float → Float) (xs : Vec Float n) (i : Fin n) → lookup (map f xs) i ≡ f (lookup xs i) lookup-map f [] () lookup-map f (x ∷ xs) zero = refl lookup-map f (x ∷ xs) (suc i) = lookup-map f xs i --- The float sum of a vector is non-negative when all entries are. +-- A vector sum is non-negative when every entry is. Right-association of +-- `sumF` matches the fold the pre-2026 corpus used, so the computation is +-- observationally identical while this proof only needs the binary closure +-- fact `add-nonneg` at each step. sumF-nonneg : ∀ {n} (xs : Vec Float n) → (∀ {i : Fin n} → 0.0 ≤ᶠ lookup xs i) → 0.0 ≤ᶠ sumF xs sumF-nonneg [] h = tt sumF-nonneg (x ∷ xs) h = add-nonneg x (sumF xs) (h {zero}) (sumF-nonneg xs λ { {i} → h {suc i} }) --- Pointwise equality transports through zipWith, and a commutative pointwise --- function makes zipWith itself symmetric in its arguments. +-- Pointwise equality transports through zipWith… zipWith-cong₂ : ∀ {n} (f g : Float → Float → Float) → (∀ x y → f x y ≡ g x y) → (xs ys : Vec Float n) → @@ -63,6 +76,8 @@ zipWith-cong₂ : ∀ {n} (f g : Float → Float → Float) → zipWith-cong₂ f g h [] [] = refl zipWith-cong₂ f g h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (h x y) (zipWith-cong₂ f g h xs ys) +-- …and a pointwise-commutative function makes zipWith symmetric in its +-- arguments (the shape the JSD midpoint needs). zipWith-comm : (f : Float → Float → Float) → (∀ x y → f x y ≡ f y x) → ∀ {n} (xs ys : Vec Float n) → @@ -71,17 +86,11 @@ zipWith-comm f h [] [] = refl zipWith-comm f h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (h x y) (zipWith-comm f h xs ys) -- ============================================================================ --- Entropy is non-negative (H ≥ 0 for p ∈ [0,1], per-entry 0·log 0 = 0) +-- Entropy is non-negative (H(X) ≥ 0 for p ∈ [0,1], 0·log 0 = 0 convention) -- ============================================================================ - --- Per-entry fact: the guarded −v·log₂ v is non-negative on [0,1]. -plogpB-nonneg : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → - (b : Bool) → 0.0 ≤ᶠ plogpB v b -plogpB-nonneg v lv lu true = tt -plogpB-nonneg v lv lu false = mul-sign v (log₂ v) lv (log₂-nonpos v lv lu) - -plogp-nonneg : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → 0.0 ≤ᶠ plogp v -plogp-nonneg v lv lu = plogpB-nonneg v lv lu (v ≡ᵇ 0.0) +-- Proven top-level theorem (POSTULATE-AUDIT Phase 2 #2): the only external +-- fact consumed is the per-entry ffi-fact `plogp-nonneg`; the summation is +-- real induction. entropy-nonneg : ∀ {n} (d : Distribution n) → 0.0 ≤ᶠ entropy d entropy-nonneg {n} d = @@ -90,43 +99,46 @@ entropy-nonneg {n} d = (plogp-nonneg (lookup (values d) i) (lower d {i}) (upper d {i})) } -- ============================================================================ --- Jensen-Shannon divergence is symmetric +-- Jensen-Shannon divergence is symmetric (POSTULATE-AUDIT Phase 2 #1) -- ============================================================================ +-- JSD(P,Q) = (D(P‖M) + D(Q‖M))/2 with M = (P+Q)/2. Swapping P and Q leaves M +-- fixed up to commutativity of float addition; the two KL terms then swap. +-- No associativity of + is ever needed — that is what keeps this honest for +-- IEEE-754. midpointF-comm : ∀ x y → midpointF x y ≡ midpointF y x midpointF-comm x y = cong (λ w → w ÷ 2.0) (add-comm x y) --- JSD(P,Q) = (D(P‖M) + D(Q‖M))/2 with M = (P+Q)/2. Swapping P and Q leaves M --- fixed up to commutativity of float addition, then the two KL terms swap. +-- Written pointfree-end-to-end (no `where` bindings): every intermediate +-- type is syntactically the term the δ-unfolding of `jensen-shannon` +-- produces on both sides, so unification never has to peel a local module. js-symmetric : ∀ {n} (p q : Distribution n) → jensen-shannon p q ≡ jensen-shannon q p -js-symmetric {n} p q = cong (λ w → w ÷ 2.0) (trans swapKL rezip) - where - pv qv : Vec Float n - pv = values p - qv = values q - - mm : zipWith midpointF pv qv ≡ zipWith midpointF qv pv - mm = zipWith-comm midpointF midpointF-comm pv qv - - swapKL : kl-divergenceF pv (zipWith midpointF pv qv) - + kl-divergenceF qv (zipWith midpointF pv qv) - ≡ kl-divergenceF qv (zipWith midpointF pv qv) - + kl-divergenceF pv (zipWith midpointF pv qv) - swapKL = add-comm _ _ - - rezip : kl-divergenceF qv (zipWith midpointF pv qv) - + kl-divergenceF pv (zipWith midpointF pv qv) - ≡ kl-divergenceF qv (zipWith midpointF qv pv) - + kl-divergenceF pv (zipWith midpointF qv pv) - rezip = cong₂ _+_ (cong (kl-divergenceF qv) mm) (cong (kl-divergenceF pv) mm) +js-symmetric {n} p q = cong (λ w → w ÷ 2.0) + (trans (add-comm (kl-divergenceF (values p) (zipWith midpointF (values p) (values q))) + (kl-divergenceF (values q) (zipWith midpointF (values p) (values q)))) + (cong₂ _+_ + (cong (kl-divergenceF (values q)) + (zipWith-comm midpointF midpointF-comm (values p) (values q))) + (cong (kl-divergenceF (values p)) + (zipWith-comm midpointF midpointF-comm (values p) (values q))))) -- ============================================================================ --- Sanity of the definitions themselves (no axioms used) +-- Definitional sanity of the guards (no axioms used) -- ============================================================================ --- The zero-guard on the KL term agrees with the 0·log convention at p = 0: --- `0.0 ≡ᵇ 0.0` computes to true, so the term reduces. +-- The strict positivity guard makes the KL term evaluate to exactly 0.0 at +-- p = 0 (`0.0 <ᵇ 0.0` computes to false): the 0·log 0 = 0 convention is not +-- merely asserted, it is what the function computes. klTerm-zero-left : ∀ q → klTerm 0.0 q ≡ 0.0 klTerm-zero-left q = refl +-- Same for the entropy term. +plogp-zero : plogp 0.0 ≡ 0.0 +plogp-zero = refl + +-- And the boundary p = 1 computes to −(1·log₂ 1) = −0.0, which the order +-- relation accepts (`0.0 ≤ᶠ - 0.0` holds because 0 ≤ᵇ −0.0 computes true): +-- negative zero does not break entropy-nonneg at the boundary. +plogp-one-boundary : 0.0 ≤ᶠ plogp 1.0 +plogp-one-boundary = tt diff --git a/proofs/theories/InformationTheory/Axioms.agda b/proofs/theories/InformationTheory/Axioms.agda index 68bf3ee..3cf4215 100644 --- a/proofs/theories/InformationTheory/Axioms.agda +++ b/proofs/theories/InformationTheory/Axioms.agda @@ -4,68 +4,92 @@ -- Information Theory — quarantined trust base -- ============================================ -- This is the ONLY module in the corpus allowed to contain `postulate`. --- It is deliberately compiled WITHOUT `--safe` (Agda's --safe rejects --- postulates outright — test/Fail/SafeFlagPostulate in the Agda tree), so --- the quarantine is enforced mechanically by --- .github/workflows/echidna-verify.yml (issue #4): +-- It is deliberately compiled WITHOUT `--safe`: `--safe` rejects `postulate` +-- outright (Agda test SafeFlagPostulate), so the quarantine is what lets an +-- honest trust base coexist with a hard `--safe` certificate on the +-- definitions layer (Foundations); the theorem header importing these axioms +-- is registered as `derived` — postulate-free by census, --safe-forbidden by +-- Agda's flag inheritance. +-- Enforced by .github/workflows/echidna-verify.yml (issue #4): -- -- * `grep postulate` outside this file is a hard CI failure; -- * every postulate declaration carries an `ECHIDNA:trust :: ` -- tag on the line above it; -- * names, classes and counts must match proofs/trust-base.json exactly --- (see scripts/audit-trust-base.py and proofs/POSTULATE-AUDIT.adoc). +-- (see scripts/audit-trust-base.sh and proofs/POSTULATE-AUDIT.adoc); +-- * each `postulate` keyword block is preceded, with no blank line in +-- between, by a leading comment containing `AXIOM:` or `TRUSTED:` — +-- the estate-wide marker consumed by standards' check-trusted-base.sh +-- (Trusted-Base Reduction Policy); and +-- * every entry is mirrored in docs/proof-debt.md. -- -- Classes: --- ffi-fact — a true property of correctly-rounded IEEE-754 operations --- that Agda cannot derive from its opaque Float primitives. --- Removing this file's --safe flag is what admits them; the --- theorems that consume them are still fully checked. --- conjecture — a classical theorem over the reals (Gibbs' inequality, --- Lin's JSD bound) whose float-lifted form is trusted modulo --- rounding; never discharged, only referenced. +-- ffi-fact — a true property of correctly-rounded IEEE-754 arithmetic +-- that Agda cannot derive from its opaque Float primitives. +-- conjecture — a classical theorem over the reals whose float-lifted form +-- is trusted modulo rounding; never used by any proven +-- result, only referenced (budgeted debt, deadline in +-- docs/proof-debt.md). -- --- The vacuous per-postulate `where _≥_/_≤_` relations of the original corpus --- (POSTULATE-AUDIT "Additional concerns") are gone: all statements below use --- the computational `InformationTheory.Foundations` order `_≤ᶠ_`. +-- Design invariant (the PR #18 review lesson): no axiom may be refutable by +-- evaluation. Statements therefore talk about the *guarded* terms from +-- Foundations (`plogp` is NaN-safe by construction), never about raw +-- `v * log₂ v` under non-strict hypotheses — an earlier draft postulating +-- `0 ≤ a → b ≤ 0 → 0 ≤ −(a·b)` was refutable at a = 0, b = −∞ (0·(−∞) = +-- NaN), which would have inhabited ⊥. {-# OPTIONS --without-K #-} module InformationTheory.Axioms where -open import Data.Bool.Base using (T) -open import Data.Float using (Float; _+_; _*_; _÷_; -_; _≤ᵇ_; _≡ᵇ_; _<ᵇ_) +open import Data.Float using (Float; _+_) open import Data.Product using (_×_) open import Relation.Binary.PropositionalEquality using (_≡_) open import InformationTheory.Foundations +-- Necessary foundational axioms (Trusted-Base Reduction Policy §c): true +-- facts about correctly-rounded hardware arithmetic, not proof debt. They +-- are what make the per-entry and algebraic theorems in InformationTheory +-- checkable without a full real-analysis model of the reals. +-- +-- AXIOM: ffi-facts — IEEE-754 properties of the runtime float primitives, +-- unverifiable in intensional type theory over opaque builtins. Listed with +-- rationale in proofs/POSTULATE-AUDIT.adoc and docs/proof-debt.md. postulate - -- log₂ is non-positive on [0,1]: 0 ≤ v ≤ 1 → log₂ v ≤ 0. True including - -- v = 0 (log 0 = −∞ ≤ 0) and v = NaN (hypothesis is `T false`, i.e. ⊥). - -- ECHIDNA:trust ffi-fact :: log₂-nonpos - log₂-nonpos : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → log₂ v ≤ᶠ 0.0 - - -- Sign law of correctly-rounded multiplication: a ≥ 0 ∧ b ≤ 0 → −(a·b) ≥ 0. - -- ECHIDNA:trust ffi-fact :: mul-sign - -- a > 0 excludes 0·(−∞) = NaN. - mul-sign : (a b : Float) → 0.0 <ᶠ a → b ≤ᶠ 0.0 → 0.0 ≤ᶠ - (a * b) + -- −p·log₂ p (the guarded `InformationTheory.Foundations.plogp`) is + -- non-negative on [0, 1]: the per-entry heart of entropy-nonneg. True + -- including the guarded out-of-domain side (which returns exactly 0.0) + -- and at p = 1 (result −0.0, and 0 ≤ᵇ −0.0 computes to true). + -- ECHIDNA:trust ffi-fact :: plogp-nonneg + plogp-nonneg : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → 0.0 ≤ᶠ plogp v - -- Non-negative floats are closed under correctly-rounded addition. + -- Non-negative floats are closed under correctly-rounded addition + -- (including +∞: NaN inputs fail the hypotheses, so no side condition). -- ECHIDNA:trust ffi-fact :: add-nonneg add-nonneg : (a b : Float) → 0.0 ≤ᶠ a → 0.0 ≤ᶠ b → 0.0 ≤ᶠ a + b - -- Correctly-rounded addition is commutative as a bitwise operation (only - -- associativity fails IEEE-754). Consumed by js-symmetric. + -- Correctly-rounded addition is commutative as a *bitwise* operation (only + -- associativity fails IEEE-754; under round-to-nearest, x + y and y + x + -- produce the identical value, including NaN payload propagation and the + -- ±0 corner: +0 + −0 = +0 = −0 + +0). Consumed by js-symmetric. -- ECHIDNA:trust ffi-fact :: add-comm add-comm : (a b : Float) → a + b ≡ b + a - -- Gibbs' inequality lifted to float sums. Kept a conjecture on purpose: - -- the real-analysis proof (log-sum inequality over reals) plus a rounding - -- bridge is out of scope; see POSTULATE-AUDIT remediation Phase 2. +-- Budgeted, dated proof debt (Trusted-Base Reduction Policy §d): classical +-- results over the reals (Gibbs' inequality via the log-sum inequality; +-- Lin 1991 JSD bounds) whose float-lifted forms need a rounding bridge on +-- top of a reals model. `Distribution`'s hypotheses (entries in [0, 1] via +-- the comparison primitives, `normalised` float sum) keep these statements +-- true-as-stated-modulo-rounding rather than vacuous or refutable — the +-- 2026-04 corpus failed on exactly this axis. See docs/proof-debt.md §(d). +-- +-- TRUSTED: enumerated as budgeted debt, owner + deadline in +-- docs/proof-debt.md; discharging either axiom must land with the matching +-- manifest and audit updates (scripts/audit-trust-base.sh fails otherwise). +postulate -- ECHIDNA:trust conjecture :: kl-nonneg kl-nonneg : ∀ {n} (p q : Distribution n) → 0.0 ≤ᶠ kl-divergence p q - -- Lin (1991): 0 ≤ JSD ≤ 1 in bits, lifted to float arithmetic. Same - -- rationale as kl-nonneg. -- ECHIDNA:trust conjecture :: js-bounded js-bounded : ∀ {n} (p q : Distribution n) → 0.0 ≤ᶠ jensen-shannon p q × jensen-shannon p q ≤ᶠ 1.0 diff --git a/proofs/theories/InformationTheory/Foundations.agda b/proofs/theories/InformationTheory/Foundations.agda index a17fb64..cf71c39 100644 --- a/proofs/theories/InformationTheory/Foundations.agda +++ b/proofs/theories/InformationTheory/Foundations.agda @@ -15,12 +15,12 @@ module InformationTheory.Foundations where -open import Data.Bool.Base using (Bool; true; false; T; if_then_else_) +open import Data.Bool.Base using (T; if_then_else_) open import Data.Float public - using (Float; _+_; _*_; _÷_; -_; log; _≤ᵇ_; _≡ᵇ_; _<ᵇ_) -open import Data.Fin using (Fin) + using (Float; _+_; _*_; _÷_; -_; log; _≤ᵇ_; _<ᵇ_) +open import Data.Fin.Base using (Fin) open import Data.Nat using (ℕ) -open import Data.Vec using (Vec; []; _∷_; map; zipWith; lookup) +open import Data.Vec.Base using (Vec; []; _∷_; map; zipWith; lookup) open import Relation.Binary.PropositionalEquality using (_≡_) -- ============================================================================ @@ -52,23 +52,26 @@ x ≥ᶠ y = y ≤ᶠ x log₂ : Float → Float log₂ v = log v ÷ log 2.0 --- −p·log₂ p with the usual 0·log 0 = 0 convention. The zero-test result is --- an explicit Boolean argument so downstream theorems can case-analyse it --- without stuck with-abstraction on a Float primitive; `plogp` is the entry --- point used in definitions. -plogpB : Float → Bool → Float -plogpB v b = if b then 0.0 else - (v * log₂ v) - +-- −p·log₂ p with the usual 0·log 0 = 0 convention. +-- +-- The guard is *strict positivity* (0.0 <ᵇ v), not a zero test. Reason (the +-- PR #18 review lesson): under IEEE-754, `0 * log₂ 0 = 0 * (−∞) = NaN`, so a +-- definition that branches on `v ≡ᵇ 0.0` computes NaN for ±0/−∞-adjacent +-- inputs and any axiom of the shape "0 ≤ v → … → 0 ≤ −(v·log₂v)" becomes +-- refutable at v = 0 — a refutable axiom inhabits ⊥ and proves everything, +-- which is exactly the class of bug this rebuild set out to kill. With the +-- strict guard, the out-of-domain side of the conditional *is* the value the +-- convention prescribes (0.0), the function is NaN-safe for every input, and +-- the accompanying FFI axiom (InformationTheory.Axioms) needs no side +-- conditions beyond the in-band bounds. v = 1 gives −(1·0) = −0.0, and +-- `0 ≤ᵇ −0.0` computes to true, so the boundary is consistent too. plogp : Float → Float -plogp v = plogpB v (v ≡ᵇ 0.0) - --- p·log₂(p/q) for KL terms, guarding p = 0 (the q = 0 case legitimately --- yields +∞ rather than a special value). -klTermB : Float → Float → Bool → Float -klTermB p q b = if b then 0.0 else p * log₂ (p ÷ q) +plogp v = if 0.0 <ᵇ v then - (v * log₂ v) else 0.0 +-- p·log₂(p/q) for KL terms, guarded the same way. The q = 0 case with +-- p > 0 legitimately yields p·log₂(+∞) = +∞ rather than a special value. klTerm : Float → Float → Float -klTerm p q = klTermB p q (p ≡ᵇ 0.0) +klTerm p q = if 0.0 <ᵇ p then p * log₂ (p ÷ q) else 0.0 -- Pointwise (P + Q)/2, the JSD midpoint construction. midpointF : Float → Float → Float @@ -120,9 +123,15 @@ kl-divergence p q = kl-divergenceF (values p) (values q) -- Jensen-Shannon divergence on raw vectors: with M = (P + Q)/2, -- JSD = (D(P‖M) + D(Q‖M))/2. +-- The midpoint is written out in both clauses rather than bound by a +-- `where`: a where-clause of a definition becomes a local module that +-- unification cannot always unfold through when the importer also matches +-- under it (live CI evidence: "blocked on _a_" while proving js-symmetric), +-- so the construction stays fully transparent. jsdF : ∀ {n} → Vec Float n → Vec Float n → Float -jsdF ps qs = ((kl-divergenceF ps m) + (kl-divergenceF qs m)) ÷ 2.0 - where m = zipWith midpointF ps qs +jsdF ps qs = + (kl-divergenceF ps (zipWith midpointF ps qs) + + kl-divergenceF qs (zipWith midpointF ps qs)) ÷ 2.0 -- Jensen-Shannon divergence on distributions. jensen-shannon : ∀ {n} → Distribution n → Distribution n → Float diff --git a/proofs/trust-base.json b/proofs/trust-base.json index 002f43e..7aa6f1c 100644 --- a/proofs/trust-base.json +++ b/proofs/trust-base.json @@ -1,29 +1,31 @@ { "comment": [ "Machine-readable trust-base manifest for proofs/theories (issue #4).", - "Enforced by scripts/audit-trust-base.py, which runs in CI", + "Enforced by scripts/audit-trust-base.sh, which runs in CI", "(.github/workflows/echidna-verify.yml) and via `just prove-audit`.", "Any change to the Agda corpus postulates, modules, or --safe status", - "must land in the same PR as the matching change here and an entry in", - "proofs/POSTULATE-AUDIT.adoc." + "must land in the same PR as the matching change here, an entry in", + "proofs/POSTULATE-AUDIT.adoc, and the docs/proof-debt.md section for", + "the estate Trusted-Base Reduction Policy." ], "schema": 1, "quarantine": "proofs/theories/InformationTheory/Axioms.agda", "safe_modules": [ - "proofs/theories/InformationTheory.agda", "proofs/theories/InformationTheory/Foundations.agda" ], + "derived_modules": [ + "proofs/theories/InformationTheory.agda" + ], "axioms": [ - { "name": "log₂-nonpos", "class": "ffi-fact" }, - { "name": "mul-sign", "class": "ffi-fact" }, + { "name": "plogp-nonneg", "class": "ffi-fact" }, { "name": "add-nonneg", "class": "ffi-fact" }, { "name": "add-comm", "class": "ffi-fact" }, { "name": "kl-nonneg", "class": "conjecture" }, { "name": "js-bounded", "class": "conjecture" } ], "class_budget": { - "ffi-fact": 4, + "ffi-fact": 3, "conjecture": 2 }, - "total_budget": 6 + "total_budget": 5 } diff --git a/scripts/audit-trust-base.py b/scripts/audit-trust-base.py deleted file mode 100644 index 150106c..0000000 --- a/scripts/audit-trust-base.py +++ /dev/null @@ -1,193 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors -""" -audit-trust-base.py — gate the quarantined Agda trust base (issue #4). - -Single implementation shared by .github/workflows/echidna-verify.yml and -`just prove-audit`. Exits non-zero (with ::error:: annotations for Actions) -when the corpus and proofs/trust-base.json disagree in ANY direction, so a -postulate can be neither smuggled in nor silently deleted from the audit. - -Checks: - 1. Every *.agda under proofs/theories is listed in the manifest as either - the quarantine module or a safe module (no unregistered files). - 2. `postulate` may only occur in the quarantine file. - 3. Safe modules carry `--safe`; the quarantine file must NOT claim it - (Agda's --safe rejects postulates, so the claim would be dishonest - tooling rather than a sound split). - 4. Every postulate declaration is preceded (within one comment line) by an - `-- ECHIDNA:trust :: ` tag whose name matches the - declaration, class is in {ffi-fact, conjecture}, and the whole set - (names, per-class counts, total) equals the manifest exactly. - 5. Regression guard for the 2026-04 soundness bug: no per-postulate - `where _≥_/_≤_ : Float → Float → Set`-style vacuous relation clauses. - 6. Non-empty corpus (fail-closed, issue #4 note 2). -""" - -import json -import re -import sys -from pathlib import Path - -REPO_ROOT = Path(__file__).resolve().parent.parent -THEORIES = REPO_ROOT / "proofs" / "theories" -MANIFEST = REPO_ROOT / "proofs" / "trust-base.json" -ALLOWED_CLASSES = {"ffi-fact", "conjecture"} - -POSTULATE_RE = re.compile(r"^\s*postulate(\s|$)") -DECL_RE = re.compile(r"^\s+(\S+)\s+:") -TAG_RE = re.compile(r"^\s*--\s*ECHIDNA:trust\s+(\S+)\s+::\s+(\S+)\s*$") -VACUOUS_RE = re.compile(r"^\s+_[≥≤]_\s*:") - -errors: list[str] = [] - - -def err(msg: str) -> None: - errors.append(msg) - print(f"::error::{msg}") - - -def rel(p: Path) -> str: - return p.relative_to(REPO_ROOT).as_posix() - - -def main() -> int: - if not MANIFEST.is_file(): - err(f"missing manifest {rel(MANIFEST)}") - return 1 - manifest = json.loads(MANIFEST.read_text(encoding="utf-8")) - - agda_files = sorted(THEORIES.rglob("*.agda")) if THEORIES.is_dir() else [] - if not agda_files: - err("no .agda corpus under proofs/theories — a gate with nothing to " - "check is no gate (fail-closed per issue #4 note 2)") - return 1 - - quarantine = manifest.get("quarantine") - safe_modules = manifest.get("safe_modules", []) - expected = manifest.get("axioms", []) - class_budget = manifest.get("class_budget", {}) - total_budget = manifest.get("total_budget") - - listed = set(map(str, [quarantine] + list(safe_modules))) - on_disk = {rel(p) for p in agda_files} - unlisted = on_disk - listed - missing = listed - on_disk - if unlisted: - err(f".agda file(s) not registered in {rel(MANIFEST)}: " - f"{sorted(unlisted)} — add to safe_modules (or extend the " - f"quarantine deliberately) in the same PR") - if missing: - err(f"manifest lists files that do not exist: {sorted(missing)}") - - qpath = REPO_ROOT / quarantine if quarantine else None - if qpath and qpath.is_file(): - qtext = qpath.read_text(encoding="utf-8") - if "--safe" in (re.search(r"\{-# OPTIONS[^\n]*", qtext).group(0) - if re.search(r"\{-# OPTIONS[^\n]*", qtext) else ""): - err(f"{rel(qpath)}: quarantine must not declare --safe " - "(Agda rejects postulates under --safe)") - - # --tag → declaration pairing, and per-declaration postulate-block walk - lines = qtext.splitlines() - found: dict[str, str] = {} - in_postulate = False - for i, line in enumerate(lines): - if POSTULATE_RE.match(line): - in_postulate = True - continue - if line.strip() == "" or line.lstrip().startswith("--"): - continue - if in_postulate and (line.startswith((" ", "\t"))): - m = DECL_RE.match(line) - if m: - name = m.group(1) - # find tag: nearest preceding non-blank comment line pair - j = i - 1 - while j >= 0 and lines[j].strip() == "": - j -= 1 - tag = TAG_RE.match(lines[j]) if j >= 0 else None - if not tag: - err(f"{rel(qpath)}:{i + 1}: postulate `{name}` is not " - f"tagged — add `-- ECHIDNA:trust :: {name}` " - f"directly above it") - else: - cls, tname = tag.group(1), tag.group(2) - if tname != name: - err(f"{rel(qpath)}:{i + 1}: tag names `{tname}` " - f"but declares `{name}`") - if cls not in ALLOWED_CLASSES: - err(f"{rel(qpath)}:{i + 1}: class `{cls}` not in " - f"{sorted(ALLOWED_CLASSES)}") - if name in found: - err(f"duplicate postulate `{name}`") - found[name] = cls - if VACUOUS_RE.match(lines[i + 1] if i + 1 < len(lines) else ""): - err(f"{rel(qpath)}:{i + 2}: `where _≥_/_≤_ : ...` — " - f"vacuous relation regression (2026-04 audit bug)") - continue - if in_postulate and not line.startswith((" ", "\t")): - in_postulate = False - for i, line in enumerate(lines): - if VACUOUS_RE.match(line): - err(f"{rel(qpath)}:{i + 1}: vacuous where-relation " - f"(2026-04 audit regression)") - else: - err(f"quarantine file missing: {quarantine}") - - # postulate keyword may not appear outside the quarantine - for p in agda_files: - if qpath and p == qpath: - continue - for n, line in enumerate(p.read_text(encoding="utf-8").splitlines(), 1): - if re.match(r"^\s*postulate(\s|$)", line): - err(f"{rel(p)}:{n}: `postulate` outside the trust-base " - f"quarantine ({quarantine})") - - # safe modules must claim --safe - for name in safe_modules: - spath = REPO_ROOT / name - if not spath.is_file(): - continue # already reported via `missing` - s = spath.read_text(encoding="utf-8") - opts = re.findall(r"\{-#\s*OPTIONS([^#]*)#-\}", s) - if not any(re.search(r"(^|\s)--safe(\s|$)", o) for o in opts): - err(f"{name}: safe module must carry `--safe` in its OPTIONS pragma") - - # manifest ⇄ source set equality - exp = {a["name"]: a["class"] for a in expected} - if set(exp) != set(found): - only_src = sorted(set(found) - set(exp)) - only_man = sorted(set(exp) - set(found)) - if only_src: - err(f"postulates not in manifest: {only_src}") - if only_man: - err(f"manifest entries absent from source: {only_man}") - for name in sorted(set(exp) & set(found)): - if exp[name] != found[name]: - err(f"`{name}`: class `{found[name]}` in source but " - f"`{exp[name]}` in manifest") - per_class: dict[str, int] = {} - for cls in found.values(): - per_class[cls] = per_class.get(cls, 0) + 1 - for cls, cap in class_budget.items(): - if per_class.get(cls, 0) != cap: - err(f"class `{cls}`: source has {per_class.get(cls, 0)}, manifest " - f"budget is {cap} — adjust proofs/trust-base.json AND " - f"POSTULATE-AUDIT.adoc together") - if total_budget is not None and len(found) != total_budget: - err(f"total postulates: source has {len(found)}, budget is " - f"{total_budget}") - - if errors: - print(f"trust-base audit: FAILED ({len(errors)} problem(s))") - return 1 - print(f"trust-base audit: OK — {len(found)} postulate(s) in quarantine " - f"({', '.join(f'{c}={n}' for c, n in sorted(per_class.items()))}), " - f"{len(safe_modules)} safe module(s), {len(agda_files)} .agda file(s) total") - return 0 - - -if __name__ == "__main__": - sys.exit(main()) diff --git a/scripts/audit-trust-base.sh b/scripts/audit-trust-base.sh new file mode 100755 index 0000000..7117be2 --- /dev/null +++ b/scripts/audit-trust-base.sh @@ -0,0 +1,249 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors +# +# audit-trust-base.sh — gate the quarantined Agda trust base (issue #4). +# +# Single implementation shared by .github/workflows/echidna-verify.yml, the +# `just prove-audit` recipe and the GitLab mirror job. Exits non-zero (with +# ::error:: annotations for Actions) when proofs/theories and +# proofs/trust-base.json disagree IN ANY DIRECTION, so a postulate can be +# neither smuggled in nor silently deleted from the audit. +# +# Checks: +# 1. Every *.agda under proofs/theories is listed in the manifest as +# either the quarantine module or a safe module (no unregistered +# files, no stale entries). +# 2. `postulate` may only occur in the quarantine file. +# 3. Safe modules carry `--safe`; the quarantine file must NOT claim it +# (Agda's --safe rejects postulates, so the claim would be dishonest +# tooling rather than a sound split). +# 4. Every postulate declaration carries an +# `-- ECHIDNA:trust :: ` tag directly above it; class is +# in {ffi-fact, conjecture}; names are unique; and the whole +# name:class set equals the manifest exactly. +# 5. Per-class and total budgets match (source count == class_budget == +# total_budget == parsed manifest length — bidirectional). +# 6. Regression guard for the 2026-04 soundness bug: no per-postulate +# `where _≥_/_≤_ : Float → Float → Set`-style vacuous relations. +# 7. Non-empty corpus (fail-closed, issue #4 note 2). +# +# Pure POSIX sh + awk + grep: no Python (banned estate-wide), no jq, works +# with whatever coreutils the runner/mirror carries. + +set -eu + +ROOT=$(CDPATH= cd -- "$(dirname -- "$0")/.." && pwd) +THEORIES="$ROOT/proofs/theories" +MANIFEST="$ROOT/proofs/trust-base.json" +TMP=$(mktemp -d 2>/dev/null || echo "/tmp/trustbase.$$") +mkdir -p "$TMP" +trap 'rm -rf "$TMP"' EXIT + +ERRFILE="$TMP/errors" +: > "$ERRFILE" + +err() { + printf '::error::%s\n' "$1" + printf '%s\n' "$1" >> "$ERRFILE" +} + +if [ ! -f "$MANIFEST" ]; then + err "missing manifest proofs/trust-base.json" + printf 'trust-base audit: FAILED\n' + exit 1 +fi + +# corpus file list (repo-relative), sorted +if [ -d "$THEORIES" ]; then + find "$THEORIES" -name '*.agda' | sed "s|$ROOT/||" | LC_ALL=C sort > "$TMP/on-disk" +else + : > "$TMP/on-disk" +fi +if [ ! -s "$TMP/on-disk" ]; then + err "no .agda corpus under proofs/theories — a gate with nothing to check is no gate (fail-closed per issue #4 note 2)" + printf 'trust-base audit: FAILED\n' + exit 1 +fi + +# -- manifest parsing --------------------------------------------------------- +awk ' + function val(line, key, re, s) { + re = "\"" key "\": *\"[^\"]+\"" + if (match(line, re)) { + s = substr(line, RSTART, RLENGTH) + sub(/^"[^"]*": *"/, "", s) + sub(/"$/, "", s) + return s + } + return "" + } + /"quarantine":/ { print "Q\t" val($0, "quarantine"); next } + /"safe_modules":/ { in_safe = 1; next } + in_safe && /]/ { in_safe = 0; next } + in_safe && /"/ { gsub(/[",]/,""); gsub(/^ +| +$/,""); print "S\t" $0; next } + /"derived_modules":/ { in_derived = 1; next } + in_derived && /]/ { in_derived = 0; next } + in_derived && /"/ { gsub(/[",]/,""); gsub(/^ +| +$/,""); print "D\t" $0; next } + /"name":/ && /"class":/ { print "A\t" val($0,"name") "\t" val($0,"class"); next } + /"class_budget":/ { next } + /"(ffi-fact|conjecture)":/ { + line = $0; gsub(/[^0-9]/, "", line) + key = $1; gsub(/[^a-zA-Z-]/,"",key) + print "B\t" key "\t" line; next + } + /"total_budget":/ { line = $0; gsub(/[^0-9]/,"",line); print "T\t" line; next } +' "$MANIFEST" > "$TMP/manifest.tsv" + +QUARANTINE=$(awk -F'\t' '$1=="Q"{print $2; exit}' "$TMP/manifest.tsv") +if [ -z "$QUARANTINE" ]; then + err "manifest: no \"quarantine\" entry" + QUARANTINE="NONE" +fi +awk -F'\t' '$1=="S"{print $2}' "$TMP/manifest.tsv" > "$TMP/safe-modules" +awk -F'\t' '$1=="D"{print $2}' "$TMP/manifest.tsv" > "$TMP/derived-modules" +awk -F'\t' '$1=="A"{print $2 " " $3}' "$TMP/manifest.tsv" | LC_ALL=C sort > "$TMP/manifest-axioms" +MANIFEST_TOTAL=$(awk -F'\t' '$1=="T"{print $2; exit}' "$TMP/manifest.tsv") +SAFE_COUNT=$(wc -l < "$TMP/safe-modules" | tr -d ' ') + +# listed set ⇄ on-disk set +{ printf '%s\n' "$QUARANTINE"; cat "$TMP/safe-modules" "$TMP/derived-modules"; } | sed 's|^/||' | LC_ALL=C sort -u > "$TMP/listed" +unlisted=$(LC_ALL=C comm -23 "$TMP/on-disk" "$TMP/listed") +missing=$(LC_ALL=C comm -13 "$TMP/on-disk" "$TMP/listed") +if [ -n "$unlisted" ]; then + err ".agda file(s) not registered in proofs/trust-base.json: $(printf '%s' "$unlisted" | tr '\n' ' ') — add to safe_modules/derived_modules (or extend the quarantine deliberately) in the same PR" +fi +if [ -n "$missing" ]; then + err "manifest lists files that do not exist: $(printf '%s' "$missing" | tr '\n' ' ')" +fi + +QPATH="$ROOT/$QUARANTINE" + +# -- parse the quarantine source: state machine over postulate blocks -------- +if [ -f "$QPATH" ]; then + if grep -qE '\{-# OPTIONS[^#]*--safe' "$QPATH"; then + err "$QUARANTINE: quarantine must not declare --safe (Agda rejects postulates under --safe)" + fi + awk -v qpath="$QUARANTINE" ' + # skip OPTIONS pragma line for the vacuity scan, track state otherwise + { lines[NR] = $0 } + END { + inpost = 0 + for (i = 1; i <= NR; i++) { + l = lines[i] + if (l ~ /^[ \t]*postulate([ \t]|$)/) { inpost = 1; continue } + if (l ~ /^[ \t]*$/) continue + if (l ~ /^[ \t]*--/) continue + if (inpost && l ~ /^[ \t]/) { + if (match(l, /^[ \t][ \t]*[^ \t:]+[ \t]*:/)) { + name = l + sub(/^[ \t]+/, "", name); sub(/[ \t]*:.*$/, "", name) + j = i - 1 + while (j >= 1 && lines[j] ~ /^[ \t]*$/) j-- + cls = "" + if (j >= 1 && match(lines[j], /-- ECHIDNA:trust [^ ]+ :: [^ ]+/)) { + tag = substr(lines[j], RSTART, RLENGTH) + split(tag, parts, / +:: +/) + cls = parts[1]; sub(/^-- ECHIDNA:trust +/, "", cls) + tname = parts[2] + if (tname != name) + printf "E %s:%d: tag names `%s` but declares `%s`\n", qpath, i, tname, name + } else { + printf "E %s:%d: postulate `%s` is not tagged — add `-- ECHIDNA:trust :: %s` directly above it\n", qpath, i, name, name + tname = name; cls = "" + } + if (cls != "" && cls != "ffi-fact" && cls != "conjecture") + printf "E %s:%d: class `%s` not in {conjecture, ffi-fact}\n", qpath, i, cls + if (seen[name]++) + printf "E duplicate postulate `%s`\n", name + if (cls != "") printf "A %s %s\n", name, cls + } + # vacuous where-relation regression (either shape: this line or the next) + if (lines[i+1] ~ /^[ \t]+_[≥≤]_[ \t]*:/) + printf "E %s:%d: `where _≥_/_≤_ : ...` — vacuous relation regression (2026-04 audit bug)\n", qpath, i + 1 + continue + } + if (inpost && l !~ /^[ \t]/) inpost = 0 + } + } + ' "$QPATH" > "$TMP/qout" + grep '^E ' "$TMP/qout" | sed 's/^E //' | while IFS= read -r e; do err "$e"; done + grep '^A ' "$TMP/qout" | sed 's/^A //' | LC_ALL=C sort > "$TMP/source-axioms" + + # explicit whole-file vacuity scan (independent of the state machine) + if grep -nE '^[[:space:]]+_[≥≤]_[[:space:]]*:' "$QPATH" > "$TMP/vacuous" 2>/dev/null; then + while IFS=: read -r ln _; do + err "$QUARANTINE:$ln: vacuous where-relation (2026-04 audit regression)" + done < "$TMP/vacuous" + fi +else + err "quarantine file missing: $QUARANTINE" + : > "$TMP/source-axioms" +fi + +# -- stray postulates outside the quarantine --------------------------------- +while IFS= read -r f; do + [ "$f" = "$QUARANTINE" ] && continue + if grep -nE '^[[:space:]]*postulate([[:space:]]|$)' "$ROOT/$f" > "$TMP/stray" 2>/dev/null; then + while IFS=: read -r ln _; do + err "$f:$ln: \`postulate\` outside the trust-base quarantine ($QUARANTINE)" + done < "$TMP/stray" + fi +done < "$TMP/on-disk" + +# -- safe modules must claim --safe ------------------------------------------- +while IFS= read -r name; do + [ -f "$ROOT/$name" ] || continue + if ! grep -qE '\{-# OPTIONS[^#]*--safe' "$ROOT/$name"; then + err "$name: safe module must carry \`--safe\` in its OPTIONS pragma" + fi +done < "$TMP/safe-modules" + +# -- derived modules: postulate-free but axiom-consuming headers. Agda's +# flag-inheritance rule ("Importing module not using the --safe flag from a +# module which does", live CI evidence) makes a --safe top file that imports +# the quarantine a hard error, so those headers sit beside the quarantine, +# carry NO --safe claim, and are still census-checked for `postulate` above. +while IFS= read -r name; do + [ -f "$ROOT/$name" ] || continue + if grep -qE '\{-# OPTIONS[^#]*--safe' "$ROOT/$name"; then + err "$name: registered as derived (axiom-importing) — it must NOT claim --safe; Agda would reject the import, so either discharge its axioms (then move it to safe_modules) or keep the honest flag" + fi +done < "$TMP/derived-modules" + +# -- set equality + budgets ---------------------------------------------------- +cut -d' ' -f1 "$TMP/source-axioms" | LC_ALL=C sort -u > "$TMP/src-names" +cut -d' ' -f1 "$TMP/manifest-axioms" | LC_ALL=C sort -u > "$TMP/man-names" +only_src=$(LC_ALL=C comm -23 "$TMP/src-names" "$TMP/man-names") +only_man=$(LC_ALL=C comm -13 "$TMP/src-names" "$TMP/man-names") +if [ -n "$only_src" ]; then err "postulates not in manifest: $(printf '%s' "$only_src" | tr '\n' ' ')"; fi +if [ -n "$only_man" ]; then err "manifest entries absent from source: $(printf '%s' "$only_man" | tr '\n' ' ')"; fi +mismatch=$(LC_ALL=C join -j 1 "$TMP/source-axioms" "$TMP/manifest-axioms" | awk '{if ($2 != $3) print $1 ": source=" $2 " manifest=" $3}') +if [ -n "$mismatch" ]; then printf '%s\n' "$mismatch" | while IFS= read -r m; do err "$m class mismatch"; done; fi + +SRC_TOTAL=$(wc -l < "$TMP/source-axioms" | tr -d ' ') +MAN_TOTAL=$(wc -l < "$TMP/manifest-axioms" | tr -d ' ') +if [ "$SRC_TOTAL" != "$MAN_TOTAL" ]; then + err "axiom count: source has $SRC_TOTAL, manifest lists $MAN_TOTAL (parse drift?)" +fi +for cls in ffi-fact conjecture; do + cap=$(awk -F'\t' -v c="$cls" '$1=="B" && $2==c {print $3; exit}' "$TMP/manifest.tsv") + got=$(cut -d' ' -f2 "$TMP/source-axioms" | grep -c "^$cls$" || true) + if [ -n "$cap" ] && [ "$got" != "$cap" ]; then + err "class \`$cls\`: source has $got, manifest budget is $cap — adjust proofs/trust-base.json AND POSTULATE-AUDIT.adoc together" + fi +done +if [ -n "$MANIFEST_TOTAL" ] && [ "$SRC_TOTAL" != "$MANIFEST_TOTAL" ]; then + err "total postulates: source has $SRC_TOTAL, budget is $MANIFEST_TOTAL" +fi + +if [ -s "$ERRFILE" ]; then + printf 'trust-base audit: FAILED (%s problem(s))\n' "$(wc -l < "$ERRFILE" | tr -d ' ')" + exit 1 +fi + +printf 'trust-base audit: OK — %s postulate(s) in quarantine (%s), %s safe module(s), %s .agda file(s) total\n' \ + "$SRC_TOTAL" \ + "$(cut -d' ' -f2 "$TMP/source-axioms" | LC_ALL=C sort | uniq -c | awk '{printf "%s=%s ", $2, $1}')" \ + "$SAFE_COUNT" \ + "$(wc -l < "$TMP/on-disk" | tr -d ' ')" diff --git a/scripts/prove-agda.sh b/scripts/prove-agda.sh new file mode 100755 index 0000000..7c92ecd --- /dev/null +++ b/scripts/prove-agda.sh @@ -0,0 +1,191 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors +# +# prove-agda.sh — type-check proofs/theories exactly as +# .github/workflows/echidna-verify.yml does (issue #4). Used by that +# workflow, by `just prove-agda`/`just prove-check-all`, and by the GitLab +# mirror job, so the three surfaces cannot drift. +# +# Layered trust: modules whose OPTIONS pragma declares `--safe` are checked +# with `--safe --without-K` (Agda then rejects any `postulate`); the +# quarantined trust base (proofs/theories/InformationTheory/Axioms.agda) is +# checked with `--without-K` only. The pragma is the source of truth; +# scripts/audit-trust-base.sh separately enforces WHICH file may carry which +# pragma and which may carry postulates. +# +# Fail-closed on: missing agda, missing/unusable stdlib, empty corpus, any +# module failing to type-check. +# +# Env overrides: AGDA (binary), AGDA_STDLIB_DIR (source tree of stdlib to +# pass via -i), AGDA_COMPILE_DIR (where .agdai go; default ./agda-compile-dir). + +set -eu + +ROOT=$(CDPATH= cd -- "$(dirname -- "$0")/.." && pwd) +cd "$ROOT" + +AGDA=${AGDA:-agda} +COMPILE_DIR=${AGDA_COMPILE_DIR:-"$ROOT/agda-compile-dir"} +THEORY_DIR=proofs/theories +fail=0 + +command -v "$AGDA" >/dev/null 2>&1 || { + echo "::error::agda not found on PATH — install it (CI: apt-get install -y agda agda-stdlib; local: the same, or nix-shell -p agda agdaPackages.stdlib)" + exit 1 +} +"$AGDA" --version 2>&1 || echo "note: agda --version failed (continuing — probe will assess)" + +# -- locate the stdlib --------------------------------------------------------- +# Ubuntu/Debian's agda-stdlib installs pre-compiled sources *loose* under +# /usr/share/agda-stdlib (there is no .agda-lib file in that package layout — +# the standards-era workflow assumed a library manifest and would have found +# nothing, silently). Register by include path when sources are loose, and by +# ~/.agda/libraries only when an .agda-lib manifest exists. +STDLIB_DIR=${AGDA_STDLIB_DIR:-} +if [ -z "$STDLIB_DIR" ]; then + for d in /usr/share/agda-stdlib /usr/share/agda/std-lib /usr/local/share/agda-stdlib; do + if [ -f "$d/Data/Nat.agda" ] || [ -f "$d/extra/AGDA-stdlib-VERSION" ]; then + STDLIB_DIR=$d + break + fi + lib=$(find "$d" -maxdepth 3 -name '*.agda-lib' 2>/dev/null | head -1 || true) + if [ -n "$lib" ]; then + mkdir -p "$HOME/.agda/libraries" + touch "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults" + grep -qxF "$lib" "$HOME/.agda/libraries/estate-stdlib" || echo "$lib" >> "$HOME/.agda/libraries/estate-stdlib" + name=$(awk '$1=="name:"{print $2; exit}' "$lib") + if [ -n "$name" ] && ! grep -qxF "$name" "$HOME/.agda/defaults"; then + echo "$name" >> "$HOME/.agda/defaults" + fi + echo "Registered stdlib library: $lib (as ${name:-unknown})" + STDLIB_DIR="" + break + fi + done +fi +if [ -n "$STDLIB_DIR" ]; then + # Any stdlib module whose packaged .agdai fingerprint no longer matches + # gets re-checked and its interface rewritten *next to the source* — + # --compile-dir only moves executables, not .agdai files. On the apt + # layout (/usr/share/agda-stdlib, root-owned) that is a hard + # "removeLink: permission denied" failure. If the tree is not writable + # for this user, work from a writable mirror instead. + if [ ! -w "$STDLIB_DIR" ]; then + MIRROR="$HOME/.cache/lol-agda-stdlib" + if [ ! -d "$MIRROR/Data" ]; then + mkdir -p "$MIRROR" + tar cf - -C "$STDLIB_DIR" . 2>/dev/null | tar xf - -C "$MIRROR" 2>/dev/null \ + || cp -a "$STDLIB_DIR/." "$MIRROR/" + fi + chmod -R u+w "$MIRROR" 2>/dev/null || true + echo "note: stdlib at $STDLIB_DIR not user-writable; mirroring to $MIRROR (interface rewrites land there)" + STDLIB_DIR="$MIRROR" + fi + echo "Using stdlib sources from: $STDLIB_DIR ($(find "$STDLIB_DIR" -name '*.agda' | wc -l) modules)" +fi + +mkdir -p "$COMPILE_DIR" + +# -- probe: prove stdlib visibility BEFORE checking anything ------------------- +# The standards-side job skipped its steps and still "passed" once the corpus +# moved; a check that cannot see its toolchain must be red, not green-skipped. +PROBE_DIR=$(mktemp -d 2>/dev/null || echo "$COMPILE_DIR/probe") +mkdir -p "$PROBE_DIR" +cat > "$PROBE_DIR/Probe.agda" <<'EOF' +module Probe where +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec) +open import Data.Float using (Float) +EOF +# `set -e` must not swallow the diagnosis: every agda invocation is funnelled +# through run_agda, which tees output to a per-call file and, on failure, +# re-emits the first lines as an annotation (workflow commands reach the +# checks API; raw logs are not always retrievable). +run_agda() { + _out="$PROBE_DIR/agda.out" + _rc=0 + "$AGDA" "$@" >"$_out" 2>&1 || _rc=$? + sed 's/^/ /' "$_out" + if [ $_rc -ne 0 ]; then + _ann=$(head -14 "$_out" | cut -c1-220 | sed 's/%/%25/g; s/::/%3A%3A/g' | awk '{printf "%s%%0A", $0}') + echo "::error::agda exit $_rc: ${_ann}" + fi + return $_rc +} +PROBE_OK=0 +if [ -n "$STDLIB_DIR" ]; then + if run_agda --compile-dir "$COMPILE_DIR" -i "$STDLIB_DIR" -i "$PROBE_DIR" "$PROBE_DIR/Probe.agda"; then + PROBE_OK=1 + else + # Older packaged .agdai trees can reject a foreign --compile-dir + # (interface staleness -> attempted write next to root-owned sources). + # Retry without it before declaring the toolchain unusable. + echo "note: probe failed with --compile-dir; retrying without (source-tree .agdai layout)" + if run_agda -i "$STDLIB_DIR" -i "$PROBE_DIR" "$PROBE_DIR/Probe.agda"; then + PROBE_OK=1 + COMPILE_DIR= + echo "note: continuing without --compile-dir" + fi + fi +else + if run_agda --compile-dir "$COMPILE_DIR" -i "$PROBE_DIR" "$PROBE_DIR/Probe.agda"; then + PROBE_OK=1 + else + run_agda -i "$PROBE_DIR" "$PROBE_DIR/Probe.agda" && { PROBE_OK=1; COMPILE_DIR=; } + fi +fi +if [ "$PROBE_OK" -ne 0 ]; then + echo "stdlib probe OK (Data.Nat / Data.Vec / Data.Float resolve (per-module pragmas))" +else + echo "::error::stdlib probe failed — Agda cannot see the standard library (STDLIB_DIR='${STDLIB_DIR:-}'); refusing to run the corpus against a broken toolchain" + exit 1 +fi + +# -- corpus --------------------------------------------------------------------- +FILES=$(find "$THEORY_DIR" -name '*.agda' | LC_ALL=C sort) +if [ -z "$FILES" ]; then + echo "::error::no .agda files under $THEORY_DIR — refusing to report success with an empty corpus (issue #4 note 2)" + exit 1 +fi + +for f in $FILES; do + # Do NOT pass --safe/--without-K on the command line: command-line flags + # are inherited by every imported module and an OPTIONS pragma cannot + # *revoke* them — the quarantined Axioms module would then die with + # "Cannot postulate ... with safe flag" merely because the importing + # header is safe (live CI evidence, iteration 4). Flags are therefore + # governed per-module by each file's `{-# OPTIONS ... #-}` pragma — and + # the pragma's honesty is what the audit step (and the check below) + # enforces, so nothing is lost: a safe module that dropped its pragma + # would be checked unsafely here AND fail the audit. + # Pragma-scoped match only: a comment mentioning --safe must not flip a + # file into safe mode (the Axioms header discusses --safe at length). + if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then + claim="--safe (per pragma)" + else + claim="--without-K only — quarantined trust base by design" + fi + echo "--- checking $f ($claim) ---" + if [ -n "$STDLIB_DIR" ]; then + inc="-i $STDLIB_DIR -i $THEORY_DIR" + else + inc="-i $THEORY_DIR" + fi + if [ -n "$COMPILE_DIR" ]; then + cdir="--compile-dir $COMPILE_DIR" + else + cdir= + fi + if ! run_agda $cdir $inc "$f"; then + echo "::error::agda type-check FAILED for $f" + fail=1 + fi +done + +rm -rf "$PROBE_DIR" + +if [ "$fail" -ne 0 ]; then + exit 1 +fi +echo "All Agda proofs type-checked cleanly under the enforced flags."