diff --git a/.gitignore b/.gitignore index 73f5db0..9bb544c 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,11 @@ Thumbs.db /dist/ /out/ +# Idris2 build artefacts (nested ABI package build dirs) +**/build/ +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Oblibeniser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Oblibeniser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Oblibeniser/ABI/Layout.idr similarity index 57% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Oblibeniser/ABI/Layout.idr index 9d61f85..3630940 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Oblibeniser/ABI/Layout.idr @@ -14,6 +14,8 @@ module Oblibeniser.ABI.Layout import Oblibeniser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -27,12 +29,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat paddingFor offset alignment = if offset `mod` alignment == 0 then 0 - else 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 + else minus alignment (offset `mod` alignment) ||| Round up to next alignment boundary public export @@ -40,12 +37,34 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat alignUp size alignment = size + paddingFor size alignment -||| Proof that alignUp produces aligned result +||| Proof that alignment divides aligned size: `m = k * n`. +public export +data Divides : Nat -> Nat -> Type where + DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m + +||| Sound decision procedure for divisibility. Returns a genuine +||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing. +||| Division by zero is undecidable here and yields Nothing. +public export +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z _ = 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 + +||| Sound divisibility check for an aligned size. The general theorem +||| "alignUp size align is always divisible by align" needs div/mod lemmas +||| from Data.Nat and is tracked as residual proof work; here we *decide* it +||| via `decDivides`, which returns a genuine witness when it holds. For the +||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`). +||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot +||| typecheck for symbolic inputs.) public export -alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align) -alignUpCorrect size align prf = - -- Proof that (size + padding) is divisible by align - DivideBy ((size + paddingFor size align) `div` align) Refl +alignUpDivides : (size : Nat) -> (align : Nat) -> + Maybe (Divides align (alignUp size align)) +alignUpDivides size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Struct Field Layout @@ -77,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 @@ -86,23 +105,26 @@ 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 +||| Decide field alignment for every field, building a real `FieldsAligned` +||| witness from per-field divisibility proofs. public export -verifyLayout : (fields : Vect n 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" +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) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -113,14 +135,8 @@ public export PlatformLayout : Platform -> Type -> Type PlatformLayout p t = StructLayout -||| Verify layout is correct for all platforms -public export -verifyAllPlatforms : - (layouts : (p : Platform) -> PlatformLayout p t) -> - Either String () -verifyAllPlatforms layouts = - -- Check that layout is valid on all platforms - Right () +-- `verifyAllLayouts` is defined at the end of this module, after the concrete +-- layouts and `checkCABI` it depends on. -------------------------------------------------------------------------------- -- C ABI Compatibility @@ -134,12 +150,15 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout -||| Check if layout follows C ABI +||| Verify a layout against the C ABI alignment rules, returning a genuine +||| `CABICompliant` proof (built from real per-field divisibility witnesses) +||| or an error when some field offset is misaligned. public export checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) checkCABI layout = - -- Verify C ABI rules - Right (CABIOk layout ?fieldsAlignedProof) + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Field offsets are not correctly aligned for the C ABI" -------------------------------------------------------------------------------- -- AuditEntry Layout (oblibeniser-specific) @@ -171,11 +190,24 @@ auditEntryLayout = ] 64 -- Total size: 64 bytes (with 4 bytes trailing padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 8 Refl} -||| Proof that AuditEntry layout is C-ABI compliant +||| Proof that AuditEntry layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|8, 16|8, 24|8, 32|8, 40|8, 48|8, 56|4. export -auditEntryLayoutValid : CABICompliant auditEntryLayout -auditEntryLayoutValid = CABIOk auditEntryLayout ?auditEntryFieldsAligned +auditEntryLayoutValid : CABICompliant Layout.auditEntryLayout +auditEntryLayoutValid = + CABIOk auditEntryLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 14 Refl) + NoFields)))))))) -------------------------------------------------------------------------------- -- StateSnapshot Layout (oblibeniser-specific) @@ -201,11 +233,21 @@ stateSnapshotLayout = ] 40 -- Total size: 40 bytes (with 4 bytes internal padding after stateSize) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 5 Refl} -||| Proof that StateSnapshot layout is C-ABI compliant +||| Proof that StateSnapshot layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|8, 16|8, 24|4, 32|8. export -stateSnapshotLayoutValid : CABICompliant stateSnapshotLayout -stateSnapshotLayoutValid = CABIOk stateSnapshotLayout ?snapshotFieldsAligned +stateSnapshotLayoutValid : CABICompliant Layout.stateSnapshotLayout +stateSnapshotLayoutValid = + CABIOk stateSnapshotLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 4 Refl) + NoFields))))) -------------------------------------------------------------------------------- -- UndoStack Layout (oblibeniser-specific) @@ -228,25 +270,53 @@ undoStackLayout = ] 24 -- Total size: 24 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 3 Refl} -||| Proof that UndoStack layout is C-ABI compliant +||| Proof that UndoStack layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|4, 12|4, 16|8. export -undoStackLayoutValid : CABICompliant undoStackLayout -undoStackLayoutValid = CABIOk undoStackLayout ?undoStackFieldsAligned +undoStackLayoutValid : CABICompliant Layout.undoStackLayout +undoStackLayoutValid = + CABIOk undoStackLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) -------------------------------------------------------------------------------- -- Offset Calculation -------------------------------------------------------------------------------- -||| Calculate field offset with proof of correctness +||| Look up a field's offset by name in a layout. public export -fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field) +fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field) fieldOffset layout name = case findIndex (\f => f.name == name) layout.fields of - Just idx => Just (finToNat idx ** index idx layout.fields) + 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 a struct's byte bounds, returning a +||| genuine proof when `offset + size <= totalSize`. The previous signature +||| asserted this for *every* field unconditionally, which is false (a field +||| need not belong to the layout); this honest version decides it. +public export +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 + +||| Verify that all oblibeniser concrete layouts are C-ABI compliant. This +||| fails (Left) if any concrete layout is misaligned, rather than asserting +||| it. Each layout's `FieldsAligned` witness is built by `checkCABI`'s sound +||| `decFieldsAligned`. public export -offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize) -offsetInBounds layout f = ?offsetInBoundsProof +verifyAllLayouts : Either String () +verifyAllLayouts = do + _ <- checkCABI auditEntryLayout + _ <- checkCABI stateSnapshotLayout + _ <- checkCABI undoStackLayout + Right () diff --git a/src/interface/abi/Oblibeniser/ABI/Proofs.idr b/src/interface/abi/Oblibeniser/ABI/Proofs.idr new file mode 100644 index 0000000..f1ee9ff --- /dev/null +++ b/src/interface/abi/Oblibeniser/ABI/Proofs.idr @@ -0,0 +1,91 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the oblibeniser ABI. +||| +||| These are not runtime tests — they are propositional statements the Idris2 +||| type checker must discharge at compile time. If any concrete ABI struct +||| layout were misaligned, the result-code encoding wrong, or a decision +||| procedure mis-defined, this module would fail to typecheck and the proof +||| build would go red. +||| +||| The C-ABI compliance witnesses are built directly from per-field +||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`). +||| Multiplication reduces during type checking, so these are fully verified +||| by the compiler; we avoid routing them through `Nat` division, which is a +||| primitive that does not reduce at the type level. + +module Oblibeniser.ABI.Proofs + +import Oblibeniser.ABI.Types +import Oblibeniser.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete reversible-computing FFI struct layouts are C-ABI compliant. +-------------------------------------------------------------------------------- + +||| Every field offset in the AuditEntry layout divides its alignment: +||| 0|8, 8|8, 16|8, 24|8, 32|8, 40|8, 48|8, 56|4. +export +auditEntryCompliant : CABICompliant Layout.auditEntryLayout +auditEntryCompliant = + CABIOk auditEntryLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 14 Refl) + NoFields)))))))) + +||| Every field offset in the StateSnapshot layout divides its alignment: +||| 0|8, 8|8, 16|8, 24|4, 32|8. +export +stateSnapshotCompliant : CABICompliant Layout.stateSnapshotLayout +stateSnapshotCompliant = + CABIOk stateSnapshotLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 4 Refl) + NoFields))))) + +||| Every field offset in the UndoStack layout divides its alignment: +||| 0|8, 8|4, 12|4, 16|8. +export +undoStackCompliant : CABICompliant Layout.undoStackLayout +undoStackCompliant = + CABIOk undoStackLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) + +-------------------------------------------------------------------------------- +-- Result-code encoding: the integer contract the Zig FFI depends on. +-------------------------------------------------------------------------------- + +||| Success is encoded as 0, matching the C convention. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| NotReversible is encoded as 5 — the inverse-computation FFI returns this +||| code and the safe wrappers decode it back to `NotReversible`. +export +notReversibleIsFive : resultToInt NotReversible = 5 +notReversibleIsFive = Refl + +||| InverseProofFailed is encoded as 7 — the central correctness failure code +||| for oblibeniser's reversibility guarantee. +export +inverseProofFailedIsSeven : resultToInt InverseProofFailed = 7 +inverseProofFailedIsSeven = Refl diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Oblibeniser/ABI/Types.idr similarity index 60% rename from src/interface/abi/Types.idr rename to src/interface/abi/Oblibeniser/ABI/Types.idr index 08a1dd2..be45e7e 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Oblibeniser/ABI/Types.idr @@ -15,6 +15,7 @@ module Oblibeniser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -26,14 +27,12 @@ import Data.Vect public export data Platform = Linux | Windows | MacOS | BSD | WASM -||| Compile-time platform detection -||| This will be set during compilation based on target +||| The platform this build targets. Defaults to Linux; the Rust/Zig build +||| layer overrides this via the codegen target selection. (Previously a +||| `%runElab` stub that required ElabReflection and did not compile.) public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Core Result Codes @@ -72,7 +71,9 @@ resultToInt NotReversible = 5 resultToInt AuditViolation = 6 resultToInt InverseProofFailed = 7 -||| Results are decidably equal +||| Results are decidably equal. The off-diagonal cases discharge the +||| disequality explicitly; the previous `decEq _ _ = No absurd` did not +||| compile (no `Uninhabited (x = y)` instance exists for these). public export DecEq Result where decEq Ok Ok = Yes Refl @@ -83,7 +84,62 @@ DecEq Result where decEq NotReversible NotReversible = Yes Refl decEq AuditViolation AuditViolation = Yes Refl decEq InverseProofFailed InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq Ok AuditViolation = No (\case Refl impossible) + decEq Ok InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq Error AuditViolation = No (\case Refl impossible) + decEq Error InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq InvalidParam AuditViolation = No (\case Refl impossible) + decEq InvalidParam InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq OutOfMemory AuditViolation = No (\case Refl impossible) + decEq OutOfMemory InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq NullPointer AuditViolation = No (\case Refl impossible) + decEq NullPointer InverseProofFailed = No (\case Refl impossible) + decEq NotReversible Ok = No (\case Refl impossible) + decEq NotReversible Error = No (\case Refl impossible) + decEq NotReversible InvalidParam = No (\case Refl impossible) + decEq NotReversible OutOfMemory = No (\case Refl impossible) + decEq NotReversible NullPointer = No (\case Refl impossible) + decEq NotReversible AuditViolation = No (\case Refl impossible) + decEq NotReversible InverseProofFailed = No (\case Refl impossible) + decEq AuditViolation Ok = No (\case Refl impossible) + decEq AuditViolation Error = No (\case Refl impossible) + decEq AuditViolation InvalidParam = No (\case Refl impossible) + decEq AuditViolation OutOfMemory = No (\case Refl impossible) + decEq AuditViolation NullPointer = No (\case Refl impossible) + decEq AuditViolation NotReversible = No (\case Refl impossible) + decEq AuditViolation InverseProofFailed = No (\case Refl impossible) + decEq InverseProofFailed Ok = No (\case Refl impossible) + decEq InverseProofFailed Error = No (\case Refl impossible) + decEq InverseProofFailed InvalidParam = No (\case Refl impossible) + decEq InverseProofFailed OutOfMemory = No (\case Refl impossible) + decEq InverseProofFailed NullPointer = No (\case Refl impossible) + decEq InverseProofFailed NotReversible = No (\case Refl impossible) + decEq InverseProofFailed AuditViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -95,12 +151,15 @@ public export data Handle : Type where MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle -||| Safely create a handle from a pointer value -||| Returns Nothing if pointer is null +||| Safely create a handle from a pointer value. Uses `choose` to obtain a +||| real `So (ptr /= 0)` witness for the non-null branch. (Previously +||| `Just (MkHandle ptr)` left the `auto` proof unsolved and did not compile.) 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 @@ -233,113 +292,20 @@ ptrSize MacOS = 64 ptrSize BSD = 64 ptrSize WASM = 32 -||| Pointer type for platform -public export -CPtr : Platform -> Type -> Type -CPtr p _ = Bits (ptrSize p) - --------------------------------------------------------------------------------- --- Memory Layout Proofs --------------------------------------------------------------------------------- - -||| Proof that a type has a specific size -public export -data HasSize : Type -> Nat -> Type where - SizeProof : {0 t : Type} -> {n : Nat} -> HasSize t n - -||| Proof that a type has a specific alignment -public export -data HasAlignment : Type -> Nat -> Type where - AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n - -||| 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 -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 -cAlignOf p _ = ptrSize p `div` 8 - --------------------------------------------------------------------------------- --- Reversible Operation Struct Layout Proofs --------------------------------------------------------------------------------- - -||| StateSnapshot has 5 fields: snapshotId(8) + timestamp(8) + stateHash(8) + -||| stateSize(4) + padding(4) + statePtr(8) = 40 bytes, aligned to 8 -public export -stateSnapshotSize : (p : Platform) -> HasSize StateSnapshot 40 -stateSnapshotSize p = SizeProof - -public export -stateSnapshotAlign : (p : Platform) -> HasAlignment StateSnapshot 8 -stateSnapshotAlign p = AlignProof - -||| AuditEntry has 8 fields laid out for C-ABI compatibility. -||| 7x Bits64 (56 bytes) + 1x Bits32 (4 bytes) + 4 padding = 64 bytes -public export -auditEntrySize : (p : Platform) -> HasSize AuditEntry 64 -auditEntrySize p = SizeProof - -public export -auditEntryAlign : (p : Platform) -> HasAlignment AuditEntry 8 -auditEntryAlign p = AlignProof - -||| UndoStack: stackPtr(8) + depth(4) + maxDepth(4) + topHash(8) = 24 bytes -public export -undoStackSize : (p : Platform) -> HasSize UndoStack 24 -undoStackSize p = SizeProof - -public export -undoStackAlign : (p : Platform) -> HasAlignment UndoStack 8 -undoStackAlign p = AlignProof - --------------------------------------------------------------------------------- --- FFI Declarations --------------------------------------------------------------------------------- - -||| Declare external C functions -||| These will be implemented in Zig FFI -namespace Foreign - - ||| Record a forward operation, returning its operation ID - export - %foreign "C:oblibeniser_record_operation, liboblibeniser" - prim__recordOperation : Bits64 -> Bits64 -> PrimIO Bits64 - - ||| Compute and apply the inverse of an operation - export - %foreign "C:oblibeniser_apply_inverse, liboblibeniser" - prim__applyInverse : Bits64 -> Bits64 -> PrimIO Bits32 - - ||| Safe wrapper around record operation - export - recordOperation : Handle -> Bits64 -> IO (Either Result Bits64) - recordOperation h namePtr = do - result <- primIO (prim__recordOperation (handlePtr h) namePtr) - if result == 0 - then pure (Left Error) - else pure (Right result) - - ||| Safe wrapper around apply inverse - export - applyInverse : Handle -> Bits64 -> IO (Either Result ()) - applyInverse h opId = do - result <- primIO (prim__applyInverse (handlePtr h) opId) - pure $ case result of - 0 => Right () - _ => Left Error +||| Note: the precise C size/alignment guarantees for the reversible-computing +||| structs (StateSnapshot, AuditEntry, UndoStack) are not asserted here via +||| vacuous `HasSize`/`HasAlignment` witnesses (the original scaffold did so +||| with constructors that proved nothing, and also pattern-matched on `Type`, +||| which Idris2 cannot do). Instead they are captured *genuinely* in +||| `Oblibeniser.ABI.Layout` as `StructLayout` values carrying real `Divides` +||| alignment proofs, and discharged as machine-checked theorems in +||| `Oblibeniser.ABI.Proofs` (`auditEntryCompliant`, `stateSnapshotCompliant`, +||| `undoStackCompliant`). + +-- The FFI primitive and safe-wrapper declarations live exclusively in +-- `Oblibeniser.ABI.Foreign`. A duplicate `namespace Foreign` here previously +-- redeclared `prim__applyInverse`/`recordOperation`, which collided with the +-- real declarations once `Foreign` imported `Types` (ambiguous elaboration). -------------------------------------------------------------------------------- -- Verification diff --git a/src/interface/abi/oblibeniser-abi.ipkg b/src/interface/abi/oblibeniser-abi.ipkg new file mode 100644 index 0000000..05368cd --- /dev/null +++ b/src/interface/abi/oblibeniser-abi.ipkg @@ -0,0 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Idris2 package for the oblibeniser ABI formal proofs. +-- Build/check with: idris2 --build oblibeniser-abi.ipkg (from src/interface/abi/) +package oblibeniser-abi + +sourcedir = "." + +modules = Oblibeniser.ABI.Types + , Oblibeniser.ABI.Layout + , Oblibeniser.ABI.Foreign + , Oblibeniser.ABI.Proofs