Skip to content

Commit e8972af

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(abi): bespoke Idris2 ABI definitions with partition/gather proofs
Replace template placeholders with chapeliser-specific formal types: Types.idr: - PartitionStrategy/GatherStrategy enums with DecEq - Slice/Partition records with completeness and disjointness proofs - GatherConservation proof (no results lost during gather) - RoundTrip witness for serialisation correctness - RetryIsolation proof (retry only affects target item) - WorkloadConfig with dependent-type bounds (items>0, locales>0) - Chapeliser-specific Result codes (RetryExhausted, CheckpointError) Layout.idr: - ItemBufferLayout with isolation proofs (no buffer overlap) - SliceDescriptorLayout (16 bytes, 8-aligned) with size proofs - ResultArrayLayout matching Chapel's 3-array representation - CheckpointLayout for tagged checkpoint buffers - Memory budget calculator for per-locale estimation Foreign.idr: - All 12 FFI functions matching Chapel extern procs - Safe IO wrappers with Result error handling - PipelineCorrect witness composing partition + gather proofs Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 0e8a19a commit e8972af

3 files changed

Lines changed: 476 additions & 390 deletions

File tree

‎src/interface/abi/Foreign.idr‎

Lines changed: 124 additions & 143 deletions
Original file line numberDiff line numberDiff line change
@@ -1,210 +1,191 @@
11
-- SPDX-License-Identifier: PMPL-1.0-or-later
2-
-- Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
--
4-
||| Foreign Function Interface Declarations
4+
||| Chapeliser Foreign Function Interface Declarations
55
|||
6-
||| This module declares all C-compatible functions that will be
7-
||| implemented in the Zig FFI layer.
6+
||| Declares all C-compatible functions that the Chapeliser runtime calls.
7+
||| These functions are implemented in the Zig FFI layer, which delegates
8+
||| to the user's workload-specific code.
89
|||
9-
||| All functions are declared here with type signatures and safety proofs.
10-
||| Implementations live in ffi/zig/
10+
||| The function signatures here MUST match:
11+
||| 1. The Chapel `extern proc` declarations in the generated .chpl file
12+
||| 2. The Zig `export fn` signatures in the generated _ffi.zig file
13+
||| 3. The C function declarations in the generated .h header
14+
|||
15+
||| Any mismatch is a linking error caught at Chapel compile time.
1116

12-
module {{PROJECT}}.ABI.Foreign
17+
module Chapeliser.ABI.Foreign
1318

14-
import {{PROJECT}}.ABI.Types
15-
import {{PROJECT}}.ABI.Layout
19+
import Chapeliser.ABI.Types
20+
import Chapeliser.ABI.Layout
1621

1722
%default total
1823

1924
--------------------------------------------------------------------------------
2025
-- Library Lifecycle
2126
--------------------------------------------------------------------------------
2227

23-
||| Initialize the library
24-
||| Returns a handle to the library instance, or Nothing on failure
28+
||| Initialise the workload library. Called once on Chapel locale 0
29+
||| before any items are loaded or processed.
30+
||| Returns 0 on success, non-zero error code on failure.
2531
export
26-
%foreign "C:{{project}}_init, lib{{project}}"
27-
prim__init : PrimIO Bits64
32+
%foreign "C:c_init, libchapeliser_ffi"
33+
prim__init : PrimIO Bits32
2834

29-
||| Safe wrapper for library initialization
35+
||| Safe wrapper for initialisation
3036
export
31-
init : IO (Maybe Handle)
37+
init : IO (Either Result ())
3238
init = do
33-
ptr <- primIO prim__init
34-
pure (createHandle ptr)
35-
36-
||| Clean up library resources
37-
export
38-
%foreign "C:{{project}}_free, lib{{project}}"
39-
prim__free : Bits64 -> PrimIO ()
40-
41-
||| Safe wrapper for cleanup
42-
export
43-
free : Handle -> IO ()
44-
free h = primIO (prim__free (handlePtr h))
45-
46-
--------------------------------------------------------------------------------
47-
-- Core Operations
48-
--------------------------------------------------------------------------------
39+
rc <- primIO prim__init
40+
pure $ if rc == 0 then Right () else Left Error
4941

