Module matrix 

The INT8 weight-stationary GEMM path of the CUDA tier — the workload a GPU (and an RDU) actually exists for: O(M×N) = A(M×K) · W(K×N) in int8, the shape every transformer projection and attention dot reduces to.

Unlike the scalar tier (super::wrap) this is NOT a lift of the C body — it is a purpose-built DP4A kernel (Ampere’s 4×int8→int32 dot-product intrinsic), so there is no device-libc question. It is gated on the SAME certified capability the fabric lowering uses (FabricTarget::require_gemm) and — crucially — its numerics are anchored to the certified crate::codegen_sva::systolic::eval_systolic reference (itself ≡ VM ≡ SAT-placed PE ≡ iverilog, weight_stationary_gemm_lock). Running the emitted kernel and comparing to eval_systolic adds a CUDA rung to that existing proof chain (cuda_matrix_lock).

Accumulation is int32 (DP4A’s native width); eval_systolic wraps in i64. For the int8 operands and the small K the lock exercises, no int32 overflow occurs, so the two agree exactly — the lock keeps K in that safe range on purpose.

Structs

CudaGemmArtifact

A complete int8 weight-stationary GEMM CUDA program (weights + activations baked, computed with DP4A, printed row-major) plus its Makefile.

Functions

blockscaled_gemm_dequant

GROUND TRUTH (f64): dequantize every element (q * scale) then multiply-accumulate. The unambiguous meaning of a Q8_0 matmul, order-independent.

blockscaled_gemm_int8

WHAT THE DP4A KERNEL COMPUTES: an exact int32 dot within each 32-block, scaled once by the two block scales, accumulated in f64. Algebraically identical to blockscaled_gemm_dequant (the scale is constant across a block) — the lock proves the implementation matches, catching any scale-indexing bug.

emit_int8_gemm

Emit a DP4A int8 GEMM CUDA program for O(m×n) = A(m×k) · W(k×n), with weights (k*n row-major, W[r][c] = weights[r*n+c]) and acts (m*k row-major) baked in. Refuses (typed) if the RDU-shaped target does not advertise int8 weight-stationary GEMM — the exact certified gate the fabric uses.

emit_scaled_int8_gemm

Emit a block-scaled Q8_0 GEMM CUDA program: DP4A int8 dot per 32-block, scaled by the baked f32 block scales, accumulated in f32. Prints O(m×n) row-major as %.9g (one per line). k must be a multiple of 32 (whole Q8_0 blocks). Refuses (typed) if the RDU-shaped target lacks int8 weight-stationary GEMM.

lower_elementwise_to_cuda

Lower a recognized elementwise op (C[p] = A[p] ⊕ B[p], from crate::tensor_recognize::recognize_elementwise) to a self-contained CUDA program — the elementwise analog of lower_matmul_to_cuda. One thread per element; the deterministic int8-range fill and the Σ C checksum match the matmul emitter’s convention, so it runs and prints on the GPU. A B of one row holds that row’s elements and is read at each element’s column.

lower_matmul_to_cuda

Lower a RECOGNIZED LOGOS matmul (C(M×N) = A(M×K)·B(K×N), from crate::tensor_recognize::recognize_matmul) to a self-contained CUDA program whose dims ARE the source program’s — the compiler generating the kernel, not a template. The emitted program reproduces the LOGOS matmul’s deterministic int8-range fill (a[p]=(p%7)-3, b[p]=(p%5)-2), computes C=A·B on the GPU, and prints the checksum Σ C — so its stdout equals the VM’s Show checksum byte-for-byte. M,N,K are baked from the spec.

lower_matmul_to_cuda_with

Lower a recognized matmul under an explicit CudaKnobs point. The precision knob selects the kernel: ResolvedPrecision::Int64 (always-correct i64 accumulation, the general default) or ResolvedPrecision::Int8Dp4a (__dp4a int8 fast path — valid only when operands fit int8, which is why it is opt-in). Both reproduce the LOGOS program’s fill + checksum, so both equal the VM byte-for-byte on any int8-safe program; they differ only in how the contraction is computed on the GPU.

lower_reduction_to_cuda

Lower a recognized reduction (rmsnorm/softmax, from crate::tensor_recognize::recognize_reduction) with the program’s epsilon to a self-contained float CUDA program — the reduction analog of lower_matmul_to_cuda. Deterministic float fill, one thread per element, and a Σ Y checksum printed with fixed precision so it compiles + runs on the GPU.

sample_gemm_data

A reproducible int8 (weights K×N row-major, acts M×K row-major) sample in [-128, 127], shared by compile_to_cuda_gemm and the lock so the emitted kernel and the eval_systolic oracle read identical data (no drift). Deterministic in the indices — no RNG.