diff --git a/.gitignore b/.gitignore index 73f5db0..3822e8d 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,11 @@ Thumbs.db /dist/ /out/ +# Idris2 build artifacts +**/build/ +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Anvomidaviser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Anvomidaviser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Anvomidaviser/ABI/Layout.idr similarity index 64% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Anvomidaviser/ABI/Layout.idr index e07fb75..5c0944e 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Anvomidaviser/ABI/Layout.idr @@ -14,6 +14,8 @@ module Anvomidaviser.ABI.Layout import Anvomidaviser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -27,7 +29,7 @@ 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 @@ -40,11 +42,25 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat alignUp size alignment = size + paddingFor size alignment -||| Proof that alignUp produces aligned result +||| Sound decision procedure: does n divide m? +||| For n = S k, compute the candidate quotient q = m `div` (S k) and check +||| that q * (S k) recovers m exactly. The equality proof is real (decEq), +||| never assumed. 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 +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z m = Nothing +decDivides (S k) m = + let q = m `div` (S k) in + case decEq m (q * (S k)) of + Yes prf => Just (DivideBy q prf) + No _ => Nothing + +||| Decide whether alignUp produced an aligned result. Returning a universal +||| proof would be unsound (paddingFor uses runtime division, which does not +||| reduce), so we hand back a genuine, checked witness via decDivides. +public export +alignUpDivides : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align)) +alignUpDivides size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Struct Field Layout @@ -76,7 +92,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 @@ -85,23 +101,40 @@ 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) +||| Decide whether every field in a vector is aligned (offset divisible by +||| alignment), building a real FieldsAligned witness if so. +public export +decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: fs) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dv => + case decFieldsAligned fs of + Nothing => Nothing + Just rest => Just (ConsField f fs dv 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 + Right _ => Left "Invalid struct size" + Left szPrf => + case decDivides align size of + Nothing => Left "Total size is not a multiple of the alignment" + Just dv => + Right (MkStructLayout fields size align {sizeCorrect = szPrf} {aligned = dv}) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -136,7 +169,9 @@ data CABICompliant : StructLayout -> Type where 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 C-ABI aligned" -------------------------------------------------------------------------------- -- ISU Element Layouts @@ -160,11 +195,23 @@ technicalElementLayout = ] 16 -- Total size: 16 bytes 4 -- Alignment: 4 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 16 = 4 * 4 ||| Proof that TechnicalElement layout is valid export -technicalElementLayoutValid : CABICompliant technicalElementLayout -technicalElementLayoutValid = CABIOk technicalElementLayout ?techElemFieldsAligned +technicalElementLayoutValid : CABICompliant Layout.technicalElementLayout +technicalElementLayoutValid = + CABIOk Layout.technicalElementLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 8 Refl) + (ConsField _ _ (DivideBy 9 Refl) + (ConsField _ _ (DivideBy 3 Refl) + NoFields)))))))) ||| Layout for ProgramScore struct in the C ABI ||| Fields: total_base (u32), total_goe (i32), deductions (u32), @@ -188,11 +235,26 @@ programScoreLayout = ] 28 -- Total size: 28 bytes 4 -- Alignment: 4 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 7 Refl} -- 28 = 7 * 4 ||| Proof that ProgramScore layout is valid export -programScoreLayoutValid : CABICompliant programScoreLayout -programScoreLayoutValid = CABIOk programScoreLayout ?progScoreFieldsAligned +programScoreLayoutValid : CABICompliant Layout.programScoreLayout +programScoreLayoutValid = + CABIOk Layout.programScoreLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 12 Refl) + (ConsField _ _ (DivideBy 13 Refl) + (ConsField _ _ (DivideBy 14 Refl) + (ConsField _ _ (DivideBy 15 Refl) + (ConsField _ _ (DivideBy 16 Refl) + (ConsField _ _ (DivideBy 17 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + NoFields))))))))))) -------------------------------------------------------------------------------- -- Offset Calculation @@ -206,7 +268,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 lies within the struct bounds. +||| Universally claiming the bound would be unsound (it is false for +||| arbitrary fields), so we return a decision via choose. 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/Anvomidaviser/ABI/Proofs.idr b/src/interface/abi/Anvomidaviser/ABI/Proofs.idr new file mode 100644 index 0000000..330422b --- /dev/null +++ b/src/interface/abi/Anvomidaviser/ABI/Proofs.idr @@ -0,0 +1,77 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked ABI theorems for Anvomidaviser +||| +||| This module collects genuine, compiler-verified proofs about the +||| concrete C-ABI struct layouts and the result-code encoding used at the +||| FFI boundary. Every witness here is built directly so that it reduces +||| during typechecking — no holes, no postulates, no believe_me. + +module Anvomidaviser.ABI.Proofs + +import Anvomidaviser.ABI.Types +import Anvomidaviser.ABI.Layout +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- C-ABI Compliance of Concrete Layouts +-------------------------------------------------------------------------------- + +||| The TechnicalElement struct layout is C-ABI compliant: every field offset +||| is an exact multiple of that field's alignment. Each DivideBy witness is +||| built directly (field.offset = k * field.alignment), since multiplication +||| reduces during typechecking while division does not. +export +technicalElementCompliant : CABICompliant Layout.technicalElementLayout +technicalElementCompliant = + CABIOk Layout.technicalElementLayout + (ConsField _ _ (DivideBy 0 Refl) -- element_type: offset 0 = 0 * 1 + (ConsField _ _ (DivideBy 1 Refl) -- subtype: offset 1 = 1 * 1 + (ConsField _ _ (DivideBy 2 Refl) -- rotation: offset 2 = 2 * 1 + (ConsField _ _ (DivideBy 3 Refl) -- level: offset 3 = 3 * 1 + (ConsField _ _ (DivideBy 1 Refl) -- base_value: offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 8 Refl) -- goe: offset 8 = 8 * 1 + (ConsField _ _ (DivideBy 9 Refl) -- padding: offset 9 = 9 * 1 + (ConsField _ _ (DivideBy 3 Refl) -- goe_value: offset 12 = 3 * 4 + NoFields)))))))) + +||| The ProgramScore struct layout is C-ABI compliant. +export +programScoreCompliant : CABICompliant Layout.programScoreLayout +programScoreCompliant = + CABIOk Layout.programScoreLayout + (ConsField _ _ (DivideBy 0 Refl) -- total_base: offset 0 = 0 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- total_goe: offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 2 Refl) -- deductions: offset 8 = 2 * 4 + (ConsField _ _ (DivideBy 12 Refl) -- pcs_skating_skills: offset 12 = 12 * 1 + (ConsField _ _ (DivideBy 13 Refl) -- pcs_transitions: offset 13 = 13 * 1 + (ConsField _ _ (DivideBy 14 Refl) -- pcs_performance: offset 14 = 14 * 1 + (ConsField _ _ (DivideBy 15 Refl) -- pcs_composition: offset 15 = 15 * 1 + (ConsField _ _ (DivideBy 16 Refl) -- pcs_interpretation: offset 16 = 16 * 1 + (ConsField _ _ (DivideBy 17 Refl) -- padding: offset 17 = 17 * 1 + (ConsField _ _ (DivideBy 5 Refl) -- component_factor: offset 20 = 5 * 4 + (ConsField _ _ (DivideBy 6 Refl) -- total_segment: offset 24 = 6 * 4 + NoFields))))))))))) + +-------------------------------------------------------------------------------- +-- Result-Code Encoding +-------------------------------------------------------------------------------- + +||| The success result encodes to the C integer 0. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| The result-code encoding is injective at the two boundary cases we rely on +||| at the FFI layer: Ok and Error encode to distinct integers. +export +okNotError : Not (resultToInt Ok = resultToInt Error) +okNotError = \case Refl impossible + +||| RuleViolation pins to 5, the highest defined error code. +export +ruleViolationIsFive : resultToInt RuleViolation = 5 +ruleViolationIsFive = Refl diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Anvomidaviser/ABI/Types.idr similarity index 83% rename from src/interface/abi/Types.idr rename to src/interface/abi/Anvomidaviser/ABI/Types.idr index dea1041..b255870 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Anvomidaviser/ABI/Types.idr @@ -15,6 +15,7 @@ module Anvomidaviser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -27,13 +28,10 @@ public export data Platform = Linux | Windows | MacOS | BSD | WASM ||| Compile-time platform detection -||| This will be set during compilation based on target +||| Default target platform; override with compiler flags at the FFI layer. public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- ISU Element Types @@ -194,7 +192,36 @@ DecEq Result where decEq OutOfMemory OutOfMemory = Yes Refl decEq NullPointer NullPointer = Yes Refl decEq RuleViolation RuleViolation = 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 RuleViolation = 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 RuleViolation = 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 RuleViolation = 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 RuleViolation = 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 RuleViolation = No (\case Refl impossible) + decEq RuleViolation Ok = No (\case Refl impossible) + decEq RuleViolation Error = No (\case Refl impossible) + decEq RuleViolation InvalidParam = No (\case Refl impossible) + decEq RuleViolation OutOfMemory = No (\case Refl impossible) + decEq RuleViolation NullPointer = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -210,8 +237,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 @@ -249,10 +278,10 @@ ptrSize MacOS = 64 ptrSize BSD = 64 ptrSize WASM = 32 -||| Pointer type for platform +||| Pointer type for platform (pointer-sized integer) public export CPtr : Platform -> Type -> Type -CPtr p _ = Bits (ptrSize p) +CPtr p _ = CSize p -------------------------------------------------------------------------------- -- Memory Layout Proofs @@ -271,8 +300,6 @@ data HasAlignment : Type -> Nat -> Type where ||| Size of C types (platform-specific) 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 @@ -281,8 +308,6 @@ cSizeOf p _ = ptrSize p `div` 8 ||| Alignment of C types (platform-specific) 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 @@ -308,53 +333,6 @@ public export data ValidPCS : PCSMark -> Type where ValidPCSProof : ValidPCS m --------------------------------------------------------------------------------- --- FFI Declarations --------------------------------------------------------------------------------- - -||| Declare external C functions -||| These will be implemented in Zig FFI -namespace Foreign - - ||| Parse an ISU element code string (e.g. "3Lz+3T") into internal representation - export - %foreign "C:anvomidaviser_parse_element, libanvomidaviser" - prim__parseElement : String -> PrimIO Bits64 - - ||| Score a complete program and return the total segment score - export - %foreign "C:anvomidaviser_score_program, libanvomidaviser" - prim__scoreProgram : Bits64 -> PrimIO Bits32 - - ||| Validate a program against ISU technical rules - export - %foreign "C:anvomidaviser_validate_program, libanvomidaviser" - prim__validateProgram : Bits64 -> PrimIO Bits32 - - ||| Safe wrapper around element parsing - export - parseElement : String -> IO (Maybe Handle) - parseElement code = do - ptr <- primIO (prim__parseElement code) - pure (createHandle ptr) - - ||| Safe wrapper around program scoring - export - scoreProgram : Handle -> IO (Either Result Bits32) - scoreProgram h = do - result <- primIO (prim__scoreProgram (handlePtr h)) - pure (Right result) - - ||| Safe wrapper around program validation - export - validateProgram : Handle -> IO (Either Result Bool) - validateProgram h = do - result <- primIO (prim__validateProgram (handlePtr h)) - pure $ case result of - 0 => Right True -- Program is valid - 1 => Right False -- Program has rule violations - _ => Left Error - -------------------------------------------------------------------------------- -- Verification -------------------------------------------------------------------------------- diff --git a/src/interface/abi/anvomidaviser-abi.ipkg b/src/interface/abi/anvomidaviser-abi.ipkg new file mode 100644 index 0000000..e1dcfcd --- /dev/null +++ b/src/interface/abi/anvomidaviser-abi.ipkg @@ -0,0 +1,4 @@ +-- SPDX-License-Identifier: MPL-2.0 +package anvomidaviser-abi +sourcedir = "." +modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs