From c3c75208030835cdba5e11635242b4b0ef0544ef Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sat, 24 Oct 2026 05:41:43 +0000 Subject: [PATCH 1/2] HOL-Light: Prepare SIMD simplifiers outside proof loops An instruction loop often applies the same arithmetic simplifier after each step. Building SIMD_SIMPLIFY_TAC inside the instruction callback rebuilds its rewrite conversion each time. The abbreviation variant also rebuilt that conversion for every selected register equation. Prepare the ARM/x86 step and SIMD tactics once before their loops. Move conversion construction and definition selection out of the abbreviation helper's per-fact callback. Still read local arithmetic equations from the current context: these change during execution. No converter-builder cache is needed. Prepared conversions capture the basic rewrite table; prepare again if it or the arithmetic rules change. Keep ordinary whole-context abbreviation, machine code and proof claims. Signed-off-by: Hanno Becker --- .../aarch64/proofs/mldsa_intt_aarch64_asm.ml | 8 +++++--- .../hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml | 8 +++++--- .../proofs/mldsa_pointwise_montgomery_aarch64_asm.ml | 8 +++++--- .../proofs/mldsa_poly_use_hint_32_aarch64_asm.ml | 8 +++++--- .../proofs/mldsa_poly_use_hint_88_aarch64_asm.ml | 8 +++++--- ...olyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml | 8 +++++--- ...olyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml | 8 +++++--- ...olyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml | 8 +++++--- .../proofs/mldsa_polyz_unpack_17_aarch64_asm.ml | 10 ++++++---- .../proofs/mldsa_polyz_unpack_19_aarch64_asm.ml | 10 ++++++---- proofs/hol_light/common/mldsa_specs.ml | 11 ++++++++--- proofs/hol_light/s2n_bignum_allowlist.txt | 1 + proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml | 10 ++++++---- proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml | 10 ++++++---- .../x86_64/proofs/mldsa_nttunpack_avx2_asm.ml | 10 ++++++---- .../x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_pointwise_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml | 10 ++++++---- .../x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_poly_decompose_88_avx2_asm.ml | 8 +++++--- .../x86_64/proofs/mldsa_poly_use_hint_32_avx2_asm.ml | 4 +++- .../x86_64/proofs/mldsa_poly_use_hint_88_avx2_asm.ml | 4 +++- .../x86_64/proofs/mldsa_polyz_unpack_17_avx2_asm.ml | 10 ++++++---- .../x86_64/proofs/mldsa_polyz_unpack_19_avx2_asm.ml | 10 ++++++---- 26 files changed, 133 insertions(+), 79 deletions(-) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml index a2dd8ee424..c7157bc570 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml @@ -813,9 +813,11 @@ let MLDSA_INTT_CORRECT = prove REPEAT STRIP_TAC THEN (*** Simulate all the way to the end, in effect unrolling loops ***) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_INTT_EXEC [n] THEN - SIMD_SIMPLIFY_ABBREV_TAC[arm_mldsa_barmul] []) - (1--2071) THEN + (let step = ARM_STEPS_TAC MLDSA_INTT_EXEC + and simplify = SIMD_SIMPLIFY_ABBREV_TAC[arm_mldsa_barmul] [] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--2071)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (*** Reverse the restructuring by splitting the 128-bit words up ***) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml index f187b963c4..c147b8317f 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml @@ -713,9 +713,11 @@ let MLDSA_NTT_CORRECT = prove (*** Simulate all the way to the end, in effect unrolling loops ***) - MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_NTT_EXEC [n] THEN - SIMD_SIMPLIFY_ABBREV_TAC[arm_mldsa_barmul] []) - (1--1959) THEN + (let step = ARM_STEPS_TAC MLDSA_NTT_EXEC + and simplify = SIMD_SIMPLIFY_ABBREV_TAC[arm_mldsa_barmul] [] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--1959)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN 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 37199f338a..3763312760 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 @@ -126,9 +126,11 @@ let MLDSA_POINTWISE_MONTGOMERY_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_MONTGOMERY_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) - (1--679) THEN + (let step = ARM_STEPS_TAC MLDSA_POINTWISE_MONTGOMERY_EXEC + and simplify = SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred'] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--679)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Split bytes128 -> bytes32 for output memory *) 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 35f931d5d0..1a5480dd9a 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 @@ -755,9 +755,11 @@ let MLDSA_POLY_USE_HINT_32_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 MLDSA_POLY_USE_HINT_32_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[]) - (1--878) THEN + (let step = ARM_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC + and simplify = SIMD_SIMPLIFY_TAC[] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--878)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Pick up the postcondition's input-bound antecedents 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 9283c5aa19..56f15dcf40 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 @@ -824,9 +824,11 @@ let MLDSA_POLY_USE_HINT_88_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 MLDSA_POLY_USE_HINT_88_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[]) - (1--1006) THEN + (let step = ARM_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC + and simplify = SIMD_SIMPLIFY_TAC[] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--1006)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Pick up the postcondition's input-bound antecedents 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 54479c5bc0..e9e09a664a 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 @@ -192,9 +192,11 @@ let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_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_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) - (1--1447) THEN + (let step = ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4_EXEC + and simplify = SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred'] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--1447)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Split bytes128 -> bytes32 for output memory *) 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 5b403c999d..9c2e7ad105 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 @@ -208,9 +208,11 @@ let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_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_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) - (1--1703) THEN + (let step = ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5_EXEC + and simplify = SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred'] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--1703)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Discard unused input memory (a, b) bytes128 reads *) 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 33493ea666..e2937fb8b0 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 @@ -240,9 +240,11 @@ let MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_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_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred']) - (1--2215) THEN + (let step = ARM_STEPS_TAC MLDSA_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7_EXEC + and simplify = SIMD_SIMPLIFY_TAC[arm_mldsa_pointwise_montred'] in + MAP_EVERY (fun n -> step [n] THEN + simplify) + (1--2215)) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Discard unused input memory (a, b) bytes128 reads *) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17_aarch64_asm.ml index 5065a0e0ae..b6776de38c 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17_aarch64_asm.ml @@ -279,10 +279,12 @@ let MLDSA_POLYZ_UNPACK_17_CORRECT = prove (0 -- 15) THEN (*** Symbolic execution with per-step simplification ***) - MAP_UNTIL_TARGET_PC (fun n -> - ARM_STEPS_TAC MLDSA_POLYZ_UNPACK_17_EXEC [n] THEN - SIMD_SIMPLIFY_TAC (map GSYM BASE_SIMPS_D18) THEN - SIMP_ZUNPACK_TAC 18 ZUNPACK17_CORRECT) 1 THEN + (let step = ARM_STEPS_TAC MLDSA_POLYZ_UNPACK_17_EXEC + and simplify = SIMD_SIMPLIFY_TAC (map GSYM BASE_SIMPS_D18) in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify THEN + SIMP_ZUNPACK_TAC 18 ZUNPACK17_CORRECT) 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19_aarch64_asm.ml index 62569dd8a1..9921d0aecd 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19_aarch64_asm.ml @@ -196,10 +196,12 @@ let MLDSA_POLYZ_UNPACK_19_CORRECT = prove (0 -- 15) THEN (*** Symbolic execution with per-step simplification ***) - MAP_UNTIL_TARGET_PC (fun n -> - ARM_STEPS_TAC MLDSA_POLYZ_UNPACK_19_EXEC [n] THEN - SIMD_SIMPLIFY_TAC (map GSYM BASE_SIMPS_D20) THEN - SIMP_ZUNPACK_TAC 20 ZUNPACK19_CORRECT) 1 THEN + (let step = ARM_STEPS_TAC MLDSA_POLYZ_UNPACK_19_EXEC + and simplify = SIMD_SIMPLIFY_TAC (map GSYM BASE_SIMPS_D20) in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify THEN + SIMP_ZUNPACK_TAC 20 ZUNPACK19_CORRECT) 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/common/mldsa_specs.ml b/proofs/hol_light/common/mldsa_specs.ml index 7bbd6f7d70..6392a3291b 100644 --- a/proofs/hol_light/common/mldsa_specs.ml +++ b/proofs/hol_light/common/mldsa_specs.ml @@ -11,6 +11,7 @@ needs "Library/words.ml";; needs "Library/isum.ml";; +needs "s2n_bignum/common/misc.ml";; (* ------------------------------------------------------------------------- *) (* The pure forms of forward and inverse NTT with no reordering. *) @@ -1163,6 +1164,8 @@ let rec LOCAL_CONGBOUND_RULE lfn asms = (* ------------------------------------------------------------------------- *) (* Simplify SIMD cruft and fold relevant definitions when encountered. *) (* The ABBREV form also introduces abbreviations for relevant subterms. *) +(* Prepare a tactic once outside an instruction loop and reuse that value. *) +(* Its conversion captures the basic rewrite rules at preparation time. *) (* ------------------------------------------------------------------------- *) let SIMD_SIMPLIFY_CONV unfold_defs = @@ -1196,13 +1199,15 @@ let SIMD_SIMPLIFY_ABBREV_TAC = can (term_match [] `read X (s:x86state):int256 = whatever`) in let simdable tm = arm_simdable tm || x86_simdable tm in fun unfold_defs unfold_aux -> + let simplify = RAND_CONV + (SIMD_SIMPLIFY_CONV (unfold_defs @ unfold_aux)) in + let local_definition = is_local_definition unfold_defs in let pats = map (lhand o snd o strip_forall o concl) unfold_defs in let pam t = exists (fun p -> can(term_match [] p) t) pats in let ttac th (asl,w) = - let th' = CONV_RULE(RAND_CONV - (SIMD_SIMPLIFY_CONV (unfold_defs @ unfold_aux))) th in + let th' = CONV_RULE simplify th in let asms = - map snd (filter (is_local_definition unfold_defs o concl o snd) asl) in + map snd (filter (local_definition o concl o snd) asl) in let th'' = GEN_REWRITE_RULE (RAND_CONV o TOP_DEPTH_CONV) asms th' in let tms = sort free_in (find_terms pam (rand(concl th''))) in (MP_TAC th'' THEN MAP_EVERY AUTO_ABBREV_TAC tms THEN DISCH_TAC) (asl,w) in diff --git a/proofs/hol_light/s2n_bignum_allowlist.txt b/proofs/hol_light/s2n_bignum_allowlist.txt index e6766fc0df..616704536a 100644 --- a/proofs/hol_light/s2n_bignum_allowlist.txt +++ b/proofs/hol_light/s2n_bignum_allowlist.txt @@ -17,6 +17,7 @@ arm/proofs/base.ml arm/proofs/consttime.ml common/consttime.ml common/int_linear.ml +common/misc.ml riscv/proofs/base.ml riscv/proofs/consttime.ml x86/proofs/base.ml diff --git a/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml index 77bc371f78..f551cbc433 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml @@ -4394,11 +4394,13 @@ let MLDSA_INTT_CORRECT = prove (*** Execute the inverse NTT simulation ***) - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_INTT_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_ABBREV_TAC[mldsa_montmul] + (let step = X86_STEPS_TAC MLDSA_INTT_TMC_EXEC + and simplify = SIMD_SIMPLIFY_ABBREV_TAC[mldsa_montmul] [WORD_ADD_MLDSA_MONTMUL; - WORD_ADD_MLDSA_MONTMUL_ALT; WORD_SUB_MLDSA_MONTMUL]) - 1 THEN + WORD_ADD_MLDSA_MONTMUL_ALT; WORD_SUB_MLDSA_MONTMUL] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (**** Reverse the restructuring by splitting the 256-bit words up ***) diff --git a/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml index fc6a7fb527..c04d3e427d 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml @@ -4489,11 +4489,13 @@ let MLDSA_NTT_CORRECT = prove (*** Do the entire simulation (very slow!) ****) - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_NTT_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_ABBREV_TAC[mldsa_montmul] + (let step = X86_STEPS_TAC MLDSA_NTT_TMC_EXEC + and simplify = SIMD_SIMPLIFY_ABBREV_TAC[mldsa_montmul] [WORD_ADD_MLDSA_MONTMUL; - WORD_ADD_MLDSA_MONTMUL_ALT; WORD_SUB_MLDSA_MONTMUL]) - 1 THEN + WORD_ADD_MLDSA_MONTMUL_ALT; WORD_SUB_MLDSA_MONTMUL] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (**** Reverse the restructuring by splitting the 256-bit words up ***) diff --git a/proofs/hol_light/x86_64/proofs/mldsa_nttunpack_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_nttunpack_avx2_asm.ml index 7c124bdda8..07b64f01e3 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_nttunpack_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_nttunpack_avx2_asm.ml @@ -458,10 +458,12 @@ let MLDSA_NTTUNPACK_CORRECT = prove REWRITE_TAC[GSYM BYTES256_WBYTES] THEN STRIP_TAC THEN (* Step through each instruction with SIMD simplification *) - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_NTTUNPACK_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_NTTUNPACK_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN (* Extract all the memory writes from the execution *) diff --git a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml index 1146a28069..1afc61f43c 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml @@ -331,9 +331,11 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove CONV_TAC INT_REDUCE_CONV]; ALL_TAC] THEN - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_POINTWISE_ACC_L4_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_POINTWISE_ACC_L4_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml index 77151bca60..d03039428e 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml @@ -358,9 +358,11 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove CONV_TAC INT_REDUCE_CONV]; ALL_TAC] THEN - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_POINTWISE_ACC_L5_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_POINTWISE_ACC_L5_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml index 26881b4b0d..4f93f956ef 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml @@ -414,9 +414,11 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove CONV_TAC INT_REDUCE_CONV]; ALL_TAC] THEN - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_POINTWISE_ACC_L7_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_POINTWISE_ACC_L7_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_avx2_asm.ml index 5c9b57c335..f8dcb7bb4d 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_pointwise_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_pointwise_avx2_asm.ml @@ -321,9 +321,11 @@ let MLDSA_POINTWISE_CORRECT = prove ALL_TAC] THEN (* Execute all 533 instructions with SIMD simplification *) - MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLDSA_POINTWISE_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_POINTWISE_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[mldsa_pointwise_montred] in + MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN 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 74497e86aa..b64cf9b9a2 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 @@ -337,10 +337,12 @@ let MLDSA_POLY_CADDQ_CORRECT = time prove ASM_REWRITE_TAC[WORD_ADD_0] THEN DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_POLY_CADDQ_TMC_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[mldsa_caddq]) - 1 THEN + (let step = X86_STEPS_TAC MLDSA_POLY_CADDQ_TMC_EXEC + and simplify = SIMD_SIMPLIFY_TAC[mldsa_caddq] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify) + 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o CONV_RULE(SIMD_SIMPLIFY_CONV[mldsa_caddq]) o 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 50dec3f938..76c351b071 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 @@ -1145,9 +1145,11 @@ let MLDSA_POLY_DECOMPOSE_32_CORRECT = prove( ASM_REWRITE_TAC[WORD_ADD_0] THEN DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_32_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[decompose32_a1; decompose32_a0]) 1 THEN + (let step = X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_32_EXEC + and simplify = SIMD_SIMPLIFY_TAC[decompose32_a1; decompose32_a0] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify) 1) 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 REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o 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 4a00f126b1..ded8a7abc5 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 @@ -1145,9 +1145,11 @@ let MLDSA_POLY_DECOMPOSE_88_CORRECT = prove( ASM_REWRITE_TAC[WORD_ADD_0] THEN DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN STRIP_TAC THEN - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_88_EXEC [n] THEN - SIMD_SIMPLIFY_TAC[decompose88_a1; decompose88_a0]) 1 THEN + (let step = X86_STEPS_TAC MLDSA_POLY_DECOMPOSE_88_EXEC + and simplify = SIMD_SIMPLIFY_TAC[decompose88_a1; decompose88_a0] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify) 1) 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 REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o 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 73a8e8fda0..c7908b939d 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 @@ -982,7 +982,9 @@ let MLDSA_POLY_USE_HINT_32_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 MLDSA_POLY_USE_HINT_32_EXEC [n] THEN SIMD_SIMPLIFY_TAC[]) (1--24)) THEN + (let step = X86_STEPS_TAC MLDSA_POLY_USE_HINT_32_EXEC + and simplify = SIMD_SIMPLIFY_TAC[] in + EVERY (map (fun n -> step [n] THEN simplify) (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 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 8a9166b238..541bd7b037 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 @@ -1273,7 +1273,9 @@ let MLDSA_POLY_USE_HINT_88_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 MLDSA_POLY_USE_HINT_88_EXEC [n] THEN SIMD_SIMPLIFY_TAC[] THEN ABBREV_BIG_TAC) (1--28)) THEN + (let step = X86_STEPS_TAC MLDSA_POLY_USE_HINT_88_EXEC + and simplify = SIMD_SIMPLIFY_TAC[] in + EVERY (map (fun n -> step [n] THEN simplify 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 diff --git a/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_17_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_17_avx2_asm.ml index d5fa05bb89..33a0a6271d 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_17_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_17_avx2_asm.ml @@ -751,10 +751,12 @@ let MLDSA_POLYZ_UNPACK_17_CORRECT = prove (*** Symbolic execution: simplify each block's lanes, then fold the just- ***) (*** computed YMM0 into atomic zunpack17 lanes before it is stored so the ***) (*** store and subsequent steps stay cheap. ***) - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_POLYZ_UNPACK_17_EXEC [n] THEN - SIMD_SIMPLIFY_TAC [] THEN - ZUNPACK17_FOLD_TAC) 1 THEN + (let step = X86_STEPS_TAC MLDSA_POLYZ_UNPACK_17_EXEC + and simplify = SIMD_SIMPLIFY_TAC [] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify THEN + ZUNPACK17_FOLD_TAC) 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_19_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_19_avx2_asm.ml index a568000208..af5b0ddaad 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_19_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_polyz_unpack_19_avx2_asm.ml @@ -753,10 +753,12 @@ let MLDSA_POLYZ_UNPACK_19_CORRECT = prove (*** Symbolic execution: simplify each block's lanes, then fold the just- ***) (*** computed YMM0 into atomic zunpack19 lanes before it is stored so the ***) (*** store and subsequent steps stay cheap. ***) - MAP_UNTIL_TARGET_PC (fun n -> - X86_STEPS_TAC MLDSA_POLYZ_UNPACK_19_EXEC [n] THEN - SIMD_SIMPLIFY_TAC [] THEN - ZUNPACK19_FOLD_TAC) 1 THEN + (let step = X86_STEPS_TAC MLDSA_POLYZ_UNPACK_19_EXEC + and simplify = SIMD_SIMPLIFY_TAC [] in + MAP_UNTIL_TARGET_PC (fun n -> + step [n] THEN + simplify THEN + ZUNPACK19_FOLD_TAC) 1) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN From fd0490947b910e9cc91c35a7d4d1af64b4d8c700 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 22 Oct 2026 12:37:58 +0000 Subject: [PATCH 2/2] HOL-Light: Drop unused context during integer closure After the NTT output congruence has been reduced to a real polynomial, REAL_INTEGER_TAC proves integer closure from the expression's structure. It does not consult context facts, but its recursive subgoals still carried the large execution context. Discard that context immediately before the four ARM/x86 NTT and INTT integer-closure calls. Leave instruction reasoning, congruence rewriting, output bounds and HOL Light's tactic unchanged. Signed-off-by: Hanno Becker --- proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml | 4 +++- proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml | 4 +++- proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml | 4 +++- proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml | 4 +++- 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml index c7157bc570..a238f135f7 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml @@ -853,7 +853,9 @@ let MLDSA_INTT_CORRECT = prove REWRITE_TAC[INT_REM_EQ] THEN REWRITE_TAC[REAL_INT_CONGRUENCE; INT_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[GSYM REAL_OF_INT_CLAUSES] THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN REAL_INTEGER_TAC; + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + (* Integer closure needs no execution assumptions. *) + POP_ASSUM_LIST(K REAL_INTEGER_TAC); MATCH_MP_TAC(INT_ARITH `l':int <= l /\ u <= u' ==> l <= x /\ x <= u ==> l' <= x /\ x <= u'`) THEN diff --git a/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml index c147b8317f..f6704c7163 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml @@ -755,7 +755,9 @@ let MLDSA_NTT_CORRECT = prove REWRITE_TAC[INT_REM_EQ] THEN REWRITE_TAC[REAL_INT_CONGRUENCE; INT_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[GSYM REAL_OF_INT_CLAUSES] THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN REAL_INTEGER_TAC; + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + (* Integer closure needs no execution assumptions. *) + POP_ASSUM_LIST(K REAL_INTEGER_TAC); MATCH_MP_TAC(INT_ARITH `l':int <= l /\ u <= u' ==> l <= x /\ x <= u ==> l' <= x /\ x <= u'`) THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml index f551cbc433..96b7aadecc 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml @@ -4458,7 +4458,9 @@ let MLDSA_INTT_CORRECT = prove REWRITE_TAC[INT_REM_EQ] THEN REWRITE_TAC[REAL_INT_CONGRUENCE; INT_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[GSYM REAL_OF_INT_CLAUSES] THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN REAL_INTEGER_TAC; + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + (* Integer closure needs no execution assumptions. *) + POP_ASSUM_LIST(K REAL_INTEGER_TAC); MATCH_MP_TAC(INT_ARITH `l':int <= l /\ u <= u' ==> l <= x /\ x <= u ==> l' <= x /\ x <= u'`) THEN diff --git a/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml index c04d3e427d..5e604b4299 100644 --- a/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml +++ b/proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml @@ -4553,7 +4553,9 @@ let MLDSA_NTT_CORRECT = prove REWRITE_TAC[INT_REM_EQ] THEN REWRITE_TAC[REAL_INT_CONGRUENCE; INT_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[GSYM REAL_OF_INT_CLAUSES] THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN REAL_INTEGER_TAC; + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + (* Integer closure needs no execution assumptions. *) + POP_ASSUM_LIST(K REAL_INTEGER_TAC); MATCH_MP_TAC(INT_ARITH `l':int <= l /\ u <= u' ==> l <= x /\ x <= u ==> l' <= x /\ x <= u'`) THEN