Skip to content

Commit 019df9b

Browse files
hanno-beckerhanno-becker
committed
HOL-Light: Avoid hardcoded lengths in HOL-Light proof scripts
Previously, the HOL-Light proof scripts contained various hardcoded constants related to the length of the code under proof, as well as the lengths of preamble and postamble (stack spill and restore). This commit replaces those hardcoded numerals with symbolic definitions. As a result, SLOTHY re-optimization should now no longer require a proof script change beyond the update of the byte code which is done by `autogen` already. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 18b4bd7 commit 019df9b

10 files changed

+229
-28
lines changed

‎proofs/hol_light/arm/proofs/mlkem_intt.ml‎

Lines changed: 33 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -547,6 +547,32 @@ let mlkem_intt_mc = define_assert_from_elf
547547

548548
let MLKEM_INTT_EXEC = ARM_MK_EXEC_RULE mlkem_intt_mc;;
549549

550+
(* ------------------------------------------------------------------------- *)
551+
(* Code length constants *)
552+
(* ------------------------------------------------------------------------- *)
553+
554+
let LENGTH_MLKEM_INTT_MC =
555+
REWRITE_CONV[mlkem_intt_mc] `LENGTH mlkem_intt_mc`
556+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
557+
558+
let MLKEM_INTT_PREAMBLE_LENGTH = new_definition
559+
`MLKEM_INTT_PREAMBLE_LENGTH = 20`;;
560+
561+
let MLKEM_INTT_POSTAMBLE_LENGTH = new_definition
562+
`MLKEM_INTT_POSTAMBLE_LENGTH = 24`;;
563+
564+
let MLKEM_INTT_CORE_START = new_definition
565+
`MLKEM_INTT_CORE_START = MLKEM_INTT_PREAMBLE_LENGTH`;;
566+
567+
let MLKEM_INTT_CORE_END = new_definition
568+
`MLKEM_INTT_CORE_END = LENGTH mlkem_intt_mc - MLKEM_INTT_POSTAMBLE_LENGTH`;;
569+
570+
let LENGTH_SIMPLIFY_CONV =
571+
REWRITE_CONV[LENGTH_MLKEM_INTT_MC;
572+
MLKEM_INTT_CORE_START; MLKEM_INTT_CORE_END;
573+
MLKEM_INTT_PREAMBLE_LENGTH; MLKEM_INTT_POSTAMBLE_LENGTH] THENC
574+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
575+
550576
let intt_constants = define
551577
`intt_constants z_12345 z_67 s <=>
552578
(!i. i < 80
@@ -564,16 +590,16 @@ let intt_constants = define
564590
let MLKEM_INTT_CORRECT = prove
565591
(`!a z_12345 z_67 x pc.
566592
ALL (nonoverlapping (a,512))
567-
[(word pc,0x828); (z_12345,160); (z_67,768)]
593+
[(word pc,LENGTH mlkem_intt_mc); (z_12345,160); (z_67,768)]
568594
==> ensures arm
569595
(\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\
570-
read PC s = word (pc + 0x14) /\
596+
read PC s = word (pc + MLKEM_INTT_CORE_START) /\
571597
C_ARGUMENTS [a; z_12345; z_67] s /\
572598
intt_constants z_12345 z_67 s /\
573599
!i. i < 256
574600
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
575601
x i)
576-
(\s. read PC s = word(pc + 0x810) /\
602+
(\s. read PC s = word(pc + MLKEM_INTT_CORE_END) /\
577603
!i. i < 256
578604
==> let zi =
579605
read(memory :> bytes16(word_add a (word(2 * i)))) s in
@@ -582,6 +608,7 @@ let MLKEM_INTT_CORRECT = prove
582608
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
583609
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
584610
MAYCHANGE [memory :> bytes(a,512)])`,
611+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
585612
MAP_EVERY X_GEN_TAC
586613
[`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN
587614
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
@@ -662,7 +689,7 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove
662689
aligned 16 stackpointer /\
663690
ALLPAIRS nonoverlapping
664691
[(a,512); (word_sub stackpointer (word 64),64)]
665-
[(word pc,0x828); (z_12345,160); (z_67,768)] /\
692+
[(word pc,LENGTH mlkem_intt_mc); (z_12345,160); (z_67,768)] /\
666693
nonoverlapping (a,512) (word_sub stackpointer (word 64),64)
667694
==> ensures arm
668695
(\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\
@@ -683,6 +710,7 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove
683710
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
684711
MAYCHANGE [memory :> bytes(a,512);
685712
memory :> bytes(word_sub stackpointer (word 64),64)])`,
713+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
686714
let TWEAK_CONV =
687715
REWRITE_CONV[intt_constants] THENC
688716
ONCE_DEPTH_CONV let_CONV THENC
@@ -692,5 +720,5 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove
692720
REWRITE_TAC[fst MLKEM_INTT_EXEC] THEN
693721
CONV_TAC TWEAK_CONV THEN
694722
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) MLKEM_INTT_EXEC
695-
(REWRITE_RULE[fst MLKEM_INTT_EXEC] (CONV_RULE TWEAK_CONV MLKEM_INTT_CORRECT))
723+
(REWRITE_RULE[fst MLKEM_INTT_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_INTT_CORRECT)))
696724
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64);;

‎proofs/hol_light/arm/proofs/mlkem_ntt.ml‎

Lines changed: 34 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -346,6 +346,33 @@ let mlkem_ntt_mc = define_assert_from_elf
346346

347347
let MLKEM_NTT_EXEC = ARM_MK_EXEC_RULE mlkem_ntt_mc;;
348348

349+
(* ------------------------------------------------------------------------- *)
350+
(* Code length constants *)
351+
(* ------------------------------------------------------------------------- *)
352+
353+
354+
let LENGTH_MLKEM_NTT_MC =
355+
REWRITE_CONV[mlkem_ntt_mc] `LENGTH mlkem_ntt_mc`
356+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
357+
358+
let MLKEM_NTT_PREAMBLE_LENGTH = new_definition
359+
`MLKEM_NTT_PREAMBLE_LENGTH = 20`;;
360+
361+
let MLKEM_NTT_POSTAMBLE_LENGTH = new_definition
362+
`MLKEM_NTT_POSTAMBLE_LENGTH = 24`;;
363+
364+
let MLKEM_NTT_CORE_START = new_definition
365+
`MLKEM_NTT_CORE_START = MLKEM_NTT_PREAMBLE_LENGTH`;;
366+
367+
let MLKEM_NTT_CORE_END = new_definition
368+
`MLKEM_NTT_CORE_END = LENGTH mlkem_ntt_mc - MLKEM_NTT_POSTAMBLE_LENGTH`;;
369+
370+
let LENGTH_SIMPLIFY_CONV =
371+
REWRITE_CONV[LENGTH_MLKEM_NTT_MC;
372+
MLKEM_NTT_CORE_START; MLKEM_NTT_CORE_END;
373+
MLKEM_NTT_PREAMBLE_LENGTH; MLKEM_NTT_POSTAMBLE_LENGTH] THENC
374+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
375+
349376
let ntt_constants = define
350377
`ntt_constants z_12345 z_67 s <=>
351378
(!i. i < 80
@@ -362,16 +389,16 @@ let ntt_constants = define
362389
let MLKEM_NTT_CORRECT = prove
363390
(`!a z_12345 z_67 x pc.
364391
ALL (nonoverlapping (a,512))
365-
[(word pc,0x504); (z_12345,160); (z_67,768)]
392+
[(word pc,LENGTH mlkem_ntt_mc); (z_12345,160); (z_67,768)]
366393
==> ensures arm
367394
(\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\
368-
read PC s = word (pc + 0x14) /\
395+
read PC s = word (pc + MLKEM_NTT_CORE_START) /\
369396
C_ARGUMENTS [a; z_12345; z_67] s /\
370397
ntt_constants z_12345 z_67 s /\
371398
!i. i < 256
372399
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
373400
x i)
374-
(\s. read PC s = word(pc + 0x4ec) /\
401+
(\s. read PC s = word(pc + MLKEM_NTT_CORE_END) /\
375402
((!i. i < 256 ==> abs(ival(x i)) <= &8191)
376403
==> !i. i < 256
377404
==> let zi =
@@ -381,6 +408,7 @@ let MLKEM_NTT_CORRECT = prove
381408
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
382409
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
383410
MAYCHANGE [memory :> bytes(a,512)])`,
411+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
384412
MAP_EVERY X_GEN_TAC
385413
[`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN
386414
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
@@ -466,7 +494,7 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove
466494
aligned 16 stackpointer /\
467495
ALLPAIRS nonoverlapping
468496
[(a,512); (word_sub stackpointer (word 64),64)]
469-
[(word pc,0x504); (z_12345,160); (z_67,768)] /\
497+
[(word pc,LENGTH mlkem_ntt_mc); (z_12345,160); (z_67,768)] /\
470498
nonoverlapping (a,512) (word_sub stackpointer (word 64),64)
471499
==> ensures arm
472500
(\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\
@@ -488,6 +516,7 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove
488516
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
489517
MAYCHANGE [memory :> bytes(a,512);
490518
memory :> bytes(word_sub stackpointer (word 64),64)])`,
519+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
491520
let TWEAK_CONV =
492521
REWRITE_CONV[ntt_constants] THENC
493522
ONCE_DEPTH_CONV let_CONV THENC
@@ -497,5 +526,5 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove
497526
REWRITE_TAC[fst MLKEM_NTT_EXEC] THEN
498527
CONV_TAC TWEAK_CONV THEN
499528
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) MLKEM_NTT_EXEC
500-
(REWRITE_RULE[fst MLKEM_NTT_EXEC] (CONV_RULE TWEAK_CONV MLKEM_NTT_CORRECT))
529+
(REWRITE_RULE[fst MLKEM_NTT_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTT_CORRECT)))
501530
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64);;

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -217,6 +217,17 @@ let basemul2_odd = define
217217

218218
let poly_basemul_acc_montgomery_cached_k2_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k2_mc;;
219219

220+
(* ------------------------------------------------------------------------- *)
221+
(* Code length constants *)
222+
(* ------------------------------------------------------------------------- *)
223+
224+
let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC =
225+
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k2_mc] `LENGTH poly_basemul_acc_montgomery_cached_k2_mc`
226+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
227+
228+
let LENGTH_SIMPLIFY_CONV =
229+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC];;
230+
220231
(* ------------------------------------------------------------------------- *)
221232
(* Hacky tweaking conversion to write away non-free state component reads. *)
222233
(* ------------------------------------------------------------------------- *)
@@ -314,6 +325,7 @@ let poly_basemul_acc_montgomery_cached_k2_GOAL = `forall srcA srcB srcBt dst x0
314325
(* ------------------------------------------------------------------------- *)
315326

316327
let poly_basemul_acc_montgomery_cached_k2_SPEC = prove(poly_basemul_acc_montgomery_cached_k2_GOAL,
328+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
317329
REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
318330
MODIFIABLE_SIMD_REGS;
319331
NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k2_EXEC] THEN

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -277,6 +277,17 @@ let basemul3_odd = define
277277

278278
let poly_basemul_acc_montgomery_cached_k3_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k3_mc;;
279279

280+
(* ------------------------------------------------------------------------- *)
281+
(* Code length constants *)
282+
(* ------------------------------------------------------------------------- *)
283+
284+
let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC =
285+
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k3_mc] `LENGTH poly_basemul_acc_montgomery_cached_k3_mc`
286+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
287+
288+
let LENGTH_SIMPLIFY_CONV =
289+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC];;
290+
280291
(* ------------------------------------------------------------------------- *)
281292
(* Hacky tweaking conversion to write away non-free state component reads. *)
282293
(* ------------------------------------------------------------------------- *)
@@ -378,6 +389,7 @@ let basemul3_odd = define
378389
(* ------------------------------------------------------------------------- *)
379390

380391
let poly_basemul_acc_montgomery_cached_k3_SPEC = prove (poly_basemul_acc_montgomery_cached_k3_GOAL,
392+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
381393
REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
382394
MODIFIABLE_SIMD_REGS;
383395
NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k3_EXEC] THEN

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -336,6 +336,16 @@ let basemul4_odd = define
336336

337337
let poly_basemul_acc_montgomery_cached_k4_EXEC = ARM_MK_EXEC_RULE poly_basemul_acc_montgomery_cached_k4_mc;;
338338

339+
(* ------------------------------------------------------------------------- *)
340+
(* Code length constants *)
341+
(* ------------------------------------------------------------------------- *)
342+
343+
let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC =
344+
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k4_mc] `LENGTH poly_basemul_acc_montgomery_cached_k4_mc`
345+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
346+
347+
let LENGTH_SIMPLIFY_CONV =
348+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC];;
339349

340350
(* ------------------------------------------------------------------------- *)
341351
(* Hacky tweaking conversion to write away non-free state component reads. *)
@@ -444,6 +454,7 @@ let basemul4_odd = define
444454
(* ------------------------------------------------------------------------- *)
445455

446456
let poly_basemul_acc_montgomery_cached_k4_SPEC = prove(poly_basemul_acc_montgomery_cached_k4_GOAL,
457+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
447458
REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
448459
MODIFIABLE_SIMD_REGS;
449460
NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_basemul_acc_montgomery_cached_k4_EXEC] THEN

‎proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,17 @@ let poly_mulcache_compute_mc = define_assert_from_elf
4949

5050
let poly_mulcache_compute_EXEC = ARM_MK_EXEC_RULE poly_mulcache_compute_mc;;
5151

52+
(* ------------------------------------------------------------------------- *)
53+
(* Code length constants *)
54+
(* ------------------------------------------------------------------------- *)
55+
56+
let LENGTH_POLY_MULCACHE_COMPUTE_MC =
57+
REWRITE_CONV[poly_mulcache_compute_mc] `LENGTH poly_mulcache_compute_mc`
58+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
59+
60+
let LENGTH_SIMPLIFY_CONV =
61+
REWRITE_CONV[LENGTH_POLY_MULCACHE_COMPUTE_MC];;
62+
5263
(* ------------------------------------------------------------------------- *)
5364
(* Specification *)
5465
(* ------------------------------------------------------------------------- *)
@@ -97,6 +108,7 @@ let poly_mulcache_compute_GOAL = `forall pc src dst zetas zetas_twisted x y retu
97108
(* ------------------------------------------------------------------------- *)
98109

