|
| 1 | +/- |
| 2 | +Copyright (c) 2026 TorchLean |
| 3 | +Released under MIT license as described in the file LICENSE. |
| 4 | +Authors: TorchLean Team |
| 5 | +-/ |
| 6 | + |
| 7 | +module |
| 8 | + |
| 9 | +public import NN.Runtime.Autograd.Engine.Cuda.Buffer |
| 10 | +public import NN.Runtime.Autograd.Engine.Cuda.TexTable |
| 11 | +public import NN.Tests.Runtime.Cuda.Utils |
| 12 | + |
| 13 | +/-! |
| 14 | +# CUDA Kernel Coverage: Lookup-Table Textures |
| 15 | +
|
| 16 | +Validates `Runtime.Autograd.Cuda.TexTable` against an executable `Float32` reference: |
| 17 | +
|
| 18 | +- **point mode** must match the reference **bit-for-bit** in both builds (the CPU stub and the |
| 19 | + CUDA kernel evaluate the same clamp/floor/lerp in float32 with FMA contraction blocked); |
| 20 | +- **hardware mode** is compared by tolerance (`2⁻⁸` of the local sample gap): CUDA's texture unit |
| 21 | + uses a 9-bit fixed-point lerp weight whose rounding is unspecified; |
| 22 | +- **integer-node fetches** must be bit-exact in *both* modes (the lerp weight is exactly 0 there) — |
| 23 | + this probe catches any texel-center (`±0.5`) coordinate-convention error; |
| 24 | +- edge behavior: clamping below/above the abscissa range, layer-index clamping, `width = 1`, |
| 25 | + and empty coordinate buffers. |
| 26 | +-/ |
| 27 | + |
| 28 | +@[expose] public section |
| 29 | + |
| 30 | +namespace Tests |
| 31 | +namespace Cuda |
| 32 | +namespace TexTable |
| 33 | + |
| 34 | +open Runtime.Autograd.Cuda |
| 35 | + |
| 36 | +/-- Float32 clamp mirroring the native kernels' `fminf(fmaxf(u, 0), wmax)`. -/ |
| 37 | +def clampF32 (x lo hi : Float32) : Float32 := |
| 38 | + if x < lo then lo else if x > hi then hi else x |
| 39 | + |
| 40 | +/-- |
| 41 | +Executable reference for `TexTable.fetch`, computed in Lean core `Float32` (IEEE binary32, the |
| 42 | +same arithmetic as the native kernels). Mirrors the CPU stub statement-for-statement; in point |
| 43 | +mode the CUDA kernel is bit-identical by construction, in hardware mode the CUDA texture unit may |
| 44 | +round the 9-bit weight differently (hence tolerance). |
| 45 | +-/ |
| 46 | +def refFetch (tab : Array Float32) (width layers : Nat) (hw : Bool) |
| 47 | + (u layer : Float32) : Float32 := |
| 48 | + let wmax : Float32 := Float32.ofNat (width - 1) |
| 49 | + let uc := clampF32 u 0.0 wmax |
| 50 | + let lF := clampF32 (layer + 0.5) 0.0 (Float32.ofNat (layers - 1)) |
| 51 | + let L := lF.toFloat.toUInt64.toNat |
| 52 | + let j := uc.floor |
| 53 | + let f := uc - j |
| 54 | + let f := if hw then Float32.floor (f * 256.0 + 0.5) / 256.0 else f |
| 55 | + let j0 := j.toFloat.toUInt64.toNat |
| 56 | + let j1 := if j0 + 1 < width then j0 + 1 else width - 1 |
| 57 | + let a := tab[L * width + j0]! |
| 58 | + let b := tab[L * width + j1]! |
| 59 | + a + f * (b - a) |
| 60 | + |
| 61 | +/-- The float64 sample grid used by every test below (3 layers × 7 samples, non-trivial values). -/ |
| 62 | +def sampleData (width layers : Nat) : FloatArray := Id.run do |
| 63 | + let mut a := FloatArray.emptyWithCapacity (width * layers) |
| 64 | + for l in [0:layers] do |
| 65 | + for i in [0:width] do |
| 66 | + let x := Float.ofNat i |
| 67 | + let y := Float.ofNat l |
| 68 | + a := a.push (0.17 * x - 0.031 * x * x + 0.4 * y + 0.05) |
| 69 | + return a |
| 70 | + |
| 71 | +/-- Run one fetch through the native path and the reference, returning both as `Float32`. -/ |
| 72 | +def runFetch (t : TexTable) (tab32 : Array Float32) (width layers : Nat) (hw : Bool) |
| 73 | + (coords layerIdx : FloatArray) : IO (Array Float32 × Array Float32) := do |
| 74 | + let out := Buffer.toFloatArray |
| 75 | + (Runtime.Autograd.Cuda.TexTable.fetch t (Buffer.ofFloatArray coords) |
| 76 | + (Buffer.ofFloatArray layerIdx)) |
| 77 | + let mut native : Array Float32 := #[] |
| 78 | + let mut refv : Array Float32 := #[] |
| 79 | + for i in [0:out.size] do |
| 80 | + native := native.push (out[i]!).toFloat32 |
| 81 | + refv := refv.push |
| 82 | + (refFetch tab32 width layers hw (coords[i]!).toFloat32 (layerIdx[i]!).toFloat32) |
| 83 | + return (native, refv) |
| 84 | + |
| 85 | +/-- Assert bitwise equality of native and reference results. -/ |
| 86 | +def assertBits (msg : String) (native refv : Array Float32) : IO Unit := do |
| 87 | + for i in [0:native.size] do |
| 88 | + let x := native[i]! |
| 89 | + let y := refv[i]! |
| 90 | + unless x.toBits == y.toBits do |
| 91 | + throw <| IO.userError |
| 92 | + s!"{msg}[{i}]: native {x} (bits {x.toBits}) ≠ reference {y} (bits {y.toBits})" |
| 93 | + |
| 94 | +/-- Assert tolerance agreement of native and reference results. -/ |
| 95 | +def assertTol (msg : String) (native refv : Array Float32) (tol : Float) : IO Unit := do |
| 96 | + for i in [0:native.size] do |
| 97 | + let x := (native[i]!).toFloat |
| 98 | + let y := (refv[i]!).toFloat |
| 99 | + Utils.assertApprox s!"{msg}[{i}]" x y (tol := tol) |
| 100 | + |
| 101 | +def widthN : Nat := 7 |
| 102 | +def layersN : Nat := 3 |
| 103 | + |
| 104 | +/-- Interior, boundary, and out-of-range grid coordinates across all layers. -/ |
| 105 | +def probeCoords : FloatArray := |
| 106 | + FloatArray.mk #[0.0, 0.25, 1.0, 2.5, 3.75, 5.999, 6.0, -1.5, 9.75, 4.125, 2.875, 0.001] |
| 107 | + |
| 108 | +def probeLayers : FloatArray := |
| 109 | + FloatArray.mk #[0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2] |
| 110 | + |
| 111 | +def runPointMode : IO Unit := do |
| 112 | + IO.println "== textable point mode (bit-exact) ==" |
| 113 | + let data := sampleData widthN layersN |
| 114 | + let tab32 := (Array.range data.size).map fun i => (data[i]!).toFloat32 |
| 115 | + let t := Runtime.Autograd.Cuda.TexTable.ofFloatArray data widthN layersN (hwFilter := false) |
| 116 | + unless Runtime.Autograd.Cuda.TexTable.width t == widthN && |
| 117 | + Runtime.Autograd.Cuda.TexTable.layers t == layersN && |
| 118 | + Runtime.Autograd.Cuda.TexTable.filterHw t == false do |
| 119 | + throw <| IO.userError "textable point: metadata mismatch" |
| 120 | + let (native, refv) ← runFetch t tab32 widthN layersN false probeCoords probeLayers |
| 121 | + assertBits "textable point" native refv |
| 122 | + |
| 123 | +def runHardwareMode : IO Unit := do |
| 124 | + IO.println "== textable hardware mode (tolerance) ==" |
| 125 | + let data := sampleData widthN layersN |
| 126 | + let tab32 := (Array.range data.size).map fun i => (data[i]!).toFloat32 |
| 127 | + let t := Runtime.Autograd.Cuda.TexTable.ofFloatArray data widthN layersN (hwFilter := true) |
| 128 | + unless Runtime.Autograd.Cuda.TexTable.filterHw t == true do |
| 129 | + throw <| IO.userError "textable hw: metadata mismatch" |
| 130 | + let (native, refv) ← runFetch t tab32 widthN layersN true probeCoords probeLayers |
| 131 | + -- Weight quantization bounds the error by 2⁻⁸ · max |Δ sample| (≈ 0.17 here), plus slack for |
| 132 | + -- the unspecified hardware weight rounding. |
| 133 | + assertTol "textable hw" native refv (tol := 2.0e-3) |
| 134 | + |
| 135 | +/-- Integer-node fetches return stored samples bit-exactly in both modes (texel-center probe). -/ |
| 136 | +def runIntegerNodes : IO Unit := do |
| 137 | + IO.println "== textable integer nodes (bit-exact, both modes) ==" |
| 138 | + let data := sampleData widthN layersN |
| 139 | + let mut coords : FloatArray := FloatArray.emptyWithCapacity (widthN * layersN) |
| 140 | + let mut lidx : FloatArray := FloatArray.emptyWithCapacity (widthN * layersN) |
| 141 | + for l in [0:layersN] do |
| 142 | + for i in [0:widthN] do |
| 143 | + coords := coords.push (Float.ofNat i) |
| 144 | + lidx := lidx.push (Float.ofNat l) |
| 145 | + for hw in [false, true] do |
| 146 | + let t := Runtime.Autograd.Cuda.TexTable.ofFloatArray data widthN layersN (hwFilter := hw) |
| 147 | + let out := Buffer.toFloatArray |
| 148 | + (Runtime.Autograd.Cuda.TexTable.fetch t (Buffer.ofFloatArray coords) |
| 149 | + (Buffer.ofFloatArray lidx)) |
| 150 | + for i in [0:out.size] do |
| 151 | + let got := (out[i]!).toFloat32 |
| 152 | + let want := (data[i]!).toFloat32 |
| 153 | + unless got.toBits == want.toBits do |
| 154 | + throw <| IO.userError |
| 155 | + s!"textable integer node (hw={hw})[{i}]: got {got}, want stored sample {want}" |
| 156 | + |
| 157 | +def runEdges : IO Unit := do |
| 158 | + IO.println "== textable edges (width=1, layer clamp, empty) ==" |
| 159 | + -- width = 1: every coordinate hits the single sample. |
| 160 | + let one := FloatArray.mk #[0.75, -0.75] |
| 161 | + let t1 := Runtime.Autograd.Cuda.TexTable.ofFloatArray one 1 2 (hwFilter := false) |
| 162 | + let outs := Buffer.toFloatArray |
| 163 | + (Runtime.Autograd.Cuda.TexTable.fetch t1 |
| 164 | + (Buffer.ofFloatArray (FloatArray.mk #[0.0, 3.5, -2.0])) |
| 165 | + (Buffer.ofFloatArray (FloatArray.mk #[0, 0, 1]))) |
| 166 | + let expect : Array Float := #[0.75, 0.75, -0.75] |
| 167 | + for i in [0:outs.size] do |
| 168 | + unless ((outs[i]!).toFloat32).toBits == ((expect[i]!).toFloat32).toBits do |
| 169 | + throw <| IO.userError s!"textable width=1[{i}]: got {outs[i]!}, want {expect[i]!}" |
| 170 | + -- layer index out of range clamps to the last layer. |
| 171 | + let outc := Buffer.toFloatArray |
| 172 | + (Runtime.Autograd.Cuda.TexTable.fetch t1 |
| 173 | + (Buffer.ofFloatArray (FloatArray.mk #[0.0])) |
| 174 | + (Buffer.ofFloatArray (FloatArray.mk #[7.0]))) |
| 175 | + unless ((outc[0]!).toFloat32).toBits == ((-0.75 : Float).toFloat32).toBits do |
| 176 | + throw <| IO.userError s!"textable layer clamp: got {outc[0]!}, want -0.75" |
| 177 | + -- empty coordinate buffer yields an empty result. |
| 178 | + let oute := Buffer.toFloatArray |
| 179 | + (Runtime.Autograd.Cuda.TexTable.fetch t1 |
| 180 | + (Buffer.ofFloatArray (FloatArray.mk #[])) |
| 181 | + (Buffer.ofFloatArray (FloatArray.mk #[]))) |
| 182 | + unless oute.size == 0 do |
| 183 | + throw <| IO.userError s!"textable empty: expected empty result, got size {oute.size}" |
| 184 | + |
| 185 | +/-- Unified TexTable test entrypoint. -/ |
| 186 | +def run : IO Unit := do |
| 187 | + runPointMode |
| 188 | + runHardwareMode |
| 189 | + runIntegerNodes |
| 190 | + runEdges |
| 191 | + |
| 192 | +end TexTable |
| 193 | +end Cuda |
| 194 | +end Tests |
0 commit comments