<!--
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
# Verification

How to verify locally and what CI does.

## Local

The `verification/` directory contains the top-level scripts.

```bash
# One-shot: install deps + run full verification
./verification/setup-and-verify.sh

# After deps are installed
./verification/run-local-verification.sh

# Just the proof suite
./verification/verify-proofs.sh
```

Or via `Justfile` recipes (more granular):

```bash
just build-all        # Agda + Idris 2 ABI (the active stack)
just build-agda
just build-idris
just verify           # proofs/verify-active-provers.sh → ACTIVE-PROVERS-GREEN
```

The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under
`archive/proofs/` and have no build recipes; the commands below for them are
historical and run against the archived trees.

## Per-prover commands

### Coq (archived)
```bash
cd archive/proofs/coq/common && coqc CNO.v
cd ../physics && coqc -R ../common CNO StatMech.v
                 coqc -R ../common CNO LandauerDerivation.v
cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v
cd ../malbolge && coqc -R ../common CNO MalbolgeCore.v
```

### Lean 4 (archived)
```bash
cd archive/proofs/lean4 && lake build
```

### Agda
```bash
cd proofs/agda && agda CNO.agda
```

### Idris2 ABI
```bash
idris2 --build absolute-zero-abi.ipkg
```

(Standalone DivMod check, useful for the issue #27 surface:)
```bash
idris2 --check src/abi/Proofs/DivMod.idr
```

## CI matrix

| Workflow | What it does | Status check name |
|----------|--------------|--------------------|
| `rust-ci.yml` | `cargo build --release`, `cargo audit`, coverage | `build`, `security`, `coverage` |
| `affinescript-deno-ci.yml` | `deno lint`, `deno fmt --check`, `deno test`, `affinescript build` | `build` |
| `codeql.yml` | CodeQL static analysis | `check` |
| `secret-scanner.yml` | trufflehog + gitleaks | `secrets` |
| `language-policy.yml` | Block new banned-language files | `check` |
| `governance.yml` | Estate-wide reusable governance bundle | `governance / *` |
| `hypatia-scan.yml` | Neurosymbolic CI/CD scan | (comment-only) |
| `cflite_pr.yml` | ClusterFuzzLite (address sanitizer) | `PR (address)` |
| `scorecard.yml` | OpenSSF Scorecard | (badge) |
| `jekyll-gh-pages.yml` | Deploy homepage | (deploy) |
| `publish-container.yml` | Build + push container image | (release) |

## Reproducible container

`Containerfile` at root pins toolchain versions. Build:

```bash
podman build -t absolute-zero:verify -f Containerfile .
podman run --rm absolute-zero:verify just verify
```

(Or `docker` in place of `podman`.)

## Status as of 2026-07-06 (PR #100)

See [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml)
and [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) for live status. Summary: both
pillars verified across **six provers + Idris** — Coq 14/14, Lean+Mathlib green,
Agda (CNO+OND), Z3, Isabelle (`AbsoluteZero-CNO`), Mizar (`CNO.miz` empty `.err`),
Idris ABI builds clean. One-shot then: `proofs/verify-all-provers.sh` (now archived as
`archive/proofs/verify-all-provers.six-prover.sh`) → `ALL-PROVERS-GREEN`.

Since the 2026-10-10 archive ruling only Agda, Z3 (bounded) and the Idris 2 ABI
are active: run `proofs/verify-active-provers.sh` → `ACTIVE-PROVERS-GREEN`.