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
//! FALSIFY contract tests for ARIMA time series model.
//!
//! Verifies mathematical invariants of ARIMA(p,d,q) forecasting:
//! - Forecast length equals requested periods
//! - All forecast values are finite (no NaN/Inf)
//! - Fit-forecast is deterministic
//! - Constant input produces near-constant forecast
// CONTRACT: arima-v1.yaml
// HASH: sha256:c4d5e6f7a8b90123
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use aprender::primitives::Vector;
use aprender::time_series::ARIMA;
use proptest::prelude::*;
proptest! {
#![proptest_config(ProptestConfig::with_cases(256))]
/// FALSIFY-ARIMA-001: Forecast length equals n_periods requested.
/// Formal: |forecast(n)| = n
#[test]
fn prop_forecast_length_equals_n_periods(
n_periods in 1usize..20,
data in proptest::collection::vec(-100.0f64..100.0, 30..60),
) {
// ARIMA(1, 0, 0) — simplest AR model
let mut model = ARIMA::new(1, 0, 0);
let series = Vector::from_vec(data);
model.fit(&series).expect("fit succeeds with sufficient data");
let forecast = model.forecast(n_periods).expect("forecast succeeds");
prop_assert!(
forecast.len() == n_periods,
"expected forecast length = {}, got {}",
n_periods, forecast.len()
);
}
/// FALSIFY-ARIMA-002: All forecast values are finite (no NaN/Inf).
/// Formal: forall i in 0..n: forecast[i].is_finite()
#[test]
fn prop_forecast_values_finite(
n_periods in 1usize..20,
data in proptest::collection::vec(-100.0f64..100.0, 30..60),
) {
let mut model = ARIMA::new(1, 1, 0);
let series = Vector::from_vec(data);
model.fit(&series).expect("fit succeeds");
let forecast = model.forecast(n_periods).expect("forecast succeeds");
for i in 0..forecast.len() {
prop_assert!(
forecast[i].is_finite(),
"forecast[{}] = {}, expected finite value",
i, forecast[i]
);
}
}
/// FALSIFY-ARIMA-003: Fit-forecast is deterministic (same data -> same forecast).
/// Formal: fit(X); forecast(n) == fit(X); forecast(n)
#[test]
fn prop_forecast_deterministic(
n_periods in 1usize..10,
data in proptest::collection::vec(-100.0f64..100.0, 30..60),
) {
// First fit-forecast cycle
let mut model1 = ARIMA::new(1, 0, 0);
let series = Vector::from_vec(data.clone());
model1.fit(&series).expect("fit succeeds (1st)");
let forecast1 = model1.forecast(n_periods).expect("forecast succeeds (1st)");
// Second fit-forecast cycle with identical data
let mut model2 = ARIMA::new(1, 0, 0);
let series2 = Vector::from_vec(data);
model2.fit(&series2).expect("fit succeeds (2nd)");
let forecast2 = model2.forecast(n_periods).expect("forecast succeeds (2nd)");
for i in 0..n_periods {
let diff = (forecast1[i] - forecast2[i]).abs();
prop_assert!(
diff < 1e-10,
"non-deterministic at [{}]: first={}, second={}, diff={}",
i, forecast1[i], forecast2[i], diff
);
}
}
/// FALSIFY-ARIMA-004: Constant input data -> forecast near constant value.
/// Formal: data = [c; N] => |forecast[i] - c| < epsilon for all i
///
/// Uses ARIMA(1,1,0): d=1 differencing on constant data produces all zeros,
/// and integration from the last observed value recovers the constant.
#[test]
fn prop_constant_input_constant_forecast(
constant_val in -50.0f64..50.0,
n_points in 30usize..60,
n_periods in 1usize..10,
) {
// Construct constant time series
let data = vec![constant_val; n_points];
let series = Vector::from_vec(data);
// ARIMA(1, 1, 0): differencing makes constant series all-zeros,
// integration recovers the constant level
let mut model = ARIMA::new(1, 1, 0);
model.fit(&series).expect("fit succeeds on constant data");
let forecast = model.forecast(n_periods).expect("forecast succeeds");
for i in 0..forecast.len() {
let diff = (forecast[i] - constant_val).abs();
prop_assert!(
diff < 1.0,
"forecast[{}] = {}, expected ~{} (diff = {})",
i, forecast[i], constant_val, diff
);
}
}
}