Add a few property-based tests

.gitignore

@@ -81,3 +81,4 @@ Cargo.lock
 .benchmarks
 .env
 .claude/
+*.proptest-regressions

Cargo.toml

@@ -32,6 +32,9 @@ binaries = []
 
 [dependencies]
 
+[dev-dependencies]
+proptest = "1.6"
+
 [profile.release]
 strip = "debuginfo"
 panic = "unwind"

tests/property_tests.rs

@@ -1 +1,391 @@
+//! Property-based tests for the chase algorithm using proptest.
 
+use proptest::prelude::*;
+
+use chase_rs::chase::rule::RuleBuilder;
+use chase_rs::{Atom, Instance, Term, chase};
+
+/// Strategy for generating constant names
+fn constant_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "a".to_string(),
+        "b".to_string(),
+        "c".to_string(),
+        "d".to_string(),
+        "e".to_string(),
+    ])
+}
+
+/// Strategy for generating variable names
+fn variable_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "X".to_string(),
+        "Y".to_string(),
+        "Z".to_string(),
+        "W".to_string(),
+    ])
+}
+
+/// Strategy for generating predicate names
+fn predicate_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "P".to_string(),
+        "Q".to_string(),
+        "R".to_string(),
+        "S".to_string(),
+    ])
+}
+
+/// Strategy for generating ground atoms (facts)
+fn ground_atom_strategy() -> impl Strategy<Value = Atom> {
+    (
+        predicate_strategy(),
+        prop::collection::vec(constant_strategy(), 1..=3),
+    )
+        .prop_map(|(pred, consts)| {
+            Atom::new(pred, consts.into_iter().map(Term::constant).collect())
+        })
+}
+
+/// Strategy for generating a small instance (set of facts)
+fn instance_strategy() -> impl Strategy<Value = Instance> {
+    prop::collection::vec(ground_atom_strategy(), 0..10)
+        .prop_map(|atoms| atoms.into_iter().collect())
+}
+
+// =============================================================================
+// Property: Chase always terminates
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
+    #[test]
+    fn chase_always_terminates(instance in instance_strategy()) {
+        // Simple rule: P(X) -> Q(X)
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        // Chase should always terminate (either fixpoint or max iterations)
+        prop_assert!(result.terminated || result.steps > 0);
+    }
+}
+
+// =============================================================================
+// Property: Chase is monotonic (facts are only added, never removed)
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
+    #[test]
+    fn chase_is_monotonic(instance in instance_strategy()) {
+        let initial_facts: Vec<_> = instance.iter().cloned().collect();
+
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        // All original facts should still be present
+        for fact in &initial_facts {
+            prop_assert!(
+                result.instance.contains(fact),
+                "Original fact {:?} was removed", fact
+            );
+        }
+
+        // Result should have at least as many facts as the input
+        prop_assert!(result.instance.len() >= initial_facts.len());
+    }
+}
+
+// =============================================================================
+// Property: Fixpoint is stable (running chase again produces no changes)
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(30))]
+
+    #[test]
+    fn fixpoint_is_stable(instance in instance_strategy()) {
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X")])
+            .build();
+
+        // Run chase to fixpoint
+        let result1 = chase(instance, &[rule.clone()]);
+        prop_assert!(result1.terminated);
+
+        // Run chase again on the result
+        let result2 = chase(result1.instance.clone(), &[rule]);
+
+        // Should terminate immediately with no new facts
+        prop_assert!(result2.terminated);
+        prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
+        prop_assert_eq!(result1.instance.len(), result2.instance.len());
+    }
+}
+
+// =============================================================================
+// Property: All derived facts are ground (no variables)
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
+    #[test]
+    fn all_facts_are_ground(instance in instance_strategy()) {
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X"), Term::var("Y")])
+            .then("R", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        for fact in result.instance.iter() {
+            prop_assert!(
+                fact.is_ground(),
+                "Fact {:?} contains variables", fact
+            );
+        }
+    }
+}
+
+// =============================================================================
+// Property: Rules without existentials don't create nulls
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
+    #[test]
+    fn no_existentials_means_no_nulls(instance in instance_strategy()) {
+        // Rule with all head variables appearing in body
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        for fact in result.instance.iter() {
+            for term in &fact.terms {
+                prop_assert!(
+                    !matches!(term, Term::Null(_)),
+                    "Found null in fact {:?} but rule has no existentials", fact
+                );
+            }
+        }
+    }
+}
+
+// =============================================================================
+// Property: Existential rules create exactly one null per trigger
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(30))]
+
+    #[test]
+    fn existentials_create_unique_nulls(
+        num_constants in 1usize..5
+    ) {
+        // Create facts P(c0), P(c1), P(c2), ... with unique constants
+        let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
+        let instance: Instance = constants
+            .iter()
+            .map(|c| Atom::new("P", vec![Term::constant(c)]))
+            .collect();
+
+        // Rule: P(X) -> Q(X, Y) where Y is existential
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");
+
+        // Should have exactly as many Q facts as P facts
+        prop_assert_eq!(q_facts.len(), num_constants);
+
+        // Each Q fact should have a null in the second position
+        for fact in &q_facts {
+            prop_assert!(
+                matches!(fact.terms[1], Term::Null(_)),
+                "Expected null in second position of {:?}", fact
+            );
+        }
+
+        // All nulls should be unique
+        let nulls: Vec<_> = q_facts
+            .iter()
+            .filter_map(|f| match &f.terms[1] {
+                Term::Null(id) => Some(*id),
+                _ => None,
+            })
+            .collect();
+
+        let mut unique_nulls = nulls.clone();
+        unique_nulls.sort();
+        unique_nulls.dedup();
+        prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
+    }
+}
+
+// =============================================================================
+// Property: Transitive closure computes correct number of facts
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(20))]
+
+    #[test]
+    fn transitive_closure_chain(chain_length in 2usize..6) {
+        // Create a chain: E(0,1), E(1,2), ..., E(n-1,n)
+        let mut facts = Vec::new();
+        for i in 0..chain_length {
+            facts.push(Atom::new(
+                "E",
+                vec![Term::constant(format!("{}", i)), Term::constant(format!("{}", i + 1))],
+            ));
+        }
+        let instance: Instance = facts.into_iter().collect();
+
+        // E(X,Y) -> T(X,Y)
+        let rule1 = RuleBuilder::new()
+            .when("E", vec![Term::var("X"), Term::var("Y")])
+            .then("T", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        // T(X,Y), E(Y,Z) -> T(X,Z)
+        let rule2 = RuleBuilder::new()
+            .when("T", vec![Term::var("X"), Term::var("Y")])
+            .when("E", vec![Term::var("Y"), Term::var("Z")])
+            .then("T", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        let result = chase(instance, &[rule1, rule2]);
+        prop_assert!(result.terminated);
+
+        let t_facts = result.instance.facts_for_predicate("T");
+
+        // For a chain of n edges, transitive closure has n*(n+1)/2 pairs
+        let expected = chain_length * (chain_length + 1) / 2;
+        prop_assert_eq!(
+            t_facts.len(),
+            expected,
+            "Chain of {} edges should have {} transitive pairs",
+            chain_length,
+            expected
+        );
+    }
+}
+
+// =============================================================================
+// Property: Empty instance with any rules produces empty or stays empty
+// =============================================================================
+
+proptest! {
+    #[test]
+    fn empty_instance_stays_bounded(_seed in 0u64..1000) {
+        let instance = Instance::new();
+
+        let rule = RuleBuilder::new()
+            .when("P", vec![Term::var("X")])
+            .then("Q", vec![Term::var("X")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        prop_assert!(result.terminated);
+        prop_assert_eq!(result.steps, 0);
+        prop_assert!(result.instance.is_empty());
+    }
+}
+
+// =============================================================================
+// Property: Substitution application is idempotent for ground terms
+// =============================================================================
+
+use chase_rs::Substitution;
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(100))]
+
+    #[test]
+    fn substitution_ground_term_unchanged(c in constant_strategy()) {
+        let term = Term::constant(&c);
+        let mut subst = Substitution::new();
+        subst.bind("X".to_string(), Term::constant("other"));
+
+        let result = subst.apply_term(&term);
+
+        prop_assert_eq!(result, term, "Ground term should be unchanged by substitution");
+    }
+}
+
+// =============================================================================
+// Property: Substitution correctly replaces variables
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(100))]
+
+    #[test]
+    fn substitution_replaces_variable(
+        var in variable_strategy(),
+        replacement in constant_strategy()
+    ) {
+        let term = Term::var(&var);
+        let mut subst = Substitution::new();
+        subst.bind(var.clone(), Term::constant(&replacement));
+
+        let result = subst.apply_term(&term);
+
+        prop_assert_eq!(
+            result,
+            Term::constant(&replacement),
+            "Variable should be replaced"
+        );
+    }
+}
+
+// =============================================================================
+// Property: Atom arity is preserved through substitution
+// =============================================================================
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
+    #[test]
+    fn substitution_preserves_arity(
+        pred in predicate_strategy(),
+        vars in prop::collection::vec(variable_strategy(), 1..4),
+        replacement in constant_strategy()
+    ) {
+        let atom = Atom::new(
+            &pred,
+            vars.iter().map(|v| Term::var(v)).collect(),
+        );
+
+        let mut subst = Substitution::new();
+        for var in &vars {
+            subst.bind(var.clone(), Term::constant(&replacement));
+        }
+
+        let result = subst.apply_atom(&atom);
+
+        prop_assert_eq!(result.arity(), atom.arity());
+        prop_assert_eq!(result.predicate, atom.predicate);
+    }
+}