From a60f95c8ca6a047481ad46969365905423b63e3f Mon Sep 17 00:00:00 2001 From: leynos Date: Wed, 20 May 2026 23:46:02 +0200 Subject: [PATCH 1/2] Deepen semantic invariant property tests (#112) Add depth-enforced formula generators for the semantic invariants introduced in PR #104. Ensure the invalid `Or` and invalid `And` properties always exercise trees with at least four levels, and keep the valid-tree strategy positive while retaining the same depth guarantee. Assert the generated tree depth inside each property so future strategy changes cannot silently shrink this coverage back to shallow trees. --- crates/sempai/src/tests/property_tests.rs | 113 ++++++++++++++++++++-- 1 file changed, 104 insertions(+), 9 deletions(-) diff --git a/crates/sempai/src/tests/property_tests.rs b/crates/sempai/src/tests/property_tests.rs index 1fb99d4b..3dca5143 100644 --- a/crates/sempai/src/tests/property_tests.rs +++ b/crates/sempai/src/tests/property_tests.rs @@ -12,6 +12,7 @@ use crate::semantic_check::validate_formula; const MAX_DEPTH: u32 = 5; const MAX_SIZE: u32 = 32; const MAX_BRANCHES: u32 = 3; +const MIN_PROPERTY_DEPTH: usize = 4; fn decorated(node: Formula, span: Option) -> Decorated { Decorated { @@ -50,6 +51,75 @@ fn atom_strategy() -> BoxedStrategy> { .boxed() } +fn unary_node(variant: u8, child: Decorated) -> Formula { + match variant { + 0 => Formula::Not(Box::new(child)), + 1 => Formula::Inside(Box::new(child)), + _ => Formula::Anywhere(Box::new(child)), + } +} + +fn valid_unary_node(is_inside: bool, child: Decorated) -> Formula { + if is_inside { + Formula::Inside(Box::new(child)) + } else { + Formula::Anywhere(Box::new(child)) + } +} + +fn deep_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + (any::(), deep_atom(min_depth - 1), span_strategy()) + .prop_map(|(is_inside, child, span)| decorated(valid_unary_node(is_inside, child), span)) + .boxed() +} + +fn deep_constraint_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + ( + any::(), + deep_constraint_atom(min_depth - 1), + span_strategy(), + ) + .prop_map(|(is_not, child, span)| { + let node = if is_not { + Formula::Not(Box::new(child)) + } else { + Formula::Inside(Box::new(child)) + }; + decorated(node, span) + }) + .boxed() +} + +fn deep_positive_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + (deep_positive_atom(min_depth - 1), span_strategy()) + .prop_map(|(child, span)| decorated(Formula::Or(vec![child]), span)) + .boxed() +} + +fn deep_atomless(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return span_strategy() + .prop_map(|span| decorated(Formula::And(vec![]), span)) + .boxed(); + } + + (0_u8..3, deep_atomless(min_depth - 1), span_strategy()) + .prop_map(|(variant, child, span)| decorated(unary_node(variant, child), span)) + .boxed() +} + fn formula_tree() -> BoxedStrategy> { atom_strategy() .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { @@ -81,7 +151,7 @@ fn formula_tree() -> BoxedStrategy> { } fn tree_with_not() -> BoxedStrategy> { - (formula_tree(), span_strategy()) + (deep_atom(MIN_PROPERTY_DEPTH - 1), span_strategy()) .prop_map(|(child, span)| decorated(Formula::Not(Box::new(child)), span)) .boxed() } @@ -124,15 +194,21 @@ fn atomless_tree_without_not_in_or() -> BoxedStrategy> { fn and_without_positive_descendant() -> BoxedStrategy> { ( - vec(atomless_tree_without_not_in_or(), 0..=MAX_BRANCHES as usize), + vec(atomless_tree_without_not_in_or(), 0..=2), + deep_atomless(MIN_PROPERTY_DEPTH - 1), + vec(atomless_tree_without_not_in_or(), 0..=2), span_strategy(), ) - .prop_map(|(branches, span)| decorated(Formula::And(branches), span)) + .prop_map(|(mut before, required, after, span)| { + before.push(required); + before.extend(after); + decorated(Formula::And(before), span) + }) .boxed() } fn valid_no_not_tree() -> BoxedStrategy> { - atom_strategy() + deep_atom(MIN_PROPERTY_DEPTH) .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { let unary = (any::(), inner.clone(), span_strategy()).prop_map( |(is_inside, child, span)| { @@ -152,17 +228,18 @@ fn valid_no_not_tree() -> BoxedStrategy> { } fn positive_tree() -> BoxedStrategy> { - atom_strategy() + deep_positive_atom(MIN_PROPERTY_DEPTH) .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { - let constraint = - (0_u8..3, atom_strategy(), span_strategy()).prop_map(|(variant, child, span)| { + let constraint = (0_u8..3, deep_constraint_atom(2), span_strategy()).prop_map( + |(variant, child, span)| { let node = match variant { 0 => Formula::Not(Box::new(child)), 1 => Formula::Inside(Box::new(child)), _ => Formula::Anywhere(Box::new(child)), }; decorated(node, span) - }); + }, + ); let and = ( vec(prop_oneof![inner.clone(), constraint], 0..=2), inner.clone(), @@ -176,7 +253,7 @@ fn positive_tree() -> BoxedStrategy> { }); let or = ( vec(valid_no_not_tree(), 0..=2), - atom_strategy(), + deep_positive_atom(MIN_PROPERTY_DEPTH - 1), vec(valid_no_not_tree(), 0..=2), span_strategy(), ) @@ -190,6 +267,18 @@ fn positive_tree() -> BoxedStrategy> { .boxed() } +fn tree_depth(formula: &Decorated) -> usize { + match &formula.node { + Formula::Atom(_) => 1, + Formula::Not(inner) | Formula::Inside(inner) | Formula::Anywhere(inner) => { + 1 + tree_depth(inner) + } + Formula::And(branches) | Formula::Or(branches) => { + 1 + branches.iter().map(tree_depth).max().unwrap_or_default() + } + } +} + fn first_diagnostic_code(formula: &Decorated) -> DiagnosticCode { let err = validate_formula(formula).expect_err("formula should fail validation"); err.diagnostics() @@ -207,6 +296,8 @@ proptest! { #[test] fn prop_or_branch_containing_negation_is_rejected(formula in or_with_not_descendant()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + prop_assert_eq!( first_diagnostic_code(&formula), DiagnosticCode::ESempaiInvalidNotInOr @@ -215,6 +306,8 @@ proptest! { #[test] fn prop_and_with_no_positive_term_is_rejected(formula in and_without_positive_descendant()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + let expected_span = formula .span .clone() @@ -234,6 +327,8 @@ proptest! { #[test] fn prop_valid_tree_with_positive_in_every_and_is_ok(formula in positive_tree()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + prop_assert!(validate_formula(&formula).is_ok()); } } From 2c4827a756512341dcd7bfe00eb77b67af110276 Mon Sep 17 00:00:00 2001 From: leynos Date: Fri, 29 May 2026 20:41:35 +0200 Subject: [PATCH 2/2] Refactor nary property strategy helper - Add module-private helper for shared required-branch composition in property test generators. - Refactor and to use helper, preserving existing strategy semantics and depth constraints. --- crates/sempai/src/tests/property_tests.rs | 40 +++++++++++++---------- 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/crates/sempai/src/tests/property_tests.rs b/crates/sempai/src/tests/property_tests.rs index 3dca5143..08a1f2dc 100644 --- a/crates/sempai/src/tests/property_tests.rs +++ b/crates/sempai/src/tests/property_tests.rs @@ -156,21 +156,34 @@ fn tree_with_not() -> BoxedStrategy> { .boxed() } -fn or_with_not_descendant() -> BoxedStrategy> { +fn nary_with_required_branch( + sibling: S, + required: R, + wrap: W, +) -> BoxedStrategy> +where + S: Strategy> + Clone + 'static, + R: Strategy> + 'static, + W: Fn(Vec>) -> Formula + Send + Sync + Clone + 'static, +{ ( - vec(formula_tree(), 0..=2), - tree_with_not(), - vec(formula_tree(), 0..=2), + vec(sibling.clone(), 0..=2), + required, + vec(sibling, 0..=2), span_strategy(), ) - .prop_map(|(mut before, not_branch, after, span)| { - before.push(not_branch); + .prop_map(move |(mut before, required_branch, after, span)| { + before.push(required_branch); before.extend(after); - decorated(Formula::Or(before), span) + decorated(wrap(before), span) }) .boxed() } +fn or_with_not_descendant() -> BoxedStrategy> { + nary_with_required_branch(formula_tree(), tree_with_not(), Formula::Or) +} + fn atomless_tree_without_not_in_or() -> BoxedStrategy> { let leaf = span_strategy() .prop_map(|span| decorated(Formula::And(vec![]), span)) @@ -193,18 +206,11 @@ fn atomless_tree_without_not_in_or() -> BoxedStrategy> { } fn and_without_positive_descendant() -> BoxedStrategy> { - ( - vec(atomless_tree_without_not_in_or(), 0..=2), + nary_with_required_branch( + atomless_tree_without_not_in_or(), deep_atomless(MIN_PROPERTY_DEPTH - 1), - vec(atomless_tree_without_not_in_or(), 0..=2), - span_strategy(), + Formula::And, ) - .prop_map(|(mut before, required, after, span)| { - before.push(required); - before.extend(after); - decorated(Formula::And(before), span) - }) - .boxed() } fn valid_no_not_tree() -> BoxedStrategy> {