50-
||| Example operation: process data
42+
||| Shut down the workload library. Called once on locale 0
43+
||| after all results have been stored.
5144
export
52-
%foreign "C:{{project}}_process, lib{{project}}"
53-
prim__process : Bits64 -> Bits32 -> PrimIO Bits32
45+
%foreign "C:c_shutdown, libchapeliser_ffi"
46+
prim__shutdown : PrimIO Bits32
5447

55-
||| Safe wrapper with error handling
48+
||| Safe wrapper for shutdown
5649
export
57-
process : Handle -> Bits32 -> IO (Either Result Bits32)
58-
process h input = do
59-
result <- primIO (prim__process (handlePtr h) input)
60-
pure $ case result of
61-
0 => Left Error
62-
n => Right n
50+
shutdown : IO (Either Result ())
51+
shutdown = do
52+
rc <- primIO prim__shutdown
53+
pure $ if rc == 0 then Right () else Left Error
6354

6455
--------------------------------------------------------------------------------
65-
-- String Operations
56+
-- Data I/O
6657
--------------------------------------------------------------------------------
6758

68-
||| Convert C string to Idris String
59+
||| Get the total number of input items. Called on locale 0.
60+
||| Returns item count (>= 0), or negative on error.
6961
export
70-
%foreign "support:idris2_getString, libidris2_support"
71-
prim__getString : Bits64 -> String
62+
%foreign "C:c_get_total_items, libchapeliser_ffi"
63+
prim__getTotalItems : PrimIO Bits32
7264

73-
||| Free C string
65+
||| Safe wrapper
7466
export
75-
%foreign "C:{{project}}_free_string, lib{{project}}"
76-
prim__freeString : Bits64 -> PrimIO ()
67+
getTotalItems : IO (Either Result Nat)
68+
getTotalItems = do
69+
n <- primIO prim__getTotalItems
70+
pure $ Right (cast n)
7771

78-
||| Get string result from library
72+
||| Load (serialise) input item at index `idx` into buffer `buf`.
73+
||| On entry, `*len` is the buffer capacity (maxItemBytes).
74+
||| On exit, `*len` is the actual serialised size.
75+
||| Returns 0 on success.
7976
export
80-
%foreign "C:{{project}}_get_string, lib{{project}}"
81-
prim__getResult : Bits64 -> PrimIO Bits64
77+
%foreign "C:c_load_item, libchapeliser_ffi"
78+
prim__loadItem : Bits32 -> Bits64 -> Bits64 -> PrimIO Bits32
8279

83-
||| Safe string getter
80+
||| Store (receive) a processed result at index `idx`.
81+
||| `buf` contains `len` bytes of serialised result data.
82+
||| Returns 0 on success.
8483
export
85-
getString : Handle -> IO (Maybe String)
86-
getString h = do
87-
ptr <- primIO (prim__getResult (handlePtr h))
88-
if ptr == 0
89-
then pure Nothing
90-
else do
91-
let str = prim__getString ptr
92-
primIO (prim__freeString ptr)
93-
pure (Just str)
84+
%foreign "C:c_store_result, libchapeliser_ffi"
85+
prim__storeResult : Bits32 -> Bits64 -> Bits64 -> PrimIO Bits32
9486

9587
--------------------------------------------------------------------------------
96-
-- Array/Buffer Operations
88+
-- Item Processing
9789
--------------------------------------------------------------------------------
9890

