feat(formal): discharge optimize_is_permutation — axiom to theorem, in both modules - #206
Merged
Merged
Conversation
…ules) #202 landed the same three-line explanatory comment twice in every module — once above `Set Printing Width 400.` where it belongs, and once orphaned immediately below it. My fault: I ran the insertion, then deleted only the `Set Printing Width 400.` line to A/B-test whether the ~78-column wrap was actually hiding any axiom from the guard, then re-ran the insertion. The sed that undid the test matched only the directive, not its comment, so the second pass stacked a fresh copy on top of the leftover. Comment-only; no directive, no proof and no guard changes. `formal/Justfile` is untouched. To be accurate about scope, since the obvious worry is that a text edit near the imports clipped something: it did not. `Import ListNotations.` and every `Require Import` are intact in all nine modules — verified before and after. (A *different* cleanup attempt of mine did briefly eat that import by skipping a fixed three lines past the marker, which in `Planner.v` overran the comment. That version was reset and never committed; it is mentioned only so the next person knows the offset-based approach is the wrong tool here. This commit removes the second matched block specifically, keyed on occurrence count.) Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub coqc -> exit 127, so the gate from #202 still fails when it should; `Normalizer.out` still prints at 157 columns, so the wrap fix is unaffected; `reuse lint` compliant.
…n both modules `optimize_is_permutation` was an `Axiom` in `formal/Planner.v` and, separately, a second identical `Axiom` in `formal/PlannerSemantic.v`. Both are now gone. **It was not merely unproven — it was unprovable.** `optimize` was a `Parameter`, so nothing constrained it: `fun _ => []` inhabits the parameter and refutes `forall lp, Permutation lp (optimize lp)`. Assuming the statement was assuming the conclusion, and no amount of proof effort against that signature would have worked. Discharging it *requires* replacing the parameter with a definition, which is what this does: * `modality` becomes an `Inductive` with the six constructors of `crate::Modality`, and `execution_priority` transcribes the Rust match arms (Temporal 10, Vector 20, Document 30, Graph 40, Tensor 50, Semantic 90). * `optimize` becomes `Coq.Sorting.Mergesort`'s `sort` under `node_leb` — execution priority first, cost as tie-breaker, i.e. the key `Optimizer::optimize`'s `sort_by` comparator actually uses. * The permutation property falls out of the standard library's `Permuted_sort`, which is itself closed under the global context. All five call sites were left untouched and still compile: the theorem statement is character-for-character what the axiom asserted. `PlannerSemantic.v` claimed in a comment to be "reusing Planner.v abstractions" while in fact re-declaring its own `modality`, `condition`, `node`, `optimize` and a duplicate axiom. The two files agreed only by coincidence, and the duplicate meant discharging Planner's axiom would have left an identical assumption standing next door. It now genuinely `Require Import Planner`, and `formal/Justfile` gains the `planner-semantic: planner` dependency edge that this makes necessary. **Whitelists tightened — this is the acceptance test, not bookkeeping.** The guards enforce "exactly these assumptions", never "no assumptions", so leaving `optimize_is_permutation` listed would have let it return silently: * Planner: `modality|condition|optimize|optimize_is_permutation` -> `condition|node_cost` * PlannerSemantic: drops `modality`, `optimize`, `optimize_is_permutation` Both `formal/Justfile` and `.github/workflows/coq-build.yml` updated together. Two `Parameter`s remain **by design**, and being parametric in them makes the result stronger, not weaker — it holds for *any* condition representation and *any* cost function: `condition` (the Rust `ConditionKind`'s nine constructors are irrelevant to whether nodes are reordered or lost) and `node_cost` (abstracts `CostModel::estimate`'s `time_ms`). Two honest model-vs-code gaps, both recorded in the module header rather than elided, neither affecting the permutation property: * `node_cost` returns `nat`; the Rust tie-breaker is `f64` compared with `partial_cmp(...).unwrap_or(Equal)`. A NaN would make that comparator non-transitive and violate `sort_by`'s contract. NaN is unreachable today — the only division in `CostModel::estimate` is guarded and feeds `selectivity`, not `time_ms` — but nothing in the Rust types enforces that. * Rust `optimize` is partial (`PlannerError::EmptyPlan`); `sort []` is `[]`. `exec_node_comm` deliberately stays. It is a genuine spec axiom over an uninterpreted `exec_node` and needs per-operator semantics to discharge — not something this change touches, and it should not look like collateral. Verified: * Clean build: `just -f formal/Justfile all` and `check-assumptions` both exit 0, 9/9 OK, with the tightened whitelists. * `optimize_is_permutation` appears zero times in either module's `Print Assumptions` output, and no `Axiom optimize_is_permutation` remains anywhere (was 2). * **Negative control** — reintroducing an axiom a theorem depends on is caught: `ERROR(Planner): unexpected axiom: sneaky_regression`, gate exit 1. The tightened whitelist genuinely fails rather than passing vacuously. * Stub `coqc` still drives the gate to exit 127, so #202's fix is intact. * `reuse lint` compliant.
Owner
Author
|
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 ✅ ApprovedReplaces the unprovable optimize_is_permutation axiom with a verified definition in both formal modules by implementing sorting and inductives, successfully discharging the assumption. 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}
hyperpolymath
marked this pull request as ready for review
July 28, 2026 19:04
hyperpolymath
added a commit
that referenced
this pull request
Jul 28, 2026
#207) fix(planner): carry projections and early_limit into the physical plan `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.
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.
feat(formal): discharge optimize_is_permutation — axiom to theorem, in both modules
optimize_is_permutationwas anAxiominformal/Planner.vand, separately,a second identical
Axiominformal/PlannerSemantic.v. Both are now gone.It was not merely unproven — it was unprovable.
optimizewas aParameter, so nothing constrained it:fun _ => []inhabits the parameter andrefutes
forall lp, Permutation lp (optimize lp). Assuming the statement wasassuming the conclusion, and no amount of proof effort against that signature
would have worked. Discharging it requires replacing the parameter with a
definition, which is what this does:
modalitybecomes anInductivewith the six constructors ofcrate::Modality, andexecution_prioritytranscribes the Rust match arms(Temporal 10, Vector 20, Document 30, Graph 40, Tensor 50, Semantic 90).
optimizebecomesCoq.Sorting.Mergesort'ssortundernode_leb—execution priority first, cost as tie-breaker, i.e. the key
Optimizer::optimize'ssort_bycomparator actually uses.Permuted_sort,which is itself closed under the global context.
All five call sites were left untouched and still compile: the theorem
statement is character-for-character what the axiom asserted.
PlannerSemantic.vclaimed in a comment to be "reusing Planner.v abstractions"while in fact re-declaring its own
modality,condition,node,optimizeand a duplicate axiom. The two files agreed only by coincidence, and the
duplicate meant discharging Planner's axiom would have left an identical
assumption standing next door. It now genuinely
Require Import Planner, andformal/Justfilegains theplanner-semantic: plannerdependency edge thatthis makes necessary.
Whitelists tightened — this is the acceptance test, not bookkeeping. The
guards enforce "exactly these assumptions", never "no assumptions", so leaving
optimize_is_permutationlisted would have let it return silently:modality|condition|optimize|optimize_is_permutation->condition|node_costmodality,optimize,optimize_is_permutationBoth
formal/Justfileand.github/workflows/coq-build.ymlupdated together.Two
Parameters remain by design, and being parametric in them makes theresult stronger, not weaker — it holds for any condition representation and
any cost function:
condition(the RustConditionKind's nine constructorsare irrelevant to whether nodes are reordered or lost) and
node_cost(abstracts
CostModel::estimate'stime_ms).Two honest model-vs-code gaps, both recorded in the module header rather than
elided, neither affecting the permutation property:
node_costreturnsnat; the Rust tie-breaker isf64compared withpartial_cmp(...).unwrap_or(Equal). A NaN would make that comparatornon-transitive and violate
sort_by's contract. NaN is unreachable today —the only division in
CostModel::estimateis guarded and feedsselectivity,not
time_ms— but nothing in the Rust types enforces that.optimizeis partial (PlannerError::EmptyPlan);sort []is[].exec_node_commdeliberately stays. It is a genuine spec axiom over anuninterpreted
exec_nodeand needs per-operator semantics to discharge — notsomething this change touches, and it should not look like collateral.
Verified:
just -f formal/Justfile allandcheck-assumptionsboth exit 0,9/9 OK, with the tightened whitelists.
optimize_is_permutationappears zero times in either module'sPrint Assumptionsoutput, and noAxiom optimize_is_permutationremainsanywhere (was 2).
ERROR(Planner): unexpected axiom: sneaky_regression, gate exit 1. Thetightened whitelist genuinely fails rather than passing vacuously.
coqcstill drives the gate to exit 127, so fix(formal): make the local Coq assumptions gate capable of failing #202's fix is intact.reuse lintcompliant.