Skip to content

Commit 65d918f

Browse files
hanno-beckerhanno-becker
committed
HOL-Light: Remove further hardcoded lengths in basemul proofs
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent b1072b9 commit 65d918f

File tree

3 files changed

+57
-12
lines changed

3 files changed

+57
-12
lines changed

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

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -225,8 +225,23 @@ let LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC =
225225
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k2_mc] `LENGTH poly_basemul_acc_montgomery_cached_k2_mc`
226226
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
227227

228+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_PREAMBLE_LENGTH = new_definition
229+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_PREAMBLE_LENGTH = 20`;;
230+
231+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH = new_definition
232+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH = 24`;;
233+
234+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_START = new_definition
235+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_START = POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_PREAMBLE_LENGTH`;;
236+
237+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END = new_definition
238+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END = LENGTH poly_basemul_acc_montgomery_cached_k2_mc - POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH`;;
239+
228240
let LENGTH_SIMPLIFY_CONV =
229-
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC];;
241+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_MC;
242+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_START; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END;
243+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_PREAMBLE_LENGTH; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH] THENC
244+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
230245

231246
(* ------------------------------------------------------------------------- *)
232247
(* Hacky tweaking conversion to write away non-free state component reads. *)
@@ -298,15 +313,15 @@ let poly_basemul_acc_montgomery_cached_k2_GOAL = `forall srcA srcB srcBt dst x0
298313
==>
299314
ensures arm
300315
(\s. aligned_bytes_loaded s (word pc) poly_basemul_acc_montgomery_cached_k2_mc /\
301-
read PC s = word (pc + 20) /\
316+
read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_START) /\
302317
C_ARGUMENTS [dst; srcA; srcB; srcBt] s /\
303318
(!i. i < 256 ==> read(memory :> bytes16(word_add srcA (word (2 * i)))) s = x0 i) /\
304319
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (2 * i)))) s = y0 i) /\
305320
(!i. i < 128 ==> read(memory :> bytes16(word_add srcBt (word (2 * i)))) s = y0t i) /\
306321
(!i. i < 256 ==> read(memory :> bytes16(word_add srcA (word (512 + 2 * i)))) s = x1 i) /\
307322
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (512 + 2 * i)))) s = y1 i) /\
308323
(!i. i < 128 ==> read(memory :> bytes16(word_add srcBt (word (256 + 2 * i)))) s = y1t i))
309-
(\s. read PC s = word (pc + 640) /\
324+
(\s. read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END) /\
310325
((!i. i < 256 ==> abs(ival(x0 i)) <= &2 pow 12 /\ abs(ival(x1 i)) <= &2 pow 12)
311326
==> (!i. i < 128
312327
==> (ival(read(memory :> bytes16(word_add dst (word (4 * i)))) s) ==
@@ -434,7 +449,7 @@ let poly_basemul_acc_montgomery_cached_k2_SPEC' = prove(
434449
REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k2_EXEC] THEN
435450
CONV_TAC TWEAK_CONV THEN
436451
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k2_EXEC
437-
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k2_EXEC] (CONV_RULE TWEAK_CONV poly_basemul_acc_montgomery_cached_k2_SPEC))
452+
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k2_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k2_SPEC)))
438453
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64 THEN
439454
WORD_ARITH_TAC)
440455
;;

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

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -285,8 +285,23 @@ let basemul3_odd = define
285285
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k3_mc] `LENGTH poly_basemul_acc_montgomery_cached_k3_mc`
286286
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
287287

288+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_PREAMBLE_LENGTH = new_definition
289+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_PREAMBLE_LENGTH = 20`;;
290+
291+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH = new_definition
292+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH = 24`;;
293+
294+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_START = new_definition
295+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_START = POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_PREAMBLE_LENGTH`;;
296+
297+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END = new_definition
298+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END = LENGTH poly_basemul_acc_montgomery_cached_k3_mc - POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH`;;
299+
288300
let LENGTH_SIMPLIFY_CONV =
289-
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC];;
301+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_MC;
302+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_START; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END;
303+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_PREAMBLE_LENGTH; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH] THENC
304+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
290305

291306
(* ------------------------------------------------------------------------- *)
292307
(* Hacky tweaking conversion to write away non-free state component reads. *)
@@ -354,7 +369,7 @@ let basemul3_odd = define
354369
==>
355370
ensures arm
356371
(\s. aligned_bytes_loaded s (word pc) poly_basemul_acc_montgomery_cached_k3_mc /\
357-
read PC s = word (pc + 20) /\
372+
read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_START) /\
358373
C_ARGUMENTS [dst; srcA; srcB; srcBt] s /\
359374
(!i. i < 256 ==> read(memory :> bytes16(word_add srcA (word (2 * i)))) s = x0 i) /\
360375
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (2 * i)))) s = y0 i) /\
@@ -366,7 +381,7 @@ let basemul3_odd = define
366381
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (1024 + 2 * i)))) s = y2 i) /\
367382
(!i. i < 128 ==> read(memory :> bytes16(word_add srcBt (word (512 + 2 * i)))) s = y2t i)
368383
)
369-
(\s. read PC s = word (pc + 856) /\
384+
(\s. read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END) /\
370385
((!i. i < 256 ==> abs(ival(x0 i)) <= &2 pow 12 /\ abs(ival(x1 i)) <= &2 pow 12
371386
/\ abs(ival(x2 i)) <= &2 pow 12)
372387
==>
@@ -504,7 +519,7 @@ let basemul3_odd = define
504519
REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k3_EXEC] THEN
505520
CONV_TAC TWEAK_CONV THEN
506521
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k3_EXEC
507-
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k3_EXEC] (CONV_RULE TWEAK_CONV poly_basemul_acc_montgomery_cached_k3_SPEC))
522+
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k3_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k3_SPEC)))
508523
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64 THEN
509524
WORD_ARITH_TAC)
510525
;;

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

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -344,8 +344,23 @@ let basemul4_odd = define
344344
REWRITE_CONV[poly_basemul_acc_montgomery_cached_k4_mc] `LENGTH poly_basemul_acc_montgomery_cached_k4_mc`
345345
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
346346

347+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_PREAMBLE_LENGTH = new_definition
348+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_PREAMBLE_LENGTH = 20`;;
349+
350+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH = new_definition
351+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH = 24`;;
352+
353+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_START = new_definition
354+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_START = POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_PREAMBLE_LENGTH`;;
355+
356+
let POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END = new_definition
357+
`POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END = LENGTH poly_basemul_acc_montgomery_cached_k4_mc - POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH`;;
358+
347359
let LENGTH_SIMPLIFY_CONV =
348-
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC];;
360+
REWRITE_CONV[LENGTH_POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_MC;
361+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_START; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END;
362+
POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_PREAMBLE_LENGTH; POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH] THENC
363+
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
349364

