diff --git a/third_party/move/move-compiler-v2/Cargo.toml b/third_party/move/move-compiler-v2/Cargo.toml
index f34ed25bb930d..c46708cc3f468 100644
--- a/third_party/move/move-compiler-v2/Cargo.toml
+++ b/third_party/move/move-compiler-v2/Cargo.toml
@@ -18,6 +18,7 @@ move-command-line-common = { path = "../move-command-line-common" }
 #move-package = { path = "../tools/move-package" }
 move-compiler = { path = "../move-compiler" }
 move-core-types = { path = "../move-core/types" }
+move-disassembler = { path = "../tools/move-disassembler" }
 move-ir-types = { path = "../move-ir/types" }
 move-model = { path = "../move-model" }
 move-stackless-bytecode = { path = "../move-model/bytecode" }
@@ -42,7 +43,6 @@ serde = { version = "1.0.124", features = ["derive"] }
 anyhow = "1.0.52"
 datatest-stable = "0.1.1"
 move-command-line-common = { path = "../move-command-line-common" }
-move-disassembler = { path = "../tools/move-disassembler" }
 move-ir-types = { path = "../move-ir/types" }
 move-prover-test-utils = { path = "../move-prover/test-utils" }
 move-stdlib = { path = "../move-stdlib" }
diff --git a/third_party/move/move-compiler-v2/src/lib.rs b/third_party/move/move-compiler-v2/src/lib.rs
index 0714725bff9a6..6455ee09da6d9 100644
--- a/third_party/move/move-compiler-v2/src/lib.rs
+++ b/third_party/move/move-compiler-v2/src/lib.rs
@@ -25,15 +25,19 @@ use anyhow::bail;
 use codespan_reporting::term::termcolor::{ColorChoice, StandardStream, WriteColor};
 pub use experiments::*;
 use log::{debug, info, log_enabled, trace, Level};
+use move_binary_format::binary_views::BinaryIndexedView;
+use move_command_line_common::files::FileHash;
 use move_compiler::{
     compiled_unit::{
-        AnnotatedCompiledModule, AnnotatedCompiledScript, AnnotatedCompiledUnit, CompiledUnit,
-        FunctionInfo,
+        verify_units, AnnotatedCompiledModule, AnnotatedCompiledScript, AnnotatedCompiledUnit,
+        CompiledUnit, FunctionInfo,
     },
     diagnostics::FilesSourceText,
     shared::{known_attributes::KnownAttribute, unique_map::UniqueMap},
 };
-use move_model::{model::GlobalEnv, PackageInfo};
+use move_disassembler::disassembler::Disassembler;
+use move_ir_types::location;
+use move_model::{add_move_lang_diagnostics, model::GlobalEnv, PackageInfo};
 use move_stackless_bytecode::function_target_pipeline::{
     FunctionTargetPipeline, FunctionTargetsHolder, FunctionVariant,
 };
