Skip to content

Commit 695cc51

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#32)
* 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 The src/interface/abi/{Types,Layout,Foreign}.idr files were scaffolded from a template and never compiler-checked. They now build clean under Idris2 0.7.0 with zero errors and zero warnings. Fixes: - Types.idr: replace `%runElab` thisPlatform stub with `thisPlatform = Linux` (ElabReflection was not enabled). - Types.idr: createHandle now obtains a real `So (ptr /= 0)` witness via `choose` instead of leaving the MkHandle auto-implicit unsolved. - Types.idr: add a genuine `DecEq Result` instance with explicit off-diagonal disequality cases (`No (\case Refl impossible)`) — a `No absurd` catch-all does not typecheck. - Layout.idr: paddingFor uses `minus` instead of Nat subtraction (`-`). - Layout.idr: lift record-local `requiredAlloc` (illegal `where` on a record) to a top-level definition. - Layout.idr: interleaved/planar/video layouts and the new mkDim/mkLayout smart constructors decide their `So` extent/stride/coverage obligations with `choose`, returning Maybe, instead of leaving unprovable symbolic auto proofs unsolved. - Layout.idr: checkCompatibility binds n,m as runtime implicits so decEq has access to them. - Layout.idr: add the C-ABI proof machinery (Divides, decDivides, StructLayout, FieldsAligned, decFieldsAligned, CABICompliant, checkCABI, offsetInBounds) plus concrete StructLayout values for halide_buffer_t and halide_dimension_t, with their erased proofs supplied explicitly ({sizeCorrect = Oh}, {aligned = DivideBy k Refl}). checkCABI is a sound decision procedure (no `?fieldsAlignedProof` hole). offsetInBounds returns Maybe (So ...) via choose rather than asserting an unsound universal bound. New machine-checked theorems (src/interface/abi/Halideiser/ABI/Proofs.idr): - halideBufferTCompliant : CABICompliant halideBufferTStruct - halideDimensionTCompliant : CABICompliant halideDimensionTStruct (each built directly from per-field DivideBy k Refl witnesses) - okIsZero, dimensionMismatchIsSeven : result-code encoding pins - avx512Width, float64Bytes : codegen sanity equalities Buildability: - Move flat files into src/interface/abi/Halideiser/ABI/ so paths match the Halideiser.ABI.* namespaces. - Add src/interface/abi/halideiser-abi.ipkg listing all four modules. - .gitignore: ignore **/build/, *.ttc, *.ttm. No believe_me / assert_total / idris_crash / postulate / %hint / holes are used anywhere; every obligation is discharged genuinely. 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 113125a commit 695cc51

6 files changed

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

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

File renamed without changes.

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

Lines changed: 202 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ import Halideiser.ABI.Types
2323
import Data.Vect
2424
import Data.So
2525
import Data.Nat
26+
import Decidable.Equality
2627

2728
%default total
2829

@@ -51,6 +52,15 @@ public export
5152
dimSpan : HalideDimension -> Nat
5253
dimSpan d = d.extent * d.stride
5354

