Skip to content

Commit dd8ea77

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: map/each fusion law (bmap f ∘ bmap g = bmap (f∘g)) (#34)
## Summary Layer 3 (second, deeper invariant): proves the **map/each fusion law** `bmap f (bmap g xs) = bmap (f . g) xs` — an algebraic loop-fusion rewrite. Distinct from and deeper than the Layer-2 sum-of-reverse rewrite. New module `Bqniser.ABI.Invariants` (imports the Layer-2 `Semantics` model). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent f4d6a44 commit dd8ea77

2 files changed

Lines changed: 162 additions & 0 deletions

File tree

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

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
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 flagship semantic proof for Bqniser (Idris2 ABI Layer 3).
5+
|||
6+
||| The Layer-2 module (`Bqniser.ABI.Semantics`) proves a *fold* rewrite:
7+
||| `+´⌽𝕩 ==> +´𝕩` (sum invariant under reverse). This module proves a
8+
||| genuinely DIFFERENT and DEEPER property: an algebraic FUSION law over the
9+
||| Each (`¨`) primitive — composition of maps fuses into a single map:
10+
|||
11+
||| f¨ g¨ 𝕩 ==> (f∘g)¨ 𝕩 (map fusion / Each fusion)
12+
|||
13+
||| This is the canonical loop-fusion rewrite BQNiser performs to eliminate an
14+
||| intermediate array: applying `g` to every element and then `f` to every
15+
||| element is the same as applying `f∘g` once per element. We prove:
16+
|||
17+
||| 1. `bmapFusion` — the headline fusion equation, by induction (∀ f g xs).
18+
||| 2. `bmapLengthPreserving` — Each preserves array length, so the rewrite
19+
||| preserves shape as well as element values (a deeper structural fact
20+
||| the fold theorem could not express, since fold collapses the array).
21+
||| 3. `decFuses` — a SOUND + COMPLETE decision that the fused form agrees
22+
||| with the staged form on a concrete input (round-trip checkable).
23+
||| 4. A certifier into the ABI `Result`, proven sound against the law.
24+
||| 5. A POSITIVE control (concrete fusion instance) and a NEGATIVE /
25+
||| non-vacuity control (`bmap` is genuinely effectful — fusing the WRONG
26+
||| composition order is refuted, so the law is not trivially true).
27+
|||
28+
||| It reuses the SAME `List Nat` model as Layer 2 — no datatype is redefined.
29+
||| (`bmap` is named to avoid clashing with Prelude `map`.)
30+
31+
module Bqniser.ABI.Invariants
32+
33+
import Bqniser.ABI.Types
34+
import Bqniser.ABI.Semantics
35+
import Data.Nat
36+
37+
%default total
38+
39+
--------------------------------------------------------------------------------
40+
-- The Each (`¨`) primitive over the shared List Nat model
41+
--------------------------------------------------------------------------------
42+
43+
||| Each (`¨`): apply a function to every element of an array.
44+
||| Defined directly so it is convenient to induct over.
45+
public export
46+
bmap : (Nat -> Nat) -> List Nat -> List Nat
47+
bmap _ [] = []
48+
bmap f (x :: xs) = f x :: bmap f xs
49+
50+
||| Length, named to avoid any List/Prelude ambiguity through this module.
51+
public export
52+
blen : List Nat -> Nat
53+
blen [] = 0
54+
blen (_ :: xs) = S (blen xs)
55+
56+
--------------------------------------------------------------------------------
57+
-- Layer-3 theorem 1: map fusion (the headline algebraic law)
58+
--------------------------------------------------------------------------------
59+
60+
||| Fusion: mapping `g` then `f` equals mapping `f ∘ g` in a single pass.
61+
||| Proven by induction over the array; semantics-preserving for all inputs.
62+
export
63+
bmapFusion : (f : Nat -> Nat) -> (g : Nat -> Nat) -> (xs : List Nat) ->
64+
bmap f (bmap g xs) = bmap (\x => f (g x)) xs
65+
bmapFusion _ _ [] = Refl
66+
bmapFusion f g (x :: xs) = cong (f (g x) ::) (bmapFusion f g xs)
67+
68+
--------------------------------------------------------------------------------
69+
-- Layer-3 theorem 2: Each preserves length (structural soundness)
70+
--------------------------------------------------------------------------------
71+
72+
||| Each preserves array length: the rewrite is shape-preserving, not just
73+
||| value-preserving. This is strictly deeper than the fold theorem, whose
74+
||| result is a scalar and therefore cannot witness shape.
75+
export
76+
bmapLengthPreserving : (f : Nat -> Nat) -> (xs : List Nat) ->
77+
blen (bmap f xs) = blen xs
78+
bmapLengthPreserving _ [] = Refl
79+
bmapLengthPreserving f (x :: xs) = cong S (bmapLengthPreserving f xs)
80+
81+
||| Corollary: the staged form and the fused form have identical length,
82+
||| obtained purely from the two theorems above (no fresh induction).
83+
export
84+
fusionLengthAgrees : (f : Nat -> Nat) -> (g : Nat -> Nat) -> (xs : List Nat) ->
85+
blen (bmap f (bmap g xs)) = blen (bmap (\x => f (g x)) xs)
86+
fusionLengthAgrees f g xs = cong blen (bmapFusion f g xs)
87+
88+
--------------------------------------------------------------------------------
89+
-- A sound + complete decision for fusion-agreement on a concrete input
90+
--------------------------------------------------------------------------------
91+
92+
||| Decide whether the staged form and the fused form agree on a given input.
93+
||| By `bmapFusion` they ALWAYS agree, so this is a total `Yes`; the point is
94+
||| that it is genuinely a `Dec` of the propositional equality (sound: the
95+
||| `Yes` carries a real proof; complete: a `No` is impossible to construct,
96+
||| witnessed by the proof itself rather than by fiat).
97+
public export
98+
decFuses : (f : Nat -> Nat) -> (g : Nat -> Nat) -> (xs : List Nat) ->
99+
Dec (bmap f (bmap g xs) = bmap (\x => f (g x)) xs)
100+
decFuses f g xs = Yes (bmapFusion f g xs)
101+
102+
||| Completeness of the decision: there is no input on which the agreement
103+
||| fails. Anything purporting to refute fusion is itself refuted.
104+
export
105+
decFusesComplete : (f : Nat -> Nat) -> (g : Nat -> Nat) -> (xs : List Nat) ->
106+
Not (Not (bmap f (bmap g xs) = bmap (\x => f (g x)) xs))
107+
decFusesComplete f g xs contra = contra (bmapFusion f g xs)
108+
109+
--------------------------------------------------------------------------------
110+
-- Certifier into the ABI Result, proven sound against the fusion law
111+
--------------------------------------------------------------------------------
112+
113+
||| The fusion rewrite is unconditionally valid, so the certifier reports `Ok`.
114+
public export
115+
certifyFusion : (Nat -> Nat) -> (Nat -> Nat) -> List Nat -> Result
116+
certifyFusion _ _ _ = Ok
117+
118+
||| Soundness: whenever the certifier reports `Ok`, the fused rewrite genuinely
119+
||| computes the same array as the staged form for that input.
120+
export
121+
certifyFusionSound : (f : Nat -> Nat) -> (g : Nat -> Nat) -> (xs : List Nat) ->
122+
certifyFusion f g xs = Ok ->
123+
bmap f (bmap g xs) = bmap (\x => f (g x)) xs
124+
certifyFusionSound f g xs _ = bmapFusion f g xs
125+
126+
--------------------------------------------------------------------------------
127+
-- Positive control: a concrete fusion instance, machine-checked
128+
--------------------------------------------------------------------------------
129+
130+
||| Doubling then incrementing every element, in two passes, equals doing
131+
||| `(+1) ∘ (*2)` in one pass, over a concrete array.
132+
export
133+
fusionConcrete : bmap (\x => x + 1) (bmap (\x => x * 2) [1, 2, 3])
134+
= bmap (\x => (x * 2) + 1) [1, 2, 3]
135+
fusionConcrete = bmapFusion (\x => x + 1) (\x => x * 2) [1, 2, 3]
136+
137+
||| The fused result is exactly what we expect (fully reduced, asserted by Refl).
138+
export
139+
fusionConcreteValue : bmap (\x => (x * 2) + 1) [1, 2, 3] = [3, 5, 7]
140+
fusionConcreteValue = Refl
141+
142+
--------------------------------------------------------------------------------
143+
-- Negative / non-vacuity control
144+
--------------------------------------------------------------------------------
145+
146+
||| Non-vacuity: fusion is order-sensitive. Mapping `(*2)` then `(+1)` is NOT
147+
||| the same as mapping `(+1)` then `(*2)` on this input — i.e. the law genuinely
148+
||| depends on composing in the right order, it is not "any two maps fuse to
149+
||| anything". This refutes the WRONG fusion and proves the theorem has content.
150+
export
151+
fusionOrderMatters :
152+
Not (bmap (\x => x + 1) (bmap (\x => x * 2) [1])
153+
= bmap (\x => x * 2) (bmap (\x => x + 1) [1]))
154+
fusionOrderMatters Refl impossible
155+
156+
||| Second non-vacuity control: `bmap` is not the constant-empty function —
157+
||| it actually produces a non-empty array from a non-empty input, so the
158+
||| length-preservation theorem is not vacuously about empty lists.
159+
export
160+
bmapNonTrivial : Not (bmap (\x => x + 1) [5] = [])
161+
bmapNonTrivial Refl impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Bqniser.ABI.Types
1010
, Bqniser.ABI.Foreign
1111
, Bqniser.ABI.Proofs
1212
, Bqniser.ABI.Semantics
13+
, Bqniser.ABI.Invariants

0 commit comments

Comments
 (0)