diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index f4ddfca..6bd847d 100644 --- a/.github/workflows/mirror.yml +++ b/.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 diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index a4c3019..bd1387d 100644 --- a/.github/workflows/rust-ci.yml +++ b/.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 diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 6961268..6e5bc8f 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.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 diff --git a/Justfile b/Justfile index 8280aef..710f550 100644 --- a/Justfile +++ b/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 diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig index 975366f..6c335aa 100644 --- a/ffi/zig/build.zig +++ b/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"); diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index 954da2d..1a71300 100644 --- a/ffi/zig/src/main.zig +++ b/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( diff --git a/rpa-elysium-abi.ipkg b/rpa-elysium-abi.ipkg new file mode 100644 index 0000000..b8ac206 --- /dev/null +++ b/rpa-elysium-abi.ipkg @@ -0,0 +1,21 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- Owner: Jonathan D.A. Jewell +-- +-- 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 diff --git a/src/abi/Foreign.idr b/src/abi/Foreign.idr index daf5b70..5a11585 100644 --- a/src/abi/Foreign.idr +++ b/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,7 +227,8 @@ 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 @@ -186,13 +236,16 @@ 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 diff --git a/src/abi/Layout.idr b/src/abi/Layout.idr index 2eda8f3..5a3be61 100644 --- a/src/abi/Layout.idr +++ b/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)))) diff --git a/src/abi/ProvenFSM.idr b/src/abi/ProvenFSM.idr index 443d4b6..4714ddd 100644 --- a/src/abi/ProvenFSM.idr +++ b/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 diff --git a/src/abi/ProvenQueue.idr b/src/abi/ProvenQueue.idr index 83c6027..8cadd57 100644 --- a/src/abi/ProvenQueue.idr +++ b/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 diff --git a/src/abi/Types.idr b/src/abi/Types.idr index b94e8f2..f0caeb8 100644 --- a/src/abi/Types.idr +++ b/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