[zzylol]

Why

Stage 3 could not use a UnivMon for anything but the exact total. Its L2 and distinct-count readouts had no guarantee, and its shape was a fixed 256 / 5×1024 / 16 layers whatever the target. Upstream asap_sketchlib now has estimators with provable bounds: #221 (unbiased calc_card, calc_l2 read directly from layer 0, top_layer_complete(), get_l2_sqr()) and #220 (a shape whose hashes are not independent is rejected at construction; at most 19 layers). This PR moves the pin to them and certifies the two readouts in the planner. This is G5 step 2, done ahead of G5.

What

• Pin. Neither upstream PR is merged yet. As the user instructed, the planner does not wait for them:
  • The workspace pins 831a504 (branch planner-pin/univmon-certifiable), which merges QueryExpr has duplicate relational/scalar-language shapes for the same semantics (Scalar/Literal, BinaryOp/Compare/Arith) #220 into feat: rewrite uniqExact to COUNT(DISTINCT ...) #221.
  • The executor needs the Float64 weighted frequency kernels. Those are in upstream controller-OMP #160, also unmerged, and 831a504 lacks them. The executor therefore pins e6b0314 (branch planner-pin/univmon-certifiable-weighted-frequency), a clean merge of controller-OMP #160's 5f03ccb into 831a504. Its UnivMon readouts now use the same estimators the planner certifies.
  • Both pins move to upstream main once those PRs merge.
• L2 (RelativeValue) is certified from layer 0's direct estimate.
• Distinct count (Cardinality) is certified with the rigorous Chebyshev bound, given the source's distinct bound.
• Entropy stays uncertified, and the total stays exact.
• Sizing. UnivMon is now sized per readout from (ε, δ).
• CountSketch. Its failure probability is now the exact binomial tail instead of exp(−depth/18).
• Executor. It rejects shapes past the hash budget with an error instead of a library panic.

How

L2. Each row of layer 0 estimates F2 with Var ≤ 2q·F2², where q is the chance two keys share a column.

• q = 1/w for a power-of-two width. Otherwise q ≤ 9/(8w), because columns are hash slices taken modulo w.
• The guarantee fixes the per-row failure probability 2q/ε₂² at 0.1, so a shape states one (ε, δ):
  • the columns give ε₂ = √(20q);
  • the rows give δ = P(Bin(r, 0.1) ≥ ⌈r/2⌉), summed exactly;
  • the norm's error is 1 − √(1 − ε₂).
• Sizing takes the smallest r meeting δ, then the smallest width meeting ε. That width may or may not be a power of two, whichever is smaller.
• The shape uses one layer and a one-key heap, because L2 reads only layer 0.
• Shapes are clamped to r·(⌈log2 w⌉ + 1) ≤ 128 and r ≤ 19. A target past that gets the largest shape that can be built, and its guarantee then misses the target.

Distinct count. The estimator is unbiased with Var ≤ 1.35·F0²/k for k ≥ 8 once the top layer is complete.

