Skip to content

HOL-Light: Avoid repeated work in proof loops #1962

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 1 commit into from
Oct 26, 2026
Merged

HOL-Light: Avoid repeated work in proof loops #1962

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 6 additions & 4 deletions proofs/hol_light/aarch64/proofs/mlkem_intt_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -655,9 +655,9 @@ let MLKEM_INTT_CORRECT = prove

(*** Simulate all the way to the end, in effect unrolling loops ***)

MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC MLKEM_INTT_EXEC [n] THEN
(SIMD_SIMPLIFY_ABBREV_TAC[barred; barmul] []))
1 THEN
(let step = ARM_STEPS_TAC MLKEM_INTT_EXEC
and simplify = SIMD_SIMPLIFY_ABBREV_TAC[barred; barmul] [] 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 128-bit words up ***)
Expand Down Expand Up @@ -695,7 +695,9 @@ let MLKEM_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
9 changes: 6 additions & 3 deletions proofs/hol_light/aarch64/proofs/mlkem_ntt_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -590,8 +590,9 @@ let MLKEM_NTT_CORRECT = prove

(*** Simulate all the way to the end, in effect unrolling loops ***)

MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC MLKEM_NTT_EXEC [n] THEN
(SIMD_SIMPLIFY_ABBREV_TAC[barmul] [])) 1 THEN
(let step = ARM_STEPS_TAC MLKEM_NTT_EXEC
and simplify = SIMD_SIMPLIFY_ABBREV_TAC[barmul] [] 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 128-bit words up ***)
Expand Down Expand Up @@ -630,7 +631,9 @@ let MLKEM_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
5 changes: 3 additions & 2 deletions proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,9 @@ let MLKEM_POLY_MULCACHE_COMPUTE_CORRECT = prove(poly_mulcache_compute_GOAL,
Note that we simplify eagerly after every step.
This reduces the proof time *)
REPEAT STRIP_TAC THEN
MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC poly_mulcache_compute_EXEC [n] THEN
(SIMD_SIMPLIFY_TAC [barmul])) 1 THEN
(let step = ARM_STEPS_TAC poly_mulcache_compute_EXEC
and simplify = SIMD_SIMPLIFY_TAC [barmul] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN
ENSURES_FINAL_STATE_TAC THEN
REPEAT CONJ_TAC THEN
ASM_REWRITE_TAC [] THEN
Expand Down
5 changes: 3 additions & 2 deletions proofs/hol_light/aarch64/proofs/mlkem_poly_reduce_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -224,8 +224,9 @@ let MLKEM_POLY_REDUCE_CORRECT = prove

(*** Do a full simulation with no breakpoints, unrolling the loop ***)

MAP_UNTIL_TARGET_PC (fun n ->
ARM_STEPS_TAC MLKEM_POLY_REDUCE_EXEC [n] THEN (SIMD_SIMPLIFY_TAC [barred])) 1 THEN
(let step = ARM_STEPS_TAC MLKEM_POLY_REDUCE_EXEC
and simplify = SIMD_SIMPLIFY_TAC [barred] 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 128-bit words up ***)
Expand Down
5 changes: 3 additions & 2 deletions proofs/hol_light/aarch64/proofs/mlkem_poly_tomont_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,9 @@ let MLKEM_POLY_TOMONT_CORRECT = prove(POLY_TOMONT_GOAL,
Note that we simplify eagerly after every step.
This reduces the proof time *)
STRIP_TAC THEN
MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC POLY_TOMONT_EXEC [n] THEN
(SIMD_SIMPLIFY_TAC [barmul])) 1 THEN
(let step = ARM_STEPS_TAC POLY_TOMONT_EXEC
and simplify = SIMD_SIMPLIFY_TAC [barmul] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN
ENSURES_FINAL_STATE_TAC THEN
REPEAT CONJ_TAC THEN
ASM_REWRITE_TAC [] THEN
Expand Down
6 changes: 4 additions & 2 deletions ...fs/hol_light/aarch64/proofs/mlkem_polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,8 +369,10 @@ let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT = prove(poly_basemul_
Note that we simplify eagerly after every step.
This reduces the proof time *)
REPEAT STRIP_TAC THEN
MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k2_EXEC [n] THEN
(SIMD_SIMPLIFY_TAC [montred])) 1 THEN
(let step =
ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k2_EXEC
and simplify = SIMD_SIMPLIFY_TAC [montred] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV)) THEN STRIP_TAC THEN
Expand Down
6 changes: 4 additions & 2 deletions ...fs/hol_light/aarch64/proofs/mlkem_polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,8 +433,10 @@ let basemul3_odd = define
Note that we simplify eagerly after every step.
This reduces the proof time *)
REPEAT STRIP_TAC THEN
MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k3_EXEC [n] THEN
(SIMD_SIMPLIFY_TAC [montred])) 1 THEN
(let step =
ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k3_EXEC
and simplify = SIMD_SIMPLIFY_TAC [montred] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV)) THEN STRIP_TAC THEN
Expand Down
6 changes: 4 additions & 2 deletions ...fs/hol_light/aarch64/proofs/mlkem_polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -498,8 +498,10 @@ let basemul4_odd = define
Note that we simplify eagerly after every step.
This reduces the proof time *)
REPEAT STRIP_TAC THEN
MAP_UNTIL_TARGET_PC (fun n -> ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k4_EXEC [n] THEN
(SIMD_SIMPLIFY_TAC [montred])) 1 THEN
(let step =
ARM_STEPS_TAC poly_basemul_acc_montgomery_cached_k4_EXEC
and simplify = SIMD_SIMPLIFY_TAC [montred] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV)) THEN STRIP_TAC THEN
Expand Down
11 changes: 8 additions & 3 deletions proofs/hol_light/common/mlkem_specs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,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 @@ -1209,6 +1210,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 @@ -1242,13 +1245,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 @@ -15,5 +15,6 @@

