koala-core 1.0.4

//! Property-based invariants. Property tests differ from the static
//! `Invariant` trait: they take a model + an operation generator and
//! search for a counter-example. When one is found, [`PropertyResult`]
//! captures the failing input + a reproduce seed and persists it to
//! `.koala/cache/invariants/<id>.json` so subsequent runs can replay
//! the exact failure.

use std::fs;
use std::io;
use std::path::{Path, PathBuf};

const CACHE_DIR: &str = ".koala/cache/invariants";

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PropertyResult {
    Pass {
        cases_run: u32,
    },
    Fail {
        seed: String,
        counter_example: String,
    },
}

#[derive(Debug)]
pub enum PersistError {
    Io(io::Error),
}

impl std::fmt::Display for PersistError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Io(e) => write!(f, "io: {e}"),
        }
    }
}

impl std::error::Error for PersistError {}

pub fn persist_counter_example(
    repo_root: &Path,
    invariant_id: &str,
    seed: &str,
    counter_example: &str,
) -> Result<PathBuf, PersistError> {
    let dir = repo_root.join(CACHE_DIR);
    fs::create_dir_all(&dir).map_err(PersistError::Io)?;
    let path = dir.join(format!("{invariant_id}.json"));
    let body = format!(
        "{{\n  \"invariant\": \"{invariant_id}\",\n  \"seed\": {seed:?},\n  \"counter_example\": {counter_example:?}\n}}\n"
    );
    fs::write(&path, body).map_err(PersistError::Io)?;
    Ok(path)
}

pub fn persisted_path(repo_root: &Path, invariant_id: &str) -> Option<PathBuf> {
    let p = repo_root
        .join(CACHE_DIR)
        .join(format!("{invariant_id}.json"));
    p.is_file().then_some(p)
}

#[cfg(test)]
mod tests {
    use super::*;
    use proptest::prelude::*;
    use tempfile::TempDir;

    /// Sample business invariant: starting from balance = 0, applying
    /// any sequence of `(deposit | withdraw)` ops where every withdraw
    /// is bounded by the running balance must leave the balance ≥ 0.
    fn balance_non_negative(ops: &[(bool, u32)]) -> bool {
        let mut bal: i64 = 0;
        for &(is_deposit, amount) in ops {
            if is_deposit {
                bal += amount as i64;
            } else {
                let amt = (amount as i64).min(bal); // bounded withdraw
                bal -= amt;
            }
        }
        bal >= 0
    }

    proptest! {
        #[test]
        fn balance_holds(ops in prop::collection::vec((any::<bool>(), 0u32..1_000_000), 0..50)) {
            prop_assert!(balance_non_negative(&ops));
        }
    }

    /// Buggy variant that doesn't bound withdraws — proptest should
    /// shrink to a small failing case.
    fn balance_non_negative_buggy(ops: &[(bool, u32)]) -> bool {
        let mut bal: i64 = 0;
        for &(is_deposit, amount) in ops {
            if is_deposit {
                bal += amount as i64;
            } else {
                bal -= amount as i64; // unbounded — bug
            }
        }
        bal >= 0
    }

    #[test]
    fn counter_example_persisted() {
        // Drive a manual property loop so we can intercept the failure
        // and persist a counter-example without the test binary
        // exiting.
        let mut runner = proptest::test_runner::TestRunner::deterministic();
        let strategy = prop::collection::vec((any::<bool>(), 0u32..1_000_000), 0..10);
        let result = runner.run(&strategy, |ops| {
            prop_assert!(balance_non_negative_buggy(&ops));
            Ok(())
        });
        let err = result.expect_err("buggy invariant must fail under proptest");
        let seed = format!("{:?}", runner.rng());
        let counter_example = format!("{err:?}");

        let tmp = TempDir::new().unwrap();
        let path = persist_counter_example(
            tmp.path(),
            "business.balance-non-negative",
            &seed,
            &counter_example,
        )
        .unwrap();

        assert!(path.is_file());
        assert!(
            path.ends_with(".koala/cache/invariants/business.balance-non-negative.json"),
            "path was {}",
            path.display()
        );
        let body = fs::read_to_string(&path).unwrap();
        assert!(body.contains("\"invariant\": \"business.balance-non-negative\""));
        assert!(body.contains("\"seed\""));
        assert!(body.contains("\"counter_example\""));

        // Round-trip helper.
        assert_eq!(
            persisted_path(tmp.path(), "business.balance-non-negative").as_deref(),
            Some(path.as_path())
        );
    }
}