diff --git a/rust-core/verisim-planner/tests/property_tests.proptest-regressions b/rust-core/verisim-planner/tests/property_tests.proptest-regressions new file mode 100644 index 0000000..c14ead8 --- /dev/null +++ b/rust-core/verisim-planner/tests/property_tests.proptest-regressions @@ -0,0 +1,8 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 8e6fbd88c3fa2d5269cef93616a351d9b34388225b8e7c668f437b7b347a0ce1 # shrinks to plan = LogicalPlan { source: Octad, nodes: [PlanNode { modality: Graph, conditions: [], projections: [], early_limit: None }], post_processing: [] } +cc 79f109ba4370312b0340787559709863d24b909839030468c36179d945fb4601 # shrinks to plan = LogicalPlan { source: Octad, nodes: [PlanNode { modality: Graph, conditions: [], projections: [], early_limit: None }], post_processing: [] } diff --git a/rust-core/verisim-planner/tests/property_tests.rs b/rust-core/verisim-planner/tests/property_tests.rs new file mode 100644 index 0000000..22f401d --- /dev/null +++ b/rust-core/verisim-planner/tests/property_tests.rs @@ -0,0 +1,261 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Property-based tests for the optimizer — the Rust image of `formal/Planner.v`. +//! +//! `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 file is that test, and closes the refinement link +//! #113 owes. +//! +//! Worth being precise about 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 of them asserts the +//! multiset — which is the actual content of the permutation property, and the +//! one thing that would catch a node being silently dropped or duplicated. +//! +//! The Coq model abstracts a node as `(modality, list condition)`. These +//! properties are stated over that same projection so the two are comparable, +//! with the caveats the Coq header records: +//! +//! * Coq's `optimize` is total; the Rust one is partial (`EmptyPlan`), so the +//! generators produce non-empty plans and emptiness is checked separately. +//! * Coq's cost carrier is `nat`; the Rust tie-breaker is `f64` compared with +//! `partial_cmp(...).unwrap_or(Equal)`, which is why `prop_optimize_never_panics` +//! exists at all. + +use std::collections::BTreeMap; + +use proptest::prelude::*; +use verisim_planner::plan::{ConditionKind, LogicalPlan, PlanNode, QuerySource}; +use verisim_planner::{Modality, Planner, PlannerConfig}; + +// --------------------------------------------------------------------------- +// Generators +// --------------------------------------------------------------------------- + +fn modality_strategy() -> impl Strategy { + prop_oneof![ + Just(Modality::Graph), + Just(Modality::Vector), + Just(Modality::Tensor), + Just(Modality::Semantic), + Just(Modality::Document), + Just(Modality::Temporal), + ] +} + +/// Covers all nine `ConditionKind` constructors. The planner treats conditions +/// opaquely when reordering, but they participate in cost estimation, so a +/// generator that only emitted one variant would exercise a single cost path. +fn condition_strategy() -> impl Strategy { + prop_oneof![ + ("[a-z]{1,8}", "[a-z0-9]{1,8}") + .prop_map(|(field, value)| ConditionKind::Equality { field, value }), + ("[a-z]{1,8}", "[0-9]{1,4}", "[0-9]{1,4}") + .prop_map(|(field, low, high)| ConditionKind::Range { field, low, high }), + "[a-z ]{1,12}".prop_map(|query| ConditionKind::Fulltext { query }), + (1usize..500).prop_map(|k| ConditionKind::Similarity { k }), + ("[a-z_]{1,10}", proptest::option::of(1u32..8)) + .prop_map(|(predicate, depth)| ConditionKind::Traversal { predicate, depth }), + "[0-9]{4}".prop_map(|timestamp| ConditionKind::AtTime { timestamp }), + "[a-z]{1,8}".prop_map(|contract| ConditionKind::ProofVerification { contract }), + "[a-z]{1,8}".prop_map(|operation| ConditionKind::TensorOp { operation }), + "[a-z ]{1,10}".prop_map(|expression| ConditionKind::Predicate { expression }), + ] +} + +fn node_strategy() -> impl Strategy { + ( + modality_strategy(), + prop::collection::vec(condition_strategy(), 0..4), + prop::collection::vec("[a-z]{1,6}", 0..3), + proptest::option::of(1usize..2000), + ) + .prop_map( + |(modality, conditions, projections, early_limit)| PlanNode { + modality, + conditions, + projections, + early_limit, + }, + ) +} + +/// Non-empty by construction: `Planner::optimize` returns `EmptyPlan` for an +/// empty node list, so an empty plan is a different property (asserted once, +/// below) rather than a case these should silently skip. +fn plan_strategy() -> impl Strategy { + prop::collection::vec(node_strategy(), 1..12).prop_map(|nodes| LogicalPlan { + source: QuerySource::Octad, + nodes, + post_processing: vec![], + }) +} + +// --------------------------------------------------------------------------- +// Helpers +// --------------------------------------------------------------------------- + +/// The Coq node projection `(modality, list condition)`, as a countable key. +/// +/// Conditions are rendered with `{:?}` because that is precisely what +/// `optimizer.rs` does when it builds `pushed_predicates` — so this compares +/// the two sides on the representation the code actually produces, rather than +/// on one invented for the test. +fn multiset(pairs: impl Iterator) -> BTreeMap<(String, String), usize> { + let mut m = BTreeMap::new(); + for (modality, conds) in pairs { + *m.entry((format!("{modality:?}"), conds)).or_insert(0) += 1; + } + m +} + +fn logical_multiset(plan: &LogicalPlan) -> BTreeMap<(String, String), usize> { + multiset(plan.nodes.iter().map(|n| { + let conds: Vec = n.conditions.iter().map(|c| format!("{c:?}")).collect(); + (n.modality, conds.join("|")) + })) +} + +fn physical_multiset(plan: &verisim_planner::PhysicalPlan) -> BTreeMap<(String, String), usize> { + multiset( + plan.steps + .iter() + .map(|s| (s.modality, s.pushed_predicates.join("|"))), + ) +} + +fn planner() -> Planner { + Planner::new(PlannerConfig::default()) +} + +// --------------------------------------------------------------------------- +// Properties +// --------------------------------------------------------------------------- + +proptest! { + /// The Rust image of `Planner.v`'s `optimize_is_permutation`. + /// + /// Nodes may be reordered; none may be added, dropped or duplicated. This + /// is the multiset equality that the existing ordering/count unit tests do + /// not cover — a swap of two nodes for each other would satisfy a count + /// assertion and fail this one. + #[test] + fn prop_optimize_is_permutation(plan in plan_strategy()) { + let physical = planner().optimize(&plan).expect("non-empty plan optimizes"); + + prop_assert_eq!( + plan.nodes.len(), + physical.steps.len(), + "node count changed" + ); + prop_assert_eq!( + logical_multiset(&plan), + physical_multiset(&physical), + "the multiset of (modality, conditions) was not preserved" + ); + } + + /// Reordering must not change what the plan is estimated to cost. + /// + /// This is the cost-invariance side of the same story: `optimize` is only a + /// legitimate optimisation if permuting the input leaves the total estimate + /// alone. Asserted with a relative tolerance rather than `==` because f64 + /// `+` and `*` are commutative but **not associative**, so `combine` is + /// permutation-invariant only up to rounding — the same caveat recorded in + /// `Planner.v`'s header. + #[test] + fn prop_optimize_total_cost_invariant( + plan in plan_strategy(), + rotation in 0usize..12, + ) { + let p = planner(); + let base = p.optimize(&plan).expect("optimizes"); + + let mut rotated_nodes = plan.nodes.clone(); + let n = rotated_nodes.len(); + rotated_nodes.rotate_left(rotation % n); + let rotated = LogicalPlan { + source: plan.source.clone(), + nodes: rotated_nodes, + post_processing: plan.post_processing.clone(), + }; + let other = p.optimize(&rotated).expect("optimizes"); + + let (a, b) = (base.total_cost.time_ms, other.total_cost.time_ms); + let tolerance = 1e-9_f64.max(a.abs().max(b.abs()) * 1e-9); + prop_assert!( + (a - b).abs() <= tolerance, + "total cost changed under permutation: {a} vs {b}" + ); + } + + /// The optimizer must not panic on any well-formed plan. + /// + /// Specifically guards the comparator. `optimizer.rs` ties on + /// `a.time_ms.partial_cmp(&b.time_ms).unwrap_or(Ordering::Equal)`, and a NaN + /// makes that non-transitive — which violates `sort_by`'s documented + /// contract and may panic outright on Rust >= 1.81. NaN is believed + /// 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 worth testing rather than asserting. + #[test] + fn prop_optimize_never_panics(plan in plan_strategy()) { + let physical = planner().optimize(&plan).expect("optimizes"); + for step in &physical.steps { + prop_assert!( + !step.cost.time_ms.is_nan(), + "NaN reached a step's time_ms; the sort comparator is unsound for this input" + ); + } + prop_assert!(!physical.total_cost.time_ms.is_nan(), "NaN total cost"); + } + + /// Pushdown fields survive optimization for every generated node. + /// + /// The unit test added with the fix covers one hand-built plan; this covers + /// the generated space. Both matter: dropping these was not merely lossy, + /// because `CostModel::estimate` already discounts a node carrying an + /// `early_limit`, so the plan was priced for a pushdown the executor could + /// not perform. + #[test] + fn prop_pushdown_fields_survive(plan in plan_strategy()) { + let physical = planner().optimize(&plan).expect("optimizes"); + + let mut want: Vec<(String, Vec, Option)> = plan + .nodes + .iter() + .map(|n| (format!("{:?}", n.modality), n.projections.clone(), n.early_limit)) + .collect(); + let mut got: Vec<(String, Vec, Option)> = physical + .steps + .iter() + .map(|s| (format!("{:?}", s.modality), s.projections.clone(), s.early_limit)) + .collect(); + + want.sort(); + got.sort(); + prop_assert_eq!(want, got, "projection/early-limit pushdown did not survive"); + } +} + +/// `optimize` is partial where the Coq model is total: the empty plan is an +/// error, not an empty result. Stated once here so the generators above can +/// stay non-empty without that difference going unrecorded. +#[test] +fn empty_plan_is_rejected() { + let empty = LogicalPlan { + source: QuerySource::Octad, + nodes: vec![], + post_processing: vec![], + }; + assert!( + planner().optimize(&empty).is_err(), + "empty plan must be rejected, not silently optimized to an empty plan" + ); +}