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

Module verifier.
  (*
  pub fn verify_module_unmetered(module: &CompiledModule) -> VMResult<()> {
      verify_module_with_config_unmetered(&VerifierConfig::default(), module)
  }
  *)
  Definition verify_module_unmetered (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ module ] =>
      ltac:(M.monadic
        (let module := M.alloc (| module |) in
        M.call_closure (|
          M.get_function (|
            "move_bytecode_verifier::verifier::verify_module_with_config_unmetered",
            []
          |),
          [
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "move_vm_config::verifier::VerifierConfig",
                  [],
                  "default",
                  []
                |),
                []
              |)
            |);
            M.read (| module |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_module_unmetered :
    M.IsFunction
      "move_bytecode_verifier::verifier::verify_module_unmetered"
      verify_module_unmetered.
  
  (*
  pub fn verify_module_with_config_for_test(
      name: &str,
      config: &VerifierConfig,
      module: &CompiledModule,
      meter: &mut (impl Meter + ?Sized),
  ) -> VMResult<()> {
      const MAX_MODULE_SIZE: usize = 65355;
      let mut bytes = vec![];
      module.serialize(&mut bytes).unwrap();
      let now = Instant::now();
      let result = verify_module_with_config_metered(config, module, meter);
      eprintln!(
          "--> {}: verification time: {:.3}ms, result: {}, size: {}kb",
          name,
          (now.elapsed().as_micros() as f64) / 1000.0,
          if let Err(e) = &result {
              format!("{:?}", e.major_status())
          } else {
              "Ok".to_string()
          },
          bytes.len() / 1000
      );
      // Also check whether the module actually fits into our payload size
      assert!(
          bytes.len() <= MAX_MODULE_SIZE,
          "test module exceeds size limit {} (given size {})",
          MAX_MODULE_SIZE,
          bytes.len()
      );
      result
  }
  *)
  Definition verify_module_with_config_for_test
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [ impl_Meter__plus___Sized ], [ name; config; module; meter ] =>
      ltac:(M.monadic
        (let name := M.alloc (| name |) in
        let config := M.alloc (| config |) in
        let module := M.alloc (| module |) in
        let meter := M.alloc (| meter |) in
        M.read (|
          let~ bytes :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  "new",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.tuple []; Ty.path "anyhow::Error" ],
                  "unwrap",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "move_binary_format::file_format::CompiledModule",
                      "serialize",
                      []
                    |),
                    [ M.read (| module |); bytes ]
                  |)
                ]
              |)
            |) in
          let~ now :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "std::time::Instant", "now", [] |),
                []
              |)
            |) in
          let~ result :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "move_bytecode_verifier::verifier::verify_module_with_config_metered",
                  [ impl_Meter__plus___Sized ]
                |),
                [ M.read (| config |); M.read (| module |); M.read (| meter |) ]
              |)
            |) in
          let~ _ :=
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "std::io::stdio::_eprint", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Arguments",
                        "new_v1_formatted",
                        []
                      |),
                      [
                        M.alloc (|
                          Value.Array
                            [
                              M.read (| Value.String "--> " |);
                              M.read (| Value.String ": verification time: " |);
                              M.read (| Value.String "ms, result: " |);
                              M.read (| Value.String ", size: " |);
                              M.read (| Value.String "kb
" |)
                            ]
                        |);
                        M.alloc (|
                          Value.Array
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_display",
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                |),
                                [ name ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_display",
                                  [ Ty.path "f64" ]
                                |),
                                [
                                  M.alloc (|
                                    BinOp.Wrap.div (|
                                      M.rust_cast
                                        (M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::time::Duration",
                                            "as_micros",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "std::time::Instant",
                                                  "elapsed",
                                                  []
                                                |),
                                                [ now ]
                                              |)
                                            |)
                                          ]
                                        |)),
                                      M.read (| UnsupportedLiteral |)
                                    |)
                                  |)
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_display",
                                  [ Ty.path "alloc::string::String" ]
                                |),
                                [
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.alloc (| result |) in
                                          let γ := M.read (| γ |) in
                                          let γ1_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::result::Result::Err",
                                              0
                                            |) in
                                          let e := M.alloc (| γ1_0 |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::hint::must_use",
                                                [ Ty.path "alloc::string::String" ]
                                              |),
                                              [
                                                M.read (|
                                                  let~ res :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "alloc::fmt::format",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Arguments",
                                                              "new_v1",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [ M.read (| Value.String "" |) ]
                                                              |);
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::fmt::rt::Argument",
                                                                        "new_debug",
                                                                        [
                                                                          Ty.path
                                                                            "move_core_types::vm_status::StatusCode"
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_binary_format::errors::VMError",
                                                                              "major_status",
                                                                              []
                                                                            |),
                                                                            [ M.read (| e |) ]
                                                                          |)
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  res
                                                |)
                                              ]
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "alloc::string::ToString",
                                                Ty.path "str",
                                                [],
                                                "to_string",
                                                []
                                              |),
                                              [ M.read (| Value.String "Ok" |) ]
                                            |)
                                          |)))
                                    ]
                                  |)
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_display",
                                  [ Ty.path "usize" ]
                                |),
                                [
                                  M.alloc (|
                                    BinOp.Wrap.div (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                          "len",
                                          []
                                        |),
                                        [ bytes ]
                                      |),
                                      Value.Integer IntegerKind.Usize 1000
                                    |)
                                  |)
                                ]
                              |)
                            ]
                        |);
                        M.alloc (|
                          Value.Array
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Placeholder",
                                  "new",
                                  []
                                |),
                                [
                                  Value.Integer IntegerKind.Usize 0;
                                  Value.UnicodeChar 32;
                                  Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                  Value.Integer IntegerKind.U32 0;
                                  Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                  Value.StructTuple "core::fmt::rt::Count::Implied" []
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Placeholder",
                                  "new",
                                  []
                                |),
                                [
                                  Value.Integer IntegerKind.Usize 1;
                                  Value.UnicodeChar 32;
                                  Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                  Value.Integer IntegerKind.U32 0;
                                  Value.StructTuple
                                    "core::fmt::rt::Count::Is"
                                    [ Value.Integer IntegerKind.Usize 3 ];
                                  Value.StructTuple "core::fmt::rt::Count::Implied" []
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Placeholder",
                                  "new",
                                  []
                                |),
                                [
                                  Value.Integer IntegerKind.Usize 2;
                                  Value.UnicodeChar 32;
                                  Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                  Value.Integer IntegerKind.U32 0;
                                  Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                  Value.StructTuple "core::fmt::rt::Count::Implied" []
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Placeholder",
                                  "new",
                                  []
                                |),
                                [
                                  Value.Integer IntegerKind.Usize 3;
                                  Value.UnicodeChar 32;
                                  Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                  Value.Integer IntegerKind.U32 0;
                                  Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                  Value.StructTuple "core::fmt::rt::Count::Implied" []
                                ]
                              |)
                            ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::UnsafeArg",
                            "new",
                            []
                          |),
                          []
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.le (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                  "len",
                                  []
                                |),
                                [ bytes ]
                              |),
                              M.read (|
                                M.get_constant (|
                                  "move_bytecode_verifier::verifier::verify_module_with_config_for_test::MAX_MODULE_SIZE"
                                |)
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (| Value.String "test module exceeds size limit " |);
                                      M.read (| Value.String " (given size " |);
                                      M.read (| Value.String ")" |)
                                    ]
                                |);
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.get_constant (|
                                            "move_bytecode_verifier::verifier::verify_module_with_config_for_test::MAX_MODULE_SIZE"
                                          |)
                                        ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                                "len",
                                                []
                                              |),
                                              [ bytes ]
                                            |)
                                          |)
                                        ]
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          result
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_module_with_config_for_test :
    M.IsFunction
      "move_bytecode_verifier::verifier::verify_module_with_config_for_test"
      verify_module_with_config_for_test.
  
  Module verify_module_with_config_for_test.
    Definition value_MAX_MODULE_SIZE : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 65355 |))).
  End verify_module_with_config_for_test.
  
  (*
  pub fn verify_module_with_config_metered(
      config: &VerifierConfig,
      module: &CompiledModule,
      meter: &mut (impl Meter + ?Sized),
  ) -> VMResult<()> {
      BoundsChecker::verify_module(module).map_err(|e| {
          // We can't point the error at the module, because if bounds-checking
          // failed, we cannot safely index into module's handle to itself.
          e.finish(Location::Undefined)
      })?;
      LimitsVerifier::verify_module(config, module)?;
      DuplicationChecker::verify_module(module)?;
      SignatureChecker::verify_module(module)?;
      InstructionConsistency::verify_module(module)?;
      constants::verify_module(module)?;
      friends::verify_module(module)?;
      ability_field_requirements::verify_module(module)?;
      RecursiveStructDefChecker::verify_module(module)?;
      InstantiationLoopChecker::verify_module(module)?;
      CodeUnitVerifier::verify_module(config, module, meter)?;
  
      script_signature::verify_module(module, no_additional_script_signature_checks)
  }
  *)
  Definition verify_module_with_config_metered
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [ impl_Meter__plus___Sized ], [ config; module; meter ] =>
      ltac:(M.monadic
        (let config := M.alloc (| config |) in
        let module := M.alloc (| module |) in
        let meter := M.alloc (| meter |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "move_binary_format::errors::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
                            "map_err",
                            [
                              Ty.path "move_binary_format::errors::VMError";
                              Ty.function
                                [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ]
                                ]
                                (Ty.path "move_binary_format::errors::VMError")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::check_bounds::BoundsChecker",
                                "verify_module",
                                []
                              |),
                              [ M.read (| module |) ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let e := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::errors::PartialVMError",
                                                  "finish",
                                                  []
                                                |),
                                                [
                                                  M.read (| e |);
                                                  Value.StructTuple
                                                    "move_binary_format::errors::Location::Undefined"
                                                    []
                                                ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => 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))
                  ]
                |) 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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_bytecode_verifier::limits::LimitsVerifier",
                            "verify_module",
                            []
                          |),
                          [ M.read (| config |); M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_bytecode_verifier::check_duplication::DuplicationChecker",
                            "verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_bytecode_verifier::signature::SignatureChecker",
                            "verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path
                              "move_bytecode_verifier::instruction_consistency::InstructionConsistency",
                            "verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_function (|
                            "move_bytecode_verifier::constants::verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_function (| "move_bytecode_verifier::friends::verify_module", [] |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_function (|
                            "move_bytecode_verifier::ability_field_requirements::verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path
                              "move_bytecode_verifier::struct_defs::RecursiveStructDefChecker",
                            "verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path
                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                            "verify_module",
                            []
                          |),
                          [ M.read (| module |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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
              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::VMError" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_bytecode_verifier::code_unit_verifier::CodeUnitVerifier",
                            "verify_module",
                            [ impl_Meter__plus___Sized ]
                          |),
                          [ M.read (| config |); M.read (| module |); M.read (| meter |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "move_binary_format::errors::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 (|
                M.call_closure (|
                  M.get_function (|
                    "move_bytecode_verifier::script_signature::verify_module",
                    []
                  |),
                  [
                    M.read (| module |);
                    (* ReifyFnPointer *)
                    M.pointer_coercion
                      (M.get_function (|
                        "move_bytecode_verifier::script_signature::no_additional_script_signature_checks",
                        []
                      |))
                  ]
                |)
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_module_with_config_metered :
    M.IsFunction
      "move_bytecode_verifier::verifier::verify_module_with_config_metered"
      verify_module_with_config_metered.
  
  (*
  pub fn verify_module_with_config_unmetered(
      config: &VerifierConfig,
      module: &CompiledModule,
  ) -> VMResult<()> {
      verify_module_with_config_metered(config, module, &mut DummyMeter)
  }
  *)
  Definition verify_module_with_config_unmetered
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ config; module ] =>
      ltac:(M.monadic
        (let config := M.alloc (| config |) in
        let module := M.alloc (| module |) in
        M.call_closure (|
          M.get_function (|
            "move_bytecode_verifier::verifier::verify_module_with_config_metered",
            [ Ty.path "move_bytecode_verifier_meter::dummy::DummyMeter" ]
          |),
          [
            M.read (| config |);
            M.read (| module |);
            M.alloc (| Value.StructTuple "move_bytecode_verifier_meter::dummy::DummyMeter" [] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_module_with_config_unmetered :
    M.IsFunction
      "move_bytecode_verifier::verifier::verify_module_with_config_unmetered"
      verify_module_with_config_unmetered.
End verifier.
