From 1f85a2a8b26d4c6cd4cebdeaae284482d6b1cab5 Mon Sep 17 00:00:00 2001 From: Andreas Hatziiliou Date: Fri, 10 Jul 2026 11:29:50 -0400 Subject: [PATCH 1/2] testing: HOL-Light: add support for cross-proofing This commit introduces a new flag --arch to the hol_light command of the tests script that allows user specification of which architecture to run/list the proofs for. If not passed, the behavior is unchanged. Signed-off-by: Andreas Hatziiliou --- scripts/tests | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/scripts/tests b/scripts/tests index 59a512acb0..45c3cfe12d 100755 --- a/scripts/tests +++ b/scripts/tests @@ -1086,7 +1086,9 @@ class Tests: def hol_light(self): machine = platform.machine().lower() - if machine in ["arm64", "aarch64"]: + if self.args.arch: + arch = self.args.arch + elif machine in ["arm64", "aarch64"]: arch = "aarch64" elif machine in ["x86_64"]: arch = "x86_64" @@ -1592,6 +1594,14 @@ def cli(): default=False, ) + hol_light_parser.add_argument( + "-a", + "--arch", + help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).", + choices=["aarch64", "x86_64"], + default=None, + ) + # func arguments func_parser = cmd_subparsers.add_parser( "func", From fc5bb9d88451a2a4abd997f86e407a1abec5b338 Mon Sep 17 00:00:00 2001 From: Andreas Hatziiliou Date: Sun, 16 Aug 2026 19:03:53 -0400 Subject: [PATCH 2/2] lint: verify that all expected theorems are present We add a check to the linting script called check-theorems that ensures that all HOL-Light proofs provide the expected set of theorems depending on the architecture. Unlike the ML-KEM theorem lister, the ML-DSA list_thms scripts scan complete top-level let bindings instead of only direct let NAME = prove lines. Several ML-DSA x86_64 safety theorems are wrapped in REWRITE_RULE around time prove, and the eta rejection-sampling subroutine theorems are built via local prove blocks or ADD_IBT_RULE aliases. The broader scan keeps those exported theorem names visible to lint without changing the proof structure. Signed-off-by: Andreas Hatziiliou --- proofs/hol_light/aarch64/list_thms.sh | 34 +++++++++ ..._f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml | 64 ++++++++-------- ...0_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml | 62 ++++++++-------- .../mldsa_pointwise_montgomery_aarch64_asm.ml | 24 +++--- .../mldsa_poly_decompose_32_aarch64_asm.ml | 52 ++++++------- .../mldsa_poly_decompose_88_aarch64_asm.ml | 52 ++++++------- .../mldsa_poly_use_hint_32_aarch64_asm.ml | 28 +++---- .../mldsa_poly_use_hint_88_aarch64_asm.ml | 28 +++---- ...pointwise_acc_montgomery_l4_aarch64_asm.ml | 26 +++---- ...pointwise_acc_montgomery_l5_aarch64_asm.ml | 26 +++---- ...pointwise_acc_montgomery_l7_aarch64_asm.ml | 26 +++---- proofs/hol_light/x86_64/list_thms.sh | 34 +++++++++ .../x86_64/proofs/keccak_f1600_x4_avx2_asm.ml | 74 +++++++++---------- .../proofs/mldsa_poly_caddq_avx2_asm.ml | 34 ++++----- .../mldsa_poly_decompose_32_avx2_asm.ml | 32 ++++---- .../mldsa_poly_decompose_88_avx2_asm.ml | 32 ++++---- .../proofs/mldsa_poly_use_hint_32_avx2_asm.ml | 46 ++++++------ .../proofs/mldsa_poly_use_hint_88_avx2_asm.ml | 46 ++++++------ scripts/lint | 74 +++++++++++++++++++ 19 files changed, 468 insertions(+), 326 deletions(-) create mode 100755 proofs/hol_light/aarch64/list_thms.sh create mode 100755 proofs/hol_light/x86_64/list_thms.sh diff --git a/proofs/hol_light/aarch64/list_thms.sh b/proofs/hol_light/aarch64/list_thms.sh new file mode 100755 index 0000000000..99f459c2ae --- /dev/null +++ b/proofs/hol_light/aarch64/list_thms.sh @@ -0,0 +1,34 @@ +#!/usr/bin/env bash +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +# +# This tiny script lists HOL-Light theorem names declared as proofs. + +ROOT=$(git rev-parse --show-toplevel) +cd "$ROOT" || exit + +if [[ $# == 0 ]]; then + set -- proofs/hol_light/aarch64/proofs/*.ml +fi + +awk ' + function flush() { + if (name != "" && block ~ /(^|[[:space:](])(time[[:space:]]+)?prove($|[[:space:]]|`|\()|(^|[[:space:](])ADD_IBT_RULE([[:space:]]|\()/) { + print name + } + } + /^let[[:space:]]+[^[:space:]]+[[:space:]]*=/ { + flush() + name = $0 + sub(/^let[[:space:]]+/, "", name) + sub(/[[:space:]]*=.*/, "", name) + block = $0 + next + } + name != "" { + block = block "\n" $0 + } + END { + flush() + } +' "$@" diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml index dd31b01ec3..14ae71218c 100644 --- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml @@ -992,7 +992,7 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;; +let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;; (*** Additional lazy/deferred rotations in the implementation, row-major ***) @@ -1003,39 +1003,39 @@ 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;; +let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;; (* ------------------------------------------------------------------------- *) (* Code length constants *) (* ------------------------------------------------------------------------- *) -let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC = +let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_HYBRID_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_HYBRID_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_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_HYBRID_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_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_HYBRID_CORE_START = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_HYBRID_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 KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = new_definition + `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_HYBRID_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 + REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_SCALAR_HYBRID_MC; + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END; + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; (* ------------------------------------------------------------------------- *) (* Correctness proof *) (* ------------------------------------------------------------------------- *) -let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove +let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove (`!a rc A1 A2 A3 A4 pc stackpointer. aligned 16 stackpointer /\ nonoverlapping (a,800) (stackpointer,216) /\ @@ -1044,7 +1044,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove [(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 + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\ + read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A1 /\ @@ -1052,7 +1052,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 + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -1071,7 +1071,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove 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 - REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_EXEC] THEN + REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN @@ -1131,7 +1131,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove MEMORY_128_FROM_64_TAC "a" 0 12 THEN MEMORY_128_FROM_64_TAC "a" 200 12 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--443) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--443) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN @@ -1202,7 +1202,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM CONJ_ASSOC]; @@ -1240,7 +1240,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove X_GEN_TAC `i:num` THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN - ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN + ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN VAL_INT64_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV); @@ -1294,7 +1294,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--442) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--442) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN @@ -1369,7 +1369,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM CONJ_ASSOC]; @@ -1409,7 +1409,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove X_GEN_TAC `i:num` THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN - ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN + ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN VAL_INT64_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV); @@ -1433,7 +1433,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--83) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--83) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN @@ -1448,7 +1448,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove (* NOTE: This must be kept in sync with the CBMC specification * in mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h *) -let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove +let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove (`!a rc A1 A2 A3 A4 pc stackpointer returnaddress. aligned 16 stackpointer /\ nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\ @@ -1483,8 +1483,8 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove (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 (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT)) + ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; @@ -1498,10 +1498,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "sha3_keccak4_f1600" subroutine_signatures) - KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT - KECCAK_F1600_X4_V8A_SCALAR_EXEC;; + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC;; -let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove +let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a rc pc stackpointer returnaddress. aligned 16 stackpointer /\ @@ -1530,4 +1530,4 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove [a,800; word_sub stackpointer (word 224),224]) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml index 5139088334..d82ea57e44 100644 --- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml @@ -898,7 +898,7 @@ let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_v84a_scalar_mc;; +let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_v84a_scalar_mc;; (*** Additional lazy/deferred rotations in the implementation, row-major ***) @@ -914,33 +914,33 @@ let deferred_rotates = define (* Code length constants *) (* ------------------------------------------------------------------------- *) -let LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_MC = +let LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_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_HYBRID_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_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_HYBRID_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_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_HYBRID_CORE_START = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_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 KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END = new_definition + `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc - KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_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 + REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_MC; + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END; + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; (* ------------------------------------------------------------------------- *) (* Correctness proof *) (* ------------------------------------------------------------------------- *) -let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove +let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT = prove (`!a rc A1 A2 A3 A4 pc stackpointer. aligned 16 stackpointer /\ nonoverlapping (a,800) (stackpointer,216) /\ @@ -949,7 +949,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove [(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 + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START) /\ + read PC s = word (pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START) /\ read SP s = stackpointer /\ C_ARGUMENTS [a; rc] s /\ wordlist_from_memory(a,25) s = A1 /\ @@ -957,7 +957,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 + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END) /\ + (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END) /\ wordlist_from_memory(a,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A2 /\ @@ -976,7 +976,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove 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 - REWRITE_TAC[fst KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC] THEN + REWRITE_TAC[fst KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN @@ -1036,7 +1036,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove MEMORY_128_FROM_64_TAC "a" 0 12 THEN MEMORY_128_FROM_64_TAC "a" 200 12 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--396) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--396) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN @@ -1107,7 +1107,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--339) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--339) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM CONJ_ASSOC]; @@ -1145,7 +1145,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove X_GEN_TAC `i:num` THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN - ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC [1] THEN + ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC [1] THEN VAL_INT64_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV); @@ -1199,7 +1199,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--395) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--395) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN @@ -1274,7 +1274,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--339) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--339) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM CONJ_ASSOC]; @@ -1314,7 +1314,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove X_GEN_TAC `i:num` THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN - ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC [1] THEN + ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC [1] THEN VAL_INT64_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV); @@ -1338,7 +1338,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN REWRITE_TAC[GSYM round_constants] THEN ENSURES_INIT_TAC "s0" THEN - ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--83) THEN + ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--83) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN @@ -1353,7 +1353,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove (* NOTE: This must be kept in sync with the CBMC specification * in mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h *) -let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove +let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove (`!a rc A1 A2 A3 A4 pc stackpointer returnaddress. aligned 16 stackpointer /\ nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\ @@ -1388,8 +1388,8 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove (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 (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT)) + ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC + (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT)) `[D8; D9; D10; D11; D12; D13; D14; D15; X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);; @@ -1403,10 +1403,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "sha3_keccak4_f1600_alt" subroutine_signatures) - KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT - KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC;; + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_CORRECT + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC;; -let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_SAFE = time prove +let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a rc pc stackpointer returnaddress. aligned 16 stackpointer /\ @@ -1435,4 +1435,4 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_SAFE = time prove [a,800; word_sub stackpointer (word 224),224]) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_pointwise_montgomery_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_pointwise_montgomery_aarch64_asm.ml index 0e6e799f62..37199f338a 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_pointwise_montgomery_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_pointwise_montgomery_aarch64_asm.ml @@ -72,13 +72,13 @@ let mldsa_pointwise_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let MLDSA_POINTWISE_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_mc;; +let MLDSA_POINTWISE_MONTGOMERY_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_mc;; (* ========================================================================= *) (* Correctness proof *) (* ========================================================================= *) -let MLDSA_POINTWISE_CORRECT = prove +let MLDSA_POINTWISE_MONTGOMERY_CORRECT = prove (`!a b x y pc. nonoverlapping (word pc, LENGTH mldsa_pointwise_mc) (a, 1024) /\ nonoverlapping (a, 1024) (b, 1024) @@ -107,7 +107,7 @@ let MLDSA_POINTWISE_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst MLDSA_POINTWISE_EXEC] THEN + fst MLDSA_POINTWISE_MONTGOMERY_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV))) THEN @@ -126,7 +126,7 @@ let MLDSA_POINTWISE_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate all 679 instructions with SIMD simplification *) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POINTWISE_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POINTWISE_MONTGOMERY_EXEC [n] THEN SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) (1--679) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -209,7 +209,7 @@ let MLDSA_POINTWISE_CORRECT = prove (* Subroutine form *) (* ========================================================================= *) -let MLDSA_POINTWISE_SUBROUTINE_CORRECT = prove +let MLDSA_POINTWISE_MONTGOMERY_SUBROUTINE_CORRECT = prove (`!a b x y pc returnaddress. nonoverlapping (word pc, LENGTH mldsa_pointwise_mc) (a, 1024) /\ nonoverlapping (a, 1024) (b, 1024) @@ -232,9 +232,9 @@ let MLDSA_POINTWISE_SUBROUTINE_CORRECT = prove abs(ival zi) <= &8380416)) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - REWRITE_TAC[fst MLDSA_POINTWISE_EXEC] THEN - ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POINTWISE_EXEC - (REWRITE_RULE[fst MLDSA_POINTWISE_EXEC] MLDSA_POINTWISE_CORRECT));; + REWRITE_TAC[fst MLDSA_POINTWISE_MONTGOMERY_EXEC] THEN + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POINTWISE_MONTGOMERY_EXEC + (REWRITE_RULE[fst MLDSA_POINTWISE_MONTGOMERY_EXEC] MLDSA_POINTWISE_MONTGOMERY_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -246,10 +246,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "mldsa_pointwise" subroutine_signatures) - MLDSA_POINTWISE_SUBROUTINE_CORRECT - MLDSA_POINTWISE_EXEC;; + MLDSA_POINTWISE_MONTGOMERY_SUBROUTINE_CORRECT + MLDSA_POINTWISE_MONTGOMERY_EXEC;; -let MLDSA_POINTWISE_SUBROUTINE_SAFE = time prove +let MLDSA_POINTWISE_MONTGOMERY_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a b pc returnaddress. nonoverlapping (word pc,LENGTH mldsa_pointwise_mc) (a,1024) /\ @@ -271,4 +271,4 @@ let MLDSA_POINTWISE_SUBROUTINE_SAFE = time prove [a,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POINTWISE_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POINTWISE_MONTGOMERY_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_32_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_32_aarch64_asm.ml index 1bf7efbe48..7a1d3266dc 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_32_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_32_aarch64_asm.ml @@ -74,30 +74,30 @@ let poly_decompose_32_aarch64_asm_mc = define_assert_from_elf "poly_decompose_32 ];; (*** BYTECODE END ***) -let POLY_DECOMPOSE_32_AARCH64_ASM_EXEC = ARM_MK_EXEC_RULE poly_decompose_32_aarch64_asm_mc;; +let MLDSA_POLY_DECOMPOSE_32_EXEC = ARM_MK_EXEC_RULE poly_decompose_32_aarch64_asm_mc;; (* ========================================================================= *) (* Constants *) (* ========================================================================= *) -let LENGTH_POLY_DECOMPOSE_32_AARCH64_ASM_MC = +let LENGTH_MLDSA_POLY_DECOMPOSE_32_MC = REWRITE_CONV[poly_decompose_32_aarch64_asm_mc] `LENGTH poly_decompose_32_aarch64_asm_mc` |> CONV_RULE (RAND_CONV LENGTH_CONV);; -let POLY_DECOMPOSE_32_AARCH64_ASM_CORE_START = new_definition - `POLY_DECOMPOSE_32_AARCH64_ASM_CORE_START = 0`;; +let MLDSA_POLY_DECOMPOSE_32_CORE_START = new_definition + `MLDSA_POLY_DECOMPOSE_32_CORE_START = 0`;; -let POLY_DECOMPOSE_32_AARCH64_ASM_POSTAMBLE_LENGTH = new_definition - `POLY_DECOMPOSE_32_AARCH64_ASM_POSTAMBLE_LENGTH = 4`;; +let MLDSA_POLY_DECOMPOSE_32_POSTAMBLE_LENGTH = new_definition + `MLDSA_POLY_DECOMPOSE_32_POSTAMBLE_LENGTH = 4`;; -let POLY_DECOMPOSE_32_AARCH64_ASM_CORE_END = new_definition - `POLY_DECOMPOSE_32_AARCH64_ASM_CORE_END = - LENGTH poly_decompose_32_aarch64_asm_mc - POLY_DECOMPOSE_32_AARCH64_ASM_POSTAMBLE_LENGTH`;; +let MLDSA_POLY_DECOMPOSE_32_CORE_END = new_definition + `MLDSA_POLY_DECOMPOSE_32_CORE_END = + LENGTH poly_decompose_32_aarch64_asm_mc - MLDSA_POLY_DECOMPOSE_32_POSTAMBLE_LENGTH`;; let LENGTH_SIMPLIFY_CONV = - REWRITE_CONV[LENGTH_POLY_DECOMPOSE_32_AARCH64_ASM_MC; - POLY_DECOMPOSE_32_AARCH64_ASM_CORE_START; POLY_DECOMPOSE_32_AARCH64_ASM_CORE_END; - POLY_DECOMPOSE_32_AARCH64_ASM_POSTAMBLE_LENGTH] THENC + REWRITE_CONV[LENGTH_MLDSA_POLY_DECOMPOSE_32_MC; + MLDSA_POLY_DECOMPOSE_32_CORE_START; MLDSA_POLY_DECOMPOSE_32_CORE_END; + MLDSA_POLY_DECOMPOSE_32_POSTAMBLE_LENGTH] THENC NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; (* ========================================================================= *) @@ -466,7 +466,7 @@ let DECOMPOSE32_A0_CORRECT = prove( (* Specification *) (* ========================================================================= *) -let POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_32_CORRECT = prove( `!pc a r1 x. nonoverlapping (word pc, LENGTH poly_decompose_32_aarch64_asm_mc) (r1, 1024) /\ @@ -475,12 +475,12 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT = prove( nonoverlapping (r1, 1024) (a, 1024) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) poly_decompose_32_aarch64_asm_mc /\ - read PC s = word(pc + POLY_DECOMPOSE_32_AARCH64_ASM_CORE_START) /\ + read PC s = word(pc + MLDSA_POLY_DECOMPOSE_32_CORE_START) /\ C_ARGUMENTS [r1; a] s /\ (!i. i < 256 ==> read(memory :> bytes32(word_add a (word(4 * i)))) s = x i)) - (\s. read PC s = word(pc + POLY_DECOMPOSE_32_AARCH64_ASM_CORE_END) /\ + (\s. read PC s = word(pc + MLDSA_POLY_DECOMPOSE_32_CORE_END) /\ ((!i. i < 256 ==> val(x i:int32) < 8380417) ==> (!i. i < 256 ==> val(read(memory :> bytes32 @@ -497,7 +497,7 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT = prove( CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`pc:num`; `a:int64`; `r1:int64`; `x:num->int32`] THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; - fst POLY_DECOMPOSE_32_AARCH64_ASM_EXEC; + fst MLDSA_POLY_DECOMPOSE_32_EXEC; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN STRIP_TAC THEN @@ -520,7 +520,7 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT = prove( (* Symbolic execution with folding to decompose32_a1/a0 *) MAP_UNTIL_TARGET_PC (fun n -> - ARM_STEPS_TAC POLY_DECOMPOSE_32_AARCH64_ASM_EXEC [n] THEN + ARM_STEPS_TAC MLDSA_POLY_DECOMPOSE_32_EXEC [n] THEN RULE_ASSUM_TAC(CONV_RULE( TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV THENC ONCE_REWRITE_CONV [GSYM h32] THENC @@ -560,7 +560,7 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT = prove( (* Subroutine form: wraps CORRECT with RET handling *) (* ========================================================================= *) -let POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_32_SUBROUTINE_CORRECT = prove( `!pc a r1 x returnaddress. nonoverlapping (word pc, LENGTH poly_decompose_32_aarch64_asm_mc) (r1, 1024) /\ @@ -599,7 +599,7 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(a, 1024)])`, CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; - fst POLY_DECOMPOSE_32_AARCH64_ASM_EXEC; + fst MLDSA_POLY_DECOMPOSE_32_EXEC; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN REPEAT STRIP_TAC THEN REWRITE_TAC(!simulation_precanon_thms) THEN @@ -607,10 +607,10 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove( MP_TAC(REWRITE_RULE[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] (SPECL [`pc:num`; `a:int64`; `r1:int64`; `x:num->int32`] - (CONV_RULE LENGTH_SIMPLIFY_CONV POLY_DECOMPOSE_32_AARCH64_ASM_CORRECT))) THEN + (CONV_RULE LENGTH_SIMPLIFY_CONV MLDSA_POLY_DECOMPOSE_32_CORRECT))) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN - ARM_BIGSTEP_TAC POLY_DECOMPOSE_32_AARCH64_ASM_EXEC "s1" THEN - ARM_STEPS_TAC POLY_DECOMPOSE_32_AARCH64_ASM_EXEC [2] THEN + ARM_BIGSTEP_TAC MLDSA_POLY_DECOMPOSE_32_EXEC "s1" THEN + ARM_STEPS_TAC MLDSA_POLY_DECOMPOSE_32_EXEC [2] THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o C MATCH_MP @@ -634,10 +634,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "poly_decompose_32_aarch64_asm" subroutine_signatures) - POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_CORRECT - POLY_DECOMPOSE_32_AARCH64_ASM_EXEC;; + MLDSA_POLY_DECOMPOSE_32_SUBROUTINE_CORRECT + MLDSA_POLY_DECOMPOSE_32_EXEC;; -let POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_32_SUBROUTINE_SAFE = time prove (`exists f_events. forall e pc a r1 returnaddress. nonoverlapping (word pc,LENGTH poly_decompose_32_aarch64_asm_mc) (r1,1024) /\ @@ -660,4 +660,4 @@ let POLY_DECOMPOSE_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove [r1,1024; a,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_DECOMPOSE_32_AARCH64_ASM_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLY_DECOMPOSE_32_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_88_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_88_aarch64_asm.ml index 4ebbe9d918..e7bd332949 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_88_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_poly_decompose_88_aarch64_asm.ml @@ -74,30 +74,30 @@ let poly_decompose_88_aarch64_asm_mc = define_assert_from_elf "poly_decompose_88 ];; (*** BYTECODE END ***) -let POLY_DECOMPOSE_88_AARCH64_ASM_EXEC = ARM_MK_EXEC_RULE poly_decompose_88_aarch64_asm_mc;; +let MLDSA_POLY_DECOMPOSE_88_EXEC = ARM_MK_EXEC_RULE poly_decompose_88_aarch64_asm_mc;; (* ========================================================================= *) (* Constants *) (* ========================================================================= *) -let LENGTH_POLY_DECOMPOSE_88_AARCH64_ASM_MC = +let LENGTH_MLDSA_POLY_DECOMPOSE_88_MC = REWRITE_CONV[poly_decompose_88_aarch64_asm_mc] `LENGTH poly_decompose_88_aarch64_asm_mc` |> CONV_RULE (RAND_CONV LENGTH_CONV);; -let POLY_DECOMPOSE_88_AARCH64_ASM_CORE_START = new_definition - `POLY_DECOMPOSE_88_AARCH64_ASM_CORE_START = 0`;; +let MLDSA_POLY_DECOMPOSE_88_CORE_START = new_definition + `MLDSA_POLY_DECOMPOSE_88_CORE_START = 0`;; -let POLY_DECOMPOSE_88_AARCH64_ASM_POSTAMBLE_LENGTH = new_definition - `POLY_DECOMPOSE_88_AARCH64_ASM_POSTAMBLE_LENGTH = 4`;; +let MLDSA_POLY_DECOMPOSE_88_POSTAMBLE_LENGTH = new_definition + `MLDSA_POLY_DECOMPOSE_88_POSTAMBLE_LENGTH = 4`;; -let POLY_DECOMPOSE_88_AARCH64_ASM_CORE_END = new_definition - `POLY_DECOMPOSE_88_AARCH64_ASM_CORE_END = - LENGTH poly_decompose_88_aarch64_asm_mc - POLY_DECOMPOSE_88_AARCH64_ASM_POSTAMBLE_LENGTH`;; +let MLDSA_POLY_DECOMPOSE_88_CORE_END = new_definition + `MLDSA_POLY_DECOMPOSE_88_CORE_END = + LENGTH poly_decompose_88_aarch64_asm_mc - MLDSA_POLY_DECOMPOSE_88_POSTAMBLE_LENGTH`;; let LENGTH_SIMPLIFY_CONV = - REWRITE_CONV[LENGTH_POLY_DECOMPOSE_88_AARCH64_ASM_MC; - POLY_DECOMPOSE_88_AARCH64_ASM_CORE_START; POLY_DECOMPOSE_88_AARCH64_ASM_CORE_END; - POLY_DECOMPOSE_88_AARCH64_ASM_POSTAMBLE_LENGTH] THENC + REWRITE_CONV[LENGTH_MLDSA_POLY_DECOMPOSE_88_MC; + MLDSA_POLY_DECOMPOSE_88_CORE_START; MLDSA_POLY_DECOMPOSE_88_CORE_END; + MLDSA_POLY_DECOMPOSE_88_POSTAMBLE_LENGTH] THENC NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; (* ========================================================================= *) @@ -466,7 +466,7 @@ let DECOMPOSE88_A0_CORRECT = prove( (* Specification *) (* ========================================================================= *) -let POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_88_CORRECT = prove( `!pc a r1 x. nonoverlapping (word pc, LENGTH poly_decompose_88_aarch64_asm_mc) (r1, 1024) /\ @@ -475,12 +475,12 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT = prove( nonoverlapping (r1, 1024) (a, 1024) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) poly_decompose_88_aarch64_asm_mc /\ - read PC s = word(pc + POLY_DECOMPOSE_88_AARCH64_ASM_CORE_START) /\ + read PC s = word(pc + MLDSA_POLY_DECOMPOSE_88_CORE_START) /\ C_ARGUMENTS [r1; a] s /\ (!i. i < 256 ==> read(memory :> bytes32(word_add a (word(4 * i)))) s = x i)) - (\s. read PC s = word(pc + POLY_DECOMPOSE_88_AARCH64_ASM_CORE_END) /\ + (\s. read PC s = word(pc + MLDSA_POLY_DECOMPOSE_88_CORE_END) /\ ((!i. i < 256 ==> val(x i:int32) < 8380417) ==> (!i. i < 256 ==> val(read(memory :> bytes32 @@ -497,7 +497,7 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT = prove( CONV_TAC LENGTH_SIMPLIFY_CONV THEN MAP_EVERY X_GEN_TAC [`pc:num`; `a:int64`; `r1:int64`; `x:num->int32`] THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; - fst POLY_DECOMPOSE_88_AARCH64_ASM_EXEC; + fst MLDSA_POLY_DECOMPOSE_88_EXEC; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN STRIP_TAC THEN @@ -520,7 +520,7 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT = prove( (* Symbolic execution with folding to decompose88_a1/a0 *) MAP_UNTIL_TARGET_PC (fun n -> - ARM_STEPS_TAC POLY_DECOMPOSE_88_AARCH64_ASM_EXEC [n] THEN + ARM_STEPS_TAC MLDSA_POLY_DECOMPOSE_88_EXEC [n] THEN RULE_ASSUM_TAC(CONV_RULE( TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV THENC ONCE_REWRITE_CONV [GSYM h88] THENC @@ -560,7 +560,7 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT = prove( (* Subroutine form: wraps CORRECT with RET handling *) (* ========================================================================= *) -let POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_88_SUBROUTINE_CORRECT = prove( `!pc a r1 x returnaddress. nonoverlapping (word pc, LENGTH poly_decompose_88_aarch64_asm_mc) (r1, 1024) /\ @@ -599,7 +599,7 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(a, 1024)])`, CONV_TAC LENGTH_SIMPLIFY_CONV THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; - fst POLY_DECOMPOSE_88_AARCH64_ASM_EXEC; + fst MLDSA_POLY_DECOMPOSE_88_EXEC; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN REPEAT STRIP_TAC THEN REWRITE_TAC(!simulation_precanon_thms) THEN @@ -607,10 +607,10 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove( MP_TAC(REWRITE_RULE[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; SOME_FLAGS; MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] (SPECL [`pc:num`; `a:int64`; `r1:int64`; `x:num->int32`] - (CONV_RULE LENGTH_SIMPLIFY_CONV POLY_DECOMPOSE_88_AARCH64_ASM_CORRECT))) THEN + (CONV_RULE LENGTH_SIMPLIFY_CONV MLDSA_POLY_DECOMPOSE_88_CORRECT))) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN - ARM_BIGSTEP_TAC POLY_DECOMPOSE_88_AARCH64_ASM_EXEC "s1" THEN - ARM_STEPS_TAC POLY_DECOMPOSE_88_AARCH64_ASM_EXEC [2] THEN + ARM_BIGSTEP_TAC MLDSA_POLY_DECOMPOSE_88_EXEC "s1" THEN + ARM_STEPS_TAC MLDSA_POLY_DECOMPOSE_88_EXEC [2] THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o C MATCH_MP @@ -635,10 +635,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "poly_decompose_88_aarch64_asm" subroutine_signatures) - POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_CORRECT - POLY_DECOMPOSE_88_AARCH64_ASM_EXEC;; + MLDSA_POLY_DECOMPOSE_88_SUBROUTINE_CORRECT + MLDSA_POLY_DECOMPOSE_88_EXEC;; -let POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_88_SUBROUTINE_SAFE = time prove (`exists f_events. forall e pc a r1 returnaddress. nonoverlapping (word pc,LENGTH poly_decompose_88_aarch64_asm_mc) (r1,1024) /\ @@ -661,4 +661,4 @@ let POLY_DECOMPOSE_88_AARCH64_ASM_SUBROUTINE_SAFE = time prove [r1,1024; a,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_DECOMPOSE_88_AARCH64_ASM_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLY_DECOMPOSE_88_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32_aarch64_asm.ml index eb0441b88a..35f931d5d0 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32_aarch64_asm.ml @@ -92,7 +92,7 @@ let poly_use_hint_32_aarch64_asm_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let POLY_USE_HINT_32_AARCH64_ASM_EXEC = ARM_MK_EXEC_RULE poly_use_hint_32_aarch64_asm_mc;; +let MLDSA_POLY_USE_HINT_32_EXEC = ARM_MK_EXEC_RULE poly_use_hint_32_aarch64_asm_mc;; (* Per-element word function matching the assembly computation *) let mldsa_use_hint_32_asm = new_definition @@ -707,7 +707,7 @@ let MLDSA_USE_HINT_32_EQUIV = prove( on val(x i) / val(y i) appear as antecedents inside the postcondition (decompose-style): the assembly executes regardless of input ranges, and only the FIPS-equivalence + output bound require the input bounds. *) -let POLY_USE_HINT_32_AARCH64_ASM_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_CORRECT = prove (`!a h x y pc. nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -736,7 +736,7 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] THEN + fst MLDSA_POLY_USE_HINT_32_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV))) THEN @@ -755,7 +755,7 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate 878 instructions (the assembly is bound-independent). *) - MAP_EVERY (fun n -> ARM_STEPS_TAC POLY_USE_HINT_32_AARCH64_ASM_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC [n] THEN SIMD_SIMPLIFY_TAC[]) (1--878) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -821,11 +821,11 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT = prove (* Public subroutine correctness (FIPS 204-aligned) *) (* ========================================================================= *) -(* Subroutine form: derives directly from POLY_USE_HINT_32_AARCH64_ASM_CORRECT +(* Subroutine form: derives directly from MLDSA_POLY_USE_HINT_32_CORRECT by adding the X30 -> RET return wiring via ARM_ADD_RETURN_NOSTACK_TAC. The bound antecedents inside the postcondition pass through unchanged (decompose pattern). *) -let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_SUBROUTINE_CORRECT = prove (`!a h x y pc returnaddress. nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -849,12 +849,12 @@ let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove (word_add a (word(4 * i)))) s) < 16))) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - REWRITE_TAC[fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] THEN + REWRITE_TAC[fst MLDSA_POLY_USE_HINT_32_EXEC] THEN CONV_TAC NUM_REDUCE_CONV THEN - ARM_ADD_RETURN_NOSTACK_TAC POLY_USE_HINT_32_AARCH64_ASM_EXEC + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POLY_USE_HINT_32_EXEC (CONV_RULE(ONCE_DEPTH_CONV NUM_REDUCE_CONV) - (REWRITE_RULE[fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] - POLY_USE_HINT_32_AARCH64_ASM_CORRECT)));; + (REWRITE_RULE[fst MLDSA_POLY_USE_HINT_32_EXEC] + MLDSA_POLY_USE_HINT_32_CORRECT)));; (* ========================================================================= *) @@ -868,10 +868,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "poly_use_hint_32_aarch64_asm" subroutine_signatures) - POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT - POLY_USE_HINT_32_AARCH64_ASM_EXEC;; + MLDSA_POLY_USE_HINT_32_SUBROUTINE_CORRECT + MLDSA_POLY_USE_HINT_32_EXEC;; -let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_32_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc returnaddress. nonoverlapping (word pc,LENGTH poly_use_hint_32_aarch64_asm_mc) (a,1024) /\ @@ -893,5 +893,5 @@ let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove [a,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_USE_HINT_32_AARCH64_ASM_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLY_USE_HINT_32_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88_aarch64_asm.ml index eacf9ca9ce..9283c5aa19 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88_aarch64_asm.ml @@ -100,7 +100,7 @@ let poly_use_hint_88_aarch64_asm_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let POLY_USE_HINT_88_AARCH64_ASM_EXEC = ARM_MK_EXEC_RULE poly_use_hint_88_aarch64_asm_mc;; +let MLDSA_POLY_USE_HINT_88_EXEC = ARM_MK_EXEC_RULE poly_use_hint_88_aarch64_asm_mc;; (* Per-element word function matching the assembly computation *) let mldsa_use_hint_88_asm = new_definition @@ -776,7 +776,7 @@ let MLDSA_USE_HINT_88_EQUIV = prove( on val(x i) / val(y i) appear as antecedents inside the postcondition (decompose-style): the assembly executes regardless of input ranges, and only the FIPS-equivalence + output bound require the input bounds. *) -let POLY_USE_HINT_88_AARCH64_ASM_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_CORRECT = prove (`!a h x y pc. nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -805,7 +805,7 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst POLY_USE_HINT_88_AARCH64_ASM_EXEC] THEN + fst MLDSA_POLY_USE_HINT_88_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV))) THEN @@ -824,7 +824,7 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate 1006 instructions (the assembly is bound-independent). *) - MAP_EVERY (fun n -> ARM_STEPS_TAC POLY_USE_HINT_88_AARCH64_ASM_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC [n] THEN SIMD_SIMPLIFY_TAC[]) (1--1006) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -893,11 +893,11 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT = prove (* Public subroutine correctness (FIPS 204-aligned) *) (* ========================================================================= *) -(* Subroutine form: derives directly from POLY_USE_HINT_88_AARCH64_ASM_CORRECT +(* Subroutine form: derives directly from MLDSA_POLY_USE_HINT_88_CORRECT by adding the X30 -> RET return wiring via ARM_ADD_RETURN_NOSTACK_TAC. The bound antecedents inside the postcondition pass through unchanged (decompose pattern). *) -let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_SUBROUTINE_CORRECT = prove (`!a h x y pc returnaddress. nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -921,12 +921,12 @@ let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove (word_add a (word(4 * i)))) s) < 44))) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - REWRITE_TAC[fst POLY_USE_HINT_88_AARCH64_ASM_EXEC] THEN + REWRITE_TAC[fst MLDSA_POLY_USE_HINT_88_EXEC] THEN CONV_TAC NUM_REDUCE_CONV THEN - ARM_ADD_RETURN_NOSTACK_TAC POLY_USE_HINT_88_AARCH64_ASM_EXEC + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POLY_USE_HINT_88_EXEC (CONV_RULE(ONCE_DEPTH_CONV NUM_REDUCE_CONV) - (REWRITE_RULE[fst POLY_USE_HINT_88_AARCH64_ASM_EXEC] - POLY_USE_HINT_88_AARCH64_ASM_CORRECT)));; + (REWRITE_RULE[fst MLDSA_POLY_USE_HINT_88_EXEC] + MLDSA_POLY_USE_HINT_88_CORRECT)));; (* ========================================================================= *) @@ -940,10 +940,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "poly_use_hint_88_aarch64_asm" subroutine_signatures) - POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT - POLY_USE_HINT_88_AARCH64_ASM_EXEC;; + MLDSA_POLY_USE_HINT_88_SUBROUTINE_CORRECT + MLDSA_POLY_USE_HINT_88_EXEC;; -let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_88_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc returnaddress. nonoverlapping (word pc,LENGTH poly_use_hint_88_aarch64_asm_mc) (a,1024) /\ @@ -965,4 +965,4 @@ let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_SAFE = time prove [a,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_USE_HINT_88_AARCH64_ASM_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLY_USE_HINT_88_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml index b7e69b48f3..54479c5bc0 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml @@ -120,13 +120,13 @@ let mldsa_pointwise_acc_l4_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let MLDSA_POINTWISE_ACC_L4_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l4_mc;; +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l4_mc;; (* ========================================================================= *) (* Correctness proof *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L4_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_CORRECT = prove (`!r a b x y pc. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l4_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l4_mc) (a, 4096) /\ @@ -159,7 +159,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst MLDSA_POINTWISE_ACC_L4_EXEC] THEN + fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN @@ -192,7 +192,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate all 1463 instructions with SIMD simplification *) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POINTWISE_ACC_L4_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC [n] THEN SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) (1--1447) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -289,7 +289,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove (* Subroutine form *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_SUBROUTINE_CORRECT = prove (`!r a b x y pc returnaddress. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l4_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l4_mc) (a, 4096) /\ @@ -316,10 +316,10 @@ let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_CORRECT = prove abs(ival zi) <= &8380416)) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(r, 1024)])`, - REWRITE_TAC[fst MLDSA_POINTWISE_ACC_L4_EXEC] THEN - ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POINTWISE_ACC_L4_EXEC - (REWRITE_RULE[fst MLDSA_POINTWISE_ACC_L4_EXEC] - MLDSA_POINTWISE_ACC_L4_CORRECT));; + REWRITE_TAC[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC] THEN + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC + (REWRITE_RULE[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC] + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -331,10 +331,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "mldsa_pointwise_acc_l4" subroutine_signatures) - MLDSA_POINTWISE_ACC_L4_SUBROUTINE_CORRECT - MLDSA_POINTWISE_ACC_L4_EXEC;; + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_SUBROUTINE_CORRECT + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC;; -let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_SAFE = time prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_SUBROUTINE_SAFE = time prove (`exists f_events. forall e r a b pc returnaddress. nonoverlapping (word pc,LENGTH mldsa_pointwise_acc_l4_mc) (r,1024) /\ @@ -360,4 +360,4 @@ let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_SAFE = time prove [r,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POINTWISE_ACC_L4_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml index 417fd2d9cc..5b403c999d 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml @@ -136,13 +136,13 @@ let mldsa_pointwise_acc_l5_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let MLDSA_POINTWISE_ACC_L5_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l5_mc;; +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l5_mc;; (* ========================================================================= *) (* Correctness proof *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L5_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_CORRECT = prove (`!r a b x y pc. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l5_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l5_mc) (a, 5120) /\ @@ -175,7 +175,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst MLDSA_POINTWISE_ACC_L5_EXEC] THEN + fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN @@ -208,7 +208,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate all 1703 instructions with SIMD simplification *) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POINTWISE_ACC_L5_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC [n] THEN SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) (1--1703) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -315,7 +315,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove (* Subroutine form *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_SUBROUTINE_CORRECT = prove (`!r a b x y pc returnaddress. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l5_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l5_mc) (a, 5120) /\ @@ -342,10 +342,10 @@ let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_CORRECT = prove abs(ival zi) <= &8380416)) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(r, 1024)])`, - REWRITE_TAC[fst MLDSA_POINTWISE_ACC_L5_EXEC] THEN - ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POINTWISE_ACC_L5_EXEC - (REWRITE_RULE[fst MLDSA_POINTWISE_ACC_L5_EXEC] - MLDSA_POINTWISE_ACC_L5_CORRECT));; + REWRITE_TAC[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC] THEN + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC + (REWRITE_RULE[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC] + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -357,10 +357,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "mldsa_pointwise_acc_l5" subroutine_signatures) - MLDSA_POINTWISE_ACC_L5_SUBROUTINE_CORRECT - MLDSA_POINTWISE_ACC_L5_EXEC;; + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_SUBROUTINE_CORRECT + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC;; -let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_SAFE = time prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_SUBROUTINE_SAFE = time prove (`exists f_events. forall e r a b pc returnaddress. nonoverlapping (word pc,LENGTH mldsa_pointwise_acc_l5_mc) (r,1024) /\ @@ -386,5 +386,5 @@ let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_SAFE = time prove [r,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POINTWISE_ACC_L5_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC);; diff --git a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml index 04e2a15344..33493ea666 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml @@ -168,13 +168,13 @@ let mldsa_pointwise_acc_l7_mc = define_assert_from_elf ];; (*** BYTECODE END ***) -let MLDSA_POINTWISE_ACC_L7_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l7_mc;; +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC = ARM_MK_EXEC_RULE mldsa_pointwise_acc_l7_mc;; (* ========================================================================= *) (* Correctness proof *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L7_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_CORRECT = prove (`!r a b x y pc. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l7_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l7_mc) (a, 7168) /\ @@ -207,7 +207,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove `x:num->int32`; `y:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst MLDSA_POINTWISE_ACC_L7_EXEC] THEN + fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN GLOBALIZE_PRECONDITION_TAC THEN @@ -240,7 +240,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN (* Simulate all 2215 instructions with SIMD simplification *) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POINTWISE_ACC_L7_EXEC [n] THEN + MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC [n] THEN SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) (1--2215) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -347,7 +347,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove (* Subroutine form *) (* ========================================================================= *) -let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_CORRECT = prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_SUBROUTINE_CORRECT = prove (`!r a b x y pc returnaddress. nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l7_mc) (r, 1024) /\ nonoverlapping (word pc, LENGTH mldsa_pointwise_acc_l7_mc) (a, 7168) /\ @@ -374,10 +374,10 @@ let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_CORRECT = prove abs(ival zi) <= &8380416)) (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(r, 1024)])`, - REWRITE_TAC[fst MLDSA_POINTWISE_ACC_L7_EXEC] THEN - ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POINTWISE_ACC_L7_EXEC - (REWRITE_RULE[fst MLDSA_POINTWISE_ACC_L7_EXEC] - MLDSA_POINTWISE_ACC_L7_CORRECT));; + REWRITE_TAC[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC] THEN + ARM_ADD_RETURN_NOSTACK_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC + (REWRITE_RULE[fst MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC] + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_CORRECT));; (* ========================================================================= *) @@ -390,10 +390,10 @@ needs "mldsa_native/aarch64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:false (assoc "mldsa_pointwise_acc_l7" subroutine_signatures) - MLDSA_POINTWISE_ACC_L7_SUBROUTINE_CORRECT - MLDSA_POINTWISE_ACC_L7_EXEC;; + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_SUBROUTINE_CORRECT + MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC;; -let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_SAFE = time prove +let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_SUBROUTINE_SAFE = time prove (`exists f_events. forall e r a b pc returnaddress. nonoverlapping (word pc,LENGTH mldsa_pointwise_acc_l7_mc) (r,1024) /\ @@ -419,4 +419,4 @@ let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_SAFE = time prove [r,1024])) (\s s'. true)`, ASSERT_CONCL_TAC full_spec THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POINTWISE_ACC_L7_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC);; diff --git a/proofs/hol_light/x86_64/list_thms.sh b/proofs/hol_light/x86_64/list_thms.sh new file mode 100755 index 0000000000..3ca7693ca8 --- /dev/null +++ b/proofs/hol_light/x86_64/list_thms.sh @@ -0,0 +1,34 @@ +#!/usr/bin/env bash +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +# +# This tiny script lists HOL-Light theorem names declared as proofs. + +ROOT=$(git rev-parse --show-toplevel) +cd "$ROOT" || exit + +if [[ $# == 0 ]]; then + set -- proofs/hol_light/x86_64/proofs/*.ml +fi + +awk ' + function flush() { + if (name != "" && block ~ /(^|[[:space:](])(time[[:space:]]+)?prove($|[[:space:]]|`|\()|(^|[[:space:](])ADD_IBT_RULE([[:space:]]|\()/) { + print name + } + } + /^let[[:space:]]+[^[:space:]]+[[:space:]]*=/ { + flush() + name = $0 + sub(/^let[[:space:]]+/, "", name) + sub(/[[:space:]]*=.*/, "", name) + block = $0 + next + } + name != "" { + block = block "\n" $0 + } + END { + flush() + } +' "$@" diff --git a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml index 102d3b8fcf..4910678438 100644 --- a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml @@ -751,32 +751,32 @@ let keccak_f1600_x4_avx2_mc = define_assert_from_elf let keccak_f1600_x4_avx2_tmc = define_trimmed "keccak_f1600_x4_avx2_tmc" keccak_f1600_x4_avx2_mc;; -let KECCAK_F1600_X4_AVX2_EXEC = X86_MK_CORE_EXEC_RULE keccak_f1600_x4_avx2_tmc;; -let keccak_f1600_x4_avx2_TMC_EXEC = KECCAK_F1600_X4_AVX2_EXEC;; +let KECCAK_F1600_X4_EXEC = X86_MK_CORE_EXEC_RULE keccak_f1600_x4_avx2_tmc;; +let keccak_f1600_x4_avx2_TMC_EXEC = KECCAK_F1600_X4_EXEC;; let LENGTH_KECCAK_F1600_X4_AVX2_TMC = REWRITE_CONV[keccak_f1600_x4_avx2_tmc] `LENGTH keccak_f1600_x4_avx2_tmc` |> CONV_RULE(RAND_CONV LENGTH_CONV);; (* Preamble: MOV r11, rsp (3) + AND rsp, -32 (4) + SUB rsp, 768 (7) = 14 bytes *) -let KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = new_definition - `KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = 14`;; +let KECCAK_F1600_X4_PREAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_PREAMBLE_LENGTH = 14`;; (* Postamble: MOV rsp, r11 (3 bytes) + RET (1 byte) = 4 bytes *) -let KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = new_definition - `KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = 4`;; +let KECCAK_F1600_X4_POSTAMBLE_LENGTH = new_definition + `KECCAK_F1600_X4_POSTAMBLE_LENGTH = 4`;; -let KECCAK_F1600_X4_AVX2_CORE_END = new_definition - `KECCAK_F1600_X4_AVX2_CORE_END = LENGTH keccak_f1600_x4_avx2_tmc - KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH`;; +let KECCAK_F1600_X4_CORE_END = new_definition + `KECCAK_F1600_X4_CORE_END = LENGTH keccak_f1600_x4_avx2_tmc - KECCAK_F1600_X4_POSTAMBLE_LENGTH`;; let LENGTH_SIMPLIFY_CONV = REWRITE_CONV[LENGTH_KECCAK_F1600_X4_AVX2_TMC; - KECCAK_F1600_X4_AVX2_CORE_END; - KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH; - KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH] THENC + KECCAK_F1600_X4_CORE_END; + KECCAK_F1600_X4_PREAMBLE_LENGTH; + KECCAK_F1600_X4_POSTAMBLE_LENGTH] THENC NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];; -let KECCAK_F1600_X4_AVX2_CORRECT = prove +let KECCAK_F1600_X4_CORRECT = prove (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64. PAIRWISE nonoverlapping [(word pc, LENGTH keccak_f1600_x4_avx2_tmc); @@ -787,7 +787,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove (rho56_ptr, 32)] ==> ensures x86 (\s. bytes_loaded s (word pc) (BUTLAST keccak_f1600_x4_avx2_tmc) /\ - read RIP s = word (pc + KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH) /\ + read RIP s = word (pc + KECCAK_F1600_X4_PREAMBLE_LENGTH) /\ read RSP s = stackpointer /\ read RDI s = bitstate_in /\ C_ARGUMENTS [bitstate_in; rc_pointer; rho8_ptr; rho56_ptr] s /\ @@ -798,7 +798,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove wordlist_from_memory(word_add bitstate_in (word 200),25) s = A2 /\ wordlist_from_memory(word_add bitstate_in (word 400),25) s = A3 /\ wordlist_from_memory(word_add bitstate_in (word 600),25) s = A4) - (\s. read RIP s = word(pc + KECCAK_F1600_X4_AVX2_CORE_END) /\ + (\s. read RIP s = word(pc + KECCAK_F1600_X4_CORE_END) /\ wordlist_from_memory(bitstate_in,25) s = keccak 24 A1 /\ wordlist_from_memory(word_add bitstate_in (word 200),25) s = keccak 24 A2 /\ wordlist_from_memory(word_add bitstate_in (word 400),25) s = keccak 24 A3 /\ @@ -882,7 +882,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--96) THEN + X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--96) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [PURE_ONCE_REWRITE_TAC[ARITH_RULE `8 * 0 = 0`] THEN @@ -940,7 +940,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove MEMORY_256_FROM_64_TAC "rho8_ptr" 0 4 THEN MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--223) THEN + X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--223) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[WORD_ADD]; @@ -992,7 +992,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove MEMORY_256_FROM_64_TAC "rho8_ptr" 0 4 THEN MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--1) THEN + X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[]; @@ -1015,7 +1015,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC [keccak; keccak_round] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--96) THEN + X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--96) THEN REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONV_RULE(READ_MEMORY_SPLIT_CONV 2) o check (can (term_match [] `read qqq s:int256 = xxx`) o concl))) THEN @@ -1025,9 +1025,9 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove BITBLAST_TAC]);; -let KECCAK_F1600_X4_AVX2_FULL_EXEC = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc;; +let KECCAK_F1600_X4_FULL_EXEC = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc;; -let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove +let KECCAK_F1600_X4_NOIBT_SUBROUTINE_CORRECT = prove (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64 returnaddress. PAIRWISE nonoverlapping [(word pc, LENGTH keccak_f1600_x4_avx2_tmc); @@ -1069,14 +1069,14 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove WORD_FORALL_OFFSET_TAC 0x31f THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN REWRITE_TAC[PAIRWISE; ALL; C_ARGUMENTS; NONOVERLAPPING_CLAUSES] THEN - REWRITE_TAC[fst KECCAK_F1600_X4_AVX2_FULL_EXEC] THEN + REWRITE_TAC[fst KECCAK_F1600_X4_FULL_EXEC] THEN REWRITE_TAC[WORDLIST_FROM_MEMORY] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN REPEAT STRIP_TAC THEN (* Step through the three preamble instructions. *) ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC (1--3) THEN + X86_STEPS_TAC KECCAK_F1600_X4_FULL_EXEC (1--3) THEN (* Abbreviate the data-dependent slack introduced by `and rsp, -32`. `delta` is the number of bytes (0..31) the alignment shaved off rsp; @@ -1101,7 +1101,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove `rho8_ptr:int64`; `rho56_ptr:int64`; `A1:int64 list`; `A2:int64 list`; `A3:int64 list`; `A4:int64 list`; `pc:num`; `word_add stackpointer (word delta):int64`] - (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_CORRECT)) THEN + (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_CORRECT)) THEN ANTS_TAC THENL [REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_imp o concl))) THEN REWRITE_TAC[PAIRWISE; ALL; C_ARGUMENTS; NONOVERLAPPING_CLAUSES] THEN @@ -1112,16 +1112,16 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove REWRITE_TAC[C_ARGUMENTS; SOME_FLAGS] THEN REWRITE_TAC[WORDLIST_FROM_MEMORY] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN - X86_BIGSTEP_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC "s4" THENL + X86_BIGSTEP_TAC KECCAK_F1600_X4_FULL_EXEC "s4" THENL [MATCH_MP_TAC BYTES_LOADED_BUTLAST THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - X86_STEPS_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC (5--6) THEN + X86_STEPS_TAC KECCAK_F1600_X4_FULL_EXEC (5--6) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[]);; (* NOTE: This must be kept in sync with the CBMC specification * in dev/fips202/x86_64/src/fips202_native_x86_64.h *) -let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove +let KECCAK_F1600_X4_SUBROUTINE_CORRECT = prove (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64 returnaddress. PAIRWISE nonoverlapping [(word pc, LENGTH keccak_f1600_x4_avx2_mc); @@ -1160,7 +1160,7 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove MATCH_ACCEPT_TAC(ADD_IBT_RULE (CONV_RULE TWEAK_CONV (REWRITE_RULE[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] - KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT))));; + KECCAK_F1600_X4_NOIBT_SUBROUTINE_CORRECT))));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -1173,10 +1173,10 @@ needs "mldsa_native/x86_64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "keccak_f1600_x4_avx2" subroutine_signatures) - (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_CORRECT) - KECCAK_F1600_X4_AVX2_EXEC;; + (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_CORRECT) + KECCAK_F1600_X4_EXEC;; -let KECCAK_F1600_X4_AVX2_SAFE = time prove +let KECCAK_F1600_X4_SAFE = time prove (`exists f_events. forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer. PAIRWISE nonoverlapping @@ -1187,12 +1187,12 @@ let KECCAK_F1600_X4_AVX2_SAFE = time prove (\s. bytes_loaded s (word pc) (BUTLAST keccak_f1600_x4_avx2_tmc) /\ - read RIP s = word (pc + KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH) /\ + read RIP s = word (pc + KECCAK_F1600_X4_PREAMBLE_LENGTH) /\ read RSP s = stackpointer /\ C_ARGUMENTS [bitstate_in; rc_pointer; rho8_ptr; rho56_ptr] s /\ read events s = e) (\s. - read RIP s = word (pc + KECCAK_F1600_X4_AVX2_CORE_END) /\ + read RIP s = word (pc + KECCAK_F1600_X4_CORE_END) /\ (exists e2. read events s = APPEND e2 e /\ e2 = f_events rc_pointer rho8_ptr rho56_ptr bitstate_in pc stackpointer /\ @@ -1211,7 +1211,7 @@ let KECCAK_F1600_X4_AVX2_SAFE = time prove CONV_TAC(ONCE_DEPTH_CONV LENGTH_SIMPLIFY_CONV) THEN ASSERT_CONCL_TAC full_spec THEN REWRITE_TAC[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] THEN - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_AVX2_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_EXEC);; (* ========================================================================= *) @@ -1254,7 +1254,7 @@ let FRAME_CONTAINED = prove REWRITE_TAC[VAL_WORD_ADD; VAL_WORD; DIMINDEX_64; CONG] THEN CONV_TAC MOD_DOWN_CONV THEN AP_THM_TAC THEN AP_TERM_TAC THEN ARITH_TAC);; -let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove +let KECCAK_F1600_X4_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer returnaddress. PAIRWISE nonoverlapping @@ -1288,7 +1288,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove stackpointer,8])) (\s s'. true)`, let EXPAND_PAIRWISE_CONV = REWRITE_CONV[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] in - let inner_safe = CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_SAFE in + let inner_safe = CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_SAFE in let execth = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc in CONV_TAC(ONCE_DEPTH_CONV EXPAND_PAIRWISE_CONV) THEN (* Skolemize the inner SAFE's existential f_events into a free term @@ -1395,7 +1395,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove REWRITE_TAC[EX] THEN ASM_MESON_TAC[CONTAINED_REFL; FRAME_CONTAINED]);; -let KECCAK_F1600_X4_AVX2_SUBROUTINE_SAFE = time prove +let KECCAK_F1600_X4_SUBROUTINE_SAFE = time prove (`exists f_events. forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer returnaddress. PAIRWISE nonoverlapping @@ -1432,4 +1432,4 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_SAFE = time prove CONV_TAC(ONCE_DEPTH_CONV EXPAND_PAIRWISE_CONV) THEN MATCH_ACCEPT_TAC(ADD_IBT_RULE (REWRITE_RULE[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] - KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE)));; + KECCAK_F1600_X4_NOIBT_SUBROUTINE_SAFE)));; diff --git a/proofs/hol_light/x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml index 459e9a328b..ac18c52198 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml @@ -252,7 +252,7 @@ let mldsa_caddq_mc = define_assert_from_elf "mldsa_caddq_mc" "x86_64/mldsa/mldsa (*** BYTECODE END ***) let mldsa_caddq_tmc = define_trimmed "mldsa_caddq_tmc" mldsa_caddq_mc;; -let MLDSA_CADDQ_TMC_EXEC = X86_MK_CORE_EXEC_RULE mldsa_caddq_tmc;; +let MLDSA_POLY_CADDQ_TMC_EXEC = X86_MK_CORE_EXEC_RULE mldsa_caddq_tmc;; (* ------------------------------------------------------------------------- *) (* Functional specification of mldsa_caddq *) @@ -274,7 +274,7 @@ let mldsa_caddq_direct = prove (* Core correctness theorem *) (* ------------------------------------------------------------------------- *) -let MLDSA_CADDQ_CORRECT = time prove +let MLDSA_POLY_CADDQ_CORRECT = time prove (`!a x pc. aligned 32 a /\ nonoverlapping (word pc,876) (a, 1024) @@ -302,11 +302,11 @@ let MLDSA_CADDQ_CORRECT = time prove MAYCHANGE [memory :> bytes(a,1024)])`, MAP_EVERY X_GEN_TAC [`a:int64`; `x:num->int32`; `pc:num`] THEN - REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; fst MLDSA_CADDQ_TMC_EXEC] THEN + REWRITE_TAC[NONOVERLAPPING_CLAUSES; C_ARGUMENTS; fst MLDSA_POLY_CADDQ_TMC_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV))) THEN CONV_TAC NUM_REDUCE_CONV THEN REPEAT STRIP_TAC THEN - REWRITE_TAC [SOME_FLAGS; fst MLDSA_CADDQ_TMC_EXEC] THEN + REWRITE_TAC [SOME_FLAGS; fst MLDSA_POLY_CADDQ_TMC_EXEC] THEN GHOST_INTRO_TAC `init_ymm0:int256` `read YMM0` THEN GHOST_INTRO_TAC `init_ymm1:int256` `read YMM1` THEN ENSURES_INIT_TAC "s0" THEN @@ -318,7 +318,7 @@ let MLDSA_CADDQ_CORRECT = time prove DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN MAP_EVERY (fun n -> - X86_STEPS_TAC MLDSA_CADDQ_TMC_EXEC [n] THEN + X86_STEPS_TAC MLDSA_POLY_CADDQ_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC[mldsa_caddq]) (1--132) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN @@ -345,7 +345,7 @@ let MLDSA_CADDQ_CORRECT = time prove (* in mldsa/src/native/x86_64/src/arith_native_x86_64.h *) (* ------------------------------------------------------------------------- *) -let MLDSA_CADDQ_NOIBT_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_CADDQ_NOIBT_SUBROUTINE_CORRECT = prove (`!a x pc stackpointer returnaddress. aligned 32 a /\ nonoverlapping (word pc,LENGTH mldsa_caddq_tmc) (a,1024) /\ @@ -373,9 +373,9 @@ let MLDSA_CADDQ_NOIBT_SUBROUTINE_CORRECT = prove (word_add a (word(4 * i)))) s) < &8380417)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,1024)])`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_caddq_tmc MLDSA_CADDQ_CORRECT);; + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_caddq_tmc MLDSA_POLY_CADDQ_CORRECT);; -let MLDSA_CADDQ_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_CADDQ_SUBROUTINE_CORRECT = prove (`!a x pc stackpointer returnaddress. aligned 32 a /\ nonoverlapping (word pc,LENGTH mldsa_caddq_mc) (a,1024) /\ @@ -403,7 +403,7 @@ let MLDSA_CADDQ_SUBROUTINE_CORRECT = prove (word_add a (word(4 * i)))) s) < &8380417)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a,1024)])`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_CADDQ_NOIBT_SUBROUTINE_CORRECT));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_CADDQ_NOIBT_SUBROUTINE_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -415,14 +415,14 @@ needs "mldsa_native/x86_64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "mldsa_poly_caddq_x86" subroutine_signatures) - (REWRITE_RULE[SOME_FLAGS] MLDSA_CADDQ_CORRECT) - MLDSA_CADDQ_TMC_EXEC;; + (REWRITE_RULE[SOME_FLAGS] MLDSA_POLY_CADDQ_CORRECT) + MLDSA_POLY_CADDQ_TMC_EXEC;; -let MLDSA_CADDQ_SAFE = time prove +let MLDSA_POLY_CADDQ_SAFE = time prove (full_spec, - PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_CADDQ_TMC_EXEC);; + PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_POLY_CADDQ_TMC_EXEC);; -let MLDSA_CADDQ_NOIBT_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_CADDQ_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a pc stackpointer returnaddress. aligned 32 a /\ @@ -444,10 +444,10 @@ let MLDSA_CADDQ_NOIBT_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_caddq_tmc MLDSA_CADDQ_SAFE THEN + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_caddq_tmc MLDSA_POLY_CADDQ_SAFE THEN DISCHARGE_SAFETY_PROPERTY_TAC);; -let MLDSA_CADDQ_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_CADDQ_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a pc stackpointer returnaddress. aligned 32 a /\ @@ -469,4 +469,4 @@ let MLDSA_CADDQ_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_CADDQ_NOIBT_SUBROUTINE_SAFE));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_CADDQ_NOIBT_SUBROUTINE_SAFE));; diff --git a/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml index 73de27c067..55f0afd742 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml @@ -727,7 +727,7 @@ let mldsa_decompose32_mc = define_assert_from_elf "mldsa_decompose32_mc" "x86_64 (*** BYTECODE END ***) let mldsa_decompose32_tmc = define_trimmed "mldsa_decompose32_tmc" mldsa_decompose32_mc;; -let MLDSA_DECOMPOSE32_EXEC = X86_MK_CORE_EXEC_RULE mldsa_decompose32_tmc;; +let MLDSA_POLY_DECOMPOSE_32_EXEC = X86_MK_CORE_EXEC_RULE mldsa_decompose32_tmc;; (* ========================================================================= *) (* Word-level lane functions matching the AVX2 instruction sequence. *) @@ -1082,7 +1082,7 @@ let DECOMPOSE32_A0_BOUND_HI = prove( (* Core correctness theorem *) (* ========================================================================= *) -let MLDSA_DECOMPOSE32_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_32_CORRECT = prove( `!a1 a (x:num->int32) pc. ALL (nonoverlapping (word pc, 2144)) [(a1,1024); (a,1024)] /\ @@ -1113,7 +1113,7 @@ let MLDSA_DECOMPOSE32_CORRECT = prove( MAYCHANGE [memory :> bytes(a,1024)])`, MAP_EVERY X_GEN_TAC [`a1:int64`; `a:int64`; `x:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; ALL; - NONOVERLAPPING_CLAUSES; fst MLDSA_DECOMPOSE32_EXEC] THEN + NONOVERLAPPING_CLAUSES; fst MLDSA_POLY_DECOMPOSE_32_EXEC] THEN STRIP_TAC THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV (EXPAND_CASES_CONV THENC ONCE_DEPTH_CONV NUM_MULT_CONV)))) THEN @@ -1127,7 +1127,7 @@ let MLDSA_DECOMPOSE32_CORRECT = prove( DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN MAP_EVERY (fun n -> - X86_STEPS_TAC MLDSA_DECOMPOSE32_EXEC [n] THEN + X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_32_EXEC [n] THEN SIMD_SIMPLIFY_TAC[decompose32_a1; decompose32_a0]) (1--399) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[WORD_NOT_JOIN_256; WORD_NOT_JOIN_128; WORD_NOT_JOIN_64]) THEN @@ -1149,7 +1149,7 @@ let MLDSA_DECOMPOSE32_CORRECT = prove( (* mldsa/src/native/x86_64/src/arith_native_x86_64.h *) (* ========================================================================= *) -let MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_32_NOIBT_SUBROUTINE_CORRECT = prove( `!a1 a (x:num->int32) pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ ALL (nonoverlapping (word pc, LENGTH mldsa_decompose32_tmc)) @@ -1183,9 +1183,9 @@ let MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_CORRECT = prove( (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a1,1024)] ,, MAYCHANGE [memory :> bytes(a,1024)])`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose32_tmc MLDSA_DECOMPOSE32_CORRECT);; + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose32_tmc MLDSA_POLY_DECOMPOSE_32_CORRECT);; -let MLDSA_DECOMPOSE32_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_32_SUBROUTINE_CORRECT = prove( `!a1 a (x:num->int32) pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ ALL (nonoverlapping (word pc, LENGTH mldsa_decompose32_mc)) @@ -1219,7 +1219,7 @@ let MLDSA_DECOMPOSE32_SUBROUTINE_CORRECT = prove( (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a1,1024)] ,, MAYCHANGE [memory :> bytes(a,1024)])`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_CORRECT));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_DECOMPOSE_32_NOIBT_SUBROUTINE_CORRECT));; (* ========================================================================= *) (* Memory safety. *) @@ -1233,18 +1233,18 @@ needs "mldsa_native/x86_64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "mldsa_poly_decompose_32_x86" subroutine_signatures) - (REWRITE_RULE[SOME_FLAGS] MLDSA_DECOMPOSE32_CORRECT) - MLDSA_DECOMPOSE32_EXEC;; + (REWRITE_RULE[SOME_FLAGS] MLDSA_POLY_DECOMPOSE_32_CORRECT) + MLDSA_POLY_DECOMPOSE_32_EXEC;; -let MLDSA_DECOMPOSE32_SAFE = +let MLDSA_POLY_DECOMPOSE_32_SAFE = REWRITE_RULE [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] (time prove (full_spec, REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] THEN PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars - MLDSA_DECOMPOSE32_EXEC));; + MLDSA_POLY_DECOMPOSE_32_EXEC));; -let MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_32_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a1 a pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ @@ -1269,10 +1269,10 @@ let MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; a1,1024; a,1024; stackpointer,8] [a1,1024; a,1024; stackpointer,8])) (\s s'. true)`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose32_tmc MLDSA_DECOMPOSE32_SAFE THEN + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose32_tmc MLDSA_POLY_DECOMPOSE_32_SAFE THEN DISCHARGE_SAFETY_PROPERTY_TAC);; -let MLDSA_DECOMPOSE32_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_32_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a1 a pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ @@ -1297,4 +1297,4 @@ let MLDSA_DECOMPOSE32_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; a1,1024; a,1024; stackpointer,8] [a1,1024; a,1024; stackpointer,8])) (\s s'. true)`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_DECOMPOSE32_NOIBT_SUBROUTINE_SAFE));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_DECOMPOSE_32_NOIBT_SUBROUTINE_SAFE));; diff --git a/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_88_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_88_avx2_asm.ml index 7813485827..2554e7e668 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_88_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_88_avx2_asm.ml @@ -727,7 +727,7 @@ let mldsa_decompose88_mc = define_assert_from_elf "mldsa_decompose88_mc" "x86_64 (*** BYTECODE END ***) let mldsa_decompose88_tmc = define_trimmed "mldsa_decompose88_tmc" mldsa_decompose88_mc;; -let MLDSA_DECOMPOSE88_EXEC = X86_MK_CORE_EXEC_RULE mldsa_decompose88_tmc;; +let MLDSA_POLY_DECOMPOSE_88_EXEC = X86_MK_CORE_EXEC_RULE mldsa_decompose88_tmc;; (* ========================================================================= *) (* Word-level lane functions matching the AVX2 instruction sequence. *) @@ -1082,7 +1082,7 @@ let DECOMPOSE88_A0_BOUND_HI = prove( (* Core correctness theorem *) (* ========================================================================= *) -let MLDSA_DECOMPOSE88_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_88_CORRECT = prove( `!a1 a (x:num->int32) pc. ALL (nonoverlapping (word pc, 2144)) [(a1,1024); (a,1024)] /\ @@ -1113,7 +1113,7 @@ let MLDSA_DECOMPOSE88_CORRECT = prove( MAYCHANGE [memory :> bytes(a,1024)])`, MAP_EVERY X_GEN_TAC [`a1:int64`; `a:int64`; `x:num->int32`; `pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; ALL; - NONOVERLAPPING_CLAUSES; fst MLDSA_DECOMPOSE88_EXEC] THEN + NONOVERLAPPING_CLAUSES; fst MLDSA_POLY_DECOMPOSE_88_EXEC] THEN STRIP_TAC THEN CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV (EXPAND_CASES_CONV THENC ONCE_DEPTH_CONV NUM_MULT_CONV)))) THEN @@ -1127,7 +1127,7 @@ let MLDSA_DECOMPOSE88_CORRECT = prove( DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN MAP_EVERY (fun n -> - X86_STEPS_TAC MLDSA_DECOMPOSE88_EXEC [n] THEN + X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_88_EXEC [n] THEN SIMD_SIMPLIFY_TAC[decompose88_a1; decompose88_a0]) (1--399) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[WORD_NOT_JOIN_256; WORD_NOT_JOIN_128; WORD_NOT_JOIN_64]) THEN @@ -1149,7 +1149,7 @@ let MLDSA_DECOMPOSE88_CORRECT = prove( (* mldsa/src/native/x86_64/src/arith_native_x86_64.h *) (* ========================================================================= *) -let MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_88_NOIBT_SUBROUTINE_CORRECT = prove( `!a1 a (x:num->int32) pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ ALL (nonoverlapping (word pc, LENGTH mldsa_decompose88_tmc)) @@ -1183,9 +1183,9 @@ let MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_CORRECT = prove( (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a1,1024)] ,, MAYCHANGE [memory :> bytes(a,1024)])`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose88_tmc MLDSA_DECOMPOSE88_CORRECT);; + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose88_tmc MLDSA_POLY_DECOMPOSE_88_CORRECT);; -let MLDSA_DECOMPOSE88_SUBROUTINE_CORRECT = prove( +let MLDSA_POLY_DECOMPOSE_88_SUBROUTINE_CORRECT = prove( `!a1 a (x:num->int32) pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ ALL (nonoverlapping (word pc, LENGTH mldsa_decompose88_mc)) @@ -1219,7 +1219,7 @@ let MLDSA_DECOMPOSE88_SUBROUTINE_CORRECT = prove( (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a1,1024)] ,, MAYCHANGE [memory :> bytes(a,1024)])`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_CORRECT));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_DECOMPOSE_88_NOIBT_SUBROUTINE_CORRECT));; (* ========================================================================= *) (* Memory safety. *) @@ -1233,18 +1233,18 @@ needs "mldsa_native/x86_64/proofs/subroutine_signatures.ml";; let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "mldsa_poly_decompose_88_x86" subroutine_signatures) - (REWRITE_RULE[SOME_FLAGS] MLDSA_DECOMPOSE88_CORRECT) - MLDSA_DECOMPOSE88_EXEC;; + (REWRITE_RULE[SOME_FLAGS] MLDSA_POLY_DECOMPOSE_88_CORRECT) + MLDSA_POLY_DECOMPOSE_88_EXEC;; -let MLDSA_DECOMPOSE88_SAFE = +let MLDSA_POLY_DECOMPOSE_88_SAFE = REWRITE_RULE [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] (time prove (full_spec, REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] THEN PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars - MLDSA_DECOMPOSE88_EXEC));; + MLDSA_POLY_DECOMPOSE_88_EXEC));; -let MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_88_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a1 a pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ @@ -1269,10 +1269,10 @@ let MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; a1,1024; a,1024; stackpointer,8] [a1,1024; a,1024; stackpointer,8])) (\s s'. true)`, - X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose88_tmc MLDSA_DECOMPOSE88_SAFE THEN + X86_PROMOTE_RETURN_NOSTACK_TAC mldsa_decompose88_tmc MLDSA_POLY_DECOMPOSE_88_SAFE THEN DISCHARGE_SAFETY_PROPERTY_TAC);; -let MLDSA_DECOMPOSE88_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_DECOMPOSE_88_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a1 a pc stackpointer returnaddress. aligned 32 a1 /\ aligned 32 a /\ @@ -1297,4 +1297,4 @@ let MLDSA_DECOMPOSE88_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; a1,1024; a,1024; stackpointer,8] [a1,1024; a,1024; stackpointer,8])) (\s s'. true)`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_DECOMPOSE88_NOIBT_SUBROUTINE_SAFE));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_DECOMPOSE_88_NOIBT_SUBROUTINE_SAFE));; diff --git a/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_32_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_32_avx2_asm.ml index c888fba0e8..5d5e337052 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_32_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_32_avx2_asm.ml @@ -91,7 +91,7 @@ let poly_use_hint_32_avx2_asm_mc = define_assert_from_elf let poly_use_hint_32_avx2_asm_tmc = define_trimmed "poly_use_hint_32_avx2_asm_tmc" poly_use_hint_32_avx2_asm_mc;; -let POLY_USE_HINT_32_AVX2_ASM_EXEC = +let MLDSA_POLY_USE_HINT_32_EXEC = X86_MK_CORE_EXEC_RULE poly_use_hint_32_avx2_asm_tmc;; (* ------------------------------------------------------------------------- *) @@ -933,7 +933,7 @@ let DUPLITS = map (fun (n,c) -> prove(mk_eq(mk_comb(`word:num->int256`, mk_numer (* or above i+1 (untouched) are preserved by the single 256-bit store. *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_32_AVX2_ASM_BODY_BLOCK_TAC : tactic = +let MLDSA_POLY_USE_HINT_32_BODY_BLOCK_TAC : tactic = REPEAT STRIP_TAC THEN ENSURES_INIT_TAC "s0" THEN MP_TAC(SPECL [`a:int64`;`i:num`] ALIGNED_BLOCK) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN @@ -964,7 +964,7 @@ let POLY_USE_HINT_32_AVX2_ASM_BODY_BLOCK_TAC : tactic = `!b. i <= b /\ b < 32 ==> read(memory :> bytes256(word_add a (word(32*b)))) s0 = xb b`) (concl th) then MP_TAC(SPEC `b:num` th) else failwith "no") THEN ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN ACCEPT_TAC]; ALL_TAC] THEN - EVERY (map (fun n -> X86_STEPS_TAC POLY_USE_HINT_32_AVX2_ASM_EXEC [n] THEN SIMD_SIMPLIFY_TAC[]) (1--24)) THEN + EVERY (map (fun n -> X86_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC [n] THEN SIMD_SIMPLIFY_TAC[]) (1--24)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN TRY(REWRITE_TAC[ARITH_RULE `32 * (i + 1) = 32 * i + 32`] THEN CONV_TAC WORD_RULE) THEN @@ -992,7 +992,7 @@ let POLY_USE_HINT_32_AVX2_ASM_BODY_BLOCK_TAC : tactic = (* through the SIMD UseHint, over 32 loop iterations. *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_32_AVX2_ASM_BLOCK_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_BLOCK_CORRECT = prove (`!a h xb yb pc. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, 0xbc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) /\ @@ -1010,7 +1010,7 @@ let POLY_USE_HINT_32_AVX2_ASM_BLOCK_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, MAP_EVERY X_GEN_TAC [`a:int64`;`h:int64`;`xb:num->int256`;`yb:num->int256`;`pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst POLY_USE_HINT_32_AVX2_ASM_EXEC] THEN + fst MLDSA_POLY_USE_HINT_32_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN REWRITE_TAC[SOME_FLAGS] THEN ENSURES_WHILE_PUP_TAC `32` `pc + 0x50` `pc + 0xba` `\i s. @@ -1037,21 +1037,21 @@ let POLY_USE_HINT_32_AVX2_ASM_BLOCK_CORRECT = prove (* INIT: run the constant-setup block to the loop top. *) REWRITE_TAC[MULT_CLAUSES; WORD_ADD_0] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC POLY_USE_HINT_32_AVX2_ASM_EXEC (1--17) THEN + X86_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC (1--17) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC DUPLITS THEN REWRITE_TAC[ARITH_RULE `b < 0 <=> F`; LE_0] THEN ASM_REWRITE_TAC[] ; (* BODY *) - POLY_USE_HINT_32_AVX2_ASM_BODY_BLOCK_TAC + MLDSA_POLY_USE_HINT_32_BODY_BLOCK_TAC ; (* BACKEDGE *) - REPEAT STRIP_TAC THEN X86_SIM_TAC POLY_USE_HINT_32_AVX2_ASM_EXEC (1--1) + REPEAT STRIP_TAC THEN X86_SIM_TAC MLDSA_POLY_USE_HINT_32_EXEC (1--1) ; (* EXIT: the invariant at i = 32 is the postcondition. *) REWRITE_TAC[ARITH_RULE `32 <= b /\ b < 32 <=> F`] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC POLY_USE_HINT_32_AVX2_ASM_EXEC (1--1) THEN + X86_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC (1--1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] ]);; @@ -1062,7 +1062,7 @@ let POLY_USE_HINT_32_AVX2_ASM_BLOCK_CORRECT = prove (* mldsa/src/native/x86_64/src/arith_native_x86_64.h *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_32_AVX2_ASM_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_CORRECT = prove (`!a h x y pc. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, 0xbc) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -1163,7 +1163,7 @@ let POLY_USE_HINT_32_AVX2_ASM_CORRECT = prove ] ; (* the block-function correctness specialised at xb = pack8 x, yb = pack8 y *) - MATCH_MP_TAC POLY_USE_HINT_32_AVX2_ASM_BLOCK_CORRECT THEN + MATCH_MP_TAC MLDSA_POLY_USE_HINT_32_BLOCK_CORRECT THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`y:num->int32`;`b:num`;`k:num`] PACK8_LANE) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN @@ -1181,7 +1181,7 @@ let POLY_USE_HINT_32_AVX2_ASM_CORRECT = prove (* Public subroutine correctness (with return). *) (* ========================================================================= *) -let POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_NOIBT_SUBROUTINE_CORRECT = prove (`!a h x y pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, LENGTH poly_use_hint_32_avx2_asm_tmc) (a, 1024) /\ @@ -1206,9 +1206,9 @@ let POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT = prove val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 16)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_32_avx2_asm_tmc POLY_USE_HINT_32_AVX2_ASM_CORRECT);; + X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_32_avx2_asm_tmc MLDSA_POLY_USE_HINT_32_CORRECT);; -let POLY_USE_HINT_32_AVX2_ASM_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_32_SUBROUTINE_CORRECT = prove (`!a h x y pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, LENGTH poly_use_hint_32_avx2_asm_mc) (a, 1024) /\ @@ -1233,7 +1233,7 @@ let POLY_USE_HINT_32_AVX2_ASM_SUBROUTINE_CORRECT = prove val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 16)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_USE_HINT_32_NOIBT_SUBROUTINE_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -1249,18 +1249,18 @@ let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "mldsa_poly_use_hint_32_x86" subroutine_signatures) (REWRITE_RULE[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] - POLY_USE_HINT_32_AVX2_ASM_CORRECT) - POLY_USE_HINT_32_AVX2_ASM_EXEC;; + MLDSA_POLY_USE_HINT_32_CORRECT) + MLDSA_POLY_USE_HINT_32_EXEC;; -let POLY_USE_HINT_32_AVX2_ASM_SAFE = time prove +let MLDSA_POLY_USE_HINT_32_SAFE = time prove (full_spec, REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] THEN GEN_PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars ~tac_before_maychange_simp:NORMALIZE_AND_EXPAND_YMM_TAC - POLY_USE_HINT_32_AVX2_ASM_EXEC + MLDSA_POLY_USE_HINT_32_EXEC [BYTES_LOADED_APPEND_CLAUSE] X86_SINGLE_STEP_TAC);; -let POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_32_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ @@ -1283,10 +1283,10 @@ let POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; h,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_32_avx2_asm_tmc POLY_USE_HINT_32_AVX2_ASM_SAFE THEN + X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_32_avx2_asm_tmc MLDSA_POLY_USE_HINT_32_SAFE THEN DISCHARGE_SAFETY_PROPERTY_TAC);; -let POLY_USE_HINT_32_AVX2_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_32_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ @@ -1309,5 +1309,5 @@ let POLY_USE_HINT_32_AVX2_ASM_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; h,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE POLY_USE_HINT_32_AVX2_ASM_NOIBT_SUBROUTINE_SAFE));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_USE_HINT_32_NOIBT_SUBROUTINE_SAFE));; diff --git a/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_88_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_88_avx2_asm.ml index d00e69c04d..3e8d3434b8 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_88_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_poly_use_hint_88_avx2_asm.ml @@ -103,7 +103,7 @@ let poly_use_hint_88_avx2_asm_mc = define_assert_from_elf let poly_use_hint_88_avx2_asm_tmc = define_trimmed "poly_use_hint_88_avx2_asm_tmc" poly_use_hint_88_avx2_asm_mc;; -let POLY_USE_HINT_88_AVX2_ASM_EXEC = +let MLDSA_POLY_USE_HINT_88_EXEC = X86_MK_CORE_EXEC_RULE poly_use_hint_88_avx2_asm_tmc;; (* ========================================================================= *) @@ -1224,7 +1224,7 @@ let DUPLITS_88 = map (fun (n,c) -> prove(mk_eq(mk_comb(`word:num->int256`, mk_nu (* Loop body (one iteration). *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_88_AVX2_ASM_BODY_BLOCK_TAC : tactic = +let MLDSA_POLY_USE_HINT_88_BODY_BLOCK_TAC : tactic = REPEAT STRIP_TAC THEN ENSURES_INIT_TAC "s0" THEN MP_TAC(SPECL [`a:int64`;`i:num`] ALIGNED_BLOCK) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN @@ -1255,7 +1255,7 @@ let POLY_USE_HINT_88_AVX2_ASM_BODY_BLOCK_TAC : tactic = `!b. i <= b /\ b < 32 ==> read(memory :> bytes256(word_add a (word(32*b)))) s0 = xb b`) (concl th) then MP_TAC(SPEC `b:num` th) else failwith "no") THEN ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN ACCEPT_TAC]; ALL_TAC] THEN - EVERY (map (fun n -> X86_STEPS_TAC POLY_USE_HINT_88_AVX2_ASM_EXEC [n] THEN SIMD_SIMPLIFY_TAC[] THEN ABBREV_BIG_TAC) (1--28)) THEN + EVERY (map (fun n -> X86_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC [n] THEN SIMD_SIMPLIFY_TAC[] THEN ABBREV_BIG_TAC) (1--28)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN TRY(REWRITE_TAC[ARITH_RULE `32 * (i + 1) = 32 * i + 32`] THEN CONV_TAC WORD_RULE) THEN @@ -1282,7 +1282,7 @@ let POLY_USE_HINT_88_AVX2_ASM_BODY_BLOCK_TAC : tactic = (* Block-function correctness. *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_88_AVX2_ASM_BLOCK_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_BLOCK_CORRECT = prove (`!a h xb yb pc. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, 0xdd) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) /\ @@ -1300,7 +1300,7 @@ let POLY_USE_HINT_88_AVX2_ASM_BLOCK_CORRECT = prove (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, MAP_EVERY X_GEN_TAC [`a:int64`;`h:int64`;`xb:num->int256`;`yb:num->int256`;`pc:num`] THEN REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; - fst POLY_USE_HINT_88_AVX2_ASM_EXEC] THEN + fst MLDSA_POLY_USE_HINT_88_EXEC] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN REWRITE_TAC[SOME_FLAGS] THEN ENSURES_WHILE_PUP_TAC `32` `pc + 0x52` `pc + 0xd7` `\i s. @@ -1326,18 +1326,18 @@ let POLY_USE_HINT_88_AVX2_ASM_BLOCK_CORRECT = prove [ REWRITE_TAC[MULT_CLAUSES; WORD_ADD_0] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC POLY_USE_HINT_88_AVX2_ASM_EXEC (1--17) THEN + X86_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC (1--17) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC DUPLITS_88 THEN REWRITE_TAC[ARITH_RULE `b < 0 <=> F`; LE_0] THEN ASM_REWRITE_TAC[] ; - POLY_USE_HINT_88_AVX2_ASM_BODY_BLOCK_TAC + MLDSA_POLY_USE_HINT_88_BODY_BLOCK_TAC ; - REPEAT STRIP_TAC THEN X86_SIM_TAC POLY_USE_HINT_88_AVX2_ASM_EXEC (1--1) + REPEAT STRIP_TAC THEN X86_SIM_TAC MLDSA_POLY_USE_HINT_88_EXEC (1--1) ; REWRITE_TAC[ARITH_RULE `32 <= b /\ b < 32 <=> F`] THEN ENSURES_INIT_TAC "s0" THEN - X86_STEPS_TAC POLY_USE_HINT_88_AVX2_ASM_EXEC (1--1) THEN + X86_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC (1--1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] ]);; @@ -1347,7 +1347,7 @@ let POLY_USE_HINT_88_AVX2_ASM_BLOCK_CORRECT = prove (* mldsa/src/native/x86_64/src/arith_native_x86_64.h *) (* ------------------------------------------------------------------------- *) -let POLY_USE_HINT_88_AVX2_ASM_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_CORRECT = prove (`!a h x y pc. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, 0xdd) (a, 1024) /\ nonoverlapping (a, 1024) (h, 1024) @@ -1445,7 +1445,7 @@ let POLY_USE_HINT_88_AVX2_ASM_CORRECT = prove ASM_ARITH_TAC ] ; - MATCH_MP_TAC POLY_USE_HINT_88_AVX2_ASM_BLOCK_CORRECT THEN + MATCH_MP_TAC MLDSA_POLY_USE_HINT_88_BLOCK_CORRECT THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`y:num->int32`;`b:num`;`k:num`] PACK8_LANE) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN @@ -1463,7 +1463,7 @@ let POLY_USE_HINT_88_AVX2_ASM_CORRECT = prove (* Public subroutine correctness (with return). *) (* ========================================================================= *) -let POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_NOIBT_SUBROUTINE_CORRECT = prove (`!a h x y pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, LENGTH poly_use_hint_88_avx2_asm_tmc) (a, 1024) /\ @@ -1488,9 +1488,9 @@ let POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT = prove val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 44)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_88_avx2_asm_tmc POLY_USE_HINT_88_AVX2_ASM_CORRECT);; + X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_88_avx2_asm_tmc MLDSA_POLY_USE_HINT_88_CORRECT);; -let POLY_USE_HINT_88_AVX2_ASM_SUBROUTINE_CORRECT = prove +let MLDSA_POLY_USE_HINT_88_SUBROUTINE_CORRECT = prove (`!a h x y pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ nonoverlapping (word pc, LENGTH poly_use_hint_88_avx2_asm_mc) (a, 1024) /\ @@ -1515,7 +1515,7 @@ let POLY_USE_HINT_88_AVX2_ASM_SUBROUTINE_CORRECT = prove val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 44)) (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, MAYCHANGE [memory :> bytes(a, 1024)])`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_CORRECT));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_USE_HINT_88_NOIBT_SUBROUTINE_CORRECT));; (* ========================================================================= *) (* Constant-time and memory safety proof. *) @@ -1531,18 +1531,18 @@ let full_spec,public_vars = mk_safety_spec ~keep_maychanges:true (assoc "mldsa_poly_use_hint_88_x86" subroutine_signatures) (REWRITE_RULE[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] - POLY_USE_HINT_88_AVX2_ASM_CORRECT) - POLY_USE_HINT_88_AVX2_ASM_EXEC;; + MLDSA_POLY_USE_HINT_88_CORRECT) + MLDSA_POLY_USE_HINT_88_EXEC;; -let POLY_USE_HINT_88_AVX2_ASM_SAFE = time prove +let MLDSA_POLY_USE_HINT_88_SAFE = time prove (full_spec, REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; SOME_FLAGS] THEN GEN_PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars ~tac_before_maychange_simp:NORMALIZE_AND_EXPAND_YMM_TAC - POLY_USE_HINT_88_AVX2_ASM_EXEC + MLDSA_POLY_USE_HINT_88_EXEC [BYTES_LOADED_APPEND_CLAUSE] X86_SINGLE_STEP_TAC);; -let POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_88_NOIBT_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ @@ -1565,10 +1565,10 @@ let POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; h,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_88_avx2_asm_tmc POLY_USE_HINT_88_AVX2_ASM_SAFE THEN + X86_PROMOTE_RETURN_NOSTACK_TAC poly_use_hint_88_avx2_asm_tmc MLDSA_POLY_USE_HINT_88_SAFE THEN DISCHARGE_SAFETY_PROPERTY_TAC);; -let POLY_USE_HINT_88_AVX2_ASM_SUBROUTINE_SAFE = time prove +let MLDSA_POLY_USE_HINT_88_SUBROUTINE_SAFE = time prove (`exists f_events. forall e a h pc stackpointer returnaddress. aligned 32 a /\ aligned 32 h /\ @@ -1591,5 +1591,5 @@ let POLY_USE_HINT_88_AVX2_ASM_SUBROUTINE_SAFE = time prove memaccess_inbounds e2 [a,1024; h,1024; stackpointer,8] [a,1024; stackpointer,8])) (\s s'. true)`, - MATCH_ACCEPT_TAC(ADD_IBT_RULE POLY_USE_HINT_88_AVX2_ASM_NOIBT_SUBROUTINE_SAFE));; + MATCH_ACCEPT_TAC(ADD_IBT_RULE MLDSA_POLY_USE_HINT_88_NOIBT_SUBROUTINE_SAFE));; diff --git a/scripts/lint b/scripts/lint index 27d4a91e34..4581e1e870 100755 --- a/scripts/lint +++ b/scripts/lint @@ -399,6 +399,80 @@ gh_group_start "Check HOL-Light imports" check-hol-light-imports gh_group_end +# Derive the theorem-name prefix from a proof routine's basename: +# - strip the platform suffix (_aarch64_asm or _avx2_asm) +# - uppercase +# The routine basename already carries the namespace (`mldsa_` for arithmetic, +# `keccak_` for the namespace-agnostic keccak proofs), so no fixup is needed. +theorem-prefix() +{ + local routine="$1" + local platform_suffix="$2" + local base="${routine%${platform_suffix}}" + echo "$base" | tr '[:lower:]' '[:upper:]' +} + +check-theorems() +{ + local success=true + for arch in aarch64 x86_64; do + local proofs_dir="$ROOT/proofs/hol_light/$arch/proofs" + local platform_suffix="_aarch64_asm" + [[ $arch == "x86_64" ]] && platform_suffix="_avx2_asm" + local proofs + proofs=$("$ROOT/proofs/hol_light/$arch/list_proofs.sh") + + for routine in $proofs; do + local file="$proofs_dir/${routine}.ml" + local prefix + local theorems + prefix=$(theorem-prefix "$routine" "$platform_suffix") + theorems=$("$ROOT/proofs/hol_light/$arch/list_thms.sh" "$file") + + # rej_uniform uses MEMSAFE in place of SAFE because no constant-time proof exists. + local safe="SAFE" + [[ ${routine} == mldsa_rej_uniform_* ]] && safe="MEMSAFE" + + local expected=( + "${prefix}_SUBROUTINE_CORRECT" + "${prefix}_SUBROUTINE_${safe}" + ) + if [[ $arch == "x86_64" ]]; then + expected+=( + "${prefix}_${safe}" + "${prefix}_NOIBT_SUBROUTINE_CORRECT" + "${prefix}_NOIBT_SUBROUTINE_${safe}" + ) + fi + + for theorem in "${expected[@]}"; do + if ! grep -qx "$theorem" <<<"$theorems"; then + gh_error "$file" "" "Missing theorem" "${file}: ${theorem} not found" + success=false + fi + done + + if grep -q "CHEAT_TAC" "$file"; then + gh_error "$file" "" "CHEAT_TAC detected" "${file}: uses CHEAT_TAC" + success=false + fi + done + done + + if $success; then + info "Check HOL-Light theorems" + gh_summary_success "Check HOL-Light theorems" + else + error "Check HOL-Light theorems" + SUCCESS=false + gh_summary_failure "Check HOL-Light theorems" + fi +} + +gh_group_start "Check HOL-Light theorems" +check-theorems +gh_group_end + if ! $SUCCESS; then if $IN_GITHUB_CONTEXT; then printf "%b%s%b\n" "${RED}" "The following checks failed, expand each for more details." "${NORMAL}"