We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5823bd7 commit 00154b2Copy full SHA for 00154b2
mlkem/src/indcpa.c
@@ -329,17 +329,18 @@ __contract__(
329
mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc);
330
#endif
331
332
- // unsigned i;
333
- // for (i = 0; i < MLKEM_K; i++)
334
- // __loop__(
335
- // assigns(i, object_whole(out))
336
- // invariant(i <= MLKEM_K)
337
- // invariant(forall(k, 0, i,
338
- // array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))))
339
- // {
340
- // mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v,
341
- // vc);
342
- // }
+ /* unsigned i;
+ * for (i = 0; i < MLKEM_K; i++)
+ * __loop__(
+ * assigns(i, object_whole(out))
+ * invariant(i <= MLKEM_K)
+ * invariant(forall(k, 0, i,
+ * array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))))
+ * {
+ * mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v,
+ * vc);
+ * }
343
+ */
344
}
345
346
/* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF].
0 commit comments