From ad66f2cdeb25323b49b2303673c0eff2487d2f60 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:37:19 +0000 Subject: [PATCH] docs(proof-status): canonical active-vs-archived reconciliation table with estate grades MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - PROOF-STATUS.adoc: add canonical proof-status reconciliation table separating ACTIVE / ARCHIVED / proved / axiomatic / generated artefacts; OND-6 kept explicitly open (not proved, not assumed) - Record closed proof-ledger vocabulary (standards PROOF-POLICY §5) and estate proof grades (mathesis estate-mathematical-architecture §5-6): active Agda = proven at Grade 3, Z3 = tested-only (bounded), Idris2 ABI = argued interface; archived Coq/Lean/Isabelle/Mizar = historical receipts - Clarify absolute-zero as consumer/domain formalisation; historical counts (115 Qed / 61 Axioms) are archived-tree figures, not estate-wide ground truth; epistemic-types@5422cd5 is independent with no dependency - Add sandbox reproduction receipts (2026-11-01): Z3 5.3.3 Z3-CHECK OK; Agda/Idris2/archived provers recorded as not runnable in sandbox (egress allowlist), remain CI receipts; --cubical-compatible recheck kept open - README/EXPLAINME/ROADMAP/docs: mark archived provers and historical counts, re-point gates to proofs/verify-active-provers.sh Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- EXPLAINME.adoc | 49 ++++++------ PROOF-STATUS.adoc | 128 ++++++++++++++++++++++++++++++-- README.adoc | 71 +++++++++++------- ROADMAP.adoc | 9 ++- docs/MACHINE_VERIFICATION.adoc | 14 ++-- docs/PROOF-COMPLETION-PLAN.adoc | 9 ++- 6 files changed, 213 insertions(+), 67 deletions(-) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 2c21a0c..5d5ebfc 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -7,6 +7,11 @@ This file backs every factual claim in link:README.adoc[README.adoc] with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code. +[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`. +==== + == Claim-to-implementation map === CNO and OND are logically independent @@ -16,19 +21,19 @@ ____ The two pillars are logically independent (a proved theorem, with witnesses). ____ -How this is implemented:: -The independence theorem is proved in Coq, anchored to the core `is_CNO` definition. Witnesses demonstrating that CNO does not entail OND and OND does not entail CNO are constructed. +How this was implemented:: +The independence theorem was proved in Coq (`archive/proofs/coq/ond/OND.v`, anchored to the core `is_CNO` definition, with witnesses that CNO does not entail OND and OND does not entail CNO); the active Agda `OND.agda` carries the same obligation zero-postulate. Caveat:: None currently known for the independence proof itself. However, the *coupling dial* between them (connecting a thing to the trace it casts) is explicitly framing, not theorem. === OND-1..5 are proved with zero axioms -[quote, README.adoc] -____OND obligations OND-1..5 are proved with zero axioms in Coq (proofs/coq/ond/OND.v, every theorem Closed under the global context)____ +[quote, README.adoc (active stack)] +____OND obligations OND-1..5 are proved with zero postulates in Agda (`proofs/agda/OND.agda`, `--safe --without-K`)____ How this is implemented:: -`link:proofs/coq/ond/OND.v[]` contains the proofs. CI verifies that the global context is closed (no axioms admitted). Mirrored in Lean 4, Agda, and Z3. +`link:proofs/agda/OND.agda[]` contains the active proofs; CI (`proofs.yml`, `agda` job) type-checks all four Agda modules under `--safe --without-K`. The historical Coq proof (`archive/proofs/coq/ond/OND.v`, every theorem `Closed under the global context`) and the Lean 4 mirror are archived; Z3 confirms the bounded instances (`proofs/z3/ond/OND_checks.smt2`, expect-annotated). Caveat:: OND proofs are axiom-free *relative to the declared observation model `O`*. The choice of `O` is a proof input, not a proof output. If `O` omits a real-world observable channel (e.g., power analysis), the OND proof is sound but physically incomplete. The residue list in `link:proofs/residue/[]` records this gap. @@ -100,17 +105,17 @@ This is a standard result. The practical consequence is that the verified CNOs i [CAUTION] ==== -**61 Coq + 52 Lean axioms are unproven.** The CNO pillar is machine-checked *relative to these axioms*. Key axioms: quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws. Discharging these is the next major obligation. +**61 Coq + 52 Lean axioms are unproven — in the ARCHIVED stack.** The archived CNO development (`archive/proofs/`) was machine-checked *relative to these axioms* (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws). These are historical counts of the archived trees, not active proof status and not estate-wide ground truth. The *active* Agda stack is zero-postulate. ==== [CAUTION] ==== -**Z3, Isabelle, and Mizar artefacts are not run.** They exist in-tree but are not part of the CI gate. Only Coq, Lean 4, and Agda are currently machine-checked evidence. +**Coq, Lean 4, Isabelle/HOL and Mizar artefacts are archived and not run.** `archive/proofs/` is not built or gated. The active machine-checked evidence is Agda (`proofs/agda/`), Z3 bounded checks (`proofs/z3/`), and the Idris 2 ABI build — via `proofs/verify-active-provers.sh`. ==== [CAUTION] ==== -**OND-6 (conditional composition) is open.** OND-1..5 are proved. The capstone composition theorem is deferred. +**OND-6 (conditional composition) is OPEN — not proved, not assumed.** OND-1..5 are proved (zero postulates, active Agda). The capstone composition theorem remains the deliberate research fork; no `Admitted` or postulate stands in for it anywhere in the active stack. ==== [CAUTION] @@ -129,26 +134,26 @@ This is a standard result. The practical consequence is that the verified CNOs i |=== | Path | Proves -| `proofs/coq/common/CNO.v` -| Core CNO framework (115 Qed, 61 Axioms) +| `proofs/agda/` (CNO, OND, EchoBridge) +| ACTIVE: both pillars, OND-1..5, zero postulates (`--safe --without-K`) -| `proofs/coq/ond/OND.v` -| OND-1..5 (zero axioms) +| `proofs/z3/` + `proofs/verify-active-provers.sh` +| ACTIVE: bounded expect-checked instances; one-shot active gate -| `proofs/coq/physics/StatMech.v` -| Landauer's principle, thermodynamic reversibility +| `archive/proofs/coq/common/CNO.v` +| ARCHIVED: core CNO framework (historical 115 Qed, 61 Axioms) -| `proofs/coq/category/CNOCategory.v` -| Universal CNO definition, model independence +| `archive/proofs/coq/ond/OND.v` +| ARCHIVED: OND-1..5 (zero axioms) -| `proofs/lean4/` -| Lean 4 mirrors (Phases 1–4, 52 Axioms) +| `archive/proofs/coq/physics/StatMech.v` +| ARCHIVED: Landauer's principle, thermodynamic reversibility -| `proofs/agda/` -| Agda Phase 1 +| `archive/proofs/coq/category/CNOCategory.v` +| ARCHIVED: universal CNO definition, model independence -| `proofs/verify-all-provers.sh` -| One-shot gate script +| `archive/proofs/lean4/` +| ARCHIVED: Lean 4 mirrors (historical Phases 1–4, 52 Axioms) | `proofs/observation-models/` | Declared `O` inputs for OND diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 12fee53..62aa215 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -11,12 +11,13 @@ records the *actually reproduced* verification state in this environment, prover by prover, and is explicit about which axioms remain and why. [IMPORTANT] -.2026-07-07 — both pillars machine-checked across six provers +.2026-07-07 — both pillars machine-checked across six provers (HISTORICAL since 2026-10-10) ==== -All six provers are installed and were *reproduced in this environment*. A single -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. +*Historical (superseded by the 2026-10-10 archive ruling below):* all six +provers were reproduced in this environment via `proofs/verify-all-provers.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. 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)` @@ -31,6 +32,123 @@ each absent or failing prover, for each verdict mutant and for both audit mutant *Archive notice (2026-10-10).* The active proof stack is now Idris 2 (ABI) and Agda (CNO, OND, EchoBridge), with Z3 as a bounded-check solver. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (see `archive/README.adoc`). Text that describes those provers as active is historical until the full rewrite lands. ==== +== Canonical proof-status reconciliation (2026-11-01) + +This table is the *single canonical statement* of proof status in this +repository. Where older prose (README, EXPLAINME, ROADMAP, `docs/*`) quotes +counts such as "115 Qed / 0 Admitted / 61 Axioms", those figures describe +the *archived* Coq tree under `archive/proofs/coq/` only. They are +historical, they are not active, and they are **not estate-wide proof-status +ground truth** — see "Role of this repository" below. + +*Grading scheme.* Statuses below use the closed proof-ledger vocabulary of +`hyperpolymath/standards` (`3-practice/PROOF-POLICY.adoc` §5 and +`docs/README-EXPLAINME-STANDARD.adoc` §5): `proven`, `proven-with-postulates`, +`tested-only`, `argued`, `open` — recorded exactly, never flattened into a +percentage. Estate grades follow mathesis's `estate-mathematical-architecture` +§5–6: **Grade 3** = type-checks locally in Agda under strict flags but not yet +translated to an independent foundational system; **Grade 2i/2ii** = +translation to one/two independent foundations (2ii requires a non-DTT +second system, e.g. Isabelle/HOL); **Grade 1** = headless CI via verified +checker APIs. Verification receipts are tied to commit hashes; superseded +claims are marked historical, not silently dropped, and axiom dependence +(`Print Assumptions` / `#print axioms`) is tracked per row. + +[cols="2,1,2,3",options="header"] +|=== +| Artefact / claim | Stack status | Proof status (ledger token — estate grade) | Scope and assumptions + +| `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 + +| `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 +| Bounds: finite/bounded programs under a finite declared `O`; not a general proof + +| `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2) +| ACTIVE (CI `idris` job) +| `argued` — engineering-path interface artefact; type-checks, proves nothing +| ABI/FFI boundary only; carries `believe_me` escape hatches (T7 ruling) — not evidence for any theorem + +| `archive/proofs/coq/` — 14 theories +| ARCHIVED 2026-10-10 — not built, not gated +| `proven-with-postulates` — *historical, superseded*: headline "115 Qed / 0 Admitted / 61 Axioms"; census 109/182 top-level theorems closed under the global context, 73 resting on stdlib classical axioms and/or tagged parameters; 17 headline theorems zero-axiom. At best a Grade 2i *candidate* (Coq is DTT-family like Agda); receipts predate the archive ruling and are not CI evidence +| Counts describe this archived tree only; class-A / METAL-BOUNDARY tag grammar as recorded in the tree + +| `archive/proofs/lean4/` +| ARCHIVED 2026-10-10 — not built, not gated +| `proven-with-postulates` — *historical*: 52 Lean axioms incl. the strengthened `FilesystemCNO` preconditions and the class-A `y_combinator_not_identity`. Lean is DTT-family, so this leg adds no foundational diversity toward Grade 2ii +| Historical counts describe this tree only + +| `archive/proofs/isabelle/`, `archive/proofs/mizar/` +| ARCHIVED 2026-10-10 — not built, not gated +| *Historical receipts*: proved in their day (Isabelle: no `sorry`/`oops`; Mizar: empty `CNO.err`). Isabelle/HOL is the non-DTT (HOL/LCF) leg that could have supported Grade 2ii diversity — but it is archived and unexecuted, so it confers no current grade +| Not evidence in the active gate + +| `archive/proofs/verify-all-provers.six-prover.sh` + `archive/proofs/tests/gate-selftest.six-prover.sh` +| ARCHIVED — superseded by `proofs/verify-active-provers.sh` +| GENERATED gate script — historical +| Former six-prover gate (Coq, Agda, Lean, Z3, Isabelle, Mizar + Idris ABI) + +| OND-6 — conditional composition (research capstone) +| OPEN in every stack +| `open` — not proved, not assumed; no `Admitted`/postulate smuggled in anywhere in the active stack +| `docs/OND-ROADMAP.adoc`; deliberately open research fork + +| `proofs/observation-models/`, `proofs/residue/` +| ACTIVE inputs +| `argued` — declarative/generate proof inputs and honesty registers, not proofs +| Declared observation models `+O+` and residue lists; every OND certificate is relative to its declared `+O+` +|=== + +=== Reproduction receipts (this environment, 2026-11-01) + +* *Z3 — REPRODUCED HERE.* `z3` 5.3.3 (64-bit, via the `z3-solver` PyPI wheel, +the only package host reachable from this sandbox) running +`bash proofs/z3/verify.sh` → `Z3-CHECK OK`: 1 file +(`proofs/z3/ond/OND_checks.smt2`), 3 `(check-sat)` verdicts `sat unsat sat`, +all matching their `; expect` annotations, exit 0. Receipt commit: working +tree on branch `arena/1a7659fe-absolute-zero` over `bb46232`. +* *Agda, Idris 2, Coq, Lean 4, Isabelle/HOL, Mizar, Rust/Creusot — NOT +RUNNABLE HERE.* The sandbox egress allowlist (github.com, codeload.github.com, +api.github.com, registry.npmjs.org, pypi.org, files.pythonhosted.org) blocks +apt mirrors, static.rust-lang.org, opam.ocaml.org and Hackage, so none of +these toolchains can be installed in this session. Per standards +`3-practice/PROOF-POLICY.adoc` §6, a leg that cannot run is *said so*, never +reported as passing: the Agda `--safe --without-K` checks, the +`--cubical-compatible` recheck (open obligation, above), and the Idris 2 ABI +build remain CI receipts (`proofs.yml`: `agda`, `z3`, `idris` jobs), not +sandbox receipts. Archived provers stay archived and unexecuted. + +=== Role of this repository (consumer, not estate-wide ground truth) + +absolute-zero is a *consumer and domain formalisation*: it applies standard +results (Landauer 1961, Bennett 1973, the non-interference literature, +category theory) to its own CNO/OND domain concepts. Its historical prover +counts (above) are evidence about its own archived trees only, and must not +be cited as proof status for any other repository. + +*Cross-repo note (2026-11-01).* `epistemic-types` (at `5422cd5`) is an +*independent* proof library with **no dependency on absolute-zero**. Any +cross-repo claim must therefore name the exact theorem, its scope, and its +assumptions (e.g. "OND-1..5, `proven`, Grade 3, Agda `--safe --without-K`, +relative to a declared `O`") — never a bare count imported from this repo. +Mathesis (the estate mathematical knowledge commons) may *catalogue* these +receipts and grades, but per its own architecture the original repositories +remain the sovereign owners of their mathematics; this file is the local +proof-status record of record. + +[NOTE] +==== +The per-prover sections below this table are *historical* for Coq, Lean 4, +Isabelle/HOL and Mizar (archived 2026-10-10) and *active* only for Agda, Z3 +(bounded) and the Idris 2 ABI. They are kept for the record; the table above +is the canonical summary. +==== + == Coq — VERIFIED (this environment) * `coqc` **8.18.0**; clean build from scratch (all `.vo`/`.glob` deleted first), diff --git a/README.adoc b/README.adoc index 953abeb..7aa1739 100644 --- a/README.adoc +++ b/README.adoc @@ -67,42 +67,42 @@ composition, the research capstone) remains open by design. -- Landauer’s principle / reversible computing Standard (Landauer 1961, Bennett 1973) -`+proofs/coq/physics/+`, `+proofs/lean4/StatMech.lean+` +`+archive/proofs/coq/physics/+`, `+archive/proofs/lean4/StatMech.lean+` (archived) -- [verse] -- Non-interference / observational determinism Standard (security literature) -OND pillar +OND pillar (`+proofs/agda/OND.agda+`, active) -- [verse] -- Identity morphisms in category theory Standard -`+proofs/coq/category/+` +`+archive/proofs/coq/category/+` (archived) -- [verse] -- -Multi-prover cross-validation +Active prover gate (Agda + Z3 bounded + Idris 2 ABI) Standard methodology -`+proofs/verify-all-provers.sh+` +`+proofs/verify-active-provers.sh+`" -- [verse] -- CNO formalisation (termination + state preservation + purity + reversibility) *Novel assembly* -`+proofs/coq/common/CNO.v+` +`+proofs/agda/CNO.agda+` (active); `+archive/proofs/coq/common/CNO.v+` (archived) -- [verse] -- OND formalisation with declared `+O+` and residue lists *Novel formalisation* -`+proofs/coq/ond/OND.v+` +`+proofs/agda/OND.agda+` (active); `+archive/proofs/coq/ond/OND.v+` (archived) -- [verse] @@ -130,55 +130,72 @@ Status | OND Status -- Coq 8.19 Constructive type theory -115 Qed, 0 Admitted, 61 Axioms -OND-1..5: zero axioms +*ARCHIVED 2026-10-10* (`archive/proofs/coq/`) — historical: 115 Qed, 0 Admitted, 61 Axioms +OND-1..5: zero axioms (archived) -- [verse] -- Lean 4 Dependent type theory + Mathlib -Phases 1–4 complete, 52 Axioms -Mirrored +*ARCHIVED 2026-10-10* (`archive/proofs/lean4/`) — historical: Phases 1–4, 52 Axioms +Mirrored (archived) -- [verse] -- Agda 2.6 Dependent types -CNO + OND + EchoBridge (`EchoBridgeCNO.agda`, `--safe --without-K`) -Mirrored +*ACTIVE* — CNO + OND + EchoBridge (`EchoBridgeCNO.agda`, `--safe --without-K`, zero postulates) +OND-1..5 proved (mirrored) -- [verse] -- Z3 4.13 SMT solving -10 theorems encoded -Mirrored +*ACTIVE as bounded-check solver* — expect-annotated `sat`/`unsat` on bounded instances only +Mirrored (bounded instances) -- [verse] -- Isabelle/HOL Higher-order logic -Phase 1 complete -Mirrored +*ARCHIVED 2026-10-10* (`archive/proofs/isabelle/`) — historical: Phase 1 +Mirrored (archived) -- [verse] -- Mizar Set theory -Phase 1 complete -Mirrored +*ARCHIVED 2026-10-10* (`archive/proofs/mizar/`) — historical: Phase 1 +Mirrored (archived) +-- + +[verse] +-- +Idris 2 +Dependent types (ABI) +*ACTIVE* — ABI/FFI boundary only (`absolute-zero-abi.ipkg`); interface artefact, proves nothing +— -- |=== +The *canonical* proof-status table — separating active, archived, proved, +axiomatic and generated artefacts, with OND-6 explicitly open — lives in +link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. Figures quoted above for archived +provers are historical counts of those archived trees, not active status. +Estate proof grades (mathesis `estate-mathematical-architecture` §5) are +recorded there too: the active Agda proofs are **Grade 3** (local, +strict-flag, zero-postulate — not yet translated to an independent +foundation), the Z3 checks are `tested-only` (bounded), and OND-6 is `open`. + == [CAUTION] -== *Axioms are unproven assumptions, not theorems.* The Coq CNO development rests on 61 axioms (e.g., quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws). "`Machine-checked`" means checked _relative to those axioms_—not an axiom-free proof. The OND pillar (OND-1..5) is axiom-free. Discharging the CNO axioms is the next major obligation. +== *Axioms are unproven assumptions, not theorems.* The *archived* Coq CNO development (`archive/proofs/coq/`) rests on 61 axioms (e.g., quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws). "`Machine-checked`" there meant checked _relative to those axioms_—not an axiom-free proof. The active Agda OND pillar (OND-1..5) is axiom-free. Discharging the archived CNO axioms remains a recorded obligation of that historical tree. [NOTE] ==== @@ -188,7 +205,7 @@ Mirrored == [CAUTION] -== *Z3, Isabelle, and Mizar are generated but not yet run.* The artefacts exist in-tree but are not part of the CI gate. Only Coq, Lean 4, and Agda are machine-checked in CI. +== *Active gate = Agda + Z3 (bounded) + Idris 2 ABI build.* `proofs/verify-active-provers.sh` (→ `ACTIVE-PROVERS-GREEN`) is the one-shot active gate; CI (`proofs.yml`) runs the Agda `--safe --without-K` checks, the expect-annotated Z3 bounded checks, and the Idris 2 ABI build. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/` and are not machine-checked. == Known scope boundaries @@ -252,8 +269,8 @@ Malbolge (AffineScript), Brainfuck (Python), Whitespace (Python) with CNO detect [verse] -- -`+proofs/verify-all-provers.sh+` -One-shot gate: both pillars, all six provers + Idris ABI +`+proofs/verify-active-provers.sh+` +One-shot ACTIVE gate: Agda + Z3 (bounded) + Idris 2 ABI (`ACTIVE-PROVERS-GREEN`) -- |=== @@ -262,17 +279,17 @@ One-shot gate: both pillars, all six provers + Idris ABI === [source,bash] -== One-shot: both pillars, all provers +== One-shot: active provers (Agda + Z3 bounded + Idris 2 ABI) -proofs/verify-all-provers.sh +proofs/verify-active-provers.sh == Or via task runner just verify -== Individual provers +== Individual active provers -just build-coq just verify-agda —- +just verify-agda just verify-z3 just verify-idris —- == Documentation diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 75fc9ce..df073c8 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -33,9 +33,12 @@ prover run in a known environment, not a reading of in-file comments. == Honest Current State -Updated 2026-07-07 (PR #100). Both pillars are now machine-checked across six -provers plus the Idris ABI; reproduce with `proofs/verify-all-provers.sh` -(`ALL-PROVERS-GREEN`). See `PROOF-STATUS.adoc` for the prover-by-prover detail. +Updated 2026-07-07 (PR #100); reconciled 2026-11-01. The active stack — Agda +(CNO, OND, EchoBridge; `--safe --without-K`, zero postulates), Z3 bounded +expect-checked instances, and the Idris 2 ABI — is machine-checked; reproduce +with `proofs/verify-active-provers.sh` (`ACTIVE-PROVERS-GREEN`). The former +six-prover gate is archived (`archive/proofs/verify-all-provers.six-prover.sh`). +See `PROOF-STATUS.adoc` for the canonical active-vs-archived proof-status table. === What genuinely verifies diff --git a/docs/MACHINE_VERIFICATION.adoc b/docs/MACHINE_VERIFICATION.adoc index fec1c9d..d23a385 100644 --- a/docs/MACHINE_VERIFICATION.adoc +++ b/docs/MACHINE_VERIFICATION.adoc @@ -2,12 +2,14 @@ // Copyright (c) Jonathan D.A. Jewell # Machine Verification Guide -> **STATUS 2026-07-07 (PR #100):** This guide's *method* still applies, but its -> illustrative pass/fail examples below are historical. The estate now verifies -> **clean across all six provers + the Idris ABI** (0 `Admitted`/`sorry`); run -> `proofs/verify-all-provers.sh` for `ALL-PROVERS-GREEN`, and see -> `PROOF-STATUS.adoc` for the reproduced prover-by-prover status. Treat the -> counts in the examples that follow as pedagogical, not current. +> **STATUS 2026-07-07 (PR #100), reconciled 2026-11-01:** This guide's *method* +> still applies, but its illustrative pass/fail examples below are historical. +> The *active* stack — Agda (`--safe --without-K`, zero postulates) + Z3 bounded +> checks + the Idris 2 ABI — verifies clean; run `proofs/verify-active-provers.sh` +> for `ACTIVE-PROVERS-GREEN`. Coq/Lean 4/Isabelle/Mizar are archived under +> `archive/proofs/`. See `PROOF-STATUS.adoc` for the canonical active-vs-archived +> proof-status table. Treat the counts in the examples that follow as pedagogical, +> not current. ## Current Status: PARTIAL VERIFICATION (historical example) diff --git a/docs/PROOF-COMPLETION-PLAN.adoc b/docs/PROOF-COMPLETION-PLAN.adoc index 90ff8e2..cc1cdda 100644 --- a/docs/PROOF-COMPLETION-PLAN.adoc +++ b/docs/PROOF-COMPLETION-PLAN.adoc @@ -8,10 +8,11 @@ .HISTORICAL PLAN — largely executed (2026-07-06, PR #100) ==== This strategy (dated 2026-02-05) has since been carried out and superseded. -There are now **0 `Admitted`** across the Coq development, both pillars are -machine-checked across six provers + Idris, and the CNO axiom base was cut -98→small. Current status: `PROOF-STATUS.adoc`; reproduce with -`proofs/verify-all-provers.sh`. The plan below is kept for provenance. +The historical Coq development reached **0 `Admitted`** and both pillars were +machine-checked across six provers + Idris; since the 2026-10-10 archive +ruling the *active* stack is Agda + Z3 (bounded) + Idris 2 ABI. Current +status: `PROOF-STATUS.adoc` (canonical active-vs-archived table); reproduce +with `proofs/verify-active-provers.sh`. The plan below is kept for provenance. ==== == Date: 2026-02-05