feat(#240): Z3-verified algebraic mid-end (strength-reduction) + range-premise hook

[avrabe]

Refs #240 (part 1 of 2). Extends the term simplifier with instruction-count-reducing rewrites toward beat-LLVM parity. Every rule is Z3-verified by loom's translation validator (the machine-checked proof); a rule the validator rejects reverts, so nothing unproven ships.

Tier 1 — unconditional folds (fire on real code today)

Each confirmed Z3-accepted (the 4 loom-core pipeline tests run full optimize_module with verification on and assert the fold happened + re-encodes):

1. (x<<k) >>u k → x & (0xFFFFFFFF >>u k) (i32, 0<k<32) — collapses synth's 256*(ch-1024)>>8 shape into a single mask today (i64 analogue already existed from opt: dissolve the seam fully — post-inline SROA/scalar-forwarding eliminates the u64 ABI pack/unpack (+ wasm-local mem2reg) → toward LLVM-LTO parity #219).
2. (x<<a)<<b → x<<(a+b) (i32/i64, a+b<width).
3. (x>>u a)>>u b → x>>u(a+b) (i32/i64, a+b<width).
4. (x&c1)&c2 → x&(c1&c2) (i32/i64, recurses into the existing &-1/&0 identities).
   All width-gated so the wasm shift-mod-width wrap can't change meaning. No existing rule regressed.

Tier 2 — range-premise hook (prototype; gust win gated on #231)

• Premise representation: OptimizationEnv.value_max: HashMap<Value,u64> (inclusive unsigned upper bound) + assume_max / fits_below_bit. Empty by default ⇒ byte-identical to plain dataflow with no premises.
• Gated rewrite: (x<<k)>>u k → x (drop the mask entirely, LLVM parity) fires only when a premise proves x < 2^(width-k); else degrades to the Tier-1 mask. Z3-verified under the assumption; 3 tests (fires with x<2^24, not without, not under a too-weak 2^25 bound).
• Deferred (honest boundary): wiring the real fact-source that populates value_max from machine-checked Verus/Rocq value-range facts is Carry Verus value-range/no-alias facts as IR premises + algebraic mid-end — feed synth's beat-LLVM specialization #240 part 2 / Design: proof-carrying wsc.facts section — loom forwards Z3-discharged invariants to synth #231 (gale/synth fact-format co-design). Not faked; the gust beat-LLVM number does not land until that contract is wired. Co-design note: premises must key on the post-simplification Value the gate sees.

Proofs

The Z3 translation validator is the machine-checked proof for every rule here. Matching Rocq theorems for StrengthReduction.v were drafted but not committed — the repo's Rocq build fails upstream in TermSemantics.v (the known Rocq CI breakage, #169) before reaching new content, so they can't be attested to compile; per the correctness philosophy, unverifiable .v is not shipped. Inline algebraic-soundness notes accompany each rule.

Checks

13 new tests (9 loom-shared unit + 4 loom-core pipeline). cargo test --release --workspace green; clippy clean; fmt clean.

Part of v1.2.0 (with #257). 🤖 Generated with Claude Code

[temper-pulseengine]

Automated review for PR #259

pulseengine/loom:feat/240-algebraic-mid-end → pulseengine/loom:main

Verdict: 🔴 Request changes

Summary: Adds Z3-verified algebraic mid-end optimizations to the Loom project.

Findings: 7 mechanical (rivet) · 0 from local AI model.

Findings (7):

1. 🟡 6 artifacts (rivet-validate)
   field 'evidence-type' has value 'test', allowed: ["test-report", "analysis", "simulation", "review", "field-data", "formal-proof"] — affecting: SOL-8, SOL-6, SOL-3, SOL-7, SOL-5, SOL-4

2. 🟡 6 artifacts (rivet-validate)
   field 'goal-type' has value 'top-level', allowed: ["system-level", "element-level", "operational", "derived"] — affecting: SG-2, SG-4, SG-6, SG-3, SG-5, SG-1

3. 🔴 6 artifacts (rivet-validate)
   Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped
   — affecting: SG-1, SG-2, SG-3, SG-4, SG-5, SG-6

4. 🟡 6 artifacts (rivet-validate)
   Top-level safety goals should have context defining scope and assumptions — affecting: SG-1, SG-2, SG-3, SG-4, SG-5, SG-6

5. 🟡 6 artifacts (rivet-validate)
   STPA losses should be addressed by safety goals in the safety case — affecting: L-1, L-2, L-3, L-4, L-5, L-6

6. 🔴 3 artifacts (rivet-validate)
   link type 'acted-on-by' is not defined in the schema — declare it in link-types: or remove the link — affecting: CP-2, CP-3, CP-1

7. 🟡 16 artifacts (rivet-validate)
   conditional rule 'approved-needs-description': field 'description' is required when condition is met — affecting: SC-CTXT-2, SG-5, SS-1, SG-3, SC-CTXT-4, SOL-7, SC-CTXT-5, SOL-6, SS-2, SG-6 (+6 more)

---

Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at 5087441