Skip to content

HOL-Light: Tweaks for better proof performance #1499

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mkannwischer merged 2 commits into from
Oct 26, 2026
Merged

HOL-Light: Tweaks for better proof performance #1499

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c3c7520
HOL-Light: Prepare SIMD simplifiers outside proof loops
hanno-becker Oct 24, 2026
fd04909
HOL-Light: Drop unused context during integer closure
hanno-becker Oct 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 8 additions & 4 deletions proofs/hol_light/aarch64/proofs/mldsa_intt_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ***)
Expand Down Expand Up @@ -851,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
Expand Down
12 changes: 8 additions & 4 deletions proofs/hol_light/aarch64/proofs/mldsa_ntt_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -753,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
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_pointwise_montgomery_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/aarch64/proofs/mldsa_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
11 changes: 8 additions & 3 deletions proofs/hol_light/common/mldsa_specs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions proofs/hol_light/s2n_bignum_allowlist.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 9 additions & 5 deletions proofs/hol_light/x86_64/proofs/mldsa_intt_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ***)
Expand Down Expand Up @@ -4456,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
Expand Down
14 changes: 9 additions & 5 deletions proofs/hol_light/x86_64/proofs/mldsa_ntt_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ***)
Expand Down Expand Up @@ -4551,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
Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/x86_64/proofs/mldsa_nttunpack_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/x86_64/proofs/mldsa_pointwise_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/x86_64/proofs/mldsa_poly_caddq_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 5 additions & 3 deletions proofs/hol_light/x86_64/proofs/mldsa_poly_decompose_32_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading