Allow the simplifier to use facts in its can_prove() predicates.

[mcourteaux]

Problem statement

While preparing #9371, I hit several dead ends trying to produce very neat IR. The reason is the simplifier cannot simplify max(x, y) = x when we give the assumption x >= y. Intuitively, one would write in Simplify_Max.cpp:

rewrite(max(x, y), a, can_prove(x >= y, this))

However, the way can_prove(Expr, Prover) is implemented is to recursively mutate() the Expr with the Prover (i.e., this instance of Simplify). This however, does not substitute in the facts (truths), and therefore fails to "prove" that x > y.

A secondary problem with rewrite rules that use can_prove() is that they recursively invoke the simplifier, which leads potentially to infinite recursions. Specifically, Andrew stated:

Calling can_prove as the third arg to rewrite recursively invokes the simplifier on every expr that matches that LHS. If one of them itself creates an intermediate expression that also matches the LHS, you get infinite recursion.

Solution: Let the simplifier use what it knows about ordering

The simplifier learns facts on the way down the IR (if conditions, asserts, loop bounds), but rewrite rules could only consult them through can_prove, which recursively re-invokes the simplifier on a freshly built condition. That is both expensive and unsound to use in a rule matching a common node type: if the rule's own left-hand side matches something built while proving its predicate, it recurses without bound. This branch replaces that mechanism for ordering questions and adds rules that use it.

What it adds

known_difference — the simplifier now keeps a ConstantInterval on the difference between pairs of expressions. Every comparison it can learn from is a statement about a - b: a < b means at most -1, !(a < b) at least 0, a == b exactly zero. Direction and strictness stop being special cases — the other direction is the negated interval, strictness is whether the bound is -1 or 0.

Because the complement of a half-line is a half-line, only a negated equality fails to be an interval, and that is always a single point removed (KnownBound::invert). A removed point tightens the bounds when it lands on an end, and is otherwise tracked only at zero, which is what decides known_not_equal.

Constant offsets are peeled off both facts and queries, so a fact about x and y + 3 settles a question about x and y. Two constants, and a min/max compared against one of its own operands, are decided from shape alone with no facts at all.

Two new rewrite predicates, min_diff(x, y, this) and max_diff(x, y, this) (plus known_equal/known_not_equal, not yet used by any rule). They read the nodes a rule has already bound — MatcherState holds raw node pointers — so testing one allocates nothing. They are restricted to wildcard operands by static_assert, which makes that property structural rather than a thing to be careful about.

known_true — a non-recursive can_prove, kept for rules whose predicate isn't a pairwise difference (the division rules).

A depth limit on can_prove, checked where the recursion happens rather than in each rule's guard, so it covers pre-existing rules too.

New rules: max/min pick a side when the facts order the operands, and a division can cancel a multiplication inside a max/min.

Why the depth limit matters

Before it, apps/lens_blurdid not compile — lowering ran for 52 minutes of CPU before I killed it. The min(x, y) - min(z, w) → y - w, can_prove(x - y == z - w) family in Simplify_Sub.cpp builds a fresh subtraction to test, which can match the same rule again; a 10-deep nest of that shape never terminates. test/correctness/simplify.cpp has a regression test for it that hangs if the limit is removed.

Compile-time impact

Lowering only (generator with -e stmt, so no LLVM codegen), against main a3690b3b6:

	main	branch	Δ
lens_blur, retired instructions	2.2161 G	2.2378 G	+0.98%
local_laplacian, retired instructions	1.4090 G	1.4201 G	+0.79%
lens_blur, wall (min of 15)	0.510 s	0.500 s	indistinguishable
local_laplacian, wall (min of 15)	0.330 s	0.320 s	indistinguishable

Lowered output is byte-identical on both apps — these pipelines pay a small cost and get nothing back; the new rules never fire in them.

Across the whole correctness suite (411 tests, 52 skipped, sequential, peak RSS and wall time per test): median wall-time change +0.00%, total 576.3 s → 576.0 s, median peak RSS −0.41%. Both trees green, 0 failures.

Most of the cost was removed rather than accepted. On lens_blur, overhead versus main went +5.0% → +0.98%:

	instructions	vs main
first working version (can_prove per node)	2.297 G	+5.0%
known_true instead of can_prove	—	+8.2%¹
difference intervals instead of building IR	2.218 G	+1.4%
gate on the difference table, not on any fact	2.216 G	+1.33%
reject the whole table in one test	2.208 G	+0.96%

¹ measured at an earlier baseline; the trend is what matters.

The lookup work itself is now 3 M instructions (0.14%) of lowering — the rest is the rules being attempted on every max/min, which no lookup change addresses.

Notes for review

• has_facts() was split. min_diff/max_diff gate on has_difference_facts(), because a boolean fact or one about a wrapping type satisfies the old predicate while leaving the difference table empty — that was a fifth of all lookups on lens_blur, each one guaranteed to find nothing.
• The rejection filter is a bitmask over a symmetric per-pair key, kept on the table (not per record, so the fallback scan touches smaller records) and saved/restored wholesale by each scope, since bits can't be cleared individually.
• ScopedFact's move constructor is no longer = default. The existing members are containers that end up empty after a move, so the moved-from destructor was harmless; a plain size_t index is not, and silently truncated away facts that had just been learned.

---

Two caveats before you post: the +0.98% is real but sits close to run-to-run variation in wall time, so I'd lead with the instruction counts as I have. And the "0 matched a fact" observation behind the filter design is a property of lens_blur, not a general law — a pipeline whose facts actually relate its max/min operands would behave differently.

Checklist

• Tests added or updated (not required for docs, CI config, or typo fixes)
• Documentation updated (if public API changed)
• Python bindings updated (if public API changed)
• Benchmarks are included here if the change is intended to affect performance.
• Commits include AI attribution where applicable (see Code of Conduct)

[codecov]

Codecov Report

❌ Patch coverage is 82.72425% with 52 lines in your changes missing coverage. Please review.
✅ Project coverage is 70.00%. Comparing base (a3690b3) to head (0d05e92).

Files with missing lines	Patch %	Lines
src/Simplify.cpp	76.99%	28 Missing and 24 partials ⚠️

Additional details and impacted files

@@ Coverage Diff @@## main #9400 +/- ##
==========================================
- Coverage 70.12% 70.00% -0.13% 
==========================================
Files 261 261 Lines 79405 79699 +294 Branches 19362 19452 +90 ==========================================
+ Hits 55684 55791 +107 - Misses 17896 17950 +54 - Partials 5825 5958 +133 

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[abadams]

Was this the one that inflated the lowering time of lens_blur? Is this superseded by your approach in aligned splits take 2?

[abadams]

Some more data: yesterday in a research branch I came across a case where max(x, y) was not simplifying inside an if (x <= y) branch, and it was causing wmma ops to fail to be extracted. This is a case we need to handle, we just need to figure out how to do it without increasing compile times.

[abadams]

I think an approach to make this fast might be to define an operator< that can compare IRMatcher patterns to Exprs, so that the pattern can be looked up in the set of known facts without constructing an IR node, rather than needing to build an Expr just to do the lookup.

[mcourteaux]

Was this the one that inflated the lowering time of lens_blur? Is this superseded by your approach in aligned splits take 2?

This indeed did slow down lens blur by 10% more ore less. It's not superseded: take 2 just works around the simplification issue by using .bound_extent() and .bound_storage().

Some more data: yesterday in a research branch I came across a case where max(x, y) was not simplifying inside an if (x <= y) branch, and it was causing wmma ops to fail to be extracted. This is a case we need to handle, we just need to figure out how to do it without increasing compile times.

🤝

I think an approach to make this fast might be to define an operator< that can compare IRMatcher patterns to Exprs, so that the pattern can be looked up in the set of known facts without constructing an IR node, rather than needing to build an Expr just to do the lookup.

That sounds like a decent approach! Feel free to take over this branch!

[mcourteaux]

What if instead, we special handle the generic-form max(x, y) and min(x, y) above the chain of rewrite rules, by doing a fact_lookup_comparison(x, y) that returns an enum: NOTHING_KNOWN, LT, LE, EQ, GE, GT.

As such, no known_true() is called for every Max node, and no new Expr is constructed.

We can keep the more expensive machinery for non-trivial rules, such as the ones now in Simplify_Div, which wouldn't trigger for every Max/Min node, because the LHS of the rewrite rule is more specific:

has_facts()&&(rewrite(max(x*c0,y)/c0,x,c0>0&&known_true(x>=y/c0,this))||rewrite(max(y,x*c0)/c0,x,c0>0&&known_true(x>=y/c0,this))||rewrite(min(x*c0,y)/c0,x,c0>0&&known_true(x<=y/c0,this))||rewrite(min(y,x*c0)/c0,x,c0>0&&known_true(x<=y/c0,this)))

The existing known_true() would then call out to fact_lookup_comparison().

Later, when we learn_true(some_expr % some_other_expr == 0) for example, we can have special handling in Simplify_Mod with a fact_lookup_modrem(x, y), which can return more info specific to those kind of facts.

[mcourteaux]

Offline discussion with @abadams, with some ideas going back and forth, Andrew proposed to:

record a list of (Expr, Expr, ConstantInterval), where the interval is constant bounds on the difference between the two Exprs. Then in the predicate you could query the lower or upper bound of the difference.

As such, we can have a function that return ConstantBounds for the difference between two Expr. Then you can write predicates like this:

rewrite(max(x, y), x, min_diff(x, y, this) >= 0) // because x - y >= 0, we know that x >= y.

[mcourteaux]

@abadams Ready for review. Original post updated. This was all Claude with a lot of guidance, so perhaps a lot of comments are still too verbose, and maybe a few names left and right could be better. However, I think the approach is good.

Performance impact of the lookups was real, so we iterated a bit to make them even faster using a cheap hashing scheme. This was the initial histogram of number of facts present, during fact lookup happening within lens_blur:

The massive amount of lookups when there were no facts was fixed after this chart was made. Claude argued by doing some analysis on different runs of retired instruction count that a std::map would not make things faster; not actually measured yet.