Skip to content

Commit d64b5fc

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#36)
* Add SPDX header to LICENSE and set Cargo.toml license field The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) Make the repo's licensing single and consistent, matching the wokelangiser reference policy and the merged iseriser pattern: - Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md). - Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0, everything else -> MPL-2.0. - READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip. Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the "never use AGPL" estate policy, and the Contributor Covenant CoC. Verified: standards/scripts/check-licence-consistency.sh passes; no residual PMPL/Palimpsest self-claims remain. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Fix Idris2 ABI proofs so they genuinely compile and verify (0.7.0) The src/interface/abi/{Types,Layout,Foreign}.idr files were scaffolded from a template and never compiler-checked. This makes the whole ABI build clean under Idris2 0.7.0 with zero errors and zero warnings, and adds real machine-checked theorems. Buildability: - Moved flat files into the Futharkiser.ABI namespace layout (src/interface/abi/Futharkiser/ABI/{Types,Layout,Foreign}.idr). - Added src/interface/abi/futharkiser-abi.ipkg listing all four modules. Types.idr: - Replaced every `decEq _ _ = No absurd` catch-all (GPUBackend, SOAC, MemorySpace, Result) with explicit off-diagonal cases of the form `decEq X Y = No (\case Refl impossible)`; imported Decidable.Equality. - createHandle now solves the `{auto 0 nonNull : So (ptr /= 0)}` obligation via `choose (ptr /= 0)` instead of leaving it unsolved. - thisPlatform = Linux (was a %runElab block needing ElabReflection). - CPtr now maps each Platform to a concrete Bits type (was the non-existent `Bits : Nat -> Type`). - verifyTransfer same-space cases made explicit (the `s s` non-linear pattern did not compile). Layout.idr: - paddingFor uses `minus alignment (mod offset alignment)` (Nat has no Neg); imported Data.Nat. - Added sound `decDivides` and `decFieldsAligned` decision procedures. - checkCABI now returns a real `FieldsAligned` witness via decFieldsAligned (was the hole `?fieldsAlignedProof`). - verifyLayout supplies both erased auto-implicits (sizeCorrect, aligned) explicitly, gating on decDivides. - offsetInBounds is now `Maybe (So ...)` via choose (the universally quantified `So` return type was unsound). - Concrete gpuBufferDescriptorLayout supplies {sizeCorrect = Oh, aligned = DivideBy 4 Refl} (32 = 4 * 8). - Replaced the false-by-Refl alignUpCorrect with the genuinely provable multipleDivides lemma. - Renamed shadowing implicit binders to clear all warnings. Proofs.idr (new): genuine theorems, all `export`, no holes/escape hatches: - gpuBufferDescriptorCompliant : CABICompliant of the FFI struct, built directly from DivideBy witnesses per field. - descriptorSizeAligned, okIsZero, errorIsOne, okDistinctFromShapeMismatch, f64IsEightBytes. .gitignore: added **/build/, *.ttc, *.ttm for Idris2 artifacts. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: 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 561c574 commit d64b5fc

6 files changed

Lines changed: 287 additions & 31 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
22+
**/build/
23+
*.ttc
24+
*.ttm
25+
2126
# Dependencies
2227
/node_modules/
2328
/vendor/

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

File renamed without changes.

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

Lines changed: 70 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ module Futharkiser.ABI.Layout
2020
import Futharkiser.ABI.Types
2121
import Data.Vect
2222
import Data.So
23+
import Data.Nat
24+
import Decidable.Equality
2325

2426
%default total
2527

@@ -33,7 +35,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
3335
paddingFor offset alignment =
3436
if offset `mod` alignment == 0
3537
then 0
36-
else alignment - (offset `mod` alignment)
38+
else minus alignment (offset `mod` alignment)
3739

3840
||| Proof that alignment divides aligned size
3941
public export
@@ -46,11 +48,16 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4648
alignUp size alignment =
4749
size + paddingFor size alignment
4850

