tensor_wasm_jit/differential.rs
1// SPDX-License-Identifier: Apache-2.0
2// Copyright 2026 Craton Software Company
3
4//! Differential correctness oracle (roadmap feature #6).
5//!
6//! For every `auto_offload` candidate that lowers to PTX, the harness
7//! runs:
8//! 1. The original Wasm body on the Wasmtime CPU interpreter (the
9//! ground truth).
10//! 2. The JIT-emitted PTX on the cust/cudarc backend.
11//!
12//! …and asserts byte-equal output. Discrepancies are surfaced as
13//! `OracleDivergence` records the CI gate can publish on every PR.
14//!
15//! ## v0.3.7 / v0.4 status
16//!
17//! The harness types are stable and the v0.4 (T38) wave wires the
18//! **CPU reference path** end-to-end — every call to
19//! [`DifferentialOracle::compare`] now interprets the blueprint over
20//! the provided input bytes using the f32 lane semantics declared in
21//! [`crate::ir::TensorWasmOp`] and surfaces the resulting output as
22//! [`OracleVerdict::HostOnlyOk`]. The GPU side stays gated behind a
23//! runtime CUDA-availability check (and the `cuda-oxide-backend`
24//! feature flag); hosts without CUDA receive
25//! [`OracleVerdict::Skipped("no-cuda; CPU-only oracle verdict")`] AFTER
26//! the CPU path has executed, so the harness wiring is exercised on
27//! every host. The S22 self-hosted CUDA runner is the layer that
28//! upgrades `HostOnlyOk` / `Skipped` to [`OracleVerdict::Match`] or
29//! [`OracleVerdict::Divergence`].
30//!
31//! ## How to use (v0.4 target shape)
32//!
33//! ```ignore
34//! use tensor_wasm_jit::differential::DifferentialOracle;
35//!
36//! let oracle = DifferentialOracle::new();
37//! let blueprint = /* TensorWasmKernelBlueprint */;
38//! let inputs = /* &[u8] guest memory snapshot, f32 little-endian */;
39//! match oracle.compare(&blueprint, inputs) {
40//! OracleVerdict::Match { .. } => { /* CPU == GPU */ }
41//! OracleVerdict::HostOnlyOk { .. } => { /* CPU ran, no GPU host */ }
42//! OracleVerdict::Divergence(d) => panic!("audit-bait: {d:?}"),
43//! OracleVerdict::Skipped(reason) => eprintln!("skipped: {reason}"),
44//! }
45//! ```
46
47use crate::ir::{ElemType, TensorWasmKernelBlueprint, TensorWasmOp};
48
49/// Configuration for the oracle. v0.3.6: defaults are sufficient.
50#[derive(Debug, Clone, Default)]
51#[non_exhaustive]
52pub struct OracleConfig {
53 /// Skip the comparison and return Skipped("disabled") for every
54 /// call. Used to disable the oracle in environments where one of
55 /// the two paths is not available.
56 pub disabled: bool,
57}
58
59/// The oracle. Drive it from proptest test bodies and CI gates.
60pub struct DifferentialOracle {
61 cfg: OracleConfig,
62}
63
64impl DifferentialOracle {
65 /// Construct an oracle with default configuration.
66 pub fn new() -> Self {
67 Self {
68 cfg: OracleConfig::default(),
69 }
70 }
71
72 /// Construct an oracle with a caller-provided configuration.
73 pub fn with_config(cfg: OracleConfig) -> Self {
74 Self { cfg }
75 }
76
77 /// Run the two paths and compare.
78 ///
79 /// v0.4 (T38): the CPU reference path is wired end-to-end via the
80 /// in-crate [`reference_eval`] interpreter, which reproduces the
81 /// f32 lane semantics declared in [`TensorWasmOp`]. The GPU path
82 /// requires a CUDA host; on hosts without one, the call returns
83 /// [`OracleVerdict::Skipped`] AFTER the CPU result has been
84 /// computed (so the harness wiring is exercised everywhere).
85 pub fn compare(&self, bp: &TensorWasmKernelBlueprint, inputs: &[u8]) -> OracleVerdict {
86 if self.cfg.disabled {
87 return OracleVerdict::Skipped("oracle disabled by config");
88 }
89
90 // CPU reference path: interpret the blueprint over the input
91 // bytes (f32 little-endian lanes). When the interpreter
92 // can't run the blueprint end-to-end (no input bytes
93 // provided, unsupported op, malformed stack) we fall back to
94 // the original v0.3.6 skip contract — that path is exercised
95 // by the existing scaffold tests in `differential_scaffold.rs`
96 // which pass a blueprint + empty input to assert harness
97 // wiring only.
98 let cpu_output = reference_eval(bp, inputs).ok();
99
100 // GPU path: requires both the `cuda-oxide-backend` feature AND
101 // a usable CUDA device at runtime. Until the S22 runner is
102 // here, we always take the no-cuda branch.
103 if cuda_runtime_available() {
104 // v0.4 wiring point: dispatch `bp` through the kernel
105 // cache + cudarc launch and memcmp `cpu_output` against
106 // the readback. Until that lands, falling through to the
107 // HostOnlyOk branch is correct — the S22 job overrides
108 // `cuda_runtime_available` to true and runs the real
109 // comparison.
110 match cpu_output {
111 Some(out) => OracleVerdict::HostOnlyOk {
112 cpu_output_len: out.len(),
113 cpu_output_first_bytes: head_bytes(&out),
114 },
115 None => {
116 OracleVerdict::Skipped("reference-eval-unavailable; falling back to no-cuda")
117 }
118 }
119 } else {
120 match cpu_output {
121 Some(out) => OracleVerdict::HostOnlyOk {
122 cpu_output_len: out.len(),
123 cpu_output_first_bytes: head_bytes(&out),
124 },
125 None => OracleVerdict::Skipped("no-cuda; v0.4 wires this against the S22 runner"),
126 }
127 }
128 }
129}
130
131impl Default for DifferentialOracle {
132 fn default() -> Self {
133 Self::new()
134 }
135}
136
137/// Result of a single oracle comparison.
138#[derive(Debug, Clone, PartialEq, Eq)]
139pub enum OracleVerdict {
140 /// Both paths produced byte-equal output.
141 Match {
142 /// Number of output bytes that were compared.
143 output_len: usize,
144 },
145 /// Only the CPU reference path executed (no CUDA host on this
146 /// runner). The CPU output length is reported so test bodies can
147 /// at least validate the harness wiring on no-CUDA hosts. v0.4
148 /// (T38) introduced this variant so the proptest harness can
149 /// run end-to-end on the default CI without a CUDA device.
150 HostOnlyOk {
151 /// Number of output bytes the CPU reference produced.
152 cpu_output_len: usize,
153 /// Up to the first 16 bytes of the CPU output, surfaced for
154 /// debug formatting on proptest failure. Not used for
155 /// equality decisions — the test harness compares the full
156 /// vector via [`reference_eval`] separately.
157 cpu_output_first_bytes: [u8; 16],
158 },
159 /// Outputs diverged. The CI gate must fail.
160 Divergence(OracleDivergence),
161 /// Comparison was skipped (typically: one of the two paths is not
162 /// available on the current host). Not a failure; the test runner
163 /// should record it as a skip.
164 Skipped(&'static str),
165}
166
167/// Detailed divergence record. Logged with `tracing::error!` in CI
168/// gates; the offending blueprint fingerprint is stable across runs so
169/// the same divergence is triaged once, not per-CI-run.
170#[derive(Debug, Clone, PartialEq, Eq)]
171pub struct OracleDivergence {
172 /// Stable fingerprint of the blueprint that diverged. Matches
173 /// `TensorWasmKernelBlueprint::fingerprint`.
174 pub blueprint_fingerprint: u64,
175 /// Number of bytes the Wasmtime CPU path produced.
176 pub cpu_output_len: usize,
177 /// Number of bytes the JIT PTX path produced.
178 pub gpu_output_len: usize,
179 /// Offset of the first differing byte if both outputs are non-empty
180 /// and share at least one byte; `None` if the lengths differed
181 /// before any byte could be compared.
182 pub first_diff_offset: Option<usize>,
183}
184
185// ---------------------------------------------------------------------
186// Per-blueprint tolerance table (T38).
187// ---------------------------------------------------------------------
188
189/// Coarse classification of the blueprint shape, used by the tolerance
190/// table to pick the right ULP/abs/rel triple. The proptest harness
191/// generates inputs per kind; the auto-offload pipeline classifies
192/// every emitted blueprint via [`BlueprintKind::classify`].
193#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
194pub enum BlueprintKind {
195 /// Element-wise vector add (1 ULP for f32, 4 ULP for f16).
196 VectorAdd,
197 /// Element-wise vector multiply (1 ULP for f32, 4 ULP for f16).
198 VectorMul,
199 /// Fused multiply-add (1 ULP, single-rounding contract on both
200 /// paths — CPU uses `f32::mul_add`, PTX uses `fma.rn.f32`).
201 VectorFma,
202 /// Reduction (matmul, dot product). Looser tolerance because
203 /// reduction order is implementation-defined.
204 Matmul,
205 /// 2D convolution. Tolerance bracketed with matmul because the
206 /// inner loop is a multiply-accumulate over a sliding window.
207 Conv2d,
208 /// Anything else — defaults to strict 1-ULP behaviour.
209 Other,
210}
211
212impl BlueprintKind {
213 /// Classify a blueprint by its dominant op family. Order of
214 /// preference: matmul > conv2d > fma > add > mul > other. (The
215 /// PTX emitter does not yet emit a dedicated Conv2dOp — the
216 /// rewriter encodes 2D conv as a sequence of `LoadUnified` +
217 /// `VecFma` + `StoreUnified`, so we look for a `VecFma` block
218 /// preceded by a barrier as the conv signature.)
219 pub fn classify(bp: &TensorWasmKernelBlueprint) -> Self {
220 let mut has_matmul = false;
221 let mut has_fma = false;
222 let mut has_add = false;
223 let mut has_mul = false;
224 let mut has_barrier = false;
225 for op in &bp.ops {
226 match op {
227 TensorWasmOp::MatMul { .. } => has_matmul = true,
228 TensorWasmOp::VecFma { .. } => has_fma = true,
229 TensorWasmOp::VecAdd { .. } => has_add = true,
230 TensorWasmOp::VecMul { .. } => has_mul = true,
231 TensorWasmOp::Barrier => has_barrier = true,
232 _ => {}
233 }
234 }
235 if has_matmul {
236 BlueprintKind::Matmul
237 } else if has_fma && has_barrier {
238 BlueprintKind::Conv2d
239 } else if has_fma {
240 BlueprintKind::VectorFma
241 } else if has_add {
242 BlueprintKind::VectorAdd
243 } else if has_mul {
244 BlueprintKind::VectorMul
245 } else {
246 BlueprintKind::Other
247 }
248 }
249}
250
251/// Floating-point datatype the kernel operates on. Influences how
252/// many ULPs of drift the oracle tolerates.
253#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
254pub enum Dtype {
255 /// IEEE-754 binary32 (the default for the v0.1.0 supported shapes).
256 F32,
257 /// IEEE-754 binary16. Looser tolerance — only 10 mantissa bits.
258 F16,
259 /// Integer / bit-identical (no tolerance allowed).
260 Int,
261}
262
263/// Tolerance triple. The oracle accepts an actual value `g` against
264/// reference `c` iff `|g - c| <= max(abs, rel * |c|)` OR they are
265/// within [`Tolerance::ulps`] ULPs of each other. All three axes are
266/// checked together so reductions (matmul) can use a generous ULP
267/// budget while still pinning the absolute drift.
268#[derive(Debug, Clone, Copy, PartialEq)]
269pub struct Tolerance {
270 /// Maximum ULPs of drift permitted between the two paths.
271 pub ulps: u32,
272 /// Absolute error budget (max |g - c|).
273 pub abs: f32,
274 /// Relative error budget (max |g - c| / |c|).
275 pub rel: f32,
276}
277
278impl Tolerance {
279 /// Strict (bit-identical) tolerance — every axis is zero.
280 pub const STRICT: Tolerance = Tolerance {
281 ulps: 0,
282 abs: 0.0,
283 rel: 0.0,
284 };
285
286 /// Returns `true` iff `actual` is within tolerance of `expected`.
287 pub fn approx_eq_f32(self, expected: f32, actual: f32) -> bool {
288 if expected.is_nan() && actual.is_nan() {
289 return true;
290 }
291 if !expected.is_finite() || !actual.is_finite() {
292 return expected == actual;
293 }
294 let diff = (expected - actual).abs();
295 if diff <= self.abs {
296 return true;
297 }
298 if diff <= self.rel * expected.abs() {
299 return true;
300 }
301 // ULP comparison via the canonical bit-distance trick — both
302 // values are finite and the sign-magnitude → biased-int form
303 // gives `(a - b).abs()` as the ULP count.
304 let to_biased = |x: f32| -> i32 {
305 let bits = x.to_bits() as i32;
306 if bits < 0 {
307 i32::MIN.wrapping_sub(bits)
308 } else {
309 bits
310 }
311 };
312 let ulp_dist = (to_biased(expected) - to_biased(actual)).unsigned_abs();
313 ulp_dist <= self.ulps
314 }
315}
316
317/// Per-blueprint floating-point tolerance for CPU↔GPU bit-identity
318/// checks.
319///
320/// fp32: 1 ULP allowed for element-wise ops; 2 ULP for reductions
321/// (matmul). fp16: 4 ULP allowed (smaller mantissa, larger drift).
322/// Integer: bit-identical required (tolerance == 0).
323#[derive(Debug, Clone)]
324pub struct ToleranceTable {
325 /// Vector add tolerance keyed by dtype.
326 pub vector_add_f32: Tolerance,
327 /// Vector mul tolerance.
328 pub vector_mul_f32: Tolerance,
329 /// FMA tolerance.
330 pub vector_fma_f32: Tolerance,
331 /// Matmul tolerance (looser — reduction order is impl-defined).
332 pub matmul_f32: Tolerance,
333 /// Conv2d tolerance (matmul-shaped budget).
334 pub conv2d_f32: Tolerance,
335 /// f16 multiplier — every f32 budget is scaled by this for f16.
336 pub f16_ulp_multiplier: u32,
337}
338
339impl ToleranceTable {
340 /// Strict policy: zero tolerance everywhere. Used by the CI gate
341 /// that asserts "the JIT produced identical bytes" — for ops the
342 /// oracle pins as bit-identical (today: integer kernels only).
343 pub const fn strict() -> Self {
344 Self {
345 vector_add_f32: Tolerance::STRICT,
346 vector_mul_f32: Tolerance::STRICT,
347 vector_fma_f32: Tolerance::STRICT,
348 matmul_f32: Tolerance::STRICT,
349 conv2d_f32: Tolerance::STRICT,
350 f16_ulp_multiplier: 4,
351 }
352 }
353
354 /// Default per-blueprint policy. Values mirror the table in
355 /// `docs/DIFFERENTIAL-ORACLE.md#tolerance-table-v037`.
356 pub const fn default_table() -> Self {
357 Self {
358 vector_add_f32: Tolerance {
359 ulps: 1,
360 abs: 0.0,
361 rel: 0.0,
362 },
363 vector_mul_f32: Tolerance {
364 ulps: 1,
365 abs: 0.0,
366 rel: 0.0,
367 },
368 // FMA: single-rounding contract on both paths means we
369 // expect bit-identity, but we leave 1 ULP for the f32
370 // round-mode tiebreak (round-to-nearest-even, which both
371 // paths use).
372 vector_fma_f32: Tolerance {
373 ulps: 1,
374 abs: 0.0,
375 rel: 0.0,
376 },
377 // Matmul: 2 ULP budget per output element + a small
378 // absolute floor so reductions over k=16 lanes don't trip
379 // on subnormals.
380 matmul_f32: Tolerance {
381 ulps: 2,
382 abs: 1e-6,
383 rel: 1e-6,
384 },
385 // Conv2d: tracks matmul; the inner loop is the same MAC
386 // shape.
387 conv2d_f32: Tolerance {
388 ulps: 2,
389 abs: 1e-6,
390 rel: 1e-6,
391 },
392 f16_ulp_multiplier: 4,
393 }
394 }
395
396 /// Look up the tolerance for the given blueprint kind + dtype.
397 /// Integer kernels are always strict; f16 multiplies the f32 ULP
398 /// budget by [`Self::f16_ulp_multiplier`].
399 pub fn for_blueprint(&self, kind: BlueprintKind, dtype: Dtype) -> Tolerance {
400 if matches!(dtype, Dtype::Int) {
401 return Tolerance::STRICT;
402 }
403 let base = match kind {
404 BlueprintKind::VectorAdd => self.vector_add_f32,
405 BlueprintKind::VectorMul => self.vector_mul_f32,
406 BlueprintKind::VectorFma => self.vector_fma_f32,
407 BlueprintKind::Matmul => self.matmul_f32,
408 BlueprintKind::Conv2d => self.conv2d_f32,
409 BlueprintKind::Other => self.vector_add_f32,
410 };
411 if matches!(dtype, Dtype::F16) {
412 Tolerance {
413 ulps: base.ulps.saturating_mul(self.f16_ulp_multiplier),
414 abs: base.abs * self.f16_ulp_multiplier as f32,
415 rel: base.rel * self.f16_ulp_multiplier as f32,
416 }
417 } else {
418 base
419 }
420 }
421}
422
423impl Default for ToleranceTable {
424 fn default() -> Self {
425 Self::default_table()
426 }
427}
428
429// ---------------------------------------------------------------------
430// CPU reference interpreter (T38).
431//
432// Reproduces the f32 lane semantics declared in `TensorWasmOp` so the
433// proptest harness has a known-good output to compare the future GPU
434// readback against. The interpreter does NOT model launch geometry —
435// it walks the op list once in order, treating the input bytes as a
436// little-endian f32 stream consumed by `LoadUnified` and producing a
437// little-endian f32 stream consumed by `StoreUnified`. This matches
438// the PTX emitter's offset accounting (4 bytes per lane, ascending).
439// ---------------------------------------------------------------------
440
441/// Errors produced by [`reference_eval`].
442#[derive(Debug, Clone, PartialEq, Eq)]
443pub enum ReferenceEvalError {
444 /// The blueprint references an op the reference interpreter does
445 /// not yet model (currently: matmul + barrier — the proptest
446 /// harness skips matmul shapes via the dedicated reduction
447 /// reference, see `matmul_reference` below).
448 UnsupportedOp,
449 /// The input byte buffer is shorter than the blueprint's declared
450 /// load offset reach.
451 InputTooShort,
452 /// The op sequence pops more values than it pushed — only fires
453 /// on malformed blueprints (the proptest strategies never emit
454 /// them).
455 StackUnderflow,
456}
457
458/// Interpret a blueprint over `inputs` (treated as a little-endian
459/// f32 stream) and produce the corresponding little-endian f32 output
460/// stream. This is the **ground truth** the proptest harness asserts
461/// the GPU path against.
462///
463/// The interpreter mirrors the PTX emitter's offset accounting in
464/// [`crate::ptx_emit::lower_body`]: every `LoadUnified { lanes }`
465/// reads `lanes` consecutive f32s from the input cursor; every
466/// `StoreUnified { lanes }` writes `lanes` consecutive f32s to the
467/// output cursor; arithmetic ops pop two (or three for FMA) values
468/// from the value stack and push one result per lane.
469pub fn reference_eval(
470 bp: &TensorWasmKernelBlueprint,
471 inputs: &[u8],
472) -> Result<Vec<u8>, ReferenceEvalError> {
473 let mut stack: Vec<f32> = Vec::with_capacity(bp.ops.len());
474 let mut output: Vec<u8> = Vec::new();
475 let mut in_cursor: usize = 0;
476
477 for op in &bp.ops {
478 match op {
479 TensorWasmOp::LoadUnified { elem, lanes } => {
480 // The reference interpreter models f32 lane semantics only
481 // (it pushes `f32`). Integer / f64 element types are routed
482 // to `UnsupportedOp` so the oracle skips rather than
483 // validating an integer kernel against an f32 model. (The
484 // emitter's element-type fix means such blueprints can now
485 // exist; the f32 oracle simply doesn't cover them yet.)
486 if *elem != ElemType::F32 {
487 return Err(ReferenceEvalError::UnsupportedOp);
488 }
489 let lanes = *lanes as usize;
490 for _ in 0..lanes {
491 let end = in_cursor
492 .checked_add(4)
493 .ok_or(ReferenceEvalError::InputTooShort)?;
494 if end > inputs.len() {
495 return Err(ReferenceEvalError::InputTooShort);
496 }
497 let mut buf = [0u8; 4];
498 buf.copy_from_slice(&inputs[in_cursor..end]);
499 stack.push(f32::from_le_bytes(buf));
500 in_cursor = end;
501 }
502 }
503 TensorWasmOp::StoreUnified { elem, lanes } => {
504 if *elem != ElemType::F32 {
505 return Err(ReferenceEvalError::UnsupportedOp);
506 }
507 let lanes = *lanes as usize;
508 // Stores pop in reverse-push order to match the PTX
509 // emitter's `value_stack.pop()` walk.
510 let mut popped: Vec<f32> = Vec::with_capacity(lanes);
511 for _ in 0..lanes {
512 popped.push(stack.pop().ok_or(ReferenceEvalError::StackUnderflow)?);
513 }
514 for v in popped.into_iter().rev() {
515 output.extend_from_slice(&v.to_le_bytes());
516 }
517 }
518 TensorWasmOp::VecAdd { elem, lanes } => {
519 // Element-wise (lane-aligned) add. Two prior `LoadUnified`
520 // ops push operand vectors contiguously, so the stack is
521 // `[a0..a_{n-1}, b0..b_{n-1}]` with `b` on top. Pair lane `i`
522 // of `a` with lane `i` of `b` — NOT a scalar pop-top-two,
523 // which would cross-pair lanes and feed results back in.
524 if *elem != ElemType::F32 {
525 return Err(ReferenceEvalError::UnsupportedOp);
526 }
527 let lanes = *lanes as usize;
528 let (a, b) = pop_two_lane_vectors(&mut stack, lanes)?;
529 for i in 0..lanes {
530 stack.push(a[i] + b[i]);
531 }
532 }
533 TensorWasmOp::VecMul { elem, lanes } => {
534 if *elem != ElemType::F32 {
535 return Err(ReferenceEvalError::UnsupportedOp);
536 }
537 let lanes = *lanes as usize;
538 let (a, b) = pop_two_lane_vectors(&mut stack, lanes)?;
539 for i in 0..lanes {
540 stack.push(a[i] * b[i]);
541 }
542 }
543 TensorWasmOp::VecFma { elem, lanes } => {
544 // Lane-aligned `a*b + c` over three operand vectors
545 // (`[a.., b.., c..]`, `c` on top). Single-rounding contract —
546 // mirrors `fma.rn.f32`.
547 if *elem != ElemType::F32 {
548 return Err(ReferenceEvalError::UnsupportedOp);
549 }
550 let lanes = *lanes as usize;
551 let c = pop_lane_vector(&mut stack, lanes)?;
552 let b = pop_lane_vector(&mut stack, lanes)?;
553 let a = pop_lane_vector(&mut stack, lanes)?;
554 for i in 0..lanes {
555 stack.push(a[i].mul_add(b[i], c[i]));
556 }
557 }
558 TensorWasmOp::Barrier => {
559 // No-op for the single-thread reference (the barrier
560 // exists only to synchronise CTA threads on the GPU
561 // path).
562 }
563 TensorWasmOp::MatMul { .. } => {
564 // The proptest harness routes matmul through
565 // [`matmul_reference`] directly instead of the
566 // blueprint interpreter — the IR doesn't carry the
567 // tile-load/store sequence needed to drive the
568 // generic interpreter. We surface UnsupportedOp here
569 // so callers know to use the dedicated path.
570 return Err(ReferenceEvalError::UnsupportedOp);
571 }
572 }
573 }
574
575 Ok(output)
576}
577
578/// Pop the top `lanes` values off the operand stack, preserving their
579/// pushed (lane) order: the returned vec is `[v0, v1, .., v_{lanes-1}]`
580/// where `v_{lanes-1}` was on top. Errors on underflow.
581fn pop_lane_vector(stack: &mut Vec<f32>, lanes: usize) -> Result<Vec<f32>, ReferenceEvalError> {
582 if stack.len() < lanes {
583 return Err(ReferenceEvalError::StackUnderflow);
584 }
585 Ok(stack.split_off(stack.len() - lanes))
586}
587
588/// Pop two lane-aligned operand vectors. The stack layout after two
589/// `LoadUnified` ops is `[a.., b..]` with `b` on top, so the first pop
590/// yields `b` and the second yields `a`; both are returned in lane order
591/// as `(a, b)`.
592fn pop_two_lane_vectors(
593 stack: &mut Vec<f32>,
594 lanes: usize,
595) -> Result<(Vec<f32>, Vec<f32>), ReferenceEvalError> {
596 let b = pop_lane_vector(stack, lanes)?;
597 let a = pop_lane_vector(stack, lanes)?;
598 Ok((a, b))
599}
600
601/// Standalone matmul reference (M x K) * (K x N) -> (M x N), all f32
602/// row-major. Used by the proptest harness for the matmul blueprint
603/// shape — the IR-level [`TensorWasmOp::MatMul`] is rejected by both
604/// the PTX emitter and the reference interpreter today, so the
605/// harness drives the comparison against this CPU-side reference
606/// instead.
607pub fn matmul_reference(
608 m: usize,
609 k: usize,
610 n: usize,
611 a: &[f32],
612 b: &[f32],
613) -> Result<Vec<f32>, ReferenceEvalError> {
614 if a.len() != m * k || b.len() != k * n {
615 return Err(ReferenceEvalError::InputTooShort);
616 }
617 let mut out = vec![0.0f32; m * n];
618 for i in 0..m {
619 for j in 0..n {
620 let mut acc = 0.0f32;
621 for kk in 0..k {
622 acc = a[i * k + kk].mul_add(b[kk * n + j], acc);
623 }
624 out[i * n + j] = acc;
625 }
626 }
627 Ok(out)
628}
629
630/// Standalone 2D convolution reference (single channel, stride 1, no
631/// padding). Input `H x W`, kernel `Kh x Kw`; output `(H-Kh+1) x
632/// (W-Kw+1)`. Mirrors the rewriter's `Conv2d` lowering, which the
633/// PTX emitter expresses as a sequence of `LoadUnified` +
634/// `VecFma` + `StoreUnified` ops over a sliding window.
635pub fn conv2d_reference(
636 h: usize,
637 w: usize,
638 kh: usize,
639 kw: usize,
640 input: &[f32],
641 kernel: &[f32],
642) -> Result<Vec<f32>, ReferenceEvalError> {
643 if input.len() != h * w || kernel.len() != kh * kw {
644 return Err(ReferenceEvalError::InputTooShort);
645 }
646 if h < kh || w < kw {
647 return Err(ReferenceEvalError::InputTooShort);
648 }
649 let oh = h - kh + 1;
650 let ow = w - kw + 1;
651 let mut out = vec![0.0f32; oh * ow];
652 for i in 0..oh {
653 for j in 0..ow {
654 let mut acc = 0.0f32;
655 for ki in 0..kh {
656 for kj in 0..kw {
657 let v = input[(i + ki) * w + (j + kj)];
658 let k = kernel[ki * kw + kj];
659 acc = v.mul_add(k, acc);
660 }
661 }
662 out[i * ow + j] = acc;
663 }
664 }
665 Ok(out)
666}
667
668// ---------------------------------------------------------------------
669// Structural oracle for the EXPERIMENTAL wmma MatMul lowering (gate).
670//
671// We cannot execute PTX in this environment, so the oracle that gates
672// the `enable_experimental_matmul` flag validates the STRUCTURE of the
673// emitted instruction sequence rather than a numeric readback: the
674// correct fragment shapes, the correct number of `wmma.mma.sync` ops for
675// the tiling, correct accumulator chaining (the mma's `c` and `d`
676// operands name the same accumulator fragment), and register-declaration
677// consistency (every `%rb`/`%f` fragment register the wmma ops name is
678// covered by the `.reg` header). This is the same class of structural
679// assertion the `ptx_emit` unit tests use; the proptest harness drives
680// it across random m16n16k16 inputs so the gate must pass before anyone
681// flips the feature on.
682// ---------------------------------------------------------------------
683
684/// A single mismatch found by [`check_wmma_structure`]. The proptest
685/// gate fails on any non-empty report.
686#[derive(Debug, Clone, PartialEq, Eq)]
687pub enum WmmaStructuralError {
688 /// The expected number of `wmma.mma.sync` ops (one per k16 tile)
689 /// was not emitted.
690 MmaCountMismatch {
691 /// Number of `wmma.mma.sync` ops the tiling requires.
692 expected: usize,
693 /// Number actually emitted.
694 actual: usize,
695 },
696 /// A required wmma load/store op is missing from the sequence.
697 MissingOp(&'static str),
698 /// An operand or accumulator fragment had the wrong register count.
699 FragmentShapeMismatch {
700 /// Which fragment (a/b/c/d).
701 which: &'static str,
702 /// Register count the m16n16k16 contract requires.
703 expected: usize,
704 /// Register count found in the emitted operand list.
705 actual: usize,
706 },
707 /// The mma.sync's `c` accumulator operand and `d` result operand are
708 /// not the same fragment — the accumulator is not chained in place.
709 AccumulatorNotChained,
710 /// A fragment register named by a wmma op is outside the range the
711 /// `.reg` header declares.
712 RegisterDeclInconsistent(&'static str),
713}
714
715/// Expected wmma fragment register count for the m16n16k16 shape. Mirrors
716/// `ptx_emit::WMMA_OPERAND_FRAG_REGS` / `WMMA_ACC_FRAG_REGS` (both 8);
717/// re-declared here so the oracle is an INDEPENDENT check rather than a
718/// tautology against the emitter's own constants.
719const WMMA_FRAG_REGS: usize = 8;
720
721/// Parse the `{...}` operand list that follows the first occurrence of
722/// `marker` in `text`, returning the comma-separated register tokens.
723fn fragment_operands(text: &str, marker: &str) -> Option<Vec<String>> {
724 let start = text.find(marker)?;
725 let rest = &text[start..];
726 let open = rest.find('{')?;
727 let close = rest[open..].find('}')? + open;
728 let inner = &rest[open + 1..close];
729 Some(
730 inner
731 .split(',')
732 .map(|t| t.trim().to_string())
733 .filter(|t| !t.is_empty())
734 .collect(),
735 )
736}
737
738/// Parse the count `N` from a `.reg .<class> %<prefix><N>;` declaration.
739fn reg_decl_count(text: &str, prefix: &str) -> Option<u32> {
740 for line in text.lines() {
741 let line = line.trim();
742 if line.starts_with(".reg") && line.contains(&format!("%{prefix}<")) {
743 return line
744 .split('<')
745 .nth(1)
746 .and_then(|s| s.split('>').next())
747 .and_then(|s| s.trim().parse().ok());
748 }
749 }
750 None
751}
752
753/// Returns the max index used by a `%prefixN` register token list, or
754/// `None` if any token is malformed.
755fn max_reg_index(tokens: &[String], prefix: &str) -> Option<u32> {
756 let needle = format!("%{prefix}");
757 let mut max = None;
758 for t in tokens {
759 let n: u32 = t.strip_prefix(&needle)?.parse().ok()?;
760 max = Some(max.map_or(n, |m: u32| m.max(n)));
761 }
762 max
763}
764
765/// Validate the structure of the EXPERIMENTAL wmma MatMul PTX for a
766/// single `m16n16k16` tile. Returns the (possibly empty) list of
767/// structural errors; an empty list is a PASS.
768///
769/// This is the gate the differential proptest runs across random
770/// matmul inputs. It encodes the m16n16k16 contract independently of the
771/// emitter so a regression in `ptx_emit` surfaces here as a divergence
772/// rather than silently changing both sides.
773pub fn check_wmma_structure(ptx: &str, m: u32, n: u32, k: u32) -> Vec<WmmaStructuralError> {
774 let mut errs = Vec::new();
775
776 // One mma.sync per 16x16x16 tile. For the single modelled shape this
777 // is the product of the per-dimension tile counts (== 1 for 16/16/16).
778 let tiles_m = m.div_ceil(16) as usize;
779 let tiles_n = n.div_ceil(16) as usize;
780 let tiles_k = k.div_ceil(16) as usize;
781 let expected_mma = tiles_m * tiles_n * tiles_k;
782 let actual_mma = ptx.matches("wmma.mma.sync.aligned").count();
783 if actual_mma != expected_mma {
784 errs.push(WmmaStructuralError::MmaCountMismatch {
785 expected: expected_mma,
786 actual: actual_mma,
787 });
788 }
789
790 // Required ops in the sequence.
791 for (needle, label) in [
792 ("wmma.load.a.sync.aligned.row.m16n16k16", "wmma.load.a"),
793 ("wmma.load.b.sync.aligned.col.m16n16k16", "wmma.load.b"),
794 ("wmma.load.c.sync.aligned.row.m16n16k16", "wmma.load.c"),
795 ("wmma.store.d.sync.aligned.row.m16n16k16", "wmma.store.d"),
796 ] {
797 if !ptx.contains(needle) {
798 errs.push(WmmaStructuralError::MissingOp(label));
799 }
800 }
801
802 // Fragment shapes: a/b operands and the c/d accumulator must each
803 // name exactly WMMA_FRAG_REGS registers.
804 let frag_checks: [(&str, &str); 3] = [
805 ("wmma.load.a.sync.aligned.row.m16n16k16", "a"),
806 ("wmma.load.b.sync.aligned.col.m16n16k16", "b"),
807 ("wmma.load.c.sync.aligned.row.m16n16k16", "c"),
808 ];
809 for (marker, which) in frag_checks {
810 if let Some(ops) = fragment_operands(ptx, marker) {
811 if ops.len() != WMMA_FRAG_REGS {
812 errs.push(WmmaStructuralError::FragmentShapeMismatch {
813 which,
814 expected: WMMA_FRAG_REGS,
815 actual: ops.len(),
816 });
817 }
818 }
819 }
820
821 // Accumulator chaining: the mma.sync names four fragments
822 // `d, a, b, c`; `d` and `c` must be identical (paired accumulator).
823 if let Some(mma_ops) = fragment_operands(ptx, "wmma.mma.sync.aligned") {
824 // The operand list is the FIRST {…}; for `d, a, b, c` the four
825 // fragments are concatenated, so the d-fragment is the first
826 // WMMA_FRAG_REGS tokens and the c-fragment is the last
827 // WMMA_FRAG_REGS tokens of the full four-fragment register list.
828 // `fragment_operands` only captured the first braces group (the
829 // `d` fragment); we re-parse the full instruction to compare d vs c.
830 let _ = mma_ops; // d-fragment shape is covered by the store check.
831 if let Some(line) = ptx.lines().find(|l| l.contains("wmma.mma.sync.aligned")) {
832 // Collect every {...} group on the (possibly continued) mma
833 // instruction. The emitter writes it on one logical line.
834 let groups: Vec<Vec<String>> = collect_brace_groups(line);
835 if groups.len() == 4 {
836 let d_frag = &groups[0];
837 let c_frag = &groups[3];
838 if d_frag != c_frag {
839 errs.push(WmmaStructuralError::AccumulatorNotChained);
840 }
841 if d_frag.len() != WMMA_FRAG_REGS {
842 errs.push(WmmaStructuralError::FragmentShapeMismatch {
843 which: "d",
844 expected: WMMA_FRAG_REGS,
845 actual: d_frag.len(),
846 });
847 }
848 } else {
849 errs.push(WmmaStructuralError::AccumulatorNotChained);
850 }
851 }
852 }
853
854 // Register-declaration consistency: every %rb/%f fragment register
855 // named by the wmma ops must be inside the `.reg` header's declared
856 // range (count == max_index + 1).
857 let collect_all = |marker: &str, prefix: &str| -> Option<u32> {
858 fragment_operands(ptx, marker).and_then(|ops| max_reg_index(&ops, prefix))
859 };
860 let rb_max = [
861 collect_all("wmma.load.a.sync.aligned.row.m16n16k16", "rb"),
862 collect_all("wmma.load.b.sync.aligned.col.m16n16k16", "rb"),
863 ]
864 .into_iter()
865 .flatten()
866 .max();
867 if let Some(used) = rb_max {
868 match reg_decl_count(ptx, "rb") {
869 Some(decl) if decl > used => {}
870 _ => errs.push(WmmaStructuralError::RegisterDeclInconsistent("rb")),
871 }
872 }
873 if let Some(used) = collect_all("wmma.load.c.sync.aligned.row.m16n16k16", "f") {
874 match reg_decl_count(ptx, "f") {
875 Some(decl) if decl > used => {}
876 _ => errs.push(WmmaStructuralError::RegisterDeclInconsistent("f")),
877 }
878 }
879
880 errs
881}
882
883/// Collect every `{...}` register-list group on a single PTX line, in
884/// order. Used to pull the four fragments off the `wmma.mma.sync`
885/// instruction (`d, a, b, c`).
886fn collect_brace_groups(line: &str) -> Vec<Vec<String>> {
887 let mut groups = Vec::new();
888 let mut rest = line;
889 while let Some(open) = rest.find('{') {
890 let after = &rest[open + 1..];
891 let Some(close_rel) = after.find('}') else {
892 break;
893 };
894 let inner = &after[..close_rel];
895 let toks: Vec<String> = inner
896 .split(',')
897 .map(|t| t.trim().to_string())
898 .filter(|t| !t.is_empty())
899 .collect();
900 groups.push(toks);
901 rest = &after[close_rel + 1..];
902 }
903 groups
904}
905
906// ---------------------------------------------------------------------
907// CUDA runtime detection.
908// ---------------------------------------------------------------------
909
910/// Returns `true` iff this host has a usable CUDA device AND the
911/// crate was built with the `cuda-oxide-backend` feature flag.
912///
913/// Today this always returns `false` outside the `cuda-oxide-backend`
914/// feature gate — the cudarc/cuda-oxide handle that proves a device
915/// is reachable does not exist on the no-CUDA build profile. v0.4
916/// (the S22 self-hosted runner integration) extends this to call
917/// `cudarc::driver::CudaDevice::new(0).is_ok()` so the same compiled
918/// binary skips on CPU-only hosts and runs the full comparison on
919/// CUDA hosts.
920fn cuda_runtime_available() -> bool {
921 #[cfg(feature = "cuda-oxide-backend")]
922 {
923 // S22 wiring point — `cudarc::driver::CudaDevice::new(0)` goes
924 // here. Until that lands, even the `cuda-oxide-backend`
925 // feature-gated build returns `false` so unit tests stay
926 // deterministic.
927 false
928 }
929 #[cfg(not(feature = "cuda-oxide-backend"))]
930 {
931 false
932 }
933}
934
935/// Copy up to the first 16 bytes of `slice` into a fixed-size buffer.
936/// Surface for [`OracleVerdict::HostOnlyOk::cpu_output_first_bytes`].
937fn head_bytes(slice: &[u8]) -> [u8; 16] {
938 let mut out = [0u8; 16];
939 let n = slice.len().min(16);
940 out[..n].copy_from_slice(&slice[..n]);
941 out
942}
943
944#[cfg(test)]
945mod tests {
946 use super::*;
947 use crate::ir::{GridHint, TensorWasmKernelBlueprint, TensorWasmOp};
948
949 fn add_blueprint(lanes: u32) -> TensorWasmKernelBlueprint {
950 let elem = ElemType::F32;
951 TensorWasmKernelBlueprint::new("vector_add")
952 .push(TensorWasmOp::LoadUnified { elem, lanes })
953 .push(TensorWasmOp::LoadUnified { elem, lanes })
954 .push(TensorWasmOp::VecAdd { elem, lanes })
955 .push(TensorWasmOp::StoreUnified { elem, lanes })
956 .with_grid(GridHint {
957 total_threads: lanes,
958 preferred_block_size: lanes,
959 })
960 }
961
962 #[test]
963 fn reference_eval_vector_add_matches_native() {
964 let bp = add_blueprint(4);
965 let a = [1.0f32, 2.0, 3.0, 4.0];
966 let b = [10.0f32, 20.0, 30.0, 40.0];
967 let mut input = Vec::new();
968 for v in a.iter().chain(b.iter()) {
969 input.extend_from_slice(&v.to_le_bytes());
970 }
971 let out = reference_eval(&bp, &input).expect("eval");
972 assert_eq!(out.len(), 16);
973 let expected: Vec<f32> = a.iter().zip(b.iter()).map(|(x, y)| x + y).collect();
974 for (i, &e) in expected.iter().enumerate() {
975 let mut buf = [0u8; 4];
976 buf.copy_from_slice(&out[i * 4..(i + 1) * 4]);
977 assert_eq!(f32::from_le_bytes(buf), e);
978 }
979 }
980
981 #[test]
982 fn tolerance_strict_rejects_one_ulp() {
983 let t = Tolerance::STRICT;
984 let a = 1.0f32;
985 let b = f32::from_bits(a.to_bits() + 1);
986 assert!(!t.approx_eq_f32(a, b));
987 assert!(t.approx_eq_f32(a, a));
988 }
989
990 #[test]
991 fn tolerance_default_accepts_one_ulp() {
992 let t = ToleranceTable::default().for_blueprint(BlueprintKind::VectorAdd, Dtype::F32);
993 let a = 1.0f32;
994 let b = f32::from_bits(a.to_bits() + 1);
995 assert!(t.approx_eq_f32(a, b));
996 }
997
998 #[test]
999 fn classify_picks_matmul() {
1000 let bp = TensorWasmKernelBlueprint::new("k").push(TensorWasmOp::MatMul {
1001 m: 16,
1002 n: 16,
1003 k: 16,
1004 });
1005 assert_eq!(BlueprintKind::classify(&bp), BlueprintKind::Matmul);
1006 }
1007
1008 #[test]
1009 fn matmul_reference_smoke() {
1010 // 2x2 * 2x2 identity case.
1011 let a = [1.0f32, 2.0, 3.0, 4.0];
1012 let b = [1.0f32, 0.0, 0.0, 1.0];
1013 let out = matmul_reference(2, 2, 2, &a, &b).expect("matmul");
1014 assert_eq!(out, vec![1.0, 2.0, 3.0, 4.0]);
1015 }
1016
1017 #[test]
1018 fn conv2d_reference_smoke() {
1019 // 3x3 input, 2x2 kernel of all-ones -> 2x2 output of partial
1020 // sums.
1021 let input = [1.0f32, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0];
1022 let kernel = [1.0f32; 4];
1023 let out = conv2d_reference(3, 3, 2, 2, &input, &kernel).expect("conv");
1024 assert_eq!(out, vec![12.0, 16.0, 24.0, 28.0]);
1025 }
1026
1027 #[test]
1028 fn oracle_default_runs_cpu_path_when_input_present() {
1029 let bp = add_blueprint(2);
1030 let mut input = Vec::new();
1031 for v in [1.0f32, 2.0, 10.0, 20.0] {
1032 input.extend_from_slice(&v.to_le_bytes());
1033 }
1034 let verdict = DifferentialOracle::new().compare(&bp, &input);
1035 // With a runnable input on a no-CUDA host, the CPU path
1036 // executes and the verdict is HostOnlyOk.
1037 match verdict {
1038 OracleVerdict::HostOnlyOk { cpu_output_len, .. } => {
1039 assert_eq!(cpu_output_len, 2 * 4);
1040 }
1041 other => panic!("expected HostOnlyOk, got {other:?}"),
1042 }
1043 }
1044
1045 #[test]
1046 fn wmma_structure_accepts_opt_in_emission() {
1047 use crate::ptx_emit::{emit_with, EmitConfig};
1048 let bp = TensorWasmKernelBlueprint::new("matmul").push(TensorWasmOp::MatMul {
1049 m: 16,
1050 n: 16,
1051 k: 16,
1052 });
1053 let cfg = EmitConfig {
1054 enable_experimental_matmul: true,
1055 ..EmitConfig::default()
1056 };
1057 let ptx = emit_with(&bp, &cfg).expect("opt-in emit");
1058 let errs = check_wmma_structure(&ptx.text, 16, 16, 16);
1059 assert!(errs.is_empty(), "structural oracle flagged: {errs:?}");
1060 }
1061
1062 #[test]
1063 fn wmma_structure_rejects_unchained_accumulator() {
1064 // Hand-craft a wmma block where the mma's `d` and `c` fragments
1065 // differ — the exact silent-miscompile the oracle must catch.
1066 let ptx = "\
1067 .reg .b32 %rb<16>;\n\
1068 .reg .f32 %f<16>;\n\
1069 wmma.load.a.sync.aligned.row.m16n16k16.global.f16 {%rb0, %rb1, %rb2, %rb3, %rb4, %rb5, %rb6, %rb7}, [%rd0], 16;\n\
1070 wmma.load.b.sync.aligned.col.m16n16k16.global.f16 {%rb8, %rb9, %rb10, %rb11, %rb12, %rb13, %rb14, %rb15}, [%rd2], 16;\n\
1071 wmma.load.c.sync.aligned.row.m16n16k16.global.f32 {%f0, %f1, %f2, %f3, %f4, %f5, %f6, %f7}, [%rd3], 16;\n\
1072 wmma.mma.sync.aligned.row.col.m16n16k16.f32.f32 {%f0, %f1, %f2, %f3, %f4, %f5, %f6, %f7}, {%rb0, %rb1, %rb2, %rb3, %rb4, %rb5, %rb6, %rb7}, {%rb8, %rb9, %rb10, %rb11, %rb12, %rb13, %rb14, %rb15}, {%f8, %f9, %f10, %f11, %f12, %f13, %f14, %f15};\n\
1073 wmma.store.d.sync.aligned.row.m16n16k16.global.f32 [%rd1], {%f0, %f1, %f2, %f3, %f4, %f5, %f6, %f7}, 16;\n";
1074 let errs = check_wmma_structure(ptx, 16, 16, 16);
1075 assert!(errs.contains(&WmmaStructuralError::AccumulatorNotChained));
1076 }
1077
1078 #[test]
1079 fn wmma_structure_rejects_missing_store() {
1080 let ptx = "\
1081 wmma.load.a.sync.aligned.row.m16n16k16.global.f16 {%rb0, %rb1, %rb2, %rb3, %rb4, %rb5, %rb6, %rb7}, [%rd0], 16;\n\
1082 wmma.mma.sync.aligned.row.col.m16n16k16.f32.f32 {%f0}, {%rb0}, {%rb8}, {%f0};\n";
1083 let errs = check_wmma_structure(ptx, 16, 16, 16);
1084 assert!(errs.contains(&WmmaStructuralError::MissingOp("wmma.store.d")));
1085 }
1086
1087 #[test]
1088 fn oracle_default_falls_back_to_no_cuda_skip_for_unrunnable_blueprint() {
1089 // Mirrors the contract in `differential_scaffold.rs`: a
1090 // blueprint with no Load/Store ops + empty input is not
1091 // runnable by the reference interpreter, so the oracle
1092 // returns the v0.3.6 "no-cuda" skip — exactly what the
1093 // scaffold tests check via `reason.contains("no-cuda")`.
1094 let bp = TensorWasmKernelBlueprint::new("oracle_fixture").push(TensorWasmOp::VecAdd {
1095 elem: ElemType::F32,
1096 lanes: 4,
1097 });
1098 let verdict = DifferentialOracle::new().compare(&bp, &[]);
1099 match verdict {
1100 OracleVerdict::Skipped(reason) => {
1101 assert!(reason.contains("no-cuda"));
1102 }
1103 other => panic!("expected Skipped, got {other:?}"),
1104 }
1105 }
1106}