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 read of a node whose computations are given (an optimize_ctx.computations entry, newest first): analyze over Low_level.instantiate_at_synthetic_read's code, the node's own traffic excluded. placements (default: empty) is the lineage the read is instantiated against — it decides which nested scopes the pipeline retracts to reads and whether a packed-uniform producer's counter can serve the lane-extract form; static_indices are the routine's. None when the inliner refuses the read.

One read of a node the lineage stored computations for, through instantiation_cost under the lineage's placements; None for a node with none. Nested virtual producers need no expansion: a stored computation carries every producer inlined when it was stored as a nested scope, exactly what a read replays, and a producer read that stayed a read is a read in the emitted code too. The flip-candidate pricer (Low_level.recompute_pricer) reaches the same instantiation through the world specialize_proc hands it per node — including, for a node a heuristic cap materialized, the computations the virtualizer's own walk stores once the node is not materialized. Memoized per lineage: partially apply to the context once per compile.

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.