MS0V2 mlir-stage-02-v1 passing 5000/5000

MLIR passage 2: Graph launch execution boundary

Test report

30generated samples
100.0%input coverage
100.0%output coverage
not measuredcode coverage
Not estimatedconfidence
30/30checker passes
Source passages for this PBT
  • dataflow.graph.launch is the SpatialCore execution boundary inside a dataflow.thread definition's body. It references a dataflow.graph callable by symbol, supplies dependency events, value inputs, stream channel bindings, and memory imports, and yields value outputs, memory exports, and a trailing done : none result.

docs/spec-compiler-part-3-dfg.md lines 490–494

Minimized conforming example

14 → 11 lines · seed 114 of run 20260911-041310

input

"builtin.module"() ({
  "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (i32, memref<4xi32>, !dataflow.channel<i32>, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({
  ^bb0(%arg0: i32, %arg1: memref<4xi32>, %arg2: !dataflow.channel<i32>, %arg3: i1, %arg4: 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"() : () -> ()
  }) : () -> ()
}) : () -> ()

output

"builtin.module"() ({
  "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (i32, memref<4xi32>, !dataflow.channel<i32>, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({
  ^bb0(%arg1: i32, %arg2: memref<4xi32>, %arg3: !dataflow.channel<i32>, %arg4: i1, %arg5: none):
    %0 = "dataflow.graph.launch"(%arg5) <{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) -> ()
  }) : () -> ()
}) : () -> ()

Conditions

input conditions — what generated inputs satisfy

Conforming input

module {
  dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%value: i32, %mem: memref<4xi32>, %chan: !dataflow.channel<i32>, %flag: i1) ctrl (%start: none) {
    %c0 = arith.constant 0 : index
    %c1 = arith.constant 1 : index
    %c4 = arith.constant 4 : index
    scf.for %i = %c0 to %c4 step %c1 {
      scf.if %flag {
      %sum_0 = "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_0", source_maps = []} :
          (i32) -> i32
      }
    }
    dataflow.thread.yield
  }
  dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%value: i32, %mem: memref<4xi32>, %chan: !dataflow.channel<i32>, %flag: i1) ctrl (%start: none) {
    %c0 = arith.constant 0 : index
    %c1 = arith.constant 1 : index
    %c4 = arith.constant 4 : index
      "loom.spatial_region"(%chan, %mem)
          <{operandSegmentSizes = array<i32: 0, 1, 1, 0>,
            resultSegmentSizes = array<i32: 0, 0>}> ({
        ^bb0(%channel: !dataflow.channel<i32>, %target: memref<4xi32>):
          %message = dataflow.channel.receive %channel : !dataflow.channel<i32>
          %zero = arith.constant 0 : index
          memref.store %message, %target[%zero] : memref<4xi32>
          "loom.spatial_yield"()
              <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
      }) {graph_name = "graph_1", source_maps = [affine_map<() -> ()>]} :
          (!dataflow.channel<i32>, memref<4xi32>) -> ()
    dataflow.thread.yield
  }
}

2 linked-input-36 · linked input 36

One binding denotes one ordered dynamic event sequence. A fixed structured scope may contain multiple sequential or structured mutually exclusive sites.

docs/spec-compiler-part-3-dfg.md lines 578–582

3 linked-input-55 · linked input 55

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.

docs/spec-compiler-part-3-dfg.md lines 591–598

4 linked-input-90 · linked input 90

Current publication supports nested scf.if completion propagation.

docs/spec-compiler-part-3-dfg.md lines 573–574

5 linked-input-140 · linked input 140

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.

docs/spec-compiler-part-3-dfg.md lines 499–506

6 linked-input-150 · linked input 150

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.

docs/spec-compiler-part-3-dfg.md lines 564–569

7 linked-input-162 · linked input 162

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.

docs/spec-compiler-part-3-dfg.md lines 23–26

8 linked-input-179 · linked input 179

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.

docs/spec-compiler-part-3-dfg.md lines 462–465

9 linked-input-180 · linked input 180

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.

docs/spec-compiler-part-3-dfg.md lines 598–601

10 linked-input-204 · linked input 204

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.

docs/spec-compiler-part-3-dfg.md lines 1413–1419

Generator grammar · candidate.pg
// Inputs: modules of `dataflow.thread` definitions that each own one explicit
// `loom.spatial_region` publication candidate, optionally nested in fixed
// structured scopes (`scf.for`, `scf.if`) that Part 3 publication supports.

start: {new COUNT = random.randint(1, 3); new I = 0}
       'module {\n'
       threads
       '}\n';

threads: (I < COUNT) thread_def {I += 1} threads
       | (I == COUNT) '';

thread_def: {new WRAP = random.randint(0, 3); new FORM = random.randint(0, 4)}
       '  dataflow.thread private @thread_' idx
       ' domain(#dataflow.thread_domain<dense>)(%value: i32, %mem: memref<4xi32>, %chan: !dataflow.channel<i32>, %flag: i1) ctrl (%start: none) {\n'
       '    %c0 = arith.constant 0 : index\n'
       '    %c1 = arith.constant 1 : index\n'
       '    %c4 = arith.constant 4 : index\n'
       wrapped
       '    dataflow.thread.yield\n'
       '  }\n';

idx: [str(I)];

wrapped: (WRAP == 0) region
       | (WRAP == 1) '    scf.for %i = %c0 to %c4 step %c1 {\n' region '    }\n'
       | (WRAP == 2) '    scf.if %flag {\n' region '    }\n'
       | (WRAP == 3) '    scf.for %i = %c0 to %c4 step %c1 {\n      scf.if %flag {\n' region '      }\n    }\n';

