Aligned splits, take 2.

[mcourteaux]

Inner loops go from 0 to factor, to help with constant bounds analysis.
2D tiled test: compute_at test overwrites the compute and storage bounds by just passing those in the schedule.

// f.split(x, xo, xi, 32);
for (xo, f.min.0, f.max.0 / 32) {
  for (xi, 0, 31) {
      let x = xo * 32 + xi 
  }
}

It's now possible to align the first iteration of the inner loop, like so:

// f.split(x, xo, xi, 32, p);
for (xo, (f.min.0 - p) / 32, (f.max.0 - p) / 32) {
  for (xi, 0, 31) {
      let x = xo * 32 + xi + p
      if (x >= f.min.0 && x <= f.max.0) { // for GuardWithIf

      }
  }
}

Replaces #9371

Breaking changes

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 95.91837% with 8 lines in your changes missing coverage. Please review.
✅ Project coverage is 69.94%. Comparing base (5f95e0c) to head (12642a9).
⚠️ Report is 10 commits behind head on main.

Files with missing lines	Patch %	Lines
src/Func.cpp	77.27%	4 Missing and 1 partial ⚠️
src/Simplify_Exprs.cpp	80.00%	0 Missing and 2 partials ⚠️
src/ApplySplit.cpp	98.55%	0 Missing and 1 partial ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #9409      +/-   ##
==========================================
- Coverage   70.12%   69.94%   -0.18%     
==========================================
  Files         261      261              
  Lines       79938    80138     +200     
  Branches    19478    19532      +54     
==========================================
  Hits        56053    56053              
- Misses      18056    18129      +73     
- Partials     5829     5956     +127     

☔ 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]

I think we have a nested tail strategy tail that tries lots of things in combination. It would be good to add aligned splits to it to get more coverage of this.

[mcourteaux]

I have two tests added: split_aligned_nested and rfactor_split_aligned_nested which do this. I'm a bit hesitant to conflate the existing nested_tail_strategies with another axis of tests.

[abadams]

The variant of this where c1 % c0 == 0 should be added too, for uniformity with the pair of rules above

[mcourteaux]

Adding this trips up nested_tail_strategies. It rewrites some bounds Expr that used to cancel into a form that no longer cancels. Precisely the opposite of what the new rule here tries to work around.

The rule we added here was very ad-hoc to make the +offset and up in the back to let the simplifier peel. As the c1 % c0 == 0 counterpart rule breaks things for now, and we are pushing back deciding what to do with this more general simplifier problem, I'd argue to just leave this rule alone without the counterpart you suggest.

I can add a comment about it though.

Note that none of the 3 rules in this block adhere to the reduction order, according to the verifier, but do according to your "constant becomes smaller" rule. This is probably something that needs to be addressed properly in the verifier, or these rules should be kicked out.

[abadams]

I think this should simplify by a different chain. First:
(0 - x % 2) / 2 is just (0 - x % 2), and then we have the pattern (0 - y) * 2 + y which I think will simplify already.

[mcourteaux]

Neither of these rules are present in the respective files. Will add those.

[mcourteaux]

Adding in the first rules brings the simplifier to: ((x % 2)*-1) which seems like a suboptimal endpoint, so I added rewrite(x * -1, 0 - x) in Simplify_Mul to have it land on (0 - (x % 2)). Does that sound right?

[abadams]

This seems like a hyper-specific rule. What's it for? Is this a pattern produced by the new split logic?

[mcourteaux]

Yes, it's hyper specific indeed. Disabling breaks one of the tests (correctness_aligned_split_mux_phase). Verified by z3 and the verifier.

[abadams]

Many comments on the simplifier rules. Were they all verified?

[mcourteaux]

I'll delete all the simplifier rules, and see what breaks, because I don't know anymore by now.

[alexreinking]

Until we fix matching in general, this needs to be

Suggested change

	rewrite(x * -1, 0 - x) ||
	rewrite(x * c0, 0 - x, c0 + 1 == 0) ||

[alexreinking]

Claude Opus 5.5 found a bug here while mechanizing the splits system I'm working on in Lean.

// Minimal reproducer: aligned_split + TailStrategy::ShiftInwardsAndBlend on an
// update definition skips required points when the required extent n is less
// than the split factor k and the anchor is not congruent to the min (mod k).
//
// Expected: every element of out is 1.
// Actual (k = 8, anchor = 0, out over [5, 10]): 1 0 0 1 1 1

#include "Halide.h"
#include <cstdio>

using namespace Halide;

int main(int argc, char **argv) {
    Var x("x"), xo("xo"), xi("xi");
    Func f("f"), out("out");

    f(x) = 0;
    f(x) = f(x) + 1;
    out(x) = f(x);

    f.compute_root();
    f.update().aligned_split(x, xo, xi, 8, 0, TailStrategy::ShiftInwardsAndBlend);

    Buffer<int> result(6);
    result.set_min(5);  // required region of f is [5, 10]: straddles the anchor-0 grid line at 8
    out.realize(result);

    int errors = 0;
    for (int i = result.min(0); i < result.min(0) + result.extent(0); i++) {
        printf("out(%d) = %d\n", i, result(i));
        if (result(i) != 1) {
            errors++;
        }
    }
    if (errors) {
        printf("FAIL: %d element(s) were never updated\n", errors);
        return 1;
    }
    printf("Success!\n");
    return 0;
}

---

Its explanation:

Why it fails. The required region is [5, 10], so n = 6 < k = 8, and it crosses the anchor-0 grid line at 8.

• Both tiles, for cells [0,7] and [8,15], get clamped to the same base, 3. Each one covers [3,10].
• Tile 0 uses  mask_low  ( xi < k − (m − a − j·k) , so  xi < 3 ) and keeps only 3, 4, 5.
• Tile 1 uses  mask_high  ( xi ≥ j·k − (M+1−k−a) , so  xi ≥ 5 ) and keeps only 8, 9, 10.
• Nobody writes 6 and 7.

The masks come from  main , where at most one tile is ever clamped per side. With anchoring and n < k, the two clamped tiles are the same tile.

When it fails. Exactly when n < k and a ≢ m (mod k). The sweep found 1862 bad configurations out of 6080, and that is exactly this set. The unaligned split and the other aligned strategies (RoundUpAndBlend, GuardWithIf, RoundUp) had no failures.

Suggested fix. Mask each tile to its own anchored cell: keep  xi  when  0 ≤ xi + (base − (a + j·k)) < k . Here that keeps 3–7 in tile 0 and 8–10 in tile 1.