MS0V8 mlir-stage-09-v1 passing 5000/5000
Estimated confidence: 78.7%. Conservative lower bound: 62.0% (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.cppMS0V | 1089/1621lines67.2% 747/1330branches56.2% | 1090/1621lines67.2%+1 750/1330branches56.4%+3 | |
1 newly covered line · 3 newly covered branches283 | |||
…/lib/Dataflow/IR/DataflowGraphValidation.cppMS0V | 1033/1540lines67.1% 571/1056branches54.1% | 1038/1540lines67.4%+5 575/1056branches54.5%+4 | |
5 newly covered lines · 4 newly covered branches711 | |||
…/lib/Dataflow/IR/OperationSchema.cppMS0V | 274/716lines38.3% 127/350branches36.3% | 274/716lines38.3%+0 128/350branches36.6%+1 | |
1 newly covered branch736 | |||
…/loom/include/Common/Artifact.hMS0V | 13/37lines35.1% 3/18branches16.7% | 13/37lines35.1%+0 3/18branches16.7%+0 | Open PBT |
…/include/Dataflow/IR/OperationSchema.hMS0V | 8/91lines8.8% 5/66branches7.6% | 8/91lines8.8%+0 5/66branches7.6%+0 | Open PBT |
…/include/Frontend/Lowering/StreamLoopAttrs.hMS0V | 31/41lines75.6% 10/14branches71.4% | 31/41lines75.6%+0 10/14branches71.4%+0 | Open PBT |
…/loom/lib/Common/DiagnosticVerbosity.cppMS0V | 12/41lines29.3% 1/28branches3.6% | 12/41lines29.3%+0 1/28branches3.6%+0 | Open PBT |
…/loom/lib/Common/IndexWidth.cppMS0V | 63/84lines75.0% 28/42branches66.7% | 63/84lines75.0%+0 28/42branches66.7%+0 | Open PBT |
…/loom/lib/Common/InvocationDiagnosticLog.cppMS0V | 6/100lines6.0% 1/70branches1.4% | 6/100lines6.0%+0 1/70branches1.4%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowChannelOps.cppMS0V | 59/88lines67.0% 13/38branches34.2% | 59/88lines67.0%+0 13/38branches34.2%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowDialect.cppMS0V | 22/32lines68.8% 4/10branches40.0% | 22/32lines68.8%+0 4/10branches40.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowFunctionLikeOps.cppMS0V | 693/1097lines63.2% 264/592branches44.6% | 693/1097lines63.2%+0 264/592branches44.6%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowGraphCausality.cppMS0V | 169/189lines89.4% 79/98branches80.6% | 169/189lines89.4%+0 79/98branches80.6%+0 | |
…/lib/Dataflow/IR/DataflowMemoryContracts.cppMS0V | 198/371lines53.4% 98/218branches45.0% | 198/371lines53.4%+0 98/218branches45.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowOps.cppMS0V | 270/410lines65.9% 103/228branches45.2% | 270/410lines65.9%+0 103/228branches45.2%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowProgramValidation.cppMS0V | 367/502lines73.1% 156/276branches56.5% | 367/502lines73.1%+0 156/276branches56.5%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowSyncRendezvous.cppMS0V | 21/21lines100.0% 6/12branches50.0% | 21/21lines100.0%+0 6/12branches50.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowThreadCompletion.cppMS0V | 288/361lines79.8% 148/218branches67.9% | 288/361lines79.8%+0 148/218branches67.9%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowVectorSemantics.cppMS0V | 81/121lines66.9% 53/106branches50.0% | 81/121lines66.9%+0 53/106branches50.0%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaCodecInternal.hMS0V | 28/120lines23.3% 4/44branches9.1% | 28/120lines23.3%+0 4/44branches9.1%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaTypeCodec.cppMS0V | 85/516lines16.5% 55/374branches14.7% | 85/516lines16.5%+0 55/374branches14.7%+0 | Open PBT |
…/lib/Dataflow/Transforms/DataflowRewritePass.cppMS0V | 338/559lines60.5% 172/340branches50.6% | 338/559lines60.5%+0 172/340branches50.6%+0 | Open PBT |
…/lib/Frontend/Analysis/MemoryProvenance.cppMS0V | 153/317lines48.3% 80/326branches24.5% | 153/317lines48.3%+0 80/326branches24.5%+0 | Open PBT |
…/lib/Frontend/IR/LoomDialect.cppMS0V | 6/6lines100.0% branchesnot measured | 6/6lines100.0%+0 branchesnot measured | Open PBT |
…/lib/Frontend/IR/LoomOps.cppMS0V | 120/184lines65.2% 71/112branches63.4% | 120/184lines65.2%+0 71/112branches63.4%+0 | Open PBT |
…/lib/Frontend/Lowering/ExactMemRefLayout.cppMS0V | 61/143lines42.7% 26/80branches32.5% | 61/143lines42.7%+0 26/80branches32.5%+0 | Open PBT |
…/lib/Frontend/Lowering/ExpandGraphMemrefCopyPass.cppMS0V | 79/90lines87.8% 20/22branches90.9% | 79/90lines87.8%+0 20/22branches90.9%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphIndexLowering.cppMS0V | 260/288lines90.3% 129/168branches76.8% | 260/288lines90.3%+0 129/168branches76.8%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphParallelLowering.cppMS0V | 651/1243lines52.4% 284/786branches36.1% | 651/1243lines52.4%+0 284/786branches36.1%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphRegionAdmission.cppMS0V | 58/110lines52.7% 29/92branches31.5% | 58/110lines52.7%+0 29/92branches31.5%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphRegionLowering.cppMS0V | 1416/1626lines87.1% 532/680branches78.2% | 1416/1626lines87.1%+0 532/680branches78.2%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.cppMS0V | 934/1072lines87.1% 299/432branches69.2% | 934/1072lines87.1%+0 299/432branches69.2%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.hMS0V | 4/4lines100.0% 4/4branches100.0% | 4/4lines100.0%+0 4/4branches100.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForToGraphPass.cppMS0V | 1033/1240lines83.3% 374/540branches69.3% | 1033/1240lines83.3%+0 374/540branches69.3%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForallToThreadPass.cppMS0V | 30/34lines88.2% 2/4branches50.0% | 30/34lines88.2%+0 2/4branches50.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphConstantsPass.cppMS0V | 80/83lines96.4% 18/24branches75.0% | 80/83lines96.4%+0 18/24branches75.0%+0 | |
…/lib/Frontend/Lowering/LowerGraphMemoryPass.cppMS0V | 525/841lines62.4% 208/400branches52.0% | 525/841lines62.4%+0 208/400branches52.0%+0 | Open PBT |
…/lib/Frontend/Lowering/Pipeline.cppMS0V | 18/21lines85.7% branchesnot measured | 18/21lines85.7%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Lowering/RankedMemRefLowering.cppMS0V | 60/133lines45.1% 27/94branches28.7% | 60/133lines45.1%+0 27/94branches28.7%+0 | Open PBT |
…/lib/Frontend/Raising/DeduplicateSCFWhileStatePass.cppMS0V | 13/135lines9.6% 0/60branches0.0% | 13/135lines9.6%+0 0/60branches0.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMArithToArithPass.cppMS0V | 300/319lines94.0% 94/116branches81.0% | 300/319lines94.0%+0 94/116branches81.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMCfToCfPass.cppMS0V | 77/80lines96.2% 8/8branches100.0% | 77/80lines96.2%+0 8/8branches100.0%+0 | Open PBT |
…/lib/Frontend/Raising/LiftCFToSCFPass.cppMS0V | 616/694lines88.8% 293/386branches75.9% | 616/694lines88.8%+0 293/386branches75.9%+0 | Open PBT |
…/lib/Frontend/Raising/MaterializeFMulAddPass.cppMS0V | 70/106lines66.0% 11/26branches42.3% | 70/106lines66.0%+0 11/26branches42.3%+0 | Open PBT |
…/lib/Frontend/Raising/NormalizeLiftedSCFExitPass.cppMS0V | 232/250lines92.8% 120/182branches65.9% | 232/250lines92.8%+0 120/182branches65.9%+0 | Open PBT |
…/lib/Frontend/Raising/Pipeline.cppMS0V | 10/19lines52.6% branchesnot measured | 10/19lines52.6%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/SCFForToForallPass.cppMS0V | 494/738lines66.9% 241/458branches52.6% | 494/738lines66.9%+0 241/458branches52.6%+0 | Open PBT |
…/lib/Frontend/Raising/SCFWhileToForPass.cppMS0V | 164/176lines93.2% 70/94branches74.5% | 164/176lines93.2%+0 70/94branches74.5%+0 | Open PBT |
…/loom/tools/loom-raise-opt/loom-raise-opt.cppMS0V | 12/12lines100.0% branchesnot measured | 12/12lines100.0%+0 branchesnot measured | Open PBT |
Review PR: Regression test from seed 109
Review PR: Regression test from seed 39
Review PR: Regression test from seed 76
The Structured Transfer Algebra defines graph-owned parallel composition only after the Structured Program Candidate has materialized its P[] ownership and schedule form in semantic SCF. That fixed-domain SCF is the transient input representation for mechanical lowering. It is recursively replicated into static lanes and removed; no parallel control op or schedule record survives in canonical graph IR.
llvm.func @imported_kernel(i64) dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 4 : index %kv = arith.constant 7 : index scf.parallel (%pi) = (%c0) to (%cw) step (%c1) { scf.parallel (%pj) = (%c0) to (%cw) step (%c1) { memref.store %kv, %tile[%pi, %pj] : memref<4x4xindex> scf.reduce } scf.reduce } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t0_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield } dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 4 : index %kv = arith.constant 7 : index scf.for %oi = %c0 to %limit step %c1 { scf.parallel (%lane) = (%c0) to (%cw) step (%c1) { %bcond = arith.cmpi slt, %lane, %cw : index scf.if %bcond { memref.store %kv, %target[%lane] : memref<8xindex> } scf.reduce } } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t1_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield }
dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 2 : index %kv = arith.constant 7 : index scf.for %oi = %c0 to %limit step %c1 { scf.parallel (%lane) = (%c0) to (%cw) step (%c1) { %bcond = arith.cmpi slt, %lane, %cw : index scf.if %bcond { memref.store %kv, %target[%lane] : memref<8xindex> } scf.reduce } } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t0_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield } dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 2 : index %kv = arith.constant 7 : index scf.parallel (%pi) = (%c0) to (%cw) step (%c1) { scf.parallel (%pj) = (%c0) to (%cw) step (%c1) { memref.store %kv, %tile[%pi, %pj] : memref<4x4xindex> scf.reduce } scf.reduce } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t1_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield }
The recursive lowering contract accepts arbitrary nesting of
scf.if, source-sequential scf.for, scf.while, and fixed-width
graph-owned scf.parallel or effect-form scf.forall. A graph-owned parallel
op must have a compile-time fixed domain, and all facts needed to establish
ownership, width, and cross-lane legality must be present in the current
Structured Program Candidate's semantic IR and resolved lowering config.
Input to graph extraction is an MLIR module containing module-scope
dataflow.thread definitions. Every selected SpatialCore candidate is already
materialized as a loom.spatial_region inside exactly one thread.
This section records Dataflow templates for SCF boundaries. Recursive lowering
applies the same transfer to scf.if, normalized scf.index_switch,
source-sequential scf.for, scf.while, and fixed-domain
effect-form scf.parallel / scf.forall.
Dynamic-width, resource-mapped, and result or reduction forms fail before any graph is mutated; the graph owner does not infer ownership, serialization, unrolling, or reduction order.
The Structured Transfer Algebra defines graph-owned parallel composition only after the Structured Program Candidate has materialized its P[] ownership and schedule form in semantic SCF. That fixed-domain SCF is the transient input representation for mechanical lowering.
Between Parts 2 and 3, SCF optimization and DSE produce the selected Structured Program Candidate. That domain owns all performance-distinct structured choices.
candidate.pg// Structured Program Candidate handoff modules for loom-lower-scf-to-dfg. // Module scope: optional llvm.func / func.func callables plus dataflow.thread // definitions; every spatial candidate is an explicit loom.spatial_region in // exactly one thread, holding fixed-domain graph-owned parallel SCF with // arbitrary nesting of scf.if / scf.for / scf.while. start: {new TCOUNT = random.randint(1, 2); new TI = 0; new PRELUDE = random.choice(['none', 'llvm', 'func'])} prelude threads; prelude: (PRELUDE == 'none') '' | (PRELUDE == 'llvm') 'llvm.func @imported_kernel(i64)\n\n' | (PRELUDE == 'func') 'func.func @native_helper(%arg0: index) -> index {\n return %arg0 : index\n}\n\n'; threads: (TI < TCOUNT) thread_def {TI += 1} threads | (TI == TCOUNT) ''; thread_def: {new RESIDENT = random.choice([0, 1]); new W = random.choice([1, 2, 4]); new PAR = random.choice([0, 1, 2]); new OUTER = random.choice([0, 1, 2]); new INNER = random.choice([0, 1, 2, 3])} 'dataflow.thread private @t' tname ' domain(#dataflow.thread_domain<dense>)(\n' ' %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>,\n' ' %n: index) ctrl (%ctrl: none) {\n' resident spatial_region ' dataflow.thread.yield\n}\n\n'; tname: [str(TI)]; // InstructionCore-resident thread body code outside the spatial boundary. resident: (RESIDENT == 0) '' | (RESIDENT == 1) ' %rzero = arith.constant 0 : index\n %rval = arith.constant 3 : index\n memref.store %rval, %scratch[%rzero] : memref<8xindex>\n'; spatial_region: ' "loom.spatial_region"(%n, %memory, %grid)\n' ' <{operandSegmentSizes = array<i32: 1, 0, 2, 0>,\n' ' resultSegmentSizes = array<i32: 0, 0>}> ({\n' ' ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>):\n' consts outer ' "loom.spatial_yield"()\n' ' <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n' ' }) {graph_name = "g_t' tname '_0", source_maps = []} :\n' ' (index, memref<8xindex>, memref<4x4xindex>) -> ()\n'; consts: ' %c0 = arith.constant 0 : index\n' ' %c1 = arith.constant 1 : index\n' ' %cw = arith.constant ' width ' : index\n' ' %kv = arith.constant 7 : index\n'; width: [str(W)]; // Optional sequential nesting around the graph-owned parallel op. outer: (OUTER == 0) par | (OUTER == 1) ' %ocond = arith.cmpi slt, %c0, %limit : index\n scf.if %ocond {\n' par ' }\n' | (OUTER == 2) ' scf.for %oi = %c0 to %limit step %c1 {\n' par ' }\n'; // Fixed-width graph-owned parallel composition: effect-form scf.forall or // fixed-domain scf.parallel with compile-time constant bounds. par: (PAR == 0) ' scf.forall (%lane) in (' width ') {\n' inner ' }\n' | (PAR == 1) ' scf.parallel (%lane) = (%c0) to (%cw) step (%c1) {\n' inner ' scf.reduce\n }\n' | (PAR == 2) ' scf.parallel (%pi) = (%c0) to (%cw) step (%c1) {\n scf.parallel (%pj) = (%c0) to (%cw) step (%c1) {\n memref.store %kv, %tile[%pi, %pj] : memref<4x4xindex>\n scf.reduce\n }\n scf.reduce\n }\n'; // Lane-disjoint body: arbitrary nesting of scf.if / scf.for / scf.while. inner: (INNER == 0) ' memref.store %kv, %target[%lane] : memref<8xindex>\n' | (INNER == 1) ' %bcond = arith.cmpi slt, %lane, %cw : index\n scf.if %bcond {\n memref.store %kv, %target[%lane] : memref<8xindex>\n }\n' | (INNER == 2) ' %bsum = scf.for %bi = %c0 to %limit step %c1 iter_args(%bacc = %lane) -> (index) {\n %bnext = arith.addi %bacc, %c1 : index\n scf.yield %bnext : index\n }\n memref.store %bsum, %target[%lane] : memref<8xindex>\n' | (INNER == 3) ' %wres = scf.while (%wi = %c0) : (index) -> index {\n %wc = arith.cmpi slt, %wi, %limit : index\n scf.condition(%wc) %wi : index\n } do {\n ^bb0(%wb: index):\n %wn = arith.addi %wb, %c1 : index\n scf.yield %wn : index\n }\n memref.store %wres, %target[%lane] : memref<8xindex>\n';
The Structured Transfer Algebra defines graph-owned parallel composition only after the Structured Program Candidate has materialized its P[] ownership and schedule form in semantic SCF. That fixed-domain SCF is the transient input representation for mechanical lowering.
candidate.spctpostcondition no_parallel_control_survives_in_graph_ir { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-dfg.md:L127-L132"; } constraints { let graphs = seq { g | g in output.operations where g.name == "dataflow.graph" }; forall g in graphs { assert no_parallel_control_op_survives: none op in mlir::descendants(g) where op.name == "scf.parallel" or op.name == "scf.forall" or op.name == "scf.forall.in_parallel" or op.name == "scf.reduce" or op.name == "scf.reduce.return" or op.name == "scf.parallel_insert_slice" or op.name == "dataflow.parallel" or op.name == "dataflow.reduce"; assert no_schedule_record_survives: none op in mlir::descendants(g) where "mapping" in op.attributes or "loom.parallel_schedule" in op.attributes or "loom.parallel_group" in op.attributes; assert graph_carries_no_schedule_record: not ("mapping" in g.attributes) and not ("loom.parallel_schedule" in g.attributes) and not ("loom.parallel_group" in g.attributes); } } }
llvm.func @imported_kernel(i64) dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 4 : index %kv = arith.constant 7 : index scf.parallel (%pi) = (%c0) to (%cw) step (%c1) { scf.parallel (%pj) = (%c0) to (%cw) step (%c1) { memref.store %kv, %tile[%pi, %pj] : memref<4x4xindex> scf.reduce } scf.reduce } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t0_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield } dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 4 : index %kv = arith.constant 7 : index scf.for %oi = %c0 to %limit step %c1 { scf.parallel (%lane) = (%c0) to (%cw) step (%c1) { %bcond = arith.cmpi slt, %lane, %cw : index scf.if %bcond { memref.store %kv, %target[%lane] : memref<8xindex> } scf.reduce } } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t1_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield }
20260911-082633started2026-09-11T08:26:34Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 2 : index %kv = arith.constant 7 : index scf.for %oi = %c0 to %limit step %c1 { scf.parallel (%lane) = (%c0) to (%cw) step (%c1) { %bcond = arith.cmpi slt, %lane, %cw : index scf.if %bcond { memref.store %kv, %target[%lane] : memref<8xindex> } scf.reduce } } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t0_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield } dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)( %scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>, %n: index) ctrl (%ctrl: none) { %rzero = arith.constant 0 : index %rval = arith.constant 3 : index memref.store %rval, %scratch[%rzero] : memref<8xindex> "loom.spatial_region"(%n, %memory, %grid) <{operandSegmentSizes = array<i32: 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>): %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %cw = arith.constant 2 : index %kv = arith.constant 7 : index scf.parallel (%pi) = (%c0) to (%cw) step (%c1) { scf.parallel (%pj) = (%c0) to (%cw) step (%c1) { memref.store %kv, %tile[%pi, %pj] : memref<4x4xindex> scf.reduce } scf.reduce } "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "g_t1_0", source_maps = []} : (index, memref<8xindex>, memref<4x4xindex>) -> () dataflow.thread.yield }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xindex>, memref<8xindex>, memref<4x4xindex>, index) -> (), sym_name = "t0", sym_visibility = "private"}> ({ ^bb0(%arg13: memref<8xindex>, %arg14: memref<8xindex>, %arg15: memref<4x4xindex>, %arg16: index, %arg17: none): %76 = "arith.constant"() <{value = 0 : index}> : () -> index %77 = "arith.constant"() <{value = 3 : index}> : () -> index "memref.store"(%77, %arg13, %76) : (index, memref<8xindex>, index) -> () %78 = "dataflow.graph.launch"(%arg17, %arg16, %arg14, %arg15) <{callee = @g_t0_0, operandSegmentSizes = array<i32: 1, 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<8xindex>, memref<4x4xindex>) -> none "dataflow.thread.yield"(%78) : (none) -> () }) : () -> () "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xindex>, memref<8xindex>, memref<4x4xindex>, index) -> (), sym_name = "t1", sym_visibility = "private"}> ({ ^bb0(%arg8: memref<8xindex>, %arg9: memref<8xindex>, %arg10: memref<4x4xindex>, %arg11: index, %arg12: none): %73 = "arith.constant"() <{value = 0 : index}> : () -> index %74 = "arith.constant"() <{value = 3 : index}> : () -> index "memref.store"(%74, %arg8, %73) : (index, memref<8xindex>, index) -> () %75 = "dataflow.graph.launch"(%arg12, %arg11, %arg9, %arg10) <{callee = @g_t1_0, operandSegmentSizes = array<i32: 1, 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<8xindex>, memref<4x4xindex>) -> none "dataflow.thread.yield"(%75) : (none) -> () }) : () -> () "dataflow.graph"() <{function_type = (index, memref<8xindex>, memref<4x4xindex>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_t0_0", sym_visibility = "private"}> ({ ^bb0(%arg4: none, %arg5: index, %arg6: memref<8xindex>, %arg7: memref<4x4xindex>): %20 = "dataflow.constant"(%arg4) <{const_value = 0 : index}> : (none) -> index %21 = "dataflow.constant"(%arg4) <{const_value = 1 : index}> : (none) -> index %22 = "dataflow.constant"(%arg4) <{const_value = 2 : index}> : (none) -> index %23 = "dataflow.constant"(%arg4) <{const_value = 7 : index}> : (none) -> index %24 = "arith.index_cast"(%20) : (index) -> i32 %25 = "arith.index_cast"(%arg5) : (index) -> i32 %26 = "arith.index_cast"(%21) : (index) -> i32 %27:2 = "dataflow.stream"(%24, %25, %26) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1) %28 = "dataflow.carry"(%27#1, %arg4, %64#0) : (i1, none, none) -> none %29:2 = "dataflow.demux"(%27#1, %28) : (i1, none) -> (none, none) %30 = "dataflow.invariant"(%27#1, %22) : (i1, index) -> index %31:2 = "dataflow.gate"(%27#1, %30) : (i1, index) -> (i1, index) %32:2 = "dataflow.demux"(%31#0, %31#1) : (i1, index) -> (index, index) %33 = "dataflow.invariant"(%27#1, %23) : (i1, index) -> index %34:2 = "dataflow.gate"(%27#1, %33) : (i1, index) -> (i1, index) %35:2 = "dataflow.demux"(%34#0, %34#1) : (i1, index) -> (index, index) %36 = "dataflow.invariant"(%27#1, %20) : (i1, index) -> index %37:2 = "dataflow.gate"(%27#1, %36) : (i1, index) -> (i1, index) %38:2 = "dataflow.demux"(%37#0, %37#1) : (i1, index) -> (index, index) %39 = "dataflow.invariant"(%27#1, %21) : (i1, index) -> index %40:2 = "dataflow.gate"(%27#1, %39) : (i1, index) -> (i1, index) %41:2 = "dataflow.demux"(%40#0, %40#1) : (i1, index) -> (index, index) %42 = "dataflow.carry"(%27#1, %arg4, %65#0) : (i1, none, none) -> none %43:2 = "dataflow.demux"(%27#1, %42) : (i1, none) -> (none, none) %44 = "dataflow.constant"(%29#1) <{const_value = 0 : index}> : (none) -> index %45 = "arith.cmpi"(%44, %31#1) <{predicate = 2 : i64}> : (index, index) -> i1 %46:2 = "dataflow.demux"(%45, %29#1) : (i1, none) -> (none, none) %47:2 = "dataflow.demux"(%45, %43#1) : (i1, none) -> (none, none) %48:2 = "dataflow.demux"(%45, %34#1) : (i1, index) -> (index, index) %49:2 = "dataflow.demux"(%45, %44) : (i1, index) -> (index, index) %50:2 = "dataflow.sync"(%46#1, %47#1) : (none, none) -> (none, none) %51 = "dataflow.store"(%arg6, %49#1, %48#1, %50#0) : (memref<8xindex>, index, index, none) -> none %52 = "dataflow.mux"(%45, %47#0, %51) : (i1, none, none) -> none %53 = "dataflow.mux"(%45, %46#0, %46#1) : (i1, none, none) -> none %54 = "dataflow.constant"(%29#1) <{const_value = 1 : index}> : (none) -> index %55 = "arith.cmpi"(%54, %31#1) <{predicate = 2 : i64}> : (index, index) -> i1 %56:2 = "dataflow.demux"(%55, %29#1) : (i1, none) -> (none, none) %57:2 = "dataflow.demux"(%55, %43#1) : (i1, none) -> (none, none) %58:2 = "dataflow.demux"(%55, %34#1) : (i1, index) -> (index, index) %59:2 = "dataflow.demux"(%55, %54) : (i1, index) -> (index, index) %60:2 = "dataflow.sync"(%56#1, %57#1) : (none, none) -> (none, none) %61 = "dataflow.store"(%arg6, %59#1, %58#1, %60#0) : (memref<8xindex>, index, index, none) -> none %62 = "dataflow.mux"(%55, %57#0, %61) : (i1, none, none) -> none %63 = "dataflow.mux"(%55, %56#0, %56#1) : (i1, none, none) -> none %64:2 = "dataflow.sync"(%53, %63) : (none, none) -> (none, none) %65:2 = "dataflow.sync"(%52, %62) : (none, none) -> (none, none) %66 = "arith.cmpi"(%24, %25) <{predicate = 2 : i64}> : (i32, i32) -> i1 %67:2 = "dataflow.demux"(%66, %29#0) : (i1, none) -> (none, none) %68:2 = "dataflow.sync"(%67#1, %32#0) : (none, index) -> (none, index) %69:2 = "dataflow.sync"(%68#0, %35#0) : (none, index) -> (none, index) %70:2 = "dataflow.sync"(%38#0, %41#0) : (index, index) -> (index, index) %71:2 = "dataflow.sync"(%69#0, %70#0) : (none, index) -> (none, index) %72 = "dataflow.mux"(%66, %67#0, %71#0) : (i1, none, none) -> none "dataflow.graph.return"(%72, %43#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> () }) : () -> () "dataflow.graph"() <{function_type = (index, memref<8xindex>, memref<4x4xindex>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_t1_0", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: index, %arg2: memref<8xindex>, %arg3: memref<4x4xindex>): %0 = "dataflow.constant"(%arg0) <{const_value = 7 : index}> : (none) -> index %1 = "dataflow.constant"(%arg0) <{const_value = 0 : index}> : (none) -> index %2 = "dataflow.constant"(%arg0) <{const_value = 1 : index}> : (none) -> index %3 = "dataflow.constant"(%arg0) <{const_value = 4 : index}> : (none) -> index %4 = "arith.muli"(%1, %3) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %5 = "arith.addi"(%4, %1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %6 = "dataflow.store"(%arg3, %5, %0, %arg0) : (memref<4x4xindex>, index, index, none) -> none %7 = "dataflow.constant"(%arg0) <{const_value = 4 : index}> : (none) -> index %8 = "arith.muli"(%1, %7) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %9 = "arith.addi"(%8, %2) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %10 = "dataflow.store"(%arg3, %9, %0, %arg0) : (memref<4x4xindex>, index, index, none) -> none %11 = "dataflow.constant"(%arg0) <{const_value = 4 : index}> : (none) -> index %12 = "arith.muli"(%2, %11) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %13 = "arith.addi"(%12, %1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %14 = "dataflow.store"(%arg3, %13, %0, %arg0) : (memref<4x4xindex>, index, index, none) -> none %15 = "dataflow.constant"(%arg0) <{const_value = 4 : index}> : (none) -> index %16 = "arith.muli"(%2, %15) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %17 = "arith.addi"(%16, %2) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index %18 = "dataflow.store"(%arg3, %17, %0, %arg0) : (memref<4x4xindex>, index, index, none) -> none %19:4 = "dataflow.sync"(%6, %10, %14, %18) : (none, none, none, none) -> (none, none, none, none) "dataflow.graph.return"(%19#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
partial source coverage: Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.
authoring-context.json{"entries":[{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"87-100","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"Between Parts 2 and 3, SCF optimization and DSE produce the selected\nStructured Program Candidate. That domain owns all performance-distinct\nstructured choices. Part 3 begins only after those choices and their typed\nownership carriers are explicit.\n\nInput to graph extraction is an MLIR module containing module-scope\n`dataflow.thread` definitions. Every selected SpatialCore candidate is already\nmaterialized as a `loom.spatial_region` inside exactly one thread. Other thread\nbody code remains InstructionCore-resident, including SCF-shaped code outside\nan explicit spatial boundary. Imported Host or InstructionCore code remains in\nits `llvm.func` envelope; genuinely standard-MLIR-native `func.func` callables\nmay coexist in the module. Either callable is ownership-neutral and does not\nauthorize graph creation through its signature, body shape, memory effects, or\nreturn convention.","why":"Normative handoff shape for Part 3 input: module-scope dataflow.thread definitions, each selected SpatialCore candidate already materialized as a loom.spatial_region in exactly one thread, InstructionCore-resident SCF outside the boundary, and ownership-neutral llvm.func / func.func callables. Drives the module skeleton, the resident-code alternative, and the prelude alternatives in candidate.pg."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"102-135","path":"docs/spec-compiler-part-3-dfg.md","roles":["applicability","context","input_construction"],"text":"Output is an initial Canonical Dataflow Program: module-level `llvm.func`\nsymbols for imported LLVM callables, any genuinely native `func.func` helpers,\nmodule-level\n`dataflow.thread` definitions reached by zero or more\n`dataflow.thread.launch` ops; and module-level `dataflow.graph`\ndefinitions reached by zero or more `dataflow.graph.launch` ops\ninside thread definitions. No `scf.*` op is left inside any\n`dataflow.graph` definition's body after successful graph-region lowering.\nThe recursive lowering contract accepts arbitrary nesting of\n`scf.if`, source-sequential `scf.for`, `scf.while`, and fixed-width\ngraph-owned `scf.parallel` or effect-form `scf.forall`. A graph-owned parallel\nop must have a compile-time fixed domain, and all facts needed to establish\nownership, width, and cross-lane legality must be present in the current\nStructured Program Candidate's semantic IR and resolved lowering config.\nThe lowerer re-proves those facts; lineage, cached analyses, and external\nprovenance cannot make an otherwise invalid candidate legal. Dynamic-width,\nresource-mapped, and result or reduction forms fail before any graph is\nmutated; the graph owner does not infer ownership, serialization, unrolling,\nor reduction order. The\n`dataflow.thread.launch` op carries the completion token and\nmapped-memory data transfer; the def remains a callable kernel\nbody, not a tensor-result returning op. Memory dependence\nconstruction runs in the recursive graph owner using basic graph-local alias\nroots and per-partition write/read frontiers (see\n`docs/spec-compiler-part-3-mem.md`).\nThe Structured Transfer Algebra defines graph-owned parallel composition only\nafter the Structured Program Candidate has materialized its P[] ownership and\nschedule form in semantic SCF. That fixed-domain SCF is the transient input\nrepresentation for mechanical lowering. It is recursively replicated into\nstatic lanes and removed; no parallel control op or schedule record survives\nin canonical graph IR.\nGraph candidate eligibility and atomic publication are governed by this\ndocument. TechMapping, SpatialMapping, and SystemMapping realization are\noutside this IR.","why":"Governing context of the sampled obligation: defines canonical graph IR (module-level dataflow.graph definitions launched from threads) that the postcondition selects, and states the accepted recursive lowering contract (arbitrary nesting of scf.if / scf.for / scf.while with fixed-width graph-owned scf.parallel or effect-form scf.forall) that the grammar samples."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"117-120","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_well_formedness"],"text":"provenance cannot make an otherwise invalid candidate legal. Dynamic-width,\nresource-mapped, and result or reduction forms fail before any graph is\nmutated; the graph owner does not infer ownership, serialization, unrolling,\nor reduction order. The","why":"Dynamic-width, resource-mapped, and result/reduction parallel forms fail before any graph is mutated; the grammar therefore only emits compile-time constant lane domains, effect-form scf.forall, and scf.parallel with an empty scf.reduce."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"1454-1461","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"This section records Dataflow templates for SCF boundaries. Recursive lowering\napplies the same transfer to `scf.if`, normalized `scf.index_switch`,\nsource-sequential `scf.for`, `scf.while`, and fixed-domain\neffect-form `scf.parallel` / `scf.forall`. A zero-case `scf.index_switch` is\nreplaced by its default region during structured normalization. Other\nunsupported source forms must be normalized by Part 2 before handoff of the\nselected Structured Program Candidate and are rejected if they remain in a\ngraph.","why":"Enumerates the SCF boundary forms the recursive transfer accepts inside a graph candidate and states that other source forms must have been normalized before handoff; bounds the nesting alternatives sampled by the grammar."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"2140-2171","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","input_construction"],"text":"For an accepted one-dimensional effect-form loop, `%N` denotes a\ncompile-time-resolved extent and the candidate has already selected\n`P[] = [%N]`:\n\n```mlir\nscf.parallel (%i) = (%c0) to (%N) step (%c1) {\n %x = memref.load %A[%i] : memref<?xf32>\n %y = arith.mulf %x, %x : f32\n memref.store %y, %B[%i] : memref<?xf32>\n scf.reduce\n}\n```\n\n`scf.parallel` is not a second Dataflow loop primitive. No\n`dataflow.parallel`, `dataflow.reduce`, reduction enum, schedule record, or\nparallel control op is introduced.\n\n#### Parallel Boundary Translation\n\nFor rank `r` and fixed widths `P[]`, the graph owner creates one static lane\nfor each logical coordinate tuple in the selected Cartesian domain. Each lane\nstarts from the same incoming execution and per-partition `(W, R)` frontier,\nsubstitutes its already selected source induction values, and recursively\nlowers the existing body. Incomparable exits are joined with fixed-arity\nall-of; an empty domain is an identity transfer. The Cartesian rank is not\nbounded by this lowering contract.\n\nLane enumeration is an implementation detail and never creates\ncross-iteration program order. A failed independence or ownership re-proof\ncauses atomic failure. No parallel boundary, coordinate tuple, `P[]` record,\ndependence summary, or traversal order survives into canonical graph IR.","why":"Terminology for the sampled obligation: the fixed-domain scf.parallel template for an already-selected P[], and the statement that no dataflow.parallel, dataflow.reduce, reduction enum, schedule record, or parallel control op is introduced and no parallel boundary or P[] record survives into canonical graph IR. Fixes what 'parallel control op' and 'schedule record' name in this IR."},{"file_sha256":"30c9c0c7b66af358b2cbdbeed35564e3c71f3e3dbcd88fa3a901229479c606b1","kind":"implementation","lines":"24-65","path":"include/Frontend/Lowering/Passes.h","roles":["applicability"],"text":"// transaction succeeds.\n//\n// Published graph symbols are deterministic, collision-free, and\n// construction-local. graph_name may supply a readability/debug stem; symbol\n// spelling is not ownership, graph identity, or artifact identity.\nstd::unique_ptr<::mlir::Pass> createLowerForToGraphPass();\n\n// Module-scope pass that expands SpatialCore-owned `memref.copy` inside\n// dataflow.graph bodies into a structured memref.load/memref.store element\n// loop. The graph-memory owner then derives the ordinary dataflow.load/store\n// pair and its ctrl/done network, so the canonical program keeps no bulk\n// transfer op. A copy outside the supported profile fails here, inside the\n// publication transaction.\nstd::unique_ptr<::mlir::Pass> createExpandGraphMemrefCopyPass();\n\n// Module-scope owner for graph-local memory and structured regions. It\n// normalizes supported scalar LLVM and memref accesses to dataflow.load/store,\n// computes basic graph-local alias-root partitions, and recursively lowers\n// scf.if/scf.for/scf.while while carrying execution, values, and independent\n// write/read frontiers. Raw parallel SCF fails before mutation.\nstd::unique_ptr<::mlir::Pass> createLowerGraphMemoryPass();\n\n// Module-scope pass that promotes each used `arith.constant` op inside a\n// dataflow.graph body into a `dataflow.constant` op driven by the body's\n// leading `thread_ctrl` block argument. Graph-local scalar literals therefore\n// remain visible to PnR as configurable hardware constants, including literals\n// feeding scalar arithmetic, structured loop bounds, or streaming primitives.\nstd::unique_ptr<::mlir::Pass> createLowerGraphConstantsPass();\n\n// Register the lowering passes with the global pass registry so\n// loom-raise-opt can drive them via --loom-lower-forall-to-thread /\n// --loom-lower-for-to-graph / --loom-expand-graph-memref-copy /\n// --loom-lower-graph-memory / --loom-lower-graph-constants plus the combined\n// --loom-lower-scf-to-dfg pipeline.\nvoid registerLoweringPasses();\n\n// Append the SCF-to-DFG lowering pipeline to the given pass manager:\n// loom-lower-for-to-graph (module-level)\n// The for-to-graph publisher internally owns canonicalization, graph\n// memref-copy expansion, graph memory/control lowering, constant promotion,\n// and native validation.\nvoid buildLoweringPipeline(::mlir::PassManager &pm);","why":"Identifies --loom-lower-scf-to-dfg as the combined SCF-to-DFG pipeline built from the module-level for-to-graph publisher (which internally owns canonicalization, graph memory/control lowering, constant promotion, and native validation). Evidence that the supplied stage flag is the one that publishes graphs and removes parallel SCF; no stage attribution mismatch."},{"file_sha256":"73f239de628bbf8d40145ecde732142ffcf6567c9483e6dc2286ae9176a6907c","kind":"language_definition","lines":"8-101","path":"include/Frontend/IR/LoomOps.td","roles":["input_construction","input_well_formedness"],"text":"def Loom_SpatialRegionOp : Loom_Op<\"spatial_region\", [\n IsolatedFromAbove,\n SingleBlock,\n AttrSizedOperandSegments,\n AttrSizedResultSegments,\n RecursiveMemoryEffects\n]> {\n let summary = \"Structured candidate for one SpatialCore graph\";\n let description = [{\n Holds one structured candidate inside a `dataflow.thread`. Operands are\n normalized as value inputs, stream input channels, memory inputs, and\n stream output channels. Results are normalized as value outputs followed\n by memory outputs. Each stream input has one affine `source_map`.\n\n This operation is temporary compiler IR. Successful publication replaces\n it with one native-valid `dataflow.graph` and its matching launch.\n }];\n\n let arguments = (ins\n Variadic<AnyType>:$valueInputs,\n Variadic<Dataflow_ChannelType>:$streamInputs,\n Variadic<AnyType>:$memoryInputs,\n Variadic<Dataflow_ChannelType>:$streamOutputs,\n AffineMapArrayAttr:$source_maps,\n OptionalAttr<StrAttr>:$graph_name);\n\n let results = (outs\n Variadic<AnyType>:$valueResults,\n Variadic<AnyType>:$memoryResults);\n\n let regions = (region AnyRegion:$body);\n\n let skipDefaultBuilders = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::ValueRange\":$valueInputs,\n \"::mlir::ValueRange\":$streamInputs,\n \"::mlir::ValueRange\":$memoryInputs,\n \"::mlir::ValueRange\":$streamOutputs,\n \"::mlir::TypeRange\":$valueResultTypes,\n \"::mlir::TypeRange\":$memoryResultTypes,\n \"::mlir::ArrayAttr\":$sourceMaps,\n CArg<\"::mlir::StringAttr\", \"{}\">:$graphName), [{\n $_state.addOperands(valueInputs);\n $_state.addOperands(streamInputs);\n $_state.addOperands(memoryInputs);\n $_state.addOperands(streamOutputs);\n $_state.addTypes(valueResultTypes);\n $_state.addTypes(memoryResultTypes);\n $_state.addAttribute(\"source_maps\", sourceMaps);\n if (graphName)\n $_state.addAttribute(\"graph_name\", graphName);\n auto &properties = $_state.getOrAddProperties<Properties>();\n properties.operandSegmentSizes = {\n static_cast<int32_t>(valueInputs.size()),\n static_cast<int32_t>(streamInputs.size()),\n static_cast<int32_t>(memoryInputs.size()),\n static_cast<int32_t>(streamOutputs.size())};\n properties.resultSegmentSizes = {\n static_cast<int32_t>(valueResultTypes.size()),\n static_cast<int32_t>(memoryResultTypes.size())};\n $_state.addRegion();\n }]>\n ];\n\n let hasVerifier = 1;\n}\n\ndef Loom_SpatialYieldOp : Loom_Op<\"spatial_yield\", [\n Terminator,\n ParentOneOf<[\"::loom::SpatialRegionOp\"]>,\n AttrSizedOperandSegments,\n Pure\n]> {\n let summary = \"Yield value and memory results from a spatial candidate\";\n\n let arguments = (ins\n Variadic<AnyType>:$values,\n Variadic<AnyType>:$memories);\n\n let skipDefaultBuilders = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::ValueRange\":$values,\n \"::mlir::ValueRange\":$memories), [{\n $_state.addOperands(values);\n $_state.addOperands(memories);\n auto &properties = $_state.getOrAddProperties<Properties>();\n properties.operandSegmentSizes = {\n static_cast<int32_t>(values.size()),\n static_cast<int32_t>(memories.size())};\n }]>\n ];","why":"Operand/result segmentation (valueInputs, streamInputs, memoryInputs, streamOutputs), source_maps and graph_name attributes of loom.spatial_region, and the loom.spatial_yield terminator; fixes the exact generic-form spelling the grammar emits for each spatial candidate."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"614-676","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def Dataflow_ThreadOp : Dataflow_Op<\"thread\", [\n AutomaticAllocationScope,\n IsolatedFromAbove,\n HasParent<\"::mlir::ModuleOp\">,\n SingleBlockImplicitTerminator<\"ThreadYieldOp\">,\n FunctionOpInterface,\n RecursiveMemoryEffects\n]> {\n let summary = \"Symbol-bearing function-like AccCore kernel definition\";\n let description = [{\n Module-scope, function-like callable that holds an AccCore kernel\n body. It does not itself execute; one or more\n `dataflow.thread.launch` ops materialize launches of it.\n\n The body's entry block has the layout\n `(args_*, thread_ctrl: none, iv_*: index)` (per spec section\n 5.4.1). The first N block args mirror `function_type.inputs`; the\n trailing `thread_ctrl` and grid index args are NOT in\n `function_type` (they are launch-instance extras). Specifically:\n\n * Args[0 .. N-1] match `function_type.inputs` position-wise.\n * Args[N] is `none` -- the per-launch `thread_ctrl`\n slot, used as the AccCore start signal and\n consumed by root `dataflow.graph.launch` ops\n in the body as a dependency event.\n * Args[N+1 .. end] are all `index` -- one per grid dim.\n\n The custom assembly format prints the required `domain(...)` immediately\n after the symbol and the trailing extras after the function-style\n signature using a separate `ctrl ( ... )` clause\n (the `thread_ctrl` slot) and an `iv ( ... )` clause (the\n grid-index slots). Either / both clauses are optional; threads\n written without them are accepted at parse time only when the op\n is external (i.e., body is empty), since a body-having thread\n must carry the trailing `thread_ctrl` slot per the verifier.\n\n The op is `IsolatedFromAbove`; values flow in only through the\n matching `dataflow.thread.launch` body operands.\n\n Every definition carries one closed `domain`: DenseRectangular or\n DynamicWork. Dense rank is derived solely from the trailing index block\n arguments. DynamicWork carries one ordinary function-input ordinal and has\n no coordinate suffix.\n }];\n\n let arguments = (ins\n SymbolNameAttr:$sym_name,\n TypeAttrOf<FunctionType>:$function_type,\n Dataflow_ThreadDomainAttr:$domain,\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 \"::dataflow::ThreadDomainAttr\":$domain,","why":"dataflow.thread definition: module-scope symbol, required domain attribute, and the entry-block layout (args_*, thread_ctrl: none, iv_*) printed with the ctrl(...) clause; fixes the thread header the grammar emits."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"839-860","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"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.","why":"dataflow.graph op definition; fixes the operation name used to select canonical graph definitions in the postcondition."},{"file_sha256":"320a66521bba7346cf97dce9b11dce757385efbfbe7c36cc03f44198965edb4b","kind":"verifier","lines":"125-165","path":"lib/Frontend/Lowering/GraphParallelLowering.cpp","roles":["input_well_formedness"],"text":"return std::nullopt;\n result.push_back(*constant);\n }\n return result;\n}\n\nstd::optional<FixedParallelDomain>\ngetFixedParallelDomain(::mlir::scf::ForallOp forall) {\n auto lower = getConstantIndices(forall.getMixedLowerBound());\n auto upper = getConstantIndices(forall.getMixedUpperBound());\n auto step = getConstantIndices(forall.getMixedStep());\n if (!lower || !upper || !step)\n return std::nullopt;\n return FixedParallelDomain{std::move(*lower), std::move(*upper),\n std::move(*step)};\n}\n\nstd::optional<FixedParallelDomain>\ngetFixedParallelDomain(::mlir::scf::ParallelOp parallel) {\n FixedParallelDomain domain;\n for (::mlir::Value value : parallel.getLowerBound()) {\n auto constant = getConstantIndex(value);\n if (!constant)\n return std::nullopt;\n domain.lower.push_back(*constant);\n }\n for (::mlir::Value value : parallel.getUpperBound()) {\n auto constant = getConstantIndex(value);\n if (!constant)\n return std::nullopt;\n domain.upper.push_back(*constant);\n }\n for (::mlir::Value value : parallel.getStep()) {\n auto constant = getConstantIndex(value);\n if (!constant)\n return std::nullopt;\n domain.step.push_back(*constant);\n }\n return domain;\n}","why":"getFixedParallelDomain for scf.forall and scf.parallel requires constant lower/upper/step; establishes that the generated lane domains must be arith.constant-backed for the candidate to be accepted rather than rejected before mutation."},{"file_sha256":"320a66521bba7346cf97dce9b11dce757385efbfbe7c36cc03f44198965edb4b","kind":"verifier","lines":"1359-1425","path":"lib/Frontend/Lowering/GraphParallelLowering.cpp","roles":["input_well_formedness","context"],"text":"::mlir::LogicalResult\ncheckParallelPreconditions(::llvm::ArrayRef<::mlir::Operation *> parallelOps,\n bool requireFixedDomain, bool selectedOwnership) {\n if (parallelOps.empty())\n return ::mlir::success();\n\n ::llvm::DenseMap<::mlir::Operation *, ParallelCheckInfo> checks;\n ::llvm::DenseSet<::mlir::Operation *> provenParallelOps;\n for (::mlir::Operation *op : parallelOps) {\n if (op->hasAttr(\"loom.parallel_group\") ||\n op->hasAttr(\"loom.parallel_schedule\"))\n return op->emitError(\n \"loom-lower-graph-memory: parallel SCF carries unsupported author \"\n \"metadata\");\n\n if (auto mapping = op->getAttrOfType<::mlir::ArrayAttr>(\"mapping\");\n mapping && !mapping.empty())\n return op->emitError(\n \"loom-lower-graph-memory: graph-owned parallel SCF must not retain \"\n \"an execution-resource mapping\");\n\n if (auto forall = ::llvm::dyn_cast<::mlir::scf::ForallOp>(op)) {\n auto inParallel = forall.getTerminator();\n if (!forall.getOutputs().empty() || forall.getNumResults() != 0 ||\n inParallel.getRegion().empty() ||\n !inParallel.getRegion().front().empty())\n return forall.emitError(\n \"loom-lower-graph-memory: graph-owned scf.forall must be in \"\n \"effect form before fixed-lane lowering\");\n } else {\n auto parallel = ::mlir::cast<::mlir::scf::ParallelOp>(op);\n auto reduce = ::mlir::cast<::mlir::scf::ReduceOp>(\n parallel.getBody()->getTerminator());\n if (!parallel.getInitVals().empty() || parallel.getNumResults() != 0 ||\n !reduce.getOperands().empty() || !reduce.getReductions().empty())\n return parallel.emitError(\n \"loom-lower-graph-memory: graph-owned scf.parallel reductions \"\n \"must be normalized before fixed-lane lowering\");\n }\n\n std::optional<FixedParallelDomain> domain;\n if (auto forall = ::llvm::dyn_cast<::mlir::scf::ForallOp>(op))\n domain = getFixedParallelDomain(forall);\n else if (auto parallel = ::llvm::dyn_cast<::mlir::scf::ParallelOp>(op))\n domain = getFixedParallelDomain(parallel);\n if (requireFixedDomain && !domain)\n return op->emitError(\n \"loom-lower-graph-memory: selected graph-owned parallel SCF \"\n \"requires a fixed compile-time lane domain\");\n if (domain &&\n ::llvm::any_of(domain->step, [](int64_t step) { return step <= 0; }))\n return op->emitError(\n \"loom-lower-graph-memory: selected graph-owned parallel SCF \"\n \"requires positive fixed lane steps\");\n\n bool graphOwned =\n static_cast<bool>(op->getParentOfType<::dataflow::GraphOp>());\n checks.try_emplace(op, ParallelCheckInfo{op,\n std::move(domain),\n selectedOwnership || graphOwned ||\n hasSpatialCarrierAncestor(op),\n {},\n nullptr});\n provenParallelOps.insert(op);\n }\n\n ::mlir::Operation *root = parallelOps.front();","why":"checkParallelPreconditions rejects parallel SCF carrying loom.parallel_group / loom.parallel_schedule author metadata or a non-empty mapping array, and requires effect-form scf.forall and reduction-free scf.parallel. Fixes both the accepted input spelling and the concrete attribute names that a surviving schedule record would use."},{"file_sha256":"dcb708e61fd42fa8e3f9a37ef7669b0fbd5b19123b648d5d66dd735b763e018d","kind":"test","lines":"18-41","path":"test/raise/scf-to-dfg-graph-owned-parallel-recurrence.mlir","roles":["input_construction"],"text":"// CHECK-NOT: scf.\n// CHECK: dataflow.graph.return\n\ndataflow.thread private @parallel_recurrence domain(#dataflow.thread_domain<dense>)(\n %n: index, %memory: memref<?xindex>) ctrl (%ctrl: none) {\n \"loom.spatial_region\"(%n, %memory)\n <{operandSegmentSizes = array<i32: 1, 0, 1, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0(%limit: index, %target: memref<?xindex>):\n %zero = arith.constant 0 : index\n %one = arith.constant 1 : index\n scf.forall (%lane) in (2) {\n %sum = scf.for %i = %zero to %limit step %one\n iter_args(%state = %lane) -> (index) {\n %next = arith.addi %state, %i : index\n scf.yield %next : index\n }\n memref.store %sum, %target[%lane] : memref<?xindex>\n }\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"g_parallel_recurrence_0\", source_maps = []} :\n (index, memref<?xindex>) -> ()\n dataflow.thread.yield","why":"Accepted spelling of a dataflow.thread holding a loom.spatial_region whose body is a fixed-width scf.forall with nested scf.for; models the grammar's thread/region/parallel nesting."},{"file_sha256":"c25a72ad99349973a47f2a1e081b6b269920e25cc5f59f74619c2e7ce0c2b65d","kind":"test","lines":"36-52","path":"test/raise/scf-to-dfg-explicit-spatial-ownership.mlir","roles":["input_construction"],"text":"dataflow.thread.yield\n}\n\ndataflow.thread private @selected_spatial domain(#dataflow.thread_domain<dense>)(\n %target: memref<1xi32>, %value: i32) ctrl (%ctrl: none) {\n \"loom.spatial_region\"(%value, %target)\n <{operandSegmentSizes = array<i32: 1, 0, 1, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0(%payload: i32, %memory: memref<1xi32>):\n %zero = arith.constant 0 : index\n memref.store %payload, %memory[%zero] : memref<1xi32>\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"selected_graph\", source_maps = []} :\n (i32, memref<1xi32>) -> ()\n dataflow.thread.yield\n}","why":"Accepted generic-form spelling of loom.spatial_region with operandSegmentSizes / resultSegmentSizes, graph_name and source_maps, plus loom.spatial_yield and dataflow.thread.yield; copied structurally by the grammar."},{"file_sha256":"91580d3883ebdf55b76d5adca6caa06d3e823f9e0b5114dfd795e16c185c3ec1","kind":"test","lines":"12-30,78-100","path":"test/raise/scf-to-dfg-memory-frontier-parallel.mlir","roles":["input_construction","input_well_formedness"],"text":"dataflow.graph private @repeat_parallel(\n %start: none, %limit: index, %memory: memref<?xi32>) -> ()\n attributes {input_segments = array<i32: 1, 0, 1>,\n result_segments = array<i32: 0, 0, 0>} {\n %c0 = arith.constant 0 : index\n %c1 = arith.constant 1 : index\n %c2 = arith.constant 2 : index\n scf.for %outer = %c0 to %limit step %c1 {\n scf.parallel (%lane) = (%c0) to (%c2) step (%c1) {\n %index = arith.addi %outer, %lane : index\n %value = memref.load %memory[%index] : memref<?xi32>\n scf.reduce\n }\n }\n dataflow.graph.return %start : none\n}\n\n// Branch-local parallel joins must precede the outer selected frontier.\n// CHECK-LABEL: dataflow.graph private @select_parallel(\n// dimensions. Descendant lane coordinates remain independent during an\n// ancestor proof.\n// CHECK-LABEL: dataflow.graph private @nested_parallel_matrix(\n// CHECK-COUNT-4: dataflow.store\n// CHECK-NOT: scf.\n// CHECK: dataflow.graph.return\ndataflow.graph private @nested_parallel_matrix(\n %start: none, %memory: memref<2x2xi32>) -> ()\n attributes {input_segments = array<i32: 0, 0, 1>,\n result_segments = array<i32: 0, 0, 0>} {\n %c0 = arith.constant 0 : index\n %c1 = arith.constant 1 : index\n %c2 = arith.constant 2 : index\n %value = arith.constant 7 : i32\n scf.parallel (%i) = (%c0) to (%c2) step (%c1) {\n scf.parallel (%j) = (%c0) to (%c2) step (%c1) {\n memref.store %value, %memory[%i, %j] : memref<2x2xi32>\n scf.reduce\n }\n scf.reduce\n }\n dataflow.graph.return %start : none\n}","why":"Accepted fixed-domain scf.parallel spelling with a trailing scf.reduce, a parallel nested inside a sequential scf.for, and a lane-disjoint nested parallel-in-parallel form; guides the lane-indexed stores that keep the generated candidates legal."},{"file_sha256":"a30ba020ae6f3ea80191d996f787ba463974694f0e0032b5323072e7538cb5d7","kind":"test","lines":"1-10","path":"test/raise/scf-to-dfg-pipeline.mlir","roles":["applicability"],"text":"// RUN: loom-raise-opt --loom-lower-scf-to-dfg %s | FileCheck %s\n\n// The production pipeline does not infer thread ownership for an unmapped\n// host forall. It publishes only explicit loom.spatial_region operations\n// already nested in dataflow.thread definitions.\n\n// CHECK-LABEL: func.func @vecadd_like\n// CHECK: scf.forall\n// CHECK-NOT: dataflow.thread.launch @t_vecadd_like_0\n// CHECK-NOT: dataflow.thread.launch @t_vecadd_like_red","why":"Shows loom-raise-opt --loom-lower-scf-to-dfg driven over a module and that graphs are published only from explicit loom.spatial_region ops already nested in dataflow.thread definitions; confirms the subject invocation and why the grammar never relies on unmapped host SCF."}],"primary_bundle_sha256":"7ad676ea93f5d6cedff5da948eb05a79108b48381eb246e9b66a9b57fa0f9959","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"880fa4fba504a817a777dd5c5d5ae12f06777550dbe8062388b85c65f96675d6"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 67526,
"duration_ms": 67576,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1236,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5037,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.18843000000000001,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 5522,
"provider": "firstParty",
"thinkingTokens": 1611,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module body consisting of an optional top-level callable declaration/definition followed by one or more `dataflow.thread` symbol definitions, with no other top-level entities.\n2. Each `dataflow.thread` is declared `private`, carries a symbol name of the form `@t<index>`, and is annotated with `domain(#dataflow.thread_domain<dense>)`.\n3. Each thread's entry signature is fixed to exactly four data block arguments \u2014 `%scratch: memref<8xindex>`, `%memory: memref<8xindex>`, `%grid: memref<4x4xindex>`, `%n: index` \u2014 plus a separate control argument `ctrl (%ctrl: none)`.\n4. Each thread body is terminated by `dataflow.thread.yield` with no operands.\n5. Each thread body contains exactly one `loom.spatial_region`; spatial regions are never nested, never absent from a thread, and never appear more than once per thread.\n6. The `loom.spatial_region` is always written in generic (quoted) operation form with an explicit inherent-attribute dictionary rather than any custom assembly syntax.\n7. The spatial region op takes exactly three operands \u2014 the `index` value `%n`, the `memref<8xindex>` value `%memory`, and the `memref<4x4xindex>` value `%grid` \u2014 and produces no results, as declared by its function type `(index, memref<8xindex>, memref<4x4xindex>) -> ()`.\n8. The operand grouping is declared by `operandSegmentSizes = array<i32: 1, 0, 2, 0>` and the (empty) result grouping by `resultSegmentSizes = array<i32: 0, 0>`, and these segment sizes are consistent with the actual operand and result lists.\n9. The spatial region carries exactly one region with exactly one block `^bb0`, whose three arguments `%limit: index`, `%target: memref<8xindex>`, `%tile: memref<4x4xindex>` correspond positionally and type-wise to the three operands.\n10. Values defined outside the spatial region (`%scratch`, `%memory`, `%grid`, `%n`) are never referenced inside the region body; all uses inside the region go through the block arguments `%limit`, `%target`, `%tile`.\n11. The region is terminated by `\"loom.spatial_yield\"()` in generic form with `operandSegmentSizes = array<i32: 0, 0>` and type `() -> ()`, yielding no values, consistent with the region-holding op having no results.\n12. The spatial region op carries a `graph_name` string attribute and a `source_maps` attribute; `graph_name` is derived from the owning thread's index so that distinct regions in the module carry distinct graph names.\n13. All index constants used inside the region (`%c0`, `%c1`, `%cw`, `%kv`) are defined by `arith.constant ... : index` operations at the top of the region block, before any control-flow construct that uses them.\n14. Every emitted program satisfies SSA dominance: each value is defined textually before use and within a region that dominates the use, including loop induction variables, iteration arguments, and `while` \"do\"-block arguments.\n15. Inside the spatial region, exactly one graph-owned parallel operation is present on every path: either an `scf.forall` or an `scf.parallel` (possibly a `scf.parallel` immediately nested in another `scf.parallel`).\n16. The parallel operation's iteration domain is fixed at compile time: `scf.forall` uses a literal integer upper bound, and `scf.parallel` uses constant lower bound `%c0`, constant upper bound `%cw`, and constant step `%c1`, so no parallel bound depends on a runtime value such as `%limit`.\n17. Parallel operations are always one-dimensional per op (a single induction variable in each `scf.parallel`/`scf.forall` header); multi-dimensional parallelism is expressed only by nesting two one-dimensional `scf.parallel` ops.\n18. Every `scf.parallel` region is terminated by `scf.reduce` with no reduction operands, and every `scf.parallel` produces no results; `scf.forall` bodies carry no `shared_outs`, no mapping attribute, and rely on the implicit terminator.\n19. Memory writes performed by the parallel body are lane-disjoint: stores into `%target: memref<8xindex>` are always indexed by the parallel induction variable `%lane`, and stores into `%tile: memref<4x4xindex>` are always indexed by the pair of induction variables `(%pi, %pj)` of the enclosing nested parallel loops.\n20. No load operations, no cross-lane data movement, and no reduction or accumulation across lanes occur inside the parallel region; the only memory effects there are stores.\n21. Sequential control flow that encloses the parallel op (`scf.if` / `scf.for`) is value-free: the `scf.if` has no results and no `else` region, and the `scf.for` has no `iter_args` and no results, so no implicit `scf.yield` operands are required.\n22. Sequential control flow inside the parallel body may carry values: `scf.for` with `iter_args` yields exactly one `index` value per iteration via `scf.yield`, and `scf.while` carries a single `index` loop-carried value with `scf.condition(%cond) %v : index` in the \"before\" region and `scf.yield` of a single `index` in the \"after\" region, with matching `(index) -> index` typing.\n23. All predicates used by `scf.if` and `scf.while` are `i1` values produced by `arith.cmpi slt` on `index` operands.\n24. Runtime-dependent trip counts appear only in sequential constructs, where the bound is the region block argument `%limit`.\n25. Code placed in the thread body outside the spatial region is self-contained: it defines its own constants and only touches `%scratch`, never values defined inside the region.\n26. All memref accesses are type-consistent with the declared shapes `memref<8xindex>` (one index) and `memref<4x4xindex>` (two indices), and all stored values are of type `index`.\n27. The optional top-level callable, when present, is a well-formed declaration or definition (`llvm.func` declaration with no body, or `func.func` with a body terminated by `return` of a matching type) and is never called from any thread; threads contain no call operations at all.\n28. The `%ctrl: none` control argument is declared but never used in any emitted body.\n\n## Sampling conventions\n\n1. The module contains either one or two `dataflow.thread` definitions; zero threads and three or more threads are never emitted.\n2. Thread symbols are named by a counter starting at zero, yielding `@t0` and, when a second thread exists, `@t1`.\n3. The top-level preamble is one of exactly three forms: nothing, the fixed declaration `llvm.func @imported_kernel(i64)`, or the fixed definition `func.func @native_helper(%arg0: index) -> index` whose body is `return %arg0 : index`; no other callable signatures, dialects, or multiple preamble entities are emitted.\n4. The preamble choice is made once for the whole module rather than per thread, and the preamble is always separated from the threads by a blank line.\n5. Thread entry argument names and types are a fixed skeleton (`%scratch`, `%memory`, `%grid`, `%n`, `%ctrl`), with memref shapes hard-coded to `8xindex` and `4x4xindex`; sizes are never varied and no other argument counts or element types occur.\n6. The thread domain attribute is always `#dataflow.thread_domain<dense>`; no other domain kind is emitted.\n7. Pre-region resident code is either omitted entirely or is one fixed three-line block defining `%rzero = arith.constant 0 : index`, `%rval = arith.constant 3 : index`, and a single `memref.store %rval, %scratch[%rzero]`; no other resident code shapes, lengths, or targets occur.\n8. The in-region constant preamble is always the same four constants in the same order: `%c0 = 0`, `%c1 = 1`, `%cw = <width>`, `%kv = 7`.\n9. The parallel width constant `%cw` (and the `scf.forall` literal bound) is drawn from exactly `{1, 2, 4}`; other widths, non-power-of-two widths, and widths larger than the `memref<8xindex>` extent are never emitted, and the same width is reused for both `%cw` and any `scf.forall` bound within a thread.\n10. The stored payload constant is always `7` and the resident payload constant is always `3`.\n11. The `graph_name` attribute always follows the scheme `\"g_t<thread index>_0\"`, with a trailing `_0` suffix implying at most one region per thread; `source_maps` is always the empty list `[]`.\n12. Sequential nesting around the parallel op is limited to three alternatives: no wrapper, exactly one `scf.if` guarded by `%ocond = arith.cmpi slt, %c0, %limit`, or exactly one `scf.for %oi = %c0 to %limit step %c1`; wrappers are never stacked, never use `else`, and `scf.while` is never used at this outer level.\n13. The wrapper induction variable `%oi` and the wrapper predicate `%ocond` are defined but never used inside the parallel body.\n14. The graph-owned parallel form is one of exactly three shapes: a single `scf.forall` with a literal bound, a single `scf.parallel` with constant bounds, or two perfectly nested `scf.parallel` ops; deeper nests, `scf.forall` with `scf.parallel` mixing, and reduction-carrying parallel ops are never emitted.\n15. In the two-level nested `scf.parallel` shape, the body is a fixed single `memref.store %kv, %tile[%pi, %pj]`, and the separately chosen inner-body shape is not emitted at all in that case.\n16. The inner (lane-disjoint) body is one of exactly four fixed shapes: a bare store, a store guarded by `scf.if` on `arith.cmpi slt, %lane, %cw`, an `scf.for` with one `index` `iter_args` accumulator initialized to `%lane` and incremented by `%c1` whose result is stored, or an `scf.while` counting `%wi` from `%c0` while `slt %limit`, incrementing by `%c1`, whose result is stored.\n17. Each inner control-flow shape is at most one level deep; `if`/`for`/`while` are never combined or nested within one another inside the parallel body.\n18. All SSA value names are fixed mnemonics (`%c0`, `%c1`, `%cw`, `%kv`, `%lane`, `%pi`, `%pj`, `%oi`, `%ocond`, `%bcond`, `%bi`, `%bacc`, `%bnext`, `%bsum`, `%wi`, `%wc`, `%wb`, `%wn`, `%wres`, `%rzero`, `%rval`), reused identically across threads since each thread is a separate symbol scope.\n19. The four per-thread shape decisions (resident code presence, width, parallel form, outer wrapper, inner body) are made independently for each thread, so two threads in one module may differ in every dimension.\n20. Comparison predicates are always `slt`, arithmetic is always `arith.addi` by `%c1`, and no other `arith` opcodes or predicates appear.\n21. Formatting is a fixed skeleton: two-space indentation for thread-body lines, six spaces inside the spatial region block, eight spaces for the parallel op, ten spaces for its body, and one blank line after the preamble and after each thread definition.",
"result_index": 0,
"session_id": "509d9c70-6d24-46c8-8a35-b6fffe88c920",
"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": 49,
"total_cost_usd": 0.18843000000000001,
"ttft_ms": 21221,
"ttft_stream_ms": 945,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5037,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5037,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 5522,
"output_tokens_details": {
"thinking_tokens": 1611
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "048acb9f-0e14-484e-ac33-94dede7f3d03"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 14776,
"duration_ms": 14806,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 2119,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5559,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.081125,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 1021,
"provider": "firstParty",
"thinkingTokens": 373,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition quantifies universally over `graphs`, the sequence of every operation in the output program whose name is exactly `\"dataflow.graph\"`, gathered from `output.operations` and therefore including graphs at any nesting depth; the input program is never consulted, so nothing relates output to input. For each such graph it makes three negative assertions and no existence claim, so a graph satisfies it only by lacking the listed constructs. The first assertion rejects the graph if any strict descendant operation has a name exactly matching one of eight literals \u2014 `scf.parallel`, `scf.forall`, `scf.forall.in_parallel`, `scf.reduce`, `scf.reduce.return`, `scf.parallel_insert_slice`, `dataflow.parallel`, or `dataflow.reduce`; any other name, including other `scf.*` operations, is accepted, and the graph operation itself is not tested against this list because `mlir::descendants` excludes its argument. The second assertion rejects the graph if any strict descendant has an entry keyed `\"mapping\"`, `\"loom.parallel_schedule\"`, or `\"loom.parallel_group\"` in its attributes-and-properties map; only key presence is tested, and the attribute values, kinds, and texts are never read. The third assertion applies the same three key-presence tests to the graph operation itself, rejecting it if any of the three keys is present. The only value sources are operation names compared to string literals and attribute-key membership tests, both of which are total; no typed projections, operands, results, regions, types, or symbol resolutions are used, so no evaluation errors can arise. Behavior is vacuously accepting whenever the output contains no `dataflow.graph` operation, and the two `none` assertions are additionally vacuously true for a graph with no descendant operations, in which case only the third assertion carries force. Operations bearing the listed names or the listed attribute keys elsewhere in the module, outside every `dataflow.graph`, are accepted without comment.",
"result_index": 0,
"session_id": "94652efc-3c8d-4db7-b2bf-79f77eaccd4f",
"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": 30,
"total_cost_usd": 0.081125,
"ttft_ms": 6842,
"ttft_stream_ms": 1591,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5559,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5559,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 1021,
"output_tokens_details": {
"thinking_tokens": 373
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "1573a491-3972-4cb1-928c-32a35fc2930e"
}
]
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.