ML-DSA Aarch64 HOL-Light proof poly_use_hint_88#375
Open
jakemas wants to merge 15 commits into
Open
Conversation
jakemas
force-pushed
the
mldsa-use-hint-88
branch
from
df869d4 to
3be154d
Compare
jakemas
force-pushed
the
mldsa-use-hint-88
branch
from
9f7d2d7 to
2072018
Compare
jakemas
force-pushed
the
mldsa-use-hint-88
branch
5 times, most recently
from
a9ba93e to
a92950b
Compare
jakemas
force-pushed
the
mldsa-use-hint-88
branch
2 times, most recently
from
a06f7a2 to
296bdf3
Compare
jakemas
force-pushed
the
mldsa-use-hint-88
branch
2 times, most recently
from
6c5ea70 to
a6c4ef5
Compare
…ctness Add formal verification proof for mldsa_poly_use_hint_88 AArch64 NEON implementation. The proof establishes full functional correctness: the assembly output equals word(mldsa_use_hint_88_spec(val(a), val(h))) for each element, matching the ML-DSA specification. Signed-off-by: Jake Massimo <jakemas@amazon.com>
Remove WORD_ISHR_ROUND_17 (superseded by VAL_DECOMPOSE_A1_88) and SPEC_BOUND_88 (output bounds lemma not needed for functional correctness). Signed-off-by: Jake Massimo <jakemas@amazon.com>
Move WORD_AND_ONES_32, WORD_MUL_1_32, REAL_INT_GT_BRIDGE, and REAL_INT_GT_BRIDGE_POS from the _88 proof file to the shared common file, so they can be reused by the _32 proof as well. Signed-off-by: Jake Massimo <jakemas@amazon.com>
Replace the 1129-line case-split Barrett proof with a general DIV_SANDWICH + BARRETT_INTERVAL lemma approach. The general lemma proves that if both formulas are sandwiched in [k*d, (k+1)*d) for a given interval, then both equal k. The proof cascades through the 45-entry interval table, discharging numeric side conditions with NUM_REDUCE_CONV. Signed-off-by: Jake Massimo <jakemas@amazon.com>
jakemas
force-pushed
the
mldsa-use-hint-88
branch
from
a6c4ef5 to
48a65f7
Compare
Add FIPS 204 definitions (mldsa_cmod, mldsa_decompose_88, mldsa_use_hint_88) and equivalence proof connecting code-aligned spec to FIPS 204 Algorithm 40. Move shared arch-independent helpers (DIV_SANDWICH, INT_MOD_RESIDUE) to common/mlkem_mldsa.ml. ENSURES_STRENGTHEN_POST stays in the proof file as it references armstate. Signed-off-by: Jake Massimo <jakemas@amazon.com>
The `let INT_MOD_RESIDUE = prove(` line was dropped, leaving an orphaned HOL term + tactic block that camlp5 could not parse: Parse error: [implem] expected after [str_item_semi] Signed-off-by: Jake Massimo <jakemas@amazon.com>
Apply the same refactor as PR awslabs#372 did for _32, mirroring pq-code-package/mldsa-native#1037 to keep the two repos consistent: - Rename the code-aligned per-coefficient spec mldsa_use_hint_88_spec to mldsa_use_hint_88_code and keep it local to the proof file. FIPS 204 mldsa_use_hint_88 (Algorithm 40) is the shared definition in common/mlkem_mldsa.ml. - Rename the code-aligned CORRECT / CORRECT_BOUND / SUBROUTINE_CORRECT to *_CODE suffixes to mark them as internal stepping stones. - Make MLDSA_USE_HINT_88_SUBROUTINE_CORRECT the single public theorem, stated in terms of FIPS 204 mldsa_use_hint_88 with the < 44 output bound as a corollary. Derived from _SUBROUTINE_CORRECT_CODE via MLDSA_USE_HINT_88_EQUIV. - Move safety proof to the end of the file. mk_safety_spec still uses _SUBROUTINE_CORRECT_CODE so the hardcoded safety goal matches. - Lift shared FIPS 204 definitions (mldsa_cmod, mldsa_decompose_88, decompose_88_r{0,1}, mldsa_use_hint_88) and helpers (LOWER/UPPER _NONWRAP_R1_88, MLDSA_USE_HINT_88_UNFOLD) into common/mlkem_mldsa.ml. - Keep ENSURES_STRENGTHEN_POST local to the proof file (armstate-specific). Signed-off-by: Jake Massimo <jakemas@amazon.com>
Resolves conflicts by including both mldsa_poly_use_hint_88 from the PR branch and the three new mldsa_pointwise_acc functions (l4, l5, l7) from main in all affected files.
These x86-only functions were added in main but missing from the onlyInX86 array after merge, causing collect-signatures.py to fail.
jakemas
force-pushed
the
mldsa-use-hint-88
branch
from
4a3abce to
fc2d495
Compare
…_hint_88 Add empty call_mldsa_poly_use_hint_88 stub in the x86 ifdef section of benchmark.c (matching the pattern used by mldsa_poly_use_hint_32), and use the `arm` enablement flag in test.c since this is an ARM-only function.
jakemas
force-pushed
the
mldsa-use-hint-88
branch
from
fc2d495 to
8526206
Compare
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
1 participant
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.
Summary
With help, and love, from Claude.
Add formal verification proof for
mldsa_poly_use_hint_88(AArch64 NEON), establishing full functional correctness: the assembly output equalsword(mldsa_use_hint_88_spec(val(a), val(h)))for each element, matching the FIPS 204 UseHint specification for GAMMA2 = (Q-1)/88 (ML-DSA security level 2, l=4).This is the companion to the
_32proof in PR #372.What the proof establishes
The proof verifies that hand-optimized NEON assembly — Barrett multiplication with magic constants, SIMD bit tricks, branchless conditional masking — produces exactly the same mathematical function as the FIPS 204 spec, for every valid input (8.4M x 2 input pairs).
Proof architecture
Barrett equivalence (
BARRETT_EQUIV_88): The assembly computesa1as((2 * a * 1477838209) / 2^32 + 65536) / 131072. The spec computes it as((a + 127) / 128 * 11275 + 8388608) / 16777216. These are completely different formulas. The proof establishes equivalence for alla < Qvia 44-case analysis, usingDIV_MONOto sandwich both formulas to the same constant in each output interval.Element correctness (
ELEMENT_CORRECT_88): Provesval(asm_result) = spec(val(a), val(h))for a single element. Splits into wrap (a1=44) and nowrap (a1<=43) cases. Uses bridge lemmas for native-modereal_gt/int_gtcompatibility, BDD-based BITBLAST for word comparison bounds, andDIV_MONO-based upper bounds for the remainder.SIMD endgame (
MLDSA_USE_HINT_88_CORRECT): After 1006-step ARM symbolic execution, pushesword_subwordthrough SIMD operations to extract per-element 32-bit results, then matches each against the element correctness theorem.Shared helpers:
WORD_AND_ONES_32,WORD_MUL_1_32,REAL_INT_GT_BRIDGE,REAL_INT_GT_BRIDGE_POSmoved tocommon/mlkem_mldsa.mlfor reuse by both_32and_88proofs.Changes
arm/proofs/mldsa_poly_use_hint_88.ml— full proof with functional correctness postcondition, constant-time and memory safetyarm/mldsa/mldsa_poly_use_hint_88.S— assembly sourcecommon/mlkem_mldsa.ml— shared helper lemmasTesting
Proof verified end-to-end in HOL Light (both interpreted MCP and native compilation CI). Also verified in the mldsa-native fork which runs native-mode CI.