Shaked Flur

Seams like the iterator of the range `0..1` confuses SH. If I change the loop to `let mut c = 0; while c < 1 { ...; c += 1;...

> Iterators are surprisingly complex - lots of method calls. > See the expansion at the bottom of [this page](https://doc.rust-lang.org/std/keyword.for.html) > With Rust optimization enabled, this goes away - but...

Here is the example with everything unfolded (I looked at mem::replace and it could be challenging for verifiers): ```rust struct MyRange { start: i32, end: i32, } impl MyRange {...

Ok, I didn't know this was intentional. Any point for leaving this issue open?

> Can you show me the more specific issue in IncrementWait? The example in this issue could be just written with a `delay` rather than loop. [cava1](https://github.com/project-oak/silveroak/blob/91e984733b0294dd52b2dc2481c24b34c510967a/firmware/IncrementWait/CavaIncrementDevice.v#L72) [cava2](https://github.com/project-oak/silveroak/blob/59688de9126ffda3d23c55fabac7364ce260043e/firmware/IncrementWait/CavaIncrementDevice.v#L29) Each of...

I haven't really looked at this PR yet but I noticed yesterday that `runUntilResp` is behaving wrong with respect to the TL protocol. The function should only send the h2d...