99-
||| Process array data
91+
||| Process a single serialised item.
92+
||| Reads from (in_buf, in_len), writes result to (out_buf, *out_len).
93+
||| Called on any locale — the user's function must be thread-safe.
94+
||| Returns 0 on success.
10095
export
101-
%foreign "C:{{project}}_process_array, lib{{project}}"
102-
prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
96+
%foreign "C:c_process_item, libchapeliser_ffi"
97+
prim__processItem : Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32
10398

104-
||| Safe array processor
99+
||| Process a chunk of items (for chunk partition strategy).
100+
||| items_buf contains item_count items at the given offsets and sizes.
101+
||| Returns 0 on success.
105102
export
106-
processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
107-
processArray h buf len = do
108-
result <- primIO (prim__processArray (handlePtr h) buf len)
109-
pure $ case resultFromInt result of
110-
Just Ok => Right ()
111-
Just err => Left err
112-
Nothing => Left Error
113-
where
114-
resultFromInt : Bits32 -> Maybe Result
115-
resultFromInt 0 = Just Ok
116-
resultFromInt 1 = Just Error
117-
resultFromInt 2 = Just InvalidParam
118-
resultFromInt 3 = Just OutOfMemory
119-
resultFromInt 4 = Just NullPointer
120-
resultFromInt _ = Nothing
103+
%foreign "C:c_process_chunk, libchapeliser_ffi"
104+
prim__processChunk : Bits64 -> Bits32 -> Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32
121105

122106
--------------------------------------------------------------------------------
123-
-- Error Handling
107+
-- Reduction
124108
--------------------------------------------------------------------------------
125109

126-
||| Get last error message
110+
||| Combine two serialised results into one.
111+
||| Used by reduce and tree-reduce gather strategies.
112+
||| Reads (a_buf, a_len) and (b_buf, b_len), writes to (out_buf, *out_len).
113+
||| The reduce function must be associative for tree-reduce correctness.
114+
||| Returns 0 on success.
127115
export
128-
%foreign "C:{{project}}_last_error, lib{{project}}"
129-
prim__lastError : PrimIO Bits64
116+
%foreign "C:c_reduce, libchapeliser_ffi"
117+
prim__reduce : Bits64 -> Bits64 -> Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32
118+
119+
--------------------------------------------------------------------------------
120+
-- Match Predicate (for 'first' gather)
121+
--------------------------------------------------------------------------------
130122

131-
||| Retrieve last error as string
123+
||| Test whether a serialised result matches the search criterion.
124+
||| Returns 1 if the result matches, 0 if not.
125+
||| Used by the 'first' gather strategy to stop early.
132126
export
133-
lastError : IO (Maybe String)
134-
lastError = do
135-
ptr <- primIO prim__lastError
136-
if ptr == 0
137-
then pure Nothing
138-
else pure (Just (prim__getString ptr))
127+
%foreign "C:c_is_match, libchapeliser_ffi"
128+
prim__isMatch : Bits64 -> Bits64 -> PrimIO Bits32
139129

140-
||| Get error description for result code
130+
||| Safe wrapper
141131
export
142-
errorDescription : Result -> String
143-
errorDescription Ok = "Success"
144-
errorDescription Error = "Generic error"
145-
errorDescription InvalidParam = "Invalid parameter"
146-
errorDescription OutOfMemory = "Out of memory"
147-
errorDescription NullPointer = "Null pointer"
132+
isMatch : (bufPtr : Bits64) -> (len : Bits64) -> IO Bool
133+
isMatch buf len = do
134+
rc <- primIO (prim__isMatch buf len)
135+
pure (rc == 1)
148136

149137
--------------------------------------------------------------------------------
150-
-- Version Information
138+
-- Key Hash (for keyed partition)
151139
--------------------------------------------------------------------------------
152140

153-
||| Get library version
141+
||| Compute a hash of the item's distribution key.
142+
||| Items with the same hash (mod numLocales) land on the same locale.
143+
||| Returns an unsigned 32-bit hash value.
154144
export
155-
%foreign "C:{{project}}_version, lib{{project}}"
156-
prim__version : PrimIO Bits64
145+
%foreign "C:c_key_hash, libchapeliser_ffi"
146+
prim__keyHash : Bits64 -> Bits64 -> PrimIO Bits32
157147

