Skip to content

Commit 95c035d

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #900 from pq-code-package/autogen_hollight
HOL-Light: Autogenerate zeta tables in proof scripts
2 parents 10bb481 + 911d9c5 commit 95c035d

File tree

5 files changed

+251
-173
lines changed

5 files changed

+251
-173
lines changed

‎.github/workflows/hol_light.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,9 @@ jobs:
3535
proof:
3636
# Dependencies on {name}.{S,ml} are implicit
3737
- name: mlkem_ntt
38-
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
38+
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
3939
- name: mlkem_intt
40-
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
40+
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
4141
- name: mlkem_poly_tomont
4242
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
4343
- name: mlkem_poly_mulcache_compute

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

Lines changed: 18 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ needs "arm/proofs/base.ml";;
1111

1212
needs "proofs/mlkem_specs.ml";;
1313
needs "proofs/mlkem_utils.ml";;
14+
needs "proofs/mlkem_zetas.ml";;
1415

1516
(**** print_literal_from_elf "mlkem/mlkem_intt.o";;
1617
****)
@@ -468,94 +469,28 @@ let mlkem_intt_mc = define_assert_from_elf
468469

469470
let MLKEM_INTT_EXEC = ARM_MK_EXEC_RULE mlkem_intt_mc;;
470471

