Loops without side effect

[W95Psp]

Currently, extracting a loop whose body performs no side effect results in the following error:

error[HAX0001]: (FunctionalizeLoops) something is not implemented yet.
                Loop without mutation?

This error comes from the phase FunctionalizeLoops, which --for now-- assumes purity. Under the assumption things are pure, a loop without side effect is a no op; such a loop is useless but should be supported anyway. Also, some backend might use FunctionalizeLoops without assuming purity.

Examples of loops without side effect

for i in i..10 {
   // empty body
}

for i in i..10 {
   f(i)
}

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

It seems like this still reproduce, but I recall you did something around this @maximebuyse: do you remember something as well?

[maximebuyse]

It seems like this still reproduce, but I recall you did something around this @maximebuyse: do you remember something as well?

Yes, the case I fixed is when the only side effect is a return.

[cmester0]

We also run into this issue when translating ElectionGuard

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[franziskuskiefer]

Lets allow this, maybe add a warning.

[franziskuskiefer]

What's the state of this? We run into this in libcrux code.

[W95Psp]

Sorry Franziskus, I missed that comment. @maximebuyse I think we wanted to fix this at some point, this should not be too complicated, what do you think?

[maximebuyse]

Sorry Franziskus, I missed that comment. @maximebuyse I think we wanted to fix this at some point, this should not be too complicated, what do you think?

Yes, I can try to find the time for that this week.

[franziskuskiefer]

I think the title is also a little misleading as the same error is thrown when there's something panicking in the loop. For example, adding an assert!(i < 10); to the example throws the same error.

[W95Psp]

Indeed, I agree: from a Rust perspective, an assert (that is, a conditional panic) can be seen as a side effect.

However, in hax, panics are not effectful: a panic is translated to a point in the program where we have to provide a proof that this point is unreachable. Similarly, every function in hax is supposed to be faithful to its signature: if the signature is pure, then the function is assumed to be pure. So if a loop body calls a function f that actually writes to disk, this error will show up.