Skip to content

Commit 2bdfea4

Browse files
claudeclaude
committed
feat(abi): prove schedule equivalence for loop split (Layer 2)
Add Halideiser.ABI.Semantics, a machine-checked proof of Halide's headline guarantee: a schedule changes only HOW a computation runs, never WHAT it computes. Models a 1-D pipeline stage as a pointwise f : Nat -> Nat over the iteration domain range n. Defines unscheduled execution (runFlat) and the split schedule (runSplit: outer blocks of inner iterations with index reconstruction o*inner + i). Theorem splitEnumerates proves runSplit f outer inner = runFlat f (outer*inner) for ALL f, outer, inner, via structural lemmas (rangeAppend, concatBlocksSnoc, runInnerAsFlat). SplitEquivalent wraps this as a proposition with a single equality-demanding constructor; splitPreservesResult inhabits it universally; certifySplitSound ties the Ok verdict to the equivalence. Controls: positive (doubleSplit3x4Equivalent + Refl on the concrete extent-12 case) and negative (dropLastNotEquivalent: a work-dropping schedule is machine-checked Not equal to the flat run). Non-vacuity confirmed adversarially -- false proofs (drop-last equivalence; wrong 2x4 factors vs extent 12) are rejected by idris2. No believe_me / postulate / assert_total / holes. Builds clean (exit 0, zero warnings) under Idris2 0.7.0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent e190e0f commit 2bdfea4

2 files changed

Lines changed: 274 additions & 0 deletions

File tree

‎src/interface/abi/Halideiser/ABI/Semantics.idr‎

