aprender-contracts 0.34.0

//! Kani bounded proof harnesses for kernel contracts.
//!
//! This module contains 45 `#[kani::proof]` harnesses that promote key
//! properties from Level 3 (statistically tested via proptest) to Level 4
//! (bounded mathematical proof for ALL inputs up to size N).
//!
//! All code here is behind `#[cfg(kani)]` and invisible to normal builds.

use super::activation;
use super::adamw;
use super::attention;
use super::batchnorm;
use super::cma_es;
use super::conv1d;
use super::cross_entropy;
use super::flash_attention;
use super::gated_delta_net;
use super::gqa;
use super::kmeans;
use super::layernorm;
use super::lbfgs;
use super::matmul;
use super::pagerank;
use super::rmsnorm;
use super::rope;
use super::silu_standalone;
use super::softmax;
use super::ssm;
use super::swiglu;

// ════════════════════════════════════════════════════════════════════════════
// Float transcendental stubs
// ════════════════════════════════════════════════════════════════════════════

/// Stub for `f32::exp` — models exp(x) for softmax after max-subtraction.
///
/// Softmax calls exp(x_i - max(x)), where x_i - max(x) ∈ (-∞, 0].
/// Therefore exp returns values in (0, 1]. The element where x_i = max(x)
/// gets exp(0) = 1.0 exactly. All others get values in (0, 1).
///
/// Soundness:
/// - Lean proves exp(x) > 0 for all x ∈ ℝ (Real.exp_pos)
/// - Lean proves exp(0) = 1 (Real.exp_zero)
/// - The upper bound 1.0 follows from x_i - max(x) ≤ 0 → exp(·) ≤ 1
fn stub_exp(_x: f32) -> f32 {
    let r: f32 = kani::any();
    // exp(x - max(x)) for x - max(x) ∈ [-88, 0] gives values in [exp(-88), 1].
    // exp(-88) ≈ 6e-39 > f32::MIN_POSITIVE (1.175e-38 is normal).
    // Exclude subnormals to prevent 1/sum overflow.
    kani::assume(r >= f32::MIN_POSITIVE && r <= 1.0);
    r
}

/// Stub for `f32::sqrt` — returns an arbitrary non-negative finite value.
fn stub_sqrt(_x: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r >= 0.0 && r.is_finite());
    r
}

/// Stub for `f32::ln` — returns an arbitrary finite value.
fn stub_ln(_x: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r.is_finite());
    r
}

/// Stub for `f32::sin` — returns a value in [-1, 1].
fn stub_sin(_x: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r >= -1.0 && r <= 1.0);
    r
}

/// Stub for `f32::cos` — returns a value in [-1, 1].
fn stub_cos(_x: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r >= -1.0 && r <= 1.0);
    r
}

/// Stub for `f32::tanh` — returns a value in (-1, 1).
fn stub_tanh(_x: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r > -1.0 && r < 1.0 && r.is_finite());
    r
}

/// Stub for `f32::powf` — returns an arbitrary positive finite value.
fn stub_powf(_base: f32, _exp: f32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r > 0.0 && r.is_finite());
    r
}

/// Stub for `f32::powi` — returns an arbitrary finite value.
fn stub_powi(_base: f32, _exp: i32) -> f32 {
    let r: f32 = kani::any();
    kani::assume(r.is_finite());
    r
}

// Group A (Activation) + Group B (Normalization): 14 harnesses
include!("kani_proofs_ab.rs");

// Group C (Gated + Positional + Loss) + Group D (Matrix + Attention): 14 harnesses
include!("kani_proofs_cd.rs");

// Group E1 (Optimizer + Sequence): 7 harnesses
include!("kani_proofs_e1.rs");

// Group E2 (Classical ML): 10 harnesses
include!("kani_proofs_e2.rs");