feat(ffi): contract-test the idris2↔zig token-buffer ABI (seams)#334
Merged
Conversation
Adds `idris2/ffi/zig/seams.zig` — 10 integration-contract tests over the tokbuf C-ABI (tokbuf.zig ↔ tokbuf.h ↔ ZigBuffer.idr's %foreign bindings), adapting the boj-server seam pattern (standards#203 trusted-base reference). The headline: `eph_tokbuf_str_ptr` ends in a `@ptrCast` that *asserts* (not checks) the NUL-sentinel. The str_ptr seams push real strings and read them back, asserting the bytes round-trip and stay NUL-terminated — turning the `// SAFETY:` comment's assertion into a tested invariant. A regression in `copyStr` (drop the +1 / the trailing NUL) now fails loudly instead of becoming UB at an Idris `String` read. Other seams cover tag/bool/line/col marshalling (incl. negatives), i32→usize clamping (`new(cap≤0)`, `str_len<0`), and realloc-growth + new/free lifecycle. Changes: - `tokbuf.zig`: `export fn` → `pub export fn` (×10) so seams.zig can `@import` them. Purely additive — the emitted C symbols are unchanged. - `seams.zig` (new): the 10 contract tests, with the methodology + an ABI finding documented in its header (integer type-width drift across the three layers: tag/bool_val/kind declared Int / int32_t / u32|u8 — functions for current ranges but not type-clean; flagged for owner triage, not auto-fixed). Run: `zig test -lc idris2/ffi/zig/seams.zig`. - `ffi-seams.yml` (new): CI gate. A dedicated workflow rather than extending abi-verify.yml (Idris2-container + src/abi-scoped — wrong env); follows the estate no-path-filter `changes`+`needs`+`if` convention so it can't strand PRs. setup-zig 0.15.2, runs `zig test -lc`. Verified locally: all 10 seams pass under zig 0.15.2. Retires the `zig_ptr_cast` finding's assurance gap (tested, not just suppressed). The Rust-side from_raw/unsafe boundary is separate and out of scope. (Methodology folded into the seams.zig header rather than a CC-BY-SA-4.0 SEAMS.adoc because this repo's pre-commit hook is the pre-fix version that still demands MPL-2.0 even for .adoc — flagged as a follow-up.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
marked this pull request as ready for review
June 29, 2026 12:22
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Seam-contract tests for the idris2↔zig token buffer
Adapts boj-server's seam pattern (
ffi/zig/src/seams.zig+ theproof-debt.mdaxiom/external-validation discipline, standards#203) to ephapax's lexer FFI boundary:tokbuf.zig↔tokbuf.h↔ZigBuffer.idr's%foreignbindings.The headline
eph_tokbuf_str_ptrends in a@ptrCastthat asserts (does not check) the NUL sentinel — the// SAFETY:comment argues it holds becausecopyStrallocateslen+1and writes a trailing0. That's a class-(J) assumption (true by construction, unprovable at the cast site). Thestr_ptrseams externally validate it: push real strings, read them back through the cast, assert byte-round-trip + NUL-termination. A regression incopyStrnow fails a seam loudly instead of becoming UB at an IdrisStringread. → turns thezig_ptr_castfinding from suppressed into tested.10 seams (all green locally, zig 0.15.2)
@ptrCast/NUL-sentinel invariant ×3 (incl. the""empty-string sentinel path)tag(u32),bool,line/colincl. negativesi32 → usizeclamping:new(cap ≤ 0),str_len < 0→0+""(no over-read)Changes
tokbuf.zigexport fn→pub export fn×10 soseams.zigcan@import. Purely additive — emitted C symbols unchanged.seams.zig(new)zig test -lc idris2/ffi/zig/seams.zigffi-seams.yml(new)setup-zig0.15.2,zig test -lc. Dedicated workflow (notabi-verify.yml, which is Idris2-container/src/abi-scoped). Follows the estate no-path-filterchanges+needs+ifconvention so it can't strand PRs.Finding (documented, not auto-fixed)
Integer type-width drift across the three layers —
tag/bool_val/kinddeclaredInt(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 regeneratingtokbuf.hfrom the zig sigs +Bits32/Bits8inZigBuffer.idr— left for owner triage (an FFI sig edit can shift the binding).Notes
from_raw(ephapax-runtime/-vram-cache) +ephapax-interpunsafe/as_ptr— different boundary, already// SAFETY:-documented.seams.zigheader rather than a CC-BY-SA-4.0SEAMS.adocbecause this repo's.git/hooks/pre-commitis the pre-fix version that demands MPL-2.0 even for.adoc(thestandardshook 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