MS2V3 mlir-stage-29-v1 passing 5000/5000
Estimated confidence: 100.0%. Conservative lower bound: 89.4% (95% level).
uniform over observed structural partitions. observed partitions; unseen partitions have no supplied target weight. Partitions use recursive production counts and derivation depth. Behavioral classes combine each input’s compiler coverage and assertion decision paths. Catalog partitions with no observations retain maximal missing mass.
Baseline tests: Every tracked test file with a RUN line invoking loom-raise-opt (77 files); other executables and native unit tests excluded
| Source file | Baseline coverage | Baseline + input | Contributing input |
|---|
| derived from the coverage profile | not measured | not measured | no drafts yet |
After recursively lowering before:
E_out;dataflow.gate projects before execution into after phase;W/R is the loop exit state;W/R enters after;SB tails leave the loop; andSB tails enter after."builtin.module"() ({ "dataflow.graph"() <{function_type = (i32, memref<?xi32>, memref<?xi32>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "while_case0", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: i32, %arg2: memref<?xi32>, %arg3: memref<?xi32>): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %3:2 = "scf.while"(%0, %0) ({ ^bb0(%arg6: i32, %arg7: i32): %6 = "arith.index_cast"(%arg6) : (i32) -> index %7 = "memref.load"(%arg2, %6) : (memref<?xi32>, index) -> i32 %8 = "arith.addi"(%arg6, %1) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %9 = "arith.addi"(%arg7, %7) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %10 = "arith.cmpi"(%8, %arg1) <{predicate = 2 : i64}> : (i32, i32) -> i1 "scf.condition"(%10, %8, %9) : (i1, i32, i32) -> () }, { ^bb0(%arg4: i32, %arg5: i32): "scf.yield"(%arg4, %arg5) : (i32, i32) -> () }) : (i32, i32) -> (i32, i32) %4 = "arith.index_cast"(%0) : (i32) -> index "memref.store"(%3#0, %arg3, %4) : (i32, memref<?xi32>, index) -> () %5 = "arith.index_cast"(%1) : (i32) -> index "memref.store"(%3#1, %arg3, %5) : (i32, memref<?xi32>, index) -> () "dataflow.graph.return"(%arg0) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
"builtin.module"() ({ "dataflow.graph"() <{function_type = (i32, memref<?xi32>, memref<?xi32>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "while_case0", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: i32, %arg2: memref<?xi32>, %arg3: memref<?xi32>): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %2 = "arith.index_cast"(%0) : (i32) -> index %3 = "arith.index_cast"(%1) : (i32) -> index %4 = "dataflow.carry"(%17, %arg0, %19#1) : (i1, none, none) -> none %5 = "dataflow.carry"(%17, %0, %23#1) : (i1, i32, i32) -> i32 %6 = "dataflow.carry"(%17, %0, %24#1) : (i1, i32, i32) -> i32 %7 = "dataflow.invariant"(%17, %1) : (i1, i32) -> i32 %8 = "dataflow.invariant"(%17, %arg1) : (i1, i32) -> i32 %9 = "dataflow.carry"(%17, %arg0, %21#1) : (i1, none, none) -> none %10 = "dataflow.carry"(%17, %arg0, %22#1) : (i1, none, none) -> none %11 = "arith.index_cast"(%5) : (i32) -> index %12:2 = "dataflow.sync"(%4, %9) : (none, none) -> (none, none) %13:2 = "dataflow.load"(%arg2, %11, %12#0) : (memref<?xi32>, index, none) -> (i32, none) %14:2 = "dataflow.sync"(%10, %13#1) : (none, none) -> (none, none) %15 = "arith.addi"(%5, %7) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %16 = "arith.addi"(%6, %13#0) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %17 = "arith.cmpi"(%15, %8) <{predicate = 2 : i64}> : (i32, i32) -> i1 %18:2 = "dataflow.demux"(%17, %4) : (i1, none) -> (none, none) %19:2 = "dataflow.gate"(%17, %4) : (i1, none) -> (i1, none) %20:2 = "dataflow.demux"(%19#0, %19#1) : (i1, none) -> (none, none) %21:2 = "dataflow.demux"(%17, %9) : (i1, none) -> (none, none) %22:2 = "dataflow.demux"(%17, %14#0) : (i1, none) -> (none, none) %23:2 = "dataflow.demux"(%17, %15) : (i1, i32) -> (i32, i32) %24:2 = "dataflow.demux"(%17, %16) : (i1, i32) -> (i32, i32) %25:2 = "dataflow.demux"(%19#0, %19#1) : (i1, none) -> (none, none) %26:2 = "dataflow.sync"(%25#0, %20#0) : (none, none) -> (none, none) %27 = "dataflow.mux"(%19#0, %26#0, %25#1) : (i1, none, none) -> none %28 = "dataflow.carry"(%17, %arg0, %27) : (i1, none, none) -> none %29:2 = "dataflow.demux"(%17, %28) : (i1, none) -> (none, none) %30:2 = "dataflow.sync"(%18#0, %29#0) : (none, none) -> (none, none) %31:2 = "dataflow.sync"(%30#0, %22#0) : (none, none) -> (none, none) %32 = "dataflow.store"(%arg3, %2, %23#0, %31#0) : (memref<?xi32>, index, i32, none) -> none %33 = "dataflow.store"(%arg3, %3, %24#0, %32) : (memref<?xi32>, index, i32, none) -> none "dataflow.graph.return"(%33) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
module { dataflow.graph private @while_case0(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %zero = arith.constant 0 : i32 %one = arith.constant 1 : i32 %bound = arith.constant 5 : i32 %res:3 = scf.while (%s0 = %zero, %s1 = %zero, %s2 = %one) : (i32, i32, i32) -> (i32, i32, i32) { %idx0 = arith.index_cast %s0 : i32 to index %v0 = memref.load %input[%idx0] : memref<?xi32> %n0 = arith.addi %s0, %one : i32 %idx1 = arith.index_cast %n0 : i32 to index %v1 = memref.load %input[%idx1] : memref<?xi32> %vsum = arith.addi %v0, %v1 : i32 %n1 = arith.addi %s1, %vsum : i32 %n2 = arith.addi %s2, %n0 : i32 memref.store %n1, %output[%idx0] : memref<?xi32> %c = arith.cmpi slt, %n0, %limit : i32 scf.condition(%c) %n0, %n1, %n2 : i32, i32, i32 } do { ^bb0(%b0: i32, %b1: i32, %b2: i32): %bidx = arith.index_cast %b0 : i32 to index memref.store %b1, %output[%bidx] : memref<?xi32> scf.yield %b0, %b1, %b2 : i32, i32, i32 } %oidx0 = arith.index_cast %zero : i32 to index memref.store %res#0, %output[%oidx0] : memref<?xi32> %oidx1 = arith.index_cast %one : i32 to index memref.store %res#1, %output[%oidx1] : memref<?xi32> %otwo = arith.constant 2 : i32 %oidx2 = arith.index_cast %otwo : i32 to index memref.store %res#2, %output[%oidx2] : memref<?xi32> dataflow.graph.return %start : none } dataflow.graph private @while_case1(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %zero = arith.constant 0 : i32 %one = arith.constant 1 : i32 %bound = arith.constant 2 : i32 %res:2 = scf.while (%s0 = %zero, %s1 = %zero) : (i32, i32) -> (i32, i32) { %idx0 = arith.index_cast %s0 : i32 to index %v0 = memref.load %input[%idx0] : memref<?xi32> %n0 = arith.addi %s0, %one : i32 %n1 = arith.addi %s1, %v0 : i32 memref.store %n1, %output[%idx0] : memref<?xi32> %c = arith.cmpi slt, %n0, %limit : i32 scf.condition(%c) %n0, %n1 : i32, i32 } do { ^bb0(%b0: i32, %b1: i32): %d1 = arith.addi %b1, %b0 : i32 scf.yield %b0, %d1 : i32, i32 } %oidx0 = arith.index_cast %zero : i32 to index memref.store %res#0, %output[%oidx0] : memref<?xi32> %oidx1 = arith.index_cast %one : i32 to index memref.store %res#1, %output[%oidx1] : memref<?xi32> dataflow.graph.return %start : none } }
LLVM memcpy, memmove, and memset intrinsics are expanded into their exact
structured loop semantics before ownership selection. Supported LLVM
load/store (including volatile and atomic contracts), atomicrmw, cmpxchg,
and fence forms are then normalized before recursive region lowering, after
which the same frontier rules apply.
When graph publication can trace every captured memory capability to a known
root, an exact service rooted at a unique thread argument mechanically inherits
that argument's llvm.noalias fact. If a root is unknown, appears through more
than one captured capability, or does not resolve to that argument, publication
must omit the fact.
memref.get_global, memref.alloca, globals, static pointer bases, and
unrecognized capability producers are not canonical roots. A pre-final
analysis may conservatively group an unresolved access while building an event
network, but finalization rejects any such residual producer rather than
granting it an external-memory authority.
A memory input binds an established external memref capability through an exact graph-launch type match. An LLVM pointer never satisfies a graph memory port.
The finalized-graph gate also rejects residual
memref.load/memref.store, memref.get_global, raw pointer arithmetic,
pointer-bearing operations, builtin.unrealized_conversion_cast, and unknown
memory-capability producers. An unsupported effectful operation inside a
structured region must likewise fail closed instead of being hoisted.
This document is the memory-order source of truth for graph-local SCF to
Dataflow lowering. The concrete owner is loom-lower-graph-memory; it
normalizes supported memory leaves and recursively lowers structured graph
regions in one traversal.
A canonical root is found by peeling an accepted side-effect-free memref view until reaching an explicit storage or boundary root. The finalized surface recognizes:
dataflow.memory.service result at that binding, which preserves the root
of its exact pointer operand while changing only the value-plane pointer into
a memory-plane capability;memref.alloc result, whose root is unique for each invocation;Graph launch memory bindings require exact memref capability types. An LLVM pointer cannot bind a graph memref through a conversion, inferred base, or special address-space-zero rule.
Until the typed producer and verifier establish this provenance, the boundary fails closed. Forged, malformed, foreign-owner, or domain-mismatched provenance is invalid even when the residual SCF shape is otherwise supported.
The owner rejects before mutation when:
none execution value.LLVM target-specific sync scopes without a compiler-target owner and atomic accesses without an explicit power-of-two source alignment fail closed. Every residual raw LLVM memory operation fails closed.
Distinct graph memory inputs are conservatively may-alias unless explicit no-alias evidence distinguishes them. Distinct fresh allocations are independent roots.
The lowering does not select parallel width, ownership, serialization, unrolling, reduction order, or any other schedule policy. Those decisions must be made before graph-region lowering and normalized into supported structured input.
A source-origin llvm.alloca accepted by the Structured
PromoteOrderedBufferToChannel decision is not an exception to this rule. That
decision must remove the complete proved allocation closure before D0; a
residual allocation or pointer use remains non-canonical and is rejected.
Residual scf.parallel or scf.forall is checked across every graph before
the pass mutates any graph. Raw or unowned parallel input fails.
arbitrary nesting of scf.if, source-sequential scf.for, and
scf.while;
Access-to-partition membership is kept in a transient operation map before SCF operands are projected. Selector demuxing must not change alias identity.
pre-mutation rejection of residual scf.parallel and scf.forall that
reach a graph without an already materialized schedule boundary.
normalized scalar memref.load and memref.store leaves over a canonical
linear memory space;
One vector addressed memory actor is one canonical firing. Its active lanes do not create independent frontier records or an implicit lane order.
candidate.pg// Graph-local structured input for loom-lower-graph-memory. // Each module holds one or two dataflow.graph definitions whose bodies are // source-sequential scf.while loops over normalized scalar memref.load / // memref.store leaves on graph memory inputs (canonical roots). start: {new NLOOP = random.randint(1, 2); new L = 0} 'module {\n' graph_list '}\n'; graph_list: (L < NLOOP) graph_def {L += 1} graph_list | (L == NLOOP) ''; graph_def: {new NARGS = random.choice([2, 3]); new LIMIT = random.randint(2, 6); new INNER_STORE = random.choice([0, 1]); new EXTRA_LOAD = random.choice([0, 1]); new USE_ARG_BOUND = random.choice([0, 1]); new AFTER_MODE = random.choice([0, 1, 2])} 'dataflow.graph private @while_case' graph_index '(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> ()\n' ' attributes {input_segments = array<i32: 1, 0, 2>,\n' ' result_segments = array<i32: 0, 0, 0>} {\n' ' %zero = arith.constant 0 : i32\n' ' %one = arith.constant 1 : i32\n' ' %bound = arith.constant ' limit_text ' : i32\n' ' %res:' nargs_text ' = scf.while (' init_list ') : (' type_list ') -> (' type_list ') {\n' before_region ' } do {\n' ' ^bb0(' after_args '):\n' after_body ' }\n' exit_uses ' dataflow.graph.return %start : none\n' '}\n'; graph_index: [str(L)]; limit_text: [str(LIMIT)]; nargs_text: [str(NARGS)]; init_list: (NARGS == 2) '%s0 = %zero, %s1 = %zero' | (NARGS == 3) '%s0 = %zero, %s1 = %zero, %s2 = %one'; type_list: (NARGS == 2) 'i32, i32' | (NARGS == 3) 'i32, i32, i32'; after_args: (NARGS == 2) '%b0: i32, %b1: i32' | (NARGS == 3) '%b0: i32, %b1: i32, %b2: i32'; // The after region either forwards its block values, recomputes one of them, // or performs its own memory access before yielding. after_body: after_statements ' scf.yield ' after_values ' : ' type_list '\n'; after_statements: (AFTER_MODE == 0) '' | (AFTER_MODE == 1) ' %d1 = arith.addi %b1, %b0 : i32\n' | (AFTER_MODE == 2) ' %bidx = arith.index_cast %b0 : i32 to index\n' ' memref.store %b1, %output[%bidx] : memref<?xi32>\n'; after_values: (AFTER_MODE == 1) '%b0, %d1' third_after_value | (AFTER_MODE == 0) '%b0, %b1' third_after_value | (AFTER_MODE == 2) '%b0, %b1' third_after_value; third_after_value: (NARGS == 3) ', %b2' | (NARGS == 2) ''; // The before region is the recursively lowered region of the while loop: it // reads memory, computes the next state, and ends in scf.condition. before_region: ' %idx0 = arith.index_cast %s0 : i32 to index\n' ' %v0 = memref.load %input[%idx0] : memref<?xi32>\n' ' %n0 = arith.addi %s0, %one : i32\n' second_load ' %n1 = arith.addi %s1, ' accumulated ' : i32\n' third_state inner_store ' %c = arith.cmpi slt, %n0, ' bound_value ' : i32\n' ' scf.condition(%c) ' condition_args ' : ' type_list '\n'; second_load: (EXTRA_LOAD == 1) ' %idx1 = arith.index_cast %n0 : i32 to index\n' ' %v1 = memref.load %input[%idx1] : memref<?xi32>\n' ' %vsum = arith.addi %v0, %v1 : i32\n' | (EXTRA_LOAD == 0) ''; accumulated: (EXTRA_LOAD == 1) '%vsum' | (EXTRA_LOAD == 0) '%v0'; third_state: (NARGS == 3) ' %n2 = arith.addi %s2, %n0 : i32\n' | (NARGS == 2) ''; inner_store: (INNER_STORE == 1) ' memref.store %n1, %output[%idx0] : memref<?xi32>\n' | (INNER_STORE == 0) ''; bound_value: (USE_ARG_BOUND == 1) '%limit' | (USE_ARG_BOUND == 0) '%bound'; condition_args: (NARGS == 2) '%n0, %n1' | (NARGS == 3) '%n0, %n1, %n2'; // Every while result is consumed after the loop, so the loop-exit lanes are // observable in the lowered graph. exit_uses: ' %oidx0 = arith.index_cast %zero : i32 to index\n' ' memref.store %res#0, %output[%oidx0] : memref<?xi32>\n' ' %oidx1 = arith.index_cast %one : i32 to index\n' ' memref.store %res#1, %output[%oidx1] : memref<?xi32>\n' third_exit_use; third_exit_use: (NARGS == 3) ' %otwo = arith.constant 2 : i32\n' ' %oidx2 = arith.index_cast %otwo : i32 to index\n' ' memref.store %res#2, %output[%oidx2] : memref<?xi32>\n' | (NARGS == 2) '';
After recursively lowering before:
- false-lane execution is
E_out;dataflow.gateprojects before execution into after phase;- false-lane condition arguments become while results;
- true-lane condition arguments become after block values;
- false-lane
W/Ris the loop exit state;- true-lane
W/Renters after;- false-lane
SBtails leave the loop; and- true-lane
SBtails enter after.
candidate.spctpostcondition while_before_lane_projection { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-mem.md:L343-L352"; } constraints { // A lowered scf.while projects its before-region execution token (a // none-typed structural event) into the after phase with dataflow.gate. // These gates select the outputs governed by the claim; their condition // operand is the before condition selector of that loop. let execution_gates = seq { g | g in output.operations where g.name == "dataflow.gate" and g.results[1].type == mlir::none }; let while_selectors = set { g.operands[0] | g in execution_gates }; // Condition arguments of the before region are the non-event values // demuxed by the before condition selector. let condition_lanes = seq { d | d in output.operations where d.name == "dataflow.demux" and d.operands[0] in while_selectors and d.operands[1].type != mlir::none }; let input_conditions = seq { c | c in input.operations where c.name == "scf.condition" }; // Every before condition argument is split into a false lane and a true // lane by the before condition selector. assert condition_arguments_are_lane_split: cardinality(condition_lanes) == sum(seq { cardinality(c.operands.drop(1)) | c in input_conditions }); forall d in condition_lanes { assert condition_lane_has_two_lanes: cardinality(d.results) == 2; // false-lane condition arguments become while results assert false_lane_condition_argument_is_while_result: cardinality(d.results[0].uses) >= 1; // true-lane condition arguments become after block values assert true_lane_condition_argument_enters_after: cardinality(d.results[1].uses) >= 1; } forall g in execution_gates { // false-lane execution is E_out: the same before execution value that // the gate projects is demuxed by the before condition selector, and // its false lane is consumed as the loop-exit execution. assert false_lane_execution_is_loop_exit: exists d in output.operations where d.name == "dataflow.demux" and d.operands[0] == g.operands[0] and d.operands[1] == g.operands[1] and cardinality(d.results) == 2 and cardinality(d.results[0].uses) >= 1; // dataflow.gate projects before execution into after phase: both the // after phase condition and the after execution value are consumed, // and the after phase drives an after-phase lane projection. assert gate_projects_before_execution_into_after_phase: cardinality(g.results[1].uses) >= 1 and exists d in output.operations where d.name == "dataflow.demux" and d.operands[0] == g.results[0]; } // Write and read frontier components produced by the recursively lowered // before region are demuxed by the before condition selector. let frontier_lanes = seq { d | d in output.operations where d.name == "dataflow.demux" and d.operands[0] in while_selectors and d.operands[1].type == mlir::none and (none g in execution_gates where g.operands[1] == d.operands[1]) and (d.operands[1].defining_operation matches some($def) and def.name != "dataflow.carry") }; forall d in frontier_lanes { assert frontier_lane_has_two_lanes: cardinality(d.results) == 2; // false-lane W/R is the loop exit state: the false lane of the // selector demux over this frontier token leaves the loop. A write and // a read component that share one completion token share one token // value, so the exit state may be carried by either of the two lane // splits of that value. assert false_lane_frontier_is_loop_exit_state: exists e in output.operations where e.name == "dataflow.demux" and e.operands[0] == d.operands[0] and e.operands[1] == d.operands[1] and cardinality(e.results[0].uses) >= 1; // true-lane W/R enters after: the true lane of the selector demux over // this frontier token is consumed by the after phase. As above, a // shared write/read completion token is split by two lane demuxes and // the after phase consumes the true lane of one of them. assert true_lane_frontier_enters_after: exists e in output.operations where e.name == "dataflow.demux" and e.operands[0] == d.operands[0] and e.operands[1] == d.operands[1] and cardinality(e.results[1].uses) >= 1; } } }
"builtin.module"() ({ "dataflow.graph"() <{function_type = (i32, memref<?xi32>, memref<?xi32>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "while_case0", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: i32, %arg2: memref<?xi32>, %arg3: memref<?xi32>): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %3:2 = "scf.while"(%0, %0) ({ ^bb0(%arg6: i32, %arg7: i32): %6 = "arith.index_cast"(%arg6) : (i32) -> index %7 = "memref.load"(%arg2, %6) : (memref<?xi32>, index) -> i32 %8 = "arith.addi"(%arg6, %1) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %9 = "arith.addi"(%arg7, %7) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %10 = "arith.cmpi"(%8, %arg1) <{predicate = 2 : i64}> : (i32, i32) -> i1 "scf.condition"(%10, %8, %9) : (i1, i32, i32) -> () }, { ^bb0(%arg4: i32, %arg5: i32): "scf.yield"(%arg4, %arg5) : (i32, i32) -> () }) : (i32, i32) -> (i32, i32) %4 = "arith.index_cast"(%0) : (i32) -> index "memref.store"(%3#0, %arg3, %4) : (i32, memref<?xi32>, index) -> () %5 = "arith.index_cast"(%1) : (i32) -> index "memref.store"(%3#1, %arg3, %5) : (i32, memref<?xi32>, index) -> () "dataflow.graph.return"(%arg0) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
20260911-183119started2026-09-11T18:31:19Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
module { dataflow.graph private @while_case0(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %zero = arith.constant 0 : i32 %one = arith.constant 1 : i32 %bound = arith.constant 5 : i32 %res:3 = scf.while (%s0 = %zero, %s1 = %zero, %s2 = %one) : (i32, i32, i32) -> (i32, i32, i32) { %idx0 = arith.index_cast %s0 : i32 to index %v0 = memref.load %input[%idx0] : memref<?xi32> %n0 = arith.addi %s0, %one : i32 %idx1 = arith.index_cast %n0 : i32 to index %v1 = memref.load %input[%idx1] : memref<?xi32> %vsum = arith.addi %v0, %v1 : i32 %n1 = arith.addi %s1, %vsum : i32 %n2 = arith.addi %s2, %n0 : i32 memref.store %n1, %output[%idx0] : memref<?xi32> %c = arith.cmpi slt, %n0, %limit : i32 scf.condition(%c) %n0, %n1, %n2 : i32, i32, i32 } do { ^bb0(%b0: i32, %b1: i32, %b2: i32): %bidx = arith.index_cast %b0 : i32 to index memref.store %b1, %output[%bidx] : memref<?xi32> scf.yield %b0, %b1, %b2 : i32, i32, i32 } %oidx0 = arith.index_cast %zero : i32 to index memref.store %res#0, %output[%oidx0] : memref<?xi32> %oidx1 = arith.index_cast %one : i32 to index memref.store %res#1, %output[%oidx1] : memref<?xi32> %otwo = arith.constant 2 : i32 %oidx2 = arith.index_cast %otwo : i32 to index memref.store %res#2, %output[%oidx2] : memref<?xi32> dataflow.graph.return %start : none } dataflow.graph private @while_case1(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} { %zero = arith.constant 0 : i32 %one = arith.constant 1 : i32 %bound = arith.constant 2 : i32 %res:2 = scf.while (%s0 = %zero, %s1 = %zero) : (i32, i32) -> (i32, i32) { %idx0 = arith.index_cast %s0 : i32 to index %v0 = memref.load %input[%idx0] : memref<?xi32> %n0 = arith.addi %s0, %one : i32 %n1 = arith.addi %s1, %v0 : i32 memref.store %n1, %output[%idx0] : memref<?xi32> %c = arith.cmpi slt, %n0, %limit : i32 scf.condition(%c) %n0, %n1 : i32, i32 } do { ^bb0(%b0: i32, %b1: i32): %d1 = arith.addi %b1, %b0 : i32 scf.yield %b0, %d1 : i32, i32 } %oidx0 = arith.index_cast %zero : i32 to index memref.store %res#0, %output[%oidx0] : memref<?xi32> %oidx1 = arith.index_cast %one : i32 to index memref.store %res#1, %output[%oidx1] : memref<?xi32> dataflow.graph.return %start : none } }
"builtin.module"() ({ "dataflow.graph"() <{function_type = (i32, memref<?xi32>, memref<?xi32>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "while_case0", sym_visibility = "private"}> ({ ^bb0(%arg4: none, %arg5: i32, %arg6: memref<?xi32>, %arg7: memref<?xi32>): %37 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %38 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %39 = "arith.constant"() <{value = 5 : i32}> : () -> i32 %40 = "arith.index_cast"(%37) : (i32) -> index %41 = "arith.index_cast"(%38) : (i32) -> index %42 = "arith.constant"() <{value = 2 : i32}> : () -> i32 %43 = "arith.index_cast"(%42) : (i32) -> index %44 = "dataflow.carry"(%65, %arg4, %67#1) : (i1, none, none) -> none %45 = "dataflow.carry"(%65, %37, %71#1) : (i1, i32, i32) -> i32 %46 = "dataflow.carry"(%65, %37, %72#1) : (i1, i32, i32) -> i32 %47 = "dataflow.carry"(%65, %38, %73#1) : (i1, i32, i32) -> i32 %48 = "dataflow.invariant"(%65, %38) : (i1, i32) -> i32 %49 = "dataflow.invariant"(%65, %arg5) : (i1, i32) -> i32 %50 = "dataflow.carry"(%65, %arg4, %76) : (i1, none, none) -> none %51 = "dataflow.carry"(%65, %arg4, %76) : (i1, none, none) -> none %52 = "arith.index_cast"(%45) : (i32) -> index %53:2 = "dataflow.sync"(%44, %50) : (none, none) -> (none, none) %54:2 = "dataflow.load"(%arg6, %52, %53#0) : (memref<?xi32>, index, none) -> (i32, none) %55:2 = "dataflow.sync"(%51, %54#1) : (none, none) -> (none, none) %56 = "arith.addi"(%45, %48) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %57 = "arith.index_cast"(%56) : (i32) -> index %58:2 = "dataflow.sync"(%44, %50) : (none, none) -> (none, none) %59:2 = "dataflow.load"(%arg6, %57, %58#0) : (memref<?xi32>, index, none) -> (i32, none) %60:2 = "dataflow.sync"(%55#0, %59#1) : (none, none) -> (none, none) %61 = "arith.addi"(%54#0, %59#0) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %62 = "arith.addi"(%46, %61) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %63 = "arith.addi"(%47, %56) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %64 = "dataflow.store"(%arg7, %52, %62, %60#0) : (memref<?xi32>, index, i32, none) -> none %65 = "arith.cmpi"(%56, %49) <{predicate = 2 : i64}> : (i32, i32) -> i1 %66:2 = "dataflow.demux"(%65, %44) : (i1, none) -> (none, none) %67:2 = "dataflow.gate"(%65, %44) : (i1, none) -> (i1, none) %68:2 = "dataflow.demux"(%67#0, %67#1) : (i1, none) -> (none, none) %69:2 = "dataflow.demux"(%65, %64) : (i1, none) -> (none, none) %70:2 = "dataflow.demux"(%65, %64) : (i1, none) -> (none, none) %71:2 = "dataflow.demux"(%65, %56) : (i1, i32) -> (i32, i32) %72:2 = "dataflow.demux"(%65, %62) : (i1, i32) -> (i32, i32) %73:2 = "dataflow.demux"(%65, %63) : (i1, i32) -> (i32, i32) %74 = "arith.index_cast"(%71#1) : (i32) -> index %75:2 = "dataflow.sync"(%67#1, %70#1) : (none, none) -> (none, none) %76 = "dataflow.store"(%arg7, %74, %72#1, %75#0) : (memref<?xi32>, index, i32, none) -> none %77:2 = "dataflow.demux"(%67#0, %67#1) : (i1, none) -> (none, none) %78:2 = "dataflow.sync"(%77#0, %68#0) : (none, none) -> (none, none) %79 = "dataflow.mux"(%67#0, %78#0, %77#1) : (i1, none, none) -> none %80 = "dataflow.carry"(%65, %arg4, %79) : (i1, none, none) -> none %81:2 = "dataflow.demux"(%65, %80) : (i1, none) -> (none, none) %82:2 = "dataflow.sync"(%66#0, %81#0) : (none, none) -> (none, none) %83:2 = "dataflow.sync"(%82#0, %70#0) : (none, none) -> (none, none) %84 = "dataflow.store"(%arg7, %40, %71#0, %83#0) : (memref<?xi32>, index, i32, none) -> none %85 = "dataflow.store"(%arg7, %41, %72#0, %84) : (memref<?xi32>, index, i32, none) -> none %86 = "dataflow.store"(%arg7, %43, %73#0, %85) : (memref<?xi32>, index, i32, none) -> none "dataflow.graph.return"(%86) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () "dataflow.graph"() <{function_type = (i32, memref<?xi32>, memref<?xi32>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "while_case1", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: i32, %arg2: memref<?xi32>, %arg3: memref<?xi32>): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %2 = "arith.constant"() <{value = 2 : i32}> : () -> i32 %3 = "arith.index_cast"(%0) : (i32) -> index %4 = "arith.index_cast"(%1) : (i32) -> index %5 = "dataflow.carry"(%19, %arg0, %21#1) : (i1, none, none) -> none %6 = "dataflow.carry"(%19, %0, %25#1) : (i1, i32, i32) -> i32 %7 = "dataflow.carry"(%19, %0, %27) : (i1, i32, i32) -> i32 %8 = "dataflow.invariant"(%19, %1) : (i1, i32) -> i32 %9 = "dataflow.invariant"(%19, %arg1) : (i1, i32) -> i32 %10 = "dataflow.carry"(%19, %arg0, %23#1) : (i1, none, none) -> none %11 = "dataflow.carry"(%19, %arg0, %24#1) : (i1, none, none) -> none %12 = "arith.index_cast"(%6) : (i32) -> index %13:2 = "dataflow.sync"(%5, %10) : (none, none) -> (none, none) %14:2 = "dataflow.load"(%arg2, %12, %13#0) : (memref<?xi32>, index, none) -> (i32, none) %15:2 = "dataflow.sync"(%11, %14#1) : (none, none) -> (none, none) %16 = "arith.addi"(%6, %8) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %17 = "arith.addi"(%7, %14#0) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %18 = "dataflow.store"(%arg3, %12, %17, %15#0) : (memref<?xi32>, index, i32, none) -> none %19 = "arith.cmpi"(%16, %9) <{predicate = 2 : i64}> : (i32, i32) -> i1 %20:2 = "dataflow.demux"(%19, %5) : (i1, none) -> (none, none) %21:2 = "dataflow.gate"(%19, %5) : (i1, none) -> (i1, none) %22:2 = "dataflow.demux"(%21#0, %21#1) : (i1, none) -> (none, none) %23:2 = "dataflow.demux"(%19, %18) : (i1, none) -> (none, none) %24:2 = "dataflow.demux"(%19, %18) : (i1, none) -> (none, none) %25:2 = "dataflow.demux"(%19, %16) : (i1, i32) -> (i32, i32) %26:2 = "dataflow.demux"(%19, %17) : (i1, i32) -> (i32, i32) %27 = "arith.addi"(%26#1, %25#1) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 %28:2 = "dataflow.demux"(%21#0, %21#1) : (i1, none) -> (none, none) %29:2 = "dataflow.sync"(%28#0, %22#0) : (none, none) -> (none, none) %30 = "dataflow.mux"(%21#0, %29#0, %28#1) : (i1, none, none) -> none %31 = "dataflow.carry"(%19, %arg0, %30) : (i1, none, none) -> none %32:2 = "dataflow.demux"(%19, %31) : (i1, none) -> (none, none) %33:2 = "dataflow.sync"(%20#0, %32#0) : (none, none) -> (none, none) %34:2 = "dataflow.sync"(%33#0, %24#0) : (none, none) -> (none, none) %35 = "dataflow.store"(%arg3, %3, %25#0, %34#0) : (memref<?xi32>, index, i32, none) -> none %36 = "dataflow.store"(%arg3, %4, %26#0, %35) : (memref<?xi32>, index, i32, none) -> none "dataflow.graph.return"(%36) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) : () -> ()
partial source coverage: Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.
authoring-context.json{"entries":[{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"331-355","path":"docs/spec-compiler-part-3-mem.md","roles":["applicability","context"],"text":"## 8. `scf.while`\n\nFor a while loop whose after region executes `K` times:\n\n* before executes `K + 1` times;\n* after executes `K` times;\n* the before condition stream is `T^K F`.\n\nExecution, source inits, touched `W/R` components, and path-live `SB` tails use\ncondition-driven carry rings. Their outputs enter before directly, because\nbefore includes the final false condition check.\n\nAfter recursively lowering before:\n\n* false-lane execution is `E_out`;\n* `dataflow.gate` projects before execution into after phase;\n* false-lane condition arguments become while results;\n* true-lane condition arguments become after block values;\n* false-lane `W/R` is the loop exit state;\n* true-lane `W/R` enters after;\n* false-lane `SB` tails leave the loop; and\n* true-lane `SB` tails enter after.\n\nAfter results feed the next before activation. A false condition consumes no\ndummy feedback.","why":"Section 8 governing context for the sampled obligation: the scf.while before/after activation counts, the T^K F condition stream, the condition-driven carry rings, and the eight after-lowering lane statements that the postcondition encodes."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"3-6","path":"docs/spec-compiler-part-3-mem.md","roles":["applicability"],"text":"This document is the memory-order source of truth for graph-local SCF to\nDataflow lowering. The concrete owner is `loom-lower-graph-memory`; it\nnormalizes supported memory leaves and recursively lowers structured graph\nregions in one traversal.","why":"Names loom-lower-graph-memory as the concrete owner of graph-local SCF to Dataflow lowering, fixing the stage under test and the pass in subject-command.json."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"21-46","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"## 1. Scope\n\nThe lowering contract covers:\n\n* scalar and fixed-ranked vector forms of canonical `dataflow.load` and\n `dataflow.store`, including the masked contiguous and gather/scatter forms\n defined by `docs/spec-dataflow-vectorization.md`;\n* canonical atomic load/store, `dataflow.atomic_rmw`,\n `dataflow.cmpxchg`, `dataflow.fence`, and volatile access contracts defined\n by `docs/spec-dataflow-memory-consistency.md`;\n* normalized scalar `memref.load` and `memref.store` leaves over a canonical\n linear memory space;\n* sequential composition;\n* arbitrary nesting of `scf.if`, source-sequential `scf.for`, and\n `scf.while`;\n* basic graph-local alias-root partitions;\n* conservative unknown accesses;\n* value, execution, write-frontier, and read-frontier projection through the\n same structured selectors;\n* pre-mutation rejection of residual `scf.parallel` and `scf.forall` that\n reach a graph without an already materialized schedule boundary.\n\nThe lowering does not select parallel width, ownership, serialization,\nunrolling, reduction order, or any other schedule policy. Those decisions\nmust be made before graph-region lowering and normalized into supported\nstructured input.","why":"Scope of accepted structured input: normalized scalar memref.load/store leaves over a canonical linear memory space, sequential composition, nesting of scf.if/scf.for/scf.while, and the exclusion of schedule policy. Determines what the grammar may sample."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"48-70","path":"docs/spec-compiler-part-3-mem.md","roles":["context"],"text":"## 2. One Recursive Owner\n\nThe compiler-local contract is:\n\n```text\nlower_region(E_in, values_in, {W_in[p], R_in[p]}, SB_in)\n -> (E_out, values_out, {W_out[p], R_out[p]}, SB_out)\n```\n\n`E` is execution permission and structural completion. `W` and `R` are\nmemory-order frontiers for alias partition `p`. They share the ordinary\n`none` SSA type but remain semantically distinct throughout lowering.\n`SB` is the path-sensitive analysis relation containing only\nsequenced-before obligations that remain observable after the selected\nStructured Program Candidate's legal transformations. It covers atomic/fence,\nvolatile, release, and acquire requirements across alias partitions. It is not\none serialized token or an IR object.\n\nThe contract is an implementation function, not an IR object. Canonical IR\ndoes not contain partition ids, dependence snapshots, compound-region\nobjects, chain-scope attributes, memory tokens, sequenced-before records, or\nmemory-specific join operations.","why":"Defines lower_region and the terminology E_out, W/R, and SB, and states that execution and memory frontiers share the ordinary none SSA type. The postcondition uses that none-typed event terminology to select the before-execution gate and the frontier lanes."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"79-90","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"A canonical root is found by peeling an accepted side-effect-free memref view\nuntil reaching an explicit storage or boundary root. The finalized surface\nrecognizes:\n\n* a graph memory input, whose root identity comes from its launch binding;\n* a `dataflow.memory.service` result at that binding, which preserves the root\n of its exact pointer operand while changing only the value-plane pointer into\n a memory-plane capability;\n* a fresh `memref.alloc` result, whose root is unique for each invocation;\n* a verified side-effect-free view that preserves the source root. The initial\n accepted set contains `memref.cast`; adding another view form requires one\n matching root, region, and simulator contract before admission.","why":"Canonical root surface; the grammar roots every access at a graph memory input (memref capability port) so that the loop has well-formed alias partitions."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"99-106","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"Graph launch memory bindings require exact memref capability types. An LLVM\npointer cannot bind a graph memref through a conversion, inferred base, or\nspecial address-space-zero rule. SCF optimization may first prove and\nmaterialize a rooted memref capability plus integer offset, or it may retain\nthe pointer as a value consumed by a `PointerAddressed` memory actor together\nwith an independently bound service capability. Neither path materializes a\ngraph-body bridge. `builtin.unrealized_conversion_cast` is never a canonical\nroot, view, actor, or boundary bridge.","why":"Graph launch memory bindings require exact memref capability types and forbid pointer or conversion bridges; the sampled graphs bind memref<?xi32> ports directly."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"470-480","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"The owner rejects before mutation when:\n\n* raw or unverifiably owned parallel SCF reaches a graph;\n* an effectful or unmodeled nested operation reaches a graph;\n* a residual LLVM load, store, atomicrmw, cmpxchg, fence, memcpy, memmove, or\n memset remains after\n normalization and therefore has no explicit completion event;\n* a source memory access has not been normalized to the canonical linear\n memory-space form required by its scalar or vector Dataflow actor;\n* structured control carries a memref result or memref loop state;\n* the graph entry lacks the leading `none` execution value.","why":"Pre-mutation rejection list (parallel SCF, residual LLVM memory ops, unnormalized accesses, memref loop state, missing leading none execution value). The grammar avoids every rejected shape so the sampled inputs reach the while lowering."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"382-387","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"Residual `scf.parallel` or `scf.forall` is checked across every graph before\nthe pass mutates any graph. Raw or unowned parallel input fails. A fixed finite\nparallel region is accepted only when its Structured Program Candidate owns a\ntyped, verifier-proven `P[]` schedule and the recursive transfer can derive one\ncomplete frontier relation for that exact domain. The lowering must not trust\nthe mere presence of string-named attributes as proof.","why":"Residual scf.parallel/scf.forall fails closed before any graph is mutated; the grammar emits no parallel region."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"145-234","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"text":"def Dataflow_CarryOp : Dataflow_Op<\"carry\", [Pure,\n CanonicalDataflowActor,\n AllTypesMatch<[\"init\", \"carry\", \"output\"]>]> {\n let summary =\n \"two-state carry: emit init once, then gate subsequent carries by cond\";\n let description = [{\n Two-state (init / carry) token-level element.\n\n * Start state is `init`.\n * In state `init`: wait for one `%init` token; forward it to\n `%output`; transition to `carry`.\n * In state `carry`: inspect the next `%cond : i1` token.\n - if `cond` is true : wait for and consume `%carry`, consume the\n condition, forward `%carry` to `%output`, and stay in `carry`;\n - if `cond` is false: consume only the condition, emit nothing, and\n return to state `init`.\n\n `%init`, `%carry` and `%output` share a single type; `%cond` is\n `i1`.\n }];\n\n let arguments = (ins I1:$cond, AnyType:$init, AnyType:$carry);\n let results = (outs AnyType:$output);\n\n let assemblyFormat = [{\n $cond `,` $init `,` $carry attr-dict `:` type($output)\n }];\n}\n\ndef Dataflow_InvariantOp : Dataflow_Op<\"invariant\", [Pure,\n CanonicalDataflowActor,\n AllTypesMatch<[\"init\", \"output\"]>]> {\n let summary =\n \"latch an init value and replay it once per true cond until reset\";\n let description = [{\n Two-state element that latches an init value and replays it.\n\n * Start state is `init`.\n * In state `init`: wait for one `%init` token, record its value,\n forward it to `%output`, and transition to `carry`.\n * In state `carry`: wait for one `%cond : i1` token. `%init` is\n not consumed in this state.\n - if `cond` is true : re-emit the recorded value to\n `%output`, stay in `carry`;\n - if `cond` is false: clear the recorded value, emit nothing,\n return to state `init`.\n\n `%init` and `%output` share a single type; `%cond` is `i1`.\n }];\n\n let arguments = (ins I1:$cond, AnyType:$init);\n let results = (outs AnyType:$output);\n\n let assemblyFormat = [{\n $cond `,` $init attr-dict `:` type($output)\n }];\n}\n\ndef Dataflow_GateOp : Dataflow_Op<\"gate\", [Pure,\n CanonicalDataflowActor,\n AllTypesMatch<[\"before_value\", \"after_value\"]>]> {\n let summary =\n \"open a value channel on the first true, reclose on the next false\";\n let description = [{\n Two-state gate over a (cond, value) pair. Both inputs are always\n consumed together on each firing.\n\n * Start state is `init`.\n * In state `init`:\n - on `(false, X)`: emit nothing on either output;\n - on `(true, X)`: emit only `X` on `%after_value` (no token\n on `%after_cond`), transition to `continue`.\n * In state `continue`:\n - on `(true, X)`: forward the pair as `(true, X)` on\n `%after_cond` and `%after_value` respectively, stay in\n `continue`;\n - on `(false, X)`: emit only `false` on `%after_cond` (no\n token on `%after_value`), return to state `init`.\n\n `%before_value` and `%after_value` share a single type;\n `%before_cond` and `%after_cond` are `i1`.\n }];\n\n let arguments = (ins I1:$before_cond, AnyType:$before_value);\n let results = (outs I1:$after_cond, AnyType:$after_value);\n\n let assemblyFormat = [{\n $before_cond `,` $before_value attr-dict `:` type($after_value)\n }];\n}","why":"dataflow.carry, dataflow.invariant, and dataflow.gate operand/result order and meaning (cond, init, carry; before_cond, before_value -> after_cond, after_value). Fixes how the postcondition reads a gate's condition operand, gated value, and after phase."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"362-437","path":"include/Dataflow/IR/DataflowOps.td","roles":["context"],"text":"def Dataflow_MuxOp : Dataflow_Op<\"mux\", [Pure, CanonicalDataflowActor]> {\n let summary = \"N-to-1 selection: forward the sel-picked input to output\";\n let description = [{\n N-input, 1-output multiplexer (N > 1). `sel` picks one input port\n index `k`. The op fires when tokens are available on *both* `%sel`\n and `%inputs[k]`. Both are consumed and the value is forwarded to\n `%output`. Tokens on the non-selected inputs are **not** consumed\n (they remain buffered; the other lanes block).\n\n `sel` type:\n * exactly 2 inputs -> `i1`\n * more than 2 inputs -> `index`\n\n All inputs and the output share one type.\n }];\n\n let arguments = (ins AnyTypeOf<[I1, Index]>:$sel,\n Variadic<AnyType>:$inputs);\n let results = (outs AnyType:$output);\n\n let assemblyFormat = [{\n $sel `,` $inputs attr-dict `:` functional-type(operands, results)\n }];\n let hasVerifier = 1;\n}\n\ndef Dataflow_DemuxOp : Dataflow_Op<\"demux\", [Pure, CanonicalDataflowActor]> {\n let summary = \"1-to-N selection: route the input to the sel-picked output\";\n let description = [{\n 1-input, N-output demultiplexer (N > 1). `sel` picks one output\n port index `k`. The op fires when tokens are available on both\n `%sel` and `%input`; both are consumed and the value is forwarded\n to `%outputs[k]`. No token is produced on the non-selected output\n ports.\n\n `sel` type:\n * exactly 2 outputs -> `i1`\n * more than 2 outputs -> `index`\n\n The input and all outputs share one type.\n }];\n\n let arguments = (ins AnyTypeOf<[I1, Index]>:$sel, AnyType:$input);\n let results = (outs Variadic<AnyType>:$outputs);\n\n let assemblyFormat = [{\n $sel `,` $input attr-dict `:` functional-type(operands, results)\n }];\n let hasVerifier = 1;\n}\n\n//===----------------------------------------------------------------------===//\n// Memory Ops\n//\n// Streaming accesses against a memref, orchestrated by none-typed ctrl / done\n// tokens. The memref's element type constrains the element data type or the\n// access vector's element type.\n//===----------------------------------------------------------------------===//\n\n// The canonical memory actors. Each projects the standard MLIR memory effects\n// through the one shared implementation in `DataflowMemoryContracts.cpp`; no\n// actor classifies its own effects. That projection names the memory operand\n// for the addressed access and reads the atomic and volatile facts back from\n// the actor's one aggregate contract to add conservative unbound effects.\nclass Dataflow_MemoryActorOp<string mnemonic, list<Trait> traits = []>\n : Dataflow_Op<mnemonic, !listconcat(traits, [\n CanonicalDataflowActor,\n DeclareOpInterfaceMethods<MemoryEffectsOpInterface>])> {\n let extraClassDefinition = [{\n void $cppClass::getEffects(\n ::llvm::SmallVectorImpl<::mlir::MemoryEffects::EffectInstance>\n &effects) {\n ::dataflow::semantics::getMemoryActorEffects(getOperation(), effects);\n }\n }];\n}","why":"dataflow.mux and dataflow.demux definitions: an i1 selector picks output port index k, so demux result 0 is the false lane and result 1 is the true lane. This is the lane polarity the postcondition asserts."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"839-860","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def Dataflow_GraphOp : Dataflow_Op<\"graph\", [\n IsolatedFromAbove,\n HasParent<\"::mlir::ModuleOp\">,\n SingleBlockImplicitTerminator<\"GraphReturnOp\">,\n FunctionOpInterface,\n RecursiveMemoryEffects,\n DeclareOpInterfaceMethods<RegionKindInterface>\n]> {\n let summary = \"Symbol-bearing function-like SpatialCore graph definition\";\n let description = [{\n Module-scope, function-like callable holding the SpatialCore body\n of a leaf dataflow graph. It does not itself execute; one or more\n `dataflow.graph.launch` ops materialise launches of it inside the\n body of a `dataflow.thread` definition.\n\n `function_type` contains only application payload ports. Normalized\n `input_segments` and `result_segments` classify those payloads as value,\n stream, and memory ports. The body's distinguished leading `none` block\n argument is the invocation start protocol endpoint, while launch `done`\n is derived exclusively from `dataflow.graph.return.complete`; neither is\n stored in the function type.","why":"dataflow.graph definition: module-scope symbol, single block, input_segments/result_segments payload classification and the leading none start block argument. Fixes the graph header the grammar emits."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"924-945","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def Dataflow_GraphReturnOp : Dataflow_Op<\"graph.return\", [\n AttrSizedOperandSegments,\n Terminator,\n ParentOneOf<[\"::dataflow::GraphOp\"]>,\n Pure\n]> {\n let summary = \"Terminator for a dataflow.graph body\";\n let description = [{\n Structurally declares the enclosing graph's value, stream, and memory\n outputs together with its mandatory retirement frontier. `complete` is\n an unordered all-of set of one or more `none` values; the launch `done`\n event is derived from that set and is not itself a return operand.\n\n The compact assembly form `%complete, %values... : none, types...` is\n retained for the common case with one completion witness and no stream\n or memory outputs. Other shapes print all four named segments.\n }];\n\n let arguments = (ins\n Variadic<AnyType>:$values,\n Variadic<AnyType>:$streams,\n Variadic<AnyType>:$memories,","why":"dataflow.graph.return operand segments and the compact `%complete : none` spelling used to terminate every sampled graph body."},{"file_sha256":"d319fc0dc5c2da65797de37d1e48d1303be02ec7d72ac1796bb45973b616d9ef","kind":"verifier","lines":"85-91","path":"lib/Frontend/Lowering/GraphRegionAdmission.cpp","roles":["input_well_formedness"],"text":"bool isGraphRegionControlOperation(mlir::Operation *operation) {\n return llvm::isa<mlir::scf::IfOp, mlir::scf::ForOp, mlir::scf::WhileOp,\n mlir::scf::IndexSwitchOp, mlir::scf::ParallelOp,\n mlir::scf::ForallOp, mlir::scf::YieldOp,\n mlir::scf::ConditionOp, mlir::scf::ReduceOp,\n mlir::scf::InParallelOp, dataflow::GraphReturnOp>(operation);\n}","why":"The admission classification of graph-region control operations (scf.while, scf.condition, scf.yield are accepted structured control), confirming that the sampled while shape passes the pre-mutation gate."},{"file_sha256":"4295a7f0089a5b35f7f7f538032b31f51ca3966d4279faa030a2d493a8f76385","kind":"implementation","lines":"963-1000","path":"lib/Frontend/Lowering/GraphRegionLowering.cpp","roles":["context"],"text":"std::pair<::mlir::Value, ::mlir::Value>\n demux(::mlir::Value selector, ::mlir::Value input, ::mlir::Location loc) {\n setInsertionPoint(loc);\n auto op = ::dataflow::DemuxOp::create(\n builder, loc, ::mlir::TypeRange{input.getType(), input.getType()},\n selector, input);\n return {op.getOutputs()[0], op.getOutputs()[1]};\n }\n\n ::mlir::Value mux(::mlir::Value selector, ::mlir::Value falseValue,\n ::mlir::Value trueValue, ::mlir::Location loc) {\n setInsertionPoint(loc);\n return ::dataflow::MuxOp::create(builder, loc, falseValue.getType(),\n selector,\n ::mlir::ValueRange{falseValue, trueValue})\n .getOutput();\n }\n\n GatedValue gateTrueLane(::mlir::Value phase, ::mlir::Value value,\n ::mlir::Location loc) {\n setInsertionPoint(loc);\n auto gate = ::dataflow::GateOp::create(builder, loc, builder.getI1Type(),\n value.getType(), phase, value);\n auto close = ::dataflow::DemuxOp::create(\n builder, loc, ::mlir::TypeRange{value.getType(), value.getType()},\n gate.getAfterCond(), gate.getAfterValue());\n return {gate.getAfterCond(), gate.getAfterValue(), close.getOutputs()[0]};\n }\n\n ::llvm::SmallVector<::mlir::Value, 4>\n projectForCaptures(::mlir::Region ®ion, ::mlir::ValueRange captures,\n ::mlir::Value phase, ::mlir::Location loc) {\n ::llvm::SmallVector<::mlir::Value, 4> closeEvents;\n for (::mlir::Value capture : captures) {\n setInsertionPoint(loc);\n ::mlir::Value raw = ::dataflow::InvariantOp::create(\n builder, loc, capture.getType(), phase, capture)\n .getOutput();","why":"The lane helpers: demux(selector, input) returns (outputs[0], outputs[1]) as (false lane, true lane) and gateTrueLane builds the dataflow.gate whose after_cond is the after phase. Establishes the concrete spelling of the documented false/true lanes."},{"file_sha256":"4295a7f0089a5b35f7f7f538032b31f51ca3966d4279faa030a2d493a8f76385","kind":"implementation","lines":"1772-1905","path":"lib/Frontend/Lowering/GraphRegionLowering.cpp","roles":["context"],"text":"RegionResult lowerWhile(::mlir::scf::WhileOp whileOp, ::mlir::Value execution,\n MemoryState memory) {\n ::mlir::Location loc = whileOp.getLoc();\n auto condition = ::llvm::cast<::mlir::scf::ConditionOp>(\n whileOp.getBefore().front().getTerminator());\n\n ::llvm::SmallVector<::mlir::Value, 8> beforeCaptures =\n collectProjectedCaptures(whileOp.getBefore());\n ::llvm::SmallVector<::mlir::Value, 8> afterCaptures =\n collectProjectedCaptures(whileOp.getAfter());\n\n setInsertionPoint(loc);\n ::mlir::Value pendingSelector =\n ::mlir::arith::ConstantOp::create(builder, loc, builder.getI1Type(),\n builder.getBoolAttr(false))\n .getResult();\n auto executionCarry =\n ::dataflow::CarryOp::create(builder, loc, builder.getNoneType(),\n pendingSelector, execution, execution);\n\n ::llvm::SmallVector<::dataflow::CarryOp, 4> valueCarries;\n for (::mlir::Value init : whileOp.getInits()) {\n auto carry = ::dataflow::CarryOp::create(builder, loc, init.getType(),\n pendingSelector, init, init);\n valueCarries.push_back(carry);\n }\n for (unsigned i = 0; i < valueCarries.size(); ++i)\n replaceUsesInside(whileOp.getBeforeArguments()[i],\n valueCarries[i].getOutput(), whileOp.getBefore());\n ::llvm::SmallVector<::dataflow::InvariantOp, 4> beforeInvariants =\n projectWhileBeforeCaptures(whileOp.getBefore(), beforeCaptures,\n pendingSelector, loc);\n\n ::llvm::SmallBitVector touched = touchedPartitions(whileOp.getBefore());\n touched |= touchedPartitions(whileOp.getAfter());\n MemoryState beforeMemory = memory;\n ::llvm::SmallVector<std::optional<::dataflow::CarryOp>, 4> writeCarries(\n partitionCount);\n ::llvm::SmallVector<std::optional<::dataflow::CarryOp>, 4> readCarries(\n partitionCount);\n for (int partition = touched.find_first(); partition >= 0;\n partition = touched.find_next(partition)) {\n setInsertionPoint(loc);\n auto writeCarry = ::dataflow::CarryOp::create(\n builder, loc, builder.getNoneType(), pendingSelector,\n memory[partition].write, memory[partition].write);\n auto readCarry = ::dataflow::CarryOp::create(\n builder, loc, builder.getNoneType(), pendingSelector,\n memory[partition].read, memory[partition].read);\n writeCarries[partition] = writeCarry;\n readCarries[partition] = readCarry;\n beforeMemory[partition] = {writeCarry.getOutput(), readCarry.getOutput()};\n }\n\n RegionResult beforeResult =\n lowerBlock(whileOp.getBefore().front(), executionCarry.getOutput(),\n std::move(beforeMemory));\n ::mlir::Value selector = condition.getCondition();\n executionCarry.getCondMutable().assign(selector);\n for (::dataflow::CarryOp carry : valueCarries)\n carry.getCondMutable().assign(selector);\n for (::dataflow::InvariantOp invariant : beforeInvariants)\n invariant.getCondMutable().assign(selector);\n for (int partition = touched.find_first(); partition >= 0;\n partition = touched.find_next(partition)) {\n writeCarries[partition]->getCondMutable().assign(selector);\n readCarries[partition]->getCondMutable().assign(selector);\n }\n pendingSelector.getDefiningOp()->erase();\n\n auto [executionExit, unusedExecution] =\n demux(selector, beforeResult.execution, loc);\n (void)unusedExecution;\n GatedValue gatedExecution =\n gateTrueLane(selector, beforeResult.execution, loc);\n ::mlir::Value executionAfter = gatedExecution.value;\n ::llvm::SmallVector<::mlir::Value, 4> closeEvents{gatedExecution.close};\n\n MemoryState afterMemory = beforeResult.memory;\n MemoryState output = memory;\n for (int partition = touched.find_first(); partition >= 0;\n partition = touched.find_next(partition)) {\n auto [writeExit, writeAfter] =\n demux(selector, beforeResult.memory[partition].write, loc);\n auto [readExit, readAfter] =\n demux(selector, beforeResult.memory[partition].read, loc);\n output[partition] = {writeExit, readExit};\n afterMemory[partition] = {writeAfter, readAfter};\n }\n\n ::llvm::SmallVector<::mlir::Value, 4> resultValues;\n for (::mlir::Value value : condition.getArgs()) {\n auto [exit, after] = demux(selector, value, loc);\n resultValues.push_back(exit);\n replaceUsesInside(whileOp.getAfterArguments()[resultValues.size() - 1],\n after, whileOp.getAfter());\n }\n ::llvm::SmallVector<::mlir::Value, 4> afterCaptureCloses =\n projectForCaptures(whileOp.getAfter(), afterCaptures, selector, loc);\n closeEvents.append(afterCaptureCloses);\n\n RegionResult afterResult = lowerBlock(\n whileOp.getAfter().front(), executionAfter, std::move(afterMemory));\n auto yield = ::llvm::cast<::mlir::scf::YieldOp>(\n whileOp.getAfter().front().getTerminator());\n executionCarry.getCarryMutable().assign(afterResult.execution);\n for (unsigned i = 0; i < valueCarries.size(); ++i)\n valueCarries[i].getCarryMutable().assign(yield.getOperand(i));\n for (int partition = touched.find_first(); partition >= 0;\n partition = touched.find_next(partition)) {\n writeCarries[partition]->getCarryMutable().assign(\n afterResult.memory[partition].write);\n readCarries[partition]->getCarryMutable().assign(\n afterResult.memory[partition].read);\n }\n\n auto [finalAfterExecution, continuingAfterExecution] =\n demux(gatedExecution.phase, afterResult.execution, loc);\n closeEvents.insert(closeEvents.begin(), finalAfterExecution);\n ::mlir::Value finalAfterCompletion = joinEvents(closeEvents, loc);\n ::mlir::Value afterCompletion =\n mux(gatedExecution.phase, finalAfterCompletion,\n continuingAfterExecution, loc);\n setInsertionPoint(loc);\n auto retirementCarry =\n ::dataflow::CarryOp::create(builder, loc, builder.getNoneType(),\n selector, execution, afterCompletion);\n auto [retirementExit, unusedRetirement] =\n demux(selector, retirementCarry.getOutput(), loc);\n (void)unusedRetirement;\n\n for (unsigned i = 0; i < whileOp.getNumResults(); ++i)\n whileOp.getResult(i).replaceAllUsesWith(resultValues[i]);\n whileOp.erase();","why":"lowerWhile: the carry rings under the before condition selector, the before-execution demux and gate, the W/R lane demuxes, and the condition-argument lane demuxes that the postcondition identifies in the output."},{"file_sha256":"9c0d8eaae32c891b641d7c6c1f5b8bde6c0b38186b4360b0732d06cbdf7a8b47","kind":"test","lines":"1-50","path":"test/raise/scf-to-dfg-nested-while-selection.mlir","roles":["input_construction","input_well_formedness"],"text":"// RUN: loom-raise-opt --loom-lower-graph-memory %s -o %t.lowered.mlir\n// RUN: loom-lower %t.lowered.mlir | FileCheck %s\n\n// A nested loop selected inside scf.while.before retires exactly once for\n// every before-region activation. Its close must therefore remain aligned\n// with the complete outer condition stream, including the final false phase.\n// CHECK-LABEL: dataflow.graph private @nested_while_selection\n// CHECK: dataflow.gate\n// CHECK: dataflow.graph.return\n// CHECK-NOT: scf.if\n// CHECK-NOT: scf.while\ndataflow.graph private @nested_while_selection(\n %start: none, %outer_limit: i32,\n %input: memref<?xi32>, %output: memref<?xi32>) -> ()\n attributes {input_segments = array<i32: 1, 0, 2>,\n result_segments = array<i32: 0, 0, 0>} {\n %zero = arith.constant 0 : i32\n %one = arith.constant 1 : i32\n %outer = scf.while (%i = %zero) : (i32) -> i32 {\n %index = arith.index_cast %i : i32 to index\n %begin = memref.load %input[%index] : memref<?xi32>\n %next = arith.addi %i, %one : i32\n %next_index = arith.index_cast %next : i32 to index\n %end = memref.load %input[%next_index] : memref<?xi32>\n %selected = arith.cmpi ult, %begin, %end : i32\n %selected_value = scf.if %selected -> (i32) {\n %inner:2 = scf.while (%j = %begin, %sum = %zero)\n : (i32, i32) -> (i32, i32) {\n %inner_index = arith.index_cast %j : i32 to index\n %value = memref.load %input[%inner_index] : memref<?xi32>\n %inner_next = arith.addi %j, %one : i32\n %next_sum = arith.addi %sum, %value : i32\n %continue = arith.cmpi ult, %inner_next, %end : i32\n scf.condition(%continue) %inner_next, %next_sum : i32, i32\n } do {\n ^bb0(%j: i32, %sum: i32):\n scf.yield %j, %sum : i32, i32\n }\n scf.yield %inner#1 : i32\n } else {\n scf.yield %zero : i32\n }\n memref.store %selected_value, %output[%index] : memref<?xi32>\n %continue = arith.cmpi slt, %next, %outer_limit : i32\n scf.condition(%continue) %next : i32\n } do {\n ^bb0(%i: i32):\n scf.yield %i : i32\n }\n dataflow.graph.return %start : none","why":"Accepted spelling of a graph-local scf.while over memref loads/stores under --loom-lower-graph-memory, including graph attributes and the scf.condition/after-block shape the grammar reproduces."}],"primary_bundle_sha256":"77d204616fa413f6b25386cd68224b22e427c7af0a2506da8dad95ea5143de6a","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"71e744e268f90ae5c09749b504552dc2fbc5784dba375c6fbbbeebc69be4934a"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 50108,
"duration_ms": 50147,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1816,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5149,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.14404999999999998,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3702,
"provider": "firstParty",
"thinkingTokens": 659,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module whose body consists only of `dataflow.graph` definitions and nothing else.\n2. Each `dataflow.graph` is declared `private`, carries a symbol name, and is given the attribute dictionary `input_segments = array<i32: 1, 0, 2>` together with `result_segments = array<i32: 0, 0, 0>`, i.e. one control-typed input, no second-class inputs, two memory inputs, and no results of any kind.\n3. Each graph's signature is `(%start: none, %limit: i32, %input: memref<?xi32>, %output: memref<?xi32>) -> ()`, so the graph produces no results and its memory operands are dynamically shaped one-dimensional `i32` memrefs that are block arguments of the graph region (canonical, unaliased roots).\n4. Each graph body is terminated by `dataflow.graph.return %start : none`, returning the incoming control token and no data values, consistent with the empty result list.\n5. Each graph body contains exactly one `scf.while` operation, and that loop is at the top level of the graph body \u2014 loops are never nested inside one another and never appear inside the before or after region of another loop.\n6. The `scf.while` is written in its explicit two-region form: a before region ending in `scf.condition`, and a `do` region whose entry block `^bb0` is explicitly labelled and whose body ends in `scf.yield`.\n7. The loop's result arity, its initializer list, its operand type list, its result type list, the arity of the `^bb0` block-argument list, the operand count of `scf.condition` after the condition value, and the operand count of `scf.yield` are all equal and all of type `i32`; the whole loop state is a homogeneous `i32` tuple.\n8. All loop-carried initializers are values defined before the loop in the same graph body (the `arith.constant` values `%zero` and `%one`), never loop-internal or region-local values.\n9. Every memory access is a scalar `memref.load` or `memref.store` on a dynamically shaped `memref<?xi32>` graph argument with exactly one index operand; no multi-dimensional, vector, strided, or aggregate accesses occur.\n10. Every index operand of a load or store is produced by an `arith.index_cast ... : i32 to index` applied to an `i32` SSA value available at that point; index values are never computed by `arith` index arithmetic, by `affine.apply`, or by constants of type `index` directly.\n11. Loads read only from `%input` and stores write only to `%output`; the two memrefs are never swapped, so no load\u2013store pair within a graph targets the same memref.\n12. Every SSA value is defined before its uses in the enclosing region, and values defined in the before region are never referenced in the after region or after the loop \u2014 cross-region communication happens exclusively through `scf.condition` operands and `^bb0` block arguments.\n13. The before region reads memory, computes the next loop state, optionally writes memory, computes an `i1` predicate with `arith.cmpi slt` on `i32` operands, and forwards exactly the computed next-state values through `scf.condition`; the value compared against the bound is the first (index-like) state lane.\n14. The loop-exit condition's bound operand is an `i32` value defined outside the loop \u2014 either a graph block argument or an `arith.constant` in the graph body \u2014 so the trip bound is loop-invariant.\n15. The after region yields exactly one value per loop lane, each of which is either an unmodified `^bb0` block argument or a value computed from block arguments within that same region; it never yields values captured from the before region.\n16. Any store performed in the after region indexes memory through an `arith.index_cast` of an after-region block argument, not through an index produced in the before region.\n17. Every result of the `scf.while` is consumed after the loop by at least one operation in the graph body, so no loop-exit lane is dead.\n18. Each post-loop consumption is a `memref.store` of the result into `%output` at a constant index obtained by `arith.index_cast` of an `i32` constant, so all exit values become observable memory effects.\n19. Within one graph body all SSA names are distinct, and the naming of values defined under a mode-dependent alternative never collides with names defined unconditionally.\n20. The program contains no function definitions, no calls, no branches other than the structured `scf.while`, no `if`/`for` constructs, no floating-point or non-`i32` scalar types, no allocations, deallocations, copies, subviews, casts of memrefs, or aliasing operations of any kind.\n21. Distinct graphs in one module have distinct symbol names and are mutually independent: no graph calls, references, or shares SSA values with another.\n\n## Sampling conventions\n\n1. The module holds either one or two graph definitions and never zero, three, or more.\n2. Graph symbols are named `@while_case` followed by the graph's zero-based position in the module, giving `@while_case0` and optionally `@while_case1`.\n3. Every graph uses the identical fixed signature and identical argument names `%start`, `%limit`, `%input`, `%output`; no other argument counts, orders, element types, or memref ranks are ever emitted.\n4. The attribute dictionary is emitted verbatim on every graph and is never varied or omitted.\n5. Every graph body opens with the same three-instruction constant preamble: `%zero = arith.constant 0 : i32`, `%one = arith.constant 1 : i32`, and `%bound = arith.constant <LIMIT> : i32`.\n6. The literal bound constant `LIMIT` is an integer chosen from 2 through 6 inclusive; no other magnitudes, negative values, or zero are emitted.\n7. The loop state width is either 2 or 3 lanes; one-lane and four-or-more-lane loops are never generated.\n8. Loop-state initializers are `%zero` for lanes 0 and 1, and `%one` for lane 2 when present; no other initializer combination is used.\n9. Loop state, loop results, block arguments, and yields are named with the fixed schemes `%s0/%s1/%s2` (initializers), `%b0/%b1/%b2` (after-region block arguments), `%n0/%n1/%n2` (next-state values), and `%res` for the loop result tuple.\n10. The before region always begins with the same fixed skeleton: index-cast of lane 0 (`%idx0`), a load `%v0` from `%input[%idx0]`, and an increment `%n0 = arith.addi %s0, %one`, so lane 0 is always an unit-stride counter.\n11. An optional second load is emitted or omitted; when emitted it index-casts `%n0` into `%idx1`, loads `%v1` from `%input[%idx1]`, and sums the two loaded values into `%vsum`, thereby producing two loads from the same memref at adjacent offsets in one iteration.\n12. Lane 1 is always updated as `%n1 = arith.addi %s1, X` where `X` is `%vsum` when the second load is present and `%v0` otherwise; no other accumulation expression is used.\n13. When the loop has three lanes, lane 2 is always updated as `%n2 = arith.addi %s2, %n0`, coupling the third lane to the freshly computed counter.\n14. An optional in-loop store is emitted or omitted; when emitted it is exactly `memref.store %n1, %output[%idx0]`, reusing the index already computed for the load, and it is placed after all state computation and before the comparison.\n15. The comparison is always `arith.cmpi slt` with `%n0` on the left; the right operand is either the graph argument `%limit` or the local constant `%bound`, chosen per graph, and no other predicate or operand order is emitted.\n16. The after region takes exactly one of three fixed shapes: a pure forwarding of all block arguments; a recomputation `%d1 = arith.addi %b1, %b0` whose result replaces lane 1 in the yield; or a store `memref.store %b1, %output[%bidx]` where `%bidx = arith.index_cast %b0`, with the yield still forwarding the unmodified block arguments.\n17. In the after region, lanes 0 and 2 are always forwarded unchanged; only lane 1 is ever recomputed.\n18. The post-loop epilogue is a fixed skeleton that stores result 0 at index 0 via `arith.index_cast %zero` and result 1 at index 1 via `arith.index_cast %one`; when a third lane exists, an extra `%otwo = arith.constant 2` is materialized and result 2 is stored at index 2.\n19. All per-graph shape decisions \u2014 lane count, bound magnitude, presence of the second load, presence of the in-loop store, choice of bound operand, and after-region mode \u2014 are drawn independently for each graph, so the two graphs in a module may differ in every respect except signature and naming scheme.\n20. Indentation is fixed: graph-body operations use two spaces and region-body operations use four, with the module braces and region delimiters laid out in a single fixed textual skeleton.\n21. All value names are reused verbatim across graphs, relying on each graph region being a separate SSA scope rather than generating globally unique names.",
"result_index": 0,
"session_id": "11fc4f03-41c3-4853-83f4-1be2087d9226",
"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": 39,
"total_cost_usd": 0.14404999999999998,
"ttft_ms": 11769,
"ttft_stream_ms": 1349,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5149,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5149,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3702,
"output_tokens_details": {
"thinking_tokens": 659
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "32a7893d-2a80-48cb-8dc7-f4e5262bcb4a"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 21469,
"duration_ms": 21492,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1601,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 6685,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.106485,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 1585,
"provider": "firstParty",
"thinkingTokens": 779,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition looks only at the output program's `dataflow.gate` operations whose second result has `none` type, treating the first operand of each such gate as a \"before condition selector,\" and it collects the set of those selector values. Against that set it selects two families of `dataflow.demux` operations in the output: \"condition lanes,\" whose first operand is one of the selectors and whose second operand is non-`none`-typed, and \"frontier lanes,\" whose first operand is a selector, whose second operand is `none`-typed, is not the second operand of any selected gate, and has a defining operation whose name is not `dataflow.carry` (a demux whose second operand is a block argument is therefore excluded). It makes one cross-program counting claim: the number of condition-lane demuxes must equal the total number of operands past the first, summed over every `scf.condition` operation in the input program; no other input construct is consulted, and the match is by count only, never by identity. Universally over condition lanes it requires exactly two results, each of which has at least one use; universally over the selected gates it requires the gate's second result to have at least one use, the existence of some output `dataflow.demux` whose first operand equals the gate's first result, and the existence of some output `dataflow.demux` sharing both of the gate's first two operands, having exactly two results, with its first result used at least once. Universally over frontier lanes it requires exactly two results and the existence of output demuxes over the same (selector, token) operand pair \u2014 possibly the lane itself, possibly a different one \u2014 one with a used first result and one with a used second result. All use requirements are merely \"at least one use\"; nothing constrains who the consumer is, what the lanes' types or names are beyond the stated ones, or that the gate and demux operations reside in the same region or loop.\n\nVacuity behaves as follows: if the output contains no `dataflow.gate` with a `none`-typed second result, both lane families and the gate quantifier are empty and every `forall` passes trivially, but the counting assertion still bites and rejects the output whenever the input contains any `scf.condition` with two or more operands. Conversely, when the input has no `scf.condition` operations (or each has at most one operand) and the output has no qualifying gates, the entire postcondition is vacuously satisfied; when gates do exist, the gate and condition-lane obligations are non-vacuous, while the frontier-lane obligations can still be vacuous if every `none`-typed selector demux is filtered out by the gate-operand or `dataflow.carry` exclusions.",
"result_index": 0,
"session_id": "954926d4-c6f6-4033-9ebb-15a6e7d9821a",
"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": 23,
"total_cost_usd": 0.106485,
"ttft_ms": 10731,
"ttft_stream_ms": 1164,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 6685,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 6685,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 1585,
"output_tokens_details": {
"thinking_tokens": 779
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "a33968f1-759e-4ca8-8d90-59a6a647aea7"
}
]
This paired revision was activated by an explicit partial-scope team review bound to both executable artifact hashes.
Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.