[Prover][Compiler-v2] add spec block to lambda expressions

[rahxephon89]

Description

This PR extends the language to allow spec block to be attached to lambda expression:

    public fun test_inline_1() {
        let v = vector[1u64, 2, 3];
        let z;
        inline_1(&mut v, |e| { *e = 2; b.v = 3; z = 2; (*e > 1, z == 2) }
        spec {
            requires e == 1;
            ensures e == 2;
            ensures z == 2;
            ensures result_1 == (e > 1);
            ensures result_2;
        }
        );
    }

Currently, only requires and ensures are supported in the spec block. Support of let, let post and old will be implemented in a separate PR.

How Has This Been Tested?

1. existing tests pass;
2. add a new prover test.

Key Areas to Review

Type of Change

• New feature
• Bug fix
• Breaking change
• Performance improvement
• Refactoring
• Dependency update
• Documentation update
• Tests

Which Components or Systems Does This Change Impact?

• Validator Node
• Full Node (API, Indexer, etc.)
• Move/Aptos Virtual Machine
• Aptos Framework
• Aptos CLI/SDK
• Developer Infrastructure
• Move Compiler
• Move prover

Checklist

• I have read and followed the CONTRIBUTING doc
• I have performed a self-review of my own code
• I have commented my code, particularly in hard-to-understand areas
• I identified and added all stakeholders and component owners affected by this change as reviewers
• I tested both happy and unhappy path of the functionality
• I have made corresponding changes to the documentation

[trunk-io]

⏱️ 1h total CI duration on this PR

Job	Cumulative Duration	Recent Runs
rust-targeted-unit-tests	28m	🟩
check-dynamic-deps	13m	🟩 🟩 🟩 🟩 🟩 (+1 more)
rust-cargo-deny	11m	🟩 🟩 🟩 🟩 🟩 (+1 more)
semgrep/ci	4m	🟩 🟩 🟩 🟩 🟩 (+1 more)
general-lints	3m	🟩 🟩 🟩 🟩 🟩 (+1 more)
file_change_determinator	1m	🟩 🟩 🟩 🟩 🟩 (+1 more)
permission-check	17s	🟩 🟩 🟩 🟩 🟩 (+1 more)
permission-check	12s	🟩 🟩 🟩 🟩 🟩 (+1 more)

_{settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io}

[rahxephon89]

• [Prover][Compiler-v2] add spec block to lambda expressions #15916 👈 (View in Graphite)
• main

This stack of pull requests is managed by Graphite. Learn more about stacking.

[rahxephon89]

don't do anything because spec is not supported in compiler V1