aprender-core 0.29.2

Next-generation machine learning library in pure Rust
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

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

use proptest::prelude::*;

/// Ollama parity grade from ratio (apr_tps / ollama_tps).
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
enum OllamaGrade {
    F,
    D,
    C,
    B,
    A,
    APlus,
}

fn ollama_grade(ratio: f64) -> OllamaGrade {
    if ratio < 0.5 {
        OllamaGrade::F
    } else if ratio < 0.75 {
        OllamaGrade::D
    } else if ratio < 1.0 {
        OllamaGrade::C
    } else if ratio < 1.5 {
        OllamaGrade::B
    } else if ratio < 2.0 {
        OllamaGrade::A
    } else {
        OllamaGrade::APlus
    }
}

/// Efficiency grade from roofline utilization fraction.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
enum EfficiencyGrade {
    F,
    D,
    C,
    B,
    A,
}

fn efficiency_grade(fraction: f64) -> EfficiencyGrade {
    if fraction < 0.10 {
        EfficiencyGrade::F
    } else if fraction < 0.20 {
        EfficiencyGrade::D
    } else if fraction < 0.40 {
        EfficiencyGrade::C
    } else if fraction < 0.50 {
        EfficiencyGrade::B
    } else {
        EfficiencyGrade::A
    }
}

proptest! {
    /// Obligation: Ollama grade exhaustive (invariant)
    /// Formal: For all ratio >= 0, exactly one grade bucket matches
    #[test]
    fn prop_ollama_grade_exhaustive(
        ratio in 0.0f64..10.0
    ) {
        let grade = ollama_grade(ratio);
        // Grade should be one of the valid values
        let valid = matches!(
            grade,
            OllamaGrade::F | OllamaGrade::D | OllamaGrade::C
            | OllamaGrade::B | OllamaGrade::A | OllamaGrade::APlus
        );
        prop_assert!(valid, "invalid grade for ratio={}", ratio);

        // Verify grade matches expected bucket
        match grade {
            OllamaGrade::F => prop_assert!(ratio < 0.5, "F grade but ratio={}", ratio),
            OllamaGrade::D => prop_assert!(ratio >= 0.5 && ratio < 0.75, "D grade but ratio={}", ratio),
            OllamaGrade::C => prop_assert!(ratio >= 0.75 && ratio < 1.0, "C grade but ratio={}", ratio),
            OllamaGrade::B => prop_assert!(ratio >= 1.0 && ratio < 1.5, "B grade but ratio={}", ratio),
            OllamaGrade::A => prop_assert!(ratio >= 1.5 && ratio < 2.0, "A grade but ratio={}", ratio),
            OllamaGrade::APlus => prop_assert!(ratio >= 2.0, "A+ grade but ratio={}", ratio),
        }
    }

    /// Obligation: Ollama grade monotonic (monotonicity)
    /// Formal: r1 > r2 => grade(r1) >= grade(r2)
    #[test]
    fn prop_ollama_grade_monotonic(
        r1 in 0.0f64..10.0,
        r2 in 0.0f64..10.0
    ) {
        if r1 > r2 {
            let g1 = ollama_grade(r1);
            let g2 = ollama_grade(r2);
            prop_assert!(
                g1 >= g2,
                "not monotonic: grade({})={:?} < grade({})={:?}",
                r1, g1, r2, g2
            );
        }
    }

    /// Obligation: Efficiency grade monotonic (monotonicity)
    /// Formal: e1 > e2 => grade(e1) >= grade(e2)
    #[test]
    fn prop_efficiency_grade_monotonic(
        e1 in 0.0f64..1.0,
        e2 in 0.0f64..1.0
    ) {
        if e1 > e2 {
            let g1 = efficiency_grade(e1);
            let g2 = efficiency_grade(e2);
            prop_assert!(
                g1 >= g2,
                "not monotonic: eff_grade({})={:?} < eff_grade({})={:?}",
                e1, g1, e2, g2
            );
        }
    }

    /// Obligation: Concrete ceiling bound (bound)
    /// Formal: DDR4 33 GB/s, 4.19 GB model => ceiling in [7.0, 9.0]
    #[test]
    fn prop_concrete_ceiling(
        _dummy in 0u8..1
    ) {
        let bw_gb_s = 33.0f64;
        let model_gb = 4.19f64;
        let ceiling = bw_gb_s / model_gb;
        prop_assert!(
            ceiling >= 7.0 && ceiling <= 9.0,
            "DDR4 ceiling={} tok/s, expected [7.0, 9.0]", ceiling
        );
    }

    /// Obligation: SIMD grading equivalence (equivalence)
    #[test]
    #[ignore = "SIMD equivalence — trueno domain"]
    fn prop_simd_equivalence(
        _x in proptest::collection::vec(0u8..=255, 1..32usize)
    ) {
        // Grading is pure math — no SIMD variant
    }
}