@@ -319,9 +319,14 @@ Each target gets one exact option. If its intent has an exact mergeable
 accumulator (Count, Sum, Min, Max, Rate, IRate, Increase; avg via exact sum and
 count accumulator states) and the accumulator can be built, the exact option is
 **exact accumulator state**: a `SummaryAgg` with an exact family →
-`FinalizeExactAccumulator`. Otherwise, for example when a filter or HAVING
-prevents the accumulator or the intent has none, it is the plain exact
-computation. Whether the accumulator is materialized is decided in Stage 2.
+`FinalizeExactAccumulator`. Otherwise, when the intent has no exact
+accumulator or it cannot be built (for example avg over a nullable input), it
+is the plain exact computation. A filter or HAVING does not prevent the
+accumulator or summary candidates: a per-measure filter goes into
+`SummaryAgg.filter`, a HAVING that reads only group keys is pushed below the
+aggregate as a row predicate, and a HAVING that reads aggregate values is a
+`Filter` above the output, with `guarantee = None` for approximate
+candidates. Whether the accumulator is materialized is decided in Stage 2.
 
 Each candidate records its input expression, filter, grouping, window,
 supported estimates and accuracy requirement. Pass 2 uses these to decide
@@ -400,7 +405,7 @@ flowchart LR
   subgraph R2["Replacements(s₂)"]
     direction TB
     d3["Exact Sum accumulator<br/>per job"]:::exact
-    a2["summary candidates<br/>✗ pruned: cannot be exact"]:::pruned
+    a2["no summary candidates:<br/>Sum has no summary family"]:::exact
   end
   subgraph R3["Replacements(s₃)"]
     direction TB
 
@@ -8,8 +8,11 @@ ASAP optimization in [planner layering](../design_docs/proposals/planner-layerin
 inventory containing the original named roots and one `LocalLogicalTarget` per
 eligible aggregate measure. Discovery includes operator producers read by
 scalar roots and expressions. Pointer identity prevents repeated discovery of one
-shared producer. Inputs with assigned execution timing or ASAP operators are
-rejected: the input `LogicalDAG` contains no ASAP summary choices.
+shared producer. Inputs with assigned execution timing or materialization, or
+with ASAP operators, are rejected: the input `LogicalDAG` contains no ASAP
+summary choices or physical annotations. An approximate accuracy requirement
+needs epsilon and delta in (0, 1); otherwise enumeration fails with
+`InvalidAccuracy`, naming the root and measure.
 
 ## Eligibility
 
@@ -43,16 +46,22 @@ the target keeps every candidate and records how the predicate is applied:
 
 - A measure's own filter is recorded as `LocalLogicalTarget.filter`; only
   rows that pass it update the state (`SummaryAgg.filter`).
-- `HAVING` is recorded as `LocalLogicalTarget.having`. The SQL frontend lowers
-  `HAVING` to a `Filter` directly above the aggregate, so that `Filter` counts,
-  as does the aggregate's own `having`. A predicate that reads only `by(...)`
-  group keys is `HavingPlacement::BelowAggregate`: it is pushed below the
-  aggregate as a row predicate, like a measure filter. A predicate that reads
-  aggregate values is `HavingPlacement::AboveOutput`: it stays a `Filter`
-  above the finalize/estimate output, and approximate candidates of the
-  target carry `guarantee = None`, since membership near the threshold may
-  change. When several such filters read one shared aggregate,
-  `AboveOutput` wins.
+- `HAVING` is recorded as `LocalLogicalTarget.having`, one `HavingEntry`
+  (consumer `Filter`, predicate, placement) each. Only the adjacent form is
+  recorded for push-down: the aggregate's own `having` (an entry with no
+  `Filter`) and a `Filter` directly above the aggregate, which is how the SQL
+  frontend lowers `HAVING`. A predicate that reads only `by(...)` group keys
+  is `HavingPlacement::BelowAggregate`: it is pushed below the aggregate as a
+  row predicate, like a measure filter. A consumer `Filter`'s predicate is
+  pushed below only when every consumer of the aggregate applies the same
+  predicate; otherwise another consumer would lose rows. Any other `HAVING`,
+  and every `HAVING` of a global aggregate (no group keys, so its one output
+  row exists even with no input rows), is `HavingPlacement::AboveOutput`: it
+  stays a `Filter` above the finalize/estimate output, and approximate
+  candidates of the target carry `guarantee = None`, since membership near
+  the threshold may change. A value predicate anywhere above an approximate
+  output, adjacent or not, gets `guarantee = None` through guarantee
+  propagation (#575); multi-level push-down is tracked in #664.
 
 For example, an approximate single-column distinct count offers exact execution,
 HLL, Theta, KMV and UnivMon; an approximate `count` offers its exact `Count`
@@ -75,6 +84,10 @@ the target's one exact option.
 Distinct-tuple counts do not acquire single-value UnivMon alternatives; that
 family is not declared for them, so it is not a pruned candidate.
 
+TopK offers its per-group heap summaries (`CmsWithHeap`,
+`CountSketchWithHeap`). The grouping-level Hydra candidate ("over all groups")
+is not generated in Pass 1 here; it is added in #605.
+
 ## Scope
 
 The API accepts no empirical cost or accuracy model, runtime capabilities, storage