Skip to content

Commit 8cea961

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]> Update auto-generated files after rebase Signed-off-by: Rod Chapman <[email protected]> Correct new CPP directives following rebase Signed-off-by: Rod Chapman <[email protected]> Restore basemul_cached() in poly.c following rebase. Signed-off-by: Rod Chapman <[email protected]> Switches to use "unsigned" not "int" for all coefficient indexes. Consistent with a similar change to the reference code on main branch. Signed-off-by: Rod Chapman <[email protected]>
1 parent 21c0c39 commit 8cea961

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

+1900
-331
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: 121 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@
2525
#include "mlkem/polyvec.c"
2626
#include "mlkem/rej_uniform.c"
2727
#include "mlkem/verify.c"
28-
#include "mlkem/zetas.c"
2928

3029

3130
/*
@@ -1144,24 +1143,129 @@
11441143
#undef KeccakF1600x4_StateXORBytes
11451144
#endif
11461145

1146+
/* mlkem/ntt.c */
1147+
#if defined(MONT_F)
1148+
#undef MONT_F
1149+
#endif
1150+
1151+
/* mlkem/ntt.c */
1152+
#if defined(NTT_BOUND1)
1153+
#undef NTT_BOUND1
1154+
#endif
1155+
1156+
/* mlkem/ntt.c */
1157+
#if defined(NTT_BOUND2)
1158+
#undef NTT_BOUND2
1159+
#endif
1160+
1161+
/* mlkem/ntt.c */
1162+
#if defined(NTT_BOUND4)
1163+
#undef NTT_BOUND4
1164+
#endif
1165+
1166+
/* mlkem/ntt.c */
1167+
#if defined(NTT_BOUND6)
1168+
#undef NTT_BOUND6
1169+
#endif
1170+
1171+
/* mlkem/ntt.c */
1172+
#if defined(NTT_BOUND7)
1173+
#undef NTT_BOUND7
1174+
#endif
1175+
1176+
/* mlkem/ntt.c */
1177+
#if defined(NTT_BOUND8)
1178+
#undef NTT_BOUND8
1179+
#endif
1180+
1181+
/* mlkem/ntt.c */
1182+
#if defined(ct_butterfly)
1183+
#undef ct_butterfly
1184+
#endif
1185+
11471186
/* mlkem/ntt.c */
11481187
#if defined(empty_cu_ntt)
11491188
#undef empty_cu_ntt
11501189
#endif
11511190

11521191
/* mlkem/ntt.c */
1153-
#if defined(invntt_layer)
1154-
#undef invntt_layer
1192+
#if defined(gs_butterfly_defer)
1193+
#undef gs_butterfly_defer
1194+
#endif
1195+
1196+
/* mlkem/ntt.c */
1197+
#if defined(gs_butterfly_reduce)
1198+
#undef gs_butterfly_reduce
1199+
#endif
1200+
1201+
/* mlkem/ntt.c */
1202+
#if defined(invntt_layer321)
1203+
#undef invntt_layer321
1204+
#endif
1205+
1206+
/* mlkem/ntt.c */
1207+
#if defined(invntt_layer54)
1208+
#undef invntt_layer54
1209+
#endif
1210+
1211+
/* mlkem/ntt.c */
1212+
#if defined(invntt_layer54_butterfly)
1213+
#undef invntt_layer54_butterfly
1214+
#endif
1215+
1216+
/* mlkem/ntt.c */
1217+
#if defined(invntt_layer6)
1218+
#undef invntt_layer6
1219+
#endif
1220+
1221+
/* mlkem/ntt.c */
1222+
#if defined(invntt_layer6_butterfly)
1223+
#undef invntt_layer6_butterfly
11551224
#endif
11561225

11571226
/* mlkem/ntt.c */
1158-
#if defined(ntt_butterfly_block)
1159-
#undef ntt_butterfly_block
1227+
#if defined(invntt_layer7_invert)
1228+
#undef invntt_layer7_invert
11601229
#endif
11611230

11621231
/* mlkem/ntt.c */
1163-
#if defined(ntt_layer)
1164-
#undef ntt_layer
1232+
#if defined(invntt_layer7_invert_butterfly)
1233+
#undef invntt_layer7_invert_butterfly
1234+
#endif
1235+
1236+
/* mlkem/ntt.c */
1237+
#if defined(ntt_layer123)
1238+
#undef ntt_layer123
1239+
#endif
1240+
1241+
/* mlkem/ntt.c */
1242+
#if defined(ntt_layer45)
1243+
#undef ntt_layer45
1244+
#endif
1245+
1246+
/* mlkem/ntt.c */
1247+
#if defined(ntt_layer45_butterfly)
1248+
#undef ntt_layer45_butterfly
1249+
#endif
1250+
1251+
/* mlkem/ntt.c */
1252+
#if defined(ntt_layer6)
1253+
#undef ntt_layer6
1254+
#endif
1255+
1256+
/* mlkem/ntt.c */
1257+
#if defined(ntt_layer6_butterfly)
1258+
#undef ntt_layer6_butterfly
1259+
#endif
1260+
1261+
/* mlkem/ntt.c */
1262+
#if defined(ntt_layer7)
1263+
#undef ntt_layer7
1264+
#endif
1265+
1266+
/* mlkem/ntt.c */
1267+
#if defined(ntt_layer7_butterfly)
1268+
#undef ntt_layer7_butterfly
11651269
#endif
11661270

11671271
/* mlkem/ntt.h */
@@ -1170,8 +1274,8 @@
11701274
#endif
11711275

11721276
/* mlkem/ntt.h */
1173-
#if defined(basemul_cached)
1174-
#undef basemul_cached
1277+
#if defined(layer7_zetas)
1278+
#undef layer7_zetas
11751279
#endif
11761280

11771281
/* mlkem/ntt.h */
@@ -1184,9 +1288,9 @@
11841288
#undef poly_ntt
11851289
#endif
11861290

1187-
/* mlkem/ntt.h */
1188-
#if defined(zetas)
1189-
#undef zetas
1291+
/* mlkem/poly.c */
1292+
#if defined(basemul_cached)
1293+
#undef basemul_cached
11901294
#endif
11911295

11921296
/* mlkem/poly.c */
@@ -1544,6 +1648,11 @@
15441648
#undef MLKEM_NATIVE_SYS_H
15451649
#endif
15461650

1651+
/* mlkem/sys.h */
1652+
#if defined(NO_INLINE)
1653+
#undef NO_INLINE
1654+
#endif
1655+
15471656
/* mlkem/sys.h */
15481657
#if defined(RESTRICT)
15491658
#undef RESTRICT
@@ -1654,9 +1763,4 @@
16541763
#undef value_barrier_u8
16551764
#endif
16561765

1657-
/* mlkem/zetas.c */
1658-
#if defined(empty_cu_zetas)
1659-
#undef empty_cu_zetas
1660-
#endif
1661-
16621766
#endif /* MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS */

0 commit comments

Comments
 (0)