Selected stage: loom-lower-graph-memory. Test exactly output obligation mlir-obligation:447d1981847b34fd70e40ebb with its governing context; report any stage at

// Input domain for `loom-raise-opt --loom-lower-graph-memory`
// (docs/spec-compiler-part-3-mem.md, the owner named in linked-input-67).
//
// The sampled claim lives in section 7 (source-sequential `scf.for`): no
// dependence is removed because a loop appears parallelizable, and source
// iteration order stays authoritative.  The grammar therefore samples
// finalized `dataflow.graph` bodies whose memory work is *inside*
// source-sequential `scf.for` loops and whose per-iteration addresses are
// visibly independent (`a[i]`, `a[i*step]`, `a[i+lb]`), i.e. exactly the
// shapes that "appear parallelizable" to a reader.
//
// Input well-formedness taken from the documentation passages:
//   * every graph entry carries the leading `none` execution value
//     (linked-input-104);
//   * memory leaves are normalized scalar `memref.load` / `memref.store`
//     over a canonical linear (1-D) memory space (linked-input-202);
//   * memory capabilities are graph memory inputs bound by exact memref
//     type (linked-input-59, linked-input-80), never LLVM pointers, never
//     `memref.get_global` / `memref.alloca` / globals / unrealized casts
//     (linked-input-50, linked-input-66, linked-input-170);
//   * no residual `scf.parallel` or `scf.forall` is emitted, since raw or
//     unowned parallel input is rejected before mutation and would never
//     reach the section 7 lowering (linked-input-182, linked-input-200,
//     linked-input-149);
//   * structured control is arbitrary nesting of `scf.if`,
//     source-sequential `scf.for`, and `scf.while` (linked-input-184), and
//     never carries a memref result or memref loop state
//     (linked-input-104);
//   * no residual raw LLVM memory operation, atomic, fence or mem-intrinsic
//     is emitted (linked-input-29, linked-input-115).
//
// Sampling convention (recorded in AUTHORING-RESULT.md): every sampled loop
// body performs at least one `memref.store`, so every sampled loop really
// does carry a memory-order dependence across iterations.  A read-only loop
// body has no cross-iteration dependence to preserve and is out of the
// domain this PBT exercises.
//
// The grammar emits source inputs only; it never spells a dataflow actor,
// carry ring, or any expected output.

start: {new COUNT = random.randint(1, 3); new I = 0}
       graphs;

graphs: (I < COUNT) graph {I += 1} graphs
      | (I == COUNT) '';

graph: for_read_write_graph
     | for_write_only_graph
     | for_iter_arg_graph
     | for_if_graph
     | nested_for_graph
     | two_memref_graph;

// --------------------------------------------------------------- shapes

// a[i] = a[i] + v : one read and one write per iteration on one root.
for_read_write_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<16xi32>', 'i32'), ('memref<?xi64>', 'i64'), ('memref<32xi32>', 'i32')]); new NAME = 'rw_' + str(I); new IDX = '%idx'; new PFX = 'b'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64, %value: ' [MT[1]] ',\n'
  '    %a: ' [MT[0]] ') -> ()\n'
  '    attributes {input_segments = array<i32: 4, 0, 1>,\n'
  '                result_segments = array<i32: 0, 0, 0>} {\n'
  '  scf.for %i = %lb to %ub step %step : i64 {\n'
  index_form
  '    %' [PFX] 'loaded = memref.load %a[' [IDX] '] : ' [MT[0]] '\n'
  '    %' [PFX] 'next = ' add_op ' %' [PFX] 'loaded, %value : ' [MT[1]] '\n'
  '    memref.store %' [PFX] 'next, %a[' [IDX] '] : ' [MT[0]] '\n'
  '  }\n'
  '  dataflow.graph.return %start : none\n'
  '}\n\n';

// a[i] = v : a write-only loop with a distinct address per iteration.
for_write_only_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<64xi32>', 'i32'), ('memref<?xf32>', 'f32')]); new NAME = 'wo_' + str(I); new IDX = '%idx'; new PFX = 'w'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64, %value: ' [MT[1]] ',\n'
  '    %a: ' [MT[0]] ') -> ()\n'
  '    attributes {input_segments = array<i32: 4, 0, 1>,\n'
  '                result_segments = array<i32: 0, 0, 0>} {\n'
  '  scf.for %i = %lb to %ub step %step : i64 {\n'
  index_form
  '    memref.store %value, %a[' [IDX] '] : ' [MT[0]] '\n'
  '  }\n'
  '  dataflow.graph.return %start : none\n'
  '}\n\n';

