Re-baseline and introduce new fast NTT and inverse NTT

code, following source re-organization in PR#674.

See comments on older PR#610.

All tests, proofs, and lint OK.

Signed-off-by: Rod Chapman <[email protected]>

Correct list of called functions for this proof.

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

examples/monolithic_build/mlkem_native_monobuild.c

@@ -1233,6 +1233,41 @@
 #undef KeccakF1600x4_StateXORBytes
 #endif
 
+/* mlkem/poly.c */
+#if defined(MONT_F)
+#undef MONT_F
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND1)
+#undef NTT_BOUND1
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND2)
+#undef NTT_BOUND2
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND4)
+#undef NTT_BOUND4
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND6)
+#undef NTT_BOUND6
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND7)
+#undef NTT_BOUND7
+#endif
+
+/* mlkem/poly.c */
+#if defined(NTT_BOUND8)
+#undef NTT_BOUND8
+#endif
+
 /* mlkem/poly.c */
 #if defined(barrett_reduce)
 #undef barrett_reduce
@@ -1248,6 +1283,11 @@
 #undef cast_uint16_to_int16
 #endif
 
+/* mlkem/poly.c */
+#if defined(ct_butterfly)
+#undef ct_butterfly
+#endif
+
 /* mlkem/poly.c */
 #if defined(empty_cu_poly)
 #undef empty_cu_poly
@@ -1259,8 +1299,38 @@
 #endif
 
 /* mlkem/poly.c */
-#if defined(invntt_layer)
-#undef invntt_layer
+#if defined(gs_butterfly_defer)
+#undef gs_butterfly_defer
+#endif
+
+/* mlkem/poly.c */
+#if defined(gs_butterfly_reduce)
+#undef gs_butterfly_reduce
+#endif
+
+/* mlkem/poly.c */
+#if defined(invntt_layer321)
+#undef invntt_layer321
+#endif
+
+/* mlkem/poly.c */
+#if defined(invntt_layer54)
+#undef invntt_layer54
+#endif
+
+/* mlkem/poly.c */
+#if defined(invntt_layer54_butterfly)
+#undef invntt_layer54_butterfly
+#endif
+
+/* mlkem/poly.c */
+#if defined(invntt_layer6)
+#undef invntt_layer6
+#endif
+
+/* mlkem/poly.c */
+#if defined(invntt_layer7_invert)
+#undef invntt_layer7_invert
 #endif
 
 /* mlkem/poly.c */
@@ -1274,13 +1344,28 @@
 #endif
 
 /* mlkem/poly.c */
-#if defined(ntt_butterfly_block)
-#undef ntt_butterfly_block
+#if defined(ntt_layer123)
+#undef ntt_layer123
+#endif
+
+/* mlkem/poly.c */
+#if defined(ntt_layer45)
+#undef ntt_layer45
+#endif
+
+/* mlkem/poly.c */
+#if defined(ntt_layer45_butterfly)
+#undef ntt_layer45_butterfly
+#endif
+
+/* mlkem/poly.c */
+#if defined(ntt_layer6)
+#undef ntt_layer6
 #endif
 
 /* mlkem/poly.c */
-#if defined(ntt_layer)
-#undef ntt_layer
+#if defined(ntt_layer7)
+#undef ntt_layer7
 #endif
 
 /* mlkem/poly.c */