From 476aa327fa6bcbf42cef1d5380e84ee8097eda3f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 23 Sep 2026 01:11:43 +0100 Subject: [PATCH 1/4] =?UTF-8?q?proofs:=20honest=20prover=20gate=20?= =?UTF-8?q?=E2=80=94=20absent=20prover=20=3D=20fail,=20z3=20expect-checked?= =?UTF-8?q?,=20Print=20Assumptions=20gated,=20Agda=204/4=20--safe=20(4b?= =?UTF-8?q?=E2=80=934d)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four defects made the gate able to say green without checking: - verify-all-provers.sh printed "skipped" for an absent Isabelle or Mizar and still said ALL-PROVERS-GREEN (four of six provers); a listed Agda module that was missing on disk was silently skipped too. - proofs/z3/verify.sh ran `z3 cno_properties.smt2` — a file that does not exist — and CI wrapped it in `|| true`; the only live z3 check was an exit code, which is 0 for sat AND unsat. - Nothing ran Print Assumptions anywhere, so "closed under the global context" was prose. - CI type-checked 2 of the 4 Agda modules and EchoBridgeCNO.agda carried no --safe pragma of its own. Changes: - proofs/verify-all-provers.sh: Isabelle/Mizar absent -> fail=1; missing Agda module -> fail; EchoBridgeScaffold added; z3 via the expect-checker. - proofs/z3/verify.sh: generic expect-checker — every (check-sat) must carry `; expect sat|unsat` and z3's verdicts must match in order; fails on unknown, (error, missing annotation, no files, z3 rc != 0. - proofs/coq/audit/Assumptions.v + proofs/coq/check-assumptions.sh: the 17 theorems PROOF-STATUS names must print Closed under the global context; --control proves the gate rejects landauer_limit_positive (kB_positive). - proofs/tests/gate-selftest.sh: 14 cases (stubbed toolchains + real-z3 mutants), each negative asserting its reason string. - proofs/agda/EchoBridgeCNO.agda: {-# OPTIONS --safe --without-K #-}. - .github/workflows/proofs.yml: coq job runs the gate + control; agda job checks 4 modules; z3 job runs the checker without `|| true` plus the self-test. - Justfile: build-agda 4 modules; verify-z3 no skip-as-pass; verify-coq runs the gate; new verify-gate-selftest in verify-all. - PROOF-STATUS.adoc: Agda section matches CI; assumptions claim is the measured 17/17-closed fact; census (109/182 closed) tracked in #171. Measured locally (2026-09-23): self-test 14/14; reverting the Isabelle fix flunks exactly case B; blinding the z3 comparison flunks exactly E/G/K/N; assumptions gate 17/17 closed, control rejects naming kB_positive, vacuous and renamed audit files fail; agda 2.6.4.3 --safe --without-K passes all 4 modules; actionlint clean; actions.lock coverage complete. Refs #171. Phase 4b–4d of the residual-evidence-types ultraplan. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- .github/workflows/proofs.yml | 18 +++++-- Justfile | 26 ++++++---- PROOF-STATUS.adoc | 27 ++++++++-- proofs/agda/EchoBridgeCNO.agda | 2 + proofs/coq/audit/Assumptions.v | 30 +++++++++++ proofs/coq/check-assumptions.sh | 63 +++++++++++++++++++++++ proofs/tests/gate-selftest.sh | 90 +++++++++++++++++++++++++++++++++ proofs/verify-all-provers.sh | 22 ++++---- proofs/z3/verify.sh | 90 ++++++++++++++++++++------------- 9 files changed, 303 insertions(+), 65 deletions(-) create mode 100644 proofs/coq/audit/Assumptions.v create mode 100755 proofs/coq/check-assumptions.sh create mode 100755 proofs/tests/gate-selftest.sh diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 6e2b3d4..bf7573a 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -56,6 +56,11 @@ jobs: coq_makefile -f _CoqProject -o Makefile.all make -f Makefile.all -j"$(nproc)" echo "✓ Coq: 14/14 theories compiled (CNO + OND)" + - name: Print Assumptions gate (17 named theorems closed) + control + working-directory: proofs/coq + run: | + bash check-assumptions.sh + bash check-assumptions.sh --control agda: name: Agda — CNO + OND @@ -79,13 +84,15 @@ jobs: mkdir -p "$HOME/.agda" echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries" echo "standard-library" > "$HOME/.agda/defaults" - - name: Type-check CNO + OND (--safe --without-K) + - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K) working-directory: proofs/agda run: | agda --version agda --safe --without-K CNO.agda agda --safe --without-K OND.agda - echo "✓ Agda: CNO + OND type-check" + agda --safe --without-K EchoBridgeScaffold.agda + agda --safe --without-K EchoBridgeCNO.agda + echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check" z3: name: Z3 — CNO + OND bounded checks @@ -97,9 +104,10 @@ jobs: - name: Run Z3 checks run: | z3 --version - sh proofs/z3/verify.sh || true - z3 proofs/z3/ond/OND_checks.smt2 - echo "✓ Z3: OND bounded instances checked" + bash proofs/z3/verify.sh + echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation" + - name: Gate self-test (stub provers + z3 mutants must turn the gate red) + run: bash proofs/tests/gate-selftest.sh lean: name: Lean — core CNO (6 modules + axiom audit) diff --git a/Justfile b/Justfile index 6c96198..81b91de 100644 --- a/Justfile +++ b/Justfile @@ -39,10 +39,10 @@ build-lean: @echo "Building Lean 4 proofs..." cd proofs/lean4 && lake build -# Build Agda proofs (CNO + OND, --safe --without-K) +# Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K) build-agda: @echo "Building Agda proofs..." - cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda + cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda && agda --safe --without-K EchoBridgeScaffold.agda && agda --safe --without-K EchoBridgeCNO.agda # Build Isabelle/HOL proofs (CNO + OND session) build-isabelle: @@ -78,21 +78,21 @@ verify: @proofs/verify-all-provers.sh # Verify all proofs (per-prover targets; `just verify` is the canonical one-shot) -verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris +verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris verify-gate-selftest @echo "✓ All verifications complete" -# Verify Coq proofs +# Verify Coq proofs: build, then the Print Assumptions gate and its control verify-coq: build-coq - @echo "✓ Coq proofs verified" + bash proofs/coq/check-assumptions.sh + bash proofs/coq/check-assumptions.sh --control + @echo "✓ Coq proofs verified (17 named theorems closed under the global context)" -# Verify Z3 SMT properties (CNO checks + OND bounded instances) +# Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass) verify-z3: @echo "Verifying Z3 SMT properties..." - @if command -v z3 >/dev/null 2>&1; then \ - sh proofs/z3/verify.sh && z3 proofs/z3/ond/OND_checks.smt2 && echo "✓ Z3 verification complete"; \ - else \ - echo "⚠ z3 not found, skipping Z3 verification"; \ - fi + @command -v z3 >/dev/null 2>&1 || { echo "✗ z3 not found (required, not skipped)"; exit 1; } + bash proofs/z3/verify.sh + @echo "✓ Z3 verification complete" # Verify Lean 4 proofs verify-lean: @@ -116,6 +116,10 @@ verify-isabelle: build-isabelle verify-mizar: build-mizar @echo "✓ Mizar proofs verified" +# Self-test the prover gate: stubbed toolchains + z3 mutants must turn it red +verify-gate-selftest: + bash proofs/tests/gate-selftest.sh + # Verify the Idris 2 ABI package verify-idris: build-idris @echo "✓ Idris ABI verified" diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 3ae3963..5d8bad1 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -17,6 +17,11 @@ All six provers are installed and were *reproduced in this environment*. A singl gate, `proofs/verify-all-provers.sh`, builds every prover and prints `ALL-PROVERS-GREEN`: *Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar*, plus the *Idris 2* ABI. Both the CNO and OND pillars are covered. +An absent prover is a *failure*, never a skip (since 2026-09-23 — before that Isabelle +and Mizar printed "skipped" and the gate could say GREEN on four of six), and Z3 +verdicts are compared with the `; expect sat|unsat` annotation on every `(check-sat)` +(`proofs/z3/verify.sh`). `proofs/tests/gate-selftest.sh` proves both gates turn red for +each absent or failing prover and for each verdict mutant (14 cases, run in CI). ==== == Coq — VERIFIED (this environment) @@ -82,9 +87,14 @@ of these, each documented in-file with its blocker: `nat -> C` single-qubit model; faithful discharge is a separate formalisation. These are the analogue of the OND-6 research fork: openly labelled, not silently -assumed. `Print Assumptions` on every headline theorem shows only Coq stdlib axioms -(`ClassicalDedekindReals.*`, `functional_extensionality*`) plus, where relevant, the -explicitly-tagged postulate above — never a hidden project axiom. +assumed. `Print Assumptions` on each of the 17 theorems this document names in backticks +prints `Closed under the global context` — no stdlib axiom and no project axiom (measured +2026-09-23, Coq 8.18). That is CI-gated: `proofs/coq/audit/Assumptions.v` lists the 17 and +`proofs/coq/check-assumptions.sh` (Coq job of `proofs.yml`) fails on any `Axioms:` block or a +missing line; its `--control` mode proves the gate bites by requiring that +`landauer_limit_positive`, which rests on `kB_positive`, is rejected. The wider tree is not +closed — 109 of 182 top-level theorems are; the other 73 rest on stdlib classical axioms +and/or the tagged parameters — see #171 for the census and the tag-grammar work. === Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites) @@ -151,8 +161,11 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. == Agda — VERIFIED (this environment) -* `agda` 2.6.3, `--safe --without-K`: `CNO.agda`, `OND.agda`, `EchoBridgeCNO.agda` - type-check. The EchoBridge modules take **funext as an explicit hypothesis** +* `agda` 2.6.3 (CI) / 2.6.4.3 (local), `--safe --without-K`: `CNO.agda`, `OND.agda`, + `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda` type-check; every file carries the + `{-# OPTIONS --safe --without-K #-}` pragma and CI (`proofs.yml`) checks all four. Until + 2026-09-23 CI checked only the first two and `EchoBridgeCNO.agda` had no pragma of its + own. The EchoBridge modules take **funext as an explicit hypothesis** (not a global `postulate`); `OND.agda` uses zero postulates. == Lean 4 — VERIFIED (this environment) @@ -225,3 +238,7 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. * Remaining axioms are exactly: (a) tagged physical postulates (the honest metal boundary), and (b) the class-A items listed above (true, provable in principle, openly labelled). No headline theorem depends on a hidden project axiom. +* Measured 2026-09-23: the 17 named theorems are closed under the global context + (CI-gated); of all 182 top-level theorems, 109 are closed and 73 rest on stdlib + classical axioms and/or the tagged parameters. The "exactly" in the bullet above is + not yet machine-checked — the tag grammar is unified under #171. diff --git a/proofs/agda/EchoBridgeCNO.agda b/proofs/agda/EchoBridgeCNO.agda index c1fe97b..06db811 100644 --- a/proofs/agda/EchoBridgeCNO.agda +++ b/proofs/agda/EchoBridgeCNO.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --safe --without-K #-} + -- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval. -- -- Primary bridge: use CNO.state-eq directly as the relation in EchoRel. diff --git a/proofs/coq/audit/Assumptions.v b/proofs/coq/audit/Assumptions.v new file mode 100644 index 0000000..adef23e --- /dev/null +++ b/proofs/coq/audit/Assumptions.v @@ -0,0 +1,30 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Print Assumptions audit over the theorems PROOF-STATUS.adoc names. + + NOT listed in _CoqProject: proofs/coq/check-assumptions.sh compiles this file + after the theories are built and FAILS unless every line below prints + "Closed under the global context" (no stdlib axiom, no project axiom). + Add a line here whenever PROOF-STATUS starts naming a theorem; the checker + counts the "Print Assumptions" lines, so a theorem cannot be dropped silently. + Measured 2026-09-23: 17/17 closed (Coq 8.18). *) +Require CNO.CNO. +Require CNO.FilesystemCNO. +Require CNO.LambdaCNO. +Require CNO.OND. +Print Assumptions CNO.CNO.cno_equiv_seq_empty_of_reverses. +Print Assumptions CNO.FilesystemCNO.create_unlink_inverse. +Print Assumptions CNO.LambdaCNO.eta_equivalence. +Print Assumptions CNO.CNO.eval_app. +Print Assumptions CNO.CNO.eval_deterministic. +Print Assumptions CNO.FilesystemCNO.mkdir_idempotent. +Print Assumptions CNO.FilesystemCNO.mkdir_not_identity. +Print Assumptions CNO.FilesystemCNO.mkdir_rmdir_inverse. +Print Assumptions CNO.FilesystemCNO.rename_inverse. +Print Assumptions CNO.CNO.reverses_seq_computes_identity. +Print Assumptions CNO.CNO.reversible_bridge_backward_upto. +Print Assumptions CNO.CNO.reversible_bridge_forward. +Print Assumptions CNO.CNO.reversible_iff_exists_reverses. +Print Assumptions CNO.OND.skip_program_is_core_CNO. +Print Assumptions CNO.FilesystemCNO.snapshot_restore_identity. +Print Assumptions CNO.FilesystemCNO.transaction_cno. +Print Assumptions CNO.OND.writer_program_not_core_CNO. diff --git a/proofs/coq/check-assumptions.sh b/proofs/coq/check-assumptions.sh new file mode 100755 index 0000000..d04bcd6 --- /dev/null +++ b/proofs/coq/check-assumptions.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — Print Assumptions gate for the Coq pillar. +# +# Compiles audit/Assumptions.v (or the file given as $1) against the built +# theories, using the -R roots from _CoqProject, and FAILS unless every +# `Print Assumptions` line answers "Closed under the global context": +# - any "Axioms:" block -> FAIL (the block is printed); +# - closed-count != line-count -> FAIL (a theorem silently missing); +# - coqc exit != 0 -> FAIL (a renamed/removed theorem); +# - a file with no Print Assumptions lines -> FAIL (vacuous gate). +# `--control` proves the gate bites: it audits CNO.StatMech.landauer_limit_positive, +# which rests on the tagged axiom PhysicsConstants.kB_positive, and requires +# the gate to REJECT it naming that axiom. +# Run after `coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all`. +set -uo pipefail +HERE="$(cd "$(dirname "$0")" && pwd)" + +command -v coqc >/dev/null || { echo "ASSUMPTIONS-CHECK FAILED: coqc not on PATH"; exit 1; } +RFLAGS=() +while read -r flag dir ns; do + [ "$flag" = "-R" ] && RFLAGS+=("-R" "$HERE/$dir" "$ns") +done < "$HERE/_CoqProject" +[ "${#RFLAGS[@]}" -gt 0 ] || { echo "ASSUMPTIONS-CHECK FAILED: no -R roots in _CoqProject"; exit 1; } + +# check_file : 0 iff every Print Assumptions line is closed. +check_file() { + local file=$1 base dir out rc expected closed axioms + base="$(basename "${file%.v}")"; dir="$(dirname "$file")" + expected=$(grep -c '^Print Assumptions' "$file") + if [ "$expected" -eq 0 ]; then + echo "ASSUMPTIONS-CHECK FAILED: $file has no 'Print Assumptions' lines (vacuous)"; return 1 + fi + out="$(coqc "${RFLAGS[@]}" "$file" 2>&1)"; rc=$? + rm -f "$dir/$base.vo" "$dir/$base.vos" "$dir/$base.vok" "$dir/$base.glob" "$dir/.$base.aux" + printf '%s\n' "$out" + if [ "$rc" -ne 0 ]; then echo "ASSUMPTIONS-CHECK FAILED: coqc exit $rc on $file"; return 1; fi + closed=$(printf '%s\n' "$out" | grep -c '^Closed under the global context') + axioms=$(printf '%s\n' "$out" | grep -c '^Axioms:') + if [ "$axioms" -ne 0 ] || [ "$closed" -ne "$expected" ]; then + echo "ASSUMPTIONS-CHECK FAILED: $file — expected $expected closed, got closed=$closed axiom-blocks=$axioms" + return 1 + fi + echo "ASSUMPTIONS-CHECK OK: $expected/$expected theorems closed under the global context ($file)" +} + +if [ "${1:-}" = "--control" ]; then + tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-assumptions-control.XXXXXX")" + trap 'rm -rf "$tmp"' EXIT + printf 'Require CNO.StatMech.\nPrint Assumptions CNO.StatMech.landauer_limit_positive.\n' > "$tmp/Control.v" + if check_file "$tmp/Control.v" > "$tmp/control.log" 2>&1; then + echo "ASSUMPTIONS-CONTROL FAILED: landauer_limit_positive (rests on kB_positive) PASSED the gate" + cat "$tmp/control.log"; exit 1 + fi + if ! grep -q 'kB_positive' "$tmp/control.log"; then + echo "ASSUMPTIONS-CONTROL FAILED: the rejection did not name PhysicsConstants.kB_positive" + cat "$tmp/control.log"; exit 1 + fi + echo "ASSUMPTIONS-CONTROL OK: landauer_limit_positive rejected, naming kB_positive (the gate bites)" + exit 0 +fi + +check_file "${1:-$HERE/audit/Assumptions.v}" diff --git a/proofs/tests/gate-selftest.sh b/proofs/tests/gate-selftest.sh new file mode 100755 index 0000000..8d60b73 --- /dev/null +++ b/proofs/tests/gate-selftest.sh @@ -0,0 +1,90 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — self-test for the prover gate. +# +# Proves that proofs/verify-all-provers.sh and proofs/z3/verify.sh turn RED when +# they should, using a stub toolchain on a private PATH (no real prover needed), +# plus two mutants under a REAL z3 (required on PATH). Every negative case must +# fail with the expected reason string, not merely a non-zero exit — a parse +# error would otherwise pass as a kill. +# HOME is overridden because the gate prepends $HOME/.local/bin:$HOME/.elan/bin. +set -uo pipefail +HERE="$(cd "$(dirname "$0")" && pwd)" +PROOFS="$(cd "$HERE/.." && pwd)" +GATE="$PROOFS/verify-all-provers.sh" +Z3CHECK="$PROOFS/z3/verify.sh" +REAL_SMT2="$PROOFS/z3/ond/OND_checks.smt2" +SCRATCH="$(mktemp -d "${TMPDIR:-/tmp}/az-gate-selftest.XXXXXX")" +trap 'rm -rf "$SCRATCH"' EXIT +STUB="$SCRATCH/bin"; mkdir -p "$STUB" "$SCRATCH/home" +cases=0; fails=0 +pass() { cases=$((cases+1)); echo "PASS: $1"; } +flunk() { cases=$((cases+1)); fails=$((fails+1)); echo "FAIL: $1"; } + +for s in "$GATE" "$Z3CHECK"; do bash -n "$s" || { echo "FAIL: $s does not parse"; exit 1; }; done + +mkstub() { printf '#!/bin/sh\n%s\n' "${2:-exit 0}" > "$STUB/$1"; chmod +x "$STUB/$1"; } +for t in coqc coq_makefile make agda lake isabelle accom verifier idris2; do mkstub "$t"; done +z3_stub() { mkstub z3 "case \"\${1:-}\" in --version) echo \"Z3 version stub\";; *) printf '$1';; esac"; } +z3_stub 'sat\nunsat\nsat\n' +for s in "$STUB"/*; do sh -n "$s" || { echo "FAIL: stub $s does not parse"; exit 1; }; done + +OUT=""; RC=0 +run_gate() { OUT="$(HOME="$SCRATCH/home" PATH="$STUB:/usr/bin:/bin" MIZFILES="${MIZ-$SCRATCH/miz}" bash "$GATE" 2>&1)"; RC=$?; } +# expect