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
// CONTRACT: ssm-kernel-v1.yaml
// HASH: sha256:f2a3b4c5d6e78901
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
proptest! {
/// Obligation: State remains finite (invariant)
/// Formal: finite(input) → finite(state) for all timesteps
#[test]
#[ignore = "SSM/Mamba not implemented"]
fn prop_state_finite(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: SSM (Mamba/S4) not yet implemented in aprender
}
/// Obligation: Output causality (invariant)
/// Formal: y_t depends only on x_{0..t}, not x_{t+1..T}
#[test]
#[ignore = "SSM/Mamba not implemented"]
fn prop_causality(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: SSM not implemented
}
/// Obligation: Discretization stability (bound)
/// Formal: eigenvalues of discretized A inside unit circle
#[test]
#[ignore = "SSM/Mamba not implemented"]
fn prop_discretization_stability(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: SSM not implemented
}
/// Obligation: Linear recurrence equivalence (equivalence)
/// Formal: parallel scan == sequential recurrence within ULP
#[test]
#[ignore = "SSM/Mamba not implemented"]
fn prop_scan_recurrence_equivalence(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: SSM not implemented
}
/// Obligation: SIMD matches scalar within ULP (equivalence)
#[test]
#[ignore = "SSM/Mamba not implemented"]
fn prop_simd_equivalence(
_x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
) {
// Blocked: SSM not implemented
}
}