Skip to content

Commit 5112f49

Browse files
mkannwischermkannwischer
authored
Merge pull request #1040 from pq-code-package/poly_mulcache_compute_hollight_consts
HOL-Light: Autogenerate mulcache twiddles
2 parents 13e1d3c + 29bef4c commit 5112f49

File tree

4 files changed

+50
-38
lines changed

4 files changed

+50
-38
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ jobs:
4141
- name: mlkem_poly_tomont
4242
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
4343
- name: mlkem_poly_mulcache_compute
44-
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
44+
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
4545
- name: mlkem_poly_reduce
4646
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
4747
- name: mlkem_poly_basemul_acc_montgomery_cached_k2

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

Lines changed: 1 addition & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ needs "arm/proofs/base.ml";;
77

88
needs "proofs/mlkem_specs.ml";;
99
needs "proofs/mlkem_utils.ml";;
10+
needs "proofs/mlkem_zetas.ml";;
1011

1112
(**** print_literal_from_elf "mlkem/poly_mulcache_compute.o";;
1213
****)
@@ -50,43 +51,6 @@ let poly_mulcache_compute_EXEC = ARM_MK_EXEC_RULE poly_mulcache_compute_mc;;
5051
(* Specification *)
5152
(* ------------------------------------------------------------------------- *)
5253

