[move-prover] add the unroll pragma

[meng-xu-cs]

We now support both function-level and module-level

pragma unroll = <depth-limit>;

The effect of specifying this pragma is:

• if a loop is in the function/module and has loop invariants, this pragma has no effect. The loop will still be verified against loop invariants.
• if a loop is in the function/module and has no loop invariants, if the loop has a spec block with invariant [unroll = K] true;, unroll the loop K times.
• if a loop is in the function/module and has no loop invariants, and has no per-loop unrolling instruction, use the pramga's count to unroll the loop.

The effect of this pragma is illustrated in the loop_unroll.move test case.

Motivation

More coarse-grained (and user-friendly) loop unrolling annotation

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

CI