pq-code-package · hanno-becker · May 22, 2026 · May 21, 2026
@@ -203,6 +203,8 @@ jobs:
       matrix:
         proof:
           # Dependencies on {name}.{S,ml} are implicit
+          - name: poly_caddq_avx2_asm
+            needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
           - name: ntt_avx2_asm
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
           - name: intt_avx2_asm

@@ -263,6 +263,7 @@ source code and documentation.
   - [proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S)
   - [proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S)
   - [proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S)
 
 ### `Round3_Spec`
 

@@ -99,7 +99,15 @@ void mld_poly_decompose_88_avx2(int32_t *a1, int32_t *a0);
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
 #define mld_poly_caddq_avx2_asm MLD_NAMESPACE(poly_caddq_avx2_asm)
-void mld_poly_caddq_avx2_asm(int32_t *r);
+void mld_poly_caddq_avx2_asm(int32_t *r)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/x86_64/proofs/poly_caddq_avx2_asm.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, 0, MLDSA_Q))
+);
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_avx2 MLD_NAMESPACE(mld_poly_use_hint_32_avx2)

@@ -46,22 +46,43 @@ vmovdqa  \reg, \offset(%rdi)
 .balign 16
 MLD_ASM_FN_SYMBOL(poly_caddq_avx2_asm)
 
-mov $8380417, %edx
-leaq 1024(%rdi), %rax
 vpxor %xmm2, %xmm2, %xmm2
-vmovd %edx, %xmm1
+mov $8380417, %eax
+vmovd %eax, %xmm1
 vpbroadcastd %xmm1, %ymm1
 
-poly_caddq_avx2_loop:
-
 caddq_vector 0, %ymm0
 caddq_vector 32, %ymm3
 caddq_vector 64, %ymm4
 caddq_vector 96, %ymm5
-
-addq   $128, %rdi        /* advance by 128 bytes (4 vectors) */ 
-cmpq   %rdi, %rax
-jne    poly_caddq_avx2_loop   /* 8 iterations (32/4 = 8) */ 
+caddq_vector 128, %ymm0
+caddq_vector 160, %ymm3
+caddq_vector 192, %ymm4
+caddq_vector 224, %ymm5
+caddq_vector 256, %ymm0
+caddq_vector 288, %ymm3
+caddq_vector 320, %ymm4
+caddq_vector 352, %ymm5
+caddq_vector 384, %ymm0
+caddq_vector 416, %ymm3
+caddq_vector 448, %ymm4
+caddq_vector 480, %ymm5
+caddq_vector 512, %ymm0
+caddq_vector 544, %ymm3
+caddq_vector 576, %ymm4
+caddq_vector 608, %ymm5
+caddq_vector 640, %ymm0
+caddq_vector 672, %ymm3
+caddq_vector 704, %ymm4
+caddq_vector 736, %ymm5
+caddq_vector 768, %ymm0
+caddq_vector 800, %ymm3
+caddq_vector 832, %ymm4
+caddq_vector 864, %ymm5
+caddq_vector 896, %ymm0
+caddq_vector 928, %ymm3
+caddq_vector 960, %ymm4
+caddq_vector 992, %ymm5
 ret
 
 /* simpasm: footer-start */

@@ -99,7 +99,15 @@ void mld_poly_decompose_88_avx2(int32_t *a1, int32_t *a0);
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
 #define mld_poly_caddq_avx2_asm MLD_NAMESPACE(poly_caddq_avx2_asm)
-void mld_poly_caddq_avx2_asm(int32_t *r);
+void mld_poly_caddq_avx2_asm(int32_t *r)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/x86_64/proofs/poly_caddq_avx2_asm.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, 0, MLDSA_Q))
+);
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_avx2 MLD_NAMESPACE(mld_poly_use_hint_32_avx2)

@@ -44,13 +44,10 @@
 MLD_ASM_FN_SYMBOL(poly_caddq_avx2_asm)
 
         .cfi_startproc
-        movl $0x7fe001, %edx         # imm = 0x7FE001
-        leaq 0x400(%rdi), %rax
         vpxor %xmm2, %xmm2, %xmm2
-        vmovd %edx, %xmm1
+        movl $0x7fe001, %eax         # imm = 0x7FE001
+        vmovd %eax, %xmm1
         vpbroadcastd %xmm1, %ymm1
-
-Lpoly_caddq_avx2_loop:
         vpcmpgtd (%rdi), %ymm2, %ymm0
         vpand %ymm1, %ymm0, %ymm0
         vpaddd (%rdi), %ymm0, %ymm0
@@ -67,9 +64,118 @@ Lpoly_caddq_avx2_loop:
         vpand %ymm1, %ymm5, %ymm5
         vpaddd 0x60(%rdi), %ymm5, %ymm5
         vmovdqa %ymm5, 0x60(%rdi)
