aprender-core 0.31.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
146
147
148
149
150
151

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

use aprender::autograd::Tensor;
use proptest::prelude::*;

proptest! {
    /// Obligation: Output shape correctness (invariant)
    /// Formal: shape(A @ B) = (rows(A), cols(B))
    #[test]
    fn prop_output_shape_correctness(
        m in 1usize..8,
        p in 1usize..8,
        n in 1usize..8
    ) {
        let a_data: Vec<f32> = (0..m * p).map(|i| (i as f32) * 0.1).collect();
        let b_data: Vec<f32> = (0..p * n).map(|i| (i as f32) * 0.1).collect();

        let a = Tensor::new(&a_data, &[m, p]);
        let b = Tensor::new(&b_data, &[p, n]);
        let c = a.matmul(&b);
        let shape = c.shape();

        prop_assert_eq!(shape[0], m, "expected rows={}, got {}", m, shape[0]);
        prop_assert_eq!(shape[1], n, "expected cols={}, got {}", n, shape[1]);
    }

    /// Obligation: Matmul associativity (associativity)
    /// Formal: |(AB)C - A(BC)| < eps (within floating point)
    #[test]
    fn prop_matmul_associativity(
        data in proptest::collection::vec(-5.0f32..5.0, 75..76usize)
    ) {
        // Fixed dimensions: A[3,5], B[5,3], C[3,2]
        let m = 3;
        let p = 5;
        let n = 3;
        let q = 2;
        let total = m * p + p * n + n * q;
        if data.len() < total { return Ok(()); }

        let a = Tensor::new(&data[..m * p], &[m, p]);
        let b = Tensor::new(&data[m * p..m * p + p * n], &[p, n]);
        let c = Tensor::new(&data[m * p + p * n..total], &[n, q]);

        // (A @ B) @ C
        let ab = a.matmul(&b);
        let left = ab.matmul(&c);

        // A @ (B @ C)
        let bc = b.matmul(&c);
        let right = a.matmul(&bc);

        let left_data = left.data();
        let right_data = right.data();
        prop_assert_eq!(left_data.len(), right_data.len());
        for i in 0..left_data.len() {
            let diff = (left_data[i] - right_data[i]).abs();
            prop_assert!(
                diff < 1e-2,
                "associativity: |(AB)C - A(BC)|[{i}]={diff}"
            );
        }
    }

    /// Obligation: Matmul distributes (linearity)
    /// Formal: |A(B+C) - AB - AC| < eps
    #[test]
    fn prop_matmul_distributes(
        data in proptest::collection::vec(-5.0f32..5.0, 54..55usize)
    ) {
        // A[3,3], B[3,3], C[3,3]
        let n = 3;
        let sz = n * n;
        if data.len() < 3 * sz { return Ok(()); }

        let a = Tensor::new(&data[..sz], &[n, n]);
        let b = Tensor::new(&data[sz..2 * sz], &[n, n]);
        let c = Tensor::new(&data[2 * sz..3 * sz], &[n, n]);

        // A @ (B + C)
        let bc_sum_data: Vec<f32> = b.data().iter()
            .zip(c.data().iter())
            .map(|(x, y)| x + y)
            .collect();
        let bc_sum = Tensor::new(&bc_sum_data, &[n, n]);
        let left = a.matmul(&bc_sum);

        // A @ B + A @ C
        let ab = a.matmul(&b);
        let ac = a.matmul(&c);
        let right_data: Vec<f32> = ab.data().iter()
            .zip(ac.data().iter())
            .map(|(x, y)| x + y)
            .collect();

        let left_data = left.data();
        for i in 0..left_data.len() {
            let diff = (left_data[i] - right_data[i]).abs();
            prop_assert!(
                diff < 1e-2,
                "distributivity: |A(B+C) - AB - AC|[{i}]={diff}"
            );
        }
    }

    /// Obligation: SIMD matches scalar (equivalence)
    #[test]
    #[ignore = "SIMD equivalence — trueno domain"]
    fn prop_simd_matches_scalar(
        _x in proptest::collection::vec(-5.0f32..5.0, 1..32usize)
    ) {
        // SIMD equivalence testing is trueno's responsibility
    }

    /// Obligation: Quantized error bounded (bound)
    #[test]
    #[ignore = "Quantized dot product not yet implemented"]
    fn prop_quantized_error_bounded(
        _x in proptest::collection::vec(-5.0f32..5.0, 1..32usize)
    ) {
        // Blocked: quantized_dot not yet in aprender
    }
}

// Identity matrix tests
#[test]
fn matmul_identity_right() {
    let a = Tensor::new(&[1.0, 2.0, 3.0, 4.0f32], &[2, 2]);
    let identity = Tensor::new(&[1.0, 0.0, 0.0, 1.0f32], &[2, 2]);
    let result = a.matmul(&identity);
    let data = result.data();
    assert!((data[0] - 1.0).abs() < 1e-6);
    assert!((data[1] - 2.0).abs() < 1e-6);
    assert!((data[2] - 3.0).abs() < 1e-6);
    assert!((data[3] - 4.0).abs() < 1e-6);
}

#[test]
fn matmul_identity_left() {
    let a = Tensor::new(&[1.0, 2.0, 3.0, 4.0f32], &[2, 2]);
    let identity = Tensor::new(&[1.0, 0.0, 0.0, 1.0f32], &[2, 2]);
    let result = identity.matmul(&a);
    let data = result.data();
    assert!((data[0] - 1.0).abs() < 1e-6);
    assert!((data[1] - 2.0).abs() < 1e-6);
    assert!((data[2] - 3.0).abs() < 1e-6);
    assert!((data[3] - 4.0).abs() < 1e-6);
}