feat(ffi): contract-test the idris2↔zig token-buffer ABI (seams) (#334)

## Seam-contract tests for the idris2↔zig token buffer

Adapts boj-server's seam pattern (`ffi/zig/src/seams.zig` + the
`proof-debt.md` axiom/external-validation discipline, standards#203) to
ephapax's lexer FFI boundary: `tokbuf.zig` ↔ `tokbuf.h` ↔
`ZigBuffer.idr`'s `%foreign` bindings.

### The headline
`eph_tokbuf_str_ptr` ends in a `@ptrCast` that **asserts** (does not
check) the NUL sentinel — the `// SAFETY:` comment argues it holds
because `copyStr` allocates `len+1` and writes a trailing `0`. That's a
class-(J) assumption (true by construction, unprovable at the cast
site). The `str_ptr` seams **externally validate** it: push real
strings, read them back through the cast, assert byte-round-trip +
NUL-termination. A regression in `copyStr` now **fails a seam loudly**
instead of becoming UB at an Idris `String` read. → turns the
`zig_ptr_cast` finding from *suppressed* into *tested*.

### 10 seams (all green locally, zig 0.15.2)
- `@ptrCast`/NUL-sentinel invariant ×3 (incl. the `""` empty-string
sentinel path)
- marshalling round-trips: `tag` (u32), `bool`, `line`/`col` incl.
negatives
- `i32 → usize` clamping: `new(cap ≤ 0)`, `str_len < 0` → `0` + `""` (no
over-read)
- realloc growth (push past cap) + new/free lifecycle

### Changes
| File | What |
|---|---|
| `tokbuf.zig` | `export fn` → `pub export fn` ×10 so `seams.zig` can
`@import`. **Purely additive — emitted C symbols unchanged.** |
| `seams.zig` *(new)* | the 10 tests + methodology + an ABI finding in
its header. Run: `zig test -lc idris2/ffi/zig/seams.zig` |
| `ffi-seams.yml` *(new)* | CI gate; `setup-zig` 0.15.2, `zig test -lc`.
Dedicated workflow (not `abi-verify.yml`, which is
Idris2-container/`src/abi`-scoped). Follows the estate no-path-filter
`changes`+`needs`+`if` convention so it can't strand PRs. |

### Finding (documented, not auto-fixed)
Integer **type-width drift** across the three layers —
`tag`/`bool_val`/`kind` declared `Int` (Idris) / `int32_t` (`.h`) /
`u32`|`u8` (zig). Functions for current value ranges but not type-clean
(sharpest: `bool_val`, 1-byte vs declared 4-byte). Recommend
regenerating `tokbuf.h` from the zig sigs + `Bits32`/`Bits8` in
`ZigBuffer.idr` — left for owner triage (an FFI sig edit can shift the
binding).

### Notes
- **Out of scope:** the Rust-side `from_raw`
(`ephapax-runtime`/`-vram-cache`) + `ephapax-interp` `unsafe`/`as_ptr` —
different boundary, already `// SAFETY:`-documented.
- The methodology lives in the `seams.zig` header rather than a
CC-BY-SA-4.0 `SEAMS.adoc` because this repo's `.git/hooks/pre-commit` is
the **pre-fix version** that demands MPL-2.0 even for `.adoc` (the
`standards` hook was fixed to allow CC-BY-SA-4.0 for docs; ephapax's
copy is stale). Minor follow-up: sync ephapax's hook to the standards
version.

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

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

Author: hyperpolymath

.github/workflows/ffi-seams.yml

@@ -0,0 +1,79 @@
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# ffi-seams.yml — contract tests for the idris2 <-> zig token-buffer ABI.
+#
+# Runs `zig test` on idris2/ffi/zig/seams.zig, which exercises the @ptrCast
+# NUL-sentinel invariant + integer/bool marshalling + i32<->usize clamping
+# across the C-ABI seam (see the header of idris2/ffi/zig/seams.zig).
+#
+# Convention (per the estate CI rule): NO workflow-level `on.*.paths` on a
+# gate — a path-filtered required check is reported "Expected" forever and
+# strands PRs as blocked. Instead an always-run `changes` job decides whether
+# the heavy `test` job runs; a job skipped via `if:` counts as a passing
+# required check.
+
+name: FFI Seam Tests
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  changes:
+    name: Detect relevant changes
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    outputs:
+      run: ${{ steps.detect.outputs.run }}
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          fetch-depth: 0
+      - id: detect
+        env:
+          EVENT: ${{ github.event_name }}
+          BASE: ${{ github.base_ref }}
+          BEFORE: ${{ github.event.before }}
+        run: |
+          # Fail-safe: default to running; only set run=false when a successful
+          # diff shows nothing under idris2/ffi/zig/ changed.
+          set -uo pipefail
+          run=true
+          if [ "$EVENT" = pull_request ]; then
+            git fetch --no-tags --depth=200 origin "$BASE" 2>/dev/null \
+              && changed=$(git diff --name-only "origin/${BASE}...HEAD" 2>/dev/null) \
+              && { printf '%s\n' "$changed" | grep -qE '^idris2/ffi/zig/' && run=true || run=false; }
+          elif [ "$EVENT" = push ] && [ -n "$BEFORE" ] && [ "$BEFORE" != 0000000000000000000000000000000000000000 ]; then
+            changed=$(git diff --name-only "${BEFORE}...${GITHUB_SHA}" 2>/dev/null) \
+              && { printf '%s\n' "$changed" | grep -qE '^idris2/ffi/zig/' && run=true || run=false; }
+          fi
+          printf 'run=%s\n' "$run" >> "$GITHUB_OUTPUT"
+          echo "relevant=$run"
+
+  test:
+    name: Zig FFI seam tests
+    needs: changes
+    if: needs.changes.outputs.run == 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Install Zig
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2
+        with:
+          version: 0.15.2
+
+      - name: Run token-buffer seam tests
+        # -lc: tokbuf.zig allocates via std.heap.c_allocator.
+        run: zig test -lc idris2/ffi/zig/seams.zig

idris2/ffi/zig/seams.zig

@@ -0,0 +1,151 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// seams.zig — integration-contract tests for the ephapax idris2 <-> zig token
+// buffer ABI: tokbuf.zig <-> tokbuf.h <-> the %foreign bindings in
+// src/Ephapax/Parse/ZigBuffer.idr. Pattern adapted from
+// boj-server/ffi/zig/src/seams.zig (the estate trusted-base reference impl).
+//
+// Each `test "seam: ..."` pins one promise the Idris2 side relies on across the
+// C-ABI boundary. A failure here is a genuine ABI/contract defect, not a flaky
+// test. In particular, the str_ptr seams EXERCISE the @ptrCast at tokbuf.zig:99
+// and assert the NUL-sentinel invariant that the `// SAFETY:` comment there only
+// *asserts* — turning asserted-safe into tested-safe (see METHODOLOGY below).
+//
+// Run:  zig test -lc idris2/ffi/zig/seams.zig
+// (-lc is required because tokbuf.zig allocates via std.heap.c_allocator.)
+// CI: .github/workflows/ffi-seams.yml (setup-zig 0.15.2).
+//
+// ── METHODOLOGY ────────────────────────────────────────────────────────────
+// Adapted from boj-server/ffi/zig/src/seams.zig + its docs/proof-debt.md
+// "axiom + external-validation" discipline (estate trusted-base reference,
+// standards#203). `eph_tokbuf_str_ptr` ends in a @ptrCast that ASSERTS (does
+// not check) the NUL sentinel; the sentinel holds because the producer
+// `copyStr` allocates len+1 and writes a trailing 0. That is a class-(J)-style
+// assumption (true by construction, not provable at the cast site). These seams
+// are its external validation: a regression in copyStr fails a seam loudly
+// instead of becoming UB at an Idris `String` read.
+//
+// ── FINDING: integer type-width drift across the three contract layers ──────
+// The seams pass (tokbuf.zig is internally consistent) but the DECLARED types
+// drift:   field      ZigBuffer.idr   tokbuf.h    tokbuf.zig
+//          tag        Int (64-bit)    int32_t     u32
+//          bool_val   Int (64-bit)    int32_t     u8
+//          kind (ret) Int (64-bit)    int32_t     u32
+// It functions for the value ranges used (small token kinds, 0/1 booleans)
+// because each callee reads the width it declares, but it is not type-clean
+// (most sharply bool_val: 1-byte u8 vs declared 4-byte int32_t). Recommended
+// follow-up (NOT done here, to keep this test-only): regenerate tokbuf.h from
+// the Zig signatures and consider Bits32/Bits8 in ZigBuffer.idr. Left for owner
+// triage — an FFI signature edit can shift the binding.
+//
+// OUT OF SCOPE: the Rust-side from_raw (ephapax-runtime / -vram-cache) and
+// ephapax-interp unsafe/as_ptr are a different boundary (Rust FFI / dlopen),
+// documented with // SAFETY: comments at their call sites; not exercised here.
+
+const std = @import("std");
+const tb = @import("tokbuf.zig");
+
+// ─── @ptrCast / NUL-sentinel invariant (the headline) ──────────────────────
+
+test "seam: str_ptr returns a NUL-terminated copy equal to the pushed string" {
+    const buf = tb.eph_tokbuf_new(4);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 7, "hello", 5, 0, 1, 1);
+    // eph_tokbuf_str_ptr performs the @ptrCast under test (tokbuf.zig:99).
+    const p = tb.eph_tokbuf_str_ptr(buf, 0);
+    try std.testing.expectEqualStrings("hello", std.mem.span(p));
+    try std.testing.expectEqual(@as(i32, 5), tb.eph_tokbuf_str_len(buf, 0));
+}
+
+test "seam: str_ptr is independently NUL-terminated for each of several tokens" {
+    const buf = tb.eph_tokbuf_new(0);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 1, "a", 1, 0, 1, 1);
+    tb.eph_tokbuf_push(buf, 2, "bb", 2, 0, 1, 2);
+    tb.eph_tokbuf_push(buf, 3, "ccc", 3, 0, 1, 3);
+    try std.testing.expectEqualStrings("a", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 0)));
+    try std.testing.expectEqualStrings("bb", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 1)));
+    try std.testing.expectEqualStrings("ccc", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 2)));
+}
+
+test "seam: empty string yields the \"\" sentinel, never a dangling cast" {
+    const buf = tb.eph_tokbuf_new(2);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 0, "", 0, 0, 1, 1);
+    // str_ptr falls through the optional-null branch to the "" literal.
+    try std.testing.expectEqualStrings("", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 0)));
+    try std.testing.expectEqual(@as(i32, 0), tb.eph_tokbuf_str_len(buf, 0));
+}
+
+// ─── marshalling round-trips ───────────────────────────────────────────────
+
+test "seam: tag (u32) round-trips through kind" {
+    const buf = tb.eph_tokbuf_new(1);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 0xABCD_1234, "x", 1, 0, 1, 1);
+    try std.testing.expectEqual(@as(u32, 0xABCD_1234), tb.eph_tokbuf_kind(buf, 0));
+}
+
+test "seam: bool_val round-trips (truthy + falsy)" {
+    const buf = tb.eph_tokbuf_new(2);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 0, "t", 1, 1, 1, 1);
+    tb.eph_tokbuf_push(buf, 0, "f", 1, 0, 1, 1);
+    try std.testing.expectEqual(@as(u8, 1), tb.eph_tokbuf_bool(buf, 0));
+    try std.testing.expectEqual(@as(u8, 0), tb.eph_tokbuf_bool(buf, 1));
+}
+
+test "seam: line/col round-trip including negatives" {
+    const buf = tb.eph_tokbuf_new(1);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 0, "x", 1, 0, -3, 42);
+    try std.testing.expectEqual(@as(i32, -3), tb.eph_tokbuf_line(buf, 0));
+    try std.testing.expectEqual(@as(i32, 42), tb.eph_tokbuf_col(buf, 0));
+}
+
+// ─── i32 <-> usize clamping at the boundary ────────────────────────────────
+
+test "seam: new(cap <= 0) yields a usable empty buffer that grows on push" {
+    const buf = tb.eph_tokbuf_new(-5);
+    defer tb.eph_tokbuf_free(buf);
+    try std.testing.expectEqual(@as(i32, 0), tb.eph_tokbuf_len(buf));
+    tb.eph_tokbuf_push(buf, 9, "g", 1, 0, 1, 1);
+    try std.testing.expectEqual(@as(i32, 1), tb.eph_tokbuf_len(buf));
+    try std.testing.expectEqual(@as(u32, 9), tb.eph_tokbuf_kind(buf, 0));
+}
+
+test "seam: negative str_len clamps to 0 and a \"\" sentinel (no over-read)" {
+    const buf = tb.eph_tokbuf_new(1);
+    defer tb.eph_tokbuf_free(buf);
+    tb.eph_tokbuf_push(buf, 0, "ignored", -1, 0, 1, 1);
+    try std.testing.expectEqual(@as(i32, 0), tb.eph_tokbuf_str_len(buf, 0));
+    try std.testing.expectEqualStrings("", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 0)));
+}
+
+// ─── lifecycle / growth ────────────────────────────────────────────────────
+
+test "seam: push beyond initial cap reallocs and preserves every token" {
+    const buf = tb.eph_tokbuf_new(2); // cap 2; push 100 to force realloc growth
+    defer tb.eph_tokbuf_free(buf);
+    var i: i32 = 0;
+    while (i < 100) : (i += 1) {
+        tb.eph_tokbuf_push(buf, @as(u32, @intCast(i)), "n", 1, 0, i, i);
+    }
+    try std.testing.expectEqual(@as(i32, 100), tb.eph_tokbuf_len(buf));
+    try std.testing.expectEqual(@as(u32, 0), tb.eph_tokbuf_kind(buf, 0));
+    try std.testing.expectEqual(@as(u32, 99), tb.eph_tokbuf_kind(buf, 99));
+    try std.testing.expectEqual(@as(i32, 99), tb.eph_tokbuf_col(buf, 99));
+    try std.testing.expectEqualStrings("n", std.mem.span(tb.eph_tokbuf_str_ptr(buf, 99)));
+}
+
+test "seam: repeated new/free cycles leave a clean state (no crash, fresh len)" {
+    var c: usize = 0;
+    while (c < 3) : (c += 1) {
+        const buf = tb.eph_tokbuf_new(1);
+        tb.eph_tokbuf_push(buf, 1, "x", 1, 0, 1, 1);
+        try std.testing.expectEqual(@as(i32, 1), tb.eph_tokbuf_len(buf));
+        tb.eph_tokbuf_free(buf);
+    }
+}

