Skip to content

ROADMAP.adoc

Latest commit

 

History

History
226 lines (188 loc) · 11 KB

ROADMAP.adoc

File metadata and controls

226 lines (188 loc) · 11 KB
Raw

Absolute Zero: Roadmap

Table of Contents

1. Executive Summary

Absolute Zero is a solo-maintained formal-methods research project that mechanises null operations — programs proven to do nothing — across proof assistants. It rests on two co-equal pillars: CNO (Certified Null Effect) and OND (Observational Null / Certified Null Disclosure).

This roadmap is deliberately scoped to what one maintainer can credibly ship. The original near-term goal — a publishable CNO result with a truthful proof ledger and the first three OND obligations landed — has been met and exceeded: OND-1..5 are landed and both pillars are machine-checked across six provers (PR #100). The remaining near-term goal is the paper and CI. Not a funded platform; The long-horizon vision (a universal CNO standard) is preserved, clearly labelled as aspirational and unfunded, in the appendix; it is a direction of travel, not a commitment with a date.

Note

Status honesty. Completion figures here describe what a checker actually reproduces (see PROOF-STATUS.adoc), not aspirations. "Verified" means a prover run in a known environment, not a reading of in-file comments.

2. 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.

2.1. What genuinely verifies

  • Coq (reproduced): 14 theories compile 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 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).

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

  • Idris 2 ABI (reproduced): absolute-zero-abi.ipkg builds clean.

  • Rust interpreters: Brainfuck and Whitespace interpreters are real.

2.2. What is honestly incomplete

Area State Note

CNO axiom base

98 → small classified remainder

filesystem/category/ QuantumMechanicsExact fully discharged (0); QuantumCNO 41→12. Kept axioms are either genuine physical postulates (tagged METAL-BOUNDARY: kB>0, temperature>0, Landauer, Second Law) or class-A (true, provable in principle, openly labelled). Three unsound axioms were removed/corrected (no_cloning, Cconj_Cexp, eta_equivalence).

Class-A open proofs

4

