Skip to content

Commit 604c7b7

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
docs(ond): add Observational Null Operations as a co-equal second pillar
Design + documentation only — NO proofs are started (the OND obligations are specified for a dedicated proof effort and are all currently Admitted, mirroring CNO's open-obligation culture). OND (Certified Null *Disclosure*) is added as a co-equal sibling to CNO (Certified Null *Effect*): it certifies that an operation reveals nothing about its secret input relative to a declared observation model O. New docs: - docs/TWO-PILLARS.adoc — narrative spine: CNO = null effect, OND = null disclosure (relative to O); the coupling-dial frame (explicitly framing, not theorem); the CNO-vs-OND independence result with witnesses; and the model-vs-metal boundary as OND's honest edge (declared O = required input, residue list = required output = formal spec of the proof/reality gap). - docs/OND-ROADMAP.adoc — prioritised obligations OND-1..7 in the PROOF-CLASSIFICATION.adoc format (statement / prover(s) / honesty label / priority), with an explicit critique+reorder of the proposed ordering and a composition deep-dive. - docs/OND-PILLAR-STRUCTURE.adoc — directory/module layout mirroring CNO per prover, plus the two OND-specific artifact trees. New artifact trees (templates only — proof inputs/outputs, not proofs): - proofs/observation-models/ — declared observation models O. - proofs/residue/ — residue lists (the model-vs-metal gap). Updated: README.adoc (Two Pillars section, co-equal tagline, artifact dirs in structure diagram) and ROADMAP.adoc (Second Pillar: OND section). Key design decisions: - Independence is a first-class theorem (OND-3), not framing. - Composition does NOT close cleanly: a negative result (OND-5) plus a conditional positive (OND-6); naive union-composition is unsound (state-chaining + emergent boundary observables; the DP-budget / quasi-identifier shape). - Priority reorder vs the proposed (i)-(vi): trivial case up to #2 (satisfiability smoke-test); model-vs-metal discipline folded into the definition (#1) + per-claim template (#4) + ongoing register (#7); composition split into cheap-negative (#5, early) and hard-conditional (#6, last). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
1 parent 1b7d963 commit 604c7b7

9 files changed

Lines changed: 919 additions & 2 deletions

File tree

‎README.adoc‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
# Absolute Zero
44

5-
**Formal Verification of Certified Null Operations: When Doing Nothing Is Everything**
5+
**Formal Verification of Null Operations — two co-equal pillars: Certified Null _Effect_ (CNO) and Certified Null _Disclosure_ (OND)**
66

77
image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[MPL-2.0]
88
image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor,link="https://github.com/sponsors/hyperpolymath"]
@@ -29,6 +29,17 @@ This seemingly trivial question leads to deep insights in:
2929
- **Reversible Computing**: Programs preserving thermodynamic reversibility
3030
- **Esoteric Languages**: Using Malbolge as proof-of-concept
3131

32+
## The Two Pillars
33+
34+
Absolute Zero rests on **two co-equal pillars** — siblings of equal weight, not parent and extension:
35+
36+
- **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**.
37+
- **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**.
38+
39+
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.
40+
41+
See **`docs/TWO-PILLARS.adoc`** (narrative), **`docs/OND-ROADMAP.adoc`** (prioritised obligations), and **`docs/OND-PILLAR-STRUCTURE.adoc`** (module layout). The OND pillar is at the design/roadmap stage: its obligations are currently `Admitted` (specified, not yet proved) — the normal honest starting state, mirroring CNO's own open obligations.
42+
3243
## Project Structure
3344

