Repository: aptos-labs/aptos-core (language: python)

Issue:
[WIP][Prover] Support enum in the Move prover.
## Description
<!-- Please include a summary of the change, including which issue it fixes or what feature it adds. Include relevant motivation, context and documentation as appropriate. List dependencies that are required for this change, if any. -->

WIP

## 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
- [ ] Other (specify)

## How Has This Been Tested?
<!--
- Please ensure that the functionality introduced by this change is well tested and verified to work as expected.
- Ensure tests cover both happy and unhappy paths.
- List and link relevant tests.
-->

## Key Areas to Review
<!--
- Identify any critical parts of the code that require special attention or understanding. Explain why these parts are crucial to the functionality or architecture of the project.
- Point out any areas where complex logic has been implemented. Provide a brief explanation of the logic and your approach to make it easier for reviewers to follow.
- Highlight any areas where you are particularly concerned or unsure about the code's impact on the change. This can include potential performance or security issues, or compatibility with existing features.
-->

## Checklist
- [ ] I have read and followed the [CONTRIBUTING](https://github.com/aptos-labs/aptos-core/blob/main/CONTRIBUTING.md) 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

<!-- Thank you for your contribution! -->



Discussion / hints:
<!-- Trunk Metrics Report -->



<details>
<summary>
⏱️ 47m total CI duration on this PR
</summary>

| Job | Cumulative Duration | Recent Runs |
|---|---|---|
| [rust-move-unit-coverage](https://github.com/aptos-labs/aptos-core/actions/runs/10275381635/job/28433905680) | 14m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381635/job/28433905680)&#8201; |
| [rust-move-tests](https://github.com/aptos-labs/aptos-core/actions/runs/10360349206/job/28678600862) | 9m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349206/job/28678600862)&#8201; |
| [rust-move-tests](https://github.com/aptos-labs/aptos-core/actions/runs/10275381638/job/28433905779) | 8m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381638/job/28433905779)&#8201; |
| [rust-move-unit-coverage](https://github.com/aptos-labs/aptos-core/actions/runs/10360349205/job/28678600938) | 7m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349205/job/28678600938)&#8201; |
| [rust-cargo-deny](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678612549) | 3m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381636/job/28433913810)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678612549)&#8201; |
| [general-lints](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678612720) | 3m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381636/job/28433914068)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678612720)&#8201; |
| [check-dynamic-deps](https://github.com/aptos-labs/aptos-core/actions/runs/10360349207/job/28678600022) | 1m | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381643/job/28433905285)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349207/job/28678600022)&#8201; |
| [semgrep/ci](https://github.com/aptos-labs/aptos-core/actions/runs/10360349211/job/28678600249) | 42s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381634/job/28433904933)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349211/job/28678600249)&#8201; |
| [file_change_determinator](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678600662) | 22s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381636/job/28433905991)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349204/job/28678600662)&#8201; |
| [file_change_determinator](https://github.com/aptos-labs/aptos-core/actions/runs/10360349054/job/28678606647) | 21s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381649/job/28433910514)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349054/job/28678606647)&#8201; |
| [permission-check](https://github.com/aptos-labs/aptos-core/actions/runs/10360349054/job/28678599807) | 6s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381649/job/28433905932)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349054/job/28678599807)&#8201; |
| [permission-check](https://github.com/aptos-labs/aptos-core/actions/runs/10360349052/job/28678599421) | 6s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381640/job/28433905074)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349052/job/28678599421)&#8201; |
| [permission-check](https://github.com/aptos-labs/aptos-core/actions/runs/10360349064/job/28678599445) | 4s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381653/job/28433905101)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349064/job/28678599445)&#8201; |
| [permission-check](https://github.com/aptos-labs/aptos-core/actions/runs/10360349055/job/28678599661) | 4s | [🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10275381632/job/28433905855)&#8201;[🟩](https://github.com/aptos-labs/aptos-core/actions/runs/10360349055/job/28678599661)&#8201; |
</details>

<sub>[settings](https://app.trunk.io/aptoslabs/settings/aptos-labs/aptos-core#ci-analytics?utm_source=gh-comment) ⋅ [feedback](https://form.typeform.com/to/w7Iv34u2?utm_source=gh-comment) ⋅ [docs](https://docs.trunk.io/ci-analytics/pull-request-metrics?utm_source=gh-comment) ⋅ learn more about [trunk.io](https://trunk.io?utm_source=gh-comment)</sub>
## [Codecov](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?dropdown=coverage&src=pr&el=h1&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) Report
Attention: Patch coverage is `19.37500%` with `387 lines` in your changes missing coverage. Please review.
> Project coverage is 59.0%. Comparing base [(`447338f`)](https://app.codecov.io/gh/aptos-labs/aptos-core/commit/447338ffa0bd62a19e232a833fcff88c715bd3a3?dropdown=coverage&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) to head [(`ea7395c`)](https://app.codecov.io/gh/aptos-labs/aptos-core/commit/ea7395c5a02b221eb6eb418f470e58f3e0288afc?dropdown=coverage&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs).

| [Files](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?dropdown=coverage&src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) | Patch % | Lines |
|---|---|---|
| [...e-prover/boogie-backend/src/bytecode\_translator.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-prover%2Fboogie-backend%2Fsrc%2Fbytecode_translator.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLXByb3Zlci9ib29naWUtYmFja2VuZC9zcmMvYnl0ZWNvZGVfdHJhbnNsYXRvci5ycw==) | 25.4% | [263 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...move/move-model/bytecode/src/stackless\_bytecode.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-model%2Fbytecode%2Fsrc%2Fstackless_bytecode.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLW1vZGVsL2J5dGVjb2RlL3NyYy9zdGFja2xlc3NfYnl0ZWNvZGUucnM=) | 8.1% | [34 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...e/move-prover/boogie-backend/src/boogie\_helpers.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-prover%2Fboogie-backend%2Fsrc%2Fboogie_helpers.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLXByb3Zlci9ib29naWUtYmFja2VuZC9zcmMvYm9vZ2llX2hlbHBlcnMucnM=) | 0.0% | [29 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...arty/move/move-model/src/builder/module\_builder.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-model%2Fsrc%2Fbuilder%2Fmodule_builder.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLW1vZGVsL3NyYy9idWlsZGVyL21vZHVsZV9idWlsZGVyLnJz) | 0.0% | [18 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...ty/move/move-model/bytecode/src/borrow\_analysis.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-model%2Fbytecode%2Fsrc%2Fborrow_analysis.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLW1vZGVsL2J5dGVjb2RlL3NyYy9ib3Jyb3dfYW5hbHlzaXMucnM=) | 0.0% | [16 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...ode-pipeline/src/data\_invariant\_instrumentation.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-prover%2Fbytecode-pipeline%2Fsrc%2Fdata_invariant_instrumentation.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLXByb3Zlci9ieXRlY29kZS1waXBlbGluZS9zcmMvZGF0YV9pbnZhcmlhbnRfaW5zdHJ1bWVudGF0aW9uLnJz) | 0.0% | [14 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...prover/bytecode-pipeline/src/eliminate\_imm\_refs.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-prover%2Fbytecode-pipeline%2Fsrc%2Feliminate_imm_refs.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLXByb3Zlci9ieXRlY29kZS1waXBlbGluZS9zcmMvZWxpbWluYXRlX2ltbV9yZWZzLnJz) | 0.0% | [11 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |
| [...model/bytecode/src/stackless\_bytecode\_generator.rs](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&filepath=third_party%2Fmove%2Fmove-model%2Fbytecode%2Fsrc%2Fstackless_bytecode_generator.rs&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs#diff-dGhpcmRfcGFydHkvbW92ZS9tb3ZlLW1vZGVsL2J5dGVjb2RlL3NyYy9zdGFja2xlc3NfYnl0ZWNvZGVfZ2VuZXJhdG9yLnJz) | 0.0% | [2 Missing :warning: ](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs) |

<details><summary>Additional details and impacted files</summary>


```diff
@@            Coverage Diff            @@
##             main   #14233     +/-   ##
=========================================
- Coverage    59.2%    59.0%   -0.3%     
=========================================
  Files         832      832             
  Lines      202740   203134    +394     
=========================================
- Hits       120218   119904    -314     
- Misses      82522    83230    +708     
```

</details>

[:umbrella: View full report in Codecov by Sentry](https://app.codecov.io/gh/aptos-labs/aptos-core/pull/14233?dropdown=coverage&src=pr&el=continue&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs).   
:loudspeaker: Have feedback on the report? [Share it here](https://about.codecov.io/codecov-pr-comment-feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=aptos-labs).


Fix patch:
diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
index c18400902fb6c..bc221ee9b1a51 100644
--- a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
+++ b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
@@ -1025,8 +1025,10 @@ impl<'a> FunctionGenerator<'a> {
             if before && ctx.is_alive_before(temp)
                 || !before && ctx.is_alive_after(temp, &[], false)
                 || self.pinned.contains(&temp)
+                || !ctx.fun_ctx.is_droppable(temp)
             {
-                // Only need to save to a local if the temp is still used afterwards
+                // Only need to save to a local if the temp is still used afterwards, is pinned,
+                // or if it is not droppable
                 let local = self.temp_to_local(fun_ctx, Some(ctx.attr_id), temp);
                 self.emit(FF::Bytecode::StLoc(local));
             } else {
@@ -1147,6 +1149,14 @@ impl<'env> FunctionContext<'env> {
             .type_abilities(self.temp_type(temp), &self.type_parameters)
             .has_ability(FF::Ability::Copy)
     }
+
+    /// Returns true of the given temporary can/should be dropped when flushing the stack.
+    pub fn is_droppable(&self, temp: TempIndex) -> bool {
+        self.module
+            .env
+            .type_abilities(self.temp_type(temp), &self.type_parameters)
+            .has_ability(FF::Ability::Drop)
+    }
 }
 
 impl<'env> BytecodeContext<'env> {


Test patch:
diff --git a/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.exp b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.exp
new file mode 100644
index 0000000000000..90b32906711cc
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.exp
@@ -0,0 +1,2 @@
+
+============ bytecode verification succeeded ========
diff --git a/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.move b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.move
new file mode 100644
index 0000000000000..2631471a3b878
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable.move
@@ -0,0 +1,9 @@
+module 0xCAFE::Module0 {
+    struct S {}
+
+    public fun f() {
+        let _x = S {};
+        abort 1;
+        let S {} = _x;
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.exp b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.exp
new file mode 100644
index 0000000000000..7686f9261cd64
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.exp
@@ -0,0 +1,7 @@
+
+Diagnostics:
+error: local `_x` of type `Module0::S` does not have the `drop` ability
+  ┌─ tests/ability-check/bug_14223_unused_non_droppable_no_abort.move:5:18
+  │
+5 │         let _x = S {};
+  │                  ^^^^ implicitly dropped here since it is no longer used
diff --git a/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.move b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.move
new file mode 100644
index 0000000000000..7c6b1f1fe3699
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-check/bug_14223_unused_non_droppable_no_abort.move
@@ -0,0 +1,9 @@
+module 0xCAFE::Module0 {
+    struct S {}
+
+    public fun f() {
+        let _x = S {};
+        //abort 1;
+        //let S {} = _x;
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/testsuite.rs b/third_party/move/move-compiler-v2/tests/testsuite.rs
index d5b17091780b4..8ea35275b6a60 100644
--- a/third_party/move/move-compiler-v2/tests/testsuite.rs
+++ b/third_party/move/move-compiler-v2/tests/testsuite.rs
@@ -283,11 +283,11 @@ const TEST_CONFIGS: Lazy<BTreeMap<&str, TestConfig>> = Lazy::new(|| {
             dump_bytecode: DumpLevel::None,
             dump_bytecode_filter:
             // For debugging (dump_bytecode set DumpLevel::AllStages)
-             Some(vec![
-               INITIAL_BYTECODE_STAGE,
-               "ReferenceSafetyProcessor",
-               "DeadStoreElimination",
-               FILE_FORMAT_STAGE,
+            Some(vec![
+                INITIAL_BYTECODE_STAGE,
+                "ReferenceSafetyProcessor",
+                "DeadStoreElimination",
+                FILE_FORMAT_STAGE,
             ]),
         },
         // Reference safety tests (with optimizations on)
diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.exp
new file mode 100644
index 0000000000000..8cd76b4c72be3
--- /dev/null
+++ b/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.exp
@@ -0,0 +1,22 @@
+comparison between v1 and v2 failed:
+- processed 2 tasks
++ processed 2 tasks
+= 
+- task 0 'publish'. lines 1-10:
+- warning[W09005]: dead or unreachable code
+-   ┌─ TEMPFILE:7:9
+-   │
+- 7 │         let S {} = _x;
+-   │         ^^^^^^^^^^^^^ Unreachable code. This statement (and any following statements) will not be executed.
+- 
+- 
+- 
+= task 1 'run'. lines 12-12:
+= Error: Function execution failed with VMError: {
+=     major_status: ABORTED,
+=     sub_status: Some(1),
+=     location: 0xcafe::m,
+=     indices: redacted,
+=     offsets: redacted,
+= }
+= 
diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.move b/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.move
new file mode 100644
index 0000000000000..0eaa24fddaba4
--- /dev/null
+++ b/third_party/move/move-compiler-v2/transactional-tests/tests/optimization/bug_14223_unused_non_droppable.move
@@ -0,0 +1,12 @@
+//# publish
+module 0xCAFE::m {
+    struct S {}
+
+    public fun f() {
+        let _x = S {};
+        abort 1;
+        let S {} = _x;
+    }
+}
+
+//# run 0xCAFE::m::f