feat(compiler): add peephole optimization system for dMIR and x86 CgIR

.github/workflows/dtvm_evm_test_x86.yml

@@ -668,3 +668,86 @@ jobs:
         run: |
           echo "::error::Performance regression detected in ${{ matrix.mode }} mode. See logs for details."
           exit 1
+
+  peephole_validation_and_timing_budget:
+    name: Peephole Validation and Timing Budget Check
+    runs-on: ubuntu-latest
+    container:
+      image: dtvmdev1/dtvm-dev-x64:main
+    steps:
+      - name: Check out code
+        uses: actions/checkout@v3
+        with:
+          submodules: "true"
+
+      - name: Build dtvm and x86CgPeepholeTests
+        run: |
+          export LLVM_SYS_150_PREFIX=/opt/llvm15
+          export LLVM_DIR=$LLVM_SYS_150_PREFIX/lib/cmake/llvm
+          export PATH=$LLVM_SYS_150_PREFIX/bin:$PATH
+          cmake -S . -B build \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DZEN_ENABLE_SINGLEPASS_JIT=OFF \
+            -DZEN_ENABLE_MULTIPASS_JIT=ON \
+            -DZEN_ENABLE_EVM=ON \
+            -DZEN_ENABLE_SPEC_TEST=ON \
+            -DZEN_ENABLE_CPU_EXCEPTION=ON \
+            -DZEN_ENABLE_VIRTUAL_STACK=ON
+          cmake --build build --target dtvm --target x86CgPeepholeTests --target dmirValidationTests -j$(nproc)
+          bash tools/easm2bytecode.sh tests/evm_asm tests/evm_asm
+
+      - name: Verify .inc generator output is up-to-date
+        run: |
+          python tools/generate_x86_cg_peephole.py \
+            --rules src/compiler/target/x86/x86_cg_peephole_rules.json \
+            --out-inc /tmp/x86_cg_peephole_generated_check.inc \
+            --out-report /tmp/x86_cg_peephole_report_check.txt
+          diff /tmp/x86_cg_peephole_generated_check.inc \
+            build/src/compiler/generated/target/x86/x86_cg_peephole_generated.inc
+
+      - name: Run peephole rule validation check
+        run: |
+          python tools/check_x86_cg_peephole_validation.py \
+            --rules src/compiler/target/x86/x86_cg_peephole_rules.json \
+            --gtest-binary build/x86CgPeepholeTests
+
+      - name: Run dmir rewrite validation tests
+        run: ./build/dmirValidationTests
+
+      - name: Collect compiler pass timings
+        run: |
+          python tools/collect_compiler_pass_timings.py \
+            --dtvm build/dtvm \
+            --manifest tests/evm_asm/compiler_pass_timing_manifest.json \
+            --runs 5 \
+            --output /tmp/ci_timing_report.json \
+            -- --format evm --mode multipass --compile-only
+
+      - name: Refresh timing budgets from CI data
+        run: |
+          python tools/update_compiler_pass_timing_budget.py \
+            --report /tmp/ci_timing_report.json \
+            --out /tmp/ci_budget_x86_cg_peephole.json \
+            --budget-in tests/evm_asm/compiler_pass_timing_budget_x86_cg_peephole.json \
+            --target-pass x86_cg_peephole \
+            --manifest tests/evm_asm/compiler_pass_timing_manifest.json \
+            --runs 5
+          python tools/update_compiler_pass_timing_budget.py \
+            --report /tmp/ci_timing_report.json \
+            --out /tmp/ci_budget_dmir_rewrite.json \
+            --budget-in tests/evm_asm/compiler_pass_timing_budget_dmir_rewrite.json \
+            --target-pass dmir_rewrite \
+            --manifest tests/evm_asm/compiler_pass_timing_manifest.json \
+            --runs 5
+
+      - name: Check timing budget (x86_cg_peephole)
+        run: |
+          python tools/check_compiler_pass_timing_budget.py \
+            --budget /tmp/ci_budget_x86_cg_peephole.json \
+            --report /tmp/ci_timing_report.json
+
+      - name: Check timing budget (dmir_rewrite)
+        run: |
+          python tools/check_compiler_pass_timing_budget.py \
+            --budget /tmp/ci_budget_dmir_rewrite.json \
+            --report /tmp/ci_timing_report.json

