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

Module script_signature.
  Axiom FnCheckScriptSignature :
    (Ty.path "move_bytecode_verifier::script_signature::FnCheckScriptSignature") =
      (Ty.function
        [
          Ty.apply (Ty.path "&") [] [ Ty.path "move_binary_format::file_format::CompiledModule" ];
          Ty.path "bool";
          Ty.path "move_binary_format::file_format::SignatureIndex";
          Ty.apply
            (Ty.path "core::option::Option")
            []
            [ Ty.path "move_binary_format::file_format::SignatureIndex" ]
        ]
        (Ty.apply
          (Ty.path "core::result::Result")
          []
          [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ])).
  
  (*
  pub fn verify_module(
      module: &CompiledModule,
      check_signature: FnCheckScriptSignature,
  ) -> VMResult<()> {
      // important for not breaking old modules
      if module.version < VERSION_5 {
          return Ok(());
      }
  
      for (idx, _fdef) in module
          .function_defs()
          .iter()
          .enumerate()
          .filter(|(_idx, fdef)| fdef.is_entry)
      {
          verify_module_function_signature(
              module,
              FunctionDefinitionIndex(idx as TableIndex),
              check_signature,
          )?
      }
      Ok(())
  }
  *)
  Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ module; check_signature ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        let check_signature := M.alloc (| check_signature |) 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.lt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| module |),
                                    "move_binary_format::file_format::CompiledModule",
                                    "version"
                                  |)
                                |),
                                M.read (|
                                  M.get_constant (|
                                    "move_binary_format::file_format_common::VERSION_5"
                                  |)
                                |)
                              |)
                            |)) 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 [] |)))
                  ]
                |) 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::filter::Filter")
                            []
                            [
                              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"
                                    ]
                                ];
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path "usize";
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition"
                                                ]
                                            ]
                                        ]
                                    ]
                                ]
                                (Ty.path "bool")
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          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"
                                    ]
                                ],
                              [],
                              "filter",
                              [
                                Ty.function
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.tuple
                                              [
                                                Ty.path "usize";
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::FunctionDefinition"
                                                  ]
                                              ]
                                          ]
                                      ]
                                  ]
                                  (Ty.path "bool")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [ Ty.path "move_binary_format::file_format::FunctionDefinition"
                                    ],
                                  [],
                                  "enumerate",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::FunctionDefinition"
                                        ],
                                      "iter",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::CompiledModule",
                                          "function_defs",
                                          []
                                        |),
                                        [ M.read (| module |) ]
                                      |)
                                    ]
                                  |)
                                ]
                              |);
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            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 fdef := M.alloc (| γ1_1 |) in
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| M.read (| fdef |) |),
                                                    "move_binary_format::file_format::FunctionDefinition",
                                                    "is_entry"
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::filter::Filter")
                                          []
                                          [
                                            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"
                                                  ]
                                              ];
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.path "usize";
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::FunctionDefinition"
                                                              ]
                                                          ]
                                                      ]
                                                  ]
                                              ]
                                              (Ty.path "bool")
                                          ],
                                        [],
                                        "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 _fdef := M.copy (| γ1_1 |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                Ty.apply
                                                  (Ty.path "core::result::Result")
                                                  []
                                                  [
                                                    Ty.tuple [];
                                                    Ty.path "move_binary_format::errors::VMError"
                                                  ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "move_bytecode_verifier::script_signature::verify_module_function_signature",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| module |);
                                                    Value.StructTuple
                                                      "move_binary_format::file_format::FunctionDefinitionIndex"
                                                      [ M.rust_cast (M.read (| idx |)) ];
                                                    M.read (| check_signature |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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::VMError"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible";
                                                                  Ty.path
                                                                    "move_binary_format::errors::VMError"
                                                                ]
                                                            ],
                                                            "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 Function_verify_module :
    M.IsFunction "move_bytecode_verifier::script_signature::verify_module" verify_module.
  
  (*
  pub fn verify_module_function_signature_by_name(
      module: &CompiledModule,
      name: &IdentStr,
      check_signature: FnCheckScriptSignature,
  ) -> VMResult<()> {
      let fdef_opt = module.function_defs().iter().enumerate().find(|(_, fdef)| {
          module.identifier_at(module.function_handle_at(fdef.function).name) == name
      });
      let (idx, _fdef) = fdef_opt.ok_or_else(|| {
          PartialVMError::new(StatusCode::VERIFICATION_ERROR)
              .with_message("function not found in verify_module_script_function".to_string())
              .finish(Location::Module(module.self_id()))
      })?;
      verify_module_function_signature(
          module,
          FunctionDefinitionIndex(idx as TableIndex),
          check_signature,
      )
  }
  *)
  Definition verify_module_function_signature_by_name
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ module; name; check_signature ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        let name := M.alloc (| name |) in
        let check_signature := M.alloc (| check_signature |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ fdef_opt :=
                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" ]
                        ],
                      [],
                      "find",
                      [
                        Ty.function
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [
                                    Ty.tuple
                                      [
                                        Ty.path "usize";
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::FunctionDefinition"
                                          ]
                                      ]
                                  ]
                              ]
                          ]
                          (Ty.path "bool")
                      ]
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                            [],
                            "enumerate",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::file_format::CompiledModule",
                                    "function_defs",
                                    []
                                  |),
                                  [ M.read (| module |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    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 fdef := M.alloc (| γ1_1 |) in
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.path "move_core_types::identifier::IdentStr" ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.path "move_core_types::identifier::IdentStr" ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::CompiledModule",
                                                  "identifier_at",
                                                  []
                                                |),
                                                [
                                                  M.read (| module |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_binary_format::file_format::CompiledModule",
                                                          "function_handle_at",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| module |);
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| M.read (| fdef |) |),
                                                              "move_binary_format::file_format::FunctionDefinition",
                                                              "function"
                                                            |)
                                                          |)
                                                        ]
                                                      |),
                                                      "move_binary_format::file_format::FunctionHandle",
                                                      "name"
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |);
                                            name
                                          ]
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                |) in
              M.match_operator (|
                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 "usize";
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                              ];
                            Ty.path "move_binary_format::errors::VMError"
                          ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path "usize";
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ]
                                  ]
                              ],
                            "ok_or_else",
                            [
                              Ty.path "move_binary_format::errors::VMError";
                              Ty.function
                                [ Ty.tuple [] ]
                                (Ty.path "move_binary_format::errors::VMError")
                            ]
                          |),
                          [
                            M.read (| fdef_opt |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "finish",
                                                  []
                                                |),
                                                [
                                                  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::VERIFICATION_ERROR"
                                                            []
                                                        ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "alloc::string::ToString",
                                                          Ty.path "str",
                                                          [],
                                                          "to_string",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "function not found in verify_module_script_function"
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |);
                                                  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))
                          ]
                        |)
                      ]
                    |)
                  |),
                  [
                    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::VMError"
                                      ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "move_binary_format::errors::VMError"
                                        ]
                                    ],
                                    "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 γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let idx := M.copy (| γ0_0 |) in
                      let _fdef := M.copy (| γ0_1 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "move_bytecode_verifier::script_signature::verify_module_function_signature",
                            []
                          |),
                          [
                            M.read (| module |);
                            Value.StructTuple
                              "move_binary_format::file_format::FunctionDefinitionIndex"
                              [ M.rust_cast (M.read (| idx |)) ];
                            M.read (| check_signature |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_module_function_signature_by_name :
    M.IsFunction
      "move_bytecode_verifier::script_signature::verify_module_function_signature_by_name"
      verify_module_function_signature_by_name.
  
  (*
  fn verify_module_function_signature(
      module: &CompiledModule,
      idx: FunctionDefinitionIndex,
      check_signature: FnCheckScriptSignature,
  ) -> VMResult<()> {
      let fdef = module.function_def_at(idx);
  
      let fhandle = module.function_handle_at(fdef.function);
      let parameters = fhandle.parameters;
      let return_ = fhandle.return_;
      verify_main_signature_impl(
          module,
          fdef.is_entry,
          parameters,
          Some(return_),
          check_signature,
      )
      .map_err(|e| {
          e.at_index(IndexKind::FunctionDefinition, idx.0)
              .finish(Location::Module(module.self_id()))
      })
  }
  *)
  Definition verify_module_function_signature
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ module; idx; check_signature ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        let idx := M.alloc (| idx |) in
        let check_signature := M.alloc (| check_signature |) in
        M.read (|
          let~ fdef :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_binary_format::file_format::CompiledModule",
                  "function_def_at",
                  []
                |),
                [ M.read (| module |); M.read (| idx |) ]
              |)
            |) in
          let~ fhandle :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_binary_format::file_format::CompiledModule",
                  "function_handle_at",
                  []
                |),
                [
                  M.read (| module |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| fdef |),
                      "move_binary_format::file_format::FunctionDefinition",
                      "function"
                    |)
                  |)
                ]
              |)
            |) in
          let~ parameters :=
            M.copy (|
              M.SubPointer.get_struct_record_field (|
                M.read (| fhandle |),
                "move_binary_format::file_format::FunctionHandle",
                "parameters"
              |)
            |) in
          let~ return_ :=
            M.copy (|
              M.SubPointer.get_struct_record_field (|
                M.read (| fhandle |),
                "move_binary_format::file_format::FunctionHandle",
                "return_"
              |)
            |) in
          M.alloc (|
            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_function (|
                    "move_bytecode_verifier::script_signature::verify_main_signature_impl",
                    []
                  |),
                  [
                    M.read (| module |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| fdef |),
                        "move_binary_format::file_format::FunctionDefinition",
                        "is_entry"
                      |)
                    |);
                    M.read (| parameters |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| return_ |) ];
                    M.read (| check_signature |)
                  ]
                |);
                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.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "at_index",
                                          []
                                        |),
                                        [
                                          M.read (| e |);
                                          Value.StructTuple
                                            "move_binary_format::IndexKind::FunctionDefinition"
                                            [];
                                          M.read (|
                                            M.SubPointer.get_struct_tuple_field (|
                                              idx,
                                              "move_binary_format::file_format::FunctionDefinitionIndex",
                                              0
                                            |)
                                          |)
                                        ]
                                      |);
                                      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 Function_verify_module_function_signature :
    M.IsFunction
      "move_bytecode_verifier::script_signature::verify_module_function_signature"
      verify_module_function_signature.
  
  (*
  fn verify_main_signature_impl(
      module: &CompiledModule,
      is_entry: bool,
      parameters_idx: SignatureIndex,
      return_idx: Option<SignatureIndex>,
      check_signature: FnCheckScriptSignature,
  ) -> PartialVMResult<()> {
      let deprecated_logic = module.version() < VERSION_5 && is_entry;
  
      if deprecated_logic {
          legacy_script_signature_checks(module, is_entry, parameters_idx, return_idx)?;
      }
      check_signature(module, is_entry, parameters_idx, return_idx)
  }
  *)
  Definition verify_main_signature_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ module; is_entry; parameters_idx; return_idx; check_signature ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        let is_entry := M.alloc (| is_entry |) in
        let parameters_idx := M.alloc (| parameters_idx |) in
        let return_idx := M.alloc (| return_idx |) in
        let check_signature := M.alloc (| check_signature |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ deprecated_logic :=
                M.alloc (|
                  LogicalOp.and (|
                    BinOp.lt (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_binary_format::file_format::CompiledModule",
                          "version",
                          []
                        |),
                        [ M.read (| module |) ]
                      |),
                      M.read (|
                        M.get_constant (| "move_binary_format::file_format_common::VERSION_5" |)
                      |)
                    |),
                    ltac:(M.monadic (M.read (| is_entry |)))
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use deprecated_logic in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.tuple [];
                                      Ty.path "move_binary_format::errors::PartialVMError"
                                    ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_function (|
                                      "move_bytecode_verifier::script_signature::legacy_script_signature_checks",
                                      []
                                    |),
                                    [
                                      M.read (| module |);
                                      M.read (| is_entry |);
                                      M.read (| parameters_idx |);
                                      M.read (| return_idx |)
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Break",
                                      0
                                    |) in
                                  let residual := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::FromResidual",
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                []
                                                [
                                                  Ty.tuple [];
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError"
                                                ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::result::Result")
                                                  []
                                                  [
                                                    Ty.path "core::convert::Infallible";
                                                    Ty.path
                                                      "move_binary_format::errors::PartialVMError"
                                                  ]
                                              ],
                                              "from_residual",
                                              []
                                            |),
                                            [ M.read (| residual |) ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Continue",
                                      0
                                    |) in
                                  let val := M.copy (| γ0_0 |) in
                                  val))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.read (| check_signature |),
                  [
                    M.read (| module |);
                    M.read (| is_entry |);
                    M.read (| parameters_idx |);
                    M.read (| return_idx |)
                  ]
                |)
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_main_signature_impl :
    M.IsFunction
      "move_bytecode_verifier::script_signature::verify_main_signature_impl"
      verify_main_signature_impl.
  
  (*
  pub fn no_additional_script_signature_checks(
      _resolver: &CompiledModule,
      _is_entry: bool,
      _parameters: SignatureIndex,
      _return_type: Option<SignatureIndex>,
  ) -> PartialVMResult<()> {
      Ok(())
  }
  *)
  Definition no_additional_script_signature_checks
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ _resolver; _is_entry; _parameters; _return_type ] =>
      ltac:(M.monadic
        (let _resolver := M.alloc (| _resolver |) in
        let _is_entry := M.alloc (| _is_entry |) in
        let _parameters := M.alloc (| _parameters |) in
        let _return_type := M.alloc (| _return_type |) in
        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_no_additional_script_signature_checks :
    M.IsFunction
      "move_bytecode_verifier::script_signature::no_additional_script_signature_checks"
      no_additional_script_signature_checks.
  
  (*
  pub fn legacy_script_signature_checks(
      module: &CompiledModule,
      _is_entry: bool,
      parameters_idx: SignatureIndex,
      return_idx: Option<SignatureIndex>,
  ) -> PartialVMResult<()> {
      use SignatureToken as S;
      let empty_vec = &vec![];
      let parameters = &module.signature_at(parameters_idx).0;
      let return_types = return_idx
          .map(|idx| &module.signature_at(idx).0)
          .unwrap_or(empty_vec);
      // Check that all `signer` arguments occur before non-`signer` arguments
      // signer is a type that can only be populated by the Move VM. And its value is filled
      // based on the sender of the transaction
      let all_args_have_valid_type = if module.version() <= VERSION_1 {
          parameters
              .iter()
              .skip_while(|typ| matches!(typ, S::Reference(inner) if matches!(&**inner, S::Signer)))
              .all(|typ| typ.is_valid_for_constant())
      } else {
          parameters
              .iter()
              .skip_while(|typ| matches!(typ, S::Signer))
              .all(|typ| typ.is_valid_for_constant())
      };
      let has_valid_return_type = return_types.is_empty();
      if !all_args_have_valid_type || !has_valid_return_type {
          Err(PartialVMError::new(
              StatusCode::INVALID_MAIN_FUNCTION_SIGNATURE,
          ))
      } else {
          Ok(())
      }
  }
  *)
  Definition legacy_script_signature_checks
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ module; _is_entry; parameters_idx; return_idx ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        let _is_entry := M.alloc (| _is_entry |) in
        let parameters_idx := M.alloc (| parameters_idx |) in
        let return_idx := M.alloc (| return_idx |) in
        M.read (|
          let~ empty_vec :=
            M.alloc (|
              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"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |)
            |) in
          let~ parameters :=
            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 (| module |); M.read (| parameters_idx |) ]
                |),
                "move_binary_format::file_format::Signature",
                0
              |)
            |) in
          let~ return_types :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.path "move_binary_format::file_format::SignatureToken";
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                    ],
                  "unwrap_or",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "move_binary_format::file_format::SignatureIndex" ],
                      "map",
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path "move_binary_format::file_format::SignatureToken";
                                Ty.path "alloc::alloc::Global"
                              ]
                          ];
                        Ty.function
                          [ Ty.tuple [ Ty.path "move_binary_format::file_format::SignatureIndex" ] ]
                          (Ty.apply
                            (Ty.path "&")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.path "move_binary_format::file_format::SignatureToken";
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ])
                      ]
                    |),
                    [
                      M.read (| return_idx |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let idx := M.copy (| γ |) in
                                        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 (| module |); M.read (| idx |) ]
                                          |),
                                          "move_binary_format::file_format::Signature",
                                          0
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |);
                  M.read (| empty_vec |)
                ]
              |)
            |) in
          let~ all_args_have_valid_type :=
            M.copy (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::CompiledModule",
                                  "version",
                                  []
                                |),
                                [ M.read (| module |) ]
                              |),
                              M.read (|
                                M.get_constant (|
                                  "move_binary_format::file_format_common::VERSION_1"
                                |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::skip_while::SkipWhile")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::SignatureToken" ];
                                Ty.function
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::SignatureToken"
                                              ]
                                          ]
                                      ]
                                  ]
                                  (Ty.path "bool")
                              ],
                            [],
                            "all",
                            [
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "move_binary_format::file_format::SignatureToken"
                                        ]
                                    ]
                                ]
                                (Ty.path "bool")
                            ]
                          |),
                          [
                            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" ],
                                  [],
                                  "skip_while",
                                  [
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::SignatureToken"
                                                  ]
                                              ]
                                          ]
                                      ]
                                      (Ty.path "bool")
                                  ]
                                |),
                                [
                                  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 (| parameters |) ]
                                      |)
                                    ]
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let typ := M.copy (| γ |) in
                                                    M.read (|
                                                      M.match_operator (|
                                                        typ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ := M.read (| γ |) in
                                                              let γ2_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "move_binary_format::file_format::SignatureToken::Reference",
                                                                  0
                                                                |) in
                                                              let inner := M.alloc (| γ2_0 |) in
                                                              let γ :=
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.read (| M.read (| inner |) |)
                                                                  |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let γ := M.read (| γ |) in
                                                                        let _ :=
                                                                          M.is_struct_tuple (|
                                                                            γ,
                                                                            "move_binary_format::file_format::SignatureToken::Signer"
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Bool true
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (M.alloc (|
                                                                          Value.Bool false
                                                                        |)))
                                                                  ]
                                                                |) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (| Value.Bool true |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Bool false |)))
                                                        ]
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let typ := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken",
                                                  "is_valid_for_constant",
                                                  []
                                                |),
                                                [ M.read (| typ |) ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::skip_while::SkipWhile")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_binary_format::file_format::SignatureToken" ];
                                Ty.function
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::SignatureToken"
                                              ]
                                          ]
                                      ]
                                  ]
                                  (Ty.path "bool")
                              ],
                            [],
                            "all",
                            [
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "move_binary_format::file_format::SignatureToken"
                                        ]
                                    ]
                                ]
                                (Ty.path "bool")
                            ]
                          |),
                          [
                            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" ],
                                  [],
                                  "skip_while",
                                  [
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::SignatureToken"
                                                  ]
                                              ]
                                          ]
                                      ]
                                      (Ty.path "bool")
                                  ]
                                |),
                                [
                                  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 (| parameters |) ]
                                      |)
                                    ]
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let typ := M.copy (| γ |) in
                                                    M.read (|
                                                      M.match_operator (|
                                                        typ,
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ := M.read (| γ |) in
                                                              let γ := M.read (| γ |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "move_binary_format::file_format::SignatureToken::Signer"
                                                                |) in
                                                              M.alloc (| Value.Bool true |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Bool false |)))
                                                        ]
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let typ := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken",
                                                  "is_valid_for_constant",
                                                  []
                                                |),
                                                [ M.read (| typ |) ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |)))
                ]
              |)
            |) in
          let~ has_valid_return_type :=
            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"
                    ],
                  "is_empty",
                  []
                |),
                [ M.read (| return_types |) ]
              |)
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        LogicalOp.or (|
                          UnOp.not (| M.read (| all_args_have_valid_type |) |),
                          ltac:(M.monadic (UnOp.not (| M.read (| has_valid_return_type |) |)))
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_binary_format::errors::PartialVMError",
                            "new",
                            []
                          |),
                          [
                            Value.StructTuple
                              "move_core_types::vm_status::StatusCode::INVALID_MAIN_FUNCTION_SIGNATURE"
                              []
                          ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_legacy_script_signature_checks :
    M.IsFunction
      "move_bytecode_verifier::script_signature::legacy_script_signature_checks"
      legacy_script_signature_checks.
End script_signature.