49-
||| Proof that alignUp produces aligned result
51+
||| Any exact multiple of an alignment is divisible by that alignment.
52+
||| This is the soundness core behind alignment: a value laid out as `k`
53+
||| whole alignment units (`k * align`) satisfies the `Divides` relation by
54+
||| construction. (`paddingFor`/`alignUp` are runtime rounding helpers whose
55+
||| general divisibility would require the Euclidean division theorem, which
56+
||| Idris2 `base` does not export; the concrete struct layouts below instead
57+
||| witness divisibility directly via this multiple-of form.)
5058
public export
51-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
52-
alignUpCorrect size align prf =
53-
DivideBy ((size + paddingFor size align) `div` align) Refl
59+
multipleDivides : (k : Nat) -> (align : Nat) -> Divides align (k * align)
60+
multipleDivides k align = DivideBy k Refl
5461

5562
--------------------------------------------------------------------------------
5663
-- GPU Buffer Layout
@@ -75,7 +82,7 @@ record GPUBufferLayout where
7582
||| Compute the GPU buffer layout from an ArrayShape and element type.
7683
||| GPU buffers typically require 128-byte or 256-byte alignment.
7784
public export
78-
gpuBufferLayout : ArrayShape rank -> (elemBytes : Nat) -> (gpuAlignment : Nat) -> GPUBufferLayout
85+
gpuBufferLayout : ArrayShape r -> (elemBytes : Nat) -> (gpuAlignment : Nat) -> GPUBufferLayout
7986
gpuBufferLayout shape elemBytes gpuAlign =
8087
let numElems = totalElements shape
8188
rawBytes = numElems * elemBytes
@@ -104,7 +111,7 @@ data LayoutAligned : GPUBufferLayout -> Type where
104111

105112
||| Verify a GPU buffer layout from an ArrayShape and Futhark element type
106113
public export
107-
verifyGPULayout : ArrayShape rank -> FutharkType -> (gpuAlignment : Nat) ->
114+
verifyGPULayout : ArrayShape r -> FutharkType -> (gpuAlignment : Nat) ->
108115
Either String GPUBufferLayout
109116
verifyGPULayout shape elemType gpuAlign =
110117
let layout = gpuBufferLayout shape (futharkTypeSize elemType) gpuAlign
@@ -142,7 +149,7 @@ record StructLayout where
142149

143150
||| Calculate total struct size with padding
144151
public export
145-
calcStructSize : Vect n Field -> Nat -> Nat
152+
calcStructSize : Vect k Field -> Nat -> Nat
146153
calcStructSize [] align = 0
147154
calcStructSize (f :: fs) align =
148155
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -151,23 +158,56 @@ calcStructSize (f :: fs) align =
151158

152159
||| Proof that field offsets are correctly aligned
153160
public export
154-
data FieldsAligned : Vect n Field -> Type where
161+
data FieldsAligned : Vect k Field -> Type where
155162
NoFields : FieldsAligned []
156163
ConsField :
157164
(f : Field) ->
158-
(rest : Vect n Field) ->
165+
(rest : Vect m Field) ->
159166
Divides f.alignment f.offset ->
160167
FieldsAligned rest ->
161168
FieldsAligned (f :: rest)
162169

