Module Ir.Cost_model

The whole-kernel extraction: footprints from Low_level.affine_accesses image cardinalities, op counts from a loop-nest walk. Input is typically post-optimize code — the analysis charges whatever materialization the code actually performs, so virtual/inlined nodes never appear and recomputation is charged as ops, not bytes.

read_bytes + write_bytes: the "bytes moved" denominator of arithmetic intensity — an accumulation's cells are charged once in each direction.

FLOPs per byte moved, flops / max 1 (total_bytes).

true when any per-node footprint is an upper bound rather than exact (fp_approx) — the byte counts over-approximate while the op count may still be exact.

Lower bounds on arithmetic work and compulsory traffic — the dual extraction (gh-ocannl-514 phase 3), for bounding every completion of a partial placement vector where analyze upper-bounds one concrete candidate. fr_exact is false when some flooring-to-zero occurred (a guarded body, a non-exact access image, opaque code): the floor is then sound but not tight.

The floor of the roofline legs over placement completions, with every approximation biased down — the exact dual of analyze's contract:

• fr_flops: guarded (If) bodies count zero (guards-never-taken, dual to guards-taken); the short-circuiting forms count only their certain part — Where its condition plus the cheaper arm's inline work (rendered as ?:), And/Or the left operand's (rendered as &&/||), both sides' hoisted scope bodies in either case (they execute regardless, gh-ocannl-637), the Arg1/Arg2 projections only the selected operand (the discarded one is never rendered, hoisted definitions included); opaque code counts zero (an under-count is sound in this direction); Tile_mma keeps the lane-cooperative attribution, exact when the lane binding is in scope. Statements producing an open_placement node — the Set family and Tile_mma with an open accumulator — count zero: an inline completion instantiates the producer only at surviving consumer sites, possibly fewer cells than the setter loop covers, so "recomputation only adds ops" does not hold and the producer's whole effect attributes to the open placement. Call this on the all-materialized specialization of the decision surface, where every open node's work sits in its own producer statement.
• fr_bytes: per node and direction, the sum of the exact images when they are pairwise provably disjoint (a disjoint union attains its sum — both extractions then agree, gh-ocannl-578), otherwise the largest exact image (a union is at least its largest member — dual to the upper extraction's capped sum; a second nonzero contribution then marks the floor loose); guarded, non-exact, dead-loop-enclosed, conditionally-evaluated (a Where arm's or an And/Or right operand's inline read — not a hoisted scope body's) and open-producer-operand accesses contribute zero — their execution is not certain in every completion. Nodes with open_placement contribute zero.

Committing a placement decision is re-evaluation with the narrowed open_placement: the suppression sets only shrink, so the floor is monotone in refinement — the property that lets a bound prune as commitments accumulate. (An incremental per-node delta cannot be sound in isolation: a Materialize commitment also makes its producer's operations and operand reads certain, not just the node's own traffic.) Committing to Inline tightens nothing for now: a nonzero recompute floor needs lower-bound multiplicity metrics, deferred until the driver proves the need.

A max (fr_flops/peak_flops) (fr_bytes/peak_bandwidth) roofline over these floors (roofline_seconds) lower-bounds every completion — the two legs' minima need not be simultaneously achievable for the max of the two to be sound.

flops_approx || footprint_approximate: some count is an upper bound rather than exact. Such counts are still upper bounds (unlike under opaque), but a candidate whose guards mostly fail can carry counts far above the work it performs — quantities derived from an approximate count (achieved throughput, the roofline bound vs. a measurement) are not evidence about the hardware. Exactness is per leg: op counts (flops_approx) and byte counts (footprint_approximate) go approximate independently.

The roofline lower-bound time: max (flops/peak_flops) (bytes/peak_memory_bandwidth) over the envelope constants present (peak_flops in FLOP/s, peak_memory_bandwidth in bytes/s — the advisory Backend_intf.hardware_limits fields); None when neither is given. Monotone: raising either constant never increases the bound. A lower bound only up to the model's upper-bound byte/op counts — rank with it, do not predict.

One stored template body (optimize_ctx.computations' (at, body) entry) as one instantiation: sibling setters (a shared-loop template) are dropped as instantiation drops them, the loops binding a bare iterator position of at — the ones the ordinary point read substitutes away — collapse to a single iteration, so a reduction loop is the only trip count left, and the passes the emitted code receives after virtualization run over the result, in their order and under the routine's static_indices interval environment — the simplifier, the one-hot reduction rewrite and the scalar CSE, which a stored template predates: a single-assignment scope under a Where arm collapses into the arm's expression (conditional, hence a bound), a dense one-hot reduction becomes a dynamic gather, two alpha-equivalent scope bodies execute once. What the query cannot see is the substitution a reader applies, and where it changes the count the result is only a bound (rc_approx): a symbol occurring inside an affine position of at, or repeated across bare positions (a diagonal producer's consistency guards), may be bound or left free with its loop range-guarded or guarded, depending on the reader's index; a packed-uniform producer (Set_from_vec) inlines as the lane-extract form rather than its vector store; and a scope local read without its definition in the priced code stands for hoisted work the price cannot see. A consumer instantiating over a sub-image that collapses a further loop (gh-ocannl-616) applies that correction itself. Reads of other virtual nodes count as reads here; recompute_cost expands them.

The transitive cost of one inlined computation of the node, summed over its stored templates (every component of a multi-setter node replays at a read site, guarded — and its body hoists, so all execute; the guards themselves are the inliner's work no template carries, so a multi-setter node's price is a bound): each template's template_cost, plus, for every read of a producer with a stored template that is not committed non-virtual in the lineage, that producer's own recompute per enclosing iteration (its read cells then are not traffic). None when the node has no stored computation — a materialized node prices through producer_cost. Memoized per lineage: partially apply to the context once per compile. Cycles (a node reached through its own producers) are cut at the node, priced once.

The per-cell cost of a materialized producer in optimized code — the twin of recompute_cost for a node a heuristic cap materialized, whose computation was never stored: per setter statement of the node, one instantiation — the code pruned to that setter with the loops its index vector mentions collapsed to one iteration, so an operand read at a fixed position counts for every cell's computation (an aggregate footprint averaged over the written cells would lose it) — summed over the setters: re-inlining a multi-setter node replays every component at a read site, guards selecting the value while the hoisted bodies all execute. Its virtual producers are already inlined there, so the count is transitive by construction. A bound rather than exact when the write is not injective over the collapsed loops or its index vector is substitution-dependent (an affine or repeated position, as in template_cost), when the node has several setters (the inliner wraps each component in the range guards and the Where that select it, work the setters do not carry), for a packed-uniform setter, or when the pruning left a scope local's hoisted definition behind. None when the code sets the node nowhere.

The calibration TSV schema (config autotune_calibration_file, gh-ocannl-491 task 4) and the envelope fitter over it (gh-ocannl-514 phase 0): one row per timed candidate, the model's inputs and roofline score next to the measured time. This module is the schema's single owner — rows are emitted through to_line (by Autotune) and read back through of_line (by tools/fit_envelope.exe), so writer and reader cannot drift apart.