From 05997284d1c6d9606990e801d7f314c31895d487 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:56:50 +0000 Subject: [PATCH 1/2] proofs: scope the vacuous Agda CNO fields, fix archived paths, pin stdlib, make OND-3 writer check real - CNO.agda (comments only): `terminates` is definitional (eval is total over a finite list, so every program "terminates") and `energy-dissipated` is the constant 0, so `thermodynamically-reversible` holds for every program. Say what they do and do not establish beside the definitions and on IsCNO. - PROOF-STATUS.adoc: new "Scope of the Agda CNO fields" section; rows and sections that pointed at proofs/coq, proofs/lean4, proofs/isabelle, proofs/mizar and proofs/verify-all-provers.sh now point at archive/proofs/ and are marked ARCHIVED instead of VERIFIED; 2026-11-09 receipts (z3 4.8.12, Agda 2.6.3 incl. --cubical-compatible); escape the `|` that split a table row. - scripts/provision-agda-stdlib.sh: register agda-stdlib v1.7.3 pinned to commit 0817da68 (fails if the tag moves); used by CI's agda job, the Justfile (`just provision-agda-stdlib`) and named in verify-active-provers.sh. - OND_checks.smt2: the OND-3 dir 2 block asserted (not (and (= 0 0) (= 1 1))), unsat for any program. It now computes the writer's O_all observable from a modelled writer_step/inj (per OND.v), plus a leaking-writer control (sat) and a writer_not_null witness (sat). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .github/workflows/proofs.yml | 16 ++-- Justfile | 5 ++ PROOF-STATUS.adoc | 149 +++++++++++++++++++++++-------- proofs/agda/CNO.agda | 32 +++++++ proofs/verify-active-provers.sh | 3 +- proofs/z3/ond/OND_checks.smt2 | 53 +++++++++-- scripts/provision-agda-stdlib.sh | 62 +++++++++++++ 7 files changed, 266 insertions(+), 54 deletions(-) create mode 100755 scripts/provision-agda-stdlib.sh diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index a808750..58cb206 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -20,6 +20,7 @@ on: - 'proofs/**' - 'src/**' - 'scripts/check-proof-patterns.sh' + - 'scripts/provision-agda-stdlib.sh' - 'tests/check-proof-patterns.sh' - '.machine_readable/contractiles/trust/trust.k9.ncl' - 'absolute-zero-abi.ipkg' @@ -56,16 +57,11 @@ jobs: # version-matched stdlib from git instead (validated locally). run: sudo apt-get update && sudo apt-get install -y agda - name: Fetch + register agda-stdlib v1.7.3 (matches Agda 2.6.3) - run: | - git clone -q --depth 1 --branch v1.7.3 \ - https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib" - # The upstream manifest is named `standard-library-1.7.3`; the repo's - # absolute-zero.agda-lib depends on `standard-library`, so align it. - sed -i 's/^name: .*/name: standard-library/' \ - "$HOME/agda-stdlib/standard-library.agda-lib" - mkdir -p "$HOME/.agda" - echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries" - echo "standard-library" > "$HOME/.agda/defaults" + # Same script for CI and local runs: clones tag v1.7.3, fails unless it + # resolves to the pinned commit, renames the manifest to + # `standard-library` (what absolute-zero.agda-lib depends on), and writes + # ~/.agda/libraries + ~/.agda/defaults. + run: bash scripts/provision-agda-stdlib.sh - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K) working-directory: proofs/agda run: | diff --git a/Justfile b/Justfile index 3d86215..e154ba0 100644 --- a/Justfile +++ b/Justfile @@ -21,6 +21,11 @@ default: build-all: build-agda build-idris @echo "✓ All builds complete" +# Register the pinned Agda standard library (v1.7.3) — same script CI runs. +# Writes $AGDA_DIR/libraries and defaults (AGDA_DIR defaults to ~/.agda). +provision-agda-stdlib: + bash scripts/provision-agda-stdlib.sh + # Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K) build-agda: @echo "Building Agda proofs..." diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 62aa215..610d417 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -14,7 +14,7 @@ by prover, and is explicit about which axioms remain and why. .2026-07-07 — both pillars machine-checked across six provers (HISTORICAL since 2026-10-10) ==== *Historical (superseded by the 2026-10-10 archive ruling below):* all six -provers were reproduced in this environment via `proofs/verify-all-provers.sh` +provers were reproduced in this environment via `proofs/verify-all-provers.sh` (now archived as `archive/proofs/verify-all-provers.six-prover.sh`) (`ALL-PROVERS-GREEN`): *Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar*, plus the *Idris 2* ABI. Today only Agda, Z3 (bounded) and the Idris 2 ABI are active — see the canonical table below. Both the CNO and OND pillars were covered. @@ -23,7 +23,7 @@ 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 +longer say no, turns it red. The six-prover self-test (now `archive/proofs/tests/gate-selftest.six-prover.sh`) proved both gates turn red for each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI). ==== @@ -61,11 +61,11 @@ claims are marked historical, not silently dropped, and axiom dependence | `proofs/agda/` — `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda` | ACTIVE (CI `agda` job; `proofs/verify-active-provers.sh`) | `proven` — **Grade 3**: type-checked locally in Agda, zero postulates, every file `{-# OPTIONS --safe --without-K #-}`; EchoBridge takes funext as an *explicit hypothesis*, not a global postulate. Not translated to any independent foundation, so not Grade 2+ -| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. Open obligation: recheck under the 2026-11-01 canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1) — prior `--safe --without-K` receipts are not receipts for the combined profile +| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. In `CNO.agda` the `IsCNO` fields `cno-terminates` and `cno-reversible` are *definitional / vacuous* (hold for every program) — only `cno-identity` constrains a program; see "Scope of the Agda CNO fields" below. Canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1): exit 0 on all four modules locally on 2026-11-09 (Agda 2.6.3, stdlib v1.7.3, see receipts); CI still runs `--safe --without-K` only, so the combined profile is not yet a CI receipt | `proofs/z3/` — `ond/OND_checks.smt2` via `proofs/z3/verify.sh` | ACTIVE as bounded-check solver (CI `z3` job) -| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (z3 5.3.3, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below +| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat\|unsat` annotation. Latest receipt 2026-11-09 (z3 4.8.12, `Z3-CHECK OK`, 5 verdicts sat/unsat/sat/sat/sat) — see receipts below. The 2026-11-01 receipt (z3 5.3.3, sat/unsat/sat) predates the fix to the OND-3 dir 2 block, whose `unsat` was then vacuous | Bounds: finite/bounded programs under a finite declared `O`; not a general proof | `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2) @@ -123,6 +123,53 @@ reported as passing: the Agda `--safe --without-K` checks, the build remain CI receipts (`proofs.yml`: `agda`, `z3`, `idris` jobs), not sandbox receipts. Archived provers stay archived and unexecuted. +=== Reproduction receipts (this environment, 2026-11-09) + +Working tree on branch `claude/ephapax-architecture-plan-gzyctr` over `cbe9ae9`. + +* *Z3 — REPRODUCED HERE.* `Z3 version 4.8.12 - 64 bit` (not the 4.16.0 the +section below records for 2026-07-07, nor the 5.3.3 of 2026-11-01). +`z3 proofs/z3/ond/OND_checks.smt2` prints `sat unsat sat sat sat` (+ the OND-5 +model `s1 = 2, s2 = 3, pub = 0`), exit 0; `bash proofs/z3/verify.sh` → +`ok: ond/OND_checks.smt2 — 5 (check-sat) verdict(s) match`, `Z3-CHECK OK`, exit 0. +Mutation check: replacing `writer_step` by a step that copies the secret to +the output cell turns the OND-3 dir 2 verdict from `unsat` to `sat`, so the +check is no longer vacuous (see the Z3 section). +* *Agda — REPRODUCED HERE.* `Agda version 2.6.3`, stdlib registered by +`scripts/provision-agda-stdlib.sh` (agda-stdlib `v1.7.3` = +`0817da6877aa045932221134913d8511caa78d97`, into a scratch `AGDA_DIR`). +`agda --safe --without-K` on `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`, +`EchoBridgeCNO.agda`: exit 0 each. `agda --safe --without-K --cubical-compatible` +on the same four: exit 0 each. (The stdlib modules themselves were checked under +the stdlib's own pragmas, not re-checked under `--cubical-compatible`.) +* *Gate self-test.* `bash proofs/tests/gate-selftest.sh` → `GATE-SELFTEST OK: 27/27 cases`. +* *Idris 2* — not run here. + +=== Scope of the Agda CNO fields (`proofs/agda/CNO.agda`) + +Two of the four `IsCNO` fields hold for *every* program, so they certify +nothing about a particular program. This is stated beside the definitions too. + +* `terminates p s = ∃ s' . eval p s ≡ s'` — *definitional*. `eval` is a total, +structurally recursive function over a finite instruction list (`Jump` only +sets the pc; execution still walks the list), so `(eval p s , refl)` inhabits +it for all `p`, `s` (`terminates-always`). It establishes only that Agda +accepts `eval` as total. It does *not* establish termination of any machine +with real control flow, and does not separate CNOs from non-CNOs. +* `energy-dissipated _ _ _ = zero` and `thermodynamically-reversible p = ∀ s → +energy-dissipated p s (eval p s) ≡ zero` — *vacuous*. The right-hand side is the +constant `0`, so the field reduces to `0 ≡ 0` and is `λ s → refl` for every +program, including ones that erase memory. It establishes nothing about energy, +heat, Landauer's bound or physical reversibility; `cno-thermo-rev` carries no +information. No energy model exists in the active Agda stack (the archived Coq +physics files postulated Landauer as a `METAL-BOUNDARY` axiom). +* `IsCNO` does not use the non-trivial `reversible` predicate (existence of an +inverse program). `cno-pure` is implied by `cno-identity`. So the content of +`IsCNO p` is exactly `cno-identity`: `eval p s` agrees with `s` on memory +(pointwise), registers, I/O and pc. +* Claims such as "CNO terminates and is thermodynamically reversible" must not be +cited as established by the Agda development. + === Role of this repository (consumer, not estate-wide ground truth) absolute-zero is a *consumer and domain formalisation*: it applies standard @@ -149,11 +196,11 @@ Isabelle/HOL and Mizar (archived 2026-10-10) and *active* only for Agda, Z3 is the canonical summary. ==== -== Coq — VERIFIED (this environment) +== Coq — ARCHIVED (historical receipt, 2026-07-07; not built or gated since 2026-10-10) * `coqc` **8.18.0**; clean build from scratch (all `.vo`/`.glob` deleted first), via `coq_makefile -f _CoqProject` over **14/14 theories → zero errors**. -* Reproduce: `cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j`. +* Reproduce (historical; the tree is archived): `cd archive/proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j`. [cols="1,3",options="header"] |=== @@ -214,9 +261,9 @@ of these, each documented in-file with its blocker: These are the analogue of the OND-6 research fork: openly labelled, not silently 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 +2026-09-23, Coq 8.18). That WAS CI-gated until the 2026-10-10 archive ruling (no longer run): `archive/proofs/coq/audit/Assumptions.v` lists the 17 and +`archive/proofs/coq/check-assumptions.sh` (formerly the Coq job of `proofs.yml`, and the then-canonical +`proofs/verify-all-provers.sh` gate, now `archive/proofs/verify-all-provers.six-prover.sh`) failed 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 @@ -224,7 +271,7 @@ and/or the tagged parameters — see #171 for the census and the tag-grammar wor === Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites) -`proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the +`archive/proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the "composes to a no-op" characterisation the MAA framework (aletheia) cites. All five new results are **`Closed under the global context` (zero axioms)**: @@ -253,7 +300,7 @@ whereas the contract is two-sided. The in-file section header documents all thre This is a genuine statement-shape finding: it tells the aletheia contract to be stated two-sided and `=st=`-relative, not a proof dodged. -*Lean mirror — `proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).* +*Lean mirror — `archive/proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).* A functional-model mirror of the five bridge results was written for Lean 4, but it could **not** be machine-checked here: the Lean toolchain and Mathlib cache download from GitHub release assets, which the egress policy blocked (HTTP 403). @@ -265,9 +312,9 @@ total function and `ProgramState.eq` includes the PC), a stronger/cleaner form than the Coq `=st=`-relative statement — a disclosed cross-model difference, not a claim of literal equivalence. -== OND — VERIFIED (this environment), the disclosure pillar +== OND — the disclosure pillar (Coq/Lean legs ARCHIVED; Agda + Z3 legs active) -`proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero +`archive/proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero axioms** — every theorem is `Closed under the global context`: * OND-1 `is_OND O o` — nullity parameterised by an observation model `O` over an @@ -279,7 +326,7 @@ axioms** — every theorem is `Closed under the global context`: * OND-5 — a non-composition counterexample (two ONDs whose composite leaks by state-chaining). -Mirrored in *Lean 4* (`proofs/lean4/OND.lean`), *Agda* (`proofs/agda/OND.agda`), +Mirrored in *Lean 4* (`archive/proofs/lean4/OND.lean`), *Agda* (`proofs/agda/OND.agda`), and *Z3* (`proofs/z3/ond/OND_checks.smt2`, the bounded/finite instances). OND-7's residue register carries its first real instance (`proofs/residue/ct_select.residue`). *OND-6* (conditional composition, research @@ -293,17 +340,25 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. 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. +* Standard library: agda-stdlib `v1.7.3` (commit `0817da6`), registered by + `scripts/provision-agda-stdlib.sh` (`just provision-agda-stdlib`) — the same + script the CI `agda` job runs; it fails if the tag no longer resolves to the + pinned commit. Set `AGDA_DIR` to keep it out of `~/.agda`. +* Type-checking `CNO.agda` does not make its `terminates` / `energy-dissipated` + fields meaningful: see "Scope of the Agda CNO fields" above. +* 2026-11-09 receipt (Agda 2.6.3): all four modules exit 0 under + `--safe --without-K` and under `--safe --without-K --cubical-compatible`. -== Lean 4 — VERIFIED (this environment) +== Lean 4 — ARCHIVED (historical receipt; not built or gated since 2026-10-10) * Toolchain `leanprover/lean4:v4.16.0` with Mathlib `@ v4.16.0`; `lake exe cache get` + `lake build` → **build completed successfully**. Covers the CNO libraries and the - new `OND` library (`proofs/lean4/OND.lean`, core-Lean only, zero `sorry`). -* **Mathlib-free core is CI-gated (2026-09-22):** `proofs/lean4/check-core.sh` (job + new `OND` library (`archive/proofs/lean4/OND.lean`, core-Lean only, zero `sorry`). +* **Mathlib-free core WAS CI-gated (2026-09-22 until the 2026-10-10 archive ruling; the `lean` job no longer exists):** `archive/proofs/lean4/check-core.sh` (job `lean` in `.github/workflows/proofs.yml`; toolchain from `lean-toolchain`, elan fetched as a checksum-verified tarball, zero third-party actions) compiles `CNO`, `OND`, `CNOCategory`, `CNOBridge`, `FilesystemCNO`, `LambdaCNO` with plain `lean` - and runs `proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom + and runs `archive/proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom signature, the three occupancy predicates in full, the #125 derivations as negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere). `just verify-lean-core` runs the same script locally. @@ -312,7 +367,7 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror; with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from - `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted + `archive/proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5` counterexample the Coq side documents above); it is now the proved @@ -329,28 +384,44 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. identical to the pre-#174 commit and to the last green `main` run before #174). #167 stays open with finishing the port as its own acceptance criterion. -== Z3 — VERIFIED (this environment) - -* `z3` 4.16.0 on `proofs/z3/ond/OND_checks.smt2`: the OND-3 timing-leak witness is - `sat`, `writer`-is-OND is `unsat` (no secret distinguishes it), and the OND-5 - composite leak is `sat` with a concrete model — the "decidable for bounded - programs" demonstration. - -== Isabelle/HOL — VERIFIED (this environment) - -* `Isabelle2025-2`, session `AbsoluteZero-CNO` (`proofs/isabelle/ROOT`): `CNO.thy` +== Z3 — ACTIVE, bounded checks (`tested-only`) + +* *Historical (2026-07-07):* `z3` 4.16.0 on `proofs/z3/ond/OND_checks.smt2`: the + OND-3 timing-leak witness is `sat`, `writer`-is-OND is `unsat`, and the OND-5 + composite leak is `sat` with a concrete model. *Correction (2026-11-09):* the + `writer`-is-OND block then asserted `(not (and (= 0 0) (= 1 1)))` — the writer's + observables written down as constants — which is `unsat` for any program, so + that `unsat` checked nothing about the writer. +* *Current (2026-11-09, z3 4.8.12, 5 verdicts `sat unsat sat sat sat`):* the + OND-3 dir 2 block now models `writer_op` per `archive/proofs/coq/ond/OND.v`: + memory as `(Array Int Int)`, `inj s p`, `writer_step m = store m 0 7`, + `writer_time = 1`, and the `O_all` observable (output cell 2, time) *computed* + from them; asserting the observables differ for two secrets at the same public + input is `unsat` (writer is OND under `O_all`). A control block runs the same + query on a writer that copies the secret to the output cell (`sat`), and a + third block witnesses `writer_not_null` (`sat`). Mutating `writer_step` to leak + flips the main verdict to `sat`. +* *Remaining scope limit:* the OND-3 dir 1 block (`time_leaky secret = secret`) + and the OND-5 block (`p_out = 0`, `comp_out = secret`) still state the + observables directly rather than computing them from step functions; they are + hand transcriptions of the OND.v results, not independent checks of the + composition. + +== Isabelle/HOL — ARCHIVED (historical receipt; not built or gated since 2026-10-10) + +* `Isabelle2025-2`, session `AbsoluteZero-CNO` (`archive/proofs/isabelle/ROOT`): `CNO.thy` (repaired — the reserved-keyword `value` type was renamed and the failing `nop`/`step` lemmas fixed) and `OND.thy` (new, OND-1..5) build with no `sorry`/`oops`. -== Mizar — VERIFIED (this environment) +== Mizar — ARCHIVED (historical receipt; not built or gated since 2026-10-10) -* Mizar `8.1.15`; `accom CNO && verifier CNO` on `proofs/mizar/CNO.miz` completes +* Mizar `8.1.15`; `accom CNO && verifier CNO` on `archive/proofs/mizar/CNO.miz` completes with an **empty `CNO.err`** (zero errors). `MIZFILES` points at the bundled MML. The original article was machine-generated and unverifiable (277 errors); it was *rewritten* into a genuine article (StateSpace = pair of `Funcs(NAT,NAT)`; state-preserving / pure / reversible / terminating / thermo-reversible attributes; 12 proved theorems incl. composition with a real inverse construction). Requires the - committed private vocabulary `proofs/mizar/dict/cno.voc` (lowercase filename, needed + committed private vocabulary `archive/proofs/mizar/dict/cno.voc` (lowercase filename, needed on Linux). Verifier build artifacts are git-ignored. == Idris 2 — VERIFIED (this environment), the ABI boundary @@ -367,9 +438,13 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. * Multi-prover, not cross-prover *equivalence* — each prover checks its own formalisation of the two pillars. * "Verified here" = a reproduced compiler/checker run in this environment, not a - reading of in-file comments. Reproduce everything with - `proofs/verify-all-provers.sh`. -* Axiom census (machine-generated via `proofs/coq/census-assumptions.sh`): + reading of in-file comments. Reproduce the active stack with + `proofs/verify-active-provers.sh` (after `scripts/provision-agda-stdlib.sh`); + the former six-prover gate is archived as + `archive/proofs/verify-all-provers.six-prover.sh` and is not run. +* The Coq census and tag-grammar bullets below describe the archived tree + (`archive/proofs/coq/`); their scripts are no longer run. +* Axiom census (machine-generated via `archive/proofs/coq/census-assumptions.sh`): of 182 top-level theorems across the 14 theories, exactly **109 are closed under the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`, @@ -380,11 +455,11 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. generated driver fail outright instead of censusing it; the table now shows `Malbolge.MalbolgeCore | 7 | 7 | 0`). A directory with no `-R` binding is a hard census failure, never a silent skip. -* All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry +* All top-level declarations are verified by `archive/proofs/coq/check-axiom-tags.sh` to carry a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics. The two former unsound declarations in `StatMechBasis.v` (`prob_nonneg` and `prob_normalized`, which claimed Kolmogorov properties over raw unconstrained functions `ProgramState -> R`) have been deleted; zero theorems depend on either. * The 17 named headline theorems remain 100% closed under the global context (zero axioms, - CI-gated by `check-assumptions.sh`). + formerly CI-gated by `archive/proofs/coq/check-assumptions.sh`; not run since the 2026-10-10 archive ruling). diff --git a/proofs/agda/CNO.agda b/proofs/agda/CNO.agda index 5b52d65..64cf53b 100644 --- a/proofs/agda/CNO.agda +++ b/proofs/agda/CNO.agda @@ -162,6 +162,18 @@ eval (i ∷ is) s = eval is (step s i) -- A program terminates if evaluation produces a result -- For finite programs, this is always true +-- +-- SCOPE NOTE (2026-11-09) — `terminates` is DEFINITIONAL, not a result. +-- `eval` is a total, structurally recursive Agda function over a finite list +-- (no loop: `Jump` only sets the pc and execution still walks the list), so +-- `eval p s` always exists and `terminates p s = ∃ s' . eval p s ≡ s'` is +-- inhabited by `(eval p s , refl)` for EVERY program and state. +-- What it establishes: nothing beyond Agda accepting `eval` as total. +-- What it does NOT establish: termination of any machine with real control +-- flow (jumps that loop, a halting PC semantics), nor any property that +-- distinguishes a CNO from a non-CNO. The `cno-terminates` field of `IsCNO` +-- is therefore satisfiable by every program. See PROOF-STATUS.adoc, +-- "Scope of the Agda CNO fields". terminates : Program → ProgramState → Set terminates p s = ∃ λ s' → eval p s ≡ s' @@ -198,6 +210,21 @@ reversible p = ∃ λ p-inv → ∀ s → eval p-inv (eval p s) ≡ s ---------------------------------------------------------------------------- -- Energy dissipated (simplified model) +-- +-- SCOPE NOTE (2026-11-09) — `energy-dissipated` is the CONSTANT 0 and +-- `thermodynamically-reversible` is VACUOUS. +-- `energy-dissipated _ _ _ = zero` ignores its program and both states, so +-- `thermodynamically-reversible p` reduces to `∀ s → zero ≡ zero` and holds for +-- EVERY program by `λ s → refl` — including programs that erase memory. +-- What it establishes: nothing about energy, heat, Landauer's bound or +-- physical reversibility; the `cno-reversible` field of `IsCNO` and +-- `cno-thermo-rev` carry no information. +-- What it does NOT establish: that a CNO dissipates no energy, or any link +-- between information erasure and dissipation. (No energy model exists in +-- the active Agda stack; the archived Coq physics files postulated Landauer +-- as a METAL-BOUNDARY axiom.) Note also that `IsCNO` does not use the +-- non-trivial `reversible` predicate above. See PROOF-STATUS.adoc, +-- "Scope of the Agda CNO fields". energy-dissipated : Program → ProgramState → ProgramState → ℕ energy-dissipated _ _ _ = zero @@ -211,6 +238,11 @@ thermodynamically-reversible p = ---------------------------------------------------------------------------- -- A Certified Null Operation +-- +-- Of the four fields, only `cno-identity` constrains `p` (`cno-pure` is +-- implied by it: purity is the io + memory part of `state-eq`). +-- `cno-terminates` and `cno-reversible` hold for every program (see the +-- SCOPE NOTEs on `terminates` and `energy-dissipated`). record IsCNO (p : Program) : Set where field cno-terminates : ∀ s → terminates p s diff --git a/proofs/verify-active-provers.sh b/proofs/verify-active-provers.sh index e554a87..5964843 100755 --- a/proofs/verify-active-provers.sh +++ b/proofs/verify-active-provers.sh @@ -9,7 +9,8 @@ # # Every active prover is REQUIRED: an absent toolchain is a failure, never a skip. # Needs on PATH: agda, z3, idris2. The Agda standard library is registered via -# ~/.agda/libraries (see .github/workflows/proofs.yml for the pinned setup). +# ~/.agda/libraries: run scripts/provision-agda-stdlib.sh first (pinned v1.7.3, +# the same script CI runs). set -uo pipefail export PATH="$HOME/.local/bin:$HOME/.elan/bin:$PATH" HERE="$(cd "$(dirname "$0")" && pwd)" diff --git a/proofs/z3/ond/OND_checks.smt2 b/proofs/z3/ond/OND_checks.smt2 index 8744670..fe54ac7 100644 --- a/proofs/z3/ond/OND_checks.smt2 +++ b/proofs/z3/ond/OND_checks.smt2 @@ -1,5 +1,5 @@ ; Absolute Zero — OND pillar, bounded/finite verification (Z3) -; Mirrors proofs/coq/ond/OND.v. Memory cells are integers: +; Mirrors archive/proofs/coq/ond/OND.v (archived 2026-10-10). Memory cells are integers: ; cell0 = secret, cell1 = public, cell2 = declared output channel. ; "Decidable for bounded programs under a finite observation model O" (OND-ROADMAP). @@ -14,12 +14,53 @@ (pop) ; ---- OND-3 dir 2: writer is OND on (output,timing) yet NOT a null op. -; output cell2 stays 0, time = 1 (both secret-independent) => OND holds: +; Modelled per archive/proofs/coq/ond/OND.v (writer_op, inj, run, O_all): +; memory = (Array Int Int), cells >= 0 stand for OND.v's nat addresses; +; inj s p = all cells 0, then cell0 := s, cell1 := p (cell2 stays 0); +; writer_step = mem_update m secret_cell 7 (op_step writer_op); +; writer_time = 1 (op_time writer_op); +; run = (output cell2 of writer_step (inj s p), writer_time (inj s p)). +; The observable is COMPUTED from the step function, not written down as a +; constant. (Before 2026-11-09 this block asserted (not (and (= 0 0) (= 1 1))), +; which is unsat for any program and so checked nothing about the writer.) (push) -(declare-const s1 Int) (declare-const s2 Int) -; observable of writer = (out=0, time=1) regardless of secret -(assert (not (and (= 0 0) (= 1 1)))) ; negation of "observable equal across secrets" -(check-sat) ; expect unsat => writer IS OND (no secret distinguishes its observable) +(define-fun inj ((s Int) (p Int)) (Array Int Int) + (store (store ((as const (Array Int Int)) 0) 0 s) 1 p)) +(define-fun writer_step ((m (Array Int Int))) (Array Int Int) (store m 0 7)) +(define-fun writer_time ((m (Array Int Int))) Int 1) +(define-fun writer_out ((s Int) (p Int)) Int (select (writer_step (inj s p)) 2)) +(define-fun writer_tm ((s Int) (p Int)) Int (writer_time (inj s p))) +(declare-const s1 Int) (declare-const s2 Int) (declare-const pub Int) +(assert (>= s1 0)) (assert (>= s2 0)) (assert (>= pub 0)) +; negation of is_OND O_all writer_op: some secret pair, same public input, +; whose (output, time) observables differ. +(assert (not (and (= (writer_out s1 pub) (writer_out s2 pub)) + (= (writer_tm s1 pub) (writer_tm s2 pub))))) +(check-sat) ; expect unsat => writer IS OND under O_all (no secret pair distinguishes it) +(pop) + +; ---- OND-3 dir 2, control: the same check BITES on a writer that leaks. +; leaky_writer writes the secret to the output cell; same model, same query. +; If this were unsat the query above would be vacuous. +(push) +(define-fun inj ((s Int) (p Int)) (Array Int Int) + (store (store ((as const (Array Int Int)) 0) 0 s) 1 p)) +(define-fun leak_step ((m (Array Int Int))) (Array Int Int) (store m 2 (select m 0))) +(define-fun leak_out ((s Int) (p Int)) Int (select (leak_step (inj s p)) 2)) +(declare-const s1 Int) (declare-const s2 Int) (declare-const pub Int) +(assert (>= s1 0)) (assert (>= s2 0)) (assert (>= pub 0)) +; time is the constant 1 for both runs, so the observables differ iff outputs do. +(assert (not (= (leak_out s1 pub) (leak_out s2 pub)))) +(check-sat) ; expect sat: control — a leaking writer IS distinguished by the same query +(pop) + +; ---- OND-3 dir 2, second half: writer is NOT a null op (writer_not_null). +; Some memory is changed by writer_step (cell0 becomes 7). +(push) +(define-fun writer_step ((m (Array Int Int))) (Array Int Int) (store m 0 7)) +(declare-const m (Array Int Int)) +(assert (not (= (writer_step m) m))) +(check-sat) ; expect sat: a memory writer_step changes, so writer is not a null op (pop) ; ---- OND-5: p_op and q_op each OND under O_all, composite p;q LEAKS. diff --git a/scripts/provision-agda-stdlib.sh b/scripts/provision-agda-stdlib.sh new file mode 100755 index 0000000..2a59dc1 --- /dev/null +++ b/scripts/provision-agda-stdlib.sh @@ -0,0 +1,62 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Absolute Zero — reproducible Agda standard-library registration. +# +# The Agda proofs (proofs/agda/, absolute-zero.agda-lib) `depend: standard-library`. +# This script fetches ONE pinned agda-stdlib release, checks that the tag still +# resolves to the pinned commit, and registers it for Agda. CI +# (.github/workflows/proofs.yml, `agda` job) and local runs use this same script, +# so both type-check against the same library bytes. +# +# Pin: agda-stdlib v1.7.3 (the release that matches Agda 2.6.3, the version +# Ubuntu 24.04 ships and CI installs). Tag v1.7.3 -> commit STDLIB_COMMIT below, +# read with `git ls-remote https://github.com/agda/agda-stdlib.git refs/tags/v1.7.3^{}` +# on 2026-11-09. If the tag is ever moved, this script fails rather than +# silently using different sources. +# +# Usage: +# bash scripts/provision-agda-stdlib.sh +# Environment (all optional): +# AGDA_DIR Agda's config directory (Agda's own variable; default ~/.agda). +# `libraries` and `defaults` are written here. +# AGDA_STDLIB_DIR Where to put the checkout (default $AGDA_DIR/agda-stdlib-v1.7.3). +# +# Idempotent: an existing checkout at the pinned commit is reused. The +# `libraries` / `defaults` files are OVERWRITTEN to name exactly this library, +# so run it with a dedicated AGDA_DIR if you keep other Agda libraries in ~/.agda. +set -euo pipefail + +STDLIB_REPO="https://github.com/agda/agda-stdlib.git" +STDLIB_TAG="v1.7.3" +STDLIB_COMMIT="0817da6877aa045932221134913d8511caa78d97" + +AGDA_DIR="${AGDA_DIR:-$HOME/.agda}" +AGDA_STDLIB_DIR="${AGDA_STDLIB_DIR:-$AGDA_DIR/agda-stdlib-$STDLIB_TAG}" + +mkdir -p "$AGDA_DIR" + +if [ -d "$AGDA_STDLIB_DIR/.git" ]; then + echo "reusing checkout $AGDA_STDLIB_DIR" +else + git -c advice.detachedHead=false clone -q --depth 1 --branch "$STDLIB_TAG" "$STDLIB_REPO" "$AGDA_STDLIB_DIR" +fi + +have="$(git -C "$AGDA_STDLIB_DIR" rev-parse HEAD)" +if [ "$have" != "$STDLIB_COMMIT" ]; then + echo "PROVISION FAILED: $AGDA_STDLIB_DIR is at $have, expected $STDLIB_TAG = $STDLIB_COMMIT" >&2 + exit 1 +fi + +# absolute-zero.agda-lib depends on the unversioned name `standard-library`; +# the upstream manifest calls itself `standard-library-1.7.3`. Rename in place +# (the only local modification to the checkout). +lib="$AGDA_STDLIB_DIR/standard-library.agda-lib" +[ -f "$lib" ] || { echo "PROVISION FAILED: $lib missing" >&2; exit 1; } +sed -i 's/^name: .*/name: standard-library/' "$lib" + +printf '%s\n' "$lib" > "$AGDA_DIR/libraries" +printf '%s\n' "standard-library" > "$AGDA_DIR/defaults" + +echo "registered standard-library ($STDLIB_TAG @ $STDLIB_COMMIT)" +echo " libraries: $AGDA_DIR/libraries -> $lib" +echo " defaults: $AGDA_DIR/defaults" From 37c792a046d74c8bc1e3c1ace5d7bbe6a8a49288 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:25:46 +0000 Subject: [PATCH 2/2] docs: point archived-prover references at archive/proofs/ and the active gate Follow-up to the PROOF-STATUS.adoc reconciliation in this PR. Docs that state current facts now cite archive/proofs/{coq,lean4,isabelle,mizar}/... and archive/proofs/verify-all-provers.six-prover.sh instead of the removed proofs/... paths, and say "archived" / past tense where they claimed those provers are currently built, verified or CI-gated. The active gate is named as proofs/verify-active-provers.sh (Agda + Z3 bounded + Idris 2 ABI). - README, EXPLAINME, ROADMAP: layout rows, evidence pointers, "what verifies" receipts and the CI row. - docs/proof-debt.adoc: ledger file pointers moved to archive/proofs/, with an archive note in the status banner. - docs/COOKBOOK.adoc, ECHIDNA.adoc: archive notice; input paths moved. - docs/JUSTFILE-COOKBOOK.adoc: build-all matches the Justfile; build-coq, build-lean and verify-coq marked historical; clean-coq/clean-lean paths match the Justfile. - docs/OND-PILLAR-STRUCTURE.adoc, OND-ROADMAP, ECOSYSTEM-CONNECTIONS, MACHINE_VERIFICATION, VERIFICATION_RESULTS: status text and commands. - docs/wiki: Architecture data flow, Verification, Proof-Systems, Home, Roadmap, Audit-Trail. Dated records (CHANGELOG, AUDIT resolved items, docs/archive/*, session notes, historical plans) are left as written. No proof file changed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- ECHIDNA.adoc | 40 +++++++++++++--------- EXPLAINME.adoc | 14 ++++---- README.adoc | 28 ++++++++++------ ROADMAP.adoc | 28 ++++++++++------ docs/COOKBOOK.adoc | 44 +++++++++++++++--------- docs/ECOSYSTEM-CONNECTIONS.adoc | 6 ++-- docs/JUSTFILE-COOKBOOK.adoc | 45 ++++++++++++------------- docs/MACHINE_VERIFICATION.adoc | 8 ++--- docs/OND-PILLAR-STRUCTURE.adoc | 22 ++++++++---- docs/OND-ROADMAP.adoc | 5 +-- docs/VERIFICATION_RESULTS.adoc | 8 +++-- docs/proof-debt.adoc | 59 ++++++++++++++++++--------------- docs/wiki/Architecture.md | 16 ++++----- docs/wiki/Audit-Trail.md | 4 +-- docs/wiki/Home.md | 12 +++---- docs/wiki/Proof-Systems.md | 28 ++++++++++------ docs/wiki/Roadmap.md | 6 ++-- docs/wiki/Verification.md | 28 +++++++++------- 18 files changed, 231 insertions(+), 170 deletions(-) diff --git a/ECHIDNA.adoc b/ECHIDNA.adoc index cff270a..2dea62d 100644 --- a/ECHIDNA.adoc +++ b/ECHIDNA.adoc @@ -15,6 +15,16 @@ This document describes integrating the **hyperpolymath ECHIDNA neurosymbolic th **Status**: ✅ **TRUSTED** - Production-ready with comprehensive trust framework +[IMPORTANT] +.Archive notice (2026-10-10) +==== +This plan was written around the Coq and Lean 4 trees, which were archived on +2026-10-10 under `archive/proofs/` (with Isabelle/HOL and Mizar) and are no +longer built or gated. Input paths below point at `archive/proofs/…`. The active +stack is Agda (`proofs/agda/`) + Z3 bounded checks (`proofs/z3/`) + the Idris 2 +ABI, run by `proofs/verify-active-provers.sh`; see `PROOF-STATUS.adoc`. +==== + --- == Trust Assessment @@ -95,7 +105,7 @@ This document describes integrating the **hyperpolymath ECHIDNA neurosymbolic th == Architecture Integration -=== Current Absolute Zero Stack +=== Absolute Zero Stack (as of writing; historical since 2026-10-10) ``` ┌─────────────────────────────────────────┐ @@ -229,7 +239,7 @@ pack install idris2-echidna # Test validator pack exec idris2-echidna -- validate \ - --proof ~/Documents/hyperpolymath-repos/absolute-zero/proofs/coq/common/CNO.v \ + --proof ~/Documents/hyperpolymath-repos/absolute-zero/archive/proofs/coq/common/CNO.v \ --prover Coq ``` @@ -248,17 +258,17 @@ cd ~/Documents/hyperpolymath-repos/absolute-zero mkdir -p tools/echidna/cno-corpus # Coq proofs (Phase 1-4 complete) -find proofs/coq -name "*.v" -exec cat {} \; > tools/echidna/cno-corpus/coq_proofs.v +find archive/proofs/coq -name "*.v" -exec cat {} \; > tools/echidna/cno-corpus/coq_proofs.v # Lean 4 proofs -find proofs/lean4 -name "*.lean" -exec cat {} \; > tools/echidna/cno-corpus/lean_proofs.lean +find archive/proofs/lean4 -name "*.lean" -exec cat {} \; > tools/echidna/cno-corpus/lean_proofs.lean # Z3 SMT specifications cp proofs/z3/cno_properties.smt2 tools/echidna/cno-corpus/ # Count theorems -echo "Coq theorems:" $(grep -c "Theorem\|Lemma" proofs/coq/common/CNO.v) -echo "Lean theorems:" $(grep -c "theorem\|lemma" proofs/lean4/CNO.lean) +echo "Coq theorems:" $(grep -c "Theorem\|Lemma" archive/proofs/coq/common/CNO.v) +echo "Lean theorems:" $(grep -c "theorem\|lemma" archive/proofs/lean4/CNO.lean) echo "Z3 assertions:" $(grep -c "assert.*theorem" proofs/z3/cno_properties.smt2) ``` @@ -340,7 +350,7 @@ echidna-repl: echidna-complete: @echo "Attempting to complete 21 Admitted proofs..." cd tools/echidna/neurosym && ./target/release/echidna complete \ - --proof-dir ../../proofs/coq \ + --proof-dir ../../archive/proofs/coq \ --output-dir ../../proofs/coq-completed \ --prover Coq \ --max-tactics 50 @@ -359,7 +369,7 @@ Target: 21 Admitted → 0 cd ~/Documents/hyperpolymath-repos/absolute-zero # List all Admitted proofs -grep -rn "Admitted" proofs/coq/ | tee admitted_list.txt +grep -rn "Admitted" archive/proofs/coq/ | tee admitted_list.txt # Use ECHIDNA to suggest completions just echidna-start @@ -371,7 +381,7 @@ cat proofs/coq-completed/*.v # Manually verify and integrate for file in proofs/coq-completed/*.v; do echo "Reviewing: $file" - diff proofs/coq/$(basename $file) $file + diff archive/proofs/coq/$(basename $file) $file # If valid, replace done ``` @@ -379,7 +389,7 @@ done **Example ECHIDNA session:** ```coq -echidna> load proofs/coq/physics/StatMech.v +echidna> load archive/proofs/coq/physics/StatMech.v echidna> focus bennett_logical_implies_thermodynamic echidna> suggest @@ -418,7 +428,7 @@ cd ~/Documents/hyperpolymath-repos/absolute-zero just echidna-start # Multi-prover verification -for thm in $(grep "Theorem\|Lemma" proofs/coq/common/CNO.v | awk '{print $2}'); do +for thm in $(grep "Theorem\|Lemma" archive/proofs/coq/common/CNO.v | awk '{print $2}'); do echo "Verifying $thm..." # Translate to multiple formats @@ -508,7 +518,7 @@ echidna_neurosym: # Verify all proofs with multi-prover consensus - cd ../../.. - ./tools/echidna/neurosym/target/release/echidna verify-all \ - --proof-dir proofs/coq \ + --proof-dir archive/proofs/coq \ --provers "Coq,Lean4,Z3" \ --consensus 2 \ --output echidna-report.json @@ -574,7 +584,7 @@ chmod +x .git/hooks/pre-commit # Interactive REPL session just echidna-repl -echidna> load proofs/coq/physics/StatMech.v +echidna> load archive/proofs/coq/physics/StatMech.v echidna> focus cno_logically_reversible echidna> suggest echidna> apply suggestion 1 @@ -604,14 +614,14 @@ cat verification_report.json | jq '.consensus' ```bash # Translate Coq proof to Lean 4 ./tools/echidna/neurosym/target/release/echidna translate \ - --input proofs/coq/common/CNO.v \ + --input archive/proofs/coq/common/CNO.v \ --from Coq \ --to Lean4 \ --output proofs/lean4/CNO_translated.lean # Verify translation is equivalent ./tools/echidna/neurosym/target/release/echidna diff \ - --proof1 proofs/coq/common/CNO.v \ + --proof1 archive/proofs/coq/common/CNO.v \ --proof2 proofs/lean4/CNO_translated.lean ``` diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5d5ebfc..2b62704 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -9,7 +9,7 @@ This file backs every factual claim in link:README.adoc[README.adoc] with code p [IMPORTANT] ==== -*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`. +*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths of the form `proofs/coq/…` / `proofs/lean4/…` in older prose and dated records refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`. ==== == Claim-to-implementation map @@ -44,7 +44,7 @@ OND proofs are axiom-free *relative to the declared observation model `O`*. The ____115 Qed / 0 Admitted / 61 Axioms across 13 files — every theorem is discharged (no Admitted), but the development rests on 61 Coq + 52 Lean axioms.____ How this is implemented:: -`link:proofs/coq/[]` contains all CNO theories. CI runs `coq_makefile` and confirms Qed counts and axiom counts. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are *assumed* but not derived within Coq. +`link:archive/proofs/coq/[]` contains all CNO theories (ARCHIVED 2026-10-10, not built or gated). Until the archive ruling, CI ran `coq_makefile` and confirmed Qed counts and axiom counts; it no longer does. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are *assumed* but not derived within Coq. Caveat:: **This is not an axiom-free machine-checked proof.** "Machine-checked" here means the proof is valid *assuming the axioms hold*. If an axiom is false in the intended model, the theorem fails. The 61 Coq + 52 Lean axioms represent the proof debt. Discharging them (especially quantum unitarity and filesystem inverse laws) is the next major obligation. @@ -55,10 +55,10 @@ Caveat:: ____Verify CNO properties in six independent proof systems.____ How this is implemented:: -Artefacts exist for Coq, Lean 4, Agda, Z3, Isabelle, and Mizar in `link:proofs/[]`. `link:proofs/verify-all-provers.sh[]` orchestrates verification. CI gates Coq, Lean 4, and Agda. +Active artefacts (Agda, Z3) are in `link:proofs/[]`; `link:proofs/verify-active-provers.sh[]` runs the active gate (Agda + Z3 bounded + Idris 2 ABI), and CI (`proofs.yml`: `agda`, `z3`, `idris` jobs) gates the same three. The Coq, Lean 4, Isabelle/HOL and Mizar artefacts are ARCHIVED under `link:archive/proofs/[]`, as is the former six-prover gate (`link:archive/proofs/verify-all-provers.six-prover.sh[]`); they are not built or gated. Caveat:: -**Z3, Isabelle, and Mizar are generated but not yet run in CI.** The artefacts exist but are not evidence until machine-executed and green. The "six prover" claim describes the target architecture, not the current CI gate. +**The six-prover claim is historical.** All six provers were reproduced on 2026-07-07 (see link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]); since the 2026-10-10 archive ruling only Agda, Z3 (bounded) and the Idris 2 ABI are run. Archived artefacts are not current evidence. === Thermodynamic reversibility follows from Landauer's principle @@ -66,7 +66,7 @@ Caveat:: ____ThermodynamicallyReversible(p) — Zero energy____ How this is implemented:: -`link:proofs/coq/physics/StatMech.v[]` and `link:proofs/lean4/StatMech.lean[]` formalise Landauer's principle and Bennett's reversible computing, proving CNOs dissipate zero energy because they erase no information. +`link:archive/proofs/coq/physics/StatMech.v[]` and `link:archive/proofs/lean4/StatMech.lean[]` (both ARCHIVED 2026-10-10, not built or gated) formalise Landauer's principle and Bennett's reversible computing, proving CNOs dissipate zero energy because they erase no information. Caveat:: The physics formalisation relies on axioms about the physical model (e.g., that the thermodynamic system satisfies the assumptions of Landauer's principle). This is standard for formalisations of physics, but the gap between the mathematical model and physical metal is real. @@ -88,8 +88,8 @@ This is a standard result. The practical consequence is that the verified CNOs i |=== | Technology / Pattern | Used here | Also used in -| Coq CNO/OND formalisation -| `proofs/coq/` +| Coq CNO/OND formalisation (archived) +| `archive/proofs/coq/` | link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoBridgeCNO) | Multi-prover pattern diff --git a/README.adoc b/README.adoc index 7aa1739..d0c44bd 100644 --- a/README.adoc +++ b/README.adoc @@ -116,7 +116,7 @@ Core proofs -- Malbolge / Brainfuck / Whitespace CNO verification *Novel application* -`+interpreters/+`, `+proofs/coq/malbolge/+` +`+interpreters/+`, `+archive/proofs/coq/malbolge/+` (archived) -- |=== @@ -227,26 +227,32 @@ foundation), the Z3 checks are `tested-only` (bounded), and OND-6 is `open`. [verse] -- -`+proofs/coq/+` -Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND +`+proofs/agda/+` +Active Agda proofs: CNO, OND, EchoBridge (checked in CI, `--safe --without-K`) -- [verse] -- -`+proofs/lean4/+` -Lean 4 mirrors of CNO and OND modules +`+proofs/z3/+` +Active Z3 bounded checks (expect-annotated; `tested-only`) -- [verse] -- -`+proofs/agda/+`, `+proofs/z3/+`, `+proofs/isabelle/+`, `+proofs/mizar/+` -Additional prover artefacts (Agda checked in CI; others generated but not yet run) +`+archive/proofs/coq/+` +ARCHIVED 2026-10-10 (not built or gated): Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem; OND module in `+archive/proofs/coq/ond/+` -- [verse] -- -`+proofs/ond/+` -OND Coq module (OND-1..5 proved, zero axioms) +`+archive/proofs/lean4/+` +ARCHIVED 2026-10-10 (not built or gated): Lean 4 mirrors of CNO and OND modules +-- + +[verse] +-- +`+archive/proofs/isabelle/+`, `+archive/proofs/mizar/+` +ARCHIVED 2026-10-10 (not built or gated): Isabelle/HOL and Mizar artefacts -- [verse] @@ -313,6 +319,6 @@ Prose documentation is licensed under CC-BY-SA-4.0; see [verse] -- -`+proofs/coq/+` -Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND +`+archive/proofs/coq/+` +ARCHIVED 2026-10-10 (not built or gated): Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND -- diff --git a/ROADMAP.adoc b/ROADMAP.adoc index df073c8..89838d7 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -42,21 +42,25 @@ See `PROOF-STATUS.adoc` for the canonical active-vs-archived proof-status table. === What genuinely verifies -* *Coq (reproduced):* **14 theories** compile from scratch under `coqc 8.18.0` +The Coq, Lean 4, Isabelle/HOL and Mizar entries below are *historical receipts +(2026-07-07)*: those trees were ARCHIVED on 2026-10-10 under `archive/proofs/` and +are no longer built or gated. Agda, Z3 (bounded) and the Idris 2 ABI are active. + +* *Coq (reproduced 2026-07-07; ARCHIVED):* **14 theories** compiled from scratch under `coqc 8.18.0` (`coq_makefile -f _CoqProject`) — `common`, `category`, `quantum`, `lambda`, `filesystem`, `physics`, `malbolge`, and the new `ond`. Both pillars. -* *OND pillar (reproduced):* `proofs/coq/ond/OND.v` proves **OND-1..5** with +* *OND pillar (reproduced):* the archived `archive/proofs/coq/ond/OND.v` proved **OND-1..5** with **zero axioms** (every theorem `Closed under the global context`); mirrored in Lean 4, Agda, and Z3. * *Agda (reproduced):* `CNO.agda`, `OND.agda`, `EchoBridgeCNO.agda` type-check under `agda 2.6.3` (`--safe --without-K`); funext is an *explicit hypothesis*. -* *Lean 4 (reproduced):* `lake build` green with Mathlib — CNO libraries + the - new `OND` library (`proofs/lean4/OND.lean`, 0 `sorry`). +* *Lean 4 (reproduced 2026-07-07; ARCHIVED):* `lake build` was green with Mathlib — CNO libraries + the + new `OND` library (`archive/proofs/lean4/OND.lean`, 0 `sorry`). * *Z3 (reproduced):* CNO checks + OND bounded instances (`proofs/z3/ond/OND_checks.smt2`). -* *Isabelle/HOL (reproduced):* session `AbsoluteZero-CNO` — `CNO.thy` (repaired) - + `OND.thy` build under Isabelle2025-2, 0 `sorry`. -* *Mizar (reproduced):* `CNO.miz` rewritten into a genuine 12-theorem article; - `accom`+`verifier` → empty `CNO.err` (needs `proofs/mizar/dict/cno.voc`). +* *Isabelle/HOL (reproduced 2026-07-07; ARCHIVED):* session `AbsoluteZero-CNO` — `CNO.thy` (repaired) + + `OND.thy` built under Isabelle2025-2, 0 `sorry`. +* *Mizar (reproduced 2026-07-07; ARCHIVED):* `CNO.miz` rewritten into a genuine 12-theorem article; + `accom`+`verifier` → empty `CNO.err` (needs `archive/proofs/mizar/dict/cno.voc`). * *Idris 2 ABI (reproduced):* `absolute-zero-abi.ipkg` builds clean. * *Rust interpreters:* Brainfuck and Whitespace interpreters are real. @@ -77,8 +81,10 @@ See `PROOF-STATUS.adoc` for the canonical active-vs-archived proof-status table. coinductive/step-indexed β non-termination argument). | OND-6 | Open by design | The conditional-composition theorem — research capstone; OND-1..5 landed, so the pillar is in honest, publishable shape. -| CI proof verification | Missing | No workflow yet runs the provers; the local - gate `proofs/verify-all-provers.sh` is the reproducible source of truth. +| CI proof verification | Active stack only | The CI `agda`, `z3` and `idris` jobs + (`proofs.yml`) check the active stack; `proofs/verify-active-provers.sh` is the local gate for the active + stack. The former six-prover gate is archived + (`archive/proofs/verify-all-provers.six-prover.sh`) and not run. | Paper | Draft stub | `papers/.latex/main.tex` is a lone draft. | Tests | Empty placeholder | `tests/` holds a README only. |=== @@ -137,7 +143,7 @@ coordinates as a pinned submodule. The theorem MAA actually cites is the *general reversibility biconditional*. * [x] *Reversibility <-> CNO bridge — landed in Coq (2026-07-16, zero axioms).* - `proofs/coq/common/CNO.v` proves the forward direction of the aletheia contract + `archive/proofs/coq/common/CNO.v` (archived 2026-10-10) proves the forward direction of the aletheia contract (`reversible_bridge_forward`: a two-sided inverse makes both composites `cno_equiv _ []`) and the backward direction up to `=st=` (`reversible_bridge_backward_upto`), via the core lemma diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc index ed13ae2..36edcbe 100644 --- a/docs/COOKBOOK.adoc +++ b/docs/COOKBOOK.adoc @@ -13,6 +13,18 @@ v1.0, 2025-11-22 This cookbook provides practical, step-by-step instructions for working with the *Absolute Zero* project — a formal verification framework for Certified Null Operations (CNOs). +[IMPORTANT] +.Archive notice (2026-10-10) +==== +The Coq, Lean 4, Isabelle/HOL and Mizar trees this cookbook was written around +were archived on 2026-10-10 under `archive/proofs/` and are no longer built or +gated. The active stack is Agda (`proofs/agda/`) + Z3 bounded checks +(`proofs/z3/`) + the Idris 2 ABI; run `just verify` +(`proofs/verify-active-provers.sh`). Paths below that name the archived provers +point at `archive/proofs/…`; the workflows and status figures for those provers +are historical. See `PROOF-STATUS.adoc` for the canonical status table. +==== + === What This Project Does Absolute Zero formally proves that certain programs provably compute *nothing*: @@ -30,11 +42,11 @@ Absolute Zero formally proves that certain programs provably compute *nothing*: |Coq 8.19 |Core CNO theory, physics proofs -|70% complete +|ARCHIVED 2026-10-10 (historical: 70% complete) |Lean 4 |Alternative verification, category theory -|66% complete +|ARCHIVED 2026-10-10 (historical: 66% complete) |Z3 4.13 |SMT-based automated verification @@ -46,7 +58,7 @@ Absolute Zero formally proves that certain programs provably compute *nothing*: |Isabelle/HOL |Higher-order logic -|100% (foundational) +|ARCHIVED 2026-10-10 (historical: 100% foundational) |=== == Quick Start @@ -158,13 +170,13 @@ If neither `just` nor Oil shell is available: [source,bash] ---- # Build Coq proofs -cd proofs/coq/common && coqc CNO.v +cd archive/proofs/coq/common && coqc CNO.v cd ../physics && coqc -R ../common CNO StatMech.v cd ../physics && coqc -R ../common CNO LandauerDerivation.v cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v # Build Lean 4 proofs -cd proofs/lean4 && lake build +cd archive/proofs/lean4 && lake build # Verify Z3 specifications z3 proofs/z3/cno_properties.smt2 @@ -180,7 +192,7 @@ npm install && npm run build ==== Project Structure [source,text] ---- -proofs/coq/ +archive/proofs/coq/ ├── common/ │ └── CNO.v # Core CNO theory (Phase 1) ├── physics/ @@ -233,10 +245,10 @@ just verify-coq [source,bash] ---- # How many theorems are incomplete? -grep -r "Admitted\." proofs/coq/ | wc -l +grep -r "Admitted\." archive/proofs/coq/ | wc -l # Where are they? -grep -r "Admitted\." proofs/coq/ +grep -r "Admitted\." archive/proofs/coq/ # Proof statistics just proof-status @@ -247,7 +259,7 @@ just proof-status ==== Project Structure [source,text] ---- -proofs/lean4/ +archive/proofs/lean4/ ├── lakefile.lean # Build configuration ├── CNO.lean # Core CNO theory ├── StatMech.lean # Statistical mechanics @@ -280,7 +292,7 @@ theorem my_new_theorem (p : CNO.Program) : [source,bash] ---- -cd proofs/lean4 +cd archive/proofs/lean4 # Update dependencies lake update @@ -329,7 +341,7 @@ z3 proofs/z3/cno_properties.smt2 *Status*: All proofs complete, 0 `Admitted` -Key theorems in `proofs/coq/common/CNO.v`: +Key theorems in `archive/proofs/coq/common/CNO.v`: [cols="1,2"] |=== @@ -531,7 +543,7 @@ Valence Shell operations can be proven as CNOs: [source,coq] ---- (* Precondition: no directory already at [path] — without it the law is false - (repeat mkdir is idempotent), see proofs/coq/filesystem/FilesystemCNO.v and + (repeat mkdir is idempotent), see archive/proofs/coq/filesystem/FilesystemCNO.v and absolute-zero#125. *) Theorem mkdir_rmdir_is_cno : forall (path : Path) (fs : Filesystem), @@ -548,7 +560,7 @@ Theorem mkdir_rmdir_is_cno : *Solution*: [source,bash] ---- -cd proofs/coq/common && coqc CNO.v +cd archive/proofs/coq/common && coqc CNO.v ---- *Problem*: `Admitted` statements @@ -562,7 +574,7 @@ cd proofs/coq/common && coqc CNO.v *Solution*: [source,bash] ---- -cd proofs/lean4 +cd archive/proofs/lean4 lake update ---- @@ -671,10 +683,10 @@ See `FORMAL_ANALYSIS_PHASE1.md` for complete analysis. |`VERIFICATION_RESULTS.md` |Latest verification results -|`proofs/coq/common/CNO.v` +|`archive/proofs/coq/common/CNO.v` |Core Coq proofs (Phase 1) -|`proofs/lean4/CNO.lean` +|`archive/proofs/lean4/CNO.lean` |Core Lean 4 proofs |`proofs/z3/cno_properties.smt2` diff --git a/docs/ECOSYSTEM-CONNECTIONS.adoc b/docs/ECOSYSTEM-CONNECTIONS.adoc index a8b3508..94a2621 100644 --- a/docs/ECOSYSTEM-CONNECTIONS.adoc +++ b/docs/ECOSYSTEM-CONNECTIONS.adoc @@ -19,8 +19,8 @@ sibling projects in the hyperpolymath estate. *Connection:* JanusKey relies on the mathematical guarantee that filesystem actions carry sufficient inversion data to guarantee exact state restoration. Absolute Zero's -`FilesystemCNO` (`proofs/coq/filesystem/FilesystemCNO.v` and `proofs/lean4/FilesystemCNO.lean`) -provides the formal verification kernel for JanusKey: +`FilesystemCNO` (`archive/proofs/coq/filesystem/FilesystemCNO.v` and `archive/proofs/lean4/FilesystemCNO.lean`, +both archived 2026-10-10 and no longer built or gated) provided the formal verification kernel for JanusKey: * `mkdir_rmdir_inverse` and `create_unlink_inverse` verify atomic create/destroy inverse pairs under occupancy preconditions (`noDirAt`, `noFileAt`). * `read_write_identity` and `chmod_identity` verify that idempotent updates cause zero net state delta. @@ -41,7 +41,7 @@ provides the formal verification kernel for JanusKey: *Domain:* Type-theoretic verification engine and categorical foundations for database query validation. *Connection:* -* `proofs/coq/category/CNOCategory.v` and `proofs/lean4/CNOCategory.lean` prove that CNOs correspond to identity morphisms in the category of state transitions. +* `archive/proofs/coq/category/CNOCategory.v` and `archive/proofs/lean4/CNOCategory.lean` (archived 2026-10-10, no longer built or gated) proved that CNOs correspond to identity morphisms in the category of state transitions. * Functors preserving CNOs guarantee that query transformations do not introduce side effects or alter transactional consistency invariants. == 4. Robodog Defensive Systems Lab (`hyperpolymath/robodog-defensive-systems-lab`) diff --git a/docs/JUSTFILE-COOKBOOK.adoc b/docs/JUSTFILE-COOKBOOK.adoc index 60d83d6..dbd34fb 100644 --- a/docs/JUSTFILE-COOKBOOK.adoc +++ b/docs/JUSTFILE-COOKBOOK.adoc @@ -13,7 +13,7 @@ v1.0, 2025-11-22 This cookbook documents all `just` recipes in the Absolute Zero project. Every recipe is explained with examples, flags, and common usage patterns. -WARNING: `just --list` is authoritative. The Appendix recipe list and dependency graph were regenerated from it on 2026-10-01. Nine per-recipe sections below describe recipes the Justfile no longer defines: `build-z3`, `check-tools`, `clean-all`, `docs-adoc`, `docs-all`, `docs-proof-stats`, `install-help`, `loc` and `quick-check`. Treat them as historical until this cookbook is rewritten. +WARNING: `just --list` is authoritative. The Appendix recipe list and dependency graph were regenerated from it on 2026-10-01. Nine per-recipe sections below describe recipes the Justfile no longer defines: `build-z3`, `check-tools`, `clean-all`, `docs-adoc`, `docs-all`, `docs-proof-stats`, `install-help`, `loc` and `quick-check`. Treat them as historical until this cookbook is rewritten. The `build-coq`, `build-lean` and `verify-coq` sections are historical too: the Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under `archive/proofs/` and are no longer built or gated. Paths in those sections point at the archived trees (sample outputs are left as originally written). The active gate is `just verify` (`proofs/verify-active-provers.sh`: Agda + Z3 bounded + Idris 2 ABI). === Quick Reference @@ -30,9 +30,9 @@ just ci # Run full CI pipeline === build-all -Build all proof systems and interpreters. +Build the active provers and the Idris ABI. -*Dependencies*: build-coq, build-lean, build-agda, build-isabelle, build-mizar, build-idris +*Dependencies*: build-agda, build-idris [source,bash] ---- @@ -40,12 +40,11 @@ just build-all ---- *What it does*: -1. Compiles Coq proofs -2. Compiles Lean 4 proofs -3. Compiles Agda proofs -4. Builds Isabelle/HOL proofs -5. Checks Mizar proofs -6. Builds the Idris2 ABI +1. Compiles the Agda proofs (`build-agda`) +2. Builds the Idris2 ABI (`build-idris`) + +Coq, Lean 4, Isabelle/HOL and Mizar were part of this recipe until the +2026-10-10 archive ruling; they are archived under `archive/proofs/` and not built. *Exit codes*: - `0`: All builds successful @@ -61,11 +60,11 @@ just build-coq ---- *Build order*: -1. `proofs/coq/common/CNO.v` (core definitions) -2. `proofs/coq/physics/StatMech.v` (requires CNO) -3. `proofs/coq/physics/LandauerDerivation.v` (requires CNO) -4. `proofs/coq/quantum/QuantumMechanicsExact.v` (requires CNO) -5. `proofs/coq/malbolge/MalbolgeCore.v` (requires CNO) +1. `archive/proofs/coq/common/CNO.v` (core definitions) +2. `archive/proofs/coq/physics/StatMech.v` (requires CNO) +3. `archive/proofs/coq/physics/LandauerDerivation.v` (requires CNO) +4. `archive/proofs/coq/quantum/QuantumMechanicsExact.v` (requires CNO) +5. `archive/proofs/coq/malbolge/MalbolgeCore.v` (requires CNO) *Flags used*: - `-R ../common CNO`: Maps `common` directory to `CNO` namespace @@ -95,7 +94,7 @@ just build-lean ---- *What it does*: -1. Changes to `proofs/lean4/` +1. Changes to `archive/proofs/lean4/` 2. Runs `lake build` 3. Compiles all `.lean` files 4. Downloads Mathlib dependencies if needed @@ -103,7 +102,7 @@ just build-lean *First-time setup*: [source,bash] ---- -cd proofs/lean4 +cd archive/proofs/lean4 lake update # Update dependencies lake build # Build everything ---- @@ -398,11 +397,11 @@ just clean-coq *Files removed*: [source,bash] ---- -find proofs/coq -name "*.vo" -delete -find proofs/coq -name "*.vok" -delete -find proofs/coq -name "*.vos" -delete -find proofs/coq -name "*.glob" -delete -find proofs/coq -name ".*.aux" -delete +find archive/proofs/coq -name "*.vo" -delete +find archive/proofs/coq -name "*.vok" -delete +find archive/proofs/coq -name "*.vos" -delete +find archive/proofs/coq -name "*.glob" -delete +find archive/proofs/coq -name ".*.aux" -delete ---- === clean-lean @@ -417,7 +416,7 @@ just clean-lean *What it does*: [source,bash] ---- -cd proofs/lean4 && lake clean +cd archive/proofs/lean4 && lake clean ---- *Removes*: @@ -720,7 +719,7 @@ import "justfile" # Override build-coq with custom flags build-coq-custom: - coqc -verbose -R proofs/coq/common CNO proofs/coq/common/CNO.v + coqc -verbose -R archive/proofs/coq/common CNO archive/proofs/coq/common/CNO.v ---- Then: diff --git a/docs/MACHINE_VERIFICATION.adoc b/docs/MACHINE_VERIFICATION.adoc index d23a385..0c2305d 100644 --- a/docs/MACHINE_VERIFICATION.adoc +++ b/docs/MACHINE_VERIFICATION.adoc @@ -71,11 +71,11 @@ Verifying Coq proofs... Run this to count incomplete proofs: ```bash -# Count Coq admits -find proofs/coq -name "*.v" -exec grep -c "Admitted" {} + | awk -F: '{sum += $2} END {print "Coq Admitted:", sum}' +# Count Coq admits (archived tree) +find archive/proofs/coq -name "*.v" -exec grep -c "Admitted" {} + | awk -F: '{sum += $2} END {print "Coq Admitted:", sum}' -# Count Lean 4 sorries -find proofs/lean4 -name "*.lean" -exec grep -c "sorry" {} + | awk -F: '{sum += $2} END {print "Lean sorry:", sum}' +# Count Lean 4 sorries (archived tree) +find archive/proofs/lean4 -name "*.lean" -exec grep -c "sorry" {} + | awk -F: '{sum += $2} END {print "Lean sorry:", sum}' ``` ### Step 4: Address Failures diff --git a/docs/OND-PILLAR-STRUCTURE.adoc b/docs/OND-PILLAR-STRUCTURE.adoc index 5f798a5..c05032b 100644 --- a/docs/OND-PILLAR-STRUCTURE.adoc +++ b/docs/OND-PILLAR-STRUCTURE.adoc @@ -14,13 +14,22 @@ artifacts CNO does not need: *declared observation models* and *residue lists*. .STATUS — 2026-07-07: OND modules AUTHORED (PR #100) ==== The dedicated proof effort has run. The OND modules specified below now exist and -are machine-checked: `proofs/coq/ond/OND.v` (OND-1..5, zero axioms, all *Closed -under the global context*), plus `proofs/lean4/OND.lean`, `proofs/agda/OND.agda`, -`proofs/isabelle/OND.thy`, and `proofs/z3/ond/OND_checks.smt2`. The first residue +were machine-checked: `archive/proofs/coq/ond/OND.v` (OND-1..5, zero axioms, all *Closed +under the global context*), plus `archive/proofs/lean4/OND.lean`, `proofs/agda/OND.agda`, +`archive/proofs/isabelle/OND.thy`, and `proofs/z3/ond/OND_checks.smt2`. The first residue instance (`proofs/residue/ct_select.residue`) and observation model (`proofs/observation-models/O_all.model`) are populated. Note: the Coq module landed at `proofs/coq/ond/OND.v` (not the `observational/` path sketched below). Only OND-6 remains to author. + +*Archive update (2026-10-10).* The Coq, Lean 4, Isabelle/HOL and Mizar trees +were archived under `archive/proofs/` and are no longer built or gated; the Coq +OND module is now `archive/proofs/coq/ond/OND.v`. The active OND legs are +`proofs/agda/OND.agda` and `proofs/z3/ond/OND_checks.smt2`. The layout tables +below are the original design sketch: their `proofs/coq/…`, `proofs/lean4/…`, +`proofs/isabelle/…` and `proofs/mizar/…` paths name the pre-archive layout, and +some (`observational/`, `ond_verify.sh`, the `ONDIndependence`/`ONDComposition` +splits, `OND.miz`) exist in neither `proofs/` nor `archive/proofs/`. ==== == Co-equality principle @@ -36,9 +45,10 @@ CNO analogue. == Per-prover module layout (mirrors CNO — AUTHORED) -Each OND module sits beside its CNO counterpart. As of PR #100 these files exist -and are verified (Coq/Lean/Agda/Z3/Isabelle); the Coq module is at -`proofs/coq/ond/OND.v`. +Each OND module sits beside its CNO counterpart. As of PR #100 these files existed +and were verified (Coq/Lean/Agda/Z3/Isabelle); the Coq module landed at +`proofs/coq/ond/OND.v`, now archived as `archive/proofs/coq/ond/OND.v`. The table +below is the design sketch (see the archive update above). [cols="1,2,2,3",options="header"] |=== diff --git a/docs/OND-ROADMAP.adoc b/docs/OND-ROADMAP.adoc index 8c002a0..659ca30 100644 --- a/docs/OND-ROADMAP.adoc +++ b/docs/OND-ROADMAP.adoc @@ -17,8 +17,9 @@ proofs themselves are deferred to a dedicated effort. .STATUS UPDATE — 2026-07-06: OND-1..5 + OND-7 LANDED ==== The dedicated effort has since run. *OND-1, OND-2, OND-3, OND-4, and OND-5 are -now proved and machine-checked* — Coq (`proofs/coq/ond/OND.v`), Lean 4 -(`proofs/lean4/OND.lean`), and Agda (`proofs/agda/OND.agda`), with the bounded +now proved and machine-checked* — Coq (`archive/proofs/coq/ond/OND.v`), Lean 4 +(`archive/proofs/lean4/OND.lean`) — both archived 2026-10-10 and no longer +built or gated — and Agda (`proofs/agda/OND.agda`), with the bounded instances confirmed in Z3 (`proofs/z3/ond/OND_checks.smt2`). Every OND theorem in Coq reports `Closed under the global context` — *zero axioms, zero admits*. The independence theorem (OND-3) is additionally anchored to the *real* core diff --git a/docs/VERIFICATION_RESULTS.adoc b/docs/VERIFICATION_RESULTS.adoc index e1e80b5..fdd3249 100644 --- a/docs/VERIFICATION_RESULTS.adoc +++ b/docs/VERIFICATION_RESULTS.adoc @@ -3,9 +3,11 @@ # Verification Results: Phase 1 Completion and Cross-Solver Proofs > **SUPERSEDED / HISTORICAL (2025-11-22 session).** This is a point-in-time -> session log. Current reproduced status: both pillars machine-checked across -> six provers + Idris (PR #100, 2026-07-06) — see `PROOF-STATUS.adoc` and run -> `proofs/verify-all-provers.sh` (`ALL-PROVERS-GREEN`). Counts below are historical. +> session log. Both pillars were machine-checked across six provers + Idris +> (PR #100, 2026-07-06); since the 2026-10-10 archive ruling the active stack is +> Agda + Z3 (bounded) + the Idris 2 ABI — run `proofs/verify-active-provers.sh` +> (`ACTIVE-PROVERS-GREEN`). The Coq and Lean files cited below are archived under +> `archive/proofs/`. See `PROOF-STATUS.adoc`. Counts below are historical. **Date**: 2025-11-22 **Session**: Proof Completion and Automated Verification diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 1827b8b..2aa053f 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -9,6 +9,11 @@ tagged `+METAL-BOUNDARY+` and (b) a small openly-labelled class-A set `+fidelity_bound+`). Three axioms turned out *unsound* and were removed/corrected (`+no_cloning+`, `+Cconj_Cexp+`, `+eta_equivalence+`). Current disposition: `+PROOF-STATUS.adoc+`. + +*Archive update (2026-10-10):* the Coq and Lean 4 trees this ledger cites were +archived under `+archive/proofs/+` and are no longer built or gated; the file +pointers below have been updated to the archived paths (line numbers are as +recorded at triage time). ____ *Schema*: @@ -44,7 +49,7 @@ https://github.com/hyperpolymath/absolute-zero/issues/27[#27]. === Phase 2a triage — Lean Lambda cluster (2026-05-27) Per-cluster Lean triage rolling out 2026-05-27 in cluster-sized PRs. -First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows). +First cluster: `+archive/proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows). [width="99%",cols=">14%,26%,28%,32%",options="header",] |=== @@ -54,7 +59,7 @@ immediate from the semantic `+Closed+` definition. |237 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim about Y combinator; requires step-indexed semantics or coinduction (same -justification as Coq `+y_not_cno+`, `+proofs/coq/lambda/LambdaCNO.v:399+`). +justification as Coq `+y_not_cno+`, `+archive/proofs/coq/lambda/LambdaCNO.v:399+`). |308 |`+eta_equivalence+` |THEOREM (restricted) |The unrestricted statement is *false* (counterexample `+f = LVar 5+`, exactly as Coq found at @@ -69,7 +74,7 @@ comments. The §(d) entry below has an owner + deadline. === Phase 2c triage — Lean Filesystem cluster (2026-05-27, DISCHARGED 2026-09-26) -Second Lean cluster: `+proofs/lean4/FilesystemCNO.lean+` (**21 → 0 axioms** — *DISCHARGED 2026-09-26*, issue #167). +Second Lean cluster: `+archive/proofs/lean4/FilesystemCNO.lean+` (**21 → 0 axioms** — *DISCHARGED 2026-09-26*, issue #167). All 10 primitive operations (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`, `stat`, `chmod`, `chown`, `rename`), the 2 snapshot operations (`snapshot`, `restore`), and all 9 laws and properties (`mkdir_rmdir_inverse`, `create_unlink_inverse`, @@ -81,7 +86,7 @@ the Coq concrete filesystem model. `AxiomAudit.lean` §D verifies that all === Phase 2d triage — Lean Quantum cluster (2026-05-27) -Third Lean cluster: `+proofs/lean4/QuantumCNO.lean+` (14 axioms). +Third Lean cluster: `+archive/proofs/lean4/QuantumCNO.lean+` (14 axioms). ==== Hilbert-space + gate primitives (§(c) AXIOM, 7) @@ -147,7 +152,7 @@ leading comments. === Phase 2e triage — Lean StatMech cluster (2026-05-27) -Fourth Lean cluster: `+proofs/lean4/StatMech.lean+` (14 axioms). +Fourth Lean cluster: `+archive/proofs/lean4/StatMech.lean+` (14 axioms). ==== Physical constants (§(c) AXIOM — duplicate of Coq, 4) @@ -229,7 +234,7 @@ longer in §(d). ==== Coq — provable, awaiting proof -* `+proofs/coq/category/CNOCategory.v:323+` — `+hom_functor+` +* `+archive/proofs/coq/category/CNOCategory.v:323+` — `+hom_functor+` ** *Owner*: @hyperpolymath ** *Plan*: replace `+Axiom hom_functor : ... Functor C C+` with the proper Yoneda construction `+Functor C SetCategory+`. The file’s leading @@ -242,93 +247,93 @@ comment (L312-322) records why this is currently axiomatised: (1) (Phase 1, #58). ** *Deadline*: INDEFINITE (blocked on `+SetCategory+` instance — universe-polymorphism scaffolding precondition). -* `+proofs/coq/filesystem/FilesystemCNO.v:300+` — `+mkdir_not_identity+` +* `+archive/proofs/coq/filesystem/FilesystemCNO.v:300+` — `+mkdir_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit one concrete `+fs+` lacking the path. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE (small proof; awaits a discharge PR). -* `+proofs/coq/filesystem/FilesystemCNO.v:316+` — +* `+archive/proofs/coq/filesystem/FilesystemCNO.v:316+` — `+write_different_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit one concrete content mismatch. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE. -* `+proofs/coq/filesystem/FilesystemCNO.v:397+` — `+transaction_cno+` +* `+archive/proofs/coq/filesystem/FilesystemCNO.v:397+` — `+transaction_cno+` ** *Owner*: @hyperpolymath ** *Plan*: composite theorem; derivable from primitive `+_inverse+` axioms once a `+transaction+` definition is in place. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE (blocked on `+transaction+` definition). -* `+proofs/coq/filesystem/FilesystemCNO.v:421+` — `+mkdir_idempotent+` +* `+archive/proofs/coq/filesystem/FilesystemCNO.v:421+` — `+mkdir_idempotent+` ** *Owner*: @hyperpolymath ** *Plan*: follows from `+mkdir_rmdir_inverse+` family + stronger repeat-mkdir semantics. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE. -* `+proofs/coq/filesystem/FilesystemCNO.v:453+` — +* `+archive/proofs/coq/filesystem/FilesystemCNO.v:453+` — `+snapshot_restore_identity+` ** *Owner*: @hyperpolymath ** *Plan*: composite theorem; derivable from primitive `+_identity+` / `+_inverse+` axioms once a snapshot model lands. Triaged DISCHARGE in #58. ** *Deadline*: INDEFINITE. -* `+proofs/coq/quantum/QuantumCNO.v:258+` — `+global_phase_unitary+` +* `+archive/proofs/coq/quantum/QuantumCNO.v:258+` — `+global_phase_unitary+` ** *Owner*: @hyperpolymath ** *Plan*: derivable from gate algebra: `+(e^{iθ} U)+` is unitary iff `+U+` is. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE (needs `+is_unitary+` algebraic lemmas). -* `+proofs/coq/quantum/QuantumCNO.v:283+` — `+X_gate_not_identity+` +* `+archive/proofs/coq/quantum/QuantumCNO.v:283+` — `+X_gate_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete basis state is in the model. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE (blocked on concrete basis-state model). -* `+proofs/coq/quantum/QuantumCNO.v:296+` — `+H_gate_not_identity+` +* `+archive/proofs/coq/quantum/QuantumCNO.v:296+` — `+H_gate_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit `\|0⟩` as witness. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE (blocked on concrete basis-state model). -* `+proofs/coq/quantum/QuantumCNO.v:487+` — `+unitary_inverse_property+` +* `+archive/proofs/coq/quantum/QuantumCNO.v:487+` — `+unitary_inverse_property+` ** *Owner*: @hyperpolymath ** *Plan*: follows from `+is_unitary+` definition (`+U†U = I+`). Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE. -* `+proofs/coq/quantum/QuantumCNO.v:545+` — +* `+archive/proofs/coq/quantum/QuantumCNO.v:545+` — `+unitary_zero_entropy_change+` ** *Owner*: @hyperpolymath ** *Plan*: derivable from `+unitary_preserves_entropy+` + entropy definition. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE. -* `+proofs/coq/quantum/QuantumCNO.v:551+` — +* `+archive/proofs/coq/quantum/QuantumCNO.v:551+` — `+reversible_quantum_zero_dissipation+` ** *Owner*: @hyperpolymath ** *Plan*: derivable from `+quantum_landauer_bound+` + unitarity. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE. -* `+proofs/coq/quantum/QuantumCNO.v:584+` — `+fidelity_bound+` +* `+archive/proofs/coq/quantum/QuantumCNO.v:584+` — `+fidelity_bound+` ** *Owner*: @hyperpolymath ** *Plan*: provable from `+inner_product_pos_def+` + Cauchy-Schwarz. Triaged DISCHARGE in #58 (Phase 2d). ** *Deadline*: INDEFINITE. -* `+proofs/coq/physics/StatMech.v:229+` — +* `+archive/proofs/coq/physics/StatMech.v:229+` — `+reversible_zero_dissipation+` ** *Owner*: @hyperpolymath ** *Plan*: derivable from `+landauer_principle+` + reversibility hypothesis. Triaged DISCHARGE in #58 (Phase 2e). ** *Deadline*: INDEFINITE. -* `+proofs/coq/physics/LandauerDerivation.v:81+` — +* `+archive/proofs/coq/physics/LandauerDerivation.v:81+` — `+shannon_entropy_additive+` ** *Owner*: @hyperpolymath ** *Plan*: chain rule of entropy; provable from the definition of `+H(X,Y)+` given an independence hypothesis. Triaged DISCHARGE in #58 (Phase 2e). ** *Deadline*: INDEFINITE (blocked on `+product_dist+` semantics). -* `+proofs/coq/physics/LandauerDerivation.v:277+` — +* `+archive/proofs/coq/physics/LandauerDerivation.v:277+` — `+cno_preserves_shannon_entropy+` ** *Owner*: @hyperpolymath ** *Plan*: should follow from the CNO definition (state in = state out) + functional Shannon entropy. Triaged DISCHARGE in #58 (Phase 2e). ** *Deadline*: INDEFINITE (blocked on bijection-preserves-entropy machinery). -* `+proofs/coq/physics/LandauerDerivation.v:326+` — +* `+archive/proofs/coq/physics/LandauerDerivation.v:326+` — `+cno_zero_energy_dissipation_derived+` ** *Owner*: @hyperpolymath ** *Plan*: name literally says `+_derived+`; the file admits this rather @@ -339,23 +344,23 @@ than discharging it. Should follow from ==== Lean — provable, awaiting proof -* `+proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED +* `+archive/proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED 2026-09-22* (fix PR for #125): now a `+theorem+`; it is immediate from the semantic definition of `+Closed+` (`+h n s (Nat.zero_le n)+`). -* `+proofs/lean4/FilesystemCNO.lean+` — all 21 axioms (`mkdir_not_identity`, +* `+archive/proofs/lean4/FilesystemCNO.lean+` — all 21 axioms (`mkdir_not_identity`, `snapshot_restore_identity`, `mkdir_idempotent`, operations and laws) — *DISCHARGED 2026-09-26* (issue #167): concrete model ported from Coq `FilesystemCNO.v`. -* `+proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+` +* `+archive/proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete basis state is in the model. Mirrors Coq site at `+QuantumCNO.v:283+`. ** *Deadline*: INDEFINITE. -* `+proofs/lean4/QuantumCNO.lean:144+` — `+H_gate_not_identity+` +* `+archive/proofs/lean4/QuantumCNO.lean:144+` — `+H_gate_not_identity+` ** *Owner*: @hyperpolymath ** *Plan*: existence proof; exhibit `\|0⟩` as witness. Mirrors Coq site at `+QuantumCNO.v:296+`. ** *Deadline*: INDEFINITE. -* `+proofs/lean4/QuantumCNO.lean:235+` — `+unitary_inverse_property+` +* `+archive/proofs/lean4/QuantumCNO.lean:235+` — `+unitary_inverse_property+` ** *Owner*: @hyperpolymath ** *Plan*: follows from `+isUnitary+` definition (`+U†U = I+`). Mirrors Coq site at `+QuantumCNO.v:487+`. diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md index e9b1b74..7520b8a 100644 --- a/docs/wiki/Architecture.md +++ b/docs/wiki/Architecture.md @@ -62,16 +62,16 @@ absolute-zero calls into it via the `echidna-llm-mcp` BoJ cartridge — ## Data flow on `just verify` ``` -verification/setup-and-verify.sh - ├── proofs/coq → coqc -R common CNO ... - ├── proofs/lean4 → lake build - ├── proofs/agda → agda CNO.agda - ├── proofs/isabelle → isabelle build - ├── proofs/z3 → z3 *.smt2 - ├── src/abi → idris2 --build absolute-zero-abi.ipkg - └── cargo build --release +proofs/verify-active-provers.sh + ├── proofs/agda → agda --safe --without-K (CNO, OND, EchoBridgeScaffold, EchoBridgeCNO) + ├── proofs/z3 → proofs/z3/verify.sh (expect-annotated bounded checks) + └── src/abi → idris2 --build absolute-zero-abi.ipkg ``` +The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 +under `archive/proofs/` (`coq/`, `lean4/`, `isabelle/`, `mizar/`) and are not run. +The former six-prover gate is `archive/proofs/verify-all-provers.six-prover.sh`. + ## Why this taxonomy The directory layout follows the [RSR-template-repo](../RSR_OUTLINE.adoc) diff --git a/docs/wiki/Audit-Trail.md b/docs/wiki/Audit-Trail.md index 4b5c5d7..6242662 100644 --- a/docs/wiki/Audit-Trail.md +++ b/docs/wiki/Audit-Trail.md @@ -24,8 +24,8 @@ Short summary; the authoritative ledger is [`AUDIT.adoc`](../../AUDIT.adoc). ## Axiom classification -The 73 Coq Axioms + 42 Parameters in `proofs/coq/` are model-layer -assumptions: +The 73 Coq Axioms + 42 Parameters in `archive/proofs/coq/` (archived 2026-10-10; +historical counts) are model-layer assumptions: * **Physics**: thermodynamic laws, Landauer bound, statistical mechanics * **Quantum**: Hilbert-space axioms, unitarity diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index 9554620..bb45096 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -38,10 +38,10 @@ of 23+ languages. ## Status (live) -* **Phase**: two-pillar completion / hardening (~88%). Both pillars machine-checked across **six provers + Idris** (PR #100) — run `proofs/verify-all-provers.sh` → `ALL-PROVERS-GREEN`. -* **Coq**: 14/14 theories compile (CNO + OND), 0 Admitted; CNO axioms cut 98→small classified remainder; **OND** (`ond/OND.v`) OND-1..5 proved with zero axioms. -* **Lean 4**: `lake build` green (Mathlib) incl. the new `OND` lib; 0 `sorry`. -* **Agda / Z3 / Isabelle / Mizar**: CNO + OND verified (Agda `OND.agda`; Z3 `ond/OND_checks.smt2`; Isabelle `AbsoluteZero-CNO` session; Mizar `CNO.miz` → empty `.err`). +* **Phase**: two-pillar completion / hardening (~88%). Both pillars were machine-checked across **six provers + Idris** (PR #100, 2026-07-06). Since the 2026-10-10 archive ruling the active stack is **Agda + Z3 (bounded) + Idris 2 ABI** — run `proofs/verify-active-provers.sh` → `ACTIVE-PROVERS-GREEN`. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (not built or gated); the six-prover gate is `archive/proofs/verify-all-provers.six-prover.sh`. +* **Coq (archived, `archive/proofs/coq/`)**: 14/14 theories compiled (CNO + OND), 0 Admitted; CNO axioms cut 98→small classified remainder; **OND** (`ond/OND.v`) OND-1..5 proved with zero axioms. +* **Lean 4 (archived, `archive/proofs/lean4/`)**: `lake build` was green (Mathlib) incl. the new `OND` lib; 0 `sorry`. +* **Agda / Z3** (active): Agda type-checks CNO + OND (`CNO.agda`, `OND.agda`); Z3 runs the OND bounded checks (`ond/OND_checks.smt2`). **Isabelle / Mizar** (archived): Isabelle `AbsoluteZero-CNO` session and Mizar `CNO.miz` → empty `.err` were verified on 2026-07-07. * **Idris2 ABI**: `absolute-zero-abi.ipkg` builds clean under 0.8.0. * For the authoritative live state, read [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml) @@ -49,8 +49,8 @@ of 23+ languages. provers + the Idris ABI: the OND (disclosure) pillar was authored from scratch (OND-1..5 proved, zero axioms; OND-6 open by design), CNO axioms were cut from 98 to a small classified remainder, three latent-unsound axioms were found and fixed, -and Isabelle/Mizar/Idris were brought to green. Reproduce with -`proofs/verify-all-provers.sh`. +and Isabelle/Mizar/Idris were brought to green. Reproduced then with +`proofs/verify-all-provers.sh` (now archived as `archive/proofs/verify-all-provers.six-prover.sh`). ## Project layout (RSR-aligned) diff --git a/docs/wiki/Proof-Systems.md b/docs/wiki/Proof-Systems.md index 6e78a6e..d26fd31 100644 --- a/docs/wiki/Proof-Systems.md +++ b/docs/wiki/Proof-Systems.md @@ -23,7 +23,12 @@ flags a foundational dependency worth understanding. ## What lives where -### `proofs/coq/` (the load-bearing system) +Since the 2026-10-10 archive ruling the active stack is Agda (`proofs/agda/`), +Z3 bounded checks (`proofs/z3/`) and the Idris 2 ABI. The Coq, Lean 4, +Isabelle/HOL and Mizar trees below are archived under `archive/proofs/` and are +no longer built or gated; their status lines are historical receipts. + +### `archive/proofs/coq/` (archived; formerly the load-bearing system) * `common/CNO.v` — core CNO definitions and properties * `physics/StatMech.v` — Landauer bound axiomatised * `physics/LandauerDerivation.v` — Landauer bound derived (the two @@ -35,7 +40,7 @@ flags a foundational dependency worth understanding. * `malbolge/MalbolgeCore.v` — Malbolge VM semantics * `filesystem/FilesystemCNO.v` — filesystem CNOs -Status (PR #100, 2026-07-06): **14/14 theories compile, 0 Admitted**, now +Status (PR #100, 2026-07-06): **14/14 theories compiled, 0 Admitted**, now including `ond/OND.v` (the OND pillar, OND-1..5, zero axioms). CNO axioms cut 98→small classified remainder: filesystem/category/QuantumMechanicsExact fully discharged; genuine physical postulates kept as tagged `METAL-BOUNDARY`; a few @@ -43,10 +48,10 @@ class-A items openly labelled; three unsound axioms removed/corrected. See [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) and [`docs/PROOF-CLASSIFICATION.adoc`](../PROOF-CLASSIFICATION.adoc). -### `proofs/lean4/` +### `archive/proofs/lean4/` (archived) * `CNO.lean`, `StatMech.lean`, `CNOCategory.lean`, `LambdaCNO.lean`, `QuantumCNO.lean`, `FilesystemCNO.lean` -* Built with `lake build`; mathlib + 6 lean_lib targets; +* Was built with `lake build`; mathlib + 6 lean_lib targets; 1631/1632 green (verified 2026-05-20). ### `proofs/z3/` @@ -56,21 +61,22 @@ candidate CNO claims before committing to a constructive proof. ### `proofs/agda/` Type-level CNO certificates exploiting dependent types. -### `proofs/isabelle/`, `proofs/mizar/` +### `archive/proofs/isabelle/`, `archive/proofs/mizar/` (archived) Cross-validation. Catches Coq-specific tactic quirks; connects Mizar's standard maths library. ## Reproducible build ```bash -just build-coq # coqc -R common CNO physics/StatMech.v ... -just build-lean # cd proofs/lean4 && lake build -just build-agda # agda CNO.agda -just build-isabelle # isabelle build -just build-z3 # z3 *.smt2 (when present) -just verify # all of the above + ABI + Rust +just build-agda # agda --safe --without-K on the four Agda modules +just build-idris # idris2 --build absolute-zero-abi.ipkg +just verify-z3 # bash proofs/z3/verify.sh (expect-annotated) +just verify # proofs/verify-active-provers.sh → ACTIVE-PROVERS-GREEN ``` +The former `build-coq`, `build-lean`, `build-isabelle` and `build-z3` recipes no +longer exist in the Justfile. + ## Discharged axioms (recent) * **ADR-007** (2026-05-20, PR #24): `eval_deterministic` diff --git a/docs/wiki/Roadmap.md b/docs/wiki/Roadmap.md index e9ad2a4..5b7495c 100644 --- a/docs/wiki/Roadmap.md +++ b/docs/wiki/Roadmap.md @@ -8,9 +8,9 @@ Short summary; the authoritative version is [`ROADMAP.adoc`](../../ROADMAP.adoc) ## Now (post v1.0.0-alpha) -* ✅ Both pillars machine-checked across six provers + Idris (PR #100) — `proofs/verify-all-provers.sh` -* ✅ OND pillar authored (OND-1..5 proved, zero axioms); ✅ Idris ABI builds; ✅ Isabelle + Mizar verify -* Wire proof verification into CI (`.github/workflows/proofs.yml` runs Coq + Z3; extend to more provers) +* ✅ Both pillars machine-checked across six provers + Idris (PR #100) — via `proofs/verify-all-provers.sh`, now archived as `archive/proofs/verify-all-provers.six-prover.sh`; since 2026-10-10 the active gate is `proofs/verify-active-provers.sh` (Agda + Z3 bounded + Idris 2 ABI) +* ✅ OND pillar authored (OND-1..5 proved, zero axioms); ✅ Idris ABI builds; ✅ Isabelle + Mizar verified (2026-07-07; both archived under `archive/proofs/` since 2026-10-10) +* Wire proof verification into CI (`.github/workflows/proofs.yml` runs the `agda`, `z3` and `idris` jobs; the Coq and Lean 4 jobs were dropped when those trees were archived on 2026-10-10) * Discharge the class-A remainder (needs finite-dim/tensor QM + coinductive-β machinery) — optional * Prove **OND-6** (conditional composition) — the research capstone diff --git a/docs/wiki/Verification.md b/docs/wiki/Verification.md index 7b06576..84b2cd3 100644 --- a/docs/wiki/Verification.md +++ b/docs/wiki/Verification.md @@ -24,29 +24,30 @@ The `verification/` directory contains the top-level scripts. Or via `Justfile` recipes (more granular): ```bash -just build-all # everything -just build-coq # Coq only -just build-lean # Lean 4 only +just build-all # Agda + Idris 2 ABI (the active stack) just build-agda -just build-isabelle -just build-affinescript -just verify # build + check +just build-idris +just verify # proofs/verify-active-provers.sh → ACTIVE-PROVERS-GREEN ``` +The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under +`archive/proofs/` and have no build recipes; the commands below for them are +historical and run against the archived trees. + ## Per-prover commands -### Coq +### Coq (archived) ```bash -cd proofs/coq/common && coqc CNO.v +cd archive/proofs/coq/common && coqc CNO.v cd ../physics && coqc -R ../common CNO StatMech.v coqc -R ../common CNO LandauerDerivation.v cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v cd ../malbolge && coqc -R ../common CNO MalbolgeCore.v ``` -### Lean 4 +### Lean 4 (archived) ```bash -cd proofs/lean4 && lake build +cd archive/proofs/lean4 && lake build ``` ### Agda @@ -97,5 +98,8 @@ See [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descri and [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) for live status. Summary: both pillars verified across **six provers + Idris** — Coq 14/14, Lean+Mathlib green, Agda (CNO+OND), Z3, Isabelle (`AbsoluteZero-CNO`), Mizar (`CNO.miz` empty `.err`), -Idris ABI builds clean. One-shot: `proofs/verify-all-provers.sh` → -`ALL-PROVERS-GREEN`. +Idris ABI builds clean. One-shot then: `proofs/verify-all-provers.sh` (now archived as +`archive/proofs/verify-all-provers.six-prover.sh`) → `ALL-PROVERS-GREEN`. + +Since the 2026-10-10 archive ruling only Agda, Z3 (bounded) and the Idris 2 ABI +are active: run `proofs/verify-active-provers.sh` → `ACTIVE-PROVERS-GREEN`.