aprender-core 0.30.0

//! FALSIFY contract tests for Bayesian inference modules.
//!
//! Verifies mathematical invariants of:
//! - BetaBinomial conjugate prior (posterior positivity, mean bounds)
//! - BayesianLinearRegression (prediction finiteness, determinism)

// CONTRACT: bayesian-v1.yaml
// HASH: sha256:d5e6f7a8b9012345
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`

use aprender::bayesian::{BayesianLinearRegression, BetaBinomial};
use aprender::primitives::{Matrix, Vector};
use proptest::prelude::*;

/// Strategy: generate BLR training data with n samples and d features.
/// Returns (x_train, y_train, n_features) where x has well-conditioned values
/// and y is a simple linear function plus noise.
fn blr_training_strategy() -> impl Strategy<Value = (Matrix<f32>, Vector<f32>, usize)> {
    // n = samples (10..=20), d = features (2..=4)
    (10usize..=20, 2usize..=4)
        .prop_flat_map(|(n, d)| {
            let features = proptest::collection::vec(-5.0f32..5.0, n * d);
            let targets = proptest::collection::vec(-10.0f32..10.0, n);
            let d_val = Just(d);
            let n_val = Just(n);
            (features, targets, n_val, d_val)
        })
        .prop_map(|(features, targets, n, d)| {
            let x = Matrix::from_vec(n, d, features).expect("valid matrix dimensions");
            let y = Vector::from_vec(targets);
            (x, y, d)
        })
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    /// FALSIFY-BAYES-001: Posterior parameters remain positive after update.
    /// Formal: alpha > 0 AND beta > 0 after any valid update
    #[test]
    fn prop_posterior_parameters_positive(
        successes in 0u32..100,
        trials_extra in 0u32..100,
    ) {
        let trials = successes + trials_extra; // ensures successes <= trials
        let mut prior = BetaBinomial::uniform(); // Beta(1, 1)
        prior.update(successes, trials);

        prop_assert!(
            prior.alpha() > 0.0,
            "alpha = {}, expected > 0 after update({}, {})",
            prior.alpha(), successes, trials
        );
        prop_assert!(
            prior.beta() > 0.0,
            "beta = {}, expected > 0 after update({}, {})",
            prior.beta(), successes, trials
        );
    }

    /// FALSIFY-BAYES-002: Posterior mean in [0, 1] for BetaBinomial.
    /// Formal: 0 <= E[theta|data] <= 1
    #[test]
    fn prop_posterior_mean_bounded(
        successes in 0u32..100,
        trials_extra in 0u32..100,
    ) {
        let trials = successes + trials_extra;
        let mut prior = BetaBinomial::uniform();
        prior.update(successes, trials);

        let mean = prior.posterior_mean();

        prop_assert!(
            (0.0..=1.0).contains(&mean),
            "posterior_mean = {}, expected in [0, 1] after update({}, {})",
            mean, successes, trials
        );
        prop_assert!(
            mean.is_finite(),
            "posterior_mean = {}, expected finite after update({}, {})",
            mean, successes, trials
        );
    }

    /// FALSIFY-BAYES-003: BLR predictions are finite (no NaN/Inf).
    /// Formal: forall i: predict(X)[i].is_finite()
    #[test]
    fn prop_blr_predictions_finite(
        (x_train, y_train, d) in blr_training_strategy(),
    ) {
        let mut model = BayesianLinearRegression::new(d);
        model.fit(&x_train, &y_train).expect("fit succeeds");

        let predictions = model.predict(&x_train).expect("predict succeeds");

        for i in 0..predictions.len() {
            prop_assert!(
                predictions[i].is_finite(),
                "prediction[{}] = {}, expected finite value",
                i, predictions[i]
            );
        }
    }

    /// FALSIFY-BAYES-004: BLR predictions are deterministic (same input -> same output).
    /// Formal: predict(X) == predict(X) for same fitted model
    #[test]
    fn prop_blr_predictions_deterministic(
        (x_train, y_train, d) in blr_training_strategy(),
    ) {
        let mut model = BayesianLinearRegression::new(d);
        model.fit(&x_train, &y_train).expect("fit succeeds");

        let pred1 = model.predict(&x_train).expect("predict succeeds (1st)");
        let pred2 = model.predict(&x_train).expect("predict succeeds (2nd)");

        prop_assert!(
            pred1.len() == pred2.len(),
            "prediction lengths differ: {} vs {}",
            pred1.len(), pred2.len()
        );

        for i in 0..pred1.len() {
            let diff = (pred1[i] - pred2[i]).abs();
            prop_assert!(
                diff < 1e-6,
                "non-deterministic at [{}]: first={}, second={}, diff={}",
                i, pred1[i], pred2[i], diff
            );
        }
    }
}