HOL-Light/x86_64: Refine output bound to 3q/4

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

dev/x86_64/src/arith_native_x86_64.h

@@ -55,7 +55,9 @@ __contract__(
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(qdata == mld_qdata)
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
-  ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  /* check-magic: off */
+  ensures(array_abs_bound(r, 0, MLDSA_N, 6285313))
+  /* check-magic: on */
 );
 
 #define mld_nttunpack_avx2 MLD_NAMESPACE(nttunpack_avx2)

mldsa/src/native/x86_64/src/arith_native_x86_64.h

@@ -55,7 +55,9 @@ __contract__(
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(qdata == mld_qdata)
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
-  ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  /* check-magic: off */
+  ensures(array_abs_bound(r, 0, MLDSA_N, 6285313))
+  /* check-magic: on */
 );
 
 #define mld_nttunpack_avx2 MLD_NAMESPACE(nttunpack_avx2)

proofs/hol_light/x86_64/proofs/mldsa_intt.ml

@@ -4305,7 +4305,7 @@ let MLDSA_INTT_CORRECT = prove
                         ==> let zi =
                       read(memory :> bytes32(word_add a (word(4 * i)))) s in
                       (ival zi == mldsa_inverse_ntt (ival o x) i) (mod &8380417) /\
-                      abs(ival zi) <= &8380416))
+                      abs(ival zi) <= &6285312))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
           MAYCHANGE [ZMM0; ZMM1; ZMM2; ZMM3; ZMM4; ZMM5; ZMM6; ZMM7; ZMM8; ZMM9; ZMM10; ZMM11; ZMM12; ZMM13; ZMM14; ZMM15] ,,
           MAYCHANGE [RAX] ,, MAYCHANGE SOME_FLAGS ,,
@@ -4477,7 +4477,7 @@ let MLDSA_INTT_NOIBT_SUBROUTINE_CORRECT = prove
                         ==> let zi =
                       read(memory :> bytes32(word_add a (word(4 * i)))) s in
                       (ival zi == mldsa_inverse_ntt (ival o x) i) (mod &8380417) /\
-                      abs(ival zi) <= &8380416))
+                      abs(ival zi) <= &6285312))
           (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
           MAYCHANGE [memory :> bytes(a,1024)])`,
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
@@ -4510,7 +4510,7 @@ let MLDSA_INTT_SUBROUTINE_CORRECT = prove
                         ==> let zi =
                       read(memory :> bytes32(word_add a (word(4 * i)))) s in
                       (ival zi == mldsa_inverse_ntt (ival o x) i) (mod &8380417) /\
-                      abs(ival zi) <= &8380416))
+                      abs(ival zi) <= &6285312))
           (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
           MAYCHANGE [memory :> bytes(a,1024)])`,
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in