docs(audits): FFI boundary §§9-11 (FLINT + Zig bridges + Zig overlay) — closes #177 (#186)

## Summary

Closes #177 (post-#104 panic-attack re-sweep — 6 new legitimate-FFI High
findings need audit + classification).

Extends `reports/audits/audit-ffi-boundary.md` with three new sections
and adds 6 matching entries to
`reports/audits/assail-classifications.a2ml`.

### `audits/audit-ffi-boundary.md`

- **§9 — `src/rust/coprocessor/flint.rs`** (UnsafeCode × 17): FLINT C
bigint library FFI (feature-gated `--features flint`). Documents the 4
unsafe-block patterns (RAII init/clear, string round-trip via
`fmpz_set_str`/`get_str` + `flint_free`, `fmpz_poly` arithmetic, integer
root/binomial), the `#[repr(C)]` layout invariants for `FmpzPolyStruct`,
and the blocking-thread-only ownership model.
- **§10 — Zig FFI bridges**:
- §10.1 `src/zig/ffi/axiom_spark_bridge.zig` (Ada/SPARK → Zig shim →
Rust `extern "C"` in `spark_axiom.rs`, §2)
- §10.2 `src/zig_ffi/chapel_bridge.zig` (Chapel C API → Zig `@cImport` →
Rust safe-call layer in `proof_search.rs`, §3)
- Documents the `@cImport` intent + enum-from-int bounds check +
owned-string-copy invariants.
- **§11 — `ffi/zig/src/` overlay** (UnsafeCode × 3): three identical
`echidna_<subsystem>_last_error()` functions in `boj.zig`,
`overlay.zig`, `typell.zig` that `@ptrCast` a module-static `error_buf
[N]u8` to `[*:0]const u8`. Documents the static-lifetime +
nul-terminator + null-fast-path + read-only contract invariants.

### `reports/audits/assail-classifications.a2ml`

Adds 6 classification entries cross-referencing §§9-11:
| File | Category | Audit ref |
|---|---|---|
| `src/rust/coprocessor/flint.rs` | UnsafeCode | §9 |
| `src/zig/ffi/axiom_spark_bridge.zig` | UnsafeFFI | §10.1 |
| `src/zig_ffi/chapel_bridge.zig` | UnsafeFFI | §10.2 |
| `ffi/zig/src/boj.zig` | UnsafeCode | §11 |
| `ffi/zig/src/overlay.zig` | UnsafeCode | §11 |
| `ffi/zig/src/typell.zig` | UnsafeCode | §11 |

Brings the total classification count from 16 → 22, covering all 6 new
High-tier FFI findings reported by `panic-attack` v2.5.0 on 2026-06-01.

## Out-of-scope observation (meander)

The panic-attack registry loader (`load_user_classifications` in
`panic-attack/src/assail/mod.rs:220`) reads from
`<project>/audits/assail-classifications.a2ml` or
`<project>/.panic-attack-classifications.a2ml`, but this repo keeps the
registry at `reports/audits/`. This means the registry entries (both
pre-existing and these new ones) do not currently flip findings to
`suppressed = true` in panic-attack output — the kanren
structural-suppression pass is what suppresses today. Out-of-scope for
this PR; can be addressed by either a one-line symlink (`audits →
reports/audits`) or moving the file. Filing separately if desired.

## Test plan

- [x] `audits/audit-ffi-boundary.md` §§9-11 follow the established §1-§8
format (header + boundary description + invariants list + classification
verdict).
- [x] All 6 new classification entries are syntactically consistent with
the existing 16 (s-expr form, `(file …)` + `(category …)` + `(audit …)`
+ `(rationale …)`).
- [x] GPG-signed commit (key `4A03639C…`).
- [ ] Auto-merge SQUASH armed post-CI.

🤖 Discovered + audited during the post-#104 panic-attack estate sweep
(2026-06-01). See
[hyperpolymath/panic-attack#32](hyperpolymath/panic-attack#32)
for campaign tracker.

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

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

Author: hyperpolymath

reports/audits/assail-classifications.a2ml

@@ -127,4 +127,49 @@ schema_version = "1.0.0"
     (audit "audits/audit-pa021-axioms-2026-05-26.md §2")
     (rationale "Conflicts is an abstract binary predicate parameter; caller supplies concrete proof of ¬ Conflicts when sets are disjoint. INTENTIONAL parameter, not proof debt. Inline justification at line 44-53."))
 
