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..ad0417f 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -17,6 +17,13 @@ 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`). Since 2026-09-23 the gate also runs the Coq `Print Assumptions` audit and +its `--control` after the build, so a theorem resting on an axiom, or an audit that can no +longer say no, turns it red. `proofs/tests/gate-selftest.sh` proves both gates turn red for +each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI). ==== == Coq — VERIFIED (this environment) @@ -82,9 +89,15 @@ 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`, and the canonical +`proofs/verify-all-provers.sh` gate since 2026-09-23) 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 +164,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 +241,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..56d54e5 --- /dev/null +++ b/proofs/coq/check-assumptions.sh @@ -0,0 +1,66 @@ +#!/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 : compile an audit with at least one Print Assumptions command. +# Print the Coq output and remove generated artefacts beside the audit file. +# Succeed only if compilation succeeds, no axiom blocks appear, and the number +# of closed results matches the number of Print Assumptions commands. +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..836b9c3 --- /dev/null +++ b/proofs/tests/gate-selftest.sh @@ -0,0 +1,122 @@ +#!/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