MS1V mlir-stage-10-v1 passing 5000/5000
Estimated confidence: 88.1%. Conservative lower bound: 41.4% (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 |
body's structural diff readable. The wrap is mandatory output, not an optimization, and is verified by the front-end's standard verifier rules in Section 9.
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<4xi32>, i32, i1, index) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg0: memref<4xi32>, %arg1: i32, %arg2: i1, %arg3: index, %arg4: none): "loom.spatial_region"() <{graph_name = "graph_0_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<4xi32>, i32, i1, index) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg1: memref<4xi32>, %arg2: i32, %arg3: i1, %arg4: index, %arg5: none): %0 = "dataflow.graph.launch"(%arg5) <{callee = @graph_0_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_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<4xi32>, %value: i32, %enabled: i1, %limit: index) ctrl (%start: none) { %c_zero_0 = arith.constant 0 : index %c_one_0 = arith.constant 1 : index scf.for %iv_0_0 = %c_zero_0 to %limit step %c_one_0 { scf.if %enabled { %out_0_0 = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb_entry(%lane_0_0: i32): %sum_0_0 = arith.addi %lane_0_0, %lane_0_0 : i32 "loom.spatial_yield"(%sum_0_0) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_0_0", source_maps = []} : (i32) -> i32 } } scf.if %enabled { "loom.spatial_region"() <{operandSegmentSizes = array<i32: 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb_entry: "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "graph_0_1", source_maps = []} : () -> () } dataflow.thread.yield } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%target: memref<4xi32>, %value: i32, %enabled: i1, %limit: index) ctrl (%start: none) { %c_zero_1 = arith.constant 0 : index %c_one_1 = arith.constant 1 : index scf.for %iv_1_0 = %c_zero_1 to %limit step %c_one_1 { %out_1_0 = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb_entry(%lane_1_0: i32): %sum_1_0 = arith.addi %lane_1_0, %lane_1_0 : i32 "loom.spatial_yield"(%sum_1_0) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_1_0", 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// Input domain: one module holding one to three `dataflow.thread` definitions. // Each thread owns one or two explicit `loom.spatial_region` publication // boundaries (sequential sites in a fixed structured scope), optionally nested // in `scf.for` and/or `scf.if` completion-propagating scopes. Operands are // normalized as value inputs, stream input channels, memory inputs and stream // output channels; results are value outputs followed by memory outputs. // No `scf.parallel`/`scf.forall`, no `dataflow.thread.launch`, no calls and no // blocking receives appear inside a region, so every candidate is publishable. start: {new NTHREADS = random.randint(1, 3); new TID = 0} 'module {\n' threads '}\n'; threads: (TID < NTHREADS) thread {TID += 1} threads | (TID == NTHREADS) ''; thread: 'dataflow.thread private @thread_' tid_text ' domain(#dataflow.thread_domain<dense>)(%target: memref<4xi32>, %value: i32, %enabled: i1, %limit: index) ctrl (%start: none) {\n' ' %c_zero_' tid_text ' = arith.constant 0 : index\n' ' %c_one_' tid_text ' = arith.constant 1 : index\n' {new NSITES = random.randint(1, 2); new SID = 0} sites ' dataflow.thread.yield\n}\n'; tid_text: [str(TID)]; sfx: [str(TID) + "_" + str(SID)]; gname: ["graph_" + str(TID) + "_" + str(SID)]; sites: (SID < NSITES) site {SID += 1} sites | (SID == NSITES) ''; site: region | for_nest | if_nest | for_if_nest; for_nest: ' scf.for %iv_' sfx ' = %c_zero_' tid_text ' to %limit step %c_one_' tid_text ' {\n' region ' }\n'; if_nest: ' scf.if %enabled {\n' region ' }\n'; for_if_nest: ' scf.for %iv_' sfx ' = %c_zero_' tid_text ' to %limit step %c_one_' tid_text ' {\n' ' scf.if %enabled {\n' region ' }\n' ' }\n'; region: empty_region | memory_region | value_region; // No boundary operands and no boundary results. empty_region: ' "loom.spatial_region"()\n' ' <{operandSegmentSizes = array<i32: 0, 0, 0, 0>,\n' ' resultSegmentSizes = array<i32: 0, 0>}> ({\n' ' ^bb_entry:\n' ' "loom.spatial_yield"()\n' ' <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n' ' }) {graph_name = "' gname '", source_maps = []} : () -> ()\n'; // One value input and one memory input, no results. memory_region: ' "loom.spatial_region"(%value, %target)\n' ' <{operandSegmentSizes = array<i32: 1, 0, 1, 0>,\n' ' resultSegmentSizes = array<i32: 0, 0>}> ({\n' ' ^bb_entry(%payload_' sfx ': i32, %memory_' sfx ': memref<4xi32>):\n' ' %slot_' sfx ' = arith.constant 0 : index\n' ' memref.store %payload_' sfx ', %memory_' sfx '[%slot_' sfx '] : memref<4xi32>\n' ' "loom.spatial_yield"()\n' ' <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n' ' }) {graph_name = "' gname '", source_maps = []} : (i32, memref<4xi32>) -> ()\n'; // One value input and one value output. value_region: ' %out_' sfx ' = "loom.spatial_region"(%value)\n' ' <{operandSegmentSizes = array<i32: 1, 0, 0, 0>,\n' ' resultSegmentSizes = array<i32: 1, 0>}> ({\n' ' ^bb_entry(%lane_' sfx ': i32):\n' ' %sum_' sfx ' = arith.addi %lane_' sfx ', %lane_' sfx ' : i32\n' ' "loom.spatial_yield"(%sum_' sfx ')\n' ' <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n' ' }) {graph_name = "' gname '", source_maps = []} : (i32) -> i32\n';
The wrap is mandatory output, not an optimization, and is verified by the front-end's standard verifier rules in Section 9.
candidate.spctpostcondition graph_def_and_launch_wrap_is_mandatory { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-dfg.md:L1569-L1571"; } constraints { let graphs = seq { op | op in output.operations where op.name == "dataflow.graph" }; let launches = seq { op | op in output.operations where op.name == "dataflow.graph.launch" }; forall g in graphs { assert definition_is_wrapped_by_launch: exists l in launches where exists target in mlir::resolve_symbol_reference(output, l, "callee") where target.name == "dataflow.graph" and target == g; } } }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<4xi32>, i32, i1, index) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg0: memref<4xi32>, %arg1: i32, %arg2: i1, %arg3: index, %arg4: none): "loom.spatial_region"() <{graph_name = "graph_0_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-082940started2026-09-11T08:29:40Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
module { dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%target: memref<4xi32>, %value: i32, %enabled: i1, %limit: index) ctrl (%start: none) { %c_zero_0 = arith.constant 0 : index %c_one_0 = arith.constant 1 : index scf.for %iv_0_0 = %c_zero_0 to %limit step %c_one_0 { scf.if %enabled { %out_0_0 = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb_entry(%lane_0_0: i32): %sum_0_0 = arith.addi %lane_0_0, %lane_0_0 : i32 "loom.spatial_yield"(%sum_0_0) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_0_0", source_maps = []} : (i32) -> i32 } } scf.if %enabled { "loom.spatial_region"() <{operandSegmentSizes = array<i32: 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({ ^bb_entry: "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> () }) {graph_name = "graph_0_1", source_maps = []} : () -> () } dataflow.thread.yield } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%target: memref<4xi32>, %value: i32, %enabled: i1, %limit: index) ctrl (%start: none) { %c_zero_1 = arith.constant 0 : index %c_one_1 = arith.constant 1 : index scf.for %iv_1_0 = %c_zero_1 to %limit step %c_one_1 { %out_1_0 = "loom.spatial_region"(%value) <{operandSegmentSizes = array<i32: 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0>}> ({ ^bb_entry(%lane_1_0: i32): %sum_1_0 = arith.addi %lane_1_0, %lane_1_0 : i32 "loom.spatial_yield"(%sum_1_0) <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> () }) {graph_name = "graph_1_0", source_maps = []} : (i32) -> i32 } dataflow.thread.yield } }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<4xi32>, i32, i1, index) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg12: memref<4xi32>, %arg13: i32, %arg14: i1, %arg15: index, %arg16: none): %8 = "arith.constant"() <{value = 0 : index}> : () -> index %9 = "arith.constant"() <{value = 1 : index}> : () -> index %10 = "scf.for"(%8, %arg15, %9, %arg16) ({ ^bb0(%arg17: index, %arg18: none): %13 = "scf.if"(%arg14) ({ %14:2 = "dataflow.graph.launch"(%arg18, %arg13) <{callee = @graph_0_0, operandSegmentSizes = array<i32: 1, 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0, 1>, source_maps = []}> : (none, i32) -> (i32, none) "scf.yield"(%14#1) : (none) -> () }, { "scf.yield"(%arg18) : (none) -> () }) : (i1) -> none "scf.yield"(%13) : (none) -> () }) : (index, index, index, none) -> none %11 = "scf.if"(%arg14) ({ %12 = "dataflow.graph.launch"(%arg16) <{callee = @graph_0_1, operandSegmentSizes = array<i32: 1, 0, 0, 0, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none) -> none "scf.yield"(%12) : (none) -> () }, { "scf.yield"(%arg16) : (none) -> () }) : (i1) -> none "dataflow.thread.yield"(%10, %11) : (none, none) -> () }) : () -> () "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<4xi32>, i32, i1, index) -> (), sym_name = "thread_1", sym_visibility = "private"}> ({ ^bb0(%arg5: memref<4xi32>, %arg6: i32, %arg7: i1, %arg8: index, %arg9: none): %4 = "arith.constant"() <{value = 0 : index}> : () -> index %5 = "arith.constant"() <{value = 1 : index}> : () -> index %6 = "scf.for"(%4, %arg8, %5, %arg9) ({ ^bb0(%arg10: index, %arg11: none): %7:2 = "dataflow.graph.launch"(%arg11, %arg6) <{callee = @graph_1_0, operandSegmentSizes = array<i32: 1, 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0, 1>, source_maps = []}> : (none, i32) -> (i32, none) "scf.yield"(%7#1) : (none) -> () }) : (index, index, index, none) -> none "dataflow.thread.yield"(%6) : (none) -> () }) : () -> () "dataflow.graph"() <{function_type = (i32) -> i32, input_segments = array<i32: 1, 0, 0>, result_segments = array<i32: 1, 0, 0>, sym_name = "graph_0_0", sym_visibility = "private"}> ({ ^bb0(%arg3: none, %arg4: i32): %2 = "arith.addi"(%arg4, %arg4) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %3:2 = "dataflow.sync"(%arg3, %2) : (none, i32) -> (none, i32) "dataflow.graph.return"(%3#1, %3#0) <{operandSegmentSizes = array<i32: 1, 0, 0, 1>}> : (i32, none) -> () }) : () -> () "dataflow.graph"() <{function_type = () -> (), input_segments = array<i32: 0, 0, 0>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_0_1", sym_visibility = "private"}> ({ ^bb0(%arg2: none): "dataflow.graph.return"(%arg2) <{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_0", 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":"1562-1571","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","applicability"],"text":"The publisher creates a deterministic, collision-free construction-local\nsymbol for each outlined graph. An existing `loom.spatial_region.graph_name`\nmay be used only as a readability or debug stem. The temporary region does not\nown graph identity, and symbol spelling does not encode cut selection, source\norder, graph identity, or artifact identity.\n\nThe templates therefore omit the def + launch wrap to keep the\nbody's structural diff readable. The wrap is mandatory output, not\nan optimization, and is verified by the front-end's standard\nverifier rules in Section 9.","why":"Governing context of the sampled obligation: the publisher outlines each graph under a construction-local symbol and the def + launch wrap is mandatory output, which fixes published dataflow.graph definitions as the governed outputs."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"23-26","path":"docs/spec-compiler-part-3-dfg.md","roles":["applicability","input_construction"],"text":"the 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.","why":"Part 3 consumes each explicit loom.spatial_region inside its owning dataflow.thread and publishes the corresponding graph definition and launch; establishes that inputs must place regions inside thread definitions for the wrap obligation to apply."},{"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: the shape the grammar samples."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"564-569","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","why":"Normalized operand order (value inputs, stream inputs, memory inputs, stream outputs) and result order (value then memory outputs), plus one affine source_map per stream input; drives the sampled operandSegmentSizes/resultSegmentSizes and empty source_maps."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"573-574","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction"],"text":"canonical graph. Current publication supports nested `scf.if` completion\n propagation. Stream channel segments become payload-typed graph stream","why":"Publication supports nested scf.if completion propagation, justifying the scf.if (and scf.for) nesting variants of the sampled publication sites."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"578-582","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction"],"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.","why":"A fixed structured scope may contain multiple sequential or mutually exclusive sites, justifying sampling one or two sequential regions per thread."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"591-598","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction"],"text":"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","why":"Enclosing loops repeatedly activate the same schedule, so a region nested in scf.for is a well-formed publication site rather than a rejected form."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"598-601","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_well_formedness"],"text":"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":"Sites under scf.parallel or scf.forall and non-fixed graph-owned parallel forms fail before publication; the grammar excludes those nestings so sampled inputs stay publishable."},{"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":"Calls that would need inlining and any transitively nested dataflow.thread.launch are invalid in this preparation state; the grammar emits no calls and no launches inside regions or threads."},{"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 require a same-activation channel witness marks a deadlocking candidate; the grammar emits no channel receives, so no sampled candidate is rejected on that ground."},{"file_sha256":"73f239de628bbf8d40145ecde732142ffcf6567c9483e6dc2286ae9176a6907c","kind":"language_definition","lines":"8-99","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 }]>","why":"TableGen definitions of loom.spatial_region and loom.spatial_yield: operand/result segment order, AffineMapArrayAttr source_maps, optional graph_name, single block, and terminator parentage — the exact generic-form spelling the grammar emits."},{"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 entry-block layout (args, thread_ctrl none, grid indices) needed to spell the enclosing thread that owns each sampled region."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"839-880","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,","why":"dataflow.graph is the only canonical graph definition surface and is materialized for execution by dataflow.graph.launch ops; fixes the operation name selected in the postcondition as the outlined graph definition."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"973-1005","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"text":"def 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);","why":"dataflow.graph.launch references a dataflow.graph definition through the FlatSymbolRefAttr callee, fixing the attribute name used to resolve the launch side of the wrap in the postcondition."},{"file_sha256":"ac9844b024e5d4761973186a7fe17c93da2de169a36f778eafc78d5277dc1f63","kind":"verifier","lines":"102-145,200-228","path":"lib/Frontend/IR/LoomOps.cpp","roles":["input_well_formedness"],"text":"LogicalResult SpatialRegionOp::verify() {\n auto thread = (*this)->getParentOfType<dataflow::ThreadOp>();\n if (!thread)\n return emitOpError(\"must appear inside a dataflow.thread body\");\n if ((*this)->getParentOfType<SpatialRegionOp>())\n return emitOpError(\"must not be nested in another loom.spatial_region\");\n if (!getBody().hasOneBlock())\n return emitOpError(\"must contain exactly one block\");\n\n Block &entry = getBody().front();\n if (entry.getNumArguments() != getNumOperands())\n return emitOpError(\"entry block argument count (\")\n << entry.getNumArguments() << \") must match operand count (\"\n << getNumOperands() << ')';\n for (auto [index, pair] : llvm::enumerate(\n llvm::zip_equal(entry.getArguments(), getOperands()))) {\n if (std::get<0>(pair).getType() != std::get<1>(pair).getType())\n return emitOpError(\"entry block argument #\")\n << index << \" type \" << std::get<0>(pair).getType()\n << \" must match operand type \" << std::get<1>(pair).getType();\n }\n\n for (auto [index, value] : llvm::enumerate(getValueInputs()))\n if (failed(verifyValueCarrier(getOperation(), value.getType(),\n \"value input\", index)))\n return failure();\n for (auto [index, value] : llvm::enumerate(getValueResults()))\n if (failed(verifyValueCarrier(getOperation(), value.getType(),\n \"value result\", index)))\n return failure();\n for (auto [index, value] : llvm::enumerate(getMemoryInputs()))\n if (failed(verifyMemoryCarrier(getOperation(), value.getType(),\n \"memory input\", index)))\n return failure();\n for (auto [index, value] : llvm::enumerate(getMemoryResults()))\n if (failed(verifyMemoryCarrier(getOperation(), value.getType(),\n \"memory result\", index)))\n return failure();\n\n ArrayAttr sourceMaps = getSourceMaps();\n if (sourceMaps.size() != getStreamInputs().size())\n return emitOpError(\"source_maps count (\")\n << sourceMaps.size() << \") must match stream input count (\"\n << getStreamInputs().size() << ')';\nLogicalResult SpatialYieldOp::verify() {\n auto parent = (*this)->getParentOfType<SpatialRegionOp>();\n if (!parent)\n return emitOpError(\"must appear inside loom.spatial_region\");\n if (getValues().size() != parent.getValueResults().size())\n return emitOpError(\"value count (\")\n << getValues().size() << \") must match parent value result count (\"\n << parent.getValueResults().size() << ')';\n if (getMemories().size() != parent.getMemoryResults().size())\n return emitOpError(\"memory count (\")\n << getMemories().size()\n << \") must match parent memory result count (\"\n << parent.getMemoryResults().size() << ')';\n for (auto [index, pair] :\n llvm::enumerate(llvm::zip_equal(getValues(), parent.getValueResults())))\n if (std::get<0>(pair).getType() != std::get<1>(pair).getType())\n return emitOpError(\"value #\")\n << index << \" type \" << std::get<0>(pair).getType()\n << \" must match parent result type \"\n << std::get<1>(pair).getType();\n for (auto [index, pair] : llvm::enumerate(\n llvm::zip_equal(getMemories(), parent.getMemoryResults())))\n if (std::get<0>(pair).getType() != std::get<1>(pair).getType())\n return emitOpError(\"memory #\")\n << index << \" type \" << std::get<0>(pair).getType()\n << \" must match parent result type \"\n << std::get<1>(pair).getType();\n return success();\n}","why":"SpatialRegionOp/SpatialYieldOp verifiers: parent thread required, no nesting, exactly one block, entry-block arguments matching operands one-for-one by type, source_maps count equal to stream inputs, and yield counts/types matching the region results — the acceptance rules the sampled inputs must satisfy."},{"file_sha256":"05567d70fd335a83ee2f46b2d0a3025a903207a88602a798b1845033e7f8ef64","kind":"implementation","lines":"912-918","path":"lib/Frontend/Lowering/LowerForToGraphPass.cpp","roles":["applicability"],"text":"::llvm::StringRef getArgument() const final {\n return \"loom-lower-for-to-graph\";\n }\n ::llvm::StringRef getDescription() const final {\n return \"Publish explicit loom.spatial_region operations as \"\n \"dataflow.graph definitions plus dataflow.graph.launch ops.\";","why":"The --loom-lower-for-to-graph pass registration and description confirm this stage publishes explicit loom.spatial_region ops as dataflow.graph definitions plus dataflow.graph.launch ops, supporting the stage attribution of the claim and the retained subject flag."},{"file_sha256":"c25a72ad99349973a47f2a1e081b6b269920e25cc5f59f74619c2e7ce0c2b65d","kind":"test","lines":"39-52","path":"test/raise/scf-to-dfg-explicit-spatial-ownership.mlir","roles":["input_construction"],"text":"dataflow.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":"Published-case spelling of a dataflow.thread owning a loom.spatial_region with one value input and one memory input in generic form, used as the concrete syntax template for the sampled memory-boundary variant."},{"file_sha256":"df76d22d1149cf2929b700df6f97b58d27b64d523346cfbb4dbf9ba8e66baa49","kind":"test","lines":"62-79","path":"test/raise/scf-to-dfg-nested-completion.mlir","roles":["input_construction"],"text":"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 }","why":"Accepted spelling of an empty-boundary loom.spatial_region nested in scf.for/scf.if inside a dataflow.thread, used as the template for the nested publication-site variants."},{"file_sha256":"197ccf7e69971f310502d6a5181dd00cdf96a9711fe3abf64e2b339bfd958513","kind":"test","lines":"86-101","path":"test/raise/spatial-candidate-surface.mlir","roles":["input_construction"],"text":"//--- weighted-selected.mlir\ndataflow.thread private @selected_weighted domain(#dataflow.thread_domain<dense>)(%c: i1, %v: i32) ctrl (%start: none) {\n %result = \"loom.spatial_region\"(%c, %v)\n <{operandSegmentSizes = array<i32: 2, 0, 0, 0>,\n resultSegmentSizes = array<i32: 1, 0>}> ({\n ^bb0(%cond: i1, %value: i32):\n cf.cond_br %cond weights([1, 9]), ^yes, ^no\n ^yes:\n \"loom.spatial_yield\"(%value)\n <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n ^no:\n \"loom.spatial_yield\"(%value)\n <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n }) {graph_name = \"selected_weighted_graph\", source_maps = []} :\n (i1, i32) -> i32\n dataflow.thread.yield","why":"Spelling of a loom.spatial_region with one value input and one value result yielded through loom.spatial_yield (segment arrays and function type); only the syntax of the value-output boundary is relied on, not this test's rejected weighted-CFG body."}],"primary_bundle_sha256":"22a1b498e96a507d7b6d70a8ebd03bfb43e4da86c39c48519a5cc9754ee3311e","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"07f36e594c96cae05ca36f29434be6127c32dfbcc9d87f1cf2ecc03df22e55c7"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 34146,
"duration_ms": 34193,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1144,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 4699,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.110875,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 2555,
"provider": "firstParty",
"thinkingTokens": 9,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR `module { ... }` whose body contains nothing but `dataflow.thread` definitions.\n2. Each emitted program contains between one and three `dataflow.thread` definitions, and never zero.\n3. Every thread is declared `private`, is named `@thread_<N>` where `<N>` is its zero-based index in the module, and carries the domain attribute `#dataflow.thread_domain<dense>`.\n4. Every thread has exactly the four data arguments `%target: memref<4xi32>`, `%value: i32`, `%enabled: i1`, `%limit: index`, in that order, and exactly one control argument `ctrl (%start: none)`.\n5. Every thread body begins with exactly two `arith.constant` definitions of type `index`, one holding `0` and one holding `1`, defined before any other operation in the body.\n6. Every thread body ends with a `dataflow.thread.yield` terminator with no operands.\n7. Every thread contains one or two `loom.spatial_region` publication sites, and never zero and never more than two; the sites are sequential siblings in the thread's structured scope (no site is nested inside another site).\n8. Every `loom.spatial_region` operation appears either directly in the thread body or inside `scf.for` and/or `scf.if` scopes contained in that thread body; no other nesting form occurs.\n9. Every `scf.for` that wraps a region runs from the thread's `index` zero constant to the thread argument `%limit` in steps of the thread's `index` one constant, i.e. its bounds and step are exactly the values defined in the enclosing thread's preamble and its argument list.\n10. Every `scf.if` that wraps a region is predicated on the thread argument `%enabled` of type `i1` and has no `else` region and no results.\n11. When both loop and conditional scopes wrap a region, the `scf.for` is the outer scope and the `scf.if` is the inner scope; the reverse nesting never occurs.\n12. Every `loom.spatial_region` is written in generic form with an explicit `operandSegmentSizes` array of four `i32` entries \u2014 value inputs, stream input channels, memory inputs, stream output channels, in that order \u2014 and an explicit `resultSegmentSizes` array of two `i32` entries \u2014 value outputs then memory outputs.\n13. The segment-size arrays of every region agree exactly with the operand list, the entry block signature and the function type written on the operation: operand counts, entry block argument count and types, and result counts are mutually consistent.\n14. Every region's operands are supplied only by values that are in scope at the site, namely the enclosing thread's own arguments.\n15. Every region's body is a single block labelled `^bb_entry` whose arguments correspond positionally to the region's operands with matching types.\n16. Every region body terminates with a generic-form `\"loom.spatial_yield\"` whose `operandSegmentSizes` is a two-entry `i32` array, and whose operand count and function type match the region's result signature: zero operands for regions with no results, one `i32` operand for regions producing one `i32` result.\n17. Every region carries a `graph_name` string attribute and a `source_maps` attribute whose value is the empty list.\n18. Every value produced inside a region body is defined before its use, and any value yielded from a region is defined within that same region body.\n19. Memory-writing regions take the memref as an explicit memory input operand and store through the corresponding entry-block argument rather than capturing the thread argument implicitly.\n20. No emitted program contains `scf.parallel`, `scf.forall`, `dataflow.thread.launch`, function calls, or blocking receive operations anywhere inside or around a region.\n21. No region contains any nested `loom.spatial_region`, and no region has both results and memory outputs \u2014 memory outputs are always zero.\n22. Stream input channels and stream output channels are always absent: their segment counts are zero in every emitted region.\n23. All SSA names within a thread are unique, and names derived per site are unique across sites of the same thread and across threads.\n\n## Sampling conventions\n\n1. The module size is sampled uniformly from the closed range one to three threads; larger modules are never emitted.\n2. The per-thread site count is sampled independently per thread from the closed range one to two; three or more sites per thread never occur.\n3. Thread names use the fixed scheme `@thread_` concatenated with the decimal thread index starting at `0`.\n4. Per-site SSA suffixes use the fixed scheme `<thread index>_<site index>`, both zero-based decimals, giving names such as `%out_1_0`, `%payload_2_1`, `%iv_0_1`.\n5. The constant preamble names are fixed as `%c_zero_<tid>` and `%c_one_<tid>`, one pair per thread, even when no loop in that thread uses them.\n6. `graph_name` values are always the literal `\"graph_\" + <thread index> + \"_\" + <site index>`; no other naming scheme or duplicate names are produced.\n7. Exactly four nesting shapes are emitted per site, chosen independently: bare region, region in `scf.for`, region in `scf.if`, and region in `scf.for` containing `scf.if`; an `scf.if` wrapping an `scf.for` is never emitted, and no nesting depth beyond two is emitted.\n8. Exactly three region bodies are emitted, chosen independently per site: an empty region with no operands and no results; a memory region with one value input and one memory input and no results; and a value region with one value input and one value output.\n9. The memory region always stores the single `i32` payload at a locally defined `index` constant `0` into slot zero of the `memref<4xi32>`; no other index, offset, or load is emitted.\n10. The value region always computes `arith.addi` of its single lane argument with itself and yields that `i32` sum; no other arithmetic, no multiple results, and no multi-operation bodies are emitted.\n11. The empty region's body consists solely of the entry block label and the yield; it never contains computation.\n12. Region operands, when present, are always drawn from the fixed thread arguments `%value` (value input) and `%target` (memory input); the thread arguments `%enabled`, `%limit` and `%start` are never passed into a region.\n13. The `i1` argument `%enabled` is used only as an `scf.if` condition, and `%limit` only as a loop upper bound; neither is otherwise consumed.\n14. The control argument `%start` is declared on every thread but never used.\n15. Types are fixed throughout: `i32` for payload values, `memref<4xi32>` for memory, `index` for loop induction and constants, `i1` for the predicate.\n16. Region results, when produced, are bound to `%out_<suffix>` and are never consumed by any subsequent operation.\n17. Regions are always written in generic (quoted) form with explicit segment attributes rather than any custom assembly form, and `scf.for`/`scf.if` are always written in custom form.\n18. The `source_maps` attribute is always the empty list; non-empty source maps are never emitted.\n19. Indentation is fixed: two spaces for thread-body statements, four spaces for the region operation, six for the entry block label, eight for region body statements; nested `scf.if` bodies are not further indented relative to their `scf.for` parent.\n20. `scf.for` loops always use unit step and zero lower bound rather than sampled bounds, and loop bodies contain exactly one site each.\n21. Each thread's sites are emitted in ascending site-index order and each thread in ascending thread-index order, with no interleaving or reordering.\n22. The nesting shape and the region body kind are chosen independently, so all twelve combinations are reachable at every site.",
"result_index": 0,
"session_id": "b2ef6bd8-719d-4a80-8d46-357b736e77c3",
"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": 47,
"total_cost_usd": 0.110875,
"ttft_ms": 1163,
"ttft_stream_ms": 1143,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 4699,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 4699,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 2555,
"output_tokens_details": {
"thinking_tokens": 9
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "d9ca4adb-0203-4f72-a01a-7509106ba47f"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 8448,
"duration_ms": 8475,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1220,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5343,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.067165,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 549,
"provider": "firstParty",
"thinkingTokens": 14,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition looks only at the subject's output program, never at the input. It first selects two sets of operations from every depth of the output: `graphs`, all operations whose name is exactly `dataflow.graph`, and `launches`, all operations whose name is exactly `dataflow.graph.launch`. The single assertion is universally quantified over `graphs`, and for each such graph it requires that there exists at least one launch operation in the output whose `callee` symbol reference resolves \u2014 via the vocabulary's symbol resolution over the whole output program \u2014 to at least one target operation that is both named `dataflow.graph` and is the very same entity as the graph under consideration. Identity here is entity identity within the one output program, so a launch pointing at a different graph with the same name does not satisfy the obligation for this graph.\n\nIt therefore rejects any output containing a `dataflow.graph` operation for which no `dataflow.graph.launch` resolves its `callee` back to that exact operation, including cases where the `callee` attribute is missing or unresolvable (resolution simply yields no target, and the `exists` fails). It accepts outputs where every selected graph has at least one such matching launch; launches whose callee resolves elsewhere, resolves to a non-`dataflow.graph` operation, or resolves to nothing are permitted so long as each graph is covered by some launch, and a single launch may cover only the one graph it names. The check is vacuously true \u2014 and so passes \u2014 on any output containing no `dataflow.graph` operations at all, regardless of how many launches are present. No values, types, attributes, operands, results, regions, or counts other than the name-based selection and symbol resolution are consulted.",
"result_index": 0,
"session_id": "640378b4-f403-43d3-91c7-064b72a647c0",
"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": 27,
"total_cost_usd": 0.067165,
"ttft_ms": 1262,
"ttft_stream_ms": 1088,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5343,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5343,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 549,
"output_tokens_details": {
"thinking_tokens": 14
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "4c448d6a-66b6-4b44-a9b1-f9f138fd80f0"
}
]
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.