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

Module acquires_list_verifier.
  (* StructRecord
    {
      name := "AcquiresVerifier";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("current_function", Ty.path "move_binary_format::file_format::FunctionDefinitionIndex");
          ("annotated_acquires",
            Ty.apply
              (Ty.path "alloc::collections::btree::set::BTreeSet")
              []
              [
                Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                Ty.path "alloc::alloc::Global"
              ]);
          ("actual_acquires",
            Ty.apply
              (Ty.path "alloc::collections::btree::set::BTreeSet")
              []
              [
                Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                Ty.path "alloc::alloc::Global"
              ]);
          ("handle_to_def",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                Ty.apply
                  (Ty.path "&")
                  []
                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ];
                Ty.path "std::hash::random::RandomState"
              ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_acquires_list_verifier_AcquiresVerifier.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier".
    
    (*
        pub(crate) fn verify(
            module: &'a CompiledModule,
            index: FunctionDefinitionIndex,
            function_definition: &'a FunctionDefinition,
            _meter: &mut (impl Meter + ?Sized), // currently unused
        ) -> PartialVMResult<()> {
            let annotated_acquires: BTreeSet<_> = function_definition
                .acquires_global_resources
                .iter()
                .cloned()
                .collect();
            let mut handle_to_def = HashMap::new();
            for func_def in module.function_defs() {
                handle_to_def.insert(func_def.function, func_def);
            }
            let mut verifier = Self {
                module,
                current_function: index,
                annotated_acquires,
                actual_acquires: BTreeSet::new(),
                handle_to_def,
            };
    
            for (offset, instruction) in safe_unwrap!(function_definition.code.as_ref())
                .code
                .iter()
                .enumerate()
            {
                verifier.verify_instruction(instruction, offset as CodeOffset)?
            }
    
            for annotation in verifier.annotated_acquires {
                if !verifier.actual_acquires.contains(&annotation) {
                    return Err(PartialVMError::new(
                        StatusCode::EXTRANEOUS_ACQUIRES_ANNOTATION,
                    ));
                }
    
                let struct_def = safe_unwrap!(module.struct_defs().get(annotation.0 as usize));
                let struct_handle = module.struct_handle_at(struct_def.struct_handle);
                if !struct_handle.abilities.has_key() {
                    return Err(PartialVMError::new(StatusCode::INVALID_ACQUIRES_ANNOTATION));
                }
            }
    
            Ok(())
        }
    *)
    Definition verify (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Meter__plus___Sized ], [ module; index; function_definition; _meter ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          let index := M.alloc (| index |) in
          let function_definition := M.alloc (| function_definition |) in
          let _meter := M.alloc (| _meter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ annotated_acquires :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::cloned::Cloned")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::StructDefinitionIndex" ]
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "alloc::collections::btree::set::BTreeSet")
                            []
                            [
                              Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        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::StructDefinitionIndex" ],
                            [],
                            "cloned",
                            [ Ty.path "move_binary_format::file_format::StructDefinitionIndex" ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::StructDefinitionIndex"
                                  ],
                                "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::StructDefinitionIndex";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| function_definition |),
                                      "move_binary_format::file_format::FunctionDefinition",
                                      "acquires_global_resources"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ handle_to_def :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "new",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ],
                            [],
                            "into_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::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 func_def := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "std::collections::hash::map::HashMap")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_binary_format::file_format::FunctionHandleIndex";
                                                      Ty.apply
                                                        (Ty.path "&")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::FunctionDefinition"
                                                        ];
                                                      Ty.path "std::hash::random::RandomState"
                                                    ],
                                                  "insert",
                                                  []
                                                |),
                                                [
                                                  handle_to_def;
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| func_def |),
                                                      "move_binary_format::file_format::FunctionDefinition",
                                                      "function"
                                                    |)
                                                  |);
                                                  M.read (| func_def |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ verifier :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier"
                      [
                        ("module", M.read (| module |));
                        ("current_function", M.read (| index |));
                        ("annotated_acquires", M.read (| annotated_acquires |));
                        ("actual_acquires",
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::set::BTreeSet")
                                []
                                [
                                  Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            []
                          |));
                        ("handle_to_def", M.read (| handle_to_def |))
                      ]
                  |) in
                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 (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [
                                                        Ty.path
                                                          "move_binary_format::file_format::CodeUnit"
                                                      ],
                                                    "as_ref",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| function_definition |),
                                                      "move_binary_format::file_format::FunctionDefinition",
                                                      "code"
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let x := M.copy (| γ0_0 |) in
                                                    x));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::option::Option::None"
                                                      |) in
                                                    let~ err :=
                                                      M.alloc (|
                                                        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",
                                                                "new",
                                                                []
                                                              |),
                                                              [
                                                                Value.StructTuple
                                                                  "move_core_types::vm_status::StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR"
                                                                  []
                                                              ]
                                                            |);
                                                            M.call_closure (|
                                                              M.get_function (|
                                                                "core::hint::must_use",
                                                                [ Ty.path "alloc::string::String" ]
                                                              |),
                                                              [
                                                                M.read (|
                                                                  let~ res :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "alloc::fmt::format",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "core::fmt::Arguments",
                                                                              "new_v1",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.alloc (|
                                                                                Value.Array
                                                                                  [
                                                                                    M.read (|
                                                                                      Value.String
                                                                                        "crates/move-bytecode-verifier/src/acquires_list_verifier.rs:59 (none)"
                                                                                    |)
                                                                                  ]
                                                                              |);
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "core::fmt::rt::Argument",
                                                                                    "none",
                                                                                    []
                                                                                  |),
                                                                                  []
                                                                                |)
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  res
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (| Value.Bool true |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::panicking::panic_fmt",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::fmt::Arguments",
                                                                        "new_v1",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.alloc (|
                                                                          Value.Array
                                                                            [
                                                                              M.read (|
                                                                                Value.String ""
                                                                              |)
                                                                            ]
                                                                        |);
                                                                        M.alloc (|
                                                                          Value.Array
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.path
                                                                                    "core::fmt::rt::Argument",
                                                                                  "new_debug",
                                                                                  [
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                  ]
                                                                                |),
                                                                                [ err ]
                                                                              |)
                                                                            ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    Value.StructTuple
                                                                      "core::result::Result::Err"
                                                                      [ M.read (| err |) ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                              ]
                                            |)
                                          |),
                                          "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 instruction := M.copy (| γ1_1 |) 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::acquires_list_verifier::AcquiresVerifier",
                                                      "verify_instruction",
                                                      []
                                                    |),
                                                    [
                                                      verifier;
                                                      M.read (| instruction |);
                                                      M.rust_cast (M.read (| offset |))
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              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
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "alloc::collections::btree::set::BTreeSet")
                              []
                              [
                                Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                verifier,
                                "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                "annotated_acquires"
                              |)
                            |)
                          ]
                        |)
                      |),
                      [
                        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 "alloc::collections::btree::set::IntoIter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::StructDefinitionIndex";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "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 annotation := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          UnOp.not (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloc::collections::btree::set::BTreeSet")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::StructDefinitionIndex";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                "contains",
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::file_format::StructDefinitionIndex"
                                                                ]
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  verifier,
                                                                  "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                                                  "actual_acquires"
                                                                |);
                                                                annotation
                                                              ]
                                                            |)
                                                          |)
                                                        |)) 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",
                                                                    "new",
                                                                    []
                                                                  |),
                                                                  [
                                                                    Value.StructTuple
                                                                      "move_core_types::vm_status::StatusCode::EXTRANEOUS_ACQUIRES_ANNOTATION"
                                                                      []
                                                                  ]
                                                                |)
                                                              ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          let~ struct_def :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::StructDefinition"
                                                        ],
                                                      "get",
                                                      [ Ty.path "usize" ]
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "struct_defs",
                                                          []
                                                        |),
                                                        [ M.read (| module |) ]
                                                      |);
                                                      M.rust_cast
                                                        (M.read (|
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            annotation,
                                                            "move_binary_format::file_format::StructDefinitionIndex",
                                                            0
                                                          |)
                                                        |))
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::option::Option::Some",
                                                          0
                                                        |) in
                                                      let x := M.copy (| γ0_0 |) in
                                                      x));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::option::Option::None"
                                                        |) in
                                                      let~ err :=
                                                        M.alloc (|
                                                          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",
                                                                  "new",
                                                                  []
                                                                |),
                                                                [
                                                                  Value.StructTuple
                                                                    "move_core_types::vm_status::StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR"
                                                                    []
                                                                ]
                                                              |);
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::hint::must_use",
                                                                  [ Ty.path "alloc::string::String"
                                                                  ]
                                                                |),
                                                                [
                                                                  M.read (|
                                                                    let~ res :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_function (|
                                                                            "alloc::fmt::format",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::Arguments",
                                                                                "new_v1",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.alloc (|
                                                                                  Value.Array
                                                                                    [
                                                                                      M.read (|
                                                                                        Value.String
                                                                                          "crates/move-bytecode-verifier/src/acquires_list_verifier.rs:74 (none)"
                                                                                      |)
                                                                                    ]
                                                                                |);
                                                                                M.alloc (|
                                                                                  M.call_closure (|
                                                                                    M.get_associated_function (|
                                                                                      Ty.path
                                                                                        "core::fmt::rt::Argument",
                                                                                      "none",
                                                                                      []
                                                                                    |),
                                                                                    []
                                                                                  |)
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |) in
                                                                    res
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (| Value.Bool true |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::panic_fmt",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "core::fmt::Arguments",
                                                                          "new_v1",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.alloc (|
                                                                            Value.Array
                                                                              [
                                                                                M.read (|
                                                                                  Value.String ""
                                                                                |)
                                                                              ]
                                                                          |);
                                                                          M.alloc (|
                                                                            Value.Array
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "core::fmt::rt::Argument",
                                                                                    "new_debug",
                                                                                    [
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError"
                                                                                    ]
                                                                                  |),
                                                                                  [ err ]
                                                                                |)
                                                                              ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    M.return_ (|
                                                                      Value.StructTuple
                                                                        "core::result::Result::Err"
                                                                        [ M.read (| err |) ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)))
                                                        ]
                                                      |)))
                                                ]
                                              |)
                                            |) 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 (| module |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| struct_def |),
                                                      "move_binary_format::file_format::StructDefinition",
                                                      "struct_handle"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::AbilitySet",
                                                              "has_key",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| struct_handle |),
                                                                  "move_binary_format::file_format::StructHandle",
                                                                  "abilities"
                                                                |)
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) 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",
                                                                  "new",
                                                                  []
                                                                |),
                                                                [
                                                                  Value.StructTuple
                                                                    "move_core_types::vm_status::StatusCode::INVALID_ACQUIRES_ANNOTATION"
                                                                    []
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) 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 : M.IsAssociatedFunction Self "verify" verify.
    
    (*
        fn verify_instruction(
            &mut self,
            instruction: &Bytecode,
            offset: CodeOffset,
        ) -> PartialVMResult<()> {
            match instruction {
                Bytecode::Call(idx) => self.call_acquire( *idx, offset),
                Bytecode::CallGeneric(idx) => {
                    let fi = self.module.function_instantiation_at( *idx);
                    self.call_acquire(fi.handle, offset)
                }
                Bytecode::MoveFromDeprecated(idx)
                | Bytecode::MutBorrowGlobalDeprecated(idx)
                | Bytecode::ImmBorrowGlobalDeprecated(idx) => self.struct_acquire( *idx, offset),
                Bytecode::MoveFromGenericDeprecated(idx)
                | Bytecode::MutBorrowGlobalGenericDeprecated(idx)
                | Bytecode::ImmBorrowGlobalGenericDeprecated(idx) => {
                    let si = self.module.struct_instantiation_at( *idx);
                    self.struct_acquire(si.def, offset)
                }
    
                Bytecode::Pop
                | Bytecode::BrTrue(_)
                | Bytecode::BrFalse(_)
                | Bytecode::Abort
                | Bytecode::Branch(_)
                | Bytecode::Nop
                | Bytecode::Ret
                | Bytecode::StLoc(_)
                | Bytecode::MoveLoc(_)
                | Bytecode::CopyLoc(_)
                | Bytecode::ImmBorrowLoc(_)
                | Bytecode::MutBorrowLoc(_)
                | Bytecode::FreezeRef
                | Bytecode::MutBorrowField(_)
                | Bytecode::MutBorrowFieldGeneric(_)
                | Bytecode::ImmBorrowField(_)
                | Bytecode::ImmBorrowFieldGeneric(_)
                | Bytecode::LdU8(_)
                | Bytecode::LdU16(_)
                | Bytecode::LdU32(_)
                | Bytecode::LdU64(_)
                | Bytecode::LdU128(_)
                | Bytecode::LdU256(_)
                | Bytecode::LdConst(_)
                | Bytecode::LdTrue
                | Bytecode::LdFalse
                | Bytecode::Pack(_)
                | Bytecode::PackGeneric(_)
                | Bytecode::Unpack(_)
                | Bytecode::UnpackGeneric(_)
                | Bytecode::ReadRef
                | Bytecode::WriteRef
                | Bytecode::CastU8
                | Bytecode::CastU16
                | Bytecode::CastU32
                | Bytecode::CastU64
                | Bytecode::CastU128
                | Bytecode::CastU256
                | Bytecode::Add
                | Bytecode::Sub
                | Bytecode::Mul
                | Bytecode::Mod
                | Bytecode::Div
                | Bytecode::BitOr
                | Bytecode::BitAnd
                | Bytecode::Xor
                | Bytecode::Shl
                | Bytecode::Shr
                | Bytecode::Or
                | Bytecode::And
                | Bytecode::Not
                | Bytecode::Eq
                | Bytecode::Neq
                | Bytecode::Lt
                | Bytecode::Gt
                | Bytecode::Le
                | Bytecode::Ge
                | Bytecode::ExistsDeprecated(_)
                | Bytecode::ExistsGenericDeprecated(_)
                | Bytecode::MoveToDeprecated(_)
                | Bytecode::MoveToGenericDeprecated(_)
                | Bytecode::VecPack(..)
                | Bytecode::VecLen(_)
                | Bytecode::VecImmBorrow(_)
                | Bytecode::VecMutBorrow(_)
                | Bytecode::VecPushBack(_)
                | Bytecode::VecPopBack(_)
                | Bytecode::VecUnpack(..)
                | Bytecode::VecSwap(_) => Ok(()),
            }
        }
    *)
    Definition verify_instruction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; instruction; offset ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let instruction := M.alloc (| instruction |) in
          let offset := M.alloc (| offset |) in
          M.read (|
            M.match_operator (|
              instruction,
              [
                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
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path
                            "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                          "call_acquire",
                          []
                        |),
                        [ M.read (| self |); M.read (| M.read (| idx |) |); M.read (| offset |) ]
                      |)
                    |)));
                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~ fi :=
                      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::acquires_list_verifier::AcquiresVerifier",
                                "module"
                              |)
                            |);
                            M.read (| M.read (| idx |) |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path
                            "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                          "call_acquire",
                          []
                        |),
                        [
                          M.read (| self |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| fi |),
                              "move_binary_format::file_format::FunctionInstantiation",
                              "handle"
                            |)
                          |);
                          M.read (| offset |)
                        ]
                      |)
                    |)));
                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::MoveFromDeprecated",
                                0
                              |) in
                            let idx := M.alloc (| γ1_0 |) in
                            Value.Tuple [ idx ]));
                        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
                            Value.Tuple [ idx ]));
                        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
                            Value.Tuple [ idx ]))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ idx ] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path
                                        "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                      "struct_acquire",
                                      []
                                    |),
                                    [
                                      M.read (| self |);
                                      M.read (| M.read (| idx |) |);
                                      M.read (| offset |)
                                    ]
                                  |)
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                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::MoveFromGenericDeprecated",
                                0
                              |) in
                            let idx := M.alloc (| γ1_0 |) in
                            Value.Tuple [ idx ]));
                        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
                            Value.Tuple [ idx ]));
                        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
                            Value.Tuple [ idx ]))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ idx ] =>
                              ltac:(M.monadic
                                (let~ si :=
                                  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::acquires_list_verifier::AcquiresVerifier",
                                            "module"
                                          |)
                                        |);
                                        M.read (| M.read (| idx |) |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path
                                        "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                      "struct_acquire",
                                      []
                                    |),
                                    [
                                      M.read (| self |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| si |),
                                          "move_binary_format::file_format::StructDefInstantiation",
                                          "def"
                                        |)
                                      |);
                                      M.read (| offset |)
                                    ]
                                  |)
                                |)))
                            | _ => 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::Pop"
                              |) 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 _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::Bytecode::Abort"
                              |) 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 _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::Bytecode::Nop"
                              |) 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::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::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::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::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::MutBorrowLoc",
                                0
                              |) in
                            Value.Tuple []));
                        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 γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::Bytecode::MutBorrowField",
                                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::MutBorrowFieldGeneric",
                                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::ImmBorrowField",
                                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::ImmBorrowFieldGeneric",
                                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::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 γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::Bytecode::Pack",
                                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::PackGeneric",
                                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::Unpack",
                                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::UnpackGeneric",
                                0
                              |) 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::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::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::ExistsDeprecated",
                                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::ExistsGenericDeprecated",
                                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::MoveToDeprecated",
                                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::MoveToGenericDeprecated",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::Bytecode::VecPack"
                              |) 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 _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::Bytecode::VecUnpack"
                              |) 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 []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_instruction :
      M.IsAssociatedFunction Self "verify_instruction" verify_instruction.
    
    (*
        fn call_acquire(
            &mut self,
            fh_idx: FunctionHandleIndex,
            offset: CodeOffset,
        ) -> PartialVMResult<()> {
            let function_handle = self.module.function_handle_at(fh_idx);
            let mut function_acquired_resources =
                self.function_acquired_resources(function_handle, fh_idx);
            for acquired_resource in &function_acquired_resources {
                if !self.annotated_acquires.contains(acquired_resource) {
                    return Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset));
                }
            }
            self.actual_acquires
                .append(&mut function_acquired_resources);
            Ok(())
        }
    *)
    Definition call_acquire (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; fh_idx; offset ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fh_idx := M.alloc (| fh_idx |) in
          let offset := M.alloc (| offset |) 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::acquires_list_verifier::AcquiresVerifier",
                            "module"
                          |)
                        |);
                        M.read (| fh_idx |)
                      ]
                    |)
                  |) in
                let~ function_acquired_resources :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                        "function_acquired_resources",
                        []
                      |),
                      [ M.read (| self |); M.read (| function_handle |); M.read (| fh_idx |) ]
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::set::BTreeSet")
                                  []
                                  [
                                    Ty.path
                                      "move_binary_format::file_format::StructDefinitionIndex";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ function_acquired_resources ]
                        |)
                      |),
                      [
                        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 "alloc::collections::btree::set::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::StructDefinitionIndex"
                                            ],
                                          [],
                                          "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 acquired_resource := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloc::collections::btree::set::BTreeSet")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::file_format::StructDefinitionIndex";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              "contains",
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::StructDefinitionIndex"
                                                              ]
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                                                "annotated_acquires"
                                                              |);
                                                              M.read (| acquired_resource |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) 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_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                                                  "error",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| self |);
                                                                  Value.StructTuple
                                                                    "move_core_types::vm_status::StatusCode::MISSING_ACQUIRES_ANNOTATION"
                                                                    [];
                                                                  M.read (| offset |)
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::set::BTreeSet")
                          []
                          [
                            Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "append",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                          "actual_acquires"
                        |);
                        function_acquired_resources
                      ]
                    |)
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_call_acquire : M.IsAssociatedFunction Self "call_acquire" call_acquire.
    
    (*
        fn struct_acquire(
            &mut self,
            sd_idx: StructDefinitionIndex,
            offset: CodeOffset,
        ) -> PartialVMResult<()> {
            if self.annotated_acquires.contains(&sd_idx) {
                self.actual_acquires.insert(sd_idx);
                Ok(())
            } else {
                Err(self.error(StatusCode::MISSING_ACQUIRES_ANNOTATION, offset))
            }
        }
    *)
    Definition struct_acquire (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; sd_idx; offset ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let sd_idx := M.alloc (| sd_idx |) in
          let offset := M.alloc (| offset |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::set::BTreeSet")
                                []
                                [
                                  Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "contains",
                              [ Ty.path "move_binary_format::file_format::StructDefinitionIndex" ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                "annotated_acquires"
                              |);
                              sd_idx
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::set::BTreeSet")
                              []
                              [
                                Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                                Ty.path "alloc::alloc::Global"
                              ],
                            "insert",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                              "actual_acquires"
                            |);
                            M.read (| sd_idx |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                              "error",
                              []
                            |),
                            [
                              M.read (| self |);
                              Value.StructTuple
                                "move_core_types::vm_status::StatusCode::MISSING_ACQUIRES_ANNOTATION"
                                [];
                              M.read (| offset |)
                            ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_struct_acquire :
      M.IsAssociatedFunction Self "struct_acquire" struct_acquire.
    
    (*
        fn function_acquired_resources(
            &self,
            function_handle: &FunctionHandle,
            fh_idx: FunctionHandleIndex,
        ) -> BTreeSet<StructDefinitionIndex> {
            if function_handle.module != self.module.self_handle_idx() {
                return BTreeSet::new();
            }
            match self.handle_to_def.get(&fh_idx) {
                Some(func_def) => func_def.acquires_global_resources.iter().cloned().collect(),
                None => BTreeSet::new(),
            }
        }
    *)
    Definition function_acquired_resources
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; function_handle; fh_idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let function_handle := M.alloc (| function_handle |) in
          let fh_idx := M.alloc (| fh_idx |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "move_binary_format::file_format::ModuleHandleIndex",
                                    [ Ty.path "move_binary_format::file_format::ModuleHandleIndex"
                                    ],
                                    "ne",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| function_handle |),
                                      "move_binary_format::file_format::FunctionHandle",
                                      "module"
                                    |);
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::CompiledModule",
                                          "self_handle_idx",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                                              "module"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::set::BTreeSet")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::StructDefinitionIndex";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    []
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "get",
                        [ Ty.path "move_binary_format::file_format::FunctionHandleIndex" ]
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                          "handle_to_def"
                        |);
                        fh_idx
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let func_def := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::cloned::Cloned")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [
                                      Ty.path
                                        "move_binary_format::file_format::StructDefinitionIndex"
                                    ]
                                ],
                              [],
                              "collect",
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::set::BTreeSet")
                                  []
                                  [
                                    Ty.path
                                      "move_binary_format::file_format::StructDefinitionIndex";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                            |),
                            [
                              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::StructDefinitionIndex"
                                    ],
                                  [],
                                  "cloned",
                                  [ Ty.path "move_binary_format::file_format::StructDefinitionIndex"
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::StructDefinitionIndex"
                                        ],
                                      "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::StructDefinitionIndex";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| M.read (| func_def |) |),
                                            "move_binary_format::file_format::FunctionDefinition",
                                            "acquires_global_resources"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::set::BTreeSet")
                                []
                                [
                                  Ty.path "move_binary_format::file_format::StructDefinitionIndex";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            []
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_function_acquired_resources :
      M.IsAssociatedFunction Self "function_acquired_resources" function_acquired_resources.
    
    (*
        fn error(&self, status: StatusCode, offset: CodeOffset) -> PartialVMError {
            PartialVMError::new(status).at_code_offset(self.current_function, offset)
        }
    *)
    Definition error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; status; offset ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let status := M.alloc (| status |) in
          let offset := M.alloc (| offset |) in
          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",
                  []
                |),
                [ M.read (| status |) ]
              |);
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                  "current_function"
                |)
              |);
              M.read (| offset |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_error : M.IsAssociatedFunction Self "error" error.
  End Impl_move_bytecode_verifier_acquires_list_verifier_AcquiresVerifier.
End acquires_list_verifier.
