Skip to content

Commit 2029b40

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(a2ml): salvage cookbook/USAGE/Idris-ABI from superseded .scm spec repos
Cherry-picks unique authored content from the now-archived standalone spec repos at verification-ecosystem/{STATE,ECOSYSTEM,META}.scm into the canonical *-a2ml/ specs: state-a2ml/docs/COOKBOOK.adoc <- STATE.scm/cookbook.adoc (794 lines) state-a2ml/docs/USAGE.adoc <- STATE.scm/USAGE.adoc (333 lines) state-a2ml/channels.scm <- STATE.scm/channels.scm (Guix channel) state-a2ml/manifest.scm <- STATE.scm/manifest.scm ecosystem-a2ml/src/abi/Foreign.idr <- ECOSYSTEM.scm/src/abi/Foreign.idr ecosystem-a2ml/src/abi/Layout.idr <- ECOSYSTEM.scm/src/abi/Layout.idr ecosystem-a2ml/src/abi/Types.idr <- ECOSYSTEM.scm/src/abi/Types.idr Rest of the old standalone repos (RSR boilerplate, .scm checkpoint files, LICENSE/CONTRIBUTING/SECURITY duplicates) is superseded by the canonical standards/{state,meta,ecosystem}-a2ml/ tree. Originals preserved with full .git history at hyperpolymath-archive/superseded-by-standards/. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 1d5047c commit 2029b40

7 files changed

Lines changed: 1818 additions & 0 deletions

File tree

‎ecosystem-a2ml/src/abi/Foreign.idr‎

