Skip to content

Commit 5416e5e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: cross-SOAC map/zipWith fusion law (#41)
* Add Semantics module: prove Futhark map-fusion law (ABI Layer 2) Add Futharkiser.ABI.Semantics, a machine-checked semantic proof raising the Idris2 ABI to Layer 2. Models the Futhark `map` SOAC over length-indexed Vects and proves, as genuine propositional equalities by structural induction (no believe_me/postulate/assert): - mapFusion: mapV f (mapV g xs) = mapV (f . g) xs (the headline law that licenses Futhark's GPU kernel-fusion optimisation) - mapIdentity: mapV id xs = xs (functor identity) - mapPreservesLength: length (mapV f xs) = length xs (shape invariant) Includes a FusionVerdict certifier with a soundness theorem, a positive control (evaluated witness on real data, also routed through the general theorem) and a negative control (machine-checked refutation of a deliberately-wrong fusion that drops the inner map). Registered in futharkiser-abi.ipkg; package builds clean with zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * feat(abi): add Layer-3 map/zipWith cross-SOAC fusion theorem (Invariants) Adds Futharkiser.ABI.Invariants over the existing Layer-2 mapV model: - mapZipWithFusion (L1): map h (zipWith g xs ys) = zipWith (h . g) xs ys - zipWithMapLeft (L2) / zipWithMapRight (L3): map pushed into a zipWith input - zipWithPreservesLength shape invariant - sound+complete Dec (isCrossSound) + certifier soundness - positive controls (witnessed instances via theorem and by Refl) - negative controls (wrong rewrite refuted; Uninhabited refutation) Genuine inductive proofs; no believe_me/postulate/assert. Clean build, zero warnings; adversarial false proof rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 88732af commit 5416e5e

2 files changed

Lines changed: 251 additions & 0 deletions

File tree

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

Lines changed: 250 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,250 @@
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+
||| Second formal theorem for Futharkiser (Idris2 ABI Layer 3).
5+
|||
6+
||| Layer 2 (`Futharkiser.ABI.Semantics`) proved the MAP-FUSION law for a single
7+
||| array SOAC: `map f (map g xs) = map (f . g) xs`, together with the functor
8+
||| identity law. Those are *unary* laws over one array.
9+
|||
10+
||| Layer 3 goes DEEPER by reasoning about the interaction of TWO array SOACs:
11+
||| the `zipWith` combinator (binary map) and how `map` fuses INTO and ACROSS it.
12+
||| Futhark's kernel fusion does not stop at chained `map`s — it also fuses a
13+
||| `map` consuming the result of a `zipWith`, and pushes `map`s applied to each
14+
||| input of a `zipWith` through the combiner. These cross-SOAC rewrites are what
15+
||| let Futhark collapse a dataflow DAG (not just a chain) into one kernel. If
16+
||| they are unsound, the fused GPU kernel computes the wrong answer.
17+
|||
18+
||| We prove, as genuine propositional equalities by structural induction over a
19+
||| length-indexed array (`Vect n a`), three NEW and DISTINCT laws:
20+
|||
21+
||| (L1) map/zipWith FUSION (post-composition naturality):
22+
||| mapV h (zipWithV g xs ys) = zipWithV (\a,b => h (g a b)) xs ys
23+
|||
24+
||| (L2) LEFT pre-fusion of map into zipWith:
25+
||| zipWithV g (mapV p xs) ys = zipWithV (\a,b => g (p a) b) xs ys
26+
|||
27+
||| (L3) RIGHT pre-fusion of map into zipWith:
28+
||| zipWithV g xs (mapV q ys) = zipWithV (\a,b => g a (q b)) xs ys
29+
|||
30+
||| plus a shape invariant: `zipWithV` preserves the common length `n`
31+
||| (by construction in the type), recorded explicitly on `length`.
32+
|||
33+
||| These are NOT restatements of map-map fusion: they relate a binary SOAC to a
34+
||| unary one, which the Layer-2 module never mentions. We REUSE the Layer-2
35+
||| `mapV` model unchanged (imported, not redefined). No escape hatches are used:
36+
||| no believe_me / idris_crash / assert_total / postulate / sorry. A sound +
37+
||| complete `Dec` for a fusion-shape check is provided, with a POSITIVE control
38+
||| (witnessed instances of all three laws on concrete data) and a NEGATIVE
39+
||| control (a machine-checked refutation of a DELIBERATELY wrong map/zipWith
40+
||| rewrite, establishing non-vacuity).
41+
42+
module Futharkiser.ABI.Invariants
43+
44+
import Data.Vect
45+
import Decidable.Equality
46+
47+
import Futharkiser.ABI.Semantics
48+
49+
%default total
50+
51+
--------------------------------------------------------------------------------
52+
-- Binary SOAC: zipWith over two length-indexed arrays of the SAME length.
53+
--------------------------------------------------------------------------------
54+
55+
||| `zipWithV` is our model of the Futhark `map2` / `zipWith` second-order array
56+
||| combinator. Both inputs and the output share the SAME length `n`; the type is
57+
||| itself the proof that this binary SOAC preserves array length / shape.
58+
public export
59+
zipWithV : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
60+
zipWithV g [] [] = []
61+
zipWithV g (x :: xs) (y :: ys) = g x y :: zipWithV g xs ys
62+
63+
--------------------------------------------------------------------------------
64+
-- Shape invariant: zipWith preserves the common length (explicit on length).
65+
--------------------------------------------------------------------------------
66+
67+
||| `zipWithV` preserves length. True by construction (result is `Vect n c`),
68+
||| recorded as an explicit equality on the runtime `length`.
69+
public export
70+
zipWithPreservesLength : (g : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) ->
71+
length (zipWithV g xs ys) = length xs
72+
zipWithPreservesLength g [] [] = Refl
73+
zipWithPreservesLength g (x :: xs) (y :: ys) =
74+
cong S (zipWithPreservesLength g xs ys)
75+
76+
--------------------------------------------------------------------------------
77+
-- (L1) THE HEADLINE FOR LAYER 3: map / zipWith fusion (post-composition).
78+
--------------------------------------------------------------------------------
79+
80+
||| Map/zipWith fusion law (naturality of `mapV` over the binary SOAC):
81+
||| post-composing a `map h` onto a `zipWith g` is the same array as folding `h`
82+
||| into the combiner. This licenses Futhark fusing a `map` that consumes a
83+
||| `zipWith` result, eliminating the intermediate device array.
84+
|||
85+
||| Proved by structural induction on BOTH input vectors simultaneously; the cons
86+
||| case rewrites under the inductive hypothesis. No axioms.
87+
public export
88+
mapZipWithFusion : (h : c -> d) -> (g : a -> b -> c) ->
89+
(xs : Vect n a) -> (ys : Vect n b) ->
90+
mapV h (zipWithV g xs ys)
91+
= zipWithV (\p, q => h (g p q)) xs ys
92+
mapZipWithFusion h g [] [] = Refl
93+
mapZipWithFusion h g (x :: xs) (y :: ys) =
94+
cong (h (g x y) ::) (mapZipWithFusion h g xs ys)
95+
96+
--------------------------------------------------------------------------------
97+
-- (L2) LEFT pre-fusion: a map on the first input pushes into the combiner.
98+
--------------------------------------------------------------------------------
99+
100+
||| Pushing a `map p` applied to the LEFT input of a `zipWith` through the
101+
||| combiner. This is the producer→consumer fusion Futhark performs on the left
102+
||| edge of a binary SOAC's dataflow.
103+
public export
104+
zipWithMapLeft : (g : b -> c -> d) -> (p : a -> b) ->
105+
(xs : Vect n a) -> (ys : Vect n c) ->
106+
zipWithV g (mapV p xs) ys
107+
= zipWithV (\u, q => g (p u) q) xs ys
108+
zipWithMapLeft g p [] [] = Refl
109+
zipWithMapLeft g p (x :: xs) (y :: ys) =
110+
cong (g (p x) y ::) (zipWithMapLeft g p xs ys)
111+
112+
--------------------------------------------------------------------------------
113+
-- (L3) RIGHT pre-fusion: a map on the second input pushes into the combiner.
114+
--------------------------------------------------------------------------------
115+
116+
||| Pushing a `map q` applied to the RIGHT input of a `zipWith` through the
117+
||| combiner — the symmetric right-edge producer→consumer fusion.
118+
public export
119+
zipWithMapRight : (g : a -> c -> d) -> (q : b -> c) ->
120+
(xs : Vect n a) -> (ys : Vect n b) ->
121+
zipWithV g xs (mapV q ys)
122+
= zipWithV (\u, v => g u (q v)) xs ys
123+
zipWithMapRight g q [] [] = Refl
124+
zipWithMapRight g q (x :: xs) (y :: ys) =
125+
cong (g x (q y) ::) (zipWithMapRight g q xs ys)
126+
127+
--------------------------------------------------------------------------------
128+
-- Cross-SOAC fusion verdict + a sound & complete decision procedure.
129+
--------------------------------------------------------------------------------
130+
131+
||| Verdict of checking a proposed cross-SOAC (map/zipWith) rewrite.
132+
public export
133+
data CrossVerdict = CrossSound | CrossUnsound
134+
135+
public export
136+
DecEq CrossVerdict where
137+
decEq CrossSound CrossSound = Yes Refl
138+
decEq CrossUnsound CrossUnsound = Yes Refl
139+
decEq CrossSound CrossUnsound = No (\case Refl impossible)
140+
decEq CrossUnsound CrossSound = No (\case Refl impossible)
141+
142+
||| A natural decision: is a given verdict the SOUND one? This is a genuine
143+
||| `Dec (v = CrossSound)`: `Yes` carries a proof, `No` carries a refutation,
144+
||| so it is both sound (only says Yes with a witness) and complete (decides
145+
||| every input). Built on `decEq` for `CrossVerdict`.
146+
public export
147+
isCrossSound : (v : CrossVerdict) -> Dec (v = CrossSound)
148+
isCrossSound v = decEq v CrossSound
149+
150+
||| Certify a map/zipWith post-fusion over a CONCRETE witness. Because (L1) holds
151+
||| for ALL inputs, the certifier always returns `CrossSound` and can discharge
152+
||| its own soundness obligation with `mapZipWithFusion`.
153+
public export
154+
certifyCross : (h : c -> d) -> (g : a -> b -> c) ->
155+
(xs : Vect n a) -> (ys : Vect n b) -> CrossVerdict
156+
certifyCross h g xs ys = CrossSound
157+
158+
||| Soundness of the certifier: whenever it reports `CrossSound`, the post-fused
159+
||| and unfused pipelines are the same array.
160+
public export
161+
certifyCrossSound : (h : c -> d) -> (g : a -> b -> c) ->
162+
(xs : Vect n a) -> (ys : Vect n b) ->
163+
certifyCross h g xs ys = CrossSound ->
164+
mapV h (zipWithV g xs ys)
165+
= zipWithV (\p, q => h (g p q)) xs ys
166+
certifyCrossSound h g xs ys _ = mapZipWithFusion h g xs ys
167+
168+
--------------------------------------------------------------------------------
169+
-- POSITIVE CONTROL: witnessed instances of all three laws on real data.
170+
--------------------------------------------------------------------------------
171+
172+
||| Concrete left input.
173+
public export
174+
arrA : Vect 3 Nat
175+
arrA = [1, 2, 3]
176+
177+
||| Concrete right input.
178+
public export
179+
arrB : Vect 3 Nat
180+
arrB = [10, 20, 30]
181+
182+
||| (L1) instance: `g = (+)`, `h = (*2)`.
183+
||| map (*2) (zipWith (+) [1,2,3] [10,20,30])
184+
||| = map (*2) [11,22,33] = [22,44,66]
185+
||| zipWith (\p q => (p+q)*2) [1,2,3] [10,20,30] = [22,44,66]
186+
||| Routed through the general theorem to show the proof term is the real one.
187+
public export
188+
crossWitnessL1 :
189+
mapV (\x => x * 2) (zipWithV (\u, v => u + v) Invariants.arrA Invariants.arrB)
190+
= zipWithV (\p, q => (p + q) * 2) Invariants.arrA Invariants.arrB
191+
crossWitnessL1 =
192+
mapZipWithFusion (\x => x * 2) (\u, v => u + v) Invariants.arrA Invariants.arrB
193+
194+
||| The same (L1) instance also holds by pure computation (`Refl`), confirming
195+
||| the model actually evaluates to the claimed array.
196+
public export
197+
crossWitnessL1Refl :
198+
mapV (\x => x * 2) (zipWithV (\u, v => u + v) Invariants.arrA Invariants.arrB)
199+
= zipWithV (\p, q => (p + q) * 2) Invariants.arrA Invariants.arrB
200+
crossWitnessL1Refl = Refl
201+
202+
||| (L2) instance: pre-map `p = (+100)` on the LEFT input.
203+
public export
204+
crossWitnessL2 :
205+
zipWithV (\u, v => u + v) (mapV (\x => x + 100) Invariants.arrA) Invariants.arrB
206+
= zipWithV (\u, q => (u + 100) + q) Invariants.arrA Invariants.arrB
207+
crossWitnessL2 =
208+
zipWithMapLeft (\u, v => u + v) (\x => x + 100) Invariants.arrA Invariants.arrB
209+
210+
||| (L3) instance: pre-map `q = (*3)` on the RIGHT input.
211+
public export
212+
crossWitnessL3 :
213+
zipWithV (\u, v => u + v) Invariants.arrA (mapV (\y => y * 3) Invariants.arrB)
214+
= zipWithV (\u, w => u + (w * 3)) Invariants.arrA Invariants.arrB
215+
crossWitnessL3 =
216+
zipWithMapRight (\u, v => u + v) (\y => y * 3) Invariants.arrA Invariants.arrB
217+
218+
||| Positive control for the decision procedure: `CrossSound` is decided `Yes`.
219+
public export
220+
soundIsAccepted : Dec (CrossSound = CrossSound)
221+
soundIsAccepted = isCrossSound CrossSound
222+
223+
--------------------------------------------------------------------------------
224+
-- NEGATIVE CONTROLS: deliberately wrong rewrites are refuted (non-vacuity).
225+
--------------------------------------------------------------------------------
226+
227+
||| A BOGUS map/zipWith "fusion" that forgets to apply `h` to the combiner's
228+
||| result, claiming
229+
||| map (*2) (zipWith (+) xs ys) = zipWith (+) xs ys
230+
||| This is FALSE on the sample data ([22,44,66] /= [11,22,33]); we prove the
231+
||| inequality. If this `Not (...)` were inhabitable, (L1) would be vacuous.
232+
public export
233+
wrongCrossRefuted :
234+
Not (mapV (\x => x * 2)
235+
(zipWithV (\u, v => u + v) Invariants.arrA Invariants.arrB)
236+
= zipWithV (\u, v => u + v) Invariants.arrA Invariants.arrB)
237+
wrongCrossRefuted Refl impossible
238+
239+
public export
240+
Uninhabited (CrossUnsound = CrossSound) where
241+
uninhabited Refl impossible
242+
243+
||| Completeness-flavoured negative control for the decision procedure:
244+
||| `CrossUnsound` is NOT equal to `CrossSound`, so `isCrossSound` must answer
245+
||| `No`. We extract and exercise that refutation directly.
246+
public export
247+
unsoundIsRejected : Not (CrossUnsound = CrossSound)
248+
unsoundIsRejected = case isCrossSound CrossUnsound of
249+
Yes prf => absurd prf
250+
No contra => contra

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ modules = Futharkiser.ABI.Types
88
, Futharkiser.ABI.Foreign
99
, Futharkiser.ABI.Proofs
1010
, Futharkiser.ABI.Semantics
11+
, Futharkiser.ABI.Invariants

0 commit comments

Comments
 (0)