# Algebraic Verification
Algebraic verification proves structural truth: the shape of the function, not just its value at sampled points.
## What It Checks
For each operation, the checker reads the declared `laws` from `OpSpec`. For every law, it evaluates both sides of the equation using the CPU reference (for self-test) and the backend dispatch (for conformance), then reports any mismatch as a concrete counterexample.
## Checked Law Variants
- **Commutative**: `f(a, b) = f(b, a)`
- **Associative**: `f(f(a, b), c) = f(a, f(b, c))`
- **Identity**: `f(a, e) = a` and `f(e, a) = a`
- **SelfInverse**: `f(a, a) = r`
- **Idempotent**: `f(a, a) = a`
- **Absorbing**: `f(a, z) = z` and `f(z, a) = z`
- **Involution**: `f(f(a)) = a`
- **Bounded**: `lo <= f(a) <= hi`
- **ZeroProduct**: either verify the property holds or, for
`ZeroProduct { holds: false }`, verify that a counterexample exists.
`AlgebraicLaw` also defines `DeMorgan`, `Complement`, `DistributiveOver`,
`Monotone`, and `Custom`, but the current algebra checker does not evaluate
those cross-operation or custom variants. Registry entries must not list them
as declared laws until checker support exists.
## Self-Test
Before a backend is ever judged, the CPU reference is tested against every declared law. If the reference violates a law, the registry entry is internally inconsistent and cannot be used for certification.
## Backend Check
The same law semantics are applied to backend output. A law failure produces a `LawViolation` containing:
- Operation ID
- Law name
- Concrete inputs (a, b, c)
- Left-hand side and right-hand side values
- Actionable fix message
## Scope
Passing algebraic verification means the operation satisfies its declared structural properties on the checked domains. It does not guarantee uniqueness unless the law set is known to uniquely characterize the operation.