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

Module stack_usage_verifier.
  (* StructRecord
    {
      name := "StackUsageVerifier";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("current_function",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ]);
          ("code",
            Ty.apply (Ty.path "&") [] [ Ty.path "move_binary_format::file_format::CodeUnit" ]);
          ("return_",
            Ty.apply (Ty.path "&") [] [ Ty.path "move_binary_format::file_format::Signature" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_stack_usage_verifier_StackUsageVerifier.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier".
    
    (*
        pub(crate) fn verify(
            config: &VerifierConfig,
            module: &'a CompiledModule,
            function_context: &'a FunctionContext,
            _meter: &mut (impl Meter + ?Sized), // TODO: metering
        ) -> PartialVMResult<()> {
            let verifier = Self {
                module,
                current_function: function_context.index(),
                code: function_context.code(),
                return_: function_context.return_(),
            };
    
            for block_id in function_context.cfg().blocks() {
                verifier.verify_block(config, block_id, function_context.cfg())?
            }
            Ok(())
        }
    *)
    Definition verify (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Meter__plus___Sized ], [ config; module; function_context; _meter ] =>
        ltac:(M.monadic
          (let config := M.alloc (| config |) in
          let module := M.alloc (| module |) in
          let function_context := M.alloc (| function_context |) in
          let _meter := M.alloc (| _meter |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ verifier :=
                  M.alloc (|
                    Value.StructRecord
                      "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier"
                      [
                        ("module", M.read (| module |));
                        ("current_function",
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier::absint::FunctionContext",
                              "index",
                              []
                            |),
                            [ M.read (| function_context |) ]
                          |));
                        ("code",
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier::absint::FunctionContext",
                              "code",
                              []
                            |),
                            [ M.read (| function_context |) ]
                          |));
                        ("return_",
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier::absint::FunctionContext",
                              "return_",
                              []
                            |),
                            [ M.read (| function_context |) ]
                          |))
                      ]
                  |) 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 "alloc::vec::Vec")
                              []
                              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "move_binary_format::control_flow_graph::ControlFlowGraph",
                                Ty.path
                                  "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                [],
                                "blocks",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_bytecode_verifier::absint::FunctionContext",
                                    "cfg",
                                    []
                                  |),
                                  [ M.read (| function_context |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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 "alloc::vec::into_iter::IntoIter")
                                            []
                                            [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                          [],
                                          "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 block_id := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.tuple [];
                                                      Ty.path
                                                        "move_binary_format::errors::PartialVMError"
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                      "verify_block",
                                                      []
                                                    |),
                                                    [
                                                      verifier;
                                                      M.read (| config |);
                                                      M.read (| block_id |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_bytecode_verifier::absint::FunctionContext",
                                                          "cfg",
                                                          []
                                                        |),
                                                        [ M.read (| function_context |) ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.tuple [];
                                                                  Ty.path
                                                                    "move_binary_format::errors::PartialVMError"
                                                                ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible";
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify : M.IsAssociatedFunction Self "verify" verify.
    
    (*
        fn verify_block(
            &self,
            config: &VerifierConfig,
            block_id: BlockId,
            cfg: &dyn ControlFlowGraph,
        ) -> PartialVMResult<()> {
            let code = &self.code.code;
            let mut stack_size_increment = 0;
            let block_start = cfg.block_start(block_id);
            let mut overall_push = 0;
            for i in block_start..=cfg.block_end(block_id) {
                let (num_pops, num_pushes) = self.instruction_effect(&code[i as usize])?;
                if let Some(new_pushes) = u64::checked_add(overall_push, num_pushes) {
                    overall_push = new_pushes
                };
    
                // Check that the accumulated pushes does not exceed a pre-defined max size
                if let Some(max_push_size) = config.max_push_size {
                    if overall_push > max_push_size as u64 {
                        return Err(PartialVMError::new(StatusCode::VALUE_STACK_PUSH_OVERFLOW)
                            .at_code_offset(self.current_function(), block_start));
                    }
                }
    
                // Check that the stack height is sufficient to accommodate the number
                // of pops this instruction does
                if stack_size_increment < num_pops {
                    return Err(
                        PartialVMError::new(StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK)
                            .at_code_offset(self.current_function(), block_start),
                    );
                }
                if let Some(new_incr) = u64::checked_sub(stack_size_increment, num_pops) {
                    stack_size_increment = new_incr
                } else {
                    return Err(
                        PartialVMError::new(StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK)
                            .at_code_offset(self.current_function(), block_start),
                    );
                };
                if let Some(new_incr) = u64::checked_add(stack_size_increment, num_pushes) {
                    stack_size_increment = new_incr
                } else {
                    return Err(
                        PartialVMError::new(StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END)
                            .at_code_offset(self.current_function(), block_start),
                    );
                };
    
                if stack_size_increment > config.max_value_stack_size as u64 {
                    return Err(PartialVMError::new(StatusCode::VALUE_STACK_OVERFLOW)
                        .at_code_offset(self.current_function(), block_start));
                }
            }
    
            if stack_size_increment == 0 {
                Ok(())
            } else {
                Err(
                    PartialVMError::new(StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END)
                        .at_code_offset(self.current_function(), block_start),
                )
            }
        }
    *)
    Definition verify_block (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; config; block_id; cfg ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let config := M.alloc (| config |) in
          let block_id := M.alloc (| block_id |) in
          let cfg := M.alloc (| cfg |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ code :=
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                          "code"
                        |)
                      |),
                      "move_binary_format::file_format::CodeUnit",
                      "code"
                    |)
                  |) in
                let~ stack_size_increment := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
                let~ block_start :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "move_binary_format::control_flow_graph::ControlFlowGraph",
                        Ty.dyn
                          [ ("move_binary_format::control_flow_graph::ControlFlowGraph::Trait", [])
                          ],
                        [],
                        "block_start",
                        []
                      |),
                      [ M.read (| cfg |); M.read (| block_id |) ]
                    |)
                  |) in
                let~ overall_push := M.alloc (| Value.Integer IntegerKind.U64 0 |) 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::ops::range::RangeInclusive")
                              []
                              [ Ty.path "u16" ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "u16" ],
                                "new",
                                []
                              |),
                              [
                                M.read (| block_start |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "move_binary_format::control_flow_graph::ControlFlowGraph",
                                    Ty.dyn
                                      [
                                        ("move_binary_format::control_flow_graph::ControlFlowGraph::Trait",
                                          [])
                                      ],
                                    [],
                                    "block_end",
                                    []
                                  |),
                                  [ M.read (| cfg |); M.read (| block_id |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::ops::range::RangeInclusive")
                                            []
                                            [ Ty.path "u16" ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let i := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.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 "u64"; Ty.path "u64" ];
                                                        Ty.path
                                                          "move_binary_format::errors::PartialVMError"
                                                      ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                        "instruction_effect",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| self |);
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::Index",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::file_format::Bytecode";
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [ Ty.path "usize" ],
                                                            "index",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| code |);
                                                            M.rust_cast (M.read (| i |))
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple [];
                                                                    Ty.path
                                                                      "move_binary_format::errors::PartialVMError"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path
                                                                        "move_binary_format::errors::PartialVMError"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |),
                                            [
                                              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 num_pops := M.copy (| γ0_0 |) in
                                                  let num_pushes := M.copy (| γ0_1 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "u64",
                                                                    "checked_add",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| overall_push |);
                                                                    M.read (| num_pushes |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let new_pushes := M.copy (| γ0_0 |) in
                                                            M.write (|
                                                              overall_push,
                                                              M.read (| new_pushes |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| config |),
                                                                "move_vm_config::verifier::VerifierConfig",
                                                                "max_push_size"
                                                              |) in
                                                            let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let max_push_size :=
                                                              M.copy (| γ0_0 |) in
                                                            M.match_operator (|
                                                              M.alloc (| Value.Tuple [] |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ :=
                                                                      M.use
                                                                        (M.alloc (|
                                                                          BinOp.gt (|
                                                                            M.read (|
                                                                              overall_push
                                                                            |),
                                                                            M.rust_cast
                                                                              (M.read (|
                                                                                max_push_size
                                                                              |))
                                                                          |)
                                                                        |)) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ |),
                                                                        Value.Bool true
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (|
                                                                          M.return_ (|
                                                                            Value.StructTuple
                                                                              "core::result::Result::Err"
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.path
                                                                                      "move_binary_format::errors::PartialVMError",
                                                                                    "at_code_offset",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.path
                                                                                          "move_binary_format::errors::PartialVMError",
                                                                                        "new",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        Value.StructTuple
                                                                                          "move_core_types::vm_status::StatusCode::VALUE_STACK_PUSH_OVERFLOW"
                                                                                          []
                                                                                      ]
                                                                                    |);
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.path
                                                                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                                                        "current_function",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.read (|
                                                                                          self
                                                                                        |)
                                                                                      ]
                                                                                    |);
                                                                                    M.read (|
                                                                                      block_start
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              ]
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.lt (|
                                                                    M.read (|
                                                                      stack_size_increment
                                                                    |),
                                                                    M.read (| num_pops |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    Value.StructTuple
                                                                      "core::result::Result::Err"
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "at_code_offset",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "new",
                                                                                []
                                                                              |),
                                                                              [
                                                                                Value.StructTuple
                                                                                  "move_core_types::vm_status::StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK"
                                                                                  []
                                                                              ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                                                "current_function",
                                                                                []
                                                                              |),
                                                                              [ M.read (| self |) ]
                                                                            |);
                                                                            M.read (| block_start |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "u64",
                                                                    "checked_sub",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      stack_size_increment
                                                                    |);
                                                                    M.read (| num_pops |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let new_incr := M.copy (| γ0_0 |) in
                                                            M.write (|
                                                              stack_size_increment,
                                                              M.read (| new_incr |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    Value.StructTuple
                                                                      "core::result::Result::Err"
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "at_code_offset",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "new",
                                                                                []
                                                                              |),
                                                                              [
                                                                                Value.StructTuple
                                                                                  "move_core_types::vm_status::StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK"
                                                                                  []
                                                                              ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                                                "current_function",
                                                                                []
                                                                              |),
                                                                              [ M.read (| self |) ]
                                                                            |);
                                                                            M.read (| block_start |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "u64",
                                                                    "checked_add",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      stack_size_increment
                                                                    |);
                                                                    M.read (| num_pushes |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let new_incr := M.copy (| γ0_0 |) in
                                                            M.write (|
                                                              stack_size_increment,
                                                              M.read (| new_incr |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  M.return_ (|
                                                                    Value.StructTuple
                                                                      "core::result::Result::Err"
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_binary_format::errors::PartialVMError",
                                                                            "at_code_offset",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_binary_format::errors::PartialVMError",
                                                                                "new",
                                                                                []
                                                                              |),
                                                                              [
                                                                                Value.StructTuple
                                                                                  "move_core_types::vm_status::StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END"
                                                                                  []
                                                                              ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                                                "current_function",
                                                                                []
                                                                              |),
                                                                              [ M.read (| self |) ]
                                                                            |);
                                                                            M.read (| block_start |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.gt (|
                                                                  M.read (| stack_size_increment |),
                                                                  M.rust_cast
                                                                    (M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| config |),
                                                                        "move_vm_config::verifier::VerifierConfig",
                                                                        "max_value_stack_size"
                                                                      |)
                                                                    |))
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                M.return_ (|
                                                                  Value.StructTuple
                                                                    "core::result::Result::Err"
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "move_binary_format::errors::PartialVMError",
                                                                          "at_code_offset",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_binary_format::errors::PartialVMError",
                                                                              "new",
                                                                              []
                                                                            |),
                                                                            [
                                                                              Value.StructTuple
                                                                                "move_core_types::vm_status::StatusCode::VALUE_STACK_OVERFLOW"
                                                                                []
                                                                            ]
                                                                          |);
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.path
                                                                                "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                                                              "current_function",
                                                                              []
                                                                            |),
                                                                            [ M.read (| self |) ]
                                                                          |);
                                                                          M.read (| block_start |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (| stack_size_increment |),
                                Value.Integer IntegerKind.U64 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Err"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::errors::PartialVMError",
                                  "at_code_offset",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::errors::PartialVMError",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "move_core_types::vm_status::StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END"
                                        []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path
                                        "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                      "current_function",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |);
                                  M.read (| block_start |)
                                ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_block : M.IsAssociatedFunction Self "verify_block" verify_block.
    
    (*
        fn instruction_effect(&self, instruction: &Bytecode) -> PartialVMResult<(u64, u64)> {
            Ok(match instruction {
                // Instructions that pop, but don't push
                Bytecode::Pop
                | Bytecode::BrTrue(_)
                | Bytecode::BrFalse(_)
                | Bytecode::StLoc(_)
                | Bytecode::Abort => (1, 0),
    
                // Instructions that push, but don't pop
                Bytecode::LdU8(_)
                | Bytecode::LdU16(_)
                | Bytecode::LdU32(_)
                | Bytecode::LdU64(_)
                | Bytecode::LdU128(_)
                | Bytecode::LdU256(_)
                | Bytecode::LdTrue
                | Bytecode::LdFalse
                | Bytecode::LdConst(_)
                | Bytecode::CopyLoc(_)
                | Bytecode::MoveLoc(_)
                | Bytecode::MutBorrowLoc(_)
                | Bytecode::ImmBorrowLoc(_) => (0, 1),
    
                // Instructions that pop and push once
                Bytecode::Not
                | Bytecode::FreezeRef
                | Bytecode::ReadRef
                | Bytecode::ExistsDeprecated(_)
                | Bytecode::ExistsGenericDeprecated(_)
                | Bytecode::MutBorrowGlobalDeprecated(_)
                | Bytecode::MutBorrowGlobalGenericDeprecated(_)
                | Bytecode::ImmBorrowGlobalDeprecated(_)
                | Bytecode::ImmBorrowGlobalGenericDeprecated(_)
                | Bytecode::MutBorrowField(_)
                | Bytecode::MutBorrowFieldGeneric(_)
                | Bytecode::ImmBorrowField(_)
                | Bytecode::ImmBorrowFieldGeneric(_)
                | Bytecode::MoveFromDeprecated(_)
                | Bytecode::MoveFromGenericDeprecated(_)
                | Bytecode::CastU8
                | Bytecode::CastU16
                | Bytecode::CastU32
                | Bytecode::CastU64
                | Bytecode::CastU128
                | Bytecode::CastU256
                | Bytecode::VecLen(_)
                | Bytecode::VecPopBack(_) => (1, 1),
    
                // Binary operations (pop twice and push once)
                Bytecode::Add
                | Bytecode::Sub
                | Bytecode::Mul
                | Bytecode::Mod
                | Bytecode::Div
                | Bytecode::BitOr
                | Bytecode::BitAnd
                | Bytecode::Xor
                | Bytecode::Shl
                | Bytecode::Shr
                | Bytecode::Or
                | Bytecode::And
                | Bytecode::Eq
                | Bytecode::Neq
                | Bytecode::Lt
                | Bytecode::Gt
                | Bytecode::Le
                | Bytecode::Ge => (2, 1),
    
                // Vector packing and unpacking
                Bytecode::VecPack(_, num) => ( *num, 1),
                Bytecode::VecUnpack(_, num) => (1, *num),
    
                // Vector indexing operations (pop twice and push once)
                Bytecode::VecImmBorrow(_) | Bytecode::VecMutBorrow(_) => (2, 1),
    
                // MoveTo, WriteRef, and VecPushBack pop twice but do not push
                Bytecode::MoveToDeprecated(_)
                | Bytecode::MoveToGenericDeprecated(_)
                | Bytecode::WriteRef
                | Bytecode::VecPushBack(_) => (2, 0),
    
                // VecSwap pops three times but does not push
                Bytecode::VecSwap(_) => (3, 0),
    
                // Branch and Nop neither pops nor pushes
                Bytecode::Branch(_) | Bytecode::Nop => (0, 0),
    
                // Return performs `return_count` pops
                Bytecode::Ret => {
                    let return_count = self.return_.len();
                    (return_count as u64, 0)
                }
    
                // Call performs `arg_count` pops and `return_count` pushes
                Bytecode::Call(idx) => {
                    let function_handle = self.module.function_handle_at( *idx);
                    let arg_count = self.module.signature_at(function_handle.parameters).len() as u64;
                    let return_count = self.module.signature_at(function_handle.return_).len() as u64;
                    (arg_count, return_count)
                }
                Bytecode::CallGeneric(idx) => {
                    let func_inst = self.module.function_instantiation_at( *idx);
                    let function_handle = self.module.function_handle_at(func_inst.handle);
                    let arg_count = self.module.signature_at(function_handle.parameters).len() as u64;
                    let return_count = self.module.signature_at(function_handle.return_).len() as u64;
                    (arg_count, return_count)
                }
    
                // Pack performs `num_fields` pops and one push
                Bytecode::Pack(idx) => {
                    let struct_definition = self.module.struct_def_at( *idx);
                    let field_count = match &struct_definition.field_information {
                        // 'Native' here is an error that will be caught by the bytecode verifier later
                        StructFieldInformation::Native => 0,
                        StructFieldInformation::Declared(fields) => fields.len(),
                    };
                    (field_count as u64, 1)
                }
                Bytecode::PackGeneric(idx) => {
                    let struct_inst = self.module.struct_instantiation_at( *idx);
                    let struct_definition = self.module.struct_def_at(struct_inst.def);
                    let field_count = match &struct_definition.field_information {
                        // 'Native' here is an error that will be caught by the bytecode verifier later
                        StructFieldInformation::Native => 0,
                        StructFieldInformation::Declared(fields) => fields.len(),
                    };
                    (field_count as u64, 1)
                }
    
                // Unpack performs one pop and `num_fields` pushes
                Bytecode::Unpack(idx) => {
                    let struct_definition = self.module.struct_def_at( *idx);
                    let field_count = match &struct_definition.field_information {
                        // 'Native' here is an error that will be caught by the bytecode verifier later
                        StructFieldInformation::Native => 0,
                        StructFieldInformation::Declared(fields) => fields.len(),
                    };
                    (1, field_count as u64)
                }
                Bytecode::UnpackGeneric(idx) => {
                    let struct_inst = self.module.struct_instantiation_at( *idx);
                    let struct_definition = self.module.struct_def_at(struct_inst.def);
                    let field_count = match &struct_definition.field_information {
                        // 'Native' here is an error that will be caught by the bytecode verifier later
                        StructFieldInformation::Native => 0,
                        StructFieldInformation::Declared(fields) => fields.len(),
                    };
                    (1, field_count as u64)
                }
            })
        }
    *)
    Definition instruction_effect (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; instruction ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let instruction := M.alloc (| instruction |) in
          Value.StructTuple
            "core::result::Result::Ok"
            [
              M.read (|
                M.match_operator (|
                  instruction,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Pop"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::BrTrue",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::BrFalse",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::StLoc",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Abort"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 1;
                                          Value.Integer IntegerKind.U64 0
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU8",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU16",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU32",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU64",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU128",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdU256",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdTrue"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdFalse"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::LdConst",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CopyLoc",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MoveLoc",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MutBorrowLoc",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ImmBorrowLoc",
                                    0
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 0;
                                          Value.Integer IntegerKind.U64 1
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Not"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::FreezeRef"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ReadRef"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ExistsDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ExistsGenericDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MutBorrowGlobalDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MutBorrowGlobalGenericDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ImmBorrowGlobalDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ImmBorrowGlobalGenericDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MutBorrowField",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MutBorrowFieldGeneric",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ImmBorrowField",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::ImmBorrowFieldGeneric",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MoveFromDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MoveFromGenericDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU8"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU16"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU32"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU64"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU128"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::CastU256"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::VecLen",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::VecPopBack",
                                    0
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 1;
                                          Value.Integer IntegerKind.U64 1
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Add"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Sub"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Mul"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Mod"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Div"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::BitOr"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::BitAnd"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Xor"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Shl"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Shr"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Or"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::And"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Eq"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Neq"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Lt"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Gt"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Le"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Ge"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 2;
                                          Value.Integer IntegerKind.U64 1
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::VecPack",
                            0
                          |) in
                        let γ1_1 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::VecPack",
                            1
                          |) in
                        let num := M.alloc (| γ1_1 |) in
                        M.alloc (|
                          Value.Tuple
                            [ M.read (| M.read (| num |) |); Value.Integer IntegerKind.U64 1 ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::VecUnpack",
                            0
                          |) in
                        let γ1_1 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::VecUnpack",
                            1
                          |) in
                        let num := M.alloc (| γ1_1 |) in
                        M.alloc (|
                          Value.Tuple
                            [ Value.Integer IntegerKind.U64 1; M.read (| M.read (| num |) |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::VecImmBorrow",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::VecMutBorrow",
                                    0
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 2;
                                          Value.Integer IntegerKind.U64 1
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MoveToDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::MoveToGenericDeprecated",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::WriteRef"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::VecPushBack",
                                    0
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 2;
                                          Value.Integer IntegerKind.U64 0
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::VecSwap",
                            0
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [ Value.Integer IntegerKind.U64 3; Value.Integer IntegerKind.U64 0 ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Branch",
                                    0
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "move_binary_format::file_format::Bytecode::Nop"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.Tuple
                                        [
                                          Value.Integer IntegerKind.U64 0;
                                          Value.Integer IntegerKind.U64 0
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_binary_format::file_format::Bytecode::Ret"
                          |) in
                        let~ return_count :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::Signature",
                                "len",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "return_"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.rust_cast (M.read (| return_count |));
                              Value.Integer IntegerKind.U64 0
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::Call",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ function_handle :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "function_handle_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ arg_count :=
                          M.alloc (|
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::Signature",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "signature_at",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                          "module"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| function_handle |),
                                          "move_binary_format::file_format::FunctionHandle",
                                          "parameters"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |))
                          |) in
                        let~ return_count :=
                          M.alloc (|
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::Signature",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "signature_at",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                          "module"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| function_handle |),
                                          "move_binary_format::file_format::FunctionHandle",
                                          "return_"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |))
                          |) in
                        M.alloc (|
                          Value.Tuple [ M.read (| arg_count |); M.read (| return_count |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::CallGeneric",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ func_inst :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "function_instantiation_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ function_handle :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "function_handle_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| func_inst |),
                                    "move_binary_format::file_format::FunctionInstantiation",
                                    "handle"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ arg_count :=
                          M.alloc (|
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::Signature",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "signature_at",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                          "module"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| function_handle |),
                                          "move_binary_format::file_format::FunctionHandle",
                                          "parameters"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |))
                          |) in
                        let~ return_count :=
                          M.alloc (|
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::file_format::Signature",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "signature_at",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                          "module"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| function_handle |),
                                          "move_binary_format::file_format::FunctionHandle",
                                          "return_"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |))
                          |) in
                        M.alloc (|
                          Value.Tuple [ M.read (| arg_count |); M.read (| return_count |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::Pack",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ struct_definition :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_def_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ field_count :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| struct_definition |),
                                  "move_binary_format::file_format::StructDefinition",
                                  "field_information"
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Native"
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ1_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Declared",
                                        0
                                      |) in
                                    let fields := M.alloc (| γ1_0 |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FieldDefinition";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| fields |) ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.rust_cast (M.read (| field_count |));
                              Value.Integer IntegerKind.U64 1
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::PackGeneric",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ struct_inst :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_instantiation_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ struct_definition :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_def_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| struct_inst |),
                                    "move_binary_format::file_format::StructDefInstantiation",
                                    "def"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ field_count :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| struct_definition |),
                                  "move_binary_format::file_format::StructDefinition",
                                  "field_information"
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Native"
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ1_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Declared",
                                        0
                                      |) in
                                    let fields := M.alloc (| γ1_0 |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FieldDefinition";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| fields |) ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.rust_cast (M.read (| field_count |));
                              Value.Integer IntegerKind.U64 1
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::Unpack",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ struct_definition :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_def_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ field_count :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| struct_definition |),
                                  "move_binary_format::file_format::StructDefinition",
                                  "field_information"
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Native"
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ1_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Declared",
                                        0
                                      |) in
                                    let fields := M.alloc (| γ1_0 |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FieldDefinition";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| fields |) ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              Value.Integer IntegerKind.U64 1;
                              M.rust_cast (M.read (| field_count |))
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_binary_format::file_format::Bytecode::UnpackGeneric",
                            0
                          |) in
                        let idx := M.alloc (| γ1_0 |) in
                        let~ struct_inst :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_instantiation_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (| M.read (| idx |) |)
                              ]
                            |)
                          |) in
                        let~ struct_definition :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::CompiledModule",
                                "struct_def_at",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                                    "module"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| struct_inst |),
                                    "move_binary_format::file_format::StructDefInstantiation",
                                    "def"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ field_count :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| struct_definition |),
                                  "move_binary_format::file_format::StructDefinition",
                                  "field_information"
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let _ :=
                                      M.is_struct_tuple (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Native"
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ1_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "move_binary_format::file_format::StructFieldInformation::Declared",
                                        0
                                      |) in
                                    let fields := M.alloc (| γ1_0 |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FieldDefinition";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| fields |) ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              Value.Integer IntegerKind.U64 1;
                              M.rust_cast (M.read (| field_count |))
                            ]
                        |)))
                  ]
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_instruction_effect :
      M.IsAssociatedFunction Self "instruction_effect" instruction_effect.
    
    (*
        fn current_function(&self) -> FunctionDefinitionIndex {
            self.current_function.unwrap_or(FunctionDefinitionIndex(0))
        }
    *)
    Definition current_function (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
              "unwrap_or",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::stack_usage_verifier::StackUsageVerifier",
                  "current_function"
                |)
              |);
              Value.StructTuple
                "move_binary_format::file_format::FunctionDefinitionIndex"
                [ Value.Integer IntegerKind.U16 0 ]
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_current_function :
      M.IsAssociatedFunction Self "current_function" current_function.
  End Impl_move_bytecode_verifier_stack_usage_verifier_StackUsageVerifier.
End stack_usage_verifier.
