# Compositional Verification
Compositional verification checks that chains of correct operations still produce correct results when glued together.
## Why Composition Fails
Individual operations can pass parity and algebraic checks while a chain of two or more operations fails because of:
- Calling convention mismatches (buffer layout, binding indices)
- Type width changes that truncate or pad unexpectedly
- Output of op A not valid input for op B
- Buffer reuse bugs (op B reads op A's stale bytes)
- Workgroup size disagreements between ops
## How It Works
1. **Chain generation**: Strategies (e.g., pairwise) generate valid multi-op sequences such as `xor -> popcount -> add`.
2. **CPU reference**: The harness runs each input through the operations sequentially on the CPU, using each op's own reference function.
3. **Backend chain**: The harness dispatches the composed WGSL (or dispatches ops sequentially, depending on the composer) on the GPU.
4. **Comparison**: Final GPU bytes are compared to final CPU bytes.
## Chain CPU Reference
If a `ChainSpec` provides `cpu_chain`, that function is the authority for the entire chain. Otherwise, the harness computes the CPU reference by feeding the output of each step into the next step's reference function.
## Coverage
Compositional verification is required for L4 conformance.