idris2/ffi/zig/tokbuf.zig

@@ -38,7 +38,7 @@ fn copyStr(alloc: std.mem.Allocator, ptr: [*:0]const u8, len: i32) ?[*]u8 {
     return out.ptr;
 }
 
-export fn eph_tokbuf_new(cap: i32) *TokBuf {
+pub export fn eph_tokbuf_new(cap: i32) *TokBuf {
     const alloc = std.heap.c_allocator;
     const cap_usize = if (cap <= 0) 0 else @as(usize, @intCast(cap));
     const items = alloc.alloc(Tok, cap_usize) catch @panic("alloc failed");
@@ -47,7 +47,7 @@ export fn eph_tokbuf_new(cap: i32) *TokBuf {
     return buf;
 }
 
-export fn eph_tokbuf_free(buf: *TokBuf) void {
+pub export fn eph_tokbuf_free(buf: *TokBuf) void {
     const alloc = buf.allocator;
     var i: usize = 0;
     while (i < buf.len) : (i += 1) {
@@ -62,7 +62,7 @@ export fn eph_tokbuf_free(buf: *TokBuf) void {
     alloc.destroy(buf);
 }
 
-export fn eph_tokbuf_push(buf: *TokBuf, tag: u32, str_ptr: [*:0]const u8, str_len: i32, bool_val: u8, line: i32, col: i32) void {
+pub export fn eph_tokbuf_push(buf: *TokBuf, tag: u32, str_ptr: [*:0]const u8, str_len: i32, bool_val: u8, line: i32, col: i32) void {
     ensureCap(buf, buf.len + 1);
     const s_ptr = copyStr(buf.allocator, str_ptr, str_len);
     buf.items[buf.len] = Tok{
@@ -76,16 +76,16 @@ export fn eph_tokbuf_push(buf: *TokBuf, tag: u32, str_ptr: [*:0]const u8, str_le
     buf.len += 1;
 }
 
-export fn eph_tokbuf_len(buf: *TokBuf) i32 {
+pub export fn eph_tokbuf_len(buf: *TokBuf) i32 {
     return @as(i32, @intCast(buf.len));
 }
 
-export fn eph_tokbuf_kind(buf: *TokBuf, idx: i32) u32 {
+pub export fn eph_tokbuf_kind(buf: *TokBuf, idx: i32) u32 {
     const i = @as(usize, @intCast(idx));
     return buf.items[i].tag;
 }
 
-export fn eph_tokbuf_str_ptr(buf: *TokBuf, idx: i32) [*:0]const u8 {
+pub export fn eph_tokbuf_str_ptr(buf: *TokBuf, idx: i32) [*:0]const u8 {
     const i = @as(usize, @intCast(idx));
     const t = buf.items[i];
     if (t.str_ptr) |p| {
@@ -101,22 +101,22 @@ export fn eph_tokbuf_str_ptr(buf: *TokBuf, idx: i32) [*:0]const u8 {
     return "";
 }
 
-export fn eph_tokbuf_str_len(buf: *TokBuf, idx: i32) i32 {
+pub export fn eph_tokbuf_str_len(buf: *TokBuf, idx: i32) i32 {
     const i = @as(usize, @intCast(idx));
     return @as(i32, @intCast(buf.items[i].str_len));
 }
 
-export fn eph_tokbuf_bool(buf: *TokBuf, idx: i32) u8 {
+pub export fn eph_tokbuf_bool(buf: *TokBuf, idx: i32) u8 {
     const i = @as(usize, @intCast(idx));
     return buf.items[i].bool_val;
 }
 
-export fn eph_tokbuf_line(buf: *TokBuf, idx: i32) i32 {
+pub export fn eph_tokbuf_line(buf: *TokBuf, idx: i32) i32 {
     const i = @as(usize, @intCast(idx));
     return buf.items[i].line;
 }
 
-export fn eph_tokbuf_col(buf: *TokBuf, idx: i32) i32 {
+pub export fn eph_tokbuf_col(buf: *TokBuf, idx: i32) i32 {
     const i = @as(usize, @intCast(idx));
     return buf.items[i].col;
 }