// SPDX-License-Identifier: MPL-2.0 = Absolute Zero — Certified Null Operations and Observational Null Disclosure :toc: preamble :toc-title: Contents :icons: font :doctype: article image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="`https://www.bestpractices.dev/projects/XXXX`"] Multi-prover formal verification of programs that provably compute nothing (CNO) and programs that provably reveal nothing (OND). Two co-equal pillars: Certified Null Effect and Certified Null Disclosure. [IMPORTANT] ==== *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. ==== == Overview Absolute Zero formalises two kinds of computational nothingness: CNO (Certified Null Effect):: A program that does nothing to the world: it terminates, maps input state to identical output state, is pure, and is thermodynamically reversible. The conserved quantity is state. OND (Observational Null Disclosure):: A program that reveals nothing about its secret input to a declared observer: its observable trace is constant over the secret, relative to a declared observation model `+O+`. The conserved quantity is the secret-to-observable channel. Every OND claim ships a residue list of out-of-scope observables: the honest boundary between the proof and the physical metal. The two pillars are logically independent (a proved theorem, with witnesses). They are connected by a coupling dial between a thing and the trace it casts to an observer—this dial is framing, not theorem. == The two pillars [cols="`1,2,2`", options="`header`"] |=== | Pillar | Certifies | Conserved quantity [verse] -- CNO Null _effect_: operation leaves state identical, is pure, and is thermodynamically reversible State -- [verse] -- OND Null _disclosure_: observable trace is constant over the secret input, relative to observation model `+O+` Secret→observable channel -- |=== Both pillars are machine-checked. OND obligations OND-1..5 are proved with zero axioms in Coq, mirrored in Lean 4, Agda, and Z3. The independence theorem is anchored to `+is_CNO+`. OND-6 (conditional composition, the research capstone) remains open by design. == What is standard and what is ours [cols="`1,2,2`", options="`header`"] |=== | Concept | Status | Home [verse] -- Landauer’s principle / reversible computing Standard (Landauer 1961, Bennett 1973) `+archive/proofs/coq/physics/+`, `+archive/proofs/lean4/StatMech.lean+` (archived) -- [verse] -- Non-interference / observational determinism Standard (security literature) OND pillar (`+proofs/agda/OND.agda+`, active) -- [verse] -- Identity morphisms in category theory Standard `+archive/proofs/coq/category/+` (archived) -- [verse] -- Active prover gate (Agda + Z3 bounded + Idris 2 ABI) Standard methodology `+proofs/verify-active-provers.sh+`" -- [verse] -- CNO formalisation (termination + state preservation + purity + reversibility) *Novel assembly* `+proofs/agda/CNO.agda+` (active); `+archive/proofs/coq/common/CNO.v+` (archived) -- [verse] -- OND formalisation with declared `+O+` and residue lists *Novel formalisation* `+proofs/agda/OND.agda+` (active); `+archive/proofs/coq/ond/OND.v+` (archived) -- [verse] -- CNO ↔ OND independence proof *Novel theorem* Core proofs -- [verse] -- Malbolge / Brainfuck / Whitespace CNO verification *Novel application* `+interpreters/+`, `+proofs/coq/malbolge/+` -- |=== == Multi-prover verification [cols="`1,2,2,2`", options="`header`"] |=== | Prover | Foundation | CNO Status | OND Status [verse] -- Coq 8.19 Constructive type theory *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 *ARCHIVED 2026-10-10* (`archive/proofs/lean4/`) — historical: Phases 1–4, 52 Axioms Mirrored (archived) -- [verse] -- Agda 2.6 Dependent types *ACTIVE* — CNO + OND + EchoBridge (`EchoBridgeCNO.agda`, `--safe --without-K`, zero postulates) OND-1..5 proved (mirrored) -- [verse] -- Z3 4.13 SMT solving *ACTIVE as bounded-check solver* — expect-annotated `sat`/`unsat` on bounded instances only Mirrored (bounded instances) -- [verse] -- Isabelle/HOL Higher-order logic *ARCHIVED 2026-10-10* (`archive/proofs/isabelle/`) — historical: Phase 1 Mirrored (archived) -- [verse] -- Mizar Set theory *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 *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] ==== 2026-10-12: the Coq, Lean 4, Isabelle/HOL and Mizar developments are archived under `archive/` (owner ruling 2026-10-10); the 61 axioms are theirs. The active stack is Idris2 (ABI) + Agda (`proofs/agda/`: CNO, OND, EchoBridgeCNO), zero axioms, with Z3 for bounded checks. See link:docs/EXCEPTION-T1-2026-10-12.adoc[] for the LANGUAGE-POLICY exception and link:docs/DECISION-T7-2026-10-12.adoc[] for the T7 ruling. ==== == [CAUTION] == *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 == [CAUTION] == *OND-6 (conditional composition) is open.* OND obligations 1–5 are proved. OND-6, the research capstone for composing OND-certified operations under conditions, remains open by design. == [CAUTION] == *OND claims are conditional on the declared observation model `+O+`.* An OND proof certifies non-disclosure _relative to `+O+`_. It ships a residue list of out-of-scope observables (timing, power, cache). The proof does not cover observables not in `+O+`. == [CAUTION] == *CNO verification is undecidable in general* (reduction from the halting problem). The formalisations here verify specific programs or finite-state classes, not arbitrary programs. == Repository Layout [cols="`1,3`", options="`header`"] |=== | Path | Purpose [verse] -- `+proofs/coq/+` Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND -- [verse] -- `+proofs/lean4/+` Lean 4 mirrors of CNO and OND modules -- [verse] -- `+proofs/agda/+`, `+proofs/z3/+`, `+proofs/isabelle/+`, `+proofs/mizar/+` Additional prover artefacts (Agda checked in CI; others generated but not yet run) -- [verse] -- `+proofs/ond/+` OND Coq module (OND-1..5 proved, zero axioms) -- [verse] -- `+proofs/observation-models/+` Declared observation models `+O+` (proof inputs for OND) -- [verse] -- `+proofs/residue/+` OND residue lists (model-vs-metal gap) -- [verse] -- `+interpreters/+` Malbolge (AffineScript), Brainfuck (Python), Whitespace (Python) with CNO detection -- [verse] -- `+proofs/verify-active-provers.sh+` One-shot ACTIVE gate: Agda + Z3 (bounded) + Idris 2 ABI (`ACTIVE-PROVERS-GREEN`) -- |=== == Build === [source,bash] == One-shot: active provers (Agda + Z3 bounded + Idris 2 ABI) proofs/verify-active-provers.sh == Or via task runner just verify == Individual active provers just verify-agda just verify-z3 just verify-idris —- == Documentation * link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps * link:GLOSSARY.adoc[GLOSSARY] — terminology reference * `+docs/TWO-PILLARS.adoc+` — narrative description of CNO and OND * `+docs/OND-ROADMAP.adoc+` — prioritised OND obligations * `+docs/ECOSYSTEM-CONNECTIONS.adoc+` — downstream applications (JanusKey, Echo Types, Typell, Robodog, Robot Vacuum) * `+PROOF-STATUS.adoc+` — per-prover verification status == License SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. Prose documentation is licensed under CC-BY-SA-4.0; see `+LICENSES/+`.==== == Repository Layout [cols="`1,3`", options="`header`"] |=== | Path | Purpose [verse] -- `+proofs/coq/+` Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND --