Sprint 50: MIR Optimization Pass Phase 1 — constant fold, copy prop, dead blocks, peephole

Four-pass MIR optimizer with fixed-point iteration (max 3 rounds), validity
checker, --no-optimize CLI flag, 24 unit tests, 3 CLI integration tests,
.forma correctness test, and benchmark script. Documentation updated across
reference, ai-reference, changelog, README, WHY_FORMA, and sprint plans.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: sfw

CHANGELOG.md

@@ -42,11 +42,36 @@ All notable changes to FORMA are documented in this file.
 - Added security warnings for `--allow-all` and capability flags to README, reference.md, and ai-reference.md.
 - Replaced predictable `/tmp/forma_*` paths with `mktemp` and `trap` cleanup in contract test script.
 
+### MIR Optimization Pass (Phase 1)
+
+- Added `src/mir/optimize.rs` with four optimization passes: constant folding, copy propagation, dead block elimination, and peephole optimizations.
+- Optimization runs by default between MIR lowering and interpretation/codegen; disable with `--no-optimize`.
+- Passes run in fixed-point rounds (max 3) so one pass can unlock another.
+- Constant folding evaluates compile-time arithmetic, comparisons, and boolean logic; simplifies constant-condition `If`/`Switch` to `Goto`.
+- Copy propagation eliminates redundant compiler temporaries with chain resolution.
+- Dead block elimination removes unreachable blocks with BlockId remapping; includes jump threading for empty goto chains.
+- Peephole optimizations: nop removal, identity ops (`x+0`, `x*1`), `x*0` folding, double negation elimination, redundant return-temp elimination.
+- Added MIR validity checker (`validate_mir()`) for post-optimization invariant checking.
+- Added `--no-optimize` CLI flag to `run`, `build`, and `compile` commands.
+- 24 unit tests covering all optimization passes and safety guards.
+- 3 CLI integration tests verifying output equivalence with and without optimization.
+- `.forma` correctness test (`test_optimization.forma`) and benchmark script (`scripts/bench_optimize.sh`).
+
+### Contract Patterns Expansion
+
+- Expanded named contract patterns from 12 to 35 across 6 categories (numeric, collection, set, sequence, ordering, state).
+- Added 8 runtime contract helpers (`set_equals`, `is_prefix`, `is_suffix`, `is_reversed`, `is_rotated`, `is_partitioned`, `stable`, `value_le`).
+- Added `pattern_to_english()` for human-readable pattern descriptions in explain output.
+- Fixed `@rotated` panic on negative k values (uses `rem_euclid`).
+- Fixed `@stable` correctness: now enforces permutation check + nondecreasing key order + stable relative ordering.
+- Fixed `is_partitioned` negative index guard.
+
 ### Test + Coverage Improvements
 
 - Added CLI JSON failure-matrix tests for `run/check/build` across lex/parse/module/type failures.
 - Added capability matrix integration tests.
 - Expanded builtin coverage and added coverage enforcement support in CI.
+- Removed global `reset_type_var_counter()` calls from tests to fix parallel test flakes.
 
 ---
 

README.md

@@ -314,7 +314,7 @@ FORMA is in **active development**. The core language and standard library are f
 
 - [x] Lexer, parser, type checker
 - [x] Borrow checker (second-class references)
-- [x] MIR interpreter
+- [x] MIR interpreter with optimization pass (constant fold, copy propagation, dead block elimination, peephole)
 - [x] Generics with monomorphization
 - [x] Linear types and capability system
 - [x] Module system

docs/WHY_FORMA.md

@@ -181,6 +181,8 @@ Interpreted languages work well with AI — but they're not systems languages. Y
 
 No. FORMA compiles to native code via LLVM — the same backend powering Rust, Clang, and Swift. The second-class reference model doesn't prevent optimization; it just changes how the compiler reasons about memory.
 
+Before execution, FORMA runs a MIR optimization pass (constant folding, copy propagation, dead block elimination, peephole optimizations) that eliminates redundant temporaries and simplifies control flow. For LLVM builds, these MIR-level optimizations complement LLVM's own passes.
+
 For the same algorithms, FORMA should produce comparable machine code to Rust. We're not trading performance for simplicity — we're trading *language complexity* for *AI compatibility*.
 
 ## Who Is FORMA For?

docs/ai-reference.md

@@ -429,6 +429,7 @@ f main()
 forma run <file>                        # run program
 forma run <file> --allow-all            # run with all capabilities (DO NOT use on untrusted code)
 forma run <file> --no-check-contracts   # disable contracts (enabled by default)
+forma run <file> --no-optimize         # disable MIR optimization pass
 forma check <file>                      # type check only
 forma check <file> --error-format json  # JSON errors
 forma explain <file> --format json      # contract intent in JSON
@@ -441,6 +442,8 @@ forma verify <path> --report --max-steps 10000 --timeout 1000
 forma verify <path> --report --allow-side-effects
 forma grammar --format ebnf             # export grammar
 forma grammar --format json             # export grammar (JSON)
+forma build <file>                      # build native binary (LLVM)
+forma build <file> --no-optimize        # build without MIR optimization
 forma fmt <file>                        # format code
 forma repl                              # interactive REPL
 forma typeof <file> --position L:C      # type at position

docs/reference.md

@@ -1239,6 +1239,7 @@ Capability-gated groups:
 forma run <file>                   # Run a FORMA program
 forma run <file> --dump-mir        # Run with MIR dump
 forma run <file> --no-check-contracts # Disable runtime contracts
+forma run <file> --no-optimize     # Disable MIR optimization pass
 forma run <file> --allow-read      # Allow file reads
 forma run <file> --allow-write     # Allow file writes
 forma run <file> --allow-network   # Allow networking
@@ -1249,6 +1250,7 @@ forma run <file> --allow-all       # Allow all capabilities (see warning below)
 forma check <file>                 # Type check without running
 forma check <file> --partial       # Partial checking
 forma build <file>                 # Build native executable (LLVM feature)
+forma build <file> --no-optimize   # Build without MIR optimization
 forma explain <file>               # Explain contracts in plain English
 forma explain <file> --examples=3 --seed 42 --format json
 forma explain <file> --max-examples 3 --seed 42 --format json

planning/sprints/SPRINT_50_1_COPY_PROP_SOUNDNESS.md

