Slice 2: make chapeliser provably-real — CI machine-checks proofs/FFI/Chapel + honest status (#27)

Follow-on to base camp (#26, merged). Goal of this slice: move
chapeliser from
"asserted in prose" to **machine-verified**, and make the docs honest
about what
is and isn't checked today.

## Provable-real — `.github/workflows/provable.yml`

The Rust CLI/codegen is already green (63 tests via `rust-ci.yml`). This
adds a
new workflow that verifies everything *outside* Rust:

| Job | What it proves |
|---|---|
| `idris2-proofs` | `idris2 --check` type-checks `Types.idr`,
`Layout.idr`, `Foreign.idr` (the dependent-type ABI proofs) |
| `zig-ffi` | `zig build test` compiles + runs the Zig FFI reference
impl (Zig 0.14) |
| `codegen-drift` | regenerates the golden sample and `diff`s against
the committed tree (fails on drift) |
| `chapel-golden` | compiles **and runs** the generated Chapel via real
`chpl`, asserting 8/8 items conserved |

## Golden sample — `examples/golden/`

A minimal end-to-end fixture that closes the `STATE.a2ml` action
*"generate +
compile + run"*:
- `echo.toml` — deliberately `per-item`/`merge` so the generated Chapel
pulls in
**no** optional modules (no BlockDist/DynamicIters/AtomicObjects) →
small,
  stable compile surface.
- `generated/` — committed codegen output (reviewable + drift-checked).
- `ffi_stub.c` — ~60-line C echo implementation of the 12 `c_*`
functions so the
  Chapel can be linked and run without user code.

## Honest status — stop claiming what isn't checked yet

- **`ROADMAP.adoc`**: Phase 1 `(COMPLETE)` → `(IMPLEMENTED —
verification gated in CI)`; new **Phase 1b** tracks the four CI jobs
(each flips `[x]` only when green); dropped "compilable" from the bare
codegen bullet.
- **Test-count fix**: the old `15 tests (6 unit + 8 integration + 1
doc)` was wrong — actual is **63 (22 + 40 + 1)**.
- **`README.adoc`**: Idris2 *"Formal proofs that…"* → *"proof
obligations, machine-checked in CI"*; corrected source paths
(`src/interface/abi`, `src/interface/ffi`); honest pre-alpha Status
paragraph.
- **`STATE.a2ml`**: blockers / next-actions / maintenance now reflect
CI-gated verification (`last-result = warn` until `provable.yml` is
green).

## Why CI is the verifier (not local)

The idris2 / zig / chpl toolchains aren't installable in the dev sandbox
(`ziglang.org` and the GitHub releases API are network-blocked here;
building
idris2 from source is sandbox-restricted). So GitHub runners are the
verifier.
**Until `provable.yml` is green, these artifacts are "written", not
"verified"** —
and the docs now say exactly that. Kept as a **draft** for that reason:
driving
the four jobs to green is the acceptance gate, and a first run may
surface real
fixes (e.g. Idris2 `DecEq` totality, Chapel `Time`/reduce API specifics)
— that
iteration *is* the "make it real" work.

**Follow-up (not blocking):** pin action/image refs (`actions/checkout`,
`mlugg/setup-zig`, `chapel/chapel`, `idris2-pack`) to SHAs per estate
policy
once the tags are confirmed working.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ

---
_Generated by [Claude
Code](https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/provable.yml

@@ -0,0 +1,88 @@
+# SPDX-License-Identifier: MPL-2.0
+# Provable — machine-checks the claims Chapeliser makes outside the Rust layer.
+#
+# The Rust CLI/codegen is covered by rust-ci.yml. This workflow verifies the
+# four things that are otherwise only asserted in prose:
+#   1. idris2-proofs  — the Idris2 ABI proofs actually type-check (`idris2 --check`).
+#   2. zig-ffi        — the Zig FFI reference implementation builds and its tests pass.
+#   3. codegen-drift  — the committed golden sample matches fresh codegen output.
+#   4. chapel-golden  — the generated Chapel actually compiles AND runs via `chpl`.
+#
+# Until every job here is green, the proofs / FFI / Chapel output are "written"
+# but NOT "verified" — ROADMAP.adoc and README.adoc are worded accordingly.
+name: Provable
+
+on:
+  push:
+    branches: [main, master, "claude/**"]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  idris2-proofs:
+    name: Idris2 — machine-check ABI proofs
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: idris2 --check the ABI modules
+        working-directory: src/interface/abi
+        # Modules are namespaced Chapeliser.ABI.*, so they live under
+        # Chapeliser/ABI/ (idris2 requires file path to match module name).
+        # Foreign imports Types + Layout, so checking it checks the lot; we
+        # check each explicitly for clearer failure attribution.
+        run: |
+          idris2 --version
+          idris2 --check Chapeliser/ABI/Types.idr
+          idris2 --check Chapeliser/ABI/Layout.idr
+          idris2 --check Chapeliser/ABI/Foreign.idr
+
+  zig-ffi:
+    name: Zig — build + test FFI reference impl
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - uses: mlugg/setup-zig@v1 # SHA-pin pending (advisory Hypatia medium)
+        with:
+          version: 0.14.0
+      - name: zig build + test
+        working-directory: src/interface/ffi
+        run: |
+          zig version
+          zig build test
+          zig build
+
+  codegen-drift:
+    name: Codegen — golden sample is up to date
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: Regenerate golden artifacts and diff against committed tree
+        run: |
+          cargo run --quiet -- generate -m examples/golden/echo.toml -o /tmp/golden
+          diff -ru examples/golden/generated /tmp/golden
+
+  chapel-golden:
+    name: Chapel — compile + run golden sample
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container: docker://chapel/chapel:latest
+    steps:
+      - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+      - name: Compile generated Chapel against the echo FFI stub
+        run: |
+          chpl --version
+          chpl --main-module echo_Distributed \
+            examples/golden/generated/chapel/echo_distributed.chpl \
+            examples/golden/ffi_stub.c \
+            -o /tmp/echo_distributed
+      - name: Run on a single locale and assert it conserves all items
+        run: |
+          /tmp/echo_distributed -nl1 | tee /tmp/echo.out
+          grep -q "Gathered 8/8 results (merge)" /tmp/echo.out
+          grep -q "complete in" /tmp/echo.out

.machine_readable/6a2/STATE.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 project = "chapeliser"
 version = "0.1.0"
-last-updated = "2026-03-21"
+last-updated = "2026-06-18"
 status = "active"
 session = "converted from scheme — 2026-04-11"
 
@@ -15,7 +15,7 @@ purpose = """General-purpose Chapel acceleration framework"""
 completion-percentage = 45
 
 [position]
-phase = "phase-1-complete"   # design | implementation | testing | maintenance | archived
+phase = "testing"   # design | implementation | testing | maintenance | archived
 maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
@@ -25,16 +25,17 @@ milestones = [
 
 [blockers-and-issues]
 issues = [
-  "Chapel compiler not installed on dev machine — generated code verified by structure, not compilation",
+  "Idris2/Zig/Chapel toolchains unavailable in the local dev sandbox — proofs, FFI, and generated Chapel are now machine-checked in CI (.github/workflows/provable.yml) rather than locally.",
+  "provable.yml has not yet had a green run — until it does, the Idris2 proofs, Zig FFI build, and golden Chapel compile/run are written but not confirmed (ROADMAP Phase 1b).",
 ]
 
 [critical-next-actions]
 actions = [
-  "End-to-end test: generate + compile + run with panic-attacker workload",
-  "Add shell completions (bash, zsh, fish)",
-  "Write additional examples (Monte Carlo, image processing)",
+  "Drive .github/workflows/provable.yml to green (idris2-proofs, zig-ffi, codegen-drift, chapel-golden).",
+  "Add golden samples for the remaining partition/gather strategies and multi-locale runs.",
+  "Add shell completions (bash, zsh, fish).",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-03-21T00:00:00Z"
-last-result = "unknown"  # unknown | pass | warn | fail
+last-run-utc = "2026-06-18T00:00:00Z"
+last-result = "warn"  # unknown | pass | warn | fail — Rust layer green (63 tests); provable.yml pending first run

README.adoc

@@ -110,13 +110,15 @@ You write **zero Chapel code**. Chapeliser generates everything.
 
 Chapeliser follows the hyperpolymath ABI-FFI standard:
 
-* **Idris2 ABI** (`src/abi/`) — Formal proofs that:
-  - Data layouts are consistent across nodes
+* **Idris2 ABI** (`src/interface/abi/`) — Dependent-type *proof obligations*,
+  machine-checked in CI (`.github/workflows/provable.yml`); the Rust mirror in
+  `src/abi/` carries the matching runtime types and checks:
   - Partition functions produce complete, non-overlapping splits
   - Gather functions preserve all results
   - Serialization round-trips are identity
+  - Memory layouts are consistent across the FFI boundary
 
-* **Zig FFI** (`ffi/zig/`) — C-ABI bridge between:
+* **Zig FFI** (`src/interface/ffi/`) — C-ABI bridge between:
   - The user's application (any language with C FFI)
   - The Chapel runtime (`chpl_*` functions)
   - Memory management across the boundary
@@ -138,7 +140,7 @@ Chapeliser follows the hyperpolymath ABI-FFI standard:
 
 [source,bash]
 ----
-# Install
+# Install (once published to crates.io — see ROADMAP Phase 3)
 cargo install chapeliser
 
 # In your project directory, create chapeliser.toml (see above)
@@ -158,7 +160,10 @@ hundreds of repositories on a compute cluster.
 
 == Status
 
-**Pre-alpha.** Architecture defined, ABI proofs in progress, codegen planned.
+**Pre-alpha.** The Rust CLI and code generator are implemented and tested
+(63 tests). The Idris2 proofs, Zig FFI, and a golden Chapel compile-and-run are
+wired into CI as the verification gate (`.github/workflows/provable.yml`) — see
+`ROADMAP.adoc` Phase 1b for their live (green/red) status. Not yet released.
 
 == License
 

ROADMAP.adoc

@@ -12,8 +12,13 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 * [x] Example manifest (panic-attacker mass-panic)
 * [x] README with architecture, SECURITY, CONTRIBUTING, GOVERNANCE
 
-== Phase 1: Core Implementation (COMPLETE)
-* [x] Chapel code generator — produces compilable .chpl with real distribution logic
+== Phase 1: Core Implementation (IMPLEMENTED — machine-verification gated in CI)
+
+NOTE: "Implemented" = the code is written and the Rust layer is tested. The
+Idris2 proofs, Zig FFI, and generated Chapel are checked by `idris2`/`zig`/`chpl`
+only in CI (`.github/workflows/provable.yml`); their live status is Phase 1b.
+
+* [x] Chapel code generator — produces .chpl with real distribution logic
   ** Per-item: even coforall distribution with locale range helper
   ** Chunk: fixed-size chunks, round-robin across locales
   ** Adaptive: work-stealing via Chapel DynamicIters
@@ -31,28 +36,39 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 * [x] Zig FFI bridge generator — 12 Chapel-facing exports delegating to user code
 * [x] C header generator — full FFI contract with documentation
 * [x] Build script generator — env var overrides, Chapel config passthrough
-* [x] Idris2 ABI proofs (Types.idr, Layout.idr, Foreign.idr)
+* [x] Idris2 ABI proofs *written* (Types.idr, Layout.idr, Foreign.idr) — machine-checked in Phase 1b
   ** Partition completeness + disjointness
   ** Gather conservation
   ** Serialisation round-trip witness
   ** Retry isolation
   ** Memory layout proofs for item/result buffers
-* [x] Zig FFI reference implementation (echo processor, FNV-1a hash, concatenation reducer)
+* [x] Zig FFI reference implementation *written* (echo processor, FNV-1a hash, concatenation reducer) — compiled in Phase 1b
 * [x] Rust ABI types with runtime verification
   ** Partition, GatherResult, MemoryBudget, FfiResult
   ** Strategy enums with parsing
-  ** 6 unit tests
+  ** 22 unit tests
 * [x] Cluster config parsing (cluster.toml → GASNET/SSH env vars)
 * [x] Build command: release/debug mode passthrough
-* [x] 15 tests passing (6 unit + 8 integration + 1 doc-test)
+* [x] 63 tests passing in the Rust layer (22 unit + 40 integration + 1 doc-test)
+
+== Phase 1b: Machine-verification (gated in CI — `.github/workflows/provable.yml`)
+
+These convert the Phase 1 artifacts from "written" to "verified". Each item
+turns `[x]` only once its CI job is green; until then the Idris2/Zig/Chapel
+artifacts above are implemented but NOT yet machine-checked.
+
+* [ ] `idris2 --check` passes for Types.idr, Layout.idr, Foreign.idr (job: `idris2-proofs`)
+* [ ] `zig build test` passes for the FFI reference impl (job: `zig-ffi`)
+* [ ] Committed golden codegen output is drift-free (job: `codegen-drift`)
+* [ ] Generated Chapel compiles + runs via `chpl` — echo sample, 8/8 items conserved (job: `chapel-golden`)
 
 == Phase 2: Polish
 * [ ] Error messages and diagnostics (human-readable codegen errors)
 * [ ] Shell completions (bash, zsh, fish)
 * [ ] `chapeliser info` — show memory budget estimate from manifest
 * [ ] Performance benchmarks (single-locale vs multi-locale scaling)
-* [ ] Additional examples (Monte Carlo, image processing, text search)
-* [ ] CI/CD for the generated Chapel artifacts
+* [ ] Additional golden samples (other 4 partition × 5 gather strategies; multi-locale)
+* [~] CI/CD for the generated Chapel artifacts — wired in `provable.yml` (see Phase 1b)
 
 == Phase 3: Ecosystem
 * [ ] PanLL panel integration (distribution visualisation)

examples/golden/README.adoc

@@ -0,0 +1,62 @@
+// SPDX-License-Identifier: MPL-2.0
+= Golden sample — end-to-end verification fixture
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:icons: font
+
+This directory is the *provable-real* fixture for Chapeliser: the one workload
+that CI takes all the way from manifest to a running Chapel binary.
+
+== Why it exists
+
+Most of Chapeliser is exercised by Rust unit/integration tests. But the whole
+point of the tool — _generate Chapel, compile it, run it_ — can only be proven
+by actually invoking `chpl`. This fixture closes that loop in CI
+(`.github/workflows/provable.yml`, job `chapel-golden`).
+
+== Contents
+
+[cols="1,3"]
+|===
+| `echo.toml` | A deliberately minimal manifest: `per-item` partition,
+`merge` gather. These are the simplest strategies, so the generated Chapel
+pulls in *no* optional modules (no `BlockDist`, `DynamicIters`, or
+`AtomicObjects`) — keeping the compile surface small and stable.
+
+| `generated/` | The Chapel wrapper, Zig FFI bridge, C header and build script
+produced by `chapeliser generate -m echo.toml`. Committed so the output is
+reviewable and drift-checked. CI regenerates and `diff`s against this tree
+(job `codegen-drift`) — if they differ, the build fails.
+
+| `ffi_stub.c` | A ~60-line C implementation of the 12 `c_*` FFI functions for
+a trivial echo workload (8 items, copy input to output). Stands in for real
+user code so the generated Chapel can be linked and run.
+|===
+
+== Reproduce locally
+
+[source,bash]
+----
+# 1. (Re)generate — must match the committed generated/ tree:
+cargo run -- generate -m examples/golden/echo.toml -o examples/golden/generated
+
+# 2. Compile the generated Chapel against the echo FFI stub (needs chpl + cc):
+chpl --main-module echo_Distributed \
+  examples/golden/generated/chapel/echo_distributed.chpl \
+  examples/golden/ffi_stub.c \
+  -o /tmp/echo_distributed
+
+# 3. Run on a single locale — expect "Gathered 8/8 results (merge)":
+/tmp/echo_distributed -nl1
+----
+
+== What this proves
+
+* The Rust codegen emits Chapel that a real `chpl` accepts (not just
+  "structurally plausible" Chapel).
+* The C-ABI contract between the generated Chapel `extern proc` declarations
+  and the FFI layer links cleanly.
+* The per-item / merge distribution path runs to completion and conserves all
+  items (8 in, 8 gathered).
+
+It does *not* prove multi-locale (`-nl>1`) behaviour or the other four
+partition/gather strategies; those are future fixtures (see `ROADMAP.adoc`).

examples/golden/echo.toml

@@ -0,0 +1,29 @@
+# SPDX-License-Identifier: MPL-2.0
+# Golden sample — a trivial "echo" workload whose only purpose is to let CI
+# machine-verify the FULL Chapeliser pipeline end to end:
+#   codegen (Rust) -> Chapel compile (chpl) -> link FFI stub -> run.
+#
+# It deliberately uses the simplest strategies (per-item / merge) so the
+# generated Chapel exercises the core distribution path WITHOUT pulling in
+# optional modules (BlockDist, DynamicIters, AtomicObjects). Keeping the
+# compile surface minimal makes this a stable verification fixture.
+#
+# Verified by: .github/workflows/provable.yml (chapel-golden job).
+
+[workload]
+name = "echo"
+entry = "examples/golden/echo.rs::echo"
+partition = "per-item"
+gather = "merge"
+
+[data]
+input-type = "Vec<Bytes>"
+output-type = "Vec<Bytes>"
+serialization = "raw"
+max-item-bytes = 4096
+
+[scaling]
+min-nodes = 1
+max-nodes = 4
+grain-size = 1
+expected-items = 8