P1: implement missing FFI functions + fix result-code semantics#32
Merged
Conversation
The Zig FFI (src/interface/ffi/src/main.zig) was generic scaffolding that drifted
from the Idris2 ABI, which is the source of truth
(src/interface/abi/Typedqliser/ABI/Foreign.idr and .../Types.idr).
Two core domain functions declared in Foreign.idr were missing from the Zig:
* typedqliser_check_query : Bits64 -> String -> Bits32 -> PrimIO Bits32
(handle pointer, query C-string, requested safety level) -> result code.
Validates a query against the registered schema up to the requested level
and records the achieved certificate level on the handle.
* typedqliser_certificate_level : Bits64 -> PrimIO Bits32
(handle pointer) -> highest safety level the last checked query achieved
(0 if none), within the ten cumulative type-safety levels.
Both are now exported `callconv(.C)` functions with arities/types matching the
Idris %foreign declarations exactly (the handle is threaded as a Bits64 pointer
value, reconstructed FFI-side).
Result-code semantics corrected to match Typedqliser.ABI.Types.resultToInt:
Ok=0, Error=1, InvalidQuery=2, SchemaError=3, NullPointer=4.
The generic scaffold encoded codes 2 and 3 as invalid_param / out_of_memory,
so cross-FFI those codes meant the WRONG thing. They are renamed to
invalid_query (2) and schema_error (3) and all usages updated.
The pre-existing extra exports (build_info, free_string, get_string,
is_initialized, last_error, process, process_array, register_callback) are kept
as a harmless superset; init/free/version are unchanged in behaviour.
Verification:
* zig test src/interface/ffi/src/main.zig -lc -> all 8 tests pass
(added tests exercising check_query + certificate_level, the malformed-query
InvalidQuery path, the SchemaError path, null-handle rejection, and a
guard pinning the result codes to resultToInt).
* idris2 --build src/interface/abi/typedqliser-abi.ipkg -> exit 0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
hyperpolymath
marked this pull request as ready for review
June 26, 2026 22:08
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
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.
Summary
Fixes ABI↔FFI drift in the Zig FFI (
src/interface/ffi/src/main.zig), which was generic scaffolding that had diverged from the Idris2 ABI. The Idris2 ABI is the source of truth (src/interface/abi/Typedqliser/ABI/Foreign.idrand.../Types.idr).Two missing core domain functions implemented
Both were declared in
Foreign.idrbut absent from the Zig layer. They are now exportedcallconv(.C)functions whose arities/types match the%foreigndeclarations exactly (the handle is threaded as aBits64pointer value and reconstructed FFI-side):typedqliser_check_query : Bits64 -> String -> Bits32 -> PrimIO Bits32→
(handle_ptr: u64, query: [*:0]const u8, level: u32) -> u32. Validates a query against the registered schema up to the requested safety level, and records the achieved certificate level on the handle.typedqliser_certificate_level : Bits64 -> PrimIO Bits32→
(handle_ptr: u64) -> u32. Returns the highest of the ten cumulative type-safety levels the last checked query achieved (0 if none).Result-code semantics corrected
The
Resultenum now matchesTypedqliser.ABI.Types.resultToIntexactly:The generic scaffold had encoded codes 2 and 3 as
invalid_param/out_of_memory— so across the FFI those codes meant the wrong thing versus the ABI. They are renamed toinvalid_query(2) andschema_error(3) and all usages updated.Kept
The pre-existing extra exports (
build_info,free_string,get_string,is_initialized,last_error,process,process_array,register_callback) are retained as a harmless superset;init/free/versionbehaviour is unchanged. Only files undersrc/interface/ffi/were touched.Verification
zig test src/interface/ffi/src/main.zig -lc→ all 8 tests pass (zig 0.14.0). Added tests cover check_query + certificate_level, the malformed-queryInvalidQuerypath, theSchemaErrorpath, null-handle rejection, and a guard pinning the result codes toresultToInt(2=invalid_query, 3=schema_error).idris2 --build src/interface/abi/typedqliser-abi.ipkg→ exit 0 (idris2 0.7.0), thenbuild/removed.Note: any rust-ci / Hypatia / governance red checks 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