idea: flow-sensitive Int.div/Int.mod safety-elision (MIR optimizer, not type-level)

[jasisz]

Exploratory idea, 0.25+. Not committed work.

The idea

0.24's const-folder (#435) folds the Int.div/Int.mod Result round-trip away when the divisor is a literal constant. Extend that elision to a non-literal divisor when the MIR optimizer can prove it's safe from control flow:

match b > 0
    true  -> ... Int.div(a, b) ...   # b > 0 holds here => can't trap => fold the Result + the match/withDefault around it down to a bare division
    false -> ...

Same payoff as the constant case ("the explicit Result disappears when it provably can't fail"), just triggered by a flow fact instead of a literal.

This is optimizer-level, NOT a refinement type

Int.div keeps its Result type; the source stays explicit. So this does not reopen the rejected "refinement / dependent types in the typechecker" direction (#407 was killed for that). It's the same "optimizer privilege" as the const-fold — totality is the user's model, eliding a proven-safe check is the optimizer's privilege.

Soundness condition (the subtle part)

Int.div(a, b) traps iff b == 0 or (a == i64::MIN && b == -1). To fold, the analysis must prove b ∉ {0, -1} on the path:

• b > 0 / b >= 1 → folds (rules out both 0 and -1).
• plain b != 0 → not enough: b could be -1 and a could be MIN → overflow. Keep the Result (or additionally prove b != -1).
• b < 0 → not enough either (-1 is in range).

This is exactly the {0, -1} exclusion the const-folder already encodes (it folds a literal k only for k ∉ {0, -1}).

Cost

Needs a flow-sensitive range/predicate analysis on MIR — propagate branch facts (b > 0 into the true arm), join at merge points, fixpoint. That's qualitatively beyond the current const-folder, which is bottom-up and literal-driven with no dataflow. A real new pass.

Payoff caveat

Guarding the divisor immediately before dividing is a less common pattern than a constant divisor, and Result.withDefault(Int.div(a, b), 0) already gives a cheap "I know it's safe" path. So as a standalone pass (just for division) the cost/benefit is weak.

Recommended framing

div/mod safety-elision is a natural client of a general MIR value-range analysis. If/when one exists for other wins (bounds-check elimination on Vector.get/Map.get, dead-arm elimination, loop opts), this rides on it nearly for free. Not worth building the dataflow machinery for division alone.