region: (FORM == 0) form_store
      | (FORM == 1) form_empty
      | (FORM == 2 and WRAP == 0) form_stream
      | (FORM == 2 and WRAP > 0) form_empty
      | (FORM == 3) form_value
      | (FORM == 4 and WRAP == 0) form_receive
      | (FORM == 4 and WRAP > 0) form_store;

// Value input plus memory import; no boundary results.
form_store: '      "loom.spatial_region"(%value, %mem)\n'
       '          <{operandSegmentSizes = array<i32: 1, 0, 1, 0>,\n'
       '            resultSegmentSizes = array<i32: 0, 0>}> ({\n'
       '        ^bb0(%payload: i32, %memory: memref<4xi32>):\n'
       '          %zero = arith.constant 0 : index\n'
       '          memref.store %payload, %memory[%zero] : memref<4xi32>\n'
       '          "loom.spatial_yield"()\n'
       '              <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n'
       '      }) {graph_name = "graph_' idx '", source_maps = []} :\n'
       '          (i32, memref<4xi32>) -> ()\n';

// Empty boundary: no inputs, no results.
form_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_' idx '", source_maps = []} : () -> ()\n';

// Value input plus one stream output channel binding.
form_stream: '      "loom.spatial_region"(%value, %chan)\n'
       '          <{operandSegmentSizes = array<i32: 1, 0, 0, 1>,\n'
       '            resultSegmentSizes = array<i32: 0, 0>}> ({\n'
       '        ^bb0(%payload: i32, %output: !dataflow.channel<i32>):\n'
       '          dataflow.channel.send %output, %payload : !dataflow.channel<i32>\n'
       '          "loom.spatial_yield"()\n'
       '              <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n'
       '      }) {graph_name = "graph_' idx '", source_maps = []} :\n'
       '          (i32, !dataflow.channel<i32>) -> ()\n';

// Value input and one value output.
form_value: '      %sum_' idx ' = "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_' idx '", source_maps = []} :\n'
       '          (i32) -> i32\n';

// One stream input channel binding with its affine `source_map`, plus a
// memory import.
form_receive: '      "loom.spatial_region"(%chan, %mem)\n'
       '          <{operandSegmentSizes = array<i32: 0, 1, 1, 0>,\n'
       '            resultSegmentSizes = array<i32: 0, 0>}> ({\n'
       '        ^bb0(%channel: !dataflow.channel<i32>, %target: memref<4xi32>):\n'
       '          %message = dataflow.channel.receive %channel : !dataflow.channel<i32>\n'
       '          %zero = arith.constant 0 : index\n'
       '          memref.store %message, %target[%zero] : memref<4xi32>\n'
       '          "loom.spatial_yield"()\n'
       '              <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n'
       '      }) {graph_name = "graph_' idx '", source_maps = [affine_map<() -> ()>]} :\n'
       '          (!dataflow.channel<i32>, memref<4xi32>) -> ()\n';

output condition — what every compiled pair must satisfy

graph_launch_is_spatialcore_execution_boundary · 10 assertion sites

derived from 1 passage: 1selected-output

dataflow.graph.launch is the SpatialCore execution boundary inside a dataflow.thread definition's body. It references a dataflow.graph callable by symbol, supplies dependency events, value inputs, stream channel bindings, and memory imports, and yields value outputs, memory exports, and a trailing done : none result.

Executable output condition · candidate.spct
postcondition graph_launch_is_spatialcore_execution_boundary {
  language v0;
  vocabulary mlir = mlir.generic@1;

  metadata {
    project = "PolyArch/loom";
    revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b";
    source = "docs/spec-compiler-part-3-dfg.md:L490-L494";
  }

  constraints {
    let threads = seq { op | op in output.operations
                        where op.name == "dataflow.thread" };
    let launches = seq { op | op in output.operations
                         where op.name == "dataflow.graph.launch" };

    forall l in launches {
      // Inside a `dataflow.thread` definition's body.
      assert inside_thread_definition:
        exists t in threads where mlir::contains(t, l);

      // References a `dataflow.graph` callable by symbol.
      assert callee_is_graph_definition:
        exists g in mlir::resolve_symbol_reference(output, l, "callee")
        where g.name == "dataflow.graph";

      // Supplies dependency events, value inputs, stream channel bindings,
      // and memory imports as the operand segments of the boundary.
      assert dependency_events_are_events:
        forall v in mlir::operand_segment(l, 0) where v.type == mlir::none;
      assert stream_bindings_are_channels:
        forall v in mlir::operand_segment(l, 2)
        where v.type.kind == "!dataflow.channel";
      assert stream_output_bindings_are_channels:
        forall v in mlir::operand_segment(l, 4)
        where v.type.kind == "!dataflow.channel";
      assert operands_are_exactly_the_named_segments:
        cardinality(mlir::operand_segment(l, 0))
          + cardinality(mlir::operand_segment(l, 1))
          + cardinality(mlir::operand_segment(l, 2))
          + cardinality(mlir::operand_segment(l, 3))
          + cardinality(mlir::operand_segment(l, 4))
          == cardinality(l.operands);

      // Yields value outputs, memory exports, and a trailing `done : none`.
      assert results_are_exactly_the_named_segments:
        cardinality(mlir::result_segment(l, 0))
          + cardinality(mlir::result_segment(l, 1))
          + cardinality(mlir::result_segment(l, 2))
          == cardinality(l.results);
      assert one_done_result: cardinality(mlir::result_segment(l, 2)) == 1;
      assert done_result_is_none:
        forall v in mlir::result_segment(l, 2) where v.type == mlir::none;
      assert done_result_is_trailing:
        forall v in mlir::result_segment(l, 2)
        where exists last in l.results.drop(cardinality(l.results) - 1)
        where last == v;
    }
  }
}
conforming example