Lines changed: 216 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,216 @@
1+
||| Foreign Function Interface Declarations
2+
|||
3+
||| This module declares all C-compatible functions that will be
4+
||| implemented in the Zig FFI layer.
5+
|||
6+
||| All functions are declared here with type signatures and safety proofs.
7+
||| Implementations live in ffi/zig/
8+
9+
module {{PROJECT}}.ABI.Foreign
10+
11+
import {{PROJECT}}.ABI.Types
12+
import {{PROJECT}}.ABI.Layout
13+
14+
%default total
15+
16+
--------------------------------------------------------------------------------
17+
-- Library Lifecycle
18+
--------------------------------------------------------------------------------
19+
20+
||| Initialize the library
21+
||| Returns a handle to the library instance, or Nothing on failure
22+
export
23+
%foreign "C:{{project}}_init, lib{{project}}"
24+
prim__init : PrimIO Bits64
25+
26+
||| Safe wrapper for library initialization
27+
export
28+
init : IO (Maybe Handle)
29+
init = do
30+
ptr <- primIO prim__init
31+
pure (createHandle ptr)
32+
33+
||| Clean up library resources
34+
export
35+
%foreign "C:{{project}}_free, lib{{project}}"
36+
prim__free : Bits64 -> PrimIO ()
37+
38+
||| Safe wrapper for cleanup
39+
export
40+
free : Handle -> IO ()
41+
free h = primIO (prim__free (handlePtr h))
42+
43+
--------------------------------------------------------------------------------
44+
-- Core Operations
45+
--------------------------------------------------------------------------------
46+
47+
||| Example operation: process data
48+
export
49+
%foreign "C:{{project}}_process, lib{{project}}"
50+
prim__process : Bits64 -> Bits32 -> PrimIO Bits32
51+
52+
||| Safe wrapper with error handling
53+
export
54+
process : Handle -> Bits32 -> IO (Either Result Bits32)
55+
process h input = do
56+
result <- primIO (prim__process (handlePtr h) input)
57+
pure $ case result of
58+
0 => Left Error
59+
n => Right n
60+
61+
--------------------------------------------------------------------------------
62+
-- String Operations
63+
--------------------------------------------------------------------------------
64+
65+
||| Convert C string to Idris String
66+
export
67+
%foreign "support:idris2_getString, libidris2_support"
68+
prim__getString : Bits64 -> String
69+
70+
||| Free C string
71+
export
72+
%foreign "C:{{project}}_free_string, lib{{project}}"
73+
prim__freeString : Bits64 -> PrimIO ()
74+
75+
||| Get string result from library
76+
export
77+
%foreign "C:{{project}}_get_string, lib{{project}}"
78+
prim__getResult : Bits64 -> PrimIO Bits64
79+
80+
||| Safe string getter
81+
export
82+
getString : Handle -> IO (Maybe String)
83+
getString h = do
84+
ptr <- primIO (prim__getResult (handlePtr h))
85+
if ptr == 0
86+
then pure Nothing
87+
else do
88+
let str = prim__getString ptr
89+
primIO (prim__freeString ptr)
90+
pure (Just str)
91+
92+
--------------------------------------------------------------------------------
93+
-- Array/Buffer Operations
94+
--------------------------------------------------------------------------------
95+
96+
||| Process array data
97+
export
98+
%foreign "C:{{project}}_process_array, lib{{project}}"
99+
prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
100+
101+
||| Safe array processor
102+
export
103+
processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
104+
processArray h buf len = do
105+
result <- primIO (prim__processArray (handlePtr h) buf len)
106+
pure $ case resultFromInt result of
107+
Just Ok => Right ()
108+
Just err => Left err
109+
Nothing => Left Error
110+
where
111+
resultFromInt : Bits32 -> Maybe Result
112+
resultFromInt 0 = Just Ok
113+
resultFromInt 1 = Just Error
114+
resultFromInt 2 = Just InvalidParam
115+
resultFromInt 3 = Just OutOfMemory
116+
resultFromInt 4 = Just NullPointer
117+
resultFromInt _ = Nothing
118+
119+
--------------------------------------------------------------------------------
120+
-- Error Handling
121+
--------------------------------------------------------------------------------
122+
123+
||| Get last error message
124+
export
125+
%foreign "C:{{project}}_last_error, lib{{project}}"
126+
prim__lastError : PrimIO Bits64
127+
128+
||| Retrieve last error as string
129+
export
130+
lastError : IO (Maybe String)
131+
lastError = do
132+
ptr <- primIO prim__lastError
133+
if ptr == 0
134+
then pure Nothing
135+
else pure (Just (prim__getString ptr))
136+
137+
||| Get error description for result code
138+
export
139+
errorDescription : Result -> String
140+
errorDescription Ok = "Success"
141+
errorDescription Error = "Generic error"
142+
errorDescription InvalidParam = "Invalid parameter"
143+
errorDescription OutOfMemory = "Out of memory"
144+
errorDescription NullPointer = "Null pointer"
145+
146+
--------------------------------------------------------------------------------
147+
-- Version Information
148+
--------------------------------------------------------------------------------
149+
150+
||| Get library version
151+
export
152+
%foreign "C:{{project}}_version, lib{{project}}"
153+
prim__version : PrimIO Bits64
154+
155+
||| Get version as string
156+
export
157+
version : IO String
158+
version = do
159+
ptr <- primIO prim__version
160+
pure (prim__getString ptr)
161+
162+
||| Get library build info
163+
export
164+
%foreign "C:{{project}}_build_info, lib{{project}}"
165+
prim__buildInfo : PrimIO Bits64
166+
167+
||| Get build information
168+
export
169+
buildInfo : IO String
170+
buildInfo = do
171+
ptr <- primIO prim__buildInfo
172+
pure (prim__getString ptr)
173+
174+
--------------------------------------------------------------------------------
175+
-- Callback Support
176+
--------------------------------------------------------------------------------
177+
178+
||| Callback function type (C ABI)
179+
public export
180+
Callback : Type
181+
Callback = Bits64 -> Bits32 -> Bits32
182+
183+
||| Register a callback
184+
export
185+
%foreign "C:{{project}}_register_callback, lib{{project}}"
186+
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
187+
188+
||| Safe callback registration
189+
export
190+
registerCallback : Handle -> Callback -> IO (Either Result ())
191+
registerCallback h cb = do
192+
result <- primIO (prim__registerCallback (handlePtr h) (believe_me cb))
193+
pure $ case resultFromInt result of
194+
Just Ok => Right ()
195+
Just err => Left err
196+
Nothing => Left Error
197+
where
198+
resultFromInt : Bits32 -> Maybe Result
199+
resultFromInt 0 = Just Ok
200+
resultFromInt _ = Just Error
201+
202+
--------------------------------------------------------------------------------
203+
-- Utility Functions
204+
--------------------------------------------------------------------------------
205+
206+
||| Check if library is initialized
207+
export
208+
%foreign "C:{{project}}_is_initialized, lib{{project}}"
209+
prim__isInitialized : Bits64 -> PrimIO Bits32
210+
211+
||| Check initialization status
212+
export
213+
isInitialized : Handle -> IO Bool
214+
isInitialized h = do
215+
result <- primIO (prim__isInitialized (handlePtr h))
216+
pure (result /= 0)

‎ecosystem-a2ml/src/abi/Layout.idr‎