158-
||| Get version as string
159-
export
160-
version : IO String
161-
version = do
162-
ptr <- primIO prim__version
163-
pure (prim__getString ptr)
148+
--------------------------------------------------------------------------------
149+
-- Checkpoint (optional)
150+
--------------------------------------------------------------------------------
164151

165-
||| Get library build info
152+
||| Save checkpoint data with a string tag.
153+
||| Returns 0 on success, -1 if checkpointing is not implemented.
166154
export
167-
%foreign "C:{{project}}_build_info, lib{{project}}"
168-
prim__buildInfo : PrimIO Bits64
155+
%foreign "C:c_checkpoint_save, libchapeliser_ffi"
156+
prim__checkpointSave : Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32
169157

170-
||| Get build information
158+
||| Load checkpoint data by tag.
159+
||| On entry, *len is buffer capacity. On exit, *len is data size.
160+
||| Returns 0 on success, -1 if no checkpoint exists or not implemented.
171161
export
172-
buildInfo : IO String
173-
buildInfo = do
174-
ptr <- primIO prim__buildInfo
175-
pure (prim__getString ptr)
162+
%foreign "C:c_checkpoint_load, libchapeliser_ffi"
163+
prim__checkpointLoad : Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32
176164

177165
--------------------------------------------------------------------------------
178-
-- Callback Support
166+
-- Version Information
179167
--------------------------------------------------------------------------------
180168

181-
||| Callback function type (C ABI)
182-
public export
183-
Callback : Type
184-
Callback = Bits64 -> Bits32 -> Bits32
185-
186-
||| Register a callback
169+
||| Chapeliser ABI version (major * 1000 + minor)
170+
||| Used to detect ABI mismatches at runtime.
187171
export
188-
%foreign "C:{{project}}_register_callback, lib{{project}}"
189-
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
190-
191-
-- TODO: Implement safe callback registration.
192-
-- The callback must be wrapped via a proper FFI callback mechanism.
193-
-- Do NOT use cast — it is banned per project safety standards.
194-
-- See: https://idris2.readthedocs.io/en/latest/ffi/ffi.html#callbacks
172+
chapeliserABIVersion : Bits32
173+
chapeliserABIVersion = 1000 -- v1.0
195174

196175
--------------------------------------------------------------------------------
197-
-- Utility Functions
176+
-- Verification: Partition + Gather Composition
198177
--------------------------------------------------------------------------------
199178

200-
||| Check if library is initialized
201-
export
202-
%foreign "C:{{project}}_is_initialized, lib{{project}}"
203-
prim__isInitialized : Bits64 -> PrimIO Bits32
204-
205-
||| Check initialization status
206-
export
207-
isInitialized : Handle -> IO Bool
208-
isInitialized h = do
209-
result <- primIO (prim__isInitialized (handlePtr h))
210-
pure (result /= 0)
179+
||| The full Chapeliser pipeline is correct if:
180+
||| 1. The partition is valid (complete + disjoint)
181+
||| 2. Each item is processed exactly once
182+
||| 3. The gather preserves all results
183+
|||
184+
||| This type witnesses that a workload configuration satisfies all three.
185+
public export
186+
data PipelineCorrect : WorkloadConfig -> Type where
187+
MkPipelineCorrect :
188+
{cfg : WorkloadConfig} ->
189+
(partition : ValidPartition (MkPartition (perItemSlices cfg.totalItems cfg.numLocales))) ->
190+
(gather : GatherConservation (MkGatherInput (replicate cfg.numLocales (cfg.totalItems `div` cfg.numLocales))) cfg.totalItems) ->
191+
PipelineCorrect cfg

0 commit comments

Comments
 (0)