14 → 11 lines · seed 114 of run 20260911-041310

"builtin.module"() ({
  "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (i32, memref<4xi32>, !dataflow.channel<i32>, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({
  ^bb0(%arg0: i32, %arg1: memref<4xi32>, %arg2: !dataflow.channel<i32>, %arg3: i1, %arg4: 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"() : () -> ()
  }) : () -> ()
}) : () -> ()

Evidence

runs: 20260911-035440 · 20260911-041310

run20260911-035440started2026-09-11T03:54:40Zsubjectloom-raise-optsubject revision48615bc5925e

run results

30saved inputs
30accepted

output condition verdicts

30pass
Additional trace diagnostics

raw trace evidence

1000accepted trace samples
14distinct trace classes
1classes seen once
sample pair · seed 0

generated input

module {
  dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%value: i32, %mem: memref<4xi32>, %chan: !dataflow.channel<i32>, %flag: i1) ctrl (%start: none) {
    %c0 = arith.constant 0 : index
    %c1 = arith.constant 1 : index
    %c4 = arith.constant 4 : index
    scf.for %i = %c0 to %c4 step %c1 {
      scf.if %flag {
      %sum_0 = "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_0", source_maps = []} :
          (i32) -> i32
      }
    }
    dataflow.thread.yield
  }
  dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%value: i32, %mem: memref<4xi32>, %chan: !dataflow.channel<i32>, %flag: i1) ctrl (%start: none) {
    %c0 = arith.constant 0 : index
    %c1 = arith.constant 1 : index
    %c4 = arith.constant 4 : index
      "loom.spatial_region"(%chan, %mem)
          <{operandSegmentSizes = array<i32: 0, 1, 1, 0>,
            resultSegmentSizes = array<i32: 0, 0>}> ({
        ^bb0(%channel: !dataflow.channel<i32>, %target: memref<4xi32>):
          %message = dataflow.channel.receive %channel : !dataflow.channel<i32>
          %zero = arith.constant 0 : index
          memref.store %message, %target[%zero] : memref<4xi32>
          "loom.spatial_yield"()
              <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
      }) {graph_name = "graph_1", source_maps = [affine_map<() -> ()>]} :
          (!dataflow.channel<i32>, memref<4xi32>) -> ()
    dataflow.thread.yield
  }
}

observed generic output

