# Algebraic Verification
The algebra proof engine verifies that each operation satisfies every
`AlgebraicLaw` declared in its `OpSpec`. It treats laws as structural
requirements, generates the input tuples needed by each law, evaluates both
sides, and reports concrete counterexamples for any disagreement.
## How Checking Works
For each registered operation, the checker reads the operation's law list. For
each law, it selects the law-specific verification procedure. Commutativity
checks `f(a, b)` against `f(b, a)`. Associativity checks `f(f(a, b), c)` against
`f(a, f(b, c))`. Identity, self-inverse, idempotence, absorbing, involution,
boundedness, and zero-product checks each have their own required input shape.
Cross-operation and custom law variants exist in the type model but are not
executed by the current checker.
The checker first self-tests the CPU reference. A law that fails on the CPU
reference proves the registry entry is invalid. Only a self-consistent
operation can be used to judge a backend.
The checker then verifies backend behavior with the same law semantics. A
failure records the operation, law, inputs, left-hand side, right-hand side,
and a fix-oriented message.
## Exhaustive Verification
Exhaustive verification checks every input tuple in a small complete domain,
such as all `u8` values embedded in `u32`. For a binary law, that means every
pair. For a ternary law such as associativity, it means every triple in the
chosen small domain. Inside that domain, the result is a proof: there are no
untested values.
## Witnessed Verification
Witnessed verification checks deterministic random and adversarial inputs in
the full production domain, such as `u32`. It cannot cover all `2^32` values,
but it reaches high bits, carries, masked shift behavior, maximum values, and
other cases that a small-domain proof cannot represent.
Witnesses are seed-based. A failing witness can be replayed exactly and becomes
a regression input.
## Combined Verification
Combined verification runs exhaustive and witnessed verification together. It
proves the complete small domain and samples the full domain with deterministic
witnesses. This is a practical proof: exact where exhaustive checking is
tractable, broad where full exhaustiveness is impossible.
L2 conformance requires this combined shape for algebraic laws: exhaustive on
the small domain and witnessed on the full domain.
## Scope
Algebraic verification proves declared laws, not undeclared laws. Passing all
law checks means the operation satisfies its registered structural
specification under the checked domains. When a law set is not unique, parity
against the CPU reference remains the tiebreaker for exact function identity.