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
152
153
154
155
156
157
158
159
160
//! FALSIFY contract tests for ranking metrics
//!
//! Verifies invariants of hit_at_k, reciprocal_rank, mrr, and ndcg_at_k
//! using property-based testing (proptest).
// CONTRACT: ranking-metrics-v1.yaml
// HASH: sha256:b4c5d6e7f8091a23
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use aprender::metrics::ranking::{hit_at_k, mrr, ndcg_at_k};
use proptest::prelude::*;
proptest! {
#![proptest_config(ProptestConfig::with_cases(256))]
// ──────────────────────────────────────────────────────────
// FALSIFY-RANK-001: hit_at_k returns exactly 0.0 or 1.0 (binary)
// Formal: hit_at_k(preds, target, k) ∈ {0.0, 1.0}
// ──────────────────────────────────────────────────────────
/// Obligation: hit_at_k is a binary indicator function
#[test]
fn prop_hit_at_k_binary(
n in 1usize..20,
target in 0i32..100,
k in 1usize..20,
seed in 0u64..10000,
) {
// Build predictions using LCG for deterministic pseudo-randomness
let mut rng = seed;
let predictions: Vec<i32> = (0..n).map(|_| {
rng = rng.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(1);
(rng >> 33) as i32 % 100
}).collect();
let k_clamped = k.min(predictions.len());
let score = hit_at_k(&predictions, &target, k_clamped);
prop_assert!(
score == 0.0 || score == 1.0,
"FALSIFY-RANK-001: hit_at_k={}, expected 0.0 or 1.0 (preds len={}, target={}, k={})",
score, predictions.len(), target, k_clamped
);
}
// ──────────────────────────────────────────────────────────
// FALSIFY-RANK-002: NDCG@K in [0, 1] for non-negative relevance
// Formal: ndcg_at_k(rel, k) ∈ [0, 1] when all rel_i >= 0
// ──────────────────────────────────────────────────────────
/// Obligation: NDCG is bounded in [0, 1] for non-negative relevance scores
#[test]
fn prop_ndcg_bounded(
n in 1usize..20,
k in 1usize..20,
seed in 0u64..10000,
) {
// Generate non-negative relevance scores in [0, 5) using LCG
let mut rng = seed;
let relevance: Vec<f32> = (0..n).map(|_| {
rng = rng.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(1);
// Map to [0.0, 5.0) range
((rng >> 33) as f32 / u32::MAX as f32) * 5.0
}).collect();
let k_clamped = k.min(relevance.len());
let score = ndcg_at_k(&relevance, k_clamped);
prop_assert!(
score >= 0.0,
"FALSIFY-RANK-002: ndcg_at_k={}, expected >= 0.0 (n={}, k={})",
score, n, k_clamped
);
prop_assert!(
score <= 1.0 + 1e-6,
"FALSIFY-RANK-002: ndcg_at_k={}, expected <= 1.0 (n={}, k={})",
score, n, k_clamped
);
}
// ──────────────────────────────────────────────────────────
// FALSIFY-RANK-003: MRR in [0, 1] for valid queries
// Formal: mrr(preds_list, targets) ∈ [0, 1]
// ──────────────────────────────────────────────────────────
/// Obligation: Mean Reciprocal Rank is bounded in [0, 1]
#[test]
fn prop_mrr_bounded(
n_queries in 2usize..5,
seed in 0u64..10000,
) {
// Generate 2-5 queries, each with 3-10 predictions
let mut rng = seed;
let mut next_rng = || -> u64 {
rng = rng.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(1);
rng >> 33
};
let mut predictions_list: Vec<Vec<i32>> = Vec::with_capacity(n_queries);
let mut targets: Vec<i32> = Vec::with_capacity(n_queries);
for _ in 0..n_queries {
let n_preds = 3 + (next_rng() as usize % 8); // 3..10
let preds: Vec<i32> = (0..n_preds)
.map(|_| (next_rng() as i32) % 50)
.collect();
let target = (next_rng() as i32) % 50;
predictions_list.push(preds);
targets.push(target);
}
let score = mrr(&predictions_list, &targets);
prop_assert!(
score >= 0.0,
"FALSIFY-RANK-003: mrr={}, expected >= 0.0 (n_queries={})",
score, n_queries
);
prop_assert!(
score <= 1.0 + 1e-6,
"FALSIFY-RANK-003: mrr={}, expected <= 1.0 (n_queries={})",
score, n_queries
);
}
// ──────────────────────────────────────────────────────────
// FALSIFY-RANK-004: Perfect ranking yields NDCG = 1.0
// Formal: ndcg_at_k(sorted_desc(rel), k) = 1.0
// ──────────────────────────────────────────────────────────
/// Obligation: Sorted-descending relevance achieves perfect NDCG
#[test]
fn prop_perfect_ranking_ndcg_one(
n in 2usize..20,
k in 1usize..20,
seed in 0u64..10000,
) {
// Generate non-negative relevance scores using LCG
let mut rng = seed;
let mut relevance: Vec<f32> = (0..n).map(|_| {
rng = rng.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(1);
// Map to [0.0, 5.0) range, ensure at least some non-zero
((rng >> 33) as f32 / u32::MAX as f32) * 5.0
}).collect();
// Sort descending => ideal ranking
relevance.sort_by(|a, b| b.partial_cmp(a).unwrap_or(std::cmp::Ordering::Equal));
let k_clamped = k.min(relevance.len());
// Skip all-zero relevance (NDCG is 0/0 = 0 by convention)
let has_nonzero = relevance.iter().take(k_clamped).any(|&r| r > 0.0);
prop_assume!(has_nonzero);
let score = ndcg_at_k(&relevance, k_clamped);
prop_assert!(
(score - 1.0).abs() < 1e-5,
"FALSIFY-RANK-004: ndcg_at_k(perfect)={}, expected ~1.0 (n={}, k={})",
score, n, k_clamped
);
}
}