[c-extraction] cloop! macro step_by variant can result in wrong iteration

[robinhundt]

The ml-kem and ml-dsa crates contain a cloop! macro that converts iterator adapters into imperative rust code for c extraction. There are bugs in the step_by variant of the macro (which are currently not hit by the existing uses).

The ML-KEM variant looks like this:

libcrux/libcrux-ml-kem/src/helper.rs

Lines 30 to 35 in e83007e

	(for $i:ident in ($start:literal..$end:expr).step_by($step:literal) $body:block) => {
	for $i in $start..$end / $step {
	let $i = $i * $step;
	$body
	}
	};

Here, there are two issues:

• the loop is only correct if $start == 0
• the loop is only correct if $end % $step == 0

If one of them is false, it would result in a wrong loop.

In ml-dsa the step_by variant is slightly different and the second issue was fixed. The first issue is still present. In ml-dsa, there is actually a use of the cloop! macro with a step that doesn't divide the end, which is why it was probably fixed already. In ml-kem, there is currently no such use.

libcrux/libcrux-ml-dsa/src/helper.rs

Lines 60 to 66 in e83007e

	(for $i:ident in ($start:literal..$end:expr).step_by($step:literal) $body:block) => {
	for $i in ($start..($end / $step + 1)) {
	let $i = $i * $step;
	if $i >= $end { break; }
	$body
	}
	};

I first noticed this issue in libcrux-iot and submitted a PR there to fix it, for which the C extraction currently doesn't compile celabshq/libcrux-iot#191.