(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module instruction_consistency.
  (* StructRecord
    {
      name := "InstructionConsistency";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("current_function",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_instruction_consistency_InstructionConsistency.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::instruction_consistency::InstructionConsistency".
    
    (*
        pub fn verify_module(module: &'a CompiledModule) -> VMResult<()> {
            Self::verify_module_impl(module).map_err(|e| e.finish(Location::Module(module.self_id())))
        }
    *)
    Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
              "map_err",
              [
                Ty.path "move_binary_format::errors::VMError";
                Ty.function
                  [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ] ]
                  (Ty.path "move_binary_format::errors::VMError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                  "verify_module_impl",
                  []
                |),
                [ M.read (| module |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let e := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::errors::PartialVMError",
                                    "finish",
                                    []
                                  |),
                                  [
                                    M.read (| e |);
                                    Value.StructTuple
                                      "move_binary_format::errors::Location::Module"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "self_id",
                                            []
                                          |),
                                          [ M.read (| module |) ]
                                        |)
                                      ]
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module :
      M.IsAssociatedFunction Self "verify_module" verify_module.
    
    (*
        fn verify_module_impl(module: &'a CompiledModule) -> PartialVMResult<()> {
            for (idx, func_def) in module.function_defs().iter().enumerate() {
                match &func_def.code {
                    None => (),
                    Some(code) => {
                        let checker = Self {
                            module,
                            current_function: Some(FunctionDefinitionIndex(idx as TableIndex)),
                        };
                        checker.check_instructions(code)?
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_module_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_defs",
                                        []
                                      |),
                                      [ M.read (| module |) ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let idx := M.copy (| γ1_0 |) in
                                          let func_def := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| func_def |),
                                                "move_binary_format::file_format::FunctionDefinition",
                                                "code"
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let code := M.alloc (| γ1_0 |) in
                                                  let~ checker :=
                                                    M.alloc (|
                                                      Value.StructRecord
                                                        "move_bytecode_verifier::instruction_consistency::InstructionConsistency"
                                                        [
                                                          ("module", M.read (| module |));
                                                          ("current_function",
                                                            Value.StructTuple
                                                              "core::option::Option::Some"
                                                              [
                                                                Value.StructTuple
                                                                  "move_binary_format::file_format::FunctionDefinitionIndex"
                                                                  [ M.rust_cast (M.read (| idx |)) ]
                                                              ])
                                                        ]
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::try_trait::Try",
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.tuple [];
                                                              Ty.path
                                                                "move_binary_format::errors::PartialVMError"
                                                            ],
                                                          [],
                                                          "branch",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "check_instructions",
                                                              []
                                                            |),
                                                            [ checker; M.read (| code |) ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Break",
                                                              0
                                                            |) in
                                                          let residual := M.copy (| γ0_0 |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::try_trait::FromResidual",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        []
                                                                        [
                                                                          Ty.tuple [];
                                                                          Ty.path
                                                                            "move_binary_format::errors::PartialVMError"
                                                                        ],
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "core::convert::Infallible";
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ]
                                                                      ],
                                                                      "from_residual",
                                                                      []
                                                                    |),
                                                                    [ M.read (| residual |) ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                              0
                                                            |) in
                                                          let val := M.copy (| γ0_0 |) in
                                                          val))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn check_instructions(&self, code: &CodeUnit) -> PartialVMResult<()> {
            for (offset, instr) in code.code.iter().enumerate() {
                use Bytecode::*;
    
                match instr {
                    MutBorrowField(field_handle_index) => {
                        self.check_field_op(offset, *field_handle_index, /* generic */ false)?;
                    }
                    MutBorrowFieldGeneric(field_inst_index) => {
                        let field_inst = self.module.field_instantiation_at( *field_inst_index);
                        self.check_field_op(offset, field_inst.handle, /* generic */ true)?;
                    }
                    ImmBorrowField(field_handle_index) => {
                        self.check_field_op(offset, *field_handle_index, /* generic */ false)?;
                    }
                    ImmBorrowFieldGeneric(field_inst_index) => {
                        let field_inst = self.module.field_instantiation_at( *field_inst_index);
                        self.check_field_op(offset, field_inst.handle, /* non_ */ true)?;
                    }
                    Call(idx) => {
                        self.check_function_op(offset, *idx, /* generic */ false)?;
                    }
                    CallGeneric(idx) => {
                        let func_inst = self.module.function_instantiation_at( *idx);
                        self.check_function_op(offset, func_inst.handle, /* generic */ true)?;
                    }
                    Pack(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    PackGeneric(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    Unpack(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    UnpackGeneric(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    MutBorrowGlobalDeprecated(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    MutBorrowGlobalGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    ImmBorrowGlobalDeprecated(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    ImmBorrowGlobalGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    ExistsDeprecated(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    ExistsGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    MoveFromDeprecated(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    MoveFromGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    MoveToDeprecated(idx) => {
                        self.check_type_op(offset, *idx, /* generic */ false)?;
                    }
                    MoveToGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        self.check_type_op(offset, struct_inst.def, /* generic */ true)?;
                    }
                    VecPack(_, num) | VecUnpack(_, num) => {
                        if *num > u16::MAX as u64 {
                            return Err(PartialVMError::new(StatusCode::CONSTRAINT_NOT_SATISFIED)
                                .at_code_offset(self.current_function(), offset as CodeOffset)
                                .with_message("VecPack/VecUnpack argument out of range".to_string()));
                        }
                    }
    
                    // List out the other options explicitly so there's a compile error if a new
                    // bytecode gets added.
                    FreezeRef | Pop | Ret | Branch(_) | BrTrue(_) | BrFalse(_) | LdU8(_) | LdU16(_)
                    | LdU32(_) | LdU64(_) | LdU128(_) | LdU256(_) | LdConst(_) | CastU8 | CastU16
                    | CastU32 | CastU64 | CastU128 | CastU256 | LdTrue | LdFalse | ReadRef
                    | WriteRef | Add | Sub | Mul | Mod | Div | BitOr | BitAnd | Xor | Shl | Shr
                    | Or | And | Not | Eq | Neq | Lt | Gt | Le | Ge | CopyLoc(_) | MoveLoc(_)
                    | StLoc(_) | MutBorrowLoc(_) | ImmBorrowLoc(_) | VecLen(_) | VecImmBorrow(_)
                    | VecMutBorrow(_) | VecPushBack(_) | VecPopBack(_) | VecSwap(_) | Abort | Nop => (),
                }
            }
            Ok(())
        }
    *)
    Definition check_instructions (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; code ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let code := M.alloc (| code |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Bytecode" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "move_binary_format::file_format::Bytecode";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| code |),
                                          "move_binary_format::file_format::CodeUnit",
                                          "code"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::Bytecode"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let offset := M.copy (| γ1_0 |) in
                                          let instr := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            instr,
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MutBorrowField",
                                                      0
                                                    |) in
                                                  let field_handle_index := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_field_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.read (| field_handle_index |)
                                                                |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MutBorrowFieldGeneric",
                                                      0
                                                    |) in
                                                  let field_inst_index := M.alloc (| γ1_0 |) in
                                                  let~ field_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "field_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| field_inst_index |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_field_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| field_inst |),
                                                                    "move_binary_format::file_format::FieldInstantiation",
                                                                    "handle"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ImmBorrowField",
                                                      0
                                                    |) in
                                                  let field_handle_index := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_field_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.read (| field_handle_index |)
                                                                |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ImmBorrowFieldGeneric",
                                                      0
                                                    |) in
                                                  let field_inst_index := M.alloc (| γ1_0 |) in
                                                  let~ field_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "field_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| field_inst_index |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_field_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| field_inst |),
                                                                    "move_binary_format::file_format::FieldInstantiation",
                                                                    "handle"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::Call",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_function_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::CallGeneric",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ func_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "function_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_function_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| func_inst |),
                                                                    "move_binary_format::file_format::FunctionInstantiation",
                                                                    "handle"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::Pack",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::PackGeneric",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::Unpack",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::UnpackGeneric",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MutBorrowGlobalDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MutBorrowGlobalGenericDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ImmBorrowGlobalDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ImmBorrowGlobalGenericDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ExistsDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::ExistsGenericDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MoveFromDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MoveFromGenericDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MoveToDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (| M.read (| idx |) |);
                                                                Value.Bool false
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::Bytecode::MoveToGenericDeprecated",
                                                      0
                                                    |) in
                                                  let idx := M.alloc (| γ1_0 |) in
                                                  let~ struct_inst :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_instantiation_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| M.read (| idx |) |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::Try",
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.tuple [];
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                "check_type_op",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| offset |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| struct_inst |),
                                                                    "move_binary_format::file_format::StructDefInstantiation",
                                                                    "def"
                                                                  |)
                                                                |);
                                                                Value.Bool true
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                0
                                                              |) in
                                                            let residual := M.copy (| γ0_0 |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::ops::try_trait::FromResidual",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.tuple [];
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::convert::Infallible";
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ]
                                                                        ],
                                                                        "from_residual",
                                                                        []
                                                                      |),
                                                                      [ M.read (| residual |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                0
                                                              |) in
                                                            let val := M.copy (| γ0_0 |) in
                                                            val))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.find_or_pattern (|
                                                    γ,
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecPack",
                                                              0
                                                            |) in
                                                          let γ1_1 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecPack",
                                                              1
                                                            |) in
                                                          let num := M.alloc (| γ1_1 |) in
                                                          Value.Tuple [ num ]));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecUnpack",
                                                              0
                                                            |) in
                                                          let γ1_1 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecUnpack",
                                                              1
                                                            |) in
                                                          let num := M.alloc (| γ1_1 |) in
                                                          Value.Tuple [ num ]))
                                                    ],
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ num ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| Value.Tuple [] |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ :=
                                                                        M.use
                                                                          (M.alloc (|
                                                                            BinOp.gt (|
                                                                              M.read (|
                                                                                M.read (| num |)
                                                                              |),
                                                                              M.rust_cast
                                                                                (M.read (|
                                                                                  M.get_constant (|
                                                                                    "core::num::MAX"
                                                                                  |)
                                                                                |))
                                                                            |)
                                                                          |)) in
                                                                      let _ :=
                                                                        M.is_constant_or_break_match (|
                                                                          M.read (| γ |),
                                                                          Value.Bool true
                                                                        |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (|
                                                                            M.return_ (|
                                                                              Value.StructTuple
                                                                                "core::result::Result::Err"
                                                                                [
                                                                                  M.call_closure (|
                                                                                    M.get_associated_function (|
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError",
                                                                                      "with_message",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError",
                                                                                          "at_code_offset",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "move_binary_format::errors::PartialVMError",
                                                                                              "new",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              Value.StructTuple
                                                                                                "move_core_types::vm_status::StatusCode::CONSTRAINT_NOT_SATISFIED"
                                                                                                []
                                                                                            ]
                                                                                          |);
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                                                                              "current_function",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                self
                                                                                              |)
                                                                                            ]
                                                                                          |);
                                                                                          M.rust_cast
                                                                                            (M.read (|
                                                                                              offset
                                                                                            |))
                                                                                        ]
                                                                                      |);
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "alloc::string::ToString",
                                                                                          Ty.path
                                                                                            "str",
                                                                                          [],
                                                                                          "to_string",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.read (|
                                                                                            Value.String
                                                                                              "VecPack/VecUnpack argument out of range"
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                ]
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.Tuple []
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.find_or_pattern (|
                                                    γ,
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::FreezeRef"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Pop"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Ret"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Branch",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::BrTrue",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::BrFalse",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU8",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU16",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU32",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU64",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU128",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdU256",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdConst",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU8"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU16"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU32"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU64"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU128"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CastU256"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdTrue"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::LdFalse"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::ReadRef"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::WriteRef"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Add"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Sub"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Mul"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Mod"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Div"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::BitOr"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::BitAnd"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Xor"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Shl"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Shr"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Or"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::And"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Not"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Eq"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Neq"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Lt"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Gt"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Le"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Ge"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::CopyLoc",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::MoveLoc",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::StLoc",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::MutBorrowLoc",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::ImmBorrowLoc",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecLen",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecImmBorrow",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecMutBorrow",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecPushBack",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecPopBack",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::VecSwap",
                                                              0
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Abort"
                                                            |) in
                                                          Value.Tuple []));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::Bytecode::Nop"
                                                            |) in
                                                          Value.Tuple []))
                                                    ],
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [] =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_instructions :
      M.IsAssociatedFunction Self "check_instructions" check_instructions.
    
    (*
        fn check_field_op(
            &self,
            offset: usize,
            field_handle_index: FieldHandleIndex,
            generic: bool,
        ) -> PartialVMResult<()> {
            let field_handle = self.module.field_handle_at(field_handle_index);
            self.check_type_op(offset, field_handle.owner, generic)
        }
    *)
    Definition check_field_op (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; offset; field_handle_index; generic ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let offset := M.alloc (| offset |) in
          let field_handle_index := M.alloc (| field_handle_index |) in
          let generic := M.alloc (| generic |) in
          M.read (|
            let~ field_handle :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_binary_format::file_format::CompiledModule",
                    "field_handle_at",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                        "module"
                      |)
                    |);
                    M.read (| field_handle_index |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                  "check_type_op",
                  []
                |),
                [
                  M.read (| self |);
                  M.read (| offset |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| field_handle |),
                      "move_binary_format::file_format::FieldHandle",
                      "owner"
                    |)
                  |);
                  M.read (| generic |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_field_op :
      M.IsAssociatedFunction Self "check_field_op" check_field_op.
    
    (*
        fn current_function(&self) -> FunctionDefinitionIndex {
            self.current_function.unwrap_or(FunctionDefinitionIndex(0))
        }
    *)
    Definition current_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
              "unwrap_or",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                  "current_function"
                |)
              |);
              Value.StructTuple
                "move_binary_format::file_format::FunctionDefinitionIndex"
                [ Value.Integer IntegerKind.U16 0 ]
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_current_function :
      M.IsAssociatedFunction Self "current_function" current_function.
    
    (*
        fn check_type_op(
            &self,
            offset: usize,
            struct_def_index: StructDefinitionIndex,
            generic: bool,
        ) -> PartialVMResult<()> {
            let struct_def = self.module.struct_def_at(struct_def_index);
            let struct_handle = self.module.struct_handle_at(struct_def.struct_handle);
            if struct_handle.type_parameters.is_empty() == generic {
                return Err(
                    PartialVMError::new(StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH)
                        .at_code_offset(self.current_function(), offset as CodeOffset),
                );
            }
            Ok(())
        }
    *)
    Definition check_type_op (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; offset; struct_def_index; generic ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let offset := M.alloc (| offset |) in
          let struct_def_index := M.alloc (| struct_def_index |) in
          let generic := M.alloc (| generic |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ struct_def :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "struct_def_at",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                            "module"
                          |)
                        |);
                        M.read (| struct_def_index |)
                      ]
                    |)
                  |) in
                let~ struct_handle :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "struct_handle_at",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                            "module"
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| struct_def |),
                            "move_binary_format::file_format::StructDefinition",
                            "struct_handle"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.eq (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::StructTypeParameter";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "is_empty",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| struct_handle |),
                                        "move_binary_format::file_format::StructHandle",
                                        "type_parameters"
                                      |)
                                    ]
                                  |),
                                  M.read (| generic |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "at_code_offset",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "move_binary_format::errors::PartialVMError",
                                              "new",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "move_core_types::vm_status::StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH"
                                                []
                                            ]
                                          |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                              "current_function",
                                              []
                                            |),
                                            [ M.read (| self |) ]
                                          |);
                                          M.rust_cast (M.read (| offset |))
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_type_op :
      M.IsAssociatedFunction Self "check_type_op" check_type_op.
    
    (*
        fn check_function_op(
            &self,
            offset: usize,
            func_handle_index: FunctionHandleIndex,
            generic: bool,
        ) -> PartialVMResult<()> {
            let function_handle = self.module.function_handle_at(func_handle_index);
            if function_handle.type_parameters.is_empty() == generic {
                return Err(
                    PartialVMError::new(StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH)
                        .at_code_offset(self.current_function(), offset as CodeOffset),
                );
            }
            Ok(())
        }
    *)
    Definition check_function_op (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; offset; func_handle_index; generic ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let offset := M.alloc (| offset |) in
          let func_handle_index := M.alloc (| func_handle_index |) in
          let generic := M.alloc (| generic |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ function_handle :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "function_handle_at",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                            "module"
                          |)
                        |);
                        M.read (| func_handle_index |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.eq (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_binary_format::file_format::AbilitySet";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "is_empty",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| function_handle |),
                                        "move_binary_format::file_format::FunctionHandle",
                                        "type_parameters"
                                      |)
                                    ]
                                  |),
                                  M.read (| generic |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "at_code_offset",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "move_binary_format::errors::PartialVMError",
                                              "new",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "move_core_types::vm_status::StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH"
                                                []
                                            ]
                                          |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                                              "current_function",
                                              []
                                            |),
                                            [ M.read (| self |) ]
                                          |);
                                          M.rust_cast (M.read (| offset |))
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_function_op :
      M.IsAssociatedFunction Self "check_function_op" check_function_op.
  End Impl_move_bytecode_verifier_instruction_consistency_InstructionConsistency.
End instruction_consistency.
