build(abi/ffi): wire the Idris2 ABI + Zig FFI to compile (first time)

.github/workflows/mirror.yml

@@ -9,5 +9,4 @@ permissions:
 jobs:
   mirror:
     uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
-    timeout-minutes: 10
     secrets: inherit

.github/workflows/rust-ci.yml

@@ -12,4 +12,3 @@ permissions:
 jobs:
   rust-ci:
     uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@412a7031577112b31ee287cc6060179d638d6500
-    timeout-minutes: 10

.github/workflows/secret-scanner.yml

@@ -11,8 +11,11 @@ permissions:
   contents: read
 jobs:
   scan:
+    permissions:
+      contents: read
+      pull-requests: write
+      actions: read
     uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
-    timeout-minutes: 10
     secrets: inherit
   trufflehog:
     runs-on: ubuntu-latest

Justfile

@@ -30,6 +30,21 @@ test:
 test-verbose:
     cargo test --workspace -- --nocapture
 
+# Build + typecheck the Idris2 ABI layer (src/abi/) via its package.
+verify-abi:
+    idris2 --build rpa-elysium-abi.ipkg
+
+# Build the Zig FFI shared + static libraries (ffi/zig/).
+build-ffi:
+    cd ffi/zig && zig build
+
+# Run the Zig FFI unit tests.
+test-ffi:
+    cd ffi/zig && zig build test
+
+# Verify the whole ABI/FFI layer compiles (Idris proofs + Zig libs + tests).
+verify-abi-ffi: verify-abi build-ffi test-ffi
+
 # Clean build artifacts
 clean:
     cargo clean

ffi/zig/build.zig

