ML-DSA x86 HOL-Light proof mldsa_caddq#398
Open
jakemas wants to merge 6 commits intoawslabs:mainfrom
Open
Conversation
Add VEX-encoded packed signed integer compare-greater-than instructions (VPCMPGTD for 32-bit lanes, VPCMPGTW for 16-bit lanes) needed for the ML-DSA caddq conditional addition implementation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add conditional addition of Q (8380417) to ML-DSA polynomial coefficients. For each coefficient, if negative, adds Q to produce a non-negative representative. Proves output equals input rem Q when |input| < Q. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add constant-time and memory safety proofs for all 4 ABI variants, proving all memory accesses stay within the declared input/output buffer. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
jakemas
added a commit
to pq-code-package/mldsa-native
that referenced
this pull request
Apr 28, 2026
Point s2n-bignum at awslabs/s2n-bignum#398 branch which includes the VPCMPGTD/VPCMPGTW instruction models needed for the x86 poly_caddq HOL Light proof. Signed-off-by: Jake Massimo <jakemas@amazon.com>
jakemas
changed the title
jakemas
changed the title
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
mldsa_caddq(conditional add Q for ML-DSA polynomial coefficients)|ival(x)| < Q, the output satisfiesival(output) = ival(x) rem QDepends on: #397 (VPCMPGTD/VPCMPGTW instruction models)
Changes
x86/mldsa/mldsa_caddq.S: Fully unrolled AVX2 assembly (VPCMPGTD + VPAND + VPADDD)x86_att/mldsa/mldsa_caddq.S: AT&T syntax version (auto-generated, binary-verified)x86/proofs/mldsa_caddq.ml: Complete formal proof (815 lines)x86/proofs/specifications.txt: 8 theorem entries (4 correct + 4 safe)x86/proofs/subroutine_signatures.ml: Signature for safety proofx86/Makefile,x86_att/Makefile: Build entriesinclude/s2n-bignum.h,include/s2n-bignum-c89.h: Function prototypetests/test.c: Functional test with reference implementationbenchmarks/benchmark.c: Benchmark entrytools/collect-signatures.py: Added to onlyInX86Test plan
loadtfrom checkpoint)makeinx86_att/)cd tests && make go— mldsa_caddq passes 100 test casescd benchmarks && make go— 14.3 ns/call🤖 Generated with Claude Code