Skip to content

test(math-cuda): pin the RPX kernel's canonicalisation loop with a deterministic witness (lane K, follow-up to #952) - #959

Merged
MauroToscano merged 2 commits into
per-table-gpufrom
pt/rpx-kat-canon
Sep 7, 2026
Merged

test(math-cuda): pin the RPX kernel's canonicalisation loop with a deterministic witness (lane K, follow-up to #952)#959
MauroToscano merged 2 commits into
per-table-gpufrom
pt/rpx-kat-canon

Conversation

@MauroToscano

Copy link
Copy Markdown
Contributor

Follow-up to #952 (lane K), the one required finding from its review: the canonicalisation loop at the end of rpx::permute was unpinned. Every oracle comparison canonicalised the kernel side before comparing, and a raw comparison on outputs that merely happen to be canonical — all but a 2^-32 slice per lane — could not see the loop either. A phase-2 edit that lost it would have produced Merkle nodes whose bytes differ from the host's in a few percent of 2^24-leaf trees, as a flaky root or auth-path mismatch. Separate small PR by the coordinator's decision; phase 2 proper still waits for lane D.

What changes (own files only)

  • crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp — the permutation, leaf and parent oracle checks compare raw (s[i] == v.output[i]; the tables are canonical by construction). New check the_canonicalisation_loop_is_pinned_by_the_witness: finds the table row named canonicalisation witness, replays the seven rounds without the loop, asserts lane 0 is the raw twin p + 1 (so the witness cannot go stale silently), then asserts permute returns the oracle's digits raw.
  • prover/tests/rpx_host_kat_vectors.rs — one hard-coded eleventh input, canonicalisation witness.
  • crypto/math-cuda/tests/host_kat/rpx_kat_vectors.h — the generator's output at e9fb361 pasted (Table 2 → 11 rows; leaf and parent tables byte-identical to the 824d678 relay, same seeds).
  • crypto/math-cuda/tests/host_kat/rpx_canon_witness.py — the derivation, self-checking: it reproduces every oracle row forward, inverts each back to its input, and asserts the generator carries its exact row.

How the witness is built (no search)

The permutation's last operation is out_i = add(m_i, ARK1[6][i]) with m_i the M-round MDS output. Choosing the canonical MDS output u_0 = p − ARK1[6][0] + 1 makes the device's final add return u_0 + ARK1[6][0] = p + 1 — the raw twin of 1 — deterministically: that sum cannot wrap, and m_0 cannot itself be a twin (u_0 + p > 2^64), whatever representation the earlier rounds carry. u_1..u_11 are seeded random; the M-round input is MDS⁻¹(u); the permutation input is the host inverse of rounds 5..0 (x^{1/7} in GF(p³) via 7⁻¹ mod p³−1 for the E rounds; x^7 → −ARK2 → MDS⁻¹ → x^{1/7} → −ARK1 → MDS⁻¹ for the FB rounds).

Gate

make test-rpx-host-kat on the laptop with the witness row present:

$ make test-rpx-host-kat
★ EXTERNAL: seven fb_round<R> = RPO256 vs miden-crypto hash_elements: 19/19 matched
★ ORACLE: rpx::permute vs Rust Rpx256::permute: 11/11 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
★ canonicalisation pin: witness leaves 1 raw lane(s) >= p before the loop; permute() returns them canonical
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

Mutant, as required: the same harness against a copy of rpx.cu with the canonicalisation loop deleted (the #pragma unroll + for … goldilocks::canonical(s[i]) lines in permute):

FAIL rpx permutation vector 10 (canonicalisation witness)
  lane  0 got 18446744069414584322 (raw) want 1
★ ORACLE: rpx::permute vs Rust Rpx256::permute: 10/11 vectors matched
★ 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
FAIL: permute must return the witness's digits RAW — the canonicalisation loop is missing
*** 2 FAILURE(S) ***

Before the oracle row was pasted, the harness reported exactly one failure (the permutation table must carry the 'canonicalisation witness' row) and nothing else. Generator run on box A at e9fb361: ``test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out (release); the relay's diff against the 824d6783 tables is exactly the count line 10 → 11 and the added row. `cargo check -p lambda-vm-prover --test rpx_host_kat_vectors`: exit 0 on this base.

Requests

  • make lint on a box (laptop rule); the only Rust delta is the generator's new row and doc comment; cargo fmt --all clean.
  • Standing gap (coordinator's, noted by the reviewer): neither host-KAT target is wired into a CI workflow.

…terministic witness

The review of the RPX host known-answer harness found that the final
canonicalisation loop of rpx::permute was unpinned: every oracle check
canonicalised the kernel's output before comparing, and a raw comparison
on outputs that merely happen to be canonical — all but a 2^-32 slice per
lane — would not see the loop either. A kernel that lost it would produce
Merkle nodes whose bytes differ from the host's in a few percent of
2^24-leaf trees.

The three oracle checks now compare RAW against the (canonical) tables,
and the generator gains one input built so that the comparison can see
the loop: its M-round MDS output lane 0 is p − ARK1[6][0] + 1, so the
device's final add returns the raw twin p + 1 where the field value is 1,
deterministically. No search was needed — the input is the host inverse
of the permutation from that target (x^{1/7} in GF(p^3) for the E rounds),
derived by tests/host_kat/rpx_canon_witness.py, which reproduces every
oracle row forward and inverts it back before it trusts itself, and
asserts the generator carries its exact row. A new harness check replays
the seven rounds on that row and asserts lane 0 is p + 1 before the loop,
so the witness cannot go stale silently, then asserts permute returns the
oracle's digits raw.

The witness's table row is printed by the generator on a box and lands in
a follow-up commit; until then the harness fails loudly on exactly that.
The generator at e9fb361, run on a box, prints eleven permutation rows:
the ten of the phase-1 relay unchanged plus the row named
"canonicalisation witness", whose output lane 0 is 1 — the field value
whose raw twin p + 1 the kernel holds before its final canonicalisation
loop. Leaf and parent tables are byte-identical to before (same seeds).

With the row present the host-KAT passes in full, including the new pin
check; a copy of rpx.cu with the loop deleted fails the witness row's raw
comparison (lane 0 reads 18446744069414584322 where the oracle says 1)
and the pin check.
@MauroToscano
MauroToscano merged commit dd2a41e into per-table-gpu Sep 7, 2026
8 checks passed
@MauroToscano
MauroToscano deleted the pt/rpx-kat-canon branch September 7, 2026 19:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant