MS0V6 mlir-stage-07-v1 passing 5000/5000
Estimated confidence: 99.7%. Conservative lower bound: 86.3% (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 |
|---|
| derived from the coverage profile | not measured | not measured | no drafts yet |
The target Part 3 dataflow surface uses module-scope, Symbol-bearing,
function-like definitions for both dataflow.thread and
dataflow.graph. Execution is materialized only by
dataflow.thread.launch and dataflow.graph.launch. Graph control
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<1xi32>, i32, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg0: memref<1xi32>, %arg1: i32, %arg2: i1, %arg3: none): "loom.spatial_region"() <{graph_name = "graph_0", operandSegmentSizes = array<i32: 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0>, source_maps = []}> ({ "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) : () -> () "dataflow.thread.yield"() : () -> () }) : () -> () }) : () -> ()
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<1xi32>, i32, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg1: memref<1xi32>, %arg2: i32, %arg3: i1, %arg4: none): %0 = "dataflow.graph.launch"(%arg4) <{callee = @graph_0, operandSegmentSizes = array<i32: 1, 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none) -> none "dataflow.thread.yield"(%0) : (none) -> () }) : () -> () "dataflow.graph"() <{function_type = () -> (), input_segments = array<i32: 0, 0, 0>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_0", sym_visibility = "private"}> ({ ^bb0(%arg0: none): "dataflow.graph.return"(%arg0) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
module { dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%target: memref<1xi32>, %value: i32, %enabled: i1) ctrl (%ctrl: none) { %c_zero = arith.constant 0 : index %c_one = arith.constant 1 : index %c_trip = arith.constant 4 : index scf.for %iv = %c_zero to %c_trip step %c_one { "loom.spatial_region"(%value, %target) <{operandSegmentSizes = array<i32: 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%payload: i32, %memory: memref<1xi32>): %zero = arith.constant 0 : index memref.store %payload, %memory[%zero] : memref<1xi32> "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "graph_0", source_maps = []} : (i32, memref<1xi32>) -> () } dataflow.thread.yield } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%target: memref<1xi32>, %value: i32, %enabled: i1) ctrl (%ctrl: none) { %c_zero = arith.constant 0 : index %c_one = arith.constant 1 : index %c_trip = arith.constant 4 : index scf.for %iv = %c_zero to %c_trip step %c_one { scf.if %enabled { %region_out = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb0(%payload: i32): %doubled = arith.addi %payload, %payload : i32 "loom.spatial_yield"(%doubled) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_1", source_maps = []} : (i32) -> i32 } } dataflow.thread.yield } }
One binding denotes one ordered dynamic event sequence. A fixed structured scope may contain multiple sequential or structured mutually exclusive sites.
Branches may have unequal or empty site sets, and a later branch selector may depend on an earlier input event. Enclosing loops repeatedly activate the same schedule, so one or several static body sites may each fire dynamically.
Current publication supports nested scf.if completion
propagation.
An llvm.call or func.call inside a
dataflow.thread definition's body is an InstructionCore call. If the callee
contains code that must become a dataflow.graph definition, Part 3 must
inline or specialize that callee into the active thread definition
before graph extraction.
loom.spatial_region is the temporary publication boundary inside an
existing dataflow.thread. Its operands are normalized as value inputs,
stream input channels, memory inputs, and stream output channels; its
results are value outputs followed by memory outputs.
Part 3 consumes each explicit
loom.spatial_region inside its owning dataflow.thread and publishes the
corresponding graph definition and launch only after complete conversion and
native finalization succeed.
loom.spatial_region is temporary compiler IR inside a
dataflow.thread. It owns one structured graph candidate with normalized
value, stream-channel, and memory boundary segments.
Endpoint
sites nested under scf.parallel or scf.forall have no inferred
traversal order and fail before publication. Unselected or non-fixed
graph-owned parallel forms also fail closed.
loom.spatial_region is a transparent structured boundary. A blocking
receive inside that region cannot be justified by a send that follows the
region in the same stored-program strand merely because the published graph
launch becomes asynchronous.
candidate.pg// Inputs for the Part 3 publication stage (loom-lower-for-to-graph). // A module holds one or more module-scope `dataflow.thread` definitions, each // owning exactly one explicit `loom.spatial_region` publication boundary with // normalized value / stream / memory operand segments and a `graph_name`. // Region sites appear directly in the thread body, inside a fixed `scf.for` // schedule, or inside a nested `scf.if` branch site (nested completion // propagation is supported). `scf.parallel` / `scf.forall` sites are not // sampled. An optional host `func.func` container carries a plain loop that // owns no spatial region. start: {new NTHREAD = random.randint(1, 3); new I = 0; new HOST = random.choice([0, 1])} 'module {\n' host_part thread_list '}\n'; host_part: (HOST == 1) host_func | (HOST == 0) ''; host_func: 'func.func @host_container(%target: memref<4xi32>, %value: i32) {\n' ' %hz = arith.constant 0 : index\n' ' %hf = arith.constant 4 : index\n' ' %ho = arith.constant 1 : index\n' ' scf.for %hi = %hz to %hf step %ho {\n' ' memref.store %value, %target[%hi] : memref<4xi32>\n' ' }\n' ' return\n' '}\n\n'; thread_list: (I < NTHREAD) thread {I += 1} thread_list | (I == NTHREAD) ''; tag: [str(I)]; thread: {new SHAPE = random.choice([0, 1, 2]); new KIND = random.choice([0, 1, 2])} 'dataflow.thread private @thread_' tag ' domain(#dataflow.thread_domain<dense>)(%target: memref<1xi32>, %value: i32, %enabled: i1)\n' ' ctrl (%ctrl: none) {\n' body ' dataflow.thread.yield\n' '}\n\n'; body: (SHAPE == 0) region_op | (SHAPE == 1) for_open region_op for_close | (SHAPE == 2) for_open if_open region_op if_close for_close; for_open: ' %c_zero = arith.constant 0 : index\n' ' %c_one = arith.constant 1 : index\n' ' %c_trip = arith.constant 4 : index\n' ' scf.for %iv = %c_zero to %c_trip step %c_one {\n'; for_close: ' }\n'; if_open: ' scf.if %enabled {\n'; if_close: ' }\n'; region_op: (KIND == 0) region_empty | (KIND == 1) region_store | (KIND == 2) region_value; region_empty: ' "loom.spatial_region"()\n' ' <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n' ' resultSegmentSizes = array<i32: 0, 0>}> ({\n' ' ^bb0:\n' ' "loom.spatial_yield"()\n' ' <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n' ' }) {graph_name = "graph_' tag '", source_maps = []} : () -> ()\n'; region_store: ' "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 = "graph_' tag '", source_maps = []} : (i32, memref<1xi32>) -> ()\n'; region_value: ' %region_out = "loom.spatial_region"(%value)\n' ' <{operandSegmentSizes = array<i32: 1, 0, 0, 0>,\n' ' resultSegmentSizes = array<i32: 1, 0>}> ({\n' ' ^bb0(%payload: i32):\n' ' %doubled = arith.addi %payload, %payload : i32\n' ' "loom.spatial_yield"(%doubled)\n' ' <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n' ' }) {graph_name = "graph_' tag '", source_maps = []} : (i32) -> i32\n';
The target Part 3 dataflow surface uses module-scope, Symbol-bearing, function-like definitions for both
dataflow.threadanddataflow.graph. Execution is materialized only bydataflow.thread.launchanddataflow.graph.launch.
candidate.spctpostcondition part3_definitions_are_module_scope_and_launch_only { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-dfg.md:L14-L17"; } constraints { let definitions = seq { op | op in output.operations where op.name == "dataflow.thread" or op.name == "dataflow.graph" }; let symbol_users = seq { op | op in output.operations where "callee" in op.attributes }; forall d in definitions { assert module_scope_definition: d.parent_operation matches some($p) and p.name == "builtin.module"; assert symbol_bearing_definition: "sym_name" in d.attributes; assert function_like_definition: "function_type" in d.attributes and d.attributes["function_type"].type.kind == "function"; } forall u in symbol_users { assert execution_materialized_only_by_launch: none t in mlir::resolve_symbol_reference(output, u, "callee") where (t.name == "dataflow.thread" and u.name != "dataflow.thread.launch") or (t.name == "dataflow.graph" and u.name != "dataflow.graph.launch"); } } }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<1xi32>, i32, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg0: memref<1xi32>, %arg1: i32, %arg2: i1, %arg3: none): "loom.spatial_region"() <{graph_name = "graph_0", operandSegmentSizes = array<i32: 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0>, source_maps = []}> ({ "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) : () -> () "dataflow.thread.yield"() : () -> () }) : () -> () }) : () -> ()
20260911-082025started2026-09-11T08:20:26Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
module { dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%target: memref<1xi32>, %value: i32, %enabled: i1) ctrl (%ctrl: none) { %c_zero = arith.constant 0 : index %c_one = arith.constant 1 : index %c_trip = arith.constant 4 : index scf.for %iv = %c_zero to %c_trip step %c_one { "loom.spatial_region"(%value, %target) <{operandSegmentSizes = array<i32: 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb0(%payload: i32, %memory: memref<1xi32>): %zero = arith.constant 0 : index memref.store %payload, %memory[%zero] : memref<1xi32> "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "graph_0", source_maps = []} : (i32, memref<1xi32>) -> () } dataflow.thread.yield } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%target: memref<1xi32>, %value: i32, %enabled: i1) ctrl (%ctrl: none) { %c_zero = arith.constant 0 : index %c_one = arith.constant 1 : index %c_trip = arith.constant 4 : index scf.for %iv = %c_zero to %c_trip step %c_one { scf.if %enabled { %region_out = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb0(%payload: i32): %doubled = arith.addi %payload, %payload : i32 "loom.spatial_yield"(%doubled) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_1", source_maps = []} : (i32) -> i32 } } dataflow.thread.yield } }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<1xi32>, i32, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg11: memref<1xi32>, %arg12: i32, %arg13: i1, %arg14: none): %10 = "arith.constant"() <{value = 0 : index}> : () -> index %11 = "arith.constant"() <{value = 1 : index}> : () -> index %12 = "arith.constant"() <{value = 4 : index}> : () -> index %13 = "scf.for"(%10, %12, %11, %arg14) ({ ^bb0(%arg15: index, %arg16: none): %14 = "dataflow.graph.launch"(%arg16, %arg12, %arg11) <{callee = @graph_0, operandSegmentSizes = array<i32: 1, 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, i32, memref<1xi32>) -> none "scf.yield"(%14) : (none) -> () }) : (index, index, index, none) -> none "dataflow.thread.yield"(%13) : (none) -> () }) : () -> () "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<1xi32>, i32, i1) -> (), sym_name = "thread_1", sym_visibility = "private"}> ({ ^bb0(%arg5: memref<1xi32>, %arg6: i32, %arg7: i1, %arg8: none): %4 = "arith.constant"() <{value = 0 : index}> : () -> index %5 = "arith.constant"() <{value = 1 : index}> : () -> index %6 = "arith.constant"() <{value = 4 : index}> : () -> index %7 = "scf.for"(%4, %6, %5, %arg8) ({ ^bb0(%arg9: index, %arg10: none): %8 = "scf.if"(%arg7) ({ %9:2 = "dataflow.graph.launch"(%arg10, %arg6) <{callee = @graph_1, operandSegmentSizes = array<i32: 1, 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0, 1>, source_maps = []}> : (none, i32) -> (i32, none) "scf.yield"(%9#1) : (none) -> () }, { "scf.yield"(%arg10) : (none) -> () }) : (i1) -> none "scf.yield"(%8) : (none) -> () }) : (index, index, index, none) -> none "dataflow.thread.yield"(%7) : (none) -> () }) : () -> () "dataflow.graph"() <{arg_attrs = [{}, {llvm.noalias}], function_type = (i32, memref<1xi32>) -> (), input_segments = array<i32: 1, 0, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_0", sym_visibility = "private"}> ({ ^bb0(%arg2: none, %arg3: i32, %arg4: memref<1xi32>): %2 = "dataflow.constant"(%arg2) <{const_value = 0 : index}> : (none) -> index %3 = "dataflow.store"(%arg4, %2, %arg3, %arg2) : (memref<1xi32>, index, i32, none) -> none "dataflow.graph.return"(%3) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () "dataflow.graph"() <{function_type = (i32) -> i32, input_segments = array<i32: 1, 0, 0>, result_segments = array<i32: 1, 0, 0>, sym_name = "graph_1", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: i32): %0 = "arith.addi"(%arg1, %arg1) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %1:2 = "dataflow.sync"(%arg0, %0) : (none, i32) -> (none, i32) "dataflow.graph.return"(%1#1, %1#0) <{operandSegmentSizes = array<i32: 1, 0, 0, 1>}> : (i32, 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":"14-32","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","applicability"],"text":"The target Part 3 dataflow surface uses module-scope, Symbol-bearing,\nfunction-like definitions for both `dataflow.thread` and\n`dataflow.graph`. Execution is materialized only by\n`dataflow.thread.launch` and `dataflow.graph.launch`. Graph control\nports are explicit in the current graph ABI: `ctrl_in` and launch-facing\n`done_out` are invocation protocol endpoints represented at every launch\nsite, not application payload slots in the `dataflow.graph` function type.\nThe graph body does not return `done_out`; its structural\n`dataflow.graph.return.complete` frontier is the unique authority from which\nthe launch result is derived. Part 3 consumes each explicit\n`loom.spatial_region` inside its owning `dataflow.thread` and publishes the\ncorresponding graph definition and launch only after complete conversion and\nnative finalization succeed.\nThe precise timing semantics of `dataflow.stream`, `dataflow.carry`,\n`dataflow.invariant`, and `dataflow.gate` are specified separately in\n`docs/spec-dataflow-part-1-streaming.md`. The precise firing semantics\nof `dataflow.constant`, `dataflow.sync`, `dataflow.mux`, and\n`dataflow.demux` are specified separately in\n`docs/spec-dataflow-part-2-control.md`.","why":"Governing context of the sampled obligation: module-scope, Symbol-bearing, function-like dataflow.thread and dataflow.graph definitions, launch-only execution, and the fact that Part 3 consumes each explicit loom.spatial_region inside its owning dataflow.thread. Fixes which outputs the claim governs and which stage must run."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"462-465","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"* `loom.spatial_region` is temporary compiler IR inside a\n `dataflow.thread`. It owns one structured graph candidate with normalized\n value, stream-channel, and memory boundary segments. It never appears in a\n finalized Canonical Dataflow Program.","why":"loom.spatial_region is temporary IR inside a dataflow.thread owning one structured graph candidate with normalized value, stream-channel, and memory boundary segments; determines the sampled input construct and its placement."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"499-506","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_well_formedness"],"text":"`llvm.func` or `func.func` definitions. An `llvm.call` or `func.call` inside a\n`dataflow.thread` definition's body is an InstructionCore call. If the callee\ncontains code that must become a `dataflow.graph` definition, Part 3 must\ninline or specialize that callee into the active thread definition\nbefore graph extraction. A `dataflow.thread.launch` is invalid\ntransitively inside every thread or graph definition. Non-inlined\nInstructionCore calls may remain only when their callee body is graph-free\nafter this preparation.","why":"InstructionCore call rules: a dataflow.thread.launch is invalid transitively inside a thread or graph definition and graph-bearing callees must be inlined; justifies sampling self-contained thread bodies with no calls and no nested launches."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"564-574","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"6. `loom.spatial_region` is the temporary publication boundary inside an\n existing `dataflow.thread`. Its operands are normalized as value inputs,\n stream input channels, memory inputs, and stream output channels; its\n results are value outputs followed by memory outputs. Each stream input\n has one affine `source_map` from the consumer thread domain to the producer\n thread domain. The lowering collects all explicit candidates before\n attempting publication, performs conversion and native validation on a\n scratch module, and replaces the live module only on success. A public pass\n failure therefore leaves temporary candidates and never exposes a partial\n canonical graph. Current publication supports nested `scf.if` completion\n propagation. Stream channel segments become payload-typed graph stream","why":"Normalized operand segmentation (value inputs, stream inputs, memory inputs, stream outputs; value then memory results) and affine source_map requirement for stream inputs, plus the statement that nested scf.if completion propagation is supported. Drives the sampled operandSegmentSizes/resultSegmentSizes shapes, the empty source_maps for stream-free candidates, and the scf.for/scf.if nesting choices."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"578-582,591-601","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"enter the canonical graph body. One binding denotes one ordered dynamic\n event sequence. A fixed structured scope may contain multiple sequential\n or structured mutually exclusive sites. Lowering emits one fixed ordinal\n schedule, filters inactive branch sites, demuxes each input from the\n filtered ordinal, and muxes outputs back into that same dynamic order.\n Branches may have unequal or empty site sets, and a later branch selector\n may depend on an earlier input event. Enclosing loops repeatedly activate\n the same schedule, so one or several static body sites may each fire\n dynamically. Across repeated thread launches, each endpoint binding and\n logical point concatenates these per-instance sequences in deterministic\n launch issue order. Channel delivery pairs the resulting producer and\n consumer sequences by message ordinal after applying `source_map`; it does\n not pair thread activations or create activation-owned segments. Endpoint\n sites nested under `scf.parallel` or `scf.forall` have no inferred\n traversal order and fail before publication. Unselected or non-fixed\n graph-owned parallel forms also fail closed.","why":"Fixed ordinal schedule, sequential and mutually exclusive sites inside a structured scope, enclosing loops repeatedly activating the schedule, and the closure that endpoint sites under scf.parallel or scf.forall fail before publication. Motivates sampling fixed scf.for and nested scf.if site placement and excluding scf.parallel/scf.forall endpoint sites."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"1413-1419","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_well_formedness"],"text":"* `loom.spatial_region` is a transparent structured boundary. A blocking\n receive inside that region cannot be justified by a send that follows the\n region in the same stored-program strand merely because the published graph\n launch becomes asynchronous. Such a transformation would turn an\n inline-semantics deadlock into progress. A resulting retirement/send cycle\n therefore identifies a deadlocking or incorrectly cut candidate; lowering\n must not remove a wait by inventing a same-activation channel witness.","why":"A blocking receive inside the region that would need a post-region send is a deadlocking/incorrectly cut candidate; justifies sampling only channel-free region bodies so that no seed is an intentionally rejected candidate."},{"file_sha256":"73f239de628bbf8d40145ecde732142ffcf6567c9483e6dc2286ae9176a6907c","kind":"language_definition","lines":"8-103","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 ];\n\n let hasVerifier = 1;\n}","why":"ODS for loom.spatial_region and loom.spatial_yield: operand/result ordering, AttrSizedOperandSegments/AttrSizedResultSegments properties, source_maps and graph_name attributes, single-block isolated body. Fixes the exact generic-form spelling emitted by the grammar."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"614-678","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,\n CArg<\"::llvm::ArrayRef<::mlir::NamedAttribute>\", \"{}\">:$attrs)>\n ];","why":"ODS and assembly description for dataflow.thread: HasParent ModuleOp, sym_name/function_type/domain attributes, and the (args_*, thread_ctrl: none, iv_*) entry-block layout with the required ctrl clause for a body-having thread. Fixes the sampled thread header and also the concrete attribute names read by the postcondition."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"verifier","lines":"839-922","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.\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}","why":"dataflow.graph ODS and verifyBody: module-scope parent, sym_name and function_type attributes on the published definition; confirms the attribute spelling used to test Symbol-bearing, function-like, module-scope definitions in the output."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"767-820,973-1008","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"text":"def Dataflow_ThreadLaunchOp : Dataflow_Op<\"thread.launch\", [\n AttrSizedOperandSegments,\n DeclareOpInterfaceMethods<SymbolUserOpInterface>\n]> {\n let summary = \"Async launch of a dataflow.thread callable\";\n let description = [{\n References a `dataflow.thread` definition by symbol and supplies\n body operands and optional grid upper bounds. Always produces one\n `!dataflow.thread_token` completion handle for all dynamic launch\n instances.\n\n Grid lower bounds and steps are not modeled; body operands, upper bounds,\n and async dependencies are explicit.\n }];\n\n let arguments = (ins\n FlatSymbolRefAttr:$callee,\n Variadic<AnyType>:$bodyOperands,\n Variadic<Index>:$gridUpperBounds,\n Variadic<Dataflow_ThreadTokenType>:$asyncDependencies);\n\n let results = (outs Dataflow_ThreadTokenType:$asyncToken);\n\n let assemblyFormat = [{\n $callee\n `(` $bodyOperands `)`\n ( `grid` `(` $gridUpperBounds^ `)` )?\n ( `wait` `(` $asyncDependencies^ `)` )?\n attr-dict `:`\n functional-type($bodyOperands, results)\n }];\n\n let skipDefaultBuilders = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::FlatSymbolRefAttr\":$callee,\n \"::mlir::ValueRange\":$bodyOperands,\n \"::mlir::ValueRange\":$gridUpperBounds,\n \"::mlir::ValueRange\":$asyncDependencies), [{\n $_state.addOperands(bodyOperands);\n $_state.addOperands(gridUpperBounds);\n $_state.addOperands(asyncDependencies);\n auto &properties = $_state.getOrAddProperties<Properties>();\n properties.operandSegmentSizes = {\n static_cast<int32_t>(bodyOperands.size()),\n static_cast<int32_t>(gridUpperBounds.size()),\n static_cast<int32_t>(asyncDependencies.size())};\n properties.callee = callee;\n $_state.addTypes(::dataflow::ThreadTokenType::get($_builder.getContext()));\n }]>\n ];\n\n let hasVerifier = 1;\n}\ndef Dataflow_GraphLaunchOp : Dataflow_Op<\"graph.launch\", [\n AttrSizedOperandSegments,\n AttrSizedResultSegments,\n DeclareOpInterfaceMethods<SymbolUserOpInterface>\n]> {\n let summary = \"Asynchronous launch of a dataflow.graph callable\";\n let description = [{\n References a `dataflow.graph` definition by symbol from inside a\n `dataflow.thread` body. Dependencies, value inputs, stream input channel\n bindings, memory imports, and stream output channel bindings are explicit\n operand segments. Each stream input binding carries one affine\n `source_map` from the enclosing consumer thread domain to its producer\n domain. Value outputs and memory exports are SSA results; the trailing\n `done` result is the graph retirement event.\n\n The operation resolves its callee through `SymbolUserOpInterface` but does\n not project callee effects through `MemoryEffectsOpInterface`.\n }];\n\n let arguments = (ins\n FlatSymbolRefAttr:$callee,\n AffineMapArrayAttr:$source_maps,\n Variadic<NoneType>:$dependencies,\n Variadic<AnyType>:$valueInputs,\n Variadic<Dataflow_ChannelType>:$streamInputs,\n Variadic<AnyType>:$memoryInputs,\n Variadic<Dataflow_ChannelType>:$streamOutputs);\n\n let results = (outs\n Variadic<AnyType>:$valueResults,\n Variadic<AnyType>:$memoryResults,\n NoneType:$done);\n\n let hasCustomAssemblyFormat = 1;\n let hasVerifier = 1;\n}","why":"dataflow.thread.launch and dataflow.graph.launch carry a FlatSymbolRefAttr callee resolved through SymbolUserOpInterface; establishes that symbol users of a thread or graph definition are identified by the callee attribute, which the postcondition uses to test launch-only execution."},{"file_sha256":"c25a72ad99349973a47f2a1e081b6b269920e25cc5f59f74619c2e7ce0c2b65d","kind":"test","lines":"22-52","path":"test/raise/scf-to-dfg-explicit-spatial-ownership.mlir","roles":["input_construction"],"text":"func.func @host_container(%target: memref<4xi32>, %value: i32) {\n %zero = arith.constant 0 : index\n %four = arith.constant 4 : index\n %one = arith.constant 1 : index\n scf.for %index = %zero to %four step %one {\n memref.store %value, %target[%index] : memref<4xi32>\n }\n return\n}\n\ndataflow.thread private @instruction_only domain(#dataflow.thread_domain<dense>)(\n %target: memref<1xi32>, %value: i32) ctrl (%ctrl: none) {\n %zero = arith.constant 0 : index\n memref.store %value, %target[%zero] : memref<1xi32>\n 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 concrete spelling of a module holding a host func.func plus dataflow.thread definitions with an explicit loom.spatial_region (memory + value operand segments, graph_name, empty source_maps) under --loom-lower-for-to-graph."},{"file_sha256":"df76d22d1149cf2929b700df6f97b58d27b64d523346cfbb4dbf9ba8e66baa49","kind":"test","lines":"60-152","path":"test/raise/scf-to-dfg-nested-completion.mlir","roles":["input_construction"],"text":"//--- supported.mlir\nmodule {\n dataflow.thread private @for_completion domain(#dataflow.thread_domain<dense>)(%limit: index, %enabled: i1)\n ctrl (%start: none) {\n %c0 = arith.constant 0 : index\n %c1 = arith.constant 1 : index\n scf.for %i = %c0 to %limit step %c1 {\n scf.if %enabled {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"for_graph\", source_maps = []} : () -> ()\n }\n }\n dataflow.thread.yield\n }\n\n dataflow.thread private @while_completion domain(#dataflow.thread_domain<dense>)(%continue: i1)\n ctrl (%start: none) {\n scf.while : () -> () {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"while_before_graph\", source_maps = []} : () -> ()\n scf.condition(%continue)\n } do {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"while_after_graph\", source_maps = []} : () -> ()\n scf.yield\n }\n dataflow.thread.yield\n }\n\n dataflow.thread private @switch_completion domain(#dataflow.thread_domain<dense>)(%selector: index)\n ctrl (%start: none) {\n scf.index_switch %selector\n case 7 {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"switch_graph\", source_maps = []} : () -> ()\n scf.yield\n }\n default {\n scf.yield\n }\n dataflow.thread.yield\n }\n\n dataflow.thread private @parallel_completion domain(#dataflow.thread_domain<dense>)() ctrl (%start: none) {\n %c0 = arith.constant 0 : index\n %c1 = arith.constant 1 : index\n %c2 = arith.constant 2 : index\n scf.parallel (%i) = (%c0) to (%c2) step (%c1) {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"parallel_graph\", source_maps = []} : () -> ()\n scf.reduce\n }\n dataflow.thread.yield\n }\n\n dataflow.thread private @forall_completion domain(#dataflow.thread_domain<dense>)() ctrl (%start: none) {\n scf.forall (%i) in (2) {\n \"loom.spatial_region\"()\n <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0:\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"forall_graph\", source_maps = []} : () -> ()\n }\n dataflow.thread.yield\n }\n}","why":"Accepted spellings of spatial-region sites nested inside scf.for and scf.if within a dataflow.thread body, including the empty-segment region form; used for the loop/branch site shapes sampled by the grammar."}],"primary_bundle_sha256":"0523bfa5e1bae819d54eed855903f63b0474238d82999c3e8e1a6fe2b0f637a2","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"d4ccd27b494b510a15c7e6a9d70a66ff6a9d47ed221e33ead426beccbaebbc0e"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 36323,
"duration_ms": 36385,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1526,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 4712,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.11732999999999999,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 2808,
"provider": "firstParty",
"thinkingTokens": 189,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single top-level `module { ... }` whose body contains only the optional host `func.func` and one or more `dataflow.thread` definitions.\n2. Every program contains at least one `dataflow.thread` definition at module scope.\n3. Every `dataflow.thread` is declared `private`, carries a symbol name, a `domain(#dataflow.thread_domain<dense>)` clause, the operand list `(%target: memref<1xi32>, %value: i32, %enabled: i1)`, and a `ctrl (%ctrl: none)` clause.\n4. Every thread body is terminated by exactly one `dataflow.thread.yield`.\n5. Every thread body contains exactly one `\"loom.spatial_region\"` operation; no thread has zero regions and none has two or more.\n6. Every `\"loom.spatial_region\"` is written in generic (quoted) form with an inherent-attribute dictionary `<{operandSegmentSizes = array<i32: ...>, resultSegmentSizes = array<i32: ...>}>` present, i.e. operand and result segmentation is always explicit and normalized.\n7. `operandSegmentSizes` on a region always has exactly four entries (a four-way value / stream / memory / fourth operand partition) and `resultSegmentSizes` always has exactly two entries.\n8. The declared segment sizes always sum to, and agree in order with, the actual operand list and result list of the region operation and with its trailing function type.\n9. Every region has exactly one entry block `^bb0` whose block-argument list matches, in order and in type, the region's operands (no arguments when there are no operands).\n10. Every region body ends with a `\"loom.spatial_yield\"` in generic form carrying its own two-entry `operandSegmentSizes`, and the yield's operand count/type matches the region's result count/type.\n11. Every `\"loom.spatial_region\"` carries a discardable attribute dictionary containing both `graph_name` (a string) and `source_maps = []`.\n12. Values consumed by a region are values already in scope in the enclosing thread: the payload operand is the thread's `%value : i32` and the memory operand is the thread's `%target : memref<1xi32>`.\n13. Values defined inside a region body (`%payload`, `%memory`, `%zero`, `%doubled`) are used only within that region body and never escape it except through the `loom.spatial_yield`.\n14. When a region occurs inside control flow, it is nested in structured control flow only: an `scf.for` loop, or an `scf.if` nested inside an `scf.for`; the region is never placed under `scf.parallel` or `scf.forall`.\n15. Every `scf.for` enclosing a region has index-typed lower bound, upper bound and step operands defined by `arith.constant ... : index` operations that dominate the loop.\n16. Every `scf.if` enclosing a region is predicated on an `i1` value in scope \u2014 the thread's `%enabled` argument \u2014 and has a `then` region only (no `else` region).\n17. `scf.if` and `scf.for` bodies containing a region carry no explicit yielded results, consistent with the region being the sole payload of the branch/loop body.\n18. When a region produces a result, that result is bound to an SSA name inside the enclosing thread/loop/branch scope and is not further consumed.\n19. The optional host container, when present, is a module-scope `func.func` with an explicit `return`, whose loop is a plain `scf.for` containing only a `memref.store`; a host function never contains a `loom.spatial_region`.\n20. All memref accesses are in-bounds and type-consistent: stores into `memref<1xi32>` use index `0`, and host stores into `memref<4xi32>` use the loop induction variable of a loop running over `[0, 4)`.\n21. Symbol names of threads are distinct within the module, and each thread's `graph_name` is distinct across threads.\n\n## Sampling conventions\n\n1. The number of threads per module is drawn from 1 to 3 inclusive; larger modules are never emitted.\n2. The host `func.func` is either present exactly once, immediately after `module {` and before all threads, or entirely absent; it is never emitted more than once and never placed after a thread.\n3. The host function has the fixed signature `@host_container(%target: memref<4xi32>, %value: i32)`, fixed constants `0`, `4`, `1` named `%hz`, `%hf`, `%ho`, and a fixed single-store loop body over induction variable `%hi`.\n4. Threads are named by a monotonically increasing zero-based counter, `@thread_0`, `@thread_1`, \u2026, and the corresponding region is tagged `graph_name = \"graph_<same index>\"`, so symbol and graph name always share their numeric suffix.\n5. Each thread independently samples one of exactly three body shapes: the region directly in the thread body, the region inside one `scf.for`, or the region inside an `scf.if` inside one `scf.for`; loop nesting deeper than one `scf.for` plus one `scf.if` is never emitted.\n6. Each thread independently samples one of exactly three region flavors: a no-operand/no-result region, a two-operand store region, or a one-operand/one-result value region; no other operand/result combination is emitted.\n7. Shape and flavor are chosen independently per thread, so all nine combinations are reachable and the same module may mix them.\n8. The generated `scf.for` schedule is always the fixed trip range `0` to `4` step `1`, with constants named `%c_zero`, `%c_one`, `%c_trip` and induction variable `%iv`; the induction variable is never used inside the region.\n9. The `scf.if` site always uses the thread's `%enabled` operand as its condition rather than a freshly computed predicate.\n10. The empty-region flavor fixes `operandSegmentSizes = array<i32: 0, 0, 0, 0>`, `resultSegmentSizes = array<i32: 0, 0>`, type `() -> ()`, and an argument-less `^bb0`.\n11. The store flavor fixes `operandSegmentSizes = array<i32: 1, 0, 1, 0>` (one value operand, no stream operands, one memory operand), `resultSegmentSizes = array<i32: 0, 0>`, type `(i32, memref<1xi32>) -> ()`, and a body of exactly one `arith.constant 0 : index` plus one `memref.store`.\n12. The value flavor fixes `operandSegmentSizes = array<i32: 1, 0, 0, 0>`, `resultSegmentSizes = array<i32: 1, 0>`, type `(i32) -> i32`, and a body of exactly one `arith.addi %payload, %payload` feeding the yield; no other arithmetic op is ever generated.\n13. Region operands are always drawn from the thread's own block arguments in the fixed order `(%value)` or `(%value, %target)`; the `%ctrl` and `%enabled` arguments are never passed into a region.\n14. Internal SSA names are fixed strings (`%payload`, `%memory`, `%zero`, `%doubled`, `%region_out`) and are reused verbatim across threads rather than uniquified.\n15. `source_maps` is always the empty list; no populated source-map attribute is ever emitted.\n16. The stream operand segment of every region is always zero and the second result segment is always zero, so stream-typed publication operands and secondary results are never exercised.\n17. All memref types are fixed to `memref<1xi32>` inside threads and `memref<4xi32>` in the host; element types are always `i32`.\n18. Indentation, blank-line separation between threads, and the trailing newline after the closing `}` of the module are fixed formatting choices.\n19. No thread declares results, attributes beyond those shown, or additional operations before or after its region site other than the constants required by the sampled loop shape.",
"result_index": 0,
"session_id": "d9ca1176-fac6-4baf-a6b5-edf9424a7577",
"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": 62,
"total_cost_usd": 0.11732999999999999,
"ttft_ms": 4706,
"ttft_stream_ms": 950,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 4712,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 4712,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 2808,
"output_tokens_details": {
"thinking_tokens": 189
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "2fe74871-e776-439c-8abf-275e525dda96"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 15810,
"duration_ms": 15834,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 2084,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5522,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.083455,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 1129,
"provider": "firstParty",
"thinkingTokens": 379,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition quantifies universally over two independently selected sets of operations drawn from `output.operations`, so it inspects the subject's output program at every nesting depth and never consults `input`. The first selection, `definitions`, is every operation whose name is exactly `\"dataflow.thread\"` or `\"dataflow.graph\"`; the second, `symbol_users`, is every operation that carries an attribute or property keyed `\"callee\"`, regardless of that attribute's kind or the operation's name or dialect. For each member of `definitions` it accepts only operations that have a parent operation whose name is `\"builtin.module\"` (a root module with no parent fails the match, and a definition nested inside anything else fails), that have a key `\"sym_name\"` present in their attribute map, and that have a key `\"function_type\"` present whose attribute projects to a type with `kind == \"function\"`; a `\"function_type\"` attribute that is not type-valued produces an evaluation error rather than a clean rejection. For each member of `symbol_users` it resolves the `\"callee\"` attribute against the output program and rejects the program if any resolved target operation is named `\"dataflow.thread\"` while the using operation is not named `\"dataflow.thread.launch\"`, or is named `\"dataflow.graph\"` while the user is not named `\"dataflow.graph.launch\"`; resolved targets with any other name are unconstrained, and users are otherwise free to be any operation. The only value sources are operation names, the `parent_operation` option, attribute-key presence, the `function_type` attribute's type kind, and the result sequence of `mlir::resolve_symbol_reference` over the same output program \u2014 no operands, results, regions, blocks, types of values, segments, or counts are read. Both `forall` blocks are vacuously satisfied when their selections are empty: an output with no `dataflow.thread` or `dataflow.graph` operations imposes no structural requirements, and an output with no `\"callee\"`-bearing operations imposes no launch requirement. The launch assertion is also vacuously true for any user whose `\"callee\"` resolves to an empty sequence of targets, since `none` over an empty sequence holds. Non-vacuous behavior therefore requires at least one thread or graph operation present, or at least one `\"callee\"` user that resolves to at least one thread or graph definition.",
"result_index": 0,
"session_id": "778724d9-41a1-45ea-ad04-1db8268673ef",
"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": 24,
"total_cost_usd": 0.083455,
"ttft_ms": 6709,
"ttft_stream_ms": 1619,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5522,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5522,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 1129,
"output_tokens_details": {
"thinking_tokens": 379
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "d7de0099-15c4-478b-889b-28df6f0af472"
}
]
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.