350365
(* ------------------------------------------------------------------------- *)
351366
(* Hacky tweaking conversion to write away non-free state component reads. *)
@@ -413,7 +428,7 @@ let basemul4_odd = define
413428
==>
414429
ensures arm
415430
(\s. aligned_bytes_loaded s (word pc) poly_basemul_acc_montgomery_cached_k4_mc /\
416-
read PC s = word (pc + 20) /\
431+
read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_START) /\
417432
C_ARGUMENTS [dst; srcA; srcB; srcBt] s /\
418433
(!i. i < 256 ==> read(memory :> bytes16(word_add srcA (word (2 * i)))) s = x0 i) /\
419434
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (2 * i)))) s = y0 i) /\
@@ -428,7 +443,7 @@ let basemul4_odd = define
428443
(!i. i < 256 ==> read(memory :> bytes16(word_add srcB (word (1536 + 2 * i)))) s = y3 i) /\
429444
(!i. i < 128 ==> read(memory :> bytes16(word_add srcBt (word (768 + 2 * i)))) s = y3t i)
430445
)
431-
(\s. read PC s = word (pc + 1072) /\
446+
(\s. read PC s = word (pc + POLY_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END) /\
432447
((!i. i < 256 ==> abs(ival(x0 i)) <= &2 pow 12 /\ abs(ival(x1 i)) <= &2 pow 12
433448
/\ abs(ival(x2 i)) <= &2 pow 12
434449
/\ abs(ival(x3 i)) <= &2 pow 12)
@@ -576,7 +591,7 @@ let basemul4_odd = define
576591
REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k4_EXEC] THEN
577592
CONV_TAC TWEAK_CONV THEN
578593
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k4_EXEC
579-
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k4_EXEC] (CONV_RULE TWEAK_CONV poly_basemul_acc_montgomery_cached_k4_SPEC))
594+
(REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k4_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k4_SPEC)))
580595
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64 THEN
581596
WORD_ARITH_TAC)
582597
;;

0 commit comments

Comments
 (0)