@@ -13,32 +13,35 @@ pub fn build(b: *std.Build) void {
     const target = b.standardTargetOptions(.{});
     const optimize = b.standardOptimizeOption(.{});
 
-    // Shared library for FFI consumers
-    const lib = b.addSharedLibrary(.{
-        .name = "rpa_ffi",
+    // The root module shared by every artifact (Zig 0.15 build API).
+    const mod = b.createModule(.{
         .root_source_file = b.path("src/main.zig"),
         .target = target,
         .optimize = optimize,
+        // main.zig uses std.heap.c_allocator for C-ABI-owned allocations.
+        .link_libc = true,
     });
 
-    // Also produce a static library for embedding
-    const static_lib = b.addStaticLibrary(.{
+    // Shared library for FFI consumers.
+    const lib = b.addLibrary(.{
         .name = "rpa_ffi",
-        .root_source_file = b.path("src/main.zig"),
-        .target = target,
-        .optimize = optimize,
+        .root_module = mod,
+        .linkage = .dynamic,
     });
 
-    // Install both artifacts
+    // Also produce a static library for embedding.
+    const static_lib = b.addLibrary(.{
+        .name = "rpa_ffi",
+        .root_module = mod,
+        .linkage = .static,
+    });
+
+    // Install both artifacts.
     b.installArtifact(lib);
     b.installArtifact(static_lib);
 
-    // Unit tests
-    const main_tests = b.addTest(.{
-        .root_source_file = b.path("src/main.zig"),
-        .target = target,
-        .optimize = optimize,
-    });
+    // Unit tests.
+    const main_tests = b.addTest(.{ .root_module = mod });
 
     const run_main_tests = b.addRunArtifact(main_tests);
     const test_step = b.step("test", "Run unit tests");

ffi/zig/src/main.zig

@@ -38,12 +38,14 @@ pub const Result = enum(c_int) {
     null_pointer = 4,
 };
 
-/// Library handle (opaque to prevent direct access)
-pub const Handle = opaque {
+/// Library handle. A regular struct used as the backing type; C consumers only
+/// ever hold a `*Handle` and never see the layout, so it is effectively opaque
+/// across the ABI. (Zig `opaque {}` types cannot carry fields, which the
+/// internal state below requires.)
+pub const Handle = struct {
     // Internal state hidden from C
     allocator: std.mem.Allocator,
     initialized: bool,
-    // Add your fields here
 };
 
 //==============================================================================
@@ -210,7 +212,7 @@ export fn rpa_elysium_build_info() [*:0]const u8 {
 //==============================================================================
 
 /// Callback function type (C ABI)
-pub const Callback = *const fn (u64, u32) callconv(.C) u32;
+pub const Callback = *const fn (u64, u32) callconv(.c) u32;
 
 /// Register a callback
 export fn rpa_elysium_register_callback(

rpa-elysium-abi.ipkg

@@ -0,0 +1,21 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- Idris2 package for the RPA Elysium ABI layer (src/abi/). Wires the
+-- previously-uncompiled ABI modules into a buildable package:
+--   idris2 --build rpa-elysium-abi.ipkg
+--
+-- Module names are flattened to match the src/abi/ layout (sourcedir below),
+-- mirroring HAR's har-abi.ipkg. LinearDispatch.eph is Ephapax, not Idris, and
+-- is built by its own toolchain — it is intentionally not listed here.
+
+package rpa-elysium-abi
+
+sourcedir = "src/abi"
+
+modules = Types
+        , Layout
+        , Foreign
+        , ProvenFSM
+        , ProvenQueue

src/abi/Foreign.idr

@@ -9,13 +9,62 @@
 ||| All functions are declared here with type signatures and safety proofs.
 ||| Implementations live in ffi/zig/
 
-module RpaElysium.ABI.Foreign
+module Foreign
 
-import RpaElysium.ABI.Types
-import RpaElysium.ABI.Layout
+import Types
+import Layout
 
 %default total
 
+--------------------------------------------------------------------------------
+-- FFI glue types (must match ffi/zig and the generated C header)
+--------------------------------------------------------------------------------
+
+||| FFI result codes returned across the C ABI. Tag values MUST match the Zig
+||| implementation (ffi/zig): Ok=0, Error=1, InvalidParam=2, OutOfMemory=3,
+||| NullPointer=4.
+public export
+data Result : Type where
+  Ok           : Result
+  Error        : Result
+  InvalidParam : Result
+  OutOfMemory  : Result
+  NullPointer  : Result
+
+public export
+Show Result where
+  show Ok           = "Ok"
+  show Error        = "Error"
+  show InvalidParam = "InvalidParam"
+  show OutOfMemory  = "OutOfMemory"
+  show NullPointer  = "NullPointer"
+
+||| The C-ABI tag byte for a result code.
+public export
+resultTag : Result -> Bits32
+resultTag Ok           = 0
+resultTag Error        = 1
+resultTag InvalidParam = 2
+resultTag OutOfMemory  = 3
+resultTag NullPointer  = 4
+
+||| An opaque handle to a library instance, wrapping the raw C pointer as a
+||| Bits64. Constructed only via `createHandle`, which rejects the null pointer.
+public export
+data Handle : Type where
+  MkHandle : Bits64 -> Handle
+
+||| Construct a handle from a raw pointer; `Nothing` for the null pointer.
+public export
+createHandle : Bits64 -> Maybe Handle
+createHandle 0 = Nothing
+createHandle p = Just (MkHandle p)
+
+||| The raw C pointer backing a handle.
+public export
+handlePtr : Handle -> Bits64
+handlePtr (MkHandle p) = p
+
 --------------------------------------------------------------------------------
 -- Library Lifecycle
 --------------------------------------------------------------------------------
@@ -178,21 +227,25 @@ buildInfo = do
 -- Callback Support
 --------------------------------------------------------------------------------
 
-||| Callback function type (C ABI)
+||| Callback function type (C ABI) — the shape a registered callback must
+||| have: `(context : Bits64) -> (event : Bits32) -> (result : Bits32)`.
 public export
 Callback : Type
 Callback = Bits64 -> Bits32 -> Bits32
 
 ||| Register a callback
 export
 %foreign "C:rpa_elysium_register_callback, librpa_elysium"
-prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
+prim__registerCallback : Bits64 -> Bits64 -> PrimIO Bits32
 
-||| Safe callback registration
+||| Safe callback registration. The callback is passed as a raw pointer to a
+||| C-callable function of type `Callback`: an Idris closure cannot be handed to
+||| C directly (that needs a foreign export), so the caller supplies the
+||| already-C-callable function pointer (`cbPtr`).
 export
-registerCallback : Handle -> Callback -> IO (Either Result ())
-registerCallback h cb = do
-  result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
+registerCallback : Handle -> (cbPtr : Bits64) -> IO (Either Result ())
+registerCallback h cbPtr = do
+  result <- primIO (prim__registerCallback (handlePtr h) cbPtr)
   pure $ case resultFromInt result of
     Just Ok => Right ()
     Just err => Left err

src/abi/Layout.idr

@@ -7,9 +7,10 @@
 -- Ensures that type representations are consistent across the
 -- Idris2 ABI definitions and the Zig FFI implementation.
 
-module RpaElysium.Abi.Layout
+module Layout
 
-import RpaElysium.Abi.Types
+import Types
+import Data.Nat
 
 %default total
 
@@ -73,9 +74,9 @@ timestampAlignValid = Align8
 ||| Proof that all event kind tags fit in a single byte
 public export
 eventKindTagFitsInByte : (ek : EventKind) -> LTE (cast (eventKindTag ek)) 255
-eventKindTagFitsInByte (FileCreated _)    = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagFitsInByte (FileModified _)   = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagFitsInByte (FileDeleted _)    = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagFitsInByte (FileRenamed _ _)  = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagFitsInByte Manual             = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
+eventKindTagFitsInByte (FileCreated _)    = LTEZero
+eventKindTagFitsInByte (FileModified _)   = LTESucc LTEZero
+eventKindTagFitsInByte (FileDeleted _)    = LTESucc (LTESucc LTEZero)
+eventKindTagFitsInByte (FileRenamed _ _)  = LTESucc (LTESucc (LTESucc LTEZero))
+eventKindTagFitsInByte Manual             = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
 eventKindTagFitsInByte (Scheduled _)      = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))

src/abi/ProvenFSM.idr

@@ -18,9 +18,9 @@
 --   EventDisposition           →  used when events arrive at the workflow engine
 --   ValidMachineTransition     →  defines which workflow state transitions are legal
 
-module RpaElysium.Abi.ProvenFSM
+module ProvenFSM
 
-import RpaElysium.Abi.Types
+import Types
 
 %default total
 

src/abi/ProvenQueue.idr

@@ -22,9 +22,9 @@
 --   DeliveryGuarantee →  configurable per-workflow
 --   QueueOp           →  operations the workflow engine can perform
 
-module RpaElysium.Abi.ProvenQueue
+module ProvenQueue
 
-import RpaElysium.Abi.Types
+import Types
 
 %default total
 

src/abi/Types.idr

@@ -7,7 +7,7 @@
 -- These types mirror the Rust rpa-core types (Event, Action, Workflow, Error)
 -- and provide formal proofs of their properties via dependent types.
 
-module RpaElysium.Abi.Types
+module Types
 
 import Data.Vect
 import Data.String
@@ -54,11 +54,11 @@ eventKindTag (Scheduled _)      = 5
 ||| Proof that event kind tags are within valid range
 public export
 eventKindTagValid : (ek : EventKind) -> LTE (cast (eventKindTag ek)) 5
-eventKindTagValid (FileCreated _)    = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagValid (FileModified _)   = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagValid (FileDeleted _)    = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagValid (FileRenamed _ _)  = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
-eventKindTagValid Manual             = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
+eventKindTagValid (FileCreated _)    = LTEZero
+eventKindTagValid (FileModified _)   = LTESucc LTEZero
+eventKindTagValid (FileDeleted _)    = LTESucc (LTESucc LTEZero)
+eventKindTagValid (FileRenamed _ _)  = LTESucc (LTESucc (LTESucc LTEZero))
+eventKindTagValid Manual             = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
 eventKindTagValid (Scheduled _)      = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
 
 ||| Timestamp as Unix epoch seconds + nanoseconds