# Strength reduction under modular arithmetic

KL-FCS-011 · Compiler optimization · version 1.0.0

## Problem

Check the rewrite x × 2 → x + x for every unsigned four-bit x.

## Context

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.

## Checked result

Equivalent: yes.

For each possible input, the original and replacement expressions yield the same four-bit result, including values that wrap.

## Checker reasoning

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.

## Dataset construction

{
  "family": "compiler",
  "task": "Check the rewrite x × 2 → x + x for every unsigned four-bit x.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete bit-vector equivalence · 16 inputs",
  "acceptance": [
    "Enumerate every value at the chosen bit width.",
    "Evaluate the source expression modulo 2ʷ.",
    "Evaluate the replacement under the same semantics.",
    "Compare outputs, including wraparound inputs."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "width": 4,
    "source": "x * 2",
    "semantics": "Pure expressions on four-bit values, with both operators modulo 16 and no observable side effects."
  },
  "claim": {
    "equivalent": true
  },
  "witness": {
    "replacement": "x + x"
  }
}
```

## Complexity

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

## Limits

This example does not establish a rewrite for language undefined behavior, side effects, overflow flags, other widths, or floating-point arithmetic. No speedup is claimed.

## Common error and further work

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

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

## Verification

Complete bit-vector equivalence · 16 inputs. 16 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html)