Skip to content

Commit 2ecf551

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#35)
## Idris2 ABI proofs — genuinely compile + machine-checked theorems Part of the family-wide ABI-proofs review. The hand-written ABI did **not** typecheck under Idris2 0.7.0; this makes it real and verified, following the merged **iseriser** reference. **Systemic fixes:** `decEq _ _ = No absurd` → explicit off-diagonal cases; `{auto 0 nonNull}` smart constructors → `choose`-based; `paddingFor` `-` → `minus`; real `decDivides`/`decFieldsAligned` replacing `?fieldsAlignedProof`; honest `offsetInBounds`; `thisPlatform` de-`%runElab`'d; buildable nested layout + ipkg; new `Proofs.idr` with real theorems. **Verified:** `idris2 --build` clean (0/0); adversarial re-verify found 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 ebd58e2 commit 2ecf551

6 files changed

Lines changed: 291 additions & 44 deletions

File tree

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,9 @@ Thumbs.db
1515
/target/
1616
/_build/
1717
/build/
18+
**/build/
19+
*.ttc
20+
*.ttm
1821
/dist/
1922
/out/
2023

src/interface/abi/Foreign.idr renamed to src/interface/abi/Betlangiser/ABI/Foreign.idr

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ module Betlangiser.ABI.Foreign
1818

1919
import Betlangiser.ABI.Types
2020
import Betlangiser.ABI.Layout
21+
import Data.So
2122

2223
%default total
2324

src/interface/abi/Layout.idr renamed to src/interface/abi/Betlangiser/ABI/Layout.idr

Lines changed: 94 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ module Betlangiser.ABI.Layout
1616
import Betlangiser.ABI.Types
1717
import Data.Vect
1818
import Data.So
19+
import Data.Nat
20+
import Decidable.Equality
1921

2022
%default total
2123

@@ -29,24 +31,39 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
2931
paddingFor offset alignment =
3032
if offset `mod` alignment == 0
3133
then 0
32-
else alignment - (offset `mod` alignment)
34+
else minus alignment (offset `mod` alignment)
3335

3436
||| Proof that alignment divides aligned size
3537
public export
3638
data Divides : Nat -> Nat -> Type where
3739
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
3840

41+
||| Sound decision procedure for divisibility.
42+
||| For n = S k, the quotient q = div m (S k) is tested by checking
43+
||| m = q * (S k) via decidable equality on Nat. Division does not reduce
44+
||| during typechecking, so we obtain the witness by an explicit equality test.
45+
public export
46+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
47+
decDivides Z _ = Nothing
48+
decDivides (S k) m =
49+
let q = div m (S k) in
50+
case decEq m (q * (S k)) of
51+
Yes prf => Just (DivideBy q prf)
52+
No _ => Nothing
53+
3954
||| Round up to next alignment boundary
4055
public export
4156
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4257
alignUp size alignment =
4358
size + paddingFor size alignment
4459

45-
||| Proof that alignUp produces aligned result
60+
||| Decide whether alignUp produced an aligned result.
61+
||| Soundly returns a divisibility witness when the rounded-up size is
62+
||| genuinely a multiple of the alignment (it always is for align > 0, but
63+
||| we obtain the witness via the decision procedure rather than asserting it).
4664
public export
47-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
48-
alignUpCorrect size align prf =
49-
DivideBy ((size + paddingFor size align) `div` align) Refl
65+
alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
66+
alignUpCorrect size align = decDivides align (alignUp size align)
5067

5168
--------------------------------------------------------------------------------
5269
-- Struct Field Layout
@@ -70,7 +87,8 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
7087
public export
7188
record StructLayout where
7289
constructor MkStructLayout
73-
fields : Vect n Field
90+
{0 fieldCount : Nat}
91+
fields : Vect fieldCount Field
7492
totalSize : Nat
7593
alignment : Nat
7694
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
@@ -102,7 +120,10 @@ verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructL
102120
verifyLayout fields align =
103121
let size = calcStructSize fields align
104122
in case decSo (size >= sum (map (\f => f.size) fields)) of
105-
Yes prf => Right (MkStructLayout fields size align)
123+
Yes prf =>
124+
case decDivides align size of
125+
Just dvd => Right (MkStructLayout fields size align {sizeCorrect = prf} {aligned = dvd})
126+
Nothing => Left "Total size not aligned"
106127
No _ => Left "Invalid struct size"
107128

