diff --git a/.gitignore b/.gitignore index 73f5db0..70ba1d9 100644 --- a/.gitignore +++ b/.gitignore @@ -15,9 +15,14 @@ Thumbs.db /target/ /_build/ /build/ +**/build/ /dist/ /out/ +# Idris2 build artifacts +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Eclexiaiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Eclexiaiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Eclexiaiser/ABI/Layout.idr similarity index 66% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Eclexiaiser/ABI/Layout.idr index 0ce30c6..06c7a42 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Eclexiaiser/ABI/Layout.idr @@ -18,6 +18,8 @@ module Eclexiaiser.ABI.Layout import Eclexiaiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -31,24 +33,38 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat paddingFor offset alignment = if offset `mod` alignment == 0 then 0 - else alignment - (offset `mod` alignment) + else minus alignment (offset `mod` alignment) ||| Proof that alignment divides aligned size public export data Divides : Nat -> Nat -> Type where DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m +||| Decision procedure for divisibility. +||| For n = S j, compute q = m `div` (S j) and check m = q * (S j). +||| Division does not reduce definitionally, so we confirm the candidate +||| witness via decidable equality on the (reducing) multiplication. +public export +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z m = Nothing +decDivides (S j) m = + let q = m `div` (S j) in + case decEq m (q * (S j)) of + Yes prf => Just (DivideBy q prf) + No _ => Nothing + ||| Round up to next alignment boundary public export alignUp : (size : Nat) -> (alignment : Nat) -> Nat alignUp size alignment = size + paddingFor size alignment -||| Proof that alignUp produces aligned result +||| Decide whether alignUp produced a genuine multiple of the alignment. +||| (alignUp is only a multiple of `align` when `align > 0`, so the +||| witness is returned in Maybe rather than asserted unconditionally.) public export -alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align) -alignUpCorrect size align prf = - DivideBy ((size + paddingFor size align) `div` align) Refl +alignUpAligned : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align)) +alignUpAligned size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Struct Field Layout @@ -72,7 +88,7 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment public export record StructLayout where constructor MkStructLayout - fields : Vect n Field + fields : Vect len Field totalSize : Nat alignment : Nat {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))} @@ -80,7 +96,7 @@ record StructLayout where ||| Calculate total struct size with padding public export -calcStructSize : Vect n Field -> Nat -> Nat +calcStructSize : Vect k Field -> Nat -> Nat calcStructSize [] align = 0 calcStructSize (f :: fs) align = let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs @@ -89,23 +105,28 @@ calcStructSize (f :: fs) align = ||| Proof that field offsets are correctly aligned public export -data FieldsAligned : Vect n Field -> Type where +data FieldsAligned : Vect k Field -> Type where NoFields : FieldsAligned [] ConsField : (f : Field) -> - (rest : Vect n Field) -> + (rest : Vect k Field) -> Divides f.alignment f.offset -> FieldsAligned rest -> FieldsAligned (f :: rest) ||| Verify a struct layout is valid public export -verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout +verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout verifyLayout fields align = let size = calcStructSize fields align - in case decSo (size >= sum (map (\f => f.size) fields)) of - Yes prf => Right (MkStructLayout fields size align) - No _ => Left "Invalid struct size" + in case choose (size >= sum (map (\f => f.size) fields)) of + Left szPrf => + case decDivides align size of + Just alPrf => + Right (MkStructLayout fields size align + {sizeCorrect = szPrf} {aligned = alPrf}) + Nothing => Left "Total size is not a multiple of alignment" + Right _ => Left "Invalid struct size" -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -136,11 +157,26 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout +||| Decide whether every field's offset is a multiple of its alignment, +||| building a FieldsAligned witness directly from per-field decDivides. +public export +decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: fs) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dvd => + case decFieldsAligned fs of + Nothing => Nothing + Just rest => Just (ConsField f fs dvd rest) + ||| Check if layout follows C ABI public export checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) checkCABI layout = - Right (CABIOk layout ?fieldsAlignedProof) + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Struct fields are not correctly aligned" -------------------------------------------------------------------------------- -- EnergyMeasurement Layout @@ -165,11 +201,19 @@ energyMeasurementLayout = ] 32 -- Total size: 32 bytes (28 data + 4 padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 32 = 4 * 8 ||| Proof that EnergyMeasurement layout is C-ABI compliant export -energyMeasurementValid : CABICompliant energyMeasurementLayout -energyMeasurementValid = CABIOk energyMeasurementLayout ?energyMeasurementAligned +energyMeasurementValid : CABICompliant Layout.energyMeasurementLayout +energyMeasurementValid = + CABIOk energyMeasurementLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8 + (ConsField _ _ (DivideBy 2 Refl) -- offset 16 = 2 * 8 + (ConsField _ _ (DivideBy 6 Refl) -- offset 24 = 6 * 4 + NoFields)))) -------------------------------------------------------------------------------- -- CarbonQuery Layout @@ -195,11 +239,20 @@ carbonQueryLayout = ] 24 -- Total size: 24 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 3 Refl} -- 24 = 3 * 8 ||| Proof that CarbonQuery layout is C-ABI compliant export -carbonQueryValid : CABICompliant carbonQueryLayout -carbonQueryValid = CABIOk carbonQueryLayout ?carbonQueryAligned +carbonQueryValid : CABICompliant Layout.carbonQueryLayout +carbonQueryValid = + CABIOk carbonQueryLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8 + (ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4 + (ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4 + NoFields))))) -------------------------------------------------------------------------------- -- BudgetEnforcement Layout @@ -226,11 +279,20 @@ budgetEnforcementLayout = ] 40 -- Total size: 40 bytes (36 data + 4 padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 5 Refl} -- 40 = 5 * 8 ||| Proof that BudgetEnforcement layout is C-ABI compliant export -budgetEnforcementValid : CABICompliant budgetEnforcementLayout -budgetEnforcementValid = CABIOk budgetEnforcementLayout ?budgetEnforcementAligned +budgetEnforcementValid : CABICompliant Layout.budgetEnforcementLayout +budgetEnforcementValid = + CABIOk budgetEnforcementLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8 + (ConsField _ _ (DivideBy 2 Refl) -- offset 16 = 2 * 8 + (ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8 + (ConsField _ _ (DivideBy 8 Refl) -- offset 32 = 8 * 4 + NoFields))))) -------------------------------------------------------------------------------- -- Offset Calculation @@ -244,7 +306,12 @@ fieldOffset layout name = Just idx => Just (finToNat idx ** index idx layout.fields) Nothing => Nothing -||| Proof that field offset is within struct bounds +||| Decide whether a field fits within the struct's total size. +||| Returns a witness only when the bound genuinely holds (it is false +||| in general), so the result is wrapped in Maybe. public export -offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize) -offsetInBounds layout f = ?offsetInBoundsProof +offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize)) +offsetInBounds layout f = + case choose (f.offset + f.size <= layout.totalSize) of + Left ok => Just ok + Right _ => Nothing diff --git a/src/interface/abi/Eclexiaiser/ABI/Proofs.idr b/src/interface/abi/Eclexiaiser/ABI/Proofs.idr new file mode 100644 index 0000000..cb73256 --- /dev/null +++ b/src/interface/abi/Eclexiaiser/ABI/Proofs.idr @@ -0,0 +1,80 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked ABI theorems for Eclexiaiser. +||| +||| This module carries the load-bearing correctness proofs for the +||| eclexiaiser ABI: every concrete C-struct layout is proven C-ABI +||| compliant by exhibiting a FieldsAligned witness directly (one +||| DivideBy per field, with field.offset = k * field.alignment, which +||| reduces by multiplication during typechecking), plus a couple of +||| result-code encoding pins. + +module Eclexiaiser.ABI.Proofs + +import Eclexiaiser.ABI.Types +import Eclexiaiser.ABI.Layout +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- C-ABI Compliance of Concrete Struct Layouts +-------------------------------------------------------------------------------- + +||| EnergyMeasurement is C-ABI compliant: all field offsets are multiples +||| of their alignment (0=0*8, 8=1*8, 16=2*8, 24=6*4). +export +energyMeasurementCompliant : CABICompliant Layout.energyMeasurementLayout +energyMeasurementCompliant = + CABIOk Layout.energyMeasurementLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + NoFields)))) + +||| CarbonQuery is C-ABI compliant: offsets 0=0*4, 4=1*4, 8=1*8, 16=4*4, 20=5*4. +export +carbonQueryCompliant : CABICompliant Layout.carbonQueryLayout +carbonQueryCompliant = + CABIOk Layout.carbonQueryLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + NoFields))))) + +||| BudgetEnforcement is C-ABI compliant: offsets 0=0*8, 8=1*8, 16=2*8, +||| 24=3*8, 32=8*4. +export +budgetEnforcementCompliant : CABICompliant Layout.budgetEnforcementLayout +budgetEnforcementCompliant = + CABIOk Layout.budgetEnforcementLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 8 Refl) + NoFields))))) + +-------------------------------------------------------------------------------- +-- Result-Code Encoding Pins +-------------------------------------------------------------------------------- + +||| The success code encodes to zero at the C boundary. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| The budget-exceeded code encodes to 5 (matching the Zig FFI contract). +export +budgetExceededIsFive : resultToInt BudgetExceeded = 5 +budgetExceededIsFive = Refl + +||| Distinct result constructors encode to distinct integers: a concrete +||| instance pinning that Ok (0) and Error (1) are not confusable. +export +okNotError : Not (resultToInt Ok = resultToInt Error) +okNotError = \case Refl impossible diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Eclexiaiser/ABI/Types.idr similarity index 73% rename from src/interface/abi/Types.idr rename to src/interface/abi/Eclexiaiser/ABI/Types.idr index 18268c4..26b3856 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Eclexiaiser/ABI/Types.idr @@ -21,6 +21,7 @@ module Eclexiaiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -33,13 +34,11 @@ public export data Platform = Linux | Windows | MacOS | BSD | WASM ||| Compile-time platform detection -||| This will be set during compilation based on target +||| This will be set during compilation based on target. +||| Defaults to Linux; override via codegen for other targets. public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Result Codes @@ -89,7 +88,62 @@ DecEq Result where decEq BudgetExceeded BudgetExceeded = Yes Refl decEq CarbonLimitExceeded CarbonLimitExceeded = Yes Refl decEq CounterUnavailable CounterUnavailable = Yes Refl - decEq _ _ = No absurd + decEq Ok Error = No (\case Refl impossible) + decEq Ok InvalidParam = No (\case Refl impossible) + decEq Ok OutOfMemory = No (\case Refl impossible) + decEq Ok NullPointer = No (\case Refl impossible) + decEq Ok BudgetExceeded = No (\case Refl impossible) + decEq Ok CarbonLimitExceeded = No (\case Refl impossible) + decEq Ok CounterUnavailable = No (\case Refl impossible) + decEq Error Ok = No (\case Refl impossible) + decEq Error InvalidParam = No (\case Refl impossible) + decEq Error OutOfMemory = No (\case Refl impossible) + decEq Error NullPointer = No (\case Refl impossible) + decEq Error BudgetExceeded = No (\case Refl impossible) + decEq Error CarbonLimitExceeded = No (\case Refl impossible) + decEq Error CounterUnavailable = No (\case Refl impossible) + decEq InvalidParam Ok = No (\case Refl impossible) + decEq InvalidParam Error = No (\case Refl impossible) + decEq InvalidParam OutOfMemory = No (\case Refl impossible) + decEq InvalidParam NullPointer = No (\case Refl impossible) + decEq InvalidParam BudgetExceeded = No (\case Refl impossible) + decEq InvalidParam CarbonLimitExceeded = No (\case Refl impossible) + decEq InvalidParam CounterUnavailable = No (\case Refl impossible) + decEq OutOfMemory Ok = No (\case Refl impossible) + decEq OutOfMemory Error = No (\case Refl impossible) + decEq OutOfMemory InvalidParam = No (\case Refl impossible) + decEq OutOfMemory NullPointer = No (\case Refl impossible) + decEq OutOfMemory BudgetExceeded = No (\case Refl impossible) + decEq OutOfMemory CarbonLimitExceeded = No (\case Refl impossible) + decEq OutOfMemory CounterUnavailable = No (\case Refl impossible) + decEq NullPointer Ok = No (\case Refl impossible) + decEq NullPointer Error = No (\case Refl impossible) + decEq NullPointer InvalidParam = No (\case Refl impossible) + decEq NullPointer OutOfMemory = No (\case Refl impossible) + decEq NullPointer BudgetExceeded = No (\case Refl impossible) + decEq NullPointer CarbonLimitExceeded = No (\case Refl impossible) + decEq NullPointer CounterUnavailable = No (\case Refl impossible) + decEq BudgetExceeded Ok = No (\case Refl impossible) + decEq BudgetExceeded Error = No (\case Refl impossible) + decEq BudgetExceeded InvalidParam = No (\case Refl impossible) + decEq BudgetExceeded OutOfMemory = No (\case Refl impossible) + decEq BudgetExceeded NullPointer = No (\case Refl impossible) + decEq BudgetExceeded CarbonLimitExceeded = No (\case Refl impossible) + decEq BudgetExceeded CounterUnavailable = No (\case Refl impossible) + decEq CarbonLimitExceeded Ok = No (\case Refl impossible) + decEq CarbonLimitExceeded Error = No (\case Refl impossible) + decEq CarbonLimitExceeded InvalidParam = No (\case Refl impossible) + decEq CarbonLimitExceeded OutOfMemory = No (\case Refl impossible) + decEq CarbonLimitExceeded NullPointer = No (\case Refl impossible) + decEq CarbonLimitExceeded BudgetExceeded = No (\case Refl impossible) + decEq CarbonLimitExceeded CounterUnavailable = No (\case Refl impossible) + decEq CounterUnavailable Ok = No (\case Refl impossible) + decEq CounterUnavailable Error = No (\case Refl impossible) + decEq CounterUnavailable InvalidParam = No (\case Refl impossible) + decEq CounterUnavailable OutOfMemory = No (\case Refl impossible) + decEq CounterUnavailable NullPointer = No (\case Refl impossible) + decEq CounterUnavailable BudgetExceeded = No (\case Refl impossible) + decEq CounterUnavailable CarbonLimitExceeded = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -105,8 +159,10 @@ data Handle : Type where ||| Returns Nothing if pointer is null public export createHandle : Bits64 -> Maybe Handle -createHandle 0 = Nothing -createHandle ptr = Just (MkHandle ptr) +createHandle ptr = + case choose (ptr /= 0) of + Left ok => Just (MkHandle ptr {nonNull = ok}) + Right _ => Nothing ||| Extract pointer value from handle public export @@ -247,10 +303,15 @@ ptrSize MacOS = 64 ptrSize BSD = 64 ptrSize WASM = 32 -||| Pointer type for platform +||| Pointer-sized unsigned integer type for a platform. +||| 64-bit platforms use Bits64; 32-bit (WASM) uses Bits32. public export CPtr : Platform -> Type -> Type -CPtr p _ = Bits (ptrSize p) +CPtr Linux _ = Bits64 +CPtr Windows _ = Bits64 +CPtr MacOS _ = Bits64 +CPtr BSD _ = Bits64 +CPtr WASM _ = Bits32 -------------------------------------------------------------------------------- -- Memory Layout Proofs @@ -266,21 +327,20 @@ public export data HasAlignment : Type -> Nat -> Type where AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n -||| Size of C types (platform-specific) +||| Size of C primitive types (platform-specific fallback for pointers). +||| Note: CInt/CSize reduce to Bits32/Bits64, so they are covered by the +||| primitive-type clauses below rather than by separate (unmatchable) +||| type-level-application patterns. public export cSizeOf : (p : Platform) -> (t : Type) -> Nat -cSizeOf p (CInt _) = 4 -cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4 cSizeOf p Bits32 = 4 cSizeOf p Bits64 = 8 cSizeOf p Double = 8 cSizeOf p _ = ptrSize p `div` 8 -||| Alignment of C types (platform-specific) +||| Alignment of C primitive types (platform-specific fallback for pointers). public export cAlignOf : (p : Platform) -> (t : Type) -> Nat -cAlignOf p (CInt _) = 4 -cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4 cAlignOf p Bits32 = 4 cAlignOf p Bits64 = 8 cAlignOf p Double = 8 diff --git a/src/interface/abi/eclexiaiser-abi.ipkg b/src/interface/abi/eclexiaiser-abi.ipkg new file mode 100644 index 0000000..713ac82 --- /dev/null +++ b/src/interface/abi/eclexiaiser-abi.ipkg @@ -0,0 +1,9 @@ +-- SPDX-License-Identifier: MPL-2.0 +package eclexiaiser-abi + +sourcedir = "." + +modules = Eclexiaiser.ABI.Types + , Eclexiaiser.ABI.Layout + , Eclexiaiser.ABI.Foreign + , Eclexiaiser.ABI.Proofs