Module Ir.Affine

A vector store's opacity (Set_from_vec: length consecutive FLAT cells from the base).

view ~dims idcs: the coordinates of the access map idcs into a node of physical dims (padding included: the buffer the map indexes). ?dyn_axis names the data-dependent axis, ?vec a vector store's run; ?range (loop bounds) lets a run be proved not to spill. A map whose rank differs from dims is one Unknown coordinate.

The spelling witnesses use for a view.

Per axis of a full-rank access, the extent of the coordinate its component indexes in the view: a component after a Sub_axis run is a flattened index over the run's whole extent product, so an edge guard or an output mask on it compares against that product, never against its own axis's dim (gh-ocannl-1165). Every other axis — the run's own, ordinary components — keeps its dim; a map of another rank is answered with dims.

pair_conflict ~range ~dup_left ~dup_right ~pairs ~left ~right: verdict on whether the accesses viewed as left and right (over the same tensor node; re-coarsened to their common frame, declined when they span different axes) can touch a common cell from different threads. range s gives the inclusive iteration bounds of loop symbol s (None for static/unknown symbols). dup_left/dup_right select the symbols iterated independently by each side (its enclosing loops within the analyzed parallel region); other symbols are shared — equal across concurrently executing threads. pairs is the thread identity: the parallel symbols of the left copy paired with those of the right copy (for same-nest analyses, pairs of the form (p, p)).

Sound and conservative: Disjoint and Same_thread are proven; everything else is Cross_thread.

The separation query: does an access's view tell apart the iterations of a set of loop symbols? Where pair_conflict asks whether two accesses of DIFFERENT program positions can collide, this asks the same engine about ONE access taken twice — the instance-vs-instance form of the question: two instances of the same statement, iterating concurrent symbols independently, can address a common cell of idcs only if they agree on every symbol of syms.

concurrent must cover every symbol whose value may differ between the two instances, not only those of syms: with idcs = acc[w1 + w2] and syms = [w1], holding w2 equal would "prove" that a common cell forces w1 equal, while instances (0, 1) and (1, 0) share acc[1]. syms is then the subset the caller needs told apart.

The rendering of one index component the engine's witnesses use, for messages that quote a cell beside a witness in one spelling.

separates with the engine's witness: None where the vector separates syms, otherwise the explanation pair_conflict gives for the cross-thread conflict — the symbol a common cell does not force equal — for a refusal message that names what failed.

within_box ~range coords: does the viewed access address a cell INSIDE its node — every coordinate within 0 <= index < size — for every valuation of its symbols within their ranges? The interval companion of covers_box, which asks about a bijection onto the box; this asks only that nothing leaves it.

Access validity, as distinct from the distinctness separates proves. A symbol with no range (a static index parameter) and an Unknown coordinate both answer false: an unknown value can be anywhere, and this query is only ever used to license moving an access to where a guard no longer covers it.

covers_box ~range coords: whether the viewed access, as its symbols range over their (loop) bounds, enumerates every cell of its node exactly once — a bijection onto the box. This is the write-dominance building block: a covering unguarded write rewrites the whole array. Requirements: each symbol used at most once across the view; per coordinate, a zero-based full-extent iterator, a mixed-radix affine combination of zero-based symbols whose radix chain exactly composes to the coordinate's size, or 0 on a unit-size coordinate. Generalizes (and is checked against) the procedural per-axis rule of C_syntax.first_access_standalone_covering.

fiber_cardinality ~domain idcs: how many points of the loop box domain (symbol, width pairs) map to one given cell in the image of the access map idcs — the per-cell visit count of a read access, and the recompute cost per read site of inlining a setter. Domain symbols absent from the map contribute the product of their widths; when the map is injective on its mentioned symbols (Indexing.affine_injective) that product is the exact fiber size of every image cell (cells outside the image have zero), otherwise it is a lower bound. Sub_axis is read in its IR meaning — it pins and mentions nothing, while the flattened component after it pins its own symbols — which is exact: a coordinate group has one component, and injective coordinates give an injective address.

