aprender-core 0.31.2

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

use proptest::prelude::*;

/// Compute bandwidth ceiling: tokens/second limited by memory bandwidth.
/// bw_ceiling = effective_bandwidth_GB_s / (model_bytes / 1e9)
fn bandwidth_ceiling(effective_bw_gb_s: f64, model_bytes: u64) -> f64 {
    effective_bw_gb_s / (model_bytes as f64 / 1e9)
}

/// Compute compute ceiling: tokens/second limited by compute throughput.
/// compute_ceiling = effective_gflops * 1e9 / ops_per_token
fn compute_ceiling(effective_gflops: f64, ops_per_token: u64) -> f64 {
    effective_gflops * 1e9 / ops_per_token as f64
}

/// Compute model bytes from params and quantization.
fn model_bytes(total_params: u64, bits_per_weight: u32) -> u64 {
    total_params * u64::from(bits_per_weight) / 8
}

proptest! {
    /// Obligation: Ceilings positive (bound)
    /// Formal: bw_ceiling > 0 ∧ compute_ceiling > 0 for valid inputs
    #[test]
    fn prop_ceiling_positive(
        bw_gb_s in 1.0f64..2000.0,        // 1 GB/s to 2 TB/s
        gflops in 1.0f64..1000.0,          // 1 GFLOPS to 1 TFLOPS
        params in 1_000u64..100_000_000_000, // 1K to 100B params
        bits in prop::sample::select(vec![2u32, 4, 8, 16, 32]),
        ops in 1_000u64..1_000_000_000     // 1K to 1B ops/token
    ) {
        let mb = model_bytes(params, bits);
        prop_assert!(mb > 0, "model_bytes must be > 0");

        let bw_ceil = bandwidth_ceiling(bw_gb_s, mb);
        prop_assert!(
            bw_ceil > 0.0 && bw_ceil.is_finite(),
            "bandwidth ceiling={}, expected > 0 and finite", bw_ceil
        );

        let compute_ceil = compute_ceiling(gflops, ops);
        prop_assert!(
            compute_ceil > 0.0 && compute_ceil.is_finite(),
            "compute ceiling={}, expected > 0 and finite", compute_ceil
        );
    }

    /// Obligation: Memory-bound classification (invariant)
    /// Formal: bw_ceiling < compute_ceiling ⟹ system is memory-bound
    #[test]
    fn prop_memory_bound_classification(
        bw_gb_s in 1.0f64..2000.0,
        gflops in 1.0f64..1000.0,
        params in 1_000_000u64..10_000_000_000,
        bits in prop::sample::select(vec![4u32, 8, 16]),
        ops in 100_000u64..100_000_000
    ) {
        let mb = model_bytes(params, bits);
        let bw_ceil = bandwidth_ceiling(bw_gb_s, mb);
        let compute_ceil = compute_ceiling(gflops, ops);

        let is_memory_bound = bw_ceil < compute_ceil;
        let bottleneck = bw_ceil.min(compute_ceil);

        // The bottleneck must equal the lower ceiling
        if is_memory_bound {
            prop_assert!(
                (bottleneck - bw_ceil).abs() < 1e-6,
                "memory-bound but bottleneck={} != bw_ceil={}", bottleneck, bw_ceil
            );
        } else {
            prop_assert!(
                (bottleneck - compute_ceil).abs() < 1e-6,
                "compute-bound but bottleneck={} != compute_ceil={}", bottleneck, compute_ceil
            );
        }
    }

    /// Obligation: Throughput bounded (bound)
    /// Formal: throughput <= min(bw_ceiling, compute_ceiling)
    #[test]
    fn prop_throughput_bounded(
        bw_gb_s in 1.0f64..2000.0,
        gflops in 1.0f64..1000.0,
        params in 1_000_000u64..10_000_000_000,
        bits in prop::sample::select(vec![4u32, 8, 16]),
        ops in 100_000u64..100_000_000,
        // Any claimed throughput
        throughput_factor in 0.0f64..2.0
    ) {
        let mb = model_bytes(params, bits);
        let bw_ceil = bandwidth_ceiling(bw_gb_s, mb);
        let compute_ceil = compute_ceiling(gflops, ops);
        let max_throughput = bw_ceil.min(compute_ceil);

        // Scale throughput relative to max
        let claimed = throughput_factor * max_throughput;

        // Valid throughput must not exceed both ceilings
        if claimed > max_throughput {
            prop_assert!(
                claimed > bw_ceil || claimed > compute_ceil,
                "throughput {} exceeds max {} but doesn't violate any ceiling",
                claimed, max_throughput
            );
        }
    }

    /// Obligation: Model bytes monotonic (monotonicity)
    /// Formal: more params (same quant) → more bytes → lower bw ceiling
    #[test]
    fn prop_model_bytes_monotonic(
        bw_gb_s in 10.0f64..1000.0,
        params1 in 1_000_000u64..1_000_000_000,
        extra in 1u64..1_000_000_000,
        bits in prop::sample::select(vec![4u32, 8, 16, 32])
    ) {
        let params2 = params1.saturating_add(extra);
        let mb1 = model_bytes(params1, bits);
        let mb2 = model_bytes(params2, bits);

        // More params → more bytes
        prop_assert!(
            mb2 >= mb1,
            "model_bytes not monotonic: params1={}->bytes={}, params2={}->bytes={}",
            params1, mb1, params2, mb2
        );

        // More bytes → lower bandwidth ceiling (if bytes differ)
        if mb2 > mb1 {
            let ceil1 = bandwidth_ceiling(bw_gb_s, mb1);
            let ceil2 = bandwidth_ceiling(bw_gb_s, mb2);
            prop_assert!(
                ceil2 <= ceil1,
                "bandwidth ceiling not monotonically decreasing: ceil1={}, ceil2={}",
                ceil1, ceil2
            );
        }
    }

    /// Obligation: SIMD roofline equivalence (equivalence)
    #[test]
    #[ignore = "SIMD equivalence — trueno domain"]
    fn prop_simd_equivalence(
        _x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
    ) {
        // Roofline is pure math — no SIMD variant
    }
}