[glyh]

DISCLAIMER: This is AI generated, then iterated and reviewed by me.

---

The subtype walk in optAssertionVNIsSubtype passes budget - 1 down each PHI edge, so budget limits depth and nothing limits work. The same merge gets re-proven by every path that reaches it, which is exponential in the number of merges, and optVisitReachingAssertions allocates two BitVecs per call so the arena climbs alongside. Nine 8-way switches into one if (o is A a) is enough to hit it (#133857).

The memo wraps the PHI walk, and only the walk. The recursive body moved to optAssertionVNIsSubtypeWorker; optAssertionVNIsSubtype creates the memo and calls it, and the recursion goes through the worker so every frame shares the one table. It lives on the top-level frame, so it dies with the query — no generation stamp, no compiler state.

Watch out for

• Never cache false. A false from this walk means either "no proof" or "ran out of budget", and the second isn't a property of the key — the same key can come back false at depth 3 and true at depth 9, so storing it would permanently discard a proof. A true is a real derivation and stays valid at any depth and on any path, cyclic or not, which is also why cyclic PHIs need no in-progress marking.
• The key is only sound because the memo sits below the direct-assertion check. That check is the one part that reads the caller's assertion set. The walk below it reads each edge's own set instead (optVisitReachingAssertions: "We assume that the caller already checked assertions for the current block"), so (value, claim) is the walk's whole input. Hoisting the lookup above the check would serve a proof derived from a different set.
• A hit can be served at a shallower budget than the one that produced it. No depth is in the key, so a true found with 9 levels left answers a frame with 3. That is safe because the budget bounds search effort, not the validity of a derivation, and it can only fold casts that are genuinely provable.

Numbers

Whole-process wall time on the reproducer: 100 in ~145 ms with this JIT, 102 at 10,688 ms against the parent commit's JIT built in the same tree, which trips the test's own 2000 ms bound.

Memory: AssertionProp goes 8,892 → 9,404 bytes on that repro, so the memo costs 512. My first cut hard-coded a 2048-entry array, which was 49,152 bytes for a method that needs 73 entries.

Not in this PR

optAssertionVNIsNonNull has the same shape and no memo. That's #134462; the attempt there (#134916) is closed rather than merged, and doesn't overlap this.

[glyh]

@dotnet-policy-service agree

[azure-pipelines]

Azure Pipelines:
Successfully started running 5 pipeline(s).
11 pipeline(s) were filtered out due to trigger conditions.
There may be pipelines that require an authorized user to comment /azp run to run.

[dotnet-policy-service]

Tagging subscribers to this area: @JulieLeeMSFT, @jakobbotsch
See info in area-owners.md if you want to be subscribed.