aprender-contracts 0.34.0

// ════════════════════════════════════════════════════════════════════════════
// Group E2 — Classical ML (10 harnesses: KM x2, PR x2, LB x2, CMA x2, GDN x2)
// ════════════════════════════════════════════════════════════════════════════

/// KANI-KM-001: K-means assigns each point to its nearest centroid.
/// Obligation: KM-INV-001
/// Strategy: stub_float
/// Bound: 4 points, 2 centroids, 2 dims
#[kani::proof]
#[kani::unwind(5)]
fn verify_kmeans_nearest() {
    const N_POINTS: usize = 4;
    const K: usize = 2;
    const D: usize = 2;

    let points: [f32; N_POINTS * D] = kani::any();
    let centroids: [f32; K * D] = kani::any();
    kani::assume(points.iter().all(|v| v.is_finite()));
    kani::assume(centroids.iter().all(|v| v.is_finite()));

    let mut assignments = [0u32; N_POINTS];
    kmeans::kmeans_assign_scalar(&points, &centroids, N_POINTS, K, D, &mut assignments);

    // Verify each point is assigned to the nearest centroid
    for p in 0..N_POINTS {
        let assigned = assignments[p] as usize;
        assert!(assigned < K, "KANI-KM-001: assignment out of range");

        // Distance to assigned centroid
        let mut d_assigned = 0.0f32;
        for j in 0..D {
            let diff = points[p * D + j] - centroids[assigned * D + j];
            d_assigned += diff * diff;
        }

        // Verify it's <= distance to all other centroids
        for c in 0..K {
            let mut d_c = 0.0f32;
            for j in 0..D {
                let diff = points[p * D + j] - centroids[c * D + j];
                d_c += diff * diff;
            }
            assert!(
                d_assigned <= d_c,
                "KANI-KM-001: point {} not nearest: d(assigned)={} > d({})={}",
                p,
                d_assigned,
                c,
                d_c
            );
        }
    }
}

/// KANI-KM-002: K-means objective (total squared distance) is non-negative.
/// Obligation: KM-INV-002
/// Strategy: stub_float
/// Bound: 4 points, 2 centroids, 2 dims
#[kani::proof]
#[kani::unwind(5)]
fn verify_kmeans_objective_nonneg() {
    const N_POINTS: usize = 4;
    const K: usize = 2;
    const D: usize = 2;

    let points: [f32; N_POINTS * D] = kani::any();
    let centroids: [f32; K * D] = kani::any();
    kani::assume(points.iter().all(|v| v.is_finite()));
    kani::assume(centroids.iter().all(|v| v.is_finite()));

    let mut assignments = [0u32; N_POINTS];
    kmeans::kmeans_assign_scalar(&points, &centroids, N_POINTS, K, D, &mut assignments);

    // Compute objective: sum of squared distances to assigned centroids
    let mut objective = 0.0f32;
    for p in 0..N_POINTS {
        let c = assignments[p] as usize;
        for j in 0..D {
            let diff = points[p * D + j] - centroids[c * D + j];
            objective += diff * diff;
        }
    }

    assert!(
        objective >= 0.0,
        "KANI-KM-002: objective = {} < 0",
        objective
    );
}

/// KANI-PR-001: PageRank output sums to approximately 1.
/// Obligation: PR-INV-001
/// Strategy: stub_float
/// Bound: n=4
#[kani::proof]
#[kani::unwind(5)]
fn verify_pagerank_distribution() {
    const N: usize = 4;

    // Build a row-stochastic transition matrix (each row sums to 1)
    // Use uniform transition for tractability
    let transition = [1.0 / N as f32; N * N];
    let rank = [1.0 / N as f32; N];

    let damping: f32 = kani::any();
    kani::assume(damping > 0.0 && damping < 1.0 && damping.is_finite());

    let mut output = [0.0f32; N];
    pagerank::pagerank_iterate_scalar(&transition, &rank, N, damping, &mut output);

    let sum: f32 = output.iter().sum();
    // With uniform transition and uniform rank, output should sum to 1
    assert!(
        (sum - 1.0).abs() < 1e-4,
        "KANI-PR-001: sum = {}, expected ~1.0",
        sum
    );
}

