Repository navigation
Propagate bounded private aggregate state through helper calls #2239
Description
Problem
OpenGL index analysis cannot carry a bounded private record field through a getter or a bounded mutating method. A direct field read is accepted, but the equivalent method call loses the range. This prevents unchanged repository kernels from using ordinary iterator/cursor objects without unchecked index assertions.
#include <metal_stdlib>
using namespace metal;
struct Cursor {
long offset = 0;
Cursor(int) thread {}
void next(int n) thread { offset += n; }
long location() thread { return offset; }
};
kernel void select_value(const device uint* input [[buffer(0)]],
device uint* output [[buffer(1)]]) {
Cursor cursor(0);
cursor.next(1);
const long at = cursor.location();
const device uint* selected = input + at;
output[0] = selected[0];
}Reproduction and Evidence
Public project translation uses workgroup size (1, 1, 1), no index assertions and no metadata requirements. The working candidate is based on cb7597e3 and includes the lexical/storage-conversion fixes for #2235/#2236.
| Body before the pointer declaration | Expected offset | OpenGL |
|---|---|---|
cursor.offset = 1; const long at = cursor.offset; |
1 | Translates |
cursor.offset = 1; const long at = cursor.location(); |
1 | Rejects |
cursor.next(1); const long at = cursor.location(); |
1 | Rejects |
Two bounded loop iterations calling cursor.next(1), then cursor.location() |
2 | Rejects |
The rejected forms report project.translate.opengl-index-type-unsupported, reason: index-range-unproven, indexExpression: at. All four forms translate to Metal and DirectX. Original/generated Metal execute all four with expected readbacks 30 or 43, one unchanged input observation and 32 output guards. DirectX translation is not a claim of Windows execution.
The lowered getter has an inout thread receiver even though its body only reads self.offset. The mutator has the same receiver qualifiers and adds a bounded argument. Qualifiers alone cannot distinguish their effects; the source body and receiver ownership must establish the proof.
Required Behavior
- Summarize integer field reads and supported updates in private, non-escaping aggregate receivers, including initialization, copies and nested helper calls.
- Propagate proven getter results and bounded updates through finite loops, preserving source integer conversions and every reachable exit state.
- Distinguish by-value receivers from writable references. Analyze actual effects before reusing facts across calls; do not remove
inoutqualifiers or assume every getter-named function is pure. - Preserve conservative invalidation for aliasing, escape, shadowing, unknown calls, recursion, uncovered metadata reads and possible arithmetic overflow.
- Require native OpenGL numerical controls with guards and unchanged inputs, alongside rejected unsafe cases. Do not replace source state with constants or assertions on generated names.
Repository Impact
At MLX pin 9c3d35571ac450a8ecf5c17b4d0e3fac52c08bc8, checked translation of col_reduce_2pass_large_1_32_32_reduce_sumfloat16 now reaches in_offset + LoopedElemToLoc_1_int64_t_false__location(loop). The specialized object stores a private integer offset; next adds a bounded count times checked strides[0], and location returns the field. The loop and initial cursor advance both need this proof.
This concerns numeric state in private aggregates, not #2178's resource-reference handles or #2186's uniformity of immutable constant-buffer fields. The implementation should apply to ordinary repository iterators and cursors, not recognize MLX type or method names.
Activity
NripeshN commentedon Oct 13, 2026
The getter and mutation paths can be separated without changing emitted computation.
An isolated source-typed return-analysis prototype recognizes a private aggregate argument, reads its declared integer fields from existing caller facts, and evaluates a read-only receiver body in its own frame. It leaves the lowered
inout threadparameter intact. The reduced direct-assignment/getter case then translates without index assertions.Four negative controls remain rejected: a getter that mutates the receiver, an uninitialized field, an unknown call, and a getter returning a negative index. The negative-index control reports the exact proven range
[-1, -1]; the other controls retain unproven-range diagnostics.The positive getter artifact also passed native software OpenGL execution with the exact expected value 30, 32 unchanged output guards and one unchanged input observation. This qualifies that isolated control only, not the mutable cursor or the full column kernel.
This remains investigation evidence, not a shipped implementation. The production change still needs a typed aggregate representation, receiver ownership/effect checks, and caller-state updates through finite loops. The current scalar/vector interpreter cannot represent aggregate fields, and its call analysis deliberately rejects mutable-reference parameters. Extending only the getter path does not solve the pinned column reduction's
nextcalls.NripeshN commentedon Oct 13, 2026
Owned Aggregate Bounds
Commit
60141b95a4dd15f62a60605fd432b8a292cafea7retains source-typed private fields across resolved getters, bounded helper updates, nested calls and by-value copies. Caller loops can summarize invariant additive field updates with positive strides and bounded varying starts. Aliases, unknown effects and source-width overflow remain diagnostic; the analysis does not replace helper computations or unroll live loops.The pinned column-reduction probe now preserves the cursor update and getter range. It still rejects a generated pointer-base offset whose source bounds are lost during alias construction. That separate limitation is tracked in #2178. The isolated two-case column execution described there is not part of this production commit.
Verification:
The PR remains draft. Current-head CI, the remaining artifact-contract reviews, complete host routing and the upstream MLX suite are still required before the release checkpoint can be qualified.
NripeshN commentedon Oct 13, 2026
The checked row-reduction case still needs aggregate cursor-state analysis after the pointer-array proof work for #2244.
Reproduction uses MLX
9c3d35571ac450a8ecf5c17b4d0e3fac52c08bc8, unchangedrow_reduce_looped_large_5_reduce_sumfloat32, workgroup(32, 1, 1), dispatch(32, 2, 1), and checked uploads:row_sizenon_row_reductionsshape[0]strides[0]ndimreduce_shape[0]reduce_strides[0]reduce_ndimAt
per_thread_row_reduce(..., &row, ...), source analysis knows the input base interval[0, 604]and loop counter[0, 2], but has no interval forrowor the cursor'soffsetfields. The source computesrow = in + loop.location()before passing the addressed view. The resulting array element therefore has no initial proof; OpenGL correctly retainscomposed-pointer-index-range-unprovenforinputs[j][i].The cursor is a nested private record. Its update increments an index, advances an offset using checked stride metadata, and conditionally resets both fields while advancing the inner cursor. Existing straight-line additive summaries do not establish this state transition. The next increment should model owned nested field initialization and conditional reset/carry updates through finite loops, with overflow, aliasing and incomplete metadata remaining conservative failures. It must not insert constants for cursor fields or assertions on generated offset parameters.
This is a remaining case within this issue's scope, not a new duplicate issue. The earlier original/generated Metal parity for the three pinned row profiles remains separate evidence; no OpenGL or Windows execution of this row entry is claimed here.
Preserve private cursor bounds through conditional updates
NripeshN commentedon Oct 13, 2026
The conditional cursor increment is published as
fafb0601742040d7fccbe35c3768fb020acc5d3don #1974.row_reduce_looped_large_5_reduce_sumfloat32entry with eight checked metadata requirements and no index assertions. Three profiles check padded rows, output guards, and nine unchanged inputs. The combined row/column native batch passes all 16 tests on Metal and software OpenGL; it keeps the existing 420-second CI budget and adds no OS jobs.The remaining simple-row wide pointer-array recurrence is isolated under #2244; its experimental OpenGL result is not part of this commit. Complete host routing and upstream-suite qualification remain unfinished. This issue stays open pending hosted/checkpoint qualification; the PR remains a draft.