+  ; ─── src/rust/coprocessor/flint.rs — FLINT C bigint FFI ───────────────────
+  ; Feature-gated CAS backend (--features flint); 17 unsafe blocks across
+  ; RAII init/clear, string round-trip, and arithmetic ops on RAII-owned
+  ; fmpz / fmpz_poly objects. Documented in audit §9 (issue #177).
+  (classification
+    (file "src/rust/coprocessor/flint.rs")
+    (category "UnsafeCode")
+    (audit "audits/audit-ffi-boundary.md §9")
+    (rationale "FLINT C bigint library FFI (feature-gated --features flint); 17 unsafe blocks across RAII init/clear, fmpz string round-trip, and fmpz_poly arithmetic; all pointers are &mut self.inner to RAII-owned objects on the blocking thread, never aliased, never shared across threads"))
+
+  ; ─── src/zig/ffi/axiom_spark_bridge.zig — Zig shim over SPARK ─────────────
+  (classification
+    (file "src/zig/ffi/axiom_spark_bridge.zig")
+    (category "UnsafeFFI")
+    (audit "audits/audit-ffi-boundary.md §10.1")
+    (rationale "Zig C-ABI shim re-exporting SPARK axiom-policy symbols with predictable C ABI; @cImport({}) is the only construct flagged. SPARK contracts enforce output-pointer write-before-return; Rust side already audited in §2"))
+
+  ; ─── src/zig_ffi/chapel_bridge.zig — Zig bridge to Chapel runtime ─────────
+  (classification
+    (file "src/zig_ffi/chapel_bridge.zig")
+    (category "UnsafeFFI")
+    (audit "audits/audit-ffi-boundary.md §10.2")
+    (rationale "Type-safe Zig bridge between Chapel parallel-search runtime and Rust core (feature-gated chapel); @cImport pulls in chapel_ffi_exports.h. Enum-from-int is bounds-checked (line 156); strings copied into Zig-owned storage before Chapel call returns; Rust side already audited in §3"))
+
+  ; ─── ffi/zig/src/boj.zig — BoJ client last_error getter ───────────────────
+  (classification
+    (file "ffi/zig/src/boj.zig")
+    (category "UnsafeCode")
+    (audit "audits/audit-ffi-boundary.md §11")
+    (rationale "Single @ptrCast at line 456 in echidna_boj_last_error(): casts module-static error_buf [N]u8 to [*:0]const u8 with null-fast-path guard. Buffer is static (lifetime = program), nul-terminated by all writers, read-only contract. Identical pattern to overlay.zig and typell.zig"))
+
+  ; ─── ffi/zig/src/overlay.zig — Overlay subsystem last_error getter ───────
+  (classification
+    (file "ffi/zig/src/overlay.zig")
+    (category "UnsafeCode")
+    (audit "audits/audit-ffi-boundary.md §11")
+    (rationale "Single @ptrCast at line 684 in echidna_overlay_last_error(): identical pattern to boj.zig — module-static error_buf [N]u8 → [*:0]const u8 with null-fast-path guard. Single-threaded request-response model"))
+
+  ; ─── ffi/zig/src/typell.zig — TypeLL subsystem last_error getter ─────────
+  (classification
+    (file "ffi/zig/src/typell.zig")
+    (category "UnsafeCode")
+    (audit "audits/audit-ffi-boundary.md §11")
+    (rationale "Single @ptrCast at line 333 in echidna_typell_last_error(): identical pattern to boj.zig and overlay.zig — module-static error_buf [N]u8 → [*:0]const u8 with null-fast-path guard"))
+
 )

reports/audits/audit-ffi-boundary.md

@@ -131,3 +131,174 @@ This is structural overhead from the 105-prover architecture, not FFI or
 memory mismanagement.
 
 **Classification**: legitimate backend registry.  No remediation required.
