From 1d748421240d31be8e8c08e53d1b8cf0c8983824 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 6 Oct 2025 09:19:46 +0100 Subject: [PATCH] HOL-Light: Avoid hardcoded lengths in HOL-Light proof scripts Previously, the HOL-Light proof scripts contained various hardcoded constants related to the length of the code under proof, as well as the lengths of preamble and postamble (stack spill and restore). This commit replaces those hardcoded numerals with symbolic definitions. As a result, SLOTHY re-optimization should now no longer require a proof script change beyond the update of the byte code which is done by `autogen` already. Signed-off-by: Hanno Becker --- .../arm/proofs/keccak_f1600_x1_scalar.ml | 38 ++++++++++++++--- .../arm/proofs/keccak_f1600_x1_v84a.ml | 38 ++++++++++++++--- .../arm/proofs/keccak_f1600_x2_v84a.ml | 40 +++++++++++++++--- .../arm/proofs/keccak_f1600_x4_v8a_scalar.ml | 39 ++++++++++++++--- .../proofs/keccak_f1600_x4_v8a_v84a_scalar.ml | 38 ++++++++++++++--- proofs/hol_light/arm/proofs/mlkem_intt.ml | 38 ++++++++++++++--- proofs/hol_light/arm/proofs/mlkem_ntt.ml | 39 ++++++++++++++--- ...m_poly_basemul_acc_montgomery_cached_k2.ml | 12 ++++++ ...m_poly_basemul_acc_montgomery_cached_k3.ml | 12 ++++++ ...m_poly_basemul_acc_montgomery_cached_k4.ml | 11 +++++ .../arm/proofs/mlkem_poly_mulcache_compute.ml | 12 ++++++ .../hol_light/arm/proofs/mlkem_poly_reduce.ml | 41 +++++++++++++++--- .../arm/proofs/mlkem_poly_tobytes.ml | 38 ++++++++++++++--- .../hol_light/arm/proofs/mlkem_poly_tomont.ml | 12 ++++++ .../hol_light/arm/proofs/mlkem_rej_uniform.ml | 42 +++++++++++++++---- 15 files changed, 397 insertions(+), 53 deletions(-) diff --git a/proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml b/proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml index 738075607..c7640e200 100644 --- a/proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml +++ b/proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml @@ -310,6 +310,32 @@ let keccak_f1600_x1_scalar_mc = define_assert_from_elf let KECCAK_F1600_X1_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_scalar_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_KECCAK_F1600_X1_SCALAR_MC = + REWRITE_CONV[keccak_f1600_x1_scalar_mc] `LENGTH keccak_f1600_x1_scalar_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH = 28`;; + +let KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH = 32`;; + +let KECCAK_F1600_X1_SCALAR_CORE_START = new_definition + `KECCAK_F1600_X1_SCALAR_CORE_START = KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH`;; + +let KECCAK_F1600_X1_SCALAR_CORE_END = new_definition + `KECCAK_F1600_X1_SCALAR_CORE_END = LENGTH keccak_f1600_x1_scalar_mc - KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_KECCAK_F1600_X1_SCALAR_MC; + KECCAK_F1600_X1_SCALAR_CORE_START; KECCAK_F1600_X1_SCALAR_CORE_END; + KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + (*** Additional lazy/deferred rotations in the implementation, row-major ***) let deferred_rotates = define @@ -339,21 +365,22 @@ let KECCAK_F1600_X1_SCALAR_CORRECT = prove nonoverlapping (a,200) (stackpointer,32) /\ ALLPAIRS nonoverlapping [(a,200); (stackpointer,32)] - [(word pc,0x480); (rc,192)] + [(word pc,LENGTH keccak_f1600_x1_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_scalar_mc /\ - read PC s = word (pc + 0x1c) /\ + read PC s = word (pc + KECCAK_F1600_X1_SCALAR_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A /\ wordlist_from_memory(rc,24) s = round_constants) - (\s. read PC s = word(pc + 0x460) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X1_SCALAR_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30] ,, MAYCHANGE [memory :> bytes(a,200); memory :> bytes(stackpointer,32)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `rc:int64`; `A:int64 list`; `pc:num`; `stackpointer:int64`] THEN REWRITE_TAC[fst KECCAK_F1600_X1_SCALAR_EXEC] THEN @@ -461,7 +488,7 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove nonoverlapping (a,200) (word_sub stackpointer (word 128),128) /\ ALLPAIRS nonoverlapping [(a,200); (word_sub stackpointer (word 128),128)] - [(word pc,0x480); (rc,192)] + [(word pc,LENGTH keccak_f1600_x1_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_scalar_mc /\ read PC s = word pc /\ @@ -475,8 +502,9 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,200); memory :> bytes(word_sub stackpointer (word 128),128)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(7,7) KECCAK_F1600_X1_SCALAR_EXEC - (CONV_RULE TWEAK_CONV KECCAK_F1600_X1_SCALAR_CORRECT) + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X1_SCALAR_CORRECT)) `[X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 128);; diff --git a/proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml b/proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml index 017c5a3d5..669964d2e 100644 --- a/proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml +++ b/proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml @@ -129,6 +129,32 @@ let keccak_f1600_x1_v84a_mc = define_assert_from_elf let KECCAK_F1600_X1_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_v84a_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_KECCAK_F1600_X1_V84A_MC = + REWRITE_CONV[keccak_f1600_x1_v84a_mc] `LENGTH keccak_f1600_x1_v84a_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH = 20`;; + +let KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH = 24`;; + +let KECCAK_F1600_X1_V84A_CORE_START = new_definition + `KECCAK_F1600_X1_V84A_CORE_START = KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH`;; + +let KECCAK_F1600_X1_V84A_CORE_END = new_definition + `KECCAK_F1600_X1_V84A_CORE_END = LENGTH keccak_f1600_x1_v84a_mc - KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_KECCAK_F1600_X1_V84A_MC; + KECCAK_F1600_X1_V84A_CORE_START; KECCAK_F1600_X1_V84A_CORE_END; + KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH; KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + (*** Introduce ghost variables for Qn given Dn register reads in a list ***) let GHOST_SUBREGLIST_TAC = @@ -144,18 +170,19 @@ let GHOST_SUBREGLIST_TAC = let KECCAK_F1600_X1_V84A_CORRECT = prove (`!a rc A pc. - ALL (nonoverlapping (a,200)) [(word pc,0x1ac); (rc,192)] + ALL (nonoverlapping (a,200)) [(word pc,LENGTH keccak_f1600_x1_v84a_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_v84a_mc /\ - read PC s = word (pc + 0x14) /\ + read PC s = word (pc + KECCAK_F1600_X1_V84A_CORE_START) /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A /\ wordlist_from_memory(rc,24) s = round_constants) - (\s. read PC s = word(pc + 0x194) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X1_V84A_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,, MAYCHANGE [memory :> bytes(a,200)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `rc:int64`; `A:int64 list`; `pc:num`] THEN REWRITE_TAC[fst KECCAK_F1600_X1_V84A_EXEC] THEN @@ -246,7 +273,7 @@ let KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT = prove nonoverlapping (a,200) (word_sub stackpointer (word 64),64) /\ ALLPAIRS nonoverlapping [(a,200); (word_sub stackpointer (word 64),64)] - [(word pc,0x1ac); (rc,192)] + [(word pc,LENGTH keccak_f1600_x1_v84a_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_v84a_mc /\ read PC s = word pc /\ @@ -260,8 +287,9 @@ let KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,200); memory :> bytes(word_sub stackpointer (word 64),64)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) KECCAK_F1600_X1_V84A_EXEC - (CONV_RULE TWEAK_CONV KECCAK_F1600_X1_V84A_CORRECT) + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X1_V84A_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15]` 64);; diff --git a/proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml b/proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml index d5d15e5de..1b45cec50 100644 --- a/proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml +++ b/proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml @@ -183,26 +183,55 @@ let keccak_f1600_x2_v84a_mc = define_assert_from_elf let KECCAK_F1600_X2_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x2_v84a_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_KECCAK_F1600_X2_V84A_MC = + REWRITE_CONV[keccak_f1600_x2_v84a_mc] `LENGTH keccak_f1600_x2_v84a_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH = 20`;; + +let KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH = 24`;; + +let KECCAK_F1600_X2_V84A_CORE_START = new_definition + `KECCAK_F1600_X2_V84A_CORE_START = KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH`;; + +let KECCAK_F1600_X2_V84A_CORE_END = new_definition + `KECCAK_F1600_X2_V84A_CORE_END = LENGTH keccak_f1600_x2_v84a_mc - KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_KECCAK_F1600_X2_V84A_MC; + KECCAK_F1600_X2_V84A_CORE_START; KECCAK_F1600_X2_V84A_CORE_END; + KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH; KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + +let KECCAK_F1600_X2_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x2_v84a_mc;; + (* ------------------------------------------------------------------------- *) (* Correctness proof *) (* ------------------------------------------------------------------------- *) let KECCAK_F1600_X2_V84A_CORRECT = prove (`!a rc A A' pc. - ALL (nonoverlapping (a,400)) [(word pc,0x284); (rc,192)] + ALL (nonoverlapping (a,400)) [(word pc,LENGTH keccak_f1600_x2_v84a_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x2_v84a_mc /\ - read PC s = word (pc + 0x14) /\ + read PC s = word (pc + KECCAK_F1600_X2_V84A_CORE_START) /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A /\ wordlist_from_memory(word_add a (word 200),25) s = A' /\ wordlist_from_memory(rc,24) s = round_constants) - (\s. read PC s = word(pc + 0x26c) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X2_V84A_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A') (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,, MAYCHANGE [memory :> bytes(a,400)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `rc:int64`; `A:int64 list`; `A':int64 list`; `pc:num`] THEN REWRITE_TAC[fst KECCAK_F1600_X2_V84A_EXEC] THEN @@ -318,7 +347,7 @@ let KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT = prove nonoverlapping (a,400) (word_sub stackpointer (word 64),64) /\ ALLPAIRS nonoverlapping [(a,400); (word_sub stackpointer (word 64),64)] - [(word pc,0x284); (rc,192)] + [(word pc,LENGTH keccak_f1600_x2_v84a_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x2_v84a_mc /\ read PC s = word pc /\ @@ -335,11 +364,12 @@ let KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,400); memory :> bytes(word_sub stackpointer (word 64),64)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV (WORDLIST_FROM_MEMORY_CONV THENC ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) KECCAK_F1600_X2_V84A_EXEC - (CONV_RULE TWEAK_CONV KECCAK_F1600_X2_V84A_CORRECT) + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X2_V84A_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15]` 64);; diff --git a/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml b/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml index c770c7267..3ad9efd06 100644 --- a/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml +++ b/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml @@ -999,6 +999,33 @@ let deferred_rotates = define 25; 8; 18; 1; 6; 10; 15; 56; 27; 36; 39; 41; 2; 62; 55]`;; +let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;; + +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC = + REWRITE_CONV[keccak_f1600_x4_v8a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_scalar_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = 44`;; + +let KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 48`;; + +let KECCAK_F1600_X4_V8A_SCALAR_CORE_START = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH`;; + +let KECCAK_F1600_X4_V8A_SCALAR_CORE_END = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC; + KECCAK_F1600_X4_V8A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_CORE_END; + KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; (* ------------------------------------------------------------------------- *) (* Correctness proof *) @@ -1010,10 +1037,10 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove nonoverlapping (a,800) (stackpointer,216) /\ ALLPAIRS nonoverlapping [(a,800); (stackpointer,216)] - [(word pc,0xf20); (rc,192)] + [(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\ - read PC s = word (pc + 0x2c) /\ + read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A1 /\ @@ -1021,7 +1048,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove wordlist_from_memory(word_add a (word 400),25) s = A3 /\ wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) - (\s. read PC s = word(pc + 0xef0) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -1036,6 +1063,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove MAYCHANGE [memory :> bytes(a,800); memory :> bytes(stackpointer,40); memory :> bytes(word_add stackpointer (word 208),8)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`; `A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN @@ -1419,7 +1447,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\ ALLPAIRS nonoverlapping [(a,800); (word_sub stackpointer (word 224),224)] - [(word pc,0xf20); (rc,192)] + [(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\ read PC s = word pc /\ @@ -1442,12 +1470,13 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,800); memory :> bytes(word_sub stackpointer (word 224),224)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV (WORDLIST_FROM_MEMORY_CONV THENC ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_EXEC - (CONV_RULE TWEAK_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT) + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; diff --git a/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml b/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml index a1b24f2dc..42982116a 100644 --- a/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml +++ b/proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml @@ -906,6 +906,32 @@ let deferred_rotates = define 10; 15; 56; 27; 36; 39; 41; 2; 62; 55]`;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_MC = + REWRITE_CONV[keccak_f1600_x4_v8a_v84a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = 44`;; + +let KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = 48`;; + +let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH`;; + +let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc - KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_MC; + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END; + KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + (* ------------------------------------------------------------------------- *) (* Correctness proof *) (* ------------------------------------------------------------------------- *) @@ -916,10 +942,10 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove nonoverlapping (a,800) (stackpointer,216) /\ ALLPAIRS nonoverlapping [(a,800); (stackpointer,216)] - [(word pc,0xda8); (rc,192)] + [(word pc,LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_v84a_scalar_mc /\ - read PC s = word (pc + 0x2c) /\ + read PC s = word (pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A1 /\ @@ -927,7 +953,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove wordlist_from_memory(word_add a (word 400),25) s = A3 /\ wordlist_from_memory(word_add a (word 600),25) s = A4 /\ wordlist_from_memory(rc,24) s = round_constants) - (\s. read PC s = word(pc + 0xd78) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -942,6 +968,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove MAYCHANGE [memory :> bytes(a,800); memory :> bytes(stackpointer,40); memory :> bytes(word_add stackpointer (word 208),8)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`; `A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN @@ -1325,7 +1352,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\ ALLPAIRS nonoverlapping [(a,800); (word_sub stackpointer (word 224),224)] - [(word pc,0xda8); (rc,192)] + [(word pc,LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc); (rc,192)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_v84a_scalar_mc /\ read PC s = word pc /\ @@ -1348,12 +1375,13 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,800); memory :> bytes(word_sub stackpointer (word 224),224)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV (WORDLIST_FROM_MEMORY_CONV THENC ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC - (CONV_RULE TWEAK_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT) + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; diff --git a/proofs/hol_light/arm/proofs/mlkem_intt.ml b/proofs/hol_light/arm/proofs/mlkem_intt.ml index 12de2a11d..53d119404 100644 --- a/proofs/hol_light/arm/proofs/mlkem_intt.ml +++ b/proofs/hol_light/arm/proofs/mlkem_intt.ml @@ -547,6 +547,32 @@ let mlkem_intt_mc = define_assert_from_elf let MLKEM_INTT_EXEC = ARM_MK_EXEC_RULE mlkem_intt_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_MLKEM_INTT_MC = + REWRITE_CONV[mlkem_intt_mc] `LENGTH mlkem_intt_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let MLKEM_INTT_PREAMBLE_LENGTH = new_definition + `MLKEM_INTT_PREAMBLE_LENGTH = 20`;; + +let MLKEM_INTT_POSTAMBLE_LENGTH = new_definition + `MLKEM_INTT_POSTAMBLE_LENGTH = 24`;; + +let MLKEM_INTT_CORE_START = new_definition + `MLKEM_INTT_CORE_START = MLKEM_INTT_PREAMBLE_LENGTH`;; + +let MLKEM_INTT_CORE_END = new_definition + `MLKEM_INTT_CORE_END = LENGTH mlkem_intt_mc - MLKEM_INTT_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_MLKEM_INTT_MC; + MLKEM_INTT_CORE_START; MLKEM_INTT_CORE_END; + MLKEM_INTT_PREAMBLE_LENGTH; MLKEM_INTT_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + let intt_constants = define `intt_constants z_12345 z_67 s <=> (!i. i < 80 @@ -564,16 +590,16 @@ let intt_constants = define let MLKEM_INTT_CORRECT = prove (`!a z_12345 z_67 x pc. ALL (nonoverlapping (a,512)) - [(word pc,0x828); (z_12345,160); (z_67,768)] + [(word pc,LENGTH mlkem_intt_mc); (z_12345,160); (z_67,768)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\ - read PC s = word (pc + 0x14) /\ + read PC s = word (pc + MLKEM_INTT_CORE_START) /\ C_ARGUMENTS [a; z_12345; z_67] s /\ intt_constants z_12345 z_67 s /\ !i. i < 256 ==> read(memory :> bytes16(word_add a (word(2 * i)))) s = x i) - (\s. read PC s = word(pc + 0x810) /\ + (\s. read PC s = word(pc + MLKEM_INTT_CORE_END) /\ !i. i < 256 ==> let zi = read(memory :> bytes16(word_add a (word(2 * i)))) s in @@ -582,6 +608,7 @@ let MLKEM_INTT_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,, MAYCHANGE [memory :> bytes(a,512)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; @@ -662,7 +689,7 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove aligned 16 stackpointer /\ ALLPAIRS nonoverlapping [(a,512); (word_sub stackpointer (word 64),64)] - [(word pc,0x828); (z_12345,160); (z_67,768)] /\ + [(word pc,LENGTH mlkem_intt_mc); (z_12345,160); (z_67,768)] /\ nonoverlapping (a,512) (word_sub stackpointer (word 64),64) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\ @@ -683,6 +710,7 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,512); memory :> bytes(word_sub stackpointer (word 64),64)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = REWRITE_CONV[intt_constants] THENC ONCE_DEPTH_CONV let_CONV THENC @@ -692,5 +720,5 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove REWRITE_TAC[fst MLKEM_INTT_EXEC] THEN CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) MLKEM_INTT_EXEC - (REWRITE_RULE[fst MLKEM_INTT_EXEC] (CONV_RULE TWEAK_CONV MLKEM_INTT_CORRECT)) + (REWRITE_RULE[fst MLKEM_INTT_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_INTT_CORRECT))) `[D8; D9; D10; D11; D12; D13; D14; D15]` 64);; diff --git a/proofs/hol_light/arm/proofs/mlkem_ntt.ml b/proofs/hol_light/arm/proofs/mlkem_ntt.ml index f9ba07b60..90a378047 100644 --- a/proofs/hol_light/arm/proofs/mlkem_ntt.ml +++ b/proofs/hol_light/arm/proofs/mlkem_ntt.ml @@ -346,6 +346,33 @@ let mlkem_ntt_mc = define_assert_from_elf let MLKEM_NTT_EXEC = ARM_MK_EXEC_RULE mlkem_ntt_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + + +let LENGTH_MLKEM_NTT_MC = + REWRITE_CONV[mlkem_ntt_mc] `LENGTH mlkem_ntt_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let MLKEM_NTT_PREAMBLE_LENGTH = new_definition + `MLKEM_NTT_PREAMBLE_LENGTH = 20`;; + +let MLKEM_NTT_POSTAMBLE_LENGTH = new_definition + `MLKEM_NTT_POSTAMBLE_LENGTH = 24`;; + +let MLKEM_NTT_CORE_START = new_definition + `MLKEM_NTT_CORE_START = MLKEM_NTT_PREAMBLE_LENGTH`;; + +let MLKEM_NTT_CORE_END = new_definition + `MLKEM_NTT_CORE_END = LENGTH mlkem_ntt_mc - MLKEM_NTT_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_MLKEM_NTT_MC; + MLKEM_NTT_CORE_START; MLKEM_NTT_CORE_END; + MLKEM_NTT_PREAMBLE_LENGTH; MLKEM_NTT_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + let ntt_constants = define `ntt_constants z_12345 z_67 s <=> (!i. i < 80 @@ -362,16 +389,16 @@ let ntt_constants = define let MLKEM_NTT_CORRECT = prove (`!a z_12345 z_67 x pc. ALL (nonoverlapping (a,512)) - [(word pc,0x504); (z_12345,160); (z_67,768)] + [(word pc,LENGTH mlkem_ntt_mc); (z_12345,160); (z_67,768)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\ - read PC s = word (pc + 0x14) /\ + read PC s = word (pc + MLKEM_NTT_CORE_START) /\ C_ARGUMENTS [a; z_12345; z_67] s /\ ntt_constants z_12345 z_67 s /\ !i. i < 256 ==> read(memory :> bytes16(word_add a (word(2 * i)))) s = x i) - (\s. read PC s = word(pc + 0x4ec) /\ + (\s. read PC s = word(pc + MLKEM_NTT_CORE_END) /\ ((!i. i < 256 ==> abs(ival(x i)) <= &8191) ==> !i. i < 256 ==> let zi = @@ -381,6 +408,7 @@ let MLKEM_NTT_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,, MAYCHANGE [memory :> bytes(a,512)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; @@ -466,7 +494,7 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove aligned 16 stackpointer /\ ALLPAIRS nonoverlapping [(a,512); (word_sub stackpointer (word 64),64)] - [(word pc,0x504); (z_12345,160); (z_67,768)] /\ + [(word pc,LENGTH mlkem_ntt_mc); (z_12345,160); (z_67,768)] /\ nonoverlapping (a,512) (word_sub stackpointer (word 64),64) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\ @@ -488,6 +516,7 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,512); memory :> bytes(word_sub stackpointer (word 64),64)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = REWRITE_CONV[ntt_constants] THENC ONCE_DEPTH_CONV let_CONV THENC @@ -497,5 +526,5 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove REWRITE_TAC[fst MLKEM_NTT_EXEC] THEN CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) MLKEM_NTT_EXEC - (REWRITE_RULE[fst MLKEM_NTT_EXEC] (CONV_RULE TWEAK_CONV MLKEM_NTT_CORRECT)) + (REWRITE_RULE[fst MLKEM_NTT_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTT_CORRECT))) `[D8; D9; D10; D11; D12; D13; D14; D15]` 64);; diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml index 5ec7a1ecb..eea50e0bc 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml @@ -217,6 +217,17 @@ let basemul2_odd = define let poly_basemul_acc_montgomery_cached_k2_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k2_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC = + REWRITE_CONV[poly_basemul_acc_montgomery_cached_k2_mc] `LENGTH poly_basemul_acc_montgomery_cached_k2_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC];; + (* ------------------------------------------------------------------------- *) (* Hacky tweaking conversion to write away non-free state component reads. *) (* ------------------------------------------------------------------------- *) @@ -314,6 +325,7 @@ let poly_basemul_acc_montgomery_cached_k2_GOAL = `forall srcA srcB srcBt dst x0 (* ------------------------------------------------------------------------- *) let poly_basemul_acc_montgomery_cached_k2_SPEC = prove(poly_basemul_acc_montgomery_cached_k2_GOAL, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; MODIFIABLE_SIMD_REGS; NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k2_EXEC] THEN diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml index 63b95e9eb..7e4a82fb7 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml @@ -277,6 +277,17 @@ let basemul3_odd = define let poly_basemul_acc_montgomery_cached_k3_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k3_mc;; + (* ------------------------------------------------------------------------- *) + (* Code length constants *) + (* ------------------------------------------------------------------------- *) + + let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC = + REWRITE_CONV[poly_basemul_acc_montgomery_cached_k3_mc] `LENGTH poly_basemul_acc_montgomery_cached_k3_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + + let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC];; + (* ------------------------------------------------------------------------- *) (* Hacky tweaking conversion to write away non-free state component reads. *) (* ------------------------------------------------------------------------- *) @@ -378,6 +389,7 @@ let basemul3_odd = define (* ------------------------------------------------------------------------- *) let poly_basemul_acc_montgomery_cached_k3_SPEC = prove (poly_basemul_acc_montgomery_cached_k3_GOAL, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; MODIFIABLE_SIMD_REGS; NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k3_EXEC] THEN diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml index b3a80e0ea..39b7086fa 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml @@ -336,6 +336,16 @@ let basemul4_odd = define let poly_basemul_acc_montgomery_cached_k4_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k4_mc;; + (* ------------------------------------------------------------------------- *) + (* Code length constants *) + (* ------------------------------------------------------------------------- *) + + let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC = + REWRITE_CONV[poly_basemul_acc_montgomery_cached_k4_mc] `LENGTH poly_basemul_acc_montgomery_cached_k4_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + + let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC];; (* ------------------------------------------------------------------------- *) (* Hacky tweaking conversion to write away non-free state component reads. *) @@ -444,6 +454,7 @@ let basemul4_odd = define (* ------------------------------------------------------------------------- *) let poly_basemul_acc_montgomery_cached_k4_SPEC = prove(poly_basemul_acc_montgomery_cached_k4_GOAL, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; MODIFIABLE_SIMD_REGS; NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k4_EXEC] THEN diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml b/proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml index 0afdd1aa9..94d7e42bd 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml @@ -49,6 +49,17 @@ let poly_mulcache_compute_mc = define_assert_from_elf let poly_mulcache_compute_EXEC = ARM_MK_EXEC_RULE poly_mulcache_compute_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_POLY_MULCACHE_COMPUTE_MC = + REWRITE_CONV[poly_mulcache_compute_mc] `LENGTH poly_mulcache_compute_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_POLY_MULCACHE_COMPUTE_MC];; + (* ------------------------------------------------------------------------- *) (* Specification *) (* ------------------------------------------------------------------------- *) @@ -97,6 +108,7 @@ let poly_mulcache_compute_GOAL = `forall pc src dst zetas zetas_twisted x y retu (* ------------------------------------------------------------------------- *) let poly_mulcache_compute_SPEC = prove(poly_mulcache_compute_GOAL, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_mulcache_compute_EXEC; have_mulcache_zetas] THEN diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml b/proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml index 684e8fa7e..d782f6c03 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml @@ -97,6 +97,32 @@ let mlkem_poly_reduce_mc = define_assert_from_elf let MLKEM_POLY_REDUCE_EXEC = ARM_MK_EXEC_RULE mlkem_poly_reduce_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_MLKEM_POLY_REDUCE_MC = + REWRITE_CONV[mlkem_poly_reduce_mc] `LENGTH mlkem_poly_reduce_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let MLKEM_POLY_REDUCE_PREAMBLE_LENGTH = new_definition + `MLKEM_POLY_REDUCE_PREAMBLE_LENGTH = 0`;; + +let MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH = new_definition + `MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH = 4`;; + +let MLKEM_POLY_REDUCE_CORE_START = new_definition + `MLKEM_POLY_REDUCE_CORE_START = MLKEM_POLY_REDUCE_PREAMBLE_LENGTH`;; + +let MLKEM_POLY_REDUCE_CORE_END = new_definition + `MLKEM_POLY_REDUCE_CORE_END = LENGTH mlkem_poly_reduce_mc - MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_MLKEM_POLY_REDUCE_MC; + MLKEM_POLY_REDUCE_CORE_START; MLKEM_POLY_REDUCE_CORE_END; + MLKEM_POLY_REDUCE_PREAMBLE_LENGTH; MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0] ;; + (* ------------------------------------------------------------------------- *) (* Some lemmas, tactics etc. *) (* ------------------------------------------------------------------------- *) @@ -122,21 +148,22 @@ let overall_lemma = prove let MLKEM_POLY_REDUCE_CORRECT = prove (`!a x pc. - nonoverlapping (word pc,0x124) (a,512) + nonoverlapping (word pc,LENGTH mlkem_poly_reduce_mc) (a,512) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_poly_reduce_mc /\ - read PC s = word pc /\ + read PC s = word (pc + MLKEM_POLY_REDUCE_CORE_START) /\ C_ARGUMENTS [a] s /\ !i. i < 256 ==> read(memory :> bytes16(word_add a (word(2 * i)))) s = x i) - (\s. read PC s = word(pc + 0x120) /\ + (\s. read PC s = word(pc + MLKEM_POLY_REDUCE_CORE_END) /\ !i. i < 256 ==> ival(read(memory :> bytes16 (word_add a (word(2 * i)))) s) = ival(x i) rem &3329) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,512)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`a:int64`; `x:num->int16`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES] THEN @@ -187,7 +214,7 @@ let MLKEM_POLY_REDUCE_CORRECT = prove let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove (`!a x pc returnaddress. - nonoverlapping (word pc,0x124) (a,512) + nonoverlapping (word pc,LENGTH mlkem_poly_reduce_mc) (a,512) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_poly_reduce_mc /\ read PC s = word pc /\ @@ -203,10 +230,12 @@ let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove ival(x i) rem &3329) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,512)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN let TWEAK_CONV = ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC ONCE_DEPTH_CONV NUM_MULT_CONV THENC - PURE_REWRITE_CONV [WORD_ADD_0] in + PURE_REWRITE_CONV [WORD_ADD_0] + in CONV_TAC TWEAK_CONV THEN ARM_ADD_RETURN_NOSTACK_TAC MLKEM_POLY_REDUCE_EXEC - (CONV_RULE TWEAK_CONV MLKEM_POLY_REDUCE_CORRECT));; + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_REDUCE_CORRECT)));; diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml b/proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml index 7cbeac8d9..244498f67 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml @@ -110,6 +110,32 @@ let mlkem_poly_tobytes_mc = define_assert_from_elf let MLKEM_POLY_TOBYTES_EXEC = ARM_MK_EXEC_RULE mlkem_poly_tobytes_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_MLKEM_POLY_TOBYTES_MC = + REWRITE_CONV[mlkem_poly_tobytes_mc] `LENGTH mlkem_poly_tobytes_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let MLKEM_POLY_TOBYTES_PREAMBLE_LENGTH = new_definition + `MLKEM_POLY_TOBYTES_PREAMBLE_LENGTH = 0`;; + +let MLKEM_POLY_TOBYTES_POSTAMBLE_LENGTH = new_definition + `MLKEM_POLY_TOBYTES_POSTAMBLE_LENGTH = 4`;; + +let MLKEM_POLY_TOBYTES_CORE_START = new_definition + `MLKEM_POLY_TOBYTES_CORE_START = MLKEM_POLY_TOBYTES_PREAMBLE_LENGTH`;; + +let MLKEM_POLY_TOBYTES_CORE_END = new_definition + `MLKEM_POLY_TOBYTES_CORE_END = LENGTH mlkem_poly_tobytes_mc - MLKEM_POLY_TOBYTES_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_MLKEM_POLY_TOBYTES_MC; + MLKEM_POLY_TOBYTES_CORE_START; MLKEM_POLY_TOBYTES_CORE_END; + MLKEM_POLY_TOBYTES_PREAMBLE_LENGTH; MLKEM_POLY_TOBYTES_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + (* ------------------------------------------------------------------------- *) (* A construct handy to expand out some lists explicitly. The conversion *) (* is a bit stupid (quadratic) but good enough for this application. *) @@ -172,18 +198,19 @@ let lemma = let MLKEM_POLY_TOBYTES_CORRECT = prove (`!r a (l:int16 list) pc. - ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)] + ALL (nonoverlapping (r,384)) [(word pc,LENGTH mlkem_poly_tobytes_mc); (a,512)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_poly_tobytes_mc /\ - read PC s = word pc /\ + read PC s = word (pc + MLKEM_POLY_TOBYTES_CORE_START) /\ C_ARGUMENTS [r;a] s /\ read (memory :> bytes(a,512)) s = num_of_wordlist l) - (\s. read PC s = word(pc + 0x154) /\ + (\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))) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(r,384)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`r:int64`; `a:int64`; `l:int16 list`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL] THEN @@ -251,7 +278,7 @@ let MLKEM_POLY_TOBYTES_CORRECT = prove let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove (`!r a (l:int16 list) pc returnaddress. - ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)] + ALL (nonoverlapping (r,384)) [(word pc,LENGTH mlkem_poly_tobytes_mc); (a,512)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_poly_tobytes_mc /\ read PC s = word pc /\ @@ -264,5 +291,6 @@ let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove 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 ARM_ADD_RETURN_NOSTACK_TAC MLKEM_POLY_TOBYTES_EXEC - MLKEM_POLY_TOBYTES_CORRECT);; + (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_TOBYTES_CORRECT));; diff --git a/proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml b/proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml index 0b514a47b..bffe6a777 100644 --- a/proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml +++ b/proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml @@ -73,6 +73,17 @@ let poly_tomont_asm_mc = define_assert_from_elf let POLY_TOMONT_EXEC = ARM_MK_EXEC_RULE poly_tomont_asm_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_POLY_TOMONT_ASM_MC = + REWRITE_CONV[poly_tomont_asm_mc] `LENGTH poly_tomont_asm_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_POLY_TOMONT_ASM_MC];; + (* ------------------------------------------------------------------------- *) (* Specification *) (* ------------------------------------------------------------------------- *) @@ -113,6 +124,7 @@ let POLY_TOMONT_GOAL = `forall pc ptr x returnaddress. (* ------------------------------------------------------------------------- *) let POLY_TOMONT_SPEC = prove(POLY_TOMONT_GOAL, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; NONOVERLAPPING_CLAUSES; C_ARGUMENTS; fst POLY_TOMONT_EXEC] THEN REPEAT STRIP_TAC THEN diff --git a/proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml b/proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml index e4135ff51..595f54c31 100644 --- a/proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml +++ b/proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml @@ -175,6 +175,32 @@ let mlkem_rej_uniform_mc = define_assert_from_elf let MLKEM_REJ_UNIFORM_EXEC = ARM_MK_EXEC_RULE mlkem_rej_uniform_mc;; +(* ------------------------------------------------------------------------- *) +(* Code length constants *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_MLKEM_REJ_UNIFORM_MC = + REWRITE_CONV[mlkem_rej_uniform_mc] `LENGTH mlkem_rej_uniform_mc` + |> CONV_RULE (RAND_CONV LENGTH_CONV);; + +let MLKEM_REJ_UNIFORM_PREAMBLE_LENGTH = new_definition + `MLKEM_REJ_UNIFORM_PREAMBLE_LENGTH = 4`;; + +let MLKEM_REJ_UNIFORM_POSTAMBLE_LENGTH = new_definition + `MLKEM_REJ_UNIFORM_POSTAMBLE_LENGTH = 8`;; + +let MLKEM_REJ_UNIFORM_CORE_START = new_definition + `MLKEM_REJ_UNIFORM_CORE_START = MLKEM_REJ_UNIFORM_PREAMBLE_LENGTH`;; + +let MLKEM_REJ_UNIFORM_CORE_END = new_definition + `MLKEM_REJ_UNIFORM_CORE_END = LENGTH mlkem_rej_uniform_mc - MLKEM_REJ_UNIFORM_POSTAMBLE_LENGTH`;; + +let LENGTH_SIMPLIFY_CONV = + REWRITE_CONV[LENGTH_MLKEM_REJ_UNIFORM_MC; + MLKEM_REJ_UNIFORM_CORE_START; MLKEM_REJ_UNIFORM_CORE_END; + MLKEM_REJ_UNIFORM_PREAMBLE_LENGTH; MLKEM_REJ_UNIFORM_POSTAMBLE_LENGTH] THENC + NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; + (* ------------------------------------------------------------------------- *) (* This is a general concept that subsumes a lot of specific cases like *) (* num_of_bytelist and bignum_of_wordlist - should standardize a bit. *) @@ -462,19 +488,19 @@ let MLKEM_REJ_UNIFORM_CORRECT = prove 24 divides val buflen /\ 8 * val buflen = 12 * LENGTH inlist /\ ALL (nonoverlapping (stackpointer,576)) - [(word pc,0x258); (buf,val buflen); (table,4096)] /\ + [(word pc,LENGTH mlkem_rej_uniform_mc); (buf,val buflen); (table,4096)] /\ ALL (nonoverlapping (res,512)) - [(word pc,0x258); (stackpointer,576)] + [(word pc,LENGTH mlkem_rej_uniform_mc); (stackpointer,576)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_rej_uniform_mc /\ - read PC s = word(pc + 0x4) /\ + read PC s = word(pc + MLKEM_REJ_UNIFORM_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [res;buf;buflen;table] s /\ read(memory :> bytes(table,4096)) s = num_of_wordlist mlkem_rej_uniform_table /\ read(memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist) - (\s. read PC s = word(pc + 0x250) /\ + (\s. read PC s = word(pc + MLKEM_REJ_UNIFORM_CORE_END) /\ let outlist = SUB_LIST(0,256) (REJ_SAMPLE inlist) in let outlen = LENGTH outlist in C_RETURN s = word outlen /\ @@ -483,6 +509,7 @@ let MLKEM_REJ_UNIFORM_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(res,512); memory :> bytes(stackpointer,576)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`res:int64`; `buf:int64`] THEN W64_GEN_TAC `buflen:num` THEN MAP_EVERY X_GEN_TAC @@ -1611,9 +1638,9 @@ let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove 24 divides val buflen /\ 8 * val buflen = 12 * LENGTH inlist /\ ALL (nonoverlapping (word_sub stackpointer (word 576),576)) - [(word pc,0x258); (buf,val buflen); (table,4096)] /\ + [(word pc,LENGTH mlkem_rej_uniform_mc); (buf,val buflen); (table,4096)] /\ ALL (nonoverlapping (res,512)) - [(word pc,0x258); (word_sub stackpointer (word 576),576)] + [(word pc,LENGTH mlkem_rej_uniform_mc); (word_sub stackpointer (word 576),576)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) mlkem_rej_uniform_mc /\ read PC s = word pc /\ @@ -1633,7 +1660,8 @@ let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(res,512); memory :> bytes(word_sub stackpointer (word 576),576)])`, + CONV_TAC LENGTH_SIMPLIFY_CONV THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ARM_ADD_RETURN_STACK_TAC MLKEM_REJ_UNIFORM_EXEC - (CONV_RULE (TOP_DEPTH_CONV let_CONV) MLKEM_REJ_UNIFORM_CORRECT) + (CONV_RULE (TOP_DEPTH_CONV let_CONV) (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_REJ_UNIFORM_CORRECT)) `[]:int64 list` 576);;