fix(planner): carry projections and early_limit into the physical plan - #207
Merged
Conversation
`PlanNode` has four fields; `PlanStep` had six, and neither `projections` nor
`early_limit` was among them. The optimizer computed both, then dropped them at
the logical -> physical boundary, so the executor never saw either pushdown.
That is worse than merely lossy, and this is the part worth flagging.
`CostModel::estimate` already *discounts* a node carrying an early limit
(`cost.rs:345-350`):
if let Some(limit) = node.early_limit {
let limit_factor = (limit as f64 / 1000.0).min(1.0);
selectivity *= limit_factor;
time_ms *= 0.5 + 0.5 * limit_factor; // At least 50% of base cost
}
So a plan was priced as cheap as half its base cost *because of* a limit
pushdown that the physical plan had no way to perform. The planner was
rewarding an optimisation it then discarded. Nothing failed loudly — plans
simply cost less on paper than they cost to run, which is the kind of defect
that shows up as unexplained latency rather than as an error.
Measured before the change: `early_limit` had exactly one non-test read in the
entire tree — the cost adjustment above. `projections` had **none**; nothing
read it after `vcl_bridge.rs` built it.
Both fields are now on `PlanStep` and populated from the node. They carry
`#[serde(default)]`, so a `PhysicalPlan` serialised before this change still
deserialises (absent -> `vec![]` / `None`, matching the old behaviour rather
than inventing a limit).
This surfaced while discharging `optimize_is_permutation` (#206). The Coq model
abstracts a node as `(modality, list condition)` — precisely the projection that
omits the two fields being lost. The abstraction was not wrong, but it was drawn
around the bug, which is why proving the permutation property could not have
caught it.
Test: `test_pushdown_survives_optimization` asserts both fields survive, and
matches steps by modality rather than index — asserting on `steps[0]` would test
the sort order, not the pushdown. Verified as a real guard, not a vacuous one:
with the population reverted it fails with `projection pushdown was dropped at
the physical boundary`; with the fix it passes.
Verified: `cargo test -p verisim-planner` 118 passed / 0 failed; `cargo clippy
-p verisim-planner --all-targets` clean; `cargo check -p verisim-api
--all-targets` clean (it maps `PlanStep` into its own GraphQL type); `reuse
lint` compliant.
Not addressed here, and deliberately so: `pushed_predicates` remains
`Vec<String>` built by `format!("{:?}", c)`, so conditions still cross the
boundary as Rust `Debug` output rather than as `ConditionKind`. Retyping it is a
larger change with its own serialisation surface, and it is not needed to stop
the cost model lying.
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedCarries projections and early_limit into the physical plan to fix silent pushdown drops during the logical-to-physical translation. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
`cargo doc` is a required check and `[`CostModel::estimate`]` does not resolve from `plan.rs` — the type lives in the sibling `cost` module and is not in scope there, so rustdoc failed the workspace build with "unresolved link". Qualified to `crate::cost::CostModel::estimate`. Verified with the same command CI runs (`cargo doc --no-deps`), plus `cargo test -p verisim-planner` still green.
This was referenced Jul 29, 2026
hyperpolymath
added a commit
that referenced
this pull request
Jul 29, 2026
#209) test(planner): property-test the Rust image of optimize_is_permutation `formal/Planner.v` proves `optimize_is_permutation` about a *Coq* function. That says nothing about this crate until something checks the Rust against the same statement, and `Planner.v:23-28` has promised exactly that since the module was written: > A property test added alongside Provenance.v's chain-link integrity check > would exercise this in Rust. It was never added. This is that test, and it closes the refinement link #113 owes — the half that #206 could not supply, because discharging an axiom in Coq tells you nothing about the Rust it models. **The gap it closes.** `optimizer.rs` already has eight unit tests, but they assert *ordering* (`test_vector_before_graph`, `test_semantic_always_last`) and *counts*. None asserts the multiset — which is the actual content of the permutation property, and the only thing that catches a node being silently dropped, duplicated, or swapped for another. Four properties, stated over the same `(modality, list condition)` projection the Coq model uses so the two are comparable: * `prop_optimize_is_permutation` — multiset preserved. * `prop_optimize_total_cost_invariant` — permuting the input must not change the estimate, since that is what makes reordering a legitimate optimisation. Compared with a relative tolerance rather than `==`: f64 `+`/`*` are commutative but **not associative**, so `combine` is permutation-invariant only up to rounding. Same caveat recorded in `Planner.v`'s header. * `prop_optimize_never_panics` — guards the comparator. The tie-break is `partial_cmp(...).unwrap_or(Equal)` on f64, which a NaN makes non-transitive, violating `sort_by`'s contract and potentially panicking on Rust >= 1.81. NaN looks unreachable today (the only division in `CostModel::estimate` is guarded and feeds `selectivity`, not `time_ms`) but nothing in the types enforces it, so the belief is tested rather than asserted. * `prop_pushdown_fields_survive` — generalises #207's single hand-built case across the generated space. Plus `empty_plan_is_rejected`, stated once because the Coq `optimize` is total while the Rust one is partial (`PlannerError::EmptyPlan`). Recording that difference beats letting the generators quietly avoid it. **Verified as real guards, not vacuous ones.** Two negative controls: 1. Dropping a node -> 2 properties fail with `node count changed`. 2. A **count-preserving** corruption (duplicating node 0 over the last node) — invisible to any length assertion — is caught by the multiset with the exact diagnostic `("Graph", "Equality { field: \"a\", ... }"): 2`. That is the specific case the existing unit tests cannot see, demonstrated rather than claimed. Both restored to green afterwards. Note on the committed `.proptest-regressions`: the repo already tracks these (see `verisim-document`), and proptest recommends checking them in. But be clear about provenance — both seeds come from the *injected* failures above, not from any real historical bug. They shrink to a trivial one-node Graph plan and pass now; they are cheap to replay and should not be read as evidence of a past defect. Verified: `cargo test -p verisim-planner` 118 + 5 + 4 + 1 passing, 0 failed; clippy clean on `--all-targets`; `cargo doc --no-deps` clean (it is a required check); `reuse lint` compliant.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
fix(planner): carry projections and early_limit into the physical plan
PlanNodehas four fields;PlanStephad six, and neitherprojectionsnorearly_limitwas among them. The optimizer computed both, then dropped them atthe logical -> physical boundary, so the executor never saw either pushdown.
That is worse than merely lossy, and this is the part worth flagging.
CostModel::estimatealready discounts a node carrying an early limit(
cost.rs:345-350):So a plan was priced as cheap as half its base cost because of a limit
pushdown that the physical plan had no way to perform. The planner was
rewarding an optimisation it then discarded. Nothing failed loudly — plans
simply cost less on paper than they cost to run, which is the kind of defect
that shows up as unexplained latency rather than as an error.
Measured before the change:
early_limithad exactly one non-test read in theentire tree — the cost adjustment above.
projectionshad none; nothingread it after
vcl_bridge.rsbuilt it.Both fields are now on
PlanStepand populated from the node. They carry#[serde(default)], so aPhysicalPlanserialised before this change stilldeserialises (absent ->
vec![]/None, matching the old behaviour ratherthan inventing a limit).
This surfaced while discharging
optimize_is_permutation(#206). The Coq modelabstracts a node as
(modality, list condition)— precisely the projection thatomits the two fields being lost. The abstraction was not wrong, but it was drawn
around the bug, which is why proving the permutation property could not have
caught it.
Test:
test_pushdown_survives_optimizationasserts both fields survive, andmatches steps by modality rather than index — asserting on
steps[0]would testthe sort order, not the pushdown. Verified as a real guard, not a vacuous one:
with the population reverted it fails with
projection pushdown was dropped at the physical boundary; with the fix it passes.Verified:
cargo test -p verisim-planner118 passed / 0 failed;cargo clippy -p verisim-planner --all-targetsclean;cargo check -p verisim-api --all-targetsclean (it mapsPlanStepinto its own GraphQL type);reuse lintcompliant.Not addressed here, and deliberately so:
pushed_predicatesremainsVec<String>built byformat!("{:?}", c), so conditions still cross theboundary as Rust
Debugoutput rather than asConditionKind. Retyping it is alarger change with its own serialisation surface, and it is not needed to stop
the cost model lying.