MS1V2 mlir-stage-11-v1 passing 5000/5000
Estimated confidence: 56.2%. Conservative lower bound: 16.9% (95% level).
uniform over observed structural partitions. observed partitions; unseen partitions have no supplied target weight. Partitions use recursive production counts and derivation depth. Behavioral classes combine each input’s compiler coverage and assertion decision paths. Catalog partitions with no observations retain maximal missing mass.
Baseline tests: Every tracked test file with a RUN line invoking loom-raise-opt (77 files); other executables and native unit tests excluded
| Source file | Baseline coverage | Baseline + input | Contributing input |
|---|---|---|---|
…/lib/Dataflow/IR/DataflowActorSemantics.cppMS1V | 1089/1621lines67.2% 747/1330branches56.2% | 1110/1621lines68.5%+21 761/1330branches57.2%+14 | |
21 newly covered lines · 14 newly covered branches1397 | |||
…/lib/Dataflow/IR/DataflowOps.cppMS1V | 270/410lines65.9% 103/228branches45.2% | 304/410lines74.1%+34 124/228branches54.4%+21 | |
34 newly covered lines · 21 newly covered branches194 | |||
…/lib/Dataflow/IR/DataflowVectorSemantics.cppMS1V | 81/121lines66.9% 53/106branches50.0% | 81/121lines66.9%+0 54/106branches50.9%+1 | |
1 newly covered branch42 | |||
…/lib/Frontend/Lowering/GraphRegionLowering.cppMS1V | 1416/1626lines87.1% 532/680branches78.2% | 1462/1626lines89.9%+46 540/680branches79.4%+8 | |
46 newly covered lines · 8 newly covered branches167 | |||
…/lib/Frontend/Lowering/RankedMemRefLowering.cppMS1V | 60/133lines45.1% 27/94branches28.7% | 106/133lines79.7%+46 54/94branches57.4%+27 | |
46 newly covered lines · 27 newly covered branches17 | |||
…/loom/include/Common/Artifact.hMS1V | 13/37lines35.1% 3/18branches16.7% | 13/37lines35.1%+0 3/18branches16.7%+0 | Open PBT |
…/include/Dataflow/IR/DataflowActorSemantics.hMS1V | 9/160lines5.6% 1/60branches1.7% | 9/160lines5.6%+0 1/60branches1.7%+0 | Open PBT |
…/include/Frontend/Lowering/StreamLoopAttrs.hMS1V | 31/41lines75.6% 10/14branches71.4% | 31/41lines75.6%+0 10/14branches71.4%+0 | Open PBT |
…/loom/lib/Common/IndexWidth.cppMS1V | 63/84lines75.0% 28/42branches66.7% | 63/84lines75.0%+0 28/42branches66.7%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowChannelOps.cppMS1V | 59/88lines67.0% 13/38branches34.2% | 59/88lines67.0%+0 13/38branches34.2%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowDialect.cppMS1V | 22/32lines68.8% 4/10branches40.0% | 22/32lines68.8%+0 4/10branches40.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowFunctionLikeOps.cppMS1V | 693/1097lines63.2% 264/592branches44.6% | 693/1097lines63.2%+0 264/592branches44.6%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowMemoryContracts.cppMS1V | 198/371lines53.4% 98/218branches45.0% | 198/371lines53.4%+0 98/218branches45.0%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchema.cppMS1V | 274/716lines38.3% 127/350branches36.3% | 274/716lines38.3%+0 127/350branches36.3%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaCodecInternal.hMS1V | 28/120lines23.3% 4/44branches9.1% | 28/120lines23.3%+0 4/44branches9.1%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaTypeCodec.cppMS1V | 85/516lines16.5% 55/374branches14.7% | 85/516lines16.5%+0 55/374branches14.7%+0 | Open PBT |
…/lib/Dataflow/Transforms/DataflowRewritePass.cppMS1V | 338/559lines60.5% 172/340branches50.6% | 338/559lines60.5%+0 172/340branches50.6%+0 | Open PBT |
…/lib/Frontend/Lowering/ExactMemRefLayout.cppMS1V | 61/143lines42.7% 26/80branches32.5% | 61/143lines42.7%+0 26/80branches32.5%+0 | Open PBT |
…/lib/Frontend/Lowering/ExpandGraphMemrefCopyPass.cppMS1V | 79/90lines87.8% 20/22branches90.9% | 79/90lines87.8%+0 20/22branches90.9%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphIndexLowering.cppMS1V | 260/288lines90.3% 129/168branches76.8% | 260/288lines90.3%+0 129/168branches76.8%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphParallelLowering.cppMS1V | 651/1243lines52.4% 284/786branches36.1% | 651/1243lines52.4%+0 284/786branches36.1%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphRegionAdmission.cppMS1V | 58/110lines52.7% 29/92branches31.5% | 58/110lines52.7%+0 29/92branches31.5%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.cppMS1V | 934/1072lines87.1% 299/432branches69.2% | 934/1072lines87.1%+0 299/432branches69.2%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.hMS1V | 4/4lines100.0% 4/4branches100.0% | 4/4lines100.0%+0 4/4branches100.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForToGraphPass.cppMS1V | 1033/1240lines83.3% 374/540branches69.3% | 1033/1240lines83.3%+0 374/540branches69.3%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForallToThreadPass.cppMS1V | 30/34lines88.2% 2/4branches50.0% | 30/34lines88.2%+0 2/4branches50.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphConstantsPass.cppMS1V | 80/83lines96.4% 18/24branches75.0% | 80/83lines96.4%+0 18/24branches75.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphMemoryPass.cppMS1V | 525/841lines62.4% 208/400branches52.0% | 525/841lines62.4%+0 208/400branches52.0%+0 | Open PBT |
…/lib/Frontend/Lowering/Pipeline.cppMS1V | 18/21lines85.7% branchesnot measured | 18/21lines85.7%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/DeduplicateSCFWhileStatePass.cppMS1V | 13/135lines9.6% 0/60branches0.0% | 13/135lines9.6%+0 0/60branches0.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMArithToArithPass.cppMS1V | 300/319lines94.0% 94/116branches81.0% | 300/319lines94.0%+0 94/116branches81.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMCfToCfPass.cppMS1V | 77/80lines96.2% 8/8branches100.0% | 77/80lines96.2%+0 8/8branches100.0%+0 | Open PBT |
…/lib/Frontend/Raising/LiftCFToSCFPass.cppMS1V | 616/694lines88.8% 293/386branches75.9% | 616/694lines88.8%+0 293/386branches75.9%+0 | Open PBT |
…/lib/Frontend/Raising/MaterializeFMulAddPass.cppMS1V | 70/106lines66.0% 11/26branches42.3% | 70/106lines66.0%+0 11/26branches42.3%+0 | Open PBT |
…/lib/Frontend/Raising/NormalizeLiftedSCFExitPass.cppMS1V | 232/250lines92.8% 120/182branches65.9% | 232/250lines92.8%+0 120/182branches65.9%+0 | Open PBT |
…/lib/Frontend/Raising/Pipeline.cppMS1V | 10/19lines52.6% branchesnot measured | 10/19lines52.6%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/SCFForToForallPass.cppMS1V | 494/738lines66.9% 241/458branches52.6% | 494/738lines66.9%+0 241/458branches52.6%+0 | Open PBT |
…/lib/Frontend/Raising/SCFWhileToForPass.cppMS1V | 164/176lines93.2% 70/94branches74.5% | 164/176lines93.2%+0 70/94branches74.5%+0 | Open PBT |
…/loom/tools/loom-raise-opt/loom-raise-opt.cppMS1V | 12/12lines100.0% branchesnot measured | 12/12lines100.0%+0 branchesnot measured | Open PBT |
One vector addressed memory actor is one canonical firing. Its active lanes do
not create independent frontier records or an implicit lane order.
P(access) is the conservative union of alias partitions that any active lane
may access. A dynamic mask or address vector cannot weaken that set merely
because one observed execution disables a lane. A statically proven all-zero
mask may be simplified by an ordinary semantics-preserving Dataflow rewrite;
otherwise the firing retains its explicit ctrl and done obligations.
module { dataflow.graph private @graph_0( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 %g0, %gd0 = dataflow.load %a[%av] %start mask %m : memref<16xi32>, vector<4xindex>, vector<4xi32> scf.if %c { %v1 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> } scf.if %c { %v5 = vector.transfer_read %b[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v5, %a[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } }
module { dataflow.graph private @graph_0( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 %lb0 = arith.constant 0 : index %ub0 = arith.constant 4 : index %sp0 = arith.constant 1 : index scf.for %k0 = %lb0 to %ub0 step %sp0 { %v1 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v1, %a[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb2 = arith.constant 0 : index %ub2 = arith.constant 4 : index %sp2 = arith.constant 1 : index scf.for %k2 = %lb2 to %ub2 step %sp2 { %v3 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v3, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb4 = arith.constant 0 : index %ub4 = arith.constant 4 : index %sp4 = arith.constant 1 : index scf.for %k4 = %lb4 to %ub4 step %sp4 { %v5 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v5, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb6 = arith.constant 0 : index %ub6 = arith.constant 4 : index %sp6 = arith.constant 1 : index scf.for %k6 = %lb6 to %ub6 step %sp6 { %v7 = vector.transfer_read %b[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v7, %a[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb8 = arith.constant 0 : index %ub8 = arith.constant 4 : index %sp8 = arith.constant 1 : index scf.for %k8 = %lb8 to %ub8 step %sp8 { %v9 = vector.transfer_read %a[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v9, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } dataflow.graph private @graph_1( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 scf.if %c { %v0 = vector.transfer_read %a[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v0, %b[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } scf.if %c { %v1 = vector.transfer_read %a[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v1, %b[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } }
LLVM memcpy, memmove, and memset intrinsics are expanded into their exact
structured loop semantics before ownership selection. Supported LLVM
load/store (including volatile and atomic contracts), atomicrmw, cmpxchg,
and fence forms are then normalized before recursive region lowering, after
which the same frontier rules apply.
When graph publication can trace every captured memory capability to a known
root, an exact service rooted at a unique thread argument mechanically inherits
that argument's llvm.noalias fact. If a root is unknown, appears through more
than one captured capability, or does not resolve to that argument, publication
must omit the fact.
memref.get_global, memref.alloca, globals, static pointer bases, and
unrecognized capability producers are not canonical roots. A pre-final
analysis may conservatively group an unresolved access while building an event
network, but finalization rejects any such residual producer rather than
granting it an external-memory authority.
A memory input binds an established external memref capability through an exact graph-launch type match. An LLVM pointer never satisfies a graph memory port.
The finalized-graph gate also rejects residual
memref.load/memref.store, memref.get_global, raw pointer arithmetic,
pointer-bearing operations, builtin.unrealized_conversion_cast, and unknown
memory-capability producers. An unsupported effectful operation inside a
structured region must likewise fail closed instead of being hoisted.
This document is the memory-order source of truth for graph-local SCF to
Dataflow lowering. The concrete owner is loom-lower-graph-memory; it
normalizes supported memory leaves and recursively lowers structured graph
regions in one traversal.
A canonical root is found by peeling an accepted side-effect-free memref view until reaching an explicit storage or boundary root. The finalized surface recognizes:
dataflow.memory.service result at that binding, which preserves the root
of its exact pointer operand while changing only the value-plane pointer into
a memory-plane capability;memref.alloc result, whose root is unique for each invocation;Graph launch memory bindings require exact memref capability types. An LLVM pointer cannot bind a graph memref through a conversion, inferred base, or special address-space-zero rule.
Until the typed producer and verifier establish this provenance, the boundary fails closed. Forged, malformed, foreign-owner, or domain-mismatched provenance is invalid even when the residual SCF shape is otherwise supported.
The owner rejects before mutation when:
none execution value.LLVM target-specific sync scopes without a compiler-target owner and atomic accesses without an explicit power-of-two source alignment fail closed. Every residual raw LLVM memory operation fails closed.
Distinct graph memory inputs are conservatively may-alias unless explicit no-alias evidence distinguishes them. Distinct fresh allocations are independent roots.
The lowering does not select parallel width, ownership, serialization, unrolling, reduction order, or any other schedule policy. Those decisions must be made before graph-region lowering and normalized into supported structured input.
A source-origin llvm.alloca accepted by the Structured
PromoteOrderedBufferToChannel decision is not an exception to this rule. That
decision must remove the complete proved allocation closure before D0; a
residual allocation or pointer use remains non-canonical and is rejected.
Residual scf.parallel or scf.forall is checked across every graph before
the pass mutates any graph. Raw or unowned parallel input fails.
arbitrary nesting of scf.if, source-sequential scf.for, and
scf.while;
Access-to-partition membership is kept in a transient operation map before SCF operands are projected. Selector demuxing must not change alias identity.
pre-mutation rejection of residual scf.parallel and scf.forall that
reach a graph without an already materialized schedule boundary.
normalized scalar memref.load and memref.store leaves over a canonical
linear memory space;
One vector addressed memory actor is one canonical firing. Its active lanes do not create independent frontier records or an implicit lane order.
candidate.pg// Graph-local SCF/vector memory inputs for loom-lower-graph-memory. // Each module holds finalized-surface dataflow.graph definitions whose bodies // carry supported memory leaves: fixed rank-one vector transfers (masked and // unmasked) over graph memref capability inputs, normalized scalar // memref.load/memref.store leaves, and nesting in scf.if / source-sequential // scf.for. No residual scf.parallel, scf.forall, LLVM memory op, pointer, // memref.alloca, memref.get_global, or unrealized conversion cast is emitted. start: {new NUM_GRAPHS = random.randint(1, 2); new G = 0} 'module {\n' graphs '}\n'; graphs: (G < NUM_GRAPHS) one_graph {G += 1} graphs | (G == NUM_GRAPHS) ''; one_graph: {new NUM_STMTS = random.randint(1, 4); new S = 0; new N = 0} ' dataflow.graph private @graph_' gid '(\n' ' %start: none, %i: index, %c: i1, %m: vector<4xi1>,\n' ' %av: vector<4xindex>, %val: i32,\n' ' %a: memref<16xi32>, %b: memref<16xi32>) -> ()\n' ' attributes {input_segments = array<i32: 5, 0, 2>,\n' ' result_segments = array<i32: 0, 0, 0>} {\n' ' %pad = arith.constant 0 : i32\n' lead_stmt stmts ' dataflow.graph.return %start : none\n' ' }\n'; gid: [str(G)]; stmts: (S < NUM_STMTS) stmt {S += 1} stmts | (S == NUM_STMTS) ''; // Sampling convention: every graph carries at least one vector addressed // access, so the governed construct is present in every sample. lead_stmt: vec_pair | gather_pair | if_stmt | for_stmt; stmt: vec_pair | gather_pair | scalar_pair | if_stmt | for_stmt; // One canonical vector addressed access pair: a masked or unmasked // fixed rank-one contiguous in-bounds transfer read feeding a transfer write. vec_pair: {new K = N} {new MASKED = random.choice([0, 1])} {new SRC = random.choice(['a', 'b'])} {new DST = random.choice(['a', 'b'])} {N += 1} ' %v' vid ' = vector.transfer_read %' src_mem '[%i], %pad' rmask ' {in_bounds = [true]} : memref<16xi32>, vector<4xi32>\n' ' vector.transfer_write %v' vid ', %' dst_mem '[%i]' wmask ' {in_bounds = [true]} : vector<4xi32>, memref<16xi32>\n'; vid: [str(K)]; src_mem: [SRC]; dst_mem: [DST]; rmask: (MASKED == 1) ', %m' | (MASKED == 0) ''; wmask: (MASKED == 1) ', %m' | (MASKED == 0) ''; // Normalized scalar leaves over the same canonical linear memory space. scalar_pair: {new SK = N} {new SMEM = random.choice(['a', 'b'])} {N += 1} ' memref.store %val, %' scalar_mem '[%i] : memref<16xi32>\n' ' %s' sid ' = memref.load %' scalar_mem '[%i] : memref<16xi32>\n'; sid: [str(SK)]; scalar_mem: [SMEM]; if_stmt: ' scf.if %c {\n' vec_pair ' }\n'; for_stmt: {new FK = N} {N += 1} ' %lb' fid ' = arith.constant 0 : index\n' ' %ub' fid ' = arith.constant 4 : index\n' ' %sp' fid ' = arith.constant 1 : index\n' ' scf.for %k' fid ' = %lb' fid ' to %ub' fid ' step %sp' fid ' {\n' vec_pair ' }\n'; fid: [str(FK)]; // A canonical gather/scatter pair already spelled as vector addressed // dataflow memory actors: one address vector per lane with a lane mask. gather_pair: {new GK = N} {N += 1} ' %g' gix ', %gd' gix ' = dataflow.load %a[%av] %start mask %m' ' : memref<16xi32>, vector<4xindex>, vector<4xi32>\n' ' %sc' gix ' = dataflow.store %b[%av] %g' gix ' %start mask %m' ' : memref<16xi32>, vector<4xindex>, vector<4xi32>\n'; gix: [str(GK)];
One vector addressed memory actor is one canonical firing. Its active lanes do not create independent frontier records or an implicit lane order.
candidate.spctpostcondition vector_memory_actor_retains_ctrl_and_done { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-mem.md:L245-L251"; } constraints { // A vector addressed memory actor: a canonical dataflow memory actor // whose address operand is an address vector (gather/scatter) or whose // access payload is a fixed vector distinct from the memref element type // (contiguous vector access), optionally lane masked. let vector_loads = seq { op | op in output.operations where op.name == "dataflow.load" and (op.operands[1].type.kind == "vector" or (op.results[0].type.kind == "vector" and op.results[0].type != op.operands[0].type.element_type)) }; let vector_stores = seq { op | op in output.operations where op.name == "dataflow.store" and (op.operands[1].type.kind == "vector" or (op.operands[2].type.kind == "vector" and op.operands[2].type != op.operands[0].type.element_type)) }; // One vector addressed memory actor is one canonical firing that retains // its explicit `ctrl` and `done` obligations: exactly one explicit `none` // control token is consumed and exactly one explicit `none` completion // token is published, with no per-lane frontier records. forall op in vector_loads { assert load_explicit_ctrl: cardinality(op.operands) >= 3 and op.operands[2].type == mlir::none; assert load_one_firing_ctrl: cardinality(seq { v | v in op.operands where v.type == mlir::none }) == 1; assert load_explicit_done: cardinality(op.results) == 2 and op.results[1].type == mlir::none; assert load_one_firing_done: cardinality(seq { v | v in op.results where v.type == mlir::none }) == 1; } forall op in vector_stores { assert store_explicit_ctrl: cardinality(op.operands) >= 4 and op.operands[3].type == mlir::none; assert store_one_firing_ctrl: cardinality(seq { v | v in op.operands where v.type == mlir::none }) == 1; assert store_explicit_done: cardinality(op.results) == 1 and op.results[0].type == mlir::none; assert store_one_firing_done: cardinality(seq { v | v in op.results where v.type == mlir::none }) == 1; } } }
module { dataflow.graph private @graph_0( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 %g0, %gd0 = dataflow.load %a[%av] %start mask %m : memref<16xi32>, vector<4xindex>, vector<4xi32> scf.if %c { %v1 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> } scf.if %c { %v5 = vector.transfer_read %b[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v5, %a[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } }
20260911-083241started2026-09-11T08:32:42Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
module { dataflow.graph private @graph_0( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 %lb0 = arith.constant 0 : index %ub0 = arith.constant 4 : index %sp0 = arith.constant 1 : index scf.for %k0 = %lb0 to %ub0 step %sp0 { %v1 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v1, %a[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb2 = arith.constant 0 : index %ub2 = arith.constant 4 : index %sp2 = arith.constant 1 : index scf.for %k2 = %lb2 to %ub2 step %sp2 { %v3 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v3, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb4 = arith.constant 0 : index %ub4 = arith.constant 4 : index %sp4 = arith.constant 1 : index scf.for %k4 = %lb4 to %ub4 step %sp4 { %v5 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v5, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb6 = arith.constant 0 : index %ub6 = arith.constant 4 : index %sp6 = arith.constant 1 : index scf.for %k6 = %lb6 to %ub6 step %sp6 { %v7 = vector.transfer_read %b[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v7, %a[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } %lb8 = arith.constant 0 : index %ub8 = arith.constant 4 : index %sp8 = arith.constant 1 : index scf.for %k8 = %lb8 to %ub8 step %sp8 { %v9 = vector.transfer_read %a[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v9, %b[%i] {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } dataflow.graph private @graph_1( %start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>) -> () attributes {input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %pad = arith.constant 0 : i32 scf.if %c { %v0 = vector.transfer_read %a[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v0, %b[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } scf.if %c { %v1 = vector.transfer_read %a[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32> vector.transfer_write %v1, %b[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32> } dataflow.graph.return %start : none } }
"builtin.module"() ({ "dataflow.graph"() <{function_type = (index, i1, vector<4xi1>, vector<4xindex>, i32, memref<16xi32>, memref<16xi32>) -> (), input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_0", sym_visibility = "private"}> ({ ^bb0(%arg8: none, %arg9: index, %arg10: i1, %arg11: vector<4xi1>, %arg12: vector<4xindex>, %arg13: i32, %arg14: memref<16xi32>, %arg15: memref<16xi32>): %26 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %27 = "arith.constant"() <{value = 0 : index}> : () -> index %28 = "arith.constant"() <{value = 4 : index}> : () -> index %29 = "arith.constant"() <{value = 1 : index}> : () -> index %30 = "arith.constant"() <{value = 0 : index}> : () -> index %31 = "arith.constant"() <{value = 4 : index}> : () -> index %32 = "arith.constant"() <{value = 1 : index}> : () -> index %33 = "arith.constant"() <{value = 0 : index}> : () -> index %34 = "arith.constant"() <{value = 4 : index}> : () -> index %35 = "arith.constant"() <{value = 1 : index}> : () -> index %36 = "arith.constant"() <{value = 0 : index}> : () -> index %37 = "arith.constant"() <{value = 4 : index}> : () -> index %38 = "arith.constant"() <{value = 1 : index}> : () -> index %39 = "arith.constant"() <{value = 0 : index}> : () -> index %40 = "arith.constant"() <{value = 4 : index}> : () -> index %41 = "arith.constant"() <{value = 1 : index}> : () -> index %42 = "arith.index_cast"(%27) : (index) -> i32 %43 = "arith.index_cast"(%28) : (index) -> i32 %44 = "arith.index_cast"(%29) : (index) -> i32 %45:2 = "dataflow.stream"(%42, %43, %44) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %46 = "dataflow.carry"(%45#1, %arg8, %47#1) : (i1, none, none) -> none %47:2 = "dataflow.demux"(%45#1, %46) : (i1, none) -> (none, none) %48 = "dataflow.invariant"(%45#1, %arg9) : (i1, index) -> index %49:2 = "dataflow.gate"(%45#1, %48) : (i1, index) -> (i1, index) %50:2 = "dataflow.demux"(%49#0, %49#1) : (i1, index) -> (index, index) %51 = "dataflow.invariant"(%45#1, %26) : (i1, i32) -> i32 %52:2 = "dataflow.gate"(%45#1, %51) : (i1, i32) -> (i1, i32) %53:2 = "dataflow.demux"(%52#0, %52#1) : (i1, i32) -> (i32, i32) %54 = "dataflow.carry"(%45#1, %arg8, %61) : (i1, none, none) -> none %55 = "dataflow.carry"(%45#1, %arg8, %61) : (i1, none, none) -> none %56:2 = "dataflow.demux"(%45#1, %54) : (i1, none) -> (none, none) %57:2 = "dataflow.demux"(%45#1, %55) : (i1, none) -> (none, none) %58:2 = "dataflow.sync"(%47#1, %56#1) : (none, none) -> (none, none) %59:2 = "dataflow.load"(%arg15, %49#1, %58#0) : (memref<16xi32>, index, none) -> (vector<4xi32>, none) %60:2 = "dataflow.sync"(%57#1, %59#1) : (none, none) -> (none, none) %61 = "dataflow.store"(%arg14, %49#1, %59#0, %60#0) : (memref<16xi32>, index, vector<4xi32>, none) -> none %62 = "arith.cmpi"(%42, %43) <{predicate = 2 : i64}> : (i32, i32) -> i1 %63:2 = "dataflow.demux"(%62, %47#0) : (i1, none) -> (none, none) %64:3 = "dataflow.sync"(%63#1, %50#0, %53#0) : (none, index, i32) -> (none, index, i32) %65 = "dataflow.mux"(%62, %63#0, %64#0) : (i1, none, none) -> none %66 = "arith.index_cast"(%30) : (index) -> i32 %67 = "arith.index_cast"(%31) : (index) -> i32 %68 = "arith.index_cast"(%32) : (index) -> i32 %69:2 = "dataflow.stream"(%66, %67, %68) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %70 = "dataflow.carry"(%69#1, %65, %71#1) : (i1, none, none) -> none %71:2 = "dataflow.demux"(%69#1, %70) : (i1, none) -> (none, none) %72 = "dataflow.invariant"(%69#1, %arg9) : (i1, index) -> index %73:2 = "dataflow.gate"(%69#1, %72) : (i1, index) -> (i1, index) %74:2 = "dataflow.demux"(%73#0, %73#1) : (i1, index) -> (index, index) %75 = "dataflow.invariant"(%69#1, %26) : (i1, i32) -> i32 %76:2 = "dataflow.gate"(%69#1, %75) : (i1, i32) -> (i1, i32) %77:2 = "dataflow.demux"(%76#0, %76#1) : (i1, i32) -> (i32, i32) %78 = "dataflow.carry"(%69#1, %56#0, %85) : (i1, none, none) -> none %79 = "dataflow.carry"(%69#1, %57#0, %85) : (i1, none, none) -> none %80:2 = "dataflow.demux"(%69#1, %78) : (i1, none) -> (none, none) %81:2 = "dataflow.demux"(%69#1, %79) : (i1, none) -> (none, none) %82:2 = "dataflow.sync"(%71#1, %80#1) : (none, none) -> (none, none) %83:2 = "dataflow.load"(%arg15, %73#1, %82#0) : (memref<16xi32>, index, none) -> (vector<4xi32>, none) %84:2 = "dataflow.sync"(%81#1, %83#1) : (none, none) -> (none, none) %85 = "dataflow.store"(%arg15, %73#1, %83#0, %84#0) : (memref<16xi32>, index, vector<4xi32>, none) -> none %86 = "arith.cmpi"(%66, %67) <{predicate = 2 : i64}> : (i32, i32) -> i1 %87:2 = "dataflow.demux"(%86, %71#0) : (i1, none) -> (none, none) %88:3 = "dataflow.sync"(%87#1, %74#0, %77#0) : (none, index, i32) -> (none, index, i32) %89 = "dataflow.mux"(%86, %87#0, %88#0) : (i1, none, none) -> none %90 = "arith.index_cast"(%33) : (index) -> i32 %91 = "arith.index_cast"(%34) : (index) -> i32 %92 = "arith.index_cast"(%35) : (index) -> i32 %93:2 = "dataflow.stream"(%90, %91, %92) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %94 = "dataflow.carry"(%93#1, %89, %95#1) : (i1, none, none) -> none %95:2 = "dataflow.demux"(%93#1, %94) : (i1, none) -> (none, none) %96 = "dataflow.invariant"(%93#1, %arg9) : (i1, index) -> index %97:2 = "dataflow.gate"(%93#1, %96) : (i1, index) -> (i1, index) %98:2 = "dataflow.demux"(%97#0, %97#1) : (i1, index) -> (index, index) %99 = "dataflow.invariant"(%93#1, %26) : (i1, i32) -> i32 %100:2 = "dataflow.gate"(%93#1, %99) : (i1, i32) -> (i1, i32) %101:2 = "dataflow.demux"(%100#0, %100#1) : (i1, i32) -> (i32, i32) %102 = "dataflow.carry"(%93#1, %80#0, %109) : (i1, none, none) -> none %103 = "dataflow.carry"(%93#1, %81#0, %109) : (i1, none, none) -> none %104:2 = "dataflow.demux"(%93#1, %102) : (i1, none) -> (none, none) %105:2 = "dataflow.demux"(%93#1, %103) : (i1, none) -> (none, none) %106:2 = "dataflow.sync"(%95#1, %104#1) : (none, none) -> (none, none) %107:2 = "dataflow.load"(%arg15, %97#1, %106#0) : (memref<16xi32>, index, none) -> (vector<4xi32>, none) %108:2 = "dataflow.sync"(%105#1, %107#1) : (none, none) -> (none, none) %109 = "dataflow.store"(%arg15, %97#1, %107#0, %108#0) : (memref<16xi32>, index, vector<4xi32>, none) -> none %110 = "arith.cmpi"(%90, %91) <{predicate = 2 : i64}> : (i32, i32) -> i1 %111:2 = "dataflow.demux"(%110, %95#0) : (i1, none) -> (none, none) %112:3 = "dataflow.sync"(%111#1, %98#0, %101#0) : (none, index, i32) -> (none, index, i32) %113 = "dataflow.mux"(%110, %111#0, %112#0) : (i1, none, none) -> none %114 = "arith.index_cast"(%36) : (index) -> i32 %115 = "arith.index_cast"(%37) : (index) -> i32 %116 = "arith.index_cast"(%38) : (index) -> i32 %117:2 = "dataflow.stream"(%114, %115, %116) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %118 = "dataflow.carry"(%117#1, %113, %119#1) : (i1, none, none) -> none %119:2 = "dataflow.demux"(%117#1, %118) : (i1, none) -> (none, none) %120 = "dataflow.invariant"(%117#1, %arg9) : (i1, index) -> index %121:2 = "dataflow.gate"(%117#1, %120) : (i1, index) -> (i1, index) %122:2 = "dataflow.demux"(%121#0, %121#1) : (i1, index) -> (index, index) %123 = "dataflow.invariant"(%117#1, %26) : (i1, i32) -> i32 %124:2 = "dataflow.gate"(%117#1, %123) : (i1, i32) -> (i1, i32) %125:2 = "dataflow.demux"(%124#0, %124#1) : (i1, i32) -> (i32, i32) %126 = "dataflow.invariant"(%117#1, %arg11) : (i1, vector<4xi1>) -> vector<4xi1> %127:2 = "dataflow.gate"(%117#1, %126) : (i1, vector<4xi1>) -> (i1, vector<4xi1>) %128:2 = "dataflow.demux"(%127#0, %127#1) : (i1, vector<4xi1>) -> (vector<4xi1>, vector<4xi1>) %129 = "dataflow.carry"(%117#1, %104#0, %136) : (i1, none, none) -> none %130 = "dataflow.carry"(%117#1, %105#0, %136) : (i1, none, none) -> none %131:2 = "dataflow.demux"(%117#1, %129) : (i1, none) -> (none, none) %132:2 = "dataflow.demux"(%117#1, %130) : (i1, none) -> (none, none) %133:2 = "dataflow.sync"(%119#1, %131#1) : (none, none) -> (none, none) %134:2 = "dataflow.load"(%arg15, %121#1, %133#0, %127#1) : (memref<16xi32>, index, none, vector<4xi1>) -> (vector<4xi32>, none) %135:2 = "dataflow.sync"(%132#1, %134#1) : (none, none) -> (none, none) %136 = "dataflow.store"(%arg14, %121#1, %134#0, %135#0, %127#1) : (memref<16xi32>, index, vector<4xi32>, none, vector<4xi1>) -> none %137 = "arith.cmpi"(%114, %115) <{predicate = 2 : i64}> : (i32, i32) -> i1 %138:2 = "dataflow.demux"(%137, %119#0) : (i1, none) -> (none, none) %139:4 = "dataflow.sync"(%138#1, %122#0, %125#0, %128#0) : (none, index, i32, vector<4xi1>) -> (none, index, i32, vector<4xi1>) %140 = "dataflow.mux"(%137, %138#0, %139#0) : (i1, none, none) -> none %141 = "arith.index_cast"(%39) : (index) -> i32 %142 = "arith.index_cast"(%40) : (index) -> i32 %143 = "arith.index_cast"(%41) : (index) -> i32 %144:2 = "dataflow.stream"(%141, %142, %143) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %145 = "dataflow.carry"(%144#1, %140, %146#1) : (i1, none, none) -> none %146:2 = "dataflow.demux"(%144#1, %145) : (i1, none) -> (none, none) %147 = "dataflow.invariant"(%144#1, %arg9) : (i1, index) -> index %148:2 = "dataflow.gate"(%144#1, %147) : (i1, index) -> (i1, index) %149:2 = "dataflow.demux"(%148#0, %148#1) : (i1, index) -> (index, index) %150 = "dataflow.invariant"(%144#1, %26) : (i1, i32) -> i32 %151:2 = "dataflow.gate"(%144#1, %150) : (i1, i32) -> (i1, i32) %152:2 = "dataflow.demux"(%151#0, %151#1) : (i1, i32) -> (i32, i32) %153 = "dataflow.carry"(%144#1, %131#0, %160) : (i1, none, none) -> none %154 = "dataflow.carry"(%144#1, %132#0, %160) : (i1, none, none) -> none %155:2 = "dataflow.demux"(%144#1, %153) : (i1, none) -> (none, none) %156:2 = "dataflow.demux"(%144#1, %154) : (i1, none) -> (none, none) %157:2 = "dataflow.sync"(%146#1, %155#1) : (none, none) -> (none, none) %158:2 = "dataflow.load"(%arg14, %148#1, %157#0) : (memref<16xi32>, index, none) -> (vector<4xi32>, none) %159:2 = "dataflow.sync"(%156#1, %158#1) : (none, none) -> (none, none) %160 = "dataflow.store"(%arg15, %148#1, %158#0, %159#0) : (memref<16xi32>, index, vector<4xi32>, none) -> none %161 = "arith.cmpi"(%141, %142) <{predicate = 2 : i64}> : (i32, i32) -> i1 %162:2 = "dataflow.demux"(%161, %146#0) : (i1, none) -> (none, none) %163:3 = "dataflow.sync"(%162#1, %149#0, %152#0) : (none, index, i32) -> (none, index, i32) %164 = "dataflow.mux"(%161, %162#0, %163#0) : (i1, none, none) -> none "dataflow.graph.return"(%164, %156#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> () }) : () -> () "dataflow.graph"() <{function_type = (index, i1, vector<4xi1>, vector<4xindex>, i32, memref<16xi32>, memref<16xi32>) -> (), input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_1", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: index, %arg2: i1, %arg3: vector<4xi1>, %arg4: vector<4xindex>, %arg5: i32, %arg6: memref<16xi32>, %arg7: memref<16xi32>): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1:2 = "dataflow.demux"(%arg2, %arg0) : (i1, none) -> (none, none) %2:2 = "dataflow.demux"(%arg2, %arg0) : (i1, none) -> (none, none) %3:2 = "dataflow.demux"(%arg2, %arg0) : (i1, none) -> (none, none) %4:2 = "dataflow.demux"(%arg2, %arg1) : (i1, index) -> (index, index) %5:2 = "dataflow.demux"(%arg2, %0) : (i1, i32) -> (i32, i32) %6:2 = "dataflow.demux"(%arg2, %arg3) : (i1, vector<4xi1>) -> (vector<4xi1>, vector<4xi1>) %7:2 = "dataflow.sync"(%1#1, %2#1) : (none, none) -> (none, none) %8:2 = "dataflow.load"(%arg6, %4#1, %7#0, %6#1) : (memref<16xi32>, index, none, vector<4xi1>) -> (vector<4xi32>, none) %9:2 = "dataflow.sync"(%3#1, %8#1) : (none, none) -> (none, none) %10 = "dataflow.store"(%arg7, %4#1, %8#0, %9#0, %6#1) : (memref<16xi32>, index, vector<4xi32>, none, vector<4xi1>) -> none %11 = "dataflow.mux"(%arg2, %2#0, %10) : (i1, none, none) -> none %12 = "dataflow.mux"(%arg2, %3#0, %10) : (i1, none, none) -> none %13 = "dataflow.mux"(%arg2, %1#0, %1#1) : (i1, none, none) -> none %14:2 = "dataflow.demux"(%arg2, %13) : (i1, none) -> (none, none) %15:2 = "dataflow.demux"(%arg2, %11) : (i1, none) -> (none, none) %16:2 = "dataflow.demux"(%arg2, %12) : (i1, none) -> (none, none) %17:2 = "dataflow.demux"(%arg2, %arg1) : (i1, index) -> (index, index) %18:2 = "dataflow.demux"(%arg2, %0) : (i1, i32) -> (i32, i32) %19:2 = "dataflow.demux"(%arg2, %arg3) : (i1, vector<4xi1>) -> (vector<4xi1>, vector<4xi1>) %20:2 = "dataflow.sync"(%14#1, %15#1) : (none, none) -> (none, none) %21:2 = "dataflow.load"(%arg6, %17#1, %20#0, %19#1) : (memref<16xi32>, index, none, vector<4xi1>) -> (vector<4xi32>, none) %22:2 = "dataflow.sync"(%16#1, %21#1) : (none, none) -> (none, none) %23 = "dataflow.store"(%arg7, %17#1, %21#0, %22#0, %19#1) : (memref<16xi32>, index, vector<4xi32>, none, vector<4xi1>) -> none %24 = "dataflow.mux"(%arg2, %16#0, %23) : (i1, none, none) -> none %25 = "dataflow.mux"(%arg2, %14#0, %14#1) : (i1, none, none) -> none "dataflow.graph.return"(%25, %24) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> () }) : () -> () }) : () -> ()
partial source coverage: Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.
authoring-context.json{"entries":[{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"3-6","path":"docs/spec-compiler-part-3-mem.md","roles":["applicability"],"text":"This document is the memory-order source of truth for graph-local SCF to\nDataflow lowering. The concrete owner is `loom-lower-graph-memory`; it\nnormalizes supported memory leaves and recursively lowers structured graph\nregions in one traversal.","why":"Names loom-lower-graph-memory as the concrete owner of graph-local SCF to Dataflow memory lowering, fixing the pass under test and the graph-local scope of the sampled inputs."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"23-46","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"The lowering contract covers:\n\n* scalar and fixed-ranked vector forms of canonical `dataflow.load` and\n `dataflow.store`, including the masked contiguous and gather/scatter forms\n defined by `docs/spec-dataflow-vectorization.md`;\n* canonical atomic load/store, `dataflow.atomic_rmw`,\n `dataflow.cmpxchg`, `dataflow.fence`, and volatile access contracts defined\n by `docs/spec-dataflow-memory-consistency.md`;\n* normalized scalar `memref.load` and `memref.store` leaves over a canonical\n linear memory space;\n* sequential composition;\n* arbitrary nesting of `scf.if`, source-sequential `scf.for`, and\n `scf.while`;\n* basic graph-local alias-root partitions;\n* conservative unknown accesses;\n* value, execution, write-frontier, and read-frontier projection through the\n same structured selectors;\n* pre-mutation rejection of residual `scf.parallel` and `scf.forall` that\n reach a graph without an already materialized schedule boundary.\n\nThe lowering does not select parallel width, ownership, serialization,\nunrolling, reduction order, or any other schedule policy. Those decisions\nmust be made before graph-region lowering and normalized into supported\nstructured input.","why":"Defines the supported input surface the grammar samples: fixed-ranked vector dataflow.load/store including masked contiguous and gather/scatter forms, normalized scalar memref.load/store leaves over a canonical linear memory space, sequential composition, scf.if/scf.for nesting, and the exclusion of residual scf.parallel/scf.forall and of schedule-policy decisions."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"79-106","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"A canonical root is found by peeling an accepted side-effect-free memref view\nuntil reaching an explicit storage or boundary root. The finalized surface\nrecognizes:\n\n* a graph memory input, whose root identity comes from its launch binding;\n* a `dataflow.memory.service` result at that binding, which preserves the root\n of its exact pointer operand while changing only the value-plane pointer into\n a memory-plane capability;\n* a fresh `memref.alloc` result, whose root is unique for each invocation;\n* a verified side-effect-free view that preserves the source root. The initial\n accepted set contains `memref.cast`; adding another view form requires one\n matching root, region, and simulator contract before admission.\n\nWhen graph publication can trace every captured memory capability to a known\nroot, an exact service rooted at a unique thread argument mechanically inherits\nthat argument's `llvm.noalias` fact. If a root is unknown, appears through more\nthan one captured capability, or does not resolve to that argument, publication\nmust omit the fact. The service result does not independently assert aliasing,\nand graph publication does not perform another alias analysis.\n\nGraph launch memory bindings require exact memref capability types. An LLVM\npointer cannot bind a graph memref through a conversion, inferred base, or\nspecial address-space-zero rule. SCF optimization may first prove and\nmaterialize a rooted memref capability plus integer offset, or it may retain\nthe pointer as a value consumed by a `PointerAddressed` memory actor together\nwith an independently bound service capability. Neither path materializes a\ngraph-body bridge. `builtin.unrealized_conversion_cast` is never a canonical\nroot, view, actor, or boundary bridge.","why":"Canonical roots and graph launch bindings: graph memref capability inputs are canonical roots with exact memref types, so the grammar binds every access to graph memref inputs and never to LLVM pointers, conversions, or bridges."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"136-161","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"A memory input binds an established external memref capability through an\nexact graph-launch type match. An LLVM pointer never satisfies a graph memory\nport. A first-class pointer value used by a `PointerAddressed` actor resolves\nthrough the runtime object registry to one object and byte offset independently\nof the service-capability binding.\n\nDistinct graph memory inputs are conservatively may-alias unless explicit\nno-alias evidence distinguishes them. Distinct fresh allocations are\nindependent roots. The analysis does not use address ranges, affine\ndisjointness, bank identity, physical ports, or element-type compatibility to\nsplit a root.\n\n`memref.get_global`, `memref.alloca`, globals, static pointer bases, and\nunrecognized capability producers are not canonical roots. A pre-final\nanalysis may conservatively group an unresolved access while building an event\nnetwork, but finalization rejects any such residual producer rather than\ngranting it an external-memory authority.\n\nA source-origin `llvm.alloca` accepted by the Structured\n`PromoteOrderedBufferToChannel` decision is not an exception to this rule. That\ndecision must remove the complete proved allocation closure before D0; a\nresidual allocation or pointer use remains non-canonical and is rejected.\n\nAccess-to-partition membership is kept in a transient operation map before\nSCF operands are projected. Selector demuxing must not change alias identity.\nThe map is discarded after explicit event edges are emitted.","why":"Distinct graph memory inputs are conservatively may-alias and memref.get_global/memref.alloca/global/static pointer bases are not canonical roots; justifies sampling two may-alias memref inputs and excluding non-root producers."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"245-251","path":"docs/spec-compiler-part-3-mem.md","roles":["applicability","context"],"text":"One vector addressed memory actor is one canonical firing. Its active lanes do\nnot create independent frontier records or an implicit lane order.\n`P(access)` is the conservative union of alias partitions that any active lane\nmay access. A dynamic mask or address vector cannot weaken that set merely\nbecause one observed execution disables a lane. A statically proven all-zero\nmask may be simplified by an ordinary semantics-preserving Dataflow rewrite;\notherwise the firing retains its explicit `ctrl` and `done` obligations.","why":"The sampled output obligation with its governing context: one vector addressed memory actor is one canonical firing that retains its explicit ctrl and done obligations; determines both the selection of vector addressed actors and the ctrl/done assertions."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"470-493","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"The owner rejects before mutation when:\n\n* raw or unverifiably owned parallel SCF reaches a graph;\n* an effectful or unmodeled nested operation reaches a graph;\n* a residual LLVM load, store, atomicrmw, cmpxchg, fence, memcpy, memmove, or\n memset remains after\n normalization and therefore has no explicit completion event;\n* a source memory access has not been normalized to the canonical linear\n memory-space form required by its scalar or vector Dataflow actor;\n* structured control carries a memref result or memref loop state;\n* the graph entry lacks the leading `none` execution value.\n\nLLVM memcpy, memmove, and memset intrinsics are expanded into their exact\nstructured loop semantics before ownership selection. Supported LLVM\nload/store (including volatile and atomic contracts), `atomicrmw`, `cmpxchg`,\nand `fence` forms are then normalized before recursive region lowering, after\nwhich the same frontier rules apply. LLVM target-specific sync scopes without\na compiler-target owner and atomic accesses without an explicit power-of-two\nsource alignment fail closed. Every residual raw LLVM memory operation fails\nclosed. The finalized-graph gate also rejects residual\n`memref.load`/`memref.store`, `memref.get_global`, raw pointer arithmetic,\npointer-bearing operations, `builtin.unrealized_conversion_cast`, and unknown\nmemory-capability producers. An unsupported effectful operation inside a\nstructured region must likewise fail closed instead of being hoisted.","why":"Pre-mutation rejection list and finalized-graph gate (raw parallel SCF, residual LLVM memory ops, unnormalized accesses, memref results on structured control, missing leading none entry value, residual memref.load/store at the gate); the grammar avoids every rejected construct and always emits the leading none graph-entry value."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"412-527","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"//===----------------------------------------------------------------------===//\n// Memory Ops\n//\n// Streaming accesses against a memref, orchestrated by none-typed ctrl / done\n// tokens. The memref's element type constrains the element data type or the\n// access vector's element type.\n//===----------------------------------------------------------------------===//\n\n// The canonical memory actors. Each projects the standard MLIR memory effects\n// through the one shared implementation in `DataflowMemoryContracts.cpp`; no\n// actor classifies its own effects. That projection names the memory operand\n// for the addressed access and reads the atomic and volatile facts back from\n// the actor's one aggregate contract to add conservative unbound effects.\nclass Dataflow_MemoryActorOp<string mnemonic, list<Trait> traits = []>\n : Dataflow_Op<mnemonic, !listconcat(traits, [\n CanonicalDataflowActor,\n DeclareOpInterfaceMethods<MemoryEffectsOpInterface>])> {\n let extraClassDefinition = [{\n void $cppClass::getEffects(\n ::llvm::SmallVectorImpl<::mlir::MemoryEffects::EffectInstance>\n &effects) {\n ::dataflow::semantics::getMemoryActorEffects(getOperation(), effects);\n }\n }];\n}\n\ndef Dataflow_LoadOp : Dataflow_MemoryActorOp<\"load\"> {\n let summary = \"streaming element, contiguous vector, or gather load\";\n let description = [{\n On the simultaneous arrival of an address token and a `%ctrl : none`\n token, consumes both and fires one memory actor.\n A result type exactly equal to the memref element type loads one\n memory element, including when that element type is itself a vector.\n Otherwise, a fixed-size vector result of any positive rank loads that many\n elements in canonical row-major lane order, contiguously from a scalar\n `%addr : index` or, with a same-shape `%addr : vector<...xindex>`, one\n element per lane from the corresponding element-index address. A vector\n access requires the memref element type as its vector element type.\n\n An optional same-shape `i1` mask restricts a vector load to active lanes.\n Inactive lanes do not access memory and are deterministically zero-filled.\n After all active lanes retire, the op emits one data token and one `none`\n token on `%done`.\n\n The optional `contract` attribute is this actor's single\n `MemoryAccessContract`; its absence is the canonical plain non-volatile\n contract.\n }];\n\n let arguments = (ins AnyMemRef:$mem, AnyType:$addr, NoneType:$ctrl,\n Optional<AnyVectorOfAnyRank>:$mask,\n OptionalAttr<Dataflow_MemoryAccessContract>:$contract);\n let results = (outs AnyType:$data, NoneType:$done);\n\n let hasCustomAssemblyFormat = 1;\n let hasVerifier = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::Type\":$data,\n \"::mlir::Type\":$done,\n \"::mlir::Value\":$mem,\n \"::mlir::Value\":$addr,\n \"::mlir::Value\":$ctrl)>,\n OpBuilder<(ins\n \"::mlir::Value\":$mem,\n \"::mlir::Value\":$addr,\n \"::mlir::Value\":$ctrl)>\n ];\n}\n\ndef Dataflow_StoreOp : Dataflow_MemoryActorOp<\"store\"> {\n let summary = \"streaming element, contiguous vector, or scatter store\";\n let description = [{\n On the simultaneous arrival of an address token, a `%data` value\n and a `%ctrl : none`, consumes all three and fires one memory actor.\n Data whose type exactly equals the memref element type writes one\n memory element, including when that element type is itself a vector.\n Otherwise, fixed-size vector data of any positive rank writes that many\n elements in canonical row-major lane order, contiguously from a scalar\n `%addr : index` or, with a same-shape `%addr : vector<...xindex>`, one\n element per lane. A vector access requires the memref element type as its\n vector element type.\n\n An optional same-shape `i1` mask restricts a vector store to active lanes.\n Inactive lanes do not access memory. After all active lanes retire, the op\n emits one `none` token on `%done`.\n\n The optional `contract` attribute is this actor's single\n `MemoryAccessContract`; its absence is the canonical plain non-volatile\n contract.\n }];\n\n let arguments = (ins AnyMemRef:$mem, AnyType:$addr, AnyType:$data,\n NoneType:$ctrl,\n Optional<AnyVectorOfAnyRank>:$mask,\n OptionalAttr<Dataflow_MemoryAccessContract>:$contract);\n let results = (outs NoneType:$done);\n\n let hasCustomAssemblyFormat = 1;\n let hasVerifier = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::Type\":$done,\n \"::mlir::Value\":$mem,\n \"::mlir::Value\":$addr,\n \"::mlir::Value\":$data,\n \"::mlir::Value\":$ctrl)>,\n OpBuilder<(ins\n \"::mlir::Value\":$mem,\n \"::mlir::Value\":$addr,\n \"::mlir::Value\":$data,\n \"::mlir::Value\":$ctrl)>\n ];\n}","why":"TableGen definition of the canonical memory actors dataflow.load and dataflow.store: operand order (mem, addr, ctrl:none, optional mask) and result order (data, done:none / done:none), which fixes both the gather/scatter input spelling and the operand/result positions read by the postcondition."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"839-950","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_well_formedness"],"text":"def Dataflow_GraphOp : Dataflow_Op<\"graph\", [\n IsolatedFromAbove,\n HasParent<\"::mlir::ModuleOp\">,\n SingleBlockImplicitTerminator<\"GraphReturnOp\">,\n FunctionOpInterface,\n RecursiveMemoryEffects,\n DeclareOpInterfaceMethods<RegionKindInterface>\n]> {\n let summary = \"Symbol-bearing function-like SpatialCore graph definition\";\n let description = [{\n Module-scope, function-like callable holding the SpatialCore body\n of a leaf dataflow graph. It does not itself execute; one or more\n `dataflow.graph.launch` ops materialise launches of it inside the\n body of a `dataflow.thread` definition.\n\n `function_type` contains only application payload ports. Normalized\n `input_segments` and `result_segments` classify those payloads as value,\n stream, and memory ports. The body's distinguished leading `none` block\n argument is the invocation start protocol endpoint, while launch `done`\n is derived exclusively from `dataflow.graph.return.complete`; neither is\n stored in the function type.\n\n This is the only canonical graph definition surface.\n }];\n\n let arguments = (ins\n SymbolNameAttr:$sym_name,\n TypeAttrOf<FunctionType>:$function_type,\n DenseI32ArrayAttr:$input_segments,\n DenseI32ArrayAttr:$result_segments,\n OptionalAttr<StrAttr>:$sym_visibility,\n OptionalAttr<DictArrayAttr>:$arg_attrs,\n OptionalAttr<DictArrayAttr>:$res_attrs);\n\n let regions = (region SizedRegion<1>:$body);\n\n let hasCustomAssemblyFormat = 1;\n let hasVerifier = 1;\n\n let builders = [\n OpBuilder<(ins\n \"::llvm::StringRef\":$name,\n \"::mlir::FunctionType\":$type,\n CArg<\"::llvm::ArrayRef<::mlir::NamedAttribute>\", \"{}\">:$attrs)>\n ];\n\n let extraClassDeclaration = [{\n /// FunctionOpInterface methods.\n ::llvm::ArrayRef<::mlir::Type> getArgumentTypes() {\n return getFunctionType().getInputs();\n }\n ::llvm::ArrayRef<::mlir::Type> getResultTypes() {\n return getFunctionType().getResults();\n }\n ::mlir::Region *getCallableRegion() {\n return isExternal() ? nullptr : &getBody();\n }\n bool isExternal() { return getBody().empty(); }\n ::mlir::BlockArgument getStart();\n ::llvm::ArrayRef<int32_t> getInputSegmentSizes();\n ::llvm::ArrayRef<int32_t> getResultSegmentSizes();\n GraphPortKind getInputPortKind(unsigned index);\n GraphPortKind getResultPortKind(unsigned index);\n ::llvm::LogicalResult verifyBody() {\n if (isExternal())\n return ::mlir::success();\n ::mlir::Block &entry = getBody().front();\n ::llvm::ArrayRef<::mlir::Type> inputs = getFunctionType().getInputs();\n if (entry.getNumArguments() != inputs.size() + 1)\n return emitOpError(\"entry block must have one start argument plus \")\n << inputs.size() << \" application inputs\";\n if (!::llvm::isa<::mlir::NoneType>(entry.getArgument(0).getType()))\n return emitOpError(\"entry block argument #0 must be start type none\");\n for (size_t i = 0, e = inputs.size(); i < e; ++i) {\n if (entry.getArgument(i + 1).getType() != inputs[i])\n return emitOpError(\"entry block argument #\")\n << (i + 1) << \" type \"\n << entry.getArgument(i + 1).getType()\n << \" must match function input type \" << inputs[i];\n }\n return ::mlir::success();\n }\n }];\n}\n\ndef Dataflow_GraphReturnOp : Dataflow_Op<\"graph.return\", [\n AttrSizedOperandSegments,\n Terminator,\n ParentOneOf<[\"::dataflow::GraphOp\"]>,\n Pure\n]> {\n let summary = \"Terminator for a dataflow.graph body\";\n let description = [{\n Structurally declares the enclosing graph's value, stream, and memory\n outputs together with its mandatory retirement frontier. `complete` is\n an unordered all-of set of one or more `none` values; the launch `done`\n event is derived from that set and is not itself a return operand.\n\n The compact assembly form `%complete, %values... : none, types...` is\n retained for the common case with one completion witness and no stream\n or memory outputs. Other shapes print all four named segments.\n }];\n\n let arguments = (ins\n Variadic<AnyType>:$values,\n Variadic<AnyType>:$streams,\n Variadic<AnyType>:$memories,\n Variadic<NoneType>:$complete);\n\n let hasCustomAssemblyFormat = 1;\n\n let skipDefaultBuilders = 1;","why":"dataflow.graph and dataflow.graph.return definitions: the leading none start block argument, the input_segments/result_segments value-stream-memory classification, and the compact return form used by every sampled graph."},{"file_sha256":"8df97a8d593919ad549cd11f13281c367f306cb3dc073d1a2793b28f8182db2a","kind":"verifier","lines":"36-59,116-146","path":"lib/Frontend/Lowering/RankedMemRefLowering.cpp","roles":["input_well_formedness"],"text":"::mlir::LogicalResult checkRankedVectorTransfer(::mlir::Operation *operation,\n ::mlir::MemRefType memory,\n ::mlir::ValueRange indices,\n ::mlir::VectorType vector,\n ::mlir::AffineMap permutation,\n ::mlir::ArrayAttr inBounds,\n unsigned indexBits) {\n ::llvm::SmallVector<std::int64_t> strides;\n std::int64_t offset = 0;\n if (vector.isScalable() || vector.getRank() != 1 || memory.getRank() != 1 ||\n memory.getElementType() != vector.getElementType() ||\n ::mlir::failed(memory.getStridesAndOffset(strides, offset)) ||\n strides.size() != 1 || strides.front() != 1 ||\n permutation !=\n ::mlir::AffineMap::getMultiDimIdentityMap(1, operation->getContext()))\n return operation->emitError(\n \"loom-lower-graph-memory: vector transfer requires a fixed rank-one \"\n \"minor-identity access over a unit-stride scalar memref\");\n if (!allTransferDimensionsInBounds(inBounds))\n return operation->emitError(\n \"loom-lower-graph-memory: vector transfer requires every lane to be \"\n \"proven in-bounds\");\n return checkRankedMemRefAccess(operation, memory, indices, indexBits);\ncheckRankedVectorTransferRead(::mlir::vector::TransferReadOp read,\n unsigned indexBits) {\n auto memory = ::llvm::dyn_cast<::mlir::MemRefType>(read.getBase().getType());\n if (!memory)\n return read.emitOpError(\n \"loom-lower-graph-memory: vector read requires a ranked memref base\");\n const bool paddingCanBeObserved =\n read.getMask() && !resultIsMaskGuarded(read);\n if (paddingCanBeObserved &&\n !::mlir::matchPattern(read.getPadding(), ::mlir::m_Zero()))\n return read.emitOpError(\n \"loom-lower-graph-memory: observable vector read padding must be \"\n \"zero\");\n return checkRankedVectorTransfer(\n read, memory, read.getIndices(), read.getVectorType(),\n read.getPermutationMap(), read.getInBounds(), indexBits);\n}\n\n::mlir::LogicalResult\ncheckRankedVectorTransferWrite(::mlir::vector::TransferWriteOp write,\n unsigned indexBits) {\n auto memory = ::llvm::dyn_cast<::mlir::MemRefType>(write.getBase().getType());\n if (!memory || write.getResult())\n return write.emitOpError(\n \"loom-lower-graph-memory: vector write requires a ranked memref base\");\n return checkRankedVectorTransfer(\n write, memory, write.getIndices(), write.getVectorType(),\n write.getPermutationMap(), write.getInBounds(), indexBits);\n}\n\n::mlir::Value buildExactLinearIndex(::mlir::OpBuilder &builder,","why":"Acceptance conditions for vector transfers in a graph: fixed rank-one minor-identity access over a unit-stride rank-one memref whose element type equals the vector element type, every lane proven in-bounds, and zero padding when masked padding is observable; the grammar emits exactly this shape."},{"file_sha256":"4295a7f0089a5b35f7f7f538032b31f51ca3966d4279faa030a2d493a8f76385","kind":"implementation","lines":"1390-1440","path":"lib/Frontend/Lowering/GraphRegionLowering.cpp","roles":["applicability"],"text":"void lowerVectorRead(::mlir::vector::TransferReadOp read,\n ::mlir::Value execution, MemoryState &memory) {\n ::llvm::SmallVector<unsigned, 4> membership = partitionsFor(read);\n ::mlir::Value ctrl = readControl(read, execution, memory);\n setInsertionPoint(read.getLoc());\n auto memoryType =\n ::llvm::cast<::mlir::MemRefType>(read.getBase().getType());\n ::mlir::Value address = ::loom::lowering::detail::buildExactLinearIndex(\n builder, read.getLoc(), memoryType, read.getIndices(), execution);\n auto lowered = ::dataflow::LoadOp::create(\n builder, read.getLoc(), read.getVectorType(), builder.getNoneType(),\n read.getBase(), address, ctrl, read.getMask(), ::mlir::Attribute{});\n partitionsByAccess.try_emplace(lowered, std::move(membership));\n read.getResult().replaceAllUsesWith(lowered.getData());\n updateReadFrontiers(lowered, lowered.getDone(), memory);\n read.erase();\n }\n\n void lowerVectorWrite(::mlir::vector::TransferWriteOp write,\n ::mlir::Value execution, MemoryState &memory) {\n ::llvm::SmallVector<unsigned, 4> membership = partitionsFor(write);\n ::mlir::Value ctrl = writeControl(write, execution, memory);\n setInsertionPoint(write.getLoc());\n auto memoryType =\n ::llvm::cast<::mlir::MemRefType>(write.getBase().getType());\n ::mlir::Value address = ::loom::lowering::detail::buildExactLinearIndex(\n builder, write.getLoc(), memoryType, write.getIndices(), execution);\n auto lowered = ::dataflow::StoreOp::create(\n builder, write.getLoc(), builder.getNoneType(), write.getBase(),\n address, write.getValueToStore(), ctrl, write.getMask(),\n ::mlir::Attribute{});\n partitionsByAccess.try_emplace(lowered, std::move(membership));\n updateWriteFrontiers(lowered, lowered.getDone(), memory);\n write.erase();\n }\n\n void lowerDataflowLoad(::dataflow::LoadOp load, ::mlir::Value execution,\n MemoryState &memory) {\n load.getCtrlMutable().assign(readControl(load, execution, memory));\n updateReadFrontiers(load, load.getDone(), memory);\n if (load->getBlock() != &entry)\n load->moveBefore(anchor);\n }\n\n void lowerDataflowStore(::dataflow::StoreOp store, ::mlir::Value execution,\n MemoryState &memory) {\n store.getCtrlMutable().assign(writeControl(store, execution, memory));\n updateWriteFrontiers(store, store.getDone(), memory);\n if (store->getBlock() != &entry)\n store->moveBefore(anchor);\n }","why":"Shows that vector.transfer_read/transfer_write become vector-addressed dataflow.load/store actors and that pre-existing dataflow.load/store actors only get their ctrl reassigned, establishing which output operations the sampled obligation governs."},{"file_sha256":"11d4b44ce36afb532b1ba720012841c38babad2962aadee232609a04fc28dbc4","kind":"test","lines":"1-23","path":"test/raise/scf-to-dfg-memory-frontier.mlir","roles":["input_construction"],"text":"// RUN: loom-raise-opt --split-input-file --loom-lower-graph-memory %s | FileCheck %s\n\n// CHECK-LABEL: dataflow.graph private @frontier_straight\n// CHECK: %[[R0:.*]], %[[D0:.*]] = dataflow.load %arg4[%arg1] %arg0 : memref<16xi32>\n// CHECK: %[[R1:.*]], %[[D1:.*]] = dataflow.load %arg4[%arg2] %arg0 : memref<16xi32>\n// CHECK: %[[WRITE:.*]] = dataflow.store %arg4[%arg1] %arg3 [[READS:%[^# ]+]]#0 : memref<16xi32>\n// CHECK: %[[R2:.*]], %[[D2:.*]] = dataflow.load %arg4[%arg2] %[[WRITE]] : memref<16xi32>\n// CHECK: [[READS]]:2 = dataflow.sync %[[D0]], %[[D1]] : (none, none) -> (none, none)\n// CHECK: %[[RB:.*]], %[[DB:.*]] = dataflow.load %arg5[%arg1] %[[WRITE]] : memref<16xi32>\n// CHECK: %[[RETIRE:.*]]:2 = dataflow.sync %[[D2]], %[[DB]] : (none, none) -> (none, none)\n// CHECK: dataflow.graph.return %[[RETIRE]]#0 : none\ndataflow.graph private @frontier_straight(\n %start: none, %i: index, %j: index, %value: i32,\n %a: memref<16xi32>, %b: memref<16xi32>) -> ()\n attributes {input_segments = array<i32: 3, 0, 2>,\n result_segments = array<i32: 0, 0, 0>} {\n %r0, %read0_done = dataflow.load %a[%i] %start : memref<16xi32>\n %r1, %read1_done = dataflow.load %a[%j] %start : memref<16xi32>\n %write_done = dataflow.store %a[%i] %value %start : memref<16xi32>\n %r2, %read2_done = dataflow.load %a[%j] %start : memref<16xi32>\n %rb = memref.load %b[%i] : memref<16xi32>\n dataflow.graph.return %start : none\n}","why":"Non-normative evidence for the accepted module spelling under this pass: a private dataflow.graph with a leading none start argument, may-alias memref inputs, memory leaves in the body, and dataflow.graph.return."},{"file_sha256":"d161de7a4a08f9902236e14b73808fc9caeadf88e4b2f2e15d61000cb648ebb0","kind":"example","lines":"69-80","path":"test/raise/scf-to-dfg-graph-memory.mlir","roles":["input_construction"],"text":"//--- ranked.mlir\nmodule {\n dataflow.graph private @rank3_row_major(\n %start: none, %i: index, %j: index, %k: index,\n %memory: memref<3x5x7xf32>) -> ()\n attributes {input_segments = array<i32: 3, 0, 1>,\n result_segments = array<i32: 0, 0, 0>} {\n %value = memref.load %memory[%i, %j, %k] : memref<3x5x7xf32>\n memref.store %value, %memory[%i, %j, %k] : memref<3x5x7xf32>\n dataflow.graph.return %start : none\n }\n}","why":"One accepted spelling of the graph attribute dictionary (input_segments/result_segments arrays) used verbatim in shape by the generated graphs."},{"file_sha256":"2eff2258b85959a00302a5bee9240d30ea330a85061eaedae51a3fad2f9e37f4","kind":"example","lines":"46-64","path":"test/dataflow/unit/load/valid.mlir","roles":["input_construction"],"text":"// CHECK-LABEL: @load_masked_vector_i32\nfunc.func @load_masked_vector_i32(\n %mem: memref<10xi32>, %addr: index, %mask: vector<4xi1>, %ctrl: none)\n -> (vector<4xi32>, none) {\n // CHECK: dataflow.load %{{.*}}[%{{.*}}] %{{.*}} mask %{{.*}} : memref<10xi32>, vector<4xi32>\n %data, %done = dataflow.load %mem[%addr] %ctrl mask %mask\n : memref<10xi32>, vector<4xi32>\n return %data, %done : vector<4xi32>, none\n}\n\n// CHECK-LABEL: @load_gather_i32\nfunc.func @load_gather_i32(\n %mem: memref<10xi32>, %addr: vector<4xindex>, %mask: vector<4xi1>,\n %ctrl: none) -> (vector<4xi32>, none) {\n // CHECK: dataflow.load %{{.*}}[%{{.*}}] %{{.*}} mask %{{.*}} : memref<10xi32>, vector<4xindex>, vector<4xi32>\n %data, %done = dataflow.load %mem[%addr] %ctrl mask %mask\n : memref<10xi32>, vector<4xindex>, vector<4xi32>\n return %data, %done : vector<4xi32>, none\n}","why":"Accepted textual spelling of masked contiguous and gather dataflow.load, used for the gather alternative emitted directly by the grammar."},{"file_sha256":"3b048f487c94803ff885832a4d9ade824e1f58c396e2838dac0cd0628c145333","kind":"example","lines":"46-64","path":"test/dataflow/unit/store/valid.mlir","roles":["input_construction"],"text":"// CHECK-LABEL: @store_masked_vector_i32\nfunc.func @store_masked_vector_i32(\n %mem: memref<10xi32>, %addr: index, %data: vector<4xi32>,\n %mask: vector<4xi1>, %ctrl: none) -> none {\n // CHECK: dataflow.store %{{.*}}[%{{.*}}] %{{.*}} %{{.*}} mask %{{.*}} : memref<10xi32>, vector<4xi32>\n %done = dataflow.store %mem[%addr] %data %ctrl mask %mask\n : memref<10xi32>, vector<4xi32>\n return %done : none\n}\n\n// CHECK-LABEL: @store_multi_rank_scatter\nfunc.func @store_multi_rank_scatter(\n %mem: memref<10xi32>, %addr: vector<2x3xindex>, %data: vector<2x3xi32>,\n %mask: vector<2x3xi1>, %ctrl: none) -> none {\n // CHECK: dataflow.store %{{.*}}[%{{.*}}] %{{.*}} %{{.*}} mask %{{.*}} : memref<10xi32>, vector<2x3xindex>, vector<2x3xi32>\n %done = dataflow.store %mem[%addr] %data %ctrl mask %mask\n : memref<10xi32>, vector<2x3xindex>, vector<2x3xi32>\n return %done : none\n}","why":"Accepted textual spelling of masked contiguous and scatter dataflow.store, used for the scatter alternative emitted directly by the grammar."}],"primary_bundle_sha256":"82b7fabd40d78b956f5f6ff6dffecb7e5318aa105f1072eb2a3c349cab37de52","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"c33a8a8330f1ceb49ed04550b36e928f86ea79b389eb91a24fb818168e05b833"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 45902,
"duration_ms": 45956,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1525,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 4740,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.13253500000000001,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3405,
"provider": "firstParty",
"thinkingTokens": 618,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR `module { ... }` containing only `dataflow.graph` definitions at the top level and nothing else.\n2. Each graph is declared as `dataflow.graph private @graph_<n>` with an empty result list `-> ()`, so no graph returns values.\n3. Every graph's entry block takes a `none`-typed token operand named `%start` as its first parameter, and the graph body is terminated by `dataflow.graph.return %start : none`, i.e. the incoming token is threaded straight to the terminator.\n4. Each graph carries both a `input_segments` and a `result_segments` `array<i32: ...>` attribute whose entries sum consistently with the declared operands and results (five non-token scalar/vector inputs, zero of the middle class, two memref inputs; zero results of every class).\n5. Memref-typed graph parameters are plain statically shaped `memref<16xi32>` capability inputs supplied by the graph signature; the body never allocates, declares, or otherwise materializes memory (`memref.alloca`, `memref.get_global`, globals, pointers, `unrealized_conversion_cast` are all absent).\n6. Every memory operation in a body addresses one of the graph's own memref parameters by name; there are no cross-graph or externally defined memory references.\n7. Vector memory traffic occurs only as a matched pair: a `vector.transfer_read` producing a value that is immediately consumed as the value operand of a following `vector.transfer_write`; a read never appears without its dependent write and the write's data operand is never an unrelated SSA value.\n8. Every `vector.transfer_read`/`vector.transfer_write` is rank-one, uses the single index operand `%i`, carries `{in_bounds = [true]}`, and transfers exactly `vector<4xi32>` to/from `memref<16xi32>` \u2014 no transposing permutation maps, no multi-dimensional indices, no out-of-bounds transfers.\n9. A `vector.transfer_read` supplies a scalar padding operand (`%pad`) of the memref element type, and the padding value is available in the graph before any transfer that uses it.\n10. Masking on a transfer pair is all-or-nothing: either both the read and the write carry the `vector<4xi1>` mask operand `%m`, or neither does; a mixed masked-read/unmasked-write pair never occurs.\n11. The mask operand's vector length matches the transfer vector length (4 lanes), and the mask is a graph parameter, not a locally computed value.\n12. Scalar memory traffic likewise occurs only as a store followed by a load, both normalized to the same single index `%i` on the same memref and with element type `i32`; the stored value is the graph's `%val` parameter.\n13. Gather/scatter traffic is expressed exclusively through `dataflow.load` / `dataflow.store` actors, each taking a `vector<4xindex>` address vector, the `%start` token, and a `mask %m` operand; the gathered result is the value operand of the paired scatter, making the scatter data-dependent on the load.\n14. `dataflow.load` yields two results (a data vector and a dependency/token result) and `dataflow.store` yields one result, and these results are bound to distinct SSA names.\n15. Nesting of memory leaves is permitted only inside `scf.if` and `scf.for`; no `scf.parallel`, `scf.forall`, `scf.while`, or LLVM-dialect memory operation appears anywhere.\n16. `scf.if` regions used here are value-free: the condition is an `i1` graph parameter, there is no `else` region, and no results are yielded.\n17. `scf.for` loops are value-free as well: no `iter_args`, no yielded results, and lower bound, upper bound, and step are `index`-typed SSA values defined by constants dominating the loop in the same block.\n18. All SSA names defined within a graph body are unique, and every use of a value is dominated by its definition (constants for a loop precede that loop, a transfer read precedes its write, a store precedes the matching load, a gather precedes its scatter).\n19. Each graph body contains at least one vector-addressed memory access (a transfer pair, a `dataflow.load`/`store` pair, or one of these nested in a region), so no graph is free of the governed construct.\n\n## Sampling conventions\n\n1. The module holds either one or two graphs, never zero and never more than two.\n2. Graphs are named by position, `@graph_0` and `@graph_1`, using a counter that starts at zero and increments per graph.\n3. Every graph uses one fixed, identical signature \u2014 `%start: none, %i: index, %c: i1, %m: vector<4xi1>, %av: vector<4xindex>, %val: i32, %a: memref<16xi32>, %b: memref<16xi32>` \u2014 rather than varying arity, types, or parameter order.\n4. The attribute preamble is a constant: `input_segments = array<i32: 5, 0, 2>` and `result_segments = array<i32: 0, 0, 0>` on every graph.\n5. Each body opens with a fixed constant preamble `%pad = arith.constant 0 : i32`, so the transfer padding value is always the integer zero and is emitted even when no unmasked/masked read follows.\n6. Exactly one leading statement is emitted, chosen from transfer pair, gather/scatter pair, `scf.if`, or `scf.for` \u2014 the scalar store/load pair is deliberately never chosen as the leading statement.\n7. After the leading statement, between zero and four further statements are emitted, each chosen freely from transfer pair, gather/scatter pair, scalar pair, `scf.if`, or `scf.for`; the maximum body length is therefore five statements plus the constant preamble and terminator.\n8. Memref element type and shape are fixed at `memref<16xi32>`, and the vector shape is fixed at four lanes (`vector<4xi32>`, `vector<4xi1>`, `vector<4xindex>`); no other widths, ranks, or element types are sampled.\n9. All memory accesses use the single graph parameter `%i` as the (only) index, even inside `scf.for`, whose induction variable is never used as an address.\n10. Masking of a transfer pair is sampled as a binary choice per pair; both the fully masked and fully unmasked forms are produced, and the mask, when present, is always the parameter `%m` rather than a constructed mask.\n11. The source and destination memrefs of a transfer pair are independently chosen from `{%a, %b}`, so read-and-write-to-the-same-memref pairs as well as `%a`\u2192`%b` and `%b`\u2192`%a` pairs all occur.\n12. The scalar pair chooses one memref from `{%a, %b}` and uses it for both the store and the load, never crossing between the two.\n13. The gather/scatter pair is fixed in its operands: it always loads from `%a` and stores to `%b`, always uses the address vector `%av`, and is always masked with `%m` \u2014 unmasked or `%b`\u2192`%a` gather/scatter forms are never emitted.\n14. A single per-graph counter supplies the numeric suffix for every named entity (`%v<k>`, `%s<k>`, `%g<k>`/`%gd<k>`/`%sc<k>`, `%lb<k>`/`%ub<k>`/`%sp<k>`/`%k<k>`), incrementing once per statement or nested pair, which guarantees unique names without reusing a per-kind counter.\n15. `scf.if` regions contain exactly one transfer pair and nothing else, and the condition is always the parameter `%c`; scalar pairs, gather pairs, and further nesting never appear inside an `if`.\n16. `scf.for` bodies likewise contain exactly one transfer pair and nothing else, so nesting depth never exceeds one region inside a graph body.\n17. Loop trip counts are fixed by a constant triple emitted immediately before each loop \u2014 lower bound `0`, upper bound `4`, step `1` \u2014 matching the vector lane count and keeping loops finite.\n18. The loop induction variable `%k<k>` is bound but unused in the loop body, exercising the loop-nesting shape without introducing loop-varying addresses.\n19. Indentation and formatting are fixed: two spaces for graph headers, four for body statements, with the multi-line signature and attribute block broken at constant positions.",
"result_index": 0,
"session_id": "f199b8a2-d994-4064-ae20-7b693fd0a0bb",
"stop_reason": "end_turn",
"subagent_stats": {
"by_type": {},
"completed": 0,
"failed": 0,
"killed": {
"parent": 0,
"system": 0,
"user": 0
},
"max_depth": 0,
"refused": {
"budget": 0,
"concurrency_limit": 0,
"depth_limit": 0
},
"requested": {
"background": 0,
"foreground": 0,
"unset": 0
},
"spawned": 0,
"spawned_by_subagents": 0,
"started_in_background": 0
},
"subtype": "success",
"terminal_reason": "completed",
"time_to_request_ms": 55,
"total_cost_usd": 0.13253500000000001,
"ttft_ms": 9932,
"ttft_stream_ms": 1081,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 4740,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 4740,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3405,
"output_tokens_details": {
"thinking_tokens": 618
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "1f059237-d372-47bc-b781-edf1b16accf9"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 13976,
"duration_ms": 14000,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1872,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5973,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.08454,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 992,
"provider": "firstParty",
"thinkingTokens": 417,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition looks only at the subject's output program, never at the input, and it scans every operation at every nesting depth of that program. It first selects two groups by name and type shape: `dataflow.load` operations whose second operand has type kind `vector`, or whose first result is a vector type differing from the first operand type's element type; and `dataflow.store` operations whose second operand has type kind `vector`, or whose third operand is a vector type differing from the first operand type's element type. Every selected load must then satisfy four things: it has at least three operands with the third one typed `none`, it has exactly one `none`-typed operand in total, it has exactly two results with the second one typed `none`, and it has exactly one `none`-typed result in total. Every selected store must likewise have at least four operands with the fourth typed `none`, exactly one `none`-typed operand overall, exactly one result, that result typed `none`, and exactly one `none`-typed result overall. A load or store is rejected if it is missing the `none` operand at the required position, carries a second `none` operand anywhere, has the wrong result count, or produces a result that is not `none` at the required position or an extra `none` result.\n\nAll values consulted come from operand and result positions, their types, type `kind`, and a vector/memref-style `element_type` projection; no attributes, symbols, regions, or block arguments are read, and no counts are compared against the input program. Operations of any other name, and loads or stores whose operand and result types do not match the vector-shaped selection predicate, are never examined and are neither accepted nor rejected by the asserts. If the output contains no operation matching either selection predicate, both `forall` blocks range over empty sequences and the postcondition holds vacuously, so an output with no `dataflow.load` or `dataflow.store` at all passes.",
"result_index": 0,
"session_id": "27b13e86-411a-4e8c-acbe-5a7518049645",
"stop_reason": "end_turn",
"subagent_stats": {
"by_type": {},
"completed": 0,
"failed": 0,
"killed": {
"parent": 0,
"system": 0,
"user": 0
},
"max_depth": 0,
"refused": {
"budget": 0,
"concurrency_limit": 0,
"depth_limit": 0
},
"requested": {
"background": 0,
"foreground": 0,
"unset": 0
},
"spawned": 0,
"spawned_by_subagents": 0,
"started_in_background": 0
},
"subtype": "success",
"terminal_reason": "completed",
"time_to_request_ms": 25,
"total_cost_usd": 0.08454,
"ttft_ms": 6352,
"ttft_stream_ms": 1321,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5973,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5973,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 992,
"output_tokens_details": {
"thinking_tokens": 417
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "80b61ad9-8ac2-452d-af17-6261fb6617b3"
}
]
This paired revision was activated by an explicit partial-scope team review bound to both executable artifact hashes.
Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.