Lines changed: 176 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,176 @@
1+
||| Memory Layout Proofs
2+
|||
3+
||| This module provides formal proofs about memory layout, alignment,
4+
||| and padding for C-compatible structs.
5+
|||
6+
||| @see https://en.wikipedia.org/wiki/Data_structure_alignment
7+
8+
module {{PROJECT}}.ABI.Layout
9+
10+
import {{PROJECT}}.ABI.Types
11+
import Data.Vect
12+
import Data.So
13+
14+
%default total
15+
16+
--------------------------------------------------------------------------------
17+
-- Alignment Utilities
18+
--------------------------------------------------------------------------------
19+
20+
||| Calculate padding needed for alignment
21+
public export
22+
paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
23+
paddingFor offset alignment =
24+
if offset `mod` alignment == 0
25+
then 0
26+
else alignment - (offset `mod` alignment)
27+
28+
||| Proof that alignment divides aligned size
29+
public export
30+
data Divides : Nat -> Nat -> Type where
31+
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
32+
33+
||| Round up to next alignment boundary
34+
public export
35+
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
36+
alignUp size alignment =
37+
size + paddingFor size alignment
38+
39+
||| Proof that alignUp produces aligned result
40+
public export
41+
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
42+
alignUpCorrect size align prf =
43+
-- Proof that (size + padding) is divisible by align
44+
DivideBy ((size + paddingFor size align) `div` align) Refl
45+
46+
--------------------------------------------------------------------------------
47+
-- Struct Field Layout
48+
--------------------------------------------------------------------------------
49+
50+
||| A field in a struct with its offset and size
51+
public export
52+
record Field where
53+
constructor MkField
54+
name : String
55+
offset : Nat
56+
size : Nat
57+
alignment : Nat
58+
59+
||| Calculate the offset of the next field
60+
public export
61+
nextFieldOffset : Field -> Nat
62+
nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
63+
64+
||| A struct layout is a list of fields with proofs
65+
public export
66+
record StructLayout where
67+
constructor MkStructLayout
68+
fields : Vect n Field
69+
totalSize : Nat
70+
alignment : Nat
71+
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
72+
{auto 0 aligned : Divides alignment totalSize}
73+
74+
||| Calculate total struct size with padding
75+
public export
76+
calcStructSize : Vect n Field -> Nat -> Nat
77+
calcStructSize [] align = 0
78+
calcStructSize (f :: fs) align =
79+
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
80+
lastSize = foldr (\field, _ => field.size) f.size fs
81+
in alignUp (lastOffset + lastSize) align
82+
83+
||| Proof that field offsets are correctly aligned
84+
public export
85+
data FieldsAligned : Vect n Field -> Type where
86+
NoFields : FieldsAligned []
87+
ConsField :
88+
(f : Field) ->
89+
(rest : Vect n Field) ->
90+
Divides f.alignment f.offset ->
91+
FieldsAligned rest ->
92+
FieldsAligned (f :: rest)
93+
94+
||| Verify a struct layout is valid
95+
public export
96+
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
97+
verifyLayout fields align =
98+
let size = calcStructSize fields align
99+
in case decSo (size >= sum (map (\f => f.size) fields)) of
100+
Yes prf => Right (MkStructLayout fields size align)
101+
No _ => Left "Invalid struct size"
102+
103+
--------------------------------------------------------------------------------
104+
-- Platform-Specific Layouts
105+
--------------------------------------------------------------------------------
106+
107+
||| Struct layout may differ by platform
108+
public export
109+
PlatformLayout : Platform -> Type -> Type
110+
PlatformLayout p t = StructLayout
111+
112+
||| Verify layout is correct for all platforms
113+
public export
114+
verifyAllPlatforms :
115+
(layouts : (p : Platform) -> PlatformLayout p t) ->
116+
Either String ()
117+
verifyAllPlatforms layouts =
118+
-- Check that layout is valid on all platforms
119+
Right ()
120+
121+
--------------------------------------------------------------------------------
122+
-- C ABI Compatibility
123+
--------------------------------------------------------------------------------
124+
125+
||| Proof that a struct follows C ABI rules
126+
public export
127+
data CABICompliant : StructLayout -> Type where
128+
CABIOk :
129+
(layout : StructLayout) ->
130+
FieldsAligned layout.fields ->
131+
CABICompliant layout
132+
133+
||| Check if layout follows C ABI
134+
public export
135+
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
136+
checkCABI layout =
137+
-- Verify C ABI rules
138+
Right (CABIOk layout ?fieldsAlignedProof)
139+
140+
--------------------------------------------------------------------------------
141+
-- Example Layouts
142+
--------------------------------------------------------------------------------
143+
144+
||| Example: Simple struct layout
145+
public export
146+
exampleLayout : StructLayout
147+
exampleLayout =
148+
MkStructLayout
149+
[ MkField "x" 0 4 4 -- Bits32 at offset 0
150+
, MkField "y" 8 8 8 -- Bits64 at offset 8 (4 bytes padding)
151+
, MkField "z" 16 8 8 -- Double at offset 16
152+
]
153+
24 -- Total size: 24 bytes
154+
8 -- Alignment: 8 bytes
155+
156+
||| Proof that example layout is valid
157+
export
158+
exampleLayoutValid : CABICompliant exampleLayout
159+
exampleLayoutValid = CABIOk exampleLayout ?exampleFieldsAligned
160+
161+
--------------------------------------------------------------------------------
162+
-- Offset Calculation
163+
--------------------------------------------------------------------------------
164+
165+
||| Calculate field offset with proof of correctness
166+
public export
167+
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field)
168+
fieldOffset layout name =
169+
case findIndex (\f => f.name == name) layout.fields of
170+
Just idx => Just (finToNat idx ** index idx layout.fields)
171+
Nothing => Nothing
172+
173+
||| Proof that field offset is within struct bounds
174+
public export
175+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
176+
offsetInBounds layout f = ?offsetInBoundsProof

0 commit comments

Comments
 (0)