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
// CONTRACT: validated-tensor-v1.yaml
// HASH: sha256:c3d4e5f678901234
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
/// Compute density: fraction of non-zero elements.
fn density(data: &[f32]) -> f64 {
if data.is_empty() {
return 0.0;
}
let nonzero = data.iter().filter(|&&v| v != 0.0).count();
nonzero as f64 / data.len() as f64
}
/// Check for NaN or Inf values.
fn has_nan_inf(data: &[f32]) -> bool {
data.iter().any(|v| v.is_nan() || v.is_infinite())
}
/// Check L2 norm non-degeneracy: no all-zero rows.
fn has_zero_row(data: &[f32], cols: usize) -> bool {
if cols == 0 {
return false;
}
data.chunks(cols).any(|row| row.iter().all(|&v| v == 0.0))
}
proptest! {
/// Obligation: Density gate (bound)
/// Formal: density(E) > 0.055 for valid embeddings
#[test]
fn prop_density_gate(
data in proptest::collection::vec(-1.0f32..1.0, 64..256usize)
) {
let d = density(&data);
// Random normal data should have density near 1.0 (almost no exact zeros)
prop_assert!(
d > 0.055,
"density={}, expected > 0.055 for random normal data", d
);
}
/// Obligation: Density gate rejects sparse (bound)
/// Formal: density < 0.055 for >= 94.5% zero matrices
#[test]
fn prop_density_rejects_sparse(
n in 100usize..500,
nonzero_pct in 0u32..5 // 0-4% non-zero
) {
let nonzero_count = (n as u64 * nonzero_pct as u64 / 100) as usize;
let mut data = vec![0.0f32; n];
for i in 0..nonzero_count.min(n) {
data[i] = 1.0;
}
let d = density(&data);
if nonzero_pct < 5 {
prop_assert!(
d < 0.055,
"sparse matrix with {}% nonzero has density={}, expected < 0.055",
nonzero_pct, d
);
}
}
/// Obligation: NaN/Inf rejection (invariant)
/// Formal: count(isnan) == 0 AND count(isinf) == 0
#[test]
fn prop_nan_inf_detection(
data in proptest::collection::vec(-10.0f32..10.0, 10..100usize),
inject_pos in 0usize..10
) {
// Clean data should pass
prop_assert!(
!has_nan_inf(&data),
"clean data has NaN/Inf"
);
// NaN injection should be detected
let mut corrupted = data.clone();
let pos = inject_pos % corrupted.len();
corrupted[pos] = f32::NAN;
prop_assert!(
has_nan_inf(&corrupted),
"NaN at position {} not detected", pos
);
// Inf injection should be detected
corrupted[pos] = f32::INFINITY;
prop_assert!(
has_nan_inf(&corrupted),
"Inf at position {} not detected", pos
);
}
/// Obligation: L2 norm non-degeneracy (invariant)
/// Formal: forall row i: ||E[i,:]||_2 > 0
#[test]
fn prop_l2_norm_nondegeneracy(
rows in 2usize..16,
cols in 2usize..16
) {
// Matrix with all non-zero entries: no zero rows
let data: Vec<f32> = (0..rows * cols).map(|i| (i as f32 + 1.0) * 0.1).collect();
prop_assert!(
!has_zero_row(&data, cols),
"non-zero matrix has zero row"
);
// Matrix with one zero row: should be detected
let mut with_zero = data;
for j in 0..cols {
with_zero[j] = 0.0; // zero out first row
}
prop_assert!(
has_zero_row(&with_zero, cols),
"zero row not detected"
);
}
/// Obligation: SIMD validation equivalence (equivalence)
#[test]
#[ignore = "SIMD equivalence — trueno domain"]
fn prop_simd_equivalence(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Validation is pure math — no SIMD variant
}
}