Skip to content

Commit 21eca08

Browse files
mkannwischerhanno-becker
mkannwischer
authored and
hanno-becker
committed
HOL-Light: Autogenerate constant tables for x86_64 NTT proof
- Resolves #648 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 501dc1f commit 21eca08

File tree

6 files changed

+175
-98
lines changed

6 files changed

+175
-98
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ jobs:
7373
proof:
7474
# Dependencies on {name}.{S,ml} are implicit
7575
- name: mldsa_ntt
76-
needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
76+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
7777
name: HOL Light proof for ${{ matrix.proof.name }}.S
7878
runs-on: pqcp-x64
7979
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎dev/x86_64/src/consts.c‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,6 @@
2727
#define MLD_AVX2_Q MLDSA_Q
2828
/* check-magic: 58728449 == pow(MLDSA_Q,-1,2^32) */
2929
#define MLD_AVX2_QINV 58728449
30-
/* check-magic: -4186625 == pow(2,32,MLDSA_Q) */
31-
#define MLD_AVX2_MONT -4186625
3230
/* check-magic: 41978 == pow(2,64-8,MLDSA_Q) */
3331
#define MLD_AVX2_DIV 41978
3432
/* check-magic: -8395782 == signed_mod(MLD_AVX2_QINV*MLD_AVX2_DIV,2^32) */
@@ -69,7 +67,6 @@ MLD_EMPTY_CU(avx2_consts)
6967
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
7068
#undef MLD_AVX2_Q
7169
#undef MLD_AVX2_QINV
72-
#undef MLD_AVX2_MONT
7370
#undef MLD_AVX2_DIV
7471
#undef MLD_AVX2_DIV_QINV
7572
/* Some macros are kept because they are also defined in a header. */

‎mldsa/src/native/x86_64/src/consts.c‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,6 @@
2727
#define MLD_AVX2_Q MLDSA_Q
2828
/* check-magic: 58728449 == pow(MLDSA_Q,-1,2^32) */
2929
#define MLD_AVX2_QINV 58728449
30-
/* check-magic: -4186625 == pow(2,32,MLDSA_Q) */
31-
#define MLD_AVX2_MONT -4186625
3230
/* check-magic: 41978 == pow(2,64-8,MLDSA_Q) */
3331
#define MLD_AVX2_DIV 41978
3432
/* check-magic: -8395782 == signed_mod(MLD_AVX2_QINV*MLD_AVX2_DIV,2^32) */
@@ -69,7 +67,6 @@ MLD_EMPTY_CU(avx2_consts)
6967
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
7068
#undef MLD_AVX2_Q
7169
#undef MLD_AVX2_QINV
72-
#undef MLD_AVX2_MONT
7370
#undef MLD_AVX2_DIV
7471
#undef MLD_AVX2_DIV_QINV
7572
/* Some macros are kept because they are also defined in a header. */

‎proofs/hol_light/x86_64/proofs/mldsa_ntt.ml‎

Lines changed: 1 addition & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
needs "x86/proofs/base.ml";;
1111
needs "proofs/mldsa_specs.ml";;
1212
needs "proofs/mldsa_utils.ml";;
13+
needs "proofs/mldsa_zetas.ml";;
1314

1415
(*** print_literal_from_elf "mldsa/mldsa_ntt.o";;
1516
***)
@@ -4370,97 +4371,6 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o"
43704371
let mldsa_ntt_tmc = define_trimmed "mldsa_ntt_tmc" mldsa_ntt_mc;;
43714372
let MLDSA_NTT_TMC_EXEC = X86_MK_CORE_EXEC_RULE mldsa_ntt_tmc;;
43724373

4373-
(* ------------------------------------------------------------------------- *)
4374-
(* Data tables that are assumed in the precondition. *)
4375-
(* ------------------------------------------------------------------------- *)
4376-
4377-
(*** ML-DSA NTT zeta array: 624 elements total
4378-
*** - [0-31]: ML-DSA constants (q=8380417, qinv=58728449, etc.)
4379-
*** - [32-39]: Initial twiddle factors
4380-
*** - [40-367]: 4x replicated twiddles for SIMD (82 unique values × 4 copies)
4381-
*** - [368-623]: Final twiddle section with 2x replication (128 unique values × 2 copies)
4382-
*** Follows bit-reversed indexing per FIPS 204 Appendix B with AVX2 optimization
4383-
***)
4384-
let mldsa_complete_qdata = define
4385-
`mldsa_complete_qdata:int list =
4386-
[
4387-
&8380417; &8380417; &8380417; &8380417; &8380417; &8380417; &8380417; &8380417;
4388-
&58728449; &58728449; &58728449; &58728449; &58728449; &58728449; &58728449; &58728449;
4389-
-- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782;
4390-
&41978; &41978; &41978; &41978; &41978; &41978; &41978; &41978;
4391-
-- &151046689;
4392-
&1830765815; -- &1929875198; -- &1927777021; &1640767044; &1477910808; &1612161320; &1640734244; &308362795;
4393-
&308362795; &308362795; &308362795; -- &1815525077; -- &1815525077; -- &1815525077; -- &1815525077;
4394-
-- &1374673747; -- &1374673747; -- &1374673747; -- &1374673747; -- &1091570561; -- &1091570561; -- &1091570561;
4395-
-- &1091570561; -- &1929495947; -- &1929495947; -- &1929495947; -- &1929495947; &515185417; &515185417;
4396-
&515185417; &515185417; -- &285697463; -- &285697463; -- &285697463; -- &285697463; &625853735; &625853735;
4397-
&625853735; &625853735; &1727305304; &1727305304; &2082316400; &2082316400; -- &1364982364; -- &1364982364;
4398-
&858240904; &858240904; &1806278032; &1806278032; &222489248; &222489248; -- &346752664; -- &346752664;
4399-
&684667771; &684667771; &1654287830; &1654287830; -- &878576921; -- &878576921; -- &1257667337; -- &1257667337;
4400-
-- &748618600; -- &748618600; &329347125; &329347125; &1837364258; &1837364258; -- &1443016191; -- &1443016191;
4401-
-- &1170414139; -- &1170414139; -- &1846138265; -- &1631226336; -- &1404529459; &1838055109; &1594295555;
4402-
-- &1076973524; -- &1898723372; -- &594436433; -- &202001019; -- &475984260; -- &561427818; &1797021249;
4403-
-- &1061813248; &2059733581; -- &1661512036; -- &1104976547; -- &1750224323; -- &901666090; &418987550;
4404-
&1831915353; -- &1925356481; &992097815; &879957084; &2024403852; &1484874664; -- &1636082790; -- &285388938;
4405-
-- &1983539117; -- &1495136972; -- &950076368; -- &1714807468; -- &952438995; -- &1574918427; &1350681039;
4406-
-- &2143979939; &1599739335; -- &1285853323; -- &993005454; -- &1440787840; &568627424; -- &783134478;
4407-
-- &588790216; &289871779; -- &1262003603; &2135294594; -- &1018755525; -- &889861155; &1665705315; &1321868265;
4408-
&1225434135; -- &1784632064; &666258756; &675310538; -- &1555941048; -- &1999506068; -- &1499481951;
4409-
-- &695180180; -- &1375177022; &1777179795; &334803717; -- &178766299; -- &518252220; &1957047970; &1146323031;
4410-
-- &654783359; -- &1974159335; &1651689966; &140455867; -- &1039411342; &1955560694; &1529189038;
4411-
-- &2131021878; -- &247357819; &1518161567; -- &86965173; &1708872713; &1787797779; &1638590967; -- &120646188;
4412-
-- &1669960606; -- &916321552; &1155548552; &2143745726; &1210558298; -- &1261461890; -- &318346816; &628664287;
4413-
-- &1729304568; &1422575624; &1424130038; -- &1185330464; &235321234; &168022240; &1206536194; &985155484;
4414-
-- &894060583; -- &898413; -- &1363460238; -- &605900043; &2027833504; &14253662; &1014493059; &863641633;
4415-
&1819892093; &2124962073; -- &1223601433; -- &1920467227; -- &1637785316; -- &1536588520; &694382729;
4416-
&235104446; -- &1045062172; &831969619; -- &300448763; &756955444; -- &260312805; &1554794072; &1339088280;
4417-
-- &2040058690; -- &853476187; -- &2047270596; -- &1723816713; -- &1591599803; -- &440824168; &1119856484;
4418-
&1544891539; &155290192; -- &973777462; &991903578; &912367099; -- &44694137; &1176904444; -- &421552614;
4419-
-- &818371958; &1747917558; -- &325927722; &908452108; &1851023419; -- &1176751719; -- &1354528380; -- &72690498;
4420-
-- &314284737; &985022747; &963438279; -- &1078959975; &604552167; -- &1021949428; &608791570; &173440395;
4421-
-- &2126092136; -- &1316619236; -- &1039370342; &6087993; -- &110126092; &565464272; -- &1758099917; -- &1600929361;
4422-
&879867909; -- &1809756372; &400711272; &1363007700; &30313375; -- &326425360; &1683520342; -- &517299994;
4423-
&2027935492; -- &1372618620; &128353682; -- &1123881663; &137583815; -- &635454918; -- &642772911; &45766801;
4424-
&671509323; -- &2070602178; &419615363; &1216882040; -- &270590488; -- &1276805128; &371462360; -- &1357098057;
4425-
-- &384158533; &827959816; -- &596344473; &702390549; -- &279505433; -- &260424530; -- &71875110; -- &1208667171;
4426-
-- &1499603926; &2036925262; -- &540420426; &746144248; -- &1420958686; &2032221021; &1904936414; &1257750362;
4427-
&1926727420; &1931587462; &1258381762; &885133339; &1629985060; &1967222129; &6363718; -- &1287922800;
4428-
&1136965286; &1779436847; &1116720494; &1042326957; &1405999311; &713994583; &940195359; -- &1542497137;
4429-
&2061661095; -- &883155599; &1726753853; -- &1547952704; &394851342; &283780712; &776003547; &1123958025;
4430-
&201262505; &1934038751; &374860238;
4431-
-- &3975713; &25847; -- &2608894; -- &518909; &237124; -- &777960; -- &876248; &466468; &1826347; &1826347; &1826347;
4432-
&1826347; &2353451; &2353451; &2353451; &2353451; -- &359251; -- &359251; -- &359251; -- &359251; -- &2091905;
4433-
-- &2091905; -- &2091905; -- &2091905; &3119733; &3119733; &3119733; &3119733; -- &2884855; -- &2884855; -- &2884855;
4434-
-- &2884855; &3111497; &3111497; &3111497; &3111497; &2680103; &2680103; &2680103; &2680103; &2725464;
4435-
&2725464; &1024112; &1024112; -- &1079900; -- &1079900; &3585928; &3585928; -- &549488; -- &549488; -- &1119584;
4436-
-- &1119584; &2619752; &2619752; -- &2108549; -- &2108549; -- &2118186; -- &2118186; -- &3859737; -- &3859737;
4437-
-- &1399561; -- &1399561; -- &3277672; -- &3277672; &1757237; &1757237; -- &19422; -- &19422; &4010497; &4010497;
4438-
&280005; &280005; &2706023; &95776; &3077325; &3530437; -- &1661693; -- &3592148; -- &2537516; &3915439;
4439-
-- &3861115; -- &3043716; &3574422; -- &2867647; &3539968; -- &300467; &2348700; -- &539299; -- &1699267;
4440-
-- &1643818; &3505694; -- &3821735; &3507263; -- &2140649; -- &1600420; &3699596; &811944; &531354; &954230;
4441-
&3881043; &3900724; -- &2556880; &2071892; -- &2797779; -- &3930395; -- &3677745; -- &1452451; &2176455;
4442-
-- &1257611; -- &4083598; -- &3190144; -- &3632928; &3412210; &2147896; -- &2967645; -- &411027; -- &671102;
4443-
-- &22981; -- &381987; &1852771; -- &3343383; &508951; &44288; &904516; -- &3724342; &1653064; &2389356;
4444-
&759969; &189548; &3159746; -- &2409325; &1315589; &1285669; -- &812732; -- &3019102; -- &3628969; -- &1528703;
4445-
-- &3041255; &3475950; -- &1585221; &1939314; -- &1000202; -- &3157330; &126922; -- &983419; &2715295;
4446-
-- &3693493; -- &2477047; -- &1228525; -- &1308169; &1349076; -- &1430430; &264944; &3097992; -- &1100098;
4447-
&3958618; -- &8578; -- &3249728; -- &210977; -- &1316856; -- &3553272; -- &1851402; -- &177440; &1341330;
4448-
-- &1584928; -- &1439742; -- &3881060; &3839961; &2091667; -- &3342478; &266997; -- &3520352; &900702;
4449-
&495491; -- &655327; -- &3556995; &342297; &3437287; &2842341; &4055324; -- &3767016; -- &2994039; -- &1333058;
4450-
-- &451100; -- &1279661; &1500165; -- &542412; -- &2584293; -- &2013608; &1957272; -- &3183426; &810149;
4451-
-- &3038916; &2213111; -- &426683; -- &1667432; -- &2939036; &183443; -- &554416; &3937738; &3407706;
4452-
&2244091; &2434439; -- &3759364; &1859098; -- &1613174; -- &3122442; -- &525098; &286988; -- &3342277;
4453-
&2691481; &1247620; &1250494; &1869119; &1237275; &1312455; &1917081; &777191; -- &2831860; -- &3724270;
4454-
&2432395; &3369112; &162844; &1652634; &3523897; -- &975884; &1723600; -- &1104333; -- &2235985; -- &976891;
4455-
&3919660; &1400424; &2316500; -- &2446433; -- &1235728; -- &1197226; &909542; -- &43260; &2031748; -- &768622;
4456-
-- &2437823; &1735879; -- &2590150; &2486353; &2635921; &1903435; -- &3318210; &3306115; -- &2546312;
4457-
&2235880; -- &1671176; &594136; &2454455; &185531; &1616392; -- &3694233; &3866901; &1717735; -- &1803090;
4458-
-- &260646; -- &420899; &1612842; -- &48306; -- &846154; &3817976; -- &3562462; &3513181; -- &3193378;
4459-
&819034; -- &522500; &3207046; -- &3595838; &4108315; &203044; &1265009; &1595974; -- &3548272; -- &1050970;
4460-
-- &1430225; -- &1962642; -- &1374803; &3406031; -- &1846953; -- &3776993; -- &164721; -- &1207385; &3014001;
4461-
-- &1799107; &269760; &472078; &1910376; -- &3833893; -- &2286327; -- &3545687; -- &1362209; &1976782
4462-
]`;;
4463-
44644374
(* ------------------------------------------------------------------------- *)
44654375
(* Correctness proof. *)
44664376
(* ------------------------------------------------------------------------- *)