#map = affine_map<() -> ()>
"builtin.module"() ({
  "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (i32, memref<4xi32>, !dataflow.channel<i32>, i1) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({
  ^bb0(%arg10: i32, %arg11: memref<4xi32>, %arg12: !dataflow.channel<i32>, %arg13: i1, %arg14: none):
    %11 = "arith.constant"() <{value = 0 : index}> : () -> index
    %12 = "arith.constant"() <{value = 1 : index}> : () -> index
    %13 = "arith.constant"() <{value = 4 : index}> : () -> index
    %14 = "scf.for"(%11, %13, %12, %arg14) ({
    ^bb0(%arg15: index, %arg16: none):
      %15 = "scf.if"(%arg13) ({
        %16:2 = "dataflow.graph.launch"(%arg16, %arg10) <{callee = @graph_0, operandSegmentSizes = array<i32: 1, 1, 0, 0, 0>, resultSegmentSizes = array<i32: 1, 0, 1>, source_maps = []}> : (none, i32) -> (i32, none)
        "scf.yield"(%16#1) : (none) -> ()
      }, {
        "scf.yield"(%arg16) : (none) -> ()
      }) : (i1) -> none
      "scf.yield"(%15) : (none) -> ()
    }) : (index, index, index, none) -> none
    "dataflow.thread.yield"(%14) : (none) -> ()
  }) : () -> ()
  "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (i32, memref<4xi32>, !dataflow.channel<i32>, i1) -> (), sym_name = "thread_1", sym_visibility = "private"}> ({
  ^bb0(%arg5: i32, %arg6: memref<4xi32>, %arg7: !dataflow.channel<i32>, %arg8: i1, %arg9: none):
    %7 = "arith.constant"() <{value = 0 : index}> : () -> index
    %8 = "arith.constant"() <{value = 1 : index}> : () -> index
    %9 = "arith.constant"() <{value = 4 : index}> : () -> index
    %10 = "dataflow.graph.launch"(%arg9, %arg7, %arg6) <{callee = @graph_1, operandSegmentSizes = array<i32: 1, 0, 1, 1, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = [#map]}> : (none, !dataflow.channel<i32>, memref<4xi32>) -> none
    "dataflow.thread.yield"(%10) : (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", sym_visibility = "private"}> ({
  ^bb0(%arg3: none, %arg4: i32):
    %5 = "arith.addi"(%arg4, %arg4) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32
    %6:2 = "dataflow.sync"(%arg3, %5) : (none, i32) -> (none, i32)
    "dataflow.graph.return"(%6#1, %6#0) <{operandSegmentSizes = array<i32: 1, 0, 0, 1>}> : (i32, none) -> ()
  }) : () -> ()
  "dataflow.graph"() <{arg_attrs = [{}, {llvm.noalias}], function_type = (i32, memref<4xi32>) -> (), input_segments = array<i32: 0, 1, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_1", sym_visibility = "private"}> ({
  ^bb0(%arg0: none, %arg1: i32, %arg2: memref<4xi32>):
    %0 = "dataflow.constant"(%arg0) <{const_value = 0 : index}> : (none) -> index
    %1 = "dataflow.constant"(%arg0) <{const_value = true}> : (none) -> i1
    %2:2 = "dataflow.demux"(%1, %arg1) : (i1, i32) -> (i32, i32)
    %3:2 = "dataflow.sync"(%arg0, %2#1) : (none, i32) -> (none, i32)
    %4 = "dataflow.store"(%arg2, %0, %3#1, %3#0) : (memref<4xi32>, index, i32, none) -> none
    "dataflow.graph.return"(%4) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> ()
  }) : () -> ()
}) : () -> ()
per-seed evidence (30 seeds)
seedsubjectverdictartifacts
0accepted exit 0 · 0.613sPASSinput · generic input · output · check report
1accepted exit 0 · 0.596sPASSinput · generic input · output · check report
2accepted exit 0 · 0.584sPASSinput · generic input · output · check report
3accepted exit 0 · 0.583sPASSinput · generic input · output · check report
4accepted exit 0 · 0.612sPASSinput · generic input · output · check report
5accepted exit 0 · 0.576sPASSinput · generic input · output · check report
6accepted exit 0 · 0.602sPASSinput · generic input · output · check report
7accepted exit 0 · 0.571sPASSinput · generic input · output · check report
8accepted exit 0 · 0.568sPASSinput · generic input · output · check report
9accepted exit 0 · 0.566sPASSinput · generic input · output · check report
10accepted exit 0 · 0.575sPASSinput · generic input · output · check report
11accepted exit 0 · 0.558sPASSinput · generic input · output · check report
12accepted exit 0 · 0.585sPASSinput · generic input · output · check report
13accepted exit 0 · 0.728sPASSinput · generic input · output · check report
14accepted exit 0 · 0.574sPASSinput · generic input · output · check report
15accepted exit 0 · 0.613sPASSinput · generic input · output · check report
16accepted exit 0 · 0.567sPASSinput · generic input · output · check report
17accepted exit 0 · 0.57sPASSinput · generic input · output · check report
18accepted exit 0 · 0.599sPASSinput · generic input · output · check report
19accepted exit 0 · 0.596sPASSinput · generic input · output · check report
20accepted exit 0 · 0.569sPASSinput · generic input · output · check report
21accepted exit 0 · 0.59sPASSinput · generic input · output · check report
22accepted exit 0 · 0.6sPASSinput · generic input · output · check report
23accepted exit 0 · 0.657sPASSinput · generic input · output · check report
24accepted exit 0 · 0.605sPASSinput · generic input · output · check report
25accepted exit 0 · 0.571sPASSinput · generic input · output · check report
26accepted exit 0 · 0.67sPASSinput · generic input · output · check report
27accepted exit 0 · 0.629sPASSinput · generic input · output · check report
28accepted exit 0 · 0.63sPASSinput · generic input · output · check report
29accepted exit 0 · 0.621sPASSinput · generic input · output · check report
How this PBT was generated and reviewed

paired production revision · manifest.json · review.json

partial source coverage: Approved to run and display existing artifacts; accuracy and completeness are measured separately.

Independent replay: 20 generated, 20 compiler-accepted; checker verdicts {"PASS": 20}. Compiler binary and revision identities matched.

Covered requirements

  • Graph-launch containment, graph symbol resolution, dependency/channel types, segment totals, and trailing done result.

Uncovered requirements

  • Partial: checks thread containment, graph-symbol resolution, dependency/channel types, segment totals and trailing done. Does not check value/memory bindings against the callable signature; generator never exercises memory exports. All 20 outputs contain launches. Empty output passes, so publication loss is undetected.
Agent-selected pinned authoring context · authoring-context.json
{"entries":[{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"457-494","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","applicability"],"text":"* `llvm.func` remains the sole function and ABI owner for a callable imported\n  from the final linked LLVM module. `func.func` is used only for a genuinely\n  standard-MLIR-native callable or helper; it cannot mirror the LLVM ABI.\n  Neither callable kind chooses HostCore or AccCore ownership. Call-context\n  classification decides where calls are legal.\n* `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.\n* `dataflow.thread` is the logical accelerator execution-domain\n  **definition** (Symbol-bearing, module-scope, function-like). It owns the\n  kernel body and one domain kind. A dense definition owns coordinate rank\n  through its canonical entry-block shape; a dynamic definition designates\n  one ordinary argument as its work-item payload.\n  It does not itself execute; dynamic logical instances are\n  materialized by one or more `dataflow.thread.launch` ops at use\n  sites, then SystemMapping decides which instances occupy physical AccCore\n  slots.\n* `dataflow.thread.launch` is the logical accelerator execution\n  boundary. It references a `dataflow.thread` callable by symbol, supplies\n  async dependencies and ordinary body operands, plus one non-negative extent\n  per dense coordinate dimension. A dynamic launch instead supplies one root\n  work item and no extents. Both produce one collective completion token.\n* `dataflow.work.spawn` publishes one child of the currently executing dynamic\n  work item after atomically acquiring its termination responsibility. It is\n  illegal in a dense thread or any graph and is not nested thread launch.\n* `dataflow.graph` is the SpatialCore leaf DFG **definition**\n  (Symbol-bearing, module-scope, function-like). Its body cannot\n  contain callable definitions, `llvm.call`, `func.call`,\n  `dataflow.thread.launch`, `dataflow.graph.launch`, or another\n  `dataflow.graph` definition.\n  It is final target-independent software IR: its validity does not assert\n  that any current Fabric can realize it. TechMapping owns that decision.\n* `dataflow.graph.launch` is the SpatialCore execution boundary\n  inside a `dataflow.thread` definition's body. It references a\n  `dataflow.graph` callable by symbol, supplies dependency events, value\n  inputs, stream channel bindings, and memory imports, and yields value\n  outputs, memory exports, and a trailing `done : none` result.","why":"Governing context of the sampled claim; fixes the terminology (dataflow.thread definition body, dataflow.graph callable, loom.spatial_region as the temporary candidate) and selects the dataflow.graph.launch operations of the output that the obligation ranges over."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"23-26","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","applicability"],"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 graph definition and launch; this is why the generator places every candidate region inside a thread definition and why the pass under test produces the launches."},{"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 boundary segmentation of loom.spatial_region operands (value inputs, stream input channels, memory inputs, stream output channels) and results (value then memory), plus the affine source_map per stream input; drives the operand/result segment sizes each generated region emits."},{"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 + scf.if wrappings the generator samples around a candidate region."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"578-582,591-598","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","why":"Fixed structured scopes with sequential or mutually exclusive sites and enclosing loops are in-domain inputs; bounds the generator to fixed loop/branch nesting with one endpoint site per scope."},{"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":"Endpoint sites nested under scf.parallel or scf.forall fail before publication, so the generator never wraps a candidate in those forms."},{"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":"Thread bodies that still contain graph-bearing llvm.call/func.call or a nested dataflow.thread.launch are out of the publishable domain; the generator emits neither inside thread bodies."},{"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 candidate whose blocking receive can only be justified by a send outside the region is a deadlocking cut; the generated send and receive regions are self-contained so no sampled input relies on such a witness."},{"file_sha256":"73f239de628bbf8d40145ecde732142ffcf6567c9483e6dc2286ae9176a6907c","kind":"language_definition","lines":"8-105","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}\n\n#endif // LOOM_FRONTEND_IR_LOOMOPS_TD","why":"Definition of loom.spatial_region and loom.spatial_yield: operand/result segment order, AttrSizedOperandSegments/AttrSizedResultSegments, source_maps and graph_name attributes, single-block isolated body; fixes the exact generic-form spelling the grammar emits."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"973-1008","path":"include/Dataflow/IR/DataflowOps.td","roles":["context","applicability"],"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);\n\n  let hasCustomAssemblyFormat = 1;\n  let hasVerifier = 1;\n}","why":"Definition of dataflow.graph.launch: operand segments (dependencies, valueInputs, streamInputs, memoryInputs, streamOutputs) and result segments (valueResults, memoryResults, trailing NoneType done); fixes the segment indices and the none-typed trailing result the postcondition reads."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"1370-1401","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_well_formedness","context"],"text":"LogicalResult GraphLaunchOp::verify() {\n  FailureOr<ThreadOp> thread = getOwningThread(getOperation());\n  if (failed(thread))\n    return failure();\n\n  if ((*thread).getDomain().getKind() == ThreadDomainKind::DynamicWork &&\n      (!getStreamInputs().empty() || !getStreamOutputs().empty()))\n    return emitOpError(\n        \"dynamic-work thread must not bind graph stream ports to channels\");\n\n  ArrayAttr sourceMaps = getSourceMaps();\n  if (sourceMaps.size() != getStreamInputs().size())\n    return emitOpError(\"source_maps count (\")\n           << sourceMaps.size() << \") must match stream input binding count (\"\n           << getStreamInputs().size() << ')';\n\n  Block &entry = thread->getBody().front();\n  unsigned consumerRank =\n      entry.getNumArguments() - thread->getFunctionType().getNumInputs() - 1;\n  for (auto [index, attr] : llvm::enumerate(sourceMaps)) {\n    AffineMap map = cast<AffineMapAttr>(attr).getValue();\n    if (map.getNumDims() != consumerRank)\n      return emitOpError(\"stream input source_map #\")\n             << index << \" has \" << map.getNumDims()\n             << \" dimensions but consumer thread domain has rank \"\n             << consumerRank;\n    if (map.getNumSymbols() != 0)\n      return emitOpError(\"stream input source_map #\")\n             << index << \" must not contain symbols\";\n  }\n  return success();\n}","why":"GraphLaunchOp::verify requires an owning thread and matches source_maps count and dimensionality to the consumer thread domain rank; confirms that a rank-0 dense thread accepts one affine_map<() -> ()> per stream input binding, which the generated stream-input candidate relies on."},{"file_sha256":"05567d70fd335a83ee2f46b2d0a3025a903207a88602a798b1845033e7f8ef64","kind":"implementation","lines":"910-919","path":"lib/Frontend/Lowering/LowerForToGraphPass.cpp","roles":["applicability"],"text":"this, \"parallel-completion-candidate-inspections\",\n      \"Number of parallel completion candidates inspected for publication\"};\n\n  ::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.\";\n  }","why":"Pass argument loom-lower-for-to-graph and its description (publish explicit loom.spatial_region as dataflow.graph definitions plus dataflow.graph.launch ops); evidence that the sampled stage is the producer of the constrained output construct, recorded in subject-command.json."},{"file_sha256":"7f380008fb405f6cf8d60d16d1b5980dc1d2e694f9842bcfeb6538fbcfa01099","kind":"implementation","lines":"1-12","path":"lib/Frontend/Lowering/Pipeline.cpp","roles":["applicability"],"text":"// Pipeline glue and pass-registry hooks for the SCF-to-DFG lowering\n// passes. The standard pipeline runs:\n//\n//     loom-lower-for-to-graph           (module-level)\n//\n// `loom-lower-for-to-graph` owns the atomic publication transaction. It\n// consumes explicit loom.spatial_region candidates, runs graph finalization\n// on a scratch module, validates the native result, and publishes only the\n// completed module. Graph memref-copy expansion is part of that finalization,\n// so a copy the current profile cannot expand fails the transaction instead of\n// reaching the published program.\n//","why":"Pipeline note that loom-lower-for-to-graph owns the atomic publication transaction at module level; supports running the single pass flag as the appropriate subject command for this claim."},{"file_sha256":"c25a72ad99349973a47f2a1e081b6b269920e25cc5f59f74619c2e7ce0c2b65d","kind":"test","lines":"1-52","path":"test/raise/scf-to-dfg-explicit-spatial-ownership.mlir","roles":["input_construction"],"text":"// RUN: loom-raise-opt --loom-lower-for-to-graph %s | FileCheck %s --implicit-check-not=@g_host_container_0 --implicit-check-not=@g_instruction_only_0\n\n// CHECK-LABEL: func.func @host_container\n// CHECK: scf.for\n// CHECK-NOT: dataflow.graph\n// CHECK: return\n\n// CHECK-LABEL: dataflow.thread private @instruction_only domain(#dataflow.thread_domain<dense>)\n// CHECK-NOT: dataflow.graph.launch\n// CHECK: memref.store\n// CHECK: dataflow.thread.yield\n\n// CHECK-LABEL: dataflow.thread private @selected_spatial domain(#dataflow.thread_domain<dense>)\n// CHECK: dataflow.graph.launch @selected_graph\n// CHECK: dataflow.thread.yield\n\n// CHECK-LABEL: dataflow.graph private @selected_graph\n// CHECK: dataflow.store\n// CHECK: dataflow.graph.return\n// CHECK-NOT: loom.spatial_region\n\nfunc.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 spelling of a module with dataflow.thread definitions and one explicit loom.spatial_region carrying a value input and a memory import, run under the same single pass flag; template for the generator's thread header, ctrl argument, segment attributes, and graph_name."},{"file_sha256":"df76d22d1149cf2929b700df6f97b58d27b64d523346cfbb4dbf9ba8e66baa49","kind":"test","lines":"60-78","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  }","why":"Accepted spelling of a candidate region nested in scf.for and scf.if inside a dense thread, including the empty-boundary region form; used for the generator's wrapping alternatives and its no-operand region."},{"file_sha256":"3e2863717e0d5713893e5cabfb8e646c854432da0abd1478ee022ec7a610e62f","kind":"test","lines":"50-63","path":"test/raise/scf-to-dfg-atomic-publication.mlir","roles":["input_construction"],"text":"//--- channel.mlir\ndataflow.thread private @channel_sender domain(#dataflow.thread_domain<dense>)(\n    %channel: !dataflow.channel<i32>, %message: i32) ctrl (%start: none) {\n  \"loom.spatial_region\"(%message, %channel)\n      <{operandSegmentSizes = array<i32: 1, 0, 0, 1>,\n        resultSegmentSizes = array<i32: 0, 0>}> ({\n    ^bb0(%payload: i32, %output: !dataflow.channel<i32>):\n      dataflow.channel.send %output, %payload : !dataflow.channel<i32>\n      \"loom.spatial_yield\"()\n          <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n  }) {graph_name = \"channel_graph\", source_maps = []} :\n      (i32, !dataflow.channel<i32>) -> ()\n  dataflow.thread.yield\n}","why":"Accepted spelling of a candidate binding one stream output channel with dataflow.channel.send inside the region and empty source_maps; used for the generator's stream-output form."},{"file_sha256":"bfda65ce4ab1fbf593346cedc9a461eaf02f9cbe97b6f04ebe63767917328c82","kind":"test","lines":"264-281","path":"test/raise/scf-to-dfg-stream-boundary.mlir","roles":["input_construction"],"text":"dataflow.thread private @stream_consumer domain(#dataflow.thread_domain<dense>)(\n      %input: !dataflow.channel<i32>, %memory: memref<1xi32>)\n      ctrl (%ctrl: none) {\n    \"loom.spatial_region\"(%input, %memory)\n        <{operandSegmentSizes = array<i32: 0, 1, 1, 0>,\n          resultSegmentSizes = array<i32: 0, 0>}> ({\n      ^bb0(%channel: !dataflow.channel<i32>, %target: memref<1xi32>):\n        %message = dataflow.channel.receive %channel\n            : !dataflow.channel<i32>\n        %zero = arith.constant 0 : index\n        memref.store %message, %target[%zero] : memref<1xi32>\n        \"loom.spatial_yield\"()\n            <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n    }) {\n      graph_name = \"consumer_graph\",\n      source_maps = [affine_map<() -> ()>]\n    } : (!dataflow.channel<i32>, memref<1xi32>) -> ()\n    dataflow.thread.yield","why":"Accepted spelling of a stream input binding with dataflow.channel.receive and source_maps = [affine_map<() -> ()>] plus a memory import; used for the generator's stream-input form so the launch stream-input segment is exercised."}],"primary_bundle_sha256":"486f3a8b33a9aeda0bd04f5ff378d543f7271c0584f5a80467852d07e51e455b","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"25b1dbc5743cf095b0fa2d3852c6015cab9497fcfc4f2db247928182260cc57d"}
generator source-blind backtranslation · sessions/reverse-generator/session-evidence/result-events.json
[
  {
    "api_error_status": null,
    "duration_api_ms": 59137,
    "duration_ms": 59177,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 1622,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 5201,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.16337,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 4454,
        "provider": "firstParty",
        "thinkingTokens": 1544,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "## Preconditions\n\n1. A valid input is a single top-level `module { ... }` whose body contains only `dataflow.thread` definitions and nothing else.\n2. Each thread is a private symbol definition of the form `dataflow.thread private @NAME domain(#dataflow.thread_domain<dense>)(...) ctrl (...) { ... }`, i.e. a thread must carry an explicit domain attribute, a data-argument list, and a separate control-argument list.\n3. Every thread's data-argument list declares exactly four arguments in the fixed order `%value: i32`, `%mem: memref<4xi32>`, `%chan: !dataflow.channel<i32>`, `%flag: i1`, and its control list declares exactly one argument `%start: none`.\n4. Every thread body is terminated by `dataflow.thread.yield` with no operands.\n5. Every thread body begins by materialising the index constants it may need \u2014 `arith.constant 0 : index`, `arith.constant 1 : index`, `arith.constant 4 : index` \u2014 before any nested scope or region that uses them, so all index operands are dominated by their definitions.\n6. Each thread body contains exactly one `loom.spatial_region` operation; a thread never contains zero regions and never contains two or more.\n7. The `loom.spatial_region` is written in generic (quoted-op) form and must carry both `operandSegmentSizes = array<i32: a, b, c, d>` and `resultSegmentSizes = array<i32: e, f>` as inherent properties in a `<{...}>` clause.\n8. The four operand segments are positional and ordered as value inputs, stream inputs, memory imports, stream outputs; the operand list of the op must match that ordering and the segment counts must sum to the number of operands supplied.\n9. The entry block `^bb0` of the region takes exactly one argument per region operand, in the same order and with the same type as the corresponding operand (i32 for value inputs, `!dataflow.channel<i32>` for stream bindings, `memref<4xi32>` for memory imports), and takes no arguments at all when the operand list is empty.\n10. The region body is terminated by a `loom.spatial_yield` operation, also in generic form, carrying its own `operandSegmentSizes = array<i32: p, q>`; the number of values it yields equals the first entry of the region's `resultSegmentSizes`, and both are `0` for a region with no results.\n11. The trailing function type of the generic `loom.spatial_region` op must agree exactly with the operand types and result types (e.g. `(i32, memref<4xi32>) -> ()`, `(i32) -> i32`, `() -> ()`).\n12. Every `loom.spatial_region` carries a `graph_name` string attribute and a `source_maps` array attribute, both mandatory.\n13. `source_maps` is non-empty exactly when the region binds a stream input (one affine map per such binding, here `affine_map<() -> ()>`); regions with no stream input carry `source_maps = []`.\n14. All operands of `loom.spatial_region` are SSA values defined in the enclosing thread (its block arguments), never values produced inside the region.\n15. Region operations that perform channel traffic \u2014 `dataflow.channel.send` and `dataflow.channel.receive` on a stream-bound block argument \u2014 occur only when the `loom.spatial_region` sits directly in the thread body and is not enclosed in any structured-control-flow scope; a region nested inside `scf.for` or `scf.if` never binds a channel and never contains channel send/receive.\n16. Permitted enclosing scopes for the region are only `scf.for` and `scf.if`, possibly an `scf.if` nested inside an `scf.for`; both are result-free forms with implicit terminators, the `scf.for` bounds and step being index values defined in the thread body and the `scf.if` condition being an `i1` value defined in the thread body.\n17. `memref.store` inside a region stores an i32 value into a memory-import block argument at a locally defined constant index within the `memref<4xi32>` bounds, and its types match the memref element type.\n18. `dataflow.channel.send` sends a value of the channel's element type on a stream-output binding, and `dataflow.channel.receive` produces a value of the channel's element type from a stream-input binding.\n19. Values produced by a region (when `resultSegmentSizes` declares one) need not be consumed; an unused region result is well formed.\n20. Thread arguments need not all be used; `%start`, `%flag`, `%chan`, and `%mem` may be left unreferenced in a given thread.\n\n## Sampling conventions\n\n1. The module contains between one and three thread definitions inclusive, never zero and never more than three.\n2. Threads are named by a zero-based counter, `@thread_0`, `@thread_1`, `@thread_2`, in emission order.\n3. The `graph_name` attribute of a thread's region reuses that same counter, `\"graph_0\"`, `\"graph_1\"`, `\"graph_2\"`, so graph names are unique per module and tied to the thread index rather than being independently chosen.\n4. Each thread independently draws one of exactly four nesting shapes: no wrapper; a single `scf.for`; a single `scf.if`; or an `scf.if` nested inside an `scf.for` \u2014 nesting depth never exceeds two and no other control-flow op (e.g. `scf.while`, `scf.parallel`, `scf.execute_region`, branches) is ever emitted.\n5. The `scf.for` is always the fixed loop `scf.for %i = %c0 to %c4 step %c1` (trip count 4, unit step), and the `scf.if` always tests the thread's `%flag` argument and has no `else` region.\n6. All three index constants `%c0 = 0`, `%c1 = 1`, `%c4 = 4` are emitted in every thread even when the chosen nesting shape uses none of them.\n7. Each thread independently draws one of exactly five region forms: a store form (value input plus memory import, no results), an empty form (no operands, no results), a stream-output form (value input plus outgoing channel), a value form (one value input, one i32 result), and a stream-input form (incoming channel plus memory import).\n8. When nesting is present, the two channel-using forms are replaced deterministically rather than resampled: the stream-output form degrades to the empty form, and the stream-input form degrades to the store form, so nested threads only ever show the store, empty, or value forms.\n9. Region body contents are fixed per form: the store form does one `memref.store` of the payload at index 0; the empty form has an empty entry block; the stream-output form does one `dataflow.channel.send`; the value form computes `arith.addi %payload, %payload`; the stream-input form does one `dataflow.channel.receive` followed by a `memref.store` at index 0.\n10. Region interfaces are limited to at most two operands and at most one result; the second result segment is always `0`, and no region ever combines a stream input with a stream output or uses more than one binding of a given kind.\n11. Only the segment patterns `1,0,1,0`, `0,0,0,0`, `1,0,0,1`, `1,0,0,0` and `0,1,1,0` are emitted; other admissible operand mixes are never produced.\n12. The single result-producing form names its result `%sum_N` using the thread index and leaves it unused; no consumer of a region result is ever emitted.\n13. `loom.spatial_region` and `loom.spatial_yield` are always printed in generic quoted form with explicit `<{...}>` property dictionaries, while `arith`, `memref`, `scf`, and `dataflow` operations are always printed in their custom assembly form.\n14. Types are monomorphic throughout: payload type is always `i32`, memory type always `memref<4xi32>`, channel type always `!dataflow.channel<i32>`, index constants always `index`, and the condition always `i1`.\n15. SSA names are fixed per position: thread arguments `%value`, `%mem`, `%chan`, `%flag`, `%start`; loop induction variable `%i`; region block arguments `%payload`, `%memory`, `%output`, `%channel`, `%target`; region-local values `%zero`, `%doubled`, `%message`.\n16. The only affine map ever emitted in `source_maps` is the nullary `affine_map<() -> ()>`, and only in the stream-input form.\n17. Indentation is a fixed skeleton \u2014 two spaces for the thread, four for body operations and wrappers, six for the region op and its attributes \u2014 and the region's own indentation does not change with nesting depth.\n18. No function definitions, global declarations, module attributes, location information, or top-level operations other than `dataflow.thread` are emitted, and the module carries no symbol-visibility or target attributes.",
    "result_index": 0,
    "session_id": "838c9d42-b175-44e4-a126-2e25e1fcdff7",
    "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": 42,
    "total_cost_usd": 0.16337,
    "ttft_ms": 24343,
    "ttft_stream_ms": 1096,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 5201,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 5201,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 4454,
      "output_tokens_details": {
        "thinking_tokens": 1544
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "93141c5b-4bf9-4cd0-9a06-8d9b5a1f6b40"
  }
]
postcondition source-blind backtranslation · sessions/reverse-postcondition/session-evidence/result-events.json
[
  {
    "api_error_status": null,
    "duration_api_ms": 15939,
    "duration_ms": 15968,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 2250,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 6024,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.084925,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 987,
        "provider": "firstParty",
        "thinkingTokens": 436,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "This postcondition looks only at the `output` program; the `input` program is never consulted, and no value source outside `output.operations` is used. It selects two flat sequences from every operation at any depth: all ops named `dataflow.thread` and all ops named `dataflow.graph.launch`, then universally quantifies over the launches, so a program containing no `dataflow.graph.launch` operation passes every assert vacuously, and the `dataflow.thread` sequence matters only as a container pool. For each launch it demands that some thread op structurally contains it, and that resolving the launch's `callee` symbol attribute against the output yields at least one operation whose name is `dataflow.graph`; zero resolutions, or resolutions that are all named something else, reject.\n\nIt then decodes the launch's `operandSegmentSizes` into five segments and its `resultSegmentSizes` into three, which requires those properties to be present on the op. Operand segment 0 must contain only values of the `none` type, and operand segments 2 and 4 must contain only values whose type kind is exactly `\"!dataflow.channel\"`; segments 1 and 3 are unconstrained in type, and any of these per-value checks passes trivially when its segment is empty. The five operand segment sizes must sum exactly to the launch's operand count, and the three result segment sizes must sum exactly to its result count, so hidden or double-counted positions reject. Result segment 2 must hold exactly one value, that value must have type `none`, and it must equal the value obtained by dropping all but the final entry of the launch's result list, so a `none`-typed single done result placed anywhere other than last rejects; result segments 0 and 1 are checked only through the total-count sum.",
    "result_index": 0,
    "session_id": "2ba82cbd-18d4-4845-adf2-c03e485293f3",
    "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": 29,
    "total_cost_usd": 0.084925,
    "ttft_ms": 8436,
    "ttft_stream_ms": 1707,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 6024,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 6024,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 987,
      "output_tokens_details": {
        "thinking_tokens": 436
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "2bba40bb-ef37-47a7-a057-6b457bd7c73e"
  }
]

Activation review

This paired revision was activated by an explicit partial-scope team review bound to both executable artifact hashes.

Approved to run and display existing artifacts; accuracy and completeness are measured separately.

Run and triage

Work progress