Propagate end-to-end accuracy guarantees for approximate-over-approximate plans

[zzylol]

Context

ASAPPlanner can structurally nest SummaryAgg nodes, but selected post-ASAP plans need machine-readable end-to-end error guarantees. Approximate parents must not consume approximate children unless their composed guarantee satisfies the callers existing AccuracyTarget`.

Accuracy legality and cost ranking are separate responsibilities.

Required planning pipeline

candidate generation
    -> guarantee propagation
    -> AccuracyTarget satisfaction check
    -> legal candidates only
    -> cost ranking/global selection

CostModel must not override accuracy legality.

Accuracy model and typed guarantees

The deployment-extensible AccuracyModel supplies local guarantees, propagates them through a CompositionOperator, and checks the result against AccuracyTarget. Guarantees retain typed metrics rather than reducing every error to an unqualified epsilon:

#[non_exhaustive]
enum ErrorMetric {
    AbsoluteValue,
    RelativeValue,
    Rank,
    Cardinality,
    Frequency,
    L2Frequency,
    TopKMembership,
}

struct ResultGuarantee {
    metric: ErrorMetric,
    bound: BoundExpr,
    failure_probability: ProbabilityExpr,
    provenance: Vec<GuaranteeSource>,
}

BoundExpr and ProbabilityExpr are serializable expression vocabularies. Provenance records selected parameters, child guarantees, composition steps, runtime observations, and unavailable statistics. Caller-visible guarantees belong on finalized/readout values; exact outputs have zero error.

Core propagation rules

The default model is conservative and fail-closed:

• Exact input contributes zero bound and zero failure probability.
• Compatible additive/Lipschitz errors compose bounds additively and probabilities by union bound.
• Supported non-negative relative errors compose as e_inner + e_outer + e_inner * e_outer.
• Exact sum over approximate values sums bounds; exact extrema take the maximum bound.
• Incompatible rank, cardinality, frequency, value, L2-frequency, and membership metrics require an explicit conversion rule.
• Unknown statistics remain unknown; unsupported compositions keep the raw/pre-ASAP alternative.

TopK membership requires widened per-key confidence intervals and is certified only when:

min_lower_bound(selected_top_k)
    > max_upper_bound(non_selected)

CountSketch uses an L2-frequency theorem and must never reuse CMS`s L1 theorem.

Accuracy-budget allocation

The full root epsilon/delta must not be allocated independently to every approximate layer. An AccuracyBudgetAllocator enumerates finite allocations; each allocation produces parameters through existing sizing, and candidates whose propagated guarantees miss the target are rejected before global selection.

Initial additive allocation may split epsilon and delta evenly across approximate layers. Root QueryRequirements.accuracy and explicitly supplied local AggIntent.accuracy must have documented precedence.

Cost model

Accuracy allocation changes state/update/read costs, but correctness filtering happens first. Recurring costs use explicit units and rates; shared state is counted once. One-shot plus recurring work requires an explicit horizon. Unknown statistics must not become zero.

Acceptance criteria

• Selected approximate-over-approximate plans carry machine-readable end-to-end guarantees.
• Guarantees are checked against the existing AccuracyTarget before costing.
• Unsupported/unprovable compositions retain the raw/pre-ASAP candidate.
• Compatible basic compositions use typed metrics and documented formulas.
• DAG export carries guarantees, probability, provenance, allocation, and rejection reasons.
• TopK membership requires a strict margin certificate.
• CountSketch uses L2-specific sizing and guarantee propagation.
• Hydra composes inner error with shared-grid error.
• KLL/HLL/KMV/Theta have conservative parameter-derived confidence contracts.
• Integrate concrete posterior/runtime observations without making them implicit planning assumptions.
• Reuse the same propagation primitives for all roll-up work in Support accuracy-aware approximate Count roll-ups #278.

PR #303 implementation status

PR #303 implements the four requested Planner-side guarantees. ASAPPlanner remains a mathematical planner and does not import asap_sketchlib; runtime observations are a separate evidence source that can instantiate symbolic terms later.

Completed in ASAPPlanner

• TopK membership-margin certificates: carry widened selected/excluded boundary intervals and their union-bound failure probability; certify only strict separation and reject missing, invalid, or overlapping evidence.
• CountSketch L2 sizing and propagation: add L2Frequency, sqrt(3 / width) * ||f||_2, epsilon-derived width, delta-derived odd median depth, and a conservative Hoeffding failure bound. CMS posterior L1 relaxation is not reused.
• Hydra shared-grid composition: add inner and outer collision bounds and union-bound their failure probabilities. Deployment/data-dependent leaves stay symbolic and fail closed until instantiated.
• KLL/HLL/KMV/Theta confidence: attach conservative 99%-confidence contracts to committed parameters; reject tighter unsupported confidence and targets missed because of parameter caps.
• Check parameter-derived guarantees against targets even for exact inputs, before cost ranking.
• Add unit/integration coverage and document the contracts.

Remaining evidence/runtime integration

• Feed runtime or planning-time TopK boundary intervals into PropagationStats; static candidates remain rejected without evidence.
• Instantiate CountSketch stream-L2 and Hydra shared-grid symbolic statistics from a serving implementation when concrete absolute bounds are required.
• Add an implementation-specific amplification/confidence model if confidence tighter than the built-in 99% contract is required.
• Preserve imported evidence as GuaranteeSource::RuntimeObservation and export it through DAG JSON.
• Keep affected candidates fail-closed when required evidence is unavailable.

Non-goals and related follow-up

• Do not add a second correctness-policy enum.
• Do not assume statistical independence by default.
• Do not claim arbitrary cross-sketch or nonlinear composition.
• Advanced nonlinear and correlation-aware error propagation #297 tracks nonlinear and correlation-aware propagation.
• Exact/archive fallback execution and runtime integration remain separate from Planner mathematics.