docs/changes/2026-03-30-peephole-optimization-system/README.md

@@ -0,0 +1,67 @@
+# Change: Peephole Optimization System for dMIR and x86 CgIR
+
+- **Status**: Implemented
+- **Date**: 2026-03-30
+- **Tier**: Full
+
+## Overview
+
+A two-level peephole optimization system targeting both dMIR (mid-level IR) and x86 CgIR (code generation IR). The dMIR level has 65 accepted rewrite rules, plus 5 hand-written starter rules, covering identity elimination, boolean algebra, shift-zero, and carry-dead rewrites. The x86 CgIR level has 13 declarative JSON rules for self-moves, zero-shifts, redundant CMP/TEST, fallthrough branches, and setcc+test+jne chain folding. The Z3-synthesized subset of the dMIR rules carries a formal proof, and a CI validation gate enforces rule freshness, semantics, and a compile-time budget.
+
+## Motivation
+
+The JIT compiler generated redundant instructions from mechanical U256 decomposition and lowering. Peephole optimization is a standard compiler technique to clean up such patterns without restructuring the pipeline. The two-level approach catches patterns at both the IR and machine code level.
+
+## Impact
+
+### Affected Modules
+
+- `docs/modules/compiler/` — new dMIR rewrite pass, carry-dead analysis, rule table infrastructure
+- `docs/modules/singlepass/` — x86 CgIR peephole pass
+- CI pipeline — new `peephole_validation_and_timing_budget` job
+
+### Affected Contracts
+
+No API or interface changes.
+
+### Compatibility
+
+- No breaking changes
+- +4.6% geomean improvement on evmone-bench (27 benchmarks)
+- Notable wins: snailtracer +3.9%, structarray_alloc +4.1%, swap_math +5.0% to +5.8% across runs, memory_grow_mstore +11% to +13% across runs
+- ~0.005ms p95 compile overhead from dMIR rewrite pass
+
+## What Changed
+
+### dMIR rewrite infrastructure
+
+A pattern-matching framework, rule table, and validation tests for the dMIR
+rewrite pass.
+
+### Carry-dead analysis
+
+`isCarryDead()` rewrites adc→add and sbb→sub on dead-carry limbs.
+
+### Z3-synthesized rules
+
+`add(x,x)→shl(x,1)`, negation folding, and boolean identities, generated and
+formally verified via `tools/synthesize_dmir_rules.py`.
+
+### x86 CgIR peephole pass
+
+13 declarative JSON rules with pattern matching on machine instructions.
+
+### CI validation gate
+
+`.inc` freshness check, structural/execution/semantics validation, and
+compile-time budget enforcement.
+
+## Compatibility Notes
+
+No backwards-incompatible changes. The optimization passes are additive and do not alter any external APIs or module interfaces.
+
+## Risks
+
+- Rewrite rules must preserve U256 semantics exactly; the Z3-synthesized rules carry a formal proof, but the carry-dead rewrites rely on the carry-chain liveness analysis, where an edge case could be missed
+- Compile-time budget (0.005ms p95) may need adjustment as more rules are added
+- JSON rule format for x86 CgIR is a new abstraction layer that adds maintenance surface

docs/changes/2026-04-18-dmir-synth-s3-extension/README.md

