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

Module check_duplication.
  (* StructRecord
    {
      name := "DuplicationChecker";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply (Ty.path "&") [] [ Ty.path "move_binary_format::file_format::CompiledModule" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_check_duplication_DuplicationChecker.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker".
    
    (*
        pub fn verify_module(module: &'a CompiledModule) -> VMResult<()> {
            Self::verify_module_impl(module).map_err(|e| e.finish(Location::Module(module.self_id())))
        }
    *)
    Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
              "map_err",
              [
                Ty.path "move_binary_format::errors::VMError";
                Ty.function
                  [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ] ]
                  (Ty.path "move_binary_format::errors::VMError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                  "verify_module_impl",
                  []
                |),
                [ M.read (| module |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let e := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::errors::PartialVMError",
                                    "finish",
                                    []
                                  |),
                                  [
                                    M.read (| e |);
                                    Value.StructTuple
                                      "move_binary_format::errors::Location::Module"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "self_id",
                                            []
                                          |),
                                          [ M.read (| module |) ]
                                        |)
                                      ]
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module :
      M.IsAssociatedFunction Self "verify_module" verify_module.
    
    (*
        fn verify_module_impl(module: &'a CompiledModule) -> PartialVMResult<()> {
            Self::check_identifiers(module.identifiers())?;
            Self::check_address_identifiers(module.address_identifiers())?;
            Self::check_constants(module.constant_pool())?;
            Self::check_signatures(module.signatures())?;
            Self::check_module_handles(module.module_handles())?;
            Self::check_module_handles(module.friend_decls())?;
            Self::check_struct_handles(module.struct_handles())?;
            Self::check_function_handles(module.function_handles())?;
            Self::check_function_instantiations(module.function_instantiations())?;
    
            let checker = Self { module };
            checker.check_field_handles()?;
            checker.check_field_instantiations()?;
            checker.check_function_defintions()?;
            checker.check_struct_definitions()?;
            checker.check_struct_instantiations()
        }
    *)
    Definition verify_module_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.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::check_duplication::DuplicationChecker",
                              "check_identifiers",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "identifiers",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_address_identifiers",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "address_identifiers",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_constants",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "constant_pool",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_signatures",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "signatures",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_module_handles",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "module_handles",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_module_handles",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "friend_decls",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_struct_handles",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "struct_handles",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_function_handles",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "function_handles",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_function_instantiations",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "function_instantiations",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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~ checker :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::check_duplication::DuplicationChecker"
                      [ ("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::check_duplication::DuplicationChecker",
                              "check_field_handles",
                              []
                            |),
                            [ checker ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_field_instantiations",
                              []
                            |),
                            [ checker ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_function_defintions",
                              []
                            |),
                            [ checker ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                              "check_struct_definitions",
                              []
                            |),
                            [ checker ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::check_duplication::DuplicationChecker",
                      "check_struct_instantiations",
                      []
                    |),
                    [ checker ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn check_identifiers(identifiers: &[Identifier]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(identifiers) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::Identifier,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_identifiers (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ identifiers ] =>
        ltac:(M.monadic
          (let identifiers := M.alloc (| identifiers |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_core_types::identifier::Identifier" ]
                        ]
                    ]
                  |),
                  [ M.read (| identifiers |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::Identifier" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_identifiers :
      M.IsAssociatedFunction Self "check_identifiers" check_identifiers.
    
    (*
        fn check_address_identifiers(address_identifiers: &[AccountAddress]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(address_identifiers) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::AddressIdentifier,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_address_identifiers
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ address_identifiers ] =>
        ltac:(M.monadic
          (let address_identifiers := M.alloc (| address_identifiers |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_core_types::account_address::AccountAddress" ]
                        ]
                    ]
                  |),
                  [ M.read (| address_identifiers |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple
                                "move_binary_format::IndexKind::AddressIdentifier"
                                [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_address_identifiers :
      M.IsAssociatedFunction Self "check_address_identifiers" check_address_identifiers.
    
    (*
        fn check_constants(constant_pool: &[Constant]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(constant_pool) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::ConstantPool,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_constants (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ constant_pool ] =>
        ltac:(M.monadic
          (let constant_pool := M.alloc (| constant_pool |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::Constant" ]
                        ]
                    ]
                  |),
                  [ M.read (| constant_pool |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::ConstantPool" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_constants :
      M.IsAssociatedFunction Self "check_constants" check_constants.
    
    (*
        fn check_signatures(signatures: &[Signature]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(signatures) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::Signature,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_signatures (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ signatures ] =>
        ltac:(M.monadic
          (let signatures := M.alloc (| signatures |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::Signature" ]
                        ]
                    ]
                  |),
                  [ M.read (| signatures |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::Signature" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_signatures :
      M.IsAssociatedFunction Self "check_signatures" check_signatures.
    
    (*
        fn check_module_handles(module_handles: &[ModuleHandle]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(module_handles) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::ModuleHandle,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_module_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module_handles ] =>
        ltac:(M.monadic
          (let module_handles := M.alloc (| module_handles |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::ModuleHandle" ]
                        ]
                    ]
                  |),
                  [ M.read (| module_handles |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::ModuleHandle" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_module_handles :
      M.IsAssociatedFunction Self "check_module_handles" check_module_handles.
    
    (*
        fn check_struct_handles(struct_handles: &[StructHandle]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(struct_handles.iter().map(|x| (x.module, x.name))) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::StructHandle,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_struct_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ struct_handles ] =>
        ltac:(M.monadic
          (let struct_handles := M.alloc (| struct_handles |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "core::iter::adapters::map::Map")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::slice::iter::Iter")
                            []
                            [ Ty.path "move_binary_format::file_format::StructHandle" ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_binary_format::file_format::StructHandle" ]
                                ]
                            ]
                            (Ty.tuple
                              [
                                Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                                Ty.path "move_binary_format::file_format::IdentifierIndex"
                              ])
                        ]
                    ]
                  |),
                  [
                    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" ],
                        [],
                        "map",
                        [
                          Ty.tuple
                            [
                              Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                              Ty.path "move_binary_format::file_format::IdentifierIndex"
                            ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_binary_format::file_format::StructHandle" ]
                                ]
                            ]
                            (Ty.tuple
                              [
                                Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                                Ty.path "move_binary_format::file_format::IdentifierIndex"
                              ])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "move_binary_format::file_format::StructHandle" ],
                            "iter",
                            []
                          |),
                          [ M.read (| struct_handles |) ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let x := M.copy (| γ |) in
                                          Value.Tuple
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::StructHandle",
                                                  "module"
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::StructHandle",
                                                  "name"
                                                |)
                                              |)
                                            ]))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::StructHandle" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_struct_handles :
      M.IsAssociatedFunction Self "check_struct_handles" check_struct_handles.
    
    (*
        fn check_function_instantiations(
            function_instantiations: &[FunctionInstantiation],
        ) -> PartialVMResult<()> {
            match Self::first_duplicate_element(function_instantiations) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::FunctionInstantiation,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_function_instantiations
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ function_instantiations ] =>
        ltac:(M.monadic
          (let function_instantiations := M.alloc (| function_instantiations |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::FunctionInstantiation" ]
                        ]
                    ]
                  |),
                  [ M.read (| function_instantiations |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple
                                "move_binary_format::IndexKind::FunctionInstantiation"
                                [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_function_instantiations :
      M.IsAssociatedFunction Self "check_function_instantiations" check_function_instantiations.
    
    (*
        fn check_function_handles(function_handles: &[FunctionHandle]) -> PartialVMResult<()> {
            match Self::first_duplicate_element(function_handles.iter().map(|x| (x.module, x.name))) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::FunctionHandle,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_function_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ function_handles ] =>
        ltac:(M.monadic
          (let function_handles := M.alloc (| function_handles |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "core::iter::adapters::map::Map")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::slice::iter::Iter")
                            []
                            [ Ty.path "move_binary_format::file_format::FunctionHandle" ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_binary_format::file_format::FunctionHandle" ]
                                ]
                            ]
                            (Ty.tuple
                              [
                                Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                                Ty.path "move_binary_format::file_format::IdentifierIndex"
                              ])
                        ]
                    ]
                  |),
                  [
                    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" ],
                        [],
                        "map",
                        [
                          Ty.tuple
                            [
                              Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                              Ty.path "move_binary_format::file_format::IdentifierIndex"
                            ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_binary_format::file_format::FunctionHandle" ]
                                ]
                            ]
                            (Ty.tuple
                              [
                                Ty.path "move_binary_format::file_format::ModuleHandleIndex";
                                Ty.path "move_binary_format::file_format::IdentifierIndex"
                              ])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionHandle" ],
                            "iter",
                            []
                          |),
                          [ M.read (| function_handles |) ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let x := M.copy (| γ |) in
                                          Value.Tuple
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::FunctionHandle",
                                                  "module"
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::FunctionHandle",
                                                  "name"
                                                |)
                                              |)
                                            ]))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::FunctionHandle" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_function_handles :
      M.IsAssociatedFunction Self "check_function_handles" check_function_handles.
    
    (*
        fn check_field_handles(&self) -> PartialVMResult<()> {
            match Self::first_duplicate_element(self.module.field_handles()) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::FieldHandle,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_field_handles (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::FieldHandle" ]
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "field_handles",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::check_duplication::DuplicationChecker",
                            "module"
                          |)
                        |)
                      ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple "move_binary_format::IndexKind::FieldHandle" [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_field_handles :
      M.IsAssociatedFunction Self "check_field_handles" check_field_handles.
    
    (*
        fn check_struct_instantiations(&self) -> PartialVMResult<()> {
            match Self::first_duplicate_element(self.module.struct_instantiations()) {
                Some(idx) => Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::StructDefInstantiation,
                    idx,
                )),
                None => Ok(()),
            }
        }
    *)
    Definition check_struct_instantiations
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                    "first_duplicate_element",
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::StructDefInstantiation" ]
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::CompiledModule",
                        "struct_instantiations",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::check_duplication::DuplicationChecker",
                            "module"
                          |)
                        |)
                      ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let idx := M.copy (| γ0_0 |) in
                    M.alloc (|
                      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::DUPLICATE_ELEMENT"
                                [];
                              Value.StructTuple
                                "move_binary_format::IndexKind::StructDefInstantiation"
                                [];
                              M.read (| idx |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_struct_instantiations :
      M.IsAssociatedFunction Self "check_struct_instantiations" check_struct_instantiations.
    
    (*
        fn check_field_instantiations(&self) -> PartialVMResult<()> {
            if let Some(idx) = Self::first_duplicate_element(self.module.field_instantiations()) {
                return Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::FieldInstantiation,
                    idx,
                ));
            }
            Ok(())
        }
    *)
    Definition check_field_instantiations
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) 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.call_closure (|
                                M.get_associated_function (|
                                  Ty.path
                                    "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                  "first_duplicate_element",
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::FieldInstantiation"
                                          ]
                                      ]
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "field_instantiations",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                          "module"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::DUPLICATE_ELEMENT"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::FieldInstantiation"
                                            [];
                                          M.read (| idx |)
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_field_instantiations :
      M.IsAssociatedFunction Self "check_field_instantiations" check_field_instantiations.
    
    (*
        fn check_struct_definitions(&self) -> PartialVMResult<()> {
            // StructDefinition - contained StructHandle defines uniqueness
            if let Some(idx) =
                Self::first_duplicate_element(self.module.struct_defs().iter().map(|x| x.struct_handle))
            {
                return Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::StructDefinition,
                    idx,
                ));
            }
            // Field names in structs must be unique
            for (struct_idx, struct_def) in self.module.struct_defs().iter().enumerate() {
                let fields = match &struct_def.field_information {
                    StructFieldInformation::Native => continue,
                    StructFieldInformation::Declared(fields) => fields,
                };
                if fields.is_empty() {
                    return Err(verification_error(
                        StatusCode::ZERO_SIZED_STRUCT,
                        IndexKind::StructDefinition,
                        struct_idx as TableIndex,
                    ));
                }
                if let Some(idx) = Self::first_duplicate_element(fields.iter().map(|x| x.name)) {
                    return Err(verification_error(
                        StatusCode::DUPLICATE_ELEMENT,
                        IndexKind::FieldDefinition,
                        idx,
                    ));
                }
            }
            // Check that each struct definition is pointing to the self module
            if let Some(idx) = self.module.struct_defs().iter().position(|x| {
                self.module.struct_handle_at(x.struct_handle).module != self.module.self_handle_idx()
            }) {
                return Err(verification_error(
                    StatusCode::INVALID_MODULE_HANDLE,
                    IndexKind::StructDefinition,
                    idx as TableIndex,
                ));
            }
            // Check that each struct handle in self module is implemented (has a declaration)
            let implemented_struct_handles: HashSet<StructHandleIndex> = self
                .module
                .struct_defs()
                .iter()
                .map(|x| x.struct_handle)
                .collect();
            if let Some(idx) = (0..self.module.struct_handles().len()).position(|x| {
                let y = StructHandleIndex::new(x as u16);
                self.module.struct_handle_at(y).module == self.module.self_handle_idx()
                    && !implemented_struct_handles.contains(&y)
            }) {
                return Err(verification_error(
                    StatusCode::UNIMPLEMENTED_HANDLE,
                    IndexKind::StructHandle,
                    idx as TableIndex,
                ));
            }
            Ok(())
        }
    *)
    Definition check_struct_definitions (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) 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.call_closure (|
                                M.get_associated_function (|
                                  Ty.path
                                    "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                  "first_duplicate_element",
                                  [
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::map::Map")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::slice::iter::Iter")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::StructDefinition"
                                          ];
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::StructDefinition"
                                                  ]
                                              ]
                                          ]
                                          (Ty.path
                                            "move_binary_format::file_format::StructHandleIndex")
                                      ]
                                  ]
                                |),
                                [
                                  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"
                                        ],
                                      [],
                                      "map",
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::StructHandleIndex";
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::StructDefinition"
                                                  ]
                                              ]
                                          ]
                                          (Ty.path
                                            "move_binary_format::file_format::StructHandleIndex")
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "slice")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::StructDefinition"
                                            ],
                                          "iter",
                                          []
                                        |),
                                        [
                                          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::check_duplication::DuplicationChecker",
                                                  "module"
                                                |)
                                              |)
                                            ]
                                          |)
                                        ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let x := M.copy (| γ |) in
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| x |),
                                                            "move_binary_format::file_format::StructDefinition",
                                                            "struct_handle"
                                                          |)
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::DUPLICATE_ELEMENT"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::StructDefinition"
                                            [];
                                          M.read (| idx |)
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (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 "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::StructDefinition" ]
                              ],
                            [],
                            "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::StructDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::StructDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    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::check_duplication::DuplicationChecker",
                                            "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::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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let struct_idx := M.copy (| γ1_0 |) in
                                          let struct_def := M.copy (| γ1_1 |) in
                                          let~ fields :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| struct_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 (|
                                                        M.never_to_any (|
                                                          M.read (| M.continue (||) |)
                                                        |)
                                                      |)));
                                                  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
                                                      fields))
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::file_format::FieldDefinition";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              "is_empty",
                                                              []
                                                            |),
                                                            [ M.read (| fields |) ]
                                                          |)
                                                        |)) 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::ZERO_SIZED_STRUCT"
                                                                      [];
                                                                    Value.StructTuple
                                                                      "move_binary_format::IndexKind::StructDefinition"
                                                                      [];
                                                                    M.rust_cast
                                                                      (M.read (| struct_idx |))
                                                                  ]
                                                                |)
                                                              ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                          "first_duplicate_element",
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::iter::adapters::map::Map")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "core::slice::iter::Iter")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::FieldDefinition"
                                                                  ];
                                                                Ty.function
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::file_format::FieldDefinition"
                                                                          ]
                                                                      ]
                                                                  ]
                                                                  (Ty.path
                                                                    "move_binary_format::file_format::IdentifierIndex")
                                                              ]
                                                          ]
                                                        |),
                                                        [
                                                          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"
                                                                ],
                                                              [],
                                                              "map",
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::IdentifierIndex";
                                                                Ty.function
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::file_format::FieldDefinition"
                                                                          ]
                                                                      ]
                                                                  ]
                                                                  (Ty.path
                                                                    "move_binary_format::file_format::IdentifierIndex")
                                                              ]
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "slice")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::FieldDefinition"
                                                                    ],
                                                                  "iter",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::deref::Deref",
                                                                      Ty.apply
                                                                        (Ty.path "alloc::vec::Vec")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "move_binary_format::file_format::FieldDefinition";
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ],
                                                                      [],
                                                                      "deref",
                                                                      []
                                                                    |),
                                                                    [ M.read (| fields |) ]
                                                                  |)
                                                                ]
                                                              |);
                                                              M.closure
                                                                (fun γ =>
                                                                  ltac:(M.monadic
                                                                    match γ with
                                                                    | [ α0 ] =>
                                                                      ltac:(M.monadic
                                                                        (M.match_operator (|
                                                                          M.alloc (| α0 |),
                                                                          [
                                                                            fun γ =>
                                                                              ltac:(M.monadic
                                                                                (let x :=
                                                                                  M.copy (| γ |) in
                                                                                M.read (|
                                                                                  M.SubPointer.get_struct_record_field (|
                                                                                    M.read (| x |),
                                                                                    "move_binary_format::file_format::FieldDefinition",
                                                                                    "name"
                                                                                  |)
                                                                                |)))
                                                                          ]
                                                                        |)))
                                                                    | _ =>
                                                                      M.impossible
                                                                        "wrong number of arguments"
                                                                    end))
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let idx := M.copy (| γ0_0 |) 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::DUPLICATE_ELEMENT"
                                                                    [];
                                                                  Value.StructTuple
                                                                    "move_binary_format::IndexKind::FieldDefinition"
                                                                    [];
                                                                  M.read (| idx |)
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            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" ],
                                  [],
                                  "position",
                                  [
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::StructDefinition"
                                              ]
                                          ]
                                      ]
                                      (Ty.path "bool")
                                  ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::StructDefinition"
                                          ],
                                        "iter",
                                        []
                                      |),
                                      [
                                        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::check_duplication::DuplicationChecker",
                                                "module"
                                              |)
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let x := M.copy (| γ |) in
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::cmp::PartialEq",
                                                        Ty.path
                                                          "move_binary_format::file_format::ModuleHandleIndex",
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::ModuleHandleIndex"
                                                        ],
                                                        "ne",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "struct_handle_at",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                  "module"
                                                                |)
                                                              |);
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| x |),
                                                                  "move_binary_format::file_format::StructDefinition",
                                                                  "struct_handle"
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          "move_binary_format::file_format::StructHandle",
                                                          "module"
                                                        |);
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "self_handle_idx",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                  "module"
                                                                |)
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      ]
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::INVALID_MODULE_HANDLE"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::StructDefinition"
                                            [];
                                          M.rust_cast (M.read (| idx |))
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ implemented_struct_handles :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::map::Map")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::StructDefinition" ];
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_binary_format::file_format::StructDefinition"
                                      ]
                                  ]
                              ]
                              (Ty.path "move_binary_format::file_format::StructHandleIndex")
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "std::collections::hash::set::HashSet")
                            []
                            [
                              Ty.path "move_binary_format::file_format::StructHandleIndex";
                              Ty.path "std::hash::random::RandomState"
                            ]
                        ]
                      |),
                      [
                        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" ],
                            [],
                            "map",
                            [
                              Ty.path "move_binary_format::file_format::StructHandleIndex";
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::StructDefinition"
                                        ]
                                    ]
                                ]
                                (Ty.path "move_binary_format::file_format::StructHandleIndex")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::StructDefinition" ],
                                "iter",
                                []
                              |),
                              [
                                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::check_duplication::DuplicationChecker",
                                        "module"
                                      |)
                                    |)
                                  ]
                                |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let x := M.copy (| γ |) in
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::StructDefinition",
                                                  "struct_handle"
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ],
                                  [],
                                  "position",
                                  [ Ty.function [ Ty.tuple [ Ty.path "usize" ] ] (Ty.path "bool") ]
                                |),
                                [
                                  M.alloc (|
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::StructHandle"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              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::check_duplication::DuplicationChecker",
                                                      "module"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |))
                                      ]
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let x := M.copy (| γ |) in
                                                    M.read (|
                                                      let~ y :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::StructHandleIndex",
                                                              "new",
                                                              []
                                                            |),
                                                            [ M.rust_cast (M.read (| x |)) ]
                                                          |)
                                                        |) in
                                                      M.alloc (|
                                                        LogicalOp.and (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::cmp::PartialEq",
                                                              Ty.path
                                                                "move_binary_format::file_format::ModuleHandleIndex",
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::ModuleHandleIndex"
                                                              ],
                                                              "eq",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "move_binary_format::file_format::CompiledModule",
                                                                    "struct_handle_at",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| self |),
                                                                        "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                        "module"
                                                                      |)
                                                                    |);
                                                                    M.read (| y |)
                                                                  ]
                                                                |),
                                                                "move_binary_format::file_format::StructHandle",
                                                                "module"
                                                              |);
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "move_binary_format::file_format::CompiledModule",
                                                                    "self_handle_idx",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| self |),
                                                                        "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                        "module"
                                                                      |)
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          ltac:(M.monadic
                                                            (UnOp.not (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "std::collections::hash::set::HashSet")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::StructHandleIndex";
                                                                      Ty.path
                                                                        "std::hash::random::RandomState"
                                                                    ],
                                                                  "contains",
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::StructHandleIndex"
                                                                  ]
                                                                |),
                                                                [ implemented_struct_handles; y ]
                                                              |)
                                                            |)))
                                                        |)
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::UNIMPLEMENTED_HANDLE"
                                            [];
                                          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.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_struct_definitions :
      M.IsAssociatedFunction Self "check_struct_definitions" check_struct_definitions.
    
    (*
        fn check_function_defintions(&self) -> PartialVMResult<()> {
            // FunctionDefinition - contained FunctionHandle defines uniqueness
            if let Some(idx) =
                Self::first_duplicate_element(self.module.function_defs().iter().map(|x| x.function))
            {
                return Err(verification_error(
                    StatusCode::DUPLICATE_ELEMENT,
                    IndexKind::FunctionDefinition,
                    idx,
                ));
            }
            // Acquires in function declarations contain unique struct definitions
            for (idx, function_def) in self.module.function_defs().iter().enumerate() {
                let acquires = function_def.acquires_global_resources.iter();
                if Self::first_duplicate_element(acquires).is_some() {
                    return Err(verification_error(
                        StatusCode::DUPLICATE_ACQUIRES_ANNOTATION,
                        IndexKind::FunctionDefinition,
                        idx as TableIndex,
                    ));
                }
            }
            // Check that each function definition is pointing to the self module
            if let Some(idx) = self.module.function_defs().iter().position(|x| {
                self.module.function_handle_at(x.function).module != self.module.self_handle_idx()
            }) {
                return Err(verification_error(
                    StatusCode::INVALID_MODULE_HANDLE,
                    IndexKind::FunctionDefinition,
                    idx as TableIndex,
                ));
            }
            // Check that each function handle in self module is implemented (has a declaration)
            let implemented_function_handles: HashSet<FunctionHandleIndex> = self
                .module
                .function_defs()
                .iter()
                .map(|x| x.function)
                .collect();
            if let Some(idx) = (0..self.module.function_handles().len()).position(|x| {
                let y = FunctionHandleIndex::new(x as u16);
                self.module.function_handle_at(y).module == self.module.self_handle_idx()
                    && !implemented_function_handles.contains(&y)
            }) {
                return Err(verification_error(
                    StatusCode::UNIMPLEMENTED_HANDLE,
                    IndexKind::FunctionHandle,
                    idx as TableIndex,
                ));
            }
            Ok(())
        }
    *)
    Definition check_function_defintions
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) 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.call_closure (|
                                M.get_associated_function (|
                                  Ty.path
                                    "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                  "first_duplicate_element",
                                  [
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::map::Map")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::slice::iter::Iter")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::FunctionDefinition"
                                          ];
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::FunctionDefinition"
                                                  ]
                                              ]
                                          ]
                                          (Ty.path
                                            "move_binary_format::file_format::FunctionHandleIndex")
                                      ]
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::FunctionDefinition"
                                        ],
                                      [],
                                      "map",
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionHandleIndex";
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::FunctionDefinition"
                                                  ]
                                              ]
                                          ]
                                          (Ty.path
                                            "move_binary_format::file_format::FunctionHandleIndex")
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "slice")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FunctionDefinition"
                                            ],
                                          "iter",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_binary_format::file_format::CompiledModule",
                                              "function_defs",
                                              []
                                            |),
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                  "module"
                                                |)
                                              |)
                                            ]
                                          |)
                                        ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let x := M.copy (| γ |) in
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| x |),
                                                            "move_binary_format::file_format::FunctionDefinition",
                                                            "function"
                                                          |)
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::DUPLICATE_ELEMENT"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::FunctionDefinition"
                                            [];
                                          M.read (| idx |)
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (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 "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::CompiledModule",
                                        "function_defs",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                            "module"
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let idx := M.copy (| γ1_0 |) in
                                          let function_def := M.copy (| γ1_1 |) in
                                          let~ acquires :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "slice")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_binary_format::file_format::StructDefinitionIndex"
                                                    ],
                                                  "iter",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::deref::Deref",
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::StructDefinitionIndex";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [],
                                                      "deref",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| function_def |),
                                                        "move_binary_format::file_format::FunctionDefinition",
                                                        "acquires_global_resources"
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "u16" ],
                                                            "is_some",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path
                                                                    "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                  "first_duplicate_element",
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::slice::iter::Iter")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "move_binary_format::file_format::StructDefinitionIndex"
                                                                      ]
                                                                  ]
                                                                |),
                                                                [ M.read (| acquires |) ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      |)) 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::DUPLICATE_ACQUIRES_ANNOTATION"
                                                                    [];
                                                                  Value.StructTuple
                                                                    "move_binary_format::IndexKind::FunctionDefinition"
                                                                    [];
                                                                  M.rust_cast (M.read (| idx |))
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [ Ty.path "move_binary_format::file_format::FunctionDefinition"
                                    ],
                                  [],
                                  "position",
                                  [
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::FunctionDefinition"
                                              ]
                                          ]
                                      ]
                                      (Ty.path "bool")
                                  ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::FunctionDefinition"
                                          ],
                                        "iter",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "function_defs",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                "module"
                                              |)
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let x := M.copy (| γ |) in
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::cmp::PartialEq",
                                                        Ty.path
                                                          "move_binary_format::file_format::ModuleHandleIndex",
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::ModuleHandleIndex"
                                                        ],
                                                        "ne",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "function_handle_at",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                  "module"
                                                                |)
                                                              |);
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| x |),
                                                                  "move_binary_format::file_format::FunctionDefinition",
                                                                  "function"
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          "move_binary_format::file_format::FunctionHandle",
                                                          "module"
                                                        |);
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "self_handle_idx",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                  "module"
                                                                |)
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      ]
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::INVALID_MODULE_HANDLE"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::FunctionDefinition"
                                            [];
                                          M.rust_cast (M.read (| idx |))
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ implemented_function_handles :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::map::Map")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ];
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ]
                                  ]
                              ]
                              (Ty.path "move_binary_format::file_format::FunctionHandleIndex")
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "std::collections::hash::set::HashSet")
                            []
                            [
                              Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                              Ty.path "std::hash::random::RandomState"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                            [],
                            "map",
                            [
                              Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::FunctionDefinition"
                                        ]
                                    ]
                                ]
                                (Ty.path "move_binary_format::file_format::FunctionHandleIndex")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::file_format::CompiledModule",
                                    "function_defs",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                        "module"
                                      |)
                                    |)
                                  ]
                                |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let x := M.copy (| γ |) in
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| x |),
                                                  "move_binary_format::file_format::FunctionDefinition",
                                                  "function"
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ],
                                  [],
                                  "position",
                                  [ Ty.function [ Ty.tuple [ Ty.path "usize" ] ] (Ty.path "bool") ]
                                |),
                                [
                                  M.alloc (|
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionHandle"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              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::check_duplication::DuplicationChecker",
                                                      "module"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |))
                                      ]
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let x := M.copy (| γ |) in
                                                    M.read (|
                                                      let~ y :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::FunctionHandleIndex",
                                                              "new",
                                                              []
                                                            |),
                                                            [ M.rust_cast (M.read (| x |)) ]
                                                          |)
                                                        |) in
                                                      M.alloc (|
                                                        LogicalOp.and (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::cmp::PartialEq",
                                                              Ty.path
                                                                "move_binary_format::file_format::ModuleHandleIndex",
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::ModuleHandleIndex"
                                                              ],
                                                              "eq",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "move_binary_format::file_format::CompiledModule",
                                                                    "function_handle_at",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| self |),
                                                                        "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                        "module"
                                                                      |)
                                                                    |);
                                                                    M.read (| y |)
                                                                  ]
                                                                |),
                                                                "move_binary_format::file_format::FunctionHandle",
                                                                "module"
                                                              |);
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "move_binary_format::file_format::CompiledModule",
                                                                    "self_handle_idx",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| self |),
                                                                        "move_bytecode_verifier::check_duplication::DuplicationChecker",
                                                                        "module"
                                                                      |)
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            ]
                                                          |),
                                                          ltac:(M.monadic
                                                            (UnOp.not (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "std::collections::hash::set::HashSet")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::FunctionHandleIndex";
                                                                      Ty.path
                                                                        "std::hash::random::RandomState"
                                                                    ],
                                                                  "contains",
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::FunctionHandleIndex"
                                                                  ]
                                                                |),
                                                                [ implemented_function_handles; y ]
                                                              |)
                                                            |)))
                                                        |)
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let idx := M.copy (| γ0_0 |) 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::UNIMPLEMENTED_HANDLE"
                                            [];
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::FunctionHandle"
                                            [];
                                          M.rust_cast (M.read (| idx |))
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_function_defintions :
      M.IsAssociatedFunction Self "check_function_defintions" check_function_defintions.
    
    (*
        fn first_duplicate_element<T>(iter: T) -> Option<TableIndex>
        where
            T: IntoIterator,
            T::Item: Eq + Hash,
        {
            let mut uniq = HashSet::new();
            for (i, x) in iter.into_iter().enumerate() {
                if !uniq.insert(x) {
                    return Some(i as TableIndex);
                }
            }
            None
        }
    *)
    Definition first_duplicate_element (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ uniq :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::set::HashSet")
                          []
                          [ Ty.associated; Ty.path "std::hash::random::RandomState" ],
                        "new",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [ Ty.associated ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.associated,
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    T,
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [ M.read (| iter |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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.associated ],
                                          [],
                                          "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 i := M.copy (| γ1_0 |) in
                                          let x := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "std::collections::hash::set::HashSet")
                                                                []
                                                                [
                                                                  Ty.associated;
                                                                  Ty.path
                                                                    "std::hash::random::RandomState"
                                                                ],
                                                              "insert",
                                                              []
                                                            |),
                                                            [ uniq; M.read (| x |) ]
                                                          |)
                                                        |)
                                                      |)) 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::option::Option::Some"
                                                            [ M.rust_cast (M.read (| i |)) ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_first_duplicate_element :
      M.IsAssociatedFunction Self "first_duplicate_element" first_duplicate_element.
  End Impl_move_bytecode_verifier_check_duplication_DuplicationChecker.
End check_duplication.