+
+---
+
+## §9 — `src/rust/coprocessor/flint.rs` (UnsafeCode × 17) — FLINT C bigint bindings
+
+**Added**: 2026-06-01 (post-#104 panic-attack re-sweep, issue #177)
+
+FLINT (Fast Library for Number Theory, LGPL-3) is the only CAS backend in
+ECHIDNA that links the library in-process rather than shelling out (earning
+`CoprocessorTrustTier::LibraryWrapped`, Tier 3).  Feature-gated via
+`--features flint`; without it the module compiles out entirely and
+`CoprocessorFactory::native(CoprocessorKind::FlintMath)` returns `None`.
+
+The 17 `unsafe` blocks (lines 145, 158, 168, 172, 173, 180, 199, 204, 214,
+233, 251, 327, 335, 349, 356, 366, 376) fall into four well-bounded patterns:
+
+- **`fmpz_init` / `fmpz_clear` / `fmpz_poly_init` / `fmpz_poly_clear`**:
+  RAII bookkeeping — each `Fmpz` / `FmpzPoly` Rust wrapper owns exactly one
+  FLINT object; `Drop` runs `fmpz_clear` / `fmpz_poly_clear` exactly once.
+  Pointers passed are always `&mut self.inner`, never null, never aliased
+  (Rust's borrow checker prevents the latter).
+- **`fmpz_set_str` / `fmpz_get_str`**: string round-trip through CString /
+  CStr.  Inputs are validated CStrings (no interior nul); outputs are
+  immediately copied into owned `String` and the FLINT-allocated buffer is
+  released via `flint_free` (line 173) — no leak, no use-after-free.
+- **`fmpz_poly_*` arithmetic** (`gcd`, `mul`, `pseudo_rem`, `content`,
+  `set_coeff_fmpz`, `get_coeff_fmpz`, `length`): all called on `&mut`
+  pointers to RAII-owned `FmpzPolyStruct` instances created on the same
+  blocking thread, used, and dropped before the thread returns.
+- **`fmpz_root` / `fmpz_bin_uiui`**: integer k-th root and binomial.
+  Input bounds (`n`, `k` as `u64`) are validated by callers before the
+  FFI call; FLINT itself returns 0/1 status to indicate exact-vs-approximate
+  result (line 366: `exact = fmpz_root(...)`).
+
+**Thread safety**: FLINT is thread-safe from version 2.4 onwards provided
+each thread owns its `fmpz` / `fmpz_poly` instances exclusively.  All FLINT
+objects in this module are created on the blocking thread, used, and dropped
+before the thread returns — no sharing occurs (module docstring lines 38-43).
+
+**Type-layout invariants**: `FmpzPolyStruct` (`#[repr(C)]`, lines 75-80) is
+a faithful mirror of FLINT's `fmpz_poly_struct` on 64-bit Linux (3 pointer-
+sized fields, 24 bytes).  We never read or write the fields directly — all
+access goes through FLINT functions (lines 73-74 docstring).
+
+**Classification**: legitimate FFI (Rust→FLINT C library via in-process
+linkage, feature-gated).  No remediation required.
+
+---
+
+## §10 — Zig FFI bridges (`src/zig/ffi/axiom_spark_bridge.zig`, `src/zig_ffi/chapel_bridge.zig`) — UnsafeFFI × 2
+
+**Added**: 2026-06-01 (post-#104 panic-attack re-sweep, issue #177)
+
+Two Zig modules that bridge between two non-Rust backends (SPARK/Ada and
+Chapel) and the Rust FFI surface.  Each contains exactly one `@cImport`
+directive — the only construct panic-attack flags as `UnsafeFFI` for Zig.
+
+### §10.1 — `src/zig/ffi/axiom_spark_bridge.zig`
+
+Zig C-ABI shim over the SPARK axiom-policy layer, sitting between the
+Ada/SPARK static library (`libechidna_spark.a`) and the Rust FFI surface
+defined in `src/rust/ffi/spark_axiom.rs` (already audited in §2).
+
+```
+SPARK/Ada (axiom_policy.ads/.adb)
+  → C exports (axiom_c_bridge.ads/.adb: echidna_spark_enforce_policy_inner)
+  → this Zig shim (input validation + C-ABI re-export)
+  → Rust extern "C" (src/rust/ffi/spark_axiom.rs)
+```
+
+The `@cImport({})` (line 20) is intentionally empty — the shim's job is to
+re-export the SPARK symbols with predictable C ABI (no name mangling,
+predictable layout) and provide a compile-time `MAX_USAGES = 1024` size
+assertion that Rust's `bindgen` cannot see across the Ada boundary
+(module header, lines 4-17).
+
+Safety invariants:
+- `danger_levels: [*]const u8` + `count: usize` is the standard
+  pointer+length C slice; validated non-empty before crossing the Rust
+  boundary in `spark_axiom.rs` (see §2).
+- Output `policy_out` / `status_out` are `*i32` to caller-allocated
+  storage; the Ada side guarantees they are always written before the
+  call returns (SPARK contract).
+
+### §10.2 — `src/zig_ffi/chapel_bridge.zig`
+
+Type-safe Zig bridge between Chapel's parallel-search runtime and the
+Rust FFI surface, gated by the `chapel` Cargo feature (see §3).
+
+```
+Chapel (C API: chapel_ffi_exports.h)
+  → Zig (@cImport, this module)
+  → Rust (safe calls via src/rust/proof_search.rs)
+```
+
+The `@cImport({ @cInclude("chapel_ffi_exports.h"); })` (lines 18-20) pulls
+in the Chapel-exported C declarations for 30 prover backends.  The Zig
+wrappers (`ProverKind`, `ProverCategory`, `ProofResult`) translate
+Chapel's C types into Zig-safe enums and structs, owning all string copies
+(`fromChapel` at line 143 takes `std.mem.Allocator` and copies before
+returning).
+
+Safety invariants:
+- Enum-from-int boundaries are bounds-checked (line 156: `c_result.prover_id
+  >= 0 and c_result.prover_id < @as(c_int, ProverKind.count)` before
+  `@enumFromInt`).
+- All string references returned from Chapel are copied into Zig-owned
+  storage before the Chapel call returns (per module header line 7).
+- Chapel runtime guarantees null-terminated string lifetime until next
+  Chapel call (see §3 for the corresponding Rust-side contract).
+
+**Classification (both files)**: legitimate FFI (Zig bridge layer between
+Ada/SPARK & Chapel backends and Rust core; both feature-gated).  No
+remediation required.
+
+---
+
+## §11 — `ffi/zig/src/*` overlay layer (UnsafeCode × 3) — pointer casts on static error buffers
+
+**Added**: 2026-06-01 (post-#104 panic-attack re-sweep, issue #177)
+
+Three Zig modules in the `ffi/zig/src/` overlay (the Idris2-ABI → Zig-FFI →
+C-ABI surface for BoJ cartridges, the overlay subsystem, and the TypeLL
+type-language) each contain exactly one `@ptrCast` flagged by panic-attack
+as `UnsafeCode`.
+
+| File                         | Line | Function                              |
+|------------------------------|------|---------------------------------------|
+| `ffi/zig/src/boj.zig`        | 456  | `echidna_boj_last_error`              |
+| `ffi/zig/src/overlay.zig`    | 684  | `echidna_overlay_last_error`          |
+| `ffi/zig/src/typell.zig`     | 333  | `echidna_typell_last_error`           |
+
+All three are the **identical pattern**: a `last_error` getter that returns
+a C-ABI null-terminated string pointer to a module-private static error
+buffer:
+
+```zig
+pub export fn echidna_<subsystem>_last_error() ?[*:0]const u8 {
+    if (error_len == 0) return null;
+    return @ptrCast(&error_buf);
+}
+```
+
+Where `error_buf: [ERROR_BUF_SIZE]u8` (typically 512 bytes) is a
+module-private static array and `error_len: usize` is its current
+fill-length.
+
+Safety invariants:
+- `error_buf` is module-static — its address is fixed at program load and
+  never freed; the returned pointer is always valid for the program
+  lifetime.
+- The cast is from `*[N]u8` (array reference) to `[*:0]const u8`
+  (sentinel-terminated many-item pointer); the buffer is guaranteed to
+  contain a trailing nul because all writers (`setError` helpers in each
+  module) explicitly write a nul terminator before incrementing
+  `error_len`.
+- Return type is `?[*:0]const u8` (optional); a null-fast-path
+  (`if (error_len == 0) return null;`) guards against returning a pointer
+  to an empty buffer, so consumers can distinguish "no error" from
+  "empty-string error".
+- Read-only on the Rust/Idris2 side — the pointer is `const`; callers
+  must not write through it.
+
+**Concurrency note**: the static error buffer is not thread-safe; each
+subsystem's contract is that errors are read on the same thread that
+triggered them (consistent with the "BoJ client" / "overlay" / "TypeLL"
+single-threaded request-response model).  Multi-threaded callers must
+serialise error retrieval externally.
+
+**Classification**: legitimate FFI (idiomatic C-style `last_error` getters
+for three FFI subsystems sharing a common pattern).  No remediation required.