3445
```
@@ -54,7 +65,10 @@ absolute-zero/
5465
│ ├── z3/ # Z3 SMT verification (automated)
5566
│ ├── agda/ # Agda proofs (dependent types)
5667
│ ├── isabelle/ # Isabelle/HOL (production-grade)
57-
│ └── mizar/ # Mizar proofs (mathematical library)
68+
│ ├── mizar/ # Mizar proofs (mathematical library)
69+
│ ├── observation-models/ # OND: declared observation models O (proof inputs)
70+
│ └── residue/ # OND: residue lists (the model-vs-metal gap)
71+
│ # Each prover dir hosts CNO.* and (to author) co-equal OND.* modules
5872
│
5973
├── interpreters/ # Language interpreters with CNO detection
6074
│ ├── rescript/ # Malbolge (ReScript)

‎ROADMAP.adoc‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,51 @@ This roadmap charts Absolute Zero's evolution from a research prototype (current
1717

1818
---
1919

20+
== The Second Pillar: Observational Null Operations (OND)
21+
22+
Absolute Zero is now a **two-pillar** project. Alongside **CNO** (Certified
23+
Null _Effect_ — "does nothing to the world"), the **OND** pillar (Certified
24+
Null _Disclosure_ — "reveals nothing about its secret input, relative to a
25+
declared observation model `O`") is added as a **co-equal sibling**, not an
26+
extension. The two are logically independent (a proved theorem, with
27+
witnesses) and connected by a *coupling-dial* frame (framing, not theorem).
28+
The honest edge of OND is the **model-vs-metal boundary**: every OND claim is
29+
*conditional* on its declared `O` and ships a **residue list** of out-of-scope
30+
observables.
31+
32+
**OND obligations** (prioritised; full detail in `docs/OND-ROADMAP.adoc`):
33+
34+
1. *OND-1* — the OND definition, formalised (parameterised by `O`, emitting a
35+
residue list). **Keystone.**
36+
2. *OND-2* — trivial-case satisfiability (skip is OND in any `O`) — the
37+
definition's smoke-test.
38+
3. *OND-3* — the CNO ⊥ OND **independence theorem** (the result that earns the
39+
two-pillar split).
40+
4. *OND-4* — a conditional-proof **template** for one real constant-time
41+
operation (+ its metal-discharge statement and residue list).
42+
5. *OND-5* — the **non-composition** counterexample (ONDs do *not* compose
43+
cleanly — state-chaining + emergent boundary observables; the DP-budget /
44+
quasi-identifier shape).
45+
6. *OND-6* — the **conditional composition** theorem (the heavily-qualified
46+
positive result; research-grade; last).
47+
7. *OND-7* — the ongoing **residue register** (the standing proof↔reality gap).
48+
49+
**Status**: design/roadmap stage. All OND obligations are currently `Admitted`
50+
(specified, not yet proved) — the normal honest starting state, mirroring
51+
CNO's own open obligations (see `docs/PROOF-CLASSIFICATION.adoc`). Authoring
52+
the OND proofs is deferred; this roadmap and `docs/OND-ROADMAP.adoc` /
53+
`docs/TWO-PILLARS.adoc` / `docs/OND-PILLAR-STRUCTURE.adoc` specify the work.
54+
55+
[NOTE]
56+
====
57+
The proof effort must investigate OND-5/OND-6 (composition) most carefully: if
58+
it concludes ONDs compose as cleanly as CNOs, that conclusion is almost
59+
certainly wrong (it has dropped either the state-chaining or the
60+
boundary-observable term) and must be re-checked.
61+
====
62+
63+
---
64+
2065
== Current State (v1.0.0-alpha, 50%)
2166

2267
=== Completed ✅

‎docs/OND-PILLAR-STRUCTURE.adoc‎

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= OND Pillar Structure: Directory and Module Layout
4+
:toc:
5+
:sectnums:
6+
7+
[abstract]
8+
This document specifies the directory and module layout for the *Observational
9+
Null Operations (OND)* pillar. It mirrors the existing CNO multi-prover layout
10+
as closely as the conceptual differences allow, and adds the two OND-specific
11+
artifacts CNO does not need: *declared observation models* and *residue lists*.
12+
*No proof files are created by this design* — the per-prover OND modules below
13+
are specified for a dedicated proof effort to author (see `OND-ROADMAP.adoc`).
14+
The OND-specific *artifact* directories and their templates *are* created, since
15+
they are documentation inputs/outputs, not proofs.
16+
17+
== Co-equality principle
18+
19+
OND modules are *siblings* of the CNO modules, not children. Wherever CNO has
20+
`CNO.<ext>` in a prover directory, OND has `OND.<ext>` *alongside* it in the
21+
same directory — same prover, same build, same composition-theorem discipline,
22+
same decidable-for-bounded-programs caveat. Neither pillar is nested under the
23+
other. The only structural *addition* for OND is the pair of artifact trees
24+
(`proofs/observation-models/`, `proofs/residue/`), because an OND claim has two
25+
extra parts — a declared `O` (input) and a residue list (output) — that have no
26+
CNO analogue.
27+
28+
== Per-prover module layout (mirrors CNO — TO BE AUTHORED)
29+
30+
Each OND module sits beside its CNO counterpart. These files are *specified
31+
here, to be created by the proof effort* — they are not created by this design.
32+
33+
[cols="1,2,2,3",options="header"]
34+
|===
35+
| Prover | CNO (exists) | OND (to author) | Obligations (see OND-ROADMAP)
36+
37+
| *Coq*
38+
| `proofs/coq/common/CNO.v`
39+
| `proofs/coq/observational/OND.v`
40+
| OND-1 definition
41+
| *Coq*
42+
| `proofs/coq/category/CNOCategory.v`
43+
| `proofs/coq/observational/ONDIndependence.v`
44+
| OND-3 independence (needs `is_CNO` + `is_OND`)
45+
| *Coq*
46+
| `proofs/coq/lambda/LambdaCNO.v`
47+
| `proofs/coq/observational/ONDComposition.v`
48+
| OND-5 non-composition, OND-6 conditional composition
49+
50+
| *Lean 4*
51+
| `proofs/lean4/CNO.lean`
52+
| `proofs/lean4/OND.lean`
53+
| OND-1, OND-2
54+
| *Lean 4*
55+
| `proofs/lean4/CNOCategory.lean`
56+
| `proofs/lean4/ONDIndependence.lean`
57+
| OND-3
58+
| *Lean 4*
59+
| `proofs/lean4/LambdaCNO.lean`
60+
| `proofs/lean4/ONDComposition.lean`
61+
| OND-5, OND-6
62+
63+
| *Agda*
64+
| `proofs/agda/CNO.agda`
65+
| `proofs/agda/OND.agda`
66+
| OND-1 (dependent-typed presentation)
67+
68+
| *Z3*
69+
| `proofs/z3/verify.sh`
70+
| `proofs/z3/ond_verify.sh`
71+
| OND-2, OND-3, OND-4, OND-5 (bounded/finite instances)
72+
73+
| *Isabelle/HOL*
74+
| `proofs/isabelle/CNO.thy`
75+
| `proofs/isabelle/OND.thy`
76+
| OND-6 (heavier metatheory)
77+
78+
| *Mizar*
79+
| `proofs/mizar/CNO.miz`
80+
| `proofs/mizar/OND.miz`
81+
| OND-1, OND-3 (mathematical-library presentation)
82+
|===
83+
84+
[NOTE]
85+
====
86+
The Coq tree introduces one new subdirectory, `proofs/coq/observational/`,
87+
parallel to the existing `common/`, `category/`, `lambda/`, `physics/`,
88+
`quantum/`, `filesystem/`, `malbolge/`. This keeps the OND Coq modules grouped
89+
without nesting them under CNO. Lean 4, Agda, Isabelle, and Mizar keep their
90+
flat per-file layout, so OND files sit directly beside the CNO files.
91+
====
92+
93+
== OND-specific artifact trees (CREATED by this design)
94+
95+
These two directories *are* created now, with `README.adoc` and a `TEMPLATE`,
96+
because they hold documentation artifacts (proof inputs/outputs), not proofs.
97+
98+
[source]
99+
----
100+
proofs/
101+
├── observation-models/ # declared observation models O (proof INPUTS)
102+
│ ├── README.adoc # what an observation model is + how to declare one
103+
│ └── TEMPLATE.adoc # copy-per-claim skeleton for a declared O
104+
└── residue/ # residue lists (proof OUTPUTS / the metal gap)
105+
├── README.adoc # what a residue list is + the discipline
106+
└── TEMPLATE.adoc # copy-per-claim skeleton for a residue list
107+
----
108+
109+
* *`proofs/observation-models/`* — one declared `O` per OND claim (or per
110+
platform/operation family). A declared `O` is the *required input* to every
111+
OND proof: the explicit, enumerated list of what the observer is assumed to
112+
see (e.g. wall-clock time, output length, allocation-size sequence, branch
113+
pattern). The proof's *consequent* ("constant over the secret") is proved
114+
relative to this `O`.
115+
116+
* *`proofs/residue/`* — one residue list per OND claim: the observables
117+
*deliberately out of scope* of that claim's `O` (e.g. power analysis,
118+
speculative-execution channels, DRAM row-buffer timing, EM emanation). The
119+
residue list is the *formal specification of the gap between the proof and
120+
physical reality* — the standing record (OND-7) an engineer reads to learn
121+
which channels they still own.
122+
123+
== Where each roadmap obligation lives
124+
125+
[cols="1,3",options="header"]
126+
|===
127+
| Obligation | Home
128+
129+
| OND-1 definition | `proofs/{coq/observational,lean4,agda,mizar}/OND*` + the
130+
`O` parameterisation pattern documented in `observation-models/README.adoc`
131+
| OND-2 trivial case | `proofs/lean4/OND.lean`, `proofs/coq/observational/OND.v`,
132+
`proofs/z3/ond_verify.sh`
133+
| OND-3 independence | `proofs/{coq/observational,lean4}/ONDIndependence.*`,
134+
witnesses checked in `proofs/z3/ond_verify.sh`
135+
| OND-4 conditional template | `proofs/{coq/observational,lean4}/OND*` for the
136+
conditional, with a declared `O` in `observation-models/` and a residue list
137+
in `residue/`
138+
| OND-5 non-composition | `proofs/{coq/observational,lean4}/ONDComposition.*`,
139+
joint-observable check in `proofs/z3/ond_verify.sh`
140+
| OND-6 conditional composition | `proofs/{coq/observational,lean4}/ONDComposition.*`,
141+
`proofs/isabelle/OND.thy`
142+
| OND-7 residue register | `proofs/residue/` (ongoing)
143+
|===
144+
145+
== Documentation and governance touch-points
146+
147+
* `docs/TWO-PILLARS.adoc` — the narrative spine (CNO + OND co-equal).
148+
* `docs/OND-ROADMAP.adoc` — the prioritised obligations.
149+
* `docs/PROOF-CLASSIFICATION.adoc` — the CNO honesty template OND mirrors; when
150+
OND proofs begin, add an OND section (or a sibling `OND-CLASSIFICATION.adoc`)
151+
using the same per-obligation format.
152+
* `README.adoc` — presents the two pillars co-equally (see its "Two Pillars"
153+
section).
154+
* `proofs/<prover>/README.adoc` — when OND modules land, list them beside the
155+
CNO modules so the co-equality is visible in each prover directory.
156+
157+
== Build and CI
158+
159+
OND modules join the *same* build as CNO in each prover (no separate
160+
toolchain): the Lean `lakefile`/`lake-manifest`, the Coq `_CoqProject`, the
161+
Agda/Isabelle/Mizar invocations, and `proofs/z3/ond_verify.sh` beside
162+
`verify.sh`. When the OND modules are authored, register them in the existing
163+
per-prover build manifests so `just`/CI cover both pillars identically.
164+
165+
[IMPORTANT]
166+
====
167+
This document creates *only* the two artifact trees (`observation-models/`,
168+
`residue/`) with their READMEs and templates. The per-prover `OND*` proof
169+
modules above are *specified, not created* — authoring them is the proof effort
170+
described in `OND-ROADMAP.adoc`, explicitly deferred.
171+
====

0 commit comments

Comments
 (0)