@@ -60,7 +64,7 @@ pub fn run_move_compiler(
     let mut env = run_checker(options.clone())?;
     check_errors(&env, error_writer, "checking errors")?;
 
-    trace!("After context check, GlobalEnv={}", env.dump_env());
+    trace!("After context check, GlobalEnv=\n{}", env.dump_env());
 
     // Flow-insensitive checks on AST
     flow_insensitive_checkers::check_for_unused_vars_and_params(&mut env);
@@ -69,7 +73,7 @@ pub fn run_move_compiler(
     check_errors(&env, error_writer, "checking errors")?;
 
     trace!(
-        "After flow-insensitive checks, GlobalEnv={}",
+        "After flow-insensitive checks, GlobalEnv=\n{}",
         env.dump_env()
     );
 
@@ -77,7 +81,7 @@ pub fn run_move_compiler(
     inliner::run_inlining(&mut env);
     check_errors(&env, error_writer, "inlining")?;
 
-    debug!("After inlining, GlobalEnv={}", env.dump_env());
+    debug!("After inlining, GlobalEnv=\n{}", env.dump_env());
 
     // Run code generator
     let mut targets = run_bytecode_gen(&env);
@@ -110,8 +114,17 @@ pub fn run_move_compiler(
 
     let modules_and_scripts = run_file_format_gen(&env, &targets);
     check_errors(&env, error_writer, "assembling errors")?;
-    let annotated = annotate_units(modules_and_scripts);
-    Ok((env, annotated))
+
+    debug!(
+        "File format bytecode:\n{}",
+        disassemble_compiled_units(&modules_and_scripts)?
+    );
+
+    let annotated_units = annotate_units(modules_and_scripts);
+    run_bytecode_verifier(&annotated_units, &mut env);
+    check_errors(&env, error_writer, "bytecode verification errors")?;
+
+    Ok((env, annotated_units))
 }
 
 /// Run the type checker and return the global env (with errors if encountered). The result
@@ -151,7 +164,7 @@ pub fn run_checker(options: Options) -> anyhow::Result<GlobalEnv> {
 // compilation, create an entry in the functions target holder which encapsulate info
 // like the generated bytecode.
 pub fn run_bytecode_gen(env: &GlobalEnv) -> FunctionTargetsHolder {
-    info!("Bytecode Generation");
+    info!("Stackless bytecode Generation");
     let mut targets = FunctionTargetsHolder::default();
     let mut todo = BTreeSet::new();
     let mut done = BTreeSet::new();
@@ -232,6 +245,30 @@ fn add_default_optimization_pipeline(pipeline: &mut FunctionTargetPipeline) {
     pipeline.add_processor(Box::new(UnreachableCodeRemover {}));
 }
 
+/// Disassemble the given compiled units and return the disassembled code as a string.
+pub fn disassemble_compiled_units(units: &[CompiledUnit]) -> anyhow::Result<String> {
+    let disassembled_units: anyhow::Result<Vec<_>> = units
+        .iter()
+        .map(|unit| {
+            let view = match unit {
+                CompiledUnit::Module(module) => BinaryIndexedView::Module(&module.module),
+                CompiledUnit::Script(script) => BinaryIndexedView::Script(&script.script),
+            };
+            Disassembler::from_view(view, location::Loc::new(FileHash::empty(), 0, 0))
+                .and_then(|d| d.disassemble())
+        })
+        .collect();
+    Ok(disassembled_units?.concat())
+}
+
+/// Run the bytecode verifier on the given compiled units and add any diagnostics to the global env.
+pub fn run_bytecode_verifier(units: &[AnnotatedCompiledUnit], env: &mut GlobalEnv) {
+    let diags = verify_units(units);
+    if !diags.is_empty() {
+        add_move_lang_diagnostics(env, diags);
+    }
+}
+
 /// Report any diags in the env to the writer and fail if there are errors.
 pub fn check_errors<W: WriteColor>(
     env: &GlobalEnv,
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/assign.exp b/third_party/move/move-compiler-v2/tests/ability-checker/assign.exp
new file mode 100644
index 0000000000000..20abc4842e034
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/assign.exp
@@ -0,0 +1,360 @@
+============ initial bytecode ================
+
+[variant baseline]
+fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
+     var $t2: &mut u64
+  0: $t2 := borrow_field<assign::S>.f($t0)
+  1: write_ref($t2, $t1)
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_int($t0: &mut u64) {
+     var $t1: u64
+  0: $t1 := 42
+  1: write_ref($t0, $t1)
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
+     var $t3: u64
+     var $t4: assign::T
+  0: ($t1, $t4) := unpack assign::S($t0)
+  1: $t2 := unpack assign::T($t4)
+  2: $t3 := +($t1, $t2)
+  3: return $t3
+}
+
+
+[variant baseline]
+fun assign::assign_struct($t0: &mut assign::S) {
+     var $t1: assign::S
+     var $t2: u64
+     var $t3: assign::T
+     var $t4: u64
+  0: $t2 := 42
+  1: $t4 := 42
+  2: $t3 := pack assign::T($t4)
+  3: $t1 := pack assign::S($t2, $t3)
+  4: write_ref($t0, $t1)
+  5: return ()
+}
+
+============ after LiveVarAnalysisProcessor: ================
+
+[variant baseline]
+fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
+     var $t2: &mut u64
+     # live vars: $t0, $t1
+  0: $t2 := borrow_field<assign::S>.f($t0)
+     # live vars: $t1, $t2
+  1: write_ref($t2, $t1)
+     # live vars:
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_int($t0: &mut u64) {
+     var $t1: u64
+     # live vars: $t0
+  0: $t1 := 42
+     # live vars: $t0, $t1
+  1: write_ref($t0, $t1)
+     # live vars:
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
+     var $t3: u64
+     var $t4: assign::T
+     # live vars: $t0
+  0: ($t1, $t4) := unpack assign::S($t0)
+     # live vars: $t1, $t4
+  1: $t2 := unpack assign::T($t4)
+     # live vars: $t1, $t2
+  2: $t3 := +($t1, $t2)
+     # live vars: $t3
+  3: return $t3
+}
+
+
+[variant baseline]
+fun assign::assign_struct($t0: &mut assign::S) {
+     var $t1: assign::S
+     var $t2: u64
+     var $t3: assign::T
+     var $t4: u64
+     # live vars: $t0
+  0: $t2 := 42
+     # live vars: $t0, $t2
+  1: $t4 := 42
+     # live vars: $t0, $t2, $t4
+  2: $t3 := pack assign::T($t4)
+     # live vars: $t0, $t2, $t3
+  3: $t1 := pack assign::S($t2, $t3)
+     # live vars: $t0, $t1
+  4: write_ref($t0, $t1)
+     # live vars:
+  5: return ()
+}
+
+============ after MemorySafetyProcessor: ================
+
+[variant baseline]
+fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
+     var $t2: &mut u64
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := borrow_field<assign::S>.f($t0)
+     # live vars: $t1, $t2
+     # graph: {L0=local($t0)[borrow_field(true) -> L1],L1=local($t2)[]}
+     # local_to_label: {$t0=L0,$t2=L1}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: write_ref($t2, $t1)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_int($t0: &mut u64) {
+     var $t1: u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t1 := 42
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: write_ref($t0, $t1)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
+     var $t3: u64
+     var $t4: assign::T
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: ($t1, $t4) := unpack assign::S($t0)
+     # live vars: $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0}
+     #
+  1: $t2 := unpack assign::T($t4)
+     # live vars: $t1, $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t4}
+     #
+  2: $t3 := +($t1, $t2)
+     # live vars: $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t2,$t4}
+     #
+  3: return $t3
+}
+
+
+[variant baseline]
+fun assign::assign_struct($t0: &mut assign::S) {
+     var $t1: assign::S
+     var $t2: u64
+     var $t3: assign::T
+     var $t4: u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := 42
+     # live vars: $t0, $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t4 := 42
+     # live vars: $t0, $t2, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t3 := pack assign::T($t4)
+     # live vars: $t0, $t2, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t4}
+     #
+  3: $t1 := pack assign::S($t2, $t3)
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4}
+     #
+  4: write_ref($t0, $t1)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4}
+     #
+  5: return ()
+}
+
+============ after ExplicitDrop: ================
+
+[variant baseline]
+fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
+     var $t2: &mut u64
+  0: $t2 := borrow_field<assign::S>.f($t0)
+  1: drop($t0)
+  2: write_ref($t2, $t1)
+  3: drop($t2)
+  4: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_int($t0: &mut u64) {
+     var $t1: u64
+  0: $t1 := 42
+  1: write_ref($t0, $t1)
+  2: drop($t0)
+  3: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
+     var $t3: u64
+     var $t4: assign::T
+  0: ($t1, $t4) := unpack assign::S($t0)
+  1: $t2 := unpack assign::T($t4)
+  2: $t3 := +($t1, $t2)
+  3: return $t3
+}
+
+
+[variant baseline]
+fun assign::assign_struct($t0: &mut assign::S) {
+     var $t1: assign::S
+     var $t2: u64
+     var $t3: assign::T
+     var $t4: u64
+  0: $t2 := 42
+  1: $t4 := 42
+  2: $t3 := pack assign::T($t4)
+  3: $t1 := pack assign::S($t2, $t3)
+  4: write_ref($t0, $t1)
+  5: drop($t0)
+  6: drop($t1)
+  7: return ()
+}
+
+
+Diagnostics:
+error: cannot drop
+   ┌─ tests/ability-checker/assign.move:17:9
+   │
+17 │         *s = S { f: 42, g: T { h: 42 } };
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: write_ref: cannot drop
+   ┌─ tests/ability-checker/assign.move:17:9
+   │
+17 │         *s = S { f: 42, g: T { h: 42 } };
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+============ after AbilityChecker: ================
+
+[variant baseline]
+fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
+     var $t2: &mut u64
+  0: $t2 := borrow_field<assign::S>.f($t0)
+  1: drop($t0)
+  2: write_ref($t2, $t1)
+  3: drop($t2)
+  4: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_int($t0: &mut u64) {
+     var $t1: u64
+  0: $t1 := 42
+  1: write_ref($t0, $t1)
+  2: drop($t0)
+  3: return ()
+}
+
+
+[variant baseline]
+fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
+     var $t3: u64
+     var $t4: assign::T
+  0: ($t1, $t4) := unpack assign::S($t0)
+  1: $t2 := unpack assign::T($t4)
+  2: $t3 := +($t1, $t2)
+  3: return $t3
+}
+
+
+[variant baseline]
+fun assign::assign_struct($t0: &mut assign::S) {
+     var $t1: assign::S
+     var $t2: u64
+     var $t3: assign::T
+     var $t4: u64
+  0: $t2 := 42
+  1: $t4 := 42
+  2: $t3 := pack assign::T($t4)
+  3: $t1 := pack assign::S($t2, $t3)
+  4: write_ref($t0, $t1)
+  5: drop($t0)
+  6: drop($t1)
+  7: return ()
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/assign.move b/third_party/move/move-compiler-v2/tests/ability-checker/assign.move
new file mode 100644
index 0000000000000..2ea2fe8d33721
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/assign.move
@@ -0,0 +1,28 @@
+module 0x42::assign {
+
+    struct S {
+        f: u64,
+        g: T
+    }
+
+    struct T {
+        h: u64
+    }
+
+    fun assign_int(x: &mut u64) {
+       *x = 42;
+    }
+
+    fun assign_struct(s: &mut S) {
+        *s = S { f: 42, g: T { h: 42 } };
+    }
+
+    fun assign_pattern(s: S, f: u64, h: u64): u64 {
+        S { f, g: T { h } } = s;
+        f + h
+    }
+
+    fun assign_field(s: &mut S, f: u64) {
+        s.f = f;
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.exp b/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.exp
new file mode 100644
index 0000000000000..985104073389f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.exp
@@ -0,0 +1,924 @@
+============ initial bytecode ================
+
+[variant baseline]
+fun fields::read_ref($t0: &fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &u64
+  0: $t2 := borrow_field<fields::S>.g($t0)
+  1: $t3 := borrow_field<fields::T>.h($t2)
+  2: $t1 := read_ref($t3)
+  3: return $t1
+}
+
+
+[variant baseline]
+fun fields::read_val($t0: fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &fields::S
+     var $t4: &u64
+  0: $t3 := borrow_local($t0)
+  1: $t2 := borrow_field<fields::S>.g($t3)
+  2: $t4 := borrow_field<fields::T>.h($t2)
+  3: $t1 := read_ref($t4)
+  4: return $t1
+}
+
+
+[variant baseline]
+fun fields::write_local_direct(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: u64
+     var $t7: &mut u64
+     var $t8: &mut fields::T
+     var $t9: &mut fields::S
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := infer($t2)
+  5: $t6 := 42
+  6: $t9 := borrow_local($t1)
+  7: $t8 := borrow_field<fields::S>.g($t9)
+  8: $t7 := borrow_field<fields::T>.h($t8)
+  9: write_ref($t7, $t6)
+ 10: $t0 := infer($t1)
+ 11: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_local_via_ref(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: &mut fields::S
+     var $t7: &mut fields::S
+     var $t8: u64
+     var $t9: &mut u64
+     var $t10: &mut fields::T
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := infer($t2)
+  5: $t7 := borrow_local($t1)
+  6: $t6 := infer($t7)
+  7: $t8 := 42
+  8: $t10 := borrow_field<fields::S>.g($t6)
+  9: $t9 := borrow_field<fields::T>.h($t10)
+ 10: write_ref($t9, $t8)
+ 11: $t0 := infer($t1)
+ 12: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_param($t0: &mut fields::S) {
+     var $t1: u64
+     var $t2: &mut u64
+     var $t3: &mut fields::T
+  0: $t1 := 42
+  1: $t3 := borrow_field<fields::S>.g($t0)
+  2: $t2 := borrow_field<fields::T>.h($t3)
+  3: write_ref($t2, $t1)
+  4: return ()
+}
+
+
+[variant baseline]
+fun fields::write_val($t0: fields::S): fields::S {
+     var $t1: fields::S
+     var $t2: u64
+     var $t3: &mut u64
+     var $t4: &mut fields::T
+     var $t5: &mut fields::S
+  0: $t2 := 42
+  1: $t5 := borrow_local($t0)
+  2: $t4 := borrow_field<fields::S>.g($t5)
+  3: $t3 := borrow_field<fields::T>.h($t4)
+  4: write_ref($t3, $t2)
+  5: $t1 := infer($t0)
+  6: return $t1
+}
+
+============ after LiveVarAnalysisProcessor: ================
+
+[variant baseline]
+fun fields::read_ref($t0: &fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &u64
+     # live vars: $t0
+  0: $t2 := borrow_field<fields::S>.g($t0)
+     # live vars: $t2
+  1: $t3 := borrow_field<fields::T>.h($t2)
+     # live vars: $t3
+  2: $t1 := read_ref($t3)
+     # live vars: $t1
+  3: return $t1
+}
+
+
+[variant baseline]
+fun fields::read_val($t0: fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &fields::S
+     var $t4: &u64
+     # live vars: $t0
+  0: $t3 := borrow_local($t0)
+     # live vars: $t3
+  1: $t2 := borrow_field<fields::S>.g($t3)
+     # live vars: $t2
+  2: $t4 := borrow_field<fields::T>.h($t2)
+     # live vars: $t4
+  3: $t1 := read_ref($t4)
+     # live vars: $t1
+  4: return $t1
+}
+
+
+[variant baseline]
+fun fields::write_local_direct(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: u64
+     var $t7: &mut u64
+     var $t8: &mut fields::T
+     var $t9: &mut fields::S
+     # live vars:
+  0: $t3 := 0
+     # live vars: $t3
+  1: $t5 := 0
+     # live vars: $t3, $t5
+  2: $t4 := pack fields::T($t5)
+     # live vars: $t3, $t4
+  3: $t2 := pack fields::S($t3, $t4)
+     # live vars: $t2
+  4: $t1 := move($t2)
+     # live vars: $t1
+  5: $t6 := 42
+     # live vars: $t1, $t6
+  6: $t9 := borrow_local($t1)
+     # live vars: $t1, $t6, $t9
+  7: $t8 := borrow_field<fields::S>.g($t9)
+     # live vars: $t1, $t6, $t8
+  8: $t7 := borrow_field<fields::T>.h($t8)
+     # live vars: $t1, $t6, $t7
+  9: write_ref($t7, $t6)
+     # live vars: $t1
+ 10: $t0 := move($t1)
+     # live vars: $t0
+ 11: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_local_via_ref(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: &mut fields::S
+     var $t7: &mut fields::S
+     var $t8: u64
+     var $t9: &mut u64
+     var $t10: &mut fields::T
+     # live vars:
+  0: $t3 := 0
+     # live vars: $t3
+  1: $t5 := 0
+     # live vars: $t3, $t5
+  2: $t4 := pack fields::T($t5)
+     # live vars: $t3, $t4
+  3: $t2 := pack fields::S($t3, $t4)
+     # live vars: $t2
+  4: $t1 := move($t2)
+     # live vars: $t1
+  5: $t7 := borrow_local($t1)
+     # live vars: $t1, $t7
+  6: $t6 := move($t7)
+     # live vars: $t1, $t6
+  7: $t8 := 42
+     # live vars: $t1, $t6, $t8
+  8: $t10 := borrow_field<fields::S>.g($t6)
+     # live vars: $t1, $t8, $t10
+  9: $t9 := borrow_field<fields::T>.h($t10)
+     # live vars: $t1, $t8, $t9
+ 10: write_ref($t9, $t8)
+     # live vars: $t1
+ 11: $t0 := move($t1)
+     # live vars: $t0
+ 12: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_param($t0: &mut fields::S) {
+     var $t1: u64
+     var $t2: &mut u64
+     var $t3: &mut fields::T
+     # live vars: $t0
+  0: $t1 := 42
+     # live vars: $t0, $t1
+  1: $t3 := borrow_field<fields::S>.g($t0)
+     # live vars: $t1, $t3
+  2: $t2 := borrow_field<fields::T>.h($t3)
+     # live vars: $t1, $t2
+  3: write_ref($t2, $t1)
+     # live vars:
+  4: return ()
+}
+
+
+[variant baseline]
+fun fields::write_val($t0: fields::S): fields::S {
+     var $t1: fields::S
+     var $t2: u64
+     var $t3: &mut u64
+     var $t4: &mut fields::T
+     var $t5: &mut fields::S
+     # live vars: $t0
+  0: $t2 := 42
+     # live vars: $t0, $t2
+  1: $t5 := borrow_local($t0)
+     # live vars: $t0, $t2, $t5
+  2: $t4 := borrow_field<fields::S>.g($t5)
+     # live vars: $t0, $t2, $t4
+  3: $t3 := borrow_field<fields::T>.h($t4)
+     # live vars: $t0, $t2, $t3
+  4: write_ref($t3, $t2)
+     # live vars: $t0
+  5: $t1 := move($t0)
+     # live vars: $t1
+  6: return $t1
+}
+
+============ after MemorySafetyProcessor: ================
+
+[variant baseline]
+fun fields::read_ref($t0: &fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := borrow_field<fields::S>.g($t0)
+     # live vars: $t2
+     # graph: {L0=local($t0)[borrow_field(false) -> L1],L1=local($t2)[]}
+     # local_to_label: {$t0=L0,$t2=L1}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t3 := borrow_field<fields::T>.h($t2)
+     # live vars: $t3
+     # graph: {L0=local($t0)[borrow_field(false) -> L1],L1=local($t2)[borrow_field(false) -> L257],L257=local($t3)[]}
+     # local_to_label: {$t0=L0,$t2=L1,$t3=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t1 := read_ref($t3)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  3: return $t1
+}
+
+
+[variant baseline]
+fun fields::read_val($t0: fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &fields::S
+     var $t4: &u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t3 := borrow_local($t0)
+     # live vars: $t3
+     # graph: {L0=local($t0)[borrow(false) -> L1],L1=local($t3)[]}
+     # local_to_label: {$t0=L0,$t3=L1}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t2 := borrow_field<fields::S>.g($t3)
+     # live vars: $t2
+     # graph: {L0=local($t0)[borrow(false) -> L1],L1=local($t3)[borrow_field(false) -> L257],L257=local($t2)[]}
+     # local_to_label: {$t0=L0,$t2=L257,$t3=L1}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t4 := borrow_field<fields::T>.h($t2)
+     # live vars: $t4
+     # graph: {L0=local($t0)[borrow(false) -> L1],L1=local($t3)[borrow_field(false) -> L257],L257=local($t2)[borrow_field(false) -> L513],L513=local($t4)[]}
+     # local_to_label: {$t0=L0,$t2=L257,$t3=L1,$t4=L513}
+     # global_to_label: {}
+     # moved: {}
+     #
+  3: $t1 := read_ref($t4)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  4: return $t1
+}
+
+
+[variant baseline]
+fun fields::write_local_direct(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: u64
+     var $t7: &mut u64
+     var $t8: &mut fields::T
+     var $t9: &mut fields::S
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t3 := 0
+     # live vars: $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t5 := 0
+     # live vars: $t3, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t4 := pack fields::T($t5)
+     # live vars: $t3, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t5}
+     #
+  3: $t2 := pack fields::S($t3, $t4)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t3,$t4,$t5}
+     #
+  4: $t1 := move($t2)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  5: $t6 := 42
+     # live vars: $t1, $t6
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  6: $t9 := borrow_local($t1)
+     # live vars: $t1, $t6, $t9
+     # graph: {L1536=local($t1)[borrow(true) -> L1537],L1537=local($t9)[]}
+     # local_to_label: {$t1=L1536,$t9=L1537}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  7: $t8 := borrow_field<fields::S>.g($t9)
+     # live vars: $t1, $t6, $t8
+     # graph: {L1536=local($t1)[borrow(true) -> L1537],L1537=local($t9)[borrow_field(true) -> L1793],L1793=local($t8)[]}
+     # local_to_label: {$t1=L1536,$t8=L1793,$t9=L1537}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  8: $t7 := borrow_field<fields::T>.h($t8)
+     # live vars: $t1, $t6, $t7
+     # graph: {L1536=local($t1)[borrow(true) -> L1537],L1537=local($t9)[borrow_field(true) -> L1793],L1793=local($t8)[borrow_field(true) -> L2049],L2049=local($t7)[]}
+     # local_to_label: {$t1=L1536,$t7=L2049,$t8=L1793,$t9=L1537}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  9: write_ref($t7, $t6)
+     # live vars: $t1
+     # graph: {L1536=local($t1)[]}
+     # local_to_label: {$t1=L1536}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+ 10: $t0 := move($t1)
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1,$t2,$t3,$t4,$t5}
+     #
+ 11: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_local_via_ref(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: &mut fields::S
+     var $t7: &mut fields::S
+     var $t8: u64
+     var $t9: &mut u64
+     var $t10: &mut fields::T
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t3 := 0
+     # live vars: $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t5 := 0
+     # live vars: $t3, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t4 := pack fields::T($t5)
+     # live vars: $t3, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t5}
+     #
+  3: $t2 := pack fields::S($t3, $t4)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t3,$t4,$t5}
+     #
+  4: $t1 := move($t2)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  5: $t7 := borrow_local($t1)
+     # live vars: $t1, $t7
+     # graph: {L1280=local($t1)[borrow(true) -> L1281],L1281=local($t7)[]}
+     # local_to_label: {$t1=L1280,$t7=L1281}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5}
+     #
+  6: $t6 := move($t7)
+     # live vars: $t1, $t6
+     # graph: {L1280=local($t1)[borrow(true) -> L1281],L1281=local($t7)[skip -> L1537],L1537=local($t6)[]}
+     # local_to_label: {$t1=L1280,$t6=L1537,$t7=L1281}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5,$t7}
+     #
+  7: $t8 := 42
+     # live vars: $t1, $t6, $t8
+     # graph: {L1280=local($t1)[borrow(true) -> L1281],L1281=local($t7)[skip -> L1537],L1537=local($t6)[]}
+     # local_to_label: {$t1=L1280,$t6=L1537,$t7=L1281}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5,$t7}
+     #
+  8: $t10 := borrow_field<fields::S>.g($t6)
+     # live vars: $t1, $t8, $t10
+     # graph: {L1280=local($t1)[borrow(true) -> L1281],L1281=local($t7)[skip -> L1537],L1537=local($t6)[borrow_field(true) -> L2049],L2049=local($t10)[]}
+     # local_to_label: {$t1=L1280,$t6=L1537,$t7=L1281,$t10=L2049}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5,$t7}
+     #
+  9: $t9 := borrow_field<fields::T>.h($t10)
+     # live vars: $t1, $t8, $t9
+     # graph: {L1280=local($t1)[borrow(true) -> L1281],L1281=local($t7)[skip -> L1537],L1537=local($t6)[borrow_field(true) -> L2049],L2049=local($t10)[borrow_field(true) -> L2305],L2305=local($t9)[]}
+     # local_to_label: {$t1=L1280,$t6=L1537,$t7=L1281,$t9=L2305,$t10=L2049}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5,$t7}
+     #
+ 10: write_ref($t9, $t8)
+     # live vars: $t1
+     # graph: {L1280=local($t1)[]}
+     # local_to_label: {$t1=L1280}
+     # global_to_label: {}
+     # moved: {$t2,$t3,$t4,$t5,$t7}
+     #
+ 11: $t0 := move($t1)
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1,$t2,$t3,$t4,$t5,$t7}
+     #
+ 12: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_param($t0: &mut fields::S) {
+     var $t1: u64
+     var $t2: &mut u64
+     var $t3: &mut fields::T
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t1 := 42
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t3 := borrow_field<fields::S>.g($t0)
+     # live vars: $t1, $t3
+     # graph: {L256=local($t0)[borrow_field(true) -> L257],L257=local($t3)[]}
+     # local_to_label: {$t0=L256,$t3=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t2 := borrow_field<fields::T>.h($t3)
+     # live vars: $t1, $t2
+     # graph: {L256=local($t0)[borrow_field(true) -> L257],L257=local($t3)[borrow_field(true) -> L513],L513=local($t2)[]}
+     # local_to_label: {$t0=L256,$t2=L513,$t3=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  3: write_ref($t2, $t1)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  4: return ()
+}
+
+
+[variant baseline]
+fun fields::write_val($t0: fields::S): fields::S {
+     var $t1: fields::S
+     var $t2: u64
+     var $t3: &mut u64
+     var $t4: &mut fields::T
+     var $t5: &mut fields::S
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := 42
+     # live vars: $t0, $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t5 := borrow_local($t0)
+     # live vars: $t0, $t2, $t5
+     # graph: {L256=local($t0)[borrow(true) -> L257],L257=local($t5)[]}
+     # local_to_label: {$t0=L256,$t5=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t4 := borrow_field<fields::S>.g($t5)
+     # live vars: $t0, $t2, $t4
+     # graph: {L256=local($t0)[borrow(true) -> L257],L257=local($t5)[borrow_field(true) -> L513],L513=local($t4)[]}
+     # local_to_label: {$t0=L256,$t4=L513,$t5=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  3: $t3 := borrow_field<fields::T>.h($t4)
+     # live vars: $t0, $t2, $t3
+     # graph: {L256=local($t0)[borrow(true) -> L257],L257=local($t5)[borrow_field(true) -> L513],L513=local($t4)[borrow_field(true) -> L769],L769=local($t3)[]}
+     # local_to_label: {$t0=L256,$t3=L769,$t4=L513,$t5=L257}
+     # global_to_label: {}
+     # moved: {}
+     #
+  4: write_ref($t3, $t2)
+     # live vars: $t0
+     # graph: {L256=local($t0)[]}
+     # local_to_label: {$t0=L256}
+     # global_to_label: {}
+     # moved: {}
+     #
+  5: $t1 := move($t0)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0}
+     #
+  6: return $t1
+}
+
+============ after ExplicitDrop: ================
+
+[variant baseline]
+fun fields::read_ref($t0: &fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &u64
+  0: $t2 := borrow_field<fields::S>.g($t0)
+  1: drop($t0)
+  2: $t3 := borrow_field<fields::T>.h($t2)
+  3: drop($t2)
+  4: $t1 := read_ref($t3)
+  5: drop($t3)
+  6: return $t1
+}
+
+
+[variant baseline]
+fun fields::read_val($t0: fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &fields::S
+     var $t4: &u64
+  0: $t3 := borrow_local($t0)
+  1: $t2 := borrow_field<fields::S>.g($t3)
+  2: drop($t3)
+  3: $t4 := borrow_field<fields::T>.h($t2)
+  4: drop($t2)
+  5: $t1 := read_ref($t4)
+  6: release($t0)
+  7: drop($t4)
+  8: return $t1
+}
+
+
+[variant baseline]
+fun fields::write_local_direct(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: u64
+     var $t7: &mut u64
+     var $t8: &mut fields::T
+     var $t9: &mut fields::S
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := move($t2)
+  5: $t6 := 42
+  6: $t9 := borrow_local($t1)
+  7: $t8 := borrow_field<fields::S>.g($t9)
+  8: drop($t9)
+  9: $t7 := borrow_field<fields::T>.h($t8)
+ 10: drop($t8)
+ 11: write_ref($t7, $t6)
+ 12: drop($t7)
+ 13: $t0 := move($t1)
+ 14: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_local_via_ref(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: &mut fields::S
+     var $t7: &mut fields::S
+     var $t8: u64
+     var $t9: &mut u64
+     var $t10: &mut fields::T
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := move($t2)
+  5: $t7 := borrow_local($t1)
+  6: $t6 := move($t7)
+  7: $t8 := 42
+  8: $t10 := borrow_field<fields::S>.g($t6)
+  9: drop($t6)
+ 10: $t9 := borrow_field<fields::T>.h($t10)
+ 11: drop($t10)
+ 12: write_ref($t9, $t8)
+ 13: drop($t9)
+ 14: $t0 := move($t1)
+ 15: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_param($t0: &mut fields::S) {
+     var $t1: u64
+     var $t2: &mut u64
+     var $t3: &mut fields::T
+  0: $t1 := 42
+  1: $t3 := borrow_field<fields::S>.g($t0)
+  2: drop($t0)
+  3: $t2 := borrow_field<fields::T>.h($t3)
+  4: drop($t3)
+  5: write_ref($t2, $t1)
+  6: drop($t2)
+  7: return ()
+}
+
+
+[variant baseline]
+fun fields::write_val($t0: fields::S): fields::S {
+     var $t1: fields::S
+     var $t2: u64
+     var $t3: &mut u64
+     var $t4: &mut fields::T
+     var $t5: &mut fields::S
+  0: $t2 := 42
+  1: $t5 := borrow_local($t0)
+  2: $t4 := borrow_field<fields::S>.g($t5)
+  3: drop($t5)
+  4: $t3 := borrow_field<fields::T>.h($t4)
+  5: drop($t4)
+  6: write_ref($t3, $t2)
+  7: drop($t3)
+  8: $t1 := move($t0)
+  9: return $t1
+}
+
+============ after AbilityChecker: ================
+
+[variant baseline]
+fun fields::read_ref($t0: &fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &u64
+  0: $t2 := borrow_field<fields::S>.g($t0)
+  1: drop($t0)
+  2: $t3 := borrow_field<fields::T>.h($t2)
+  3: drop($t2)
+  4: $t1 := read_ref($t3)
+  5: drop($t3)
+  6: return $t1
+}
+
+
+[variant baseline]
+fun fields::read_val($t0: fields::S): u64 {
+     var $t1: u64
+     var $t2: &fields::T
+     var $t3: &fields::S
+     var $t4: &u64
+  0: $t3 := borrow_local($t0)
+  1: $t2 := borrow_field<fields::S>.g($t3)
+  2: drop($t3)
+  3: $t4 := borrow_field<fields::T>.h($t2)
+  4: drop($t2)
+  5: $t1 := read_ref($t4)
+  6: release($t0)
+  7: drop($t4)
+  8: return $t1
+}
+
+
+[variant baseline]
+fun fields::write_local_direct(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: u64
+     var $t7: &mut u64
+     var $t8: &mut fields::T
+     var $t9: &mut fields::S
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := move($t2)
+  5: $t6 := 42
+  6: $t9 := borrow_local($t1)
+  7: $t8 := borrow_field<fields::S>.g($t9)
+  8: drop($t9)
+  9: $t7 := borrow_field<fields::T>.h($t8)
+ 10: drop($t8)
+ 11: write_ref($t7, $t6)
+ 12: drop($t7)
+ 13: $t0 := move($t1)
+ 14: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_local_via_ref(): fields::S {
+     var $t0: fields::S
+     var $t1: fields::S
+     var $t2: fields::S
+     var $t3: u64
+     var $t4: fields::T
+     var $t5: u64
+     var $t6: &mut fields::S
+     var $t7: &mut fields::S
+     var $t8: u64
+     var $t9: &mut u64
+     var $t10: &mut fields::T
+  0: $t3 := 0
+  1: $t5 := 0
+  2: $t4 := pack fields::T($t5)
+  3: $t2 := pack fields::S($t3, $t4)
+  4: $t1 := move($t2)
+  5: $t7 := borrow_local($t1)
+  6: $t6 := move($t7)
+  7: $t8 := 42
+  8: $t10 := borrow_field<fields::S>.g($t6)
+  9: drop($t6)
+ 10: $t9 := borrow_field<fields::T>.h($t10)
+ 11: drop($t10)
+ 12: write_ref($t9, $t8)
+ 13: drop($t9)
+ 14: $t0 := move($t1)
+ 15: return $t0
+}
+
+
+[variant baseline]
+fun fields::write_param($t0: &mut fields::S) {
+     var $t1: u64
+     var $t2: &mut u64
+     var $t3: &mut fields::T
+  0: $t1 := 42
+  1: $t3 := borrow_field<fields::S>.g($t0)
+  2: drop($t0)
+  3: $t2 := borrow_field<fields::T>.h($t3)
+  4: drop($t3)
+  5: write_ref($t2, $t1)
+  6: drop($t2)
+  7: return ()
+}
+
+
+[variant baseline]
+fun fields::write_val($t0: fields::S): fields::S {
+     var $t1: fields::S
+     var $t2: u64
+     var $t3: &mut u64
+     var $t4: &mut fields::T
+     var $t5: &mut fields::S
+  0: $t2 := 42
+  1: $t5 := borrow_local($t0)
+  2: $t4 := borrow_field<fields::S>.g($t5)
+  3: drop($t5)
+  4: $t3 := borrow_field<fields::T>.h($t4)
+  5: drop($t4)
+  6: write_ref($t3, $t2)
+  7: drop($t3)
+  8: $t1 := move($t0)
+  9: return $t1
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.move b/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.move
new file mode 100644
index 0000000000000..da6bea9d1d449
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/failing/fields.move
@@ -0,0 +1,41 @@
+module 0x42::fields {
+
+    struct S {
+        f: u64,
+        g: T
+    }
+
+    struct T {
+        h: u64
+    }
+
+    fun read_val(x: S): u64 {
+        x.g.h
+    }
+
+    fun read_ref(x: &S): u64 {
+        x.g.h
+    }
+
+    fun write_val(x: S): S {
+        x.g.h = 42;
+        x
+    }
+
+    fun write_param(x: &mut S) {
+        x.g.h = 42;
+    }
+
+    fun write_local_via_ref(): S {
+        let x = S { f: 0, g: T { h: 0 } };
+        let r = &mut x;
+        r.g.h = 42;
+        x
+    }
+
+    fun write_local_direct(): S {
+        let x = S { f: 0, g: T { h: 0 } };
+        x.g.h = 42;
+        x
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.exp b/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.exp
new file mode 100644
index 0000000000000..53c3cfa378102
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.exp
@@ -0,0 +1,1354 @@
+============ initial bytecode ================
+
+[variant baseline]
+fun operators::arithm($t0: u64, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t6 := -($t0, $t1)
+  1: $t5 := /($t1, $t6)
+  2: $t4 := *($t5, $t1)
+  3: $t3 := %($t4, $t0)
+  4: $t2 := +($t0, $t3)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bits($t0: u64, $t1: u8): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t4 := <<($t0, $t1)
+  1: $t3 := &($t4, $t0)
+  2: $t6 := >>($t0, $t1)
+  3: $t5 := ^($t6, $t0)
+  4: $t2 := |($t3, $t5)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bools($t0: bool, $t1: bool): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: if ($t0) goto 1 else goto 4
+  1: label L0
+  2: $t5 := infer($t1)
+  3: goto 6
+  4: label L1
+  5: $t5 := false
+  6: label L2
+  7: if ($t5) goto 8 else goto 11
+  8: label L3
+  9: $t4 := true
+ 10: goto 19
+ 11: label L4
+ 12: if ($t0) goto 13 else goto 16
+ 13: label L6
+ 14: $t4 := !($t1)
+ 15: goto 18
+ 16: label L7
+ 17: $t4 := false
+ 18: label L8
+ 19: label L5
+ 20: if ($t4) goto 21 else goto 24
+ 21: label L9
+ 22: $t3 := true
+ 23: goto 33
+ 24: label L10
+ 25: $t6 := !($t0)
+ 26: if ($t6) goto 27 else goto 30
+ 27: label L12
+ 28: $t3 := infer($t1)
+ 29: goto 32
+ 30: label L13
+ 31: $t3 := false
+ 32: label L14
+ 33: label L11
+ 34: if ($t3) goto 35 else goto 38
+ 35: label L15
+ 36: $t2 := true
+ 37: goto 47
+ 38: label L16
+ 39: $t7 := !($t0)
+ 40: if ($t7) goto 41 else goto 44
+ 41: label L18
+ 42: $t2 := !($t1)
+ 43: goto 46
+ 44: label L19
+ 45: $t2 := false
+ 46: label L20
+ 47: label L17
+ 48: return $t2
+}
+
+
+[variant baseline]
+fun operators::equality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := ==($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::inequality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := !=($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::order($t0: u64, $t1: u64): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: $t5 := <($t0, $t1)
+  1: if ($t5) goto 2 else goto 5
+  2: label L0
+  3: $t4 := <=($t0, $t1)
+  4: goto 7
+  5: label L1
+  6: $t4 := false
+  7: label L2
+  8: if ($t4) goto 9 else goto 13
+  9: label L3
+ 10: $t6 := >($t0, $t1)
+ 11: $t3 := !($t6)
+ 12: goto 15
+ 13: label L4
+ 14: $t3 := false
+ 15: label L5
+ 16: if ($t3) goto 17 else goto 21
+ 17: label L6
+ 18: $t7 := >=($t0, $t1)
+ 19: $t2 := !($t7)
+ 20: goto 23
+ 21: label L7
+ 22: $t2 := false
+ 23: label L8
+ 24: return $t2
+}
+
+============ after LiveVarAnalysisProcessor: ================
+
+[variant baseline]
+fun operators::arithm($t0: u64, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     # live vars: $t0, $t1
+  0: $t6 := -($t0, $t1)
+     # live vars: $t0, $t1, $t6
+  1: $t5 := /($t1, $t6)
+     # live vars: $t0, $t1, $t5
+  2: $t4 := *($t5, $t1)
+     # live vars: $t0, $t4
+  3: $t3 := %($t4, $t0)
+     # live vars: $t0, $t3
+  4: $t2 := +($t0, $t3)
+     # live vars: $t2
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bits($t0: u64, $t1: u8): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     # live vars: $t0, $t1
+  0: $t4 := <<($t0, $t1)
+     # live vars: $t0, $t1, $t4
+  1: $t3 := &($t4, $t0)
+     # live vars: $t0, $t1, $t3
+  2: $t6 := >>($t0, $t1)
+     # live vars: $t0, $t3, $t6
+  3: $t5 := ^($t6, $t0)
+     # live vars: $t3, $t5
+  4: $t2 := |($t3, $t5)
+     # live vars: $t2
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bools($t0: bool, $t1: bool): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+     # live vars: $t0, $t1
+  0: if ($t0) goto 1 else goto 4
+     # live vars: $t0, $t1
+  1: label L0
+     # live vars: $t0, $t1
+  2: $t5 := copy($t1)
+     # live vars: $t0, $t1, $t5
+  3: goto 6
+     # live vars: $t0, $t1
+  4: label L1
+     # live vars: $t0, $t1
+  5: $t5 := false
+     # live vars: $t0, $t1, $t5
+  6: label L2
+     # live vars: $t0, $t1, $t5
+  7: if ($t5) goto 8 else goto 11
+     # live vars: $t0, $t1
+  8: label L3
+     # live vars: $t0, $t1
+  9: $t4 := true
+     # live vars: $t0, $t1, $t4
+ 10: goto 19
+     # live vars: $t0, $t1
+ 11: label L4
+     # live vars: $t0, $t1
+ 12: if ($t0) goto 13 else goto 16
+     # live vars: $t0, $t1
+ 13: label L6
+     # live vars: $t0, $t1
+ 14: $t4 := !($t1)
+     # live vars: $t0, $t1, $t4
+ 15: goto 18
+     # live vars: $t0, $t1
+ 16: label L7
+     # live vars: $t0, $t1
+ 17: $t4 := false
+     # live vars: $t0, $t1, $t4
+ 18: label L8
+     # live vars: $t0, $t1, $t4
+ 19: label L5
+     # live vars: $t0, $t1, $t4
+ 20: if ($t4) goto 21 else goto 24
+     # live vars: $t0, $t1
+ 21: label L9
+     # live vars: $t0, $t1
+ 22: $t3 := true
+     # live vars: $t0, $t1, $t3
+ 23: goto 33
+     # live vars: $t0, $t1
+ 24: label L10
+     # live vars: $t0, $t1
+ 25: $t6 := !($t0)
+     # live vars: $t0, $t1, $t6
+ 26: if ($t6) goto 27 else goto 30
+     # live vars: $t0, $t1
+ 27: label L12
+     # live vars: $t0, $t1
+ 28: $t3 := copy($t1)
+     # live vars: $t0, $t1, $t3
+ 29: goto 32
+     # live vars: $t0, $t1
+ 30: label L13
+     # live vars: $t0, $t1
+ 31: $t3 := false
+     # live vars: $t0, $t1, $t3
+ 32: label L14
+     # live vars: $t0, $t1, $t3
+ 33: label L11
+     # live vars: $t0, $t1, $t3
+ 34: if ($t3) goto 35 else goto 38
+     # live vars: $t0, $t1
+ 35: label L15
+     # live vars:
+ 36: $t2 := true
+     # live vars: $t2
+ 37: goto 47
+     # live vars: $t0, $t1
+ 38: label L16
+     # live vars: $t0, $t1
+ 39: $t7 := !($t0)
+     # live vars: $t1, $t7
+ 40: if ($t7) goto 41 else goto 44
+     # live vars: $t1
+ 41: label L18
+     # live vars: $t1
+ 42: $t2 := !($t1)
+     # live vars: $t2
+ 43: goto 46
+     # live vars: $t1
+ 44: label L19
+     # live vars:
+ 45: $t2 := false
+     # live vars: $t2
+ 46: label L20
+     # live vars: $t2
+ 47: label L17
+     # live vars: $t2
+ 48: return $t2
+}
+
+
+[variant baseline]
+fun operators::equality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+     # live vars: $t0, $t1
+  0: $t2 := ==($t0, $t1)
+     # live vars: $t2
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::inequality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+     # live vars: $t0, $t1
+  0: $t2 := !=($t0, $t1)
+     # live vars: $t2
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::order($t0: u64, $t1: u64): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+     # live vars: $t0, $t1
+  0: $t5 := <($t0, $t1)
+     # live vars: $t0, $t1, $t5
+  1: if ($t5) goto 2 else goto 5
+     # live vars: $t0, $t1
+  2: label L0
+     # live vars: $t0, $t1
+  3: $t4 := <=($t0, $t1)
+     # live vars: $t0, $t1, $t4
+  4: goto 7
+     # live vars: $t0, $t1
+  5: label L1
+     # live vars: $t0, $t1
+  6: $t4 := false
+     # live vars: $t0, $t1, $t4
+  7: label L2
+     # live vars: $t0, $t1, $t4
+  8: if ($t4) goto 9 else goto 13
+     # live vars: $t0, $t1
+  9: label L3
+     # live vars: $t0, $t1
+ 10: $t6 := >($t0, $t1)
+     # live vars: $t0, $t1, $t6
+ 11: $t3 := !($t6)
+     # live vars: $t0, $t1, $t3
+ 12: goto 15
+     # live vars: $t0, $t1
+ 13: label L4
+     # live vars: $t0, $t1
+ 14: $t3 := false
+     # live vars: $t0, $t1, $t3
+ 15: label L5
+     # live vars: $t0, $t1, $t3
+ 16: if ($t3) goto 17 else goto 21
+     # live vars: $t0, $t1
+ 17: label L6
+     # live vars: $t0, $t1
+ 18: $t7 := >=($t0, $t1)
+     # live vars: $t7
+ 19: $t2 := !($t7)
+     # live vars: $t2
+ 20: goto 23
+     # live vars: $t0, $t1
+ 21: label L7
+     # live vars:
+ 22: $t2 := false
+     # live vars: $t2
+ 23: label L8
+     # live vars: $t2
+ 24: return $t2
+}
+
+============ after MemorySafetyProcessor: ================
+
+[variant baseline]
+fun operators::arithm($t0: u64, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t6 := -($t0, $t1)
+     # live vars: $t0, $t1, $t6
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  1: $t5 := /($t1, $t6)
+     # live vars: $t0, $t1, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+  2: $t4 := *($t5, $t1)
+     # live vars: $t0, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t5,$t6}
+     #
+  3: $t3 := %($t4, $t0)
+     # live vars: $t0, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t4,$t5,$t6}
+     #
+  4: $t2 := +($t0, $t3)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t3,$t4,$t5,$t6}
+     #
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bits($t0: u64, $t1: u8): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t4 := <<($t0, $t1)
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  1: $t3 := &($t4, $t0)
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t4}
+     #
+  2: $t6 := >>($t0, $t1)
+     # live vars: $t0, $t3, $t6
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t4}
+     #
+  3: $t5 := ^($t6, $t0)
+     # live vars: $t3, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t4,$t6}
+     #
+  4: $t2 := |($t3, $t5)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t3,$t4,$t5,$t6}
+     #
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bools($t0: bool, $t1: bool): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: if ($t0) goto 1 else goto 4
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: label L0
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  2: $t5 := copy($t1)
+     # live vars: $t0, $t1, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  3: goto 6
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  4: label L1
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  5: $t5 := false
+     # live vars: $t0, $t1, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  6: label L2
+     # live vars: $t0, $t1, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  7: if ($t5) goto 8 else goto 11
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  8: label L3
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  9: $t4 := true
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 10: goto 19
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 11: label L4
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 12: if ($t0) goto 13 else goto 16
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 13: label L6
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 14: $t4 := !($t1)
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 15: goto 18
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 16: label L7
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+ 17: $t4 := false
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 18: label L8
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 19: label L5
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 20: if ($t4) goto 21 else goto 24
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 21: label L9
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 22: $t3 := true
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 23: goto 33
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 24: label L10
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t1}
+     #
+ 25: $t6 := !($t0)
+     # live vars: $t0, $t1, $t6
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 26: if ($t6) goto 27 else goto 30
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 27: label L12
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 28: $t3 := copy($t1)
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 29: goto 32
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 30: label L13
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 31: $t3 := false
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 32: label L14
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 33: label L11
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 34: if ($t3) goto 35 else goto 38
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 35: label L15
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 36: $t2 := true
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 37: goto 47
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 38: label L16
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 39: $t7 := !($t0)
+     # live vars: $t1, $t7
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 40: if ($t7) goto 41 else goto 44
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 41: label L18
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 42: $t2 := !($t1)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 43: goto 46
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 44: label L19
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 45: $t2 := false
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 46: label L20
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 47: label L17
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 48: return $t2
+}
+
+
+[variant baseline]
+fun operators::equality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := ==($t0, $t1)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::inequality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := !=($t0, $t1)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::order($t0: u64, $t1: u64): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t5 := <($t0, $t1)
+     # live vars: $t0, $t1, $t5
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  1: if ($t5) goto 2 else goto 5
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  2: label L0
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  3: $t4 := <=($t0, $t1)
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  4: goto 7
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  5: label L1
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  6: $t4 := false
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  7: label L2
+     # live vars: $t0, $t1, $t4
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  8: if ($t4) goto 9 else goto 13
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+  9: label L3
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 10: $t6 := >($t0, $t1)
+     # live vars: $t0, $t1, $t6
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 11: $t3 := !($t6)
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 12: goto 15
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 13: label L4
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1}
+     #
+ 14: $t3 := false
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 15: label L5
+     # live vars: $t0, $t1, $t3
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 16: if ($t3) goto 17 else goto 21
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 17: label L6
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 18: $t7 := >=($t0, $t1)
+     # live vars: $t7
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 19: $t2 := !($t7)
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6,$t7}
+     #
+ 20: goto 23
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 21: label L7
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6}
+     #
+ 22: $t2 := false
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6,$t7}
+     #
+ 23: label L8
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t6,$t7}
+     #
+ 24: return $t2
+}
+
+============ after ExplicitDrop: ================
+
+[variant baseline]
+fun operators::arithm($t0: u64, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t6 := -($t0, $t1)
+  1: $t5 := /($t1, $t6)
+  2: $t4 := *($t5, $t1)
+  3: $t3 := %($t4, $t0)
+  4: $t2 := +($t0, $t3)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bits($t0: u64, $t1: u8): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t4 := <<($t0, $t1)
+  1: $t3 := &($t4, $t0)
+  2: $t6 := >>($t0, $t1)
+  3: $t5 := ^($t6, $t0)
+  4: $t2 := |($t3, $t5)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bools($t0: bool, $t1: bool): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: if ($t0) goto 1 else goto 4
+  1: label L0
+  2: $t5 := copy($t1)
+  3: goto 6
+  4: label L1
+  5: $t5 := false
+  6: label L2
+  7: if ($t5) goto 8 else goto 11
+  8: label L3
+  9: $t4 := true
+ 10: goto 19
+ 11: label L4
+ 12: if ($t0) goto 13 else goto 16
+ 13: label L6
+ 14: $t4 := !($t1)
+ 15: goto 18
+ 16: label L7
+ 17: $t4 := false
+ 18: label L8
+ 19: label L5
+ 20: if ($t4) goto 21 else goto 24
+ 21: label L9
+ 22: $t3 := true
+ 23: goto 33
+ 24: label L10
+ 25: $t6 := !($t0)
+ 26: if ($t6) goto 27 else goto 30
+ 27: label L12
+ 28: $t3 := copy($t1)
+ 29: goto 32
+ 30: label L13
+ 31: $t3 := false
+ 32: label L14
+ 33: label L11
+ 34: if ($t3) goto 35 else goto 38
+ 35: label L15
+ 36: $t2 := true
+ 37: goto 47
+ 38: label L16
+ 39: $t7 := !($t0)
+ 40: if ($t7) goto 41 else goto 44
+ 41: label L18
+ 42: $t2 := !($t1)
+ 43: goto 46
+ 44: label L19
+ 45: $t2 := false
+ 46: label L20
+ 47: label L17
+ 48: return $t2
+}
+
+
+[variant baseline]
+fun operators::equality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := ==($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::inequality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := !=($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::order($t0: u64, $t1: u64): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: $t5 := <($t0, $t1)
+  1: if ($t5) goto 2 else goto 5
+  2: label L0
+  3: $t4 := <=($t0, $t1)
+  4: goto 7
+  5: label L1
+  6: $t4 := false
+  7: label L2
+  8: if ($t4) goto 9 else goto 13
+  9: label L3
+ 10: $t6 := >($t0, $t1)
+ 11: $t3 := !($t6)
+ 12: goto 15
+ 13: label L4
+ 14: $t3 := false
+ 15: label L5
+ 16: if ($t3) goto 17 else goto 21
+ 17: label L6
+ 18: $t7 := >=($t0, $t1)
+ 19: $t2 := !($t7)
+ 20: goto 23
+ 21: label L7
+ 22: $t2 := false
+ 23: label L8
+ 24: return $t2
+}
+
+============ after AbilityChecker: ================
+
+[variant baseline]
+fun operators::arithm($t0: u64, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t6 := -($t0, $t1)
+  1: $t5 := /($t1, $t6)
+  2: $t4 := *($t5, $t1)
+  3: $t3 := %($t4, $t0)
+  4: $t2 := +($t0, $t3)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bits($t0: u64, $t1: u8): u64 {
+     var $t2: u64
+     var $t3: u64
+     var $t4: u64
+     var $t5: u64
+     var $t6: u64
+  0: $t4 := <<($t0, $t1)
+  1: $t3 := &($t4, $t0)
+  2: $t6 := >>($t0, $t1)
+  3: $t5 := ^($t6, $t0)
+  4: $t2 := |($t3, $t5)
+  5: return $t2
+}
+
+
+[variant baseline]
+fun operators::bools($t0: bool, $t1: bool): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: if ($t0) goto 1 else goto 4
+  1: label L0
+  2: $t5 := copy($t1)
+  3: goto 6
+  4: label L1
+  5: $t5 := false
+  6: label L2
+  7: if ($t5) goto 8 else goto 11
+  8: label L3
+  9: $t4 := true
+ 10: goto 19
+ 11: label L4
+ 12: if ($t0) goto 13 else goto 16
+ 13: label L6
+ 14: $t4 := !($t1)
+ 15: goto 18
+ 16: label L7
+ 17: $t4 := false
+ 18: label L8
+ 19: label L5
+ 20: if ($t4) goto 21 else goto 24
+ 21: label L9
+ 22: $t3 := true
+ 23: goto 33
+ 24: label L10
+ 25: $t6 := !($t0)
+ 26: if ($t6) goto 27 else goto 30
+ 27: label L12
+ 28: $t3 := copy($t1)
+ 29: goto 32
+ 30: label L13
+ 31: $t3 := false
+ 32: label L14
+ 33: label L11
+ 34: if ($t3) goto 35 else goto 38
+ 35: label L15
+ 36: $t2 := true
+ 37: goto 47
+ 38: label L16
+ 39: $t7 := !($t0)
+ 40: if ($t7) goto 41 else goto 44
+ 41: label L18
+ 42: $t2 := !($t1)
+ 43: goto 46
+ 44: label L19
+ 45: $t2 := false
+ 46: label L20
+ 47: label L17
+ 48: return $t2
+}
+
+
+[variant baseline]
+fun operators::equality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := ==($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::inequality<#0>($t0: #0, $t1: #0): bool {
+     var $t2: bool
+  0: $t2 := !=($t0, $t1)
+  1: return $t2
+}
+
+
+[variant baseline]
+fun operators::order($t0: u64, $t1: u64): bool {
+     var $t2: bool
+     var $t3: bool
+     var $t4: bool
+     var $t5: bool
+     var $t6: bool
+     var $t7: bool
+  0: $t5 := <($t0, $t1)
+  1: if ($t5) goto 2 else goto 5
+  2: label L0
+  3: $t4 := <=($t0, $t1)
+  4: goto 7
+  5: label L1
+  6: $t4 := false
+  7: label L2
+  8: if ($t4) goto 9 else goto 13
+  9: label L3
+ 10: $t6 := >($t0, $t1)
+ 11: $t3 := !($t6)
+ 12: goto 15
+ 13: label L4
+ 14: $t3 := false
+ 15: label L5
+ 16: if ($t3) goto 17 else goto 21
+ 17: label L6
+ 18: $t7 := >=($t0, $t1)
+ 19: $t2 := !($t7)
+ 20: goto 23
+ 21: label L7
+ 22: $t2 := false
+ 23: label L8
+ 24: return $t2
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.move b/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.move
new file mode 100644
index 0000000000000..b06cebbbde997
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/failing/operators.move
@@ -0,0 +1,25 @@
+module 0x42::operators {
+    fun arithm(x: u64, y: u64): u64 {
+        x + y / (x - y) * y % x
+    }
+
+    fun bits(x: u64, y: u8): u64 {
+        x << y & x | x >> y ^ x
+    }
+
+    fun bools(x: bool, y: bool): bool {
+        x && y || x && !y || !x && y || !x && !y
+    }
+
+    fun equality<T>(x: T, y: T): bool {
+        x == y
+    }
+
+    fun inequality<T>(x: T, y: T): bool {
+        x != y
+    }
+
+    fun order(x: u64, y: u64): bool {
+        x < y && x <= y && !(x > y) && !(x >= y)
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/globals.exp b/third_party/move/move-compiler-v2/tests/ability-checker/globals.exp
new file mode 100644
index 0000000000000..58aec4093351e
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/globals.exp
@@ -0,0 +1,422 @@
+
+Diagnostics:
+warning: Unused parameter `x`. Consider removing or prefixing with an underscore: `_x`
+   ┌─ tests/ability-checker/globals.move:18:27
+   │
+18 │     fun write(a: address, x: u64): u64 {
+   │                           ^
+
+============ initial bytecode ================
+
+[variant baseline]
+fun globals::check($t0: address): bool {
+     var $t1: bool
+  0: $t1 := exists<globals::R>($t0)
+  1: return $t1
+}
+
+
+[variant baseline]
+fun globals::publish($t0: &signer) {
+     var $t1: globals::R
+     var $t2: u64
+  0: $t2 := 1
+  1: $t1 := pack globals::R($t2)
+  2: move_to<globals::R>($t0, $t1)
+  3: return ()
+}
+
+
+[variant baseline]
+fun globals::read($t0: address): u64 {
+     var $t1: u64
+     var $t2: &globals::R
+     var $t3: &globals::R
+     var $t4: &u64
+  0: $t3 := borrow_global<globals::R>($t0)
+  1: $t2 := infer($t3)
+  2: $t4 := borrow_field<globals::R>.f($t2)
+  3: $t1 := read_ref($t4)
+  4: return $t1
+}
+
+
+[variant baseline]
+fun globals::write($t0: address, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: &mut globals::R
+     var $t4: &mut globals::R
+     var $t5: u64
+     var $t6: &mut u64
+  0: $t4 := borrow_global<globals::R>($t0)
+  1: $t3 := infer($t4)
+  2: $t5 := 2
+  3: $t6 := borrow_field<globals::R>.f($t3)
+  4: write_ref($t6, $t5)
+  5: $t2 := 9
+  6: return $t2
+}
+
+============ after LiveVarAnalysisProcessor: ================
+
+[variant baseline]
+fun globals::check($t0: address): bool {
+     var $t1: bool
+     # live vars: $t0
+  0: $t1 := exists<globals::R>($t0)
+     # live vars: $t1
+  1: return $t1
+}
+
+
+[variant baseline]
+fun globals::publish($t0: &signer) {
+     var $t1: globals::R
+     var $t2: u64
+     # live vars: $t0
+  0: $t2 := 1
+     # live vars: $t0, $t2
+  1: $t1 := pack globals::R($t2)
+     # live vars: $t0, $t1
+  2: move_to<globals::R>($t0, $t1)
+     # live vars:
+  3: return ()
+}
+
+
+[variant baseline]
+fun globals::read($t0: address): u64 {
+     var $t1: u64
+     var $t2: &globals::R
+     var $t3: &globals::R
+     var $t4: &u64
+     # live vars: $t0
+  0: $t3 := borrow_global<globals::R>($t0)
+     # live vars: $t3
+  1: $t2 := move($t3)
+     # live vars: $t2
+  2: $t4 := borrow_field<globals::R>.f($t2)
+     # live vars: $t4
+  3: $t1 := read_ref($t4)
+     # live vars: $t1
+  4: return $t1
+}
+
+
+[variant baseline]
+fun globals::write($t0: address, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: &mut globals::R
+     var $t4: &mut globals::R
+     var $t5: u64
+     var $t6: &mut u64
+     # live vars: $t0
+  0: $t4 := borrow_global<globals::R>($t0)
+     # live vars: $t4
+  1: $t3 := move($t4)
+     # live vars: $t3
+  2: $t5 := 2
+     # live vars: $t3, $t5
+  3: $t6 := borrow_field<globals::R>.f($t3)
+     # live vars: $t5, $t6
+  4: write_ref($t6, $t5)
+     # live vars:
+  5: $t2 := 9
+     # live vars: $t2
+  6: return $t2
+}
+
+============ after MemorySafetyProcessor: ================
+
+[variant baseline]
+fun globals::check($t0: address): bool {
+     var $t1: bool
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t1 := exists<globals::R>($t0)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0}
+     #
+  1: return $t1
+}
+
+
+[variant baseline]
+fun globals::publish($t0: &signer) {
+     var $t1: globals::R
+     var $t2: u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t2 := 1
+     # live vars: $t0, $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  1: $t1 := pack globals::R($t2)
+     # live vars: $t0, $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t2}
+     #
+  2: move_to<globals::R>($t0, $t1)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t0,$t1,$t2}
+     #
+  3: return ()
+}
+
+
+[variant baseline]
+fun globals::read($t0: address): u64 {
+     var $t1: u64
+     var $t2: &globals::R
+     var $t3: &globals::R
+     var $t4: &u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t3 := borrow_global<globals::R>($t0)
+     # live vars: $t3
+     # graph: {L0=global<globals::R>[borrow_global(false) -> L1],L1=local($t3)[]}
+     # local_to_label: {$t3=L1}
+     # global_to_label: {globals::R=L0}
+     # moved: {}
+     #
+  1: $t2 := move($t3)
+     # live vars: $t2
+     # graph: {L0=global<globals::R>[borrow_global(false) -> L1],L1=local($t3)[skip -> L257],L257=local($t2)[]}
+     # local_to_label: {$t2=L257,$t3=L1}
+     # global_to_label: {globals::R=L0}
+     # moved: {$t3}
+     #
+  2: $t4 := borrow_field<globals::R>.f($t2)
+     # live vars: $t4
+     # graph: {L0=global<globals::R>[borrow_global(false) -> L1],L1=local($t3)[skip -> L257],L257=local($t2)[borrow_field(false) -> L513],L513=local($t4)[]}
+     # local_to_label: {$t2=L257,$t3=L1,$t4=L513}
+     # global_to_label: {globals::R=L0}
+     # moved: {$t3}
+     #
+  3: $t1 := read_ref($t4)
+     # live vars: $t1
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t3}
+     #
+  4: return $t1
+}
+
+
+[variant baseline]
+fun globals::write($t0: address, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: &mut globals::R
+     var $t4: &mut globals::R
+     var $t5: u64
+     var $t6: &mut u64
+     # live vars: $t0
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {}
+     #
+  0: $t4 := borrow_global<globals::R>($t0)
+     # live vars: $t4
+     # graph: {L0=global<globals::R>[borrow_global(true) -> L1],L1=local($t4)[]}
+     # local_to_label: {$t4=L1}
+     # global_to_label: {globals::R=L0}
+     # moved: {}
+     #
+  1: $t3 := move($t4)
+     # live vars: $t3
+     # graph: {L0=global<globals::R>[borrow_global(true) -> L1],L1=local($t4)[skip -> L257],L257=local($t3)[]}
+     # local_to_label: {$t3=L257,$t4=L1}
+     # global_to_label: {globals::R=L0}
+     # moved: {$t4}
+     #
+  2: $t5 := 2
+     # live vars: $t3, $t5
+     # graph: {L0=global<globals::R>[borrow_global(true) -> L1],L1=local($t4)[skip -> L257],L257=local($t3)[]}
+     # local_to_label: {$t3=L257,$t4=L1}
+     # global_to_label: {globals::R=L0}
+     # moved: {$t4}
+     #
+  3: $t6 := borrow_field<globals::R>.f($t3)
+     # live vars: $t5, $t6
+     # graph: {L0=global<globals::R>[borrow_global(true) -> L1],L1=local($t4)[skip -> L257],L257=local($t3)[borrow_field(true) -> L769],L769=local($t6)[]}
+     # local_to_label: {$t3=L257,$t4=L1,$t6=L769}
+     # global_to_label: {globals::R=L0}
+     # moved: {$t4}
+     #
+  4: write_ref($t6, $t5)
+     # live vars:
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t4}
+     #
+  5: $t2 := 9
+     # live vars: $t2
+     # graph: {}
+     # local_to_label: {}
+     # global_to_label: {}
+     # moved: {$t4}
+     #
+  6: return $t2
+}
+
+============ after ExplicitDrop: ================
+
+[variant baseline]
+fun globals::check($t0: address): bool {
+     var $t1: bool
+  0: $t1 := exists<globals::R>($t0)
+  1: return $t1
+}
+
+
+[variant baseline]
+fun globals::publish($t0: &signer) {
+     var $t1: globals::R
+     var $t2: u64
+  0: $t2 := 1
+  1: $t1 := pack globals::R($t2)
+  2: move_to<globals::R>($t0, $t1)
+  3: return ()
+}
+
+
+[variant baseline]
+fun globals::read($t0: address): u64 {
+     var $t1: u64
+     var $t2: &globals::R
+     var $t3: &globals::R
+     var $t4: &u64
+  0: $t3 := borrow_global<globals::R>($t0)
+  1: $t2 := move($t3)
+  2: $t4 := borrow_field<globals::R>.f($t2)
+  3: drop($t2)
+  4: $t1 := read_ref($t4)
+  5: drop($t4)
+  6: return $t1
+}
+
+
+[variant baseline]
+fun globals::write($t0: address, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: &mut globals::R
+     var $t4: &mut globals::R
+     var $t5: u64
+     var $t6: &mut u64
+  0: $t4 := borrow_global<globals::R>($t0)
+  1: $t3 := move($t4)
+  2: $t5 := 2
+  3: $t6 := borrow_field<globals::R>.f($t3)
+  4: drop($t3)
+  5: write_ref($t6, $t5)
+  6: drop($t6)
+  7: $t2 := 9
+  8: return $t2
+}
+
+
+Diagnostics:
+error: no key ability
+  ┌─ tests/ability-checker/globals.move:6:9
+  │
+6 │         move_to(s, R{f: 1});
+  │         ^^^^^^^^^^^^^^^^^^^
+
+error: no key ability
+   ┌─ tests/ability-checker/globals.move:10:9
+   │
+10 │         exists<R>(a)
+   │         ^^^^^^^^^^^^
+
+error: no key ability
+   ┌─ tests/ability-checker/globals.move:14:17
+   │
+14 │         let r = borrow_global<R>(a);
+   │                 ^^^^^^^^^^^^^^^^^^^
+
+error: no key ability
+   ┌─ tests/ability-checker/globals.move:19:17
+   │
+19 │         let r = borrow_global_mut<R>(a);
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^
+
+============ after AbilityChecker: ================
+
+[variant baseline]
+fun globals::check($t0: address): bool {
+     var $t1: bool
+  0: $t1 := exists<globals::R>($t0)
+  1: return $t1
+}
+
+
+[variant baseline]
+fun globals::publish($t0: &signer) {
+     var $t1: globals::R
+     var $t2: u64
+  0: $t2 := 1
+  1: $t1 := pack globals::R($t2)
+  2: move_to<globals::R>($t0, $t1)
+  3: return ()
+}
+
+
+[variant baseline]
+fun globals::read($t0: address): u64 {
+     var $t1: u64
+     var $t2: &globals::R
+     var $t3: &globals::R
+     var $t4: &u64
+  0: $t3 := borrow_global<globals::R>($t0)
+  1: $t2 := move($t3)
+  2: $t4 := borrow_field<globals::R>.f($t2)
+  3: drop($t2)
+  4: $t1 := read_ref($t4)
+  5: drop($t4)
+  6: return $t1
+}
+
+
+[variant baseline]
+fun globals::write($t0: address, $t1: u64): u64 {
+     var $t2: u64
+     var $t3: &mut globals::R
+     var $t4: &mut globals::R
+     var $t5: u64
+     var $t6: &mut u64
+  0: $t4 := borrow_global<globals::R>($t0)
+  1: $t3 := move($t4)
+  2: $t5 := 2
+  3: $t6 := borrow_field<globals::R>.f($t3)
+  4: drop($t3)
+  5: write_ref($t6, $t5)
+  6: drop($t6)
+  7: $t2 := 9
+  8: return $t2
+}
diff --git a/third_party/move/move-compiler-v2/tests/ability-checker/globals.move b/third_party/move/move-compiler-v2/tests/ability-checker/globals.move
new file mode 100644
index 0000000000000..e2da286af777a
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/ability-checker/globals.move
@@ -0,0 +1,23 @@
+module 0x42::globals {
+
+    struct R has store { f: u64 }
+
+    fun publish(s: &signer) {
+        move_to(s, R{f: 1});
+    }
+
+    fun check(a: address): bool {
+        exists<R>(a)
+    }
+
+    fun read(a: address): u64 {
+        let r = borrow_global<R>(a);
+        r.f
+    }
+
+    fun write(a: address, x: u64): u64 {
+        let r = borrow_global_mut<R>(a);
+        r.f = 2;
+        9
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.exp b/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.exp
new file mode 100644
index 0000000000000..c6971722dbe49
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.exp
@@ -0,0 +1,49 @@
+
+============ disassembled file-format ==================
+// Move bytecode v7
+module c0ffee.m {
+
+
+equality<Ty0>(Arg0: Ty0, Arg1: Ty0): bool /* def_idx: 0 */ {
+B0:
+	0: MoveLoc[0](Arg0: Ty0)
+	1: MoveLoc[1](Arg1: Ty0)
+	2: Eq
+	3: Ret
+}
+}
+Diagnostics:
+bug: BYTECODE VERIFICATION FAILED
+  ┌─ tests/bytecode-verify-failure/equality.move:1:1
+  │
+1 │ ╭ module 0xc0ffee::m {
+2 │ │   fun equality<T>(x: T, y: T): bool {
+3 │ │         x == y
+4 │ │     }
+5 │ │ }
+  │ ╰─^ ICE failed bytecode verifier: VMError {
+    major_status: EQUALITY_OP_TYPE_MISMATCH_ERROR,
+    sub_status: None,
+    message: None,
+    exec_state: None,
+    location: Module(
+        ModuleId {
+            address: 0000000000000000000000000000000000000000000000000000000000c0ffee,
+            name: Identifier(
+                "m",
+            ),
+        },
+    ),
+    indices: [
+        (
+            FunctionDefinition,
+            0,
+        ),
+    ],
+    offsets: [
+        (
+            FunctionDefinitionIndex(0),
+            2,
+        ),
+    ],
+}
diff --git a/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.move b/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.move
new file mode 100644
index 0000000000000..4764e4d4cad8e
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.move
@@ -0,0 +1,5 @@
+module 0xc0ffee::m {
+  fun equality<T>(x: T, y: T): bool {
+        x == y
+    }
+}
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/assign.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/assign.exp
index cbbd99c02299a..7d114d1b2dadf 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/assign.exp
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/assign.exp
@@ -108,10 +108,10 @@ fun assign::assign_struct($t0: &mut assign::S) {
 ============ disassembled file-format ==================
 // Move bytecode v7
 module 42.assign {
-struct T {
+struct T has drop {
 	h: u64
 }
-struct S {
+struct S has drop {
 	f: u64,
 	g: T
 }
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/assign.move b/third_party/move/move-compiler-v2/tests/file-format-generator/assign.move
index 2ea2fe8d33721..afa8188675dd0 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/assign.move
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/assign.move
@@ -1,11 +1,11 @@
 module 0x42::assign {
 
-    struct S {
+    struct S has drop {
         f: u64,
         g: T
     }
 
-    struct T {
+    struct T has drop {
         h: u64
     }
 
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/fields.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/fields.exp
index 5918bfd282cbc..e38f7b731faa9 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/fields.exp
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/fields.exp
@@ -274,10 +274,10 @@ fun fields::write_val($t0: fields::S): fields::S {
 ============ disassembled file-format ==================
 // Move bytecode v7
 module 42.fields {
-struct T {
+struct T has drop {
 	h: u64
 }
-struct S {
+struct S has drop {
 	f: u64,
 	g: T
 }
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/fields.move b/third_party/move/move-compiler-v2/tests/file-format-generator/fields.move
index da6bea9d1d449..1d43aae913f18 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/fields.move
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/fields.move
@@ -1,11 +1,11 @@
 module 0x42::fields {
 
-    struct S {
+    struct S has drop {
         f: u64,
         g: T
     }
 
-    struct T {
+    struct T has drop {
         h: u64
     }
 
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/globals.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/globals.exp
index 0ad865102c8d2..18cf1c0cffec8 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/globals.exp
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/globals.exp
@@ -130,7 +130,7 @@ fun globals::write($t0: address, $t1: u64): u64 {
 ============ disassembled file-format ==================
 // Move bytecode v7
 module 42.globals {
-struct R has store {
+struct R has store, key {
 	f: u64
 }
 
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/globals.move b/third_party/move/move-compiler-v2/tests/file-format-generator/globals.move
index e2da286af777a..711bc02fb9701 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/globals.move
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/globals.move
@@ -1,6 +1,6 @@
 module 0x42::globals {
 
-    struct R has store { f: u64 }
+    struct R has key, store { f: u64 }
 
     fun publish(s: &signer) {
         move_to(s, R{f: 1});
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/operators.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/operators.exp
index db97c6526e6ce..ecc5a567b8c58 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/operators.exp
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/operators.exp
@@ -490,14 +490,14 @@ B18:
 	47: MoveLoc[5](loc3: bool)
 	48: Ret
 }
-equality<Ty0>(Arg0: Ty0, Arg1: Ty0): bool /* def_idx: 3 */ {
+equality<Ty0: drop>(Arg0: Ty0, Arg1: Ty0): bool /* def_idx: 3 */ {
 B0:
 	0: MoveLoc[0](Arg0: Ty0)
 	1: MoveLoc[1](Arg1: Ty0)
 	2: Eq
 	3: Ret
 }
-inequality<Ty0>(Arg0: Ty0, Arg1: Ty0): bool /* def_idx: 4 */ {
+inequality<Ty0: drop>(Arg0: Ty0, Arg1: Ty0): bool /* def_idx: 4 */ {
 B0:
 	0: MoveLoc[0](Arg0: Ty0)
 	1: MoveLoc[1](Arg1: Ty0)
diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/operators.move b/third_party/move/move-compiler-v2/tests/file-format-generator/operators.move
index b06cebbbde997..19bae2370d574 100644
--- a/third_party/move/move-compiler-v2/tests/file-format-generator/operators.move
+++ b/third_party/move/move-compiler-v2/tests/file-format-generator/operators.move
@@ -11,11 +11,11 @@ module 0x42::operators {
         x && y || x && !y || !x && y || !x && !y
     }
 
-    fun equality<T>(x: T, y: T): bool {
+    fun equality<T: drop>(x: T, y: T): bool {
         x == y
     }
 
-    fun inequality<T>(x: T, y: T): bool {
+    fun inequality<T: drop>(x: T, y: T): bool {
         x != y
     }
 
diff --git a/third_party/move/move-compiler-v2/tests/testsuite.rs b/third_party/move/move-compiler-v2/tests/testsuite.rs
index 85278f36c1f11..f37efdb752be7 100644
--- a/third_party/move/move-compiler-v2/tests/testsuite.rs
+++ b/third_party/move/move-compiler-v2/tests/testsuite.rs
@@ -4,11 +4,9 @@
 
 use codespan_reporting::{diagnostic::Severity, term::termcolor::Buffer};
 use log::{debug, trace};
-use move_binary_format::binary_views::BinaryIndexedView;
-use move_command_line_common::files::FileHash;
-use move_compiler::compiled_unit::CompiledUnit;
 use move_compiler_v2::{
-    flow_insensitive_checkers, function_checker, inliner, logging, pipeline,
+    annotate_units, disassemble_compiled_units, flow_insensitive_checkers, function_checker,
+    inliner, logging, pipeline,
     pipeline::{
         ability_checker::AbilityChecker, avail_copies_analysis::AvailCopiesAnalysisProcessor,
         copy_propagation::CopyPropagation, dead_store_elimination::DeadStoreElimination,
@@ -18,10 +16,8 @@ use move_compiler_v2::{
         unreachable_code_analysis::UnreachableCodeProcessor,
         unreachable_code_remover::UnreachableCodeRemover, visibility_checker::VisibilityChecker,
     },
-    run_file_format_gen, Options,
+    run_bytecode_verifier, run_file_format_gen, Options,
 };
-use move_disassembler::disassembler::Disassembler;
-use move_ir_types::location;
 use move_model::model::GlobalEnv;
 use move_prover_test_utils::{baseline_test, extract_test_directives};
 use move_stackless_bytecode::function_target_pipeline::FunctionTargetPipeline;
@@ -286,6 +282,21 @@ impl TestConfig {
                 dump_annotated_targets: true,
                 dump_for_only_some_stages: None,
             }
+        } else if path.contains("/bytecode-verify-failure/") {
+            pipeline.add_processor(Box::new(LiveVarAnalysisProcessor {
+                with_copy_inference: true,
+            }));
+            // Note that we do not run ability checker here, as we want to induce
+            // a bytecode verification failure. The test in /bytecode-verify-failure/
+            // has erroneous ability annotations.
+            Self {
+                type_check_only: false,
+                dump_ast: false,
+                pipeline,
+                generate_file_format: true,
+                dump_annotated_targets: false,
+                dump_for_only_some_stages: None,
+            }
         } else {
             panic!(
                 "unexpected test path `{}`, cannot derive configuration",
@@ -341,7 +352,7 @@ impl TestConfig {
         if ok && !self.type_check_only {
             // Run stackless bytecode generator
             let mut targets = move_compiler_v2::run_bytecode_gen(&env);
-            let ok = Self::check_diags(&mut test_output.borrow_mut(), &env);
+            ok = Self::check_diags(&mut test_output.borrow_mut(), &env);
             if ok {
                 // Run the target pipeline.
                 self.pipeline.run_with_hook(
@@ -411,22 +422,17 @@ impl TestConfig {
                         }
                     },
                 );
-                let ok = Self::check_diags(&mut test_output.borrow_mut(), &env);
+                ok = Self::check_diags(&mut test_output.borrow_mut(), &env);
                 if ok && self.generate_file_format {
                     let units = run_file_format_gen(&env, &targets);
                     let out = &mut test_output.borrow_mut();
                     out.push_str("\n============ disassembled file-format ==================\n");
-                    Self::check_diags(out, &env);
-                    for compiled_unit in units {
-                        let disassembled = match compiled_unit {
-                            CompiledUnit::Module(module) => {
-                                Self::disassemble(BinaryIndexedView::Module(&module.module))?
-                            },
-                            CompiledUnit::Script(script) => {
-                                Self::disassemble(BinaryIndexedView::Script(&script.script))?
-                            },
-                        };
-                        out.push_str(&disassembled);
+                    ok = Self::check_diags(out, &env);
+                    out.push_str(&disassemble_compiled_units(&units)?);
+                    if ok {
+                        let annotated_units = annotate_units(units);
+                        run_bytecode_verifier(&annotated_units, &mut env);
+                        Self::check_diags(out, &env);
                     }
                 }
             }
@@ -450,11 +456,6 @@ impl TestConfig {
         env.clear_diag();
         ok
     }
-
-    fn disassemble(view: BinaryIndexedView) -> anyhow::Result<String> {
-        let diss = Disassembler::from_view(view, location::Loc::new(FileHash::empty(), 0, 0))?;
-        diss.disassemble()
-    }
 }
 
 datatest_stable::harness!(test_runner, "tests", r".*\.move$");
diff --git a/third_party/move/move-model/src/lib.rs b/third_party/move/move-model/src/lib.rs
index ad37b73f6c278..fbca4039901dc 100644
--- a/third_party/move/move-model/src/lib.rs
+++ b/third_party/move/move-model/src/lib.rs
@@ -496,7 +496,7 @@ fn collect_related_modules_recursive<'a>(
     }
 }
 
-fn add_move_lang_diagnostics(env: &mut GlobalEnv, diags: Diagnostics) {
+pub fn add_move_lang_diagnostics(env: &mut GlobalEnv, diags: Diagnostics) {
     let mk_label = |is_primary: bool, (loc, msg): (move_ir_types::location::Loc, String)| {
         let style = if is_primary {
             LabelStyle::Primary