@@ -0,0 +1,165 @@
+# Sprint 50.1: MIR Copy Propagation Soundness Hotfix
+
+## Goal
+
+Fix the semantic unsoundness in MIR copy propagation introduced in Sprint 50 by enforcing reassignment and control-flow safety. Preserve optimization benefits while guaranteeing behavior equivalence with `--no-optimize`.
+
+---
+
+## Why This Sprint Exists
+
+Current copy propagation in `src/mir/optimize.rs` builds a global substitution map and rewrites uses without proving safety across:
+
+1. source local reassignments, and
+2. control-flow joins/branches.
+
+This can rewrite a use to a newer value than the original copied value, producing incorrect runtime behavior.
+
+---
+
+## Scope
+
+### 50.1.1 Make Copy Propagation Sound by Construction (P0)
+
+**Files:** `src/mir/optimize.rs`
+
+Replace current global substitution strategy with a conservative, semantics-safe approach.
+
+### Required implementation constraints
+
+Implement **block-local forward propagation only** for Phase 1:
+
+1. Only propagate from `Assign(dest, Use(Copy(src)|Local(src)|Move(src)))`.
+2. `dest` must be a compiler temp (`LocalDecl.name == None`).
+3. Propagation candidates are valid **only within the same basic block**.
+4. Stop propagation when either `src` or `dest` is assigned again.
+5. Do not propagate through `Ref`, `Discriminant`, `EnumField`, or contract-sensitive contexts.
+6. Do not propagate into/through terminators if safety cannot be proven for block-local ordering.
+7. Never create/keep cyclic substitutions.
+
+This is intentionally conservative. Correctness is mandatory; aggressiveness can return in Sprint 51 with data-flow analysis.
+
+### Acceptance criteria
+
+1. No behavior divergence between optimized and non-optimized execution on reassignment/control-flow edge cases.
+2. Copy propagation still optimizes trivial safe chains inside a block.
+3. Existing optimizer tests pass.
+
+---
+
+### 50.1.2 Add Regression Tests for the Bug Class (P0)
+
+**Files:** `src/mir/optimize.rs` (test module), `tests/cli_tests.rs`, optionally `tests/forma/test_optimization.forma`
+
+Add targeted tests that failed conceptually under old logic:
+
+1. **Reassignment barrier test (unit):**
+   - copy temp from `x`,
+   - reassign `x`,
+   - ensure return/use still points to copied temp semantics.
+2. **Branch/join test (unit):**
+   - copy in one block,
+   - reassign source in successor,
+   - verify no illegal substitution through join.
+3. **CLI equivalence regression (integration):**
+   - run fixture with and without `--no-optimize`,
+   - assert identical stdout and exit code.
+
+### Acceptance criteria
+
+1. At least 3 new tests directly covering the unsoundness class.
+2. New tests fail on old algorithm and pass with fix.
+
+---
+
+### 50.1.3 Validate Optimizer Invariants Post-Pass (P1)
+
+**Files:** `src/mir/optimize.rs`
+
+After each optimization round (or in debug/test builds), run `validate_mir()` and fail fast in tests if invariants break.
+
+### Acceptance criteria
+
+1. Optimization tests assert `validate_mir(program).is_empty()`.
+2. Any malformed MIR from pass bugs is caught immediately.
+
+---
+
+### 50.1.4 Sprint-Report Accuracy Cleanup (P2)
+
+**Files:** sprint notes/docs only as needed
+
+Clarify .forma suite status from this environment:
+- `test_contract_errors.forma` is intentional negative.
+- `test_tcp.forma` may be environment-dependent and not introduced by Sprint 50.
+
+Do not block merge on infra-dependent networking tests unless regression is proven against `--no-optimize`.
+
+### Acceptance criteria
+
+1. Sprint summary language is precise and non-misleading.
+
+---
+
+## Implementation Notes
+
+Recommended minimal algorithm (safe):
+
+1. For each basic block, scan statements top-to-bottom.
+2. Maintain a local map `dest -> src` valid for current scan window.
+3. On assignment to any local `l`, remove mappings where `dest == l` or `src == l`.
+4. Rewrite operands only using currently valid mappings.
+5. Do not carry mapping across block boundaries.
+
+This gives deterministic safety without requiring dominance/use-def infrastructure.
+
+---
+
+## Verification Plan
+
+```bash
+# Core
+cargo fmt --all -- --check
+cargo clippy --all-targets -- -D warnings
+cargo test --all
+
+# Targeted optimizer tests
+cargo test mir::optimize::tests -- --nocapture
+
+# Optimization equivalence check
+./target/release/forma run --allow-all tests/forma/test_optimization.forma > /tmp/opt_on.out
+./target/release/forma run --allow-all --no-optimize tests/forma/test_optimization.forma > /tmp/opt_off.out
+diff -u /tmp/opt_off.out /tmp/opt_on.out
+```
+
+Optional reproduction fixture (for manual validation):
+
+```forma
+f main() -> Int
+    x := 1
+    z := if true then x else 0
+    x := 2
+    if z == 1 then 0 else 99
+```
+
+Expected exit code is identical with and without optimization.
+
+---
+
+## Out of Scope
+
+1. Global data-flow copy propagation across blocks.
+2. Dominator tree construction.
+3. Dead store elimination.
+4. CSE/inlining/loop opts.
+
+---
+
+## Definition of Done
+
+1. Copy propagation no longer performs unsound cross-assignment or cross-flow rewrites.
+2. New regression tests for reassignment + branch/join cases are present and passing.
+3. `cargo test --all` passes.
+4. CLI output/exit equivalence for optimization fixture remains identical (`opt` vs `--no-optimize`).
+5. MIR invariants are validated after optimization in tests.
+