163-
||| Verify a struct layout is valid
170+
||| Sound decision procedure for divisibility.
171+
||| For `n = S k`, compute the quotient `q = m `div` (S k)` and check whether
172+
||| `m` is exactly `q * (S k)`. If so, `DivideBy q` witnesses `Divides n m`.
173+
||| `n = 0` divides only `0` (`0 * 0 = 0`); a nonzero `m` is rejected.
164174
public export
165-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
175+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
176+
decDivides Z Z = Just (DivideBy Z Refl)
177+
decDivides Z (S _) = Nothing
178+
decDivides (S k) m =
179+
let q = m `div` (S k)
180+
in case decEq m (q * (S k)) of
181+
Yes prf => Just (DivideBy q prf)
182+
No _ => Nothing
183+
184+
||| Decide, over an entire field vector, whether every field's offset is a
185+
||| multiple of its declared alignment, building the `FieldsAligned` witness.
186+
public export
187+
decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
188+
decFieldsAligned [] = Just NoFields
189+
decFieldsAligned (f :: fs) =
190+
case decDivides f.alignment f.offset of
191+
Nothing => Nothing
192+
Just dvd =>
193+
case decFieldsAligned fs of
194+
Nothing => Nothing
195+
Just rest => Just (ConsField f fs dvd rest)
196+
197+
||| Verify a struct layout is valid.
198+
||| Succeeds only when the computed size dominates the summed field sizes AND
199+
||| the alignment genuinely divides that size (both proofs are supplied
200+
||| explicitly to the erased auto-implicits of `MkStructLayout`).
201+
public export
202+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
166203
verifyLayout fields align =
167204
let size = calcStructSize fields align
168205
in case decSo (size >= sum (map (\f => f.size) fields)) of
169-
Yes prf => Right (MkStructLayout fields size align)
170206
No _ => Left "Invalid struct size"
207+
Yes prf =>
208+
case decDivides align size of
209+
Nothing => Left "Total size is not a multiple of the alignment"
210+
Just dvd => Right (MkStructLayout fields size align {sizeCorrect = prf, aligned = dvd})
171211

172212
--------------------------------------------------------------------------------
173213
-- Futhark Context Layout (opaque struct passed through FFI)
@@ -221,11 +261,15 @@ data CABICompliant : StructLayout -> Type where
221261
FieldsAligned layout.fields ->
222262
CABICompliant layout
223263

224-
||| Check if layout follows C ABI
264+
||| Check if layout follows C ABI.
265+
||| Runs the sound `decFieldsAligned` decision procedure over the layout's
266+
||| fields; only returns `CABIOk` when a genuine `FieldsAligned` witness exists.
225267
public export
226268
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
227269
checkCABI layout =
228-
Right (CABIOk layout ?fieldsAlignedProof)
270+
case decFieldsAligned layout.fields of
271+
Just prf => Right (CABIOk layout prf)
272+
Nothing => Left "Struct fields are not all alignment-correct"
229273

230274
--------------------------------------------------------------------------------
231275
-- GPU Buffer Descriptor (FFI struct)
@@ -247,6 +291,7 @@ gpuBufferDescriptorLayout =
247291
]
248292
32 -- Total size: 32 bytes
249293
8 -- Alignment: 8 bytes
294+
{sizeCorrect = Oh, aligned = DivideBy 4 Refl} -- 32 >= 32, and 32 = 4 * 8
250295

251296
--------------------------------------------------------------------------------
252297
-- Offset Calculation
@@ -260,7 +305,14 @@ fieldOffset layout name =
260305
Just idx => Just (finToNat idx ** index idx layout.fields)
261306
Nothing => Nothing
262307