/// KANI-PR-002: PageRank outputs are all non-negative.
/// Obligation: PR-INV-002
/// Strategy: stub_float
/// Bound: n=4
#[kani::proof]
#[kani::unwind(5)]
fn verify_pagerank_nonneg() {
    const N: usize = 4;

    let transition: [f32; N * N] = kani::any();
    let rank: [f32; N] = kani::any();
    kani::assume(transition.iter().all(|x| *x >= 0.0 && x.is_finite()));
    kani::assume(rank.iter().all(|x| *x >= 0.0 && x.is_finite()));

    let damping: f32 = kani::any();
    kani::assume(damping >= 0.0 && damping <= 1.0 && damping.is_finite());

    let mut output = [0.0f32; N];
    pagerank::pagerank_iterate_scalar(&transition, &rank, N, damping, &mut output);

    for i in 0..N {
        assert!(
            output[i] >= 0.0,
            "KANI-PR-002: output[{}] = {} < 0",
            i,
            output[i]
        );
    }
}

/// KANI-LB-001: L-BFGS direction is a descent direction: dot(dir, grad) < 0.
/// Obligation: LB-INV-001
/// Strategy: stub_float
/// Bound: d=4, m=0 (steepest descent case)
#[kani::proof]
#[kani::unwind(5)]
fn verify_lbfgs_descent() {
    const D: usize = 4;

    let gradient: [f32; D] = kani::any();
    kani::assume(gradient.iter().all(|x| x.is_finite()));
    // Ensure gradient is non-zero
    kani::assume(gradient.iter().any(|x| x.abs() > 1e-6));

    let s_history: [f32; 0] = [];
    let y_history: [f32; 0] = [];

    let mut direction = [0.0f32; D];
    lbfgs::lbfgs_direction_scalar(&gradient, &s_history, &y_history, 0, D, &mut direction);

    // With m=0, direction = -gradient, so dot(direction, gradient) = -||gradient||^2 < 0
    let mut dot = 0.0f32;
    for j in 0..D {
        dot += direction[j] * gradient[j];
    }

    assert!(dot < 0.0, "KANI-LB-001: dot(dir, grad) = {} >= 0", dot);
}

/// KANI-LB-002: L-BFGS history access is bounded (no OOB).
/// Obligation: LB-INV-002
/// Strategy: exhaustive
/// Bound: d=4, m=2
#[kani::proof]
#[kani::unwind(9)]
fn verify_lbfgs_history_bound() {
    const D: usize = 4;
    const M: usize = 2;

    let gradient: [f32; D] = kani::any();
    let s_history: [f32; M * D] = kani::any();
    let y_history: [f32; M * D] = kani::any();
    kani::assume(gradient.iter().all(|x| x.is_finite()));
    kani::assume(s_history.iter().all(|x| x.is_finite()));
    kani::assume(y_history.iter().all(|x| x.is_finite()));

    let mut direction = [0.0f32; D];
    // This should not panic (no OOB access)
    lbfgs::lbfgs_direction_scalar(&gradient, &s_history, &y_history, M, D, &mut direction);

    for j in 0..D {
        assert!(
            direction[j].is_finite(),
            "KANI-LB-002: direction[{}] not finite",
            j
        );
    }
}

/// KANI-CMA-001: CMA-ES sigma remains positive (structural preservation).
/// Obligation: CMA-INV-001
/// Strategy: stub_float
/// Bound: d=4
#[kani::proof]
#[kani::unwind(5)]
fn verify_cma_sigma_positive() {
    const D: usize = 4;

    let mean: [f32; D] = kani::any();
    let z: [f32; D] = kani::any();
    kani::assume(mean.iter().all(|x| x.is_finite()));
    kani::assume(z.iter().all(|x| x.is_finite()));

    let sigma: f32 = kani::any();
    kani::assume(sigma > 0.0 && sigma.is_finite());

    // Identity Cholesky factor (L = I)
    let mut cholesky_l = [0.0f32; D * D];
    for i in 0..D {
        cholesky_l[i * D + i] = 1.0;
    }

    let mut output = [0.0f32; D];
    cma_es::cma_sample_scalar(&mean, sigma, &cholesky_l, D, &z, &mut output);

    // The sample is mean + sigma * L * z, sigma is passed in positive,
    // and the function doesn't modify sigma. We verify the output is finite.
    for i in 0..D {
        assert!(
            output[i].is_finite(),
            "KANI-CMA-001: output[{}] not finite",
            i
        );
    }
    // sigma is unchanged (it's passed by value)
    assert!(sigma > 0.0, "KANI-CMA-001: sigma = {} <= 0", sigma);
}