@@ -0,0 +1,160 @@
+# Change: dMIR synth extended enumeration — auto-synthesize all 70 production dMIR rules
+
+- **Status**: Implemented
+- **Date**: 2026-04-18
+- **Tier**: Light
+
+The dMIR rule synthesizer now reproduces all 70 production rewrite rules
+(69/69 canonical patterns, 70/70 by name); the change is Python-tooling-only,
+with no C++ touched.
+
+## Overview
+
+Extend the dMIR rule synthesizer (`tools/synthesize_dmir_rules.py`) so that its
+output covers the 70 hand-written production rewrite rules in
+`src/compiler/mir/dmir_rewrite_rules.json`. The changes are all in the Python
+tooling layer: richer enumeration, a pattern-config import path reusing the
+seed-miner config, always-on Z3 verification for pattern pairs, and canonical
+dedup against existing rules and commute-variant twins. No C++ or production
+compiler pipeline is touched.
+
+## Motivation
+
+The prior feasibility study
+(`docs/research/directions/peephole-optimization/submissions/experiments/m1b-70rules-synth/report.md`)
+found 0/70 alpha-normalized LHS overlap between the 458 synth survivors
+and the 70 production rules. Root cause was mechanical, not fundamental:
+signature dedup in `ExprBank` discarded structural-equality LHS (`(and x x)`
+collapses to `x`), `CONSTANTS` lacked small integers like `2`, and
+`BINARY_OPS` excluded `not` / `select` / `shl` / `ushr` / `sshr` as LHS tops.
+Each gap is a small, local pipeline addition — the extended-enumeration
+approach from the report (richer LHS tops, depth-2 RHS, expanded constant
+set), extended with a pattern-config import path for the structural-equality
+family that the pure enumerator cannot express.
+
+## Impact
+
+Single module: `tools/` (Python synthesis tooling). No runtime, no C++
+compiler code, no header files. Synth output JSON gains a `source` field
+(`enumerator` or `pattern_config`) — already accepted by the duck-typed
+validator in `tools/test_check_dmir_rewrite_rules.py`.
+
+### Scope changed
+
+**Primary files (3)**:
+- `tools/synthesize_dmir_rules.py` — expanded LHS tops, depth-2 RHS
+  patterns, Z3 select encoder, `expand_pattern_config` integration, always-Z3
+  path for pattern pairs, `--no-z3` scope restricted to enumerator, provenance
+  `source` field, commute-variant collapse, dedup-against-existing pass.
+- `tools/mine_dmir_seed_rules.py` — added `__all__` and a docstring so
+  `synthesize_dmir_rules.py` can import the miner's pattern config as a library.
+- `tools/measure_prod_overlap.py` (new file) — measures prod-70
+  coverage on synth output using `canonicalize_expr` for alpha-normalized LHS
+  comparison; counts by unique canonical pattern (69 unique of 70 — one
+  commutative twin pair).
+
+**New tests (3)**:
+- `tools/test_synth_pattern_struct_eq.py` — structural-equality LHS
+  (`(and x x)`, `(or x x)`, `(xor x x)`) must survive.
+- `tools/test_synth_pattern_coverage.py` — ≥12 specific prod-rule names must
+  be discovered end-to-end; pins the discovered rule names as a regression guard.
+- `tools/test_synth_commute_dedup.py` — no commute-variant duplicates in final
+  output.
+
+## Metrics
+
+### Before (prior feasibility-study baseline)
+
+- `0/70` alpha-normalized LHS overlap between synth output and production rules.
+- 458 synth candidates, 318 survivors after the drop-0-var and subsumption
+  filter, none matched a prod rule.
+
+### After (final synthesis run)
+
+- **Matched prod unique patterns: 69/69**
+- **Matched prod names: 70/70** (one commutative-twin pair — `or x y` vs
+  `or y x` — collapses to a single canonical pattern, which both rules match).
+- Total synth rules: 1966 (unique canonical LHS keys: 1964, since two pairs
+  share canonical form after alpha-normalization).
+- Source split: 1856 enumerator + 110 pattern_config = 1966.
+- Z3 verification: always on for pattern-config pairs. `--no-z3` only skips
+  the enumerator's Z3 pass (pattern-config cross-product emits invalid pairs
+  that only Z3 can filter, so this path is non-optional).
+- Pattern-config pairs: 2964 candidates → 349 Z3-verified → 110 new after
+  dedup against enumerator output and the existing `dmir_rewrite_rules.json`.
+- Elapsed: ~140s at `--max-depth 2`.
+
+### Test coverage
+
+All 7 Python unit tests pass:
+
+| Test | Status |
+|------|--------|
+| `tools/test_mine_dmir_seed_rules.py` | PASS |
+| `tools/test_mine_dmir_novel_rules.py` | PASS |
+| `tools/test_mine_dmir_bootstrap_config.py` | PASS |
+| `tools/test_check_dmir_rewrite_rules.py` | PASS (accepts new `source` field) |
+| `tools/test_synth_pattern_struct_eq.py` | PASS (new) |
+| `tools/test_synth_pattern_coverage.py` | PASS — 12/12 required rules, 69 total matches |
+| `tools/test_synth_commute_dedup.py` | PASS — 0 commute duplicates in 1966 rules |
+
+## Risk / Rollback
+
+Risk: Low.
+
+- All changes live in `tools/` (Python tooling). No C++ source is touched, no
+  production compiler pipeline is changed, no header APIs shift.
+- The `source` field is additive. `tools/check_dmir_rewrite_rules.py`
+  duck-types it and remains green.
+- Z3 always-on for pattern pairs means `--no-z3` no longer produces unverified
+  output for the pattern-config path — explicit (reported as a stderr line in
+  synth output), not silent.
+- The hand-written `src/compiler/mir/dmir_rewrite.h` C++ switch is untouched.
+  Synth output remains advisory tooling data, not compiled-in rewrites — the
+  same invariant `reference_dmir_rule_spec_vs_runtime.md` documents.
+
+**Rollback**: `git revert` the 11 tool commits on this branch (or
+`git reset --hard 04f2c8a` to the branch base). No persistent state change.
+
+## Follow-ups
+
+1. **Not in scope**: integrating the `pattern_config`-sourced 110 rules into
+   the hand-coded `src/compiler/mir/dmir_rewrite.h` C++ switch. That is a
+   separate code-generation effort and was never part of this tooling change.
+2. **Not currently needed**: widening `DEFAULT_SEARCH_CONFIG.base_terms`
+   beyond the present set. Full prod-70 coverage (69/69 canonical patterns) is
+   reached with the current terms; adding more would inflate the search space
+   without adding matches.
+
+## References
+
+- Plan: `docs/superpowers/plans/2026-04-18-dmir-synth-s3-extension.md`
+- Feasibility study (motivation):
+  `docs/research/directions/peephole-optimization/submissions/experiments/m1b-70rules-synth/report.md`
+- Direction: `docs/research/directions/peephole-optimization/`
+- Related invariant:
+  `~/.claude/projects/-home-abmcar-DTVM/memory/reference_dmir_rule_spec_vs_runtime.md`
+  (synth output is tooling-layer; runtime rewrites are hand-coded in
+  `dmir_rewrite.h`).
+
+## Checklist
+
+- [x] Implementation complete
+- [x] Tests added/updated (3 new tests, all green)
+- [ ] Module specs in `docs/modules/` updated (N/A — tooling only, no module
+      contract change)
+- [x] Build and tests pass (7/7 Python tests pass; `tools/format.sh check`
+      clean; no C++ touched so no cmake build required)
+
+## Coverage across synthesis modes
+
+Synthesis covers 71 dMIR production rules across two modes: the 70 scalar-limb
+rules plus `u256-xor-self-zero`, the latter validated through a separate u256
+composite lane.
+
+- scalar synthesis coverage: 70/70 production names
+- scalar canonical-pattern coverage: 69/69 because one commutative-twin pair
+  shares a canonical representative
+- u256 synthesis coverage: 1/1 production names
+- total dMIR production coverage: 71/71 names across the two synthesis modes,
+  with both coverage tests passing

