test(planner): property-test the Rust image of optimize_is_permutation - #209
Merged
Conversation
`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.
|
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 ✅ ApprovedAdds property-based tests for the Rust implementation of optimize_is_permutation to verify multiset preservation, cost invariants, and safety guarantees against the Coq model. 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}
`rustfmt` is a required check and `physical_multiset`'s signature was wrapped across three lines where it fits on one. My pre-commit verification ran test, clippy, doc and reuse but not `cargo fmt --check` — adding it to the list. No behaviour change; the 5 property tests still pass.
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.
test(planner): property-test the Rust image of optimize_is_permutation
formal/Planner.vprovesoptimize_is_permutationabout a Coq function.That says nothing about this crate until something checks the Rust against the
same statement, and
Planner.v:23-28has promised exactly that since the modulewas written:
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.rsalready has eight unit tests, but theyassert ordering (
test_vector_before_graph,test_semantic_always_last) andcounts. 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)projectionthe 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 theestimate, since that is what makes reordering a legitimate optimisation.
Compared with a relative tolerance rather than
==: f64+/*arecommutative but not associative, so
combineis permutation-invariantonly up to rounding. Same caveat recorded in
Planner.v's header.prop_optimize_never_panics— guards the comparator. The tie-break ispartial_cmp(...).unwrap_or(Equal)on f64, which a NaN makes non-transitive,violating
sort_by's contract and potentially panicking on Rust >= 1.81. NaNlooks unreachable today (the only division in
CostModel::estimateis guardedand feeds
selectivity, nottime_ms) but nothing in the types enforces it,so the belief is tested rather than asserted.
prop_pushdown_fields_survive— generalises fix(planner): carry projections and early_limit into the physical plan #207's single hand-built caseacross the generated space.
Plus
empty_plan_is_rejected, stated once because the Coqoptimizeis totalwhile the Rust one is partial (
PlannerError::EmptyPlan). Recording thatdifference beats letting the generators quietly avoid it.
Verified as real guards, not vacuous ones. Two negative controls:
node count changed.invisible to any length assertion — is caught by the multiset with the exact
diagnostic
("Graph", "Equality { field: \"a\", ... }"): 2. That is thespecific 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 clearabout 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-planner118 + 5 + 4 + 1 passing, 0 failed;clippy clean on
--all-targets;cargo doc --no-depsclean (it is a requiredcheck);
reuse lintcompliant.