• The library proves 1.35 and also states the looser 2. This PR uses 1.35.
• The top layer is incomplete with probability at most (e/4)^(k/2) when layers ≥ ⌈log2(F0_max/k)⌉ + 2.
• Sizing takes the smallest k with 1.35/(kε²) + (e/4)^(k/2) ≤ δ and records δ in a new optional SketchParams::UnivMon.distinct_failure_probability. Like KLL's failure_probability, it is ignored by equality and omitted from JSON when None.
• Stage 1 never reads the data workload, so it keeps the maximum of 19 layers.
• For a distinct count over a source's own rows, the guarantee is ε = √(1.35/(k·δ_c)), where δ_c = δ − (e/4)^(k/2). Its failure probability is UnionBound[δ_c, univmon_incomplete_top_layer_probability[k=…,layers=…](max_distinct[source])].
• Stage 3 binds that statistic from feat(planner): HLL confidence from a deployment distinct-count bound (#678) #693's max_distinct_per_evaluation:
  • 0 when F0_max ≤ k;
  • (e/4)^(k/2) when F0_max ≤ k·2^(layers−2);
  • 1 otherwise.
  • When the bound is missing, the statistic stays unknown and the target is unmet.
• The Count Sketch inside a distinct-sized UnivMon is a single counter per layer. The bound holds whatever the Count Sketch keeps in the heaps.

CountSketch. A row fails with probability q·w/3: 1/3 for a power-of-two width and 3/8 otherwise. exp(−depth/18) assumed 1/3, so it understated δ for every non-power-of-two width. The guarantee now uses P(Bin(d, p) ≥ (d+1)/2), and count_sketch_depth(width, δ) takes the smallest odd depth meeting it.

Not certified:

• Entropy. I found no sound data-dependent bound for the heap-recursion estimator: upstream documents none, and Monte Carlo checks none. It stays uncertified rather than resting on an invented bound.
• Terminal-mode distinct counts and OctoSketch aggregators fed promoted deltas. The executor rejects terminal-mode states.

Key code interfaces added / modified

crates/types/src/post_asap/sketch.rs, family_capability.rs

/// Concrete parameters of one sketch instance; the variant must match its
/// `SketchAlgorithm`. Equality compares the built shape, not the sizing targets.
/// The type stays; UnivMon gains one field.
pub enum SketchParams {
    /// A UnivMon's shape: a heap per layer over a Count Sketch per layer.
    UnivMon {
        /// Keys each layer's heavy-hitter heap holds.
        heap_size: u32,   // unchanged
        /// Rows of each layer's Count Sketch.
        sketch_rows: u32,   // unchanged
        /// Columns of each layer's Count Sketch.
        sketch_cols: u32,   // unchanged
        /// Number of layers (at most 19 for independent hashes).
        layers: u8,   // unchanged
        /// The failure probability the heap was sized for when this UnivMon answers a
        /// distinct count; `None`: not sized for one, which then has no guarantee.
        /// Ignored by equality; omitted from JSON when `None`.
        #[serde(default, skip_serializing_if = "Option::is_none")]
        distinct_failure_probability: Option<f64>,   // new
    },
    /// A KLL quantile sketch: `k` and the failure probability `k` was sized for
    /// (`None`: the empirical 99% calibration; ignored by equality).
    Kll { k: u32, failure_probability: Option<f64> },   // unchanged
    /// A Count-Min sketch of `depth` rows by `width` columns.
    Cms { width: u32, depth: u32 },   // unchanged
    /// A HyperLogLog with `2^precision` registers.
    Hll { precision: u8 },   // unchanged
    /// A DDSketch with relative accuracy `alpha`.
    DDSketch { alpha: f64 },   // unchanged
    /// A Count-Min sketch with a top-k heap of `heap_size` keys.
    CmsWithHeap { width: u32, depth: u32, heap_size: u32 },   // unchanged
    /// A KMV sketch keeping the `k` smallest hashes.
    Kmv { k: u32 },   // unchanged
    /// A Theta sketch with nominal size `k`.
    Theta { k: u32 },   // unchanged
    /// A Count Sketch of `depth` rows by `width` columns.
    CountSketch { width: u32, depth: u32 },   // unchanged
    /// A Count Sketch with a top-k heap of `heap_size` keys.
    CountSketchWithHeap { width: u32, depth: u32, heap_size: u32 },   // unchanged
}

impl FamilyCapability {
    /// The capability of `family`; UnivMon now merges with the guarantee of one
    /// build over the union, except heap readouts.
    pub fn of(family: &FieldDataType) -> Self;   // UnivMon: with_heaps(MergedError::SameAsUnionBuild), was with_heaps(MergedError::Approximate)
    /// The merged error of `readout`; entropy and top-k from a heap family are
    /// approximate, other readouts take the family's `error`.
    pub fn merged_error(&self, readout: &SketchStatistic) -> Option<MergedError>;  // heap_readouts now apply to FrequencyEntropy and TopK only (Cardinality removed)
}

crates/asap-aware-mapping/src/accuracy/estimators/univmon.rs

/// Layers `asap_sketchlib` builds with independent hashes.
pub(crate) const MAX_LAYERS: u8 = 19;   // new; shared with the cost model

/// UnivMon's guarantee for `query`: exact for the unit-update total, certified
/// L2 for a hash-independent shape; `None` otherwise (distinct count goes via `distinct_guarantee`).
pub(super) fn guarantee(
    algorithm: &SketchAlgorithm,
    params: &SketchParams,
    query: &SketchStatistic,
) -> Option<AccuracyGuarantee>;   // was guarantee(query); certifies L2 from the shape
/// Sizes a UnivMon for one readout's `(eps, delta)`: L2 and distinct count get
/// the smallest shape meeting the target; total and entropy get a baseline.
pub(super) fn size_params(intent: &AggIntent, eps: f64, delta: f64) -> SketchParams;  // was size_params(), a fixed baseline

/// Whether `asap_sketchlib` builds this shape with independent hashes; the
/// bounds and the evidence check both require it.
pub(crate) fn hash_independent(rows: u32, cols: u32, layers: u8) -> bool;   // new: rows · (⌈log2 cols⌉ + 1) ≤ 128, layers ≤ 19

// new: "univmon_incomplete_top_layer_probability[k=…,layers=…](max_distinct[source])", bound by Stage 3
/// The statistic name a distinct count over `source` leaves its top-layer
/// failure probability as, for Stage 3 to bind.
pub(crate) fn incomplete_top_layer_statistic(heap_size: u32, layers: u8, source: &str) -> String;
/// The heap, layers and source such a statistic names; `None` for any other string.
pub(crate) fn parse_incomplete_top_layer_statistic(statistic: &str) -> Option<(u32, u8, &str)>;
/// That probability given the source's distinct bound: 0 when it fits the heap,
/// `(e/4)^(k/2)` when the pyramid is deep enough, else 1 (no certificate).
pub(crate) fn incomplete_top_layer_probability(heap_size: u32, layers: u8, max_distinct: u64) -> f64;
/// A distinct count's guarantee over `source`'s own rows; `None` for a shape not
/// sized for a distinct count, a heap under 8, or one the library would not build.
pub(crate) fn distinct_guarantee(params: &SketchParams, source: &str) -> Option<AccuracyGuarantee>;  // new

crates/asap-aware-mapping/src/accuracy/estimators/count_sketch.rs, mod.rs

/// The smallest positive odd depth whose binomial median failure probability
/// at `width` is at most `delta`, capped at 255.
pub(crate) fn count_sketch_depth(width: u32, delta: f64) -> u32;   // was count_sketch_depth(delta); smallest odd depth meeting the binomial tail
// contract renamed: "count_sketch_l2_median_hoeffding_v1" -> "count_sketch_l2_median_binomial_v1"

/// `P(Binomial(n, p) ≥ k)`
/// Rounded up slightly so rounding never certifies a smaller tail.
pub(crate) fn binomial_upper_tail(n: u32, p: f64, k: u32) -> f64;   // new
/// `P(c_i = c_j)` for two keys in one Count Sketch row of `cols` columns, as
/// `asap_sketchlib` hashes them.
pub(crate) fn column_collision(cols: u32) -> f64;                    // new: at most 9/(8 cols) off powers of two

crates/asap-aware-mapping/src/per_computation_candidates.rs, empirical_cost.rs

/// The guarantee of a per-group distinct count (classic HLL or UnivMon) over a
/// source's own rows; `None` for other summaries or computed rows.
fn source_distinct_guarantee(
    family: &FieldDataType,
    query: &SketchStatistic,
    input: &Rc<OperatorNode>,
) -> Option<AccuracyGuarantee>;   // renamed from classic_hll_guarantee; also covers UnivMon distinct counts

/// Whether a sketch's parameters are valid for offline evidence; a UnivMon
/// needs a non-empty heap and a hash-independent shape.
fn valid_params(algorithm: &SketchAlgorithm, params: &SketchParams) -> bool;   // UnivMon evidence uses hash_independent (was layers 1..=64)

crates/asap-physical-operators/src/summary_kernels/univmon.rs, capability.rs

/// Rejects more than MAX_LAYER_SIZE (19) layers, or rows · (⌈log2 cols⌉ + 1) > 128.
/// Executor-side shape check for a UnivMon, so invalid shapes are kernel
/// errors (bad input) rather than library panics.
pub(crate) fn check_dimensions(
    heap_size: usize,
    rows: usize,
    cols: usize,
    layers: usize,
) -> Result<(), Error>;   // was private; validate_summary_kernel now calls it, so these shapes are errors instead of library panics

Cargo.toml, crates/asap-physical-operators/Cargo.toml

# Cargo.toml: the planner pins the certifiable UnivMon branch
asap_sketchlib = { git = "https://github.com/ProjectASAP/asap_sketchlib", rev = "831a5045847010a3a65f5a8e614e0208581d4a05" }
# crates/asap-physical-operators/Cargo.toml: was rev 5f03ccb; adds the weighted frequency kernels
asap_sketchlib = { git = "https://github.com/ProjectASAP/asap_sketchlib", rev = "e6b03142628a3109b6482ebe8512bff7e75f5b35" }

Usage, end to end (numbers from running the stages at this PR's merge commit b788fc52, Example 2's Q1 alone):

// 1. What the user writes: the number of distinct source IPs in the last minute, every 10 s,
//    within relative error ε = 0.02 with failure probability δ = 0.01. `q1` is the workload
//    entry; Stage 1 sizes summaries from its (ε, δ) and Stage 3 checks the result against it.
let q1 = RepeatingEntry {
    query: Query("distinct_over_time(flows_src_ip[1m])".into()),
    demand: RepeatedDemand::FixedInterval(RepetitionInterval(10_000)),
    requirements: QueryRequirements {
        accuracy: AccuracyRequirement::Explicit(AccuracyTarget::EpsilonDelta { epsilon: 0.02, delta: 0.01 }),
        response_latency: LatencyRequirement::Unspecified,
    },
    predictability: Predictability::Predictable { known_at: None },   // a dashboard panel, known ahead
    time_selection: TimeSelection {                                    // real time, over the last minute
        scope: QueryTimeScope::RealTime,
        lookback: Some(DurationMs(60_000)),
        as_of: None,
    },
};

// 2. What the deployment declares: at most 10M distinct values of `flows_src_ip` per evaluation
//    (#693's bound). `data` is the data workload; only Stage 3 reads this bound.
let data = DataWorkload {
    max_distinct_per_evaluation: declared(BTreeMap::from([("flows_src_ip".into(), 10_000_000)])),
    arrival: DataArrival::ContinuouslyIngesting,                     // a live flow stream
    data_ingestion_interval: declared(DurationMs(15_000)),           // PromQL source cadence
    ingestion_volume: Evidence::default(),                           // unknown
    ingestion_rate: declared(Rate(1_000_000.0 / 15.0)),              // rows per second, for the cost model
    input_cardinality: declared(10_000_000),                         // 10M source IPs, for the cost model
    distribution: declared(DataDistribution::Zipf),                  // value skew, for the cost model
    stream_norms: Evidence::default(),                               // none; no Count-Min/Count Sketch here
    metric_types: BTreeMap::new(),                                   // no declared metric types
};

// 3. `workload` is the planner input; `run` holds every stage's output (what stage_pipeline runs).
let workload = PlanningWorkload {
    query_workload: QueryWorkload { language: QueryLanguage::PromQL, query_batch: None, repeating_queries: Some(vec![q1]) },
    data_workload: Some(data),
};
let run = run_planning_stages(&workload, lower_promql_roots(&workload)?, None)?;

// 4. Stage 1 (stage1_logical_asap_optimization) offers L1 exact, L2 HLL, L3 KMV and L4 UnivMon.
//    For L4 it calls univmon::size_params(&AggIntent::Cardinality { .. }, 0.02, 0.01): the smallest
//    k with 1.35/(k·0.02²) + (e/4)^(k/2) ≤ 0.01, with 19 layers since Stage 1 does not read the bound:
//      UnivMon { heap_size: 337500, sketch_rows: 1, sketch_cols: 1, layers: 19, distinct_failure_probability: Some(0.01) }
//    univmon::distinct_guarantee(&params, "flows_src_ip") gives relative error 0.02 and a failure
//    probability with one term left symbolic in the source's bound
//    (incomplete_top_layer_statistic(337500, 19, "flows_src_ip")):
//      UnionBound [0.01, "univmon_incomplete_top_layer_probability[k=337500,layers=19](max_distinct[flows_src_ip])"]

// 5. Stage 3 (stage3_plan_selection) binds that term: parse_incomplete_top_layer_statistic gives
//    (337500, 19, "flows_src_ip"); incomplete_top_layer_probability(337500, 19, 10_000_000) is
//    (e/4)^(337500/2) ≈ 0, since 10M ≤ k·2^(19−2). The total is 0.01 ≤ δ, so P4 is valid.

// 6. What the user gets back in `run.stage3_plan_selection`:
//    selected: "P1" (exact, 2.88 cost/s; exact is cheapest here)
//    P3 KMV k = 250,002: valid, 3.28 cost/s
//    P4 UnivMon (heap 337,500, 1×1, 19 layers): valid, 4.48 cost/s
//    P2 HLL precision 12: rejected, "failure probability Some(1.0)": 10M is past classic HLL's range
//    Without the bound, P4 is rejected too: "q1: the output guarantees bound Some(0.02),
//    failure probability None, which misses target EpsilonDelta { epsilon: 0.02, delta: 0.01 }".

Before this PR

• Every UnivMon readout except the total had no guarantee. Stage 3 rejected those candidates.
• Every UnivMon had the fixed 256 / 5×1024 / 16 shape.
• The executor's L2 ran the heap recursion with g = x².
• The executor's distinct count dropped heap keys with non-positive estimates, which biased it low.
• A shape past the 128-bit hash budget or above 19 layers was built silently.
• CountSketch's δ was understated for non-power-of-two widths.

After this PR

Example 2 (PromQL stand-in; Q1 distinct (0.02, 0.01), Q2 entropy (0.05, 0.01), Q3 L2 (0.01, 0.01)):

	Q1 distinct UnivMon	Q3 L2 UnivMon
shape	heap 337,500, 1×1, 19 layers	heap 1, 5 × 56,817, 1 layer
no distinct bound	unmet (failure probability unknown)	certified
bound 9	certified (top layer always complete)	certified
bound 10M	certified (7 layers suffice; classic HLL certifies nothing here)	certified
bound > 337,500·2¹⁷	unmet (19 layers too shallow)	certified

• Valid physical candidates: 12 without a bound, 24 with a bound of 9, and 18 with 10M.
• Stage 3 still selects all-exact, at 8.64 cost/s.
• The cheapest UnivMon plans:
  • UnivMon/exact/exact at 10.24 (needs a distinct bound);
  • exact/exact/UnivMon at 11.04.

Example 1: its CountSketch has a non-power-of-two width and now needs depth 149 instead of 125 for δ. The committed viewer fixture is regenerated.

Verification

• Unit tests (estimators/univmon.rs, count_sketch.rs):
  • for each of six (ε, δ) targets, the sized L2 shape and distinct heap meet their target, and one fewer row, column or heap key does not;
  • the L2 error uses the 9/(8w) collision bound off powers of two;
  • the failure probabilities equal hand-computed binomial tails;
  • shapes past the hash budget or 19 layers certify nothing, and sizing never builds them;
  • the distinct count is unmet without a bound and unmet past the layers;
  • the statistic round-trips;
  • the total is exact and entropy is uncertified;
  • CountSketch depths are the smallest meeting the binomial tail.
• Executor: rejects_shapes_past_the_hash_budget. It failed (a library panic) before the fix.
• Example 2 (planner_layering_example2.rs):
  • new: stage3_plan_selection_accepts_univmon_distinct_given_a_distinct_bound, stage3_plan_selection_rejects_univmon_distinct_past_its_layers and stage3_plan_selection_accepts_univmon_l2;
  • un-ignored: stage1_logical_asap_optimization_univmon_is_sized_per_accuracy_target;
  • stage3_plan_selection_judges_univmon_with_an_accuracy_model stays ignored, since entropy has no model.
• Tests whose expectations were tied to the old behavior:
  • frontend-promql/tests/univmon_candidates.rs: the four readouts no longer share one state, because each is sized for itself. The total and entropy keep the baseline shape and still share it. Sharing across readouts is G5's summary-capability rule. L2 and the distinct count now carry guarantees, so the "uncalibrated" test covers entropy only.
  • replacement.rs (legacy search) cardinality tests: at ε ≈ 0.008 the distinct-sized UnivMon (a 2M-key heap on 19 layers, about 2.5 GB) exceeds the search's 512 MiB cap. These tests now use ε = 0.05.
  • tools/dag-viewer/examples/planner-layering-example1.json: CountSketch depth 125 → 149.
• With only the pin moved, the executor and integration tests passed unchanged, including the UnivMon adoption and readout tests. QueryExpr has duplicate relational/scalar-language shapes for the same semantics (Scalar/Literal, BinaryOp/Compare/Arith) #220 keeps the hashing of shapes that were already valid.
• Full gate on the rebased head, on the remote runner: cargo fmt --all -- --check, cargo clippy --workspace --all-targets --all-features --locked -- -D warnings and cargo nextest run --workspace on head c544d62: all pass, 1666 tests.

Limitations and follow-ups

• The pins point at unmerged upstream commits. Move them to upstream main once QueryExpr has duplicate relational/scalar-language shapes for the same semantics (Scalar/Literal, BinaryOp/Compare/Arith) #220, feat: rewrite uniqExact to COUNT(DISTINCT ...) #221 and controller-OMP #160 merge.
• Entropy has no certified bound. It needs an upstream derivation with Monte Carlo tests first.
• A distinct-sized UnivMon is large. At (0.02, 0.01) it keeps 19 heaps of 337,500 keys.
• A distinct-sized UnivMon always has 19 layers. Stage 3 could lower the layer count once F0_max is bound, but Stage 3 does not resize today.
• The L2 guarantee fixes the per-row failure at 0.1. Small δ therefore needs many rows, and the 128-bit budget then caps the width. For example, (0.01, 1e-6) is unreachable.
• distinct_failure_probability is ignored by equality, following KLL's precedent. G5's per-parameter merge must also take the minimum δ of a shared build. Because the guarantee is a point on a δ–ε curve, a shared UnivMon must be re-checked against each consumer.
• CountSketch keeps width ⌈3/ε²⌉. For targets with a small δ, a power-of-two width (p = 1/3) would need fewer rows.