Operations and Observational Null Disclosure :toc: preamble :toc-title: Contents :icons: font :doctype: article

" class="bare">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

CNO
Null effect: operation leaves state identical, is pure, and is thermodynamically reversible
State

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

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)

Lean 4
Dependent type theory + Mathlib
ARCHIVED 2026-10-10 (archive/proofs/lean4/) — historical: Phases 1–4, 52 Axioms
Mirrored (archived)

Agda 2.6
Dependent types
ACTIVE — CNO + OND + EchoBridge (EchoBridgeCNO.agda, --safe --without-K, zero postulates)
OND-1..5 proved (mirrored)

Z3 4.13
SMT solving
ACTIVE as bounded-check solver — expect-annotated sat/unsat on bounded instances only
Mirrored (bounded instances)

Isabelle/HOL
Higher-order logic
ARCHIVED 2026-10-10 (archive/proofs/isabelle/) — historical: Phase 1
Mirrored (archived)

Mizar
Set theory
ARCHIVED 2026-10-10 (archive/proofs/mizar/) — historical: Phase 1
Mirrored (archived)

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 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 docs/EXCEPTION-T1-2026-10-12.adoc for the LANGUAGE-POLICY exception and 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

• EXPLAINME — claim-by-claim receipts and known gaps

• 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 LICENSE.

Prose documentation is licensed under CC-BY-SA-4.0; see LICENSES/.====

Repository Layout

[cols=“1,3”, options=“header”] |=== | Path | Purpose

proofs/coq/
Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND