fix(proofs): NaN-safe trust base, estate proof-debt ledger, POSIX-sh gate port (follow-up to #18; closes #4)

.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: |

.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/
 

.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
 
 # =============================================================================

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)

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

docs/proof-debt.md

@@ -0,0 +1,92 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors
+
+docs/proof-debt.md — estate Trusted-Base Reduction Policy ledger for this
+repo (hyperpolymath/standards docs/TRUSTED-BASE-REDUCTION-POLICY.adoc).
+Enforced by `standards/scripts/check-trusted-base.sh` via the governance
+workflow; every `postulate` in `proofs/**/*.agda` must appear here or carry
+an inline `TRUSTED:`/`AXIOM:` leading comment. This repo does both: the
+inline blocks are in `proofs/theories/InformationTheory/Axioms.agda`, and
+this document is the ledger.
+
+Machine-readable counterpart (name/class/budget, gated by
+`scripts/audit-trust-base.sh`): `proofs/trust-base.json`.
+Human prose rationale: `proofs/POSTULATE-AUDIT.adoc`.
+-->
+
+# 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)