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
// CONTRACT: softmax-kernel-v1.yaml
// HASH: sha256:b4539665debeed0a
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use aprender::autograd::Tensor;
use aprender::nn::functional::softmax;
use proptest::prelude::*;
proptest! {
/// Obligation: Output sums to 1 (invariant)
/// Formal: |Σ σ(x)_i - 1.0| < ε
#[test]
fn prop_output_sums_to_1(
data in proptest::collection::vec(-100.0f32..100.0, 1..128usize)
) {
let n = data.len();
let x = Tensor::new(&data, &[1, n]);
let y = softmax(&x, -1);
let sum: f32 = y.data().iter().sum();
prop_assert!(
(sum - 1.0).abs() < 1e-5,
"sum={sum}, expected 1.0"
);
}
/// Obligation: All outputs strictly positive (invariant)
/// Formal: σ(x)_i > 0 for all i
/// Note: f32 underflows to 0 for extreme input differences (>~88).
/// This test uses a moderate range where f32 can represent the result.
#[test]
fn prop_all_outputs_strictly_positive(
data in proptest::collection::vec(-40.0f32..40.0, 1..128usize)
) {
let n = data.len();
let x = Tensor::new(&data, &[1, n]);
let y = softmax(&x, -1);
for (i, &val) in y.data().iter().enumerate() {
prop_assert!(
val > 0.0,
"output[{i}]={val}, expected > 0"
);
}
}
/// Obligation: Each output bounded in [0,1] (bound)
/// Formal: 0 <= σ(x)_i <= 1 for all i
/// Note: Lower bound is 0 (not strictly positive) due to f32 underflow
/// for extreme input ranges. Strict positivity tested separately above.
#[test]
fn prop_each_output_bounded_in_0_1(
data in proptest::collection::vec(-100.0f32..100.0, 1..128usize)
) {
let n = data.len();
let x = Tensor::new(&data, &[1, n]);
let y = softmax(&x, -1);
for (i, &val) in y.data().iter().enumerate() {
prop_assert!(
val >= 0.0 && val <= 1.0,
"output[{i}]={val}, expected in [0,1]"
);
}
}
/// Obligation: Order preservation (monotonicity)
/// Formal: x_i > x_j => σ(x)_i > σ(x)_j
#[test]
fn prop_order_preservation(
data in proptest::collection::vec(-50.0f32..50.0, 2..64usize)
) {
let n = data.len();
let x = Tensor::new(&data, &[1, n]);
let y = softmax(&x, -1);
let x_data = x.data();
let y_data = y.data();
for i in 0..n {
for j in 0..n {
if x_data[i] > x_data[j] {
prop_assert!(
y_data[i] >= y_data[j],
"monotonicity: x[{i}]={} > x[{j}]={} but y[{i}]={} < y[{j}]={}",
x_data[i], x_data[j], y_data[i], y_data[j]
);
}
}
}
}
/// Obligation: SIMD matches scalar within ULP (equivalence)
#[test]
#[ignore = "SIMD equivalence — trueno domain"]
fn prop_simd_matches_scalar_within_ulp(
_x in proptest::collection::vec(-100.0f32..100.0, 1..32usize)
) {
// SIMD equivalence testing is trueno's responsibility
}
/// Obligation: Translation invariance (invariant)
/// Formal: σ(x + c·1) = σ(x) for any scalar c
#[test]
fn prop_translation_invariance(
data in proptest::collection::vec(-50.0f32..50.0, 2..64usize),
c in -100.0f32..100.0
) {
let n = data.len();
let x = Tensor::new(&data, &[1, n]);
let shifted: Vec<f32> = data.iter().map(|&v| v + c).collect();
let x_shifted = Tensor::new(&shifted, &[1, n]);
let y_orig = softmax(&x, -1);
let y_shifted = softmax(&x_shifted, -1);
let orig_data = y_orig.data();
let shifted_data = y_shifted.data();
for i in 0..n {
let diff = (orig_data[i] - shifted_data[i]).abs();
prop_assert!(
diff < 1e-5,
"translation invariance: y[{i}] diff={diff}"
);
}
}
}