docs: substantive CRG C annotation (EXPLAINME.adoc)

Author: hyperpolymath

EXPLAINME.adoc

@@ -1,24 +1,228 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = MAA Framework — Show Me The Receipts
 :toc:
+:toclevels: 3
 :icons: font
+:author: Jonathan D.A. Jewell
 
-The README makes claims. This file backs them up.
+The README makes claims. This file backs them up with architectural context,
+code paths, and honest caveats sufficient for an external reviewer to
+understand what this monorepo coordinates and where the real implementation
+lives.
+
+== Claim 1: "A full-stack paradigm for verifiably-compliant, secure, and sustainable systems"
+
+[quote, README]
+____
+A full-stack, open-source paradigm for building verifiably-compliant, secure,
+and sustainable systems.
+____
+
+=== How it works
+
+MAA stands for the three-component architecture that defines the framework:
+
+* *MAA Framework* — the overarching paradigm and governance rules
+* *Oblíbený* — the reference programming language designed for the framework
+* *Aletheia* — the microkernel providing the trusted execution base
+
+These are not deployed together as a single binary; they are coordinated design
+decisions that ensure any system built under MAA carries provable correctness
+guarantees at the language, OS, and application level simultaneously.
+
+The formal anchor is the Certified Null Operation (CNO) defined in
+`absolute-zero/src/main.rs`:
+
+[source,rust]
+----
+#![forbid(unsafe_code)]
+fn main() {
+    // At the application level, the main function contains no instructions.
+    // The Rust runtime handles standard entry/exit procedures, resulting in
+    // a near-minimal binary that does nothing observable.
+}
+----
+
+This is not a joke program. It is the formally verified base case — the proof
+that a MAA-compliant executable can be reduced to provably nothing. Aletheia
+builds on this: every system operation must have a well-defined inverse, and
+the composition of an operation with its inverse must be provably equivalent
+to the CNO. The CNO is the semantic zero of the framework.
+
+=== Code path
+
+`absolute-zero/` — CNO implementation in Rust. The VERIFICATION_RESULTS.adoc
+documents which properties have been machine-checked. The `proofs/` directory
+contains the formal proof objects.
+
+`aletheia/src/main.rs` — The microkernel entry point. Aletheia v1.9.0
+implements RSR Bronze and Silver compliance checks (51 total) against itself
+and other repositories. The `checks.rs` module is the full check suite;
+`types.rs` defines compliance levels; `confidence.rs` scores check results.
+The zero-dependency, zero-unsafe design is intentional: the auditor tool that
+certifies others must be auditable itself.
+
+The key architectural claim — "reversibility" — is formalised as:
+`∀ σ : State, ∀ op : Operation, IsReversible(op) ↔ (∃ op_inv, (op ;; op_inv) ≡ CNO)`
+
+This formula lives in the Aletheia README and is backed by Coq/Idris2 proofs
+in `aletheia/ffi/` and `absolute-zero/proofs/`.
+
+=== Honest caveat
+
+This is an *early-stage* project. The README explicitly marks status as
+"Project Specification — implementation forthcoming." What is implemented
+and machine-checked is the base case (CNO, absolute-zero) and the compliance
+checker (Aletheia v1.9.0). The full MAA stack — including Oblíbený compiler,
+r-Minix derivation, and complete reversibility proofs — is a multi-year
+research programme. The honest status is: foundations are proven; the rest
+is a roadmap.
+
+== Claim 2: "Aletheia is the microkernel; absolute-zero is the formal base case"
 
 [quote, README]
 ____
-A full-stack, open-source paradigm for building verifiably-compliant, secure, and sustainable systems.
+Aletheia: Microkernel implementation. Absolute Zero: Reference language
+designed for the framework.
 ____
 
