diff --git a/.gitignore b/.gitignore index 73f5db0..f539f3d 100644 --- a/.gitignore +++ b/.gitignore @@ -15,6 +15,9 @@ Thumbs.db /target/ /_build/ /build/ +**/build/ +*.ttc +*.ttm /dist/ /out/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Atsiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Atsiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Atsiser/ABI/Layout.idr similarity index 71% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Atsiser/ABI/Layout.idr index ddf27df..e678b43 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Atsiser/ABI/Layout.idr @@ -16,6 +16,8 @@ module Atsiser.ABI.Layout import Atsiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -29,24 +31,39 @@ 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 +||| Sound decision procedure: does `n` divide `m`? +||| For n = S k, compute the quotient and check m = q * (S k) by decidable +||| equality. Division does not reduce during typechecking, so the equation +||| is genuinely checked at runtime rather than asserted. +public export +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z _ = Nothing +decDivides (S k) m = + let q = div m (S k) in + case decEq m (q * (S k)) 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 that `alignUp size align` is divisible by `align`. +||| Returns a genuine `Divides` witness when the quotient checks out, and +||| `Nothing` otherwise (e.g. align = 0). A `Refl`-only proof is impossible +||| here because division does not reduce during typechecking. 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 +alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align)) +alignUpCorrect size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Ownership-Annotated Fields @@ -109,7 +126,7 @@ ownedFieldCount layout = length (filter requiresOwnershipTracking (toList layout ||| Calculate total struct size with padding public export -calcStructSize : Vect n Field -> Nat -> Nat +calcStructSize : Vect len Field -> Nat -> Nat calcStructSize [] align = 0 calcStructSize (f :: fs) align = let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs @@ -118,23 +135,30 @@ calcStructSize (f :: fs) align = ||| Proof that field offsets are correctly aligned public export -data FieldsAligned : Vect n Field -> Type where +data FieldsAligned : Vect len Field -> Type where NoFields : FieldsAligned [] ConsField : (f : Field) -> - (rest : Vect n Field) -> + (rest : Vect len Field) -> Divides f.alignment f.offset -> FieldsAligned rest -> FieldsAligned (f :: rest) -||| Verify a struct layout is valid +||| Verify a struct layout is valid. +||| Both erased obligations of `MkStructLayout` are discharged with genuine +||| witnesses: the size bound via `choose`, and `Divides align size` via +||| `decDivides`. If either fails to hold for the computed size, we report an +||| error instead of fabricating a proof. public export -verifyLayout : (name : String) -> (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout +verifyLayout : (name : String) -> (fields : Vect len Field) -> (align : Nat) -> Either String StructLayout verifyLayout name fields align = - let size = calcStructSize fields align - in case decSo (size >= sum (map (\f => f.size) fields)) of - Yes prf => Right (MkStructLayout name fields size align) - No _ => Left "Invalid struct size for \{name}" + let size = calcStructSize fields align in + case choose (size >= sum (map (\f => f.size) fields)) of + Right _ => Left "Invalid struct size for \{name}" + Left szOk => case decDivides align size of + Nothing => Left "Total size of \{name} is not aligned to \{show align}" + Just dvd => Right (MkStructLayout name fields size align + {sizeCorrect = szOk} {aligned = dvd}) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -165,11 +189,25 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout +||| Decide whether every field's offset is aligned to its alignment, +||| building a FieldsAligned witness over the whole vector. +public export +decFieldsAligned : (fields : Vect len Field) -> Maybe (FieldsAligned fields) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: rest) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dvd => case decFieldsAligned rest of + Nothing => Nothing + Just restPrf => Just (ConsField f rest dvd restPrf) + ||| 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 \{layout.structName} has misaligned fields" -------------------------------------------------------------------------------- -- Ownership Graph for Structs @@ -216,6 +254,8 @@ exampleOwnedLayout = ] 16 -- Total size: 16 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 2 Refl} -- 16 = 2 * 8 ||| Example: Layout for a struct with a borrowed pointer. ||| This is what atsiser generates when it finds: @@ -231,6 +271,8 @@ exampleBorrowedLayout = ] 16 -- Total size: 16 bytes (with padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 2 Refl} -- 16 = 2 * 8 -------------------------------------------------------------------------------- -- Offset Calculation @@ -244,7 +286,11 @@ 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's offset+size fits within the struct's total size. +||| Returns a proof when the bound holds, Nothing otherwise (it does not hold +||| in general, so a universally-quantified return type would be unsound). 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/Atsiser/ABI/Proofs.idr b/src/interface/abi/Atsiser/ABI/Proofs.idr new file mode 100644 index 0000000..a971ad7 --- /dev/null +++ b/src/interface/abi/Atsiser/ABI/Proofs.idr @@ -0,0 +1,65 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked theorems about the Atsiser ABI. +||| +||| These theorems pin down properties that the rest of the ABI relies on: +||| * the example struct layouts are genuinely C-ABI compliant +||| (every field offset is a multiple of its alignment), and +||| * the result-code encoding agrees with the C contract. +||| +||| Each compliance witness is built DIRECTLY (one `DivideBy` per field), +||| because multiplication reduces during typechecking while division does +||| not — so these are checked, not asserted. + +module Atsiser.ABI.Proofs + +import Atsiser.ABI.Types +import Atsiser.ABI.Layout +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- Struct Layout Compliance +-------------------------------------------------------------------------------- + +||| `exampleOwnedLayout` follows the C ABI: field `data` at offset 0 (= 0 * 8) +||| and field `len` at offset 8 (= 1 * 8) are both aligned to 8. +export +exampleOwnedCompliant : CABICompliant Layout.exampleOwnedLayout +exampleOwnedCompliant = + CABIOk Layout.exampleOwnedLayout + (ConsField _ _ (DivideBy 0 Refl) -- data: offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 1 Refl) -- len: offset 8 = 1 * 8 + NoFields)) + +||| `exampleBorrowedLayout` follows the C ABI: field `name` at offset 0 (= 0 * 8) +||| aligned to 8, and field `flags` at offset 8 (= 2 * 4) aligned to 4. +export +exampleBorrowedCompliant : CABICompliant Layout.exampleBorrowedLayout +exampleBorrowedCompliant = + CABIOk Layout.exampleBorrowedLayout + (ConsField _ _ (DivideBy 0 Refl) -- name: offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 2 Refl) -- flags: offset 8 = 2 * 4 + NoFields)) + +-------------------------------------------------------------------------------- +-- Result-Code Encoding +-------------------------------------------------------------------------------- + +||| The success code encodes to 0, as the C FFI contract requires. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| The generic-error code encodes to 1, distinct from success. +export +errorIsOne : resultToInt Error = 1 +errorIsOne = Refl + +||| The result encoding is injective on the two codes that the FFI layer +||| branches on most: success and bounds violation map to different integers. +export +okNotBounds : Not (resultToInt Ok = resultToInt BoundsViolation) +okNotBounds = \case Refl impossible diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Atsiser/ABI/Types.idr similarity index 77% rename from src/interface/abi/Types.idr rename to src/interface/abi/Atsiser/ABI/Types.idr index 8401e4b..4c6fd17 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Atsiser/ABI/Types.idr @@ -17,6 +17,7 @@ module Atsiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -29,13 +30,10 @@ public export data Platform = Linux | Windows | MacOS | BSD | WASM ||| Compile-time platform detection -||| This will be set during compilation based on target +||| This is the default target; override with compiler flags as needed. public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Result Codes @@ -81,7 +79,48 @@ DecEq Result where decEq NullPointer NullPointer = Yes Refl decEq OwnershipViolation OwnershipViolation = Yes Refl decEq BoundsViolation BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq Ok BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq Error BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq InvalidParam BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq OutOfMemory BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq NullPointer BoundsViolation = No (\case Refl impossible) + decEq OwnershipViolation Ok = No (\case Refl impossible) + decEq OwnershipViolation Error = No (\case Refl impossible) + decEq OwnershipViolation InvalidParam = No (\case Refl impossible) + decEq OwnershipViolation OutOfMemory = No (\case Refl impossible) + decEq OwnershipViolation NullPointer = No (\case Refl impossible) + decEq OwnershipViolation BoundsViolation = No (\case Refl impossible) + decEq BoundsViolation Ok = No (\case Refl impossible) + decEq BoundsViolation Error = No (\case Refl impossible) + decEq BoundsViolation InvalidParam = No (\case Refl impossible) + decEq BoundsViolation OutOfMemory = No (\case Refl impossible) + decEq BoundsViolation NullPointer = No (\case Refl impossible) + decEq BoundsViolation OwnershipViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Ownership State Machine @@ -165,8 +204,9 @@ 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 @@ -281,9 +321,10 @@ data HasAlignment : Type -> Nat -> Type where ||| Size of C types (platform-specific) public export +||| Note: `CInt p` / `CSize p` are type synonyms that reduce to `Bits32`/`Bits64`, +||| so they are covered by the `Bits32`/`Bits64` cases below rather than matched +||| as constructors (Idris2 cannot pattern-match on a type-level function). 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 @@ -291,9 +332,9 @@ cSizeOf p _ = ptrSize p `div` 8 ||| Alignment of C types (platform-specific) public export +||| As with `cSizeOf`, `CInt`/`CSize` reduce to `Bits32`/`Bits64` and are +||| handled by those cases rather than matched as constructors. 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/atsiser-abi.ipkg b/src/interface/abi/atsiser-abi.ipkg new file mode 100644 index 0000000..3c3df1e --- /dev/null +++ b/src/interface/abi/atsiser-abi.ipkg @@ -0,0 +1,9 @@ +-- SPDX-License-Identifier: MPL-2.0 +package atsiser-abi + +sourcedir = "." + +modules = Atsiser.ABI.Types + , Atsiser.ABI.Layout + , Atsiser.ABI.Foreign + , Atsiser.ABI.Proofs