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

Issue:
[Bug][move-compiler-v2] Missing `BorrowVariantField/GetVariantField` handling in `Bytecode::instantiate()`
# 🐛 Bug

Around line 765 in `third_party/move/move-model/bytecode/src/stackless_bytecode.rs` is a match which does not handle `BorrowVariantField` and `GetVariantField`.




Discussion / hints:

Fix patch:
diff --git a/third_party/move/evm/move-to-yul/src/functions.rs b/third_party/move/evm/move-to-yul/src/functions.rs
index 7e24f6757b828..f2c6765691443 100644
--- a/third_party/move/evm/move-to-yul/src/functions.rs
+++ b/third_party/move/evm/move-to-yul/src/functions.rs
@@ -558,6 +558,7 @@ impl<'a> FunctionGenerator<'a> {
                     // Specification or other operations which can be ignored here
                     Release
                     | GetField(_, _, _, _)
+                    | GetVariantField(_, _, _, _, _)
                     | GetGlobal(_, _, _)
                     | IsParent(_, _)
                     | WriteBack(_, _)
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 bc221ee9b1a51..6535bd242728b 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
@@ -609,6 +609,7 @@ impl<'a> FunctionGenerator<'a> {
             | Operation::OpaqueCallBegin(_, _, _)
             | Operation::OpaqueCallEnd(_, _, _)
             | Operation::GetField(_, _, _, _)
+            | Operation::GetVariantField(_, _, _, _, _)
             | Operation::GetGlobal(_, _, _)
             | Operation::Uninit
             | Operation::Havoc(_)
diff --git a/third_party/move/move-model/bytecode/src/borrow_analysis.rs b/third_party/move/move-model/bytecode/src/borrow_analysis.rs
index 2ab8c96f9843a..358f06c9a8f72 100644
--- a/third_party/move/move-model/bytecode/src/borrow_analysis.rs
+++ b/third_party/move/move-model/bytecode/src/borrow_analysis.rs
@@ -683,6 +683,22 @@ impl<'a> TransferFunctions for BorrowAnalysis<'a> {
                             ),
                         );
                     },