99110
let poly_mulcache_compute_SPEC = prove(poly_mulcache_compute_GOAL,
111+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
100112
REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
101113
NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_mulcache_compute_EXEC;
102114
have_mulcache_zetas] THEN

‎proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml‎

Lines changed: 35 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,32 @@ let mlkem_poly_reduce_mc = define_assert_from_elf
9797

9898
let MLKEM_POLY_REDUCE_EXEC = ARM_MK_EXEC_RULE mlkem_poly_reduce_mc;;
9999

100+
(* ------------------------------------------------------------------------- *)
101+
(* Code length constants *)
102+
(* ------------------------------------------------------------------------- *)
103+
104+
let LENGTH_MLKEM_POLY_REDUCE_MC =
105+
REWRITE_CONV[mlkem_poly_reduce_mc] `LENGTH mlkem_poly_reduce_mc`
106+
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
107+
108+
let MLKEM_POLY_REDUCE_PREAMBLE_LENGTH = new_definition
109+
`MLKEM_POLY_REDUCE_PREAMBLE_LENGTH = 0`;;
110+
111+
let MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH = new_definition
112+
`MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH = 4`;;
113+
114+
let MLKEM_POLY_REDUCE_CORE_START = new_definition
115+
`MLKEM_POLY_REDUCE_CORE_START = MLKEM_POLY_REDUCE_PREAMBLE_LENGTH`;;
116+
117+
let MLKEM_POLY_REDUCE_CORE_END = new_definition
118+
`MLKEM_POLY_REDUCE_CORE_END = LENGTH mlkem_poly_reduce_mc - MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH`;;
119+
120+
let LENGTH_SIMPLIFY_CONV =
121+
REWRITE_CONV[LENGTH_MLKEM_POLY_REDUCE_MC;
122+
MLKEM_POLY_REDUCE_CORE_START; MLKEM_POLY_REDUCE_CORE_END;
123+
MLKEM_POLY_REDUCE_PREAMBLE_LENGTH; MLKEM_POLY_REDUCE_POSTAMBLE_LENGTH] THENC
124+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0] ;;
125+
100126
(* ------------------------------------------------------------------------- *)
101127
(* Some lemmas, tactics etc. *)
102128
(* ------------------------------------------------------------------------- *)
@@ -122,21 +148,22 @@ let overall_lemma = prove
122148