471-
(* ------------------------------------------------------------------------- *)
472-
(* Data tables that are assumed in the precondition. *)
473-
(* ------------------------------------------------------------------------- *)
474-
475-
let intt_zetas_layer01234 = define
476-
`intt_zetas_layer01234:int list =
477-
[&1583; &15582; -- &821; -- &8081; &1355; &13338; &0; &0; -- &569; -- &5601;
478-
&450; &4429; &936; &9213; &0; &0; &69; &679; &447; &4400; -- &535;
479-
-- &5266; &0; &0; &543; &5345; &1235; &12156; -- &1426; -- &14036; &0;
480-
&0; -- &797; -- &7845; -- &1333; -- &13121; &1089; &10719; &0; &0;
481-
-- &193; -- &1900; -- &56; -- &551; &283; &2786; &0; &0; &1410; &13879;
482-
-- &1476; -- &14529; -- &1339; -- &13180; &0; &0; -- &1062; -- &10453;
483-
&882; &8682; -- &296; -- &2914; &0; &0; &1600; &15749; &40; &394;
484-
&749; &7373; -- &848; -- &8347; &1432; &14095; -- &630; -- &6201;
485-
&687; &6762; &0; &0]`;;
486-
487-
let intt_zetas_layer56 = define
488-
`intt_zetas_layer56:int list =
489-
[-- &910; -- &910; -- &1227; -- &1227; &219; &219; &855; &855; -- &8957;
490-
-- &8957; -- &12078; -- &12078; &2156; &2156; &8416; &8416; &1175;
491-
&1175; &394; &394; -- &1029; -- &1029; -- &1212; -- &1212; &11566;
492-
&11566; &3878; &3878; -- &10129; -- &10129; -- &11930; -- &11930;
493-
-- &885; -- &885; &1219; &1219; &1455; &1455; &1607; &1607; -- &8711;
494-
-- &8711; &11999; &11999; &14322; &14322; &15818; &15818; -- &648;
495-
-- &648; -- &1481; -- &1481; &712; &712; &682; &682; -- &6378; -- &6378;
496-
-- &14578; -- &14578; &7008; &7008; &6713; &6713; -- &886; -- &886;
497-
&1179; &1179; -- &1026; -- &1026; -- &1092; -- &1092; -- &8721;
498-
-- &8721; &11605; &11605; -- &10099; -- &10099; -- &10749; -- &10749;
499-
&554; &554; -- &1143; -- &1143; -- &403; -- &403; &525; &525; &5453;
500-
&5453; -- &11251; -- &11251; -- &3967; -- &3967; &5168; &5168; &927;
501-
&927; -- &1534; -- &1534; &461; &461; -- &1438; -- &1438; &9125;
502-
&9125; -- &15099; -- &15099; &4538; &4538; -- &14155; -- &14155; &735;
503-
&735; -- &561; -- &561; -- &757; -- &757; -- &319; -- &319; &7235;
504-
&7235; -- &5522; -- &5522; -- &7451; -- &7451; -- &3140; -- &3140;
505-
&863; &863; &1230; &1230; &556; &556; -- &1063; -- &1063; &8495;
506-
&8495; &12107; &12107; &5473; &5473; -- &10463; -- &10463; -- &452;
507-
-- &452; -- &807; -- &807; -- &1435; -- &1435; &1010; &1010; -- &4449;
508-
-- &4449; -- &7943; -- &7943; -- &14125; -- &14125; &9942; &9942;
509-
-- &1645; -- &1645; &780; &780; &109; &109; &1031; &1031; -- &16192;
510-
-- &16192; &7678; &7678; &1073; &1073; &10148; &10148; &1239; &1239;
511-
-- &375; -- &375; &1292; &1292; -- &1584; -- &1584; &12196; &12196;
512-
-- &3691; -- &3691; &12717; &12717; -- &15592; -- &15592; &1414; &1414;
513-
-- &1320; -- &1320; -- &33; -- &33; &464; &464; &13918; &13918;
514-
-- &12993; -- &12993; -- &325; -- &325; &4567; &4567; -- &641; -- &641;
515-
&992; &992; &941; &941; &1021; &1021; -- &6309; -- &6309; &9764;
516-
&9764; &9262; &9262; &10050; &10050; -- &268; -- &268; -- &733;
517-
-- &733; &892; &892; -- &939; -- &939; -- &2638; -- &2638; -- &7215;
518-
-- &7215; &8780; &8780; -- &9243; -- &9243; -- &632; -- &632; &816; &816;
519-
&1352; &1352; -- &650; -- &650; -- &6221; -- &6221; &8032; &8032;
520-
&13308; &13308; -- &6398; -- &6398; &642; &642; -- &952; -- &952;
521-
&1540; &1540; -- &1651; -- &1651; &6319; &6319; -- &9371; -- &9371;
522-
&15159; &15159; -- &16251; -- &16251; -- &1461; -- &1461; &1482;
523-
&1482; &540; &540; &1626; &1626; -- &14381; -- &14381; &14588; &14588;
524-
&5315; &5315; &16005; &16005; &1274; &1274; &1052; &1052; &1025;
525-
&1025; -- &1197; -- &1197; &12540; &12540; &10355; &10355; &10089;
526-
&10089; -- &11782; -- &11782; &279; &279; &1173; &1173; -- &233;
527-
-- &233; &667; &667; &2746; &2746; &11546; &11546; -- &2293; -- &2293;
528-
&6565; &6565; &314; &314; -- &756; -- &756; &48; &48; -- &1409;
529-
-- &1409; &3091; &3091; -- &7441; -- &7441; &472; &472; -- &13869;
530-
-- &13869; &1573; &1573; &76; &76; -- &331; -- &331; -- &289; -- &289;
531-
&15483; &15483; &748; &748; -- &3258; -- &3258; -- &2845; -- &2845;
532-
-- &1100; -- &1100; -- &723; -- &723; &680; &680; &568; &568; -- &10828;
533-
-- &10828; -- &7117; -- &7117; &6693; &6693; &5591; &5591; &1041;
534-
&1041; -- &1637; -- &1637; -- &583; -- &583; -- &17; -- &17; &10247;
535-
&10247; -- &16113; -- &16113; -- &5739; -- &5739; -- &167; -- &167]`;;
536-
537472
let intt_constants = define
538-
`intt_constants z_01234 z_56 s <=>
473+
`intt_constants z_12345 z_67 s <=>
539474
(!i. i < 80
540-
==> read(memory :> bytes16(word_add z_01234 (word(2 * i)))) s =
541-
iword(EL i intt_zetas_layer01234)) /\
475+
==> read(memory :> bytes16(word_add z_12345 (word(2 * i)))) s =
476+
iword(EL i intt_zetas_layer12345)) /\
542477
(!i. i < 384
543-
==> read(memory :> bytes16(word_add z_56 (word(2 * i)))) s =
544-
iword(EL i intt_zetas_layer56))`;;
478+
==> read(memory :> bytes16(word_add z_67 (word(2 * i)))) s =
479+
iword(EL i intt_zetas_layer67))`;;
545480

546481
(* ------------------------------------------------------------------------- *)
547482
(* Correctness proof. *)
548483
(* ------------------------------------------------------------------------- *)
549484

550485
let MLKEM_INTT_CORRECT = prove
551-
(`!a z_01234 z_56 x pc.
486+
(`!a z_12345 z_67 x pc.
552487
ALL (nonoverlapping (a,512))
553-
[(word pc,0x6f8); (z_01234,160); (z_56,768)]
488+
[(word pc,0x6f8); (z_12345,160); (z_67,768)]
554489
==> ensures arm
555490
(\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\
556491
read PC s = word (pc + 0x14) /\
557-
C_ARGUMENTS [a; z_01234; z_56] s /\
558-
intt_constants z_01234 z_56 s /\
492+
C_ARGUMENTS [a; z_12345; z_67] s /\
493+
intt_constants z_12345 z_67 s /\
559494
!i. i < 256
560495
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
561496
x i)
@@ -569,7 +504,7 @@ let MLKEM_INTT_CORRECT = prove
569504
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
570505
MAYCHANGE [memory :> bytes(a,512)])`,
571506
MAP_EVERY X_GEN_TAC
572-
[`a:int64`; `z_01234:int64`; `z_56:int64`; `x:num->int16`; `pc:num`] THEN
507+
[`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN
573508
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
574509
NONOVERLAPPING_CLAUSES; ALL] THEN
575510
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
@@ -579,7 +514,7 @@ let MLKEM_INTT_CORRECT = prove
579514
REWRITE_TAC[intt_constants] THEN
580515
CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV
581516
(EXPAND_CASES_CONV THENC ONCE_DEPTH_CONV NUM_MULT_CONV)))) THEN
582-
REWRITE_TAC[intt_zetas_layer01234; intt_zetas_layer56] THEN
517+
REWRITE_TAC[intt_zetas_layer12345; intt_zetas_layer67] THEN
583518
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN
584519
CONV_TAC(ONCE_DEPTH_CONV WORD_IWORD_CONV) THEN REWRITE_TAC[WORD_ADD_0] THEN
585520
ENSURES_INIT_TAC "s0" THEN
@@ -589,8 +524,8 @@ let MLKEM_INTT_CORRECT = prove
589524
***)
590525