arm/proofs/base.ml
arm/proofs/consttime.ml
common/misc.ml
x86/proofs/base.ml
x86/proofs/consttime.ml
13 changes: 8 additions & 5 deletions proofs/hol_light/x86_64/proofs/mlkem_intt_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1128,10 +1128,11 @@ let MLKEM_INTT_CORRECT = prove
CONV_TAC(LAND_CONV(READ_MEMORY_SPLIT_CONV 2)) THEN
CONV_TAC(LAND_CONV WORD_REDUCE_CONV) THEN STRIP_TAC THEN

MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_INTT_TMC_EXEC [n] THEN
SIMD_SIMPLIFY_ABBREV_TAC[ntt_montmul; barred_x86]
[ntt_montmul_add; ntt_montmul_sub])
1 THEN
(let step = X86_STEPS_TAC MLKEM_INTT_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_ABBREV_TAC[ntt_montmul; barred_x86]
[ntt_montmul_add; ntt_montmul_sub] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN

Expand Down Expand Up @@ -1201,7 +1202,9 @@ let MLKEM_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/x86_64/proofs/mlkem_ntt_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1140,9 +1140,11 @@ let MLKEM_NTT_CORRECT = prove
CONV_TAC(LAND_CONV(READ_MEMORY_SPLIT_CONV 2)) THEN
CONV_TAC(LAND_CONV WORD_REDUCE_CONV) THEN STRIP_TAC THEN

MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_NTT_TMC_EXEC [n] THEN
SIMD_SIMPLIFY_ABBREV_TAC[ntt_montmul] [ntt_montmul_add; ntt_montmul_sub])
1 THEN
(let step = X86_STEPS_TAC MLKEM_NTT_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_ABBREV_TAC[ntt_montmul]
[ntt_montmul_add; ntt_montmul_sub] 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
Expand Down Expand Up @@ -1209,7 +1211,9 @@ let MLKEM_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
6 changes: 3 additions & 3 deletions proofs/hol_light/x86_64/proofs/mlkem_nttfrombytes_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,9 +415,9 @@ let MLKEM_NTTFROMBYTES_CORRECT = prove(

(*** Simulate and simplify ***)

MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC mlkem_frombytes_TMC_EXEC [n] THEN
SIMD_SIMPLIFY_TAC[])
1 THEN
(let step = X86_STEPS_TAC mlkem_frombytes_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

(*** Final reasoning ***)
Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/x86_64/proofs/mlkem_ntttobytes_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,10 +353,12 @@ let MLKEM_NTTTOBYTES_CORRECT = prove(
CONV_TAC(LAND_CONV BYTES_EQ_NUM_OF_WORDLIST_EXPAND_CONV) THEN
REWRITE_TAC[GSYM BYTES256_WBYTES] THEN STRIP_TAC THEN

MAP_UNTIL_TARGET_PC (fun n ->
X86_STEPS_TAC mlkem_tobytes_TMC_EXEC [n] THEN
SIMD_SIMPLIFY_TAC[])
1 THEN
(let step = X86_STEPS_TAC mlkem_tobytes_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

REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o
Expand Down
10 changes: 6 additions & 4 deletions proofs/hol_light/x86_64/proofs/mlkem_nttunpack_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,10 +350,12 @@ let MLKEM_NTTUNPACK_CORRECT = prove(
CONV_TAC(LAND_CONV BYTES_EQ_NUM_OF_WORDLIST_EXPAND_CONV) THEN
REWRITE_TAC[GSYM BYTES256_WBYTES] THEN STRIP_TAC THEN

MAP_UNTIL_TARGET_PC (fun n ->
X86_STEPS_TAC mlkem_unpack_TMC_EXEC [n] THEN
SIMD_SIMPLIFY_TAC[])
1 THEN
(let step = X86_STEPS_TAC mlkem_unpack_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

REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o
Expand Down
11 changes: 8 additions & 3 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d10_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -856,9 +856,14 @@ let MLKEM_POLY_COMPRESS_D10_CORRECT = prove(
ALL_TAC] THEN

(*** Symbolic execution ***)
MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_COMPRESS_D10_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC
[GSYM WORD_JOIN_AND_TYBIT0; GSYM WORD_JOIN_NOT_TYBIT0; compress_d10_avx2;
GSYM DECOMPRESS_MULADD_1024_JOIN; GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN); GSYM WORD_ZX_128_256_128; GSYM WORD_64_SUB_8_8_JOIN_16]) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_COMPRESS_D10_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
[GSYM WORD_JOIN_AND_TYBIT0; GSYM WORD_JOIN_NOT_TYBIT0;
compress_d10_avx2; GSYM DECOMPRESS_MULADD_1024_JOIN;
GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN);
GSYM WORD_ZX_128_256_128; GSYM WORD_64_SUB_8_8_JOIN_16] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN

Expand Down
12 changes: 9 additions & 3 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d11_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -926,9 +926,15 @@ let MLKEM_POLY_COMPRESS_D11_CORRECT = prove(
ALL_TAC] THEN

(*** Symbolic execution ***)
MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_COMPRESS_D11_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC
[GSYM WORD_SUBWORD_USHR_HIGH_64; GSYM WORD_SUBWORD_USHR_64; GSYM WORD_JOIN_AND_TYBIT0; GSYM WORD_JOIN_NOT_TYBIT0; compress_d11_avx2;
GSYM DECOMPRESS_MULADD_2048_JOIN; GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN); GSYM WORD_ZX_128_256_128; GSYM WORD_64_SUB_8_8_JOIN_16]) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_COMPRESS_D11_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
[GSYM WORD_SUBWORD_USHR_HIGH_64; GSYM WORD_SUBWORD_USHR_64;
GSYM WORD_JOIN_AND_TYBIT0; GSYM WORD_JOIN_NOT_TYBIT0;
compress_d11_avx2; GSYM DECOMPRESS_MULADD_2048_JOIN;
GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN);
GSYM WORD_ZX_128_256_128; GSYM WORD_64_SUB_8_8_JOIN_16] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN

Expand Down
16 changes: 11 additions & 5 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d4_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -405,11 +405,17 @@ let MLKEM_POLY_COMPRESS_D4_CORRECT = prove(
ALL_TAC] THEN

(*** Symbolic execution ***)
MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_COMPRESS_D4_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC
([compress_d4_avx2_alt]
@ map GSYM [BIT_15_ZX_4_16; MIN_ZX_4_16; GSYM ADD_ASSOC; (CONV_RULE NUM_REDUCE_CONV BYTES256_JOIN);
WORD_VAL_4_8; WORD_ZX_ZX_4_8_32; MULADD_16_1_JOIN; BIT_31_ZX_8_32; BIT_15_ZX_8_32;
WORD_SUBWORD_8_0_16; BIT_15_ZX_8_16; MIN_ZX_8_16; WORD_VAL])) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_COMPRESS_D4_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
([compress_d4_avx2_alt]
@ map GSYM
[BIT_15_ZX_4_16; MIN_ZX_4_16; GSYM ADD_ASSOC;
(CONV_RULE NUM_REDUCE_CONV BYTES256_JOIN);
WORD_VAL_4_8; WORD_ZX_ZX_4_8_32; MULADD_16_1_JOIN;
BIT_31_ZX_8_32; BIT_15_ZX_8_32; WORD_SUBWORD_8_0_16;
BIT_15_ZX_8_16; MIN_ZX_8_16; WORD_VAL]) in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

