fix(shader): prove masked lanes unread across loops

Kena: Bridge of Spirits (PPSA01802) refuses ten pixel shaders with

  packed pixel ancillary input has an unsupported live use (used by SelectU32 ? ?)

at any visit limit. All ten have 30 to 33 phis on loop back edges (reported
on Linux with an RX 9070 XT).

Two rules stopped the proof at a loop, and the first one fires before the
second is ever asked:
- The walk from the select gave up at the first use inside a loop. A value
  derived from the select reaches a loop phi as soon as its register is
  written inside the loop, because the masked write becomes
  Select(loopExec, new, phi). A loop that leaves exec alone needs nothing
  more than this.
- An exec that a loop narrows and carries around its back edge is a phi
  inside the loop, and such phis counted as not implying the write's exec.

The walk now follows uses into loops. A phi inside a loop implies the
write's exec when all of its incoming values do, where the phi itself counts
as implying it while its back-edge values are checked. This is sound because
each rule of the proof takes a lane bit of one value from a value computed
earlier: a phi's value on each iteration is the incoming value computed
before the edge was taken, a set lane of an And is set in both operands, a
set lane of a ballot is a lane whose predicate held. If any value in the
proof had a lane set where the write's exec is clear, the earliest such
value would take that lane from an earlier value of the proof that is set
there too, which contradicts it being the earliest. Two conditions keep this
true:
- The write's exec must be computed once, outside every loop. Otherwise a
  phi can carry a ballot of it from an earlier iteration, which is not the
  value the select used. Masks computed inside a loop keep the old rules.
- A result may only be kept if the assumptions it used held. When a value
  that was assumed turns out not to be implied, every result recorded since
  it was assumed is dropped. Results that say "not implied" are kept; they
  only make the proof refuse more.

A lane that is turned back on inside the loop makes the back-edge exec wider
than the write's exec, so the phi is not implied and a read under it keeps
the select. A lane that is turned back on but never reads the derived value
does not.

New tests cover a loop that carries the write with exec saved, narrowed and
restored (read inside and after the loop), a loop that leaves exec alone,
and the helper-only ancillary select feeding such loops. The refusing tests
each fail when the matching check is removed: a revived lane that reads the
write inside the loop (ignoring back-edge values), a result proven under an
assumption that later fails (keeping it), and a write mask computed inside
an earlier loop (allowing such masks). Two existing tests expected a loop to
keep the select although every read is under the write's own exec; they now
expect it to go, next to new counterparts with a wider exec.

On the Taxi Chaos 2 requests, compute shaders with a loop inside a branch now
lose the branch's masked writes: 0x194000b400 removes 207 selects instead of
36, 0x19002bd200 111 instead of 28, and seven more gain 5 to 43. In
0x16400cf700 the 26 new removals are writes under the branch condition
tid < count; the loop's exec starts as a ballot of that condition, only loses
lanes at the latch, and every store and atomic inside the loop runs under it.
No proof on these requests had to drop a result.

Walks now go on into loops, so the pass takes longer on loop shaders, but it
stays below main. Time in MaskedSelectEliminator per prepare (median of 3,
the pass runs twice per prepare), 54 Taxi Chaos 2 requests, one run:

  shader          previous commit   this commit   main 5edae353
  0x1ac0413000         334 ms           349 ms         424 ms
  0x19002bd200          38 ms           103 ms         112 ms
  0x19c016aa00           9 ms            74 ms          16 ms
  0x194000b400          13 ms            31 ms          32 ms
  all 54               547 ms           805 ms         977 ms

0x19c016aa00 removes nothing more; its walks only end later inside its
loops. The 144 requests of the NVIDIA dump go from 1283 to 1589 ms and gain
removals in the copies of the same shaders. 197 of the 198 requests prepare,
as before.

Related: #2548

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

core/libs/prx/libSceAgcDriver/tests/MaskedSelect.cpp

@@ -77,6 +77,22 @@ struct Builder {
         return threadBit(low, high);
     }
 
+    std::pair<IrValue*, IrValue*> ballotWords(IrValue& predicate) {
+        auto& ballot = emit(IrOpcode::Ballot, IrType::U32x4, {&predicate});
+        return {&emit(IrOpcode::CompositeExtractU32x4, IrType::U32, {&ballot, &constant(0u)}), &emit(IrOpcode::CompositeExtractU32x4, IrType::U32, {&ballot, &constant(1u)})};
+    }
+
+    IrValue& wordAnd(IrValue& left, IrValue& right) {
+        return emit(IrOpcode::BitwiseAnd32, IrType::U32, {&left, &right});
+    }
+
+    IrValue& phi(IrType type, IrBlock& predecessor, IrValue& incoming) {
+        auto& created = program.CreateValue(IrOpcode::Phi, type);
+        block->AppendInstruction(&created);
+        created.AddPhiOperand(&predecessor, &incoming);
+        return created;
+    }
+
     void keep(IrValue& value) {
         (void)emit(IrOpcode::ReferenceU32, IrType::Void, {&value});
     }
@@ -339,8 +355,13 @@ int main() {
         return count == 0u && !gone;
     });
 
-    passed &= run("an exec merged by a phi inside a loop keeps the select", [&] {
+    passed &= run("an exec carried around a loop whose every incoming exec implies the write's exec drops the select", [&] {
         const auto [count, gone] = mergedExec(false, true);
+        return count == 1u && gone;
+    });
+
+    passed &= run("an exec carried around a loop with a wider incoming exec keeps the select", [&] {
+        const auto [count, gone] = mergedExec(true, true);
         return count == 0u && !gone;
     });
 
@@ -425,9 +446,10 @@ int main() {
         return b.eliminate() == 0u && !removed(written);
     });
 
-    passed &= run("a write read inside a later loop must keep its select", [] {
+    const auto laterLoop = [](bool wideRead) {
         Builder b;
-        auto& exec = b.mask(16u);
+        auto& wide = b.mask(48u);
+        auto& exec = b.logicalAnd(wide, b.mask(16u));
         auto& old = b.lane();
         auto& written = b.select(exec, b.add(old, 1u), old);
         IrBlock& head = *b.block;
@@ -435,7 +457,138 @@ int main() {
         head.AddBranch(&loop);
         loop.AddBranch(&loop);
         b.block = &loop;
-        b.keep(b.select(exec, b.add(written, 2u), old));
+        b.keep(b.select(wideRead ? wide : exec, b.add(written, 2u), old));
+        return std::pair{b.eliminate(), removed(written)};
+    };
+
+    passed &= run("a write read inside a later loop under its own exec loses its select", [&] {
+        const auto [count, gone] = laterLoop(false);
+        return count == 1u && gone;
+    });
+
+    passed &= run("a write read inside a later loop under a wider exec keeps its select", [&] {
+        const auto [count, gone] = laterLoop(true);
+        return count == 0u && !gone;
+    });
+
+    enum class Latch { Narrowed, Revived };
+    const auto carried = [](Latch latch, bool readInside) {
+        Builder b;
+        auto& wide = b.mask(48u);
+        auto& exec = b.logicalAnd(wide, b.mask(40u));
+        auto& old = b.lane();
+        auto& written = b.select(exec, b.add(old, 1u), old);
+        const auto [savedLow, savedHigh] = b.ballotWords(exec);
+        IrBlock& entry = *b.block;
+        IrBlock& header = b.newBlock();
+        IrBlock& exit = b.newBlock();
+        entry.AddBranch(&header);
+        header.AddBranch(&header);
+        header.AddBranch(&exit);
+        b.block = &header;
+        auto& low = b.phi(IrType::U32, entry, *savedLow);
+        auto& high = b.phi(IrType::U32, entry, *savedHigh);
+        auto& value = b.phi(IrType::U32, entry, written);
+        auto& loopExec = b.threadBit(low, high);
+        auto& next = b.select(loopExec, b.add(value, 2u), value);
+        if (readInside) b.keep(b.select(loopExec, b.add(value, 3u), old));
+        if (latch == Latch::Narrowed) {
+            const auto [stayLow, stayHigh] = b.ballotWords(b.mask(24u));
+            low.AddPhiOperand(&header, &b.wordAnd(low, *stayLow));
+            high.AddPhiOperand(&header, &b.wordAnd(high, *stayHigh));
+        } else {
+            const auto [revivedLow, revivedHigh] = b.ballotWords(wide);
+            low.AddPhiOperand(&header, revivedLow);
+            high.AddPhiOperand(&header, revivedHigh);
+        }
+        value.AddPhiOperand(&header, &next);
+        b.block = &exit;
+        b.keep(b.select(b.threadBit(*savedLow, *savedHigh), b.add(value, 4u), old));
+        return std::pair{b.eliminate(), removed(written)};
+    };
+
+    passed &= run("a write carried through a loop whose exec is saved, narrowed and restored loses its select", [&] {
+        const auto [count, gone] = carried(Latch::Narrowed, false);
+        return count == 1u && gone;
+    });
+
+    passed &= run("a write read inside a loop under the loop's narrowed exec loses its select", [&] {
+        const auto [count, gone] = carried(Latch::Narrowed, true);
+        return count == 1u && gone;
+    });
+
+    passed &= run("a lane that becomes active again inside a loop and reads the write keeps the select", [&] {
+        const auto [count, gone] = carried(Latch::Revived, true);
+        return count == 0u && !gone;
+    });
+
+    passed &= run("a lane that becomes active again inside a loop but never reads the write lets the select go", [&] {
+        const auto [count, gone] = carried(Latch::Revived, false);
+        return count == 1u && gone;
+    });
+
+    passed &= run("an exec proven only by assuming a loop phi is forgotten once that phi turns out wider", [] {
+        Builder b;
+        auto& wide = b.mask(48u);
+        auto& exec = b.logicalAnd(wide, b.mask(40u));
+        auto& old = b.lane();
+        auto& written = b.select(exec, b.add(old, 1u), old);
+        const auto [savedLow, savedHigh] = b.ballotWords(exec);
+        IrBlock& entry = *b.block;
+        IrBlock& header = b.newBlock();
+        IrBlock& kill = b.newBlock();
+        IrBlock& revive = b.newBlock();
+        IrBlock& latch = b.newBlock();
+        IrBlock& exit = b.newBlock();
+        entry.AddBranch(&header);
+        header.AddBranch(&kill);
+        header.AddBranch(&revive);
+        kill.AddBranch(&latch);
+        revive.AddBranch(&latch);
+        latch.AddBranch(&header);
+        latch.AddBranch(&exit);
+        b.block = &header;
+        auto& low = b.phi(IrType::U32, entry, *savedLow);
+        auto& high = b.phi(IrType::U32, entry, *savedHigh);
+        (void)b.select(b.threadBit(low, high), written, old);
+        b.block = &kill;
+        const auto [stayLow, stayHigh] = b.ballotWords(b.mask(24u));
+        auto& killedLow = b.wordAnd(low, *stayLow);
+        auto& killedHigh = b.wordAnd(high, *stayHigh);
+        b.keep(b.select(b.threadBit(killedLow, killedHigh), written, old));
+        b.block = &revive;
+        const auto [revivedLow, revivedHigh] = b.ballotWords(wide);
+        b.block = &latch;
+        auto& mergedLow = b.phi(IrType::U32, kill, killedLow);
+        auto& mergedHigh = b.phi(IrType::U32, kill, killedHigh);
+        mergedLow.AddPhiOperand(&revive, revivedLow);
+        mergedHigh.AddPhiOperand(&revive, revivedHigh);
+        low.AddPhiOperand(&latch, &mergedLow);
+        high.AddPhiOperand(&latch, &mergedHigh);
+        return b.eliminate() == 0u && !removed(written);
+    });
+
+    passed &= run("a write mask computed inside an earlier loop does not let that loop's phis stand for it", [] {
+        Builder b;
+        auto& old = b.lane();
+        IrBlock& entry = *b.block;
+        IrBlock& header = b.newBlock();
+        IrBlock& exit = b.newBlock();
+        entry.AddBranch(&header);
+        header.AddBranch(&header);
+        header.AddBranch(&exit);
+        b.block = &header;
+        auto& low = b.phi(IrType::U32, entry, b.constant(0u));
+        auto& high = b.phi(IrType::U32, entry, b.constant(0u));
+        auto& bound = b.phi(IrType::U32, entry, b.constant(64u));
+        auto& exec = b.emit(IrOpcode::ULessThan32, IrType::Bool, {&b.lane(), &bound});
+        const auto [stayLow, stayHigh] = b.ballotWords(exec);
+        low.AddPhiOperand(&header, stayLow);
+        high.AddPhiOperand(&header, stayHigh);
+        bound.AddPhiOperand(&header, &b.emit(IrOpcode::ISub32, IrType::U32, {&bound, &b.constant(8u)}));
+        b.block = &exit;
+        auto& written = b.select(exec, b.add(old, 1u), old);
+        b.keep(b.select(b.threadBit(low, high), b.add(written, 2u), old));
         return b.eliminate() == 0u && !removed(written);
     });
 

core/libs/tests/PixelAncillary.cpp

@@ -340,6 +340,93 @@ static void HelperLanesRefused(HelperRead read, std::uint32_t chain = 0u) {
     }
     Require(false);
 }
+enum class LoopRead { ExportAfter, ExportInside, UniformLoop, RevivedExportInside };
+
+static IrValue& LaneBit(IrBuilder& builder, IrValue& low, IrValue& high) {
+    IrValue& lane = builder.Emit(IrOpcode::LaneId, IrType::U32, {});
+    IrValue& word = builder.Select(builder.Emit(IrOpcode::ULessThan32, IrType::Bool, {&lane, &builder.Constant(32u)}), low, high);
+    IrValue& shifted = builder.Emit(IrOpcode::ShiftRightLogical32, IrType::U32, {&word, &builder.BitwiseAnd(lane, builder.Constant(31u))});
+    return builder.INotEqual(builder.BitwiseAnd(shifted, builder.Constant(1u)), builder.Constant(0u));
+}
+static HelperProgram HelperLoop(IrProgram& program, LoopRead read) {
+    auto& entry = Begin(program);
+    auto& header = program.CreateBlock();
+    auto& exit = program.CreateBlock();
+    program.BlockOrder().push_back(&header);
+    program.BlockOrder().push_back(&exit);
+    entry.AddBranch(&header);
+    header.AddBranch(&header);
+    header.AddBranch(&exit);
+    IrBuilder builder(program);
+    builder.SetInsertionPoint(entry);
+    IrValue& helper = builder.Emit(IrOpcode::GetBuiltin, IrType::U32, {&builder.Constant(static_cast<std::uint32_t>(StageInputKind::HelperInvocation)), &builder.Constant(0u)});
+    IrValue& live = builder.IEqual(helper, builder.Constant(0u));
+    IrValue& ancillary = AncillaryBuiltin(builder);
+    IrValue& layer = builder.Emit(IrOpcode::BitFieldUExtract, IrType::U32, {&ancillary, &builder.Constant(16u), &builder.Constant(11u)});
+    IrValue& target = builder.Select(live, layer, builder.Constant(0u));
+    IrValue& written = builder.Select(live, builder.Constant(SelectOther), ancillary);
+    IrValue& frontFacing = FrontFacingBuiltin(builder);
+    IrValue& saved = builder.Emit(IrOpcode::Ballot, IrType::U32x4, {&live});
+    IrValue& savedLow = builder.CompositeExtract(saved, 0u);
+    IrValue& savedHigh = builder.CompositeExtract(saved, 1u);
+    IrValue& low = program.CreateValue(IrOpcode::Phi, IrType::U32);
+    IrValue& high = program.CreateValue(IrOpcode::Phi, IrType::U32);
+    IrValue& value = program.CreateValue(IrOpcode::Phi, IrType::U32);
+    header.AppendInstruction(&low);
+    header.AppendInstruction(&high);
+    header.AppendInstruction(&value);
+    low.AddPhiOperand(&entry, &savedLow);
+    high.AddPhiOperand(&entry, &savedHigh);
+    value.AddPhiOperand(&entry, &written);
+    builder.SetInsertionPoint(header);
+    IrValue& loopExec = read == LoopRead::UniformLoop ? live : LaneBit(builder, low, high);
+    IrValue& squared = builder.Emit(IrOpcode::FPMul32, IrType::F32, {&builder.BitCastF32(value), &builder.BitCastF32(value)});
+    IrValue& next = builder.Select(loopExec, builder.BitCastU32(squared), value);
+    IrValue& stay = builder.Emit(IrOpcode::Ballot, IrType::U32x4, {&frontFacing});
+    IrValue& stayLow = builder.CompositeExtract(stay, 0u);
+    IrValue& stayHigh = builder.CompositeExtract(stay, 1u);
+    const bool revived = read == LoopRead::RevivedExportInside;
+    low.AddPhiOperand(&header, revived ? &stayLow : &builder.BitwiseAnd(low, stayLow));
+    high.AddPhiOperand(&header, revived ? &stayHigh : &builder.BitwiseAnd(high, stayHigh));
+    value.AddPhiOperand(&header, &next);
+    program.Metadata().exportInfo.push_back(ExportInfo {.kind = ExportTargetKind::Mrt, .index = 0u, .en = 0xFu, .done = true, .vm = true});
+    const auto exportValue = [&](IrValue& guard) {
+        IrValue& data = builder.Emit(IrOpcode::CompositeConstructU32x4, IrType::U32x4, {&value, &target, &builder.Constant(0u), &builder.Constant(0u)});
+        static_cast<void>(builder.Emit(IrOpcode::SetAttribute, IrType::Void, {&data, &guard}, ExportFlags {0u, 0u}));
+    };
+    if (read == LoopRead::ExportInside || revived) exportValue(loopExec);
+    builder.SetInsertionPoint(exit);
+    if (read == LoopRead::ExportAfter) exportValue(LaneBit(builder, savedLow, savedHigh));
+    if (read == LoopRead::UniformLoop) exportValue(live);
+    static_cast<void>(builder.Emit(IrOpcode::Return, IrType::Void, {}));
+    return HelperProgram {&written, &layer, &value};
+}
+static void HelperLoopOnly(LoopRead read) {
+    IrProgram program;
+    const HelperProgram built = HelperLoop(program, read);
+    LowerMasked(program);
+    for (const IrBlock* block : program.BlockOrder()) {
+        for (const IrValue* inst : block->Instructions()) {
+            Require(inst->Opcode() != IrOpcode::GetBuiltin || static_cast<StageInputKind>(inst->Argument(0)->Resolve()->ImmediateU32()) != StageInputKind::PackedAncillary);
+        }
+    }
+    Require(built.written->Parent() == nullptr);
+    const IrValue* field = built.layer->Argument(0)->Resolve();
+    Require(field->Opcode() == IrOpcode::GetBuiltin && static_cast<StageInputKind>(field->Argument(0)->Resolve()->ImmediateU32()) == StageInputKind::Layer);
+    const IrValue* entryValue = built.exported->Argument(0)->Resolve();
+    Require(entryValue->HasImmediate() && entryValue->ImmediateU32() == SelectOther);
+}
+static void HelperLoopRefused(LoopRead read) {
+    IrProgram program;
+    static_cast<void>(HelperLoop(program, read));
+    try {
+        LowerMasked(program);
+    } catch (const std::runtime_error& error) {
+        Require(std::string(error.what()).find("unsupported live use") != std::string::npos);
+        return;
+    }
+    Require(false);
+}
 int main() {
     Extract(IrOpcode::BitFieldUExtract, 8u, 4u, StageInputKind::SampleId, 0u);
     Extract(IrOpcode::BitFieldUExtract, 9u, 2u, StageInputKind::SampleId, 1u);
@@ -385,4 +472,8 @@ int main() {
     HelperLanesRefused(HelperRead::DataTestExport);
     HelperLanesRefused(HelperRead::Ballot);
     HelperLanesRefused(HelperRead::FullWaveExport, 6000u);
+    HelperLoopOnly(LoopRead::ExportAfter);
+    HelperLoopOnly(LoopRead::ExportInside);
+    HelperLoopOnly(LoopRead::UniformLoop);
+    HelperLoopRefused(LoopRead::RevivedExportInside);
 }

core/shader/recompiler/Optimization/src/MaskedSelectEliminator.cpp

@@ -274,6 +274,11 @@ Region regionOf(const std::vector<Region>& regions, const IrBlock* block) {
     return block != nullptr && block->Id() < regions.size() ? regions[block->Id()] : Region::Unreached;
 }
 
+bool followable(const std::vector<Region>& regions, const IrBlock* block, bool acrossLoops) {
+    const Region region = regionOf(regions, block);
+    return region == Region::Once || (acrossLoops && region == Region::Loop);
+}
+
 struct ImplicationKey {
     const IrValue* first = nullptr;
     const IrValue* second = nullptr;
@@ -291,10 +296,13 @@ class Implications {
 public:
     Implications(const std::vector<Region>& regions, std::uint32_t waveSize, std::size_t& work) : regions(regions), waveSize(waveSize), work(work) {}
 
-    void Reset(const IrValue* writeMask) {
+    void Reset(const IrValue* writeMask, bool acrossLoops) {
         mask = writeMask;
+        loops = acrossLoops;
         always = alwaysTrue(writeMask, waveSize);
         results.clear();
+        proven.clear();
+        assumptionReads = 0;
     }
 
     bool Implies(const IrValue* condition, std::uint32_t depth = 0) {
@@ -302,33 +310,61 @@ public:
         if (condition == mask || always) return true;
         if (condition->HasImmediate()) return condition->Type() == IrType::Bool && !condition->ImmediateBool();
         const ImplicationKey key{condition, nullptr};
-        if (const auto known = results.find(key); known != results.end()) return known->second;
+        if (const auto known = lookup(key)) return *known;
         if (depth > ImplicationDepthLimit || work == 0) return false;
         --work;
-        results.emplace(key, false);
+        const Attempt attempt = assume(key);
         bool result = false;
         if (condition->Opcode() == IrOpcode::LogicalAnd) {
             result = Implies(condition->Argument(0), depth + 1u) || Implies(condition->Argument(1), depth + 1u);
         } else if (condition->IsPhi()) {
-            result = mergesOutsideLoops(*condition);
+            result = merges(*condition);
             for (std::size_t index = 0; result && index < condition->ArgumentCount(); ++index) {
                 result = Implies(condition->Argument(index), depth + 1u);
             }
         } else if (const auto bit = threadBit(condition, waveSize)) {
             result = wordsImply(bit->low, bit->high, depth + 1u);
         }
-        results[key] = result;
-        return result;
+        return settle(key, attempt, result);
     }
 
 private:
     static constexpr std::uint32_t ImplicationDepthLimit = 64;
 
-    bool mergesOutsideLoops(const IrValue& phi) const {
-        if (regionOf(regions, phi.Parent()) != Region::Once || phi.ArgumentCount() != phi.PhiBlockCount()) return false;
+    enum class Proof : std::uint8_t { Assumed, Implied, NotImplied };
+
+    struct Attempt {
+        std::size_t proven = 0;
+        std::size_t assumptionReads = 0;
+    };
+
+    std::optional<bool> lookup(const ImplicationKey& key) {
+        const auto known = results.find(key);
+        if (known == results.end()) return std::nullopt;
+        if (known->second == Proof::Assumed) ++assumptionReads;
+        return known->second != Proof::NotImplied;
+    }
+
+    Attempt assume(const ImplicationKey& key) {
+        results.emplace(key, Proof::Assumed);
+        return Attempt{proven.size(), assumptionReads};
+    }
+
+    bool settle(const ImplicationKey& key, const Attempt& attempt, bool implied) {
+        if (!implied && assumptionReads != attempt.assumptionReads) {
+            for (std::size_t index = attempt.proven; index < proven.size(); ++index) results.erase(proven[index]);
+            proven.resize(attempt.proven);
+        }
+        results[key] = implied ? Proof::Implied : Proof::NotImplied;
+        if (implied) proven.push_back(key);
+        return implied;
+    }
+
+    bool merges(const IrValue& phi) const {
+        if (!followable(regions, phi.Parent(), loops) || phi.ArgumentCount() != phi.PhiBlockCount()) return false;
         for (std::size_t index = 0; index < phi.ArgumentCount(); ++index) {
             const IrValue* incoming = phi.Argument(index)->Resolve();
-            if (!incoming->HasImmediate() && regionOf(regions, incoming->Parent()) != Region::Once) return false;
+            if (!incoming->HasImmediate() && !followable(regions, incoming->Parent(), loops)) return false;
         }
         return true;
     }
@@ -343,10 +379,10 @@ private:
     bool wordsImply(const IrValue* low, const IrValue* high, std::uint32_t depth) {
         if (isImmediate(low, 0u) && (waveSize == 32u || isImmediate(high, 0u))) return true;
         const ImplicationKey key{low, high};
-        if (const auto known = results.find(key); known != results.end()) return known->second;
+        if (const auto known = lookup(key)) return *known;
         if (depth > ImplicationDepthLimit || work == 0) return false;
         --work;
-        results.emplace(key, false);
+        const Attempt attempt = assume(key);
         bool result = false;
         if (low->Opcode() == IrOpcode::CompositeExtractU32x4 && isImmediate(low->Argument(1)->Resolve(), 0u)) {
             const IrValue* ballot = low->Argument(0)->Resolve();
@@ -364,23 +400,25 @@ private:
                 }
             }
         }
-        if (!result && low->IsPhi() && mergesOutsideLoops(*low) && (waveSize == 32u || (high->IsPhi() && high->Parent() == low->Parent() && mergesOutsideLoops(*high)))) {
+        if (!result && low->IsPhi() && merges(*low) && (waveSize == 32u || (high->IsPhi() && high->Parent() == low->Parent() && merges(*high)))) {
             result = true;
             for (std::size_t index = 0; result && index < low->PhiBlockCount(); ++index) {
                 const IrValue* highIncoming = waveSize == 32u ? high : incomingFrom(*high, low->PhiBlock(index));
                 result = highIncoming != nullptr && wordsImply(low->Argument(index)->Resolve(), highIncoming, depth + 1u);
             }
         }
-        results[key] = result;
-        return result;
+        return settle(key, attempt, result);
     }
 
     const std::vector<Region>& regions;
     std::uint32_t waveSize;
     std::size_t& work;
     const IrValue* mask = nullptr;
+    bool loops = false;
     bool always = false;
-    std::unordered_map<ImplicationKey, bool, ImplicationKeyHash> results;
+    std::unordered_map<ImplicationKey, Proof, ImplicationKeyHash> results;
+    std::vector<ImplicationKey> proven;
+    std::size_t assumptionReads = 0;
 };
 
 std::vector<Region> blockRegions(const IrProgram& program) {
@@ -436,8 +474,9 @@ public:
     MaskedLaneWalk(const IrProgram& program, const std::vector<Region>& regions) : program(program), regions(regions), limit(walkLimit(program)), implications(regions, program.WaveSize(), work) {}
 
     bool UnobservedWhereMasked(const IrValue& select, const IrValue* mask) {
+        const bool acrossLoops = mask->HasImmediate() || regionOf(regions, mask->Parent()) == Region::Once;
         work = limit;
-        implications.Reset(mask);
+        implications.Reset(mask, acrossLoops);
         startVisits();
         pending.clear();
         pending.push_back(&select);
@@ -447,7 +486,7 @@ public:
             pending.pop_back();
             for (const IrUse& use : value->OperandUses()) {
                 const IrValue* user = use.user;
-                if (regionOf(regions, user->Parent()) != Region::Once) return false;
+                if (!followable(regions, user->Parent(), acrossLoops)) return false;
                 if (isSelect(user->Opcode()) && use.operand == 1u && implications.Implies(user->Argument(0))) continue;
                 if (user->Opcode() == IrOpcode::LogicalAnd && use.operand < 2u && implications.Implies(user->Argument(1u - use.operand))) continue;
                 if (readsOnlyWhereActive(user->Opcode()) && use.operand + 1u < user->ArgumentCount() && implications.Implies(user->Argument(user->ArgumentCount() - 1u))) continue;