Skip to content

Commit 99a7781

Browse files
claudeclaude
committed
docs(wiki): seed in-repo wiki source under docs/wiki/
Per the user's chosen wiki strategy: build the wiki content in-repo where it gets PR review + git history, then sync to the GitHub Wiki via the recipe documented in docs/wiki/README.md. Pages: Home, Architecture, Proof-Systems, Verification, ABI, Roadmap, Contributing, Glossary, FAQ, Audit-Trail, _Sidebar Each page is short and cross-links to the authoritative root doc (ROADMAP.adoc, CONTRIBUTING.adoc, AUDIT.adoc, etc.) so the wiki stays in sync mechanically rather than by duplication. Includes a TODO for a `just wiki-sync` recipe + workflow to push docs/wiki/ to github.com/hyperpolymath/absolute-zero.wiki.git automatically.
1 parent 1ca4fa0 commit 99a7781

12 files changed

Lines changed: 716 additions & 0 deletions

‎docs/wiki/ABI.md‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# ABI
3+
4+
The Idris2 ABI surface at `src/abi/` declares the FFI boundary that the
5+
Zig shim (`ffi/zig/`) implements.
6+
7+
## Modules
8+
9+
| Module | Purpose |
10+
|--------|---------|
11+
| `AbsoluteZero.ABI.Types` | Core types: `Platform`, `Result`, `Instruction`, `ProgramState`, opaque handles |
12+
| `AbsoluteZero.ABI.Layout` | Memory layout proofs: field offsets, sizes, alignments per platform |
13+
| `AbsoluteZero.ABI.Foreign` | `%foreign` declarations + safe wrappers |
14+
| `AbsoluteZero.ABI.Proofs.DivMod` | Trusted div/mod lemma surface (estate-wide) |
15+
16+
## Building
17+
18+
```bash
19+
idris2 --build absolute-zero-abi.ipkg
20+
```
21+
22+
The package file at the repo root is `absolute-zero-abi.ipkg`.
23+
24+
## DivMod — the estate-wide div/mod lemma surface
25+
26+
`src/abi/Proofs/DivMod.idr` consolidates the trusted base of
27+
number-theoretic lemmas used by ABI alignment proofs across the
28+
hyperpolymath estate. Each axiom is individually named so discharge
29+
can be incremental:
30+
31+
```idris
32+
alignedSizeCorrect :
33+
(size : Nat) -> (align : Nat) ->
34+
{auto 0 nonZero : So (align /= 0)} ->
35+
So (alignedSize size align `mod` align == 0)
36+
37+
divModIdentity :
38+
(n : Nat) -> (d : Nat) ->
39+
{auto 0 nonZero : So (d /= 0)} ->
40+
n = (n `div` d) * d + (n `mod` d)
41+
42+
multModZero :
43+
(k : Nat) -> (d : Nat) ->
44+
{auto 0 nonZero : So (d /= 0)} ->
45+
So ((k * d) `mod` d == 0)
46+
47+
addModDistrib :
48+
(a : Nat) -> (b : Nat) -> (d : Nat) ->
49+
{auto 0 nonZero : So (d /= 0)} ->
50+
(a + b) `mod` d = ((a `mod` d) + (b `mod` d)) `mod` d
51+
```
52+
53+
All four currently route through `believe_me ()` — the Idris2 0.8.0
54+
canonical axiom idiom. Discharge path:
55+
* `divModIdentity` is provable from `Data.Nat.Division.DivisionTheorem` in idris2-contrib
56+
* `multModZero` follows by induction on `k`
57+
* `addModDistrib` is in `Data.Nat.Equational` territory
58+
* `alignedSizeCorrect` then chains them
59+
60+
Cross-estate: civic-connect's `src/Abi/Layout.idr` defers the same
61+
family (`alignUpDivides`, `mkFieldsAligned`, `offsetInBoundsPrf`).
62+
The intent is for those to migrate to import from
63+
`AbsoluteZero.ABI.Proofs.DivMod` rather than re-postulate per repo.
64+
65+
## History: the unsound `alignmentMatchesPlatformWord`
66+
67+
A previous postulate, `alignmentMatchesPlatformWord : HasAlignment t n -> So (n `mod` word == 0)`,
68+
was deleted as unsound on 2026-05-25 (ADR-009, issue #27). `HasAlignment t n`
69+
has only an information-free constructor `AlignProof`, so the universal
70+
claim could derive `So (1 mod 8 == 0)` ≡ `So False` from the file's own
71+
`CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1`. The
72+
single consumer (`programStateAlignmentValid`) is now discharged
73+
per-instance.
74+
75+
See [`AUDIT.adoc`](../../AUDIT.adoc) AUDIT-2026-05-20-#27 for the full
76+
write-up.
77+
78+
## Open AUDIT items
79+
80+
* **AUDIT-2026-05-20-A** — `src/abi/Types.idr` has 5 pre-existing
81+
errors blocking standalone typecheck under Idris2 0.8.0 (missing
82+
`Decidable.Equality` import; `%runElab` without `ElabReflection`;
83+
`MkStateHandle ptr` not supplying `nonNull` proof; `No absurd`
84+
lacks `Uninhabited` instances). Independent of #27.

‎docs/wiki/Architecture.md‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# Architecture
3+
4+
Three layers, loosely coupled.
5+
6+
## 1. Proof layer (`proofs/`)
7+
8+
The load-bearing verification. Six prover backends prove the same CNO
9+
properties from different angles:
10+
11+
| Prover | Strength | What we prove with it |
12+
|--------|----------|------------------------|
13+
| **Coq** | Constructive, mature | Core CNO theory, statistical mechanics (Landauer), category, lambda, quantum, filesystem |
14+
| **Lean 4** | Mathlib + tooling | Modern restatement, cross-validation |
15+
| **Z3** | Automated SMT | Decidable fragments — fast counterexample search |
16+
| **Agda** | Dependent types | Type-level CNO certificates |
17+
| **Isabelle/HOL** | Production-grade | Industrial-style verification |
18+
| **Mizar** | Mathematical library | Connection to standard maths corpus |
19+
20+
Multi-prover is intentional: each catches what the others miss. See
21+
[Proof Systems](Proof-Systems.md) for the choice rationale.
22+
23+
## 2. Interpreter + ABI layer (`src/`, `interpreters/`, `ffi/`)
24+
25+
* **`src/abi/`** — Idris2 type declarations for the C ABI, with formal
26+
alignment + size proofs. See [ABI](ABI.md).
27+
* **`interpreters/rescript/`** — Malbolge interpreter in ReScript with
28+
CNO detection. ReScript is the project's primary application
29+
language (per [`docs/CLAUDE.adoc`](../CLAUDE.adoc) language policy).
30+
* **`ffi/zig/`** — Zig FFI shim that the Idris2 ABI binds to.
31+
32+
## 3. Examples + tooling (`examples/`, `verification/`, `Justfile`)
33+
34+
* **`examples/<lang>/`** — CNOs in 23+ languages (ada, brainfuck, c,
35+
clojure, cobol, cpp, csharp, elixir, erlang, fortran, fsharp, haskell,
36+
javascript, lisp, malbolge, ocaml, php, prolog, rust, scala, scheme,
37+
special-ops, whitespace). Banned-language examples (go, java, kotlin,
38+
swift, ruby, perl) were removed 2026-05-25 per project policy.
39+
* **`verification/`** — top-level verify scripts (`verify-proofs.sh`,
40+
`setup-and-verify.sh`, `run-local-verification.sh`).
41+
* **`Justfile`** — recipes for everything; `just build-all`, `just verify`, etc.
42+
43+
## ECHIDNA integration (external)
44+
45+
ECHIDNA is the estate-wide neurosymbolic prover gateway, separate repo.
46+
absolute-zero calls into it via the `echidna-llm-mcp` BoJ cartridge —
47+
**never directly**. See [ECHIDNA.adoc](../../ECHIDNA.adoc).
48+
49+
```
50+
┌──────────────────────────┐ ┌──────────────────────────┐
51+
│ absolute-zero │ calls │ ECHIDNA (separate) │
52+
│ - proofs/ ├────────►│ - neural tactics │
53+
│ - src/ │ via BoJ │ - 105 prover backends │
54+
│ - interpreters/ │ │ - 66,674-proof corpus │
55+
└──────────────────────────┘ └──────────────────────────┘
56+
```
57+
58+
## Data flow on `just verify`
59+
60+
```
61+
verification/setup-and-verify.sh
62+
├── proofs/coq → coqc -R common CNO ...
63+
├── proofs/lean4 → lake build
64+
├── proofs/agda → agda CNO.agda
65+
├── proofs/isabelle → isabelle build
66+
├── proofs/z3 → z3 *.smt2
67+
├── src/abi → idris2 --build absolute-zero-abi.ipkg
68+
└── cargo build --release
69+
```
70+
71+
## Why this taxonomy
72+
73+
The directory layout follows the [RSR-template-repo](../RSR_OUTLINE.adoc)
74+
convention. Compliance state is tracked in [RSR_COMPLIANCE.adoc](../../RSR_COMPLIANCE.adoc).

‎docs/wiki/Audit-Trail.md‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# Audit Trail
3+
4+
Short summary; the authoritative ledger is [`AUDIT.adoc`](../../AUDIT.adoc).
5+
6+
## Resolved
7+
8+
| ID | Date | What | Where |
9+
|----|------|------|-------|
10+
| AUDIT-2026-05-20-#27 | 2026-05-25 | Unsound `alignmentMatchesPlatformWord` Idris2 postulate deleted; `alignedSizeCorrect` isolated into shared `Proofs/DivMod.idr` | PR #41, ADR-009 |
11+
| AUDIT-2026-05-20-#32 | 2026-05-20 | Deleted unsound `eval_respects_state_eq_{left,right}` axioms; observational reversibility (`=st=`) | PR #32, ADR-008 |
12+
| AUDIT-2026-05-20-#24 | 2026-05-20 | `eval_deterministic`: Axiom → Theorem via `step_deterministic_strong` | PR #24, ADR-007 |
13+
| AUDIT-2026-02-05 | 2026-02-05 | License canonicalisation to PMPL-1.0-or-later (79 files) | [archived](../archive/LICENSE-AUDIT-2026-02-05.adoc) |
14+
15+
## Open
16+
17+
| ID | Severity | What | Status |
18+
|----|---------|------|--------|
19+
| AUDIT-2026-05-20-A | Medium | `src/abi/Types.idr` has 5 pre-existing errors blocking Idris2 0.8.0 typecheck | Filed, needs separate PR |
20+
| AUDIT-2026-05-20-B | Low | `cflite_pr.yml` missing `actions/checkout` before fuzzer | Filed, needs separate PR |
21+
22+
## Axiom classification
23+
24+
The 73 Coq Axioms + 42 Parameters in `proofs/coq/` are model-layer
25+
assumptions:
26+
27+
* **Physics**: thermodynamic laws, Landauer bound, statistical mechanics
28+
* **Quantum**: Hilbert-space axioms, unitarity
29+
* **POSIX**: filesystem semantics
30+
* **Computational complexity**: standard model assumptions
31+
32+
These are *intentional* axiomatisations of the external world, not
33+
verification gaps for the CNO claim itself.
34+
35+
Tracked under [`hyperpolymath/standards`#133](https://github.com/hyperpolymath/standards/issues/133).
36+
37+
## Discharge mechanism
38+
39+
To turn an axiom into a theorem:
40+
41+
1. Identify the axiom in `proofs/<prover>/<file>.<ext>`
42+
2. Find or write a helper that lets you derive it from less-trusted
43+
axioms (ideally Prelude-only)
44+
3. Replace `Axiom name : ...` / `axiom name : ...` / `name = believe_me ()`
45+
with the proven theorem
46+
4. Add an ADR-NNN entry to `META.scm`
47+
5. Add an AUDIT-YYYY-MM-DD-#PR row to `AUDIT.adoc`
48+
49+
See ADR-007 (#24) for a worked example.
50+
51+
## Trust-escape inventory
52+
53+
Estate-wide cross-trust-escape sweeps are run periodically. Most recent:
54+
2026-05-20 (the sweep that surfaced #27). All findings either:
55+
* land in `AUDIT.adoc` if absolute-zero-local, or
56+
* land in [`hyperpolymath/standards`#133](https://github.com/hyperpolymath/standards/issues/133) for model-layer.

‎docs/wiki/Contributing.md‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# Contributing
3+
4+
Short summary; the authoritative version is [`CONTRIBUTING.adoc`](../../CONTRIBUTING.adoc) at the root.
5+
6+
## Language policy (hard rule)
7+
8+
Read [`docs/CLAUDE.adoc`](../CLAUDE.adoc) Language Policy section first.
9+
TL;DR:
10+
11+
* **Allowed**: ReScript, Deno, Rust, Tauri, Dioxus, Gleam, Bash, JavaScript
12+
(where ReScript cannot reach), Nickel, Guile Scheme, Julia, OCaml, Ada, Idris2
13+
* **Banned**: TypeScript, Node.js, npm/Bun/pnpm/yarn, Go, Python, Java/Kotlin,
14+
Swift, React Native, Flutter/Dart, Ruby, Perl
15+
16+
`.github/workflows/language-policy.yml` blocks new banned-language files at CI.
17+
18+
## Commit conventions
19+
20+
Conventional commits. Examples:
21+
22+
```
23+
proof(coq): discharge eval_deterministic via step_deterministic_strong
24+
proof(idris2/abi): port to Idris2 0.8.0 syntax (#27)
25+
chore(docs): reconcile and tidy root
26+
fix(licence): canonicalise to PMPL-1.0-or-later (#133)
27+
```
28+
29+
* Never amend published commits.
30+
* Hook bypass (`--no-verify`, `--no-gpg-sign`) only with explicit owner approval.
31+
32+
## Verify before pushing
33+
34+
```bash
35+
just verify # full suite
36+
just lint
37+
just fmt
38+
```
39+
40+
## ADR / Audit trail
41+
42+
* If your change is an **architectural decision** going forward, add an ADR
43+
entry to [`.machine_readable/META.scm`](../../.machine_readable/META.scm)
44+
(next ADR-NNN).
45+
* If your change **discharges a postulate / deletes unsound code**, add an
46+
AUDIT entry to [`AUDIT.adoc`](../../AUDIT.adoc).
47+
48+
## PR checklist
49+
50+
* [ ] SPDX-License-Identifier on all new files (`PMPL-1.0-or-later` unless reason otherwise)
51+
* [ ] No new banned-language files
52+
* [ ] Tests / proofs updated where relevant
53+
* [ ] If you touched workflows, all `uses:` references pinned to commit SHAs
54+
* [ ] If you added a new top-level dir, it's listed in
55+
[`RSR_COMPLIANCE.adoc`](../../RSR_COMPLIANCE.adoc)

‎docs/wiki/FAQ.md‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# FAQ
3+
4+
### Why prove that a program does nothing?
5+
6+
Because the universe of "no-op" candidates is huge and most of them
7+
aren't no-ops. A `for i in 1..1e9` loop that increments and decrements
8+
a counter looks like a no-op until you notice it heats the CPU. Formal
9+
verification draws the line: a program is a CNO iff a machine-checkable
10+
proof says so, in a model that captures the side-effects you care about
11+
(state, I/O, *and* entropy).
12+
13+
### Why six proof systems?
14+
15+
Each catches what the others miss. A property proved in Coq + Lean +
16+
Agda + Isabelle + Mizar + Z3 doesn't depend on any single backend's
17+
foundational quirks. When something is provable only in some, that
18+
tells you something about the foundational dependency. See
19+
[Proof Systems](Proof-Systems.md).
20+
21+
### Why is Idris2 here separately from `proofs/`?
22+
23+
`src/abi/` is the FFI surface, not a proof system in its own right —
24+
it carries formal alignment + size proofs for the C ABI used by the
25+
Zig shim. See [ABI](ABI.md).
26+
27+
### What's the difference between an Axiom and an Admitted?
28+
29+
* **Axiom** (Coq) / `axiom` (Lean) / `believe_me ()` (Idris2 0.8.0): an
30+
asserted proposition. Permanent unless discharged.
31+
* **Admitted** (Coq) / `sorry` (Lean) / `?hole` (Idris2): a placeholder
32+
in a proof, marking incomplete work. Should not ship.
33+
34+
absolute-zero core: **0 Admitted**, 73 Axioms + 42 Parameters, all
35+
owner-classified.
36+
37+
### Why is `examples/python` / `examples/go` / `examples/java` missing?
38+
39+
Deleted 2026-05-25 per the strict CLAUDE.md language policy. See
40+
[Contributing](Contributing.md). The CNO concept generalises across
41+
languages; the demonstrations now cover the 23 still-allowed ones.
42+
43+
### Where do I file issues?
44+
45+
`hyperpolymath/absolute-zero/issues`. For audit / trust-escape findings,
46+
use the existing [`AUDIT.adoc`](../../AUDIT.adoc) issue template; for
47+
proof discharges, the regular issue template + an ADR plan.
48+
49+
### How do I talk to ECHIDNA from a script?
50+
51+
Through the `echidna-llm-mcp` BoJ cartridge — never directly. See the
52+
ECHIDNA tool table in [`0-AI-MANIFEST.a2ml`](../../0-AI-MANIFEST.a2ml).
53+
54+
### Is the Coq proof complete?
55+
56+
Core theory: yes (11/11 files compile, 0 Admitted). Model-layer
57+
assumptions (Parameters about abstract physics, quantum, POSIX) are
58+
owner-classified — these are *intended* axiomatisations of the
59+
external world, not gaps in the verification of the computational claim.
60+
61+
### Where's the live state?
62+
63+
`.machine_readable/6a2/STATE.a2ml`. Updated on every meaningful change.
64+
65+
### Why "Absolute Zero"?
66+
67+
The thermodynamic analogy: at 0 K, a system has no entropy to release.
68+
A CNO is a program at "computational absolute zero" — it has no
69+
side-effect entropy to release into the world.

‎docs/wiki/Glossary.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# Glossary
3+
4+
| Term | Definition |
5+
|------|------------|
6+
| **CNO** | Certified Null Operation. A program that compiles + runs and is formally proven to have zero net computational effect — no state change, no I/O, no entropy. |
7+
| **Identity morphism** | In category theory, the morphism `id_X : X → X` that leaves `X` unchanged. CNOs are identity morphisms in the category of computational states (ADR-001). |
8+
| **Observational reversibility (`=st=`)** | The weakened reversibility property used after ADR-008. State equality modulo program-counter bookkeeping; PC is not observable, so two states with different PC but same observable content are `=st=`. |
9+
| **Landauer bound** | Lower thermodynamic cost of erasing one bit (`kT ln 2`). CNOs erase nothing, so any logically-reversible CNO can in principle be thermodynamically reversible too. Formalised in `StatMech.v` (axiom) + derived in `LandauerDerivation.v` (ADR-002). |
10+
| **Postulate / Axiom** | Asserted, unproven proposition. In Coq: `Axiom`. In Lean: `axiom`. In Idris2 0.8.0: `name = believe_me ()` (the `postulate` keyword was removed). Every estate-wide axiom is tracked in [`AUDIT.adoc`](../../AUDIT.adoc) or [`META.scm`](../../.machine_readable/META.scm). |
11+
| **HasAlignment t n** | Idris2 type asserting that type `t` has byte alignment `n`. The constructor `AlignProof` is information-free — the obligation sits on the producer to construct it only for the genuinely-correct `n`. |
12+
| **alignedSize** | `(size, align) ↦` smallest multiple of `align` that is ≥ `size`. Core ABI primitive; correctness proved (via `believe_me`, pending discharge) in `Proofs.DivMod`. |
13+
| **BoJ** | Brain of Jonathan — the estate's cross-repo automation cartridge layer. ECHIDNA invocations route through `echidna-llm-mcp` BoJ. |
14+
| **ECHIDNA** | Estate-wide neurosymbolic prover gateway. 105 prover backends, 66,674-proof corpus, ML tactic suggestion. Lives in a separate repo; called via BoJ. |
15+
| **PMPL-1.0** | Palimpsest-MPL 1.0. The project's licence. MPL-2.0 is the OSI-fallback. |
16+
| **RSR** | Rhodium Standard Repository — the estate-wide taxonomy convention defined by [`hyperpolymath/rsr-template-repo`](https://github.com/hyperpolymath/rsr-template-repo). Conformance tracked in [`RSR_COMPLIANCE.adoc`](../../RSR_COMPLIANCE.adoc). |
17+
| **ADR** | Architectural Decision Record. Forward-looking design choice. Recorded in [`META.scm`](../../.machine_readable/META.scm). |
18+
| **AUDIT-ID** | Backward-looking trust event (discharged axiom, deleted unsound code, license correction). Format `AUDIT-YYYY-MM-DD-<seq-or-PR>`. Recorded in [`AUDIT.adoc`](../../AUDIT.adoc). |
19+
| **6a2** | The `.a2ml` machine-readable format under `.machine_readable/6a2/`. Successor to the older `.scm` (Guile Scheme) format which is kept side-by-side during the migration window. |
20+
| **Trust escape** | An axiom or `believe_me` use that lets you bypass the type system. Hunted by the estate-wide cross-trust-escape sweep. |

0 commit comments

Comments
 (0)