[Bug][Prover] loop invariants of for loops are not intuitive

[rahxephon89]

🐛 Bug

loop1 and loop2 are functionally equivalent but the loop invariant in the for loop cannot be proved because of the way how it is rewritten into a while loop. To avoid confusion for users, we need to improve documentation.

      fun loop1 (xs: &vector<u8>): vector<u8> {
        let r = vector<u8>[];
        for (
            i in 0..vector::length(xs)
            spec { invariant i == len(r); } // cannot be proved because of how i it is updated
        )
        {
            vector::push_back(&mut r, *vector::borrow(xs, i));
        };
        r
    }

    fun loop2 (xs: &vector<u8>): vector<u8> {
        let r = vector<u8>[];
        let i = 0;
        while ({
            spec { invariant i == len(r); }; // can be proved
            i < vector::length(xs)
        })
        {
            vector::push_back(&mut r, *vector::borrow(xs, i));
            i = i + 1
        };
        r
    }