[b-re-w]

Closes #148

Feature added:

• The verifier's intervals now come from more sources, and the front end produces the same facts:
  • guards (if x < e, while lo < hi, an early-returning guard), dropped on assignment and at loop back-edges;
  • each plain local's joined assignments, by a widening fixpoint;
  • // and % by constants, whose results are bounded;
  • the front end's len() bound now equals the verifier's 2**62.
• // and % by a power-of-two constant, applied to a proven non-negative value, emit a shift or mask.

Behaviour change: proven ADD, SUB, MUL and NEG are now emitted unchecked (tp_proven*). Before, they still called the checked helper plus a SystemError check.

• The verifier is the guard.
• As a safety net, the sanitizer CI job builds with -DTP_CHECK_PROVEN, which turns a wrong proof into a SystemError, and now also runs test_interval_proofs.py.
• SPEC N-9 has a row for this.

Defect fixed: x % 10 + 1 used to be proven by the front end but rejected by the verifier, so the whole function stayed interpreted.

Tests added: test_interval_proofs.py, 84 tests.

• IR-level accept and reject cases, plus end-to-end comparisons with CPython at 263-1 and -263.
• Red before the change: 41 failed. The 43 that passed are rejection-direction tests and the result comparisons, whose results were already correct.
• Mutations: 11 mutations of the analysis (skipped interval check, a guard surviving assignment, <= narrowed as <, no join, ...) all fail tests.

Tests changed (each where a fact changed):

• In test_verify: the mod/floordiv bounds test, the intervals-cannot-prove test, the wrong-node mutation, and a stale comment.
• In test_cgen: the generation test, the bad-proven case, and the lying-proof test (which now builds with -DTP_CHECK_PROVEN).
• In test_frontend: the i // 2 parameter became i // 3.
• In test_frontend_classes: binary-trees make is no longer may_deopt.

Checked ops in the benchmarks' C:

benchmark	before	after
fannkuch	sub 5, add 6, mod 1	sub 4, add 4, mod 0
binary-trees	sub 2, add 2	sub 0, add 2
spectral-norm	unchanged	unchanged
wordfreq	unchanged	unchanged

The remaining checks come from full-range function parameters and would need interprocedural facts.

Measured (quiet window, interleaved against develop, 11 pairs; benchmarks/typedpython/results/2026-10-17-interval-proofs-ab.json): fannkuch 0.997 (0.63 to 1.21), binary-trees 1.001 (0.75 to 1.20). No measurable speedup: the removed checks were well-predicted branches.

Verification (local, 3.15.0rc1t): full suite 1090 passed, 3 skipped. The compiled function sets of all five benchmarks equal develop's.