UnivMon: certify L2 from layer 0's F2

[zzylol]

Stack: #574 → #620 → #618 → #621 → #627 → #625 → #628 → #632 → #634 → #616 → #617 → #622 → #624 → #629 → #630 → #631 → #633 → #635 → #636 → #637

Problem

Stage 3 rejected every UnivMon candidate ("no accuracy model for UnivMon"). The only certified readout was the exact total. The kernel read L2 via calc_l2, the square root of the heavy-hitter G-sum heuristic, and no theory covers that readout. UnivMon's shape was a fixed 5×1024×16 whatever the requirement, and Stage 3 priced it through the catch-all (1, 1_024).

Changes

• Executor: FrequencyL2 now reads l2_sketch_layers[0].get_l2(). That is √(median over rows of Σ C²) on layer 0, which sees the whole stream. It is the textbook AMS F₂ estimator and is linear under merge. No sketchlib change.
• Guarantee (estimators/univmon.rs): FrequencyL2 is now certified.
  • Per row, Chebyshev with p = 0.1 gives ε₂ = √(20/w), since Var[R] ≤ 2F₂²/w.
  • The median of d odd rows fails with probability at most the binomial tail Σ_{i≥(d+1)/2} C(d,i)pⁱ(1−p)^(d−i).
  • The L2 bound is 1 − √(1 − ε₂), the lower side. The upper side √(1+ε₂) − 1 is smaller.
  • Reported as RelativeValue under contract univmon_layer0_f2_median_chebyshev_v1. The contract records the idealized 128-bit-hash assumption, p and the readout.
  • Fails closed (None) unless d is odd, w is a power of two and d·log₂w + d ≤ 128. sketchlib slices each row's column and sign from one 128-bit hash, so outside these conditions the rows are not independent.
  • Distinct count and entropy stay uncertified. The total stays exact.
• Sizing: depends only on (ε, δ), not on the intent, so Pass 2's capability sharing still gives identical states.
  • d is the smallest odd depth whose tail is ≤ δ, capped at 19 because the executor's kernel rejects more than 20 rows.
  • w is the next power of two ≥ 20/(2ε−ε²)².
  • Heap stays 256 and layers stay 16.
  • Shapes past the bit budget are kept, and the guarantee rejects them. For example (0.01, 0.001) gives 9×2¹⁶ and is rejected.
  • With no positive ε (the exact-count alternative, which reads only the exact total) the old 5×1024 baseline is kept.
• Stage 3 pricing: summary_shape gets a UnivMon arm. Ops per row are 2·(2d + 4), since an insert reaches about 2 layers. State bytes come from Pass 1's sketch_state_bytes.
• Tests:
  • univmon.rs units: L2 certified at (0.01, 0.01) with RelativeValue; even d, non-power-of-two w and bit-budget overflow give None; tighter ε/δ give more columns/rows; F0 and entropy stay None.
  • Executor: the readout equals layer-0 get_l2, and on a Zipf(1) stream at the (0.01, 0.01) sizing it is within 1% of the true L2.
  • plan-selection: Example 2's Q3 UnivMon passes build_violation, while Q1 and Q2 still fail with "no accuracy model".
• Tests changed by side effects of this PR:
  • frontend-promql/tests/univmon_candidates.rs: count now uses the same ε as the other three readouts, so all four share one shape. L2 is now expected to be certified, and the "uncalibrated" test covers entropy only.
  • integration-tests/tests/precompute_raw_samples.rs: raises this test's executor max_bytes to 1 GiB. A UnivMon sized at ε = 0.02 is about 10 MiB per population (16 layers × 5 × 2¹⁴ × 8 B), so five series exceed the default 64 MiB.
  • planner/tests/summary_sharing.rs (stage-pipeline sharing test): with synthetic evidence, the plan whose three estimates read one UnivMon build is valid. It is no longer selected, because the new pricing (28 updates/row) costs more than exact counting. The test now asserts that the valid shared candidate exists.
• Docs: accuracy-models.md table row and univmon-frequency-summary.md updated. Doc comments updated in devtools/tests/stage_pipeline.rs and summary_sharing.rs.

Example 2 (stage_pipeline --example planner-layering-2):

• Before and after, the selection is the same: P86 "Q1 exact · Q2 exact (Count acc) · Q3 exact (Count acc) · shared summary", at 0.02367 cost/s.
• Valid candidates go from 8 to 16. The 8 new ones use UnivMon for Q3.
• The cheapest UnivMon plan is P88, "Q1 exact · Q2 exact (Count acc) · Q3 UnivMon (Count acc) · shared summary", at 0.06867 cost/s.
• tools/dag-viewer/examples/planner-layering-example1.json is unchanged (the fixture test passes).
• fix: integrate with fix(pass1): offer no per-group sketch for SQL COUNT(*) #620: fix(pass1): offer no per-group sketch for SQL COUNT(*) #620 requires every priced Stage 3 candidate to bind. With L2 certified, Example 2's UnivMon over src_ip (a unit-weight item update) is now priced, but the executor's physical planner sent it to the keyed weighted-frequency build, which has no UnivMon kernel. It now binds as UnivMon's value-frequency build over the item column, which already counts typed SQL identities (priced_example2_candidates_bind).

Test plan

• cargo fmt --all --check
• cargo clippy --workspace --all-targets -- -D warnings
• cargo test --workspace: 1677 passed, 0 failed, 21 ignored (re-run after the rebase on main d4869a7)

🤖 Generated with Claude Code