Skip to main content

ftts_kernels/
selftest.rs

1//! Shipped integer-overflow proofs for the kernels this crate can dispatch.
2//!
3//! The canonical Q8 converter emits symmetric signed weights in `[-127, 127]`; `-128` is
4//! deliberately excluded. Dynamic unsigned activations can span `[0, 255]`. Every dot-product
5//! route therefore has to prove its i32 accumulator against `255 * 127 * K` at this checkpoint's
6//! real reduction lengths, not a bound borrowed from another model.
7//!
8//! Two proof families run at every census binding K:
9//!
10//! - **U8S8 envelope** (`255 * 127 * K`): the contract ceiling for a future unsigned-activation
11//!   route (x86 VNNI's +128 fold), executed on the checked scalar path. It strictly dominates the
12//!   S8S8 magnitude, so it remains the conservative bound for every row.
13//! - **S8S8 kernel** (`±127 * 127 * K`): executed through the *real* [`crate::int8::dot_i32`]
14//!   kernel on every tier this build can dispatch ([`crate::int8::Int8Tier::available`]), each
15//!   result compared against the independent i64 oracle and the scalar route's i32.
16//!
17//! A native tier must appear here, through its real kernel function, before it may be selected.
18//! The rows mirror the binding component maxima in `docs/truth-pack/EXECUTION_CENSUS.json`, plus
19//! the seq-16 microdecoder verifier, whose larger M does not alter its per-output reduction
20//! length.
21
22/// Largest unsigned activation byte accepted by the U8S8 contract.
23pub const U8_MAX: u8 = u8::MAX;
24/// Largest absolute signed Q8 weight byte under the canonical symmetric recipe.
25pub const S8_MAX_ABS: i8 = 127;
26
27/// A route that this build can actually execute and certify.
28///
29/// Do not add an ISA variant merely because the CPU can report that feature. A variant belongs
30/// here only after the corresponding implementation exists and its exact scalar comparison is
31/// wired into [`run_selftest`].
32#[derive(Clone, Copy, Debug, Eq, PartialEq)]
33pub enum KernelTier {
34    /// The portable, safe integer reference route.
35    Scalar,
36    /// The portable eight-lane route shaped for LLVM autovectorization.
37    Autovec,
38    /// The aarch64 SDOT island (`neon-dotprod` feature + runtime FEAT_DotProd).
39    NeonSdot,
40}
41
42impl KernelTier {
43    /// Stable machine-readable route name.
44    #[must_use]
45    pub const fn as_str(self) -> &'static str {
46        match self {
47            Self::Scalar => "scalar",
48            Self::Autovec => "autovec",
49            Self::NeonSdot => "neon-sdot",
50        }
51    }
52
53    const fn from_int8(tier: crate::int8::Int8Tier) -> Self {
54        match tier {
55            crate::int8::Int8Tier::Scalar => Self::Scalar,
56            crate::int8::Int8Tier::Autovec => Self::Autovec,
57            crate::int8::Int8Tier::NeonSdot => Self::NeonSdot,
58        }
59    }
60}
61
62/// Which numeric contract a proof check exercised.
63#[derive(Clone, Copy, Debug, Eq, PartialEq)]
64pub enum DotContract {
65    /// `255 * 127 * K` on the checked scalar path — the conservative envelope for a future
66    /// unsigned-activation (VNNI +128 fold) route.
67    U8S8Envelope,
68    /// `±127 * 127 * K` executed through the real [`crate::int8::dot_i32`] kernel.
69    S8S8Kernel,
70}
71
72impl DotContract {
73    /// Stable machine-readable contract name.
74    #[must_use]
75    pub const fn as_str(self) -> &'static str {
76        match self {
77            Self::U8S8Envelope => "u8s8-envelope",
78            Self::S8S8Kernel => "s8s8-kernel",
79        }
80    }
81}
82
83/// The model component whose maximum reduction length a proof row represents.
84#[derive(Clone, Copy, Debug, Eq, PartialEq)]
85pub enum ExecutionScope {
86    /// Enrollment-only codec encoder.
87    Enrollment,
88    /// Per-frame decode path.
89    Decode,
90    /// Prompt-time text projection/embedding path.
91    Prefill,
92    /// The residual-code microdecoder's one-step execution.
93    Microdecoder,
94    /// The seq-16 residual-code verifier; it shares the microdecoder's per-output K.
95    MicrodecoderVerify,
96    /// Main Qwen talker.
97    Talker,
98}
99
100impl ExecutionScope {
101    /// Stable machine-readable scope name.
102    #[must_use]
103    pub const fn as_str(self) -> &'static str {
104        match self {
105            Self::Enrollment => "enrollment",
106            Self::Decode => "decode",
107            Self::Prefill => "prefill",
108            Self::Microdecoder => "microdecoder",
109            Self::MicrodecoderVerify => "microdecoder_verify_seq16",
110            Self::Talker => "talker",
111        }
112    }
113}
114
115/// One permanent, model-specific i32-overflow obligation.
116#[derive(Clone, Copy, Debug, Eq, PartialEq)]
117pub struct OverflowProofRow {
118    /// Stable row identifier consumed by selftest output and future release receipts.
119    pub id: &'static str,
120    /// Execution regime covered by this row.
121    pub scope: ExecutionScope,
122    /// Pinned census tensor that established this component maximum.
123    pub census_tensor: &'static str,
124    /// Actual reduction length for one output element.
125    pub reduction_k: u32,
126}
127
128/// Component maxima generated from the pinned execution census.
129///
130/// The global 8192 row is enrollment-only; the 7168 codec-decoder row is the binding decode
131/// maximum. Keeping both prevents the larger enrollment shape from accidentally shadowing the
132/// actual real-time requirement.
133pub const OVERFLOW_PROOF_ROWS: &[OverflowProofRow] = &[
134    OverflowProofRow {
135        id: "codec_encoder_global_k8192",
136        scope: ExecutionScope::Enrollment,
137        census_tensor: "encoder.encoder.layers.12.conv.weight",
138        reduction_k: 8192,
139    },
140    OverflowProofRow {
141        id: "codec_decoder_decode_k7168",
142        scope: ExecutionScope::Decode,
143        census_tensor: "decoder.decoder.0.conv.weight",
144        reduction_k: 7168,
145    },
146    OverflowProofRow {
147        id: "speaker_encoder_k4608",
148        scope: ExecutionScope::Enrollment,
149        census_tensor: "speaker_encoder.asp.tdnn.conv.weight",
150        reduction_k: 4608,
151    },
152    OverflowProofRow {
153        id: "microdecoder_step_k3072",
154        scope: ExecutionScope::Microdecoder,
155        census_tensor: "talker.code_predictor.model.layers.0.mlp.down_proj.weight",
156        reduction_k: 3072,
157    },
158    OverflowProofRow {
159        id: "microdecoder_verify_seq16_k3072",
160        scope: ExecutionScope::MicrodecoderVerify,
161        census_tensor: "talker.code_predictor.model.layers.0.mlp.down_proj.weight",
162        reduction_k: 3072,
163    },
164    OverflowProofRow {
165        id: "talker_down_proj_k3072",
166        scope: ExecutionScope::Talker,
167        census_tensor: "talker.model.layers.0.mlp.down_proj.weight",
168        reduction_k: 3072,
169    },
170    OverflowProofRow {
171        id: "text_projection_k2048",
172        scope: ExecutionScope::Prefill,
173        census_tensor: "talker.model.text_embedding.weight",
174        reduction_k: 2048,
175    },
176];
177
178/// One completed proof result.
179#[derive(Clone, Copy, Debug, Eq, PartialEq)]
180pub struct SelftestCheck {
181    /// Row selected from [`OVERFLOW_PROOF_ROWS`].
182    pub row: OverflowProofRow,
183    /// Route that executed the check.
184    pub tier: KernelTier,
185    /// Numeric contract this check exercised.
186    pub contract: DotContract,
187    /// Accumulation performed by that route using all-extreme operands.
188    ///
189    /// `None` means the route overflowed before producing an i32 result; that is a failed proof,
190    /// not a panic or an implicitly widened success.
191    pub accumulator_i32: Option<i32>,
192    /// Independent widened reference for the same dot product.
193    pub reference_i64: i64,
194    /// Whether the route retained exact i32 equality and fit in range.
195    pub passed: bool,
196}
197
198/// A complete selftest result for the dispatched routes in this build.
199#[derive(Clone, Debug, Eq, PartialEq)]
200pub struct SelftestReport {
201    /// Currently selected executable route.
202    pub dispatched: KernelTier,
203    /// Every binding row executed against that route.
204    pub checks: Vec<SelftestCheck>,
205}
206
207impl SelftestReport {
208    /// Whether every executed check has exact i32 equality with its widened reference.
209    #[must_use]
210    pub fn passed(&self) -> bool {
211        self.checks.iter().all(|check| check.passed)
212    }
213}
214
215/// Runs the permanent overflow proof against every route this build can dispatch.
216///
217/// This is deliberately not a compile-time arithmetic assertion. The deployed route executes the
218/// actual all-extreme dot loop and compares that i32 result with a separately widened i64 oracle,
219/// so the same entrypoint can later compare an intrinsic backend before dispatch enables it.
220#[must_use]
221pub fn run_selftest() -> SelftestReport {
222    run_selftest_inner(None)
223}
224
225fn run_selftest_inner(fault_row: Option<&str>) -> SelftestReport {
226    let dispatched = KernelTier::from_int8(crate::int8::Int8Tier::dispatch());
227    let mut checks = Vec::new();
228    for row in OVERFLOW_PROOF_ROWS.iter().copied() {
229        // U8S8 envelope: the contract ceiling, on the checked scalar path.
230        let accumulator_i32 = scalar_all_extreme_dot_i32(row.reduction_k);
231        let reference_i64 = all_extreme_dot_i64(row.reduction_k);
232        let accumulator_i32 = if fault_row == Some(row.id) {
233            accumulator_i32.map(|accumulator| accumulator.saturating_sub(1))
234        } else {
235            accumulator_i32
236        };
237        checks.push(SelftestCheck {
238            row,
239            tier: KernelTier::Scalar,
240            contract: DotContract::U8S8Envelope,
241            accumulator_i32,
242            reference_i64,
243            passed: accumulator_i32
244                .is_some_and(|accumulator| i64::from(accumulator) == reference_i64),
245        });
246
247        // S8S8 kernel proof: the real dot kernel, on every tier this build can dispatch, at both
248        // all-extreme signs, against the independent i64 oracle and the scalar route's i32.
249        let k = row.reduction_k as usize;
250        let positive = vec![crate::int8::Q8_MAX_ABS; k];
251        let negative = vec![-crate::int8::Q8_MAX_ABS; k];
252        let s8_reference_i64 =
253            i64::from(S8_MAX_ABS) * i64::from(S8_MAX_ABS) * i64::from(row.reduction_k);
254        let scalar_positive =
255            crate::int8::dot_i32(&positive, &positive, crate::int8::Int8Tier::Scalar);
256        for tier in crate::int8::Int8Tier::available() {
257            let up = crate::int8::dot_i32(&positive, &positive, tier);
258            let down = crate::int8::dot_i32(&positive, &negative, tier);
259            let up = if fault_row == Some(row.id) {
260                up.saturating_sub(1)
261            } else {
262                up
263            };
264            let passed = i64::from(up) == s8_reference_i64
265                && i64::from(down) == -s8_reference_i64
266                && up == scalar_positive;
267            checks.push(SelftestCheck {
268                row,
269                tier: KernelTier::from_int8(tier),
270                contract: DotContract::S8S8Kernel,
271                accumulator_i32: Some(up),
272                reference_i64: s8_reference_i64,
273                passed,
274            });
275        }
276    }
277    SelftestReport { dispatched, checks }
278}
279
280fn scalar_all_extreme_dot_i32(reduction_k: u32) -> Option<i32> {
281    let term = i32::from(U8_MAX) * i32::from(S8_MAX_ABS);
282    (0..reduction_k).try_fold(0_i32, |accumulator, _| accumulator.checked_add(term))
283}
284
285fn all_extreme_dot_i64(reduction_k: u32) -> i64 {
286    i64::from(U8_MAX) * i64::from(S8_MAX_ABS) * i64::from(reduction_k)
287}
288
289#[cfg(test)]
290mod tests {
291    use super::*;
292
293    //  Crate-local pinned copy; byte-identity with the truth-pack canonical is asserted by a
294    //  unit test whenever the repository checkout is present (crates.io builds have no repo).
295    const CENSUS: &str = include_str!("../pinned/EXECUTION_CENSUS.json");
296
297    #[test]
298    fn every_deployed_row_equals_its_i64_reference_on_every_tier() {
299        let report = run_selftest();
300        assert!(report.passed(), "{report:#?}");
301
302        let envelope: Vec<_> = report
303            .checks
304            .iter()
305            .filter(|check| check.contract == DotContract::U8S8Envelope)
306            .collect();
307        assert_eq!(envelope.len(), OVERFLOW_PROOF_ROWS.len());
308        for check in &envelope {
309            assert_eq!(check.tier, KernelTier::Scalar, "{}", check.row.id);
310            assert_eq!(
311                check.accumulator_i32.map(i64::from),
312                Some(check.reference_i64),
313                "{}",
314                check.row.id
315            );
316        }
317
318        let tiers = crate::int8::Int8Tier::available();
319        let s8s8: Vec<_> = report
320            .checks
321            .iter()
322            .filter(|check| check.contract == DotContract::S8S8Kernel)
323            .collect();
324        assert_eq!(s8s8.len(), OVERFLOW_PROOF_ROWS.len() * tiers.len());
325        for check in &s8s8 {
326            assert_eq!(
327                check.accumulator_i32.map(i64::from),
328                Some(check.reference_i64),
329                "{} on {}",
330                check.row.id,
331                check.tier.as_str()
332            );
333        }
334
335        assert!(
336            tiers
337                .iter()
338                .any(|tier| KernelTier::from_int8(*tier) == report.dispatched),
339            "dispatched route {:?} is not among the available tiers",
340            report.dispatched
341        );
342    }
343
344    #[test]
345    fn the_sdot_island_is_proven_on_this_silicon_when_present() {
346        // On an Apple Silicon dev host the island must actually run — a silently absent
347        // FEAT_DotProd would turn every SDOT proof row into vacuous truth.
348        if cfg!(all(target_arch = "aarch64", feature = "neon-dotprod"))
349            && crate::int8::neon_sdot_available()
350        {
351            let report = run_selftest();
352            assert!(
353                report.checks.iter().any(|check| {
354                    check.tier == KernelTier::NeonSdot
355                        && check.contract == DotContract::S8S8Kernel
356                        && check.passed
357                }),
358                "FEAT_DotProd reported but no SDOT proof row executed"
359            );
360        }
361    }
362
363    #[test]
364    fn census_binding_rows_are_not_replaced_by_a_stale_talker_only_bound() {
365        for (tensor, reduction_k) in [
366            ("encoder.encoder.layers.12.conv.weight", 8192),
367            ("decoder.decoder.0.conv.weight", 7168),
368            ("speaker_encoder.asp.tdnn.conv.weight", 4608),
369            (
370                "talker.code_predictor.model.layers.0.mlp.down_proj.weight",
371                3072,
372            ),
373            ("talker.model.layers.0.mlp.down_proj.weight", 3072),
374            ("talker.model.text_embedding.weight", 2048),
375        ] {
376            assert!(
377                OVERFLOW_PROOF_ROWS
378                    .iter()
379                    .any(|row| { row.census_tensor == tensor && row.reduction_k == reduction_k }),
380                "proof row missing for {tensor} K={reduction_k}"
381            );
382            assert!(
383                CENSUS.contains(&format!("\"tensor\": \"{tensor}\"")),
384                "pinned census no longer contains {tensor}; regenerate the proof table"
385            );
386            assert!(
387                CENSUS.split('{').any(|object| {
388                    object.contains(&format!("\"tensor\": \"{tensor}\""))
389                        && object.contains(&format!("\"k\": {reduction_k}"))
390                }),
391                "pinned census no longer gives {tensor} reduction K={reduction_k}; regenerate the proof table"
392            );
393        }
394        assert!(
395            CENSUS.contains("\"decode_path_binding_row\""),
396            "proof table requires a separately named decode binding"
397        );
398    }
399
400    #[test]
401    fn a_corrupted_route_fails_the_selftest_instead_of_reporting_green() {
402        let report = run_selftest_inner(Some("codec_decoder_decode_k7168"));
403        assert!(
404            !report.passed(),
405            "fault injection must fail the aggregate verdict"
406        );
407        assert!(
408            report
409                .checks
410                .iter()
411                .any(|check| { check.row.id == "codec_decoder_decode_k7168" && !check.passed })
412        );
413    }
414
415    #[test]
416    fn i32_bound_remains_strictly_below_the_widened_limit() {
417        for row in OVERFLOW_PROOF_ROWS {
418            let reference = all_extreme_dot_i64(row.reduction_k);
419            assert!(
420                reference < i64::from(i32::MAX),
421                "{} no longer fits i32: {reference}",
422                row.id
423            );
424        }
425    }
426
427    #[test]
428    fn pinned_census_copy_matches_the_truth_pack_canonical() {
429        //  The crate-local copy exists because `cargo package` cannot ship the truth pack; the
430        //  truth pack stays canonical. A drifted copy silently pins the selftest to a stale
431        //  census, so equality is asserted byte-for-byte whenever the repo checkout is present.
432        let canonical = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
433            .join("../../docs/truth-pack/EXECUTION_CENSUS.json");
434        match std::fs::read_to_string(&canonical) {
435            Ok(bytes) => assert_eq!(
436                bytes, CENSUS,
437                "pinned/EXECUTION_CENSUS.json drifted from the truth-pack canonical; re-copy it"
438            ),
439            Err(_) => eprintln!(
440                "SKIP pinned_census_copy_matches_the_truth_pack_canonical: no repo checkout at {}",
441                canonical.display()
442            ),
443        }
444    }
445}