feat(math-cuda): RPX256 permutation kernel source + host known-answer harness (lane K, phase 1)

[MauroToscano]

Lane K, phase 1 of the per-table GPU redo (EXECUTION step 4): the RPX256 / XHash12 permutation as CUDA kernel source that also compiles on the host through the Track G shim, plus the host known-answer harness. New files only; no build.rs / lib.rs / device.rs / lde.rs / fri.rs / Makefile edits (those are requests below).

Files

• crypto/math-cuda/kernels/rpx.cu — rpx::permute (schedule FB E FB E FB E M), rpx::Sponge + rpx::sponge_leaf (rate-8 OVERWRITE duplex, capacity lane 8 = len mod 8, lane 9 = "LFML"), rpx::compress (one permutation of [l ‖ r ‖ 0⁴]). Constants are RPO's ARK1/ARK2/MDS row, transcribed by script from rpo.rs. Output is canonicalised so digests match digest_to_commitment bytes.
• crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp — the harness (make test-rpx-host-kat once the Makefile target lands; see request 1).
• crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h — data: miden-crypto's 19 RPO hash_elements vectors (external) + the three Rust-oracle tables.
• prover/tests/rpx_host_kat_vectors.rs — #[ignore]d generator that prints the oracle tables from lfm::rpx::Rpx256, algebraic_commit::sponge_leaf, HasherKind::Rpx.compress.
• crypto/math-cuda/src/rpx.rs — phase-2 placeholder, deliberately not declared in lib.rs.

Oracle and anchoring

The oracle is prover/src/lfm/rpx.rs byte for byte. The harness layers its anchoring the way that module's own provenance note does: (1) field primitives vs schoolbook __int128; (2) MDS vs its per-term definition, S-boxes vs generic exponentiation (incl. x^INV_ALPHA), cubic extension vs naive polynomial arithmetic mod φ³ − φ − 1; (3) external: seven fb_round<R> composed = RPO256, replayed over miden's 19 vectors — pins ARK1/ARK2, MDS row + orientation, both S-box chains, the sponge lane convention; (4) the Rust oracle: permutation (10 states incl. all-zero, all-(p−1)), leaf at 0/1/7/8/9/16/17 felts, two parents; (5) negative controls (RPX ≠ RPO, every lane reaches the output, raw [p, 2^64) inputs ≡ canonical, outputs canonical); (6) op counts measured.

The u128 MDS property (rpo.rs:527-536) is ported, not rediscovered: one reduction per output lane, no per-term field multiply; the device assembles the same 73-bit integer from two 32-bit half-sums (each ≤ 160·(2^32−1) < 2^40), so the MDS is 288 single 32×32→64 MACs + 12 reductions.

Gate (host compile, laptop, Makefile's HOST_KAT_CXXFLAGS)

$ c++ -std=c++17 -O2 -Wall -Wno-unknown-pragmas -Icrypto/math-cuda/tests/host_kat -Icrypto/math-cuda/kernels \
      -o target/host_kat/rpx_host_kat crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp   # 2.1 s, no diagnostics
$ ./target/host_kat/rpx_host_kat
field primitives vs schoolbook __int128: 644 edge pairs + random, mul/add/dot3
MDS (u128-property port) vs per-term definition: 79 states incl. raw-max and one-hot
S-boxes vs generic exponentiation: 60 values, x^7, x^{1/7}, both compositions
cubic extension (φ³ = φ + 1) vs naive polynomial arithmetic: 67 pairs, mul/square/power7
★ EXTERNAL: seven fb_round<R> = RPO256 vs miden-crypto hash_elements: 19/19 matched
★ ORACLE: rpx::permute vs Rust Rpx256::permute: 10/10 vectors matched
leaf: rpx::Sponge vs sponge_leaf transcription at 41 lengths (0..40)
★ ORACLE: rpx::sponge_leaf vs Rust sponge_leaf(Rpx): 7/7 lengths matched
★ ORACLE: rpx::compress vs Rust HasherKind::Rpx.compress: 2/2 parents matched
negative control: RPX(0..12) != RPO(0..12); permute(0) != 0
representation: raw [p, 2^64) inputs agree with canonical; outputs canonical (32 states)
negative control: each of the 12 input lanes moves the output
ALL HOST KAT CHECKS PASS

Before the oracle tables were pasted, the same binary reported exactly the five expected FAIL lines for the three empty tables and nothing else. The generator ran on box A at 824d678 (release): test result: ok. 1 passed; 0 failed. cargo check -p lambda-vm-prover --test rpx_host_kat_vectors: clean, 32.7 s.

Op counts (measured by the harness; MDS static)

unit	Goldilocks mul	3-term dot3 (wide products)	add	MDS
x^7	4	–	–	–
x^{1/7}	72 (63 sq + 9)	–	–	–
ext_mul	–	3 (9)	2	–
FB round	912	–	48	2
E round	–	48 (144)	44	–
M round	–	–	24	1
RPX permutation	2736	144 (432)	300	7 (2016 narrow MACs)
RPO permutation	6384	–	336	14

Inverse S-box = 2592 / 2736 of the field multiplications.

Requests to the coordinator

1. Makefile: add test-rpx-host-kat to the .PHONY list (line 6, after test-blake3-host-kat) and, after the test-blake3-host-kat recipe (~line 623):

   test-rpx-host-kat:
   	@mkdir -p target/host_kat
   	$(CXX) $(HOST_KAT_CXXFLAGS) \
   	    -o target/host_kat/rpx_host_kat $(HOST_KAT_DIR)/rpx_host_kat.cpp
   	./target/host_kat/rpx_host_kat

2. make lint on a box (laptop rule): expect the only Rust delta, prover/tests/rpx_host_kat_vectors.rs, to be clean; cargo fmt --all already ran.
3. Phase 2 (after lane D merges): build.rs gets compile_kernel("rpx.cu", "rpx.cubin", have_nvcc, &[]) (+ rerun-if-changed), lib.rs gets pub mod rpx;. Until then nothing compiles rpx.cu under nvcc.

Open risks

• nvcc acceptance is unverified (no local CUDA). Constructs used all have in-tree precedent (__device__ __constant__ arrays, __device__ constexpr scalars, templated __device__ functions, #pragma unroll), but the first cubin build is phase 2's.
• No published RPX vector exists; the E round and the schedule are pinned to the Rust oracle only, as on the host.
• Register pressure / spills in inv_sbox (72-deep chain × 12 lanes) and the dynamic index in Sponge::absorb are phase-2 measurements (-Xptxas -v).