108129
--------------------------------------------------------------------------------
@@ -135,6 +156,8 @@ distributionLayout =
135156
]
136157
40 -- Total size: 40 bytes
137158
8 -- Alignment: 8 bytes
159+
{sizeCorrect = Oh}
160+
{aligned = DivideBy 5 Refl}
138161

139162
--------------------------------------------------------------------------------
140163
-- Sample Buffer Layout
@@ -166,6 +189,8 @@ sampleBufferLayout =
166189
]
167190
56 -- Total size: 56 bytes
168191
8 -- Alignment: 8 bytes
192+
{sizeCorrect = Oh}
193+
{aligned = DivideBy 7 Refl}
169194

170195
--------------------------------------------------------------------------------
171196
-- Confidence Interval Layout
@@ -189,6 +214,8 @@ confidenceIntervalLayout =
189214
]
190215
24 -- Total size: 24 bytes
191216
8 -- Alignment: 8 bytes
217+
{sizeCorrect = Oh}
218+
{aligned = DivideBy 3 Refl}
192219

193220
--------------------------------------------------------------------------------
194221
-- Ternary Bool Array Layout
@@ -211,6 +238,8 @@ ternaryArrayLayout =
211238
]
212239
16 -- Total size: 16 bytes
213240
8 -- Alignment: 8 bytes
241+
{sizeCorrect = Oh}
242+
{aligned = DivideBy 2 Refl}
214243

215244
--------------------------------------------------------------------------------
216245
-- Platform-Specific Layouts
@@ -241,26 +270,65 @@ data CABICompliant : StructLayout -> Type where
241270
FieldsAligned layout.fields ->
242271
CABICompliant layout
243272

244-
||| Check if layout follows C ABI
273+
||| Sound decision procedure: build a FieldsAligned witness for a Vect of
274+
||| fields by checking, for each field, that its alignment divides its offset.
275+
||| Returns Nothing if any field is misaligned.
276+
public export
277+
decFieldsAligned : (fields : Vect n Field) -> Maybe (FieldsAligned fields)
278+
decFieldsAligned [] = Just NoFields
279+
decFieldsAligned (f :: fs) =
280+
case decDivides f.alignment f.offset of
281+
Just dvd =>
282+
case decFieldsAligned fs of
283+
Just rest => Just (ConsField f fs dvd rest)
284+
Nothing => Nothing
285+
Nothing => Nothing
286+
287+
||| Check if layout follows C ABI by deciding field alignment soundly.
245288
public export
246289
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
247290
checkCABI layout =
248-
Right (CABIOk layout ?fieldsAlignedProof)
249-
250-
||| Proof that distribution layout is valid
291+
case decFieldsAligned layout.fields of
292+
Just prf => Right (CABIOk layout prf)
293+
Nothing => Left "Struct fields are not correctly aligned"
294+
295+
||| Proof that distribution layout is valid.
296+
||| Each field offset is a literal multiple of its alignment, so the
297+
||| divisibility witnesses are built directly (multiplication reduces during
298+
||| typechecking; division does not).
251299
export
252-
distributionLayoutValid : CABICompliant distributionLayout
253-
distributionLayoutValid = CABIOk distributionLayout ?distributionFieldsAligned
300+
distributionLayoutValid : CABICompliant Layout.distributionLayout
301+
distributionLayoutValid =
302+
CABIOk distributionLayout
303+
(ConsField _ _ (DivideBy 0 Refl)
304+
(ConsField _ _ (DivideBy 1 Refl)
305+
(ConsField _ _ (DivideBy 1 Refl)
306+
(ConsField _ _ (DivideBy 2 Refl)
307+
(ConsField _ _ (DivideBy 3 Refl)
308+
(ConsField _ _ (DivideBy 8 Refl)
309+
(ConsField _ _ (DivideBy 9 Refl) NoFields)))))))
254310