docs/changes/2026-04-26-u256-composite-peephole-evidence/README.md

@@ -0,0 +1,24 @@
+# Change: U256 composite peephole evidence for xor-self-zero
+
+- **Status**: Implemented
+- **Date**: 2026-04-26
+- **Tier**: Light
+
+## Overview
+
+`u256-xor-self-zero` rewrites each limb result of `u256_xor(x, x)` to zero
+after checking that the corresponding left/right limbs are structurally equal.
+This change moves the rule from a branch-only extension into the main rule set,
+covered by unit tests and a 256-bit SMT proof. The rule lets the compiler fold
+a self-XOR to a constant zero without a runtime computation.
+
+## Evidence
+
+- Metadata checker accepts `synthesized-u256` and `smt_256`.
+- `dmirValidationTests` covers the positive rewrite and negative non-matches.
+- `tools/verify_dmir_u256_soundness.py` runs a Z3 proof that the rewrite equals
+  zero for all 256-bit inputs.
+- `tools/test_synth_u256_pattern_coverage.py` verifies synthesis rediscovery.
+- The change adds one composite U256 rule to the dMIR rule set, bringing the
+  total to 71: 70 scalar-limb rules plus one composite U256 rule.
+- Both CTest and the peephole GitHub Actions job run the checks listed above.