Skip to content

P1: implement real Zig FFI matching the Idris2 ABI#42

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/new-session-1fphit
Jun 26, 2026
Merged

P1: implement real Zig FFI matching the Idris2 ABI#42
hyperpolymath merged 1 commit into
mainfrom
claude/new-session-1fphit

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

What was wrong

The Zig FFI at src/interface/ffi/src/main.zig did not compile. The analysis-engine handle was declared as:

pub const Handle = opaque {
    allocator: std.mem.Allocator,
    initialized: bool,
    ...
};

Zig rejects this with error: opaque types cannot have fields. The file was effectively a half-/unrendered template that never built, so it could not honour the ABI contract defined by the Idris2 ABI (the source of truth).

The fix

main.zig is rewritten as a self-contained, compiling reference FFI driven by src/interface/abi/Atsiser/ABI/Foreign.idr and Types.idr:

  • Exact symbols: exports all 20 C:atsiser_* symbols declared in Foreign.idr, verbatim (atsiser_init, atsiser_free, atsiser_parse_header, atsiser_analyse_allocations, atsiser_build_ownership_graph, atsiser_detect_buffers, atsiser_generate_viewtypes, atsiser_generate_proofs, atsiser_generate_bounds_proofs, atsiser_compile_ats2, atsiser_verify_linkage, atsiser_allocation_count, atsiser_ownership_edge_count, atsiser_proof_count, atsiser_analysis_report, atsiser_free_string, atsiser_last_error, atsiser_version, atsiser_build_info, atsiser_is_initialized). All callconv(.C).
  • Matching signatures: Bits64 handle ↔ opaque ?*Engine; Idris String arg ↔ ?[*:0]const u8; returns-a-string Bits64 ↔ ?[*:0]const u8; result-returning Bits32 ↔ Result enum as c_int; counts ↔ c_uint.
  • Matching result codes: Result = enum(c_int) whose values exactly match Atsiser.ABI.Types.resultToInt — Ok=0, Error=1 (err), InvalidParam=2, OutOfMemory=3, NullPointer=4, OwnershipViolation=5, BoundsViolation=6 (7 codes).
  • Memory-sane in-memory reference: a real Engine tracking allocation sites, ownership edges, and buffer/proof counts via std.heap.c_allocator, with proper deinit and C-string ownership (dup / std.mem.span / allocPrintZ / atsiser_free_string). libclang parsing and patsopt (ATS2 → C) bridging remain stubs, but signatures, symbols, and result codes match the ABI.
  • Tests: two test blocks — the main analysis pipeline (parse → analyse → ownership graph → proofs → JSON report) and null-handle / invalid-param rejection.

Only src/interface/ffi/ (the Zig) was touched. The Idris ABI, Cargo, and other files are unchanged.

Verification

  • cd src/interface/ffi && zig test src/main.zig -lcall tests pass, zero errors/warnings:
    1/2 main.test.analysis pipeline and report...OK
    2/2 main.test.null handle and invalid params are rejected...OK
    All 2 tests passed.
    
  • cd src/interface/abi && idris2 --build atsiser-abi.ipkgexits 0 clean (builds Types, Layout, Proofs, Foreign), build dir removed afterward.
  • Symbol cross-check: every C:<name> in Foreign.idr has a matching export fn <name> in main.zig (20/20, perfect diff match).
  • Result codes match resultToInt exactly (7/7).

Note: any rust-ci / Hypatia / governance CI reds are pre-existing estate-infra issues unrelated to this Zig-only change.

🤖 Generated with Claude Code

https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH


Generated by Claude Code

The Zig FFI at src/interface/ffi/src/main.zig did not compile: the engine
handle was declared as `pub const Handle = opaque { ... }` with struct
fields, which Zig rejects ("opaque types cannot have fields"). The file was
effectively an unrendered/half-rendered template that never built and so
could not honour the ABI contract.

This rewrites main.zig as a self-contained, compiling reference FFI driven
by the Idris2 ABI (the source of truth):

- Exports exactly the 20 `C:atsiser_*` symbols declared in
  src/interface/abi/Atsiser/ABI/Foreign.idr, with C-compatible signatures
  matching the Idris types (Bits64 handle <-> opaque `?*Engine`; Idris
  `String` arg <-> `?[*:0]const u8`; returns-a-string Bits64 <->
  `?[*:0]const u8`; result-returning Bits32 <-> `Result` enum as c_int;
  counts <-> c_uint). All `callconv(.C)`.
- `Result = enum(c_int)` whose values exactly match
  Atsiser.ABI.Types.resultToInt: Ok=0, Error=1, InvalidParam=2,
  OutOfMemory=3, NullPointer=4, OwnershipViolation=5, BoundsViolation=6.
- A real in-memory engine (allocation sites, ownership edges, buffer/proof
  counts) using std.heap.c_allocator, with proper deinit and C-string
  ownership via dup / std.mem.span / allocPrintZ / atsiser_free_string.
  libclang parsing and patsopt (ATS2 -> C) bridging remain stubs, but
  signatures, symbols, and result codes match the ABI.
- Two `test` blocks: the main analysis pipeline (parse -> analyse ->
  ownership graph -> proofs -> report) and null-handle / invalid-param
  rejection.

Verification:
- `zig test src/main.zig -lc` -> all tests pass, zero errors/warnings.
- `idris2 --build atsiser-abi.ipkg` -> exits 0 clean.
- Every `C:<name>` in Foreign.idr has a matching `export fn <name>`; Result
  values match resultToInt.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
@hyperpolymath hyperpolymath marked this pull request as ready for review June 26, 2026 22:08
@hyperpolymath hyperpolymath merged commit 458701d into main Jun 26, 2026
20 of 22 checks passed
@hyperpolymath hyperpolymath deleted the claude/new-session-1fphit branch June 26, 2026 22:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants