[REFACTOR] Share the Term to Z3 lowering between compiled clients

[mark14wu]

Summary

Moves the compiled sanitizer's Term → Z3 evaluator into a shared module, tilelens/ir/lowering.py: the one reading of the TTIR reader's term algebra as Z3 terms. The compiled race detector, which is being ported next, will build on the same semantics instead of a second copy. No user-visible change.

Stacked on #480 (base branch ir-mode), which is stacked on #479; review and merge those first.

What changes

• tilelens/ir/lowering.py (new) is mechanism only:
  • the operator semantics live here once: truncating // / %, unsigned ops and predicates read as their signed twins and IntCast as its operand (exact under the reader's width obligations, which the client discharges), i1 coercion, and LoopVar / IterArgOffset through the client's loop iteration;
  • every leaf (scalar arguments, program ids, grid, lanes, the loop iteration, atomic observations, unmodeled values) comes from the client's TermLeaves, which also raises the client's own refusals;
  • it never creates a Z3 context: constants use the leaves' context and every other term its operands', so the sanitizer keeps one context per check and the race detector can keep the main context its solver's pid renaming needs;
  • the walk is iterative and memoized by term identity, so terms deeper than the recursion limit lower.
• The compiled sanitizer (oob.py) runs on it. Its policy (overflow and division-by-zero findings, refusals, solving, timeouts) is unchanged. Two points worth a look:
  • the leaves reach the lowering through a weakref.proxy, and a refused loop keeps a never-raised copy of its refusal, so each check's Z3 context is freed when the check returns. A reference cycle would leave it to the cyclic GC on an arbitrary thread; concurrent checks hung or crashed that way in testing;
  • the sanitizer's own walks still stop at the induction variable, so a loop bound that is read only through a tl.where arm keeps that arm's guard.
• Hand-built graphs outside the reader's invariants (e.g. an iter arg naming another loop) now raise instead of being misread. The reader never produces them.

Evaluation

• Parity with the previous evaluator, every field compared (status, findings with their witnesses, refusals, abstentions):

  • Triton 3.6: 556 rows (64 golden TTIRs × 8 bindings) and 684 rows (10 bindings, including negative and wide scalars, missing scalars and an unknown grid), all identical;
  • Triton 3.8: 166 rows, all identical.

  A single-operator mutant of the lowering changes 47 of the 556 rows, so the comparison is sensitive.

• Differential corpus (223 kernels against Triton's interpreter): 0 false proofs and 0 false out-of-bounds findings on Triton 3.6 and 3.8. The results are byte-identical to [FEAT] Add a compiled mode to the sanitizer #480's, and so is every solver query's SMT-LIB text.

Testing

• New tests/unit/ir/test_lowering.py (52 tests): context ownership (no context created; main vs. given context), depth-5000 chains, operator semantics, and out-of-algebra terms.
• New sanitizer tests: a loop bound that wraps in a discarded tl.where arm (2 cases), and no Z3 object left to the cyclic GC (a check with a finding, and a check whose loop is refused).
• IR-mode affected set (IR layer, compiled sanitizer, conformance, host compile), CPU only: Triton 3.6 1277 passed / 31 skipped; Triton 3.8 1292 passed / 23 skipped.