aprender-core 0.31.2

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

use aprender::classification::LinearSVM;
use aprender::primitives::Matrix;
use proptest::prelude::*;

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

    // ──────────────────────────────────────────────────────────
    // FALSIFY-SVM-001: Binary prediction range
    // Formal: ∀ pred ∈ predict(X), pred ∈ {0, 1}
    // ──────────────────────────────────────────────────────────
    /// Obligation: All predictions from a binary SVM are in {0, 1}.
    #[test]
    fn prop_binary_prediction_range(
        n in 10usize..30,
        seed in 0u64..10000,
    ) {
        let d = 2usize;

        // Build pseudo-random feature data using xorshift64
        let mut rng = seed.max(1);
        let mut next_f32 = || -> f32 {
            rng ^= rng << 13;
            rng ^= rng >> 7;
            rng ^= rng << 17;
            (rng as f32 / u64::MAX as f32) * 10.0 - 5.0
        };

        let features: Vec<f32> = (0..n * d).map(|_| next_f32()).collect();
        let labels: Vec<usize> = (0..n).map(|i| i % 2).collect();

        let x = Matrix::from_vec(n, d, features).expect("valid matrix");

        let mut svm = LinearSVM::new()
            .with_c(1.0)
            .with_learning_rate(0.001)
            .with_max_iter(500);
        svm.fit(&x, &labels).expect("fit succeeds");

        let predictions = svm.predict(&x).expect("predict succeeds");

        prop_assert!(
            predictions.len() == n,
            "FALSIFY-SVM-001: predicted {} samples, expected {}", predictions.len(), n
        );

        for (i, &pred) in predictions.iter().enumerate() {
            prop_assert!(
                pred == 0 || pred == 1,
                "FALSIFY-SVM-001: prediction[{}] = {}, expected 0 or 1", i, pred
            );
        }
    }

    // ──────────────────────────────────────────────────────────
    // FALSIFY-SVM-002: Prediction deterministic
    // Formal: predict(X) = predict(X) for fitted model
    // ──────────────────────────────────────────────────────────
    /// Obligation: Predictions are deterministic given identical input.
    #[test]
    fn prop_prediction_deterministic(
        n in 10usize..30,
        seed in 0u64..10000,
    ) {
        let d = 2usize;

        let mut rng = seed.max(1);
        let mut next_f32 = || -> f32 {
            rng ^= rng << 13;
            rng ^= rng >> 7;
            rng ^= rng << 17;
            (rng as f32 / u64::MAX as f32) * 10.0 - 5.0
        };

        let features: Vec<f32> = (0..n * d).map(|_| next_f32()).collect();
        let labels: Vec<usize> = (0..n).map(|i| i % 2).collect();

        let x = Matrix::from_vec(n, d, features).expect("valid matrix");

        let mut svm = LinearSVM::new()
            .with_c(1.0)
            .with_learning_rate(0.001)
            .with_max_iter(500);
        svm.fit(&x, &labels).expect("fit succeeds");

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

        prop_assert!(
            pred1 == pred2,
            "FALSIFY-SVM-002: predictions differ between two identical calls"
        );

        // Also verify decision_function is deterministic
        let dec1 = svm.decision_function(&x).expect("decision_function succeeds (1st)");
        let dec2 = svm.decision_function(&x).expect("decision_function succeeds (2nd)");

        prop_assert!(
            dec1 == dec2,
            "FALSIFY-SVM-002: decision_function values differ between two identical calls"
        );
    }

    // ──────────────────────────────────────────────────────────
    // FALSIFY-SVM-003: Separable data accuracy > 0.9
    // Formal: accuracy(predict(X), y) > 0.9 for well-separated clusters
    // ──────────────────────────────────────────────────────────
    /// Obligation: LinearSVM achieves >90% accuracy on linearly separable data.
    #[test]
    fn prop_separable_data_high_accuracy(
        noise_scale in 0.01f32..0.5,
        seed in 0u64..10000,
    ) {
        let n_per_class = 15usize;
        let n = 2 * n_per_class;
        let d = 2usize;

        // xorshift64 for reproducible noise
        let mut rng = seed.max(1);
        let mut next_noise = || -> f32 {
            rng ^= rng << 13;
            rng ^= rng >> 7;
            rng ^= rng << 17;
            let val = (rng as f32 / u64::MAX as f32) * 2.0 - 1.0;
            val * noise_scale
        };

        let mut data = Vec::with_capacity(n * d);
        let mut labels = Vec::with_capacity(n);

        // Cluster 0 centered at (-5, -5)
        for _ in 0..n_per_class {
            data.push(-5.0 + next_noise());
            data.push(-5.0 + next_noise());
            labels.push(0);
        }
        // Cluster 1 centered at (5, 5)
        for _ in 0..n_per_class {
            data.push(5.0 + next_noise());
            data.push(5.0 + next_noise());
            labels.push(1);
        }

        let x = Matrix::from_vec(n, d, data).expect("valid matrix");

        let mut svm = LinearSVM::new()
            .with_c(1.0)
            .with_learning_rate(0.001)
            .with_max_iter(2000);
        svm.fit(&x, &labels).expect("fit succeeds");

        let predictions = svm.predict(&x).expect("predict succeeds");

        let correct: usize = predictions
            .iter()
            .zip(labels.iter())
            .filter(|(&pred, &actual)| pred == actual)
            .count();
        let accuracy = correct as f32 / n as f32;

        prop_assert!(
            accuracy > 0.9,
            "FALSIFY-SVM-003: accuracy = {} ({}/{}), expected > 0.9 with noise_scale={}",
            accuracy, correct, n, noise_scale
        );
    }

    // ──────────────────────────────────────────────────────────
    // FALSIFY-SVM-004: Fit-predict consistency
    // Formal: ∀ pred ∈ predict(X), pred ∈ {labels seen during fit}
    // ──────────────────────────────────────────────────────────
    /// Obligation: Predictions only contain labels from the training set.
    #[test]
    fn prop_fit_predict_consistency(
        n in 10usize..30,
        seed in 0u64..10000,
    ) {
        let d = 2usize;

        let mut rng = seed.max(1);
        let mut next_f32 = || -> f32 {
            rng ^= rng << 13;
            rng ^= rng >> 7;
            rng ^= rng << 17;
            (rng as f32 / u64::MAX as f32) * 10.0 - 5.0
        };

        let features: Vec<f32> = (0..n * d).map(|_| next_f32()).collect();
        let labels: Vec<usize> = (0..n).map(|i| i % 2).collect();

        let x = Matrix::from_vec(n, d, features).expect("valid matrix");

        let mut svm = LinearSVM::new()
            .with_c(1.0)
            .with_learning_rate(0.001)
            .with_max_iter(500);
        svm.fit(&x, &labels).expect("fit succeeds");

        // Build unique training label set
        let mut train_labels: Vec<usize> = labels.clone();
        train_labels.sort_unstable();
        train_labels.dedup();

        let predictions = svm.predict(&x).expect("predict succeeds");

        prop_assert!(
            predictions.len() == n,
            "FALSIFY-SVM-004: predicted {} samples, expected {}", predictions.len(), n
        );

        for (i, &pred) in predictions.iter().enumerate() {
            prop_assert!(
                train_labels.contains(&pred),
                "FALSIFY-SVM-004: prediction[{}] = {}, not in training labels {:?}",
                i, pred, train_labels
            );
        }
    }
}