|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +//! Property-based tests for the optimizer — the Rust image of `formal/Planner.v`. |
| 3 | +//! |
| 4 | +//! `Planner.v` proves `optimize_is_permutation` about a *Coq* function. That |
| 5 | +//! says nothing about this crate until something checks the Rust against the |
| 6 | +//! same statement, and `Planner.v:23-28` has promised exactly that since the |
| 7 | +//! module was written: |
| 8 | +//! |
| 9 | +//! > A property test added alongside Provenance.v's chain-link integrity check |
| 10 | +//! > would exercise this in Rust. |
| 11 | +//! |
| 12 | +//! It was never added. This file is that test, and closes the refinement link |
| 13 | +//! #113 owes. |
| 14 | +//! |
| 15 | +//! Worth being precise about the gap it closes. `optimizer.rs` already has |
| 16 | +//! eight unit tests, but they assert *ordering* (`test_vector_before_graph`, |
| 17 | +//! `test_semantic_always_last`) and *counts*. None of them asserts the |
| 18 | +//! multiset — which is the actual content of the permutation property, and the |
| 19 | +//! one thing that would catch a node being silently dropped or duplicated. |
| 20 | +//! |
| 21 | +//! The Coq model abstracts a node as `(modality, list condition)`. These |
| 22 | +//! properties are stated over that same projection so the two are comparable, |
| 23 | +//! with the caveats the Coq header records: |
| 24 | +//! |
| 25 | +//! * Coq's `optimize` is total; the Rust one is partial (`EmptyPlan`), so the |
| 26 | +//! generators produce non-empty plans and emptiness is checked separately. |
| 27 | +//! * Coq's cost carrier is `nat`; the Rust tie-breaker is `f64` compared with |
| 28 | +//! `partial_cmp(...).unwrap_or(Equal)`, which is why `prop_optimize_never_panics` |
| 29 | +//! exists at all. |
| 30 | +
|
| 31 | +use std::collections::BTreeMap; |
| 32 | + |
| 33 | +use proptest::prelude::*; |
| 34 | +use verisim_planner::plan::{ConditionKind, LogicalPlan, PlanNode, QuerySource}; |
| 35 | +use verisim_planner::{Modality, Planner, PlannerConfig}; |
| 36 | + |
| 37 | +// --------------------------------------------------------------------------- |
| 38 | +// Generators |
| 39 | +// --------------------------------------------------------------------------- |
| 40 | + |
| 41 | +fn modality_strategy() -> impl Strategy<Value = Modality> { |
| 42 | + prop_oneof![ |
| 43 | + Just(Modality::Graph), |
| 44 | + Just(Modality::Vector), |
| 45 | + Just(Modality::Tensor), |
| 46 | + Just(Modality::Semantic), |
| 47 | + Just(Modality::Document), |
| 48 | + Just(Modality::Temporal), |
| 49 | + ] |
| 50 | +} |
| 51 | + |
| 52 | +/// Covers all nine `ConditionKind` constructors. The planner treats conditions |
| 53 | +/// opaquely when reordering, but they participate in cost estimation, so a |
| 54 | +/// generator that only emitted one variant would exercise a single cost path. |
| 55 | +fn condition_strategy() -> impl Strategy<Value = ConditionKind> { |
| 56 | + prop_oneof![ |
| 57 | + ("[a-z]{1,8}", "[a-z0-9]{1,8}") |
| 58 | + .prop_map(|(field, value)| ConditionKind::Equality { field, value }), |
| 59 | + ("[a-z]{1,8}", "[0-9]{1,4}", "[0-9]{1,4}") |
| 60 | + .prop_map(|(field, low, high)| ConditionKind::Range { field, low, high }), |
| 61 | + "[a-z ]{1,12}".prop_map(|query| ConditionKind::Fulltext { query }), |
| 62 | + (1usize..500).prop_map(|k| ConditionKind::Similarity { k }), |
| 63 | + ("[a-z_]{1,10}", proptest::option::of(1u32..8)) |
| 64 | + .prop_map(|(predicate, depth)| ConditionKind::Traversal { predicate, depth }), |
| 65 | + "[0-9]{4}".prop_map(|timestamp| ConditionKind::AtTime { timestamp }), |
| 66 | + "[a-z]{1,8}".prop_map(|contract| ConditionKind::ProofVerification { contract }), |
| 67 | + "[a-z]{1,8}".prop_map(|operation| ConditionKind::TensorOp { operation }), |
| 68 | + "[a-z ]{1,10}".prop_map(|expression| ConditionKind::Predicate { expression }), |
| 69 | + ] |
| 70 | +} |
| 71 | + |
| 72 | +fn node_strategy() -> impl Strategy<Value = PlanNode> { |
| 73 | + ( |
| 74 | + modality_strategy(), |
| 75 | + prop::collection::vec(condition_strategy(), 0..4), |
| 76 | + prop::collection::vec("[a-z]{1,6}", 0..3), |
| 77 | + proptest::option::of(1usize..2000), |
| 78 | + ) |
| 79 | + .prop_map( |
| 80 | + |(modality, conditions, projections, early_limit)| PlanNode { |
| 81 | + modality, |
| 82 | + conditions, |
| 83 | + projections, |
| 84 | + early_limit, |
| 85 | + }, |
| 86 | + ) |
| 87 | +} |
| 88 | + |
| 89 | +/// Non-empty by construction: `Planner::optimize` returns `EmptyPlan` for an |
| 90 | +/// empty node list, so an empty plan is a different property (asserted once, |
| 91 | +/// below) rather than a case these should silently skip. |
| 92 | +fn plan_strategy() -> impl Strategy<Value = LogicalPlan> { |
| 93 | + prop::collection::vec(node_strategy(), 1..12).prop_map(|nodes| LogicalPlan { |
| 94 | + source: QuerySource::Octad, |
| 95 | + nodes, |
| 96 | + post_processing: vec![], |
| 97 | + }) |
| 98 | +} |
| 99 | + |
| 100 | +// --------------------------------------------------------------------------- |
| 101 | +// Helpers |
| 102 | +// --------------------------------------------------------------------------- |
| 103 | + |
| 104 | +/// The Coq node projection `(modality, list condition)`, as a countable key. |
| 105 | +/// |
| 106 | +/// Conditions are rendered with `{:?}` because that is precisely what |
| 107 | +/// `optimizer.rs` does when it builds `pushed_predicates` — so this compares |
| 108 | +/// the two sides on the representation the code actually produces, rather than |
| 109 | +/// on one invented for the test. |
| 110 | +fn multiset(pairs: impl Iterator<Item = (Modality, String)>) -> BTreeMap<(String, String), usize> { |
| 111 | + let mut m = BTreeMap::new(); |
| 112 | + for (modality, conds) in pairs { |
| 113 | + *m.entry((format!("{modality:?}"), conds)).or_insert(0) += 1; |
| 114 | + } |
| 115 | + m |
| 116 | +} |
| 117 | + |
| 118 | +fn logical_multiset(plan: &LogicalPlan) -> BTreeMap<(String, String), usize> { |
| 119 | + multiset(plan.nodes.iter().map(|n| { |
| 120 | + let conds: Vec<String> = n.conditions.iter().map(|c| format!("{c:?}")).collect(); |
| 121 | + (n.modality, conds.join("|")) |
| 122 | + })) |
| 123 | +} |
| 124 | + |
| 125 | +fn physical_multiset(plan: &verisim_planner::PhysicalPlan) -> BTreeMap<(String, String), usize> { |
| 126 | + multiset( |
| 127 | + plan.steps |
| 128 | + .iter() |
| 129 | + .map(|s| (s.modality, s.pushed_predicates.join("|"))), |
| 130 | + ) |
| 131 | +} |
| 132 | + |
| 133 | +fn planner() -> Planner { |
| 134 | + Planner::new(PlannerConfig::default()) |
| 135 | +} |
| 136 | + |
| 137 | +// --------------------------------------------------------------------------- |
| 138 | +// Properties |
| 139 | +// --------------------------------------------------------------------------- |
| 140 | + |
| 141 | +proptest! { |
| 142 | + /// The Rust image of `Planner.v`'s `optimize_is_permutation`. |
| 143 | + /// |
| 144 | + /// Nodes may be reordered; none may be added, dropped or duplicated. This |
| 145 | + /// is the multiset equality that the existing ordering/count unit tests do |
| 146 | + /// not cover — a swap of two nodes for each other would satisfy a count |
| 147 | + /// assertion and fail this one. |
| 148 | + #[test] |
| 149 | + fn prop_optimize_is_permutation(plan in plan_strategy()) { |
| 150 | + let physical = planner().optimize(&plan).expect("non-empty plan optimizes"); |
| 151 | + |
| 152 | + prop_assert_eq!( |
| 153 | + plan.nodes.len(), |
| 154 | + physical.steps.len(), |
| 155 | + "node count changed" |
| 156 | + ); |
| 157 | + prop_assert_eq!( |
| 158 | + logical_multiset(&plan), |
| 159 | + physical_multiset(&physical), |
| 160 | + "the multiset of (modality, conditions) was not preserved" |
| 161 | + ); |
| 162 | + } |
| 163 | + |
| 164 | + /// Reordering must not change what the plan is estimated to cost. |
| 165 | + /// |
| 166 | + /// This is the cost-invariance side of the same story: `optimize` is only a |
| 167 | + /// legitimate optimisation if permuting the input leaves the total estimate |
| 168 | + /// alone. Asserted with a relative tolerance rather than `==` because f64 |
| 169 | + /// `+` and `*` are commutative but **not associative**, so `combine` is |
| 170 | + /// permutation-invariant only up to rounding — the same caveat recorded in |
| 171 | + /// `Planner.v`'s header. |
| 172 | + #[test] |
| 173 | + fn prop_optimize_total_cost_invariant( |
| 174 | + plan in plan_strategy(), |
| 175 | + rotation in 0usize..12, |
| 176 | + ) { |
| 177 | + let p = planner(); |
| 178 | + let base = p.optimize(&plan).expect("optimizes"); |
| 179 | + |
| 180 | + let mut rotated_nodes = plan.nodes.clone(); |
| 181 | + let n = rotated_nodes.len(); |
| 182 | + rotated_nodes.rotate_left(rotation % n); |
| 183 | + let rotated = LogicalPlan { |
| 184 | + source: plan.source.clone(), |
| 185 | + nodes: rotated_nodes, |
| 186 | + post_processing: plan.post_processing.clone(), |
| 187 | + }; |
| 188 | + let other = p.optimize(&rotated).expect("optimizes"); |
| 189 | + |
| 190 | + let (a, b) = (base.total_cost.time_ms, other.total_cost.time_ms); |
| 191 | + let tolerance = 1e-9_f64.max(a.abs().max(b.abs()) * 1e-9); |
| 192 | + prop_assert!( |
| 193 | + (a - b).abs() <= tolerance, |
| 194 | + "total cost changed under permutation: {a} vs {b}" |
| 195 | + ); |
| 196 | + } |
| 197 | + |
| 198 | + /// The optimizer must not panic on any well-formed plan. |
| 199 | + /// |
| 200 | + /// Specifically guards the comparator. `optimizer.rs` ties on |
| 201 | + /// `a.time_ms.partial_cmp(&b.time_ms).unwrap_or(Ordering::Equal)`, and a NaN |
| 202 | + /// makes that non-transitive — which violates `sort_by`'s documented |
| 203 | + /// contract and may panic outright on Rust >= 1.81. NaN is believed |
| 204 | + /// unreachable today (the only division in `CostModel::estimate` is guarded |
| 205 | + /// and feeds `selectivity`, not `time_ms`), but nothing in the types |
| 206 | + /// enforces it, so the belief is worth testing rather than asserting. |
| 207 | + #[test] |
| 208 | + fn prop_optimize_never_panics(plan in plan_strategy()) { |
| 209 | + let physical = planner().optimize(&plan).expect("optimizes"); |
| 210 | + for step in &physical.steps { |
| 211 | + prop_assert!( |
| 212 | + !step.cost.time_ms.is_nan(), |
| 213 | + "NaN reached a step's time_ms; the sort comparator is unsound for this input" |
| 214 | + ); |
| 215 | + } |
| 216 | + prop_assert!(!physical.total_cost.time_ms.is_nan(), "NaN total cost"); |
| 217 | + } |
| 218 | + |
| 219 | + /// Pushdown fields survive optimization for every generated node. |
| 220 | + /// |
| 221 | + /// The unit test added with the fix covers one hand-built plan; this covers |
| 222 | + /// the generated space. Both matter: dropping these was not merely lossy, |
| 223 | + /// because `CostModel::estimate` already discounts a node carrying an |
| 224 | + /// `early_limit`, so the plan was priced for a pushdown the executor could |
| 225 | + /// not perform. |
| 226 | + #[test] |
| 227 | + fn prop_pushdown_fields_survive(plan in plan_strategy()) { |
| 228 | + let physical = planner().optimize(&plan).expect("optimizes"); |
| 229 | + |
| 230 | + let mut want: Vec<(String, Vec<String>, Option<usize>)> = plan |
| 231 | + .nodes |
| 232 | + .iter() |
| 233 | + .map(|n| (format!("{:?}", n.modality), n.projections.clone(), n.early_limit)) |
| 234 | + .collect(); |
| 235 | + let mut got: Vec<(String, Vec<String>, Option<usize>)> = physical |
| 236 | + .steps |
| 237 | + .iter() |
| 238 | + .map(|s| (format!("{:?}", s.modality), s.projections.clone(), s.early_limit)) |
| 239 | + .collect(); |
| 240 | + |
| 241 | + want.sort(); |
| 242 | + got.sort(); |
| 243 | + prop_assert_eq!(want, got, "projection/early-limit pushdown did not survive"); |
| 244 | + } |
| 245 | +} |
| 246 | + |
| 247 | +/// `optimize` is partial where the Coq model is total: the empty plan is an |
| 248 | +/// error, not an empty result. Stated once here so the generators above can |
| 249 | +/// stay non-empty without that difference going unrecorded. |
| 250 | +#[test] |
| 251 | +fn empty_plan_is_rejected() { |
| 252 | + let empty = LogicalPlan { |
| 253 | + source: QuerySource::Octad, |
| 254 | + nodes: vec![], |
| 255 | + post_processing: vec![], |
| 256 | + }; |
| 257 | + assert!( |
| 258 | + planner().optimize(&empty).is_err(), |
| 259 | + "empty plan must be rejected, not silently optimized to an empty plan" |
| 260 | + ); |
| 261 | +} |
0 commit comments