Commit ce8cdc7
P1: implement real Zig FFI matching the Idris2 ABI (#30)
## Problem
The Idris2 ABI is the source of truth for this `-iser` project. Its
`%foreign "C:eclexiaiser_*"` declarations live in **two** places:
- `src/interface/abi/Eclexiaiser/ABI/Foreign.idr` — 18 symbols
- the `namespace Foreign` block inside
`src/interface/abi/Eclexiaiser/ABI/Types.idr` — **3 more symbols**:
`eclexiaiser_measure_energy`, `eclexiaiser_query_carbon`,
`eclexiaiser_enforce_budget`
The Zig FFI (`src/interface/ffi/src/main.zig`) exported the 18 from
`Foreign.idr` but was **missing all 3** declared in `Types.idr`. Those
symbols have no matching `export fn`, so they would fail to link when
the ABI is compiled against `libeclexiaiser`. The Zig FFI therefore did
not fully match its ABI.
## Fix
Added the three missing C-ABI exports, with C signatures matching their
`%foreign` types exactly (Idris `Bits64`/`Bits32` ↔ Zig `u64`/`u32`;
opaque handle ↔ `?*anyopaque`; result `Bits32` ↔ the `Result` enum):
| Idris `%foreign` (Types.idr `namespace Foreign`) | Zig export |
| --- | --- |
| `eclexiaiser_measure_energy : Bits64 -> PrimIO Bits64` |
`eclexiaiser_measure_energy(handle) u64` |
| `eclexiaiser_query_carbon : Bits32 -> PrimIO Bits32` |
`eclexiaiser_query_carbon(zone_id: u32) u32` (handle-free) |
| `eclexiaiser_enforce_budget : Bits64 -> Bits64 -> PrimIO Bits32` |
`eclexiaiser_enforce_budget(budget_uj, measured_uj: u64) Result`
(handle-free) |
The handle-free forms mirror the safe wrappers `measureEnergy` /
`queryCarbon` / `enforceBudget` in the `Types.idr` `namespace Foreign`
block. `eclexiaiser_enforce_budget` returns the `Result` enum, whose
values already equal `Types.idr` `resultToInt` (`Ok=0 ..
CounterUnavailable=7`).
Three `test` blocks were added covering the new symbols:
`measure_energy` main path + null-handle rejection, handle-free
`query_carbon`, and `enforce_budget` result codes (ok /
budget_exceeded).
Only `src/interface/ffi/` is touched.
## Verification
- `zig test src/main.zig -lc` → **11/11 pass**, no errors/warnings
- `idris2 --build eclexiaiser-abi.ipkg` → **exit 0**, clean (build dir
removed afterward)
- All **21** `C:eclexiaiser_*` ABI symbols now have a matching `export
fn`
- `Result` enum values equal `resultToInt`
## CI note
Any rust-ci / Hypatia / governance reds are pre-existing estate-infra
checks unrelated to this Zig-only change.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
---
_Generated by [Claude
Code](https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH)_
Co-authored-by: Claude <noreply@anthropic.com>1 parent 890972d commit ce8cdc7
1 file changed
Lines changed: 63 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
247 | 247 | | |
248 | 248 | | |
249 | 249 | | |
| 250 | + | |
| 251 | + | |
| 252 | + | |
| 253 | + | |
| 254 | + | |
| 255 | + | |
| 256 | + | |
| 257 | + | |
| 258 | + | |
| 259 | + | |
| 260 | + | |
| 261 | + | |
| 262 | + | |
| 263 | + | |
| 264 | + | |
| 265 | + | |
| 266 | + | |
| 267 | + | |
| 268 | + | |
| 269 | + | |
| 270 | + | |
| 271 | + | |
250 | 272 | | |
251 | 273 | | |
252 | 274 | | |
| |||
280 | 302 | | |
281 | 303 | | |
282 | 304 | | |
| 305 | + | |
| 306 | + | |
| 307 | + | |
| 308 | + | |
| 309 | + | |
| 310 | + | |
| 311 | + | |
| 312 | + | |
283 | 313 | | |
284 | 314 | | |
285 | 315 | | |
| |||
317 | 347 | | |
318 | 348 | | |
319 | 349 | | |
| 350 | + | |
| 351 | + | |
| 352 | + | |
| 353 | + | |
| 354 | + | |
| 355 | + | |
| 356 | + | |
| 357 | + | |
| 358 | + | |
| 359 | + | |
| 360 | + | |
| 361 | + | |
| 362 | + | |
320 | 363 | | |
321 | 364 | | |
322 | 365 | | |
| |||
639 | 682 | | |
640 | 683 | | |
641 | 684 | | |
| 685 | + | |
| 686 | + | |
| 687 | + | |
| 688 | + | |
| 689 | + | |
| 690 | + | |
| 691 | + | |
| 692 | + | |
| 693 | + | |
| 694 | + | |
| 695 | + | |
| 696 | + | |
| 697 | + | |
| 698 | + | |
| 699 | + | |
| 700 | + | |
| 701 | + | |
| 702 | + | |
| 703 | + | |
| 704 | + | |
0 commit comments