Skip to content

Commit 9a6a0f7

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + de-vacuify partition/round-trip theorems (#37)
## Idris2 ABI proofs — genuinely compile + machine-checked theorems Part of the family-wide ABI-proofs review, following the merged **iseriser** reference. chapeliser uses a domain-specific proof set (partitions/slices/gather for Chapel distribution). **Systemic fixes** applied (build went from non-compiling to clean), **plus** two theorems that were *vacuously inhabited* and are now genuine — caught by an adversarial verification pass: - `PartitionComplete` (invariant #1, "no items lost/duplicated") bound a **free implicit `n`** disconnected from the partition index, so `IsComplete Refl` typechecked for *any* partition. Now `{n}{k}{p}` are bound so the obligation `sliceSum p.slices = n` is real — an incomplete partition (sum 9, n=10) is rejected. - `RoundTrip` accepted every format unconditionally; re-indexed on `(origLen, decodedLen)` with a real `decodedLen = origLen` obligation (`RoundTrip Bincode 128 64` is now uninhabited). **Verified:** `idris2 --build chapeliser-abi.ipkg` clean (0/0); **negative controls** for both theorems fail to typecheck as required; no `believe_me`/`postulate`/holes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA)_ --------- Co-authored-by: Jonathan D.A. Jewell <paraordinate@yahoo.co.uk> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 72c92e1 commit 9a6a0f7

4 files changed

Lines changed: 228 additions & 8 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ Thumbs.db
1818
/dist/
1919
/out/
2020

21+
# Idris2 build artifacts (anywhere in the tree)
22+
**/build/
23+
*.ttc
24+
*.ttm
25+
2126
# Dependencies
2227
/node_modules/
2328
/vendor/

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

Lines changed: 194 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,194 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Machine-checked proofs over the Chapeliser ABI.
5+
|||
6+
||| These are not runtime tests — they are propositional statements the Idris2
7+
||| type checker must discharge at compile time. If a concrete partition were
8+
||| incomplete, a gather lost results, a slice descriptor were mis-laid-out, or
9+
||| the result-code encoding the Zig FFI depends on were wrong, this module
10+
||| would fail to typecheck and the proof build would go red.
11+
|||
12+
||| Design note on what reduces at the type level: Idris2's `Nat` `div`/`mod`
13+
||| and the `where`-block helpers inside `perItemSlices` do NOT reduce during
14+
||| conversion checking, so we never route a proof through them. Instead the
15+
||| concrete partition/gather witnesses are built from EXPLICIT slice vectors,
16+
||| where `sliceSum`, `allDisjoint`, and `gatherTotal` reduce fully. Record
17+
||| projections of top-level layout values reduce, so the layout pins are `Refl`.
18+
19+
module Chapeliser.ABI.Proofs
20+
21+
import Chapeliser.ABI.Types
22+
import Chapeliser.ABI.Layout
23+
import Data.So
24+
import Data.Vect
25+
import Data.Nat
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- Result-code round-trip: the encoding the Zig FFI depends on.
31+
--------------------------------------------------------------------------------
32+
33+
||| Ok must encode as the C value 0 — the success sentinel every FFI wrapper
34+
||| (`init`, `shutdown`, ...) tests against.
35+
export
36+
okIsZero : resultToInt Ok = 0
37+
okIsZero = Refl
38+
39+
||| NullPointer must encode as the C value 4.
40+
export
41+
nullPointerIsFour : resultToInt NullPointer = 4
42+
nullPointerIsFour = Refl
43+
44+
||| RetryExhausted must encode as the C value 5.
45+
export
46+
retryExhaustedIsFive : resultToInt RetryExhausted = 5
47+
retryExhaustedIsFive = Refl
48+
49+
||| CheckpointError must encode as the C value 6 (the highest code).
50+
export
51+
checkpointErrorIsSix : resultToInt CheckpointError = 6
52+
checkpointErrorIsSix = Refl
53+
54+
--------------------------------------------------------------------------------
55+
-- Slice-descriptor layout: the (start, count) pair crossing the FFI boundary.
56+
--------------------------------------------------------------------------------
57+
58+
||| The canonical slice descriptor is exactly 16 bytes.
59+
export
60+
sliceDescTotalSize : Layout.sliceDescLayout.totalSize = 16
61+
sliceDescTotalSize = Refl
62+
63+
||| `start` lives at offset 0.
64+
export
65+
sliceDescStartOffset : Layout.sliceDescLayout.startOffset = 0
66+
sliceDescStartOffset = Refl
67+
68+
||| `count` lives at offset 8.
69+
export
70+
sliceDescCountOffset : Layout.sliceDescLayout.countOffset = 8
71+
sliceDescCountOffset = Refl
72+
73+
||| The descriptor is 8-byte aligned.
74+
export
75+
sliceDescAlignment : Layout.sliceDescLayout.alignment = 8
76+
sliceDescAlignment = Refl
77+
78+
||| The `count` field begins exactly 8 bytes after `start` — i.e. the two
79+
||| uint64s are adjacent with no padding between them, matching the Rust
80+
||| `(u64, u64)` representation.
81+
export
82+
sliceDescCountFollowsStart :
83+
Layout.sliceDescLayout.countOffset = Layout.sliceDescLayout.startOffset + 8
84+
sliceDescCountFollowsStart = Refl
85+
86+
--------------------------------------------------------------------------------
87+
-- Default checkpoint layout pins.
88+
--------------------------------------------------------------------------------
89+
90+
||| The default checkpoint tag buffer is 64 bytes.
91+
export
92+
checkpointDefaultTagLen : Layout.defaultCheckpointLayout.maxTagLen = 64
93+
checkpointDefaultTagLen = Refl
94+
95+
||| The default checkpoint data buffer is exactly 1 MiB.
96+
export
97+
checkpointDefaultDataLen : Layout.defaultCheckpointLayout.maxDataLen = 1048576
98+
checkpointDefaultDataLen = Refl
99+
100+
--------------------------------------------------------------------------------
101+
-- Partition completeness + disjointness on a concrete, explicit partition.
102+
--------------------------------------------------------------------------------
103+
104+
||| A concrete partition of 10 items across 2 locales, given by an explicit
105+
||| slice vector (not via `perItemSlices`, whose `div`/`mod` do not reduce at
106+
||| the type level). Locale 0 gets items [0,4), locale 1 gets items [4,10).
107+
export
108+
tenAcrossTwo : Partition 10 2
109+
tenAcrossTwo = MkPartition [MkSlice 0 4, MkSlice 4 6]
110+
111+
||| The slices cover all 10 items with none lost or duplicated:
112+
||| 4 + 6 = 10. This is partition completeness (invariant #1).
113+
export
114+
tenAcrossTwoComplete : PartitionComplete Proofs.tenAcrossTwo
115+
tenAcrossTwoComplete = IsComplete Refl
116+
117+
||| The two slices do not overlap: [0,4) and [4,10) are disjoint.
118+
export
119+
tenAcrossTwoDisjoint : PartitionDisjoint Proofs.tenAcrossTwo
120+
tenAcrossTwoDisjoint = IsDisjoint Oh
121+
122+
||| Therefore the partition is valid: complete AND disjoint. This is the full
123+
||| correctness witness the Chapel codegen relies on to place items.
124+
export
125+
tenAcrossTwoValid : ValidPartition Proofs.tenAcrossTwo
126+
tenAcrossTwoValid = MkValid tenAcrossTwoComplete tenAcrossTwoDisjoint
127+
128+
||| A three-locale example to show completeness is not a one-off:
129+
||| [0,3) + [3,6) + [6,10) = 3 + 3 + 4 = 10.
130+
export
131+
tenAcrossThree : Partition 10 3
132+
tenAcrossThree = MkPartition [MkSlice 0 3, MkSlice 3 3, MkSlice 6 4]
133+
134+
export
135+
tenAcrossThreeValid : ValidPartition Proofs.tenAcrossThree
136+
tenAcrossThreeValid =
137+
MkValid (IsComplete Refl) (IsDisjoint Oh)
138+
139+
--------------------------------------------------------------------------------
140+
-- Gather conservation (invariant #2): no results lost when collecting.
141+
--------------------------------------------------------------------------------
142+
143+
||| Gathering per-locale result counts [3, 3, 4] yields exactly 10 outputs —
144+
||| the sum is conserved, matching the 10-item partition above.
145+
export
146+
gatherTenConserved : GatherConservation (MkGatherInput [3, 3, 4]) 10
147+
gatherTenConserved = Conserved Refl
148+
149+
||| An empty gather conserves to zero (degenerate base case).
150+
export
151+
gatherEmptyConserved : GatherConservation (MkGatherInput []) 0
152+
gatherEmptyConserved = Conserved Refl
153+
154+
--------------------------------------------------------------------------------
155+
-- Serialisation length-conservation (invariant #3): decoded length = original.
156+
--------------------------------------------------------------------------------
157+
158+
||| A 128-byte Bincode payload decodes back to exactly 128 bytes. The proof
159+
||| obligation `decodedLen = origLen` is real: `RoundTrip Bincode 128 64` has
160+
||| no inhabitant.
161+
export
162+
bincodeRoundTrips : RoundTrip Bincode 128 128
163+
bincodeRoundTrips = RoundTripOk Bincode Refl
164+
165+
||| The raw (identity) format conserves a 64-byte payload's length.
166+
export
167+
rawRoundTrips : RoundTrip Raw 64 64
168+
rawRoundTrips = RoundTripOk Raw Refl
169+
170+
--------------------------------------------------------------------------------
171+
-- Retry isolation (invariant #4) + item-buffer isolation.
172+
--------------------------------------------------------------------------------
173+
174+
||| Retrying item 3 of a 10-item workload is isolated: 3 < 10, so the retry
175+
||| writes only to result slot 3 and cannot corrupt other items' results.
176+
export
177+
retryItemThreeIsolated : RetryIsolation 3 10
178+
retryItemThreeIsolated = Isolated Oh
179+
180+
||| Item 2's buffer (with 16-byte buffers) starts at byte offset 32 in the
181+
||| contiguous allocation: 2 * 16 = 32.
182+
export
183+
itemTwoOffset : itemOffset 2 16 = 32
184+
itemTwoOffset = Refl
185+
186+
||| Items 0 and 1 occupy non-overlapping 16-byte buffers.
187+
export
188+
buffersZeroOneDisjoint : So (buffersDisjoint 0 1 16 {neq = Oh})
189+
buffersZeroOneDisjoint = Oh
190+
191+
||| Total contiguous memory for 4 buffers of 16 bytes each is 64 bytes.
192+
export
193+
fourBuffersMemory : totalItemMemory 4 16 = 64
194+
fourBuffersMemory = Refl

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

Lines changed: 18 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -134,9 +134,15 @@ sliceSum (s :: ss) = s.count + sliceSum ss
134134

135135
||| Partition completeness: the sum of all slice counts equals the total items.
136136
||| This guarantees no items are lost or duplicated.
137+
|||
138+
||| The index `n` is bound explicitly in the constructor and shared with the
139+
||| `Partition n k` of `p`, so the obligation `sliceSum p.slices = n` is tied to
140+
||| the partition's declared item count. (A free `n` here would be existential —
141+
||| solvable to the actual slice sum — making the proof vacuous.)
137142
public export
138143
data PartitionComplete : (p : Partition n k) -> Type where
139-
IsComplete : (prf : sliceSum p.slices = n) -> PartitionComplete p
144+
IsComplete : {n : Nat} -> {k : Nat} -> {p : Partition n k} ->
145+
(prf : sliceSum p.slices = n) -> PartitionComplete p
140146

141147
||| Two slices do not overlap if one ends before the other starts.
142148
public export
@@ -221,14 +227,18 @@ record SerBuffer where
221227
maxLen : Nat
222228
{auto 0 fits : So (len <= maxLen)}
223229

224-
||| Proof that serialisation round-trips: for any item x,
225-
||| deserialize(serialize(x)) produces a value equivalent to x.
226-
||| This is stated as a type — the proof obligation is discharged
227-
||| by the user's implementation satisfying the contract.
230+
||| Length-conservation witness for serialisation: for a value whose payload
231+
||| is `origLen` bytes, decoding the encoded buffer restores exactly `origLen`
232+
||| bytes (`decodedLen = origLen`). This is the byte-length invariant that
233+
||| actually crosses the Zig/C FFI boundary — the full semantic round-trip of
234+
||| the payload bytes is the FFI implementation's contract, but the length
235+
||| equality is a genuine, machine-checkable obligation here (a mismatched
236+
||| `decodedLen` is rejected). `RoundTripOk` therefore carries a real proof,
237+
||| not an unconditional assertion.
228238
public export
229-
data RoundTrip : (fmt : SerFormat) -> Type where
230-
||| Witness that the format preserves data across serialize/deserialize.
231-
RoundTripOk : (fmt : SerFormat) -> RoundTrip fmt
239+
data RoundTrip : (fmt : SerFormat) -> (origLen : Nat) -> (decodedLen : Nat) -> Type where
240+
RoundTripOk : {origLen : Nat} -> {decodedLen : Nat} -> (fmt : SerFormat) ->
241+
(prf : decodedLen = origLen) -> RoundTrip fmt origLen decodedLen
232242

233243
--------------------------------------------------------------------------------
234244
-- Retry Safety

‎src/interface/abi/chapeliser-abi.ipkg‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Idris2 package for the chapeliser ABI formal proofs.
3+
-- Build/check with: idris2 --build chapeliser-abi.ipkg (from src/interface/abi/)
4+
package chapeliser-abi
5+
6+
sourcedir = "."
7+
8+
modules = Chapeliser.ABI.Types
9+
, Chapeliser.ABI.Layout
10+
, Chapeliser.ABI.Foreign
11+
, Chapeliser.ABI.Proofs

0 commit comments

Comments
 (0)