/// KANI-CMA-002: CMA-ES recombination weights sum to 1 (structural test).
/// Obligation: CMA-INV-002
/// Strategy: stub_float
/// Bound: 8 weights
/// This is an abstract verification: weights normalized to sum 1.
#[kani::proof]
#[kani::unwind(9)]
fn verify_cma_weights_normalized() {
    const N: usize = 8;

    let raw_weights: [f32; N] = kani::any();
    kani::assume(raw_weights.iter().all(|x| *x > 0.0 && x.is_finite()));

    // Normalize weights
    let sum: f32 = raw_weights.iter().sum();
    kani::assume(sum > 0.0 && sum.is_finite());

    let mut normalized = [0.0f32; N];
    for i in 0..N {
        normalized[i] = raw_weights[i] / sum;
    }

    let norm_sum: f32 = normalized.iter().sum();
    assert!(
        (norm_sum - 1.0).abs() < 1e-4,
        "KANI-CMA-002: sum = {}, expected ~1.0",
        norm_sum
    );
}

/// KANI-GDN-001: Sigmoid decay gate output is in (0, 1).
/// Obligation: GDN-INV-001
/// Strategy: stub_float
/// Bound: 8 elements
/// Inlines the sigmoid computation.
#[kani::proof]
#[kani::unwind(9)]
#[kani::stub(f32::exp, stub_exp)]
fn verify_decay_bound() {
    const N: usize = 8;
    let x: [f32; N] = kani::any();
    kani::assume(x.iter().all(|v| v.is_finite()));

    // sigmoid(x) = 1 / (1 + exp(-x))
    // With stub_exp returning r > 0: sigmoid = 1/(1+r), which is in (0, 1)
    for i in 0..N {
        let exp_neg_x = stub_exp(-x[i]);
        let sigmoid = 1.0 / (1.0 + exp_neg_x);
        assert!(
            sigmoid > 0.0 && sigmoid < 1.0,
            "KANI-GDN-001: sigmoid(x[{}]) = {} not in (0, 1)",
            i,
            sigmoid
        );
    }
}

/// KANI-GDN-002: GDN output shape is preserved (seq_len x v_dim).
/// Obligation: GDN-INV-002
/// Strategy: bounded_int
/// Bound: seq_len=2, k_dim=2, v_dim=2
#[kani::proof]
#[kani::unwind(5)]
fn verify_state_shape_preserved() {
    const SEQ_LEN: usize = 2;
    const K_DIM: usize = 2;
    const V_DIM: usize = 2;

    let q: [f32; SEQ_LEN * K_DIM] = kani::any();
    let k: [f32; SEQ_LEN * K_DIM] = kani::any();
    let v: [f32; SEQ_LEN * V_DIM] = kani::any();
    let alpha: [f32; SEQ_LEN] = kani::any();
    let beta: [f32; SEQ_LEN] = kani::any();
    kani::assume(q.iter().all(|x| x.is_finite()));
    kani::assume(k.iter().all(|x| x.is_finite()));
    kani::assume(v.iter().all(|x| x.is_finite()));
    kani::assume(alpha.iter().all(|x| x.is_finite()));
    kani::assume(beta.iter().all(|x| x.is_finite()));

    let mut output = [0.0f32; SEQ_LEN * V_DIM];
    gated_delta_net::gdn_recurrence_scalar(
        &q,
        &k,
        &v,
        &alpha,
        &beta,
        SEQ_LEN,
        K_DIM,
        V_DIM,
        &mut output,
    );

    // Verify output shape is correct (SEQ_LEN * V_DIM elements, all finite)
    for i in 0..output.len() {
        assert!(
            output[i].is_finite(),
            "KANI-GDN-002: output[{}] not finite",
            i
        );
    }
}