CNOT_gate_unitary, unitary_inverse_property, fidelity_bound (need a finite-dim/tensor QM model), and y_not_cno (needs a 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.

Paper

Draft stub

papers/.latex/main.tex is a lone draft.

Tests

Empty placeholder

tests/ holds a README only.

3. The Second Pillar: Observational Null Operations (OND)

Absolute Zero is a two-pillar project. Alongside CNO (Certified Null Effect — "does nothing to the world"), the OND pillar (Certified Null Disclosure — "reveals nothing about its secret input, relative to a declared observation model O`") is a co-equal sibling, not an extension. The two are logically independent (a proved theorem, with witnesses) and connected by a coupling-dial frame (framing, not theorem). The honest edge of OND is the model-vs-metal boundary: every OND claim is conditional on its declared `O and ships a residue list of out-of-scope observables.

OND obligations (prioritised; full detail in docs/OND-ROADMAP.adoc):

  1. OND-1 — the OND definition, formalised (parameterised by O, emitting a residue list). Keystone.

  2. OND-2 — trivial-case satisfiability (skip is OND in any O) — the definition’s smoke-test.

  3. OND-3 — the CNO ⊥ OND independence theorem (the result that earns the two-pillar split).

  4. OND-4 — a conditional-proof template for one real constant-time operation (+ its metal-discharge statement and residue list).

  5. OND-5 — the non-composition counterexample (ONDs do not compose cleanly — state-chaining + emergent boundary observables; the DP-budget / quasi-identifier shape).

  6. OND-6 — the conditional composition theorem (the heavily-qualified positive result; research-grade; last).

  7. OND-7 — the ongoing residue register (the standing proof↔reality gap).

Status (2026-07-07): OND-1..5 and OND-7 are landed — proved and machine-checked in Coq (zero axioms), Lean 4, and Agda, with Z3 for the bounded instances, and OND-3 anchored to the real core is_CNO. Only OND-6 (conditional composition) remains open, by design — the pillar is in the honest, publishable shape this roadmap targeted (see docs/OND-ROADMAP.adoc).

Note

The proof effort must investigate OND-5/OND-6 (composition) most carefully: if it concludes ONDs compose as cleanly as CNOs, that conclusion is almost certainly wrong (it has dropped either the state-chaining or the boundary-observable term) and must be re-checked.

4. Near-Term Roadmap (the actual next steps)

No fixed dates — a solo project proceeds as time allows. Ordered by value.

4.1. Milestone 1: Truthful ledger + the theorem MAA needs

Absolute Zero is the CNO foundation that hyperpolymath/maa-framework coordinates as a pinned submodule. The theorem MAA actually cites is the general reversibility biconditional.

  • ✓ Reversibility <→ CNO bridge — landed in Coq (2026-07-16, zero axioms). proofs/coq/common/CNO.v 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 reverses_seq_computes_identity. All Closed under the global context. Finding: the literal reversible p ↔ ∃ p_inv, is_CNO (p;;p_inv) ∧ is_CNO (p_inv;;p) is not provable here — is_CNO over-demands purity/totality, state_eq excludes the PC (forcing up-to-=st=), and reversible is one-sided; so the contract should be stated two-sided and =st=-relative (see PROOF-STATUS.adoc). Remaining: Lean mirror.

  • ❏ Discharge the filesystem existence axioms in FilesystemCNO.v so valence_reversible_pair_is_cno becomes axiom-free.

  • ❏ Discharge the "provable debt" axioms triaged in proof-debt-triage.md (existence witnesses: mkdir_not_identity, write_different_not_identity, X_gate_not_identity, H_gate_not_identity; dedupe triple-declared physics constants).

  • ❏ Repair the Idris2 ABI package (align module names ↔ paths ↔ sourcedir; fix the Types.idr errors) so idris2 --build absolute-zero-abi.ipkg succeeds.

  • ❏ Make CI truthful: run Coq(13) + Agda(3) + Rust; either add a real cno_properties.smt2 or delete the Z3 job and its "10 theorems" claim; drop ReScript/TS/Python jobs; fix the mangled README table and the CNO-acronym inconsistency.

Done means: the proof ledger reflects only what actually checks, the reversibility bridge is proved, and MAA can build against a stable surface.

4.2. Milestone 2: OND minimum viable pillar

  • ❏ OND-1 definition (observation model O + residue) in Coq + Lean.

  • ❏ OND-2 trivial-case satisfiability.

  • ❏ OND-3 CNO ⊥ OND independence theorem.

Done means: OND has a credible, checked core; OND-4..6 remain openly Admitted — an honest, publishable state.

4.3. Milestone 3: The paper

  • ❏ "Certified Null Operations: machine-checked nothingness across proof assistants" — submission-viable on the CNO pillar alone (13 Coq + 3 Agda
    honest axiom disclosure). Target: ITP / CPP / VSTTE, or a PACMPL venue.

  • ❏ Artifact-evaluation package: one-command container verification.

4.4. Milestone 4: Make it demonstrable

  • ❏ cno-verify Rust library + CLI as a small, real deliverable.

  • ❏ Coupling-dial demo in the existing Elm playground (elm/): toggle the observation model O, watch CNO=yes / OND=no flip — the live witness for OND-3 and the paper’s best figure.

  • ❏ Populate tests/ with unit tests for the Rust interpreters and proof-property checks.

Appendix A: Long-Horizon Vision (aspirational, unfunded)

Important

Everything below is a direction of travel, not a plan with dates, staffing, or budget. It is retained so the ambition is not lost, but it is explicitly out of scope for the solo effort described above. Treat the figures as illustrative of scale, not as commitments.

The long-term ambition is to establish Certified Null Operations as a universal computational primitive — CNO detection built into compilers, proof assistants, and verification tools; a shared specification; a community around computational nullity. Plausible directions, roughly in order:

  • Language expansion — CNO verification beyond esoteric languages (C, Rust, SQL, assembly nop, WebAssembly), via a language-agnostic specification and a plugin architecture.

  • Tooling integration — LLVM/GCC/rustc passes, cargo cno-verify, IDE plugins; bridges to Frama-C, Why3, Dafny, F*, TLA+; standard proof-certificate output (SMT-LIB, TPTP, LFSC/Dedukti).

  • Automated proof support — SMT-backed proof search and ML-assisted proof suggestion for the decidable/bounded fragments.

  • New domains — quantum CNOs (unitary/state preservation), hardware (nop/RTL), scientific computing (Julia-native).

  • Standardisation & adoption — a reference specification others can implement against; curriculum material; long-run community stewardship.

The original multi-year phase/FTE/budget breakdown that once stood in the body of this document was disproportionate to a repo still discharging existence lemmas, and has been retired. If the project ever attracts funding and contributors, a resourced roadmap can be written against reality at that point.

"From nothing, everything. From zero, infinity."

— Jonathan D. A. Jewell