Lines changed: 273 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,273 @@
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+
||| Flagship semantic proof for Halideiser: SCHEDULE EQUIVALENCE.
5+
|||
6+
||| Halide's central guarantee is that a *schedule* changes only HOW a
7+
||| computation executes (loop order, tiling, splitting), never WHAT it
8+
||| computes. This module makes that guarantee machine-checked for the
9+
||| canonical schedule transformation: the loop SPLIT.
10+
|||
11+
||| Domain model
12+
||| ------------
13+
||| A 1-D pipeline stage is a pure pointwise function `f : Nat -> Nat`
14+
||| applied at every index of an iteration domain `[0 .. n-1]`.
15+
|||
16+
||| * unscheduled execution : evaluate f at the flat index list
17+
||| `range n = [0,1,...,n-1]` in order.
18+
||| * scheduled (split f=k) : split the domain into `outer` blocks of
19+
||| `inner` iterations (n = outer * inner),
20+
||| run the nested loop, and reconstruct each
21+
||| global index as `o*inner + i`.
22+
|||
23+
||| Headline property (`SplitEquivalent`): for every stage `f` and every
24+
||| split `(outer, inner)`, the scheduled result equals the unscheduled
25+
||| result over the domain of size `outer * inner`. This is a genuine,
26+
||| non-vacuous theorem: the proof rests on a structural lemma that the
27+
||| split enumeration reproduces the flat index enumeration exactly.
28+
|||
29+
||| The bad case (a schedule that silently REORDERS or DROPS work and so
30+
||| changes the result) has NO inhabitant of `SplitEquivalent`: the
31+
||| negative control exhibits a concrete fake "schedule" whose output
32+
||| differs, and proves it is `Not` equivalent.
33+
module Halideiser.ABI.Semantics
34+
35+
import Halideiser.ABI.Types
36+
import Data.Nat
37+
import Data.List
38+
import Decidable.Equality
39+
40+
%default total
41+
42+
--------------------------------------------------------------------------------
43+
-- Iteration domain: the flat index list executed by the unscheduled loop
44+
--------------------------------------------------------------------------------
45+
46+
||| `range n = [0, 1, ..., n-1]` — the iteration domain of a 1-D stage.
47+
public export
48+
range : Nat -> List Nat
49+
range Z = []
50+
range (S k) = range k ++ [k]
51+
52+
||| Unscheduled execution: apply the pointwise stage `f` at every index.
53+
public export
54+
runFlat : (f : Nat -> Nat) -> (n : Nat) -> List Nat
55+
runFlat f n = map f (range n)
56+
57+
--------------------------------------------------------------------------------
58+
-- The SPLIT schedule
59+
--------------------------------------------------------------------------------
60+
61+
||| Reconstruct the global index from an (outer, inner) loop pair.
62+
||| This is exactly Halide's `split(x, xo, xi, inner)` index arithmetic:
63+
||| the original index is `xo * inner + xi`.
64+
public export
65+
splitIndex : (inner : Nat) -> (o : Nat) -> (i : Nat) -> Nat
66+
splitIndex inner o i = o * inner + i
67+
68+
||| Run one inner block: for a fixed outer `o`, apply `f` at every inner
69+
||| index `i in [0 .. inner-1]`, reconstructing the global index each time.
70+
public export
71+
runInner : (f : Nat -> Nat) -> (inner : Nat) -> (o : Nat) -> List Nat
72+
runInner f inner o = map (\i => f (splitIndex inner o i)) (range inner)
73+
74+
||| Concatenate a list of blocks left-to-right. Defined by explicit
75+
||| structural recursion (NOT `concatMap`/`foldl`) so it reduces cleanly
76+
||| during proof: `concatBlocks (b :: bs) = b ++ concatBlocks bs`.
77+
public export
78+
concatBlocks : List (List a) -> List a
79+
concatBlocks [] = []
80+
concatBlocks (b :: bs) = b ++ concatBlocks bs
81+
82+
||| Scheduled execution under `split` with `outer` blocks of `inner`
83+
||| iterations each: concatenate the inner blocks in outer order.
84+
public export
85+
runSplit : (f : Nat -> Nat) -> (outer : Nat) -> (inner : Nat) -> List Nat
86+
runSplit f outer inner =
87+
concatBlocks (map (runInner f inner) (range outer))
88+
89+
--------------------------------------------------------------------------------
90+
-- Structural lemmas about `range` under splitting
91+
--------------------------------------------------------------------------------
92+
93+
||| `map` distributes over `++`. (Local, total; avoids relying on the
94+
||| exact library lemma name.)
95+
mapAppendL : (g : a -> b) -> (xs, ys : List a) ->
96+
map g (xs ++ ys) = map g xs ++ map g ys
97+
mapAppendL g [] ys = Refl
98+
mapAppendL g (x :: xs) ys = cong (g x ::) (mapAppendL g xs ys)
99+
100+
||| `map` fuses: mapping `g` then `h` is mapping `(h . g)`.
101+
mapFusionL : (h : b -> c) -> (g : a -> b) -> (xs : List a) ->
102+
map h (map g xs) = map (\x => h (g x)) xs
103+
mapFusionL h g [] = Refl
104+
mapFusionL h g (x :: xs) = cong (h (g x) ::) (mapFusionL h g xs)
105+
106+
||| `concatBlocks` distributes over `++` of block-lists.
107+
concatBlocksAppend : (xs, ys : List (List a)) ->
108+
concatBlocks (xs ++ ys)
109+
= concatBlocks xs ++ concatBlocks ys
110+
concatBlocksAppend [] ys = Refl
111+
concatBlocksAppend (b :: bs) ys =
112+
rewrite concatBlocksAppend bs ys in
113+
appendAssociative b (concatBlocks bs) (concatBlocks ys)
114+
115+
||| Peel the last block: `concatBlocks (bs ++ [b]) = concatBlocks bs ++ b`.
116+
concatBlocksSnoc : (bs : List (List a)) -> (b : List a) ->
117+
concatBlocks (bs ++ [b]) = concatBlocks bs ++ b
118+
concatBlocksSnoc bs b =
119+
rewrite concatBlocksAppend bs [b] in
120+
cong (concatBlocks bs ++) (appendNilRightNeutral b)
121+
122+
||| Decompose a range at an addition point:
123+
||| `range (a + b) = range a ++ map (+ a) (range b)`.
124+
||| The new block `[a, a+1, ..., a+b-1]` is exactly the old indices of
125+
||| `range b` shifted up by `a`. Proof by induction on `b` using the snoc
126+
||| structure of `range`.
127+
rangeAppend : (a, b : Nat) ->
128+
range (a + b) = range a ++ map (\i => i + a) (range b)
129+
rangeAppend a Z = rewrite plusZeroRightNeutral a in
130+
sym (appendNilRightNeutral (range a))
131+
rangeAppend a (S k) =
132+
rewrite sym (plusSuccRightSucc a k) in
133+
-- LHS: range (S (a+k)) = range (a+k) ++ [a+k]
134+
rewrite rangeAppend a k in
135+
-- LHS: (range a ++ map (+a) (range k)) ++ [a+k]
136+
rewrite mapAppendL (\i => i + a) (range k) [k] in
137+
-- RHS inner: map (+a) (range k) ++ [k+a]
138+
rewrite plusCommutative k a in
139+
-- now [k+a] becomes [a+k] on the RHS, matching the LHS snoc element
140+
sym (appendAssociative (range a) (map (\i => i + a) (range k)) [a + k])
141+
142+
||| One outer block, expressed flatly: applying `f` after the inner-index
143+
||| reconstruction `(+ o*inner)` equals `f` mapped over the shifted range.
144+
||| This lines `runInner f inner o` up with the block that `rangeAppend`
145+
||| produces for the flat run.
146+
runInnerAsFlat :
147+
(f : Nat -> Nat) -> (inner, o : Nat) ->
148+
runInner f inner o = map f (map (\i => i + o * inner) (range inner))
149+
runInnerAsFlat f inner o =
150+
rewrite mapFusionL f (\i => i + o * inner) (range inner) in
151+
mapExtFn (range inner)
152+
where
153+
||| `splitIndex inner o i = o*inner + i = i + o*inner`, pointwise.
154+
mapExtFn : (xs : List Nat) ->
155+
map (\i => f (splitIndex inner o i)) xs
156+
= map (\i => f (i + o * inner)) xs
157+
mapExtFn [] = Refl
158+
mapExtFn (x :: xs) =
159+
cong2 (::)
160+
(cong f (plusCommutative (o * inner) x))
161+
(mapExtFn xs)
162+
163+
||| The heart of the theorem. Enumerating the FLAT domain
164+
||| `range (outer * inner)` and applying `f`, versus enumerating the SPLIT
165+
||| nested domain and reconstructing each index via `o*inner + i`, produce
166+
||| the SAME list.
167+
|||
168+
||| Proof by induction on `outer`. The successor case peels the last outer
169+
||| block off both sides: `runSplit` via `concatBlocksSnoc`, and `runFlat`
170+
||| via `rangeAppend` (`S o * inner = o*inner + inner`). The two peeled
171+
||| blocks coincide by `runInnerAsFlat`.
172+
splitEnumerates :
173+
(f : Nat -> Nat) -> (outer : Nat) -> (inner : Nat) ->
174+
runSplit f outer inner = runFlat f (outer * inner)
175+
splitEnumerates f Z inner = Refl
176+
splitEnumerates f (S o) inner =
177+
-- LHS: concatBlocks (map (runInner f inner) (range o ++ [o]))
178+
rewrite mapAppendL (runInner f inner) (range o) [o] in
179+
rewrite concatBlocksSnoc (map (runInner f inner) (range o)) (runInner f inner o) in
180+
-- LHS = runSplit f o inner ++ runInner f inner o
181+
rewrite splitEnumerates f o inner in
182+
-- LHS = map f (range (o*inner)) ++ runInner f inner o
183+
rewrite runInnerAsFlat f inner o in
184+
-- LHS = map f (range (o*inner)) ++ map f (map (+ o*inner) (range inner))
185+
rewrite sym (mapAppendL f (range (o * inner)) (map (\i => i + o * inner) (range inner))) in
186+
-- LHS = map f (range (o*inner) ++ map (+ o*inner) (range inner))
187+
rewrite sym (rangeAppend (o * inner) inner) in
188+
-- LHS = map f (range (o*inner + inner))
189+
-- RHS: map f (range (S o * inner)) ; S o * inner = inner + o*inner.
190+
-- Show o*inner + inner = S o * inner so the ranges match.
191+
rewrite plusCommutative (o * inner) inner in
192+
Refl
193+
194+
--------------------------------------------------------------------------------
195+
-- Headline property
196+
--------------------------------------------------------------------------------
197+
198+
||| `SplitEquivalent f outer inner` is the proposition that the scheduled
199+
||| (split) run equals the unscheduled (flat) run over the domain of size
200+
||| `outer * inner`. There is NO way to inhabit this for a schedule that
201+
||| changes the result — the only constructor demands a real equality.
202+
public export
203+
data SplitEquivalent : (f : Nat -> Nat) -> (outer, inner : Nat) -> Type where
204+
MkSplitEquivalent :
205+
runSplit f outer inner = runFlat f (outer * inner) ->
206+
SplitEquivalent f outer inner
207+
208+
||| The theorem: EVERY split schedule is equivalent to the flat schedule.
209+
public export
210+
splitPreservesResult :
211+
(f : Nat -> Nat) -> (outer, inner : Nat) -> SplitEquivalent f outer inner
212+
splitPreservesResult f outer inner =
213+
MkSplitEquivalent (splitEnumerates f outer inner)
214+
215+
--------------------------------------------------------------------------------
216+
-- Certifier
217+
--------------------------------------------------------------------------------
218+
219+
||| Certify a split schedule against a stage. Always returns `Ok` because
220+
||| `splitPreservesResult` shows every split is sound; the soundness fact
221+
||| below ties the `Ok` verdict back to the equivalence proposition.
222+
public export
223+
certifySplit : (f : Nat -> Nat) -> (outer, inner : Nat) -> Result
224+
certifySplit f outer inner = Ok
225+
226+
||| Soundness of the certifier: an `Ok` verdict really does imply the
227+
||| scheduled and unscheduled runs agree.
228+
public export
229+
certifySplitSound :
230+
(f : Nat -> Nat) -> (outer, inner : Nat) ->
231+
certifySplit f outer inner = Ok ->
232+
runSplit f outer inner = runFlat f (outer * inner)
233+
certifySplitSound f outer inner _ = splitEnumerates f outer inner
234+
235+
--------------------------------------------------------------------------------
236+
-- Positive control: a concrete schedule equivalence witness
237+
--------------------------------------------------------------------------------
238+
239+
||| A concrete stage: double each pixel index value.
240+
public export
241+
double : Nat -> Nat
242+
double n = n + n
243+
244+
||| POSITIVE CONTROL. Splitting an extent-12 domain into 3 outer blocks of
245+
||| 4 inner iterations is equivalent to running it flat. An inhabited
246+
||| witness — the proof obligation is discharged by the general theorem.
247+
public export
248+
doubleSplit3x4Equivalent : SplitEquivalent Semantics.double 3 4
249+
doubleSplit3x4Equivalent = splitPreservesResult double 3 4
250+
251+
||| And the underlying lists are literally equal on this concrete case.
252+
public export
253+
doubleSplit3x4Concrete : runSplit Semantics.double 3 4 = runFlat Semantics.double 12
254+
doubleSplit3x4Concrete = Refl
255+
256+
--------------------------------------------------------------------------------
257+
-- Negative control: a result-changing "schedule" is NOT equivalent
258+
--------------------------------------------------------------------------------
259+
260+
||| A FAKE schedule that drops the last block (executes only `outer-1`
261+
||| blocks). This models an unsound schedule that silently omits work.
262+
public export
263+
runSplitDropLast : (f : Nat -> Nat) -> (outer, inner : Nat) -> List Nat
264+
runSplitDropLast f outer inner =
265+
concatMap (runInner f inner) (range (pred outer))
266+
267+
||| NEGATIVE CONTROL. On the concrete extent-12 case, the work-dropping
268+
||| schedule does NOT reproduce the flat run: their output lists differ.
269+
||| Machine-checked: the two concrete lists are unequal.
270+
public export
271+
dropLastNotEquivalent :
272+
Not (runSplitDropLast Semantics.double 3 4 = runFlat Semantics.double 12)
273+
dropLastNotEquivalent eq = case eq of Refl impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Halideiser.ABI.Types
99
, Halideiser.ABI.Layout
1010
, Halideiser.ABI.Foreign
1111
, Halideiser.ABI.Proofs
12+
, Halideiser.ABI.Semantics

0 commit comments

Comments
 (0)