Skip to content

Commit 5b068c6

Browse files
committed
Simplify loop invariant in ntt_2_layers()
Signed-off-by: Rod Chapman <[email protected]>
1 parent e6f6e79 commit 5b068c6

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

mlkem/poly.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -369,7 +369,8 @@ __contract__(
369369
invariant(start < MLKEM_N + 2 * len)
370370
invariant(len % 2 == 0)
371371
invariant(len == 4 || len == 8 || len == 16 || len == 32 || len == 64 || len == 128)
372-
invariant(k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N)
372+
invariant(k <= MLKEM_N / 2)
373+
invariant(2 * len * k == start + MLKEM_N)
373374
invariant(array_abs_bound(r, 0, start, (layer + 2) * MLKEM_Q))
374375
invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q))
375376
)

0 commit comments

Comments
 (0)