[move-prover] loop unrolling

[meng-xu-cs]

Prover now supports bounded loop unrolling with

invariant [unroll = <iteration-limit>] true;

The semantics of loop unrolling aligns with most of the bounded model checking work, which can be illustrated below:

loop {
    invariant [unroll = N] true;
    assert C1;
}
assert C2;

• If C1 holds for iteration 0, 1, ..., N, the prover will not complain about C1, even when C1 fails in the K-th iteration (K > N).
• If C2 holds when loop exits within 0, 1, ... N iterations, the prover will not complain about C2, even when C2 fails when loop exits after K iterations (K > N).

This is evident in the loop_unroll.move test case.

Motivation

(Write your motivation for proposed changes here.)

Have you read the Contributing Guidelines on pull requests?

(Write your answer here.)

Test Plan

(Share your test plan here. If you changed code, please provide us with clear instructions for verifying that your changes work.)

[wrwg]

Do you mind filing this in third_party/move? You can also do here but this is ready now

On Sat, Mar 18, 2023 at 5:47 PM Meng Xu @.***> wrote:

Motivation

(Write your motivation for proposed changes here.) Have you read the Contributing Guidelines on pull requests https://github.com/move-language/move/blob/main/CONTRIBUTING.md#developer-workflow ?

(Write your answer here.) Test Plan

(Share your test plan here. If you changed code, please provide us with clear instructions for verifying that your changes work.)

You can view, comment on, or merge this pull request online at:

https://github.com/move-language/move/pull/992 Commit Summary

• f498d35 https://github.com/move-language/move/pull/992/commits/f498d3585d60d44085979f21018c5e0d821d44c1 [move-prover] add a hook-point for loop unrolling workflow

File Changes

(1 file https://github.com/move-language/move/pull/992/files)

• M language/move-prover/bytecode/src/loop_analysis.rs https://github.com/move-language/move/pull/992/files#diff-9ba6c6dec301c0ccc9e7bcdfa4e2b7b073d3c2a9af600e187889a2e97d3b3b75 (71)

Patch Links:

• https://github.com/move-language/move/pull/992.patch
• https://github.com/move-language/move/pull/992.diff

— Reply to this email directly, view it on GitHub https://github.com/move-language/move/pull/992, or unsubscribe https://github.com/notifications/unsubscribe-auth/AC2MSOWADKCMC4HSC4TK4J3W4ZJRZANCNFSM6AAAAAAV7Y3YO4 . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[meng-xu-cs]

Will move it to third_party/move.

[meng-xu-cs]

Run into some issues with third_party/move (mostly due to not being on a Mac). Plus, as I am not sure how test cases are run there, I'll develop here for a bit longer and once I get tests passing I'll patch up third_party/move and submit PRs from there.

[wrwg]

Run into some issues with third_party/move (mostly due to not being on a Mac). Plus, as I am not sure how test cases are run there, I'll develop here for a bit longer and once I get tests passing I'll patch up third_party/move and submit PRs from there.

Not sure what issues that could be. You do not need to run copybara, only 'admins' do this. Relevant tests in third_party/move are all run as part of standard CI. But no issue to develop here and then sync into aptos-core.

[junkil-park]

@meng-xu-cs , this PR seems to have merge conflicts.