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
// CONTRACT: kernel-launch-budget-v1.yaml
// HASH: sha256:a3b4c5d6e7f89012
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`
use proptest::prelude::*;
/// Per-token kernel launch count for standard transformer.
/// 12 launches per layer + 2 (final_norm + lm_head).
fn kernel_launches(layers: u32) -> u32 {
12 * layers + 2
}
/// Per-layer decomposition components.
const NORM_KERNELS: u32 = 2; // pre-attn norm + pre-ffn norm
const MATMUL_KERNELS: u32 = 5; // QKV + attn_output + gate + up + down
const ROPE_KERNELS: u32 = 1; // rotary position embedding
const ATTN_KERNELS: u32 = 1; // scaled dot-product attention
const SWIGLU_KERNELS: u32 = 1; // SiLU activation (fused in SwiGLU)
const RESIDUAL_KERNELS: u32 = 2; // post-attn residual + post-ffn residual
const PER_LAYER_TOTAL: u32 =
NORM_KERNELS + MATMUL_KERNELS + ROPE_KERNELS + ATTN_KERNELS + SWIGLU_KERNELS + RESIDUAL_KERNELS;
proptest! {
/// Obligation: Per-token formula (invariant)
/// Formal: kernel_launches(L) = 12 * L + 2 for all L >= 1
#[test]
fn prop_per_token_formula(
layers in 1u32..200
) {
let expected = 12 * layers + 2;
let actual = kernel_launches(layers);
prop_assert_eq!(
actual, expected,
"kernel_launches({}) = {}, expected {}",
layers, actual, expected
);
}
/// Obligation: Decomposition sum (invariant)
/// Formal: 2 + 5 + 1 + 1 + 1 + 2 = 12
#[test]
fn prop_decomposition_sum(
_dummy in 0u8..1 // proptest requires at least one input
) {
prop_assert_eq!(
PER_LAYER_TOTAL, 12,
"per-layer decomposition sums to {}, expected 12",
PER_LAYER_TOTAL
);
// Also verify each component is at least 1
prop_assert!(NORM_KERNELS >= 1, "norm_kernels = {}", NORM_KERNELS);
prop_assert!(MATMUL_KERNELS >= 1, "matmul_kernels = {}", MATMUL_KERNELS);
prop_assert!(ROPE_KERNELS >= 1, "rope_kernels = {}", ROPE_KERNELS);
prop_assert!(ATTN_KERNELS >= 1, "attn_kernels = {}", ATTN_KERNELS);
prop_assert!(SWIGLU_KERNELS >= 1, "swiglu_kernels = {}", SWIGLU_KERNELS);
prop_assert!(RESIDUAL_KERNELS >= 1, "residual_kernels = {}", RESIDUAL_KERNELS);
}
/// Obligation: Launch count monotonic (monotonicity)
/// Formal: L1 < L2 => kernel_launches(L1) < kernel_launches(L2)
#[test]
fn prop_launch_monotonic(
l1 in 1u32..100,
delta in 1u32..100
) {
let l2 = l1 + delta;
let launches_1 = kernel_launches(l1);
let launches_2 = kernel_launches(l2);
prop_assert!(
launches_2 > launches_1,
"not monotonic: launches({})={} >= launches({})={}",
l1, launches_1, l2, launches_2
);
}
/// Obligation: SIMD kernel equivalence (equivalence)
#[test]
#[ignore = "SIMD equivalence — trueno domain"]
fn prop_simd_equivalence(
_x in proptest::collection::vec(0u32..100, 1..32usize)
) {
// Kernel launch budget is pure math — no SIMD variant
}
}