{include:preamble}
TARGET: {op_name}
PROPERTY: {law_name} ({law_description})
ORACLE: Algebraic law — the checker has verified this law holds exhaustively on u8.
INPUT CLASS: {input_class}
Write a test that asserts {law_formula} for inputs {specific_inputs}.
The test must fail if:
- The law declaration is removed from the OpSpec for {op}
- The identity/absorbing element in the law declaration is corrupted
- The op's reference_fn is swapped with a non-{law}-satisfying function
REQUIRED:
- Use only values from the input class.
- Use the reference interpreter as execution environment.
- Assert the law formula directly, not by computing expected values.
FORBIDDEN:
- DO NOT compute the expected value and assert equality. Assert the law formula structurally.
- DO NOT test more than one law per test.
- DO NOT use random or property-based inputs.