Skip to content

Commit 16cdf94

Browse files
rod-chapmanrod-chapman
committed
Add fast, layer-merged forward and inverse NTT code.
Adjust and move proof files accordingly. Signed-off-by: Rod Chapman <[email protected]> Add support for NO_INLINE attribute and its use with CBMC. Signed-off-by: Rod Chapman <[email protected]> Make top-level ntt_layer*() functions NO_INLINE to improve comprehension and review of auto-vectorization of this code. Signed-off-by: Rod Chapman <[email protected]> Add first two fast Invert NTT functions Adds invntt_layer7_invert_inner() invntt_layer7_invert() and their proof files. Signed-off-by: Rod Chapman <[email protected]> Remove dummy call to invntt_layer7_invert() Signed-off-by: Rod Chapman <[email protected]> Add Invert NTT Layer 6 functions. Adds invntt_layer6_inner() invntt_layer6() functions and their proof files. Signed-off-by: Rod Chapman <[email protected]> Simplify Zeta tables for layers 4 and 5. Signed-off-by: Rod Chapman <[email protected]> Adds Inverse NTT Layer54 (marged) Adds functions invntt_layer54_inner() invntt_layer54() and their proof files. Signed-off-by: Rod Chapman <[email protected]> Use new zeta constants in ntt_layer123() Signed-off-by: Rod Chapman <[email protected]> Adds first full implemenation of Inverse NTT with layer merging. Adds function invntt_layer321() and its proof. Updates top-level poly_invntt_tomont() to call new layer-merged implementation. Renames existing implementation as poly_invntt_tomont_ref() for now. Signed-off-by: Rod Chapman <[email protected]> Update proof of poly_invntt_tomont() Signed-off-by: Rod Chapman <[email protected]> Remove reference implementation of poly_invntt_tomont() Also removes local function invntt_layer() and its proof. Signed-off-by: Rod Chapman <[email protected]> Switch to Z3 for these proofs, which is much faster than Bitwuzla. Signed-off-by: Rod Chapman <[email protected]> Switch back to Z3 for proof of ntt_layer123() Signed-off-by: Rod Chapman <[email protected]> Rename ntt_layer45_slice() to ntt_inner45_inner() Signed-off-by: Rod Chapman <[email protected]> Rename proof files Signed-off-by: Rod Chapman <[email protected]> Further renaming of ntt_layer45_slice() to ntt_layer45_inner() Signed-off-by: Rod Chapman <[email protected]> Rename *_slice() to *_inner() functions - phase 1 Signed-off-by: Rod Chapman <[email protected]> Rename *_slice() functions to *_inner() - phase 2 Signed-off-by: Rod Chapman <[email protected]> renaming *slioce() to *inner() - phase 3 Signed-off-by: Rod Chapman <[email protected]> Display final 4 lines of logs/result.txt after make result Signed-off-by: Rod Chapman <[email protected]> Rename inner to butterfly for all internal ntt functions Signed-off-by: Rod Chapman <[email protected]> Rename harness function source files Signed-off-by: Rod Chapman <[email protected]> Adjust proof Makefiles and harnesses for renaming inner to butterfly Signed-off-by: Rod Chapman <[email protected]> Update Makefiles for function renaming Signed-off-by: Rod Chapman <[email protected]> Rename all inner functions to butterfly Signed-off-by: Rod Chapman <[email protected]> Replace literal 255 with (MLKEM_N - 1) throughout Signed-off-by: Rod Chapman <[email protected]> Move declaration of Zeta tables to be as close to their point of first use as possible. Add and adjust comments. Signed-off-by: Rod Chapman <[email protected]> Align and rename Zetas tables. Signed-off-by: Rod Chapman <[email protected]> Zetas tables are all declared with static scope Signed-off-by: Rod Chapman <[email protected]> Auto-generate Zeta tables for new layer-merged NTT Signed-off-by: Rod Chapman <[email protected]> This proof no longer needs zetas.c as a source file Signed-off-by: Rod Chapman <[email protected]> Move basemul_cached() function from ntt.[hc] to poly.c It is now local, and static within poly.c, so is amenable to inlining and auto-vectorization within that unit. Signed-off-by: Rod Chapman <[email protected]> Make basemul_cached() inline-able Signed-off-by: Rod Chapman <[email protected]> Add top-level explanatory comments Signed-off-by: Rod Chapman <[email protected]> Clarify and correct 1 typo in comment only. Signed-off-by: Rod Chapman <[email protected]> Move symlink from zetas.c to zetas.i Signed-off-by: Rod Chapman <[email protected]> Correct INVNTT_BOUND_REF for new implementation of Inverse NTT Signed-off-by: Rod Chapman <[email protected]> Add MLKEM_NAMESPACE to mlkem_layer7_zetas, since it is a global symbol Signed-off-by: Rod Chapman <[email protected]> Remove boilerplate comments from proof harness sources. Signed-off-by: Rod Chapman <[email protected]> Updates for namespacing of all static functions. Signed-off-by: Rod Chapman <[email protected]> Update this file following changes to other files Signed-off-by: Rod Chapman <[email protected]> Remove pc typedef and use int16_t r[MLKEM_N] instead throughout Signed-off-by: Rod Chapman <[email protected]> Adds namespacing to all static constant lookup tables. In support of the monolithic build. Signed-off-by: Rod Chapman <[email protected]> Update auto-generates files following name-spacing of Zeta tables Signed-off-by: Rod Chapman <[email protected]> Remove declaration of basmul_cached() from ntt.h following rebase against PR 623 Signed-off-by: Rod Chapman <[email protected]> Correct declaration of basemul_cached() to be static Signed-off-by: Rod Chapman <[email protected]> basemul_cached() is explicitly static, so does not also need MLKEM_NATIVE_INTERNAL_API Signed-off-by: Rod Chapman <[email protected]> remove sym link to zetas.c Signed-off-by: Rod Chapman <[email protected]> Add new symlink for zetas.i Signed-off-by: Rod Chapman <[email protected]> Add internal ct_butterfly() function and use it in ntt_layer123() Same for other NTT layers and InvNTT is TBD. Signed-off-by: Rod Chapman <[email protected]> Update autogenerated file Signed-off-by: Rod Chapman <[email protected]> Update invariant and constants for exclusive array bounds checks. Updates only ntt_layer123() for now to confirm effectiveness of updates. Other functions will be updated once all is well. Signed-off-by: Rod Chapman <[email protected]> Update proofs for exclusive upper bound. 1. Upper bound of quantitied ranges is now exclusive 2. Upper bound of array element range constraint is now exclusive. Signed-off-by: Rod Chapman <[email protected]> Re-generate all auto-generated files after rebase Signed-off-by: Rod Chapman <[email protected]> Use inner ct_butterfly() function in all forward NTT functions. Signed-off-by: Rod Chapman <[email protected]> Updates for readability following review. Introduces local gs_butterfly_reduce() and gs_butterfly_defer() functions, which are inlined for both compilation and proof, but significantly simplify and improve readability of the calling functions. Signed-off-by: Rod Chapman <[email protected]> Update auto-generated files after rebase Signed-off-by: Rod Chapman <[email protected]> Remove final STATIC_ASSERT() macro use Signed-off-by: Rod Chapman <[email protected]> Switch to unsigned type for loop index variables. Signed-off-by: Rod Chapman <[email protected]> Clarify comment on vectorization strategy Signed-off-by: Rod Chapman <[email protected]> Remove redundant proof files no longer needed on this branch. Signed-off-by: Rod Chapman <[email protected]> Correct use of BOUND() macro to debug_assert_abs_bound() Signed-off-by: Rod Chapman <[email protected]> Use "unsigned" where possible for zeta_index, start formal parameters and loop index variables. Drop redundant lower-bound for these objects in pre-conditions and loop invariants. Signed-off-by: Rod Chapman <[email protected]> Correct bound pre-condition on basemul_cached() Signed-off-by: Rod Chapman <[email protected]>
1 parent c79b97a commit 16cdf94

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

