1- ||| ABI Type Definitions Template
1+ ||| UNIVERSAL-PROJECT-MANAGER (upm) — ABI Type Definitions
22|||
3- ||| This module defines the Application Binary Interface (ABI) for this library.
4- ||| All type definitions include formal proofs of correctness.
5- |||
6- ||| Replace {{PROJECT}} with your project name.
7- ||| Replace {{TYPES}} with your actual type definitions.
8- |||
9- ||| @see https://idris2.readthedocs.io for Idris2 documentation
3+ ||| This module defines the Application Binary Interface for the project
4+ ||| manager logic. It ensures that project metadata and lifecycle events
5+ ||| are handled with strict type safety across language boundaries.
106
11- module {{ PROJECT }} . ABI . Types
7+ module UNIVERSAL_PROJECT_MANAGER .ABI.Types
128
139import Data.Bits
1410import Data.So
@@ -17,215 +13,50 @@ import Data.Vect
1713%default total
1814
1915-- ------------------------------------------------------------------------------
20- -- Platform Detection
16+ -- Platform Context
2117-- ------------------------------------------------------------------------------
2218
23- ||| Supported platforms for this ABI
19+ ||| Supported targets for the UPM core.
2420public export
2521data Platform = Linux | Windows | MacOS | BSD | WASM
2622
27- ||| Compile-time platform detection
28- ||| This will be set during compilation based on target
23+ ||| Resolves the execution environment at compile time.
2924public export
3025thisPlatform : Platform
3126thisPlatform =
3227 % runElab do
33- -- Platform detection logic
34- pure Linux -- Default, override with compiler flags
28+ pure Linux
3529
3630-- ------------------------------------------------------------------------------
37- -- Core Types
31+ -- Core Result Codes
3832-- ------------------------------------------------------------------------------
3933
40- ||| Result codes for FFI operations
41- ||| Use C-compatible integers for cross-language compatibility
34+ ||| Formal outcome of a project management operation.
4235public export
4336data Result : Type where
44- ||| Operation succeeded
37+ ||| Operation Successful
4538 Ok : Result
46- ||| Generic error
39+ ||| Operation Failed: Generic failure
4740 Error : Result
48- ||| Invalid parameter provided
41+ ||| Invalid Parameter: malformed project metadata
4942 InvalidParam : Result
50- ||| Out of memory
43+ ||| System Error: out of memory
5144 OutOfMemory : Result
52- ||| Null pointer encountered
45+ ||| Safety Error: null pointer encountered
5346 NullPointer : Result
5447
55- ||| Convert Result to C integer
56- public export
57- resultToInt : Result -> Bits32
58- resultToInt Ok = 0
59- resultToInt Error = 1
60- resultToInt InvalidParam = 2
61- resultToInt OutOfMemory = 3
62- resultToInt NullPointer = 4
63-
64- ||| Results are decidably equal
65- public export
66- DecEq Result where
67- decEq Ok Ok = Yes Refl
68- decEq Error Error = Yes Refl
69- decEq InvalidParam InvalidParam = Yes Refl
70- decEq OutOfMemory OutOfMemory = Yes Refl
71- decEq NullPointer NullPointer = Yes Refl
72- decEq _ _ = No absurd
73-
7448-- ------------------------------------------------------------------------------
75- -- Opaque Handles
49+ -- Safety Handles
7650-- ------------------------------------------------------------------------------
7751
78- ||| Opaque handle type for FFI
79- ||| Prevents direct construction, enforces creation through safe API
52+ ||| Opaque handle to a UPM session.
53+ ||| INVARIANT: The internal pointer is guaranteed to be non-null.
8054public export
8155data Handle : Type where
8256 MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
8357
84- ||| Safely create a handle from a pointer value
85- ||| Returns Nothing if pointer is null
58+ ||| Safe constructor for project handles.
8659public export
8760createHandle : Bits64 -> Maybe Handle
8861createHandle 0 = Nothing
8962createHandle ptr = Just (MkHandle ptr)
90-
91- ||| Extract pointer value from handle
92- public export
93- handlePtr : Handle -> Bits64
94- handlePtr (MkHandle ptr) = ptr
95-
96- -- ------------------------------------------------------------------------------
97- -- Platform-Specific Types
98- -- ------------------------------------------------------------------------------
99-
100- ||| C int size varies by platform
101- public export
102- CInt : Platform -> Type
103- CInt Linux = Bits32
104- CInt Windows = Bits32
105- CInt MacOS = Bits32
106- CInt BSD = Bits32
107- CInt WASM = Bits32
108-
109- ||| C size_t varies by platform
110- public export
111- CSize : Platform -> Type
112- CSize Linux = Bits64
113- CSize Windows = Bits64
114- CSize MacOS = Bits64
115- CSize BSD = Bits64
116- CSize WASM = Bits32
117-
118- ||| C pointer size varies by platform
119- public export
120- ptrSize : Platform -> Nat
121- ptrSize Linux = 64
122- ptrSize Windows = 64
123- ptrSize MacOS = 64
124- ptrSize BSD = 64
125- ptrSize WASM = 32
126-
127- ||| Pointer type for platform
128- public export
129- CPtr : Platform -> Type -> Type
130- CPtr p _ = Bits (ptrSize p)
131-
132- -- ------------------------------------------------------------------------------
133- -- Memory Layout Proofs
134- -- ------------------------------------------------------------------------------
135-
136- ||| Proof that a type has a specific size
137- public export
138- data HasSize : Type -> Nat -> Type where
139- SizeProof : {0 t : Type } -> {n : Nat } -> HasSize t n
140-
141- ||| Proof that a type has a specific alignment
142- public export
143- data HasAlignment : Type -> Nat -> Type where
144- AlignProof : {0 t : Type } -> {n : Nat } -> HasAlignment t n
145-
146- ||| Size of C types (platform-specific)
147- public export
148- cSizeOf : (p : Platform) -> (t : Type ) -> Nat
149- cSizeOf p (CInt _ ) = 4
150- cSizeOf p (CSize _ ) = if ptrSize p == 64 then 8 else 4
151- cSizeOf p Bits32 = 4
152- cSizeOf p Bits64 = 8
153- cSizeOf p Double = 8
154- cSizeOf p _ = ptrSize p `div` 8
155-
156- ||| Alignment of C types (platform-specific)
157- public export
158- cAlignOf : (p : Platform) -> (t : Type ) -> Nat
159- cAlignOf p (CInt _ ) = 4
160- cAlignOf p (CSize _ ) = if ptrSize p == 64 then 8 else 4
161- cAlignOf p Bits32 = 4
162- cAlignOf p Bits64 = 8
163- cAlignOf p Double = 8
164- cAlignOf p _ = ptrSize p `div` 8
165-
166- -- ------------------------------------------------------------------------------
167- -- Example Struct with Layout Proof
168- -- ------------------------------------------------------------------------------
169-
170- ||| Example C-compatible struct
171- ||| Replace this with your actual data types
172- public export
173- record ExampleStruct where
174- constructor MkExampleStruct
175- field1 : Bits32
176- field2 : Bits64
177- field3 : Double
178-
179- ||| Prove the struct has correct size
180- public export
181- exampleStructSize : (p : Platform) -> HasSize ExampleStruct 16
182- exampleStructSize p =
183- -- 4 bytes (Bits32) + 4 padding + 8 bytes (Bits64) + 8 bytes (Double) = 24
184- -- But with alignment, it's actually platform-specific
185- SizeProof
186-
187- ||| Prove the struct has correct alignment
188- public export
189- exampleStructAlign : (p : Platform) -> HasAlignment ExampleStruct 8
190- exampleStructAlign p = AlignProof
191-
192- -- ------------------------------------------------------------------------------
193- -- FFI Declarations
194- -- ------------------------------------------------------------------------------
195-
196- ||| Declare external C functions
197- ||| These will be implemented in Zig FFI
198- namespace Foreign
199-
200- ||| External function example
201- export
202- % foreign " C:example_function, libexample"
203- prim__exampleFunction : Bits64 -> PrimIO Bits32
204-
205- ||| Safe wrapper around FFI function
206- export
207- exampleFunction : Handle -> IO (Either Result Bits32)
208- exampleFunction h = do
209- result <- primIO (prim__exampleFunction (handlePtr h))
210- pure (Right result)
211-
212- -- ------------------------------------------------------------------------------
213- -- Verification
214- -- ------------------------------------------------------------------------------
215-
216- ||| Compile-time verification of ABI properties
217- namespace Verify
218-
219- ||| Verify struct sizes are correct
220- export
221- verifySizes : IO ()
222- verifySizes = do
223- -- Add compile-time checks here
224- putStrLn " ABI sizes verified"
225-
226- ||| Verify struct alignments are correct
227- export
228- verifyAlignments : IO ()
229- verifyAlignments = do
230- -- Add compile-time checks here
231- putStrLn " ABI alignments verified"
0 commit comments