Repository navigation
ML-KEM AArch64: the noise sampler and PRF call are 16-bit only - #2858
Merged
Merged
Conversation
Every caller of the noise sampler, `prfCbdUsing` and the readonly transforms passes `w16 := true` since the 16-bit whole-KEM replaced the paired u32 compositions, so the flag and its 32-bit branches go, with the lemmas only those branches used (`readonly_out_ok`) and the 16-bit subtraction nothing calls (`subW`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #991.
This is the cleanup that #2849 left as a follow-up. Since #2849, every caller of the AArch64 ML-KEM noise sampler (
noiseAllWith,noisePairWith,noiseOutWith),cbdCallandprfCbdUsingpassesw16 := true.Changes
w16:cbdCallnow always callsvg_mlkem16_cbd2.nttAtRis deleted; callers usenttAtWithW.Proof/MlKem/AArch64/Noise/andOptimized/PrfUsing.leanlose theirw16binders and their 32-bit cases.readonly_out_oknoise*With_originaltheoremssubW/hsubOpand its proofs, added in ML-KEM AArch64: 16-bit paired key generation, encapsulation and decapsulation #2849 but never calledImpl/andProof/finds nothing else that became dead since before ML-KEM AArch64: 16-bit paired key generation, encapsulation and decapsulation #2849.No changes to
TCB/orSpec/.Not changed
The rejection sampler (
Rej8,Paired,Hybrid) keeps itsw16parameter. Its proofs shareSampleLoop's width-generic invariants with the 32-bitsampleNTT, which the instances without the SHA-3 extension still emit. Making it 16-bit only would touch about 120 proof files with no runtime change.Speed
The generated code is unchanged:
Emit.lean --checkpasses. No benchmark run, since the change cannot affect speed.Checks
These pass locally:
lake buildEmit.lean --checkcheck_lean_imports,check_lean_modules,check_registrations,check_lean_speed,check_vectors,check_arch_gates,check_variants,check_mcdtalgorithms_table.py(table unchanged)Generated by Claude Code