255311
||| Proof that sample buffer layout is valid
256312
export
257-
sampleBufferLayoutValid : CABICompliant sampleBufferLayout
258-
sampleBufferLayoutValid = CABIOk sampleBufferLayout ?sampleBufferFieldsAligned
313+
sampleBufferLayoutValid : CABICompliant Layout.sampleBufferLayout
314+
sampleBufferLayoutValid =
315+
CABIOk sampleBufferLayout
316+
(ConsField _ _ (DivideBy 0 Refl)
317+
(ConsField _ _ (DivideBy 1 Refl)
318+
(ConsField _ _ (DivideBy 2 Refl)
319+
(ConsField _ _ (DivideBy 3 Refl)
320+
(ConsField _ _ (DivideBy 4 Refl)
321+
(ConsField _ _ (DivideBy 5 Refl)
322+
(ConsField _ _ (DivideBy 6 Refl) NoFields)))))))
259323

260324
||| Proof that confidence interval layout is valid
261325
export
262-
confidenceIntervalLayoutValid : CABICompliant confidenceIntervalLayout
263-
confidenceIntervalLayoutValid = CABIOk confidenceIntervalLayout ?confidenceIntervalFieldsAligned
326+
confidenceIntervalLayoutValid : CABICompliant Layout.confidenceIntervalLayout
327+
confidenceIntervalLayoutValid =
328+
CABIOk confidenceIntervalLayout
329+
(ConsField _ _ (DivideBy 0 Refl)
330+
(ConsField _ _ (DivideBy 1 Refl)
331+
(ConsField _ _ (DivideBy 2 Refl) NoFields)))
264332

265333
--------------------------------------------------------------------------------
266334
-- Offset Calculation
@@ -274,7 +342,13 @@ fieldOffset layout name =
274342
Just idx => Just (finToNat idx ** index idx layout.fields)
275343
Nothing => Nothing
276344

