ABI: make Idris2 proofs genuinely compile + de-vacuify partition/round-trip theorems

.gitignore

@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2 build artifacts (anywhere in the tree)
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/

src/interface/abi/Chapeliser/ABI/Proofs.idr

@@ -0,0 +1,194 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked proofs over the Chapeliser ABI.
+|||
+||| These are not runtime tests — they are propositional statements the Idris2
+||| type checker must discharge at compile time. If a concrete partition were
+||| incomplete, a gather lost results, a slice descriptor were mis-laid-out, or
+||| the result-code encoding the Zig FFI depends on were wrong, this module
+||| would fail to typecheck and the proof build would go red.
+|||
+||| Design note on what reduces at the type level: Idris2's `Nat` `div`/`mod`
+||| and the `where`-block helpers inside `perItemSlices` do NOT reduce during
+||| conversion checking, so we never route a proof through them. Instead the
+||| concrete partition/gather witnesses are built from EXPLICIT slice vectors,
+||| where `sliceSum`, `allDisjoint`, and `gatherTotal` reduce fully. Record
+||| projections of top-level layout values reduce, so the layout pins are `Refl`.
+
+module Chapeliser.ABI.Proofs
+
+import Chapeliser.ABI.Types
+import Chapeliser.ABI.Layout
+import Data.So
+import Data.Vect
+import Data.Nat
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Result-code round-trip: the encoding the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+||| Ok must encode as the C value 0 — the success sentinel every FFI wrapper
+||| (`init`, `shutdown`, ...) tests against.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| NullPointer must encode as the C value 4.
+export
+nullPointerIsFour : resultToInt NullPointer = 4
+nullPointerIsFour = Refl
+
+||| RetryExhausted must encode as the C value 5.
+export
+retryExhaustedIsFive : resultToInt RetryExhausted = 5
+retryExhaustedIsFive = Refl
+
+||| CheckpointError must encode as the C value 6 (the highest code).
+export
+checkpointErrorIsSix : resultToInt CheckpointError = 6
+checkpointErrorIsSix = Refl
+
+--------------------------------------------------------------------------------
+-- Slice-descriptor layout: the (start, count) pair crossing the FFI boundary.
+--------------------------------------------------------------------------------
+
+||| The canonical slice descriptor is exactly 16 bytes.
+export
+sliceDescTotalSize : Layout.sliceDescLayout.totalSize = 16
+sliceDescTotalSize = Refl
+
+||| `start` lives at offset 0.
+export
+sliceDescStartOffset : Layout.sliceDescLayout.startOffset = 0
+sliceDescStartOffset = Refl
+
+||| `count` lives at offset 8.
+export
+sliceDescCountOffset : Layout.sliceDescLayout.countOffset = 8
+sliceDescCountOffset = Refl
+
+||| The descriptor is 8-byte aligned.
+export
+sliceDescAlignment : Layout.sliceDescLayout.alignment = 8
+sliceDescAlignment = Refl
+
+||| The `count` field begins exactly 8 bytes after `start` — i.e. the two
+||| uint64s are adjacent with no padding between them, matching the Rust
+||| `(u64, u64)` representation.
+export
+sliceDescCountFollowsStart :
+  Layout.sliceDescLayout.countOffset = Layout.sliceDescLayout.startOffset + 8
+sliceDescCountFollowsStart = Refl
+
+--------------------------------------------------------------------------------
+-- Default checkpoint layout pins.
+--------------------------------------------------------------------------------
+
+||| The default checkpoint tag buffer is 64 bytes.
+export
+checkpointDefaultTagLen : Layout.defaultCheckpointLayout.maxTagLen = 64
+checkpointDefaultTagLen = Refl
+
+||| The default checkpoint data buffer is exactly 1 MiB.
+export
+checkpointDefaultDataLen : Layout.defaultCheckpointLayout.maxDataLen = 1048576
+checkpointDefaultDataLen = Refl
+
+--------------------------------------------------------------------------------
+-- Partition completeness + disjointness on a concrete, explicit partition.
+--------------------------------------------------------------------------------
+
+||| A concrete partition of 10 items across 2 locales, given by an explicit
+||| slice vector (not via `perItemSlices`, whose `div`/`mod` do not reduce at
+||| the type level). Locale 0 gets items [0,4), locale 1 gets items [4,10).
+export
+tenAcrossTwo : Partition 10 2
+tenAcrossTwo = MkPartition [MkSlice 0 4, MkSlice 4 6]
+
+||| The slices cover all 10 items with none lost or duplicated:
+||| 4 + 6 = 10. This is partition completeness (invariant #1).
+export
+tenAcrossTwoComplete : PartitionComplete Proofs.tenAcrossTwo
+tenAcrossTwoComplete = IsComplete Refl
+
+||| The two slices do not overlap: [0,4) and [4,10) are disjoint.
+export
+tenAcrossTwoDisjoint : PartitionDisjoint Proofs.tenAcrossTwo
+tenAcrossTwoDisjoint = IsDisjoint Oh
+
+||| Therefore the partition is valid: complete AND disjoint. This is the full
+||| correctness witness the Chapel codegen relies on to place items.
+export
+tenAcrossTwoValid : ValidPartition Proofs.tenAcrossTwo
+tenAcrossTwoValid = MkValid tenAcrossTwoComplete tenAcrossTwoDisjoint
+
+||| A three-locale example to show completeness is not a one-off:
+||| [0,3) + [3,6) + [6,10) = 3 + 3 + 4 = 10.
+export
+tenAcrossThree : Partition 10 3
+tenAcrossThree = MkPartition [MkSlice 0 3, MkSlice 3 3, MkSlice 6 4]
+
+export
+tenAcrossThreeValid : ValidPartition Proofs.tenAcrossThree
+tenAcrossThreeValid =
+  MkValid (IsComplete Refl) (IsDisjoint Oh)
+
+--------------------------------------------------------------------------------
+-- Gather conservation (invariant #2): no results lost when collecting.
+--------------------------------------------------------------------------------
+
+||| Gathering per-locale result counts [3, 3, 4] yields exactly 10 outputs —
+||| the sum is conserved, matching the 10-item partition above.
+export
+gatherTenConserved : GatherConservation (MkGatherInput [3, 3, 4]) 10
+gatherTenConserved = Conserved Refl
+
+||| An empty gather conserves to zero (degenerate base case).
+export
+gatherEmptyConserved : GatherConservation (MkGatherInput []) 0
+gatherEmptyConserved = Conserved Refl
+
+--------------------------------------------------------------------------------
+-- Serialisation length-conservation (invariant #3): decoded length = original.
+--------------------------------------------------------------------------------
+
+||| A 128-byte Bincode payload decodes back to exactly 128 bytes. The proof
+||| obligation `decodedLen = origLen` is real: `RoundTrip Bincode 128 64` has
+||| no inhabitant.
+export
+bincodeRoundTrips : RoundTrip Bincode 128 128
+bincodeRoundTrips = RoundTripOk Bincode Refl
+
+||| The raw (identity) format conserves a 64-byte payload's length.
+export
+rawRoundTrips : RoundTrip Raw 64 64
+rawRoundTrips = RoundTripOk Raw Refl
+
+--------------------------------------------------------------------------------
+-- Retry isolation (invariant #4) + item-buffer isolation.
+--------------------------------------------------------------------------------
+
+||| Retrying item 3 of a 10-item workload is isolated: 3 < 10, so the retry
+||| writes only to result slot 3 and cannot corrupt other items' results.
+export
+retryItemThreeIsolated : RetryIsolation 3 10
+retryItemThreeIsolated = Isolated Oh
+
+||| Item 2's buffer (with 16-byte buffers) starts at byte offset 32 in the
+||| contiguous allocation: 2 * 16 = 32.
+export
+itemTwoOffset : itemOffset 2 16 = 32
+itemTwoOffset = Refl
+
+||| Items 0 and 1 occupy non-overlapping 16-byte buffers.
+export
+buffersZeroOneDisjoint : So (buffersDisjoint 0 1 16 {neq = Oh})
+buffersZeroOneDisjoint = Oh
+
+||| Total contiguous memory for 4 buffers of 16 bytes each is 64 bytes.
+export
+fourBuffersMemory : totalItemMemory 4 16 = 64
+fourBuffersMemory = Refl

src/interface/abi/Chapeliser/ABI/Types.idr

@@ -134,9 +134,15 @@ sliceSum (s :: ss) = s.count + sliceSum ss
 
 ||| Partition completeness: the sum of all slice counts equals the total items.
 ||| This guarantees no items are lost or duplicated.
+|||
+||| The index `n` is bound explicitly in the constructor and shared with the
+||| `Partition n k` of `p`, so the obligation `sliceSum p.slices = n` is tied to
+||| the partition's declared item count. (A free `n` here would be existential —
+||| solvable to the actual slice sum — making the proof vacuous.)
 public export
 data PartitionComplete : (p : Partition n k) -> Type where
-  IsComplete : (prf : sliceSum p.slices = n) -> PartitionComplete p
+  IsComplete : {n : Nat} -> {k : Nat} -> {p : Partition n k} ->
+               (prf : sliceSum p.slices = n) -> PartitionComplete p
 
 ||| Two slices do not overlap if one ends before the other starts.
 public export
@@ -221,14 +227,18 @@ record SerBuffer where
   maxLen : Nat
   {auto 0 fits : So (len <= maxLen)}
 
-||| Proof that serialisation round-trips: for any item x,
-||| deserialize(serialize(x)) produces a value equivalent to x.
-||| This is stated as a type — the proof obligation is discharged
-||| by the user's implementation satisfying the contract.
+||| Length-conservation witness for serialisation: for a value whose payload
+||| is `origLen` bytes, decoding the encoded buffer restores exactly `origLen`
+||| bytes (`decodedLen = origLen`). This is the byte-length invariant that
+||| actually crosses the Zig/C FFI boundary — the full semantic round-trip of
+||| the payload bytes is the FFI implementation's contract, but the length
+||| equality is a genuine, machine-checkable obligation here (a mismatched
+||| `decodedLen` is rejected). `RoundTripOk` therefore carries a real proof,
+||| not an unconditional assertion.
 public export
-data RoundTrip : (fmt : SerFormat) -> Type where
-  ||| Witness that the format preserves data across serialize/deserialize.
-  RoundTripOk : (fmt : SerFormat) -> RoundTrip fmt
+data RoundTrip : (fmt : SerFormat) -> (origLen : Nat) -> (decodedLen : Nat) -> Type where
+  RoundTripOk : {origLen : Nat} -> {decodedLen : Nat} -> (fmt : SerFormat) ->
+                (prf : decodedLen = origLen) -> RoundTrip fmt origLen decodedLen
 
 --------------------------------------------------------------------------------
 -- Retry Safety

src/interface/abi/chapeliser-abi.ipkg

@@ -0,0 +1,11 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Idris2 package for the chapeliser ABI formal proofs.
+-- Build/check with:  idris2 --build chapeliser-abi.ipkg   (from src/interface/abi/)
+package chapeliser-abi
+
+sourcedir = "."
+
+modules = Chapeliser.ABI.Types
+        , Chapeliser.ABI.Layout
+        , Chapeliser.ABI.Foreign
+        , Chapeliser.ABI.Proofs