63 files changed

+1902
-322
lines changed

‎examples/bring_your_own_fips202/mlkem_native/zetas.c

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎examples/bring_your_own_fips202/mlkem_native/zetas.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../../../mlkem/zetas.i

‎examples/custom_backend/mlkem_native/mlkem/zetas.c

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎examples/custom_backend/mlkem_native/mlkem/zetas.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../../../../mlkem/zetas.i

‎examples/monolithic_build/mlkem_native_monobuild.c

Lines changed: 138 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@
2828
#include "mlkem/polyvec.c"
2929
#include "mlkem/rej_uniform.c"
3030
#include "mlkem/verify.c"
31-
#include "mlkem/zetas.c"
3231

3332
#if !defined(MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES)
3433
#include "mlkem/fips202/fips202.c"
@@ -1314,18 +1313,123 @@
13141313
#endif
13151314

13161315
/* mlkem/ntt.c */
1317-
#if defined(invntt_layer)
1318-
#undef invntt_layer
1316+
#if defined(MONT_F)
1317+
#undef MONT_F
13191318
#endif
13201319

13211320
/* mlkem/ntt.c */
1322-
#if defined(ntt_butterfly_block)
1323-
#undef ntt_butterfly_block
1321+
#if defined(NTT_BOUND1)
1322+
#undef NTT_BOUND1
13241323
#endif
13251324

