MS1V5 mlir-stage-14-v1 passing 5000/5000
Estimated confidence: 94.9%. Conservative lower bound: 72.9% (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 |
The whole callable is the preferred exact CFG-to-SCF projection. When a local obstacle makes that projection inadmissible, raising may instead recover a maximal dominance- and post-dominance-closed region with one external entry and one continuation. The boundary carries continuation arguments and every SSA value used outside the region; the rewrite is attempted on a detached callable clone and is published only after the upstream transformation succeeds. Any transient structured region used to establish that boundary is
"builtin.module"() ({ "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i1, i32, i32)>, linkage = #llvm.linkage<external>, sym_name = "plain_diamond_1", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg0: i1, %arg1: i32, %arg2: i32): "cf.cond_br"(%arg0)[^bb1, ^bb2] <{operandSegmentSizes = array<i32: 1, 0, 0>}> : (i1) -> () ^bb1: // pred: ^bb0 "cf.br"(%arg1)[^bb3] : (i32) -> () ^bb2: // pred: ^bb0 "cf.br"(%arg2)[^bb3] : (i32) -> () ^bb3(%0: i32): // 2 preds: ^bb1, ^bb2 "llvm.return"(%0) : (i32) -> () }) : () -> () }) : () -> ()
"builtin.module"() ({ "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i1, i32, i32)>, linkage = #llvm.linkage<external>, sym_name = "plain_diamond_1", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg0: i1, %arg1: i32, %arg2: i32): %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "scf.if"(%arg0) ({ "scf.yield"(%arg1) : (i32) -> () }, { "scf.yield"(%arg2) : (i32) -> () }) : (i1) -> i32 "llvm.return"(%1) : (i32) -> () }) : () -> () }) : () -> ()
#loop_ann = #llvm.loop_annotation<mustProgress = true> llvm.func @weighted_then_plain_0(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 { cf.cond_br %weighted weights([5, 5]), ^weighted_true, ^weighted_false ^weighted_true: cf.br ^plain_entry(%a : i32) ^weighted_false: cf.br ^plain_entry(%b : i32) ^plain_entry(%seed: i32): cf.cond_br %plain, ^plain_true, ^plain_false ^plain_true: cf.br ^exit(%seed : i32) ^plain_false: cf.br ^exit(%seed : i32) ^exit(%r: i32): llvm.return %r : i32 } llvm.func @counted_cycle_1(%limit: i32) -> i32 { %zero = arith.constant 0 : i32 %step = arith.constant 2 : i32 cf.br ^header(%zero : i32) ^header(%iv: i32): %done = arith.cmpi eq, %iv, %limit : i32 cf.cond_br %done, ^exit, ^latch ^latch: %next = arith.addi %iv, %step : i32 cf.br ^header(%next : i32) ^exit: llvm.return %iv : i32 } llvm.func @nested_weighted_arm_2(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 { cf.cond_br %weighted weights([5, 5]), ^left, ^right ^left: cf.cond_br %plain, ^left_true, ^left_false ^left_true: cf.br ^exit(%a : i32) ^left_false: cf.br ^exit(%b : i32) ^right: cf.br ^exit(%b : i32) ^exit(%r: i32): llvm.return %r : i32 }
The final linked LLVM module enters S0 without replacing its LLVM callable envelopes. The LLVM dialect operation remains the sole owner of linkage, calling convention, COMDAT, personality, argument and result attributes, memory effects, target features, floating-point environment, and every other LLVM ABI fact.
The whole callable is the preferred exact CFG-to-SCF projection. When a local obstacle makes that projection inadmissible, raising may instead recover a maximal dominance- and post-dominance-closed region with one external entry and one continuation.
Mechanical CFG recovery operates on callable regions rather than requiring
conversion to func.func. For an imported LLVM function, Loom converts LLVM
branch structure to exact cf structure where required, invokes the upstream
region-level CFG-to-SCF transformation, and uses an LLVM-compatible adapter
for return and unreachable behavior.
LLVM loop metadata has a loop owner only when its carrier terminator closes a backedge to one exact dominating loop header. Mechanical structuring moves that hint to the recovered loop.
Profile-bearing control, an unsupported
terminator, or an unproved loop-hint association prevents only a region whose
boundary contains that obstacle. A candidate with no common continuation or
no exact live-out boundary remains in cf form without preventing independent
regions in the same callable from being recovered.
A carrier that can close backedges to multiple headers remains unstructured because its owner is ambiguous.
candidate.pg// Input domain for loom-raise-opt --loom-lift-cf-to-scf. // // A linked LLVM module enters the raising pipeline with its LLVM callable // envelopes intact, so every callable is an llvm.func that owns its own body. // Mechanical CFG recovery runs on that callable region in `cf` form, so the // bodies below spell exact `cf` branch structure inside llvm.func. // // Sampled callable shapes: // * wholly admissible callables (diamond, sequential diamonds, counted // cycle with a latch-owned loop annotation); // * callables holding one profile-bearing (weighted) branch, which is a // local obstacle to the whole-callable projection but leaves independent // regions before/after/inside it recoverable. start: {new COUNT = random.randint(2, 4); new I = 0} preamble funcs; preamble: '#loop_ann = #llvm.loop_annotation<mustProgress = true>\n\n'; funcs: (I < COUNT) func {I += 1} funcs | (I == COUNT) ''; func: plain_diamond | sequential_diamonds | counted_cycle | weighted_then_plain | plain_then_weighted | nested_weighted_arm | weighted_then_cycle; // ---------------------------------------------------------------- no obstacle plain_diamond: {new NAME = 'plain_diamond_' + str(I)} 'llvm.func @' [NAME] '(%c: i1, %a: i32, %b: i32) -> i32 {\n' ' cf.cond_br %c, ^yes, ^no\n' '^yes:\n' ' cf.br ^exit(%a : i32)\n' '^no:\n' ' cf.br ^exit(%b : i32)\n' '^exit(%r: i32):\n' ' llvm.return %r : i32\n' '}\n\n'; sequential_diamonds: {new NAME = 'sequential_diamonds_' + str(I); new K = random.randint(1, 6)} 'llvm.func @' [NAME] '(%first: i1, %second: i1, %a: i32, %b: i32) -> i32 {\n' ' %k = arith.constant ' [str(K)] ' : i32\n' ' cf.cond_br %first, ^one_yes, ^one_no\n' '^one_yes:\n' ' cf.br ^middle(%a : i32)\n' '^one_no:\n' ' cf.br ^middle(%b : i32)\n' '^middle(%seed: i32):\n' ' cf.cond_br %second, ^two_yes, ^two_no\n' '^two_yes:\n' ' %sum = arith.addi %seed, %k : i32\n' ' cf.br ^exit(%sum : i32)\n' '^two_no:\n' ' cf.br ^exit(%seed : i32)\n' '^exit(%r: i32):\n' ' llvm.return %r : i32\n' '}\n\n'; counted_cycle: {new NAME = 'counted_cycle_' + str(I); new STEP = random.randint(1, 4)} 'llvm.func @' [NAME] '(%limit: i32) -> i32 {\n' ' %zero = arith.constant 0 : i32\n' ' %step = arith.constant ' [str(STEP)] ' : i32\n' ' cf.br ^header(%zero : i32)\n' '^header(%iv: i32):\n' ' %done = arith.cmpi eq, %iv, %limit : i32\n' ' cf.cond_br %done, ^exit, ^latch\n' '^latch:\n' ' %next = arith.addi %iv, %step : i32\n' ' cf.br ^header(%next : i32)' loop_hint '\n' '^exit:\n' ' llvm.return %iv : i32\n' '}\n\n'; // A hint on a latch that closes a backedge to one dominating header has an // exact loop owner; the alternative omits the hint entirely. loop_hint: ' {llvm.loop_annotation = #loop_ann}' | ''; // ------------------------------------------------- one profile-bearing branch weighted_then_plain: {new NAME = 'weighted_then_plain_' + str(I); new WA = random.randint(1, 9)} 'llvm.func @' [NAME] '(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 {\n' ' cf.cond_br %weighted weights([' [str(WA)] ', ' [str(10 - WA)] ']), ^weighted_true, ^weighted_false\n' '^weighted_true:\n' ' cf.br ^plain_entry(%a : i32)\n' '^weighted_false:\n' ' cf.br ^plain_entry(%b : i32)\n' '^plain_entry(%seed: i32):\n' ' cf.cond_br %plain, ^plain_true, ^plain_false\n' '^plain_true:\n' ' cf.br ^exit(%seed : i32)\n' '^plain_false:\n' ' cf.br ^exit(%seed : i32)\n' '^exit(%r: i32):\n' ' llvm.return %r : i32\n' '}\n\n'; plain_then_weighted: {new NAME = 'plain_then_weighted_' + str(I); new WB = random.randint(1, 9)} 'llvm.func @' [NAME] '(%plain: i1, %weighted: i1, %a: i32, %b: i32) -> i32 {\n' ' cf.cond_br %plain, ^plain_true, ^plain_false\n' '^plain_true:\n' ' cf.br ^weighted_entry(%a : i32)\n' '^plain_false:\n' ' cf.br ^weighted_entry(%b : i32)\n' '^weighted_entry(%seed: i32):\n' ' cf.cond_br %weighted weights([' [str(WB)] ', ' [str(10 - WB)] ']), ^weighted_true, ^weighted_false\n' '^weighted_true:\n' ' cf.br ^exit(%seed : i32)\n' '^weighted_false:\n' ' cf.br ^exit(%seed : i32)\n' '^exit(%r: i32):\n' ' llvm.return %r : i32\n' '}\n\n'; nested_weighted_arm: {new NAME = 'nested_weighted_arm_' + str(I); new WC = random.randint(1, 9)} 'llvm.func @' [NAME] '(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 {\n' ' cf.cond_br %weighted weights([' [str(WC)] ', ' [str(10 - WC)] ']), ^left, ^right\n' '^left:\n' ' cf.cond_br %plain, ^left_true, ^left_false\n' '^left_true:\n' ' cf.br ^exit(%a : i32)\n' '^left_false:\n' ' cf.br ^exit(%b : i32)\n' '^right:\n' ' cf.br ^exit(%b : i32)\n' '^exit(%r: i32):\n' ' llvm.return %r : i32\n' '}\n\n'; weighted_then_cycle: {new NAME = 'weighted_then_cycle_' + str(I); new WD = random.randint(1, 9)} 'llvm.func @' [NAME] '(%weighted: i1, %limit: i32) -> i32 {\n' ' %zero = arith.constant 0 : i32\n' ' %one = arith.constant 1 : i32\n' ' cf.cond_br %weighted weights([' [str(WD)] ', ' [str(10 - WD)] ']), ^left, ^right\n' '^left:\n' ' cf.br ^header(%zero : i32)\n' '^right:\n' ' cf.br ^header(%one : i32)\n' '^header(%iv: i32):\n' ' %done = arith.cmpi eq, %iv, %limit : i32\n' ' cf.cond_br %done, ^exit, ^latch\n' '^latch:\n' ' %next = arith.addi %iv, %one : i32\n' ' cf.br ^header(%next : i32)' loop_hint '\n' '^exit:\n' ' llvm.return %iv : i32\n' '}\n\n';
The whole callable is the preferred exact CFG-to-SCF projection. When a local obstacle makes that projection inadmissible, raising may instead recover a maximal dominance- and post-dominance-closed region with one external entry and one continuation.
candidate.spctpostcondition whole_callable_or_local_region_projection { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-2-scf.md:L63-L69"; } // A local obstacle to the whole-callable projection, as named by the // governing context: profile-bearing control or an unsupported terminator. definition local_obstacles(callable: mlir::Operation): Seq<mlir::Operation> = seq { d | d in mlir::descendants(callable) where "branch_weights" in d.attributes or d.name == "llvm.indirectbr" or d.name == "llvm.blocktag" or d.name == "cf.switch" }; definition cf_control(callable: mlir::Operation): Seq<mlir::Operation> = seq { d | d in mlir::descendants(callable) where d.dialect == "cf" }; definition callable_names(p: mlir::Program): Set<String> = set { c.attributes["sym_name"].string | c in p.operations where c.name == "llvm.func" and "sym_name" in c.attributes }; constraints { let callables = seq { c | c in output.operations where c.name == "llvm.func" }; let recovered = seq { s | s in output.operations where s.dialect == "scf" }; // The whole callable is the preferred exact CFG-to-SCF projection: a // callable holding no local obstacle is projected in whole, so no `cf` // control survives in it. forall c in callables where cardinality(local_obstacles(c)) == 0 { assert whole_callable_projection_preferred: cardinality(cf_control(c)) == 0; } // Each recovered region's boundary carries every SSA value that is used // outside the region: no value defined inside a recovered structured // operation escapes it other than through that operation's boundary. forall s in recovered { assert boundary_carries_values_used_outside: forall d in mlir::descendants(s) where forall r in d.results where forall u in r.uses where mlir::contains(s, u.owner); } // The rewrite is attempted on a detached callable clone and published // into the original callable only after the transformation succeeds, so // publication never adds or drops a callable envelope. assert callables_published_in_place: callable_names(output) == callable_names(input); } }
"builtin.module"() ({ "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i1, i32, i32)>, linkage = #llvm.linkage<external>, sym_name = "plain_diamond_1", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg0: i1, %arg1: i32, %arg2: i32): "cf.cond_br"(%arg0)[^bb1, ^bb2] <{operandSegmentSizes = array<i32: 1, 0, 0>}> : (i1) -> () ^bb1: // pred: ^bb0 "cf.br"(%arg1)[^bb3] : (i32) -> () ^bb2: // pred: ^bb0 "cf.br"(%arg2)[^bb3] : (i32) -> () ^bb3(%0: i32): // 2 preds: ^bb1, ^bb2 "llvm.return"(%0) : (i32) -> () }) : () -> () }) : () -> ()
20260911-084157started2026-09-11T08:41:58Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
#loop_ann = #llvm.loop_annotation<mustProgress = true> llvm.func @weighted_then_plain_0(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 { cf.cond_br %weighted weights([5, 5]), ^weighted_true, ^weighted_false ^weighted_true: cf.br ^plain_entry(%a : i32) ^weighted_false: cf.br ^plain_entry(%b : i32) ^plain_entry(%seed: i32): cf.cond_br %plain, ^plain_true, ^plain_false ^plain_true: cf.br ^exit(%seed : i32) ^plain_false: cf.br ^exit(%seed : i32) ^exit(%r: i32): llvm.return %r : i32 } llvm.func @counted_cycle_1(%limit: i32) -> i32 { %zero = arith.constant 0 : i32 %step = arith.constant 2 : i32 cf.br ^header(%zero : i32) ^header(%iv: i32): %done = arith.cmpi eq, %iv, %limit : i32 cf.cond_br %done, ^exit, ^latch ^latch: %next = arith.addi %iv, %step : i32 cf.br ^header(%next : i32) ^exit: llvm.return %iv : i32 } llvm.func @nested_weighted_arm_2(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 { cf.cond_br %weighted weights([5, 5]), ^left, ^right ^left: cf.cond_br %plain, ^left_true, ^left_false ^left_true: cf.br ^exit(%a : i32) ^left_false: cf.br ^exit(%b : i32) ^right: cf.br ^exit(%b : i32) ^exit(%r: i32): llvm.return %r : i32 }
"builtin.module"() ({ "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i1, i1, i32, i32)>, linkage = #llvm.linkage<external>, sym_name = "weighted_then_plain_0", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg9: i1, %arg10: i1, %arg11: i32, %arg12: i32): "cf.cond_br"(%arg9)[^bb1, ^bb2] <{branch_weights = array<i32: 5, 5>, operandSegmentSizes = array<i32: 1, 0, 0>}> : (i1) -> () ^bb1: // pred: ^bb0 "cf.br"(%arg11)[^bb3] : (i32) -> () ^bb2: // pred: ^bb0 "cf.br"(%arg12)[^bb3] : (i32) -> () ^bb3(%13: i32): // 2 preds: ^bb1, ^bb2 %14 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %15 = "scf.if"(%arg10) ({ "scf.yield"(%13) : (i32) -> () }, { "scf.yield"(%13) : (i32) -> () }) : (i1) -> i32 "cf.br"(%15)[^bb4] : (i32) -> () ^bb4(%16: i32): // pred: ^bb3 "llvm.return"(%16) : (i32) -> () }) : () -> () "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i32)>, linkage = #llvm.linkage<external>, sym_name = "counted_cycle_1", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg4: i32): %3 = "llvm.mlir.undef"() : () -> i32 %4 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %5 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %6 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %7 = "arith.constant"() <{value = 2 : i32}> : () -> i32 %8:2 = "scf.while"(%6, %3) ({ ^bb0(%arg7: i32, %arg8: i32): %9 = "arith.cmpi"(%arg7, %arg4) <{predicate = 0 : i64}> : (i32, i32) -> i1 %10:3 = "scf.if"(%9) ({ "scf.yield"(%3, %4, %5) : (i32, i32, i32) -> () }, { %12 = "arith.addi"(%arg7, %7) <{overflowFlags = #arith.overflow<none>}> : (i32, i32) -> i32 "scf.yield"(%12, %5, %4) : (i32, i32, i32) -> () }) : (i1) -> (i32, i32, i32) %11 = "arith.trunci"(%10#2) <{overflowFlags = #arith.overflow<none>}> : (i32) -> i1 "scf.condition"(%11, %10#0, %arg7) : (i1, i32, i32) -> () }, { ^bb0(%arg5: i32, %arg6: i32): "scf.yield"(%arg5, %arg6) : (i32, i32) -> () }) : (i32, i32) -> (i32, i32) "llvm.return"(%8#1) : (i32) -> () }) : () -> () "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i32 (i1, i1, i32, i32)>, linkage = #llvm.linkage<external>, sym_name = "nested_weighted_arm_2", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({ ^bb0(%arg0: i1, %arg1: i1, %arg2: i32, %arg3: i32): "cf.cond_br"(%arg0)[^bb1, ^bb2] <{branch_weights = array<i32: 5, 5>, operandSegmentSizes = array<i32: 1, 0, 0>}> : (i1) -> () ^bb1: // pred: ^bb0 %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32 %1 = "scf.if"(%arg1) ({ "scf.yield"(%arg2) : (i32) -> () }, { "scf.yield"(%arg3) : (i32) -> () }) : (i1) -> i32 "cf.br"(%1)[^bb3] : (i32) -> () ^bb2: // pred: ^bb0 "cf.br"(%arg3)[^bb3] : (i32) -> () ^bb3(%2: i32): // 2 preds: ^bb1, ^bb2 "llvm.return"(%2) : (i32) -> () }) : () -> () }) : () -> ()
partial source coverage: Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.
authoring-context.json{"entries":[{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"63-74","path":"docs/spec-compiler-part-2-scf.md","roles":["applicability","context"],"text":"The whole callable is the preferred exact CFG-to-SCF projection. When a local\nobstacle makes that projection inadmissible, raising may instead recover a\nmaximal dominance- and post-dominance-closed region with one external entry\nand one continuation. The boundary carries continuation arguments and every\nSSA value used outside the region; the rewrite is attempted on a detached\ncallable clone and is published only after the upstream transformation\nsucceeds. Any transient structured region used to establish that boundary is\ninlined before publication. Profile-bearing control, an unsupported\nterminator, or an unproved loop-hint association prevents only a region whose\nboundary contains that obstacle. A candidate with no common continuation or\nno exact live-out boundary remains in `cf` form without preventing independent\nregions in the same callable from being recovered.","why":"Sampled output obligation plus its governing context: whole-callable projection is preferred, a local obstacle (profile-bearing control, unsupported terminator, unproved loop-hint association) only prevents the region whose boundary contains it. Used to select which output callables the whole-callable assert applies to."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"48-58","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction","input_well_formedness"],"text":"The final linked LLVM module enters S0 without replacing its LLVM callable\nenvelopes. The LLVM dialect operation remains the sole owner of linkage,\ncalling convention, COMDAT, personality, argument and result attributes,\nmemory effects, target features, floating-point environment, and every other\nLLVM ABI fact.\n\nMechanical CFG recovery operates on callable regions rather than requiring\nconversion to `func.func`. For an imported LLVM function, Loom converts LLVM\nbranch structure to exact `cf` structure where required, invokes the upstream\nregion-level CFG-to-SCF transformation, and uses an LLVM-compatible adapter\nfor return and unreachable behavior. Pass wrappers that participate in this","why":"Normative input shape: the linked module keeps its LLVM callable envelopes, and mechanical recovery runs on the callable region in exact `cf` form. The grammar therefore emits llvm.func callables whose bodies spell cf.br/cf.cond_br directly."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"124-130","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction","input_well_formedness"],"text":"LLVM loop metadata has a loop owner only when its carrier terminator closes a\nbackedge to one exact dominating loop header. Mechanical structuring moves that\nhint to the recovered loop. Metadata on a terminator with no such backedge is\nan orphan under the LLVM loop contract: successful structuring removes the\norphan carrier, preserves the corresponding analysis fact as unknown, and does\nnot guess a loop owner. A carrier that can close backedges to multiple headers\nremains unstructured because its owner is ambiguous.","why":"Loop metadata has an owner only when its carrier closes a backedge to one exact dominating header, and an ambiguous carrier stays unstructured. The generator only attaches llvm.loop_annotation to a latch with a single dominating header, so sampled inputs carry no unproved hint association."},{"file_sha256":"cb2eccd216a4270d4b483cc2d2e246393bc3ba47dae1a0c7680d6ee9839015b9","kind":"implementation","lines":"39-64","path":"lib/Frontend/Raising/LiftCFToSCFPass.cpp","roles":["applicability","input_construction"],"text":"// A completely admissible callable is structured as one region. If an exact\n// local obstacle prevents that, maximal single-entry, single-continuation CFG\n// regions around the obstacle are considered independently. Each local region\n// is moved into a temporary scf.execute_region in a detached callable clone,\n// transformed with the same upstream utility, and immediately inlined. The\n// temporary operation is only an implementation boundary: it is never\n// published. An unprovable local region stays as `cf`, while independent local\n// regions in the same callable can still be recovered.\n//\n// A local region is excluded when:\n//\n// * a reachable branch carries weights -- `scf.if` and `scf.index_switch`\n// state no branch probability, so lifting would drop imported profile data;\n// * a reachable terminator with successors is not exactly cf.br, cf.cond_br,\n// or cf.switch -- the transformation erases a one-successor terminator it\n// does not recognize and splices its successor away, which would silently\n// restate a one-target llvm.indirectbr as an unconditional branch;\n// * a `cf.switch` selector or case value does not fit the structured\n// switch's index and 64-bit case carriers;\n// * a block owns llvm.blocktag, whose parent block identity may be observed\n// by a module-level llvm.blockaddress independently of SSA uses;\n// * an imported callable holds a value whose type LLVM cannot spell, since\n// the adapter would otherwise have to state an undefined value of that type\n// as the stronger `ub.poison`; or\n// * a loop annotation's owning loop is not exactly identifiable.\n//","why":"Enumerates exactly which local conditions exclude a region (weighted branch, unrecognized terminator such as llvm.indirectbr, wide cf.switch carrier, llvm.blocktag, LLVM-unspellable value type, unidentifiable loop owner). This fixes the obstacle guard used to select obstacle-free callables and the constructs the generator deliberately does or does not sample."},{"file_sha256":"cb2eccd216a4270d4b483cc2d2e246393bc3ba47dae1a0c7680d6ee9839015b9","kind":"implementation","lines":"65-87","path":"lib/Frontend/Raising/LiftCFToSCFPass.cpp","roles":["context"],"text":"// Every structuring traversal works on a detached clone of the callable op.\n// Unreachable components with no externally visible block identity are erased\n// from that clone, which is the one cleanup upstream's documented structural\n// preconditions require. An unreachable component containing llvm.blocktag is\n// instead retained because a module-level llvm.blockaddress can observe that\n// identity without an SSA or CFG use. The whole-callable path declines such a\n// clone. A local region may still structure when the retained component does\n// not enter its extraction boundary. Each clone is taken from the then-current\n// original and published back into its original callable op only after the\n// complete attempted rewrite succeeds. The walk is\n// post-order, so a nested callable is structured and published before its\n// enclosing callable: the ancestor is therefore cloned from an original that\n// already holds the structured descendant, and its clone carries that structure\n// through. A deferred publication would instead clone the ancestor from a\n// snapshot taken before the descendant published, so publishing that stale\n// ancestor clone would overwrite the descendant's structured body with the\n// unstructured copy the clone still held. Upstream's documented \"unspecified IR\n// on interface failure\" unwinds inside the clone, and an annotation the\n// completed clone could not place leaves that region preserved, so a clone that\n// declines is dropped without publishing. Publishing cannot fail: it preserves\n// the region's owning callable op and carries already-structured descendant\n// bodies through ancestor clones, leaving each imported callable in llvm.func\n// form as the sole ABI envelope of its body.","why":"Confirms the detached-clone/publish discipline of the obligation: each clone is published back into its original callable op only after the complete rewrite succeeds, and publishing preserves the owning callable op. Supports the callable-set publication assert."},{"file_sha256":"cb2eccd216a4270d4b483cc2d2e246393bc3ba47dae1a0c7680d6ee9839015b9","kind":"implementation","lines":"953-964","path":"lib/Frontend/Raising/LiftCFToSCFPass.cpp","roles":["context"],"text":"struct LiftCFToSCFPass\n : public ::mlir::PassWrapper<LiftCFToSCFPass, ::mlir::OperationPass<>> {\n MLIR_DEFINE_EXPLICIT_INTERNAL_INLINE_TYPE_ID(LiftCFToSCFPass)\n\n ::llvm::StringRef getArgument() const final { return \"loom-lift-cf-to-scf\"; }\n ::llvm::StringRef getDescription() const final {\n return \"Structure each maximal exactly provable cf-shaped region with \"\n \"the upstream CFG-to-SCF transformation, leaving an imported \"\n \"llvm.func as the callable and ABI owner of its body, retaining \"\n \"weighted or unsupported local control, and moving each imported \"\n \"loop annotation to the loop that owns its cycle.\";\n }","why":"Pass registration establishing that --loom-lift-cf-to-scf is the stage named by the claim; its description confirms the pass operates in place on callables and retains weighted or unsupported local control."},{"file_sha256":"292696bf5fab87a93df111d14e2e80fc8c172ce2b13fed973df96fbb4878bde5","kind":"implementation","lines":"174-187","path":"include/Frontend/Raising/Passes.h","roles":["context"],"text":"// Register all raising passes with the global pass registry. Lets\n// `mlir-opt` style drivers expose them via --loom-llvm-cf-to-cf,\n// --loom-lift-cf-to-scf, --loom-llvm-arith-to-arith.\nvoid registerRaisingPasses();\n\n// Append the standard Loom raising pipeline to the given pass manager:\n// loom-llvm-cf-to-cf\n// loom-lift-cf-to-scf\n// loom-llvm-arith-to-arith\n// loom-normalize-lifted-scf-exit\n// loom-deduplicate-scf-while-state\n// loom-scf-while-to-for\n// Selected SCF optimization decisions are outside this pipeline.\nvoid buildRaisingPipeline(::mlir::PassManager &pm);","why":"Documents the driver flag spelling and the ordered raising pipeline, evidencing that loom-lift-cf-to-scf can be invoked alone when the input is already in cf form (loom-llvm-cf-to-cf precedes it only to convert LLVM branch terminators)."},{"file_sha256":"5abba37ed266cb6a9b2a18dc28ff3e0f763b9c3d95d7fd13713d8cbe2c1515a1","kind":"test","lines":"1-12","path":"test/raise/cfg-structurization.mlir","roles":["context"],"text":"// RUN: split-file %s %t\n// RUN: %loom-raise %t/counted.ll | FileCheck %s --check-prefix=LOOP\n// RUN: %loom-raise %t/spin.ll | FileCheck %s --check-prefix=SPIN\n// RUN: %loom-raise %t/irreducible.ll | FileCheck %s --check-prefix=UNDEF --implicit-check-not=ub.poison\n// RUN: loom-raise-opt --loom-llvm-cf-to-cf --loom-lift-cf-to-scf %t/switch-carrier.mlir | FileCheck %s --check-prefix=SWITCH\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/preserved.mlir | FileCheck %s --check-prefix=PRESERVE\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/nested.mlir | FileCheck %s --check-prefix=NESTED --implicit-check-not=cf.cond_br\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/orphan-loop-hint.mlir | FileCheck %s --check-prefix=ORPHAN --implicit-check-not=cf.cond_br\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/numbered-default.mlir -o %t/numbered-default.out.mlir\n// RUN: loom-raise-opt %t/numbered-default.out.mlir | FileCheck %s --check-prefix=NUMBERED-DEFAULT\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/local-regions.mlir -o %t/local-regions.out.mlir\n// RUN: loom-raise-opt --loom-lift-cf-to-scf %t/local-regions.out.mlir | FileCheck %s --check-prefix=LOCAL --implicit-check-not=scf.execute_region","why":"RUN lines showing the accepted invocations; cf-form inputs are run with --loom-lift-cf-to-scf alone, which is the invocation recorded in subject-command.json."},{"file_sha256":"5abba37ed266cb6a9b2a18dc28ff3e0f763b9c3d95d7fd13713d8cbe2c1515a1","kind":"test","lines":"349-470","path":"test/raise/cfg-structurization.mlir","roles":["input_construction","input_well_formedness"],"text":"//--- local-regions.mlir\n#local_loop = #llvm.loop_annotation<mustProgress = true>\n\nmodule attributes {\n dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 32>>\n} {\nllvm.func @weighted_then_plain(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 {\n cf.cond_br %weighted weights([1, 9]), ^weighted_true, ^weighted_false\n^weighted_true:\n cf.br ^plain_entry(%a : i32)\n^weighted_false:\n cf.br ^plain_entry(%b : i32)\n^plain_entry(%seed: i32):\n cf.cond_br %plain, ^plain_true, ^plain_false\n^plain_true:\n cf.br ^exit(%seed : i32)\n^plain_false:\n cf.br ^exit(%seed : i32)\n^exit(%result: i32):\n llvm.return %result : i32\n}\n\nllvm.func @plain_then_weighted(%plain: i1, %weighted: i1, %a: i32, %b: i32) -> i32 {\n cf.cond_br %plain, ^plain_true, ^plain_false\n^plain_true:\n cf.br ^weighted_entry(%a : i32)\n^plain_false:\n cf.br ^weighted_entry(%b : i32)\n^weighted_entry(%seed: i32):\n cf.cond_br %weighted weights([2, 8]), ^weighted_true, ^weighted_false\n^weighted_true:\n cf.br ^exit(%seed : i32)\n^weighted_false:\n cf.br ^exit(%seed : i32)\n^exit(%result: i32):\n llvm.return %result : i32\n}\n\nllvm.func @nested_weighted_arm(%weighted: i1, %plain: i1, %a: i32, %b: i32) -> i32 {\n cf.cond_br %weighted weights([3, 7]), ^left, ^right\n^left:\n cf.cond_br %plain, ^left_true, ^left_false\n^left_true:\n cf.br ^exit(%a : i32)\n^left_false:\n cf.br ^exit(%b : i32)\n^right:\n cf.br ^exit(%b : i32)\n^exit(%result: i32):\n llvm.return %result : i32\n}\n\nllvm.func @unsupported_then_plain(%address: !llvm.ptr, %plain: i1, %a: i32, %b: i32) -> i32 {\n llvm.indirectbr %address : !llvm.ptr, [^target]\n^target:\n cf.cond_br %plain, ^yes, ^no\n^yes:\n cf.br ^exit(%a : i32)\n^no:\n cf.br ^exit(%b : i32)\n^exit(%result: i32):\n llvm.return %result : i32\n}\n\nllvm.func @weighted_then_loop(%weighted: i1, %limit: i32) -> i32 {\n %zero = arith.constant 0 : i32\n %one = arith.constant 1 : i32\n cf.cond_br %weighted weights([4, 6]), ^left, ^right\n^left:\n cf.br ^header(%zero : i32)\n^right:\n cf.br ^header(%one : i32)\n^header(%iv: i32):\n %done = arith.cmpi eq, %iv, %limit : i32\n cf.cond_br %done, ^exit, ^latch\n^latch:\n %next = arith.addi %iv, %one : i32\n cf.br ^header(%next : i32) {llvm.loop_annotation = #local_loop}\n^exit:\n llvm.return %iv : i32\n}\n\nllvm.func @local_wide_switch(%weighted: i1, %selector: i64, %plain: i1, %a: i32, %b: i32) -> i32 {\n cf.cond_br %weighted weights([5, 5]), ^left, ^right\n^left:\n cf.br ^switch_entry\n^right:\n cf.br ^switch_entry\n^switch_entry:\n cf.switch %selector : i64, [\n default: ^default,\n 0: ^case\n ]\n^case:\n cf.br ^plain_entry(%a : i32)\n^default:\n cf.br ^plain_entry(%b : i32)\n^plain_entry(%seed: i32):\n cf.cond_br %plain, ^plain_true, ^plain_false\n^plain_true:\n cf.br ^exit(%seed : i32)\n^plain_false:\n cf.br ^exit(%seed : i32)\n^exit(%result: i32):\n llvm.return %result : i32\n}\n\nllvm.func @direct_liveout(%weighted: i1, %plain: i1) -> i32 {\n cf.cond_br %weighted weights([6, 4]), ^left, ^right\n^left:\n cf.br ^plain_entry\n^right:\n cf.br ^plain_entry\n^plain_entry:\n %seven = arith.constant 7 : i32\n cf.cond_br %plain, ^yes, ^no\n^yes:\n cf.br ^exit\n^no:\n cf.br ^exit\n^exit:\n llvm.return %seven : i32","why":"Accepted concrete spellings of cf-form llvm.func callables with weighted cond_br, sequential and nested diamonds, and a latch-annotated cycle. The grammar's callable shapes follow these spellings (block-argument continuations, weights([a, b]) syntax, llvm.loop_annotation alias on the latch)."},{"file_sha256":"5abba37ed266cb6a9b2a18dc28ff3e0f763b9c3d95d7fd13713d8cbe2c1515a1","kind":"example","lines":"313-333","path":"test/raise/cfg-structurization.mlir","roles":["input_well_formedness"],"text":"//--- orphan-loop-hint.mlir\n#orphan_annotation = #llvm.loop_annotation<mustProgress = true>\n\nllvm.func @orphan_loop_hint(%limit: i32, %skip: i1) -> i32 {\n %zero = arith.constant 0 : i32\n %one = arith.constant 1 : i32\n cf.br ^header(%zero : i32)\n^header(%iv: i32):\n cf.cond_br %skip, ^latch, ^body {\n llvm.loop_annotation = #orphan_annotation\n }\n^body:\n cf.br ^latch\n^latch:\n %next = arith.addi %iv, %one : i32\n %done = arith.cmpi eq, %next, %limit : i32\n cf.cond_br %done, ^exit, ^header(%next : i32)\n^exit:\n llvm.return %next : i32\n}","why":"Accepted orphan/latch loop-hint spelling and the #llvm.loop_annotation<mustProgress = true> alias declaration plus its {llvm.loop_annotation = ...} placement on a cf branch, used verbatim by the generator preamble and latch hint."}],"primary_bundle_sha256":"f73a24e5313c93a2c025d93bf6ea31506b713068175c37610ab99428498b0ff3","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"b843419ef908c9a5f485cfa99c736cc30236445ab1544d6eab51ad892f55f870"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 41973,
"duration_ms": 42010,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 995,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 6056,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.13819499999999998,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3105,
"provider": "firstParty",
"thinkingTokens": 11,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module body consisting of a top-level loop-annotation attribute alias definition followed by one or more top-level function definitions, with no enclosing `module { ... }` wrapper.\n2. The attribute alias `#loop_ann` is defined exactly once, at the top of the file, as `#llvm.loop_annotation<mustProgress = true>`, before any function that may reference it.\n3. Every callable is an `llvm.func` with an explicit, non-empty body region written between braces; no callable is declared without a body, and no other callable-defining operation (for example `func.func`) ever appears.\n4. Every `llvm.func` has a single result type `i32` and returns through `llvm.return %r : i32` (or `llvm.return %iv : i32`), so every terminating block of every function yields exactly one `i32` value.\n5. Every function's parameters are explicitly typed in the signature, drawn only from `i1` (branch conditions) and `i32` (data values), and every SSA value referenced in a body is either such a parameter, a block argument declared on that block, or a value defined earlier in the same block.\n6. All intra-function control flow is expressed in `cf` dialect form: only `cf.br` and `cf.cond_br` terminate blocks; no `scf` operation, no unstructured `llvm.br`/`llvm.cond_br`, and no switch-like terminator ever appears.\n7. Every block other than the entry block is introduced by an explicit `^label:` (or `^label(%arg: i32):`) header, and the entry block is implicit (unlabeled) and holds the function's first operations and terminator.\n8. Every block is terminated by exactly one terminator operation, and every block in every function is reachable from the entry block.\n9. Every branch target named in a `cf.br` or `cf.cond_br` is a block defined within the same function, and no branch crosses function boundaries.\n10. Value flow across control-flow merges is carried exclusively by block arguments passed through branch operand lists (`^exit(%a : i32)`), never by cross-block direct SSA references into dominated blocks; block-argument types in the branch operand list match the declared block-argument types.\n11. Any block declaring an argument is entered only by branches supplying exactly that arity and type of operand; blocks declaring no arguments are entered only by operand-free branches.\n12. Non-control operations appearing inside bodies are restricted to `arith.constant`, `arith.addi`, and `arith.cmpi eq`, all at `i32` operand type, with `arith.cmpi` producing the `i1` consumed by the following `cf.cond_br`; no memory, call, or side-effecting operation ever appears.\n13. Each SSA name is assigned at most once within its function, and every function's names are self-contained (no cross-function value references).\n14. Branch weights, when present, appear only on `cf.cond_br` in the form `weights([w_true, w_false])` placed immediately after the condition operand and before the successor list, with exactly two nonnegative integer entries corresponding to the two successors.\n15. At most one weighted `cf.cond_br` occurs per function; all other conditional branches in that function are weight-free, and functions that contain a loop-carrying backedge either contain exactly one weighted branch outside the loop or none at all.\n16. A `llvm.loop_annotation = #loop_ann` discardable attribute, when present, is attached only to an unconditional `cf.br` that closes a backedge to a single dominating header block, i.e. to the loop latch's branch, and never to a conditional branch, an exiting branch, or a branch outside a cycle.\n17. Every cycle emitted is a single-entry, single-latch, single-exit natural loop: one header block taking an `i32` induction block argument, a conditional exit test in the header, a latch block computing the next induction value and branching back to the header, and an exit block that returns the induction value.\n18. The loop induction value enters the header only as a block argument, is initialized by the branches that enter the header from outside, and is updated only by the latch's `arith.addi` before the backedge.\n19. Loop entry from outside the header occurs on all paths before the header is executed, and no branch jumps into the loop body (latch) from outside the header.\n20. Function names are unique within the module, formed from a shape-identifying prefix and the index of the function in emission order.\n21. Every function body, and the module as a whole, is syntactically complete and self-contained: no unresolved attribute alias, no dangling block label, no unterminated block.\n\n## Sampling conventions\n\n1. The module contains between 2 and 4 functions inclusive, chosen uniformly per program.\n2. Functions are emitted in sequence with a running index starting at 0, and each function's name is suffixed with that index, so names are `<shape>_0`, `<shape>_1`, \u2026 and two functions of different shapes can share an index only if they are at different positions (they cannot; the index is global and increments per function).\n3. Each function independently takes one of exactly seven fixed skeletons: `plain_diamond`, `sequential_diamonds`, `counted_cycle`, `weighted_then_plain`, `plain_then_weighted`, `nested_weighted_arm`, `weighted_then_cycle`; no other shape is ever produced and shapes may repeat within a module.\n4. The name prefix always equals the skeleton's identifier, so the shape of each function is textually recoverable from its symbol name.\n5. The constant preamble is always exactly `#loop_ann = #llvm.loop_annotation<mustProgress = true>` followed by a blank line, and it is emitted whether or not any function actually uses it; no other alias, and no other loop-annotation payload fields, are ever emitted.\n6. Each function is followed by a blank line, giving a uniform two-newline separator between top-level items and a trailing blank line at end of file.\n7. Parameter names are fixed per skeleton (`%c`, `%a`, `%b`, `%first`, `%second`, `%limit`, `%weighted`, `%plain`) rather than generated, and block labels are fixed mnemonic names (`^yes`, `^no`, `^exit`, `^one_yes`, `^middle`, `^header`, `^latch`, `^left`, `^right`, etc.) reused verbatim across functions of the same shape.\n8. `plain_diamond` is a fixed, parameter-only body with no arithmetic: a condition parameter selecting between two `i32` parameters via a two-armed diamond merging at `^exit`.\n9. `sequential_diamonds` emits exactly two diamonds in series sharing a merge-to-merge chain, with an `arith.constant` named `%k` whose literal value is an integer chosen uniformly from 1 through 6, added to the merged value only on the second diamond's true arm.\n10. `counted_cycle` initializes the induction variable from a `%zero` constant that is always literally `0`, and uses a `%step` constant whose value is chosen uniformly from 1 through 4; the exit test is always `arith.cmpi eq` between the induction variable and the `%limit` parameter, with the equal case taking the exit successor.\n11. The loop latch's backedge branch in `counted_cycle` and `weighted_then_cycle` either carries the `{llvm.loop_annotation = #loop_ann}` attribute or carries no attribute at all, chosen independently per loop; no intermediate or alternative annotation form is emitted.\n12. Every weighted branch uses a weight pair summing to exactly 10, of the form `[w, 10 - w]` with `w` chosen uniformly from 1 through 9, so neither weight is ever 0 and the pair is never degenerate or non-normalized.\n13. Exactly one weighted branch is placed per weighted skeleton, and its position varies by skeleton: before a plain diamond (`weighted_then_plain`), after a plain diamond (`plain_then_weighted`), dominating a nested plain diamond on one arm only (`nested_weighted_arm`), or before a counted loop (`weighted_then_cycle`).\n14. In `weighted_then_plain` and `plain_then_weighted` the second diamond's two arms both forward the same merged `%seed` value, so the trailing diamond is data-trivial while remaining structurally a two-armed merge.\n15. In `nested_weighted_arm` the weighted branch's right arm is a bare unconditional branch to the merge while the left arm holds the whole plain diamond, producing an asymmetric nesting rather than two symmetric nested arms.\n16. In `weighted_then_cycle` the loop's step is always the constant `%one` (literally `1`), and the two weighted arms differ only in the loop's initial induction value, `%zero` versus `%one`; no per-program randomization of these constants occurs.\n17. Loops are never nested inside one another, never appear more than once per function, and never follow a loop within the same function; loop-bearing shapes are exactly `counted_cycle` and `weighted_then_cycle`.\n18. No function takes or returns aggregate, pointer, floating-point, or non-32-bit integer types, and no attribute other than the loop annotation is ever attached to any operation or function.\n19. All whitespace is fixed: two-space indentation for operations, column-zero block labels, and a single space before the loop-annotation attribute brace on the latch branch.",
"result_index": 0,
"session_id": "c8a7f3bf-5a5a-4717-9083-ad18c51399ab",
"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": 36,
"total_cost_usd": 0.13819499999999998,
"ttft_ms": 996,
"ttft_stream_ms": 903,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 6056,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 6056,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3105,
"output_tokens_details": {
"thinking_tokens": 11
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "d67c16fc-855b-492c-a933-7dca3c16cc79"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 19373,
"duration_ms": 19405,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1594,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5914,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.0912,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 1282,
"provider": "firstParty",
"thinkingTokens": 582,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition looks only at operations selected by name and dialect from the full pre-order operation lists of the two artifact roots: `callables` is every `llvm.func` in `output` at any depth, and `recovered` is every operation in `output` whose dialect prefix is `scf`. The first assertion is universally quantified over those callables but filtered to the ones with no \"local obstacle\" \u2014 that is, no transitive descendant that either carries a `branch_weights` attribute key or is named `llvm.indirectbr`, `llvm.blocktag`, or `cf.switch`; for each such obstacle-free callable it rejects the program unless that callable has zero transitive descendants in the `cf` dialect, and it says nothing at all about callables that do contain an obstacle. The second assertion is universally quantified over every `scf` operation `s`, and inside it over every transitive descendant `d` of `s`, every result `r` of `d`, and every use `u` of `r`, requiring that the using operation `u.owner` be structurally contained in `s`; it therefore rejects any value defined strictly inside a recovered structured operation that is consumed by an operation outside it, while placing no requirement on the results of `s` itself or on its block arguments. The third assertion is a single unquantified comparison of two string sets: the `sym_name` attribute strings (read via the `.string` projection, guarded by an `in` presence test) of all `llvm.func` operations in `output` must equal the same set computed over `input`, so a renamed, added, or removed symbol name is rejected while duplicate names and any change in count, order, ordering, or body are invisible to it. The only value sources are attribute presence and string projections, operation names and dialect prefixes, results and use lists, and the vocabulary's `descendants` and `contains` helpers \u2014 no operand segments, types, or symbol resolution are consulted. The first two assertions are vacuously satisfied when their selections are empty or when every callable carries an obstacle and when no `scf` operation has result-producing descendants with uses; the third is non-vacuous always, and is trivially satisfied when neither program contains any named `llvm.func` (both sets empty).",
"result_index": 0,
"session_id": "5ea230fe-b075-48fe-a75e-d442e9feac4d",
"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": 30,
"total_cost_usd": 0.0912,
"ttft_ms": 10187,
"ttft_stream_ms": 1161,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5914,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5914,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 1282,
"output_tokens_details": {
"thinking_tokens": 582
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "b6ebfd49-1f71-4c98-a2d7-6427ba36ad09"
}
]
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.