loom-raise-opt: publication rejects two scf.if ops that share a predicate across an scf.for

[benlimpa]

Observed on main at edb3e56c16593024f78a70e85b13b4a9ba742fb8 (2026-08-31).

Spec

docs/spec-compiler-part-3-dfg.md:110-112:

The recursive lowering contract accepts arbitrary nesting of scf.if,
source-sequential scf.for, scf.while, and fixed-width graph-owned
scf.parallel or effect-form scf.forall.

Input

One loom.spatial_region whose body is scf.if, scf.for, scf.if, with both
conditionals guarded by the same i1 value. No results, no else, constant
trip count.

module {
  dataflow.thread private @t domain(#dataflow.thread_domain<dense>)(%target: memref<16xi32>, %value: i32) ctrl (%ctrl: none) {
    "loom.spatial_region"(%value, %target) <{operandSegmentSizes = array<i32: 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0>}> ({
    ^bb0(%payload: i32, %memory: memref<16xi32>):
      %one = arith.constant 1 : i32
      %p = arith.cmpi ne, %payload, %one : i32
      %i0 = arith.constant 0 : index
      %i1 = arith.constant 1 : index
      %n = arith.constant 4 : index
      scf.if %p {
        memref.store %payload, %memory[%i0] : memref<16xi32>
      }
      scf.for %i = %i0 to %n step %i1 {
        memref.store %one, %memory[%i] : memref<16xi32>
      }
      scf.if %p {
        memref.store %payload, %memory[%i1] : memref<16xi32>
      }
      "loom.spatial_yield"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
    }) {graph_name = "g", source_maps = []} : (i32, memref<16xi32>) -> ()
    dataflow.thread.yield
  }
}

Actual

$ loom-raise-opt --loom-lower-for-to-graph repro.mlir
repro.mlir:5:1: error: canonical Dataflow publication failed: graph @g completion witness #1 is not statically one-shot

Expected

The module publishes, with no scf.* op left in @g.

Explanation

The rejection is not a property of the program. Three one-edit variants are all accepted:

edit	result
guard the second scf.if with a second, distinct arith.cmpi	accepted
move the scf.for above the first scf.if	accepted
delete the scf.for	accepted

For the first, the lowered graph is identical operation for operation to the
rejected one. The only difference is that the second conditional's selector is a
different SSA value from the first's.

The cause looks like memoization in GraphCardinalityAnalysis
(lib/Dataflow/IR/DataflowGraphValidation.cpp). The analysis walks a cyclic
graph, so a query that re-enters itself is cut off and answered conservatively
(isExactOne and evaluateAlignment answer false, isCarrySystemAligned
answers true). Those answers hold only while that recurrence is open, but the
result computed above them is written into a cache shared across the whole
validation, so a later independent query reads a provisional answer as a fact.
Sharing one predicate makes the two conditionals reconvergent, which is what
puts both witness queries on the same cached values.

Confirmed by rebuilding loom-raise-opt with the five memo tables disabled and
the cutoffs kept: the reproducer publishes, as do all 30 samples from the
generator that found this. Disabling only the exactOne table instead makes
other samples newly fail, so the cached values are contaminated in both
directions rather than simply being too strict.

Possible fix, with a caveat

Skipping memoization of any result whose computation depended on a cutoff (one
provisional flag threaded through CardinalitySharedState) makes all 30
samples publish, with test/raise and test/dataflow unchanged at 123/124
(the one failure is pre-existing and unrelated).

But it costs the complexity bound that cfc799c3e added. On a synthetic region
with k shared-predicate conditionals interleaved with k loops, k=4 takes 2.4 s
and k>=5 does not finish in 60 s, where today's build is flat at ~30 ms because
it stops early on an answer that is wrong from k=2 on. So the caching appears to
be holding that bound partly by returning these wrong answers. A real fix
probably has to scope provisional entries to the recurrence that produced them,
committing only when its head closes, rather than writing them to the shared
table immediately.