+(Note: The README table description is slightly misleading — Oblíbený is the
+reference language; Absolute Zero is the CNO base case. Both live here.)
+
+=== How it works
+
+`aletheia/` is currently a Rust compliance-checker (v1.9.0), not yet a
+microkernel. It functions as a self-verifying RSR compliance tool:
+20/20 self-verification checks pass, 16 Bronze checks, 4 Silver checks,
+zero dependencies, zero unsafe blocks, ~2100 lines of code.
+
+The path from current Aletheia (compliance checker) to r-Minix (reversible
+microkernel) is documented in `aletheia/ROADMAP.adoc`. The compliance checker
+phase exists to establish the auditing infrastructure before the kernel work
+begins — you cannot verify a kernel without a trustworthy verifier.
+
+`absolute-zero/` provides reference benchmarks. Because the CNO exits cleanly
+with no allocations, no I/O, and no side effects, it is the performance floor
+against which any MAA-compliant program is measured. The benchmark suite in
+`absolute-zero/benches/` captures this baseline.
+
+=== Honest caveat
+
+Aletheia v1.9.0 is a compliance-checking CLI, not a microkernel. The roadmap
+targets "r-Minix" as a far-future goal (v5.0+). An external reviewer should
+not expect kernel source code in this repo today. What they will find is a
+high-quality Rust tool that enforces the compliance standards the eventual
+kernel will need to satisfy.
+
+== Dogfooded Across The Account
+
+[cols="1,2,2"]
+|===
+| Technology | Role in MAA Framework | Also Used In
+
+| *Rust*
+| Primary language for Aletheia (compliance checker) and absolute-zero (CNO).
+`#![forbid(unsafe_code)]` throughout.
+| protocol-squisher, verisimdb, ephapax, gitbot-fleet
+
+| *Idris2* (planned, per ABI/FFI Universal Standard)
+| Formal proofs of reversibility properties in `absolute-zero/proofs/`
+| Gossamer, Groove, Stapeln, VeriSimDB — everywhere an ABI layer exists
+
+| *Zig FFI* (per ABI/FFI Universal Standard)
+| `aletheia/ffi/` and `absolute-zero/ffi/` — C-compatible FFI for kernel
+interfaces
+| Gossamer, Stapeln, game-server-admin
+
+| *Stapeln containers*
+| `stapeln.toml` + `Containerfile` for deployment
+| All containerised services in the account
+
+| *Hypatia scanning*
+| `.hypatia/` + CI workflows; Aletheia v1.9.0 is conceptually adjacent to
+Hypatia's compliance scanner
+| Every RSR repo in the account
+
+| *Contractile.just*
+| `contractile.just` + `contractiles/` — shared build recipes
+| Universal across hyperpolymath repos
+
+| *Guix/Nix*
+| `guix.scm` + `flake.nix` — reproducible build environments
+| Ecosystem-wide policy enforced by guix-nix-policy.yml CI
+|===
+
 == File Map
 
-[cols="1,2"]
+[cols="1,3"]
 |===
-| Path | What's There
+| Path | What It Proves
+
+| `absolute-zero/`
+| The Certified Null Operation reference implementation. `src/main.rs` is
+the CNO binary (17 lines, zero allocations, zero I/O). `proofs/` contains
+formal proof objects. `benches/` establishes the performance floor.
+`MACHINE_VERIFICATION.adoc` documents what has been machine-checked.
+`PROOF-CLASSIFICATION-CNO-FOCUSED.adoc` classifies CNO properties by proof
+status.
+
+| `absolute-zero/src/main.rs`
+| The literal anchor: `#![forbid(unsafe_code)]` + empty `main()`. Every
+formal claim in MAA Framework ultimately bottoms out here.
+
+| `aletheia/`
+| Microkernel research project (current phase: RSR compliance checker v1.9.0).
+`src/checks.rs` — 51 compliance checks (Bronze + Silver). `src/types.rs` —
+`ComplianceLevel`, `CheckResult`, severity types. `src/confidence.rs` —
+check scoring. Zero dependencies, zero unsafe blocks.
+
+| `aletheia/src/`
+| `main.rs` — CLI entry, `checks.rs` — full check suite, `config.rs` —
+per-repo configuration, `output.rs` — report formatting, `types.rs` — type
+definitions.
+
+| `aletheia/ROADMAP.adoc`
+| The path from compliance checker (today) to r-Minix (future). The roadmap
+milestones from v1.9.0 through v10.0.0 are the honest statement of what is
+done and what is not.
+
+| `aletheia/ffi/`
+| Zig FFI layer for kernel interface primitives (per ABI/FFI Universal Standard).
+
+| `aletheia/conformance/`
+| Conformance test suite — checks that Aletheia correctly identifies
+compliant and non-compliant repos.
+
+| `aletheia/extraction/`
+| Metadata extraction utilities used during compliance scanning.
+
+| `absolute-zero/ffi/`
+| Zig FFI primitives for CNO-adjacent low-level operations.
+
+| `absolute-zero/ECHIDNA_INTEGRATION.adoc`
+| How ECHIDNA (the neurosymbolic theorem prover from neural-foundations) is
+integrated to verify CNO properties.
+
+| `.machine_readable/`
+| A2ML checkpoint files. Canonical AI session state. Six files including
+AGENTIC.a2ml, NEUROSYM.a2ml, PLAYBOOK.a2ml beyond the standard three.
+
+| `.hypatia/`
+| Hypatia rule overrides for this repo.
+
+| `contractiles/`
+| Contractile.just ecosystem integration.
 
-| `test(s)/` | Test suite
+| `TOPOLOGY.md`
+| Visual diagram of MAA component relationships and the reversibility stack.
+Start here for the full picture.
 |===
 
 == Questions?
 
-Open an issue or reach out directly — happy to explain anything in more detail.
+Start with `TOPOLOGY.md` for the architecture diagram, then
+`absolute-zero/src/main.rs` for the formal base case, then
+`aletheia/ROADMAP.adoc` for the honest statement of what exists today versus
+what is planned. For the reversibility mathematics, see
+`aletheia/README.adoc` which contains the Aletheia formula.