diff --git a/README.md b/README.md index ee7ef47..24b1743 100644 --- a/README.md +++ b/README.md @@ -1,502 +1,210 @@ - - -**Formal Verification of Null Operations — two co-equal pillars: -Certified Null *Effect* (CNO) and Certified Null *Disclosure* (OND)** - -![MPL-2](https://img.shields.io/badge/License-MPL_2.0-blue.svg) [![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) - -# License - -[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/absolute-zero) - -**SPDX-License-Identifier: CC-BY-SA-4.0** - -Licensed under the Mozilla Public License 2.0. See `LICENSE` for full -text. - -\> **"The universe tends toward maximum entropy. A Certified Null -Operation is a pocket of perfect computational order—a program that -resists the Second Law. It does nothing, but in doing nothing, it says -everything about the structure of computation itself."** - -# What is Absolute Zero? - -**Absolute Zero** is a research project exploring the formal -verification of programs that provably compute nothing. We formalize -**Certified Null Operations (CNOs)**—programs that, despite potentially -complex implementations, can be mathematically proven to have zero net -computational effect. - -**The Central Question**: Can we formally prove that a program does -absolutely nothing? - -This seemingly trivial question leads to deep insights in: - **Formal -Verification**: Machine-checked proofs of program properties - -**Computational Complexity**: Understanding minimal computation - -**Reversible Computing**: Programs preserving thermodynamic -reversibility - **Esoteric Languages**: Using Malbolge as -proof-of-concept - -# The Two Pillars - -Absolute Zero rests on **two co-equal pillars** — siblings of equal -weight, not parent and extension: - -- **CNO — Certified Null *Effect*.** Certifies that an operation does - **nothing to the world**: it terminates, maps input state to identical - output state, is functionally pure, and is thermodynamically - reversible (Landauer/Bennett). The conserved quantity is **state**. - -- **OND — Observational Null Operations / Certified Null *Disclosure*.** - Certifies that an operation **reveals nothing about its secret input** - to a declared observer: its observable trace (timing, size, …) is - constant over the secret, **relative to a declared observation model - `O`**. The conserved quantity is the **secret→observable channel**. - -The two are **logically independent** (neither entails the other — a -proved theorem, with witnesses), connected by a single **coupling dial** -between a thing and the trace it casts to an observer: CNO witnesses the -emptiness of the **effect** channel; OND certifies the emptiness of the -**disclosure** channel (this dial is **framing, not theorem**). Unlike -CNO — which lives entirely inside the formal model — every OND claim is -**conditional on its declared `O`** and ships a **residue list** of -out-of-scope observables: the honest, explicit boundary between the -proof and the physical metal. - -See **`docs/TWO-PILLARS.adoc`** (narrative), **`docs/OND-ROADMAP.adoc`** -(prioritised obligations), and **`docs/OND-PILLAR-STRUCTURE.adoc`** -(module layout). **Both pillars are now machine-checked.** OND obligations -**OND-1..5** are proved with **zero axioms** in Coq (`proofs/coq/ond/OND.v`, -every theorem *Closed under the global context*), mirrored in Lean 4, Agda, -and Z3; the independence theorem is anchored to the real core `is_CNO`. Only -**OND-6** (conditional composition, the research capstone) remains open, by -design. Reproduce the whole estate — both pillars, all six provers plus the -Idris ABI — with **`proofs/verify-all-provers.sh`** (`ALL-PROVERS-GREEN`). - -# Project Structure - - absolute-zero/ - ├── proofs/ # Formal proofs in multiple systems - │ ├── coq/ # Coq proofs (constructive) - │ │ ├── common/ # Core CNO framework (CNO.v) - │ │ ├── malbolge/ # Malbolge-specific proofs - │ │ ├── physics/ # Statistical mechanics (StatMech.v) - │ │ ├── category/ # Category theory (CNOCategory.v) - │ │ ├── lambda/ # Lambda calculus (LambdaCNO.v) - │ │ ├── quantum/ # Quantum computing (QuantumCNO.v) - │ │ └── filesystem/ # Filesystem CNOs (FilesystemCNO.v) - │ │ - │ ├── lean4/ # Lean 4 proofs (modern) - │ │ ├── CNO.lean # Core CNO framework - │ │ ├── StatMech.lean # Statistical mechanics - │ │ ├── CNOCategory.lean # Category theory - │ │ ├── LambdaCNO.lean # Lambda calculus - │ │ ├── QuantumCNO.lean # Quantum computing - │ │ └── FilesystemCNO.lean # Filesystem operations - │ │ - │ ├── z3/ # Z3 SMT verification (automated) - │ ├── agda/ # Agda proofs (dependent types) - │ ├── isabelle/ # Isabelle/HOL (production-grade) - │ ├── mizar/ # Mizar proofs (mathematical library) - │ ├── ond/ # OND Coq module (OND-1..5 proved, zero axioms) - │ ├── observation-models/ # OND: declared observation models O (proof inputs) - │ ├── residue/ # OND: residue lists (the model-vs-metal gap) - │ └── verify-all-provers.sh # one-shot gate: both pillars, all six provers + Idris - │ # Each prover dir hosts CNO.* and co-equal OND.* modules (OND now authored) - │ - ├── interpreters/ # Language interpreters with CNO detection - │ ├── rescript/ # Malbolge (ReScript) - │ ├── brainfuck/ # Brainfuck (Python) - │ └── whitespace/ # Whitespace (Python) - │ - ├── docs/ # Comprehensive documentation - │ ├── theory.md # Theoretical foundations - │ ├── examples.md # CNO examples across languages - │ ├── proofs-guide.md # How to write proofs - │ └── philosophy.md # Epistemology of nothingness - │ - ├── examples/ # CNO example programs - │ ├── malbolge/ - │ ├── brainfuck/ - │ └── whitespace/ - │ - ├── tests/ # Comprehensive test suite - │ ├── unit/ - │ └── proofs/ - │ - ├── papers/ # Research paper drafts - │ └── .latex/ - │ - ├── Justfile # Build automation - ├── Containerfile # Containerized verification (Podman/Docker) - ├── PROOF-STATUS.adoc # Reproduced verification status, prover by prover - └── .github/workflows/ # CI/CD (GitHub Actions) - -# Quick Start - -## Prerequisites - -The proofs span six provers plus the Idris 2 ABI. Coq, Agda, Z3, and Idris 2 are -the lightest; Lean needs Mathlib, and Isabelle/Mizar are large downloads. - -- **Coq** 8.18+ (`coqc`, `coq_makefile`) -- **Agda** 2.6.3 (with agda-stdlib) -- **Lean 4** (via `elan`; toolchain pinned in `proofs/lean4/lean-toolchain`, needs Mathlib) -- **Z3** 4.16+ -- **Isabelle** 2025-2 (ships a prebuilt HOL image) -- **Mizar** 8.1.x (set `MIZFILES` to its MML) -- **Idris 2** 0.8+ -- **just** (task runner), **Rust/cargo** (interpreters/tools) - -## Build & verify - -```bash -# One-shot: both pillars, all six provers + the Idris ABI → ALL-PROVERS-GREEN -proofs/verify-all-provers.sh - -# Or via the task runner (canonical gate) -just verify - -# Individual prover targets also exist, e.g. -just build-coq # all 14 Coq theories (CNO + OND) via coq_makefile -just verify-agda -just verify-mizar -``` - -## Container (Podman/Docker) - -```bash -# Build image (Podman recommended) -podman build -t absolute-zero . - -# Run verification -podman run --rm absolute-zero just verify-all - -# Docker compatibility -docker build -t absolute-zero . -docker run --rm absolute-zero just verify-all -``` - -# What is a CNO? - -A **Certified Null Operation** is a program with the following formally -proven properties: - -## Formal Definition - - ∀ σ : ProgramState, ∀ p : Program, - IsCNO(p) ↔ ( - Terminates(p, σ) ∧ // Always halts - FinalState(p, σ) = σ ∧ // Identity mapping - NoSideEffects(p) ∧ // Pure - ThermodynamicallyReversible(p) // Zero energy - ) - -## Properties - -- ✅ **Termination**: Always halts - -- ✅ **State Preservation**: Input state = Output state - -- ✅ **Purity**: No I/O, no memory allocation - -- ✅ **Reversibility**: Can be undone with zero energy cost (Landauer’s - principle) - -# Examples - -## Brainfuck CNOs - -```brainfuck - (empty program) ->< (move right then left) -+- (increment then decrement) ->><< (multiple balanced moves) -``` - -## Whitespace CNOs - -```whitespace - -(three linefeeds = immediate halt) -``` - -## Malbolge CNOs - -```malbolge -(empty program - "Absolute Zero") -``` - -# Multi-Prover Verification - -For maximum confidence, we verify CNO properties in **six independent -proof systems**: - -\| Proof System \| Foundation \| Lines of Proof \| Status \| -\|-------------\|------------\|----------------\|--------\| \| **Coq -8.19** \| Constructive type theory \| ~4000+ \| ✅ 81 Qed, 19 Admitted -(81% complete) \| \| **Z3 4.13** \| SMT solving \| ~400 \| ✅ Complete -(10 theorems encoded, awaiting `z3`) \| \| **Lean 4** \| Dependent type -theory \| ~2500+ \| ✅ Phases 1-4 complete \| \| **Agda 2.6** \| -Dependent types \| ~400 \| ✅ Phase 1 complete (awaiting `agda`) \| \| -**Isabelle/HOL** \| Higher-order logic \| ~350 \| ✅ Phase 1 complete -(awaiting `isabelle`) \| \| **Mizar** \| Set theory \| ~300 \| ⚠️ -Requires complex installation \| - -## Verification Phases - -**🎉 Phase 1 Complete**: All core composition theorems proven, all -proofs syntax-complete. - -**🎉 Phase 2-4 Complete**: Advanced theoretical foundations implemented -(5 new modules, 10 proof files, ~3500 lines): - -\| Module \| Description \| Coq \| Lean 4 \| -\|--------\|-------------\|-----\|--------\| \| **Statistical -Mechanics** \| Landauer’s Principle, thermodynamic reversibility \| ✅ 9 -Qed \| ✅ \| \| **Category Theory** \| Universal CNO definition, model -independence \| ✅ 8 Qed \| ✅ \| \| **Lambda Calculus** \| Functional -programming CNOs \| ✅ 9 Qed, 1 Admitted \| ✅ \| \| **Quantum -Computing** \| Quantum gates, unitary operations \| 🟡 12 Qed, 5 -Admitted \| ✅ \| \| **Filesystem Operations** \| Valence Shell -integration, practical CNOs \| 🟡 8 Qed, 6 Admitted \| ✅ \| +// SPDX-License-Identifier: MPL-2.0 += Absolute Zero — Certified Null Operations and Observational Null Disclosure +:toc: preamble +:toc-title: Contents +:icons: font +:doctype: article -See \[VERIFICATION.md\](VERIFICATION.md) for detailed status and -\[PROOF-INSIGHTS.md\](PROOF-INSIGHTS.md) for proof engineering -knowledge. +image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"] -**Coq Proof Status** (2026-06-29): 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* (unproven assumptions, not theorems: e.g. -quantum-gate unitarity, complex-analysis identities, Shannon-entropy -non-negativity, filesystem inverse laws). "Machine-checked" here means checked -*relative to those axioms* — not an axiom-free proof. (The status table above is -pre-conversion and stale; these are the current figures.) +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. -**Verification scope**: Coq, Lean 4 and Agda are machine-checkable in-tree; the -Z3, Isabelle and Mizar artefacts are *generated but not yet run* — not evidence. +== Overview -**Next Step**: Discharge (or justify) the axioms — especially the domain-specific -ones (gate unitarity, filesystem inverse laws) — and machine-run Z3/Isabelle/Mizar. +Absolute Zero formalises two kinds of computational nothingness: -# Research Contributions +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. -## Core Formalization (Phase 1) +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. -1. **Formal Definitions**: Define CNOs in 6 proof systems +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. -2. **Multi-Prover Verification**: Cross-validate results across Coq, - Z3, Lean 4, Agda, Isabelle +== The two pillars -3. **Composition Theorems**: Prove CNOs compose under sequential - execution +[cols="1,2,2", options="header"] +|=== +| Pillar | Certifies | Conserved quantity -4. **Malbolge Verification**: Prove esoteric language CNOs +| CNO +| Null *effect*: operation leaves state identical, is pure, and is thermodynamically reversible +| State -5. **Complexity Analysis**: Show CNO verification is undecidable in - general +| OND +| Null *disclosure*: observable trace is constant over the secret input, relative to observation model `O` +| Secret→observable channel +|=== -## Advanced Foundations (Phases 2-4) +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. -6. **Thermodynamic Formalization**: Rigorous Landauer’s Principle and - Bennett’s reversible computing +== What is standard and what is ours -7. **Category Theory**: Universal CNO definition as identity morphisms, - model independence proofs +[cols="1,2,2", options="header"] +|=== +| Concept | Status | Home -8. **Lambda Calculus**: Prove identity function (λx.x) is canonical - functional CNO +| Landauer's principle / reversible computing +| Standard (Landauer 1961, Bennett 1973) +| `proofs/coq/physics/`, `proofs/lean4/StatMech.lean` -9. **Quantum Computing**: Extend CNO theory to quantum gates and - circuits +| Non-interference / observational determinism +| Standard (security literature) +| OND pillar -10. **Filesystem Operations**: Integrate Valence Shell reversibility, - prove real-world CNOs +| Identity morphisms in category theory +| Standard +| `proofs/coq/category/` -## Practical Applications +| Multi-prover cross-validation +| Standard methodology +| `proofs/verify-all-provers.sh` -11. **Secure Sandboxing**: Run untrusted code proven inert +| CNO formalisation (termination + state preservation + purity + reversibility) +| **Novel assembly** +| `proofs/coq/common/CNO.v` -12. **Compiler Optimization**: Detect and eliminate dead code +| OND formalisation with declared `O` and residue lists +| **Novel formalisation** +| `proofs/coq/ond/OND.v` -13. **Energy-Efficient Computing**: Baseline for zero-energy computation +| CNO ↔ OND independence proof +| **Novel theorem** +| Core proofs -14. **Transaction Systems**: Prove database rollback operations are CNOs +| Malbolge / Brainfuck / Whitespace CNO verification +| **Novel application** +| `interpreters/`, `proofs/coq/malbolge/` +|=== -# Theoretical Foundations +== Multi-prover verification -## Landauer’s Principle +[cols="1,2,2,2", options="header"] +|=== +| Prover | Foundation | CNO Status | OND Status -**Landauer’s Principle** (1961): Erasing one bit of information -dissipates at least `kT` `ln` `2` of energy. +| Coq 8.19 +| Constructive type theory +| 115 Qed, 0 Admitted, 61 Axioms +| OND-1..5: zero axioms -At room temperature (300K): `` ` `` `E_min` `=` `kT` `ln` `2` `≈` `2.87` -`×` `10⁻²¹` `Joules` `per` `bit`\` +| Lean 4 +| Dependent type theory + Mathlib +| Phases 1–4 complete, 52 Axioms +| Mirrored -**Implication**: A CNO dissipates **zero energy** because it erases no -information. +| Agda 2.6 +| Dependent types +| Phase 1 complete +| Mirrored -## Computational Complexity +| Z3 4.13 +| SMT solving +| 10 theorems encoded +| Mirrored -**Theorem**: The problem "Is program p a CNO?" is **undecidable** in -general. +| Isabelle/HOL +| Higher-order logic +| Phase 1 complete +| Mirrored -**Proof**: Reduction from the halting problem. +| Mizar +| Set theory +| Phase 1 complete +| Mirrored +|=== -For finite-state programs with bounded execution, CNO verification is -decidable. +[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. +==== -# Applications +[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. +==== -## 1. Secure Sandboxing +== Known scope boundaries -Run untrusted code proven to be inert: `` `python `` `if` -`verify_cno(untrusted_program):` `allow_execution(untrusted_program)`\` +[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. +==== -## 2. Compiler Optimization +[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`. +==== -Detect and eliminate dead code: `` `c `` `x` `=` `x` `+` `1;` `x` `=` -`x` `-` `1;` \` +[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. +==== -## 3. Reversible Computing +== Repository Layout -CNOs establish baseline for zero-energy computation. +[cols="1,3", options="header"] +|=== +| Path | Purpose -## 4. Formal Methods Education +| `proofs/coq/` +| Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND -CNOs provide pedagogical examples for learning proof assistants. +| `proofs/lean4/` +| Lean 4 mirrors of CNO and OND modules -# Development +| `proofs/agda/`, `proofs/z3/`, `proofs/isabelle/`, `proofs/mizar/` +| Additional prover artefacts (Agda checked in CI; others generated but not yet run) -## Build Commands +| `proofs/ond/` +| OND Coq module (OND-1..5 proved, zero axioms) -```bash -just build-all # Build everything -just verify-all # Verify all proofs -just test-all # Run all tests -just clean # Clean build artifacts -just stats # Project statistics -``` +| `proofs/observation-models/` +| Declared observation models `O` (proof inputs for OND) -## Testing +| `proofs/residue/` +| OND residue lists (model-vs-metal gap) -```bash -# Python tests -python3 tests/unit/test_cno_properties.py +| `interpreters/` +| Malbolge (ReScript), Brainfuck (Python), Whitespace (Python) with CNO detection -# Interpreter tests -python3 interpreters/brainfuck/brainfuck.py -python3 interpreters/whitespace/whitespace.py +| `proofs/verify-all-provers.sh` +| One-shot gate: both pillars, all six provers + Idris ABI +|=== -# Proof verification -just verify-coq -just verify-z3 -``` +== Build -## CI/CD - -GitLab CI automatically: - Builds all proofs in multiple systems - Runs -interpreter tests - Verifies CNO properties - Deploys documentation - -# Documentation - -- **\[Theory\](docs/theory.md)**: Mathematical foundations - -- **\[Examples\](docs/examples.md)**: CNO examples across languages - -- **\[Proofs Guide\](docs/proofs-guide.md)**: How to write proofs - -- **\[Philosophy\](docs/philosophy.md)**: Epistemology of nothingness - -- **\[CLAUDE.md\](CLAUDE.md)**: AI assistant guide - -# License - -**SPDX-License-Identifier: CC-BY-SA-4.0** - -This project is licensed under the **Palimpsest-MPL License 1.0 or -later** (MPL-2.0). - -The Palimpsest-MPL extends Mozilla Public License 2.0 with provisions -for ethical use, post-quantum cryptographic provenance, and emotional -lineage protection. - -See \[LICENSE\](LICENSE) for full license text. - -**Fallback**: Where platform requirements mandate OSI-approved licenses, -MPL-2.0 may be used with appropriate documentation. - -# Citation - -If you use Absolute Zero in research, please cite: - -```bibtex -@misc{jewell2025absolute, - title={Absolute Zero: Formal Verification of Certified Null Operations}, - author={Jewell, Jonathan D. A.}, - year={2025}, - publisher={GitLab}, - howpublished={\url{https://gitlab.com/maa-framework/6-the-foundation/absolute-zero}}, - note={Coq and Z3 verification of computationally inert programs} -} -``` - -# Related Work - -- **CompCert**: Formally verified C compiler (Isabelle/HOL) - -- **seL4**: Formally verified microkernel - -- **Landauer, R. (1961)**: "Irreversibility and Heat Generation" - -- **Bennett, C. (1973)**: "Logical Reversibility of Computation" - -# Research Questions - -1. **Classification**: Can we classify all CNOs up to equivalence? - -2. **Complexity**: What is the computational complexity of CNO - verification? - -3. **Obfuscation**: What’s the most complex program provable as a CNO? - -4. **Language-Independence**: Do CNO properties hold across languages? - -5. **Quantum CNOs**: What does "null operation" mean for quantum - programs? - -# Contributing - -Contributions welcome! See \[CONTRIBUTING.md\](CONTRIBUTING.md). - -Areas of interest: - Proof engineering (porting to other assistants) - -PL theory (new CNO classifications) - Esoteric languages (more test -cases) - Applications (practical use cases) +[source,bash] +---- +# One-shot: both pillars, all provers +proofs/verify-all-provers.sh -# Contact +# Or via task runner +just verify -**Jonathan D. A. Jewell** - GitLab: -\[@hyperpolymath\]() - GitHub: -\[@Hyperpolymath\]() - Email: -[jonathan@metadatastician.art](jonathan@metadatastician.art) +# Individual provers +just build-coq +just verify-agda +---- -# Acknowledgments +== Documentation -- **Ben Olmstead**: Creator of Malbolge +* 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 +* `PROOF-STATUS.adoc` — per-prover verification status -- **Coq Development Team**: Excellent proof assistant +== License -- **Microsoft Research**: Z3 SMT solver +SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. -- **Proof Assistant Communities**: Lean, Agda, Isabelle, Mizar +Prose documentation is licensed under CC-BY-SA-4.0; see `LICENSES/`.==== ------------------------------------------------------------------------- +== Repository Layout -**Status**: Proofs verified ✓ \| Theorems established ✓ \| More work to -do ✓ +[cols="1,3", options="header"] +|=== +| Path | Purpose -**"Absolute Zero does nothing. But in doing nothing, it does -everything."** +| `proofs/coq/`