55+
||| Calculate the minimum allocation needed for the given dimensions.
56+
||| This is the max over all dimensions of (extent_i * stride_i).
57+
||| (Previously a record-local `where` definition, which does not compile;
58+
||| lifted to top level so the record's `allocCovers` proof can reference it.)
59+
public export
60+
requiredAlloc : Vect m HalideDimension -> Nat
61+
requiredAlloc [] = 0
62+
requiredAlloc (d :: ds) = max (dimSpan d) (requiredAlloc ds)
63+
5464
--------------------------------------------------------------------------------
5565
-- Halide Buffer Layout
5666
--------------------------------------------------------------------------------
@@ -73,14 +83,6 @@ record HalideBufferLayout (n : Nat) where
7383
allocSize : Nat
7484
||| Proof that allocation covers the full extent
7585
{auto 0 allocCovers : So (allocSize >= requiredAlloc dimensions)}
76-
where
77-
||| Calculate the minimum allocation needed for the given dimensions.
78-
||| This is the product of (extent_i * stride_i) across all dimensions,
79-
||| but more precisely it is max over all dimensions of (extent_i * stride_i).
80-
public export
81-
requiredAlloc : Vect m HalideDimension -> Nat
82-
requiredAlloc [] = 0
83-
requiredAlloc (d :: ds) = max (dimSpan d) (requiredAlloc ds)
8486

8587
||| Total bytes for a buffer layout
8688
public export
@@ -91,6 +93,34 @@ layoutBytes buf = buf.allocSize * pixelBytes buf.elemType
9193
-- Standard Image Layouts
9294
--------------------------------------------------------------------------------
9395

96+
||| Smart constructor for a Halide dimension. The extent/stride positivity
97+
||| proofs cannot be solved for symbolic `Nat`s at the type level, so we
98+
||| decide them at runtime with `choose`, returning Nothing when either is
99+
||| zero. (Previously `MkHalideDimension 0 extent stride` left the erased
100+
||| `extentPos`/`stridePos` auto-implicits unsolved and did not compile.)
101+
public export
102+
mkDim : (mn : Int) -> (extent : Nat) -> (stride : Nat) -> Maybe HalideDimension
103+
mkDim mn extent stride =
104+
case choose (extent > 0) of
105+
Right _ => Nothing
106+
Left ep => case choose (stride > 0) of
107+
Right _ => Nothing
108+
Left sp => Just (MkHalideDimension mn extent stride
109+
{extentPos = ep} {stridePos = sp})
110+
111+
||| Assemble a buffer layout from already-built dimensions and an allocation
112+
||| size, deciding the `allocCovers` coverage bound with `choose`. Returns
113+
||| Nothing when the allocation does not cover the required span. This is an
114+
||| honest decision: the bound is false for under-sized allocations and cannot
115+
||| be asserted for symbolic inputs.
116+
public export
117+
mkLayout : Vect n HalideDimension -> PixelType -> (allocSize : Nat) ->
118+
Maybe (HalideBufferLayout n)
119+
mkLayout dims ptype allocSize =
120+
case choose (allocSize >= requiredAlloc dims) of
121+
Left ok => Just (MkHalideBufferLayout dims ptype allocSize {allocCovers = ok})
122+
Right _ => Nothing
123+
94124
||| Row-major interleaved layout (RGBRGBRGB...).
95125
||| This is the most common layout for 8-bit images.
96126
|||
@@ -99,15 +129,12 @@ layoutBytes buf = buf.allocSize * pixelBytes buf.elemType
99129
||| dim 2 (y): extent=height, stride=width*channels
100130
public export
101131
interleavedLayout : (dim : BufferDimension) -> (ptype : PixelType) ->
102-
HalideBufferLayout 3
103-
interleavedLayout dim ptype =
104-
MkHalideBufferLayout
105-
[ MkHalideDimension 0 dim.channels 1
106-
, MkHalideDimension 0 dim.width dim.channels
107-
, MkHalideDimension 0 dim.height (dim.width * dim.channels)
108-
]
109-
ptype
110-
(dim.width * dim.height * dim.channels)
132+
Maybe (HalideBufferLayout 3)
133+
interleavedLayout dim ptype = do
134+
d0 <- mkDim 0 dim.channels 1
135+
d1 <- mkDim 0 dim.width dim.channels
136+
d2 <- mkDim 0 dim.height (dim.width * dim.channels)
137+
mkLayout [d0, d1, d2] ptype (dim.width * dim.height * dim.channels)
111138

112139
||| Planar layout (all R, then all G, then all B).
113140
||| Common for processing — better SIMD utilisation per channel.
@@ -117,30 +144,24 @@ interleavedLayout dim ptype =
117144
||| dim 2 (channel): extent=channels, stride=width*height
118145
public export
119146
planarLayout : (dim : BufferDimension) -> (ptype : PixelType) ->
120-
HalideBufferLayout 3
121-
planarLayout dim ptype =
122-
MkHalideBufferLayout
123-
[ MkHalideDimension 0 dim.width 1
124-
, MkHalideDimension 0 dim.height dim.width
125-
, MkHalideDimension 0 dim.channels (dim.width * dim.height)
126-
]
127-
ptype
128-
(dim.width * dim.height * dim.channels)
147+
Maybe (HalideBufferLayout 3)
148+
planarLayout dim ptype = do
149+
d0 <- mkDim 0 dim.width 1
150+
d1 <- mkDim 0 dim.height dim.width
151+
d2 <- mkDim 0 dim.channels (dim.width * dim.height)
152+
mkLayout [d0, d1, d2] ptype (dim.width * dim.height * dim.channels)
129153

130154
||| Video buffer layout (4D: x, y, channel, frame).
131155
||| Planar within each frame, frames stored contiguously.
132156
public export
133157
videoLayout : (dim : BufferDimension) -> (ptype : PixelType) ->
134-
HalideBufferLayout 4
135-
videoLayout dim ptype =
136-
MkHalideBufferLayout
137-
[ MkHalideDimension 0 dim.width 1
138-
, MkHalideDimension 0 dim.height dim.width
139-
, MkHalideDimension 0 dim.channels (dim.width * dim.height)
140-
, MkHalideDimension 0 dim.frames (dim.width * dim.height * dim.channels)
141-
]
142-
ptype
143-
(bufferElements dim)
158+
Maybe (HalideBufferLayout 4)
159+
videoLayout dim ptype = do
160+
d0 <- mkDim 0 dim.width 1
161+
d1 <- mkDim 0 dim.height dim.width
162+
d2 <- mkDim 0 dim.channels (dim.width * dim.height)
163+
d3 <- mkDim 0 dim.frames (dim.width * dim.height * dim.channels)
164+
mkLayout [d0, d1, d2, d3] ptype (bufferElements dim)
144165

145166
--------------------------------------------------------------------------------
146167
-- Alignment Utilities
@@ -152,7 +173,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
152173
paddingFor offset alignment =
153174
if offset `mod` alignment == 0
154175
then 0
155-
else alignment - (offset `mod` alignment)
176+
else minus alignment (offset `mod` alignment)
156177

157178
||| Round up to next alignment boundary
158179
public export
@@ -212,7 +233,7 @@ data LayoutCompatible : HalideBufferLayout n -> HalideBufferLayout m -> Type whe
212233

213234
||| Verify two layouts are compatible for pipeline stage connection
214235
public export
215-
checkCompatibility : HalideBufferLayout n -> HalideBufferLayout m ->
236+
checkCompatibility : {n, m : Nat} -> HalideBufferLayout n -> HalideBufferLayout m ->
216237
Either String (n = m)
217238
checkCompatibility a b =
218239
case decEq n m of
@@ -294,3 +315,146 @@ halideDimensionTSize = 16
294315
public export
295316
halideDimensionTAlign : Nat
296317
halideDimensionTAlign = 4
318+
319+
--------------------------------------------------------------------------------
320+
-- C ABI Alignment Proof Machinery
321+
--------------------------------------------------------------------------------
322+
323+
||| Offset for the next field after `f`, rounded up to `f`'s alignment.
324+
public export
325+
nextFieldOffset : Field -> Nat
326+
nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
327+
328+
||| Proof that `n` divides `m`: `m = k * n`.
329+
public export
330+
data Divides : Nat -> Nat -> Type where
331+
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
332+
333+
||| Sound decision procedure for divisibility. Returns a genuine `Divides n m`
334+
||| witness when `n` evenly divides `m`, otherwise Nothing. Division by zero is
335+
||| undecidable here and yields Nothing.
336+
public export
337+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
338+
decDivides Z _ = Nothing
339+
decDivides (S k) m =
340+
let q = m `div` (S k) in
341+
case decEq m (q * (S k)) of
342+
Yes prf => Just (DivideBy q prf)
343+
No _ => Nothing
344+
345+
||| A C-ABI struct layout: a vector of fields with a total size and alignment,
346+
||| carrying erased proofs that the size covers all fields and that the
347+
||| alignment divides the total size.
348+
public export
349+
record StructLayout where
350+
constructor MkStructLayout
351+
fields : Vect n Field
352+
totalSize : Nat
353+
alignment : Nat
354+
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
355+
{auto 0 aligned : Divides alignment totalSize}
356+
357+
||| C-ABI `StructLayout` for `halide_buffer_t` (8 fields, 56 bytes, align 8).
358+
public export
359+
halideBufferTStruct : StructLayout
360+
halideBufferTStruct =
361+
MkStructLayout
362+
[ MkField "device" 0 8 8
363+
, MkField "device_interface" 8 8 8
364+
, MkField "host" 16 8 8
365+
, MkField "flags" 24 8 8
366+
, MkField "type" 32 4 4
367+
, MkField "dimensions" 36 4 4
368+
, MkField "dim" 40 8 8
369+
, MkField "padding" 48 8 8
370+
]
371+
56
372+
8
373+
{sizeCorrect = Oh}
374+
{aligned = DivideBy 7 Refl}
375+
376+
||| C-ABI `StructLayout` for `halide_dimension_t` (4 fields, 16 bytes, align 4).
377+
public export
378+
halideDimensionTStruct : StructLayout
379+
halideDimensionTStruct =
380+
MkStructLayout
381+
[ MkField "min" 0 4 4
382+
, MkField "extent" 4 4 4
383+
, MkField "stride" 8 4 4
384+
, MkField "flags" 12 4 4
385+
]
386+
16
387+
4
388+
{sizeCorrect = Oh}
389+
{aligned = DivideBy 4 Refl}
390+
391+
||| Proof that every field offset in a layout is correctly aligned.
392+
public export
393+
data FieldsAligned : Vect k Field -> Type where
394+
NoFields : FieldsAligned []
395+
ConsField :
396+
(f : Field) ->
397+
(rest : Vect k Field) ->
398+
Divides f.alignment f.offset ->
399+
FieldsAligned rest ->
400+
FieldsAligned (f :: rest)
401+
402+
||| Decide field alignment for every field, building a real `FieldsAligned`
403+
||| witness from per-field divisibility proofs.
404+
public export
405+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
406+
decFieldsAligned [] = Just NoFields
407+
decFieldsAligned (f :: fs) =
408+
case decDivides f.alignment f.offset of
409+
Nothing => Nothing
410+
Just dvd => case decFieldsAligned fs of
411+
Nothing => Nothing
412+
Just rest => Just (ConsField f fs dvd rest)
413+
414+
||| Proof that a struct layout follows C ABI alignment rules.
415+
public export
416+
data CABICompliant : StructLayout -> Type where
417+
CABIOk :
418+
(layout : StructLayout) ->
419+
FieldsAligned layout.fields ->
420+
CABICompliant layout
421+
422+
||| Verify a layout against the C ABI alignment rules, returning a genuine
423+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
424+
||| or an error when some field offset is misaligned. (Previously a hole
425+
||| `?fieldsAlignedProof`; now a sound decision procedure.)
426+
public export
427+
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
428+
checkCABI layout =
429+
case decFieldsAligned layout.fields of
430+
Just prf => Right (CABIOk layout prf)
431+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
432+
433+
||| Verify that both halide C structs are C-ABI compliant. Fails (Left) if any
434+
||| concrete layout is misaligned, rather than asserting it.
435+
public export
436+
verifyAllStructLayouts : Either String ()
437+
verifyAllStructLayouts = do
438+
_ <- checkCABI halideBufferTStruct
439+
_ <- checkCABI halideDimensionTStruct
440+
Right ()
441+
442+
||| Look up a field's offset by name in a layout.
443+
public export
444+
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
445+
fieldOffset layout name =
446+
case findIndex (\f => f.name == name) layout.fields of
447+
Just idx => Just (finToNat idx, index idx layout.fields)
448+
Nothing => Nothing
449+
450+
||| Decide whether a field lies within a struct's byte bounds, returning a
451+
||| genuine proof when `offset + size <= totalSize`. The previous template
452+
||| signature asserted this for *every* field unconditionally, which is false
453+
||| (a field need not belong to the layout); this honest version decides it.
454+
public export
455+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
456+
Maybe (So (f.offset + f.size <= layout.totalSize))
457+
offsetInBounds layout f =
458+
case choose (f.offset + f.size <= layout.totalSize) of
459+
Left ok => Just ok
460+
Right _ => Nothing

0 commit comments

Comments
 (0)