‎proofs/hol_light/x86_64/proofs/mldsa_zetas.ml‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
(*
2+
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
4+
*)
5+
6+
(*
7+
* WARNING: This file is auto-generated from scripts/autogen
8+
* in the mldsa-native repository.
9+
* Do not modify it directly.
10+
*)
11+
12+
(*
13+
* Table of zeta values used in the AVX2 NTTs
14+
* See autogen for details.
15+
*)
16+
17+
let mldsa_complete_qdata = define `mldsa_complete_qdata:int list = [
18+
&8380417; &8380417; &8380417; &8380417; &8380417; &8380417; &8380417; &8380417;
19+
&58728449; &58728449; &58728449; &58728449; &58728449; &58728449; &58728449; &58728449;
20+
-- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782; -- &8395782;
21+
&41978; &41978; &41978; &41978; &41978; &41978; &41978; &41978;
22+
-- &151046689; &1830765815; -- &1929875198; -- &1927777021; &1640767044; &1477910808; &1612161320; &1640734244;
23+
&308362795; &308362795; &308362795; &308362795; -- &1815525077; -- &1815525077; -- &1815525077; -- &1815525077;
24+
-- &1374673747; -- &1374673747; -- &1374673747; -- &1374673747; -- &1091570561; -- &1091570561; -- &1091570561; -- &1091570561;
25+
-- &1929495947; -- &1929495947; -- &1929495947; -- &1929495947; &515185417; &515185417; &515185417; &515185417;
26+
-- &285697463; -- &285697463; -- &285697463; -- &285697463; &625853735; &625853735; &625853735; &625853735;
27+
&1727305304; &1727305304; &2082316400; &2082316400; -- &1364982364; -- &1364982364; &858240904; &858240904;
28+
&1806278032; &1806278032; &222489248; &222489248; -- &346752664; -- &346752664; &684667771; &684667771;
29+
&1654287830; &1654287830; -- &878576921; -- &878576921; -- &1257667337; -- &1257667337; -- &748618600; -- &748618600;
30+
&329347125; &329347125; &1837364258; &1837364258; -- &1443016191; -- &1443016191; -- &1170414139; -- &1170414139;
31+
-- &1846138265; -- &1631226336; -- &1404529459; &1838055109; &1594295555; -- &1076973524; -- &1898723372; -- &594436433;
32+
-- &202001019; -- &475984260; -- &561427818; &1797021249; -- &1061813248; &2059733581; -- &1661512036; -- &1104976547;
33+
-- &1750224323; -- &901666090; &418987550; &1831915353; -- &1925356481; &992097815; &879957084; &2024403852;
34+
&1484874664; -- &1636082790; -- &285388938; -- &1983539117; -- &1495136972; -- &950076368; -- &1714807468; -- &952438995;
35+
-- &1574918427; &1350681039; -- &2143979939; &1599739335; -- &1285853323; -- &993005454; -- &1440787840; &568627424;
36+
-- &783134478; -- &588790216; &289871779; -- &1262003603; &2135294594; -- &1018755525; -- &889861155; &1665705315;
37+
&1321868265; &1225434135; -- &1784632064; &666258756; &675310538; -- &1555941048; -- &1999506068; -- &1499481951;
38+
-- &695180180; -- &1375177022; &1777179795; &334803717; -- &178766299; -- &518252220; &1957047970; &1146323031;
39+
-- &654783359; -- &1974159335; &1651689966; &140455867; -- &1039411342; &1955560694; &1529189038; -- &2131021878;
40+
-- &247357819; &1518161567; -- &86965173; &1708872713; &1787797779; &1638590967; -- &120646188; -- &1669960606;
41+
-- &916321552; &1155548552; &2143745726; &1210558298; -- &1261461890; -- &318346816; &628664287; -- &1729304568;
42+
&1422575624; &1424130038; -- &1185330464; &235321234; &168022240; &1206536194; &985155484; -- &894060583;
43+
-- &898413; -- &1363460238; -- &605900043; &2027833504; &14253662; &1014493059; &863641633; &1819892093;
44+
&2124962073; -- &1223601433; -- &1920467227; -- &1637785316; -- &1536588520; &694382729; &235104446; -- &1045062172;
45+
&831969619; -- &300448763; &756955444; -- &260312805; &1554794072; &1339088280; -- &2040058690; -- &853476187;
46+
-- &2047270596; -- &1723816713; -- &1591599803; -- &440824168; &1119856484; &1544891539; &155290192; -- &973777462;
47+
&991903578; &912367099; -- &44694137; &1176904444; -- &421552614; -- &818371958; &1747917558; -- &325927722;
48+
&908452108; &1851023419; -- &1176751719; -- &1354528380; -- &72690498; -- &314284737; &985022747; &963438279;
49+
-- &1078959975; &604552167; -- &1021949428; &608791570; &173440395; -- &2126092136; -- &1316619236; -- &1039370342;
50+
&6087993; -- &110126092; &565464272; -- &1758099917; -- &1600929361; &879867909; -- &1809756372; &400711272;
51+
&1363007700; &30313375; -- &326425360; &1683520342; -- &517299994; &2027935492; -- &1372618620; &128353682;
52+
-- &1123881663; &137583815; -- &635454918; -- &642772911; &45766801; &671509323; -- &2070602178; &419615363;
53+
&1216882040; -- &270590488; -- &1276805128; &371462360; -- &1357098057; -- &384158533; &827959816; -- &596344473;
54+
&702390549; -- &279505433; -- &260424530; -- &71875110; -- &1208667171; -- &1499603926; &2036925262; -- &540420426;
55+
&746144248; -- &1420958686; &2032221021; &1904936414; &1257750362; &1926727420; &1931587462; &1258381762;
56+
&885133339; &1629985060; &1967222129; &6363718; -- &1287922800; &1136965286; &1779436847; &1116720494;
57+
&1042326957; &1405999311; &713994583; &940195359; -- &1542497137; &2061661095; -- &883155599; &1726753853;
58+
-- &1547952704; &394851342; &283780712; &776003547; &1123958025; &201262505; &1934038751; &374860238;
59+
-- &3975713; &25847; -- &2608894; -- &518909; &237124; -- &777960; -- &876248; &466468;
60+
&1826347; &1826347; &1826347; &1826347; &2353451; &2353451; &2353451; &2353451;
61+
-- &359251; -- &359251; -- &359251; -- &359251; -- &2091905; -- &2091905; -- &2091905; -- &2091905;
62+
&3119733; &3119733; &3119733; &3119733; -- &2884855; -- &2884855; -- &2884855; -- &2884855;
63+
&3111497; &3111497; &3111497; &3111497; &2680103; &2680103; &2680103; &2680103;
64+
&2725464; &2725464; &1024112; &1024112; -- &1079900; -- &1079900; &3585928; &3585928;
65+
-- &549488; -- &549488; -- &1119584; -- &1119584; &2619752; &2619752; -- &2108549; -- &2108549;
66+
-- &2118186; -- &2118186; -- &3859737; -- &3859737; -- &1399561; -- &1399561; -- &3277672; -- &3277672;
67+
&1757237; &1757237; -- &19422; -- &19422; &4010497; &4010497; &280005; &280005;
68+
&2706023; &95776; &3077325; &3530437; -- &1661693; -- &3592148; -- &2537516; &3915439;
69+
-- &3861115; -- &3043716; &3574422; -- &2867647; &3539968; -- &300467; &2348700; -- &539299;
70+
-- &1699267; -- &1643818; &3505694; -- &3821735; &3507263; -- &2140649; -- &1600420; &3699596;
71+
&811944; &531354; &954230; &3881043; &3900724; -- &2556880; &2071892; -- &2797779;
72+
-- &3930395; -- &3677745; -- &1452451; &2176455; -- &1257611; -- &4083598; -- &3190144; -- &3632928;
73+
&3412210; &2147896; -- &2967645; -- &411027; -- &671102; -- &22981; -- &381987; &1852771;
74+
-- &3343383; &508951; &44288; &904516; -- &3724342; &1653064; &2389356; &759969;
75+
&189548; &3159746; -- &2409325; &1315589; &1285669; -- &812732; -- &3019102; -- &3628969;
76+
-- &1528703; -- &3041255; &3475950; -- &1585221; &1939314; -- &1000202; -- &3157330; &126922;
77+
-- &983419; &2715295; -- &3693493; -- &2477047; -- &1228525; -- &1308169; &1349076; -- &1430430;
78+
&264944; &3097992; -- &1100098; &3958618; -- &8578; -- &3249728; -- &210977; -- &1316856;
79+
-- &3553272; -- &1851402; -- &177440; &1341330; -- &1584928; -- &1439742; -- &3881060; &3839961;
80+
&2091667; -- &3342478; &266997; -- &3520352; &900702; &495491; -- &655327; -- &3556995;
81+
&342297; &3437287; &2842341; &4055324; -- &3767016; -- &2994039; -- &1333058; -- &451100;
82+
-- &1279661; &1500165; -- &542412; -- &2584293; -- &2013608; &1957272; -- &3183426; &810149;
83+
-- &3038916; &2213111; -- &426683; -- &1667432; -- &2939036; &183443; -- &554416; &3937738;
84+
&3407706; &2244091; &2434439; -- &3759364; &1859098; -- &1613174; -- &3122442; -- &525098;
85+
&286988; -- &3342277; &2691481; &1247620; &1250494; &1869119; &1237275; &1312455;
86+
&1917081; &777191; -- &2831860; -- &3724270; &2432395; &3369112; &162844; &1652634;
87+
&3523897; -- &975884; &1723600; -- &1104333; -- &2235985; -- &976891; &3919660; &1400424;
88+
&2316500; -- &2446433; -- &1235728; -- &1197226; &909542; -- &43260; &2031748; -- &768622;
89+
-- &2437823; &1735879; -- &2590150; &2486353; &2635921; &1903435; -- &3318210; &3306115;
90+
-- &2546312; &2235880; -- &1671176; &594136; &2454455; &185531; &1616392; -- &3694233;
91+
&3866901; &1717735; -- &1803090; -- &260646; -- &420899; &1612842; -- &48306; -- &846154;
92+
&3817976; -- &3562462; &3513181; -- &3193378; &819034; -- &522500; &3207046; -- &3595838;
93+
&4108315; &203044; &1265009; &1595974; -- &3548272; -- &1050970; -- &1430225; -- &1962642;
94+
-- &1374803; &3406031; -- &1846953; -- &3776993; -- &164721; -- &1207385; &3014001; -- &1799107;
95+
&269760; &472078; &1910376; -- &3833893; -- &2286327; -- &3545687; -- &1362209; &1976782
96+
]`;;

0 commit comments

Comments
 (0)