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

Module limits.
  (* StructRecord
    {
      name := "LimitsVerifier";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply (Ty.path "&") [] [ Ty.path "move_binary_format::file_format::CompiledModule" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_limits_LimitsVerifier.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::limits::LimitsVerifier".
    
    (*
        pub fn verify_module(config: &VerifierConfig, module: &'a CompiledModule) -> VMResult<()> {
            Self::verify_module_impl(config, module)
                .map_err(|e| e.finish(Location::Module(module.self_id())))
        }
    *)
    Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ config; module ] =>
        ltac:(M.monadic
          (let config := M.alloc (| config |) in
          let module := M.alloc (| module |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
              "map_err",
              [
                Ty.path "move_binary_format::errors::VMError";
                Ty.function
                  [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ] ]
                  (Ty.path "move_binary_format::errors::VMError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                  "verify_module_impl",
                  []
                |),
                [ M.read (| config |); M.read (| module |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let e := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::errors::PartialVMError",
                                    "finish",
                                    []
                                  |),
                                  [
                                    M.read (| e |);
                                    Value.StructTuple
                                      "move_binary_format::errors::Location::Module"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "self_id",
                                            []
                                          |),
                                          [ M.read (| module |) ]
                                        |)
                                      ]
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module :
      M.IsAssociatedFunction Self "verify_module" verify_module.
    
    (*
        fn verify_module_impl(
            config: &VerifierConfig,
            module: &'a CompiledModule,
        ) -> PartialVMResult<()> {
            let limit_check = Self { module };
            limit_check.verify_constants(config)?;
            limit_check.verify_function_handles(config)?;
            limit_check.verify_struct_handles(config)?;
            limit_check.verify_type_nodes(config)?;
            limit_check.verify_identifiers(config)?;
            limit_check.verify_definitions(config)
        }
    *)
    Definition verify_module_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ config; module ] =>
        ltac:(M.monadic
          (let config := M.alloc (| config |) in
          let module := M.alloc (| module |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ limit_check :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::limits::LimitsVerifier"
                      [ ("module", M.read (| module |)) ]
                  |) 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::limits::LimitsVerifier",
                              "verify_constants",
                              []
                            |),
                            [ limit_check; M.read (| config |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_associated_function (|
                              Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                              "verify_function_handles",
                              []
                            |),
                            [ limit_check; M.read (| config |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_associated_function (|
                              Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                              "verify_struct_handles",
                              []
                            |),
                            [ limit_check; M.read (| config |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_associated_function (|
                              Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                              "verify_type_nodes",
                              []
                            |),
                            [ limit_check; M.read (| config |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_associated_function (|
                              Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                              "verify_identifiers",
                              []
                            |),
                            [ limit_check; M.read (| config |) ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_associated_function (|
                      Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                      "verify_definitions",
                      []
                    |),
                    [ limit_check; M.read (| config |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn verify_struct_handles(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            if let Some(limit) = config.max_generic_instantiation_length {
                for (idx, struct_handle) in self.module.struct_handles().iter().enumerate() {
                    if struct_handle.type_parameters.len() > limit {
                        return Err(PartialVMError::new(StatusCode::TOO_MANY_TYPE_PARAMETERS)
                            .at_index(IndexKind::StructHandle, idx as u16));
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_struct_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_generic_instantiation_length"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let limit := M.copy (| γ0_0 |) in
                          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::StructHandle"
                                          ]
                                      ],
                                    [],
                                    "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::StructHandle"
                                          ],
                                        [],
                                        "enumerate",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "slice")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::StructHandle"
                                              ],
                                            "iter",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path
                                                  "move_binary_format::file_format::CompiledModule",
                                                "struct_handles",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "move_bytecode_verifier::limits::LimitsVerifier",
                                                    "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::StructHandle"
                                                        ]
                                                    ],
                                                  [],
                                                  "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 struct_handle := M.copy (| γ1_1 |) 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
                                                                            "move_binary_format::file_format::StructTypeParameter";
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ],
                                                                      "len",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| struct_handle |),
                                                                        "move_binary_format::file_format::StructHandle",
                                                                        "type_parameters"
                                                                      |)
                                                                    ]
                                                                  |),
                                                                  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_index",
                                                                          []
                                                                        |),
                                                                        [
                                                                          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_TYPE_PARAMETERS"
                                                                                []
                                                                            ]
                                                                          |);
                                                                          Value.StructTuple
                                                                            "move_binary_format::IndexKind::StructHandle"
                                                                            [];
                                                                          M.rust_cast
                                                                            (M.read (| idx |))
                                                                        ]
                                                                      |)
                                                                    ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        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_struct_handles :
      M.IsAssociatedFunction Self "verify_struct_handles" verify_struct_handles.
    
    (*
        fn verify_function_handles(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            for (idx, function_handle) in self.module.function_handles().iter().enumerate() {
                if let Some(limit) = config.max_generic_instantiation_length {
                    if function_handle.type_parameters.len() > limit {
                        return Err(PartialVMError::new(StatusCode::TOO_MANY_TYPE_PARAMETERS)
                            .at_index(IndexKind::FunctionHandle, idx as u16));
                    }
                };
                if let Some(limit) = config.max_function_parameters {
                    if self.module.signature_at(function_handle.parameters).0.len() > limit {
                        return Err(PartialVMError::new(StatusCode::TOO_MANY_PARAMETERS)
                            .at_index(IndexKind::FunctionHandle, idx as u16));
                    }
                };
            }
            Ok(())
        }
    *)
    Definition verify_function_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionHandle" ]
                              ],
                            [],
                            "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::FunctionHandle" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::FunctionHandle" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_handles",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "move_bytecode_verifier::limits::LimitsVerifier",
                                            "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::FunctionHandle"
                                                ]
                                            ],
                                          [],
                                          "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_handle := M.copy (| γ1_1 |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| config |),
                                                        "move_vm_config::verifier::VerifierConfig",
                                                        "max_generic_instantiation_length"
                                                      |) 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
                                                                              "move_binary_format::file_format::AbilitySet";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (|
                                                                            function_handle
                                                                          |),
                                                                          "move_binary_format::file_format::FunctionHandle",
                                                                          "type_parameters"
                                                                        |)
                                                                      ]
                                                                    |),
                                                                    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_index",
                                                                            []
                                                                          |),
                                                                          [
                                                                            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_TYPE_PARAMETERS"
                                                                                  []
                                                                              ]
                                                                            |);
                                                                            Value.StructTuple
                                                                              "move_binary_format::IndexKind::FunctionHandle"
                                                                              [];
                                                                            M.rust_cast
                                                                              (M.read (| idx |))
                                                                          ]
                                                                        |)
                                                                      ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (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 (| config |),
                                                        "move_vm_config::verifier::VerifierConfig",
                                                        "max_function_parameters"
                                                      |) 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
                                                                              "move_binary_format::file_format::SignatureToken";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        "len",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_binary_format::file_format::CompiledModule",
                                                                              "signature_at",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (|
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| self |),
                                                                                  "move_bytecode_verifier::limits::LimitsVerifier",
                                                                                  "module"
                                                                                |)
                                                                              |);
                                                                              M.read (|
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (|
                                                                                    function_handle
                                                                                  |),
                                                                                  "move_binary_format::file_format::FunctionHandle",
                                                                                  "parameters"
                                                                                |)
                                                                              |)
                                                                            ]
                                                                          |),
                                                                          "move_binary_format::file_format::Signature",
                                                                          0
                                                                        |)
                                                                      ]
                                                                    |),
                                                                    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_index",
                                                                            []
                                                                          |),
                                                                          [
                                                                            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_PARAMETERS"
                                                                                  []
                                                                              ]
                                                                            |);
                                                                            Value.StructTuple
                                                                              "move_binary_format::IndexKind::FunctionHandle"
                                                                              [];
                                                                            M.rust_cast
                                                                              (M.read (| idx |))
                                                                          ]
                                                                        |)
                                                                      ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_function_handles :
      M.IsAssociatedFunction Self "verify_function_handles" verify_function_handles.
    
    (*
        fn verify_type_nodes(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            for sign in self.module.signatures() {
                for ty in &sign.0 {
                    self.verify_type_node(config, ty)?
                }
            }
            for cons in self.module.constant_pool() {
                self.verify_type_node(config, &cons.type_)?
            }
            let sdefs = self.module.struct_defs();
            {
                for sdef in sdefs {
                    if let StructFieldInformation::Declared(fdefs) = &sdef.field_information {
                        for fdef in fdefs {
                            self.verify_type_node(config, &fdef.signature.0)?
                        }
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_type_nodes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Signature" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "signatures",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::limits::LimitsVerifier",
                                    "module"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [ Ty.path "move_binary_format::file_format::Signature"
                                            ],
                                          [],
                                          "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 sign := M.copy (| γ0_0 |) in
                                          M.use
                                            (M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::collect::IntoIterator",
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_binary_format::file_format::SignatureToken";
                                                            Ty.path "alloc::alloc::Global"
                                                          ]
                                                      ],
                                                    [],
                                                    "into_iter",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      M.read (| sign |),
                                                      "move_binary_format::file_format::Signature",
                                                      0
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let iter := M.copy (| γ |) in
                                                    M.loop (|
                                                      ltac:(M.monadic
                                                        (let~ _ :=
                                                          M.match_operator (|
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::iter::traits::iterator::Iterator",
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::slice::iter::Iter")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::SignatureToken"
                                                                    ],
                                                                  [],
                                                                  "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 ty := M.copy (| γ0_0 |) in
                                                                  M.match_operator (|
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::try_trait::Try",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::result::Result")
                                                                            []
                                                                            [
                                                                              Ty.tuple [];
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError"
                                                                            ],
                                                                          [],
                                                                          "branch",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_bytecode_verifier::limits::LimitsVerifier",
                                                                              "verify_type_node",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (| self |);
                                                                              M.read (| config |);
                                                                              M.read (| ty |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ0_0 :=
                                                                            M.SubPointer.get_struct_tuple_field (|
                                                                              γ,
                                                                              "core::ops::control_flow::ControlFlow::Break",
                                                                              0
                                                                            |) in
                                                                          let residual :=
                                                                            M.copy (| γ0_0 |) in
                                                                          M.alloc (|
                                                                            M.never_to_any (|
                                                                              M.read (|
                                                                                M.return_ (|
                                                                                  M.call_closure (|
                                                                                    M.get_trait_method (|
                                                                                      "core::ops::try_trait::FromResidual",
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "core::result::Result")
                                                                                        []
                                                                                        [
                                                                                          Ty.tuple
                                                                                            [];
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError"
                                                                                        ],
                                                                                      [
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "core::result::Result")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "core::convert::Infallible";
                                                                                            Ty.path
                                                                                              "move_binary_format::errors::PartialVMError"
                                                                                          ]
                                                                                      ],
                                                                                      "from_residual",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.read (|
                                                                                        residual
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                |)
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ0_0 :=
                                                                            M.SubPointer.get_struct_tuple_field (|
                                                                              γ,
                                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                                              0
                                                                            |) in
                                                                          let val :=
                                                                            M.copy (| γ0_0 |) in
                                                                          val))
                                                                    ]
                                                                  |)))
                                                            ]
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                    |)))
                                              ]
                                            |))))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Constant" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "constant_pool",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::limits::LimitsVerifier",
                                    "module"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [ Ty.path "move_binary_format::file_format::Constant" ],
                                          [],
                                          "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 cons := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_bytecode_verifier::limits::LimitsVerifier",
                                                      "verify_type_node",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| self |);
                                                      M.read (| config |);
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| cons |),
                                                        "move_binary_format::file_format::Constant",
                                                        "type_"
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ sdefs :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "struct_defs",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::limits::LimitsVerifier",
                            "module"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::StructDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| sdefs |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::StructDefinition"
                                            ],
                                          [],
                                          "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 sdef := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.alloc (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| sdef |),
                                                        "move_binary_format::file_format::StructDefinition",
                                                        "field_information"
                                                      |)
                                                    |) in
                                                  let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::StructFieldInformation::Declared",
                                                      0
                                                    |) in
                                                  let fdefs := M.alloc (| γ1_0 |) in
                                                  M.use
                                                    (M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::iter::traits::collect::IntoIterator",
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "alloc::vec::Vec")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::FieldDefinition";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ]
                                                              ],
                                                            [],
                                                            "into_iter",
                                                            []
                                                          |),
                                                          [ M.read (| fdefs |) ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let iter := M.copy (| γ |) in
                                                            M.loop (|
                                                              ltac:(M.monadic
                                                                (let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::iter::traits::iterator::Iterator",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::slice::iter::Iter")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "move_binary_format::file_format::FieldDefinition"
                                                                            ],
                                                                          [],
                                                                          "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 fdef :=
                                                                            M.copy (| γ0_0 |) in
                                                                          M.match_operator (|
                                                                            M.alloc (|
                                                                              M.call_closure (|
                                                                                M.get_trait_method (|
                                                                                  "core::ops::try_trait::Try",
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::result::Result")
                                                                                    []
                                                                                    [
                                                                                      Ty.tuple [];
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError"
                                                                                    ],
                                                                                  [],
                                                                                  "branch",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.call_closure (|
                                                                                    M.get_associated_function (|
                                                                                      Ty.path
                                                                                        "move_bytecode_verifier::limits::LimitsVerifier",
                                                                                      "verify_type_node",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.read (|
                                                                                        self
                                                                                      |);
                                                                                      M.read (|
                                                                                        config
                                                                                      |);
                                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                                        M.SubPointer.get_struct_record_field (|
                                                                                          M.read (|
                                                                                            fdef
                                                                                          |),
                                                                                          "move_binary_format::file_format::FieldDefinition",
                                                                                          "signature"
                                                                                        |),
                                                                                        "move_binary_format::file_format::TypeSignature",
                                                                                        0
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (let γ0_0 :=
                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                      γ,
                                                                                      "core::ops::control_flow::ControlFlow::Break",
                                                                                      0
                                                                                    |) in
                                                                                  let residual :=
                                                                                    M.copy (|
                                                                                      γ0_0
                                                                                    |) in
                                                                                  M.alloc (|
                                                                                    M.never_to_any (|
                                                                                      M.read (|
                                                                                        M.return_ (|
                                                                                          M.call_closure (|
                                                                                            M.get_trait_method (|
                                                                                              "core::ops::try_trait::FromResidual",
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "core::result::Result")
                                                                                                []
                                                                                                [
                                                                                                  Ty.tuple
                                                                                                    [];
                                                                                                  Ty.path
                                                                                                    "move_binary_format::errors::PartialVMError"
                                                                                                ],
                                                                                              [
                                                                                                Ty.apply
                                                                                                  (Ty.path
                                                                                                    "core::result::Result")
                                                                                                  []
                                                                                                  [
                                                                                                    Ty.path
                                                                                                      "core::convert::Infallible";
                                                                                                    Ty.path
                                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                                  ]
                                                                                              ],
                                                                                              "from_residual",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                residual
                                                                                              |)
                                                                                            ]
                                                                                          |)
                                                                                        |)
                                                                                      |)
                                                                                    |)
                                                                                  |)));
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (let γ0_0 :=
                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                      γ,
                                                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                                                      0
                                                                                    |) in
                                                                                  let val :=
                                                                                    M.copy (|
                                                                                      γ0_0
                                                                                    |) in
                                                                                  val))
                                                                            ]
                                                                          |)))
                                                                    ]
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)))
                                                            |)))
                                                      ]
                                                    |))));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_type_nodes :
      M.IsAssociatedFunction Self "verify_type_nodes" verify_type_nodes.
    
    (*
        fn verify_type_node(
            &self,
            config: &VerifierConfig,
            ty: &SignatureToken,
        ) -> PartialVMResult<()> {
            if let Some(max) = &config.max_type_nodes {
                // Structs and Parameters can expand to an unknown number of nodes, therefore
                // we give them a higher size weight here.
                const STRUCT_SIZE_WEIGHT: usize = 4;
                const PARAM_SIZE_WEIGHT: usize = 4;
                let mut size = 0;
                for t in ty.preorder_traversal() {
                    // Notice that the preorder traversal will iterate all type instantiations, so we
                    // why we can ignore them below.
                    match t {
                        SignatureToken::Struct(..) | SignatureToken::StructInstantiation(..) => {
                            size += STRUCT_SIZE_WEIGHT
                        }
                        SignatureToken::TypeParameter(..) => size += PARAM_SIZE_WEIGHT,
                        _ => size += 1,
                    }
                }
                if size > *max {
                    return Err(PartialVMError::new(StatusCode::TOO_MANY_TYPE_NODES));
                }
            }
            Ok(())
        }
    *)
    Definition verify_type_node (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config; ty ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          let ty := M.alloc (| ty |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| config |),
                                "move_vm_config::verifier::VerifierConfig",
                                "max_type_nodes"
                              |)
                            |) in
                          let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max := M.alloc (| γ1_0 |) in
                          let~ size := 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.path
                                        "move_binary_format::file_format::SignatureTokenPreorderTraversalIter",
                                      [],
                                      "into_iter",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::SignatureToken",
                                          "preorder_traversal",
                                          []
                                        |),
                                        [ M.read (| ty |) ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  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.path
                                                      "move_binary_format::file_format::SignatureTokenPreorderTraversalIter",
                                                    [],
                                                    "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 t := M.copy (| γ0_0 |) in
                                                    M.match_operator (|
                                                      t,
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.find_or_pattern (|
                                                              γ,
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ := M.read (| γ |) in
                                                                    let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::SignatureToken::Struct"
                                                                      |) in
                                                                    Value.Tuple []));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ := M.read (| γ |) in
                                                                    let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::SignatureToken::StructInstantiation"
                                                                      |) in
                                                                    Value.Tuple []))
                                                              ],
                                                              M.closure
                                                                (fun γ =>
                                                                  ltac:(M.monadic
                                                                    match γ with
                                                                    | [] =>
                                                                      ltac:(M.monadic
                                                                        (let β := size in
                                                                        M.write (|
                                                                          β,
                                                                          BinOp.Wrap.add (|
                                                                            M.read (| β |),
                                                                            M.read (|
                                                                              M.get_constant (|
                                                                                "move_bytecode_verifier::limits::verify_type_node::STRUCT_SIZE_WEIGHT"
                                                                              |)
                                                                            |)
                                                                          |)
                                                                        |)))
                                                                    | _ =>
                                                                      M.impossible
                                                                        "wrong number of arguments"
                                                                    end))
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ := M.read (| γ |) in
                                                            let _ :=
                                                              M.is_struct_tuple (|
                                                                γ,
                                                                "move_binary_format::file_format::SignatureToken::TypeParameter"
                                                              |) in
                                                            let β := size in
                                                            M.write (|
                                                              β,
                                                              BinOp.Wrap.add (|
                                                                M.read (| β |),
                                                                M.read (|
                                                                  M.get_constant (|
                                                                    "move_bytecode_verifier::limits::verify_type_node::PARAM_SIZE_WEIGHT"
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let β := size in
                                                            M.write (|
                                                              β,
                                                              BinOp.Wrap.add (|
                                                                M.read (| β |),
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                      |)))
                                ]
                              |)) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| size |),
                                          M.read (| M.read (| max |) |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "new",
                                                  []
                                                |),
                                                [
                                                  Value.StructTuple
                                                    "move_core_types::vm_status::StatusCode::TOO_MANY_TYPE_NODES"
                                                    []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              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_type_node :
      M.IsAssociatedFunction Self "verify_type_node" verify_type_node.
    
    (*
        fn verify_definitions(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            let defs = self.module.function_defs();
            if let Some(max_function_definitions) = config.max_function_definitions {
                if defs.len() > max_function_definitions {
                    return Err(PartialVMError::new(
                        StatusCode::MAX_FUNCTION_DEFINITIONS_REACHED,
                    ));
                }
            }
    
            let defs = self.module.struct_defs();
            if let Some(max_struct_definitions) = config.max_struct_definitions {
                if defs.len() > max_struct_definitions {
                    return Err(PartialVMError::new(
                        StatusCode::MAX_STRUCT_DEFINITIONS_REACHED,
                    ));
                }
            }
            if let Some(max_fields_in_struct) = config.max_fields_in_struct {
                for def in defs {
                    match &def.field_information {
                        StructFieldInformation::Native => (),
                        StructFieldInformation::Declared(fields) => {
                            if fields.len() > max_fields_in_struct {
                                return Err(PartialVMError::new(
                                    StatusCode::MAX_FIELD_DEFINITIONS_REACHED,
                                ));
                            }
                        }
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_definitions (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ defs :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "function_defs",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::limits::LimitsVerifier",
                            "module"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_function_definitions"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max_function_definitions := 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 "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| defs |) ]
                                          |),
                                          M.read (| max_function_definitions |)
                                        |)
                                      |)) 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::MAX_FUNCTION_DEFINITIONS_REACHED"
                                                    []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ defs :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "struct_defs",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::limits::LimitsVerifier",
                            "module"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_struct_definitions"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max_struct_definitions := 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 "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::StructDefinition"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| defs |) ]
                                          |),
                                          M.read (| max_struct_definitions |)
                                        |)
                                      |)) 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::MAX_STRUCT_DEFINITIONS_REACHED"
                                                    []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (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 (| config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_fields_in_struct"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max_fields_in_struct := M.copy (| γ0_0 |) in
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::StructDefinition"
                                          ]
                                      ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [ M.read (| defs |) ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_binary_format::file_format::StructDefinition"
                                                    ],
                                                  [],
                                                  "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 def := M.copy (| γ0_0 |) in
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| def |),
                                                        "move_binary_format::file_format::StructDefinition",
                                                        "field_information"
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "move_binary_format::file_format::StructFieldInformation::Native"
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::StructFieldInformation::Declared",
                                                              0
                                                            |) in
                                                          let fields := M.alloc (| γ1_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
                                                                                    "move_binary_format::file_format::FieldDefinition";
                                                                                  Ty.path
                                                                                    "alloc::alloc::Global"
                                                                                ],
                                                                              "len",
                                                                              []
                                                                            |),
                                                                            [ M.read (| fields |) ]
                                                                          |),
                                                                          M.read (|
                                                                            max_fields_in_struct
                                                                          |)
                                                                        |)
                                                                      |)) 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::MAX_FIELD_DEFINITIONS_REACHED"
                                                                                    []
                                                                                ]
                                                                              |)
                                                                            ]
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        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_definitions :
      M.IsAssociatedFunction Self "verify_definitions" verify_definitions.
    
    (*
        fn verify_constants(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            for (idx, constant) in self.module.constant_pool().iter().enumerate() {
                if let SignatureToken::Vector(_) = constant.type_ {
                    if let MoveValue::Vector(cons) =
                        constant.deserialize_constant().ok_or_else(|| {
                            verification_error(
                                StatusCode::MALFORMED_CONSTANT_DATA,
                                IndexKind::ConstantPool,
                                idx as TableIndex,
                            )
                        })?
                    {
                        if let Some(lim) = config.max_constant_vector_len {
                            if cons.len() > lim as usize {
                                return Err(PartialVMError::new(StatusCode::TOO_MANY_VECTOR_ELEMENTS)
                                    .with_message(format!("vector size limit is {}", lim)));
                            }
                        }
                    } else {
                        return Err(verification_error(
                            StatusCode::INVALID_CONSTANT_TYPE,
                            IndexKind::ConstantPool,
                            idx as TableIndex,
                        ));
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_constants (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Constant" ]
                              ],
                            [],
                            "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::Constant" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::Constant" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "constant_pool",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "move_bytecode_verifier::limits::LimitsVerifier",
                                            "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::Constant"
                                                ]
                                            ],
                                          [],
                                          "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 constant := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| constant |),
                                                      "move_binary_format::file_format::Constant",
                                                      "type_"
                                                    |) in
                                                  let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_binary_format::file_format::SignatureToken::Vector",
                                                      0
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (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.path
                                                                          "move_core_types::runtime_value::MoveValue";
                                                                        Ty.path
                                                                          "move_binary_format::errors::PartialVMError"
                                                                      ],
                                                                    [],
                                                                    "branch",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::option::Option")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_core_types::runtime_value::MoveValue"
                                                                          ],
                                                                        "ok_or_else",
                                                                        [
                                                                          Ty.path
                                                                            "move_binary_format::errors::PartialVMError";
                                                                          Ty.function
                                                                            [ Ty.tuple [] ]
                                                                            (Ty.path
                                                                              "move_binary_format::errors::PartialVMError")
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::Constant",
                                                                            "deserialize_constant",
                                                                            []
                                                                          |),
                                                                          [ M.read (| constant |) ]
                                                                        |);
                                                                        M.closure
                                                                          (fun γ =>
                                                                            ltac:(M.monadic
                                                                              match γ with
                                                                              | [ α0 ] =>
                                                                                ltac:(M.monadic
                                                                                  (M.match_operator (|
                                                                                    M.alloc (|
                                                                                      α0
                                                                                    |),
                                                                                    [
                                                                                      fun γ =>
                                                                                        ltac:(M.monadic
                                                                                          (M.call_closure (|
                                                                                            M.get_function (|
                                                                                              "move_binary_format::errors::verification_error",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              Value.StructTuple
                                                                                                "move_core_types::vm_status::StatusCode::MALFORMED_CONSTANT_DATA"
                                                                                                [];
                                                                                              Value.StructTuple
                                                                                                "move_binary_format::IndexKind::ConstantPool"
                                                                                                [];
                                                                                              M.rust_cast
                                                                                                (M.read (|
                                                                                                  idx
                                                                                                |))
                                                                                            ]
                                                                                          |)))
                                                                                    ]
                                                                                  |)))
                                                                              | _ =>
                                                                                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 γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_core_types::runtime_value::MoveValue::Vector",
                                                              0
                                                            |) in
                                                          let cons := M.copy (| γ0_0 |) in
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| config |),
                                                                      "move_vm_config::verifier::VerifierConfig",
                                                                      "max_constant_vector_len"
                                                                    |) in
                                                                  let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::option::Option::Some",
                                                                      0
                                                                    |) in
                                                                  let lim := 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
                                                                                            "move_core_types::runtime_value::MoveValue";
                                                                                          Ty.path
                                                                                            "alloc::alloc::Global"
                                                                                        ],
                                                                                      "len",
                                                                                      []
                                                                                    |),
                                                                                    [ cons ]
                                                                                  |),
                                                                                  M.rust_cast
                                                                                    (M.read (|
                                                                                      lim
                                                                                    |))
                                                                                |)
                                                                              |)) in
                                                                          let _ :=
                                                                            M.is_constant_or_break_match (|
                                                                              M.read (| γ |),
                                                                              Value.Bool true
                                                                            |) in
                                                                          M.alloc (|
                                                                            M.never_to_any (|
                                                                              M.read (|
                                                                                M.return_ (|
                                                                                  Value.StructTuple
                                                                                    "core::result::Result::Err"
                                                                                    [
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError",
                                                                                          "with_message",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "move_binary_format::errors::PartialVMError",
                                                                                              "new",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              Value.StructTuple
                                                                                                "move_core_types::vm_status::StatusCode::TOO_MANY_VECTOR_ELEMENTS"
                                                                                                []
                                                                                            ]
                                                                                          |);
                                                                                          M.call_closure (|
                                                                                            M.get_function (|
                                                                                              "core::hint::must_use",
                                                                                              [
                                                                                                Ty.path
                                                                                                  "alloc::string::String"
                                                                                              ]
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                let~
                                                                                                      res :=
                                                                                                  M.alloc (|
                                                                                                    M.call_closure (|
                                                                                                      M.get_function (|
                                                                                                        "alloc::fmt::format",
                                                                                                        []
                                                                                                      |),
                                                                                                      [
                                                                                                        M.call_closure (|
                                                                                                          M.get_associated_function (|
                                                                                                            Ty.path
                                                                                                              "core::fmt::Arguments",
                                                                                                            "new_v1",
                                                                                                            []
                                                                                                          |),
                                                                                                          [
                                                                                                            M.alloc (|
                                                                                                              Value.Array
                                                                                                                [
                                                                                                                  M.read (|
                                                                                                                    Value.String
                                                                                                                      "vector size limit is "
                                                                                                                  |)
                                                                                                                ]
                                                                                                            |);
                                                                                                            M.alloc (|
                                                                                                              Value.Array
                                                                                                                [
                                                                                                                  M.call_closure (|
                                                                                                                    M.get_associated_function (|
                                                                                                                      Ty.path
                                                                                                                        "core::fmt::rt::Argument",
                                                                                                                      "new_display",
                                                                                                                      [
                                                                                                                        Ty.path
                                                                                                                          "u64"
                                                                                                                      ]
                                                                                                                    |),
                                                                                                                    [
                                                                                                                      lim
                                                                                                                    ]
                                                                                                                  |)
                                                                                                                ]
                                                                                                            |)
                                                                                                          ]
                                                                                                        |)
                                                                                                      ]
                                                                                                    |)
                                                                                                  |) in
                                                                                                res
                                                                                              |)
                                                                                            ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    ]
                                                                                |)
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                    ]
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  Value.StructTuple
                                                                    "core::result::Result::Err"
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "move_binary_format::errors::verification_error",
                                                                          []
                                                                        |),
                                                                        [
                                                                          Value.StructTuple
                                                                            "move_core_types::vm_status::StatusCode::INVALID_CONSTANT_TYPE"
                                                                            [];
                                                                          Value.StructTuple
                                                                            "move_binary_format::IndexKind::ConstantPool"
                                                                            [];
                                                                          M.rust_cast
                                                                            (M.read (| idx |))
                                                                        ]
                                                                      |)
                                                                    ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)))
                                                    ]
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_constants :
      M.IsAssociatedFunction Self "verify_constants" verify_constants.
    
    (*
        fn verify_identifiers(&self, config: &VerifierConfig) -> PartialVMResult<()> {
            if let Some(max_idenfitier_len) = config.max_idenfitier_len {
                for (idx, identifier) in self.module.identifiers().iter().enumerate() {
                    if identifier.len() > (max_idenfitier_len as usize) {
                        return Err(verification_error(
                            StatusCode::IDENTIFIER_TOO_LONG,
                            IndexKind::Identifier,
                            idx as TableIndex,
                        ));
                    }
                }
            }
            Ok(())
        }
    *)
    Definition verify_identifiers (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| config |),
                              "move_vm_config::verifier::VerifierConfig",
                              "max_idenfitier_len"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max_idenfitier_len := M.copy (| γ0_0 |) in
                          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_core_types::identifier::Identifier" ]
                                      ],
                                    [],
                                    "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_core_types::identifier::Identifier" ],
                                        [],
                                        "enumerate",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "slice")
                                              []
                                              [ Ty.path "move_core_types::identifier::Identifier" ],
                                            "iter",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path
                                                  "move_binary_format::file_format::CompiledModule",
                                                "identifiers",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "move_bytecode_verifier::limits::LimitsVerifier",
                                                    "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_core_types::identifier::Identifier"
                                                        ]
                                                    ],
                                                  [],
                                                  "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 identifier := M.copy (| γ1_1 |) 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.path
                                                                        "move_core_types::identifier::IdentStr",
                                                                      "len",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::ops::deref::Deref",
                                                                          Ty.path
                                                                            "move_core_types::identifier::Identifier",
                                                                          [],
                                                                          "deref",
                                                                          []
                                                                        |),
                                                                        [ M.read (| identifier |) ]
                                                                      |)
                                                                    ]
                                                                  |),
                                                                  M.rust_cast
                                                                    (M.read (|
                                                                      max_idenfitier_len
                                                                    |))
                                                                |)
                                                              |)) 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_function (|
                                                                          "move_binary_format::errors::verification_error",
                                                                          []
                                                                        |),
                                                                        [
                                                                          Value.StructTuple
                                                                            "move_core_types::vm_status::StatusCode::IDENTIFIER_TOO_LONG"
                                                                            [];
                                                                          Value.StructTuple
                                                                            "move_binary_format::IndexKind::Identifier"
                                                                            [];
                                                                          M.rust_cast
                                                                            (M.read (| idx |))
                                                                        ]
                                                                      |)
                                                                    ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        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_identifiers :
      M.IsAssociatedFunction Self "verify_identifiers" verify_identifiers.
  End Impl_move_bytecode_verifier_limits_LimitsVerifier.
End limits.
