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    // The receipt must name the route the process actually RUNS, which is the autotuned plan's
227    // decode pick — Int8Tier::dispatch() reports raw capability (SDOT whenever present) and can
228    // disagree with a measured or persisted plan that chose scalar.
229    let dispatched = KernelTier::from_int8(crate::int8::autotuned_plan().decode_gemv);
230    let mut checks = Vec::new();
231    for row in OVERFLOW_PROOF_ROWS.iter().copied() {
232        // U8S8 envelope: the contract ceiling, on the checked scalar path.
233        let accumulator_i32 = scalar_all_extreme_dot_i32(row.reduction_k);
234        let reference_i64 = all_extreme_dot_i64(row.reduction_k);
235        let accumulator_i32 = if fault_row == Some(row.id) {
236            accumulator_i32.map(|accumulator| accumulator.saturating_sub(1))
237        } else {
238            accumulator_i32
239        };
240        checks.push(SelftestCheck {
241            row,
242            tier: KernelTier::Scalar,
243            contract: DotContract::U8S8Envelope,
244            accumulator_i32,
245            reference_i64,
246            passed: accumulator_i32
247                .is_some_and(|accumulator| i64::from(accumulator) == reference_i64),
248        });
249
250        // S8S8 kernel proof: the real dot kernel, on every tier this build can dispatch, at both
251        // all-extreme signs, against the independent i64 oracle and the scalar route's i32.
252        let k = row.reduction_k as usize;
253        let positive = vec![crate::int8::Q8_MAX_ABS; k];
254        let negative = vec![-crate::int8::Q8_MAX_ABS; k];
255        let s8_reference_i64 =
256            i64::from(S8_MAX_ABS) * i64::from(S8_MAX_ABS) * i64::from(row.reduction_k);
257        let scalar_positive =
258            crate::int8::dot_i32(&positive, &positive, crate::int8::Int8Tier::Scalar);
259        for tier in crate::int8::Int8Tier::available() {
260            let up = crate::int8::dot_i32(&positive, &positive, tier);
261            let down = crate::int8::dot_i32(&positive, &negative, tier);
262            let up = if fault_row == Some(row.id) {
263                up.saturating_sub(1)
264            } else {
265                up
266            };
267            let passed = i64::from(up) == s8_reference_i64
268                && i64::from(down) == -s8_reference_i64
269                && up == scalar_positive;
270            checks.push(SelftestCheck {
271                row,
272                tier: KernelTier::from_int8(tier),
273                contract: DotContract::S8S8Kernel,
274                accumulator_i32: Some(up),
275                reference_i64: s8_reference_i64,
276                passed,
277            });
278        }
279    }
280    SelftestReport { dispatched, checks }
281}
282
283fn scalar_all_extreme_dot_i32(reduction_k: u32) -> Option<i32> {
284    let term = i32::from(U8_MAX) * i32::from(S8_MAX_ABS);
285    (0..reduction_k).try_fold(0_i32, |accumulator, _| accumulator.checked_add(term))
286}
287
288fn all_extreme_dot_i64(reduction_k: u32) -> i64 {
289    i64::from(U8_MAX) * i64::from(S8_MAX_ABS) * i64::from(reduction_k)
290}
291
292#[cfg(test)]
293mod tests {
294    use super::*;
295
296    //  Crate-local pinned copy; byte-identity with the truth-pack canonical is asserted by a
297    //  unit test whenever the repository checkout is present (crates.io builds have no repo).
298    const CENSUS: &str = include_str!("../pinned/EXECUTION_CENSUS.json");
299
300    #[test]
301    fn every_deployed_row_equals_its_i64_reference_on_every_tier() {
302        let report = run_selftest();
303        assert!(report.passed(), "{report:#?}");
304
305        let envelope: Vec<_> = report
306            .checks
307            .iter()
308            .filter(|check| check.contract == DotContract::U8S8Envelope)
309            .collect();
310        assert_eq!(envelope.len(), OVERFLOW_PROOF_ROWS.len());
311        for check in &envelope {
312            assert_eq!(check.tier, KernelTier::Scalar, "{}", check.row.id);
313            assert_eq!(
314                check.accumulator_i32.map(i64::from),
315                Some(check.reference_i64),
316                "{}",
317                check.row.id
318            );
319        }
320
321        let tiers = crate::int8::Int8Tier::available();
322        let s8s8: Vec<_> = report
323            .checks
324            .iter()
325            .filter(|check| check.contract == DotContract::S8S8Kernel)
326            .collect();
327        assert_eq!(s8s8.len(), OVERFLOW_PROOF_ROWS.len() * tiers.len());
328        for check in &s8s8 {
329            assert_eq!(
330                check.accumulator_i32.map(i64::from),
331                Some(check.reference_i64),
332                "{} on {}",
333                check.row.id,
334                check.tier.as_str()
335            );
336        }
337
338        assert!(
339            tiers
340                .iter()
341                .any(|tier| KernelTier::from_int8(*tier) == report.dispatched),
342            "dispatched route {:?} is not among the available tiers",
343            report.dispatched
344        );
345    }
346
347    #[test]
348    fn the_sdot_island_is_proven_on_this_silicon_when_present() {
349        // On an Apple Silicon dev host the island must actually run — a silently absent
350        // FEAT_DotProd would turn every SDOT proof row into vacuous truth.
351        if cfg!(all(target_arch = "aarch64", feature = "neon-dotprod"))
352            && crate::int8::neon_sdot_available()
353        {
354            let report = run_selftest();
355            assert!(
356                report.checks.iter().any(|check| {
357                    check.tier == KernelTier::NeonSdot
358                        && check.contract == DotContract::S8S8Kernel
359                        && check.passed
360                }),
361                "FEAT_DotProd reported but no SDOT proof row executed"
362            );
363        }
364    }
365
366    #[test]
367    fn census_binding_rows_are_not_replaced_by_a_stale_talker_only_bound() {
368        for (tensor, reduction_k) in [
369            ("encoder.encoder.layers.12.conv.weight", 8192),
370            ("decoder.decoder.0.conv.weight", 7168),
371            ("speaker_encoder.asp.tdnn.conv.weight", 4608),
372            (
373                "talker.code_predictor.model.layers.0.mlp.down_proj.weight",
374                3072,
375            ),
376            ("talker.model.layers.0.mlp.down_proj.weight", 3072),
377            ("talker.model.text_embedding.weight", 2048),
378        ] {
379            assert!(
380                OVERFLOW_PROOF_ROWS
381                    .iter()
382                    .any(|row| { row.census_tensor == tensor && row.reduction_k == reduction_k }),
383                "proof row missing for {tensor} K={reduction_k}"
384            );
385            assert!(
386                CENSUS.contains(&format!("\"tensor\": \"{tensor}\"")),
387                "pinned census no longer contains {tensor}; regenerate the proof table"
388            );
389            assert!(
390                CENSUS.split('{').any(|object| {
391                    object.contains(&format!("\"tensor\": \"{tensor}\""))
392                        && object.contains(&format!("\"k\": {reduction_k}"))
393                }),
394                "pinned census no longer gives {tensor} reduction K={reduction_k}; regenerate the proof table"
395            );
396        }
397        assert!(
398            CENSUS.contains("\"decode_path_binding_row\""),
399            "proof table requires a separately named decode binding"
400        );
401    }
402
403    #[test]
404    fn a_corrupted_route_fails_the_selftest_instead_of_reporting_green() {
405        let report = run_selftest_inner(Some("codec_decoder_decode_k7168"));
406        assert!(
407            !report.passed(),
408            "fault injection must fail the aggregate verdict"
409        );
410        assert!(
411            report
412                .checks
413                .iter()
414                .any(|check| { check.row.id == "codec_decoder_decode_k7168" && !check.passed })
415        );
416    }
417
418    #[test]
419    fn i32_bound_remains_strictly_below_the_widened_limit() {
420        for row in OVERFLOW_PROOF_ROWS {
421            let reference = all_extreme_dot_i64(row.reduction_k);
422            assert!(
423                reference < i64::from(i32::MAX),
424                "{} no longer fits i32: {reference}",
425                row.id
426            );
427        }
428    }
429
430    #[test]
431    fn pinned_census_copy_matches_the_truth_pack_canonical() {
432        //  The crate-local copy exists because `cargo package` cannot ship the truth pack; the
433        //  truth pack stays canonical. A drifted copy silently pins the selftest to a stale
434        //  census, so equality is asserted byte-for-byte whenever the repo checkout is present.
435        let canonical = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
436            .join("../../docs/truth-pack/EXECUTION_CENSUS.json");
437        match std::fs::read_to_string(&canonical) {
438            Ok(bytes) => assert_eq!(
439                bytes, CENSUS,
440                "pinned/EXECUTION_CENSUS.json drifted from the truth-pack canonical; re-copy it"
441            ),
442            Err(_) => eprintln!(
443                "SKIP pinned_census_copy_matches_the_truth_pack_canonical: no repo checkout at {}",
444                canonical.display()
445            ),
446        }
447    }
448}