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

Module signature.
  (* StructRecord
    {
      name := "SignatureChecker";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("abilities_cache",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "move_binary_format::file_format::SignatureIndex";
                Ty.apply
                  (Ty.path "std::collections::hash::set::HashSet")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_binary_format::file_format::AbilitySet";
                        Ty.path "alloc::alloc::Global"
                      ];
                    Ty.path "std::hash::random::RandomState"
                  ];
                Ty.path "std::hash::random::RandomState"
              ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_signature_SignatureChecker.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::signature::SignatureChecker".
    
    (*
        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::signature::SignatureChecker",
                  "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<()> {
            let mut sig_check = Self {
                module,
                abilities_cache: HashMap::new(),
            };
            sig_check.verify_signature_pool(module.signatures())?;
            sig_check.verify_function_signatures(module.function_handles())?;
            sig_check.verify_fields(module.struct_defs())?;
            sig_check.verify_code_units(module.function_handles(), module.function_defs())
        }
    *)
    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~ sig_check :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::signature::SignatureChecker"
                      [
                        ("module", M.read (| module |));
                        ("abilities_cache",
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "std::collections::hash::map::HashMap")
                                []
                                [
                                  Ty.path "move_binary_format::file_format::SignatureIndex";
                                  Ty.apply
                                    (Ty.path "std::collections::hash::set::HashSet")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_binary_format::file_format::AbilitySet";
                                          Ty.path "alloc::alloc::Global"
                                        ];
                                      Ty.path "std::hash::random::RandomState"
                                    ];
                                  Ty.path "std::hash::random::RandomState"
                                ],
                              "new",
                              []
                            |),
                            []
                          |))
                      ]
                  |) 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::signature::SignatureChecker",
                              "verify_signature_pool",
                              []
                            |),
                            [
                              sig_check;
                              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::signature::SignatureChecker",
                              "verify_function_signatures",
                              []
                            |),
                            [
                              sig_check;
                              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::signature::SignatureChecker",
                              "verify_fields",
                              []
                            |),
                            [
                              sig_check;
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "struct_defs",
                                  []
                                |),
                                [ 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
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                      "verify_code_units",
                      []
                    |),
                    [
                      sig_check;
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_binary_format::file_format::CompiledModule",
                          "function_handles",
                          []
                        |),
                        [ M.read (| module |) ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_binary_format::file_format::CompiledModule",
                          "function_defs",
                          []
                        |),
                        [ M.read (| module |) ]
                      |)
                    ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn verify_signature_pool(&self, signatures: &[Signature]) -> PartialVMResult<()> {
            for i in 0..signatures.len() {
                self.check_signature(SignatureIndex::new(i as TableIndex))?
            }
            Ok(())
        }
    *)
    Definition verify_signature_pool (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; signatures ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let signatures := M.alloc (| signatures |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            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::Signature" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| signatures |) ]
                                  |))
                              ]
                          ]
                        |)
                      |),
                      [
                        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::ops::range::Range")
                                            []
                                            [ Ty.path "usize" ],
                                          [],
                                          "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 i := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_bytecode_verifier::signature::SignatureChecker",
                                                      "check_signature",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| self |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::SignatureIndex",
                                                          "new",
                                                          []
                                                        |),
                                                        [ M.rust_cast (M.read (| i |)) ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_signature_pool :
      M.IsAssociatedFunction Self "verify_signature_pool" verify_signature_pool.
    
    (*
        fn verify_function_signatures(
            &mut self,
            function_handles: &[FunctionHandle],
        ) -> PartialVMResult<()> {
            let err_handler = |err: PartialVMError, idx| {
                err.at_index(IndexKind::Signature, idx as TableIndex)
                    .at_index(IndexKind::FunctionHandle, idx as TableIndex)
            };
    
            for (idx, fh) in function_handles.iter().enumerate() {
                self.check_instantiation(fh.return_, &fh.type_parameters)
                    .map_err(|err| err_handler(err, idx))?;
                self.check_instantiation(fh.parameters, &fh.type_parameters)
                    .map_err(|err| err_handler(err, idx))?;
                if !fh.type_parameters.is_empty() {}
            }
            Ok(())
        }
    *)
    Definition verify_function_signatures
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; function_handles ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let function_handles := M.alloc (| function_handles |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ err_handler :=
                  M.alloc (|
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let err := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let idx := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "at_index",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError",
                                                      "at_index",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| err |);
                                                      Value.StructTuple
                                                        "move_binary_format::IndexKind::Signature"
                                                        [];
                                                      M.rust_cast (M.read (| idx |))
                                                    ]
                                                  |);
                                                  Value.StructTuple
                                                    "move_binary_format::IndexKind::FunctionHandle"
                                                    [];
                                                  M.rust_cast (M.read (| idx |))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |) 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::FunctionHandle" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionHandle" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::FunctionHandle" ],
                                    "iter",
                                    []
                                  |),
                                  [ M.read (| function_handles |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionHandle"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let idx := M.copy (| γ1_0 |) in
                                          let fh := M.copy (| γ1_1 |) 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.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [
                                                            Ty.tuple [];
                                                            Ty.path
                                                              "move_binary_format::errors::PartialVMError"
                                                          ],
                                                        "map_err",
                                                        [
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError";
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ]
                                                            ]
                                                            (Ty.path
                                                              "move_binary_format::errors::PartialVMError")
                                                        ]
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                            "check_instantiation",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| self |);
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| fh |),
                                                                "move_binary_format::file_format::FunctionHandle",
                                                                "return_"
                                                              |)
                                                            |);
                                                            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::AbilitySet";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                [],
                                                                "deref",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| fh |),
                                                                  "move_binary_format::file_format::FunctionHandle",
                                                                  "type_parameters"
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |);
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ α0 ] =>
                                                                ltac:(M.monadic
                                                                  (M.match_operator (|
                                                                    M.alloc (| α0 |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let err :=
                                                                            M.copy (| γ |) in
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::ops::function::Fn",
                                                                              Ty.function
                                                                                [
                                                                                  Ty.tuple
                                                                                    [
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError";
                                                                                      Ty.path
                                                                                        "usize"
                                                                                    ]
                                                                                ]
                                                                                (Ty.path
                                                                                  "move_binary_format::errors::PartialVMError"),
                                                                              [
                                                                                Ty.tuple
                                                                                  [
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError";
                                                                                    Ty.path "usize"
                                                                                  ]
                                                                              ],
                                                                              "call",
                                                                              []
                                                                            |),
                                                                            [
                                                                              err_handler;
                                                                              Value.Tuple
                                                                                [
                                                                                  M.read (| err |);
                                                                                  M.read (| idx |)
                                                                                ]
                                                                            ]
                                                                          |)))
                                                                    ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple [];
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path
                                                                        "move_binary_format::errors::PartialVMError"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |) in
                                          let~ _ :=
                                            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.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [
                                                            Ty.tuple [];
                                                            Ty.path
                                                              "move_binary_format::errors::PartialVMError"
                                                          ],
                                                        "map_err",
                                                        [
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError";
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ]
                                                            ]
                                                            (Ty.path
                                                              "move_binary_format::errors::PartialVMError")
                                                        ]
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                            "check_instantiation",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| self |);
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| fh |),
                                                                "move_binary_format::file_format::FunctionHandle",
                                                                "parameters"
                                                              |)
                                                            |);
                                                            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::AbilitySet";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                [],
                                                                "deref",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| fh |),
                                                                  "move_binary_format::file_format::FunctionHandle",
                                                                  "type_parameters"
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |);
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ α0 ] =>
                                                                ltac:(M.monadic
                                                                  (M.match_operator (|
                                                                    M.alloc (| α0 |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let err :=
                                                                            M.copy (| γ |) in
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::ops::function::Fn",
                                                                              Ty.function
                                                                                [
                                                                                  Ty.tuple
                                                                                    [
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError";
                                                                                      Ty.path
                                                                                        "usize"
                                                                                    ]
                                                                                ]
                                                                                (Ty.path
                                                                                  "move_binary_format::errors::PartialVMError"),
                                                                              [
                                                                                Ty.tuple
                                                                                  [
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError";
                                                                                    Ty.path "usize"
                                                                                  ]
                                                                              ],
                                                                              "call",
                                                                              []
                                                                            |),
                                                                            [
                                                                              err_handler;
                                                                              Value.Tuple
                                                                                [
                                                                                  M.read (| err |);
                                                                                  M.read (| idx |)
                                                                                ]
                                                                            ]
                                                                          |)))
                                                                    ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple [];
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path
                                                                        "move_binary_format::errors::PartialVMError"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::file_format::AbilitySet";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              "is_empty",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| fh |),
                                                                "move_binary_format::file_format::FunctionHandle",
                                                                "type_parameters"
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_function_signatures :
      M.IsAssociatedFunction Self "verify_function_signatures" verify_function_signatures.
    
    (*
        fn verify_fields(&self, struct_defs: &[StructDefinition]) -> PartialVMResult<()> {
            for (struct_def_idx, struct_def) in struct_defs.iter().enumerate() {
                let fields = match &struct_def.field_information {
                    StructFieldInformation::Native => continue,
                    StructFieldInformation::Declared(fields) => fields,
                };
                let struct_handle = self.module.struct_handle_at(struct_def.struct_handle);
                let err_handler = |err: PartialVMError, idx| {
                    err.at_index(IndexKind::FieldDefinition, idx as TableIndex)
                        .at_index(IndexKind::StructDefinition, struct_def_idx as TableIndex)
                };
                for (field_offset, field_def) in fields.iter().enumerate() {
                    self.check_signature_token(&field_def.signature.0)
                        .map_err(|err| err_handler(err, field_offset))?;
                    let type_param_constraints: Vec<_> =
                        struct_handle.type_param_constraints().collect();
                    self.check_type_instantiation(&field_def.signature.0, &type_param_constraints)
                        .map_err(|err| err_handler(err, field_offset))?;
    
                    self.check_phantom_params(
                        &field_def.signature.0,
                        false,
                        &struct_handle.type_parameters,
                    )
                    .map_err(|err| err_handler(err, field_offset))?;
                }
            }
            Ok(())
        }
    *)
    Definition verify_fields (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; struct_defs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let struct_defs := M.alloc (| struct_defs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::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.read (| struct_defs |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::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_def_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~ struct_handle :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::CompiledModule",
                                                  "struct_handle_at",
                                                  []
                                                |),
                                                [
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "move_bytecode_verifier::signature::SignatureChecker",
                                                      "module"
                                                    |)
                                                  |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| struct_def |),
                                                      "move_binary_format::file_format::StructDefinition",
                                                      "struct_handle"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let~ err_handler :=
                                            M.alloc (|
                                              M.closure
                                                (fun γ =>
                                                  ltac:(M.monadic
                                                    match γ with
                                                    | [ α0; α1 ] =>
                                                      ltac:(M.monadic
                                                        (M.match_operator (|
                                                          M.alloc (| α0 |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let err := M.copy (| γ |) in
                                                                M.match_operator (|
                                                                  M.alloc (| α1 |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let idx :=
                                                                          M.copy (| γ |) in
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "at_index",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "at_index",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| err |);
                                                                                Value.StructTuple
                                                                                  "move_binary_format::IndexKind::FieldDefinition"
                                                                                  [];
                                                                                M.rust_cast
                                                                                  (M.read (| idx |))
                                                                              ]
                                                                            |);
                                                                            Value.StructTuple
                                                                              "move_binary_format::IndexKind::StructDefinition"
                                                                              [];
                                                                            M.rust_cast
                                                                              (M.read (|
                                                                                struct_def_idx
                                                                              |))
                                                                          ]
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                    | _ => M.impossible "wrong number of arguments"
                                                    end))
                                            |) in
                                          M.use
                                            (M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::collect::IntoIterator",
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::iter::adapters::enumerate::Enumerate")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::slice::iter::Iter")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_binary_format::file_format::FieldDefinition"
                                                          ]
                                                      ],
                                                    [],
                                                    "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::FieldDefinition"
                                                          ],
                                                        [],
                                                        "enumerate",
                                                        []
                                                      |),
                                                      [
                                                        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 |) ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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::FieldDefinition"
                                                                        ]
                                                                    ],
                                                                  [],
                                                                  "next",
                                                                  []
                                                                |),
                                                                [ iter ]
                                                              |)
                                                            |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let _ :=
                                                                    M.is_struct_tuple (|
                                                                      γ,
                                                                      "core::option::Option::None"
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (| M.break (||) |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::option::Option::Some",
                                                                      0
                                                                    |) in
                                                                  let γ1_0 :=
                                                                    M.SubPointer.get_tuple_field (|
                                                                      γ0_0,
                                                                      0
                                                                    |) in
                                                                  let γ1_1 :=
                                                                    M.SubPointer.get_tuple_field (|
                                                                      γ0_0,
                                                                      1
                                                                    |) in
                                                                  let field_offset :=
                                                                    M.copy (| γ1_0 |) in
                                                                  let field_def :=
                                                                    M.copy (| γ1_1 |) 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.apply
                                                                                  (Ty.path
                                                                                    "core::result::Result")
                                                                                  []
                                                                                  [
                                                                                    Ty.tuple [];
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                  ],
                                                                                "map_err",
                                                                                [
                                                                                  Ty.path
                                                                                    "move_binary_format::errors::PartialVMError";
                                                                                  Ty.function
                                                                                    [
                                                                                      Ty.tuple
                                                                                        [
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError"
                                                                                        ]
                                                                                    ]
                                                                                    (Ty.path
                                                                                      "move_binary_format::errors::PartialVMError")
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "move_bytecode_verifier::signature::SignatureChecker",
                                                                                    "check_signature_token",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      self
                                                                                    |);
                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                      M.SubPointer.get_struct_record_field (|
                                                                                        M.read (|
                                                                                          field_def
                                                                                        |),
                                                                                        "move_binary_format::file_format::FieldDefinition",
                                                                                        "signature"
                                                                                      |),
                                                                                      "move_binary_format::file_format::TypeSignature",
                                                                                      0
                                                                                    |)
                                                                                  ]
                                                                                |);
                                                                                M.closure
                                                                                  (fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      match γ with
                                                                                      | [ α0 ] =>
                                                                                        ltac:(M.monadic
                                                                                          (M.match_operator (|
                                                                                            M.alloc (|
                                                                                              α0
                                                                                            |),
                                                                                            [
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        err :=
                                                                                                    M.copy (|
                                                                                                      γ
                                                                                                    |) in
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::function::Fn",
                                                                                                      Ty.function
                                                                                                        [
                                                                                                          Ty.tuple
                                                                                                            [
                                                                                                              Ty.path
                                                                                                                "move_binary_format::errors::PartialVMError";
                                                                                                              Ty.path
                                                                                                                "usize"
                                                                                                            ]
                                                                                                        ]
                                                                                                        (Ty.path
                                                                                                          "move_binary_format::errors::PartialVMError"),
                                                                                                      [
                                                                                                        Ty.tuple
                                                                                                          [
                                                                                                            Ty.path
                                                                                                              "move_binary_format::errors::PartialVMError";
                                                                                                            Ty.path
                                                                                                              "usize"
                                                                                                          ]
                                                                                                      ],
                                                                                                      "call",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      err_handler;
                                                                                                      Value.Tuple
                                                                                                        [
                                                                                                          M.read (|
                                                                                                            err
                                                                                                          |);
                                                                                                          M.read (|
                                                                                                            field_offset
                                                                                                          |)
                                                                                                        ]
                                                                                                    ]
                                                                                                  |)))
                                                                                            ]
                                                                                          |)))
                                                                                      | _ =>
                                                                                        M.impossible
                                                                                          "wrong number of arguments"
                                                                                      end))
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                                0
                                                                              |) in
                                                                            let residual :=
                                                                              M.copy (| γ0_0 |) in
                                                                            M.alloc (|
                                                                              M.never_to_any (|
                                                                                M.read (|
                                                                                  M.return_ (|
                                                                                    M.call_closure (|
                                                                                      M.get_trait_method (|
                                                                                        "core::ops::try_trait::FromResidual",
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "core::result::Result")
                                                                                          []
                                                                                          [
                                                                                            Ty.tuple
                                                                                              [];
                                                                                            Ty.path
                                                                                              "move_binary_format::errors::PartialVMError"
                                                                                          ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::result::Result")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible";
                                                                                              Ty.path
                                                                                                "move_binary_format::errors::PartialVMError"
                                                                                            ]
                                                                                        ],
                                                                                        "from_residual",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.read (|
                                                                                          residual
                                                                                        |)
                                                                                      ]
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)
                                                                            |)));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                                0
                                                                              |) in
                                                                            let val :=
                                                                              M.copy (| γ0_0 |) in
                                                                            val))
                                                                      ]
                                                                    |) in
                                                                  let~ type_param_constraints :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::iter::traits::iterator::Iterator",
                                                                          Ty.associated,
                                                                          [],
                                                                          "collect",
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "alloc::vec::Vec")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "move_binary_format::file_format::AbilitySet";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ]
                                                                          ]
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_binary_format::file_format::StructHandle",
                                                                              "type_param_constraints",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (|
                                                                                struct_handle
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) 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.apply
                                                                                  (Ty.path
                                                                                    "core::result::Result")
                                                                                  []
                                                                                  [
                                                                                    Ty.tuple [];
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                  ],
                                                                                "map_err",
                                                                                [
                                                                                  Ty.path
                                                                                    "move_binary_format::errors::PartialVMError";
                                                                                  Ty.function
                                                                                    [
                                                                                      Ty.tuple
                                                                                        [
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError"
                                                                                        ]
                                                                                    ]
                                                                                    (Ty.path
                                                                                      "move_binary_format::errors::PartialVMError")
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "move_bytecode_verifier::signature::SignatureChecker",
                                                                                    "check_type_instantiation",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      self
                                                                                    |);
                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                      M.SubPointer.get_struct_record_field (|
                                                                                        M.read (|
                                                                                          field_def
                                                                                        |),
                                                                                        "move_binary_format::file_format::FieldDefinition",
                                                                                        "signature"
                                                                                      |),
                                                                                      "move_binary_format::file_format::TypeSignature",
                                                                                      0
                                                                                    |);
                                                                                    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::AbilitySet";
                                                                                            Ty.path
                                                                                              "alloc::alloc::Global"
                                                                                          ],
                                                                                        [],
                                                                                        "deref",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        type_param_constraints
                                                                                      ]
                                                                                    |)
                                                                                  ]
                                                                                |);
                                                                                M.closure
                                                                                  (fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      match γ with
                                                                                      | [ α0 ] =>
                                                                                        ltac:(M.monadic
                                                                                          (M.match_operator (|
                                                                                            M.alloc (|
                                                                                              α0
                                                                                            |),
                                                                                            [
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        err :=
                                                                                                    M.copy (|
                                                                                                      γ
                                                                                                    |) in
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::function::Fn",
                                                                                                      Ty.function
                                                                                                        [
                                                                                                          Ty.tuple
                                                                                                            [
                                                                                                              Ty.path
                                                                                                                "move_binary_format::errors::PartialVMError";
                                                                                                              Ty.path
                                                                                                                "usize"
                                                                                                            ]
                                                                                                        ]
                                                                                                        (Ty.path
                                                                                                          "move_binary_format::errors::PartialVMError"),
                                                                                                      [
                                                                                                        Ty.tuple
                                                                                                          [
                                                                                                            Ty.path
                                                                                                              "move_binary_format::errors::PartialVMError";
                                                                                                            Ty.path
                                                                                                              "usize"
                                                                                                          ]
                                                                                                      ],
                                                                                                      "call",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      err_handler;
                                                                                                      Value.Tuple
                                                                                                        [
                                                                                                          M.read (|
                                                                                                            err
                                                                                                          |);
                                                                                                          M.read (|
                                                                                                            field_offset
                                                                                                          |)
                                                                                                        ]
                                                                                                    ]
                                                                                                  |)))
                                                                                            ]
                                                                                          |)))
                                                                                      | _ =>
                                                                                        M.impossible
                                                                                          "wrong number of arguments"
                                                                                      end))
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                                0
                                                                              |) in
                                                                            let residual :=
                                                                              M.copy (| γ0_0 |) in
                                                                            M.alloc (|
                                                                              M.never_to_any (|
                                                                                M.read (|
                                                                                  M.return_ (|
                                                                                    M.call_closure (|
                                                                                      M.get_trait_method (|
                                                                                        "core::ops::try_trait::FromResidual",
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "core::result::Result")
                                                                                          []
                                                                                          [
                                                                                            Ty.tuple
                                                                                              [];
                                                                                            Ty.path
                                                                                              "move_binary_format::errors::PartialVMError"
                                                                                          ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::result::Result")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible";
                                                                                              Ty.path
                                                                                                "move_binary_format::errors::PartialVMError"
                                                                                            ]
                                                                                        ],
                                                                                        "from_residual",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.read (|
                                                                                          residual
                                                                                        |)
                                                                                      ]
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)
                                                                            |)));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                                0
                                                                              |) in
                                                                            let val :=
                                                                              M.copy (| γ0_0 |) in
                                                                            val))
                                                                      ]
                                                                    |) in
                                                                  let~ _ :=
                                                                    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.apply
                                                                                  (Ty.path
                                                                                    "core::result::Result")
                                                                                  []
                                                                                  [
                                                                                    Ty.tuple [];
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                  ],
                                                                                "map_err",
                                                                                [
                                                                                  Ty.path
                                                                                    "move_binary_format::errors::PartialVMError";
                                                                                  Ty.function
                                                                                    [
                                                                                      Ty.tuple
                                                                                        [
                                                                                          Ty.path
                                                                                            "move_binary_format::errors::PartialVMError"
                                                                                        ]
                                                                                    ]
                                                                                    (Ty.path
                                                                                      "move_binary_format::errors::PartialVMError")
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "move_bytecode_verifier::signature::SignatureChecker",
                                                                                    "check_phantom_params",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      self
                                                                                    |);
                                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                                      M.SubPointer.get_struct_record_field (|
                                                                                        M.read (|
                                                                                          field_def
                                                                                        |),
                                                                                        "move_binary_format::file_format::FieldDefinition",
                                                                                        "signature"
                                                                                      |),
                                                                                      "move_binary_format::file_format::TypeSignature",
                                                                                      0
                                                                                    |);
                                                                                    Value.Bool
                                                                                      false;
                                                                                    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::StructTypeParameter";
                                                                                            Ty.path
                                                                                              "alloc::alloc::Global"
                                                                                          ],
                                                                                        [],
                                                                                        "deref",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.SubPointer.get_struct_record_field (|
                                                                                          M.read (|
                                                                                            struct_handle
                                                                                          |),
                                                                                          "move_binary_format::file_format::StructHandle",
                                                                                          "type_parameters"
                                                                                        |)
                                                                                      ]
                                                                                    |)
                                                                                  ]
                                                                                |);
                                                                                M.closure
                                                                                  (fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      match γ with
                                                                                      | [ α0 ] =>
                                                                                        ltac:(M.monadic
                                                                                          (M.match_operator (|
                                                                                            M.alloc (|
                                                                                              α0
                                                                                            |),
                                                                                            [
                                                                                              fun
                                                                                                  γ =>
                                                                                                ltac:(M.monadic
                                                                                                  (let
                                                                                                        err :=
                                                                                                    M.copy (|
                                                                                                      γ
                                                                                                    |) in
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::function::Fn",
                                                                                                      Ty.function
                                                                                                        [
                                                                                                          Ty.tuple
                                                                                                            [
                                                                                                              Ty.path
                                                                                                                "move_binary_format::errors::PartialVMError";
                                                                                                              Ty.path
                                                                                                                "usize"
                                                                                                            ]
                                                                                                        ]
                                                                                                        (Ty.path
                                                                                                          "move_binary_format::errors::PartialVMError"),
                                                                                                      [
                                                                                                        Ty.tuple
                                                                                                          [
                                                                                                            Ty.path
                                                                                                              "move_binary_format::errors::PartialVMError";
                                                                                                            Ty.path
                                                                                                              "usize"
                                                                                                          ]
                                                                                                      ],
                                                                                                      "call",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      err_handler;
                                                                                                      Value.Tuple
                                                                                                        [
                                                                                                          M.read (|
                                                                                                            err
                                                                                                          |);
                                                                                                          M.read (|
                                                                                                            field_offset
                                                                                                          |)
                                                                                                        ]
                                                                                                    ]
                                                                                                  |)))
                                                                                            ]
                                                                                          |)))
                                                                                      | _ =>
                                                                                        M.impossible
                                                                                          "wrong number of arguments"
                                                                                      end))
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Break",
                                                                                0
                                                                              |) in
                                                                            let residual :=
                                                                              M.copy (| γ0_0 |) in
                                                                            M.alloc (|
                                                                              M.never_to_any (|
                                                                                M.read (|
                                                                                  M.return_ (|
                                                                                    M.call_closure (|
                                                                                      M.get_trait_method (|
                                                                                        "core::ops::try_trait::FromResidual",
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "core::result::Result")
                                                                                          []
                                                                                          [
                                                                                            Ty.tuple
                                                                                              [];
                                                                                            Ty.path
                                                                                              "move_binary_format::errors::PartialVMError"
                                                                                          ],
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::result::Result")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "core::convert::Infallible";
                                                                                              Ty.path
                                                                                                "move_binary_format::errors::PartialVMError"
                                                                                            ]
                                                                                        ],
                                                                                        "from_residual",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.read (|
                                                                                          residual
                                                                                        |)
                                                                                      ]
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)
                                                                            |)));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ0_0 :=
                                                                              M.SubPointer.get_struct_tuple_field (|
                                                                                γ,
                                                                                "core::ops::control_flow::ControlFlow::Continue",
                                                                                0
                                                                              |) in
                                                                            let val :=
                                                                              M.copy (| γ0_0 |) in
                                                                            val))
                                                                      ]
                                                                    |) in
                                                                  M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                    |)))
                                              ]
                                            |))))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_fields :
      M.IsAssociatedFunction Self "verify_fields" verify_fields.
    
    (*
        fn verify_code_units(
            &mut self,
            function_handles: &[FunctionHandle],
            function_defs: &[FunctionDefinition],
        ) -> PartialVMResult<()> {
            for (func_def_idx, func_def) in function_defs.iter().enumerate() {
                // skip native functions
                let code = match &func_def.code {
                    Some(code) => code,
                    None => continue,
                };
                let func_handle = &function_handles[func_def.function.0 as usize];
                self.verify_code(code, &func_handle.type_parameters)
                    .map_err(|err| {
                        err.at_index(IndexKind::Signature, code.locals.0)
                            .at_index(IndexKind::FunctionDefinition, func_def_idx as TableIndex)
                    })?
            }
            Ok(())
        }
    *)
    Definition verify_code_units (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; function_handles; function_defs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let function_handles := M.alloc (| function_handles |) in
          let function_defs := M.alloc (| function_defs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [ M.read (| function_defs |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::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 func_def_idx := M.copy (| γ1_0 |) in
                                          let func_def := M.copy (| γ1_1 |) in
                                          let~ code :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| func_def |),
                                                    "move_binary_format::file_format::FunctionDefinition",
                                                    "code"
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ := M.read (| γ |) in
                                                      let γ1_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::option::Option::Some",
                                                          0
                                                        |) in
                                                      let code := M.alloc (| γ1_0 |) in
                                                      code));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ := M.read (| γ |) in
                                                      let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::option::Option::None"
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (| M.continue (||) |)
                                                        |)
                                                      |)))
                                                ]
                                              |)
                                            |) in
                                          let~ func_handle :=
                                            M.alloc (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| function_handles |),
                                                M.alloc (|
                                                  M.rust_cast
                                                    (M.read (|
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| func_def |),
                                                          "move_binary_format::file_format::FunctionDefinition",
                                                          "function"
                                                        |),
                                                        "move_binary_format::file_format::FunctionHandleIndex",
                                                        0
                                                      |)
                                                    |))
                                                |)
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.tuple [];
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError"
                                                        ],
                                                      "map_err",
                                                      [
                                                        Ty.path
                                                          "move_binary_format::errors::PartialVMError";
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ]
                                                          ]
                                                          (Ty.path
                                                            "move_binary_format::errors::PartialVMError")
                                                      ]
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_bytecode_verifier::signature::SignatureChecker",
                                                          "verify_code",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| self |);
                                                          M.read (| code |);
                                                          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::AbilitySet";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              [],
                                                              "deref",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| func_handle |),
                                                                "move_binary_format::file_format::FunctionHandle",
                                                                "type_parameters"
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |);
                                                      M.closure
                                                        (fun γ =>
                                                          ltac:(M.monadic
                                                            match γ with
                                                            | [ α0 ] =>
                                                              ltac:(M.monadic
                                                                (M.match_operator (|
                                                                  M.alloc (| α0 |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let err :=
                                                                          M.copy (| γ |) in
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "at_index",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "at_index",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| err |);
                                                                                Value.StructTuple
                                                                                  "move_binary_format::IndexKind::Signature"
                                                                                  [];
                                                                                M.read (|
                                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                                    M.SubPointer.get_struct_record_field (|
                                                                                      M.read (|
                                                                                        code
                                                                                      |),
                                                                                      "move_binary_format::file_format::CodeUnit",
                                                                                      "locals"
                                                                                    |),
                                                                                    "move_binary_format::file_format::SignatureIndex",
                                                                                    0
                                                                                  |)
                                                                                |)
                                                                              ]
                                                                            |);
                                                                            Value.StructTuple
                                                                              "move_binary_format::IndexKind::FunctionDefinition"
                                                                              [];
                                                                            M.rust_cast
                                                                              (M.read (|
                                                                                func_def_idx
                                                                              |))
                                                                          ]
                                                                        |)))
                                                                  ]
                                                                |)))
                                                            | _ =>
                                                              M.impossible
                                                                "wrong number of arguments"
                                                            end))
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_code_units :
      M.IsAssociatedFunction Self "verify_code_units" verify_code_units.
    
    (*
        fn verify_code(
            &mut self,
            code: &CodeUnit,
            type_parameters: &[AbilitySet],
        ) -> PartialVMResult<()> {
            self.check_instantiation(code.locals, type_parameters)?;
    
            // Check if the type actuals in certain bytecode instructions are well defined.
            use Bytecode::*;
            for (offset, instr) in code.code.iter().enumerate() {
                let result = match instr {
                    CallGeneric(idx) => {
                        let func_inst = self.module.function_instantiation_at( *idx);
                        let func_handle = self.module.function_handle_at(func_inst.handle);
                        let type_arguments = &self.module.signature_at(func_inst.type_parameters).0;
                        self.check_signature_tokens(type_arguments)?;
                        self.check_generic_instance(
                            type_arguments,
                            func_handle.type_parameters.iter().copied(),
                            type_parameters,
                        )
                    }
                    PackGeneric(idx)
                    | UnpackGeneric(idx)
                    | ExistsGenericDeprecated(idx)
                    | MoveFromGenericDeprecated(idx)
                    | MoveToGenericDeprecated(idx)
                    | ImmBorrowGlobalGenericDeprecated(idx)
                    | MutBorrowGlobalGenericDeprecated(idx) => {
                        let struct_inst = self.module.struct_instantiation_at( *idx);
                        let struct_def = self.module.struct_def_at(struct_inst.def);
                        let struct_handle = self.module.struct_handle_at(struct_def.struct_handle);
                        let type_arguments = &self.module.signature_at(struct_inst.type_parameters).0;
                        self.check_signature_tokens(type_arguments)?;
                        self.check_generic_instance(
                            type_arguments,
                            struct_handle.type_param_constraints(),
                            type_parameters,
                        )
                    }
                    ImmBorrowFieldGeneric(idx) | MutBorrowFieldGeneric(idx) => {
                        let field_inst = self.module.field_instantiation_at( *idx);
                        let field_handle = self.module.field_handle_at(field_inst.handle);
                        let struct_def = self.module.struct_def_at(field_handle.owner);
                        let struct_handle = self.module.struct_handle_at(struct_def.struct_handle);
                        let type_arguments = &self.module.signature_at(field_inst.type_parameters).0;
                        self.check_signature_tokens(type_arguments)?;
                        self.check_generic_instance(
                            type_arguments,
                            struct_handle.type_param_constraints(),
                            type_parameters,
                        )
                    }
                    VecPack(idx, _)
                    | VecLen(idx)
                    | VecImmBorrow(idx)
                    | VecMutBorrow(idx)
                    | VecPushBack(idx)
                    | VecPopBack(idx)
                    | VecUnpack(idx, _)
                    | VecSwap(idx) => {
                        let type_arguments = &self.module.signature_at( *idx).0;
                        if type_arguments.len() != 1 {
                            return Err(PartialVMError::new(
                                StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH,
                            )
                            .with_message(format!(
                                "expected 1 type token for vector operations, got {}",
                                type_arguments.len()
                            )));
                        }
                        self.check_signature_tokens(type_arguments)
                    }
    
                    // List out the other options explicitly so there's a compile error if a new
                    // bytecode gets added.
                    Pop
                    | Ret
                    | Branch(_)
                    | BrTrue(_)
                    | BrFalse(_)
                    | LdU8(_)
                    | LdU16(_)
                    | LdU32(_)
                    | LdU64(_)
                    | LdU128(_)
                    | LdU256(_)
                    | LdConst(_)
                    | CastU8
                    | CastU16
                    | CastU32
                    | CastU64
                    | CastU128
                    | CastU256
                    | LdTrue
                    | LdFalse
                    | Call(_)
                    | Pack(_)
                    | Unpack(_)
                    | ReadRef
                    | WriteRef
                    | FreezeRef
                    | Add
                    | Sub
                    | Mul
                    | Mod
                    | Div
                    | BitOr
                    | BitAnd
                    | Xor
                    | Shl
                    | Shr
                    | Or
                    | And
                    | Not
                    | Eq
                    | Neq
                    | Lt
                    | Gt
                    | Le
                    | Ge
                    | CopyLoc(_)
                    | MoveLoc(_)
                    | StLoc(_)
                    | MutBorrowLoc(_)
                    | ImmBorrowLoc(_)
                    | MutBorrowField(_)
                    | ImmBorrowField(_)
                    | MutBorrowGlobalDeprecated(_)
                    | ImmBorrowGlobalDeprecated(_)
                    | ExistsDeprecated(_)
                    | MoveToDeprecated(_)
                    | MoveFromDeprecated(_)
                    | Abort
                    | Nop => Ok(()),
                };
                result.map_err(|err| {
                    err.append_message_with_separator(' ', format!("at offset {} ", offset))
                })?
            }
            Ok(())
        }
    *)
    Definition verify_code (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; code; type_parameters ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let code := M.alloc (| code |) in
          let type_parameters := M.alloc (| type_parameters |) 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::signature::SignatureChecker",
                              "check_instantiation",
                              []
                            |),
                            [
                              M.read (| self |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| code |),
                                  "move_binary_format::file_format::CodeUnit",
                                  "locals"
                                |)
                              |);
                              M.read (| type_parameters |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Bytecode" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "move_binary_format::file_format::Bytecode";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| code |),
                                          "move_binary_format::file_format::CodeUnit",
                                          "code"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::Bytecode"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let offset := M.copy (| γ1_0 |) in
                                          let instr := M.copy (| γ1_1 |) in
                                          let~ result :=
                                            M.copy (|
                                              M.match_operator (|
                                                instr,
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ := M.read (| γ |) in
                                                      let γ1_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "move_binary_format::file_format::Bytecode::CallGeneric",
                                                          0
                                                        |) in
                                                      let idx := M.alloc (| γ1_0 |) in
                                                      let~ func_inst :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "function_instantiation_at",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::signature::SignatureChecker",
                                                                  "module"
                                                                |)
                                                              |);
                                                              M.read (| M.read (| idx |) |)
                                                            ]
                                                          |)
                                                        |) in
                                                      let~ func_handle :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::CompiledModule",
                                                              "function_handle_at",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_bytecode_verifier::signature::SignatureChecker",
                                                                  "module"
                                                                |)
                                                              |);
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| func_inst |),
                                                                  "move_binary_format::file_format::FunctionInstantiation",
                                                                  "handle"
                                                                |)
                                                              |)
                                                            ]
                                                          |)
                                                        |) in
                                                      let~ type_arguments :=
                                                        M.alloc (|
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_binary_format::file_format::CompiledModule",
                                                                "signature_at",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "move_bytecode_verifier::signature::SignatureChecker",
                                                                    "module"
                                                                  |)
                                                                |);
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| func_inst |),
                                                                    "move_binary_format::file_format::FunctionInstantiation",
                                                                    "type_parameters"
                                                                  |)
                                                                |)
                                                              ]
                                                            |),
                                                            "move_binary_format::file_format::Signature",
                                                            0
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::Try",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple [];
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ],
                                                                [],
                                                                "branch",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "move_bytecode_verifier::signature::SignatureChecker",
                                                                    "check_signature_tokens",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| self |);
                                                                    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::SignatureToken";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        [],
                                                                        "deref",
                                                                        []
                                                                      |),
                                                                      [ M.read (| type_arguments |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            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::signature::SignatureChecker",
                                                            "check_generic_instance",
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::iter::adapters::copied::Copied")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::slice::iter::Iter")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::AbilitySet"
                                                                    ]
                                                                ]
                                                            ]
                                                          |),
                                                          [
                                                            M.read (| self |);
                                                            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::SignatureToken";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                [],
                                                                "deref",
                                                                []
                                                              |),
                                                              [ M.read (| type_arguments |) ]
                                                            |);
                                                            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::AbilitySet"
                                                                  ],
                                                                [],
                                                                "copied",
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::file_format::AbilitySet"
                                                                ]
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "slice")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "move_binary_format::file_format::AbilitySet"
                                                                      ],
                                                                    "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::AbilitySet";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        [],
                                                                        "deref",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| func_handle |),
                                                                          "move_binary_format::file_format::FunctionHandle",
                                                                          "type_parameters"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |);
                                                            M.read (| type_parameters |)
                                                          ]
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.find_or_pattern (|
                                                        γ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::PackGeneric",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::UnpackGeneric",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ExistsGenericDeprecated",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MoveFromGenericDeprecated",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MoveToGenericDeprecated",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ImmBorrowGlobalGenericDeprecated",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MutBorrowGlobalGenericDeprecated",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]))
                                                        ],
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ idx ] =>
                                                                ltac:(M.monadic
                                                                  (let~ struct_inst :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "struct_instantiation_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.read (| idx |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ struct_def :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "struct_def_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                struct_inst
                                                                              |),
                                                                              "move_binary_format::file_format::StructDefInstantiation",
                                                                              "def"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ struct_handle :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "struct_handle_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                struct_def
                                                                              |),
                                                                              "move_binary_format::file_format::StructDefinition",
                                                                              "struct_handle"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ type_arguments :=
                                                                    M.alloc (|
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::CompiledModule",
                                                                            "signature_at",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (| self |),
                                                                                "move_bytecode_verifier::signature::SignatureChecker",
                                                                                "module"
                                                                              |)
                                                                            |);
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  struct_inst
                                                                                |),
                                                                                "move_binary_format::file_format::StructDefInstantiation",
                                                                                "type_parameters"
                                                                              |)
                                                                            |)
                                                                          ]
                                                                        |),
                                                                        "move_binary_format::file_format::Signature",
                                                                        0
                                                                      |)
                                                                    |) in
                                                                  let~ _ :=
                                                                    M.match_operator (|
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::Try",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              []
                                                                              [
                                                                                Ty.tuple [];
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError"
                                                                              ],
                                                                            [],
                                                                            "branch",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::signature::SignatureChecker",
                                                                                "check_signature_tokens",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| self |);
                                                                                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::SignatureToken";
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    [],
                                                                                    "deref",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      type_arguments
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        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::signature::SignatureChecker",
                                                                        "check_generic_instance",
                                                                        [ Ty.associated ]
                                                                      |),
                                                                      [
                                                                        M.read (| self |);
                                                                        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::SignatureToken";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ],
                                                                            [],
                                                                            "deref",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              type_arguments
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::StructHandle",
                                                                            "type_param_constraints",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              struct_handle
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.read (| type_parameters |)
                                                                      ]
                                                                    |)
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.find_or_pattern (|
                                                        γ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ImmBorrowFieldGeneric",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MutBorrowFieldGeneric",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]))
                                                        ],
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ idx ] =>
                                                                ltac:(M.monadic
                                                                  (let~ field_inst :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "field_instantiation_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.read (| idx |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ field_handle :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "field_handle_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                field_inst
                                                                              |),
                                                                              "move_binary_format::file_format::FieldInstantiation",
                                                                              "handle"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ struct_def :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "struct_def_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                field_handle
                                                                              |),
                                                                              "move_binary_format::file_format::FieldHandle",
                                                                              "owner"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ struct_handle :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::file_format::CompiledModule",
                                                                          "struct_handle_at",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                                              "module"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                struct_def
                                                                              |),
                                                                              "move_binary_format::file_format::StructDefinition",
                                                                              "struct_handle"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ type_arguments :=
                                                                    M.alloc (|
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::CompiledModule",
                                                                            "signature_at",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (| self |),
                                                                                "move_bytecode_verifier::signature::SignatureChecker",
                                                                                "module"
                                                                              |)
                                                                            |);
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  field_inst
                                                                                |),
                                                                                "move_binary_format::file_format::FieldInstantiation",
                                                                                "type_parameters"
                                                                              |)
                                                                            |)
                                                                          ]
                                                                        |),
                                                                        "move_binary_format::file_format::Signature",
                                                                        0
                                                                      |)
                                                                    |) in
                                                                  let~ _ :=
                                                                    M.match_operator (|
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::Try",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              []
                                                                              [
                                                                                Ty.tuple [];
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError"
                                                                              ],
                                                                            [],
                                                                            "branch",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::signature::SignatureChecker",
                                                                                "check_signature_tokens",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (| self |);
                                                                                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::SignatureToken";
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    [],
                                                                                    "deref",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      type_arguments
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |),
                                                                      [
                                                                        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::signature::SignatureChecker",
                                                                        "check_generic_instance",
                                                                        [ Ty.associated ]
                                                                      |),
                                                                      [
                                                                        M.read (| self |);
                                                                        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::SignatureToken";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ],
                                                                            [],
                                                                            "deref",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              type_arguments
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::StructHandle",
                                                                            "type_param_constraints",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              struct_handle
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.read (| type_parameters |)
                                                                      ]
                                                                    |)
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.find_or_pattern (|
                                                        γ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecPack",
                                                                  0
                                                                |) in
                                                              let γ1_1 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecPack",
                                                                  1
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecLen",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecImmBorrow",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecMutBorrow",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecPushBack",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecPopBack",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecUnpack",
                                                                  0
                                                                |) in
                                                              let γ1_1 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecUnpack",
                                                                  1
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::VecSwap",
                                                                  0
                                                                |) in
                                                              let idx := M.alloc (| γ1_0 |) in
                                                              Value.Tuple [ idx ]))
                                                        ],
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ idx ] =>
                                                                ltac:(M.monadic
                                                                  (let~ type_arguments :=
                                                                    M.alloc (|
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::file_format::CompiledModule",
                                                                            "signature_at",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (| self |),
                                                                                "move_bytecode_verifier::signature::SignatureChecker",
                                                                                "module"
                                                                              |)
                                                                            |);
                                                                            M.read (|
                                                                              M.read (| idx |)
                                                                            |)
                                                                          ]
                                                                        |),
                                                                        "move_binary_format::file_format::Signature",
                                                                        0
                                                                      |)
                                                                    |) in
                                                                  let~ _ :=
                                                                    M.match_operator (|
                                                                      M.alloc (| Value.Tuple [] |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ :=
                                                                              M.use
                                                                                (M.alloc (|
                                                                                  BinOp.ne (|
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "alloc::vec::Vec")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "move_binary_format::file_format::SignatureToken";
                                                                                            Ty.path
                                                                                              "alloc::alloc::Global"
                                                                                          ],
                                                                                        "len",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.read (|
                                                                                          type_arguments
                                                                                        |)
                                                                                      ]
                                                                                    |),
                                                                                    Value.Integer
                                                                                      IntegerKind.Usize
                                                                                      1
                                                                                  |)
                                                                                |)) in
                                                                            let _ :=
                                                                              M.is_constant_or_break_match (|
                                                                                M.read (| γ |),
                                                                                Value.Bool true
                                                                              |) in
                                                                            M.alloc (|
                                                                              M.never_to_any (|
                                                                                M.read (|
                                                                                  M.return_ (|
                                                                                    Value.StructTuple
                                                                                      "core::result::Result::Err"
                                                                                      [
                                                                                        M.call_closure (|
                                                                                          M.get_associated_function (|
                                                                                            Ty.path
                                                                                              "move_binary_format::errors::PartialVMError",
                                                                                            "with_message",
                                                                                            []
                                                                                          |),
                                                                                          [
                                                                                            M.call_closure (|
                                                                                              M.get_associated_function (|
                                                                                                Ty.path
                                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                                "new",
                                                                                                []
                                                                                              |),
                                                                                              [
                                                                                                Value.StructTuple
                                                                                                  "move_core_types::vm_status::StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH"
                                                                                                  []
                                                                                              ]
                                                                                            |);
                                                                                            M.call_closure (|
                                                                                              M.get_function (|
                                                                                                "core::hint::must_use",
                                                                                                [
                                                                                                  Ty.path
                                                                                                    "alloc::string::String"
                                                                                                ]
                                                                                              |),
                                                                                              [
                                                                                                M.read (|
                                                                                                  let~
                                                                                                        res :=
                                                                                                    M.alloc (|
                                                                                                      M.call_closure (|
                                                                                                        M.get_function (|
                                                                                                          "alloc::fmt::format",
                                                                                                          []
                                                                                                        |),
                                                                                                        [
                                                                                                          M.call_closure (|
                                                                                                            M.get_associated_function (|
                                                                                                              Ty.path
                                                                                                                "core::fmt::Arguments",
                                                                                                              "new_v1",
                                                                                                              []
                                                                                                            |),
                                                                                                            [
                                                                                                              M.alloc (|
                                                                                                                Value.Array
                                                                                                                  [
                                                                                                                    M.read (|
                                                                                                                      Value.String
                                                                                                                        "expected 1 type token for vector operations, got "
                                                                                                                    |)
                                                                                                                  ]
                                                                                                              |);
                                                                                                              M.alloc (|
                                                                                                                Value.Array
                                                                                                                  [
                                                                                                                    M.call_closure (|
                                                                                                                      M.get_associated_function (|
                                                                                                                        Ty.path
                                                                                                                          "core::fmt::rt::Argument",
                                                                                                                        "new_display",
                                                                                                                        [
                                                                                                                          Ty.path
                                                                                                                            "usize"
                                                                                                                        ]
                                                                                                                      |),
                                                                                                                      [
                                                                                                                        M.alloc (|
                                                                                                                          M.call_closure (|
                                                                                                                            M.get_associated_function (|
                                                                                                                              Ty.apply
                                                                                                                                (Ty.path
                                                                                                                                  "alloc::vec::Vec")
                                                                                                                                []
                                                                                                                                [
                                                                                                                                  Ty.path
                                                                                                                                    "move_binary_format::file_format::SignatureToken";
                                                                                                                                  Ty.path
                                                                                                                                    "alloc::alloc::Global"
                                                                                                                                ],
                                                                                                                              "len",
                                                                                                                              []
                                                                                                                            |),
                                                                                                                            [
                                                                                                                              M.read (|
                                                                                                                                type_arguments
                                                                                                                              |)
                                                                                                                            ]
                                                                                                                          |)
                                                                                                                        |)
                                                                                                                      ]
                                                                                                                    |)
                                                                                                                  ]
                                                                                                              |)
                                                                                                            ]
                                                                                                          |)
                                                                                                        ]
                                                                                                      |)
                                                                                                    |) in
                                                                                                  res
                                                                                                |)
                                                                                              ]
                                                                                            |)
                                                                                          ]
                                                                                        |)
                                                                                      ]
                                                                                  |)
                                                                                |)
                                                                              |)
                                                                            |)));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (M.alloc (|
                                                                              Value.Tuple []
                                                                            |)))
                                                                      ]
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "move_bytecode_verifier::signature::SignatureChecker",
                                                                        "check_signature_tokens",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| self |);
                                                                        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::SignatureToken";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ],
                                                                            [],
                                                                            "deref",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              type_arguments
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.find_or_pattern (|
                                                        γ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Pop"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Ret"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Branch",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::BrTrue",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::BrFalse",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU8",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU16",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU32",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU64",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU128",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdU256",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdConst",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU8"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU16"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU32"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU64"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU128"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CastU256"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdTrue"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::LdFalse"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Call",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Pack",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Unpack",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ReadRef"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::WriteRef"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::FreezeRef"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Add"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Sub"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Mul"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Mod"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Div"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::BitOr"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::BitAnd"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Xor"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Shl"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Shr"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Or"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::And"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Not"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Eq"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Neq"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Lt"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Gt"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Le"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Ge"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::CopyLoc",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MoveLoc",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::StLoc",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MutBorrowLoc",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ImmBorrowLoc",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MutBorrowField",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ImmBorrowField",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MutBorrowGlobalDeprecated",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ImmBorrowGlobalDeprecated",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::ExistsDeprecated",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MoveToDeprecated",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ1_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::MoveFromDeprecated",
                                                                  0
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Abort"
                                                                |) in
                                                              Value.Tuple []));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::Bytecode::Nop"
                                                                |) in
                                                              Value.Tuple []))
                                                        ],
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [] =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::result::Result::Ok"
                                                                      [ Value.Tuple [] ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      |)))
                                                ]
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.tuple [];
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError"
                                                        ],
                                                      "map_err",
                                                      [
                                                        Ty.path
                                                          "move_binary_format::errors::PartialVMError";
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::errors::PartialVMError"
                                                              ]
                                                          ]
                                                          (Ty.path
                                                            "move_binary_format::errors::PartialVMError")
                                                      ]
                                                    |),
                                                    [
                                                      M.read (| result |);
                                                      M.closure
                                                        (fun γ =>
                                                          ltac:(M.monadic
                                                            match γ with
                                                            | [ α0 ] =>
                                                              ltac:(M.monadic
                                                                (M.match_operator (|
                                                                  M.alloc (| α0 |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let err :=
                                                                          M.copy (| γ |) in
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "append_message_with_separator",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (| err |);
                                                                            Value.UnicodeChar 32;
                                                                            M.call_closure (|
                                                                              M.get_function (|
                                                                                "core::hint::must_use",
                                                                                [
                                                                                  Ty.path
                                                                                    "alloc::string::String"
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.read (|
                                                                                  let~ res :=
                                                                                    M.alloc (|
                                                                                      M.call_closure (|
                                                                                        M.get_function (|
                                                                                          "alloc::fmt::format",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "core::fmt::Arguments",
                                                                                              "new_v1",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.alloc (|
                                                                                                Value.Array
                                                                                                  [
                                                                                                    M.read (|
                                                                                                      Value.String
                                                                                                        "at offset "
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      Value.String
                                                                                                        " "
                                                                                                    |)
                                                                                                  ]
                                                                                              |);
                                                                                              M.alloc (|
                                                                                                Value.Array
                                                                                                  [
                                                                                                    M.call_closure (|
                                                                                                      M.get_associated_function (|
                                                                                                        Ty.path
                                                                                                          "core::fmt::rt::Argument",
                                                                                                        "new_display",
                                                                                                        [
                                                                                                          Ty.path
                                                                                                            "usize"
                                                                                                        ]
                                                                                                      |),
                                                                                                      [
                                                                                                        offset
                                                                                                      ]
                                                                                                    |)
                                                                                                  ]
                                                                                              |)
                                                                                            ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |) in
                                                                                  res
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)))
                                                                  ]
                                                                |)))
                                                            | _ =>
                                                              M.impossible
                                                                "wrong number of arguments"
                                                            end))
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_code : M.IsAssociatedFunction Self "verify_code" verify_code.
    
    (*
        fn check_phantom_params(
            &self,
            ty: &SignatureToken,
            is_phantom_pos: bool,
            type_parameters: &[StructTypeParameter],
        ) -> PartialVMResult<()> {
            match ty {
                SignatureToken::Vector(ty) => self.check_phantom_params(ty, false, type_parameters)?,
                SignatureToken::StructInstantiation(struct_inst) => {
                    let (idx, type_arguments) = &**struct_inst;
                    let sh = self.module.struct_handle_at( *idx);
                    for (i, ty) in type_arguments.iter().enumerate() {
                        self.check_phantom_params(
                            ty,
                            sh.type_parameters[i].is_phantom,
                            type_parameters,
                        )?;
                    }
                }
                SignatureToken::TypeParameter(idx) => {
                    if type_parameters[*idx as usize].is_phantom && !is_phantom_pos {
                        return Err(PartialVMError::new(
                            StatusCode::INVALID_PHANTOM_TYPE_PARAM_POSITION,
                        )
                        .with_message(
                            "phantom type parameter cannot be used in non-phantom position".to_string(),
                        ));
                    }
                }
    
                SignatureToken::Struct(_)
                | SignatureToken::Reference(_)
                | SignatureToken::MutableReference(_)
                | SignatureToken::Bool
                | SignatureToken::U8
                | SignatureToken::U16
                | SignatureToken::U32
                | SignatureToken::U64
                | SignatureToken::U128
                | SignatureToken::U256
                | SignatureToken::Address
                | SignatureToken::Signer => {}
            }
            Ok(())
        }
    *)
    Definition check_phantom_params (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ty; is_phantom_pos; type_parameters ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ty := M.alloc (| ty |) in
          let is_phantom_pos := M.alloc (| is_phantom_pos |) in
          let type_parameters := M.alloc (| type_parameters |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    ty,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "move_binary_format::file_format::SignatureToken::Vector",
                              0
                            |) in
                          let ty := M.alloc (| γ1_0 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.tuple [];
                                      Ty.path "move_binary_format::errors::PartialVMError"
                                    ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                                      "check_phantom_params",
                                      []
                                    |),
                                    [
                                      M.read (| self |);
                                      M.read (| M.read (| ty |) |);
                                      Value.Bool false;
                                      M.read (| type_parameters |)
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              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))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "move_binary_format::file_format::SignatureToken::StructInstantiation",
                              0
                            |) in
                          let struct_inst := M.alloc (| γ1_0 |) in
                          M.match_operator (|
                            M.alloc (| M.read (| M.read (| struct_inst |) |) |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let idx := M.alloc (| γ1_0 |) in
                                  let type_arguments := M.alloc (| γ1_1 |) in
                                  let~ sh :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::CompiledModule",
                                          "struct_handle_at",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_bytecode_verifier::signature::SignatureChecker",
                                              "module"
                                            |)
                                          |);
                                          M.read (| M.read (| idx |) |)
                                        ]
                                      |)
                                    |) in
                                  M.use
                                    (M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::collect::IntoIterator",
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::slice::iter::Iter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::SignatureToken"
                                                  ]
                                              ],
                                            [],
                                            "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::SignatureToken"
                                                  ],
                                                [],
                                                "enumerate",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "slice")
                                                      []
                                                      [
                                                        Ty.path
                                                          "move_binary_format::file_format::SignatureToken"
                                                      ],
                                                    "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::SignatureToken";
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        [],
                                                        "deref",
                                                        []
                                                      |),
                                                      [ M.read (| type_arguments |) ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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::SignatureToken"
                                                                ]
                                                            ],
                                                          [],
                                                          "next",
                                                          []
                                                        |),
                                                        [ iter ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "core::option::Option::None"
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (| M.break (||) |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::option::Option::Some",
                                                              0
                                                            |) in
                                                          let γ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 ty := M.copy (| γ1_1 |) 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::signature::SignatureChecker",
                                                                        "check_phantom_params",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| self |);
                                                                        M.read (| ty |);
                                                                        M.read (|
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::ops::index::Index",
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "alloc::vec::Vec")
                                                                                  []
                                                                                  [
                                                                                    Ty.path
                                                                                      "move_binary_format::file_format::StructTypeParameter";
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ],
                                                                                [ Ty.path "usize" ],
                                                                                "index",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| sh |),
                                                                                  "move_binary_format::file_format::StructHandle",
                                                                                  "type_parameters"
                                                                                |);
                                                                                M.read (| i |)
                                                                              ]
                                                                            |),
                                                                            "move_binary_format::file_format::StructTypeParameter",
                                                                            "is_phantom"
                                                                          |)
                                                                        |);
                                                                        M.read (| type_parameters |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::ops::control_flow::ControlFlow::Break",
                                                                        0
                                                                      |) in
                                                                    let residual :=
                                                                      M.copy (| γ0_0 |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (|
                                                                          M.return_ (|
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::ops::try_trait::FromResidual",
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "core::result::Result")
                                                                                  []
                                                                                  [
                                                                                    Ty.tuple [];
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError"
                                                                                  ],
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::result::Result")
                                                                                    []
                                                                                    [
                                                                                      Ty.path
                                                                                        "core::convert::Infallible";
                                                                                      Ty.path
                                                                                        "move_binary_format::errors::PartialVMError"
                                                                                    ]
                                                                                ],
                                                                                "from_residual",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (|
                                                                                  residual
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                                        0
                                                                      |) in
                                                                    let val := M.copy (| γ0_0 |) in
                                                                    val))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)))
                                            |)))
                                      ]
                                    |))))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "move_binary_format::file_format::SignatureToken::TypeParameter",
                              0
                            |) in
                          let idx := M.alloc (| γ1_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| type_parameters |),
                                                M.alloc (|
                                                  M.rust_cast (M.read (| M.read (| idx |) |))
                                                |)
                                              |),
                                              "move_binary_format::file_format::StructTypeParameter",
                                              "is_phantom"
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (UnOp.not (| M.read (| is_phantom_pos |) |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "with_message",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError",
                                                      "new",
                                                      []
                                                    |),
                                                    [
                                                      Value.StructTuple
                                                        "move_core_types::vm_status::StatusCode::INVALID_PHANTOM_TYPE_PARAM_POSITION"
                                                        []
                                                    ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "alloc::string::ToString",
                                                      Ty.path "str",
                                                      [],
                                                      "to_string",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "phantom type parameter cannot be used in non-phantom position"
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.find_or_pattern (|
                            γ,
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let γ1_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::Struct",
                                      0
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let γ1_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::Reference",
                                      0
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let γ1_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::MutableReference",
                                      0
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::Bool"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U8"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U16"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U32"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U64"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U128"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::U256"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::Address"
                                    |) in
                                  Value.Tuple []));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.read (| γ |) in
                                  let _ :=
                                    M.is_struct_tuple (|
                                      γ,
                                      "move_binary_format::file_format::SignatureToken::Signer"
                                    |) in
                                  Value.Tuple []))
                            ],
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [] => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_phantom_params :
      M.IsAssociatedFunction Self "check_phantom_params" check_phantom_params.
    
    (*
        fn check_signature(&self, idx: SignatureIndex) -> PartialVMResult<()> {
            for token in &self.module.signature_at(idx).0 {
                match token {
                    SignatureToken::Reference(inner) | SignatureToken::MutableReference(inner) => {
                        self.check_signature_token(inner)?
                    }
                    _ => self.check_signature_token(token)?,
                }
            }
            Ok(())
        }
    *)
    Definition check_signature (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let idx := M.alloc (| idx |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.path "move_binary_format::file_format::SignatureToken";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "signature_at",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_bytecode_verifier::signature::SignatureChecker",
                                      "module"
                                    |)
                                  |);
                                  M.read (| idx |)
                                ]
                              |),
                              "move_binary_format::file_format::Signature",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let token := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            token,
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.find_or_pattern (|
                                                    γ,
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::SignatureToken::Reference",
                                                              0
                                                            |) in
                                                          let inner := M.alloc (| γ1_0 |) in
                                                          Value.Tuple [ inner ]));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ := M.read (| γ |) in
                                                          let γ1_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "move_binary_format::file_format::SignatureToken::MutableReference",
                                                              0
                                                            |) in
                                                          let inner := M.alloc (| γ1_0 |) in
                                                          Value.Tuple [ inner ]))
                                                    ],
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ inner ] =>
                                                            ltac:(M.monadic
                                                              (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::signature::SignatureChecker",
                                                                          "check_signature_token",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (| self |);
                                                                          M.read (|
                                                                            M.read (| inner |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |),
                                                                [
                                                                  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))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (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::signature::SignatureChecker",
                                                              "check_signature_token",
                                                              []
                                                            |),
                                                            [ M.read (| self |); M.read (| token |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Break",
                                                              0
                                                            |) in
                                                          let residual := M.copy (| γ0_0 |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::try_trait::FromResidual",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        []
                                                                        [
                                                                          Ty.tuple [];
                                                                          Ty.path
                                                                            "move_binary_format::errors::PartialVMError"
                                                                        ],
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "core::convert::Infallible";
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ]
                                                                      ],
                                                                      "from_residual",
                                                                      []
                                                                    |),
                                                                    [ M.read (| residual |) ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                              0
                                                            |) in
                                                          let val := M.copy (| γ0_0 |) in
                                                          val))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_signature :
      M.IsAssociatedFunction Self "check_signature" check_signature.
    
    (*
        fn check_signature_tokens(&self, tys: &[SignatureToken]) -> PartialVMResult<()> {
            for ty in tys {
                self.check_signature_token(ty)?
            }
            Ok(())
        }
    *)
    Definition check_signature_tokens (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; tys ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let tys := M.alloc (| tys |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::SignatureToken" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| tys |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let ty := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_bytecode_verifier::signature::SignatureChecker",
                                                      "check_signature_token",
                                                      []
                                                    |),
                                                    [ M.read (| self |); M.read (| ty |) ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_signature_tokens :
      M.IsAssociatedFunction Self "check_signature_tokens" check_signature_tokens.
    
    (*
        fn check_signature_token(&self, ty: &SignatureToken) -> PartialVMResult<()> {
            use SignatureToken::*;
            match ty {
                U8 | U16 | U32 | U64 | U128 | U256 | Bool | Address | Signer | Struct(_)
                | TypeParameter(_) => Ok(()),
                Reference(_) | MutableReference(_) => {
                    // TODO: Prop tests expect us to NOT check the inner types.
                    // Revisit this once we rework prop tests.
                    Err(PartialVMError::new(StatusCode::INVALID_SIGNATURE_TOKEN)
                        .with_message("reference not allowed".to_string()))
                }
                Vector(ty) => self.check_signature_token(ty),
                StructInstantiation(struct_inst) => {
                    let (_, type_arguments) = &**struct_inst;
                    self.check_signature_tokens(type_arguments)
                }
            }
        }
    *)
    Definition check_signature_token (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ty ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ty := M.alloc (| ty |) in
          M.read (|
            M.match_operator (|
              ty,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U8"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U16"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U32"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U64"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U128"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U256"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Bool"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Address"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Signer"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Struct",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::TypeParameter",
                                0
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Reference",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::MutableReference",
                                0
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "with_message",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "move_binary_format::errors::PartialVMError",
                                              "new",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "move_core_types::vm_status::StatusCode::INVALID_SIGNATURE_TOKEN"
                                                []
                                            ]
                                          |);
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "alloc::string::ToString",
                                              Ty.path "str",
                                              [],
                                              "to_string",
                                              []
                                            |),
                                            [ M.read (| Value.String "reference not allowed" |) ]
                                          |)
                                        ]
                                      |)
                                    ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::file_format::SignatureToken::Vector",
                        0
                      |) in
                    let ty := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                          "check_signature_token",
                          []
                        |),
                        [ M.read (| self |); M.read (| M.read (| ty |) |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::file_format::SignatureToken::StructInstantiation",
                        0
                      |) in
                    let struct_inst := M.alloc (| γ1_0 |) in
                    M.match_operator (|
                      M.alloc (| M.read (| M.read (| struct_inst |) |) |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let type_arguments := M.alloc (| γ1_1 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                                  "check_signature_tokens",
                                  []
                                |),
                                [
                                  M.read (| self |);
                                  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::SignatureToken";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [ M.read (| type_arguments |) ]
                                  |)
                                ]
                              |)
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_signature_token :
      M.IsAssociatedFunction Self "check_signature_token" check_signature_token.
    
    (*
        fn check_instantiation(
            &mut self,
            idx: SignatureIndex,
            type_parameters: &[AbilitySet],
        ) -> PartialVMResult<()> {
            if let Some(checked_abilities) = self.abilities_cache.get(&idx) {
                if checked_abilities.contains(type_parameters) {
                    return Ok(());
                }
            };
            for ty in &self.module.signature_at(idx).0 {
                self.check_type_instantiation(ty, type_parameters)?
            }
            let checked_abilities = self.abilities_cache.entry(idx).or_default();
            checked_abilities.insert(type_parameters.to_vec());
            Ok(())
        }
    *)
    Definition check_instantiation (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; idx; type_parameters ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let idx := M.alloc (| idx |) in
          let type_parameters := M.alloc (| type_parameters |) 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.apply
                                    (Ty.path "std::collections::hash::map::HashMap")
                                    []
                                    [
                                      Ty.path "move_binary_format::file_format::SignatureIndex";
                                      Ty.apply
                                        (Ty.path "std::collections::hash::set::HashSet")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path "move_binary_format::file_format::AbilitySet";
                                              Ty.path "alloc::alloc::Global"
                                            ];
                                          Ty.path "std::hash::random::RandomState"
                                        ];
                                      Ty.path "std::hash::random::RandomState"
                                    ],
                                  "get",
                                  [ Ty.path "move_binary_format::file_format::SignatureIndex" ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::signature::SignatureChecker",
                                    "abilities_cache"
                                  |);
                                  idx
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let checked_abilities := M.copy (| γ0_0 |) 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 "std::collections::hash::set::HashSet")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::AbilitySet";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.path "std::hash::random::RandomState"
                                              ],
                                            "contains",
                                            [
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::AbilitySet"
                                                ]
                                            ]
                                          |),
                                          [
                                            M.read (| checked_abilities |);
                                            M.read (| type_parameters |)
                                          ]
                                        |)
                                      |)) 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::Ok"
                                            [ Value.Tuple [] ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      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 "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.path "move_binary_format::file_format::SignatureToken";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "signature_at",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_bytecode_verifier::signature::SignatureChecker",
                                      "module"
                                    |)
                                  |);
                                  M.read (| idx |)
                                ]
                              |),
                              "move_binary_format::file_format::Signature",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let ty := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_bytecode_verifier::signature::SignatureChecker",
                                                      "check_type_instantiation",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| self |);
                                                      M.read (| ty |);
                                                      M.read (| type_parameters |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ checked_abilities :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::Entry")
                          []
                          [
                            Ty.path "move_binary_format::file_format::SignatureIndex";
                            Ty.apply
                              (Ty.path "std::collections::hash::set::HashSet")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.path "move_binary_format::file_format::AbilitySet";
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "std::hash::random::RandomState"
                              ]
                          ],
                        "or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "std::collections::hash::map::HashMap")
                              []
                              [
                                Ty.path "move_binary_format::file_format::SignatureIndex";
                                Ty.apply
                                  (Ty.path "std::collections::hash::set::HashSet")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_binary_format::file_format::AbilitySet";
                                        Ty.path "alloc::alloc::Global"
                                      ];
                                    Ty.path "std::hash::random::RandomState"
                                  ];
                                Ty.path "std::hash::random::RandomState"
                              ],
                            "entry",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_bytecode_verifier::signature::SignatureChecker",
                              "abilities_cache"
                            |);
                            M.read (| idx |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::set::HashSet")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path "move_binary_format::file_format::AbilitySet";
                                Ty.path "alloc::alloc::Global"
                              ];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "insert",
                        []
                      |),
                      [
                        M.read (| checked_abilities |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                            "to_vec",
                            []
                          |),
                          [ M.read (| type_parameters |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_instantiation :
      M.IsAssociatedFunction Self "check_instantiation" check_instantiation.
    
    (*
        fn check_type_instantiation(
            &self,
            s: &SignatureToken,
            type_parameters: &[AbilitySet],
        ) -> PartialVMResult<()> {
            if self.module.version() >= VERSION_6 {
                for ty in s.preorder_traversal() {
                    self.check_type_instantiation_(ty, type_parameters)?
                }
                Ok(())
            } else {
                // preserve buggy, but harmless old behavior for backward compatibility
                self.check_type_instantiation_(s, type_parameters)
            }
        }
    *)
    Definition check_type_instantiation (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; s; type_parameters ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let s := M.alloc (| s |) in
          let type_parameters := M.alloc (| type_parameters |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ge (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::file_format::CompiledModule",
                                    "version",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::signature::SignatureChecker",
                                        "module"
                                      |)
                                    |)
                                  ]
                                |),
                                M.read (|
                                  M.get_constant (|
                                    "move_binary_format::file_format_common::VERSION_6"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.path
                                      "move_binary_format::file_format::SignatureTokenPreorderTraversalIter",
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_binary_format::file_format::SignatureToken",
                                        "preorder_traversal",
                                        []
                                      |),
                                      [ M.read (| s |) ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureTokenPreorderTraversalIter",
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let ty := M.copy (| γ0_0 |) in
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::try_trait::Try",
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.tuple [];
                                                              Ty.path
                                                                "move_binary_format::errors::PartialVMError"
                                                            ],
                                                          [],
                                                          "branch",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_bytecode_verifier::signature::SignatureChecker",
                                                              "check_type_instantiation_",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| self |);
                                                              M.read (| ty |);
                                                              M.read (| type_parameters |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Break",
                                                              0
                                                            |) in
                                                          let residual := M.copy (| γ0_0 |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::ops::try_trait::FromResidual",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        []
                                                                        [
                                                                          Ty.tuple [];
                                                                          Ty.path
                                                                            "move_binary_format::errors::PartialVMError"
                                                                        ],
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::result::Result")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "core::convert::Infallible";
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError"
                                                                          ]
                                                                      ],
                                                                      "from_residual",
                                                                      []
                                                                    |),
                                                                    [ M.read (| residual |) ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                              0
                                                            |) in
                                                          let val := M.copy (| γ0_0 |) in
                                                          val))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                              "check_type_instantiation_",
                              []
                            |),
                            [ M.read (| self |); M.read (| s |); M.read (| type_parameters |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_type_instantiation :
      M.IsAssociatedFunction Self "check_type_instantiation" check_type_instantiation.
    
    (*
        fn check_type_instantiation_(
            &self,
            s: &SignatureToken,
            type_parameters: &[AbilitySet],
        ) -> PartialVMResult<()> {
            match s {
                SignatureToken::StructInstantiation(struct_inst) => {
                    let (idx, type_arguments) = &**struct_inst;
                    // Check that the instantiation satisfies the `idx` struct's constraints
                    // Cannot be checked completely if we do not know the constraints of type parameters
                    // i.e. it cannot be checked unless we are inside some module member. The only case
                    // where that happens is when checking the signature pool itself
                    let sh = self.module.struct_handle_at( *idx);
                    self.check_generic_instance(
                        type_arguments,
                        sh.type_param_constraints(),
                        type_parameters,
                    )
                }
                SignatureToken::Reference(_)
                | SignatureToken::MutableReference(_)
                | SignatureToken::Vector(_)
                | SignatureToken::TypeParameter(_)
                | SignatureToken::Struct(_)
                | SignatureToken::Bool
                | SignatureToken::U8
                | SignatureToken::U16
                | SignatureToken::U32
                | SignatureToken::U64
                | SignatureToken::U128
                | SignatureToken::U256
                | SignatureToken::Address
                | SignatureToken::Signer => Ok(()),
            }
        }
    *)
    Definition check_type_instantiation_
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; s; type_parameters ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let s := M.alloc (| s |) in
          let type_parameters := M.alloc (| type_parameters |) in
          M.read (|
            M.match_operator (|
              s,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::file_format::SignatureToken::StructInstantiation",
                        0
                      |) in
                    let struct_inst := M.alloc (| γ1_0 |) in
                    M.match_operator (|
                      M.alloc (| M.read (| M.read (| struct_inst |) |) |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let idx := M.alloc (| γ1_0 |) in
                            let type_arguments := M.alloc (| γ1_1 |) in
                            let~ sh :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::file_format::CompiledModule",
                                    "struct_handle_at",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::signature::SignatureChecker",
                                        "module"
                                      |)
                                    |);
                                    M.read (| M.read (| idx |) |)
                                  ]
                                |)
                              |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                                  "check_generic_instance",
                                  [ Ty.associated ]
                                |),
                                [
                                  M.read (| self |);
                                  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::SignatureToken";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [ M.read (| type_arguments |) ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::StructHandle",
                                      "type_param_constraints",
                                      []
                                    |),
                                    [ M.read (| sh |) ]
                                  |);
                                  M.read (| type_parameters |)
                                ]
                              |)
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.find_or_pattern (|
                      γ,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Reference",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::MutableReference",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Vector",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::TypeParameter",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Struct",
                                0
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Bool"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U8"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U16"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U32"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U64"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U128"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::U256"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Address"
                              |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_binary_format::file_format::SignatureToken::Signer"
                              |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_type_instantiation_ :
      M.IsAssociatedFunction Self "check_type_instantiation_" check_type_instantiation_.
    
    (*
        fn check_generic_instance(
            &self,
            type_arguments: &[SignatureToken],
            constraints: impl ExactSizeIterator<Item = AbilitySet>,
            global_abilities: &[AbilitySet],
        ) -> PartialVMResult<()> {
            if type_arguments.len() != constraints.len() {
                return Err(
                    PartialVMError::new(StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH).with_message(
                        format!(
                            "expected {} type argument(s), got {}",
                            constraints.len(),
                            type_arguments.len()
                        ),
                    ),
                );
            }
    
            for (constraint, ty) in constraints.into_iter().zip(type_arguments) {
                let given = self.module.abilities(ty, global_abilities)?;
                if !constraint.is_subset(given) {
                    return Err(PartialVMError::new(StatusCode::CONSTRAINT_NOT_SATISFIED)
                        .with_message(format!(
                            "expected type with abilities {:?} got type actual {:?} with incompatible \
                            abilities {:?}",
                            constraint, ty, given
                        )));
                }
            }
            Ok(())
        }
    *)
    Definition check_generic_instance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [],
          [ impl_ExactSizeIterator_Item___AbilitySet_ ],
          [ self; type_arguments; constraints; global_abilities ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let type_arguments := M.alloc (| type_arguments |) in
          let constraints := M.alloc (| constraints |) in
          let global_abilities := M.alloc (| global_abilities |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ne (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [ Ty.path "move_binary_format::file_format::SignatureToken"
                                        ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| type_arguments |) ]
                                  |),
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::exact_size::ExactSizeIterator",
                                      impl_ExactSizeIterator_Item___AbilitySet_,
                                      [],
                                      "len",
                                      []
                                    |),
                                    [ constraints ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "with_message",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "move_binary_format::errors::PartialVMError",
                                              "new",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "move_core_types::vm_status::StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH"
                                                []
                                            ]
                                          |);
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::hint::must_use",
                                              [ Ty.path "alloc::string::String" ]
                                            |),
                                            [
                                              M.read (|
                                                let~ res :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (| "alloc::fmt::format", [] |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (|
                                                                    Value.String "expected "
                                                                  |);
                                                                  M.read (|
                                                                    Value.String
                                                                      " type argument(s), got "
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [ Ty.path "usize" ]
                                                                    |),
                                                                    [
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::iter::traits::exact_size::ExactSizeIterator",
                                                                            impl_ExactSizeIterator_Item___AbilitySet_,
                                                                            [],
                                                                            "len",
                                                                            []
                                                                          |),
                                                                          [ constraints ]
                                                                        |)
                                                                      |)
                                                                    ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [ Ty.path "usize" ]
                                                                    |),
                                                                    [
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "move_binary_format::file_format::SignatureToken"
                                                                              ],
                                                                            "len",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              type_arguments
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                res
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      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::zip::Zip")
                              []
                              [
                                impl_ExactSizeIterator_Item___AbilitySet_;
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::SignatureToken" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                impl_ExactSizeIterator_Item___AbilitySet_,
                                [],
                                "zip",
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [ Ty.path "move_binary_format::file_format::SignatureToken"
                                        ]
                                    ]
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    impl_ExactSizeIterator_Item___AbilitySet_,
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [ M.read (| constraints |) ]
                                |);
                                M.read (| type_arguments |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::zip::Zip")
                                            []
                                            [
                                              impl_ExactSizeIterator_Item___AbilitySet_;
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken"
                                                ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let constraint := M.copy (| γ1_0 |) in
                                          let ty := M.copy (| γ1_1 |) in
                                          let~ given :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::AbilitySet";
                                                          Ty.path
                                                            "move_binary_format::errors::PartialVMError"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "abilities",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_bytecode_verifier::signature::SignatureChecker",
                                                              "module"
                                                            |)
                                                          |);
                                                          M.read (| ty |);
                                                          M.read (| global_abilities |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "move_binary_format::file_format::AbilitySet",
                                                              "is_subset",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| constraint |);
                                                              M.read (| given |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError",
                                                                  "with_message",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "move_binary_format::errors::PartialVMError",
                                                                      "new",
                                                                      []
                                                                    |),
                                                                    [
                                                                      Value.StructTuple
                                                                        "move_core_types::vm_status::StatusCode::CONSTRAINT_NOT_SATISFIED"
                                                                        []
                                                                    ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::hint::must_use",
                                                                      [
                                                                        Ty.path
                                                                          "alloc::string::String"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (|
                                                                        let~ res :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_function (|
                                                                                "alloc::fmt::format",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "core::fmt::Arguments",
                                                                                    "new_v1",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.alloc (|
                                                                                      Value.Array
                                                                                        [
                                                                                          M.read (|
                                                                                            Value.String
                                                                                              "expected type with abilities "
                                                                                          |);
                                                                                          M.read (|
                                                                                            Value.String
                                                                                              " got type actual "
                                                                                          |);
                                                                                          M.read (|
                                                                                            Value.String
                                                                                              " with incompatible abilities "
                                                                                          |)
                                                                                        ]
                                                                                    |);
                                                                                    M.alloc (|
                                                                                      Value.Array
                                                                                        [
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "core::fmt::rt::Argument",
                                                                                              "new_debug",
                                                                                              [
                                                                                                Ty.path
                                                                                                  "move_binary_format::file_format::AbilitySet"
                                                                                              ]
                                                                                            |),
                                                                                            [
                                                                                              constraint
                                                                                            ]
                                                                                          |);
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "core::fmt::rt::Argument",
                                                                                              "new_debug",
                                                                                              [
                                                                                                Ty.apply
                                                                                                  (Ty.path
                                                                                                    "&")
                                                                                                  []
                                                                                                  [
                                                                                                    Ty.path
                                                                                                      "move_binary_format::file_format::SignatureToken"
                                                                                                  ]
                                                                                              ]
                                                                                            |),
                                                                                            [ ty ]
                                                                                          |);
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "core::fmt::rt::Argument",
                                                                                              "new_debug",
                                                                                              [
                                                                                                Ty.path
                                                                                                  "move_binary_format::file_format::AbilitySet"
                                                                                              ]
                                                                                            |),
                                                                                            [ given
                                                                                            ]
                                                                                          |)
                                                                                        ]
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |) in
                                                                        res
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check_generic_instance :
      M.IsAssociatedFunction Self "check_generic_instance" check_generic_instance.
  End Impl_move_bytecode_verifier_signature_SignatureChecker.
End signature.
