MS1V4 mlir-stage-13-v1 passing 5000/5000
Estimated confidence: 27.4%. Conservative lower bound: 9.3% (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 |
|---|---|---|---|
…/lib/Dataflow/IR/DataflowMemoryContracts.cppMS1V | 198/371lines53.4% 98/218branches45.0% | 234/371lines63.1%+36 123/218branches56.4%+25 | |
36 newly covered lines · 25 newly covered branches45 | |||
…/lib/Frontend/Lowering/LowerGraphMemoryPass.cppMS1V | 525/841lines62.4% 208/400branches52.0% | 557/841lines66.2%+32 229/400branches57.2%+21 | |
32 newly covered lines · 21 newly covered branches457 | |||
…/loom/include/Common/Artifact.hMS1V | 13/37lines35.1% 3/18branches16.7% | 13/37lines35.1%+0 3/18branches16.7%+0 | Open PBT |
…/include/Dataflow/IR/DataflowActorSemantics.hMS1V | 9/160lines5.6% 1/60branches1.7% | 9/160lines5.6%+0 1/60branches1.7%+0 | Open PBT |
…/include/Frontend/Lowering/StreamLoopAttrs.hMS1V | 31/41lines75.6% 10/14branches71.4% | 31/41lines75.6%+0 10/14branches71.4%+0 | Open PBT |
…/loom/lib/Common/IndexWidth.cppMS1V | 63/84lines75.0% 28/42branches66.7% | 63/84lines75.0%+0 28/42branches66.7%+0 | Open PBT |
…/loom/lib/Common/PointerLayout.cppMS1V | 36/58lines62.1% 16/32branches50.0% | 36/58lines62.1%+0 16/32branches50.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowActorSemantics.cppMS1V | 1089/1621lines67.2% 747/1330branches56.2% | 1089/1621lines67.2%+0 747/1330branches56.2%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowChannelOps.cppMS1V | 59/88lines67.0% 13/38branches34.2% | 59/88lines67.0%+0 13/38branches34.2%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowDialect.cppMS1V | 22/32lines68.8% 4/10branches40.0% | 22/32lines68.8%+0 4/10branches40.0%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowFunctionLikeOps.cppMS1V | 693/1097lines63.2% 264/592branches44.6% | 693/1097lines63.2%+0 264/592branches44.6%+0 | Open PBT |
…/lib/Dataflow/IR/DataflowOps.cppMS1V | 270/410lines65.9% 103/228branches45.2% | 270/410lines65.9%+0 103/228branches45.2%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchema.cppMS1V | 274/716lines38.3% 127/350branches36.3% | 274/716lines38.3%+0 127/350branches36.3%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaCodecInternal.hMS1V | 28/120lines23.3% 4/44branches9.1% | 28/120lines23.3%+0 4/44branches9.1%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchemaTypeCodec.cppMS1V | 85/516lines16.5% 55/374branches14.7% | 85/516lines16.5%+0 55/374branches14.7%+0 | Open PBT |
…/lib/Dataflow/Transforms/DataflowRewritePass.cppMS1V | 338/559lines60.5% 172/340branches50.6% | 338/559lines60.5%+0 172/340branches50.6%+0 | Open PBT |
…/lib/Frontend/Lowering/ExpandGraphMemrefCopyPass.cppMS1V | 79/90lines87.8% 20/22branches90.9% | 79/90lines87.8%+0 20/22branches90.9%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphIndexLowering.cppMS1V | 260/288lines90.3% 129/168branches76.8% | 260/288lines90.3%+0 129/168branches76.8%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphMemoryAddressing.cppMS1V | 189/557lines33.9% 83/442branches18.8% | 189/557lines33.9%+0 83/442branches18.8%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphParallelLowering.cppMS1V | 651/1243lines52.4% 284/786branches36.1% | 651/1243lines52.4%+0 284/786branches36.1%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphRegionAdmission.cppMS1V | 58/110lines52.7% 29/92branches31.5% | 58/110lines52.7%+0 29/92branches31.5%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphRegionLowering.cppMS1V | 1416/1626lines87.1% 532/680branches78.2% | 1416/1626lines87.1%+0 532/680branches78.2%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.cppMS1V | 934/1072lines87.1% 299/432branches69.2% | 934/1072lines87.1%+0 299/432branches69.2%+0 | Open PBT |
…/lib/Frontend/Lowering/GraphStreamBoundaryLowering.hMS1V | 4/4lines100.0% 4/4branches100.0% | 4/4lines100.0%+0 4/4branches100.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForToGraphPass.cppMS1V | 1033/1240lines83.3% 374/540branches69.3% | 1033/1240lines83.3%+0 374/540branches69.3%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForallToThreadPass.cppMS1V | 30/34lines88.2% 2/4branches50.0% | 30/34lines88.2%+0 2/4branches50.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphConstantsPass.cppMS1V | 80/83lines96.4% 18/24branches75.0% | 80/83lines96.4%+0 18/24branches75.0%+0 | Open PBT |
…/lib/Frontend/Lowering/Pipeline.cppMS1V | 18/21lines85.7% branchesnot measured | 18/21lines85.7%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/DeduplicateSCFWhileStatePass.cppMS1V | 13/135lines9.6% 0/60branches0.0% | 13/135lines9.6%+0 0/60branches0.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMArithToArithPass.cppMS1V | 300/319lines94.0% 94/116branches81.0% | 300/319lines94.0%+0 94/116branches81.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMCfToCfPass.cppMS1V | 77/80lines96.2% 8/8branches100.0% | 77/80lines96.2%+0 8/8branches100.0%+0 | Open PBT |
…/lib/Frontend/Raising/LiftCFToSCFPass.cppMS1V | 616/694lines88.8% 293/386branches75.9% | 616/694lines88.8%+0 293/386branches75.9%+0 | Open PBT |
…/lib/Frontend/Raising/MaterializeFMulAddPass.cppMS1V | 70/106lines66.0% 11/26branches42.3% | 70/106lines66.0%+0 11/26branches42.3%+0 | Open PBT |
…/lib/Frontend/Raising/NormalizeLiftedSCFExitPass.cppMS1V | 232/250lines92.8% 120/182branches65.9% | 232/250lines92.8%+0 120/182branches65.9%+0 | Open PBT |
…/lib/Frontend/Raising/Pipeline.cppMS1V | 10/19lines52.6% branchesnot measured | 10/19lines52.6%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/SCFForToForallPass.cppMS1V | 494/738lines66.9% 241/458branches52.6% | 494/738lines66.9%+0 241/458branches52.6%+0 | Open PBT |
…/lib/Frontend/Raising/SCFWhileToForPass.cppMS1V | 164/176lines93.2% 70/94branches74.5% | 164/176lines93.2%+0 70/94branches74.5%+0 | Open PBT |
…/loom/tools/loom-raise-opt/loom-raise-opt.cppMS1V | 12/12lines100.0% branchesnot measured | 12/12lines100.0%+0 branchesnot measured | Open PBT |
Review PR: Regression test from seed 207
Review PR: Regression test from seed 3
Review PR: Regression test from seed 31
Review PR: Regression test from seed 40
Review PR: Regression test from seed 528
Review PR: Regression test from seed 1608
Review PR: Regression test from seed 1617
Review PR: Regression test from seed 2
Review PR: Regression test from seed 207
Review PR: Regression test from seed 2249
Review PR: Regression test from seed 2449
Review PR: Regression test from seed 2631
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. LLVM target-specific sync scopes without
module attributes { llvm.data_layout = "e-p:64:64", dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>> } { dataflow.graph private @source_memory_graph( %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32, %index: i64, %cond: i1) -> () attributes {input_segments = array<i32: 5, 0, 0>, result_segments = array<i32: 0, 0, 0>} { %ptr = llvm.getelementptr inbounds %base[%index] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8> %val1 = llvm.load volatile %ptr {alignment = 4 : i64} : !llvm.ptr -> i32 %rmw3 = llvm.atomicrmw _and %ptr, %desired release {alignment = 4 : i64} : !llvm.ptr, i32 %rmw4 = llvm.atomicrmw umax %ptr, %desired syncscope("system") acquire {alignment = 8 : i64} : !llvm.ptr, i32 dataflow.graph.return %start : none } }
module attributes { llvm.data_layout = "e-p:64:64", dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>> } { dataflow.graph private @source_memory_graph( %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32, %index: i64, %cond: i1) -> () attributes {input_segments = array<i32: 5, 0, 0>, result_segments = array<i32: 0, 0, 0>} { %ptr = llvm.getelementptr inbounds %base[%index] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8> llvm.store %desired, %ptr : i32, !llvm.ptr llvm.store volatile %desired, %ptr {alignment = 8 : i64} : i32, !llvm.ptr %val2 = llvm.load %ptr atomic seq_cst {alignment = 8 : i64} : !llvm.ptr -> i32 llvm.fence syncscope("system") seq_cst 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 source memory inputs for loom-lower-graph-memory. // One construction-local dataflow.graph whose body holds supported residual // LLVM memory leaves (load/store including volatile and atomic contracts, // atomicrmw, cmpxchg, fence) over one pointer-addressed graph value input. // The graph entry carries the leading `none` execution value, the module // declares one canonical index width, and every atomic access carries an // explicit power-of-two source alignment. start: {new COUNT = random.randint(1, 6); new I = 0; new REGION = random.choice(['FLAT', 'FLAT', 'IF', 'FOR'])} 'module attributes {\n' ' llvm.data_layout = "e-p:64:64",\n' ' dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>>\n' '} {\n' ' dataflow.graph private @source_memory_graph(\n' ' %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32,\n' ' %index: i64, %cond: i1) -> ()\n' ' attributes {input_segments = array<i32: 5, 0, 0>,\n' ' result_segments = array<i32: 0, 0, 0>} {\n' ' %ptr = llvm.getelementptr inbounds %base[%index]\n' ' : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8>\n' region_open leaves region_close ' dataflow.graph.return %start : none\n' ' }\n' '}\n'; // Sequential composition, or one structured region that the owner lowers // recursively after the memory leaves have been normalized. region_open: (REGION == 'FLAT') '' | (REGION == 'IF') ' scf.if %cond {\n' | (REGION == 'FOR') ' %lower = arith.constant 0 : index\n' ' %upper = arith.constant 4 : index\n' ' %step = arith.constant 1 : index\n' ' scf.for %iv = %lower to %upper step %step {\n'; region_close: (REGION == 'FLAT') '' | (REGION == 'IF') ' }\n' | (REGION == 'FOR') ' }\n'; leaves: (I < COUNT) leaf {I += 1} leaves | (I == COUNT) ''; leaf: load_plain | load_volatile | load_atomic | store_plain | store_volatile | store_atomic | rmw_leaf // Sampling convention: a compare-exchange leaf is sampled only in // sequential composition. See AUTHORING-RESULT.md. | (REGION == 'FLAT') cmpxchg_leaf | fence_leaf; // Supported LLVM load forms: plain, volatile, and atomic contract. load_plain: ' %val' num ' = llvm.load %ptr : !llvm.ptr -> i32\n'; load_volatile: ' %val' num ' = llvm.load volatile %ptr {alignment = ' align ' : i64} : !llvm.ptr -> i32\n'; load_atomic: ' %val' num ' = llvm.load %ptr atomic' scope ' ' load_order ' {alignment = ' align ' : i64} : !llvm.ptr -> i32\n'; // Supported LLVM store forms: plain, volatile, and atomic contract. store_plain: ' llvm.store %desired, %ptr : i32, !llvm.ptr\n'; store_volatile: ' llvm.store volatile %desired, %ptr {alignment = ' align ' : i64} : i32, !llvm.ptr\n'; store_atomic: ' llvm.store %desired, %ptr atomic' scope ' ' store_order ' {alignment = ' align ' : i64} : i32, !llvm.ptr\n'; // Supported LLVM read-modify-write form. rmw_leaf: ' %rmw' num ' = llvm.atomicrmw ' rmw_kind ' %ptr, %desired' scope ' ' rmw_order ' {alignment = ' align ' : i64} : !llvm.ptr, i32\n'; // Supported LLVM compare-exchange form. cmpxchg_leaf: ' %pair' num ' = llvm.cmpxchg ' volatile_mark '%ptr, %expected, %desired' scope ' ' rmw_order ' ' load_order ' {alignment = ' align ' : i64} : !llvm.ptr, i32\n'; // Supported LLVM fence form. fence_leaf: ' llvm.fence' scope ' ' fence_order '\n'; num: [str(I)]; volatile_mark: '' | 'volatile '; // Only the system scope and the single-thread scope have a compiler-target // owner; a target-specific scope is out of the supported input domain. scope: '' | ' syncscope("singlethread")' | ' syncscope("system")'; align: '4' | '8'; load_order: 'monotonic' | 'acquire' | 'seq_cst'; store_order: 'monotonic' | 'release' | 'seq_cst'; rmw_order: 'monotonic' | 'acquire' | 'release' | 'acq_rel' | 'seq_cst'; fence_order: 'acquire' | 'release' | 'acq_rel' | 'seq_cst'; rmw_kind: 'xchg' | 'add' | 'sub' | '_and' | '_or' | '_xor' | 'max' | 'min' | 'umax' | 'umin';
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, andfenceforms are then normalized before recursive region lowering, after which the same frontier rules apply.
candidate.spctpostcondition llvm_memory_forms_are_expanded_and_normalized { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-mem.md:L482-L486"; } // The LLVM memcpy/memmove/memset intrinsic spellings, which the claim // expands into structured loop semantics before ownership selection. definition is_expanded_intrinsic(op: mlir::Operation): Bool = op.name == "llvm.intr.memcpy" or op.name == "llvm.intr.memcpy.inline" or op.name == "llvm.intr.memmove" or op.name == "llvm.intr.memset" or op.name == "llvm.intr.memset.inline"; // The supported LLVM load/store (including volatile and atomic contracts), // atomicrmw, cmpxchg, and fence spellings, which the claim normalizes // before recursive region lowering. definition is_normalized_leaf(op: mlir::Operation): Bool = op.name == "llvm.load" or op.name == "llvm.store" or op.name == "llvm.atomicrmw" or op.name == "llvm.cmpxchg" or op.name == "llvm.fence"; constraints { let graphs = seq { op | op in output.operations where op.name == "dataflow.graph" }; forall g in graphs { assert intrinsics_expanded: none op in output.operations where mlir::contains(g, op) and is_expanded_intrinsic(op); assert supported_leaves_normalized: none op in output.operations where mlir::contains(g, op) and is_normalized_leaf(op); } } }
module attributes { llvm.data_layout = "e-p:64:64", dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>> } { dataflow.graph private @source_memory_graph( %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32, %index: i64, %cond: i1) -> () attributes {input_segments = array<i32: 5, 0, 0>, result_segments = array<i32: 0, 0, 0>} { %ptr = llvm.getelementptr inbounds %base[%index] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8> %val1 = llvm.load volatile %ptr {alignment = 4 : i64} : !llvm.ptr -> i32 %rmw3 = llvm.atomicrmw _and %ptr, %desired release {alignment = 4 : i64} : !llvm.ptr, i32 %rmw4 = llvm.atomicrmw umax %ptr, %desired syncscope("system") acquire {alignment = 8 : i64} : !llvm.ptr, i32 dataflow.graph.return %start : none } }
20260911-083853started2026-09-11T08:38:53Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
module attributes { llvm.data_layout = "e-p:64:64", dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>> } { dataflow.graph private @source_memory_graph( %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32, %index: i64, %cond: i1) -> () attributes {input_segments = array<i32: 5, 0, 0>, result_segments = array<i32: 0, 0, 0>} { %ptr = llvm.getelementptr inbounds %base[%index] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8> llvm.store %desired, %ptr : i32, !llvm.ptr llvm.store volatile %desired, %ptr {alignment = 8 : i64} : i32, !llvm.ptr %val2 = llvm.load %ptr atomic seq_cst {alignment = 8 : i64} : !llvm.ptr -> i32 llvm.fence syncscope("system") seq_cst dataflow.graph.return %start : none } }
"builtin.module"() ({ "dataflow.graph"() <{function_type = (!llvm.ptr, i32, i32, i64, i1, memref<?xi32>) -> (), input_segments = array<i32: 5, 0, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "source_memory_graph", sym_visibility = "private"}> ({ ^bb0(%arg0: none, %arg1: !llvm.ptr, %arg2: i32, %arg3: i32, %arg4: i64, %arg5: i1, %arg6: memref<?xi32>): %0 = "llvm.getelementptr"(%arg1, %arg4) <{elem_type = !llvm.array<4 x i8>, noWrapFlags = 3 : i32, rawConstantIndices = array<i32: -2147483648>}> : (!llvm.ptr, i64) -> !llvm.ptr %1 = "dataflow.store"(%arg6, %0, %arg3, %arg0) <{contract = #dataflow.plain_access<is_volatile = false>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> none %2 = "dataflow.store"(%arg6, %0, %arg3, %1) <{contract = #dataflow.plain_access<is_volatile = true>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> none %3:2 = "dataflow.load"(%arg6, %0, %2) <{contract = #dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 8>}> : (memref<?xi32>, !llvm.ptr, none) -> (i32, none) %4 = "dataflow.fence"(%3#1) <{contract = #dataflow.fence_contract<ordering = seq_cst, sync_scope = <system>>}> : (none) -> none "dataflow.graph.return"(%4) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> () }) : () -> () }) {dlti.dl_spec = #dlti.dl_spec<index = 64 : i64>, llvm.data_layout = "e-p:64:64"} : () -> ()
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":"3-6","path":"docs/spec-compiler-part-3-mem.md","roles":["applicability","context"],"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 that normalizes supported memory leaves and recursively lowers structured graph regions; fixes the pass under test and the graph-local applicability of the claim."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"23-41","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"The 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.","why":"The supported input domain: atomic load/store, rmw, cmpxchg, fence and volatile contracts, normalized scalar leaves over a canonical linear memory space, sequential composition, and nesting of scf.if / source-sequential scf.for. Drives the sampled leaf forms and the optional structured region in the grammar."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"43-46","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness"],"text":"The 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":"The lowering selects no schedule policy, so generated inputs must already be normalized structured input; justifies excluding scf.parallel/forall from sampling."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"99-106","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction"],"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":"A source pointer may be retained as a first-class graph value consumed by a pointer-addressed actor with an independently bound service capability, and unrealized_conversion_cast is never a bridge; justifies the !llvm.ptr graph value input plus typed GEP access function used by the sampled leaves."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"136-140","path":"docs/spec-compiler-part-3-mem.md","roles":["input_construction","input_well_formedness"],"text":"A memory input binds an established external memref capability through an\nexact graph-launch type match. An LLVM pointer never satisfies a graph memory\nport. A first-class pointer value used by a `PointerAddressed` actor resolves\nthrough the runtime object registry to one object and byte offset independently\nof the service-capability binding.","why":"An LLVM pointer never satisfies a graph memory port; the sampled pointer is a value input, not a memory input, which fixes the input_segments classification of the generated graph."},{"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 (raw parallel SCF, effectful/unmodeled nested ops, non-normalized access forms, memref-carrying structured control, missing leading none execution value); every generated input avoids these so the claim's inputs stay inside the accepted domain."},{"file_sha256":"6410a79f49a8948c0858239ee95ae88854c74469afe91ec0e22773de50fba131","kind":"documentation_input","lines":"486-493","path":"docs/spec-compiler-part-3-mem.md","roles":["input_well_formedness","context"],"text":"which the same frontier rules apply. LLVM target-specific sync scopes without\na compiler-target owner and atomic accesses without an explicit power-of-two\nsource alignment fail closed. Every residual raw LLVM memory operation fails\nclosed. The finalized-graph gate also rejects residual\n`memref.load`/`memref.store`, `memref.get_global`, raw pointer arithmetic,\npointer-bearing operations, `builtin.unrealized_conversion_cast`, and unknown\nmemory-capability producers. An unsupported effectful operation inside a\nstructured region must likewise fail closed instead of being hoisted.","why":"Governing context of the selected obligation: unsupported sync scopes and atomic accesses without an explicit power-of-two alignment fail closed, and residual raw LLVM memory operations fail closed. Constrains the sampled sync scopes to system/singlethread and every sampled atomic leaf to an explicit power-of-two alignment."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"838-873","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.\n\n This is the only canonical graph definition surface.\n }];\n\n let arguments = (ins\n SymbolNameAttr:$sym_name,\n TypeAttrOf<FunctionType>:$function_type,\n DenseI32ArrayAttr:$input_segments,\n DenseI32ArrayAttr:$result_segments,\n OptionalAttr<StrAttr>:$sym_visibility,\n OptionalAttr<DictArrayAttr>:$arg_attrs,\n OptionalAttr<DictArrayAttr>:$res_attrs);\n\n let regions = (region SizedRegion<1>:$body);","why":"dataflow.graph definition: module-scope symbol, single body region, required input_segments/result_segments payload classification, and the distinguished leading none start block argument. Fixes the exact spelling of the generated graph shell."},{"file_sha256":"34146c800f3e3b4f3b6b5669f141c5917299da28c40e543fee3a3638d6c626d3","kind":"verifier","lines":"51-66,89-95,126-138","path":"lib/Frontend/Lowering/LowerGraphMemoryPass.cpp","roles":["input_construction"],"text":"bool isGraphPtrBlockArg(::mlir::Value v, ::dataflow::GraphOp graph) {\n auto blockArg = ::llvm::dyn_cast<::mlir::BlockArgument>(v);\n if (!blockArg || blockArg.getOwner() != &graph.getBody().front())\n return false;\n return ::llvm::isa<::mlir::LLVM::LLVMPointerType>(blockArg.getType());\n}\n\n// The distinguished leading `none` block argument is the graph start firing\n// token; it is separate from the payload-only FunctionType.\n::mlir::Value getThreadCtrl(::dataflow::GraphOp graph) {\n ::mlir::Block &entry = graph.getBody().front();\n if (entry.getNumArguments() == 0)\n return {};\n ::mlir::Value first = entry.getArgument(0);\n return ::llvm::isa<::mlir::NoneType>(first.getType()) ? first\n : ::mlir::Value{};\n }\n};\n\n::mlir::Value resolvePointerServiceRoot(::mlir::Value pointer,\n ::dataflow::GraphOp graph) {\n return ::loom::lowering::resolveMemoryServiceBoundaryRoot(\n pointer,\n}\n\n::mlir::Value getImportedMemrefView(\n ::dataflow::GraphOp graph,\n ::llvm::DenseMap<ImportedViewKey, ::mlir::Value, ImportedViewKeyInfo>\n &cache,\n ::mlir::Value ptr, ::mlir::Type elem, ::mlir::Location loc) {\n if (!isGraphPtrBlockArg(ptr, graph))\n return {};\n ImportedViewKey key{ptr, elem};\n if (auto it = cache.find(key); it != cache.end())\n return it->second;\n auto memrefTy = ::mlir::MemRefType::get({::mlir::ShapedType::kDynamic}, elem);","why":"Acceptance implementation for the graph entry start token and for an !llvm.ptr entry block argument as the address root that gets an imported memref view appended; establishes that the sampled pointer value input is a resolvable root for the LLVM leaves."},{"file_sha256":"34146c800f3e3b4f3b6b5669f141c5917299da28c40e543fee3a3638d6c626d3","kind":"verifier","lines":"473-483,539-566","path":"lib/Frontend/Lowering/LowerGraphMemoryPass.cpp","roles":["input_well_formedness"],"text":"std::optional<::dataflow::SyncScopeRefAttr>\nconvertSyncScope(::mlir::MLIRContext *context,\n std::optional<::llvm::StringRef> syncscope) {\n if (!syncscope || syncscope->empty() || *syncscope == \"system\")\n return ::dataflow::SyncScopeRefAttr::get(\n context, ::dataflow::SyncScopeKind::System);\n if (*syncscope == \"singlethread\" || *syncscope == \"single_thread\")\n return ::dataflow::SyncScopeRefAttr::get(\n context, ::dataflow::SyncScopeKind::SingleThread);\n return std::nullopt;\n}\nstd::optional<::dataflow::AtomicAccessContractAttr>\nmakeAtomicAccessContract(AtomicOp op, ::mlir::MLIRContext *context,\n ::mlir::Type dataType) {\n auto ordering = convertAtomicOrdering(op.getOrdering());\n auto scope = convertSyncScope(context, op.getSyncscope());\n auto alignment = op.getAlignment();\n if (!ordering || !scope || !alignment || *alignment == 0 ||\n !::llvm::isPowerOf2_64(*alignment)) {\n op.emitError(\n \"loom-lower-graph-memory: atomic source requires a supported \"\n \"ordering/scope and an explicit power-of-two alignment\");\n return std::nullopt;\n }\n std::optional<::dataflow::VectorAtomicGranularity> granularity;\n if (auto vector = ::llvm::dyn_cast<::mlir::VectorType>(dataType)) {\n if (vector.isScalable() || vector.getRank() == 0 ||\n vector.getNumElements() == 0) {\n op.emitError(\"loom-lower-graph-memory: scalable or empty atomic vector is \"\n \"not representable\");\n return std::nullopt;\n }\n granularity = ::dataflow::VectorAtomicGranularity::WholePayload;\n }\n return ::dataflow::AtomicAccessContractAttr::get(\n context, *ordering, *scope, *alignment, granularity,\n op.getVolatile_());\n}","why":"Sync-scope acceptance (empty/system and singlethread/single_thread only) and the explicit nonzero power-of-two alignment requirement for atomic accesses; fixes the sampled syncscope spellings and alignment values."},{"file_sha256":"34146c800f3e3b4f3b6b5669f141c5917299da28c40e543fee3a3638d6c626d3","kind":"verifier","lines":"567-572,589-596,878-890,901-921","path":"lib/Frontend/Lowering/LowerGraphMemoryPass.cpp","roles":["applicability","input_construction"],"text":"// Translate the LLVM memory spelling while keeping all ordering, scope,\n// alignment, volatility, and atomic-action semantics in Dataflow contracts.\nbool tryRewriteOne(::mlir::Operation *op, ::mlir::OpBuilder &builder,\n RewriteCtx &ctx) {\n if (auto fence = ::llvm::dyn_cast<::mlir::LLVM::FenceOp>(op)) {\n auto ordering = convertAtomicOrdering(fence.getOrdering());\n ::mlir::Value ptrArg;\n ::mlir::Type elemTy;\n const bool isLoad = ::llvm::isa<::mlir::LLVM::LoadOp>(op);\n const bool isStore = ::llvm::isa<::mlir::LLVM::StoreOp>(op);\n const bool isRmw = ::llvm::isa<::mlir::LLVM::AtomicRMWOp>(op);\n const bool isCmpXchg = ::llvm::isa<::mlir::LLVM::AtomicCmpXchgOp>(op);\n if (isLoad) {\n auto load = ::llvm::cast<::mlir::LLVM::LoadOp>(op);\n // Collect rewrite targets up front so the walk is independent of\n // mutations performed by tryRewriteOne.\n ::llvm::SmallVector<::mlir::Operation *, 16> targets;\n graph.getBody().walk([&](::mlir::Operation *op) {\n if (::llvm::isa<::mlir::LLVM::LoadOp, ::mlir::LLVM::StoreOp,\n ::mlir::LLVM::AtomicRMWOp,\n ::mlir::LLVM::AtomicCmpXchgOp,\n ::mlir::LLVM::FenceOp>(op))\n targets.push_back(op);\n return ::mlir::WalkResult::advance();\n });\n\n for (::mlir::Operation *target : targets)\n::mlir::LogicalResult checkResidualMemoryEffects(::dataflow::GraphOp graph) {\n ::mlir::WalkResult result =\n graph.getBody().walk(\n [](::mlir::Operation *op) -> ::mlir::WalkResult {\n bool lacksCompletion =\n ::llvm::isa<::mlir::LLVM::LoadOp, ::mlir::LLVM::StoreOp,\n ::mlir::LLVM::AtomicRMWOp,\n ::mlir::LLVM::AtomicCmpXchgOp,\n ::mlir::LLVM::FenceOp, ::mlir::LLVM::MemcpyOp,\n ::mlir::LLVM::MemmoveOp, ::mlir::LLVM::MemsetOp,\n ::mlir::LLVM::AllocaOp>(op);\n if (!lacksCompletion)\n return ::mlir::WalkResult::advance();\n\n op->emitError()\n << \"loom-lower-graph-memory: residual memory operation '\"\n << op->getName().getStringRef()\n << \"' has no explicit completion event or local-memory \"\n \"normalization\";\n return ::mlir::WalkResult::interrupt();\n });","why":"The set of LLVM leaf spellings the owner rewrites (fence, load, store, atomicrmw, cmpxchg) and the residual-memory-effect gate listing those plus the memcpy/memmove/memset intrinsics; identifies the exact op set the claim's inputs must contain and the output must no longer contain."},{"file_sha256":"d319fc0dc5c2da65797de37d1e48d1303be02ec7d72ac1796bb45973b616d9ef","kind":"implementation","lines":"107-140","path":"lib/Frontend/Lowering/GraphRegionAdmission.cpp","roles":["input_well_formedness"],"text":"GraphLeafLowering classifyGraphLoweringLeaf(mlir::Operation *operation) {\n const bool isEffectFree =\n mlir::isMemoryEffectFree(operation) ||\n dataflow::isCanonicalDataflowActor(\n operation, dataflow::CanonicalDataflowActorKind::Compute);\n if (operation->getNumRegions() == 0 && isEffectFree &&\n (dataflow::isCanonicalDataflowActor(operation) ||\n isGraphMemoryAddressLeaf(operation)))\n return GraphLeafLowering::Movable;\n if (llvm::isa<mlir::memref::AssumeAlignmentOp,\n mlir::memref::DistinctObjectsOp, mlir::memref::LoadOp,\n mlir::memref::StoreOp, mlir::vector::TransferReadOp,\n mlir::vector::TransferWriteOp, mlir::memref::DeallocOp,\n dataflow::LoadOp, dataflow::StoreOp, dataflow::AtomicRmwOp,\n dataflow::CmpXchgOp, dataflow::FenceOp, dataflow::ChannelSendOp,\n dataflow::ChannelReceiveOp>(operation))\n return GraphLeafLowering::Implemented;\n if (detail::isGraphRegionRepresentationBitcast(operation))\n return GraphLeafLowering::Implemented;\n if (llvm::isa<mlir::LLVM::LoadOp, mlir::LLVM::StoreOp,\n mlir::LLVM::AtomicRMWOp, mlir::LLVM::AtomicCmpXchgOp,\n mlir::LLVM::FenceOp, mlir::LLVM::MemcpyOp,\n mlir::LLVM::MemmoveOp, mlir::LLVM::MemsetOp>(operation))\n return GraphLeafLowering::Implemented;\n // Static LLVM stack objects are normalized by graph-memory lowering before\n // structured regions are flattened. Unsupported dynamic or aggregate forms\n // fail at that owner with a typed diagnostic.\n if (llvm::isa<mlir::LLVM::AllocaOp>(operation))\n return GraphLeafLowering::Implemented;\n if (llvm::isa<mlir::LLVM::LifetimeStartOp, mlir::LLVM::LifetimeEndOp>(\n operation))\n return GraphLeafLowering::Implemented;\n if (llvm::isa<mlir::memref::AllocOp>(operation))\n return isGraphFrontier(operation->getBlock())","why":"Graph leaf classification showing which leaves are admitted for graph-region lowering; non-normative evidence that the sampled LLVM memory leaves are accepted rather than treated as unmodeled effectful ops."},{"file_sha256":"128c6033549d3d40d46cc75197f2cd1afa403cf42c3bc80daf06397a1ea25522","kind":"test","lines":"5,54-79","path":"test/raise/scf-to-dfg-serial-actor-completion-invalid.mlir","roles":["input_construction"],"text":"// RUN: loom-raise-opt --loom-lower-graph-memory --mlir-disable-threading %t.dir/source.mlir | FileCheck %s --check-prefix=SOURCE\n//--- source.mlir\nmodule attributes {\n llvm.data_layout = \"e-p:64:64\",\n dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>>\n} {\n dataflow.graph private @source_atomic(\n %start: none, %base: !llvm.ptr, %expected: i32, %desired: i32,\n %index: i64) -> ()\n attributes {input_segments = array<i32: 4, 0, 0>,\n result_segments = array<i32: 0, 0, 0>} {\n %ptr = llvm.getelementptr inbounds %base[%index]\n : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8>\n %old = llvm.atomicrmw add %ptr, %desired monotonic {alignment = 4 : i64}\n : !llvm.ptr, i32\n %pair = llvm.cmpxchg volatile %ptr, %expected, %desired\n syncscope(\"singlethread\") acq_rel monotonic {alignment = 4 : i64}\n : !llvm.ptr, i32\n %old_pair = llvm.extractvalue %pair[0] : !llvm.struct<(i32, i1)>\n %success = llvm.extractvalue %pair[1] : !llvm.struct<(i32, i1)>\n llvm.fence seq_cst\n llvm.store volatile %old_pair, %ptr {alignment = 4 : i64}\n : i32, !llvm.ptr\n llvm.store %success, %ptr : i1, !llvm.ptr\n dataflow.graph.return %start : none\n }\n}","why":"Existing accepted input for --loom-lower-graph-memory with a module-level data layout and index dl_spec, one dataflow.graph with an !llvm.ptr value input, a typed GEP, and llvm.atomicrmw / llvm.cmpxchg / llvm.fence / volatile llvm.store leaves. Non-normative model for the generated input spelling."},{"file_sha256":"128c6033549d3d40d46cc75197f2cd1afa403cf42c3bc80daf06397a1ea25522","kind":"example","lines":"15-24,36-52","path":"test/raise/scf-to-dfg-serial-actor-completion-invalid.mlir","roles":["input_construction"],"text":"//--- fence.mlir\ndataflow.graph private @serial_fence(%start: none, %cond: i1) -> ()\n attributes {input_segments = array<i32: 1, 0, 0>,\n result_segments = array<i32: 0, 0, 0>} {\n scf.if %cond {\n %done = dataflow.fence %start\n {contract = #dataflow.fence_contract<ordering = seq_cst,\n sync_scope = <system>>}\n }\n dataflow.graph.return %start : none\n\n//--- atomic.mlir\ndataflow.graph private @serial_atomic(\n %start: none, %cond: i1, %a: memref<10xi32>) -> ()\n attributes {input_segments = array<i32: 1, 0, 1>,\n result_segments = array<i32: 0, 0, 0>} {\n %c0 = arith.constant 0 : index\n %v = arith.constant 7 : i32\n scf.if %cond {\n %old, %done = dataflow.atomic_rmw %a[%c0] %v %start\n {contract = #dataflow.rmw_contract<kind = add,\n access = <ordering = monotonic, sync_scope = <system>,\n source_alignment_bytes = 4>>}\n : memref<10xi32>\n }\n dataflow.graph.return %start : none\n}","why":"Shows effectful memory actors nested in one scf.if inside a graph body accepted by the same pass; one accepted spelling for the optional structured region sampled by the grammar."},{"file_sha256":"62de9dab33ec24a09ff8453454afc607e608a9e499d432db2f43183e79d5480a","kind":"example","lines":"22-45","path":"test/raise/lower-graph-memory-index-width.mlir","roles":["input_well_formedness"],"text":"//--- declared.mlir\nmodule attributes {\n llvm.data_layout = \"e-p:64:64\",\n dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 32>>\n} {\n dataflow.thread private @declared_index\n domain(#dataflow.thread_domain<dense>)(%base: !llvm.ptr, %address: i16)\n ctrl (%ctrl: none) {\n \"loom.spatial_region\"(%address, %base)\n <{operandSegmentSizes = array<i32: 2, 0, 0, 0>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0(%offset: i16, %memory: !llvm.ptr):\n %ptr = llvm.getelementptr inbounds %memory[%offset]\n : (!llvm.ptr, i16) -> !llvm.ptr, !llvm.array<4 x i8>\n %value = llvm.load %ptr : !llvm.ptr -> f32\n llvm.store %value, %ptr : f32, !llvm.ptr\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"declared_index_graph\", source_maps = []} :\n (i16, !llvm.ptr) -> ()\n dataflow.thread.yield\n }\n}","why":"One accepted spelling of the module-level llvm.data_layout plus dlti index width that the pass requires as a canonical graph index width; the generated module reuses that declaration form."}],"primary_bundle_sha256":"dcc990660cebf9daaf21f38e5d68da59847ad718e741457f71b07dd8ac5e0c88","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"65b9a1cd58d14bdc1cb2924ac673668d8ce846f21b8f43ff58779cb90760b058"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 40454,
"duration_ms": 40499,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1536,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 4984,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.129375,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3181,
"provider": "firstParty",
"thinkingTokens": 176,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module whose `module attributes` carry both `llvm.data_layout = \"e-p:64:64\"` and a `dlti.dl_spec` declaring exactly one entry, `#dlti.dl_entry<index, 64>`, so an index width is always declared at module scope.\n2. The module contains exactly one operation, a `dataflow.graph` named `@source_memory_graph` with `private` visibility.\n3. The graph's signature is fixed at six block arguments in this order and with these types: `%start: none`, `%base: !llvm.ptr`, `%expected: i32`, `%desired: i32`, `%index: i64`, `%cond: i1`, and it returns `()`.\n4. The leading graph argument is always the `none`-typed execution value `%start`, and the graph body always terminates with `dataflow.graph.return %start : none`, so the execution token entering the graph is the one returned.\n5. The graph carries the attributes `input_segments = array<i32: 5, 0, 0>` and `result_segments = array<i32: 0, 0, 0>`, i.e. five non-execution inputs and no results, consistent with the six-argument/zero-result signature.\n6. The first body operation is always a pointer computation, `llvm.getelementptr inbounds %base[%index] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8>`, producing `%ptr`.\n7. Every memory leaf in the body addresses that single derived pointer `%ptr`; no leaf addresses `%base` or any other pointer, and no additional pointer is ever computed.\n8. Every value an operation consumes is either a graph block argument (`%desired`, `%expected`, `%index`, `%base`, `%cond`, `%start`) or `%ptr`; loaded values, `atomicrmw` results and `cmpxchg` results are never consumed by any later operation.\n9. The data type of every memory access is `i32`, and the GEP index type is `i64`, matching the declared 64-bit index width.\n10. The body's memory leaves are drawn only from the residual LLVM memory set: `llvm.load` (plain, volatile, atomic), `llvm.store` (plain, volatile, atomic), `llvm.atomicrmw`, `llvm.cmpxchg`, and `llvm.fence`; no other LLVM operation and no non-memory computation appear among the leaves.\n11. Every operation with an atomic contract \u2014 atomic load, atomic store, `atomicrmw`, `cmpxchg` \u2014 and every volatile load or volatile store carries an explicit `{alignment = N : i64}` attribute whose value is a power of two.\n12. Plain (non-volatile, non-atomic) loads and stores carry no alignment attribute, and `llvm.fence` carries neither an alignment attribute nor an operand.\n13. Memory orderings are constrained per operation class: atomic loads use only load-legal orderings, atomic stores only store-legal orderings, `atomicrmw` and the success ordering of `cmpxchg` any read-modify-write ordering, the failure ordering of `cmpxchg` a load-legal ordering, and fences only orderings stronger than `monotonic`; `unordered` and a bare `monotonic` fence never appear.\n14. A `cmpxchg` always supplies both a comparison value `%expected` and a new value `%desired`, and always states two orderings (success then failure) in that order.\n15. Every synchronization scope, when present, is one of the two scopes with a compiler-target owner \u2014 `syncscope(\"singlethread\")` or `syncscope(\"system\")` \u2014 or is absent (the implicit default); target-specific scope names are excluded from the input domain.\n16. All result names are unique within the graph: load results are `%val<k>`, `atomicrmw` results `%rmw<k>`, and `cmpxchg` results `%pair<k>`, where `<k>` is the leaf's position index in the body.\n17. The memory leaves either sit directly in the graph body or are all nested inside exactly one structured control-flow region; the leaves are never split across a region boundary and regions are never nested inside one another.\n18. When a structured region is used it is either an `scf.if %cond { ... }` guarded by the `i1` block argument, with no `else` branch and no results, or an `scf.for` loop with no iteration arguments and no results.\n19. When the `scf.for` form is used, its three bounds are `index`-typed `arith.constant` operations defined immediately before the loop, and the loop induction variable `%iv` is never used by any leaf inside the body.\n20. Both region forms are terminator-implicit (no explicit `scf.yield` is written), and the region is always closed before the graph's `dataflow.graph.return`.\n21. The graph body always contains at least one memory leaf.\n\n## Sampling conventions\n\n1. The number of memory leaves is sampled uniformly from 1 to 6 inclusive; no empty body and no body larger than six leaves is emitted.\n2. The body shape is chosen from exactly three options \u2014 flat sequential composition, one `scf.if`, one `scf.for` \u2014 with the flat form listed twice so it is weighted more heavily, and no other structured construct (e.g. `scf.while`, nested regions, `else` branch) is ever produced.\n3. All leaves are emitted by one right-recursive list rule counted by a state variable `I` against the sampled `COUNT`, so leaf positions are consecutive integers starting at 0.\n4. The result-name suffix `<k>` is exactly the current loop counter `I` rendered with `str`, so names run `%val0`, `%rmw1`, `%pair2`, \u2026 following the leaf's position rather than a separate counter per operation kind.\n5. Each leaf is independently chosen from a fixed nine-way menu: plain load, volatile load, atomic load, plain store, volatile store, atomic store, `atomicrmw`, `cmpxchg`, fence.\n6. The `cmpxchg` alternative is guarded so it is only admissible in the flat (non-region) shape; inside `scf.if` or `scf.for` bodies the grammar samples only the other eight leaf kinds.\n7. Alignment values are drawn from the two-element set `{4, 8}` only, always printed as `alignment = N : i64`.\n8. Synchronization scope is sampled from three alternatives \u2014 empty string, `syncscope(\"singlethread\")`, `syncscope(\"system\")` \u2014 and is offered on atomic loads, atomic stores, `atomicrmw`, `cmpxchg` and `fence`, but never on plain or volatile accesses.\n9. Atomic-load ordering is sampled from `monotonic`, `acquire`, `seq_cst`; atomic-store ordering from `monotonic`, `release`, `seq_cst`; read-modify-write ordering from `monotonic`, `acquire`, `release`, `acq_rel`, `seq_cst`; fence ordering from `acquire`, `release`, `acq_rel`, `seq_cst`.\n10. For `cmpxchg`, the grammar reuses the read-modify-write ordering set for the success ordering and the load ordering set for the failure ordering, and it does not restrict the failure ordering relative to the success ordering.\n11. A `volatile` marker is sampled independently for `cmpxchg` only (empty or `volatile `); loads and stores instead get volatility by selecting the dedicated volatile alternatives, and `atomicrmw` and `fence` are never marked volatile.\n12. The `atomicrmw` operation kind is drawn from a ten-element list emitted literally as `xchg`, `add`, `sub`, `_and`, `_or`, `_xor`, `max`, `min`, `umax`, `umin` \u2014 the bitwise kinds carrying a leading underscore in the emitted text \u2014 and floating-point, `nand`, and pointer-oriented kinds are excluded.\n13. Values `%expected`, `%index`, `%cond` are emitted in the signature in every program regardless of whether any sampled leaf uses them, so unused block arguments are common.\n14. The module preamble, graph signature, attribute dictionaries and the `getelementptr` line are fixed constant text, with the GEP element type pinned to `!llvm.array<4 x i8>` and the loop trip count pinned to `0` to `4` step `1`.\n15. All body lines are emitted with a fixed four-space indentation, including operations nested inside the `scf.if`/`scf.for` regions, which therefore are not indented further than their enclosing region header.\n16. Names are fixed literals (`@source_memory_graph`, `%start`, `%base`, `%expected`, `%desired`, `%index`, `%cond`, `%ptr`, `%lower`, `%upper`, `%step`, `%iv`), so no name is randomly generated and no uniqueness postcondition is needed.\n17. Only one graph and only one module are ever emitted; the grammar never produces multiple graphs, a second GEP, or calls between graphs.",
"result_index": 0,
"session_id": "a6873e83-fcd2-4f67-8d0f-ad99e4e4e2a8",
"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": 45,
"total_cost_usd": 0.129375,
"ttft_ms": 3884,
"ttft_stream_ms": 1148,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 4984,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 4984,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3181,
"output_tokens_details": {
"thinking_tokens": 176
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "11edbcdd-3f46-48f3-b3e6-fd8e1c516ef8"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 14105,
"duration_ms": 14132,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1770,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5683,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.07979,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 918,
"provider": "firstParty",
"thinkingTokens": 329,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition looks only at the subject's output program; the `input` root is never referenced, so no output-to-input correspondence is checked. It first selects, from every operation of the output at any nesting depth, those whose name is exactly `dataflow.graph`, and then universally quantifies over that selected sequence. For each such graph it makes two assertions, each a `none` quantification over all of the output's operations filtered by transitive structural containment in that graph. The first rejects any contained operation whose name is one of the five literal strings `llvm.intr.memcpy`, `llvm.intr.memcpy.inline`, `llvm.intr.memmove`, `llvm.intr.memset`, or `llvm.intr.memset.inline`; the second rejects any contained operation whose name is one of `llvm.load`, `llvm.store`, `llvm.atomicrmw`, `llvm.cmpxchg`, or `llvm.fence`. Matching is by exact operation name only \u2014 no attributes, operands, types, dialect prefixes, or regions are inspected \u2014 so any other spelling, including other `llvm.*` operations or memory operations from other dialects, is accepted, while volatile or atomic variants that share those exact names are rejected because they are indistinguishable here. The only permitted value source is the literal name strings written in the two definitions; nothing is drawn from the program's values, attributes, or symbol table. Occurrences of these ten names that lie outside every `dataflow.graph` region are accepted, since containment in some graph is required for a violation. The postcondition is vacuously satisfied when the output contains no `dataflow.graph` operation, and likewise per graph when a graph's body is empty or contains none of the named operations; it is non-vacuous only when at least one `dataflow.graph` exists and contains operations to scan.",
"result_index": 0,
"session_id": "4d94b77e-74a7-490a-9323-a6a79e7e52f0",
"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.07979,
"ttft_ms": 6243,
"ttft_stream_ms": 1330,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5683,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5683,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 918,
"output_tokens_details": {
"thinking_tokens": 329
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "9d348cbd-b27a-4948-80a0-a97427d533ef"
}
]
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.