+                    BorrowVariantField(mid, sid, variants, inst, field)
+                        if livevar_annotation_at.after.contains(&dests[0]) =>
+                    {
+                        let dest_node = self.borrow_node(dests[0]);
+                        let src_node = self.borrow_node(srcs[0]);
+                        state.add_node(dest_node.clone());
+                        state.add_edge(
+                            src_node,
+                            dest_node,
+                            BorrowEdge::Field(
+                                mid.qualified_inst(*sid, inst.to_owned()),
+                                Some(variants.clone()),
+                                *field,
+                            ),
+                        );
+                    },
                     Function(mid, fid, targs) => {
                         let callee_env = &self
                             .func_target
diff --git a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
index 0b9f56e82fd64..fbac30950c984 100644
--- a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
+++ b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
@@ -233,6 +233,7 @@ pub enum Operation {
 
     // Get shortcut
     GetField(ModuleId, StructId, Vec<Type>, usize),
+    GetVariantField(ModuleId, StructId, Vec<Symbol>, Vec<Type>, usize),
     GetGlobal(ModuleId, StructId, Vec<Type>),
 
     // Special ops
@@ -272,6 +273,7 @@ impl Operation {
             Operation::BorrowField(_, _, _, _) => false,
             Operation::BorrowGlobal(_, _, _) => true,
             Operation::GetField(_, _, _, _) => false,
+            Operation::GetVariantField(_, _, _, _, _) => true, // aborts if not given variant
             Operation::GetGlobal(_, _, _) => true,
             Operation::Uninit => false,
             Operation::Drop => false,
@@ -369,7 +371,7 @@ pub enum BorrowEdge {
     /// Direct borrow.
     Direct,
     /// Field borrow with static offset.
-    Field(QualifiedInstId<StructId>, Option<Symbol>, usize),
+    Field(QualifiedInstId<StructId>, Option<Vec<Symbol>>, usize),
     /// Vector borrow with dynamic index.
     Index(IndexEdgeKind),
     /// Composed sequence of edges.
@@ -388,7 +390,7 @@ impl BorrowEdge {
     pub fn instantiate(&self, params: &[Type]) -> Self {
         match self {
             Self::Field(qid, variant, offset) => {
-                Self::Field(qid.instantiate_ref(params), *variant, *offset)
+                Self::Field(qid.instantiate_ref(params), variant.clone(), *offset)
             },
             Self::Hyper(edges) => {
                 let new_edges = edges.iter().map(|e| e.instantiate(params)).collect();
@@ -768,6 +770,20 @@ impl Bytecode {
                     GetField(mid, sid, tys, field_num) => {
                         GetField(*mid, *sid, Type::instantiate_slice(tys, params), *field_num)
                     },
+                    BorrowVariantField(mid, sid, variants, tys, field_num) => BorrowVariantField(
+                        *mid,
+                        *sid,
+                        variants.clone(),
+                        Type::instantiate_slice(tys, params),
+                        *field_num,
+                    ),
+                    GetVariantField(mid, sid, variants, tys, field_num) => GetVariantField(
+                        *mid,
+                        *sid,
+                        variants.clone(),
+                        Type::instantiate_slice(tys, params),
+                        *field_num,
+                    ),
                     // storage
                     MoveTo(mid, sid, tys) => {
                         MoveTo(*mid, *sid, Type::instantiate_slice(tys, params))
@@ -1160,7 +1176,6 @@ impl<'env> fmt::Display for OperationDisplay<'env> {
                 )?;
             },
             BorrowVariantField(mid, sid, variants, targs, offset) => {
-                assert!(!variants.is_empty());
                 let variants_str = variants
                     .iter()
                     .map(|v| v.display(self.func_target.symbol_pool()))
@@ -1201,6 +1216,30 @@ impl<'env> fmt::Display for OperationDisplay<'env> {
                     field_env.get_name().display(struct_env.symbol_pool())
                 )?;
             },
+            GetVariantField(mid, sid, variants, targs, offset) => {
+                let variants_str = variants
+                    .iter()
+                    .map(|v| v.display(self.func_target.symbol_pool()))
+                    .join("|");
+                write!(
+                    f,
+                    "get_variant_field<{}::{}>",
+                    self.struct_str(*mid, *sid, targs),
+                    variants_str,
+                )?;
+                let struct_env = self
+                    .func_target
+                    .global_env()
+                    .get_module(*mid)
+                    .into_struct(*sid);
+                let field_env =
+                    struct_env.get_field_by_offset_optional_variant(Some(variants[0]), *offset);
+                write!(
+                    f,
+                    ".{}",
+                    field_env.get_name().display(struct_env.symbol_pool())
+                )?;
+            },
             GetGlobal(mid, sid, targs) => {
                 write!(f, "get_global<{}>", self.struct_str(*mid, *sid, targs))?;
             },
@@ -1447,7 +1486,12 @@ impl<'a> std::fmt::Display for BorrowEdgeDisplay<'a> {
         match self.edge {
             Field(qid, variant, field) => {
                 let struct_env = self.env.get_struct(qid.to_qualified_id());
-                let field_env = struct_env.get_field_by_offset_optional_variant(*variant, *field);
+                let field_env = if variant.is_none() {
+                    struct_env.get_field_by_offset_optional_variant(None, *field)
+                } else {
+                    let v = variant.clone().unwrap()[0];
+                    struct_env.get_field_by_offset_optional_variant(Some(v), *field)
+                };
                 let field_type = field_env.get_type().instantiate(&qid.inst);
                 write!(
                     f,
diff --git a/third_party/move/move-model/bytecode/src/stackless_bytecode_generator.rs b/third_party/move/move-model/bytecode/src/stackless_bytecode_generator.rs
index a1db2225c0956..d0b4e19044fcf 100644
--- a/third_party/move/move-model/bytecode/src/stackless_bytecode_generator.rs
+++ b/third_party/move/move-model/bytecode/src/stackless_bytecode_generator.rs
@@ -464,7 +464,7 @@ impl<'a> StacklessBytecodeGenerator<'a> {
                     vec![struct_ref_index],
                 ));
                 self.temp_count += 1;
-                let is_mut = matches!(bytecode, MoveBytecode::MutBorrowField(..));
+                let is_mut = matches!(bytecode, MoveBytecode::MutBorrowVariantField(..));
                 self.local_types.push(Type::Reference(
                     ReferenceKind::from_is_mut(is_mut),
                     Box::new(field_type),
@@ -495,7 +495,7 @@ impl<'a> StacklessBytecodeGenerator<'a> {
                     vec![struct_ref_index],
                 ));
                 self.temp_count += 1;
-                let is_mut = matches!(bytecode, MoveBytecode::MutBorrowField(..));
+                let is_mut = matches!(bytecode, MoveBytecode::MutBorrowVariantFieldGeneric(..));
                 self.local_types.push(Type::Reference(
                     ReferenceKind::from_is_mut(is_mut),
                     Box::new(field_type),
diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index 7c1ba18e37f6c..aea5722fd631b 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -1805,6 +1805,14 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
                         let struct_type = Type::Struct(entry.module_id, entry.struct_id, vec![]);
                         et.define_local(loc, receiver_param_name, struct_type, None, None);
                     }
+                } else if let StructLayout::Variants(_) = &entry.layout {
+                    et.enter_scope();
+                    if et.env().language_version.is_at_least(LanguageVersion::V2_0) {
+                        let receiver_param_name =
+                            et.symbol_pool().make(well_known::RECEIVER_PARAM_NAME);
+                        let struct_type = Type::Struct(entry.module_id, entry.struct_id, vec![]);
+                        et.define_local(loc, receiver_param_name, struct_type, None, None);
+                    }
                 }
 
                 et
diff --git a/third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs b/third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs
index dab2d556da1bd..0062a401306a7 100644
--- a/third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs
+++ b/third_party/move/move-prover/boogie-backend/src/boogie_helpers.rs
@@ -49,6 +49,16 @@ pub fn boogie_struct_name(struct_env: &StructEnv<'_>, inst: &[Type]) -> String {
     boogie_struct_name_bv(struct_env, inst, false)
 }
 
+pub fn boogie_struct_variant_name(
+    struct_env: &StructEnv<'_>,
+    inst: &[Type],
+    variant: Symbol,
+) -> String {
+    let struct_name = boogie_struct_name(struct_env, inst);
+    let variant_name = variant.display(struct_env.symbol_pool());
+    format!("{}_{}", struct_name, variant_name)
+}
+
 pub fn boogie_struct_name_bv(struct_env: &StructEnv<'_>, inst: &[Type], bv_flag: bool) -> String {
     if struct_env.is_intrinsic_of(INTRINSIC_TYPE_MAP) {
         // Map to the theory type representation, which is `Table int V`. The key
@@ -385,6 +395,14 @@ pub fn boogie_type_suffix_for_struct(
     }
 }
 
+pub fn boogie_type_suffix_for_struct_variant(
+    struct_env: &StructEnv<'_>,
+    inst: &[Type],
+    variant: &Symbol,
+) -> String {
+    boogie_struct_variant_name(struct_env, inst, *variant)
+}
+
 /// Generate suffix after instantiation of type parameters
 pub fn boogie_inst_suffix_bv(env: &GlobalEnv, inst: &[Type], bv_flag: &[bool]) -> String {
     if inst.is_empty() {
diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
index 87d6f02af9b69..3917c7de48fa1 100644
--- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
@@ -12,10 +12,11 @@ use crate::{
         boogie_function_bv_name, boogie_function_name, boogie_make_vec_from_strings,
         boogie_modifies_memory_name, boogie_num_literal, boogie_num_type_base,
         boogie_num_type_string_capital, boogie_reflection_type_info, boogie_reflection_type_name,
-        boogie_resource_memory_name, boogie_struct_name, boogie_temp, boogie_temp_from_suffix,
-        boogie_type, boogie_type_param, boogie_type_suffix, boogie_type_suffix_bv,
-        boogie_type_suffix_for_struct, boogie_well_formed_check, boogie_well_formed_expr_bv,
-        TypeIdentToken,
+        boogie_resource_memory_name, boogie_struct_name, boogie_struct_variant_name, boogie_temp,
+        boogie_temp_from_suffix, boogie_type, boogie_type_param, boogie_type_suffix,
+        boogie_type_suffix_bv, boogie_type_suffix_for_struct,
+        boogie_type_suffix_for_struct_variant, boogie_well_formed_check,
+        boogie_well_formed_expr_bv, TypeIdentToken,
     },
     options::BoogieOptions,
     spec_translator::SpecTranslator,
@@ -30,11 +31,12 @@ use move_model::{
     ast::{Attribute, TempIndex, TraceKind},
     code_writer::CodeWriter,
     emit, emitln,
-    model::{FieldId, GlobalEnv, Loc, NodeId, QualifiedInstId, StructEnv, StructId},
+    model::{FieldEnv, FieldId, GlobalEnv, Loc, NodeId, QualifiedInstId, StructEnv, StructId},
     pragmas::{
         ADDITION_OVERFLOW_UNCHECKED_PRAGMA, SEED_PRAGMA, TIMEOUT_PRAGMA,
         VERIFY_DURATION_ESTIMATE_PRAGMA,
     },
+    symbol::Symbol,
     ty::{PrimitiveType, Type, TypeDisplayContext, BOOL_TYPE},
     well_known::{TYPE_INFO_MOVE, TYPE_NAME_GET_MOVE, TYPE_NAME_MOVE},
 };
@@ -349,6 +351,212 @@ impl<'env> StructTranslator<'env> {
         ty.instantiate(self.type_inst)
     }
 
+    /// Return equality check for the field `f`
+    pub fn boogie_field_is_equal(&self, f: &FieldEnv<'_>, sep: &str) -> String {
+        let field_sel = boogie_field_sel(f);
+        let bv_flag = self.field_bv_flag(&f.get_id());
+        let field_suffix =
+            boogie_type_suffix_bv(self.parent.env, &self.inst(&f.get_type()), bv_flag);
+        format!(
+            "{}$IsEqual'{}'(s1->{}, s2->{})",
+            sep, field_suffix, field_sel, field_sel,
+        )
+    }
+
+    /// Return validity check of the field `f`
+    pub fn boogie_field_is_valid(&self, field: &FieldEnv<'_>, sep: &str) -> String {
+        let sel = format!("s->{}", boogie_field_sel(field));
+        let ty = &field.get_type().instantiate(self.type_inst);
+        let bv_flag = self.field_bv_flag(&field.get_id());
+        format!(
+            "{}{}",
+            sep,
+            boogie_well_formed_expr_bv(self.parent.env, &sel, ty, bv_flag)
+        )
+    }
+
+    /// Return argument of constructor for the field `f`
+    pub fn boogie_field_arg_for_fun_sig(&self, f: &FieldEnv<'_>) -> String {
+        format!(
+            "{}: {}",
+            boogie_field_sel(f),
+            self.boogie_type_for_struct_field(
+                &f.get_id(),
+                self.parent.env,
+                &self.inst(&f.get_type())
+            )
+        )
+    }
+
+    /// Emit is_valid and update for fields of `variant`
+    pub fn emit_struct_variant_is_valid_and_update(
+        &self,
+        struct_env: &StructEnv,
+        variant: Symbol,
+        field_variant_map: &mut BTreeMap<(String, String), Vec<String>>,
+    ) {
+        let writer = self.parent.writer;
+        let env = self.parent.env;
+        let suffix_variant =
+            boogie_type_suffix_for_struct_variant(struct_env, self.type_inst, &variant);
+        let struct_variant_name = boogie_struct_variant_name(struct_env, self.type_inst, variant);
+        let struct_name = boogie_struct_name(struct_env, self.type_inst);
+        let fields = struct_env.get_fields_of_variant(variant).collect_vec();
+        // Emit $Update function for each field in `variant`.
+        for (pos, field_env) in struct_env.get_fields_of_variant(variant).enumerate() {
+            let field_name = field_env.get_name().display(env.symbol_pool()).to_string();
+            let field_type_name = self.boogie_type_for_struct_field(
+                &field_env.get_id(),
+                env,
+                &self.inst(&field_env.get_type()),
+            );
+            if field_variant_map.contains_key(&(field_name.clone(), field_type_name.clone())) {
+                let variants_vec = field_variant_map
+                    .get_mut(&(field_name.clone(), field_type_name.clone()))
+                    .unwrap();
+                variants_vec.push(struct_variant_name.clone());
+            } else {
+                let variants_vec = vec![struct_variant_name.clone()];
+                field_variant_map.insert(
+                    (field_name.to_string(), field_type_name.to_string()),
+                    variants_vec,
+                );
+            }
+            self.emit_function(
+                &format!(
+                    "$Update'{}'_{}(s: {}, x: {}): {}",
+                    suffix_variant, field_name, struct_name, field_type_name, struct_name
+                ),
+                || {
+                    let args = fields
+                        .iter()
+                        .enumerate()
+                        .map(|(p, f)| {
+                            if p == pos {
+                                "x".to_string()
+                            } else {
+                                format!("s->{}", boogie_field_sel(f))
+                            }
+                        })
+                        .join(", ");
+                    emitln!(writer, "{}({})", struct_variant_name, args);
+                },
+            );
+        }
+
+        // Emit $IsValid function for `variant`.
+        self.emit_function_with_attr(
+            "", // not inlined!
+            &format!("$IsValid'{}'(s: {}): bool", suffix_variant, struct_name),
+            || {
+                if struct_env.is_intrinsic() || struct_env.get_field_count() == 0 {
+                    emitln!(writer, "true")
+                } else {
+                    let mut sep = "";
+                    for field in &fields {
+                        emitln!(writer, "{}", self.boogie_field_is_valid(field, sep));
+                        sep = "  && ";
+                    }
+                }
+            },
+        );
+    }
+
+    // Emit $IsValid function for struct.
+    fn emit_is_valid_struct(&self, struct_env: &StructEnv, struct_name: &str, emit_fn: impl Fn()) {
+        let writer = self.parent.writer;
+        self.emit_function_with_attr(
+            "", // not inlined!
+            &format!("$IsValid'{}'(s: {}): bool", struct_name, struct_name),
+            || {
+                if struct_env.is_intrinsic() || struct_env.get_field_count() == 0 {
+                    emitln!(writer, "true")
+                } else {
+                    emit_fn()
+                }
+            },
+        );
+    }
+
+    /// Emit $Update and $IsValid for enum
+    fn emit_update_is_valid_for_enum(&self, struct_env: &StructEnv, struct_name: &str) {
+        let writer = self.parent.writer;
+        let mut field_variant_map: BTreeMap<(String, String), Vec<String>> = BTreeMap::new();
+        for variant in struct_env.get_variants() {
+            self.emit_struct_variant_is_valid_and_update(
+                struct_env,
+                variant,
+                &mut field_variant_map,
+            );
+        }
+        for ((field, field_type), variant_name) in field_variant_map {
+            self.emit_function(
+                &format!(
+                    "$Update'{}'_{}(s: {}, x: {}): {}",
+                    struct_name, field, struct_name, field_type, struct_name
+                ),
+                || {
+                    let mut else_symbol = "";
+                    for struct_variant_name in &variant_name {
+                        let match_condition = format!("s is {}", struct_variant_name);
+                        let update_str =
+                            format!("$Update'{}'_{}(s, x)", struct_variant_name, field);
+                        emitln!(writer, "{} if {} then", else_symbol, match_condition);
+                        emitln!(writer, "{}", update_str);
+                        if else_symbol.is_empty() {
+                            else_symbol = "else";
+                        }
+                    }
+                    emitln!(writer, "else s");
+                },
+            );
+        }
+
+        self.emit_is_valid_struct(struct_env, struct_name, || {
+            let mut else_symbol = "";
+            for variant in struct_env.get_variants() {
+                let struct_variant_name =
+                    boogie_struct_variant_name(struct_env, self.type_inst, variant);
+                let match_condition = format!("s is {}", struct_variant_name);
+                let str = format!("$IsValid'{}'(s)", struct_variant_name,);
+                emitln!(writer, "{} if {} then", else_symbol, match_condition);
+                emitln!(writer, "{}", str);
+                if else_symbol.is_empty() {
+                    else_symbol = "else";
+                }
+            }
+            emitln!(writer, "else false");
+        });
+    }
+
+    /// Emit the function body of $IsEqual for enum
+    fn emit_is_equal_fn_body_for_enum(&self, struct_env: &StructEnv) {
+        let writer = self.parent.writer;
+        let mut sep = "";
+        let mut else_symbol = "";
+        for variant in struct_env.get_variants() {
+            let mut equal_statement = "".to_string();
+            for f in struct_env.get_fields_of_variant(variant) {
+                let field_equal_str = self.boogie_field_is_equal(&f, sep);
+                equal_statement = format!("{}{}", equal_statement, field_equal_str);
+                sep = "&& ";
+            }
+            let struct_variant_name =
+                boogie_struct_variant_name(struct_env, self.type_inst, variant);
+            let match_condition = format!(
+                "s1 is {} && s2 is {}",
+                struct_variant_name, struct_variant_name
+            );
+            emitln!(writer, "{} if {} then", else_symbol, match_condition);
+            emitln!(writer, "{}", equal_statement);
+            if else_symbol.is_empty() {
+                else_symbol = "else";
+            }
+            sep = "";
+        }
+        emitln!(writer, "else false");
+    }
+
     /// Return whether a field involves bitwise operations
     pub fn field_bv_flag(&self, field_id: &FieldId) -> bool {
         let global_state = &self
@@ -359,8 +567,11 @@ impl<'env> StructTranslator<'env> {
         let operation_map = &global_state.struct_operation_map;
         let mid = self.struct_env.module_env.get_id();
         let sid = self.struct_env.get_id();
-        let field_oper = operation_map.get(&(mid, sid)).unwrap().get(field_id);
-        matches!(field_oper, Some(&Bitwise))
+        if let Some(struct_info) = operation_map.get(&(mid, sid)) {
+            matches!(struct_info.get(field_id), Some(&Bitwise))
+        } else {
+            false
+        }
     }
 
     /// Return boogie type for a struct
@@ -387,9 +598,15 @@ impl<'env> StructTranslator<'env> {
         let qid = struct_env
             .get_qualified_id()
             .instantiate(self.type_inst.to_owned());
+        let struct_or_enum = if struct_env.has_variants() {
+            "enum"
+        } else {
+            "struct"
+        };
         emitln!(
             writer,
-            "// struct {} {}",
+            "// {} {} {}",
+            struct_or_enum,
             env.display(&qid),
             struct_env.get_loc().display(env)
         );
@@ -402,108 +619,96 @@ impl<'env> StructTranslator<'env> {
         emitln!(writer, "datatype {} {{", struct_name);
 
         // Emit constructor
-        let fields = struct_env
-            .get_fields()
-            .map(|field| {
-                format!(
-                    "${}: {}",
-                    field.get_name().display(env.symbol_pool()),
-                    self.boogie_type_for_struct_field(
-                        &field.get_id(),
-                        env,
-                        &self.inst(&field.get_type())
-                    )
-                )
-            })
-            .join(", ");
-        emitln!(writer, "    {}({})", struct_name, fields,);
-        emitln!(writer, "}");
-
-        let suffix = boogie_type_suffix_for_struct(struct_env, self.type_inst, false);
+        if struct_env.has_variants() {
+            let constructor = struct_env
+                .get_variants()
+                .map(|variant| {
+                    let struct_variant_name =
+                        boogie_struct_variant_name(struct_env, self.type_inst, variant);
+                    let variant_fields = struct_env
+                        .get_fields_of_variant(variant)
+                        .map(|f| self.boogie_field_arg_for_fun_sig(&f))
+                        .join(", ");
+                    format!("    {}({})", struct_variant_name, variant_fields,)
+                })
+                .join(", \n");
+            emitln!(writer, "{}", constructor);
+            emitln!(writer, "}");
+        } else {
+            let fields = struct_env
+                .get_fields()
+                .map(|f| self.boogie_field_arg_for_fun_sig(&f))
+                .join(", ");
+            emitln!(writer, "    {}({})", struct_name, fields,);
+            emitln!(writer, "}");
+        }
 
         // Emit $UpdateField functions.
-        let fields = struct_env.get_fields().collect_vec();
-        for (pos, field_env) in fields.iter().enumerate() {
-            let field_name = field_env.get_name().display(env.symbol_pool()).to_string();
-            self.emit_function(
-                &format!(
-                    "$Update'{}'_{}(s: {}, x: {}): {}",
-                    suffix,
-                    field_name,
-                    struct_name,
-                    self.boogie_type_for_struct_field(
-                        &field_env.get_id(),
-                        env,
-                        &self.inst(&field_env.get_type())
+        if struct_env.has_variants() {
+            self.emit_update_is_valid_for_enum(struct_env, &struct_name);
+        } else {
+            let suffix = boogie_type_suffix_for_struct(struct_env, self.type_inst, false);
+            let fields = struct_env.get_fields().collect_vec();
+            for (pos, field_env) in fields.iter().enumerate() {
+                let field_name = field_env.get_name().display(env.symbol_pool()).to_string();
+                self.emit_function(
+                    &format!(
+                        "$Update'{}'_{}(s: {}, x: {}): {}",
+                        suffix,
+                        field_name,
+                        struct_name,
+                        self.boogie_type_for_struct_field(
+                            &field_env.get_id(),
+                            env,
+                            &self.inst(&field_env.get_type())
+                        ),
+                        struct_name
                     ),
-                    struct_name
-                ),
-                || {
-                    let args = fields
-                        .iter()
-                        .enumerate()
-                        .map(|(p, f)| {
-                            if p == pos {
-                                "x".to_string()
-                            } else {
-                                format!("s->{}", boogie_field_sel(f))
-                            }
-                        })
-                        .join(", ");
-                    emitln!(writer, "{}({})", struct_name, args);
-                },
-            );
-        }
+                    || {
+                        let args = fields
+                            .iter()
+                            .enumerate()
+                            .map(|(p, f)| {
+                                if p == pos {
+                                    "x".to_string()
+                                } else {
+                                    format!("s->{}", boogie_field_sel(f))
+                                }
+                            })
+                            .join(", ");
+                        emitln!(writer, "{}({})", struct_name, args);
+                    },
+                );
+            }
 
-        // Emit $IsValid function.
-        self.emit_function_with_attr(
-            "", // not inlined!
-            &format!("$IsValid'{}'(s: {}): bool", suffix, struct_name),
-            || {
-                if struct_env.is_intrinsic() || struct_env.get_field_count() == 0 {
-                    emitln!(writer, "true")
-                } else {
-                    let mut sep = "";
-                    for field in struct_env.get_fields() {
-                        let sel = format!("s->{}", boogie_field_sel(&field));
-                        let ty = &field.get_type().instantiate(self.type_inst);
-                        let bv_flag = self.field_bv_flag(&field.get_id());
-                        emitln!(
-                            writer,
-                            "{}{}",
-                            sep,
-                            boogie_well_formed_expr_bv(env, &sel, ty, bv_flag)
-                        );
-                        sep = "  && ";
-                    }
+            // Emit $IsValid function.
+            self.emit_is_valid_struct(struct_env, &struct_name, || {
+                let mut sep = "";
+                for field in struct_env.get_fields() {
+                    emitln!(writer, "{}", self.boogie_field_is_valid(&field, sep));
+                    sep = "  && ";
                 }
-            },
-        );
+            });
+        }
 
         // Emit equality
         self.emit_function(
             &format!(
                 "$IsEqual'{}'(s1: {}, s2: {}): bool",
-                suffix, struct_name, struct_name
+                boogie_type_suffix_for_struct(struct_env, self.type_inst, false),
+                struct_name,
+                struct_name
             ),
             || {
                 if struct_has_native_equality(struct_env, self.type_inst, self.parent.options) {
                     emitln!(writer, "s1 == s2")
+                } else if struct_env.has_variants() {
+                    self.emit_is_equal_fn_body_for_enum(struct_env);
                 } else {
                     let mut sep = "";
-                    for field in &fields {
-                        let field_sel = boogie_field_sel(field);
-                        let bv_flag = self.field_bv_flag(&field.get_id());
-                        let field_suffix =
-                            boogie_type_suffix_bv(env, &self.inst(&field.get_type()), bv_flag);
-                        emit!(
-                            writer,
-                            "{}$IsEqual'{}'(s1->{}, s2->{})",
-                            sep,
-                            field_suffix,
-                            field_sel,
-                            field_sel,
-                        );
+                    for field in &struct_env.get_fields().collect_vec() {
+                        let field_equal_str = self.boogie_field_is_equal(field, sep);
+                        emit!(writer, "{}", field_equal_str,);
                         sep = "\n&& ";
                     }
                 }
@@ -1119,12 +1324,26 @@ impl<'env> FunctionTranslator<'env> {
             Call(_, dests, oper, srcs, aa) => {
                 use Operation::*;
                 match oper {
-                    TestVariant(..)
-                    | PackVariant(..)
-                    | UnpackVariant(..)
-                    | BorrowVariantField(..) => {
-                        let loc = self.fun_target.get_bytecode_loc(attr_id);
-                        self.parent.env.error(&loc, "variants not yet implemented")
+                    TestVariant(mid, sid, variant, inst) => {
+                        let inst = &self.inst_slice(inst);
+                        let src_type = self.get_local_type(srcs[0]);
+                        let src_str = if src_type.is_reference() {
+                            format!("$Dereference({})", str_local(srcs[0]))
+                        } else {
+                            str_local(srcs[0])
+                        };
+                        let dst_str = str_local(dests[0]);
+                        let struct_env = env.get_module(*mid).into_struct(*sid);
+                        let struct_variant_name =
+                            boogie_struct_variant_name(&struct_env, inst, *variant);
+                        emitln!(
+                            writer,
+                            "if ({} is {}) {{ {} := true; }}",
+                            src_str,
+                            struct_variant_name,
+                            dst_str
+                        );
+                        emitln!(writer, "else {{ {} := false; }}", dst_str);
                     },
                     FreezeRef(_) => unreachable!(),
                     UnpackRef | UnpackRefDeep | PackRef | PackRefDeep => {
@@ -1467,6 +1686,19 @@ impl<'env> FunctionTranslator<'env> {
                             args
                         );
                     },
+                    PackVariant(mid, sid, variant, inst) => {
+                        let inst = &self.inst_slice(inst);
+                        let struct_env = env.get_module(*mid).into_struct(*sid);
+                        let args = srcs.iter().cloned().map(str_local).join(", ");
+                        let dest_str = str_local(dests[0]);
+                        emitln!(
+                            writer,
+                            "{} := {}({});",
+                            dest_str,
+                            boogie_struct_variant_name(&struct_env, inst, *variant),
+                            args
+                        );
+                    },
                     Unpack(mid, sid, _) => {
                         let struct_env = env.get_module(*mid).into_struct(*sid);
                         for (i, ref field_env) in struct_env.get_fields().enumerate() {
@@ -1475,6 +1707,22 @@ impl<'env> FunctionTranslator<'env> {
                             emitln!(writer, "{} := {};", str_local(dests[i]), field_sel);
                         }
                     },
+                    UnpackVariant(mid, sid, variant, inst) => {
+                        let inst = &self.inst_slice(inst);
+                        let src_str = str_local(srcs[0]);
+                        let struct_env = env.get_module(*mid).into_struct(*sid);
+                        let struct_variant_name =
+                            boogie_struct_variant_name(&struct_env, inst, *variant);
+                        emitln!(writer, "if ({} is {}) {{", src_str, struct_variant_name);
+                        for (i, ref field_env) in
+                            struct_env.get_fields_of_variant(*variant).enumerate()
+                        {
+                            let field_sel =
+                                format!("{}->{}", str_local(srcs[0]), boogie_field_sel(field_env),);
+                            emitln!(writer, "{} := {};", str_local(dests[i]), field_sel);
+                        }
+                        emitln!(writer, "} else { call $ExecFailureAbort(); }");
+                    },
                     BorrowField(mid, sid, _, field_offset) => {
                         let src_str = str_local(srcs[0]);
                         let dest_str = str_local(dests[0]);
@@ -1492,6 +1740,36 @@ impl<'env> FunctionTranslator<'env> {
                             field_sel,
                         );
                     },
+                    BorrowVariantField(mid, sid, variants, inst, field_offset) => {
+                        let inst = &self.inst_slice(inst);
+                        let src_str = str_local(srcs[0]);
+                        let deref_src_str = format!("$Dereference({})", src_str);
+                        let dest_str = str_local(dests[0]);
+                        let struct_env = env.get_module(*mid).into_struct(*sid);
+                        self.check_intrinsic_select(attr_id, &struct_env);
+                        emit!(writer, "if (");
+                        let mut select_condition = vec![];
+                        for variant in variants {
+                            let struct_variant_name =
+                                boogie_struct_variant_name(&struct_env, inst, *variant);
+                            let call = format!("{} is {}", deref_src_str, struct_variant_name);
+                            select_condition.push(call.clone());
+                        }
+                        let field_env = struct_env
+                            .get_field_by_offset_optional_variant(Some(variants[0]), *field_offset);
+                        let field_sel = boogie_field_sel(&field_env);
+                        emitln!(writer, "{}) {{", select_condition.join(" || "));
+                        emitln!(
+                            writer,
+                            "{} := $ChildMutation({}, {}, {}->{});",
+                            dest_str,
+                            src_str,
+                            field_offset,
+                            deref_src_str,
+                            field_sel,
+                        );
+                        emitln!(writer, "} else { call $ExecFailureAbort(); }");
+                    },
                     GetField(mid, sid, _, field_offset) => {
                         let src = srcs[0];
                         let mut src_str = str_local(src);
@@ -1505,6 +1783,31 @@ impl<'env> FunctionTranslator<'env> {
                         };
                         emitln!(writer, "{} := {}->{};", dest_str, src_str, field_sel);
                     },
+                    GetVariantField(mid, sid, variants, inst, field_offset) => {
+                        let inst = &self.inst_slice(inst);
+                        let src = srcs[0];
+                        let mut src_str = str_local(src);
+                        let dest_str = str_local(dests[0]);
+                        let struct_env = env.get_module(*mid).into_struct(*sid);
+                        self.check_intrinsic_select(attr_id, &struct_env);
+                        emit!(writer, "if (");
+                        let mut select_condition = vec![];
+                        for variant in variants {
+                            let struct_variant_name =
+                                boogie_struct_variant_name(&struct_env, inst, *variant);
+                            if self.get_local_type(src).is_reference() {
+                                src_str = format!("$Dereference({})", src_str);
+                            };
+                            let call = format!("{} is {}", src_str, struct_variant_name);
+                            select_condition.push(call.clone());
+                        }
+                        let field_env = struct_env
+                            .get_field_by_offset_optional_variant(Some(variants[0]), *field_offset);
+                        let field_sel = boogie_field_sel(&field_env);
+                        emitln!(writer, "{}) {{", select_condition.join(" || "));
+                        emitln!(writer, "{} := {}->{};", dest_str, src_str, field_sel);
+                        emitln!(writer, "} else { call $ExecFailureAbort(); }");
+                    },
                     Exists(mid, sid, inst) => {
                         let inst = self.inst_slice(inst);
                         let addr_str = str_local(srcs[0]);
@@ -2368,9 +2671,15 @@ impl<'env> FunctionTranslator<'env> {
                 BorrowEdge::Field(memory, variant, offset) => {
                     let memory = memory.to_owned().instantiate(self.type_inst);
                     let struct_env = &self.parent.env.get_struct_qid(memory.to_qualified_id());
-                    let field_env =
-                        &struct_env.get_field_by_offset_optional_variant(*variant, *offset);
-                    let field_sel = boogie_field_sel(field_env);
+                    let field_env = if variant.is_none() {
+                        struct_env.get_field_by_offset_optional_variant(None, *offset)
+                    } else {
+                        struct_env.get_field_by_offset_optional_variant(
+                            Some(variant.clone().unwrap()[0]),
+                            *offset,
+                        )
+                    };
+                    let field_sel = boogie_field_sel(&field_env);
                     let new_dest = format!("{}->{}", (*mk_dest)(), field_sel);
                     let mut new_dest_needed = false;
                     let new_src = self.translate_write_back_update(
@@ -2383,7 +2692,7 @@ impl<'env> FunctionTranslator<'env> {
                         edges,
                         at + 1,
                     );
-                    let update_fun = boogie_field_update(field_env, &memory.inst);
+                    let update_fun = boogie_field_update(&field_env, &memory.inst);
                     if new_dest_needed {
                         format!(
                             "(var $$sel{} := {}; {}({}, {}))",
@@ -2634,13 +2943,27 @@ fn struct_has_native_equality(
         // Everything has native equality
         return true;
     }
-    for field in struct_env.get_fields() {
-        if !has_native_equality(
-            struct_env.module_env.env,
-            options,
-            &field.get_type().instantiate(inst),
-        ) {
-            return false;
+    if struct_env.has_variants() {
+        for variant in struct_env.get_variants() {
+            for field in struct_env.get_fields_of_variant(variant) {
+                if !has_native_equality(
+                    struct_env.module_env.env,
+                    options,
+                    &field.get_type().instantiate(inst),
+                ) {
+                    return false;
+                }
+            }
+        }
+    } else {
+        for field in struct_env.get_fields() {
+            if !has_native_equality(
+                struct_env.module_env.env,
+                options,
+                &field.get_type().instantiate(inst),
+            ) {
+                return false;
+            }
         }
     }
     true
diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
index c7768b6d43278..7541577b532da 100644
--- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
@@ -10,9 +10,9 @@ use crate::{
         boogie_choice_fun_name, boogie_declare_global, boogie_field_sel, boogie_inst_suffix,
         boogie_modifies_memory_name, boogie_num_type_base, boogie_reflection_type_info,
         boogie_reflection_type_is_struct, boogie_reflection_type_name, boogie_resource_memory_name,
-        boogie_spec_fun_name, boogie_spec_var_name, boogie_struct_name, boogie_type,
-        boogie_type_suffix, boogie_type_suffix_bv, boogie_value_blob, boogie_well_formed_expr,
-        boogie_well_formed_expr_bv,
+        boogie_spec_fun_name, boogie_spec_var_name, boogie_struct_name, boogie_struct_variant_name,
+        boogie_type, boogie_type_suffix, boogie_type_suffix_bv, boogie_value_blob,
+        boogie_well_formed_expr, boogie_well_formed_expr_bv,
     },
     options::BoogieOptions,
 };
@@ -846,8 +846,8 @@ impl<'env> SpecTranslator<'env> {
             Operation::SpecFunction(module_id, fun_id, memory_labels) => {
                 self.translate_spec_fun_call(node_id, *module_id, *fun_id, args, memory_labels)
             },
-            Operation::Pack(_, _, Some(_)) => {
-                self.error(&loc, "variants not yet supported");
+            Operation::Pack(mid, sid, Some(variant)) => {
+                self.translate_pack_variant(node_id, *mid, *sid, variant, args)
             },
             Operation::Pack(mid, sid, None) => self.translate_pack(node_id, *mid, *sid, args),
             Operation::Tuple if args.len() == 1 => self.translate_exp(&args[0]),
@@ -855,13 +855,11 @@ impl<'env> SpecTranslator<'env> {
             Operation::Select(module_id, struct_id, field_id) => {
                 self.translate_select(node_id, *module_id, *struct_id, *field_id, args)
             },
-            Operation::SelectVariants(_module_id, _struct_id, _field_ids) => {
-                // TODO(#13806): implement for variants
-                self.error(&loc, "selection from variants no yet supported");
+            Operation::SelectVariants(module_id, struct_id, field_ids) => {
+                self.translate_select(node_id, *module_id, *struct_id, field_ids[0], args);
             },
-            Operation::TestVariants(_module_id, _struct_id, _variants) => {
-                // TODO(#13806): implement for variants
-                self.error(&loc, "testing of variants no yet supported");
+            Operation::TestVariants(module_id, struct_id, variants) => {
+                self.translate_test_variants(node_id, *module_id, *struct_id, variants, args);
             },
             Operation::UpdateField(module_id, struct_id, field_id) => {
                 self.translate_update_field(node_id, *module_id, *struct_id, *field_id, args)
@@ -1045,6 +1043,30 @@ impl<'env> SpecTranslator<'env> {
         emit!(self.writer, ")");
     }
 
+    fn translate_pack_variant(
+        &self,
+        node_id: NodeId,
+        mid: ModuleId,
+        sid: StructId,
+        variant: &Symbol,
+        args: &[Exp],
+    ) {
+        let struct_env = &self.env.get_module(mid).into_struct(sid);
+        let inst = &self.get_node_instantiation(node_id);
+        emit!(
+            self.writer,
+            "{}(",
+            boogie_struct_variant_name(struct_env, inst, *variant)
+        );
+        let mut sep = "";
+        for arg in args {
+            emit!(self.writer, sep);
+            self.translate_exp(arg);
+            sep = ", ";
+        }
+        emit!(self.writer, ")");
+    }
+
     fn translate_spec_fun_call(
         &self,
         node_id: NodeId,
@@ -1197,6 +1219,38 @@ impl<'env> SpecTranslator<'env> {
         emit!(self.writer, "->{}", boogie_field_sel(&field_env));
     }
 
+    fn translate_test_variants(
+        &self,
+        node_id: NodeId,
+        module_id: ModuleId,
+        struct_id: StructId,
+        variants: &[Symbol],
+        args: &[Exp],
+    ) {
+        let struct_env = self.env.get_module(module_id).into_struct(struct_id);
+        if struct_env.is_intrinsic() {
+            self.env.error(
+                &self.env.get_node_loc(node_id),
+                "cannot test variants of intrinsic struct",
+            );
+        }
+        let struct_type = &self.get_node_type(args[0].node_id());
+        let (_, _, _) = struct_type.skip_reference().require_struct();
+        let inst = self.env.get_node_instantiation(node_id);
+        let inst = &self.inst_slice(&inst);
+        let test_var_result = self.fresh_var_name("test_variant_var");
+        emit!(self.writer, "(var {} := ", test_var_result);
+        self.translate_exp(&args[0]);
+        emit!(self.writer, ";");
+        let mut condition = vec![];
+        for variant in variants {
+            let struct_variant_name = boogie_struct_variant_name(&struct_env, inst, *variant);
+            let call = format!("{} is {}", test_var_result, struct_variant_name);
+            condition.push(call.clone());
+        }
+        emitln!(self.writer, "{})", condition.join(" || "),);
+    }
+
     fn translate_update_field(
         &self,
         node_id: NodeId,
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/data_invariant_instrumentation.rs b/third_party/move/move-prover/bytecode-pipeline/src/data_invariant_instrumentation.rs
index 3613255120a1f..061b703bce084 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/data_invariant_instrumentation.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/data_invariant_instrumentation.rs
@@ -16,6 +16,7 @@ use move_model::{
     ast,
     ast::{ConditionKind, Exp, ExpData, QuantKind, RewriteResult, TempIndex},
     exp_generator::ExpGenerator,
+    metadata::LanguageVersion,
     model::{FunctionEnv, Loc, NodeId, StructEnv},
     pragmas::{INTRINSIC_FUN_MAP_SPEC_GET, INTRINSIC_TYPE_MAP},
     ty::Type,
@@ -112,6 +113,20 @@ impl<'a> Instrumenter<'a> {
                 // Emit a shallow assert of the data invariant.
                 self.emit_data_invariant_for_temp(false, PropKind::Assert, struct_temp);
             },
+            Call(id, dests, PackVariant(mid, sid, variant, targs), srcs, aa)
+                if self.for_verification =>
+            {
+                let struct_temp = dests[0];
+                self.builder.emit(Call(
+                    id,
+                    dests,
+                    PackVariant(mid, sid, variant, targs),
+                    srcs,
+                    aa,
+                ));
+                // Emit a shallow assert of the data invariant.
+                self.emit_data_invariant_for_temp(false, PropKind::Assert, struct_temp);
+            },
             Call(_, _, PackRef, srcs, _) if self.for_verification => {
                 // Emit a shallow assert of the data invariant.
                 self.emit_data_invariant_for_temp(false, PropKind::Assert, srcs[0]);
@@ -243,6 +258,11 @@ impl<'a> Instrumenter<'a> {
         use ast::Operation::*;
         use ExpData::*;
 
+        let lang_ver_ge_2 = self
+            .builder
+            .global_env()
+            .language_version()
+            .is_at_least(LanguageVersion::V2_0);
         // First generate a conjunction for all invariants on this struct.
         let mut result = vec![];
         for cond in struct_env
@@ -254,21 +274,21 @@ impl<'a> Instrumenter<'a> {
             // an empty argument list. It is guaranteed that this uniquely identifies the
             // target, as any other `Select` will have exactly one argument.
             let exp_rewriter = &mut |e: Exp| match e.as_ref() {
-                Call(id, oper @ Select(..), args) if args.is_empty() => RewriteResult::Rewritten(
-                    Call(*id, oper.to_owned(), vec![value.clone()]).into_exp(),
-                ),
-                Call(id, oper @ Select(..), args) => {
-                    if args.len() == 1
-                        && args[0].display(self.builder.global_env()).to_string()
+                LocalVar(_, var) => {
+                    if lang_ver_ge_2
+                        && var
+                            .display(self.builder.global_env().symbol_pool())
+                            .to_string()
                             == well_known::RECEIVER_PARAM_NAME
                     {
-                        RewriteResult::Rewritten(
-                            Call(*id, oper.to_owned(), vec![value.clone()]).into_exp(),
-                        )
+                        RewriteResult::Rewritten(value.clone())
                     } else {
                         RewriteResult::Unchanged(e)
                     }
                 },
+                Call(id, oper @ Select(..), args) if args.is_empty() => RewriteResult::Rewritten(
+                    Call(*id, oper.to_owned(), vec![value.clone()]).into_exp(),
+                ),
                 _ => RewriteResult::Unchanged(e),
             };
             // Also instantiate types.
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/eliminate_imm_refs.rs b/third_party/move/move-prover/bytecode-pipeline/src/eliminate_imm_refs.rs
index d55a8ec63e909..d69a1862469ed 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/eliminate_imm_refs.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/eliminate_imm_refs.rs
@@ -107,6 +107,17 @@ impl<'a> EliminateImmRefs<'a> {
                         aa,
                     ));
                 },
+                BorrowVariantField(mid, sid, variants, type_actuals, offset)
+                    if self.is_imm_ref(dests[0]) =>
+                {
+                    self.builder.emit(Call(
+                        attr_id,
+                        dests,
+                        GetVariantField(mid, sid, variants, type_actuals, offset),
+                        srcs,
+                        aa,
+                    ));
+                },
                 BorrowGlobal(mid, sid, type_actuals) if self.is_imm_ref(dests[0]) => {
                     self.builder.emit(Call(
                         attr_id,
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/memory_instrumentation.rs b/third_party/move/move-prover/bytecode-pipeline/src/memory_instrumentation.rs
index fbf03c344fdd5..0839554ad8db5 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/memory_instrumentation.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/memory_instrumentation.rs
@@ -163,7 +163,7 @@ impl<'a> Instrumenter<'a> {
         if let Call(attr_id, dests, op, _, _) = bytecode {
             use Operation::*;
             match op {
-                BorrowLoc | BorrowField(..) | BorrowGlobal(..) => {
+                BorrowLoc | BorrowField(..) | BorrowGlobal(..) | BorrowVariantField(..) => {
                     let ty = &self
                         .builder
                         .get_target()
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs b/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
index 3efd6b1595f6c..e4810482c25ab 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
@@ -277,26 +277,29 @@ impl GlobalNumberOperationState {
         let struct_env = struct_env.module_env.env.get_module(mid).into_struct(sid);
         let mut field_oper_map = BTreeMap::new();
 
-        for (i, field) in struct_env.get_fields().enumerate() {
-            if field_idx_vec.contains(&i) {
-                field_oper_map.insert(field.get_id(), Bitwise);
-            } else {
-                let field_ty = field.get_type();
-                let arith_flag = if let Type::Reference(_, tr) = field_ty {
-                    tr.is_number()
-                } else if let Type::Vector(tr) = field_ty {
-                    tr.is_number()
-                } else {
-                    field_ty.is_number()
-                };
-                if arith_flag {
-                    field_oper_map.insert(field.get_id(), Arithmetic);
+        // TODO(#14349): add support for enum type
+        if !struct_env.has_variants() {
+            for (i, field) in struct_env.get_fields().enumerate() {
+                if field_idx_vec.contains(&i) {
+                    field_oper_map.insert(field.get_id(), Bitwise);
                 } else {
-                    field_oper_map.insert(field.get_id(), Bottom);
+                    let field_ty = field.get_type();
+                    let arith_flag = if let Type::Reference(_, tr) = field_ty {
+                        tr.is_number()
+                    } else if let Type::Vector(tr) = field_ty {
+                        tr.is_number()
+                    } else {
+                        field_ty.is_number()
+                    };
+                    if arith_flag {
+                        field_oper_map.insert(field.get_id(), Arithmetic);
+                    } else {
+                        field_oper_map.insert(field.get_id(), Bottom);
+                    }
                 }
             }
+            self.struct_operation_map.insert((mid, sid), field_oper_map);
         }
-        self.struct_operation_map.insert((mid, sid), field_oper_map);
     }
 
     /// Updates the number operation for the given node id.
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
index 630d71ddcda10..84a1104b496c8 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
@@ -1097,6 +1097,7 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                             } // empty, do nothing
                         }
                     },
+                    // TODO(#14349): add support for enum type related operation
                     _ => {},
                 }
             },


Test patch:
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.exp b/third_party/move/move-prover/tests/sources/functional/enum.exp
new file mode 100644
index 0000000000000..914ff680e45c2
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum.exp
@@ -0,0 +1,24 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum.move:3:5
+  │
+3 │     enum CommonFields has copy, drop {
+  │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum.move:10:25
+   │
+10 │         invariant (self is CommonFields::Bar) ==> self.z > 10;
+   │                         ^^ Move 2 language construct is not enabled: `is` expression
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum.move:39:9
+   │
+39 │         match (&common) {
+   │         ^^^^^ Move 2 language construct is not enabled: match expression
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum.move:49:5
+   │
+49 │     enum CommonFieldsVector has drop {
+   │     ^^^^ Move 2 language construct is not enabled: enum types
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.move b/third_party/move/move-prover/tests/sources/functional/enum.move
new file mode 100644
index 0000000000000..9ac6876a40186
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum.move
@@ -0,0 +1,86 @@
+module 0x815::m {
+
+    enum CommonFields has copy, drop {
+        Foo{x: u64, y: u8},
+        Bar{x: u64, y: u8, z: u32}
+    }
+
+    spec CommonFields {
+        invariant self.x > 20;
+        invariant (self is CommonFields::Bar) ==> self.z > 10;
+    }
+
+    fun t9_common_field(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        common.x = 15; // struct invariant fails
+        common.x
+    }
+
+    fun test_data_invariant() {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Bar {x: _x, y: _y, z} = &mut common;
+        *z = 9; // struct invariant fails
+    }
+
+    fun test_match_ref(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        match (&common) {
+            Foo {x, y: _} => *x,
+            Bar {x, y: _, z: _ } => *x + 1
+        }
+    }
+
+    spec test_match_ref {
+        ensures result == 31;
+    }
+
+    enum CommonFieldsVector has drop {
+        Foo{x: vector<u8>},
+        Bar{x: vector<u8>, y: vector<CommonFields>}
+    }
+
+    fun test_enum_vector() {
+        let _common_vector_1 = CommonFieldsVector::Foo {
+            x: vector[2]
+        };
+        let _common_fields = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let _common_vector_2 = CommonFieldsVector::Bar {
+            x: vector[2],
+            y: vector[_common_fields]
+        };
+        spec {
+            assert _common_vector_1.x != _common_vector_2.x; // this fails
+            assert _common_vector_2.y[0] == CommonFields::Bar {
+                x: 30,
+                y: 40,
+                z: 50
+            };
+        };
+        let _common_vector_3 = CommonFieldsVector::Bar {
+            x: vector[2],
+            y: vector[_common_fields]
+        };
+        spec {
+            assert _common_vector_2.x == _common_vector_3.x;
+            assert _common_vector_2 == _common_vector_3;
+        };
+
+    }
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp
new file mode 100644
index 0000000000000..3532e5a697a25
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp
@@ -0,0 +1,64 @@
+Move prover returns: exiting with verification errors
+error: data invariant does not hold
+  ┌─ tests/sources/functional/enum.move:9:9
+  │
+9 │         invariant self.x > 20;
+  │         ^^^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/enum.move:15: t9_common_field
+  =     at tests/sources/functional/enum.move:16: t9_common_field
+  =     at tests/sources/functional/enum.move:17: t9_common_field
+  =     at tests/sources/functional/enum.move:14: t9_common_field
+  =     at tests/sources/functional/enum.move:9
+  =     at tests/sources/functional/enum.move:10
+  =     at tests/sources/functional/enum.move:14: t9_common_field
+  =         common = <redacted>
+  =     at tests/sources/functional/enum.move:19: t9_common_field
+  =     at tests/sources/functional/enum.move:9
+
+error: data invariant does not hold
+   ┌─ tests/sources/functional/enum.move:10:9
+   │
+10 │         invariant (self is CommonFields::Bar) ==> self.z > 10;
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/enum.move:25: test_data_invariant
+   =     at tests/sources/functional/enum.move:26: test_data_invariant
+   =     at tests/sources/functional/enum.move:27: test_data_invariant
+   =     at tests/sources/functional/enum.move:24: test_data_invariant
+   =     at tests/sources/functional/enum.move:9
+   =     at tests/sources/functional/enum.move:10
+   =     at tests/sources/functional/enum.move:24: test_data_invariant
+   =         common = <redacted>
+   =     at tests/sources/functional/enum.move:29: test_data_invariant
+   =         <redacted> = <redacted>
+   =         z = <redacted>
+   =     at tests/sources/functional/enum.move:30: test_data_invariant
+   =     at tests/sources/functional/enum.move:9
+   =     at tests/sources/functional/enum.move:10
+
+error: unknown assertion failed
+   ┌─ tests/sources/functional/enum.move:68:13
+   │
+68 │             assert _common_vector_1.x != _common_vector_2.x; // this fails
+   │             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/enum.move:56: test_enum_vector
+   =     at tests/sources/functional/enum.move:55: test_enum_vector
+   =         _common_vector_1 = <redacted>
+   =     at tests/sources/functional/enum.move:59: test_enum_vector
+   =     at tests/sources/functional/enum.move:60: test_enum_vector
+   =     at tests/sources/functional/enum.move:61: test_enum_vector
+   =     at tests/sources/functional/enum.move:58: test_enum_vector
+   =     at tests/sources/functional/enum.move:9
+   =     at tests/sources/functional/enum.move:10
+   =     at tests/sources/functional/enum.move:64: test_enum_vector
+   =     at tests/sources/functional/enum.move:65: test_enum_vector
+   =         <redacted> = <redacted>
+   =         _common_fields = <redacted>
+   =     at tests/sources/functional/enum.move:9
+   =     at tests/sources/functional/enum.move:65: test_enum_vector
+   =     at tests/sources/functional/enum.move:63: test_enum_vector
+   =         <redacted> = <redacted>
+   =         _common_vector_2 = <redacted>
+   =     at tests/sources/functional/enum.move:68: test_enum_vector
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_abort.exp b/third_party/move/move-prover/tests/sources/functional/enum_abort.exp
new file mode 100644
index 0000000000000..198891b5558ed
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_abort.exp
@@ -0,0 +1,24 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_abort.move:3:5
+  │
+3 │     enum CommonFields has copy, drop {
+  │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum_abort.move:41:9
+   │
+41 │         match (common) {
+   │         ^^^^^ Move 2 language construct is not enabled: match expression
+
+error: unsupported language construct
+    ┌─ tests/sources/functional/enum_abort.move:106:5
+    │
+106 │     enum CommonFields2 has drop {
+    │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+    ┌─ tests/sources/functional/enum_abort.move:121:9
+    │
+121 │         match (_common_vector_2) {
+    │         ^^^^^ Move 2 language construct is not enabled: match expression
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_abort.move b/third_party/move/move-prover/tests/sources/functional/enum_abort.move
new file mode 100644
index 0000000000000..8bd01cb8b2b2d
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_abort.move
@@ -0,0 +1,134 @@
+module 0x815::m {
+
+    enum CommonFields has copy, drop {
+        Foo{x: u64, y: u8},
+        Bar{x: u64, y: u8, z: u32}
+    }
+
+
+    fun select_abort(): u32 {
+        let common = CommonFields::Foo {
+            x: 30,
+            y: 40,
+        };
+        common.z // aborts
+    }
+
+    spec select_abort {
+        aborts_if false;
+    }
+
+    fun unpack_abort(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Foo {x, y: _y} = common; // aborts
+        x
+    }
+
+    spec unpack_abort {
+        aborts_if false;
+    }
+
+    fun test_match(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        match (common) {
+            Foo {x, y: _} => x,
+            Bar {x, y: _, z: _ } => x + 1
+        }
+    }
+
+    spec test_match {
+        aborts_if false;
+    }
+
+    fun test_borrow_field_abort() {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Foo {x, y: _y} = &mut common; // aborts
+        *x = 20;
+    }
+
+    spec test_borrow_field_abort {
+        aborts_if false;
+    }
+
+    fun test_borrow_field_not_abort() {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Bar {x, y: _y, z: _z} = &mut common;
+        *x = 20;
+    }
+
+    spec test_borrow_field_not_abort {
+        aborts_if false;
+    }
+
+    fun test_borrow_field_not_abort_2() {
+        let common = CommonFields::Foo {
+            x: 30,
+            y: 40,
+        };
+        let CommonFields::Foo {x, y: _y} = &mut common;
+        *x = 20;
+    }
+
+    spec test_borrow_field_not_abort_2 {
+        aborts_if false;
+    }
+
+    fun test_get_field_abort(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let CommonFields::Foo {x, y: _y} = & common; // aborts
+        *x
+    }
+
+    spec test_get_field_abort {
+        aborts_if false;
+    }
+
+    enum CommonFields2 has drop {
+        Foo{x: vector<u8>},
+        Bar{x: vector<u8>, y: CommonFields}
+    }
+
+    fun test_match_abort(): u64 {
+        let common = CommonFields::Bar {
+            x: 30,
+            y: 40,
+            z: 50
+        };
+        let _common_vector_2 = CommonFields2::Bar {
+            x: vector[2],
+            y: common
+        };
+        match (_common_vector_2) {
+            CommonFields2::Bar {x:_x, y: CommonFields::Bar {x:_, y:_, z:_z} } if _x[0] > 80 || _z <= 50 => {
+                abort 30 // aborts
+            }
+            _ => 2
+        }
+    }
+
+    spec test_match_abort {
+        aborts_if false;
+    }
+
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
new file mode 100644
index 0000000000000..e8b4f1b0ae992
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
@@ -0,0 +1,110 @@
+Move prover returns: exiting with verification errors
+error: abort not covered by any of the `aborts_if` clauses
+   ┌─ tests/sources/functional/enum_abort.move:17:5
+   │
+14 │           common.z // aborts
+   │           -------- abort happened here with execution failure
+   ·
+17 │ ╭     spec select_abort {
+18 │ │         aborts_if false;
+19 │ │     }
+   │ ╰─────^
+   │
+   =     at tests/sources/functional/enum_abort.move:11: select_abort
+   =     at tests/sources/functional/enum_abort.move:12: select_abort
+   =     at tests/sources/functional/enum_abort.move:10: select_abort
+   =         common = <redacted>
+   =     at tests/sources/functional/enum_abort.move:14: select_abort
+   =         ABORTED
+
+error: abort not covered by any of the `aborts_if` clauses
+   ┌─ tests/sources/functional/enum_abort.move:31:5
+   │
+27 │           let CommonFields::Foo {x, y: _y} = common; // aborts
+   │               ---------------------------- abort happened here with execution failure
+   ·
+31 │ ╭     spec unpack_abort {
+32 │ │         aborts_if false;
+33 │ │     }
+   │ ╰─────^
+   │
+   =     at tests/sources/functional/enum_abort.move:23: unpack_abort
+   =     at tests/sources/functional/enum_abort.move:24: unpack_abort
+   =     at tests/sources/functional/enum_abort.move:25: unpack_abort
+   =     at tests/sources/functional/enum_abort.move:22: unpack_abort
+   =     at tests/sources/functional/enum_abort.move:27: unpack_abort
+   =         ABORTED
+
+error: abort not covered by any of the `aborts_if` clauses
+   ┌─ tests/sources/functional/enum_abort.move:61:5
+   │
+57 │           let CommonFields::Foo {x, y: _y} = &mut common; // aborts
+   │               ---------------------------- abort happened here with execution failure
+   ·
+61 │ ╭     spec test_borrow_field_abort {
+62 │ │         aborts_if false;
+63 │ │     }
+   │ ╰─────^
+   │
+   =     at tests/sources/functional/enum_abort.move:53: test_borrow_field_abort
+   =     at tests/sources/functional/enum_abort.move:54: test_borrow_field_abort
+   =     at tests/sources/functional/enum_abort.move:55: test_borrow_field_abort
+   =     at tests/sources/functional/enum_abort.move:52: test_borrow_field_abort
+   =         common = <redacted>
+   =     at tests/sources/functional/enum_abort.move:57: test_borrow_field_abort
+   =         <redacted> = <redacted>
+   =     at tests/sources/functional/enum_abort.move:57: test_borrow_field_abort
+   =         ABORTED
+
+error: abort not covered by any of the `aborts_if` clauses
+    ┌─ tests/sources/functional/enum_abort.move:102:5
+    │
+ 98 │           let CommonFields::Foo {x, y: _y} = & common; // aborts
+    │               ---------------------------- abort happened here with execution failure
+    ·
+102 │ ╭     spec test_get_field_abort {
+103 │ │         aborts_if false;
+104 │ │     }
+    │ ╰─────^
+    │
+    =     at tests/sources/functional/enum_abort.move:94: test_get_field_abort
+    =     at tests/sources/functional/enum_abort.move:95: test_get_field_abort
+    =     at tests/sources/functional/enum_abort.move:96: test_get_field_abort
+    =     at tests/sources/functional/enum_abort.move:93: test_get_field_abort
+    =         common = <redacted>
+    =     at tests/sources/functional/enum_abort.move:98: test_get_field_abort
+    =         <redacted> = <redacted>
+    =         ABORTED
+
+error: abort not covered by any of the `aborts_if` clauses
+    ┌─ tests/sources/functional/enum_abort.move:129:5
+    │
+123 │                   abort 30 // aborts
+    │                   -------- abort happened here with code 0x1E
+    ·
+129 │ ╭     spec test_match_abort {
+130 │ │         aborts_if false;
+131 │ │     }
+    │ ╰─────^
+    │
+    =     at tests/sources/functional/enum_abort.move:113: test_match_abort
+    =     at tests/sources/functional/enum_abort.move:114: test_match_abort
+    =     at tests/sources/functional/enum_abort.move:115: test_match_abort
+    =     at tests/sources/functional/enum_abort.move:112: test_match_abort
+    =     at tests/sources/functional/enum_abort.move:118: test_match_abort
+    =     at tests/sources/functional/enum_abort.move:117: test_match_abort
+    =         <redacted> = <redacted>
+    =         common = <redacted>
+    =         _common_vector_2 = <redacted>
+    =     at tests/sources/functional/enum_abort.move:122: test_match_abort
+    =         <redacted> = <redacted>
+    =         _x = <redacted>
+    =     at tests/sources/functional/enum_abort.move:122: test_match_abort
+    =         _z = <redacted>
+    =         <redacted> = <redacted>
+    =     at tests/sources/functional/enum_abort.move:122: test_match_abort
+    =         <redacted> = <redacted>
+    =     at tests/sources/functional/enum_abort.move:122: test_match_abort
+    =         <redacted> = <redacted>
+    =     at tests/sources/functional/enum_abort.move:123: test_match_abort
+    =         ABORTED
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_positional.exp b/third_party/move/move-prover/tests/sources/functional/enum_positional.exp
new file mode 100644
index 0000000000000..ddb42a216da47
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_positional.exp
@@ -0,0 +1,45 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_positional.move:3:5
+  │
+3 │     enum Positional has drop {
+  │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_positional.move:4:10
+  │
+4 │         A(u8),
+  │          ^ Move 2 language construct is not enabled: positional fields
+
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_positional.move:5:10
+  │
+5 │         B(u8),
+  │          ^ Move 2 language construct is not enabled: positional fields
+
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_positional.move:9:24
+  │
+9 │         invariant self.0 > 20;
+  │                        ^ Move 2 language construct is not enabled: positional field
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum_positional.move:15:21
+   │
+15 │            assert x.0 == 42;
+   │                     ^ Move 2 language construct is not enabled: positional field
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/enum_positional.move:17:9
+   │
+17 │         match (&mut x) {
+   │         ^^^^^ Move 2 language construct is not enabled: match expression
+
+error: unexpected token
+   ┌─ tests/sources/functional/enum_positional.move:18:26
+   │
+18 │             Positional::A(y) => *y = 3, // aborts
+   │                          ^
+   │                          │
+   │                          Unexpected '('
+   │                          Expected '{'
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_positional.move b/third_party/move/move-prover/tests/sources/functional/enum_positional.move
new file mode 100644
index 0000000000000..59794a64656f1
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_positional.move
@@ -0,0 +1,39 @@
+module 0x815::m {
+
+    enum Positional has drop {
+        A(u8),
+        B(u8),
+    }
+
+    spec Positional {
+        invariant self.0 > 20;
+    }
+
+    fun test_positional_incorrect(): u8 {
+        let x = Positional::A(42);
+        spec {
+           assert x.0 == 42;
+        };
+        match (&mut x) {
+            Positional::A(y) => *y = 3, // aborts
+            B(y) => *y = 50
+        };
+        20
+    }
+
+    fun test_positional_correct(): u8 {
+        let x = Positional::A(42);
+        spec {
+            assert x.0 == 42;
+        };
+        let z = &mut x;
+        match (z) {
+            Positional::A(y) => *y = 21,
+            B(y) => *y = 2
+        };
+        20
+    }
+
+
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_positional.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum_positional.v2_exp
new file mode 100644
index 0000000000000..5cb6cb81c4c63
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_positional.v2_exp
@@ -0,0 +1,18 @@
+Move prover returns: exiting with verification errors
+error: data invariant does not hold
+  ┌─ tests/sources/functional/enum_positional.move:9:9
+  │
+9 │         invariant self.0 > 20;
+  │         ^^^^^^^^^^^^^^^^^^^^^^
+  │
+  =     at tests/sources/functional/enum_positional.move:13: test_positional_incorrect
+  =     at tests/sources/functional/enum_positional.move:9
+  =     at tests/sources/functional/enum_positional.move:13: test_positional_incorrect
+  =         x = <redacted>
+  =     at tests/sources/functional/enum_positional.move:15: test_positional_incorrect
+  =     at tests/sources/functional/enum_positional.move:17: test_positional_incorrect
+  =         <redacted> = <redacted>
+  =     at tests/sources/functional/enum_positional.move:18: test_positional_incorrect
+  =         <redacted> = <redacted>
+  =         y = <redacted>
+  =     at tests/sources/functional/enum_positional.move:9
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_self.exp b/third_party/move/move-prover/tests/sources/functional/enum_self.exp
new file mode 100644
index 0000000000000..716e9ee097a93
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_self.exp
@@ -0,0 +1,12 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_self.move:3:5
+  │
+3 │     enum EnumSelf has copy, drop {
+  │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+  ┌─ tests/sources/functional/enum_self.move:7:5
+  │
+7 │     enum EnumUseSelf has copy, drop {
+  │     ^^^^ Move 2 language construct is not enabled: enum types
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_self.move b/third_party/move/move-prover/tests/sources/functional/enum_self.move
new file mode 100644
index 0000000000000..e65000b87e551
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_self.move
@@ -0,0 +1,27 @@
+module 0x815::m {
+
+    enum EnumSelf has copy, drop {
+        A { self: u64}
+    }
+
+    enum EnumUseSelf has copy, drop {
+       Self { self: EnumSelf }
+    }
+
+    spec EnumUseSelf {
+        invariant self.self.self > 10;
+    }
+
+    fun test_enum_self() {
+        let s = EnumSelf::A {
+            self: 30
+        };
+        let self_s = EnumUseSelf::Self {
+            self: s
+        };
+        let EnumUseSelf::Self {self: A {self} } = &mut self_s;
+        *self = 10; // aborts
+    }
+
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_self.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum_self.v2_exp
new file mode 100644
index 0000000000000..a7f2aa23e0cc0
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/enum_self.v2_exp
@@ -0,0 +1,18 @@
+Move prover returns: exiting with verification errors
+error: data invariant does not hold
+   ┌─ tests/sources/functional/enum_self.move:12:9
+   │
+12 │         invariant self.self.self > 10;
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   │
+   =     at tests/sources/functional/enum_self.move:17: test_enum_self
+   =     at tests/sources/functional/enum_self.move:16: test_enum_self
+   =     at tests/sources/functional/enum_self.move:19: test_enum_self
+   =     at tests/sources/functional/enum_self.move:12
+   =     at tests/sources/functional/enum_self.move:19: test_enum_self
+   =         self_s = <redacted>
+   =     at tests/sources/functional/enum_self.move:22: test_enum_self
+   =     at tests/sources/functional/enum_self.move:23: test_enum_self
+   =         <redacted> = <redacted>
+   =         self = <redacted>
+   =     at tests/sources/functional/enum_self.move:12