13261325
/* mlkem/ntt.c */
1327-
#if defined(ntt_layer)
1328-
#undef ntt_layer
1326+
#if defined(NTT_BOUND2)
1327+
#undef NTT_BOUND2
1328+
#endif
1329+
1330+
/* mlkem/ntt.c */
1331+
#if defined(NTT_BOUND4)
1332+
#undef NTT_BOUND4
1333+
#endif
1334+
1335+
/* mlkem/ntt.c */
1336+
#if defined(NTT_BOUND6)
1337+
#undef NTT_BOUND6
1338+
#endif
1339+
1340+
/* mlkem/ntt.c */
1341+
#if defined(NTT_BOUND7)
1342+
#undef NTT_BOUND7
1343+
#endif
1344+
1345+
/* mlkem/ntt.c */
1346+
#if defined(NTT_BOUND8)
1347+
#undef NTT_BOUND8
1348+
#endif
1349+
1350+
/* mlkem/ntt.c */
1351+
#if defined(ct_butterfly)
1352+
#undef ct_butterfly
1353+
#endif
1354+
1355+
/* mlkem/ntt.c */
1356+
#if defined(gs_butterfly_defer)
1357+
#undef gs_butterfly_defer
1358+
#endif
1359+
1360+
/* mlkem/ntt.c */
1361+
#if defined(gs_butterfly_reduce)
1362+
#undef gs_butterfly_reduce
1363+
#endif
1364+
1365+
/* mlkem/ntt.c */
1366+
#if defined(invntt_layer321)
1367+
#undef invntt_layer321
1368+
#endif
1369+
1370+
/* mlkem/ntt.c */
1371+
#if defined(invntt_layer54)
1372+
#undef invntt_layer54
1373+
#endif
1374+
1375+
/* mlkem/ntt.c */
1376+
#if defined(invntt_layer54_butterfly)
1377+
#undef invntt_layer54_butterfly
1378+
#endif
1379+
1380+
/* mlkem/ntt.c */
1381+
#if defined(invntt_layer6)
1382+
#undef invntt_layer6
1383+
#endif
1384+
1385+
/* mlkem/ntt.c */
1386+
#if defined(invntt_layer6_butterfly)
1387+
#undef invntt_layer6_butterfly
1388+
#endif
1389+
1390+
/* mlkem/ntt.c */
1391+
#if defined(invntt_layer7_invert)
1392+
#undef invntt_layer7_invert
1393+
#endif
1394+
1395+
/* mlkem/ntt.c */
1396+
#if defined(invntt_layer7_invert_butterfly)
1397+
#undef invntt_layer7_invert_butterfly
1398+
#endif
1399+
1400+
/* mlkem/ntt.c */
1401+
#if defined(ntt_layer123)
1402+
#undef ntt_layer123
1403+
#endif
1404+
1405+
/* mlkem/ntt.c */
1406+
#if defined(ntt_layer45)
1407+
#undef ntt_layer45
1408+
#endif
1409+
1410+
/* mlkem/ntt.c */
1411+
#if defined(ntt_layer45_butterfly)
1412+
#undef ntt_layer45_butterfly
1413+
#endif
1414+
1415+
/* mlkem/ntt.c */
1416+
#if defined(ntt_layer6)
1417+
#undef ntt_layer6
1418+
#endif
1419+
1420+
/* mlkem/ntt.c */
1421+
#if defined(ntt_layer6_butterfly)
1422+
#undef ntt_layer6_butterfly
1423+
#endif
1424+
1425+
/* mlkem/ntt.c */
1426+
#if defined(ntt_layer7)
1427+
#undef ntt_layer7
1428+
#endif
1429+
1430+
/* mlkem/ntt.c */
1431+
#if defined(ntt_layer7_butterfly)
1432+
#undef ntt_layer7_butterfly
13291433
#endif
13301434

13311435
/* mlkem/ntt.h */
@@ -1334,8 +1438,8 @@
13341438
#endif
13351439

13361440
/* mlkem/ntt.h */
1337-
#if defined(basemul_cached)
1338-
#undef basemul_cached
1441+
#if defined(layer7_zetas)
1442+
#undef layer7_zetas
13391443
#endif
13401444

13411445
/* mlkem/ntt.h */
@@ -1348,11 +1452,6 @@
13481452
#undef poly_ntt
13491453
#endif
13501454

1351-
/* mlkem/ntt.h */
1352-
#if defined(zetas)
1353-
#undef zetas
1354-
#endif
1355-
13561455
/* mlkem/params.h */
13571456
#if defined(KECCAK_WAY)
13581457
#undef KECCAK_WAY
@@ -1463,6 +1562,11 @@
14631562
#undef UINT12_LIMIT
14641563
#endif
14651564

1565+
/* mlkem/poly.c */
1566+
#if defined(basemul_cached)
1567+
#undef basemul_cached
1568+
#endif
1569+
14661570
/* mlkem/poly.h */
14671571
#if defined(INVNTT_BOUND)
14681572
#undef INVNTT_BOUND
@@ -1863,6 +1967,26 @@
18631967
#undef MLKEM_NATIVE_SYS_H
18641968
#endif
18651969

1970+
/* mlkem/sys.h */
1971+
#if defined(NO_INLINE)
1972+
#undef NO_INLINE
1973+
#endif
1974+
1975+
/* mlkem/sys.h */
1976+
#if defined(NO_INLINE)
1977+
#undef NO_INLINE
1978+
#endif
1979+
1980+
/* mlkem/sys.h */
1981+
#if defined(NO_INLINE)
1982+
#undef NO_INLINE
1983+
#endif
1984+
1985+
/* mlkem/sys.h */
1986+
#if defined(NO_INLINE)
1987+
#undef NO_INLINE
1988+
#endif
1989+
18661990
/* mlkem/sys.h */
18671991
#if defined(RESTRICT)
18681992
#undef RESTRICT

0 commit comments

Comments
 (0)