591526
MEMORY_128_FROM_16_TAC "a" 32 THEN
592-
MEMORY_128_FROM_16_TAC "z_01234" 10 THEN
593-
MEMORY_128_FROM_16_TAC "z_56" 48 THEN
527+
MEMORY_128_FROM_16_TAC "z_12345" 10 THEN
528+
MEMORY_128_FROM_16_TAC "z_67" 48 THEN
594529
ASM_REWRITE_TAC[WORD_ADD_0] THEN CONV_TAC WORD_REDUCE_CONV THEN
595530
DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes16 a) s = x`] THEN
596531
REPEAT STRIP_TAC THEN
@@ -641,19 +576,19 @@ let MLKEM_INTT_CORRECT = prove
641576
(*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
642577

643578
let MLKEM_INTT_SUBROUTINE_CORRECT = prove
644-
(`!a z_01234 z_56 x pc stackpointer returnaddress.
579+
(`!a z_12345 z_67 x pc stackpointer returnaddress.
645580
aligned 16 stackpointer /\
646581
ALLPAIRS nonoverlapping
647582
[(a,512); (word_sub stackpointer (word 64),64)]
648-
[(word pc,0x6f8); (z_01234,160); (z_56,768)] /\
583+
[(word pc,0x6f8); (z_12345,160); (z_67,768)] /\
649584
nonoverlapping (a,512) (word_sub stackpointer (word 64),64)
650585
==> ensures arm
651586
(\s. aligned_bytes_loaded s (word pc) mlkem_intt_mc /\
652587
read PC s = word pc /\
653588
read SP s = stackpointer /\
654589
read X30 s = returnaddress /\
655-
C_ARGUMENTS [a; z_01234; z_56] s /\
656-
intt_constants z_01234 z_56 s /\
590+
C_ARGUMENTS [a; z_12345; z_67] s /\
591+
intt_constants z_12345 z_67 s /\
657592
!i. i < 256
658593
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
659594
x i)

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

Lines changed: 18 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ needs "arm/proofs/base.ml";;
1111

1212
needs "proofs/mlkem_specs.ml";;
1313
needs "proofs/mlkem_utils.ml";;
14+
needs "proofs/mlkem_zetas.ml";;
1415

1516
(**** print_literal_from_elf "mlkem/mlkem_ntt.o";;
1617
****)
@@ -343,95 +344,28 @@ let mlkem_ntt_mc = define_assert_from_elf
343344

344345
let MLKEM_NTT_EXEC = ARM_MK_EXEC_RULE mlkem_ntt_mc;;
345346

346-
(* ------------------------------------------------------------------------- *)
347-
(* Data tables that are assumed in the precondition. *)
348-
(* ------------------------------------------------------------------------- *)
349-
350-
let ntt_zetas_layer01234 = define
351-
`ntt_zetas_layer01234:int list =
352-
[-- &1600; -- &15749; -- &749; -- &7373; -- &40; -- &394; -- &687; -- &6762;
353-
&630; &6201; -- &1432; -- &14095; &848; &8347; &0; &0; &1062; &10453; &296;
354-
&2914; -- &882; -- &8682; &0; &0; -- &1410; -- &13879; &1339; &13180; &1476;
355-
&14529; &0; &0; &193; &1900; -- &283; -- &2786; &56; &551; &0; &0; &797;
356-
&7845; -- &1089; -- &10719; &1333; &13121; &0; &0; -- &543; -- &5345;
357-
&1426; &14036; -- &1235; -- &12156; &0; &0; -- &69; -- &679; &535; &5266;
358-
-- &447; -- &4400; &0; &0; &569; &5601; -- &936; -- &9213; -- &450;
359-
-- &4429; &0; &0; -- &1583; -- &15582; -- &1355; -- &13338; &821;
360-
&8081; &0; &0]`;;
361-
362-
let ntt_zetas_layer56 = define
363-
`ntt_zetas_layer56:int list =
364-
[&289; &289; &331; &331; -- &76; -- &76; -- &1573; -- &1573; &2845;
365-
&2845; &3258; &3258; -- &748; -- &748; -- &15483; -- &15483; &17; &17;
366-
&583; &583; &1637; &1637; -- &1041; -- &1041; &167; &167; &5739;
367-
&5739; &16113; &16113; -- &10247; -- &10247; -- &568; -- &568;
368-
-- &680; -- &680; &723; &723; &1100; &1100; -- &5591; -- &5591; -- &6693;
369-
-- &6693; &7117; &7117; &10828; &10828; &1197; &1197; -- &1025;
370-
-- &1025; -- &1052; -- &1052; -- &1274; -- &1274; &11782; &11782;
371-
-- &10089; -- &10089; -- &10355; -- &10355; -- &12540; -- &12540; &1409;
372-
&1409; -- &48; -- &48; &756; &756; -- &314; -- &314; &13869; &13869;
373-
-- &472; -- &472; &7441; &7441; -- &3091; -- &3091; -- &667; -- &667;
374-
&233; &233; -- &1173; -- &1173; -- &279; -- &279; -- &6565; -- &6565;
375-
&2293; &2293; -- &11546; -- &11546; -- &2746; -- &2746; &650; &650;
376-
-- &1352; -- &1352; -- &816; -- &816; &632; &632; &6398; &6398;
377-
-- &13308; -- &13308; -- &8032; -- &8032; &6221; &6221; -- &1626;
378-
-- &1626; -- &540; -- &540; -- &1482; -- &1482; &1461; &1461; -- &16005;
379-
-- &16005; -- &5315; -- &5315; -- &14588; -- &14588; &14381; &14381;
380-
&1651; &1651; -- &1540; -- &1540; &952; &952; -- &642; -- &642;
381-
&16251; &16251; -- &15159; -- &15159; &9371; &9371; -- &6319;
382-
-- &6319; -- &464; -- &464; &33; &33; &1320; &1320; -- &1414; -- &1414;
383-
-- &4567; -- &4567; &325; &325; &12993; &12993; -- &13918; -- &13918;
384-
&939; &939; -- &892; -- &892; &733; &733; &268; &268; &9243; &9243;
385-
-- &8780; -- &8780; &7215; &7215; &2638; &2638; -- &1021; -- &1021;
386-
-- &941; -- &941; -- &992; -- &992; &641; &641; -- &10050; -- &10050;
387-
-- &9262; -- &9262; -- &9764; -- &9764; &6309; &6309; -- &1010; -- &1010;
388-
&1435; &1435; &807; &807; &452; &452; -- &9942; -- &9942; &14125;
389-
&14125; &7943; &7943; &4449; &4449; &1584; &1584; -- &1292; -- &1292;
390-
&375; &375; -- &1239; -- &1239; &15592; &15592; -- &12717; -- &12717;
391-
&3691; &3691; -- &12196; -- &12196; -- &1031; -- &1031; -- &109;
392-
-- &109; -- &780; -- &780; &1645; &1645; -- &10148; -- &10148; -- &1073;
393-
-- &1073; -- &7678; -- &7678; &16192; &16192; &1438; &1438; -- &461;
394-
-- &461; &1534; &1534; -- &927; -- &927; &14155; &14155; -- &4538;
395-
-- &4538; &15099; &15099; -- &9125; -- &9125; &1063; &1063; -- &556;
396-
-- &556; -- &1230; -- &1230; -- &863; -- &863; &10463; &10463; -- &5473;
397-
-- &5473; -- &12107; -- &12107; -- &8495; -- &8495; &319; &319; &757;
398-
&757; &561; &561; -- &735; -- &735; &3140; &3140; &7451; &7451; &5522;
399-
&5522; -- &7235; -- &7235; -- &682; -- &682; -- &712; -- &712; &1481;
400-
&1481; &648; &648; -- &6713; -- &6713; -- &7008; -- &7008; &14578;
401-
&14578; &6378; &6378; -- &525; -- &525; &403; &403; &1143; &1143;
402-
-- &554; -- &554; -- &5168; -- &5168; &3967; &3967; &11251; &11251;
403-
-- &5453; -- &5453; &1092; &1092; &1026; &1026; -- &1179; -- &1179; &886;
404-
&886; &10749; &10749; &10099; &10099; -- &11605; -- &11605; &8721;
405-
&8721; -- &855; -- &855; -- &219; -- &219; &1227; &1227; &910; &910;
406-
-- &8416; -- &8416; -- &2156; -- &2156; &12078; &12078; &8957; &8957;
407-
-- &1607; -- &1607; -- &1455; -- &1455; -- &1219; -- &1219; &885;
408-
&885; -- &15818; -- &15818; -- &14322; -- &14322; -- &11999;
409-
-- &11999; &8711; &8711; &1212; &1212; &1029; &1029; -- &394; -- &394;
410-
-- &1175; -- &1175; &11930; &11930; &10129; &10129; -- &3878; -- &3878;
411-
-- &11566; -- &11566]`;;
412-
413347
let ntt_constants = define
414-
`ntt_constants z_01234 z_56 s <=>
348+
`ntt_constants z_12345 z_67 s <=>
415349
(!i. i < 80
416-
==> read(memory :> bytes16(word_add z_01234 (word(2 * i)))) s =
417-
iword(EL i ntt_zetas_layer01234)) /\
350+
==> read(memory :> bytes16(word_add z_12345 (word(2 * i)))) s =
351+
iword(EL i ntt_zetas_layer12345)) /\
418352
(!i. i < 384
419-
==> read(memory :> bytes16(word_add z_56 (word(2 * i)))) s =
420-
iword(EL i ntt_zetas_layer56))`;;
353+
==> read(memory :> bytes16(word_add z_67 (word(2 * i)))) s =
354+
iword(EL i ntt_zetas_layer67))`;;
421355

422356
(* ------------------------------------------------------------------------- *)
423357
(* Correctness proof. *)
424358
(* ------------------------------------------------------------------------- *)
425359

426360
let MLKEM_NTT_CORRECT = prove
427-
(`!a z_01234 z_56 x pc.
361+
(`!a z_12345 z_67 x pc.
428362
ALL (nonoverlapping (a,512))
429-
[(word pc,0x504); (z_01234,160); (z_56,768)]
363+
[(word pc,0x504); (z_12345,160); (z_67,768)]
430364
==> ensures arm
431365
(\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\
432366
read PC s = word (pc + 0x14) /\
433-
C_ARGUMENTS [a; z_01234; z_56] s /\
434-
ntt_constants z_01234 z_56 s /\
367+
C_ARGUMENTS [a; z_12345; z_67] s /\
368+
ntt_constants z_12345 z_67 s /\
435369
!i. i < 256
436370
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
437371
x i)
@@ -446,7 +380,7 @@ let MLKEM_NTT_CORRECT = prove
446380
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
447381
MAYCHANGE [memory :> bytes(a,512)])`,
448382
MAP_EVERY X_GEN_TAC
449-
[`a:int64`; `z_01234:int64`; `z_56:int64`; `x:num->int16`; `pc:num`] THEN
383+
[`a:int64`; `z_12345:int64`; `z_67:int64`; `x:num->int16`; `pc:num`] THEN
450384
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
451385
NONOVERLAPPING_CLAUSES; ALL] THEN
452386
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
@@ -456,7 +390,7 @@ let MLKEM_NTT_CORRECT = prove
456390
REWRITE_TAC[ntt_constants] THEN
457391
CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV
458392
(EXPAND_CASES_CONV THENC ONCE_DEPTH_CONV NUM_MULT_CONV)))) THEN
459-
REWRITE_TAC[ntt_zetas_layer01234; ntt_zetas_layer56] THEN
393+
REWRITE_TAC[ntt_zetas_layer12345; ntt_zetas_layer67] THEN
460394
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN
461395
CONV_TAC(ONCE_DEPTH_CONV WORD_IWORD_CONV) THEN REWRITE_TAC[WORD_ADD_0] THEN
462396
ENSURES_INIT_TAC "s0" THEN
@@ -466,8 +400,8 @@ let MLKEM_NTT_CORRECT = prove
466400
***)
467401