123149
let MLKEM_POLY_REDUCE_CORRECT = prove
124150
(`!a x pc.
125-
nonoverlapping (word pc,0x124) (a,512)
151+
nonoverlapping (word pc,LENGTH mlkem_poly_reduce_mc) (a,512)
126152
==> ensures arm
127153
(\s. aligned_bytes_loaded s (word pc) mlkem_poly_reduce_mc /\
128-
read PC s = word pc /\
154+
read PC s = word (pc + MLKEM_POLY_REDUCE_CORE_START) /\
129155
C_ARGUMENTS [a] s /\
130156
!i. i < 256
131157
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
132158
x i)
133-
(\s. read PC s = word(pc + 0x120) /\
159+
(\s. read PC s = word(pc + MLKEM_POLY_REDUCE_CORE_END) /\
134160
!i. i < 256
135161
==> ival(read(memory :> bytes16
136162
(word_add a (word(2 * i)))) s) =
137163
ival(x i) rem &3329)
138164
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
139165
MAYCHANGE [memory :> bytes(a,512)])`,
166+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
140167
MAP_EVERY X_GEN_TAC [`a:int64`; `x:num->int16`; `pc:num`] THEN
141168
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
142169
NONOVERLAPPING_CLAUSES] THEN
@@ -187,7 +214,7 @@ let MLKEM_POLY_REDUCE_CORRECT = prove
187214

188215
let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove
189216
(`!a x pc returnaddress.
190-
nonoverlapping (word pc,0x124) (a,512)
217+
nonoverlapping (word pc,LENGTH mlkem_poly_reduce_mc) (a,512)
191218
==> ensures arm
192219
(\s. aligned_bytes_loaded s (word pc) mlkem_poly_reduce_mc /\
193220
read PC s = word pc /\
@@ -203,10 +230,12 @@ let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove
203230
ival(x i) rem &3329)
204231
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
205232
MAYCHANGE [memory :> bytes(a,512)])`,
233+
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
206234
let TWEAK_CONV =
207235
ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC
208236
ONCE_DEPTH_CONV NUM_MULT_CONV THENC
209-
PURE_REWRITE_CONV [WORD_ADD_0] in
237+
PURE_REWRITE_CONV [WORD_ADD_0]
238+
in
210239
CONV_TAC TWEAK_CONV THEN
211240
ARM_ADD_RETURN_NOSTACK_TAC MLKEM_POLY_REDUCE_EXEC
212-
(CONV_RULE TWEAK_CONV MLKEM_POLY_REDUCE_CORRECT));;
241+
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_REDUCE_CORRECT)));;

0 commit comments

Comments
 (0)