P1: implement real Zig FFI matching the Idris2 ABI#30
Merged
Conversation
The Idris2 ABI is the source of truth. Its %foreign declarations live in
two places: Foreign.idr (18 symbols) and the `namespace Foreign` block in
Types.idr (3 symbols: eclexiaiser_measure_energy, eclexiaiser_query_carbon,
eclexiaiser_enforce_budget). The Zig FFI exported the 18 from Foreign.idr
but was missing all 3 from Types.idr, so those symbols would fail to link
when the ABI is compiled against libeclexiaiser.
This adds the three missing C-ABI exports with signatures matching their
%foreign types exactly:
eclexiaiser_measure_energy : Bits64 -> PrimIO Bits64
(handle: opaque ptr) -> u64 microjoules
eclexiaiser_query_carbon : Bits32 -> PrimIO Bits32
(zone_id: u32) -> u32 mgCO2/kWh (handle-free)
eclexiaiser_enforce_budget : Bits64 -> Bits64 -> PrimIO Bits32
(budget_uj, measured_uj: u64) -> Result (handle-free)
eclexiaiser_enforce_budget returns the Result enum, whose values already
match Types.idr resultToInt (Ok=0 .. CounterUnavailable=7); the handle-free
forms mirror the safe wrappers measureEnergy/queryCarbon/enforceBudget in
the Types.idr namespace Foreign block.
Adds three `test` blocks covering the new symbols: measure_energy main
path plus null-handle rejection, handle-free query_carbon, and
enforce_budget result codes (ok / budget_exceeded).
Verification:
- zig test src/main.zig -lc : 11/11 pass, no warnings
- idris2 --build eclexiaiser-abi.ipkg : exit 0, clean
- all 21 C:eclexiaiser_* ABI symbols now have a matching export fn
- Result enum values equal resultToInt
Only src/interface/ffi/ is touched.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
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
2 participants
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.
Problem
The Idris2 ABI is the source of truth for this
-iserproject. Its%foreign "C:eclexiaiser_*"declarations live in two places:src/interface/abi/Eclexiaiser/ABI/Foreign.idr— 18 symbolsnamespace Foreignblock insidesrc/interface/abi/Eclexiaiser/ABI/Types.idr— 3 more symbols:eclexiaiser_measure_energy,eclexiaiser_query_carbon,eclexiaiser_enforce_budgetThe Zig FFI (
src/interface/ffi/src/main.zig) exported the 18 fromForeign.idrbut was missing all 3 declared inTypes.idr. Those symbols have no matchingexport fn, so they would fail to link when the ABI is compiled againstlibeclexiaiser. The Zig FFI therefore did not fully match its ABI.Fix
Added the three missing C-ABI exports, with C signatures matching their
%foreigntypes exactly (IdrisBits64/Bits32↔ Zigu64/u32; opaque handle ↔?*anyopaque; resultBits32↔ theResultenum):%foreign(Types.idrnamespace Foreign)eclexiaiser_measure_energy : Bits64 -> PrimIO Bits64eclexiaiser_measure_energy(handle) u64eclexiaiser_query_carbon : Bits32 -> PrimIO Bits32eclexiaiser_query_carbon(zone_id: u32) u32(handle-free)eclexiaiser_enforce_budget : Bits64 -> Bits64 -> PrimIO Bits32eclexiaiser_enforce_budget(budget_uj, measured_uj: u64) Result(handle-free)The handle-free forms mirror the safe wrappers
measureEnergy/queryCarbon/enforceBudgetin theTypes.idrnamespace Foreignblock.eclexiaiser_enforce_budgetreturns theResultenum, whose values already equalTypes.idrresultToInt(Ok=0 .. CounterUnavailable=7).Three
testblocks were added covering the new symbols:measure_energymain path + null-handle rejection, handle-freequery_carbon, andenforce_budgetresult codes (ok / budget_exceeded).Only
src/interface/ffi/is touched.Verification
zig test src/main.zig -lc→ 11/11 pass, no errors/warningsidris2 --build eclexiaiser-abi.ipkg→ exit 0, clean (build dir removed afterward)C:eclexiaiser_*ABI symbols now have a matchingexport fnResultenum values equalresultToIntCI 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.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
Generated by Claude Code