[move-compiler][move-model] complete the lambda lifting part

[meng-xu-cs]

This is to piggyback compiler and prover support of translating move functions that are generated after lambda lifting.

The complete workflow of the verificaiton compilation will be like this:

1. compile to expansion AST (short for E-AST), take a copy
2. compile E-AST until inlining to get inlined AST (short for I-AST)
3. extract functions generated out of lambda lifting, downgrade its AST into expansion AST. Add these new expansion AST to E-AST and call it E-AST'
4. compile resumes from E-AST' and up until compiled units.

In this way, the lambda lifted functions will be recognized by move-model in later phases as if the developers write them in the code.

To take a concrete example, the following program will be converted to AST at the expansion level that is equilavent as if the developers write the two lambda-lifted functions in the source code:

module 0x42::Test {
    inline fun apply(v: u64, predicate: |u64| bool): bool {
        spec {
            assert v != 42;
            assert predicate(v);
        };
        predicate(v)
    }

    public fun test_apply(a1: u64, a2: u64) {
        apply(0, |v| v >= 0);
        apply(0, |v| v != a1 + a2);
    }
}

After inlining and lambda-lifting:

module 0x42::Test {
    public fun test_apply(a1: u64, a2: u64) {
        /* inlined */
        spec {
            assert 0 != 42;
            assert test_apply_predicate_0(0);
        }
        test_apply_predicate_0(0);

        /* inlined */
        spec {
            assert 0 != 42;
            assert test_apply_predicate_1(0);
        }
        test_apply_predicate_1(0);
    }

    /* generated */
    fun test_apply_predicate_0(v: u64): bool {
        v >= 0
    }
    /* move-model will create spec fun automatically */

    /* generated */
    fun test_apply_predicate_1(v: u64, a1: u64, a2: u64): bool {
        v != a1 + a2
    }
    /* move-model will create spec fun automatically */
}

Motivation

Complete the inlining feature in spec world

This, combined with two previously landed PRs #879, #891 completes the support of inlining of inline specs (yes, a lot of inlining).

The compiler changes are mostly confined to two places:

• the Spec(..) variant in various AST trees and
• the inlining pass

The move-model changes are mostly for downgrading inlining AST (i.e., typing AST) to expansion AST and a slight modification of the compilation workflow (i.e., to include the enriched expansion AST).

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

• CI
• a new test case