[Bug] Simple for-loop verification fails

[franck44]

🐛 Bug

This bug is related to the use the Move Prover.
There seems to be some issues with the encoding of for-loops in Boogie.
Any for-loop seems to have an abort path, leading to EXECUTION_FAILURE. The problem is illustrated below with a minimal example (a loop that with an empty body). Hopefully, this will help to fix the problem.

To reproduce

Code snippet to reproduce

The code snippet to reproduce the error is:

module 0x02::SimpleLoop {
// Spec of the loop. Does not abort
spec loop1(k: u8): () {
        aborts_if false;
    }

// simple function. Does nothing
fun loop1(k: u8): () {
        for (i in 0..k) 
          {

           };
    }
}

Stack trace/error message

simpleloop git:(master) ✗ aptos move prove 
[INFO] preparing module 0x2:: SimpleLoop
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 5 verification conditions
[INFO] running solver
[INFO] 0.223s build, 0.008s trafo, 0.016s gen, 0.920s verify, total 1.166s
error: abort not covered by any of the `aborts_if` clauses
   ┌─ move-learning/simpleloop/sources/simpleloop.move:46:5
   │    
46 │ ╭       spec loop1(k: u8): () {
47 │ │           aborts_if false;
48 │ │       }
   │ ╰───────^
   · │  
51 │   ╭         for (i in 0..k)
52 │   │         {
53 │   │ 
54 │   │         };
   │   ╰─────────' abort happened here with execution failure
   │    
   =     at move-learning/simpleloop/sources/simpleloop.move:50: loop1
   =         k = 190u8
   =     atmove-learning/simpleloop/sources/simpleloop.move:51: loop1
   =         i = 0u8
   =         __update_iter_flag = false
   =     at move-learning/simpleloop/sources/simpleloop.move:51: loop1
   =     enter loop, variable(s) i, __update_iter_flag havocked and reassigned
   =         i = 255u8
   =         __update_iter_flag = true
   =         ABORTED

{
  "Error": "Move Prover failed: exiting with verification errors"
}

The same behaviour is observed with the Move-2 version (running Aptos move prove --move-2.

Expected Behavior

The expected behaviour is that the spec verifies as there is no overflow and no code in the body.

System information

Please complete the following information:

• Aptos Core Version

simpleloop git:(master) ✗ aptos --version
aptos 4.4.0

• Rust Version
  NA
• Computer OS
  MacOS.

Additional context

In a separate discussion (Tg/slack) I already reported some difficulties in proving loop invariants with for-loops. It looks like for-loops are not translated into equivalent while-loops: for example I can prove while-loop invariants using a loop counter that I update manually, but I am unable to prove the same properties with afor-loop.
@rahxephon89 explained the limitation to me, but the problem I reported above seems to suggest that the for-loop encoding into boogie is flawed.

Related issue: issue #15022