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

Module code_unit_verifier.
  (* StructRecord
    {
      name := "CodeUnitVerifier";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("function_context", Ty.path "move_bytecode_verifier::absint::FunctionContext");
          ("name_def_map",
            Ty.apply
              (Ty.path "&")
              []
              [
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.path "move_binary_format::file_format::IdentifierIndex";
                    Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                    Ty.path "std::hash::random::RandomState"
                  ]
              ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_code_unit_verifier_CodeUnitVerifier.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier".
    
    (*
        pub fn verify_module(
            verifier_config: &VerifierConfig,
            module: &'a CompiledModule,
            meter: &mut (impl Meter + ?Sized),
        ) -> VMResult<()> {
            Self::verify_module_impl(verifier_config, module, meter)
                .map_err(|e| e.finish(Location::Module(module.self_id())))
        }
    *)
    Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Meter__plus___Sized ], [ verifier_config; module; meter ] =>
        ltac:(M.monadic
          (let verifier_config := M.alloc (| verifier_config |) in
          let module := M.alloc (| module |) in
          let meter := M.alloc (| meter |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
              "map_err",
              [
                Ty.path "move_binary_format::errors::VMError";
                Ty.function
                  [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ] ]
                  (Ty.path "move_binary_format::errors::VMError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                  "verify_module_impl",
                  [ impl_Meter__plus___Sized ]
                |),
                [ M.read (| verifier_config |); M.read (| module |); M.read (| meter |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let e := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::errors::PartialVMError",
                                    "finish",
                                    []
                                  |),
                                  [
                                    M.read (| e |);
                                    Value.StructTuple
                                      "move_binary_format::errors::Location::Module"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "self_id",
                                            []
                                          |),
                                          [ M.read (| module |) ]
                                        |)
                                      ]
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module :
      M.IsAssociatedFunction Self "verify_module" verify_module.
    
    (*
        fn verify_module_impl(
            verifier_config: &VerifierConfig,
            module: &CompiledModule,
            meter: &mut (impl Meter + ?Sized),
        ) -> PartialVMResult<()> {
            let mut name_def_map = HashMap::new();
            for (idx, func_def) in module.function_defs().iter().enumerate() {
                let fh = module.function_handle_at(func_def.function);
                name_def_map.insert(fh.name, FunctionDefinitionIndex(idx as u16));
            }
            let mut total_back_edges = 0;
            for (idx, function_definition) in module.function_defs().iter().enumerate() {
                let index = FunctionDefinitionIndex(idx as TableIndex);
                let num_back_edges = Self::verify_function(
                    verifier_config,
                    index,
                    function_definition,
                    module,
                    &name_def_map,
                    meter,
                )
                .map_err(|err| err.at_index(IndexKind::FunctionDefinition, index.0))?;
                total_back_edges += num_back_edges;
            }
            if let Some(limit) = verifier_config.max_back_edges_per_module {
                if total_back_edges > limit {
                    return Err(PartialVMError::new(StatusCode::TOO_MANY_BACK_EDGES));
                }
            }
            Ok(())
        }
    *)
    Definition verify_module_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Meter__plus___Sized ], [ verifier_config; module; meter ] =>
        ltac:(M.monadic
          (let verifier_config := M.alloc (| verifier_config |) in
          let module := M.alloc (| module |) in
          let meter := M.alloc (| meter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ name_def_map :=
                  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::IdentifierIndex";
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            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 "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_defs",
                                        []
                                      |),
                                      [ M.read (| module |) ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let idx := M.copy (| γ1_0 |) in
                                          let func_def := M.copy (| γ1_1 |) in
                                          let~ fh :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::CompiledModule",
                                                  "function_handle_at",
                                                  []
                                                |),
                                                [
                                                  M.read (| module |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| func_def |),
                                                      "move_binary_format::file_format::FunctionDefinition",
                                                      "function"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |) 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::IdentifierIndex";
                                                      Ty.path
                                                        "move_binary_format::file_format::FunctionDefinitionIndex";
                                                      Ty.path "std::hash::random::RandomState"
                                                    ],
                                                  "insert",
                                                  []
                                                |),
                                                [
                                                  name_def_map;
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| fh |),
                                                      "move_binary_format::file_format::FunctionHandle",
                                                      "name"
                                                    |)
                                                  |);
                                                  Value.StructTuple
                                                    "move_binary_format::file_format::FunctionDefinitionIndex"
                                                    [ M.rust_cast (M.read (| idx |)) ]
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ total_back_edges := M.alloc (| Value.Integer IntegerKind.Usize 0 |) 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::FunctionDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_defs",
                                        []
                                      |),
                                      [ M.read (| module |) ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let idx := M.copy (| γ1_0 |) in
                                          let function_definition := M.copy (| γ1_1 |) in
                                          let~ index :=
                                            M.alloc (|
                                              Value.StructTuple
                                                "move_binary_format::file_format::FunctionDefinitionIndex"
                                                [ M.rust_cast (M.read (| idx |)) ]
                                            |) in
                                          let~ num_back_edges :=
                                            M.copy (|
                                              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.path "usize";
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.path "usize";
                                                              Ty.path
                                                                "move_binary_format::errors::PartialVMError"
                                                            ],
                                                          "map_err",
                                                          [
                                                            Ty.path
                                                              "move_binary_format::errors::PartialVMError";
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ]
                                                              (Ty.path
                                                                "move_binary_format::errors::PartialVMError")
                                                          ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                                              "verify_function",
                                                              [ impl_Meter__plus___Sized ]
                                                            |),
                                                            [
                                                              M.read (| verifier_config |);
                                                              M.read (| index |);
                                                              M.read (| function_definition |);
                                                              M.read (| module |);
                                                              name_def_map;
                                                              M.read (| meter |)
                                                            ]
                                                          |);
                                                          M.closure
                                                            (fun γ =>
                                                              ltac:(M.monadic
                                                                match γ with
                                                                | [ α0 ] =>
                                                                  ltac:(M.monadic
                                                                    (M.match_operator (|
                                                                      M.alloc (| α0 |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let err :=
                                                                              M.copy (| γ |) in
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "at_index",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| err |);
                                                                                Value.StructTuple
                                                                                  "move_binary_format::IndexKind::FunctionDefinition"
                                                                                  [];
                                                                                M.read (|
                                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                                    index,
                                                                                    "move_binary_format::file_format::FunctionDefinitionIndex",
                                                                                    0
                                                                                  |)
                                                                                |)
                                                                              ]
                                                                            |)))
                                                                      ]
                                                                    |)))
                                                                | _ =>
                                                                  M.impossible
                                                                    "wrong number of arguments"
                                                                end))
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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
                                          let~ _ :=
                                            let β := total_back_edges in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.add (|
                                                M.read (| β |),
                                                M.read (| num_back_edges |)
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| verifier_config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_back_edges_per_module"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let limit := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| total_back_edges |),
                                          M.read (| limit |)
                                        |)
                                      |)) 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::TOO_MANY_BACK_EDGES"
                                                    []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn verify_function(
            verifier_config: &VerifierConfig,
            index: FunctionDefinitionIndex,
            function_definition: &FunctionDefinition,
            module: &CompiledModule,
            name_def_map: &HashMap<IdentifierIndex, FunctionDefinitionIndex>,
            meter: &mut (impl Meter + ?Sized),
        ) -> PartialVMResult<usize> {
            meter.enter_scope(
                module
                    .identifier_at(module.function_handle_at(function_definition.function).name)
                    .as_str(),
                Scope::Function,
            );
            // nothing to verify for native function
            let code = match &function_definition.code {
                Some(code) => code,
                None => return Ok(0),
            };
    
            // create `FunctionContext` and `BinaryIndexedView`
            let function_context = control_flow::verify_function(
                verifier_config,
                module,
                index,
                function_definition,
                code,
                meter,
            )?;
    
            if let Some(limit) = verifier_config.max_basic_blocks {
                if function_context.cfg().blocks().len() > limit {
                    return Err(
                        PartialVMError::new(StatusCode::TOO_MANY_BASIC_BLOCKS).at_code_offset(index, 0)
                    );
                }
            }
    
            let num_back_edges = function_context.cfg().num_back_edges();
            if let Some(limit) = verifier_config.max_back_edges_per_function {
                if num_back_edges > limit {
                    return Err(
                        PartialVMError::new(StatusCode::TOO_MANY_BACK_EDGES).at_code_offset(index, 0)
                    );
                }
            }
    
            // verify
            let code_unit_verifier = CodeUnitVerifier {
                module,
                function_context,
                name_def_map,
            };
            code_unit_verifier.verify_common(verifier_config, meter)?;
            AcquiresVerifier::verify(module, index, function_definition, meter)?;
    
            meter.transfer(Scope::Function, Scope::Module, 1.0)?;
    
            Ok(num_back_edges)
        }
    *)
    Definition verify_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [],
          [ impl_Meter__plus___Sized ],
          [ verifier_config; index; function_definition; module; name_def_map; meter ] =>
        ltac:(M.monadic
          (let verifier_config := M.alloc (| verifier_config |) in
          let index := M.alloc (| index |) in
          let function_definition := M.alloc (| function_definition |) in
          let module := M.alloc (| module |) in
          let name_def_map := M.alloc (| name_def_map |) in
          let meter := M.alloc (| meter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "move_bytecode_verifier_meter::Meter",
                        impl_Meter__plus___Sized,
                        [],
                        "enter_scope",
                        []
                      |),
                      [
                        M.read (| meter |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_core_types::identifier::IdentStr",
                            "as_str",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "identifier_at",
                                []
                              |),
                              [
                                M.read (| module |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_handle_at",
                                        []
                                      |),
                                      [
                                        M.read (| module |);
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| function_definition |),
                                            "move_binary_format::file_format::FunctionDefinition",
                                            "function"
                                          |)
                                        |)
                                      ]
                                    |),
                                    "move_binary_format::file_format::FunctionHandle",
                                    "name"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |);
                        Value.StructTuple "move_bytecode_verifier_meter::Scope::Function" []
                      ]
                    |)
                  |) in
                let~ code :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| function_definition |),
                          "move_binary_format::file_format::FunctionDefinition",
                          "code"
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let code := M.alloc (| γ1_0 |) in
                            code));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Ok"
                                      [ Value.Integer IntegerKind.Usize 0 ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ function_context :=
                  M.copy (|
                    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.path "move_bytecode_verifier::absint::FunctionContext";
                                Ty.path "move_binary_format::errors::PartialVMError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (|
                                "move_bytecode_verifier::control_flow::verify_function",
                                [ impl_Meter__plus___Sized ]
                              |),
                              [
                                M.read (| verifier_config |);
                                M.read (| module |);
                                M.read (| index |);
                                M.read (| function_definition |);
                                M.read (| code |);
                                M.read (| meter |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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.path "usize";
                                            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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| verifier_config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_basic_blocks"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let limit := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "move_binary_format::control_flow_graph::ControlFlowGraph",
                                                    Ty.path
                                                      "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                                    [],
                                                    "blocks",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_bytecode_verifier::absint::FunctionContext",
                                                        "cfg",
                                                        []
                                                      |),
                                                      [ function_context ]
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            ]
                                          |),
                                          M.read (| limit |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "at_code_offset",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError",
                                                      "new",
                                                      []
                                                    |),
                                                    [
                                                      Value.StructTuple
                                                        "move_core_types::vm_status::StatusCode::TOO_MANY_BASIC_BLOCKS"
                                                        []
                                                    ]
                                                  |);
                                                  M.read (| index |);
                                                  Value.Integer IntegerKind.U16 0
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ num_back_edges :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "move_binary_format::control_flow_graph::ControlFlowGraph",
                        Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
                        [],
                        "num_back_edges",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_bytecode_verifier::absint::FunctionContext",
                            "cfg",
                            []
                          |),
                          [ function_context ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| verifier_config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_back_edges_per_function"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let limit := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| num_back_edges |),
                                          M.read (| limit |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "at_code_offset",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError",
                                                      "new",
                                                      []
                                                    |),
                                                    [
                                                      Value.StructTuple
                                                        "move_core_types::vm_status::StatusCode::TOO_MANY_BACK_EDGES"
                                                        []
                                                    ]
                                                  |);
                                                  M.read (| index |);
                                                  Value.Integer IntegerKind.U16 0
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ code_unit_verifier :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier"
                      [
                        ("module", M.read (| module |));
                        ("function_context", M.read (| function_context |));
                        ("name_def_map", M.read (| name_def_map |))
                      ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                              "verify_common",
                              [ impl_Meter__plus___Sized ]
                            |),
                            [ code_unit_verifier; M.read (| verifier_config |); M.read (| meter |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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.path "usize";
                                          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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "move_bytecode_verifier::acquires_list_verifier::AcquiresVerifier",
                              "verify",
                              [ impl_Meter__plus___Sized ]
                            |),
                            [
                              M.read (| module |);
                              M.read (| index |);
                              M.read (| function_definition |);
                              M.read (| meter |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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.path "usize";
                                          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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "move_bytecode_verifier_meter::Meter",
                              impl_Meter__plus___Sized,
                              [],
                              "transfer",
                              []
                            |),
                            [
                              M.read (| meter |);
                              Value.StructTuple "move_bytecode_verifier_meter::Scope::Function" [];
                              Value.StructTuple "move_bytecode_verifier_meter::Scope::Module" [];
                              M.read (| UnsupportedLiteral |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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.path "usize";
                                          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.StructTuple "core::result::Result::Ok" [ M.read (| num_back_edges |) ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_function :
      M.IsAssociatedFunction Self "verify_function" verify_function.
    
    (*
        fn verify_common(
            &self,
            verifier_config: &VerifierConfig,
            meter: &mut (impl Meter + ?Sized),
        ) -> PartialVMResult<()> {
            StackUsageVerifier::verify(verifier_config, self.module, &self.function_context, meter)?;
            type_safety::verify(self.module, &self.function_context, meter)?;
            locals_safety::verify(self.module, &self.function_context, meter)?;
            reference_safety::verify(
                self.module,
                &self.function_context,
                self.name_def_map,
                meter,
            )
        }
    *)
    Definition verify_common (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Meter__plus___Sized ], [ self; verifier_config; meter ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let verifier_config := M.alloc (| verifier_config |) in
          let meter := M.alloc (| meter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                              "verify",
                              [ impl_Meter__plus___Sized ]
                            |),
                            [
                              M.read (| verifier_config |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                  "module"
                                |)
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                "function_context"
                              |);
                              M.read (| meter |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "move_bytecode_verifier::type_safety::verify",
                              [ impl_Meter__plus___Sized ]
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                  "module"
                                |)
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                "function_context"
                              |);
                              M.read (| meter |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "move_bytecode_verifier::locals_safety::verify",
                              [ impl_Meter__plus___Sized ]
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                  "module"
                                |)
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                                "function_context"
                              |);
                              M.read (| meter |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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 (|
                  M.call_closure (|
                    M.get_function (|
                      "move_bytecode_verifier::reference_safety::verify",
                      [ impl_Meter__plus___Sized ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                          "module"
                        |)
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                        "function_context"
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                          "name_def_map"
                        |)
                      |);
                      M.read (| meter |)
                    ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_common :
      M.IsAssociatedFunction Self "verify_common" verify_common.
  End Impl_move_bytecode_verifier_code_unit_verifier_CodeUnitVerifier.
End code_unit_verifier.
