From effb28fcb1039278780080ff40de1ad9a62c2c6a Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 7 Sep 2026 13:53:01 -0300 Subject: [PATCH 1/3] test(prover): Rust-oracle vector generator for the RPX host known-answer harness An #[ignore]d integration test that prints, as C++ source, the tables crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h embeds: the bare RPX permutation on ten states (all-zero, all-(p-1), 0..12, alternating, two one-hot lanes, four seeded random), the rate-8 overwrite-duplex leaf at lengths 0, 1, 7, 8, 9, 16 and 17 felts, and two parents. miden publishes no RPX known-answer table, so lfm::rpx::Rpx256 is the oracle the device kernel is pinned to. Outputs are canonical; inputs are derived from fixed seeds and printed alongside them so the header stays self-contained data. --- prover/tests/rpx_host_kat_vectors.rs | 188 +++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 prover/tests/rpx_host_kat_vectors.rs diff --git a/prover/tests/rpx_host_kat_vectors.rs b/prover/tests/rpx_host_kat_vectors.rs new file mode 100644 index 000000000..1ed80b11f --- /dev/null +++ b/prover/tests/rpx_host_kat_vectors.rs @@ -0,0 +1,188 @@ +//! Generator for the Rust-oracle tables in +//! `crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h`. +//! +//! The RPX device kernel (`crypto/math-cuda/kernels/rpx.cu`) is pinned to THIS +//! crate's `Rpx256` through the host known-answer harness `rpx_host_kat.cpp`. +//! miden publishes no RPX known-answer table (`lfm/rpx.rs`, "PROVENANCE"), so +//! the Rust host implementation IS the oracle, and this test prints the tables +//! the harness embeds, as C++ source: +//! +//! Table 2 — the bare permutation on ten states: all-zero, all-(p−1), +//! `0..12`, alternating, two one-hot lanes, four random; +//! Table 3 — the rate-8 OVERWRITE-duplex leaf (`algebraic_commit::sponge_leaf`) +//! at lengths 0, 1, 7, 8, 9, 16, 17 felts; +//! Table 4 — the parent `compress(l, r)` = one permutation of `[l ‖ r ‖ 0⁴]`. +//! +//! Every printed value is CANONICAL (`< p`); the harness canonicalises the +//! kernel's output before comparing, so the representation the two sides keep +//! internally never enters the comparison. +//! +//! `#[ignore]`d because it prints rather than asserts. Run with +//! +//! cargo test -p lambda-vm-prover --test rpx_host_kat_vectors -- --ignored --nocapture +//! +//! and paste everything between the `>>> BEGIN` / `<<< END` lines over the +//! matching region of `rpx_kat_vectors.h`. The inputs are DERIVED HERE from +//! fixed seeds and printed alongside the outputs, so the header stays +//! self-contained data — the harness never regenerates anything. + +use lambda_vm_prover::lfm::algebraic_commit::sponge_leaf; +use lambda_vm_prover::lfm::hash::{HASH_STATE_FELTS, HasherKind, LfmHasher}; +use lambda_vm_prover::lfm::rpx::Rpx256; +use lambda_vm_prover::tables::types::FE; + +/// The Goldilocks prime, for canonicalising raw values and for the `p − 1` +/// input. +const P: u64 = 0xFFFF_FFFF_0000_0001; + +/// The leaf lengths the phase-1 gate names: empty, a partial block, one felt +/// under a block, an exact block (no trailing permutation), one over, two exact +/// blocks, two blocks plus one. +const LEAF_LENGTHS: [usize; 7] = [0, 1, 7, 8, 9, 16, 17]; + +/// Widest leaf in Table 3 — the header's fixed-width `felts[]` array. +const LEAF_MAX_FELTS: usize = 17; + +/// splitmix64 — a fixed, documented PRNG so the inputs are reproducible from +/// the seed alone. +fn splitmix64(seed: &mut u64) -> u64 { + *seed = seed.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = *seed; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) +} + +/// A canonical random felt. +fn random_felt(seed: &mut u64) -> u64 { + splitmix64(seed) % P +} + +/// The canonical `u64` of a field element. `value()` is the raw storage, which +/// the field allows to sit in `[p, 2^64)`; one subtraction canonicalises it. +fn canonical(f: &FE) -> u64 { + let v = *f.value(); + if v >= P { v - P } else { v } +} + +fn fe_array(raw: &[u64; N]) -> [FE; N] { + core::array::from_fn(|i| FE::from(raw[i])) +} + +fn cpp_list(vals: &[u64]) -> String { + vals.iter() + .map(|v| format!("{v}ull")) + .collect::>() + .join(", ") +} + +/// The ten permutation inputs, each with the name the harness prints on a +/// failure. +fn permutation_inputs() -> Vec<(&'static str, [u64; HASH_STATE_FELTS])> { + let mut v: Vec<(&'static str, [u64; HASH_STATE_FELTS])> = vec![ + ("all-zero", [0; HASH_STATE_FELTS]), + ("all-(p-1)", [P - 1; HASH_STATE_FELTS]), + ("lanes 0..12", core::array::from_fn(|i| i as u64)), + ( + "alternating 0 / p-1", + core::array::from_fn(|i| if i % 2 == 0 { 0 } else { P - 1 }), + ), + ("one-hot lane 0", core::array::from_fn(|i| u64::from(i == 0))), + ( + "one-hot lane 11", + core::array::from_fn(|i| u64::from(i == HASH_STATE_FELTS - 1)), + ), + ]; + let names = ["random #1", "random #2", "random #3", "random #4"]; + for (k, name) in names.iter().enumerate() { + let mut seed = 0x5250_5800_0000_0000 + k as u64; // "RPX\0" + k + v.push((name, core::array::from_fn(|_| random_felt(&mut seed)))); + } + v +} + +#[test] +#[ignore = "prints the Rust-oracle tables for rpx_kat_vectors.h; run with --ignored --nocapture"] +fn print_rpx_host_kat_vectors() { + let mut out = String::new(); + out.push_str("// >>> BEGIN RUST-ORACLE TABLES — generated by\n"); + out.push_str( + "// cargo test -p lambda-vm-prover --test rpx_host_kat_vectors -- --ignored --nocapture\n", + ); + out.push_str("// (prover/tests/rpx_host_kat_vectors.rs). Paste verbatim; do not edit by hand.\n\n"); + + // ---- Table 2: the bare permutation ------------------------------------ + let inputs = permutation_inputs(); + out.push_str(&format!( + "inline constexpr int NUM_RPX_PERMUTATION_VECTORS = {};\n", + inputs.len() + )); + out.push_str( + "inline constexpr RpxPermutationVector RPX_PERMUTATION_VECTORS[NUM_RPX_PERMUTATION_VECTORS] = {\n", + ); + for (name, input) in &inputs { + let got = Rpx256.permute(fe_array(input)); + let got: Vec = got.iter().map(canonical).collect(); + out.push_str(&format!( + " {{\"{name}\",\n {{{}}},\n {{{}}}}},\n", + cpp_list(input), + cpp_list(&got) + )); + } + out.push_str("};\n\n"); + + // ---- Table 3: the leaf sponge ----------------------------------------- + out.push_str(&format!( + "inline constexpr int NUM_RPX_LEAF_VECTORS = {};\n", + LEAF_LENGTHS.len() + )); + out.push_str("inline constexpr RpxLeafVector RPX_LEAF_VECTORS[NUM_RPX_LEAF_VECTORS] = {\n"); + for &len in &LEAF_LENGTHS { + let mut seed = 0x1EAF_0000_0000_0000 + len as u64; + let raw: Vec = (0..len).map(|_| random_felt(&mut seed)).collect(); + let felts: Vec = raw.iter().map(|&r| FE::from(r)).collect(); + let digest = sponge_leaf(HasherKind::Rpx, &felts); + let digest: Vec = digest.iter().map(canonical).collect(); + // Fixed-width row: the tail beyond `len` is zero and never read. + let mut padded = raw.clone(); + padded.resize(LEAF_MAX_FELTS, 0); + out.push_str(&format!( + " {{{len}u,\n {{{}}},\n {{{}}}}},\n", + cpp_list(&padded), + cpp_list(&digest) + )); + } + out.push_str("};\n\n"); + + // ---- Table 4: the parent ------------------------------------------------ + let mut seed = 0x5041_5245_4E54_0000; // "PARENT" + let random_l: [u64; 4] = core::array::from_fn(|_| random_felt(&mut seed)); + let random_r: [u64; 4] = core::array::from_fn(|_| random_felt(&mut seed)); + let parents: [(&str, [u64; 4], [u64; 4]); 2] = [ + ( + "digits 0..8", + core::array::from_fn(|i| i as u64), + core::array::from_fn(|i| i as u64 + 4), + ), + ("random", random_l, random_r), + ]; + out.push_str(&format!( + "inline constexpr int NUM_RPX_PARENT_VECTORS = {};\n", + parents.len() + )); + out.push_str("inline constexpr RpxParentVector RPX_PARENT_VECTORS[NUM_RPX_PARENT_VECTORS] = {\n"); + for (name, l, r) in &parents { + let got = HasherKind::Rpx.compress(&fe_array(l), &fe_array(r)); + let got: Vec = got.iter().map(canonical).collect(); + out.push_str(&format!( + " {{\"{name}\",\n {{{}}},\n {{{}}},\n {{{}}}}},\n", + cpp_list(l), + cpp_list(r), + cpp_list(&got) + )); + } + out.push_str("};\n"); + out.push_str("// <<< END RUST-ORACLE TABLES\n"); + + println!("{out}"); +} From 50c633e1b8f77d2828cbfad56447496aca753647 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 7 Sep 2026 15:37:42 -0300 Subject: [PATCH 2/3] feat(math-cuda): RPX256 permutation kernel source with a host known-answer harness Lane K, phase 1 of the per-table GPU redo: kernels/rpx.cu carries the Rescue-Prime eXtended (XHash12) permutation over Goldilocks at width 12, the rate-8 overwrite-duplex leaf sponge and the Merkle parent, written to compile both under nvcc and on the host through cuda_host_shim.h. No launch code, no build.rs/lib.rs wiring yet (phase 2; src/rpx.rs is a documented placeholder that nothing compiles). The oracle is the Rust host implementation, prover/src/lfm/rpx.rs, and the constants are RPO's, transcribed mechanically from rpo.rs. The MDS ports rpo.rs's u128-accumulation property: one reduction per output lane and no per-term field multiplication, assembled on device from two 32-bit half-sums (each below 2^40 because the circulant row sums to 160), so the whole MDS is 288 narrow multiply-adds and 12 reductions. The inverse S-box is miden's 72-step chain (63 squarings, 9 products) per lane; the cubic extension is phi^3 = phi + 1 with each coefficient folded into one three-term dot product, deliberately NOT ext3.cuh's w^3 = 2 product. tests/host_kat/rpx_host_kat.cpp layers its anchoring the way the Rust module does: field primitives against schoolbook __int128 arithmetic; the MDS, both S-boxes and the extension against independent algorithms; seven FB rounds composed into RPO256 and replayed over miden-crypto's nineteen hash_elements vectors (external); and the RPX permutation, leaf sponge and parent against tables printed by the Rust oracle (prover/tests/rpx_host_kat_vectors.rs, run on a box). It also checks raw vs canonical inputs, that RPX is not RPO, that every lane reaches the output, and counts the field operations per round kind so the cost model is a measurement: 2736 multiplications, 144 dot products and 300 adds plus 7 MDS per permutation, against RPO's 6384 and 14. --- crypto/math-cuda/kernels/rpx.cu | 451 ++++++++++++ crypto/math-cuda/src/rpx.rs | 21 + .../math-cuda/tests/host_kat/rpx_host_kat.cpp | 687 ++++++++++++++++++ .../tests/host_kat/rpx_kat_vectors.h | 162 +++++ prover/tests/rpx_host_kat_vectors.rs | 13 +- 5 files changed, 1331 insertions(+), 3 deletions(-) create mode 100644 crypto/math-cuda/kernels/rpx.cu create mode 100644 crypto/math-cuda/src/rpx.rs create mode 100644 crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp create mode 100644 crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h diff --git a/crypto/math-cuda/kernels/rpx.cu b/crypto/math-cuda/kernels/rpx.cu new file mode 100644 index 000000000..cd5657d48 --- /dev/null +++ b/crypto/math-cuda/kernels/rpx.cu @@ -0,0 +1,451 @@ +// RPX256 (Rescue-Prime eXtended / XHash12) over Goldilocks at width 12 on +// device — the permutation, the rate-8 overwrite-duplex leaf sponge and the +// Merkle parent. Phase 1 of the per-table GPU redo's lane K: arithmetic only. +// The leaf/tree kernels that stream table rows through `rpx::Sponge` and +// `rpx::compress` are phase 2 and follow `blake3.cu:338-620`'s shape. +// +// THE ORACLE is the Rust host implementation, byte for byte: +// `prover/src/lfm/rpx.rs` `Rpx256::permute` (:280-316) — schedule FB E FB E FB E M, +// `cubic_ext::{mul, power7}` (:118-140); +// `prover/src/lfm/rpo.rs` ARK1/ARK2 (:119-321, RPX imports RPO's tables +// literally), `sbox` (:455-460), `inv_sbox_layer` +// (:481-509, the 72-multiplication chain), `mds` +// (:539-557, the u128 accumulation); +// `prover/src/lfm/algebraic_commit.rs` `leaf_capacity` (:142-147), +// `sponge_leaf` (:169-184), `parent` (:248-252); +// `prover/src/lfm/hash.rs` `permute_two_cells` (:95-108): `[a ‖ b ‖ iv]`, +// digest = lanes 0..4. +// +// PROVENANCE, layered exactly as the Rust module's own (rpx.rs "PROVENANCE"): +// the FB round IS RPO's round with RPO's constants, and those are pinned by +// nineteen EXTERNAL miden-crypto vectors, which `tests/host_kat/rpx_host_kat.cpp` +// replays through `fb_round` composed seven times. The E round (the cubic +// extension) and the schedule have no published vector anywhere; they are +// pinned to the Rust oracle's output (`prover/tests/rpx_host_kat_vectors.rs`) +// and, independently, to naive polynomial arithmetic in the harness. +// +// REPRESENTATION. Inputs may be raw `[0, 2^64)` Goldilocks storage exactly as +// `goldilocks.cuh` allows everywhere else; every step here (`add`, `mul`, +// `dot3`, the MDS bound) accepts that. `permute` CANONICALISES its output, so +// digests are canonical `< p` and their big-endian bytes are what +// `digest_to_commitment` (algebraic_commit.rs:112-118) writes — the device +// Merkle tree can be compared to the host's byte for byte. +// +// ⚠ TWO CUBIC EXTENSIONS EXIST AND THIS FILE USES THE OTHER ONE. `ext3.cuh` is +// the VM's `w³ = 2`; RPX's is `φ³ = φ + 1` (rpx.rs:98-103). Only the GENERIC +// three-term dot product `ext3::dot3` is borrowed from that header — never +// `ext3::mul`. The reduction polynomial lives in `rpx::ext_mul` alone. +// +// COST MODEL (one permutation; counted by the harness's op counters, static +// for the MDS): +// FB round ×3 : 12·(4 + 72) = 912 Goldilocks multiplications (48 forward +// S-box, 864 inverse), 2 MDS, 24 constant adds; +// E round ×3 : 4 triples × 4 extension products = 16 `ext_mul` = 144 wide +// 64×64 products folded into 48 reductions (`dot3`), 12 +// constant adds, 32 operand pre-adds; +// M round ×1 : 1 MDS, 12 constant adds; +// MDS ×7 : 288 32×32→64 multiply-adds + 12 reductions each — the ported +// u128 property (see `mds`), ~6× under twelve field +// multiplications per lane. +// Total: 2736 field multiplications + 144 dot3 (432 wide products) + 300 adds +// + 2016 narrow MACs. The inverse S-box is 2592/2736 = 95% of the field +// multiplications; RPO spends 7 such layers, RPX 3 — that is the whole +// reason RPX exists (rpx.rs:22-28). +// +// PHASE-2 TUNING NOTES (not done here, do not guess at them): `inv_sbox` is a +// serial 72-deep chain per lane — one thread per permutation interleaves twelve +// of them; register pressure is what to measure (`-Xptxas -v`). `Sponge::absorb` +// indexes the state dynamically, which nvcc lowers to local memory unless the +// caller's loop is unrolled — the same trade `Blake3Chain::push_word` makes. +// ARK reads are warp-uniform constant-bank operands and cost nothing. + +#include +#include "goldilocks.cuh" +#include "ext3.cuh" + +namespace rpx { + +enum : int { + STATE_FELTS = 12, + RATE_FELTS = 8, + CAPACITY_FELTS = 4, + DIGEST_FELTS = 4, + NUM_ROUNDS = 7, + EXT_DEGREE = 3, + EXT_ELEMENTS = 4, + // Absolute lanes of the two capacity cells the socket names: the padding + // flag (`rpo.rs:339` CAPACITY_PAD_LANE = 0 within the capacity) and the + // domain tag (`rpo.rs:343` CAPACITY_DOMAIN_LANE = 1). Capacity = lanes 8..12. + CAPACITY_PAD_LANE = RATE_FELTS + 0, + CAPACITY_DOMAIN_LANE = RATE_FELTS + 1, +}; + +// The Merkle-parent domain is ZERO on purpose (rpo.rs:350): a parent is a +// standard `Rpx256::merge`, checkable against miden without this codebase. +__device__ constexpr uint64_t DOMAIN_COMPRESS = 0; +// The leaf domain: `u32::from_le_bytes(b"LFML")` (rpo.rs:358) = 1280132684. +__device__ constexpr uint64_t DOMAIN_LEAF = 0x4C4D464CULL; + +// --------------------------------------------------------------------------- +// Constants. Transcribed MECHANICALLY (a script over rpo.rs, not by hand) from +// `rpo.rs` ARK1 (:119-218), ARK2 (:222-321) and MDS_CIRC_ROW (:114). RPX +// imports exactly these (rpx.rs:69); `rpx_uses_rpos_constant_tables` asserts +// the import on the host, and the miden vectors in the harness pin them here. +// Only the FB rounds (0, 2, 4) consume ARK2; E and M rounds add ARK1 alone. +// --------------------------------------------------------------------------- +__device__ __constant__ uint64_t ARK1[NUM_ROUNDS][STATE_FELTS] = { + {5789762306288267392ull, 6522564764413701783ull, 17809893479458208203ull, 107145243989736508ull, + 6388978042437517382ull, 15844067734406016715ull, 9975000513555218239ull, 3344984123768313364ull, + 9959189626657347191ull, 12960773468763563665ull, 9602914297752488475ull, 16657542370200465908ull}, + {12987190162843096997ull, 653957632802705281ull, 4441654670647621225ull, 4038207883745915761ull, + 5613464648874830118ull, 13222989726778338773ull, 3037761201230264149ull, 16683759727265180203ull, + 8337364536491240715ull, 3227397518293416448ull, 8110510111539674682ull, 2872078294163232137ull}, + {18072785500942327487ull, 6200974112677013481ull, 17682092219085884187ull, 10599526828986756440ull, + 975003873302957338ull, 8264241093196931281ull, 10065763900435475170ull, 2181131744534710197ull, + 6317303992309418647ull, 1401440938888741532ull, 8884468225181997494ull, 13066900325715521532ull}, + {5674685213610121970ull, 5759084860419474071ull, 13943282657648897737ull, 1352748651966375394ull, + 17110913224029905221ull, 1003883795902368422ull, 4141870621881018291ull, 8121410972417424656ull, + 14300518605864919529ull, 13712227150607670181ull, 17021852944633065291ull, 6252096473787587650ull}, + {4887609836208846458ull, 3027115137917284492ull, 9595098600469470675ull, 10528569829048484079ull, + 7864689113198939815ull, 17533723827845969040ull, 5781638039037710951ull, 17024078752430719006ull, + 109659393484013511ull, 7158933660534805869ull, 2955076958026921730ull, 7433723648458773977ull}, + {16308865189192447297ull, 11977192855656444890ull, 12532242556065780287ull, 14594890931430968898ull, + 7291784239689209784ull, 5514718540551361949ull, 10025733853830934803ull, 7293794580341021693ull, + 6728552937464861756ull, 6332385040983343262ull, 13277683694236792804ull, 2600778905124452676ull}, + {7123075680859040534ull, 1034205548717903090ull, 7717824418247931797ull, 3019070937878604058ull, + 11403792746066867460ull, 10280580802233112374ull, 337153209462421218ull, 13333398568519923717ull, + 3596153696935337464ull, 8104208463525993784ull, 14345062289456085693ull, 17036731477169661256ull}, +}; + +__device__ __constant__ uint64_t ARK2[NUM_ROUNDS][STATE_FELTS] = { + {6077062762357204287ull, 15277620170502011191ull, 5358738125714196705ull, 14233283787297595718ull, + 13792579614346651365ull, 11614812331536767105ull, 14871063686742261166ull, 10148237148793043499ull, + 4457428952329675767ull, 15590786458219172475ull, 10063319113072092615ull, 14200078843431360086ull}, + {6202948458916099932ull, 17690140365333231091ull, 3595001575307484651ull, 373995945117666487ull, + 1235734395091296013ull, 14172757457833931602ull, 707573103686350224ull, 15453217512188187135ull, + 219777875004506018ull, 17876696346199469008ull, 17731621626449383378ull, 2897136237748376248ull}, + {8023374565629191455ull, 15013690343205953430ull, 4485500052507912973ull, 12489737547229155153ull, + 9500452585969030576ull, 2054001340201038870ull, 12420704059284934186ull, 355990932618543755ull, + 9071225051243523860ull, 12766199826003448536ull, 9045979173463556963ull, 12934431667190679898ull}, + {18389244934624494276ull, 16731736864863925227ull, 4440209734760478192ull, 17208448209698888938ull, + 8739495587021565984ull, 17000774922218161967ull, 13533282547195532087ull, 525402848358706231ull, + 16987541523062161972ull, 5466806524462797102ull, 14512769585918244983ull, 10973956031244051118ull}, + {6982293561042362913ull, 14065426295947720331ull, 16451845770444974180ull, 7139138592091306727ull, + 9012006439959783127ull, 14619614108529063361ull, 1394813199588124371ull, 4635111139507788575ull, + 16217473952264203365ull, 10782018226466330683ull, 6844229992533662050ull, 7446486531695178711ull}, + {3736792340494631448ull, 577852220195055341ull, 6689998335515779805ull, 13886063479078013492ull, + 14358505101923202168ull, 7744142531772274164ull, 16135070735728404443ull, 12290902521256031137ull, + 12059913662657709804ull, 16456018495793751911ull, 4571485474751953524ull, 17200392109565783176ull}, + {17130398059294018733ull, 519782857322261988ull, 9625384390925085478ull, 1664893052631119222ull, + 7629576092524553570ull, 3485239601103661425ull, 9755891797164033838ull, 15218148195153269027ull, + 16460604813734957368ull, 9643968136937729763ull, 3611348709641382851ull, 18256379591337759196ull}, +}; + +// First ROW of the circulant MDS: `M[i][j] = MDS_CIRC_ROW[(j − i) mod 12]` +// (rpo.rs:107-114). Stored 32-bit so each MDS term is one 32×32→64 MAC. The +// row sums to 160, which is the bound `mds` rests on. +__device__ __constant__ uint32_t MDS_CIRC_ROW[STATE_FELTS] = {7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8}; + +// --------------------------------------------------------------------------- +// Field-op forwarders. Under nvcc they are the `goldilocks.cuh` / `ext3.cuh` +// primitives, nothing more. The host-KAT harness defines RPX_HOST_OP_COUNT +// before including this file so it can COUNT them per round kind and print the +// cost model above as a measurement rather than a claim. +// --------------------------------------------------------------------------- +#ifdef RPX_HOST_OP_COUNT +struct OpCount { + unsigned long long mul, dot3, add; +}; +static OpCount g_ops = {0, 0, 0}; +#define RPX_COUNT(field) (++g_ops.field) +#else +#define RPX_COUNT(field) ((void)0) +#endif + +__device__ __forceinline__ uint64_t fmul(uint64_t a, uint64_t b) { + RPX_COUNT(mul); + return goldilocks::mul(a, b); +} + +__device__ __forceinline__ uint64_t fadd(uint64_t a, uint64_t b) { + RPX_COUNT(add); + return goldilocks::add(a, b); +} + +// `a0·b0 + a1·b1 + a2·b2` with ONE reduction — the generic part of `ext3.cuh`, +// independent of that header's reduction polynomial. +__device__ __forceinline__ uint64_t fdot3(uint64_t a0, uint64_t b0, uint64_t a1, uint64_t b1, + uint64_t a2, uint64_t b2) { + RPX_COUNT(dot3); + return ext3::dot3(a0, b0, a1, b1, a2, b2); +} + +// --------------------------------------------------------------------------- +// The circulant MDS, `out_i = Σ_j MDS_CIRC_ROW[(j − i) mod 12] · s_j`, in +// `rpo.rs:539-557`'s orientation (the one the miden vectors pin). +// +// ★ THE PORTED PROPERTY (rpo.rs:527-536): one accumulation and ONE reduction +// per output lane, no per-term field multiplication. Every coefficient is ≤ 26 +// and every stored lane is < 2^64, so the twelve-term row sum is < 12·26·2^64 +// < 2^73 and needs no reduction before the end. The host accumulates it in a +// u128; the device has no u128, so the SAME integer is assembled from 32-bit +// halves. With `s_j = h_j·2^32 + l_j`, +// +// acc = 2^32 · Σ_j c_j·h_j + Σ_j c_j·l_j , +// +// and each half-sum is ≤ 160·(2^32 − 1) < 2^40 — the row sums to 160 — so both +// fit a u64 with 24 bits to spare and every term is a single 32×32→64 +// multiply-add (no 64-bit multiplier anywhere in the MDS). The halves are then +// recombined into the u128's `(lo, hi)` exactly as the host holds them and +// reduced the host's way: `acc = hi·2^64 + lo ≡ lo + hi·EPSILON (mod p)`, with +// `hi < 2^9` so `hi·EPSILON < 2^41` needs no reduction of its own +// (`the_mds_row_sum_cannot_overflow_a_u128` asserts the same bound on the host). +// --------------------------------------------------------------------------- +__device__ __forceinline__ void mds(uint64_t s[STATE_FELTS]) { + uint32_t lo32[STATE_FELTS], hi32[STATE_FELTS]; +#pragma unroll + for (int j = 0; j < STATE_FELTS; ++j) { + lo32[j] = (uint32_t)s[j]; + hi32[j] = (uint32_t)(s[j] >> 32); + } + uint64_t out[STATE_FELTS]; +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) { + uint64_t acc_lo = 0, acc_hi = 0; // Σ c·l_j and Σ c·h_j, each < 2^40 +#pragma unroll + for (int j = 0; j < STATE_FELTS; ++j) { + const uint32_t c = MDS_CIRC_ROW[(j + STATE_FELTS - i) % STATE_FELTS]; + acc_lo += (uint64_t)c * (uint64_t)lo32[j]; + acc_hi += (uint64_t)c * (uint64_t)hi32[j]; + } + // acc = acc_hi·2^32 + acc_lo, exactly. Split it at bit 64. + const uint64_t lo = (acc_hi << 32) + acc_lo; + const uint64_t carry = (lo < acc_lo) ? 1ull : 0ull; + const uint64_t hi = (acc_hi >> 32) + carry; // < 2^9 + out[i] = fadd(lo, hi * goldilocks::EPSILON); + } +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = out[i]; +} + +// --------------------------------------------------------------------------- +// S-boxes. +// --------------------------------------------------------------------------- + +// `x^7` in the association the AIR's degree-3 lowering uses (rpo.rs:455-460): +// `x², x³ = x²·x, x^7 = (x³)²·x`. Two squarings, two products. +__device__ __forceinline__ uint64_t sbox(uint64_t x) { + const uint64_t x2 = fmul(x, x); + const uint64_t x3 = fmul(x2, x); + const uint64_t x6 = fmul(x3, x3); + return fmul(x6, x); +} + +template +__device__ __forceinline__ uint64_t square_n(uint64_t x) { +#pragma unroll + for (int i = 0; i < N; ++i) x = fmul(x, x); + return x; +} + +// `base^(2^M) · tail` — the inverse chain's one building block (rpo.rs:483-495). +template +__device__ __forceinline__ uint64_t exp_acc(uint64_t base, uint64_t tail) { + return fmul(square_n(base), tail); +} + +// `x^{1/7} = x^10540996611094048183` by miden-crypto's addition chain, as +// `rpo.rs:481-509` runs it lane-wise: 63 squarings + 9 products = 72 +// multiplications against ~93 for square-and-multiply. Per lane rather than +// whole-state: on a GPU the twelve lanes' independence is the compiler's to +// interleave, and a lane-wise body keeps only six values live. +__device__ __forceinline__ uint64_t inv_sbox(uint64_t x) { + const uint64_t t1 = fmul(x, x); // x^2 + const uint64_t t2 = fmul(t1, t1); // x^4 + const uint64_t t3 = exp_acc<3>(t2, t2); // x^36 + const uint64_t t4 = exp_acc<6>(t3, t3); // x^(36·65) + const uint64_t t5 = exp_acc<12>(t4, t4); // x^(36·65·4097) + const uint64_t t6 = exp_acc<6>(t5, t3); // x^0x24924924 + const uint64_t t7 = exp_acc<31>(t6, t6); // x^0x1249249224924924 + // ((t7² · t6)²)² · ((t1 · t2) · x) — rpo.rs:504-508. + const uint64_t a = square_n<2>(fmul(fmul(t7, t7), t6)); + const uint64_t b = fmul(fmul(t1, t2), x); + return fmul(a, b); +} + +// --------------------------------------------------------------------------- +// The cubic extension `GF(p)[φ] / (φ³ − φ − 1)` — rpx.rs:98-140. NOT `ext3.cuh`'s. +// --------------------------------------------------------------------------- +struct CubicExt { + uint64_t c0, c1, c2; // c0 + c1·φ + c2·φ² +}; + +// The product reduced by `φ³ = φ + 1`, `φ⁴ = φ² + φ`. `rpx.rs:118-125`'s +// closed form, regrouped so each coefficient is ONE three-term dot product +// with a single reduction (the same fold `dot_product_3` gives the VM's own +// extension): +// c0 = a0·b0 + a1·b2 + a2·b1 +// c1 = a0·b1 + a1·(b0 + b2) + a2·(b1 + b2) [= a0b1 + a1b0 + a1b2 + a2b1 + a2b2] +// c2 = a0·b2 + a1·b1 + a2·(b0 + b2) [= a0b2 + a1b1 + a2b0 + a2b2] +// Nine wide products, three reductions, two operand pre-adds. +__device__ __forceinline__ CubicExt ext_mul(const CubicExt &a, const CubicExt &b) { + const uint64_t b02 = fadd(b.c0, b.c2); + const uint64_t b12 = fadd(b.c1, b.c2); + CubicExt r; + r.c0 = fdot3(a.c0, b.c0, a.c1, b.c2, a.c2, b.c1); + r.c1 = fdot3(a.c0, b.c1, a.c1, b02, a.c2, b12); + r.c2 = fdot3(a.c0, b.c2, a.c1, b.c1, a.c2, b02); + return r; +} + +// One function for squaring and product, as on the host (rpx.rs:128-130). +__device__ __forceinline__ CubicExt ext_square(const CubicExt &a) { return ext_mul(a, a); } + +// `a^7` by `a² → a³ → a⁶ → a⁷` (rpx.rs:135-140): two squarings, two products. +__device__ __forceinline__ CubicExt ext_power7(const CubicExt &a) { + const CubicExt a2 = ext_square(a); + const CubicExt a3 = ext_mul(a2, a); + const CubicExt a6 = ext_square(a3); + return ext_mul(a6, a); +} + +// --------------------------------------------------------------------------- +// Rounds. `R` is the round index into ARK1/ARK2 — a template parameter so the +// constant-bank offsets fold at compile time. +// --------------------------------------------------------------------------- + +// FB: `MDS → +ARK1 → x^7 → MDS → +ARK2 → x^{1/7}` — RPO's round exactly +// (rpo.rs:561-582, rpx.rs:283-295). RPX runs it at R = 0, 2, 4; RPO at 0..7. +template +__device__ __forceinline__ void fb_round(uint64_t s[STATE_FELTS]) { + mds(s); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = fadd(s[i], ARK1[R][i]); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = sbox(s[i]); + mds(s); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = fadd(s[i], ARK2[R][i]); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = inv_sbox(s[i]); +} + +// E: `+ARK1 → x^7` in the cubic extension on four lane-triples, NO linear +// layer (rpx.rs:296-307; the design, not an omission — rpx.rs:275-279). +template +__device__ __forceinline__ void ext_round(uint64_t s[STATE_FELTS]) { +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = fadd(s[i], ARK1[R][i]); +#pragma unroll + for (int e = 0; e < EXT_ELEMENTS; ++e) { + const int base = e * EXT_DEGREE; + CubicExt x; + x.c0 = s[base]; + x.c1 = s[base + 1]; + x.c2 = s[base + 2]; + const CubicExt y = ext_power7(x); + s[base] = y.c0; + s[base + 1] = y.c1; + s[base + 2] = y.c2; + } +} + +// M: `MDS → +ARK1`, a linear finish with no S-box (rpx.rs:308-313). +template +__device__ __forceinline__ void final_round(uint64_t s[STATE_FELTS]) { + mds(s); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = fadd(s[i], ARK1[R][i]); +} + +// The permutation: `FB E FB E FB E M` (rpx.rs:280-316), output CANONICAL. +__device__ void permute(uint64_t s[STATE_FELTS]) { + fb_round<0>(s); + ext_round<1>(s); + fb_round<2>(s); + ext_round<3>(s); + fb_round<4>(s); + ext_round<5>(s); + final_round<6>(s); +#pragma unroll + for (int i = 0; i < STATE_FELTS; ++i) s[i] = goldilocks::canonical(s[i]); +} + +// --------------------------------------------------------------------------- +// The socket's two constructions over the permutation. +// --------------------------------------------------------------------------- + +// The rate-8 OVERWRITE duplex — `algebraic_commit::sponge_leaf` (:169-184) +// with `leaf_capacity` (:142-147), streamed. Capacity lane 8 carries the +// padding flag `len mod 8`, lane 9 the LEAF domain, lanes 10-11 zero. Each +// block OVERWRITES the eight rate lanes (spec §2.6): absorption is a store, no +// field arithmetic. The total length is needed BEFORE the first permutation +// (algebraic_commit.rs "A1"), hence `init(num_felts)`; callers absorb exactly +// that many felts. +struct Sponge { + uint64_t s[STATE_FELTS]; + int pos; + + __device__ __forceinline__ void init(uint64_t num_felts) { +#pragma unroll + for (int i = 0; i < RATE_FELTS; ++i) s[i] = 0; + s[CAPACITY_PAD_LANE] = num_felts % RATE_FELTS; + s[CAPACITY_DOMAIN_LANE] = DOMAIN_LEAF; + s[CAPACITY_DOMAIN_LANE + 1] = 0; + s[CAPACITY_DOMAIN_LANE + 2] = 0; + pos = 0; + } + + __device__ __forceinline__ void absorb(uint64_t felt) { + s[pos++] = felt; + if (pos == RATE_FELTS) { + permute(s); + pos = 0; + } + } + + // A pending partial block is zero-padded and permuted. An exact multiple of + // the rate spends no trailing permutation — including the EMPTY leaf, whose + // digest is therefore the untouched zero rate lanes, exactly what + // `sponge_leaf` returns for `felts.is_empty()` (:174-176). + __device__ __forceinline__ void finalize(uint64_t digest[DIGEST_FELTS]) { + if (pos != 0) { + for (int k = pos; k < RATE_FELTS; ++k) s[k] = 0; + permute(s); + pos = 0; + } +#pragma unroll + for (int i = 0; i < DIGEST_FELTS; ++i) digest[i] = s[i]; + } +}; + +// `sponge_leaf` over a contiguous array — the one-call form for the KAT and +// for any phase-2 kernel that has its felts in hand. +__device__ __forceinline__ void sponge_leaf(const uint64_t *felts, uint64_t num_felts, + uint64_t digest[DIGEST_FELTS]) { + Sponge sp; + sp.init(num_felts); + for (uint64_t i = 0; i < num_felts; ++i) sp.absorb(felts[i]); + sp.finalize(digest); +} + +// The Merkle parent: ONE permutation of `[left ‖ right ‖ capacity]` with the +// compress domain, which is zero (algebraic_commit.rs:248-252 → +// hash.rs:95-108). Capacity = `domain_iv(0)` = all zeros. +__device__ __forceinline__ void compress(const uint64_t left[DIGEST_FELTS], + const uint64_t right[DIGEST_FELTS], + uint64_t out[DIGEST_FELTS]) { + uint64_t s[STATE_FELTS]; +#pragma unroll + for (int i = 0; i < DIGEST_FELTS; ++i) { + s[i] = left[i]; + s[DIGEST_FELTS + i] = right[i]; + s[RATE_FELTS + i] = 0; + } + s[CAPACITY_DOMAIN_LANE] = DOMAIN_COMPRESS; + permute(s); +#pragma unroll + for (int i = 0; i < DIGEST_FELTS; ++i) out[i] = s[i]; +} + +} // namespace rpx diff --git a/crypto/math-cuda/src/rpx.rs b/crypto/math-cuda/src/rpx.rs new file mode 100644 index 000000000..3468b1e29 --- /dev/null +++ b/crypto/math-cuda/src/rpx.rs @@ -0,0 +1,21 @@ +//! RPX256 (Rescue-Prime eXtended, width 12) device launch code — PHASE 2. +//! +//! Phase 1 (lane K) ships the kernel SOURCE, `kernels/rpx.cu`, pinned by the +//! host known-answer harness `tests/host_kat/rpx_host_kat.cpp` (run with +//! `make test-rpx-host-kat`): the permutation, the rate-8 overwrite-duplex +//! leaf sponge and the Merkle parent, compiled on the host through +//! `cuda_host_shim.h` and checked against miden-crypto's RPO vectors and the +//! Rust oracle `prover/src/lfm/rpx.rs`. +//! +//! This module is the placeholder for the phase-2 launch wrappers — the leaf +//! kernels mirroring `blake3.rs`'s, `merkle_level` / `merkle_tail` over +//! `rpx::compress`, and the third arm in every `match hash` — and it is +//! deliberately NOT declared in `lib.rs` yet: nothing compiles it. Phase 2 +//! adds `pub mod rpx;` to `lib.rs` and +//! `compile_kernel("rpx.cu", "rpx.cubin", have_nvcc, &[])` to `build.rs` +//! (both lane D's files, requested through the coordinator). +//! +//! Digest layout contract for that work: a digest is four CANONICAL Goldilocks +//! felts (the kernel canonicalises every permutation output), serialised as +//! `digest_to_commitment` does — each felt's eight big-endian bytes, 32 bytes +//! per node, the same slot width as a BLAKE3 digest. diff --git a/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp b/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp new file mode 100644 index 000000000..3a980d8ff --- /dev/null +++ b/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp @@ -0,0 +1,687 @@ +// Known-answer tests for `kernels/rpx.cu`, run on the host. +// +// WHY THIS EXISTS. The GPU parity suite runs only where a GPU does, and per-PR +// CI has none — GPU CI is merge_group-only. This compiles the real kernel +// source through `cuda_host_shim.h` and pins its arithmetic in seconds, with no +// GPU and no cargo, exactly as `blake3_host_kat.cpp` does for BLAKE3. +// +// WHAT IT COVERS: the field primitives the kernel is built from, the MDS, both +// S-boxes, the cubic extension, the seven-round schedule, the rate-8 overwrite +// duplex leaf, the Merkle parent, and the raw-vs-canonical representation. +// +// WHAT IT DOES NOT COVER, and what the GPU tests are still required for: +// whether nvcc accepts the file, and every property of execution rather than +// arithmetic — grid indexing, register pressure, local-memory spills from the +// sponge's dynamic indexing. Passing here is necessary, never sufficient. +// +// HOW THE ANCHORING LAYERS. Nothing here is checked only against itself: +// 1. The field primitives (`goldilocks::mul/add`, `ext3::dot3`) against +// schoolbook `__int128` arithmetic — the definition, no shared code. +// 2. The MDS against its per-term definition; the S-boxes against generic +// exponentiation (including `x^{1/7}` as `x^INV_ALPHA`); the cubic +// extension against naive polynomial multiplication reduced by +// `φ³ = φ + 1` — the same independent algorithms `rpx.rs`'s own tests use. +// 3. ★ EXTERNAL: RPX's FB round IS RPO's round with RPO's constants. Seven +// `fb_round` compose to RPO256, and that composition is replayed over +// miden-crypto's nineteen `hash_elements` vectors, which nothing in this +// tree produced. That pins ARK1/ARK2, the MDS row and orientation, both +// S-box chains and the sponge lane convention from outside. +// 4. ★ THE ORACLE: the Rust host `Rpx256` (`prover/src/lfm/rpx.rs`), through +// the tables `prover/tests/rpx_host_kat_vectors.rs` prints — the bare +// permutation, the leaf sponge at seven lengths, the parent. miden +// publishes no RPX vector, so the E round and the schedule rest on this +// layer alone, as the Rust module's own provenance note says they must. +// 5. Negative controls: RPX ≠ RPO on the same state; every input lane +// reaches the output; raw (`≥ p`) and canonical inputs agree; outputs are +// canonical. +// 6. The cost model, COUNTED rather than asserted from a comment. +// +// Build and run with `make test-rpx-host-kat`. + +#include +#include +#include +#include + +#include "cuda_host_shim.h" + +// The kernel under test. Included, not linked: the shim turns its device +// functions into host functions, and there is no other way to call them. +// RPX_HOST_OP_COUNT turns on its field-op counters (layer 6). +#define RPX_HOST_OP_COUNT +#include "rpx.cu" + +#include "rpx_kat_vectors.h" + +namespace { + +int failures = 0; + +void check(bool ok, const char *what) { + if (!ok) { + printf("FAIL: %s\n", what); + ++failures; + } +} + +typedef unsigned __int128 u128; +const uint64_t P = 0xFFFFFFFF00000001ull; +// `7^{-1} mod (p − 1)` — rpo.rs:96. Re-derived below rather than trusted. +const uint64_t INV_ALPHA = 10540996611094048183ull; + +uint64_t canon(uint64_t x) { return x >= P ? x - P : x; } + +// =========================================================================== +// Reference arithmetic: schoolbook over `__int128`. It shares no code with the +// kernel — it is the definition the kernel's shortcuts are checked against. +// =========================================================================== + +uint64_t ref_mul(uint64_t a, uint64_t b) { + return (uint64_t)(((u128)canon(a) * (u128)canon(b)) % P); +} + +uint64_t ref_add(uint64_t a, uint64_t b) { + return (uint64_t)(((u128)canon(a) + (u128)canon(b)) % P); +} + +uint64_t ref_pow(uint64_t x, uint64_t e) { + uint64_t r = 1, b = canon(x); + while (e != 0) { + if (e & 1) r = ref_mul(r, b); + b = ref_mul(b, b); + e >>= 1; + } + return r; +} + +struct RefExt { + uint64_t c[3]; +}; + +// Naive polynomial multiplication reduced by `φ³ = φ + 1`, `φ⁴ = φ² + φ` — the +// obvious slow way, as `rpx.rs:341-352` writes it, so it shares no structure +// with the kernel's regrouped closed form. +RefExt ref_ext_mul(const RefExt &a, const RefExt &b) { + uint64_t c[5] = {0, 0, 0, 0, 0}; + for (int i = 0; i < 3; ++i) { + for (int j = 0; j < 3; ++j) c[i + j] = ref_add(c[i + j], ref_mul(a.c[i], b.c[j])); + } + RefExt r; + r.c[0] = ref_add(c[0], c[3]); + r.c[1] = ref_add(ref_add(c[1], c[3]), c[4]); + r.c[2] = ref_add(c[2], c[4]); + return r; +} + +RefExt ref_ext_pow(RefExt a, unsigned e) { + RefExt r = {{1, 0, 0}}; + while (e != 0) { + if (e & 1) r = ref_ext_mul(r, a); + a = ref_ext_mul(a, a); + e >>= 1; + } + return r; +} + +// The MDS as defined: `out_i = Σ_j ROW[(j − i) mod 12] · s_j`, one reduced +// field multiplication per term (rpo.rs:522-524). +void ref_mds(const uint64_t in[12], uint64_t out[12]) { + static const uint64_t ROW[12] = {7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8}; + for (int i = 0; i < 12; ++i) { + uint64_t acc = 0; + for (int j = 0; j < 12; ++j) acc = ref_add(acc, ref_mul(ROW[(j + 12 - i) % 12], in[j])); + out[i] = acc; + } +} + +// A deterministic value stream. Every fifth value is a RAW representation in +// `[p, 2^64)` — the field's non-canonical storage, which the kernel must read +// as `value − p` — so the reduction paths are exercised rather than assumed. +uint64_t splitmix(uint64_t &seed) { + seed += 0x9E3779B97F4A7C15ull; + uint64_t z = seed; + z = (z ^ (z >> 30)) * 0xBF58476D1CE4E5B9ull; + z = (z ^ (z >> 27)) * 0x94D049BB133111EBull; + return z ^ (z >> 31); +} + +uint64_t sample(uint64_t &seed, uint64_t i) { + uint64_t x = splitmix(seed); + // Raw values above p exist only for canonical values below 2^32 − 1. + return (i % 5 == 0) ? (x % 0xFFFFFFFFull) + P : x % P; +} + +// Values at every edge of the representation: zero, one, the modulus and its +// neighbours (raw zero, raw one), EPSILON and 2^32, the top of the u64 range. +const uint64_t EDGES[] = {0ull, 1ull, 2ull, P - 1, P, + P + 1, 0xFFFFFFFFull, 0x100000000ull, 1ull << 63, ~0ull, + ~0ull - 1, 0x0123456789ABCDEFull}; +const int NUM_EDGES = (int)(sizeof(EDGES) / sizeof(EDGES[0])); + +// =========================================================================== +// Layer 1 — the field primitives the kernel is built from. +// =========================================================================== + +void field_primitives_match_schoolbook_arithmetic() { + int checked = 0; + for (int i = 0; i < NUM_EDGES; ++i) { + for (int j = 0; j < NUM_EDGES; ++j) { + const uint64_t a = EDGES[i], b = EDGES[j]; + check(canon(goldilocks::mul(a, b)) == ref_mul(a, b), "goldilocks::mul at an edge"); + check(canon(goldilocks::add(a, b)) == ref_add(a, b), "goldilocks::add at an edge"); + // Three equal products: the 128-bit sum overflows for the large edges. + const uint64_t want = ref_add(ref_add(ref_mul(a, b), ref_mul(a, b)), ref_mul(a, b)); + check(canon(ext3::dot3(a, b, a, b, a, b)) == want, "ext3::dot3 at an edge (3 equal terms)"); + ++checked; + } + } + // The two-overflow case explicitly: six maximal operands. + { + const uint64_t m = ~0ull; + const uint64_t want = ref_add(ref_add(ref_mul(m, m), ref_mul(m, m)), ref_mul(m, m)); + check(canon(ext3::dot3(m, m, m, m, m, m)) == want, "ext3::dot3 with two 2^128 overflows"); + const uint64_t want1 = ref_add(ref_mul(m, m), ref_mul(m, m)); + check(canon(ext3::dot3(m, m, m, m, 0, 0)) == want1, "ext3::dot3 with one 2^128 overflow"); + } + uint64_t seed = 0xF1E1D; + for (int k = 0; k < 500; ++k) { + uint64_t v[6]; + for (int t = 0; t < 6; ++t) v[t] = sample(seed, (uint64_t)k * 6 + t); + const uint64_t want = + ref_add(ref_add(ref_mul(v[0], v[1]), ref_mul(v[2], v[3])), ref_mul(v[4], v[5])); + check(canon(ext3::dot3(v[0], v[1], v[2], v[3], v[4], v[5])) == want, "ext3::dot3 on random"); + check(canon(goldilocks::mul(v[0], v[1])) == ref_mul(v[0], v[1]), "goldilocks::mul on random"); + ++checked; + } + printf("field primitives vs schoolbook __int128: %d edge pairs + random, mul/add/dot3\n", checked); +} + +// =========================================================================== +// Layer 2 — the building blocks against independent algorithms. +// =========================================================================== + +void mds_matches_its_per_term_definition() { + std::vector> states; + states.push_back(std::vector(12, 0)); + states.push_back(std::vector(12, P - 1)); + states.push_back(std::vector(12, ~0ull)); // the raw maximum: the u128 bound's worst case + for (int k = 0; k < 12; ++k) { // one-hot lanes pin the orientation + std::vector s(12, 0); + s[k] = 1; + states.push_back(s); + } + uint64_t seed = 0x3D5; + for (int k = 0; k < 64; ++k) { + std::vector s(12); + for (int i = 0; i < 12; ++i) s[i] = sample(seed, (uint64_t)k * 12 + i); + states.push_back(s); + } + for (size_t n = 0; n < states.size(); ++n) { + uint64_t got[12], want[12]; + memcpy(got, states[n].data(), sizeof(got)); + rpx::mds(got); + ref_mds(states[n].data(), want); + for (int i = 0; i < 12; ++i) { + if (canon(got[i]) != want[i]) { + printf("FAIL mds state %zu lane %d: got %llu want %llu\n", n, i, + (unsigned long long)canon(got[i]), (unsigned long long)want[i]); + ++failures; + break; + } + } + } + printf("MDS (u128-property port) vs per-term definition: %zu states incl. raw-max and one-hot\n", + states.size()); +} + +void sboxes_are_the_seventh_power_and_its_inverse() { + // `7 · INV_ALPHA ≡ 1 (mod p − 1)`, re-derived as rpo.rs:797-806 does. + const u128 p_minus_one = (u128)P - 1; + check(((u128)7 * (u128)INV_ALPHA) % p_minus_one == 1, "INV_ALPHA must invert 7 in the exponent group"); + + std::vector xs(EDGES, EDGES + NUM_EDGES); + uint64_t seed = 0x5B0; + for (int k = 0; k < 48; ++k) xs.push_back(sample(seed, (uint64_t)k)); + for (size_t n = 0; n < xs.size(); ++n) { + const uint64_t x = xs[n]; + check(canon(rpx::sbox(x)) == ref_pow(x, 7), "sbox(x) must be x^7"); + check(canon(rpx::inv_sbox(x)) == ref_pow(x, INV_ALPHA), "inv_sbox(x) must be x^INV_ALPHA"); + check(canon(rpx::sbox(rpx::inv_sbox(x))) == canon(x), "sbox(inv_sbox(x)) must be x"); + check(canon(rpx::inv_sbox(rpx::sbox(x))) == canon(x), "inv_sbox(sbox(x)) must be x"); + } + check(rpx::inv_sbox(0) == 0, "inv_sbox(0) must be 0 (the padding row's fixed point)"); + check(canon(rpx::inv_sbox(P)) == 0, "inv_sbox(raw zero) must be 0"); + check(canon(rpx::inv_sbox(1)) == 1, "inv_sbox(1) must be 1"); + printf("S-boxes vs generic exponentiation: %zu values, x^7, x^{1/7}, both compositions\n", + xs.size()); +} + +void cubic_extension_matches_naive_polynomial_arithmetic() { + // The reduction rule itself, pinned on the basis: φ·φ² = φ³ = 1 + φ, and + // φ²·φ² = φ⁴ = φ + φ². + { + rpx::CubicExt phi = {0, 1, 0}, phi2 = {0, 0, 1}, one = {1, 0, 0}; + rpx::CubicExt r = rpx::ext_mul(phi, phi2); + check(canon(r.c0) == 1 && canon(r.c1) == 1 && canon(r.c2) == 0, "φ·φ² must be 1 + φ"); + r = rpx::ext_mul(phi2, phi2); + check(canon(r.c0) == 0 && canon(r.c1) == 1 && canon(r.c2) == 1, "φ²·φ² must be φ + φ²"); + r = rpx::ext_mul(phi2, one); + check(canon(r.c0) == 0 && canon(r.c1) == 0 && canon(r.c2) == 1, "1 must be the identity"); + } + std::vector as, bs; + as.push_back(RefExt{{P - 1, P - 1, P - 1}}); + bs.push_back(RefExt{{P - 1, P - 1, P - 1}}); + as.push_back(RefExt{{~0ull, ~0ull, ~0ull}}); // raw maxima + bs.push_back(RefExt{{~0ull, ~0ull, ~0ull}}); + as.push_back(RefExt{{0, 0, 0}}); + bs.push_back(RefExt{{P - 1, 0, 1}}); + uint64_t seed = 0xE3; + for (int k = 0; k < 64; ++k) { + RefExt a, b; + for (int t = 0; t < 3; ++t) { + a.c[t] = sample(seed, (uint64_t)k * 6 + t); + b.c[t] = sample(seed, (uint64_t)k * 6 + 3 + t); + } + as.push_back(a); + bs.push_back(b); + } + for (size_t n = 0; n < as.size(); ++n) { + const rpx::CubicExt a = {as[n].c[0], as[n].c[1], as[n].c[2]}; + const rpx::CubicExt b = {bs[n].c[0], bs[n].c[1], bs[n].c[2]}; + const rpx::CubicExt m = rpx::ext_mul(a, b); + const RefExt mw = ref_ext_mul(as[n], bs[n]); + check(canon(m.c0) == mw.c[0] && canon(m.c1) == mw.c[1] && canon(m.c2) == mw.c[2], + "ext_mul must equal the naive polynomial product"); + const rpx::CubicExt s = rpx::ext_square(a); + const RefExt sw = ref_ext_mul(as[n], as[n]); + check(canon(s.c0) == sw.c[0] && canon(s.c1) == sw.c[1] && canon(s.c2) == sw.c[2], + "ext_square must equal the naive square"); + const rpx::CubicExt p7 = rpx::ext_power7(a); + const RefExt pw = ref_ext_pow(as[n], 7); + check(canon(p7.c0) == pw.c[0] && canon(p7.c1) == pw.c[1] && canon(p7.c2) == pw.c[2], + "ext_power7 must equal generic exponentiation to 7"); + } + printf("cubic extension (φ³ = φ + 1) vs naive polynomial arithmetic: %zu pairs, mul/square/power7\n", + as.size()); +} + +// =========================================================================== +// Layer 3 — ★ the EXTERNAL anchor: seven FB rounds are RPO256. +// =========================================================================== + +// RPO256's permutation composed from the kernel's FB round — rpo.rs:567-583. +void rpo_permute(uint64_t s[12]) { + rpx::fb_round<0>(s); + rpx::fb_round<1>(s); + rpx::fb_round<2>(s); + rpx::fb_round<3>(s); + rpx::fb_round<4>(s); + rpx::fb_round<5>(s); + rpx::fb_round<6>(s); + for (int i = 0; i < 12; ++i) s[i] = goldilocks::canonical(s[i]); +} + +// miden's `hash_elements` in this lane convention — a transcription of the +// test-only `rpo.rs:747-767`: capacity lane 8 takes `len % 8`, the rate is +// OVERWRITTEN, the tail zero-padded, the digest is lanes 0-3. +void miden_hash_elements(const uint64_t *elements, size_t n, uint64_t out[4]) { + uint64_t state[12] = {0}; + state[8] = (uint64_t)(n % 8); + size_t i = 0; + for (size_t k = 0; k < n; ++k) { + state[i++] = elements[k]; + if (i == 8) { + rpo_permute(state); + i = 0; + } + } + if (i > 0) { + for (; i < 8; ++i) state[i] = 0; + rpo_permute(state); + } + for (int d = 0; d < 4; ++d) out[d] = state[d]; +} + +void seven_fb_rounds_reproduce_the_miden_rpo_vectors() { + check(NUM_MIDEN_HASH_ELEMENTS == 19, "miden vector table lost entries"); + int matched = 0; + for (int n = 0; n < NUM_MIDEN_HASH_ELEMENTS; ++n) { + uint64_t elements[19]; + for (int k = 0; k <= n; ++k) elements[k] = (uint64_t)k; + uint64_t got[4]; + miden_hash_elements(elements, (size_t)n + 1, got); + bool ok = true; + for (int d = 0; d < 4; ++d) ok = ok && got[d] == MIDEN_HASH_ELEMENTS[n][d]; + if (!ok) { + printf("FAIL miden hash_elements(0..=%d)\n got %llu %llu %llu %llu\n want %llu %llu %llu %llu\n", + n, (unsigned long long)got[0], (unsigned long long)got[1], + (unsigned long long)got[2], (unsigned long long)got[3], + (unsigned long long)MIDEN_HASH_ELEMENTS[n][0], + (unsigned long long)MIDEN_HASH_ELEMENTS[n][1], + (unsigned long long)MIDEN_HASH_ELEMENTS[n][2], + (unsigned long long)MIDEN_HASH_ELEMENTS[n][3]); + ++failures; + } else { + ++matched; + } + } + // The compress layout, pinned the way rpo.rs:789-795 pins it: one + // permutation of `[0..8 ‖ 0⁴]` is the eight-element vector, so + // `[left ‖ right ‖ zero capacity]` with left = 0..4, right = 4..8 IS + // `Rpo256::merge` — the layout `rpx::compress` builds. + { + uint64_t s[12] = {0, 1, 2, 3, 4, 5, 6, 7, 0, 0, 0, 0}; + rpo_permute(s); + bool ok = true; + for (int d = 0; d < 4; ++d) ok = ok && s[d] == MIDEN_HASH_ELEMENTS[7][d]; + check(ok, "permute([0..8 ‖ 0⁴]) must be miden's eight-element vector (compress layout)"); + } + printf("★ EXTERNAL: seven fb_round = RPO256 vs miden-crypto hash_elements: %d/19 matched\n", + matched); +} + +// =========================================================================== +// Layer 4 — ★ the Rust oracle. +// =========================================================================== + +void rpx_permutation_matches_the_rust_oracle() { + check(NUM_RPX_PERMUTATION_VECTORS >= 8, + "Rust-oracle permutation table must hold >= 8 vectors (run the generator, see rpx_kat_vectors.h)"); + bool saw_zero = false, saw_p_minus_one = false; + int matched = 0; + for (int n = 0; n < NUM_RPX_PERMUTATION_VECTORS; ++n) { + const RpxPermutationVector &v = RPX_PERMUTATION_VECTORS[n]; + bool all_zero = true, all_pm1 = true; + uint64_t s[12]; + for (int i = 0; i < 12; ++i) { + s[i] = v.input[i]; + all_zero = all_zero && v.input[i] == 0; + all_pm1 = all_pm1 && v.input[i] == P - 1; + } + saw_zero = saw_zero || all_zero; + saw_p_minus_one = saw_p_minus_one || all_pm1; + rpx::permute(s); + bool ok = true; + for (int i = 0; i < 12; ++i) ok = ok && canon(s[i]) == v.output[i]; + if (!ok) { + printf("FAIL rpx permutation vector %d (%s)\n", n, v.name); + for (int i = 0; i < 12; ++i) { + if (canon(s[i]) != v.output[i]) { + printf(" lane %2d got %llu want %llu\n", i, (unsigned long long)canon(s[i]), + (unsigned long long)v.output[i]); + } + } + ++failures; + } else { + ++matched; + } + } + check(saw_zero, "the permutation table must include the all-zero state"); + check(saw_p_minus_one, "the permutation table must include the all-(p-1) state"); + printf("★ ORACLE: rpx::permute vs Rust Rpx256::permute: %d/%d vectors matched\n", matched, + NUM_RPX_PERMUTATION_VECTORS); +} + +// The array-form transcription of `algebraic_commit::sponge_leaf` (:169-184), +// over the kernel's permutation — so the STREAMING struct's block bookkeeping +// is checked against the direct transcription at every length, independently +// of which lengths the oracle table carries. +void ref_sponge_leaf(const uint64_t *felts, size_t n, uint64_t digest[4]) { + uint64_t state[12] = {0}; + state[8] = (uint64_t)(n % 8); + state[9] = 0x4C4D464Cull; // u32::from_le_bytes(b"LFML") + if (n == 0) { + for (int d = 0; d < 4; ++d) digest[d] = state[d]; + return; + } + for (size_t start = 0; start < n; start += 8) { + for (size_t lane = 0; lane < 8; ++lane) { + state[lane] = (start + lane < n) ? felts[start + lane] : 0; + } + rpx::permute(state); + } + for (int d = 0; d < 4; ++d) digest[d] = state[d]; +} + +void leaf_sponge_matches_the_rust_oracle() { + // The streaming struct against the array transcription, lengths 0..40. + { + uint64_t seed = 0x1EAF; + std::vector felts(40); + for (size_t i = 0; i < felts.size(); ++i) felts[i] = sample(seed, i); + for (size_t n = 0; n <= felts.size(); ++n) { + uint64_t got[4], want[4]; + rpx::sponge_leaf(felts.data(), n, got); + ref_sponge_leaf(felts.data(), n, want); + check(memcmp(got, want, sizeof(got)) == 0, "rpx::Sponge must equal the sponge_leaf transcription"); + } + uint64_t empty[4] = {1, 1, 1, 1}; + rpx::sponge_leaf(felts.data(), 0, empty); + check(empty[0] == 0 && empty[1] == 0 && empty[2] == 0 && empty[3] == 0, + "the empty leaf's digest is the zero rate lanes, with NO permutation"); + uint64_t one[4]; + rpx::sponge_leaf(felts.data(), 1, one); + check(one[0] != 0 || one[1] != 0 || one[2] != 0 || one[3] != 0, "a one-felt leaf must permute"); + printf("leaf: rpx::Sponge vs sponge_leaf transcription at 41 lengths (0..40)\n"); + } + // The oracle table: exactly the gate's seven lengths. + std::set lengths; + for (int n = 0; n < NUM_RPX_LEAF_VECTORS; ++n) lengths.insert(RPX_LEAF_VECTORS[n].len); + const uint32_t required[7] = {0, 1, 7, 8, 9, 16, 17}; + bool all_present = NUM_RPX_LEAF_VECTORS > 0; + for (int k = 0; k < 7; ++k) all_present = all_present && lengths.count(required[k]) == 1; + check(all_present, + "Rust-oracle leaf table must hold lengths 0, 1, 7, 8, 9, 16, 17 (run the generator, see rpx_kat_vectors.h)"); + int matched = 0; + for (int n = 0; n < NUM_RPX_LEAF_VECTORS; ++n) { + const RpxLeafVector &v = RPX_LEAF_VECTORS[n]; + check(v.len <= (uint32_t)RPX_LEAF_KAT_MAX_FELTS, "leaf vector wider than the table row"); + uint64_t got[4]; + rpx::sponge_leaf(v.felts, v.len, got); + bool ok = true; + for (int d = 0; d < 4; ++d) ok = ok && canon(got[d]) == v.digest[d]; + if (!ok) { + printf("FAIL rpx leaf vector len=%u\n got %llu %llu %llu %llu\n want %llu %llu %llu %llu\n", + v.len, (unsigned long long)canon(got[0]), (unsigned long long)canon(got[1]), + (unsigned long long)canon(got[2]), (unsigned long long)canon(got[3]), + (unsigned long long)v.digest[0], (unsigned long long)v.digest[1], + (unsigned long long)v.digest[2], (unsigned long long)v.digest[3]); + ++failures; + } else { + ++matched; + } + } + printf("★ ORACLE: rpx::sponge_leaf vs Rust sponge_leaf(Rpx): %d/%d lengths matched\n", matched, + NUM_RPX_LEAF_VECTORS); +} + +void parent_matches_the_rust_oracle() { + check(NUM_RPX_PARENT_VECTORS >= 1, + "Rust-oracle parent table must hold >= 1 vector (run the generator, see rpx_kat_vectors.h)"); + int matched = 0; + for (int n = 0; n < NUM_RPX_PARENT_VECTORS; ++n) { + const RpxParentVector &v = RPX_PARENT_VECTORS[n]; + uint64_t got[4]; + rpx::compress(v.left, v.right, got); + bool ok = true; + for (int d = 0; d < 4; ++d) ok = ok && canon(got[d]) == v.digest[d]; + if (!ok) { + printf("FAIL rpx parent vector %d (%s)\n got %llu %llu %llu %llu\n want %llu %llu %llu %llu\n", + n, v.name, (unsigned long long)canon(got[0]), (unsigned long long)canon(got[1]), + (unsigned long long)canon(got[2]), (unsigned long long)canon(got[3]), + (unsigned long long)v.digest[0], (unsigned long long)v.digest[1], + (unsigned long long)v.digest[2], (unsigned long long)v.digest[3]); + ++failures; + } else { + ++matched; + } + // Structure: a parent is ONE permutation of `[l ‖ r ‖ 0⁴]`, and the + // order of the children matters. + uint64_t s[12] = {v.left[0], v.left[1], v.left[2], v.left[3], v.right[0], v.right[1], + v.right[2], v.right[3], 0, 0, 0, 0}; + rpx::permute(s); + check(memcmp(s, got, sizeof(got)) == 0, "compress must be permute([l ‖ r ‖ 0⁴]) truncated"); + uint64_t swapped[4]; + rpx::compress(v.right, v.left, swapped); + bool same_children = memcmp(v.left, v.right, sizeof(swapped)) == 0; + check(same_children || memcmp(swapped, got, sizeof(got)) != 0, "compress(r, l) must differ from compress(l, r)"); + } + printf("★ ORACLE: rpx::compress vs Rust HasherKind::Rpx.compress: %d/%d parents matched\n", matched, + NUM_RPX_PARENT_VECTORS); +} + +// =========================================================================== +// Layer 5 — negative controls and the representation. +// =========================================================================== + +void rpx_is_not_rpo() { + // rpx.rs:577-580: the two share constants, an MDS and three of seven + // rounds, so a schedule bug could collapse one into the other. + uint64_t a[12], b[12]; + for (int i = 0; i < 12; ++i) a[i] = b[i] = (uint64_t)i; + rpx::permute(a); + rpo_permute(b); + check(memcmp(a, b, sizeof(a)) != 0, "RPX must not be RPO on the same state"); + uint64_t z[12] = {0}; + rpx::permute(z); + bool nonzero = false; + for (int i = 0; i < 12; ++i) nonzero = nonzero || z[i] != 0; + check(nonzero, "with its constants present, permute(0) must not be 0"); + printf("negative control: RPX(0..12) != RPO(0..12); permute(0) != 0\n"); +} + +void raw_and_canonical_inputs_agree_and_outputs_are_canonical() { + uint64_t seed = 0xCA0; + for (int k = 0; k < 32; ++k) { + uint64_t raw[12], can[12]; + for (int i = 0; i < 12; ++i) { + // Canonical values below 2^32 − 1 have a raw twin `c + p`; alternate + // lanes between the twin and a plain canonical value. + const uint64_t c = splitmix(seed) % 0xFFFFFFFFull; + const bool twin = ((k + i) % 3) != 0; + can[i] = twin ? c : splitmix(seed) % P; + raw[i] = twin ? c + P : can[i]; + } + uint64_t r1[12], c1[12]; + memcpy(r1, raw, sizeof(r1)); + memcpy(c1, can, sizeof(c1)); + rpx::permute(r1); + rpx::permute(c1); + check(memcmp(r1, c1, sizeof(r1)) == 0, "permute(raw) must equal permute(canonical)"); + for (int i = 0; i < 12; ++i) check(c1[i] < P, "permute output must be canonical"); + + uint64_t d_raw[4], d_can[4]; + rpx::sponge_leaf(raw, 12, d_raw); + rpx::sponge_leaf(can, 12, d_can); + check(memcmp(d_raw, d_can, sizeof(d_raw)) == 0, "sponge_leaf(raw) must equal sponge_leaf(canonical)"); + + uint64_t p_raw[4], p_can[4]; + rpx::compress(raw, raw + 4, p_raw); + rpx::compress(can, can + 4, p_can); + check(memcmp(p_raw, p_can, sizeof(p_raw)) == 0, "compress(raw) must equal compress(canonical)"); + } + printf("representation: raw [p, 2^64) inputs agree with canonical; outputs canonical (32 states)\n"); +} + +void every_input_lane_reaches_the_output() { + uint64_t seed = 0x1A4E; + uint64_t base[12]; + for (int i = 0; i < 12; ++i) base[i] = splitmix(seed) % P; + uint64_t out0[12]; + memcpy(out0, base, sizeof(out0)); + rpx::permute(out0); + for (int k = 0; k < 12; ++k) { + uint64_t s[12]; + memcpy(s, base, sizeof(s)); + s[k] = (s[k] + 1) % P; + rpx::permute(s); + check(memcmp(s, out0, sizeof(s)) != 0, "changing one input lane must move the output"); + } + printf("negative control: each of the 12 input lanes moves the output\n"); +} + +// =========================================================================== +// Layer 6 — the cost model, counted. +// =========================================================================== + +struct Counted { + unsigned long long mul, dot3, add; +}; + +template +Counted count_ops(F f) { + rpx::g_ops = rpx::OpCount{0, 0, 0}; + f(); + return Counted{rpx::g_ops.mul, rpx::g_ops.dot3, rpx::g_ops.add}; +} + +void the_cost_model_is_what_the_header_claims() { + uint64_t s[12]; + for (int i = 0; i < 12; ++i) s[i] = (uint64_t)i + 1; + const Counted fb = count_ops([&] { rpx::fb_round<0>(s); }); + const Counted ext = count_ops([&] { rpx::ext_round<1>(s); }); + const Counted fin = count_ops([&] { rpx::final_round<6>(s); }); + const Counted all = count_ops([&] { rpx::permute(s); }); + const Counted rpo = count_ops([&] { rpo_permute(s); }); + const Counted inv = count_ops([&] { (void)rpx::inv_sbox(s[0]); }); + const Counted fwd = count_ops([&] { (void)rpx::sbox(s[0]); }); + const Counted emul = count_ops([&] { + rpx::CubicExt a = {s[0], s[1], s[2]}; + (void)rpx::ext_mul(a, a); + }); + + printf("op counts (Goldilocks mul | 3-term dot3 | add); MDS = 288 narrow 32x32 MACs each, uncounted:\n"); + printf(" x^7 (sbox) %4llu | %3llu | %3llu\n", fwd.mul, fwd.dot3, fwd.add); + printf(" x^{1/7} (inv_sbox) %4llu | %3llu | %3llu (63 squarings + 9 products)\n", inv.mul, + inv.dot3, inv.add); + printf(" ext_mul %4llu | %3llu | %3llu (9 wide products in 3 reductions)\n", emul.mul, + emul.dot3, emul.add); + printf(" FB round %4llu | %3llu | %3llu + 2 MDS\n", fb.mul, fb.dot3, fb.add); + printf(" E round %4llu | %3llu | %3llu (4 triples x power7)\n", ext.mul, ext.dot3, + ext.add); + printf(" M round %4llu | %3llu | %3llu + 1 MDS\n", fin.mul, fin.dot3, fin.add); + printf(" RPX permutation %4llu | %3llu | %3llu + 7 MDS (2016 MACs)\n", all.mul, all.dot3, + all.add); + printf(" RPO permutation %4llu | %3llu | %3llu + 14 MDS (4032 MACs), for comparison\n", + rpo.mul, rpo.dot3, rpo.add); + printf(" inverse S-box share of RPX field multiplications: %llu / %llu\n", 3ull * 12ull * inv.mul, + all.mul); + + check(fwd.mul == 4 && inv.mul == 72, "S-box costs must be 4 and 72 multiplications"); + check(emul.mul == 0 && emul.dot3 == 3 && emul.add == 2, "ext_mul must be 3 dot3 + 2 adds"); + check(fb.mul == 912 && fb.dot3 == 0 && fb.add == 48, "FB round must be 912 mul / 48 add"); + check(ext.mul == 0 && ext.dot3 == 48 && ext.add == 44, "E round must be 48 dot3 / 44 add"); + check(fin.mul == 0 && fin.dot3 == 0 && fin.add == 24, "M round must be 24 add"); + check(all.mul == 2736 && all.dot3 == 144 && all.add == 300, "RPX permutation must be 2736 mul / 144 dot3 / 300 add"); + check(rpo.mul == 6384 && rpo.dot3 == 0 && rpo.add == 336, "RPO permutation must be 6384 mul / 336 add"); +} + +} // namespace + +int main() { + printf("RPX device-kernel known-answer tests, host-compiled from crypto/math-cuda/kernels/rpx.cu\n\n"); + printf("-- layer 1/2: primitives and building blocks vs independent algorithms --\n"); + field_primitives_match_schoolbook_arithmetic(); + mds_matches_its_per_term_definition(); + sboxes_are_the_seventh_power_and_its_inverse(); + cubic_extension_matches_naive_polynomial_arithmetic(); + printf("\n-- layer 3: the external anchor --\n"); + seven_fb_rounds_reproduce_the_miden_rpo_vectors(); + printf("\n-- layer 4: the Rust oracle --\n"); + rpx_permutation_matches_the_rust_oracle(); + leaf_sponge_matches_the_rust_oracle(); + parent_matches_the_rust_oracle(); + printf("\n-- layer 5: negative controls and representation --\n"); + rpx_is_not_rpo(); + raw_and_canonical_inputs_agree_and_outputs_are_canonical(); + every_input_lane_reaches_the_output(); + printf("\n-- layer 6: cost model --\n"); + the_cost_model_is_what_the_header_claims(); + if (failures != 0) { + printf("\n*** %d FAILURE(S) ***\n", failures); + return 1; + } + printf("\nALL HOST KAT CHECKS PASS\n"); + printf("NOTE: arithmetic only. nvcc acceptance and GPU execution are phase 2's GPU tests.\n"); + return 0; +} diff --git a/crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h b/crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h new file mode 100644 index 000000000..cc2ddeaf6 --- /dev/null +++ b/crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h @@ -0,0 +1,162 @@ +// Known-answer vectors for the RPX device kernel (`kernels/rpx.cu`), embedded +// rather than parsed at run time — a table cannot have a zero-vector run, and +// `rpx_host_kat.cpp` asserts every count below as well. +// +// This file is DATA. Table 1 is transcribed; Tables 2-4 are printed by the Rust +// oracle and pasted. Nothing here is computed by the harness. +#pragma once +#include + +// --------------------------------------------------------------------------- +// Table 1 — miden-crypto's RPO256 `hash_elements` known-answer vectors. +// EXTERNAL: nothing in this repository produced these seventy-six numbers. +// +// Transcribed mechanically (a script over the source, not by hand) from +// `prover/src/lfm/rpo.rs:624-739` `MIDEN_HASH_ELEMENTS`, itself transcribed +// from miden-crypto `src/hash/algebraic_sponge/rescue/rpo/tests.rs`. Entry `n` +// is the digest of the field elements `[0, 1, …, n]` under miden's convention: +// capacity lane 8 = `len mod 8`, rate OVERWRITTEN, zero-padded tail, digest = +// lanes 0..4 (rpo.rs:741-767). +// +// What they pin in `rpx.cu`: RPX's FB round IS RPO's round, so seven +// `fb_round<0..7>` compose to RPO256 and must reproduce this table. That pins +// ARK1/ARK2 (all seven rows), the MDS row AND its orientation, both S-box +// exponents including the 72-step inverse chain, the u128-property MDS, and the +// sponge lane convention — externally. Entries 1-7 and 9-19 exercise padding, +// 8 and 16 the exact-block path, everything above 8 the capacity carry. +// --------------------------------------------------------------------------- +inline constexpr int NUM_MIDEN_HASH_ELEMENTS = 19; +inline constexpr uint64_t MIDEN_HASH_ELEMENTS[NUM_MIDEN_HASH_ELEMENTS][4] = { + {8563248028282119176ull, 14757918088501470722ull, 14042820149444308297ull, 7607140247535155355ull}, + {8762449007102993687ull, 4386081033660325954ull, 5000814629424193749ull, 8171580292230495897ull}, + {16710087681096729759ull, 10808706421914121430ull, 14661356949236585983ull, 5683478730832134441ull}, + {5309818427047650994ull, 17172251659920546244ull, 8288476618870804357ull, 18080473279382182941ull}, + {3647545403045515695ull, 3358383208908083302ull, 8797161010298072910ull, 2412100201132087248ull}, + {8409780526028662686ull, 214479528340808320ull, 13626616722984122219ull, 13991752159726061594ull}, + {4800410126693035096ull, 8293686005479024958ull, 16849389505608627981ull, 12129312715917897796ull}, + {5421234586123900205ull, 9738602082989433872ull, 7017816005734536787ull, 8635896173743411073ull}, + {11707446879505873182ull, 7588005580730590001ull, 4664404372972250366ull, 17613162115550587316ull}, + {6991094187713033844ull, 10140064581418506488ull, 1235093741254112241ull, 16755357411831959519ull}, + {18007834547781860956ull, 5262789089508245576ull, 4752286606024269423ull, 15626544383301396533ull}, + {5419895278045886802ull, 10747737918518643252ull, 14861255521757514163ull, 3291029997369465426ull}, + {16916426112258580265ull, 8714377345140065340ull, 14207246102129706649ull, 6226142825442954311ull}, + {7320977330193495928ull, 15630435616748408136ull, 10194509925259146809ull, 15938750299626487367ull}, + {9872217233988117092ull, 5336302253150565952ull, 9650742686075483437ull, 8725445618118634861ull}, + {12539853708112793207ull, 10831674032088582545ull, 11090804155187202889ull, 105068293543772992ull}, + {7287113073032114129ull, 6373434548664566745ull, 8097061424355177769ull, 14780666619112596652ull}, + {17147873541222871127ull, 17350918081193545524ull, 5785390176806607444ull, 12480094913955467088ull}, + {17273934282489765074ull, 8007352780590012415ull, 16690624932024962846ull, 8137543572359747206ull}, +}; + +// --------------------------------------------------------------------------- +// Tables 2-4 — THE RUST ORACLE. miden publishes no RPX known-answer table +// (rpx.rs "PROVENANCE"), so the host `Rpx256` is the oracle the kernel is +// pinned to. Printed by `prover/tests/rpx_host_kat_vectors.rs`: +// +// cargo test -p lambda-vm-prover --test rpx_host_kat_vectors -- --ignored --nocapture +// +// and pasted verbatim between the `>>> BEGIN` / `<<< END` markers. Inputs are +// derived there from fixed seeds and printed next to the outputs, so this file +// is self-contained. All values are canonical (`< p`). +// +// Table 2 — the bare permutation: all-zero, all-(p−1), `0..12`, alternating, +// two one-hot lanes, four seeded random states. +// Table 3 — the leaf sponge (`algebraic_commit::sponge_leaf`) at 0, 1, 7, 8, +// 9, 16 and 17 felts; `felts[]` is zero beyond `len`. +// Table 4 — the parent `compress(l, r)`. +// --------------------------------------------------------------------------- +struct RpxPermutationVector { + const char *name; + uint64_t input[12]; + uint64_t output[12]; +}; + +inline constexpr int RPX_LEAF_KAT_MAX_FELTS = 17; +struct RpxLeafVector { + uint32_t len; + uint64_t felts[RPX_LEAF_KAT_MAX_FELTS]; + uint64_t digest[4]; +}; + +struct RpxParentVector { + const char *name; + uint64_t left[4]; + uint64_t right[4]; + uint64_t digest[4]; +}; + +// >>> BEGIN RUST-ORACLE TABLES — generated by +// cargo test -p lambda-vm-prover --test rpx_host_kat_vectors -- --ignored --nocapture +// (prover/tests/rpx_host_kat_vectors.rs). Paste verbatim; do not edit by hand. + +inline constexpr int NUM_RPX_PERMUTATION_VECTORS = 10; +inline constexpr RpxPermutationVector RPX_PERMUTATION_VECTORS[NUM_RPX_PERMUTATION_VECTORS] = { + {"all-zero", + {0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {8760086638283468260ull, 18228666152919569253ull, 4041825754230271128ull, 16906183286731764961ull, 4664375192219530269ull, 271590372761485506ull, 5612474514543166805ull, 8933101171974180471ull, 1556877437237031065ull, 7026397410864970258ull, 15101742939622740655ull, 4524429088483979565ull}}, + {"all-(p-1)", + {18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull, 18446744069414584320ull}, + {7040074528728887770ull, 10474261017970959672ull, 6160748039461781206ull, 9121740959127811013ull, 7259505444118573102ull, 6771278935515018093ull, 18386914479072470354ull, 17160039764143535473ull, 1815780993504974800ull, 17309055307915657636ull, 5977169316478634398ull, 4250629519753691035ull}}, + {"lanes 0..12", + {0ull, 1ull, 2ull, 3ull, 4ull, 5ull, 6ull, 7ull, 8ull, 9ull, 10ull, 11ull}, + {3614697924784493998ull, 4917065433670799835ull, 12893407190838344317ull, 16769932886818781879ull, 17010299523770013195ull, 9826755761378503206ull, 1872785960340665977ull, 7783788981462778586ull, 45778307605882514ull, 7437259891664617628ull, 17010253034795346176ull, 6863075881906649113ull}}, + {"alternating 0 / p-1", + {0ull, 18446744069414584320ull, 0ull, 18446744069414584320ull, 0ull, 18446744069414584320ull, 0ull, 18446744069414584320ull, 0ull, 18446744069414584320ull, 0ull, 18446744069414584320ull}, + {12839024277220712229ull, 1805658617972785851ull, 11708832562581917975ull, 2207339757364837492ull, 457975798096500050ull, 15656130651128894835ull, 3485815494872446363ull, 10687968103458402677ull, 10384294655078062232ull, 1487178939946482695ull, 12310600107129561463ull, 18388841767871832735ull}}, + {"one-hot lane 0", + {1ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {8423002511501289529ull, 6761734748202534392ull, 17987336675889252592ull, 14012777376234247391ull, 15293807115397414812ull, 15290017247514670316ull, 10548590320248089637ull, 9459855167724924903ull, 10549768014422457033ull, 13045952392708592140ull, 3310663857881768756ull, 7584810783597460418ull}}, + {"one-hot lane 11", + {0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 1ull}, + {18436166275486246010ull, 14000894557392395452ull, 10767551609857089912ull, 12516698445112165012ull, 13131066481882004069ull, 9858979976142754244ull, 11402636824743634507ull, 10600727647028701714ull, 11200928220555719329ull, 7317761145158236061ull, 16857331551667002769ull, 16879508045812612150ull}}, + {"random #1", + {303661977215735624ull, 5244312915552057691ull, 9817756985327366386ull, 15550273871372065883ull, 5764353057648779642ull, 16198122637140758912ull, 7462824619408935181ull, 3819703627846067891ull, 10378249170554155646ull, 11473525795005675318ull, 8246620909628934680ull, 4793144044164964625ull}, + {15068850129045079395ull, 15287067578585128518ull, 13369562146120321575ull, 10561395445440413441ull, 9652992371859647144ull, 4276856065313043669ull, 5527444075954724606ull, 7786060382866009904ull, 16451772069079981395ull, 198876956612152837ull, 15815343923951857286ull, 16122126005548441717ull}}, + {"random #2", + {5204068831683694011ull, 601380814908431653ull, 258667317409904638ull, 8486618912357792900ull, 16418043790810515027ull, 10319906524521615844ull, 8286207029444254408ull, 17770698039797916230ull, 12310900488678790115ull, 11195649432216834664ull, 13332813278057623446ull, 16898620073423657296ull}, + {9523479656024648568ull, 5510889535488554715ull, 8599619832581755346ull, 3318619196771576895ull, 12581966946741818379ull, 12200018864226225973ull, 4385075405488142149ull, 8051813774684357414ull, 3019406547981393239ull, 7453667634993074437ull, 9864259903669275905ull, 6156796699962990553ull}}, + {"random #3", + {13533914130435405040ull, 15234815373149021432ull, 10183913914233800905ull, 9526239132464493568ull, 5375977297676405297ull, 5765388458641153407ull, 4908125521970473579ull, 4421030864271922041ull, 15641279279696351384ull, 16893076439662162884ull, 7253714011824234117ull, 14616467593891397000ull}, + {15514260962038810700ull, 190255547175148079ull, 15766300047716671382ull, 10145444481310349528ull, 6135237967701788176ull, 11361125511081474273ull, 9927005018743801106ull, 17211086950078547559ull, 10833199580085782023ull, 13634008743082439065ull, 6687522208929839355ull, 3545879585555314384ull}}, + {"random #4", + {389113379214421922ull, 1947929307647562990ull, 667333451960644926ull, 3487966933876559811ull, 4195385248066926332ull, 2153180418459341747ull, 2727969323864685845ull, 29633526854483411ull, 990649808851061115ull, 1355410330370587755ull, 11605520071788416946ull, 4884409355120715354ull}, + {7025469669435110295ull, 17270957437800346011ull, 13702589935335807876ull, 3666927270871270796ull, 16666721215101099684ull, 531487850530305024ull, 15550553335698242665ull, 8959489596577675281ull, 11020601500923732075ull, 16110845767020565054ull, 4778394010005480449ull, 7715575140819562371ull}}, +}; + +inline constexpr int NUM_RPX_LEAF_VECTORS = 7; +inline constexpr RpxLeafVector RPX_LEAF_VECTORS[NUM_RPX_LEAF_VECTORS] = { + {0u, + {0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {0ull, 0ull, 0ull, 0ull}}, + {1u, + {14681136968691612469ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {16400186102935428425ull, 12817983163740802970ull, 13449009006350391325ull, 2209445548780258712ull}}, + {7u, + {2664695409302073823ull, 17298518342786888931ull, 17367242851809685948ull, 13566833943477212382ull, 6789339537410032387ull, 5202847705797706501ull, 6869254230765949416ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {2289345357069865559ull, 8509266780934512918ull, 13810958145049281723ull, 5769431894700133303ull}}, + {8u, + {3521541860211663897ull, 5585621328801039182ull, 3314063895810834828ull, 6286715337571703139ull, 9272399501810688383ull, 17378448552699642502ull, 9663403628134293866ull, 8225575178453385283ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {14052993739410942603ull, 8384701950754250190ull, 11473922331550289114ull, 16644313465254305812ull}}, + {9u, + {15923052634311126246ull, 10423360080185943333ull, 4604695570423031111ull, 15959212651715575539ull, 4341333374822801132ull, 3169961389438585383ull, 7059846953207312362ull, 6231597079039193598ull, 14413065529971692326ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull, 0ull}, + {15453186885173297365ull, 11395279108043639065ull, 15954005188014354330ull, 2854892578083306874ull}}, + {16u, + {9660685076555889599ull, 4027567791223379602ull, 11432600011703367870ull, 6441517771629429252ull, 8272264386868866348ull, 16565648022353132158ull, 16844837242675693755ull, 12942506659476152817ull, 11839051358503478840ull, 1846358602548732379ull, 118703897581348635ull, 14480592082795401517ull, 12015885875590073011ull, 7433808365622677077ull, 13247077855319202624ull, 17837888200692576115ull, 0ull}, + {18135965004560326100ull, 1948492279228612931ull, 17772968542724134453ull, 12116464713281646840ull}}, + {17u, + {14169068543591784110ull, 12906798066534908639ull, 1898134805181953282ull, 3700382130787856361ull, 10455317549184205797ull, 1564511190292879407ull, 5954886065046464361ull, 10320234224067579215ull, 17095047743397986079ull, 8434180870595516882ull, 17706992797230203878ull, 813257427175065251ull, 13312284969041468023ull, 15899260221184366980ull, 5770785055252949875ull, 11176385994046687487ull, 8142444693260481147ull}, + {430819886588247494ull, 10400188655761849356ull, 3003730485848167815ull, 13484379440855863704ull}}, +}; + +inline constexpr int NUM_RPX_PARENT_VECTORS = 2; +inline constexpr RpxParentVector RPX_PARENT_VECTORS[NUM_RPX_PARENT_VECTORS] = { + {"digits 0..8", + {0ull, 1ull, 2ull, 3ull}, + {4ull, 5ull, 6ull, 7ull}, + {10386438340626196987ull, 10820383641790274229ull, 5711121060683785078ull, 11046870009967209474ull}}, + {"random", + {10430052842846219471ull, 4016318112082366688ull, 17186674839268073878ull, 16606021345024473049ull}, + {1405896845186672283ull, 13799610513837549656ull, 17571522367612218822ull, 18082329703565322844ull}, + {18019606657308693634ull, 10494109104368286361ull, 7943124261980338770ull, 17971490172695632899ull}}, +}; +// <<< END RUST-ORACLE TABLES diff --git a/prover/tests/rpx_host_kat_vectors.rs b/prover/tests/rpx_host_kat_vectors.rs index 1ed80b11f..0c3dfef84 100644 --- a/prover/tests/rpx_host_kat_vectors.rs +++ b/prover/tests/rpx_host_kat_vectors.rs @@ -87,7 +87,10 @@ fn permutation_inputs() -> Vec<(&'static str, [u64; HASH_STATE_FELTS])> { "alternating 0 / p-1", core::array::from_fn(|i| if i % 2 == 0 { 0 } else { P - 1 }), ), - ("one-hot lane 0", core::array::from_fn(|i| u64::from(i == 0))), + ( + "one-hot lane 0", + core::array::from_fn(|i| u64::from(i == 0)), + ), ( "one-hot lane 11", core::array::from_fn(|i| u64::from(i == HASH_STATE_FELTS - 1)), @@ -109,7 +112,9 @@ fn print_rpx_host_kat_vectors() { out.push_str( "// cargo test -p lambda-vm-prover --test rpx_host_kat_vectors -- --ignored --nocapture\n", ); - out.push_str("// (prover/tests/rpx_host_kat_vectors.rs). Paste verbatim; do not edit by hand.\n\n"); + out.push_str( + "// (prover/tests/rpx_host_kat_vectors.rs). Paste verbatim; do not edit by hand.\n\n", + ); // ---- Table 2: the bare permutation ------------------------------------ let inputs = permutation_inputs(); @@ -170,7 +175,9 @@ fn print_rpx_host_kat_vectors() { "inline constexpr int NUM_RPX_PARENT_VECTORS = {};\n", parents.len() )); - out.push_str("inline constexpr RpxParentVector RPX_PARENT_VECTORS[NUM_RPX_PARENT_VECTORS] = {\n"); + out.push_str( + "inline constexpr RpxParentVector RPX_PARENT_VECTORS[NUM_RPX_PARENT_VECTORS] = {\n", + ); for (name, l, r) in &parents { let got = HasherKind::Rpx.compress(&fe_array(l), &fe_array(r)); let got: Vec = got.iter().map(canonical).collect(); From 62a22f0192d8b05faae542145ff3f82ca1926746 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 7 Sep 2026 15:59:02 -0300 Subject: [PATCH 3/3] build: test-rpx-host-kat target for the RPX host known-answer harness Same shape as test-blake3-host-kat: host compile of the kernel source through the shim, then run. Lane K's harness; the Makefile is the coordinator's file. --- Makefile | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b3a69a62a..9bf689141 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ compile-programs compile-recursion-elfs clean-asm clean-rust clean-bench clean-s clean-recursion-elfs clean test test-asm \ test-rust test-ethrex test-ethrex-offline test-executor test-syscalls test-flamegraph flamegraph-prover test-profile-recursion test-profile-recursion-single test-profile-recursion-multi \ test-profile-recursion-block recursion-profile-block-input \ -test-fast test-prover test-prover-all test-prover-debug test-disk-spill test-math-cuda test-blake3-host-kat test-blake3-second-source test-cuda-integration test-cuda-d1 test-cuda-fallback \ +test-fast test-prover test-prover-all test-prover-debug test-disk-spill test-math-cuda test-blake3-host-kat test-rpx-host-kat test-blake3-second-source test-cuda-integration test-cuda-d1 test-cuda-fallback \ test-prover-cuda test-prover-comprehensive-cuda \ bench-math-cuda bench-prover bench-prover-cuda build check clippy fmt lint regen-ethrex-fixtures \ update-ethrex-fixture-checksums check-ethrex-fixture-checksums ethrex-real-block-fixture \ @@ -621,6 +621,17 @@ test-blake3-host-kat: -o target/host_kat/blake3_host_kat_6r $(HOST_KAT_DIR)/blake3_host_kat.cpp ./target/host_kat/blake3_host_kat_6r +# Known-answer tests for the RPX256 device kernel source, run on the HOST through +# the Track G shim (no GPU, no nvcc): the permutation, the rate-8 overwrite-duplex +# leaf and the parent compress against vectors printed from the Rust oracle +# (`prover/tests/rpx_host_kat_vectors.rs`), plus miden-crypto's 19 RPO vectors +# through the shared FB round. +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 + # SECOND-SOURCE validation of the 6-round vectors the KAT above trusts. # # `test-blake3-host-kat` checks the KERNEL against the committed tables. This