MLIR passage 4: Graph bodies exclude calls and nested callables

{"entries":[{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"457-494","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","input_construction"],"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 obligation: fixes the callable kinds (llvm.func, func.func, dataflow.thread, dataflow.graph), the roles of loom.spatial_region, dataflow.thread, dataflow.graph.launch and dataflow.thread.launch, so the generator builds module-scope thread definitions owning explicit spatial candidates and the postcondition names exactly the excluded constructs."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"23-26","path":"docs/spec-compiler-part-3-dfg.md","roles":["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 graph definition and launch only on complete success; this is why every sampled input places the candidate inside a thread definition and why fail-closed samples publish nothing."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"499-506","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","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":"An llvm.call/func.call in a thread body is an InstructionCore call and may remain when its callee body is graph-free; motivates the optional thread-level func.call site (published graph must still exclude it) and the adversarial call-inside-candidate forms."},{"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 of loom.spatial_region (value inputs, stream inputs, memory inputs, stream outputs; value then memory results) and the source_map requirement; determines the operandSegmentSizes/resultSegmentSizes and source_maps the generator 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":"Nested scf.if completion propagation is supported, so candidate sites are sampled under scf.if as well as at thread top level."},{"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; justifies sampling one or two candidate sites per thread and a branch-shaped candidate body."},{"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; justifies sampling candidate sites nested under scf.for and loop-carried arithmetic inside a candidate."},{"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 have no inferred traversal order and fail before publication; the generator therefore never nests a candidate under those forms."},{"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 transparent region boundary may not be justified by a later send; the generator emits no channel send/receive endpoints so no sampled candidate is a deadlocking or incorrectly cut candidate."},{"file_sha256":"73f239de628bbf8d40145ecde732142ffcf6567c9483e6dc2286ae9176a6907c","kind":"language_definition","lines":"8-103","path":"include/Frontend/IR/LoomOps.td","roles":["input_construction","input_well_formedness"],"text":"def Loom_SpatialRegionOp : Loom_Op<\"spatial_region\", [\n    IsolatedFromAbove,\n    SingleBlock,\n    AttrSizedOperandSegments,\n    AttrSizedResultSegments,\n    RecursiveMemoryEffects\n]> {\n  let summary = \"Structured candidate for one SpatialCore graph\";\n  let description = [{\n    Holds one structured candidate inside a `dataflow.thread`. Operands are\n    normalized as value inputs, stream input channels, memory inputs, and\n    stream output channels. Results are normalized as value outputs followed\n    by memory outputs. Each stream input has one affine `source_map`.\n\n    This operation is temporary compiler IR. Successful publication replaces\n    it with one native-valid `dataflow.graph` and its matching launch.\n  }];\n\n  let arguments = (ins\n      Variadic<AnyType>:$valueInputs,\n      Variadic<Dataflow_ChannelType>:$streamInputs,\n      Variadic<AnyType>:$memoryInputs,\n      Variadic<Dataflow_ChannelType>:$streamOutputs,\n      AffineMapArrayAttr:$source_maps,\n      OptionalAttr<StrAttr>:$graph_name);\n\n  let results = (outs\n      Variadic<AnyType>:$valueResults,\n      Variadic<AnyType>:$memoryResults);\n\n  let regions = (region AnyRegion:$body);\n\n  let skipDefaultBuilders = 1;\n  let builders = [\n    OpBuilder<(ins\n        \"::mlir::ValueRange\":$valueInputs,\n        \"::mlir::ValueRange\":$streamInputs,\n        \"::mlir::ValueRange\":$memoryInputs,\n        \"::mlir::ValueRange\":$streamOutputs,\n        \"::mlir::TypeRange\":$valueResultTypes,\n        \"::mlir::TypeRange\":$memoryResultTypes,\n        \"::mlir::ArrayAttr\":$sourceMaps,\n        CArg<\"::mlir::StringAttr\", \"{}\">:$graphName), [{\n      $_state.addOperands(valueInputs);\n      $_state.addOperands(streamInputs);\n      $_state.addOperands(memoryInputs);\n      $_state.addOperands(streamOutputs);\n      $_state.addTypes(valueResultTypes);\n      $_state.addTypes(memoryResultTypes);\n      $_state.addAttribute(\"source_maps\", sourceMaps);\n      if (graphName)\n        $_state.addAttribute(\"graph_name\", graphName);\n      auto &properties = $_state.getOrAddProperties<Properties>();\n      properties.operandSegmentSizes = {\n          static_cast<int32_t>(valueInputs.size()),\n          static_cast<int32_t>(streamInputs.size()),\n          static_cast<int32_t>(memoryInputs.size()),\n          static_cast<int32_t>(streamOutputs.size())};\n      properties.resultSegmentSizes = {\n          static_cast<int32_t>(valueResultTypes.size()),\n          static_cast<int32_t>(memoryResultTypes.size())};\n      $_state.addRegion();\n    }]>\n  ];\n\n  let hasVerifier = 1;\n}\n\ndef Loom_SpatialYieldOp : Loom_Op<\"spatial_yield\", [\n    Terminator,\n    ParentOneOf<[\"::loom::SpatialRegionOp\"]>,\n    AttrSizedOperandSegments,\n    Pure\n]> {\n  let summary = \"Yield value and memory results from a spatial candidate\";\n\n  let arguments = (ins\n      Variadic<AnyType>:$values,\n      Variadic<AnyType>:$memories);\n\n  let skipDefaultBuilders = 1;\n  let builders = [\n    OpBuilder<(ins\n        \"::mlir::ValueRange\":$values,\n        \"::mlir::ValueRange\":$memories), [{\n      $_state.addOperands(values);\n      $_state.addOperands(memories);\n      auto &properties = $_state.getOrAddProperties<Properties>();\n      properties.operandSegmentSizes = {\n          static_cast<int32_t>(values.size()),\n          static_cast<int32_t>(memories.size())};\n    }]>\n  ];\n\n  let hasVerifier = 1;\n}","why":"Definition of loom.spatial_region and loom.spatial_yield: AttrSizedOperandSegments/AttrSizedResultSegments, the four operand segments, the AffineMapArrayAttr source_maps and optional graph_name, and the terminator's two operand segments; fixes the exact generic-form spelling emitted by the grammar."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"614-620,767-773,839-845,973-979","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"text":"def Dataflow_ThreadOp : Dataflow_Op<\"thread\", [\n    AutomaticAllocationScope,\n    IsolatedFromAbove,\n    HasParent<\"::mlir::ModuleOp\">,\n    SingleBlockImplicitTerminator<\"ThreadYieldOp\">,\n    FunctionOpInterface,\n    RecursiveMemoryEffects\ndef Dataflow_ThreadLaunchOp : Dataflow_Op<\"thread.launch\", [\n    AttrSizedOperandSegments,\n    DeclareOpInterfaceMethods<SymbolUserOpInterface>\n]> {\n  let summary = \"Async launch of a dataflow.thread callable\";\n  let description = [{\n    References a `dataflow.thread` definition by symbol and supplies\ndef Dataflow_GraphOp : Dataflow_Op<\"graph\", [\n    IsolatedFromAbove,\n    HasParent<\"::mlir::ModuleOp\">,\n    SingleBlockImplicitTerminator<\"GraphReturnOp\">,\n    FunctionOpInterface,\n    RecursiveMemoryEffects,\n    DeclareOpInterfaceMethods<RegionKindInterface>\ndef Dataflow_GraphLaunchOp : Dataflow_Op<\"graph.launch\", [\n    AttrSizedOperandSegments,\n    AttrSizedResultSegments,\n    DeclareOpInterfaceMethods<SymbolUserOpInterface>\n]> {\n  let summary = \"Asynchronous launch of a dataflow.graph callable\";\n  let description = [{","why":"Canonical op-name spellings dataflow.thread, dataflow.thread.launch, dataflow.graph and dataflow.graph.launch used verbatim in the generated thread definitions and in the postcondition's name tests."},{"file_sha256":"4295a7f0089a5b35f7f7f538032b31f51ca3966d4279faa030a2d493a8f76385","kind":"verifier","lines":"262-303","path":"lib/Frontend/Lowering/GraphRegionLowering.cpp","roles":["input_well_formedness"],"text":"}\n    if (::llvm::isa<::mlir::scf::SCFDialect>(op->getDialect()) &&\n        !::llvm::isa<::mlir::scf::IfOp, ::mlir::scf::ForOp,\n                     ::mlir::scf::WhileOp, ::mlir::scf::IndexSwitchOp,\n                     ::mlir::scf::ParallelOp, ::mlir::scf::ForallOp,\n                     ::mlir::scf::YieldOp, ::mlir::scf::ConditionOp,\n                     ::mlir::scf::ReduceOp, ::mlir::scf::InParallelOp>(op)) {\n      op->emitError(\"loom-lower-graph-memory: unsupported residual SCF \"\n                    \"must be normalized before graph-region lowering\");\n      return ::mlir::WalkResult::interrupt();\n    }\n    bool modeled =\n        ::loom::lowering::detail::isGraphRegionControlOperation(op) ||\n        ::loom::lowering::classifyGraphLoweringLeaf(op) !=\n            ::loom::lowering::GraphLeafLowering::Unsupported;\n    if (::llvm::isa<::dataflow::ChannelSendOp, ::dataflow::ChannelReceiveOp>(\n            op))\n      modeled = boundary.isTransient();\n    // A registered actor that no capability covers is reported for what it is,\n    // so an effectful memory actor is not mistaken for an unregistered one.\n    if (!modeled && ::dataflow::isCanonicalDataflowActor(op)) {\n      op->emitError() << \"loom-lower-graph-memory: canonical Dataflow actor '\"\n                      << op->getName().getStringRef()\n                      << \"' has no graph-region lowering\";\n      return ::mlir::WalkResult::interrupt();\n    }\n    if (!modeled && (op->getNumRegions() != 0 || op->getNumSuccessors() != 0)) {\n      op->emitError()\n          << \"loom-lower-graph-memory: effectful or unmodeled graph \"\n             \"operation '\"\n          << op->getName().getStringRef() << \"' is unsupported\";\n      return ::mlir::WalkResult::interrupt();\n    }\n    if (!modeled) {\n      op->emitError()\n          << \"loom-lower-graph-memory: operation '\"\n          << op->getName().getStringRef()\n          << \"' is not a registered canonical Dataflow actor or a supported \"\n             \"graph-lowering operation\";\n      return ::mlir::WalkResult::interrupt();\n    }\n    return ::mlir::WalkResult::advance();","why":"Acceptance rule for operations inside a candidate: only supported SCF control forms and registered canonical Dataflow actors or supported graph-lowering leaves survive. Determines which body ops (arith, memref.store, llvm.freeze, scf.if/scf.for) the grammar samples as publishable and which calls fail closed."},{"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":"loom-lower-for-to-graph owns the atomic publication transaction that consumes explicit loom.spatial_region candidates and publishes the completed module; evidence that this flag is the stage whose output the obligation constrains."},{"file_sha256":"05567d70fd335a83ee2f46b2d0a3025a903207a88602a798b1845033e7f8ef64","kind":"implementation","lines":"905-919","path":"lib/Frontend/Lowering/LowerForToGraphPass.cpp","roles":["applicability"],"text":"LowerForToGraphPass() = default;\n  LowerForToGraphPass(const LowerForToGraphPass &) : PassWrapper() {}\n\n  Statistic parallelCompletionCandidateInspections{\n      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":"The pass argument string loom-lower-for-to-graph and its description (publish loom.spatial_region as dataflow.graph definitions plus dataflow.graph.launch ops) confirm the subject-command flag and the output population selected by the postcondition."},{"file_sha256":"c25a72ad99349973a47f2a1e081b6b269920e25cc5f59f74619c2e7ce0c2b65d","kind":"example","lines":"22-52","path":"test/raise/scf-to-dfg-explicit-spatial-ownership.mlir","roles":["input_construction"],"text":"func.func @host_container(%target: memref<4xi32>, %value: i32) {\n  %zero = arith.constant 0 : index\n  %four = arith.constant 4 : index\n  %one = arith.constant 1 : index\n  scf.for %index = %zero to %four step %one {\n    memref.store %value, %target[%index] : memref<4xi32>\n  }\n  return\n}\n\ndataflow.thread private @instruction_only domain(#dataflow.thread_domain<dense>)(\n    %target: memref<1xi32>, %value: i32) ctrl (%ctrl: none) {\n  %zero = arith.constant 0 : index\n  memref.store %value, %target[%zero] : memref<1xi32>\n  dataflow.thread.yield\n}\n\ndataflow.thread private @selected_spatial domain(#dataflow.thread_domain<dense>)(\n    %target: memref<1xi32>, %value: i32) ctrl (%ctrl: none) {\n  \"loom.spatial_region\"(%value, %target)\n      <{operandSegmentSizes = array<i32: 1, 0, 1, 0>,\n        resultSegmentSizes = array<i32: 0, 0>}> ({\n    ^bb0(%payload: i32, %memory: memref<1xi32>):\n      %zero = arith.constant 0 : index\n      memref.store %payload, %memory[%zero] : memref<1xi32>\n      \"loom.spatial_yield\"()\n          <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n  }) {graph_name = \"selected_graph\", source_maps = []} :\n      (i32, memref<1xi32>) -> ()\n  dataflow.thread.yield\n}","why":"Accepted spelling of a module with a host func.func, a dataflow.thread with dense domain and ctrl argument, and a value+memory loom.spatial_region candidate; used as the skeleton for the generated modules."},{"file_sha256":"fa58edd15b93582934f4f94945c053d793a5b1edefdfdcbadbd37e0be4e7dc6d","kind":"example","lines":"9-20","path":"test/raise/freeze-candidate-finalization.mlir","roles":["input_construction"],"text":"dataflow.thread private @selected_freeze domain(#dataflow.thread_domain<dense>)(%input: i32) ctrl (%start: none) {\n  %result = \"loom.spatial_region\"(%input)\n      <{operandSegmentSizes = array<i32: 1, 0, 0, 0>,\n        resultSegmentSizes = array<i32: 1, 0>}> ({\n    ^bb0(%value: i32):\n      %stable = llvm.freeze %value : i32\n      \"loom.spatial_yield\"(%stable)\n          <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n  }) {graph_name = \"selected_freeze_graph\", source_maps = []} :\n      (i32) -> i32\n  dataflow.thread.yield\n}","why":"Accepted spelling of a single-value-input candidate with one value result (llvm.freeze body); basis for the value-result region forms."},{"file_sha256":"df76d22d1149cf2929b700df6f97b58d27b64d523346cfbb4dbf9ba8e66baa49","kind":"example","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 site nested under scf.for and scf.if inside a thread whose input terminator is a bare dataflow.thread.yield; basis for the nesting variants."},{"file_sha256":"3a48482db91f758cf3933d286ceeda00d8a00c1457435fce086635a0ca918a3a","kind":"test","lines":"1-42","path":"test/raise/library-call-candidate-rejection.mlir","roles":["input_construction"],"text":"// RUN: not loom-raise-opt --loom-lower-for-to-graph --mlir-disable-threading --mlir-print-ir-after-failure --mlir-print-ir-module-scope %s 2>&1 | FileCheck %s --implicit-check-not=\"dataflow.graph private\" --implicit-check-not=dataflow.graph.launch\n\n// A library spelling and matching arity do not prove call semantics. The call\n// remains under the imported LLVM declaration and makes only the candidate\n// that selected it for SpatialCore non-finalizable.\n// CHECK: error: loom-lower-graph-memory: operation 'llvm.call' is not a registered canonical Dataflow actor or a supported graph-lowering operation\n// CHECK-LABEL: llvm.func @arm_nn_vec_mat_mult_t_s8\n// CHECK-LABEL: dataflow.thread private @selected_library_call domain(#dataflow.thread_domain<dense>)\n// CHECK: loom.spatial_region\n// CHECK: llvm.call @arm_nn_vec_mat_mult_t_s8\n\nllvm.func @arm_nn_vec_mat_mult_t_s8(i32, i32, i32, i32, i32, i32, i32,\n                                    i32, i32, i32, i32, i32, i32, i32,\n                                    i32) -> i32\n\ndataflow.thread private @selected_library_call domain(#dataflow.thread_domain<dense>)(\n    %arg0: i32, %arg1: i32, %arg2: i32, %arg3: i32, %arg4: i32,\n    %arg5: i32, %arg6: i32, %arg7: i32, %arg8: i32, %arg9: i32,\n    %arg10: i32, %arg11: i32, %arg12: i32, %arg13: i32, %arg14: i32)\n    ctrl (%start: none) {\n  %status = \"loom.spatial_region\"(\n      %arg0, %arg1, %arg2, %arg3, %arg4, %arg5, %arg6, %arg7, %arg8,\n      %arg9, %arg10, %arg11, %arg12, %arg13, %arg14)\n      <{operandSegmentSizes = array<i32: 15, 0, 0, 0>,\n        resultSegmentSizes = array<i32: 1, 0>}> ({\n    ^bb0(%value0: i32, %value1: i32, %value2: i32, %value3: i32,\n         %value4: i32, %value5: i32, %value6: i32, %value7: i32,\n         %value8: i32, %value9: i32, %value10: i32, %value11: i32,\n         %value12: i32, %value13: i32, %value14: i32):\n      %result = llvm.call @arm_nn_vec_mat_mult_t_s8(\n          %value0, %value1, %value2, %value3, %value4, %value5, %value6,\n          %value7, %value8, %value9, %value10, %value11, %value12,\n          %value13, %value14)\n          : (i32, i32, i32, i32, i32, i32, i32, i32, i32, i32, i32,\n             i32, i32, i32, i32) -> i32\n      \"loom.spatial_yield\"(%result)\n          <{operandSegmentSizes = array<i32: 1, 0>}> : (i32) -> ()\n  }) {graph_name = \"selected_library_call_graph\", source_maps = []} :\n      (i32, i32, i32, i32, i32, i32, i32, i32, i32, i32, i32, i32,\n       i32, i32, i32) -> i32\n  dataflow.thread.yield\n}","why":"Evidence that a call selected into a candidate makes the publication transaction fail closed rather than publishing a graph containing the call; supports sampling those adversarial forms at a low rate as direct falsification attempts for the obligation."}],"primary_bundle_sha256":"e5045156ba6a108940f1e743febf4bd26c9d4ddf6c59857d83f7f0c30b3798e1","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"239f291d7a3a7fbe0ba28026177beb1ab089ca6189bb4fde208e11bfe6c6892d"}

[
  {
    "api_error_status": null,
    "duration_api_ms": 45196,
    "duration_ms": 45258,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 1480,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 6504,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.1525,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 3498,
        "provider": "firstParty",
        "thinkingTokens": 273,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "## Preconditions\n\n1. Every emitted program is a single top-level `module { ... }` whose body contains, in this order, a `func.func` definition, an `llvm.func` declaration, a `func.func` host function, and one or more `dataflow.thread` definitions.\n2. Every program defines `func.func @helper_double(%a: i32) -> i32` whose body is `arith.addi %a, %a : i32` followed by `return`, i.e. a callee containing no graph or region construct.\n3. Every program declares the external symbol `llvm.func @extern_scale(i32) -> i32` with no body.\n4. Every program defines `func.func @host_container(%target: memref<4xi32>, %value: i32)` containing three `arith.constant ... : index` values (0, 4, 1), an `scf.for` over them whose body is a single `memref.store %value, %target[%hi] : memref<4xi32>`, and a bare `return`; this function contains no `loom.spatial_region`.\n5. Every `dataflow.thread` is declared `private`, carries `domain(#dataflow.thread_domain<dense>)`, takes exactly the argument list `(%mem: memref<4xi32>, %val: i32, %flag: i1)`, and has a control operand list `ctrl (%start: none)`.\n6. Every thread body begins with exactly three index constants bound to `%lo` = 0, `%hi` = 2, `%stp` = 1, before any other operation.\n7. Every thread body ends with `dataflow.thread.yield` as its terminator.\n8. Every thread body contains at least one `loom.spatial_region` operation.\n9. Every `loom.spatial_region` appears inside a `dataflow.thread` body, either directly at the thread's top level or nested exactly one level inside a structured `scf.if` or `scf.for` of that thread; regions are never nested inside one another and never appear in `func.func` or `llvm.func` bodies.\n10. Any `scf.if` wrapping a region is predicated on the thread argument `%flag` of type `i1` and has no results and no `else` branch; any `scf.for` wrapping a region iterates from `%lo` to `%hi` step `%stp` using the thread-level index constants and carries no iteration arguments.\n11. Every `loom.spatial_region` is written in generic operation form with a `<{operandSegmentSizes = array<i32: ...>, resultSegmentSizes = array<i32: ...>}>` properties dictionary, a single entry block region, and a trailing discardable attribute dictionary.\n12. The `operandSegmentSizes` array of each region has exactly four entries and the `resultSegmentSizes` array exactly two entries, and both sum-match the actual operand list and result list of the region's functional type signature.\n13. Every region's entry block `^bb0` has one block argument per region operand, with matching types, and those block arguments are the only values flowing into the region body from outside.\n14. Every region body is terminated by a `\"loom.spatial_yield\"` operation in generic form with its own two-entry `operandSegmentSizes` array, whose operand count and types match the region's result count and types.\n15. Region operands are drawn only from the enclosing thread's own arguments (`%val` of type `i32`, `%mem` of type `memref<4xi32>`, `%flag` of type `i1`), never from values defined earlier in the thread body or from another region's results.\n16. Every `loom.spatial_region` carries exactly the two discardable attributes `graph_name` (a string) and `source_maps` (an empty array), and the `graph_name` value is unique across the whole module.\n17. Region results, when present, are bound to SSA names that are unique across the whole module.\n18. Regions that yield no value produce no SSA result and are written as a bare operation of type `... -> ()`.\n19. Any memory access inside a region body addresses only a `memref<4xi32>` passed in as a region operand, indexed by a constant defined inside that region body, never by an index constant defined in the enclosing thread.\n20. Calls occurring inside a region body target only symbols declared at module scope (`@helper_double` via `func.call`, `@extern_scale` via `llvm.call`), and the same is true of any call placed in a thread body outside a region.\n21. A `func.call` to `@helper_double` may appear directly in a thread body, positioned after the thread's index constants and before the first region site.\n22. Control flow inside a region body is limited to structured `scf.if` with both branches and `scf.yield`, or `scf.for` with `iter_args` and `scf.yield`; no unstructured branches, no multi-block regions beyond `^bb0` plus structured nesting.\n23. All integer values in the program are `i32` except the predicate `%flag`/`%c`, which is `i1`, and all loop bounds and memref indices, which are `index`.\n24. Thread symbol names, graph names and region result names are correlated: no two threads share a symbol name and no two regions share either a graph name or a result name.\n\n## Sampling conventions\n\n1. The number of `dataflow.thread` definitions is exactly 1 or 2.\n2. Threads are named `@thread_0` and, if present, `@thread_1`, using a counter starting at 0 and incremented per thread.\n3. Each thread contains exactly 1 or 2 region sites, chosen independently per thread, so a module holds between 1 and 4 regions in total.\n4. A single module-wide counter starting at 0 numbers the regions in emission order, producing result names `%r0, %r1, ...` and graph names `\"graph_0\", \"graph_1\", ...\"`; the counter is shared across threads rather than reset per thread.\n5. The counter is incremented once per region site, including for the value-less memory form that emits no `%r` name, so graph-name indices may skip values used by no SSA result.\n6. Whether a thread contains the top-level `func.call @helper_double(%val)` is an independent binary choice per thread; when present it is emitted exactly once, bound to `%icall`, and its result is never used.\n7. The nesting of each site is chosen from exactly three options \u2014 no nesting, an `scf.if %flag` wrapper, or an `scf.for` wrapper \u2014 with the un-nested form sampled at twice the weight of each wrapper.\n8. Each site's region contents are chosen from exactly six fixed bodies: pure arithmetic value-in/value-out, value-plus-memref store with no result, internal `scf.if` selection, `llvm.freeze`, internal `scf.for` with `iter_args`, and an in-region call; the first five are sampled at twice the weight of the call form.\n9. The in-region call form further chooses uniformly between `func.call @helper_double` and `llvm.call @extern_scale`.\n10. The arithmetic body is fixed as `%s = arith.addi %a, %a` then `%p = arith.muli %s, %a`, yielding `%p`.\n11. The memory body is fixed as a zero `index` constant followed by `memref.store %payload, %memory[%z]`, yielding nothing, and it is the only form whose `operandSegmentSizes` is `array<i32: 1, 0, 1, 0>` and `resultSegmentSizes` is `array<i32: 0, 0>`.\n12. The branch body is fixed as `scf.if %c -> (i32)` with `arith.addi %a, %a` in the then branch and `arith.muli %a, %a` in the else branch; it is the only form taking `%flag` as a region operand and the only one with `operandSegmentSizes = array<i32: 2, 0, 0, 0>`.\n13. The loop body is fixed with constants 0, 2, 1 and a single `arith.addi %carry, %a` accumulation, yielding the loop result.\n14. All value-producing forms use the operand segment layout `array<i32: 1, 0, 0, 0>` and result segment layout `array<i32: 1, 0>`, and never exercise the second, third or fourth operand segments beyond the memory and branch cases above.\n15. `source_maps` is always emitted as the literal empty list `[]`; no non-empty source map is ever generated.\n16. The helper preamble is a constant: exactly one `func.func` callee and one `llvm.func` declaration, both fixed in name, arity and body, regardless of whether any emitted region or thread actually calls them.\n17. The `@host_container` function is a constant preamble with fixed argument names and bounds 0/4/1, and it is emitted exactly once even though nothing calls it.\n18. Memref types are fixed at `memref<4xi32>` and thread-level loop trip counts at 2 (`%lo`=0, `%hi`=2, `%stp`=1) everywhere; no other shape, element type, or bound is ever emitted.\n19. Region-internal SSA names are reused verbatim across regions in distinct scopes (`%a`, `%s`, `%p`, `%z`, `%sel`, `%acc`, `%called`, `%stable`), and wrapper induction variables are always `%iv` inside a thread and `%i` inside a region loop.\n20. Indentation is fixed: thread-level operations at two spaces, wrapped operations and region headers at four, region bodies at six or more; each thread definition is followed by a blank line.\n21. No thread ever emits zero sites, and no program ever emits a region outside a thread, so the empty-thread and host-side-region shapes are never exercised.\n22. Nesting depth is capped at one wrapper level per site; `scf.if` inside `scf.for` or any deeper nesting of sites is never emitted.\n23. No `dataflow.thread` uses a domain other than `dense`, no non-`private` visibility is emitted, and the `ctrl` list always has exactly one `none`-typed operand.",
    "result_index": 0,
    "session_id": "6d6f6fb0-ea77-4120-89f5-2927c8443a0f",
    "stop_reason": "end_turn",
    "subagent_stats": {
      "by_type": {},
      "completed": 0,
      "failed": 0,
      "killed": {
        "parent": 0,
        "system": 0,
        "user": 0
      },
      "max_depth": 0,
      "refused": {
        "budget": 0,
        "concurrency_limit": 0,
        "depth_limit": 0
      },
      "requested": {
        "background": 0,
        "foreground": 0,
        "unset": 0
      },
      "spawned": 0,
      "spawned_by_subagents": 0,
      "started_in_background": 0
    },
    "subtype": "success",
    "terminal_reason": "completed",
    "time_to_request_ms": 62,
    "total_cost_usd": 0.1525,
    "ttft_ms": 4699,
    "ttft_stream_ms": 949,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 6504,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 6504,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 3498,
      "output_tokens_details": {
        "thinking_tokens": 273
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "3b089a98-3054-4240-953a-c975465908aa"
  }
]

[
  {
    "api_error_status": null,
    "duration_api_ms": 10803,
    "duration_ms": 10830,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 1573,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 5538,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.073765,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 735,
        "provider": "firstParty",
        "thinkingTokens": 154,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "This postcondition selects, from the subject's output program only, every operation named `dataflow.graph` at any nesting depth, since `output.operations` enumerates the whole program in pre-order; the `input` program is never consulted, and no attributes, types, operands, results, or symbol references are examined \u2014 the only value source is each operation's `name` string compared against fixed literals. For each selected graph it universally quantifies over `mlir::descendants(g)`, the transitive set of operations strictly inside that graph (the graph op itself is excluded), and asserts six separate `none ... where` conditions over that same descendant set. It rejects a graph whose body transitively contains any operation named `func.func`, `llvm.func`, `dataflow.thread`, or `dataflow.graph` (the first assert), or named `llvm.call`, `func.call`, `dataflow.thread.launch`, `dataflow.graph.launch`, or again `dataflow.graph` (the remaining asserts); a nested `dataflow.graph` therefore trips two asserts, and the sixth assert is subsumed by the first. It accepts any graph whose descendants carry none of those nine names, regardless of what other operations, regions, or blocks appear there, and regardless of how deeply they nest. A graph with an empty body, or with no regions at all, passes every assert, because each `none` quantifier is vacuously true over an empty descendant sequence. If the output program contains no operation named `dataflow.graph`, the enclosing `forall` ranges over an empty sequence and the entire postcondition holds vacuously. Non-vacuous checking occurs exactly when at least one `dataflow.graph` operation exists and has at least one descendant; failure is reported per-graph, per-assert, with the offending descendant operation as the witness.",
    "result_index": 0,
    "session_id": "8cc0758c-2576-418c-a715-d152f7a25e8d",
    "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.073765,
    "ttft_ms": 3523,
    "ttft_stream_ms": 1100,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 5538,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 5538,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 735,
      "output_tokens_details": {
        "thinking_tokens": 154
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "17402c3b-9348-4659-b1a2-e1fc0356c633"
  }
]