docs(abi): honest marker for generated/abi/ gap

generated/abi/ is reserved for an Idris2 -> C header pipeline that
does not exist yet. The Zig FFI at ffi/zig/src/main.zig is
hand-maintained in parallel with the Idris2 ABI; this commit makes
that fact legible rather than aspirational:

- generated/abi/README.adoc: RESERVED marker + gap analysis + plan.
- ffi/zig/src/main.zig: header comment no longer cites non-existent
  src/abi/Foreign.idr / src/abi/Types.idr; now names the actual
  .idr modules the FFI mirrors and points at generated/abi/README.adoc.

Closes the "ABI/header pipeline" Track B investigation. The pipeline
itself is deferred — it is a multi-session undertaking either as a
reflection-based Idris2 tool or a dedicated codegen plugin.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

ffi/zig/src/main.zig

@@ -1,7 +1,11 @@
 // TYPED_WASM FFI Implementation
 //
-// This module implements the C-compatible FFI declared in src/abi/Foreign.idr
-// All types and layouts must match the Idris2 ABI definitions.
+// This module is the C-compatible Zig FFI surface. Types and result codes
+// are hand-maintained in parallel with the Idris2 ABI spread across
+// src/abi/{Region,TypedAccess,Pointer,Effects,Lifetime,Linear,
+// MultiModule}.idr and src/abi/Layout/*.idr. There is no automated
+// Idris2 -> C header pipeline yet; see generated/abi/README.adoc for the
+// gap analysis and the plan for closing it.
 //
 // SPDX-License-Identifier: PMPL-1.0-or-later
 

generated/abi/README.adoc

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= generated/abi/ — Auto-generated C headers (reserved)
+
+:status: RESERVED — not yet populated
+:last-reviewed: 2026-04-18
+
+== Intent
+
+Per the hyperpolymath ABI/FFI standard (see `~/.claude/CLAUDE.md`):
+
+[cols="1,1,3"]
+|===
+| Layer | Language | Purpose
+
+| ABI | Idris2 | Interface definitions with formal proofs
+| FFI | Zig | C-compatible implementation
+| Headers | C (generated) | Bridge between ABI and FFI
+|===
+
+`generated/abi/` is the standard home for the C headers the Idris2 ABI
+should emit and the Zig FFI should consume. When the pipeline is live,
+`zig build` in `ffi/zig/` will depend on a fresh generation step that
+walks `src/abi/**/*.idr` and emits matching `.h` files here.
+
+== Current state (2026-04-18)
+
+**No pipeline exists yet.** The 21 Idris2 `.idr` modules in `src/abi/`
+define types, predicates, and theorems but do not emit C headers.
+`ffi/zig/src/main.zig` is hand-maintained in parallel with the Idris2
+definitions; the comment at `main.zig:3` citing `src/abi/Foreign.idr`
+and `src/abi/Types.idr` points at files that do not exist — the real
+ABI is spread across `Region.idr`, `TypedAccess.idr`, `Pointer.idr`,
+`Effects.idr`, `Lifetime.idr`, `Linear.idr`, `MultiModule.idr`, and
+the `Layout/*.idr` aggregate.
+
+== Why it is a gap worth closing
+
+Until the pipeline is live, every change to an Idris2 type must be
+manually mirrored in Zig. That divergence is the single most common
+source of FFI bugs in the estate — the hand-written Zig side drifts
+from the proven Idris2 side. A real generator would:
+
+. Walk each `src/abi/**/*.idr` module declaring foreign-visible types
+. Emit a matching `generated/abi/<Module>.h` with
+  `struct`/`enum`/`typedef` definitions
+. Be reproducible (byte-for-byte identical across runs)
+. Fail the Zig build when `generated/abi/` is stale relative to `src/abi/`
+
+== Why it is deferred
+
+Idris2's built-in C backend (`idris2 --cg rts`) produces implementation
+bodies rather than header surfaces. A real header generator would need
+either:
+
+* a small reflection-based tool that pattern-matches on top-level
+  `data` and `record` declarations and emits matching C, or
+* a dedicated Idris2 codegen plugin that targets `.h` output only.
+
+Both options are multi-session undertakings. The first is the lighter
+option and is the recommended starting point when the pipeline is next
+prioritised.
+
+== Tracking
+
+* `AI-WORK-todo.md` §2 Track B lists "ABI/header pipeline" as an open
+  item — it remains open as of this file's creation.
+* `PROOF-NEEDS.md` carries the verification-side story; the header
+  pipeline is the runtime/FFI counterpart.
+* Nothing currently imports from `generated/abi/`, so marking this
+  directory `RESERVED` does not break any build.