263-
||| Proof that field offset is within struct bounds
308+
||| Decide whether a field offset+size lies within the struct's total size.
309+
||| This is a genuine decision (it is false in general — a `Field` value need
310+
||| not belong to `layout`), so the result is `Maybe` and is computed via
311+
||| `choose` on the boolean bound.
264312
public export
265-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
266-
offsetInBounds layout f = ?offsetInBoundsProof
313+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
314+
Maybe (So (f.offset + f.size <= layout.totalSize))
315+
offsetInBounds layout f =
316+
case choose (f.offset + f.size <= layout.totalSize) of
317+
Left ok => Just ok
318+
Right _ => Nothing

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

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
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 Futharkiser.
5+
|||
6+
||| These are genuine, fully-elaborated proofs (no holes and no escape
7+
||| hatches of any kind). They pin down two classes of fact:
8+
|||
9+
||| 1. C-ABI compliance of the concrete FFI struct layouts — every field's
10+
||| offset is an exact multiple of its declared alignment. The witnesses
11+
||| are built DIRECTLY as `DivideBy k Refl` (multiplication reduces during
12+
||| type-checking; division does not, so we never route through the
13+
||| `decFieldsAligned` decision procedure here).
14+
|||
15+
||| 2. The result-code encoding contract used across the FFI boundary
16+
||| (`Ok` maps to 0, distinct codes stay distinct).
17+
|||
18+
||| @see Futharkiser.ABI.Layout for the layout definitions
19+
||| @see Futharkiser.ABI.Types for the result-code definitions
20+
21+
module Futharkiser.ABI.Proofs
22+
23+
import Futharkiser.ABI.Types
24+
import Futharkiser.ABI.Layout
25+
import Data.Vect
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- C-ABI compliance of the concrete GPU buffer descriptor struct
31+
--------------------------------------------------------------------------------
32+
33+
||| The GPU buffer descriptor struct passed through the Zig FFI is C-ABI
34+
||| compliant: each of its six fields sits at an offset that is an exact
35+
||| multiple of that field's alignment.
36+
|||
37+
||| data_ptr @ 0 align 8 -> 0 = 0 * 8
38+
||| num_elements @ 8 align 8 -> 8 = 1 * 8
39+
||| element_bytes @ 16 align 4 -> 16 = 4 * 4
40+
||| rank @ 20 align 4 -> 20 = 5 * 4
41+
||| space @ 24 align 4 -> 24 = 6 * 4
42+
||| padding @ 28 align 4 -> 28 = 7 * 4
43+
export
44+
gpuBufferDescriptorCompliant : CABICompliant Layout.gpuBufferDescriptorLayout
45+
gpuBufferDescriptorCompliant =
46+
CABIOk Layout.gpuBufferDescriptorLayout
47+
(ConsField _ _ (DivideBy 0 Refl)
48+
(ConsField _ _ (DivideBy 1 Refl)
49+
(ConsField _ _ (DivideBy 4 Refl)
50+
(ConsField _ _ (DivideBy 5 Refl)
51+
(ConsField _ _ (DivideBy 6 Refl)
52+
(ConsField _ _ (DivideBy 7 Refl)
53+
NoFields))))))
54+
55+
--------------------------------------------------------------------------------
56+
-- Divisibility primitive sanity
57+
--------------------------------------------------------------------------------
58+
59+
||| The total size of the descriptor struct (32 bytes) is an exact multiple of
60+
||| its 8-byte alignment: 32 = 4 * 8.
61+
export
62+
descriptorSizeAligned : Divides 8 32
63+
descriptorSizeAligned = DivideBy 4 Refl
64+
65+
--------------------------------------------------------------------------------
66+
-- Result-code encoding contract
67+
--------------------------------------------------------------------------------
68+
69+
||| `Ok` is the zero result code, as the C FFI boundary relies on.
70+
export
71+
okIsZero : resultToInt Ok = 0
72+
okIsZero = Refl
73+
74+
||| The error code is one, distinct from success.
75+
export
76+
errorIsOne : resultToInt Error = 1
77+
errorIsOne = Refl
78+
79+
||| Success and shape-mismatch encode to genuinely different integers,
80+
||| so callers can discriminate them across the FFI boundary.
81+
export
82+
okDistinctFromShapeMismatch : Not (resultToInt Ok = resultToInt ShapeMismatch)
83+
okDistinctFromShapeMismatch = \case Refl impossible
84+
85+
--------------------------------------------------------------------------------
86+
-- Element-size contract
87+
--------------------------------------------------------------------------------
88+
89+
||| A 64-bit float occupies eight bytes, matching the descriptor's element
90+
||| layout assumptions.
91+
export
92+
f64IsEightBytes : futharkTypeSize F64 = 8
93+
f64IsEightBytes = Refl

0 commit comments

Comments
 (0)