277-
||| Proof that field offset is within struct bounds
345+
||| Decide whether a field lies within the struct bounds.
346+
||| This is not universally true for arbitrary fields, so it is decided at
347+
||| runtime via `choose` and only yields the witness when it actually holds.
278348
public export
279-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
280-
offsetInBounds layout f = ?offsetInBoundsProof
349+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
350+
Maybe (So (f.offset + f.size <= layout.totalSize))
351+
offsetInBounds layout f =
352+
case choose (f.offset + f.size <= layout.totalSize) of
353+
Left ok => Just ok
354+
Right _ => Nothing

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

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
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 ABI Theorems for Betlangiser
5+
|||
6+
||| This module collects genuine, machine-checked theorems about the
7+
||| betlangiser ABI: that each concrete C-struct layout is C-ABI compliant
8+
||| (every field offset is a multiple of its alignment), and that the
9+
||| result-code encoding pins the success code to zero.
10+
|||
11+
||| Every proof below reduces by computation alone — no holes, no postulates,
12+
||| no `believe_me`. The divisibility witnesses are built DIRECTLY (each field
13+
||| offset is a literal `k * alignment`, and multiplication reduces during
14+
||| typechecking) rather than via the runtime decision procedure.
15+
16+
module Betlangiser.ABI.Proofs
17+
18+
import Betlangiser.ABI.Types
19+
import Betlangiser.ABI.Layout
20+
import Data.Vect
21+
22+
%default total
23+
24+
--------------------------------------------------------------------------------
25+
-- Layout Compliance Theorems
26+
--------------------------------------------------------------------------------
27+
28+
||| The Distribution C-struct layout is C-ABI compliant: every field offset
29+
||| is an exact multiple of that field's alignment.
30+
||| Offsets/alignments: tag 0/4, _pad0 4/4, param1 8/8, param2 16/8,
31+
||| custom_ptr 24/8, custom_len 32/4, _pad1 36/4.
32+
export
33+
distributionCompliant : CABICompliant Layout.distributionLayout
34+
distributionCompliant =
35+
CABIOk Layout.distributionLayout
36+
(ConsField _ _ (DivideBy 0 Refl)
37+
(ConsField _ _ (DivideBy 1 Refl)
38+
(ConsField _ _ (DivideBy 1 Refl)
39+
(ConsField _ _ (DivideBy 2 Refl)
40+
(ConsField _ _ (DivideBy 3 Refl)
41+
(ConsField _ _ (DivideBy 8 Refl)
42+
(ConsField _ _ (DivideBy 9 Refl) NoFields)))))))
43+
44+
||| The sample-buffer C-struct layout is C-ABI compliant.
45+
||| All seven fields are 8 bytes at offsets 0,8,16,24,32,40,48 with align 8.
46+
export
47+
sampleBufferCompliant : CABICompliant Layout.sampleBufferLayout
48+
sampleBufferCompliant =
49+
CABIOk Layout.sampleBufferLayout
50+
(ConsField _ _ (DivideBy 0 Refl)
51+
(ConsField _ _ (DivideBy 1 Refl)
52+
(ConsField _ _ (DivideBy 2 Refl)
53+
(ConsField _ _ (DivideBy 3 Refl)
54+
(ConsField _ _ (DivideBy 4 Refl)
55+
(ConsField _ _ (DivideBy 5 Refl)
56+
(ConsField _ _ (DivideBy 6 Refl) NoFields)))))))
57+
58+
||| The confidence-interval C-struct layout is C-ABI compliant.
59+
||| Three 8-byte doubles at offsets 0,8,16 with align 8.
60+
export
61+
confidenceIntervalCompliant : CABICompliant Layout.confidenceIntervalLayout
62+
confidenceIntervalCompliant =
63+
CABIOk Layout.confidenceIntervalLayout
64+
(ConsField _ _ (DivideBy 0 Refl)
65+
(ConsField _ _ (DivideBy 1 Refl)
66+
(ConsField _ _ (DivideBy 2 Refl) NoFields)))
67+
68+
||| The ternary-array C-struct layout is C-ABI compliant.
69+
||| Two 8-byte fields at offsets 0,8 with align 8.
70+
export
71+
ternaryArrayCompliant : CABICompliant Layout.ternaryArrayLayout
72+
ternaryArrayCompliant =
73+
CABIOk Layout.ternaryArrayLayout
74+
(ConsField _ _ (DivideBy 0 Refl)
75+
(ConsField _ _ (DivideBy 1 Refl) NoFields))
76+
77+
--------------------------------------------------------------------------------
78+
-- Result-Code Encoding Theorems
79+
--------------------------------------------------------------------------------
80+
81+
||| The success result code encodes to the integer 0, as required by the
82+
||| C-ABI convention (zero means success).
83+
export
84+
okIsZero : resultToInt Ok = 0
85+
okIsZero = Refl
86+
87+
||| The result-code encoding is injective on the two codes that matter most
88+
||| at the boundary: success (0) is distinct from the generic error (1).
89+
||| Pinned here so a future re-ordering of the `Result` enum cannot silently
90+
||| collide success with an error.
91+
export
92+
okNotError : Not (resultToInt Ok = resultToInt Error)
93+
okNotError = \case Refl impossible
94+
95+
--------------------------------------------------------------------------------
96+
-- Ternary Logic Theorems
97+
--------------------------------------------------------------------------------
98+
99+
||| Kleene NOT is self-inverse on the indeterminate value: re-exported as a
100+
||| concrete, fully-applied theorem (no universally-quantified variable) so it
101+
||| witnesses a closed fact about the ABI's Unknown encoding.
102+
export
103+
notUnknownIsUnknown : ternaryNot TUnknown = TUnknown
104+
notUnknownIsUnknown = Refl
105+
106+
||| Kleene AND is annihilated by False regardless of the other operand being
107+
||| the indeterminate value — the strong-falsity law at the ABI boundary.
108+
export
109+
falseAndUnknownIsFalse : ternaryAnd TFalse TUnknown = TFalse
110+
falseAndUnknownIsFalse = Refl

0 commit comments

Comments
 (0)