Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
79 changes: 79 additions & 0 deletions .github/workflows/ffi-seams.yml
Original file line number Diff line number Diff line change
@@ -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
151 changes: 151 additions & 0 deletions idris2/ffi/zig/seams.zig
Original file line number Diff line number Diff line change
@@ -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);
}
}
20 changes: 10 additions & 10 deletions idris2/ffi/zig/tokbuf.zig
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand All @@ -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) {
Expand All @@ -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{
Expand All @@ -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| {
Expand All @@ -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;
}
Loading