# Compiler optimization

A rewrite is correct when source and target agree under the exact language semantics and observable behavior.

## Definitions

- **Semantic equivalence**: The same observable result for every input in the declared domain.
- **Modular arithmetic**: Arithmetic wraps modulo 2ʷ for width w.
- **Strength reduction**: Replacing an operation with another expression whose performance must be evaluated separately.

## Acceptance procedure

1. Enumerate every value at the chosen bit width.
2. Evaluate the source expression modulo 2ʷ.
3. Evaluate the replacement under the same semantics.
4. Compare outputs, including wraparound inputs.

## Complexity

Unary width-w equivalence by enumeration checks 2ʷ inputs. This is practical for small widths, not a general large-program optimizer.

## Common failure

Correctness is not a speedup claim; duplicating an expression with side effects can be invalid.

## Extensions

Add expression DAGs, observable-state semantics, and checked equivalence certificates.

## Instances

- KL-FCS-011: Strength reduction under modular arithmetic — Equivalent: yes
- KL-FCS-026: Eliminate an eight-bit neutral addition — Equivalent: yes
- KL-FCS-027: Triple a six-bit value by addition — Equivalent: yes

## References

- https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html