Upper-bound companion of fiber_cardinality: at most how many points of the loop box domain map to any single cell of the image of idcs. Domain symbols absent from the map contribute the product of their widths exactly; when the map is injective on its mentioned symbols that is the whole fiber and the bound is exact. Otherwise the mentioned symbols' contribution is bounded per component (see the implementation), and the smallest component-wise bound is taken.

Proves exact dense coverage of the row-major LHS buffer from the product-component extents. Handles signed affine sums, shared symbols, Sub_axis strides and independent complete concatenations. Returns false for holes, unknown/runtime extents, unsupported concat-coordinate mixtures or arithmetic outside the proof's safe integer range. When RHS maps are supplied, every target block must have a viable producer (segment-choice proof capped at 1024 combinations); an empty RHS array asks only about the mathematical LHS map.

gh-561: one component of an access's program position (a_path). Stmt components are per-Seq statement indices; the other constructors encode intra-statement order, which bare statement positions cannot express. Constructor order is execution order, so the derived compare makes lexicographic path comparison program order: a statement's Cond (If condition) evaluates before its Body, and a Set-family statement's Rhs (right-hand side and dynamic-index reads, including Local_scope bodies inlined there) executes before its Write. Every access path ends in Cond, Rhs or Write, and nothing extends a path past Write (writes have no interior), so a write's path is never a proper prefix of a read's.

Whether two accesses sit in the same Set-family statement — their paths agree above their final component (the write's Write against the statement's own direct Rhs/Cond reads; reads nested deeper, e.g. in a Local_scope body's statements, have longer paths and do not match). This is the path-level counterpart of the a_stmt_write subordination.

The top-level statement index of a path, -1 when the whole routine is a single statement (its accesses' paths start with an intra-statement component).

A scope local's identity, as Low_level.scope_id spells it: the node naming the local and its scope id. Two locals are the same local only when both agree.

Whether every enclosing loop of an access or effect executes: a row under a dead loop (to_ < from_) never happens.

Whether a path lies inside a Local_scope body (it crosses an Arg component).

within_statement ~write path: whether path lies inside the Set-family statement whose own write sits at write — its right-hand side, the Local_scope bodies inlined there, or the write itself. false when write is not a write position.

Whether two accesses (of the same node) can touch a common cell, each access taken over its whole loop box — the two sides' iterations paired independently, including iterations of loops the sides share (the accesses need not be simultaneous, so a shared loop's symbol varies independently between one side's visit and the other's). Symbols bound by neither side's loops (static indices) are shared parameters, equal on both sides, bounded by static_range when known. dims is the node's dims (the coordinate view's). Conservative: false only when pair_conflict proves disjointness. A dynamic access's data-dependent axis is an Unknown coordinate of its view, so its other coordinates still decide (gh-ocannl-1174); a vectorized access is viewed as a Run of its length (vec_view), its own loop bounds proving whether the run stays inside its minor coordinate; whole-node accesses count as overlapping.

Whether the runs of a vectorized access (a_vec_last) are pairwise disjoint in the node's flat cell space — the access then touches exactly base image * a_vec_len distinct cells (gh-ocannl-578). dims is the node's dims; the runs move along the minor coordinate of the view. Conservative: false when any of the sufficient conditions (documented in the implementation) is not proved.

The containment query. read_covered_before ~read ~writes (): is every cell the read access can touch necessarily written before the read executes — the dominance side of dependence analysis, and the fifth decision procedure (gh-494 waypoint 2). Unlike the ∃-flavored pair_conflict (negated to prove disjointness), containment is a ∀∃ query — for every read instance there must exist a covering write instance. Visibility is same-common-iteration program order over path_comp paths; loop-carried coverage is declined, conservatively. An Unknown read coordinate (a dynamic gather's row, gh-ocannl-1174) ranges over its whole extent; an Unknown write coordinate (a scatter's row) declines that write. With ?thread naming the parallel (thread-identity) symbols, `Covered proves the cell side of the per-thread-copy transform. The full variable treatment, the cross-statement value side condition, and the union rule for partial covers are documented in the implementation.

Guarded writes are the caller's choice: include them to mirror guards-taken analyses (Low_level.trace_node_facts and the coverage queries take guards unconditionally), pre-filter a_guarded for execution-accurate coverage. writes must be accesses of the same node as read, whose dims are dims: each write is compared with the read in their views' common frame.