HOL-Light: Simplify proof of poly_tobytes

The precondition in the HOL-Light proof for mlkem_poly_tobytes
abstracts the memory contents at the source pointer as a list
of 16-bit words. However, it is only in the post-condition that
the length of this list is constrained to be 256.
This does not seem to increase the expressivity of the spec
but complicates the proof; in particular, it adds the need for
another tactic currently fed the total number of instructions
in the function, and which is not readily amenable to wrapping
by the recently introduced MAP_UNTIL_TARGET_PC function.

This commit moves the length constraints on the abstract list
of 16-bit values to the precondition, simplifying the proof
and thereby making it agnostic to the total number of instructions.

Note that in general there can be value to pushing preconditions
into premises of the post-condition: For example, in the NTT or
invNTT, one can shove the constraint that the provided twiddle
table should contain the right twiddles into a premise of the
post-condition. This strictly increases expressivity, because even
for wrong twiddle tables, one still gets safety properties from
the proof. However, in the case of poly_tobytes, there does not
seem to be such gain from moving the length constraint into the
post-condition.

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

Author: hanno-becker

proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml

@@ -203,11 +203,11 @@ let MLKEM_POLY_TOBYTES_CORRECT = prove
              (\s. aligned_bytes_loaded s (word pc) mlkem_poly_tobytes_mc /\
                   read PC s = word (pc + MLKEM_POLY_TOBYTES_CORE_START) /\
                   C_ARGUMENTS [r;a] s /\
+                  LENGTH l = 256 /\
                   read (memory :> bytes(a,512)) s = num_of_wordlist l)
              (\s. read PC s = word(pc + MLKEM_POLY_TOBYTES_CORE_END) /\
-                  (LENGTH l = 256
-                   ==> read(memory :> bytes(r,384)) s =
-                       num_of_wordlist (MAP word_zx l:(12 word)list)))
+                  read(memory :> bytes(r,384)) s =
+                    num_of_wordlist (MAP word_zx l:(12 word)list))
              (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
               MAYCHANGE [memory :> bytes(r,384)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
@@ -216,12 +216,7 @@ let MLKEM_POLY_TOBYTES_CORRECT = prove
               NONOVERLAPPING_CLAUSES; ALL] THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
 
-  (*** Globalize the LENGTH l = 256 hypothesis ***)
-
-  ASM_CASES_TAC `LENGTH(l:int16 list) = 256` THENL
-   [ASM_REWRITE_TAC[] THEN ENSURES_INIT_TAC "s0";
-    ARM_QUICKSIM_TAC MLKEM_POLY_TOBYTES_EXEC
-     [`read X0 s = a`; `read X1 s = z`; `read X2 s = i`] (1--169)] THEN
+  ASM_REWRITE_TAC[] THEN ENSURES_INIT_TAC "s0" THEN
 
   (*** Digitize and tweak the input digits to match 128-bit load size  ****)
 
@@ -283,11 +278,11 @@ let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove
                   read PC s = word pc /\
                   read X30 s = returnaddress /\
                   C_ARGUMENTS [r;a] s /\
+                  LENGTH l = 256 /\
                   read (memory :> bytes(a,512)) s = num_of_wordlist l)
              (\s. read PC s = returnaddress /\
-                  (LENGTH l = 256
-                   ==> read(memory :> bytes(r,384)) s =
-                       num_of_wordlist (MAP word_zx l:(12 word)list)))
+                  read(memory :> bytes(r,384)) s =
+                       num_of_wordlist (MAP word_zx l:(12 word)list))
              (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
               MAYCHANGE [memory :> bytes(r,384)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN