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
// CONTRACT: kv-cache-equivalence-v1.yaml
// HASH: sha256:b890123456789012
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
proptest! {
/// Obligation: Prefill/incremental equivalence (equivalence)
/// Formal: |forward_with_cache(t_n) - forward_all([t_0..t_n])[n]| < 1e-5
#[test]
#[ignore = "Requires realizar inference API"]
fn prop_prefill_incremental(
_tokens in proptest::collection::vec(0u32..32000, 2..64usize)
) {
// Requires full inference pipeline — realizar domain
}
/// Obligation: Page shape formula (invariant)
/// Formal: page_elements = block_size * n_kv * d_k
#[test]
fn prop_page_shape(
block_size in 1u32..256,
n_kv in 1u32..32,
d_k in 16u32..256
) {
let page_elements = block_size as u64 * n_kv as u64 * d_k as u64;
prop_assert!(
page_elements > 0,
"page_elements must be > 0, got {}", page_elements
);
// Verify formula composition
let expected = block_size as u64 * n_kv as u64 * d_k as u64;
prop_assert_eq!(
page_elements, expected,
"page formula mismatch: {} != {}", page_elements, expected
);
}
/// Obligation: Batched/serial equivalence (equivalence)
/// Formal: |batched_prefill(tokens) - serial_prefill(tokens)| < 1e-5
#[test]
#[ignore = "Requires realizar inference API"]
fn prop_batched_serial(
_tokens in proptest::collection::vec(0u32..32000, 2..128usize)
) {
// Requires full inference pipeline — realizar domain
}
/// Obligation: Fused kernel equivalence (equivalence)
/// Formal: |fused_q4k_matvec(W,x) - matmul(dequant(W),x)| < 1e-3
#[test]
#[ignore = "Requires trueno fused kernel API"]
fn prop_fused_kernel(
_rows in 1u32..1024,
_cols in 1u32..1024
) {
// Requires trueno fused dequant+matmul — trueno domain
}
}