468402
MEMORY_128_FROM_16_TAC "a" 32 THEN
469-
MEMORY_128_FROM_16_TAC "z_01234" 10 THEN
470-
MEMORY_128_FROM_16_TAC "z_56" 48 THEN
403+
MEMORY_128_FROM_16_TAC "z_12345" 10 THEN
404+
MEMORY_128_FROM_16_TAC "z_67" 48 THEN
471405
ASM_REWRITE_TAC[WORD_ADD_0] THEN CONV_TAC WORD_REDUCE_CONV THEN
472406
DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes16 a) s = x`] THEN
473407
REPEAT STRIP_TAC THEN
@@ -523,19 +457,19 @@ let MLKEM_NTT_CORRECT = prove
523457
(*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
524458

525459
let MLKEM_NTT_SUBROUTINE_CORRECT = prove
526-
(`!a z_01234 z_56 x pc stackpointer returnaddress.
460+
(`!a z_12345 z_67 x pc stackpointer returnaddress.
527461
aligned 16 stackpointer /\
528462
ALLPAIRS nonoverlapping
529463
[(a,512); (word_sub stackpointer (word 64),64)]
530-
[(word pc,0x504); (z_01234,160); (z_56,768)] /\
464+
[(word pc,0x504); (z_12345,160); (z_67,768)] /\
531465
nonoverlapping (a,512) (word_sub stackpointer (word 64),64)
532466
==> ensures arm
533467
(\s. aligned_bytes_loaded s (word pc) mlkem_ntt_mc /\
534468
read PC s = word pc /\
535469
read SP s = stackpointer /\
536470
read X30 s = returnaddress /\
537-
C_ARGUMENTS [a; z_01234; z_56] s /\
538-
ntt_constants z_01234 z_56 s /\
471+
C_ARGUMENTS [a; z_12345; z_67] s /\
472+
ntt_constants z_12345 z_67 s /\
539473
!i. i < 256
540474
==> read(memory :> bytes16(word_add a (word(2 * i)))) s =
541475
x i)

0 commit comments

Comments
 (0)