Module Ir.Affine

pair_conflict ~range ~dup_left ~dup_right ~pairs ~left ~right: verdict on whether the accesses with index vectors left and right (over the same tensor node; rank-padded with Fixed_idx 0) 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 index vector 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.

within_box ~range ~dims idcs: does the index vector address a cell INSIDE the dims box 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 a component the engine cannot interpret 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 ~dims idcs: whether the index vector idcs, as its symbols range over their (loop) bounds, enumerates every cell of the dims box 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 vector; per axis, a zero-based full-extent iterator, a mixed-radix affine combination of zero-based symbols whose radix chain exactly composes to the axis dimension, or Fixed_idx 0 on a unit axis. 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.

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.

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).

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. Conservative: false only when pair_conflict proves disjointness; uninterpretable access kinds (dynamic, whole-node, vectorized) 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). minor_dim is the node's minor-axis extent. 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. 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.