-        addq $0x80, %rdi
-        cmpq %rdi, %rax
-        jne Lpoly_caddq_avx2_loop
+        vpcmpgtd 0x80(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x80(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x80(%rdi)
+        vpcmpgtd 0xa0(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0xa0(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0xa0(%rdi)
+        vpcmpgtd 0xc0(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0xc0(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0xc0(%rdi)
+        vpcmpgtd 0xe0(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0xe0(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0xe0(%rdi)
+        vpcmpgtd 0x100(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x100(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x100(%rdi)
+        vpcmpgtd 0x120(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x120(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x120(%rdi)
+        vpcmpgtd 0x140(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x140(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x140(%rdi)
+        vpcmpgtd 0x160(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x160(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x160(%rdi)
+        vpcmpgtd 0x180(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x180(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x180(%rdi)
+        vpcmpgtd 0x1a0(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x1a0(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x1a0(%rdi)
+        vpcmpgtd 0x1c0(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x1c0(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x1c0(%rdi)
+        vpcmpgtd 0x1e0(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x1e0(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x1e0(%rdi)
+        vpcmpgtd 0x200(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x200(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x200(%rdi)
+        vpcmpgtd 0x220(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x220(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x220(%rdi)
+        vpcmpgtd 0x240(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x240(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x240(%rdi)
+        vpcmpgtd 0x260(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x260(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x260(%rdi)
+        vpcmpgtd 0x280(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x280(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x280(%rdi)
+        vpcmpgtd 0x2a0(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x2a0(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x2a0(%rdi)
+        vpcmpgtd 0x2c0(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x2c0(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x2c0(%rdi)
+        vpcmpgtd 0x2e0(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x2e0(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x2e0(%rdi)
+        vpcmpgtd 0x300(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x300(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x300(%rdi)
+        vpcmpgtd 0x320(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x320(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x320(%rdi)
+        vpcmpgtd 0x340(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x340(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x340(%rdi)
+        vpcmpgtd 0x360(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x360(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x360(%rdi)
+        vpcmpgtd 0x380(%rdi), %ymm2, %ymm0
+        vpand %ymm1, %ymm0, %ymm0
+        vpaddd 0x380(%rdi), %ymm0, %ymm0
+        vmovdqa %ymm0, 0x380(%rdi)
+        vpcmpgtd 0x3a0(%rdi), %ymm2, %ymm3
+        vpand %ymm1, %ymm3, %ymm3
+        vpaddd 0x3a0(%rdi), %ymm3, %ymm3
+        vmovdqa %ymm3, 0x3a0(%rdi)
+        vpcmpgtd 0x3c0(%rdi), %ymm2, %ymm4
+        vpand %ymm1, %ymm4, %ymm4
+        vpaddd 0x3c0(%rdi), %ymm4, %ymm4
+        vmovdqa %ymm4, 0x3c0(%rdi)
+        vpcmpgtd 0x3e0(%rdi), %ymm2, %ymm5
+        vpand %ymm1, %ymm5, %ymm5
+        vpaddd 0x3e0(%rdi), %ymm5, %ymm5
+        vmovdqa %ymm5, 0x3e0(%rdi)
         retq
         .cfi_endproc
 

@@ -4,12 +4,12 @@
 { stdenv, fetchFromGitHub, writeText, ... }:
 stdenv.mkDerivation rec {
   pname = "s2n_bignum";
-  version = "f3c5acff6948d559194245237f6aaa7ebf7fcae8";
+  version = "ccef24569ed5c41f4e7fcb19965bf48eff3fdaa0";
   src = fetchFromGitHub {
     owner = "awslabs";
     repo = "s2n-bignum";
     rev = "${version}";
-    hash = "sha256-kfc8X2e+voefttshSUdifDc3Qn+dx0Gq5ENNLhWIdw0=";
+    hash = "sha256-1KHAmHtBKMO+8Ea+1TTF6adKW3XKRmfcJC1vNZ/guRA=";
   };
   setupHook = writeText "setup-hook.sh" ''
     export S2N_BIGNUM_DIR="$1"

@@ -0,0 +1,58 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_caddq_native_x86_64_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = poly_caddq_native_x86_64
+
+# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
+# included, which contains the CBMC specifications.
+DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/x86_64/meta.h\"" -DMLD_CHECK_APIS
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
+
+CHECK_FUNCTION_CONTRACTS=mld_poly_caddq_native
+USE_FUNCTION_CONTRACTS = mld_poly_caddq_avx2_asm
+USE_FUNCTION_CONTRACTS += mld_sys_check_capability
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = poly_caddq_native_x86_64
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
@@ -0,0 +1,15 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stdint.h>
+#include "cbmc.h"
+#include "params.h"
+
+int mld_poly_caddq_native(int32_t a[MLDSA_N]);
+
+void harness(void)
+{
+  int32_t *a;
+  int t;
+  t = mld_poly_caddq_native(a);
+}
@@ -139,6 +139,7 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
 - ML-DSA Arithmetic:
   * x86_64 forward NTT: [ntt_avx2_asm.S](x86_64/mldsa/ntt_avx2_asm.S)
   * x86_64 inverse NTT: [intt_avx2_asm.S](x86_64/mldsa/intt_avx2_asm.S)
+  * x86_64 poly_caddq: [poly_caddq_avx2_asm.S](x86_64/mldsa/poly_caddq_avx2_asm.S)
   * x86_64 NTT unpack: [nttunpack_avx2_asm.S](x86_64/mldsa/nttunpack_avx2_asm.S)
   * x86_64 pointwise multiplication: [pointwise_avx2_asm.S](x86_64/mldsa/pointwise_avx2_asm.S)
   * x86_64 pointwise multiplication-accumulation (l=4): [pointwise_acc_l4_avx2_asm.S](x86_64/mldsa/pointwise_acc_l4_avx2_asm.S)

@@ -1732,6 +1732,44 @@ let MLDSA_USE_HINT_88_UNFOLD = prove(
   SPEC_TAC(`mldsa_decompose_88 r`, `p:num#int`) THEN
   REWRITE_TAC[FORALL_PAIR_THM] THEN
   CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[]);;
+
+(* ========================================================================= *)
+(* caddq: conditional addition of q for signed-to-unsigned reduction          *)
+(*                                                                           *)
+(* Maps a coefficient in (-q, q) to [0, q) by adding q if negative.          *)
+(* ========================================================================= *)
+
+let mldsa_caddq_spec = new_definition
+  `mldsa_caddq_spec (x:int) : int =
+    if x < &0 then x + &8380417 else x`;;
+
+let MLDSA_CADDQ_SPEC_REM = prove
+ (`!x. abs x < &8380417 ==> mldsa_caddq_spec x = x rem &8380417`,
+  GEN_TAC THEN REWRITE_TAC[mldsa_caddq_spec] THEN DISCH_TAC THEN
+  COND_CASES_TAC THENL
+   [ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
+    REWRITE_TAC[INT_REM_UNIQUE] THEN
+    CONV_TAC INT_REDUCE_CONV THEN
+    CONJ_TAC THENL [ASM_INT_ARITH_TAC; CONV_TAC INTEGER_RULE];
+    MATCH_MP_TAC(GSYM INT_REM_LT) THEN ASM_INT_ARITH_TAC]);;
+
+let MLDSA_CADDQ_SPEC_BOUNDS = prove
+ (`!x. abs x < &8380417
+       ==> &0 <= mldsa_caddq_spec x /\ mldsa_caddq_spec x < &8380417`,
+  GEN_TAC THEN DISCH_TAC THEN
+  MP_TAC(SPEC `x:int` MLDSA_CADDQ_SPEC_REM) THEN ASM_REWRITE_TAC[] THEN
+  DISCH_THEN SUBST1_TAC THEN CONJ_TAC THENL
+   [MP_TAC(SPECL [`x:int`; `&8380417:int`] INT_REM_POS) THEN INT_ARITH_TAC;
+    MP_TAC(SPECL [`x:int`; `&8380417:int`] INT_LT_REM) THEN INT_ARITH_TAC]);;
+
+let MLDSA_CADDQ_SPEC_LOWER = prove
+ (`!x. abs x < &8380417 ==> &0 <= mldsa_caddq_spec x`,
+  MESON_TAC[MLDSA_CADDQ_SPEC_BOUNDS]);;
+
+let MLDSA_CADDQ_SPEC_UPPER = prove
+ (`!x. abs x < &8380417 ==> mldsa_caddq_spec x < &8380417`,
+  MESON_TAC[MLDSA_CADDQ_SPEC_BOUNDS]);;
+
 (* ========================================================================= *)
 (* decompose: bound lemmas for FST/SND of mldsa_decompose_{32,88}            *)
 (*                                                                           *)

@@ -53,6 +53,7 @@ SPLIT=tr ';' '\n'
 OBJ = mldsa/ntt_avx2_asm.o \
       mldsa/intt_avx2_asm.o \
       mldsa/nttunpack_avx2_asm.o \
+      mldsa/poly_caddq_avx2_asm.o \
       mldsa/pointwise_avx2_asm.o \
       mldsa/pointwise_acc_l4_avx2_asm.o \
       mldsa/pointwise_acc_l5_avx2_asm.o \