REWRITE_COMPRESS THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
Expand Down
30 changes: 17 additions & 13 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d5_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -657,19 +657,23 @@ let MLKEM_POLY_COMPRESS_D5_CORRECT = prove(

(*** Symbolic execution ***)

MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_COMPRESS_D5_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC
([compress_d5_avx2_alt;
GSYM DECOMPRESS_MULADD_D5;
GSYM MULADD_32_1_JOIN; GSYM MULADD_1024_1_JOIN;
GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN);
GSYM WORD_ZX_128_256_128;
GSYM WORD_64_SUB_8_8_JOIN_16;
GSYM WORD_ZX_WORD_VAL_5_32;
GSYM BIT_15_ZX_5_16;
GSYM BIT_31_ZX_10_32;
GSYM BIT_15_ZX_10_32;
GSYM MIN_ZX_5_16; GSYM WORD_SUBWORD_ZX;
ADD_ASSOC; GSYM (CONV_RULE NUM_REDUCE_CONV BYTES256_JOIN)])) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_COMPRESS_D5_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
[compress_d5_avx2_alt;
GSYM DECOMPRESS_MULADD_D5;
GSYM MULADD_32_1_JOIN; GSYM MULADD_1024_1_JOIN;
GSYM (CONV_RULE NUM_REDUCE_CONV BYTES128_JOIN);
GSYM WORD_ZX_128_256_128;
GSYM WORD_64_SUB_8_8_JOIN_16;
GSYM WORD_ZX_WORD_VAL_5_32;
GSYM BIT_15_ZX_5_16;
GSYM BIT_31_ZX_10_32;
GSYM BIT_15_ZX_10_32;
GSYM MIN_ZX_5_16; GSYM WORD_SUBWORD_ZX;
ADD_ASSOC;
GSYM (CONV_RULE NUM_REDUCE_CONV BYTES256_JOIN)] in
MAP_UNTIL_TARGET_PC (fun n -> step [n] THEN simplify) 1) THEN

DISCARD_MATCHING_ASSUMPTIONS [`read ymm s = (t : 256 word)`] THEN
REWRITE_COMPRESS THEN
Expand Down
9 changes: 7 additions & 2 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_decompress_d10_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -464,8 +464,13 @@ let MLKEM_POLY_DECOMPRESS_D10_CORRECT = prove(
THENL [ASM_REWRITE_TAC [LENGTH_SUB_LIST] THEN NUM_REDUCE_TAC; ALL_TAC]) (0 -- 15) THEN

(*** Symbolic execution ***)
MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_DECOMPRESS_D10_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC (map GSYM (BASE_SIMPS_D10 @ WORD_MUL_2EXP @ WORD_MUL_2EXP_3329))
THEN SIMP_DECOMPRESS_D10_TAC) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_DECOMPRESS_D10_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
(map GSYM
(BASE_SIMPS_D10 @ WORD_MUL_2EXP @ WORD_MUL_2EXP_3329)) in
MAP_UNTIL_TARGET_PC (fun n ->
step [n] THEN simplify THEN SIMP_DECOMPRESS_D10_TAC) 1) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN

(* Unwrap assumptions *)
Expand Down
9 changes: 7 additions & 2 deletions proofs/hol_light/x86_64/proofs/mlkem_poly_decompress_d11_avx2_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -548,8 +548,13 @@ let MLKEM_POLY_DECOMPRESS_D11_CORRECT = prove(
THENL [ASM_REWRITE_TAC [LENGTH_SUB_LIST] THEN NUM_REDUCE_TAC; ALL_TAC]) (0 -- 15) THEN

(*** Symbolic execution ***)
MAP_UNTIL_TARGET_PC (fun n -> X86_STEPS_TAC MLKEM_POLY_DECOMPRESS_D11_TMC_EXEC [n] THEN SIMD_SIMPLIFY_TAC (map GSYM (BASE_SIMPS_D11 @ WORD_MUL_2EXP @ WORD_MUL_2EXP_3329))
THEN SIMP_DECOMPRESS_D11_TAC) 1 THEN
(let step = X86_STEPS_TAC MLKEM_POLY_DECOMPRESS_D11_TMC_EXEC
and simplify =
SIMD_SIMPLIFY_TAC
(map GSYM
(BASE_SIMPS_D11 @ WORD_MUL_2EXP @ WORD_MUL_2EXP_3329)) in
MAP_UNTIL_TARGET_PC (fun n ->
step [n] THEN simplify THEN SIMP_DECOMPRESS_D11_TAC) 1) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN

(* Unwrap assumptions *)
Expand Down
Loading
Loading