# Triple a six-bit value by addition

KL-FCS-027 · Compiler optimization · version 1.0.0

## Problem

Check a pure unsigned modular rewrite at every input.

## 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.

The checker evaluates both expressions at every representable value. Overflow wraps identically in the two expressions.

## 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 a pure unsigned modular rewrite at every input.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete equivalence · 64 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": 6,
    "source": "x * 3",
    "semantics": "Pure unsigned 6-bit arithmetic modulo 64, with no side effects."
  },
  "claim": {
    "equivalent": true
  },
  "witness": {
    "replacement": "(x + 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

The result does not transfer automatically to signed-overflow undefined behavior or effectful expressions.

## 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 equivalence · 64 inputs. 64 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)