# Law Composition
Law composition turns verified operation laws into smaller composed-operation test spaces. A composition theorem is valid only when every referenced operation has already passed CPU parity and the declared law checks for the same spec version.
## Commutative Inner Reordering
If binary `f` is commutative, then for any unary or context operation `g` that only consumes the result of `f`:
```text
f(a, b) = f(b, a)
g(f(a, b)) = g(f(b, a))
```
This theorem does not require `g` itself to be commutative because `g` receives one value. If `g` is also a commutative binary operation and the composed expression is `g(f(a, b), c)`, then the verified fact still gives:
```text
g(f(a, b), c) = g(f(b, a), c)
```
The test generator therefore does not need to test both `(a, b)` and `(b, a)` for the inner operation when the outer context observes only the inner result.
## Identity Propagation
If binary `f` has identity `e`, then:
```text
f(a, e) = a
f(e, a) = a
g(f(a, e)) = g(a)
g(f(e, a)) = g(a)
```
For binary `g`, this lifts through either argument position:
```text
g(f(a, e), x) = g(a, x)
g(x, f(e, a)) = g(x, a)
```
Any generated composition containing `f(a, e)` can be reduced to the same test as `a` in that position. The reduction is legal only for a declared two-sided `Identity(e)` law, not a custom right-identity law such as `sub(a, 0) = a`.
## Associative Flattening
If `f` is associative, nested chains using only `f` can be flattened:
```text
f(f(a, b), c) = f(a, f(b, c))
```
The composition checker chooses one canonical grouping for parity and uses the law checker to verify alternate groupings. This catches backend order bugs without multiplying every chain by every parenthesization.
## Idempotent And Absorbing Reductions
If `f` is idempotent, duplicated equal operands collapse:
```text
f(a, a) = a
g(f(a, a)) = g(a)
```
If `f` has absorbing element `z`, any composition containing `f(a, z)` or `f(z, a)` reduces to `z`:
```text
f(a, z) = z
g(f(a, z)) = g(z)
```
These reductions are mandatory coverage cases because they exercise exactly the inputs where optimized GPU code often removes work.
## Test Space Reduction
Composition tests are generated from canonical representatives after applying all proven reductions. The checker still records which reductions were used in the failure context. A failed reduced test reports the original expression, the reduced expression, the theorem used, and `Fix: verify the referenced primitive law and the composed backend expression use the same operand order and identity element`.