HOL-Light: x86 INTT output bound <=26632 -> <=26631

During #1393, we noticed
that the HOL-Light proof for the x86 INTT proves the bound <=26632, while
our contract requires <= 26631.
This commit corrects the bound in the HOL-Light specification.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

proofs/hol_light/x86/proofs/mlkem_intt.ml

@@ -1051,7 +1051,7 @@ let MLKEM_INTT_CORRECT = prove
                         ==> let zi =
                       read(memory :> bytes16(word_add a (word(2 * i)))) s in
                       (ival zi == avx2_inverse_ntt (ival o x) i) (mod &3329) /\
-                      abs(ival zi) <= &26632))
+                      abs(ival zi) <= &26631))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI  ,,
            MAYCHANGE [ZMM0; ZMM1; ZMM2; ZMM3; ZMM4; ZMM5; ZMM6; ZMM7; ZMM8;
                       ZMM9; ZMM10; ZMM11; ZMM12; ZMM13; ZMM14; ZMM15] ,,
@@ -1187,7 +1187,7 @@ let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT  = prove
                         ==> let zi =
                       read(memory :> bytes16(word_add a (word(2 * i)))) s in
                       (ival zi == avx2_inverse_ntt (ival o x) i) (mod &3329) /\
-                      abs(ival zi) <= &26632))
+                      abs(ival zi) <= &26631))
           (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
            MAYCHANGE [memory :> bytes(a, 512)])`,
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
@@ -1217,7 +1217,7 @@ let MLKEM_INTT_SUBROUTINE_CORRECT  = prove
                         ==> let zi =
                       read(memory :> bytes16(word_add a (word(2 * i)))) s in
                       (ival zi == avx2_inverse_ntt (ival o x) i) (mod &3329) /\
-                      abs(ival zi) <= &26632))
+                      abs(ival zi) <= &26631))
           (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
            MAYCHANGE [memory :> bytes(a, 512)])`,
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in