Backend-neutral vectorization eligibility gate

Goal

Implement the gate that proves a loop is safe to vectorize.

Implementation Sketch

From canonical typed IR plus the frozen AIMS ownership/disjointness facts, prove no loop-carried dependence (data + captured-mutable + stateful-adaptor), capability purity, element-body panic-freedom, primitive-Value lane, and a statically-analyzable trip count. Classify reductions reorder-safe vs reorder-unsafe.

This eligibility analysis is backend-neutral but is not part of the AIMS calculus. AIMS supplies only its logical ownership, alias/disjointness, effect, and unwind facts; it does not select SIMD instructions, lane widths, LLVM metadata, or any other physical vectorization mechanism. VM and compiled planners may consume one eligibility verdict, while the evaluator remains the scalar behavioral oracle unless the language defines a reordered evaluation mode.

Spec References

Proposal §1 gate table; §4 reduction-reassociation stance.

Work Items

• Implement the provability gate: prove no loop-carried dependence (data AND through captured-mutable state / stateful adaptors), capability purity, element-body panic-freedom, primitive-Value lane, and statically-analyzable trip count.
• Classify reductions: reorder-safe (bitwise / min / max incl. float min/max via Ori’s total order on float) vs reorder-unsafe (checked int +/, FP +/); implement the no-overflow promotion analysis that can lift a bounded checked-int reduction to reorder-safe.
• Emit the per-loop eligibility verdict plus the cost-model-veto reason as queryable analysis output the codegen + diagnostic consume.