// A loop with an ordinary (non-memref) iter_arg accumulated per iteration.
for_iter_arg_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<128xi32>', 'i32')]); new NAME = 'acc_' + str(I); new IDX = '%idx'; new PFX = 'a'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64, %init: ' [MT[1]] ',\n'
  '    %a: ' [MT[0]] ') -> (' [MT[1]] ')\n'
  '    attributes {input_segments = array<i32: 4, 0, 1>,\n'
  '                result_segments = array<i32: 1, 0, 0>} {\n'
  '  %total = scf.for %i = %lb to %ub step %step\n'
  '      iter_args(%state = %init) -> (' [MT[1]] ') : i64 {\n'
  index_form
  '    %' [PFX] 'loaded = memref.load %a[' [IDX] '] : ' [MT[0]] '\n'
  '    %' [PFX] 'sum = arith.addi %state, %' [PFX] 'loaded : ' [MT[1]] '\n'
  '    memref.store %' [PFX] 'sum, %a[' [IDX] '] : ' [MT[0]] '\n'
  '    scf.yield %' [PFX] 'sum : ' [MT[1]] '\n'
  '  }\n'
  '  dataflow.graph.return %start, %total : none, ' [MT[1]] '\n'
  '}\n\n';

// A conditionally executed access nested inside the loop body.
for_if_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<16xi32>', 'i32')]); new NAME = 'guard_' + str(I); new IDX = '%idx'; new PFX = 'g'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64, %limit: i64,\n'
  '    %value: ' [MT[1]] ', %a: ' [MT[0]] ') -> ()\n'
  '    attributes {input_segments = array<i32: 5, 0, 1>,\n'
  '                result_segments = array<i32: 0, 0, 0>} {\n'
  '  scf.for %i = %lb to %ub step %step : i64 {\n'
  index_form
  '    %' [PFX] 'cond = arith.cmpi slt, %i, %limit : i64\n'
  '    scf.if %' [PFX] 'cond {\n'
  '      memref.store %value, %a[' [IDX] '] : ' [MT[0]] '\n'
  '    }\n'
  '  }\n'
  '  dataflow.graph.return %start : none\n'
  '}\n\n';

// Nested source-sequential loops (linked-input-184 nesting).
nested_for_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<256xi32>', 'i32')]); new NAME = 'nest_' + str(I); new IDX = '%inner_idx'; new PFX = 'n'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64, %value: ' [MT[1]] ',\n'
  '    %a: ' [MT[0]] ') -> ()\n'
  '    attributes {input_segments = array<i32: 4, 0, 1>,\n'
  '                result_segments = array<i32: 0, 0, 0>} {\n'
  '  scf.for %outer = %lb to %ub step %step : i64 {\n'
  '    scf.for %i = %lb to %outer step %step : i64 {\n'
  '      %inner_idx = arith.index_cast %i : i64 to index\n'
  '      %' [PFX] 'loaded = memref.load %a[' [IDX] '] : ' [MT[0]] '\n'
  '      %' [PFX] 'next = arith.addi %' [PFX] 'loaded, %value : ' [MT[1]] '\n'
  '      memref.store %' [PFX] 'next, %a[' [IDX] '] : ' [MT[0]] '\n'
  '    }\n'
  '  }\n'
  '  dataflow.graph.return %start : none\n'
  '}\n\n';

// Two distinct graph memory inputs, conservatively may-alias
// (linked-input-126), both accessed from the same loop body.
two_memref_graph: {new MT = random.choice([('memref<?xi32>', 'i32'), ('memref<16xi32>', 'i32')]); new NAME = 'pair_' + str(I); new IDX = '%idx'; new PFX = 'p'}
  'dataflow.graph private @' [NAME]
  '(%start: none, %lb: i64, %ub: i64, %step: i64,\n'
  '    %a: ' [MT[0]] ', %b: ' [MT[0]] ') -> ()\n'
  '    attributes {input_segments = array<i32: 3, 0, 2>,\n'
  '                result_segments = array<i32: 0, 0, 0>} {\n'
  '  scf.for %i = %lb to %ub step %step : i64 {\n'
  index_form
  '    %' [PFX] 'loaded = memref.load %b[' [IDX] '] : ' [MT[0]] '\n'
  '    memref.store %' [PFX] 'loaded, %a[' [IDX] '] : ' [MT[0]] '\n'
  '  }\n'
  '  dataflow.graph.return %start : none\n'
  '}\n\n';

// -------------------------------------------------------- address forms

// Every form is a one-dimensional, per-iteration-distinct address on the
// canonical linear memory space, so the loop "appears parallelizable".
index_form: '    %idx = arith.index_cast %i : i64 to index\n'
          | '    %scaled = arith.muli %i, %step : i64\n'
            '    %idx = arith.index_cast %scaled : i64 to index\n'
          | '    %shifted = arith.addi %i, %lb : i64\n'
            '    %idx = arith.index_cast %shifted : i64 to index\n';

add_op: 'arith.addi'
      | 'arith.muli';