[move-prover] add test cases for lambda lifting and inlining

language/move-prover/tests/sources/functional/inline-lambda.exp

@@ -0,0 +1,45 @@
+Move prover returns: exiting with verification errors
+error: unknown assertion failed
+  ┌─ tests/sources/functional/inline-lambda.move:5:13
+  │
+5 │             assert predicate(v);
+  │             ^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/inline-lambda.move:10: test_apply
+  =         a1 = <redacted>
+  =         a2 = <redacted>
+  =     at tests/sources/functional/inline-lambda.move:11: test_apply
+  =         v#0 = <redacted>
+  =     at tests/sources/functional/inline-lambda.move:4
+  =     at tests/sources/functional/inline-lambda.move:5
+  =     at tests/sources/functional/inline-lambda.move:11: test_apply
+  =         r1 = <redacted>
+  =     at tests/sources/functional/inline-lambda.move:13: test_apply
+  =     at tests/sources/functional/inline-lambda.move:16: test_apply
+  =         v#3 = <redacted>
+  =     at tests/sources/functional/inline-lambda.move:4
+  =     at tests/sources/functional/inline-lambda.move:5
+
+error: unknown assertion failed
+   ┌─ tests/sources/functional/inline-lambda.move:18:13
+   │
+18 │             assert !r2;
+   │             ^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/inline-lambda.move:10: test_apply
+   =         a1 = <redacted>
+   =         a2 = <redacted>
+   =     at tests/sources/functional/inline-lambda.move:11: test_apply
+   =         v#0 = <redacted>
+   =     at tests/sources/functional/inline-lambda.move:4
+   =     at tests/sources/functional/inline-lambda.move:5
+   =     at tests/sources/functional/inline-lambda.move:11: test_apply
+   =         r1 = <redacted>
+   =     at tests/sources/functional/inline-lambda.move:13: test_apply
+   =     at tests/sources/functional/inline-lambda.move:16: test_apply
+   =         v#3 = <redacted>
+   =     at tests/sources/functional/inline-lambda.move:4
+   =     at tests/sources/functional/inline-lambda.move:5
+   =     at tests/sources/functional/inline-lambda.move:16: test_apply
+   =         r2 = <redacted>
+   =     at tests/sources/functional/inline-lambda.move:18: test_apply

language/move-prover/tests/sources/functional/inline-lambda.move

@@ -0,0 +1,21 @@
+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) {
+        let r1 = apply(0, |v| v >= 0);
+        spec {
+            assert r1;
+        };
+
+        let r2 = apply(0, |v| v != a1 + a2);
+        spec {
+            assert !r2;
+        };
+    }
+}