53-
let mulcache_zetas = define
54-
`mulcache_zetas:int list =
55-
[
56-
&17; -- &17; -- &568; &568; &583; -- &583; -- &680; &680; &1637; -- &1637; &723;
57-
-- &723; -- &1041; &1041; &1100; -- &1100; &1409; -- &1409; -- &667; &667; -- &48; &48;
58-
&233; -- &233; &756; -- &756; -- &1173; &1173; -- &314; &314; -- &279; &279; -- &1626;
59-
&1626; &1651; -- &1651; -- &540; &540; -- &1540; &1540; -- &1482; &1482; &952; -- &952;
60-
&1461; -- &1461; -- &642; &642; &939; -- &939; -- &1021; &1021; -- &892; &892; -- &941;
61-
&941; &733; -- &733; -- &992; &992; &268; -- &268; &641; -- &641; &1584; -- &1584;
62-
-- &1031; &1031; -- &1292; &1292; -- &109; &109; &375; -- &375; -- &780; &780; -- &1239;
63-
&1239; &1645; -- &1645; &1063; -- &1063; &319; -- &319; -- &556; &556; &757; -- &757;
64-
-- &1230; &1230; &561; -- &561; -- &863; &863; -- &735; &735; -- &525; &525; &1092;
65-
-- &1092; &403; -- &403; &1026; -- &1026; &1143; -- &1143; -- &1179; &1179; -- &554; &554;
66-
&886; -- &886; -- &1607; &1607; &1212; -- &1212; -- &1455; &1455; &1029; -- &1029; -- &1219;
67-
&1219; -- &394; &394; &885; -- &885; -- &1175; &1175
68-
]`;;
69-
70-
let mulcache_zetas_twisted = define
71-
`mulcache_zetas_twisted: int list =
72-
[
73-
&167; -- &167; -- &5591; &5591; &5739; -- &5739; -- &6693; &6693; &16113;
74-
-- &16113; &7117; -- &7117; -- &10247; &10247; &10828; -- &10828; &13869; -- &13869;
75-
-- &6565; &6565; -- &472; &472; &2293; -- &2293; &7441; -- &7441; -- &11546;
76-
&11546; -- &3091; &3091; -- &2746; &2746; -- &16005; &16005; &16251; -- &16251;
77-
-- &5315; &5315; -- &15159; &15159; -- &14588; &14588; &9371; -- &9371; &14381;
78-
-- &14381; -- &6319; &6319; &9243; -- &9243; -- &10050; &10050; -- &8780; &8780;
79-
-- &9262; &9262; &7215; -- &7215; -- &9764; &9764; &2638; -- &2638; &6309;
80-
-- &6309; &15592; -- &15592; -- &10148; &10148; -- &12717; &12717; -- &1073; &1073;
81-
&3691; -- &3691; -- &7678; &7678; -- &12196; &12196; &16192; -- &16192; &10463;
82-
-- &10463; &3140; -- &3140; -- &5473; &5473; &7451; -- &7451; -- &12107; &12107;
83-
&5522; -- &5522; -- &8495; &8495; -- &7235; &7235; -- &5168; &5168; &10749;
84-
-- &10749; &3967; -- &3967; &10099; -- &10099; &11251; -- &11251; -- &11605; &11605;
85-
-- &5453; &5453; &8721; -- &8721; -- &15818; &15818; &11930; -- &11930; -- &14322;
86-
&14322; &10129; -- &10129; -- &11999; &11999; -- &3878; &3878; &8711; -- &8711;
87-
-- &11566; &11566
88-
]`;;
89-
9054
let have_mulcache_zetas = define
9155
`have_mulcache_zetas zetas zetas_twisted s <=>
9256
(!i. i < 128 ==> read(memory :> bytes16(word_add zetas (word (2*i)))) s =

‎proofs/hol_light/arm/proofs/mlkem_zetas.ml‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,3 +140,42 @@ let intt_zetas_layer67 = define `intt_zetas_layer67:int list = [
140140
&1041; &1041; -- &1637; -- &1637; -- &583; -- &583; -- &17; -- &17;
141141
&10247; &10247; -- &16113; -- &16113; -- &5739; -- &5739; -- &167; -- &167
142142
]`;;
143+
144+
let mulcache_zetas = define `mulcache_zetas:int list = [
145+
&17; -- &17; -- &568; &568; &583; -- &583; -- &680; &680;
146+
&1637; -- &1637; &723; -- &723; -- &1041; &1041; &1100; -- &1100;
147+
&1409; -- &1409; -- &667; &667; -- &48; &48; &233; -- &233;
148+
&756; -- &756; -- &1173; &1173; -- &314; &314; -- &279; &279;
149+
-- &1626; &1626; &1651; -- &1651; -- &540; &540; -- &1540; &1540;
150+
-- &1482; &1482; &952; -- &952; &1461; -- &1461; -- &642; &642;
151+
&939; -- &939; -- &1021; &1021; -- &892; &892; -- &941; &941;
152+
&733; -- &733; -- &992; &992; &268; -- &268; &641; -- &641;
153+
&1584; -- &1584; -- &1031; &1031; -- &1292; &1292; -- &109; &109;
154+
&375; -- &375; -- &780; &780; -- &1239; &1239; &1645; -- &1645;
155+
&1063; -- &1063; &319; -- &319; -- &556; &556; &757; -- &757;
156+
-- &1230; &1230; &561; -- &561; -- &863; &863; -- &735; &735;
157+
-- &525; &525; &1092; -- &1092; &403; -- &403; &1026; -- &1026;
158+
&1143; -- &1143; -- &1179; &1179; -- &554; &554; &886; -- &886;
159+
-- &1607; &1607; &1212; -- &1212; -- &1455; &1455; &1029; -- &1029;
160+
-- &1219; &1219; -- &394; &394; &885; -- &885; -- &1175; &1175
161+
]`;;
162+
163+
164+
let mulcache_zetas_twisted = define `mulcache_zetas_twisted:int list = [
165+
&167; -- &167; -- &5591; &5591; &5739; -- &5739; -- &6693; &6693;
166+
&16113; -- &16113; &7117; -- &7117; -- &10247; &10247; &10828; -- &10828;
167+
&13869; -- &13869; -- &6565; &6565; -- &472; &472; &2293; -- &2293;
168+
&7441; -- &7441; -- &11546; &11546; -- &3091; &3091; -- &2746; &2746;
169+
-- &16005; &16005; &16251; -- &16251; -- &5315; &5315; -- &15159; &15159;
170+
-- &14588; &14588; &9371; -- &9371; &14381; -- &14381; -- &6319; &6319;
171+
&9243; -- &9243; -- &10050; &10050; -- &8780; &8780; -- &9262; &9262;
172+
&7215; -- &7215; -- &9764; &9764; &2638; -- &2638; &6309; -- &6309;
173+
&15592; -- &15592; -- &10148; &10148; -- &12717; &12717; -- &1073; &1073;
174+
&3691; -- &3691; -- &7678; &7678; -- &12196; &12196; &16192; -- &16192;
175+
&10463; -- &10463; &3140; -- &3140; -- &5473; &5473; &7451; -- &7451;
176+
-- &12107; &12107; &5522; -- &5522; -- &8495; &8495; -- &7235; &7235;
177+
-- &5168; &5168; &10749; -- &10749; &3967; -- &3967; &10099; -- &10099;
178+
&11251; -- &11251; -- &11605; &11605; -- &5453; &5453; &8721; -- &8721;
179+
-- &15818; &15818; &11930; -- &11930; -- &14322; &14322; &10129; -- &10129;
180+
-- &11999; &11999; -- &3878; &3878; &8711; -- &8711; -- &11566; &11566
181+
]`;;

‎scripts/autogen‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -715,6 +715,15 @@ def gen_aarch64_hol_light_zeta_file(dry_run=False):
715715
yield from print_hol_light_array(gen_aarch64_inv_ntt_zetas_layer67())
716716
yield "]`;;"
717717
yield ""
718+
yield "let mulcache_zetas = define `mulcache_zetas:int list = ["
719+
yield from print_hol_light_array(gen_aarch64_mulcache_twiddles())
720+
yield "]`;;"
721+
yield ""
722+
yield ""
723+
yield "let mulcache_zetas_twisted = define `mulcache_zetas_twisted:int list = ["
724+
yield from print_hol_light_array(gen_aarch64_mulcache_twiddles_twisted())
725+
yield "]`;;"
726+
yield ""
718727

719728
update_file(
720729
"proofs/hol_light/arm/proofs/mlkem_zetas.ml",

0 commit comments

Comments
 (0)