chore(bb): pin the sparse masking generator to its machine-checked domain

[AztecBot]

Stacked onto #23224 — aligns the masking-poly generator with the machine-checked theorem (productionTailHalvingSparseMasking_of_staircase, shplemini_lean/ on the companion proof branch), which covers tail_halving_support exactly as implemented for every d ≥ 3 and every extent with N/2 < extent ≤ N, collision extents included.

Three changes:

1. sparse_masking_poly.hpp — pin the proven domain with BB_ASSERT_GTE(d, 3) and BB_ASSERT_GT(2 * extent, n), and cite the theorem in the generator comment. Any caller outside the proven range (e.g. a padded trace whose max_end_index drops to N/2 or below) now fails loudly instead of silently running an unproven configuration. The translator call site passes extent = N (always in domain); the Oink call site passes max_end_index, which minimal dyadic sizing keeps above N/2 — if CI trips this assert anywhere, that caller was outside the proof and we want to know.

2. SHPLEMINI_ZK_MASKING.md — add the machine-checked status section: the exceptional-E selection rule in the setup is unnecessary (the theorem covers the implemented de-dup/tail-fill generator for every extent), d ≥ 3 holds uniformly (Appendix B's saturated case is an instance of the main argument), and the lemma-by-lemma correspondence to the Lean theorem names is recorded so the note and the formalization cannot drift silently.

3. shplemini_zk_mask_rank.test.cpp — extend the conformance test to sweep the entire proven domain N/2 < extent ≤ N for each test dimension, pinning the staircase witness columns (top pair, level anchors, N/2, column 1) — including the collision extents E ∈ {B, B+2} where the generator de-duplicates and tail-fills.

---

Created by claudebox · group: slackbot