Skip to content

Commit 88732af

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Add Semantics module: prove Futhark map-fusion law (ABI Layer 2) (#40)
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. Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent 3fa6ff2 commit 88732af

2 files changed

Lines changed: 152 additions & 0 deletions

File tree

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

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
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 Futharkiser (Idris2 ABI Layer 2).
5+
|||
6+
||| Futharkiser compiles annotated array operations to GPU kernels via Futhark.
7+
||| The single most important optimisation that justifies that pipeline is
8+
||| MAP FUSION: rewriting `map f (map g xs)` into `map (f . g) xs`. Futhark's
9+
||| whole performance story rests on fusing chained SOACs so that intermediate
10+
||| arrays are never materialised on the device. If fusion is not semantically
11+
||| sound, the generated GPU kernel computes the WRONG answer.
12+
|||
13+
||| This module gives a faithful, length-indexed model of `map` over a Futhark
14+
||| array (a `Vect n a`) and proves, as a real propositional equality, that:
15+
|||
16+
||| (1) map preserves length : mapV f xs : Vect n b (by construction)
17+
||| (2) FUSION LAW : mapV f (mapV g xs) = mapV (f . g) xs
18+
||| (3) IDENTITY LAW (functor identity) : mapV id xs = xs
19+
|||
20+
||| (2) is the headline. Both are proved by structural induction with no
21+
||| escape hatches (no believe_me / postulate / assert). A certifier maps a
22+
||| concrete fused/unfused pair to a ProofStatus-like verdict, and there is a
23+
||| positive control (a witnessed instance of the law) plus a negative control
24+
||| (a machine-checked refutation of a DELIBERATELY wrong fusion).
25+
26+
module Futharkiser.ABI.Semantics
27+
28+
import Data.Vect
29+
import Decidable.Equality
30+
31+
%default total
32+
33+
--------------------------------------------------------------------------------
34+
-- Faithful model of the Futhark `map` SOAC over a length-indexed array.
35+
--------------------------------------------------------------------------------
36+
37+
||| `mapV` is our model of the Futhark `map` second-order array combinator.
38+
||| The output Vect has exactly the same length `n` as the input: the type
39+
||| itself is the proof that `map` preserves array length / shape, which is the
40+
||| rank-and-length invariant the GPU codegen relies on.
41+
public export
42+
mapV : (a -> b) -> Vect n a -> Vect n b
43+
mapV f [] = []
44+
mapV f (x :: xs) = f x :: mapV f xs
45+
46+
--------------------------------------------------------------------------------
47+
-- Length preservation (made explicit as a value-level fact).
48+
--------------------------------------------------------------------------------
49+
50+
||| `mapV` preserves length. This is true by construction (the result type is
51+
||| `Vect n b` for input `Vect n a`), and we record it as an explicit equality
52+
||| on the runtime `length`.
53+
public export
54+
mapPreservesLength : (f : a -> b) -> (xs : Vect n a) ->
55+
length (mapV f xs) = length xs
56+
mapPreservesLength f [] = Refl
57+
mapPreservesLength f (x :: xs) = cong S (mapPreservesLength f xs)
58+
59+
--------------------------------------------------------------------------------
60+
-- THE HEADLINE: the map-fusion law (sound fusion of chained SOACs).
61+
--------------------------------------------------------------------------------
62+
63+
||| Map fusion law: applying `map g` then `map f` is exactly the same array as
64+
||| applying `map (f . g)` once. This is what licenses Futhark's kernel-fusion
65+
||| optimisation — eliminating the intermediate device array is observationally
66+
||| equivalent to the unfused pipeline, element for element.
67+
|||
68+
||| Proved by structural induction on the input vector; the cons case rewrites
69+
||| under the inductive hypothesis. No axioms.
70+
public export
71+
mapFusion : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a) ->
72+
mapV f (mapV g xs) = mapV (\x => f (g x)) xs
73+
mapFusion f g [] = Refl
74+
mapFusion f g (x :: xs) = cong (f (g x) ::) (mapFusion f g xs)
75+
76+
||| Functor identity law: fusing with the identity function is a no-op. Together
77+
||| with `mapFusion` this makes `mapV` a lawful functor, so any chain of fused
78+
||| maps in the generated kernel is equal to the unfused source pipeline.
79+
public export
80+
mapIdentity : (xs : Vect n a) -> mapV (\x => x) xs = xs
81+
mapIdentity [] = Refl
82+
mapIdentity (x :: xs) = cong (x ::) (mapIdentity xs)
83+
84+
--------------------------------------------------------------------------------
85+
-- Fusion verdict + soundness certifier.
86+
--------------------------------------------------------------------------------
87+
88+
||| Verdict of checking a proposed fusion rewrite.
89+
public export
90+
data FusionVerdict = FusionSound | FusionUnsound
91+
92+
public export
93+
DecEq FusionVerdict where
94+
decEq FusionSound FusionSound = Yes Refl
95+
decEq FusionUnsound FusionUnsound = Yes Refl
96+
decEq FusionSound FusionUnsound = No (\case Refl impossible)
97+
decEq FusionUnsound FusionSound = No (\case Refl impossible)
98+
99+
||| Certify that fusing `map f . map g` into `map (f . g)` over a CONCRETE
100+
||| witness vector produces the identical array. Because the fusion law holds
101+
||| for ALL vectors, the certifier can always return `FusionSound` and discharge
102+
||| its own soundness obligation with `mapFusion`.
103+
public export
104+
certifyFusion : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a) -> FusionVerdict
105+
certifyFusion f g xs = FusionSound
106+
107+
||| Soundness of the certifier: whenever it reports `FusionSound`, the fused and
108+
||| unfused pipelines really are the same array.
109+
public export
110+
certifyFusionSound : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a) ->
111+
certifyFusion f g xs = FusionSound ->
112+
mapV f (mapV g xs) = mapV (\x => f (g x)) xs
113+
certifyFusionSound f g xs _ = mapFusion f g xs
114+
115+
--------------------------------------------------------------------------------
116+
-- POSITIVE CONTROL: an inhabited witness of the fusion law on real data.
117+
--------------------------------------------------------------------------------
118+
119+
||| Concrete input array.
120+
public export
121+
sampleArray : Vect 3 Nat
122+
sampleArray = [10, 20, 30]
123+
124+
||| `g = (+1)`, `f = (*2)`. The fused and unfused pipelines must agree.
125+
||| This is a fully evaluated, machine-checked instance of the headline law:
126+
||| map (*2) (map (+1) [10,20,30]) = map (\x => (x+1)*2) [10,20,30] = [22,42,62]
127+
public export
128+
fusionWitness : mapV (\x => x * 2) (mapV (\x => x + 1) Semantics.sampleArray)
129+
= mapV (\x => (x + 1) * 2) Semantics.sampleArray
130+
fusionWitness = Refl
131+
132+
||| The same instance routed through the general theorem (not just `Refl`),
133+
||| showing the proof term is the genuine inductive one.
134+
public export
135+
fusionWitnessViaTheorem : mapV (\x => x * 2) (mapV (\x => x + 1) Semantics.sampleArray)
136+
= mapV (\x => (x + 1) * 2) Semantics.sampleArray
137+
fusionWitnessViaTheorem = mapFusion (\x => x * 2) (\x => x + 1) Semantics.sampleArray
138+
139+
--------------------------------------------------------------------------------
140+
-- NEGATIVE CONTROL: a DELIBERATELY wrong fusion is refuted (non-vacuity).
141+
--------------------------------------------------------------------------------
142+
143+
||| A bogus "fusion" that drops the inner map's effect: claiming
144+
||| map (*2) (map (+1) xs) = map (*2) xs
145+
||| This is FALSE for our sample data, and we prove the inequality.
146+
||| If this `Not (...)` were inhabitable, the fusion law would be vacuous.
147+
public export
148+
wrongFusionRefuted :
149+
Not (mapV (\x => x * 2) (mapV (\x => x + 1) Semantics.sampleArray)
150+
= mapV (\x => x * 2) Semantics.sampleArray)
151+
wrongFusionRefuted Refl impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ modules = Futharkiser.ABI.Types
77
, Futharkiser.ABI.Layout
88
, Futharkiser.ABI.Foreign
99
, Futharkiser.ABI.Proofs
10+
, Futharkiser.ABI.Semantics

0 commit comments

Comments
 (0)