koala_core/invariant/
property.rs

1//! Property-based invariants. Property tests differ from the static
2//! `Invariant` trait: they take a model + an operation generator and
3//! search for a counter-example. When one is found, [`PropertyResult`]
4//! captures the failing input + a reproduce seed and persists it to
5//! `.koala/cache/invariants/<id>.json` so subsequent runs can replay
6//! the exact failure.
7
8use std::fs;
9use std::io;
10use std::path::{Path, PathBuf};
11
12const CACHE_DIR: &str = ".koala/cache/invariants";
13
14#[derive(Debug, Clone, PartialEq, Eq)]
15pub enum PropertyResult {
16    Pass {
17        cases_run: u32,
18    },
19    Fail {
20        seed: String,
21        counter_example: String,
22    },
23}
24
25#[derive(Debug)]
26pub enum PersistError {
27    Io(io::Error),
28}
29
30impl std::fmt::Display for PersistError {
31    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
32        match self {
33            Self::Io(e) => write!(f, "io: {e}"),
34        }
35    }
36}
37
38impl std::error::Error for PersistError {}
39
40pub fn persist_counter_example(
41    repo_root: &Path,
42    invariant_id: &str,
43    seed: &str,
44    counter_example: &str,
45) -> Result<PathBuf, PersistError> {
46    let dir = repo_root.join(CACHE_DIR);
47    fs::create_dir_all(&dir).map_err(PersistError::Io)?;
48    let path = dir.join(format!("{invariant_id}.json"));
49    let body = format!(
50        "{{\n  \"invariant\": \"{invariant_id}\",\n  \"seed\": {seed:?},\n  \"counter_example\": {counter_example:?}\n}}\n"
51    );
52    fs::write(&path, body).map_err(PersistError::Io)?;
53    Ok(path)
54}
55
56pub fn persisted_path(repo_root: &Path, invariant_id: &str) -> Option<PathBuf> {
57    let p = repo_root
58        .join(CACHE_DIR)
59        .join(format!("{invariant_id}.json"));
60    p.is_file().then_some(p)
61}
62
63#[cfg(test)]
64mod tests {
65    use super::*;
66    use proptest::prelude::*;
67    use tempfile::TempDir;
68
69    /// Sample business invariant: starting from balance = 0, applying
70    /// any sequence of `(deposit | withdraw)` ops where every withdraw
71    /// is bounded by the running balance must leave the balance ≥ 0.
72    fn balance_non_negative(ops: &[(bool, u32)]) -> bool {
73        let mut bal: i64 = 0;
74        for &(is_deposit, amount) in ops {
75            if is_deposit {
76                bal += amount as i64;
77            } else {
78                let amt = (amount as i64).min(bal); // bounded withdraw
79                bal -= amt;
80            }
81        }
82        bal >= 0
83    }
84
85    proptest! {
86        #[test]
87        fn balance_holds(ops in prop::collection::vec((any::<bool>(), 0u32..1_000_000), 0..50)) {
88            prop_assert!(balance_non_negative(&ops));
89        }
90    }
91
92    /// Buggy variant that doesn't bound withdraws — proptest should
93    /// shrink to a small failing case.
94    fn balance_non_negative_buggy(ops: &[(bool, u32)]) -> bool {
95        let mut bal: i64 = 0;
96        for &(is_deposit, amount) in ops {
97            if is_deposit {
98                bal += amount as i64;
99            } else {
100                bal -= amount as i64; // unbounded — bug
101            }
102        }
103        bal >= 0
104    }
105
106    #[test]
107    fn counter_example_persisted() {
108        // Drive a manual property loop so we can intercept the failure
109        // and persist a counter-example without the test binary
110        // exiting.
111        let mut runner = proptest::test_runner::TestRunner::deterministic();
112        let strategy = prop::collection::vec((any::<bool>(), 0u32..1_000_000), 0..10);
113        let result = runner.run(&strategy, |ops| {
114            prop_assert!(balance_non_negative_buggy(&ops));
115            Ok(())
116        });
117        let err = result.expect_err("buggy invariant must fail under proptest");
118        let seed = format!("{:?}", runner.rng());
119        let counter_example = format!("{err:?}");
120
121        let tmp = TempDir::new().unwrap();
122        let path = persist_counter_example(
123            tmp.path(),
124            "business.balance-non-negative",
125            &seed,
126            &counter_example,
127        )
128        .unwrap();
129
130        assert!(path.is_file());
131        assert!(
132            path.ends_with(".koala/cache/invariants/business.balance-non-negative.json"),
133            "path was {}",
134            path.display()
135        );
136        let body = fs::read_to_string(&path).unwrap();
137        assert!(body.contains("\"invariant\": \"business.balance-non-negative\""));
138        assert!(body.contains("\"seed\""));
139        assert!(body.contains("\"counter_example\""));
140
141        // Round-trip helper.
142        assert_eq!(
143            persisted_path(tmp.path(), "business.balance-non-negative").as_deref(),
144            Some(path.as_path())
145        );
146    }
147}
koala_core/invariant/property.rs

koala_core/invariant/
property.rs
