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

Module vm_status.
  Definition value_VALIDATION_STATUS_MIN_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 0 |) |))).
  
  Definition value_VALIDATION_STATUS_MAX_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 999 |) |))).
  
  Definition value_VERIFICATION_STATUS_MIN_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 1000 |) |))).
  
  Definition value_VERIFICATION_STATUS_MAX_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 1999 |) |))).
  
  Definition value_INVARIANT_VIOLATION_STATUS_MIN_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 2000 |) |))).
  
  Definition value_INVARIANT_VIOLATION_STATUS_MAX_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 2999 |) |))).
  
  Definition value_DESERIALIZATION_STATUS_MIN_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 3000 |) |))).
  
  Definition value_DESERIALIZATION_STATUS_MAX_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 3999 |) |))).
  
  Definition value_EXECUTION_STATUS_MIN_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 4000 |) |))).
  
  Definition value_EXECUTION_STATUS_MAX_CODE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| M.alloc (| Value.Integer IntegerKind.U64 4999 |) |))).
  
  (*
  Enum StatusType
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Validation";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Verification";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "InvariantViolation";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Deserialization";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Execution";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Unknown";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::Validation"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::vm_status::StatusType::Validation" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::Verification"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::vm_status::StatusType::Verification" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::InvariantViolation"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::vm_status::StatusType::InvariantViolation"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::Deserialization"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::vm_status::StatusType::Deserialization" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::Execution"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::vm_status::StatusType::Execution" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::vm_status::StatusType::Unknown"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::vm_status::StatusType::Unknown" []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_core_types_vm_status_StatusType.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_vm_status_StatusType.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusType" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusType" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_core_types_vm_status_StatusType.
  
  Module Impl_core_cmp_Eq_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_core_types_vm_status_StatusType.
  
  Module Impl_core_fmt_Debug_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [
              M.read (| f |);
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::Validation"
                          |) in
                        M.alloc (| M.read (| Value.String "Validation" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::Verification"
                          |) in
                        M.alloc (| M.read (| Value.String "Verification" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::InvariantViolation"
                          |) in
                        M.alloc (| M.read (| Value.String "InvariantViolation" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::Deserialization"
                          |) in
                        M.alloc (| M.read (| Value.String "Deserialization" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::Execution"
                          |) in
                        M.alloc (| M.read (| Value.String "Execution" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusType::Unknown"
                          |) in
                        M.alloc (| M.read (| Value.String "Unknown" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_vm_status_StatusType.
  
  Module Impl_core_hash_Hash_for_move_core_types_vm_status_StatusType.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusType".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusType" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                [ __self_discr; M.read (| state |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_move_core_types_vm_status_StatusType.
  
  (*
  Enum StatusCode
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "UNKNOWN_VALIDATION_STATUS";
          item := StructTuple [];
          discriminant := Some 0;
        };
        {
          name := "INVALID_SIGNATURE";
          item := StructTuple [];
          discriminant := Some 1;
        };
        {
          name := "INVALID_AUTH_KEY";
          item := StructTuple [];
          discriminant := Some 2;
        };
        {
          name := "SEQUENCE_NUMBER_TOO_OLD";
          item := StructTuple [];
          discriminant := Some 3;
        };
        {
          name := "SEQUENCE_NUMBER_TOO_NEW";
          item := StructTuple [];
          discriminant := Some 4;
        };
        {
          name := "INSUFFICIENT_BALANCE_FOR_TRANSACTION_FEE";
          item := StructTuple [];
          discriminant := Some 5;
        };
        {
          name := "TRANSACTION_EXPIRED";
          item := StructTuple [];
          discriminant := Some 6;
        };
        {
          name := "SENDING_ACCOUNT_DOES_NOT_EXIST";
          item := StructTuple [];
          discriminant := Some 7;
        };
        {
          name := "REJECTED_WRITE_SET";
          item := StructTuple [];
          discriminant := Some 8;
        };
        {
          name := "INVALID_WRITE_SET";
          item := StructTuple [];
          discriminant := Some 9;
        };
        {
          name := "EXCEEDED_MAX_TRANSACTION_SIZE";
          item := StructTuple [];
          discriminant := Some 10;
        };
        {
          name := "UNKNOWN_SCRIPT";
          item := StructTuple [];
          discriminant := Some 11;
        };
        {
          name := "UNKNOWN_MODULE";
          item := StructTuple [];
          discriminant := Some 12;
        };
        {
          name := "MAX_GAS_UNITS_EXCEEDS_MAX_GAS_UNITS_BOUND";
          item := StructTuple [];
          discriminant := Some 13;
        };
        {
          name := "MAX_GAS_UNITS_BELOW_MIN_TRANSACTION_GAS_UNITS";
          item := StructTuple [];
          discriminant := Some 14;
        };
        {
          name := "GAS_UNIT_PRICE_BELOW_MIN_BOUND";
          item := StructTuple [];
          discriminant := Some 15;
        };
        {
          name := "GAS_UNIT_PRICE_ABOVE_MAX_BOUND";
          item := StructTuple [];
          discriminant := Some 16;
        };
        {
          name := "INVALID_GAS_SPECIFIER";
          item := StructTuple [];
          discriminant := Some 17;
        };
        {
          name := "SENDING_ACCOUNT_FROZEN";
          item := StructTuple [];
          discriminant := Some 18;
        };
        {
          name := "UNABLE_TO_DESERIALIZE_ACCOUNT";
          item := StructTuple [];
          discriminant := Some 19;
        };
        {
          name := "CURRENCY_INFO_DOES_NOT_EXIST";
          item := StructTuple [];
          discriminant := Some 20;
        };
        {
          name := "INVALID_MODULE_PUBLISHER";
          item := StructTuple [];
          discriminant := Some 21;
        };
        {
          name := "NO_ACCOUNT_ROLE";
          item := StructTuple [];
          discriminant := Some 22;
        };
        {
          name := "BAD_CHAIN_ID";
          item := StructTuple [];
          discriminant := Some 23;
        };
        {
          name := "SEQUENCE_NUMBER_TOO_BIG";
          item := StructTuple [];
          discriminant := Some 24;
        };
        {
          name := "BAD_TRANSACTION_FEE_CURRENCY";
          item := StructTuple [];
          discriminant := Some 25;
        };
        {
          name := "FEATURE_UNDER_GATING";
          item := StructTuple [];
          discriminant := Some 26;
        };
        {
          name := "SECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH";
          item := StructTuple [];
          discriminant := Some 27;
        };
        {
          name := "SIGNERS_CONTAIN_DUPLICATES";
          item := StructTuple [];
          discriminant := Some 28;
        };
        {
          name := "SEQUENCE_NONCE_INVALID";
          item := StructTuple [];
          discriminant := Some 29;
        };
        {
          name := "CHAIN_ACCOUNT_INFO_DOES_NOT_EXIST";
          item := StructTuple [];
          discriminant := Some 30;
        };
        {
          name := "UNKNOWN_VERIFICATION_ERROR";
          item := StructTuple [];
          discriminant := Some 1000;
        };
        {
          name := "INDEX_OUT_OF_BOUNDS";
          item := StructTuple [];
          discriminant := Some 1001;
        };
        {
          name := "INVALID_SIGNATURE_TOKEN";
          item := StructTuple [];
          discriminant := Some 1003;
        };
        {
          name := "RECURSIVE_STRUCT_DEFINITION";
          item := StructTuple [];
          discriminant := Some 1005;
        };
        {
          name := "FIELD_MISSING_TYPE_ABILITY";
          item := StructTuple [];
          discriminant := Some 1006;
        };
        {
          name := "INVALID_FALL_THROUGH";
          item := StructTuple [];
          discriminant := Some 1007;
        };
        {
          name := "NEGATIVE_STACK_SIZE_WITHIN_BLOCK";
          item := StructTuple [];
          discriminant := Some 1009;
        };
        {
          name := "INVALID_MAIN_FUNCTION_SIGNATURE";
          item := StructTuple [];
          discriminant := Some 1011;
        };
        {
          name := "DUPLICATE_ELEMENT";
          item := StructTuple [];
          discriminant := Some 1012;
        };
        {
          name := "INVALID_MODULE_HANDLE";
          item := StructTuple [];
          discriminant := Some 1013;
        };
        {
          name := "UNIMPLEMENTED_HANDLE";
          item := StructTuple [];
          discriminant := Some 1014;
        };
        {
          name := "LOOKUP_FAILED";
          item := StructTuple [];
          discriminant := Some 1017;
        };
        {
          name := "TYPE_MISMATCH";
          item := StructTuple [];
          discriminant := Some 1020;
        };
        {
          name := "MISSING_DEPENDENCY";
          item := StructTuple [];
          discriminant := Some 1021;
        };
        {
          name := "POP_WITHOUT_DROP_ABILITY";
          item := StructTuple [];
          discriminant := Some 1023;
        };
        {
          name := "BR_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1025;
        };
        {
          name := "ABORT_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1026;
        };
        {
          name := "STLOC_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1027;
        };
        {
          name := "STLOC_UNSAFE_TO_DESTROY_ERROR";
          item := StructTuple [];
          discriminant := Some 1028;
        };
        {
          name := "UNSAFE_RET_LOCAL_OR_RESOURCE_STILL_BORROWED";
          item := StructTuple [];
          discriminant := Some 1029;
        };
        {
          name := "RET_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1030;
        };
        {
          name := "RET_BORROWED_MUTABLE_REFERENCE_ERROR";
          item := StructTuple [];
          discriminant := Some 1031;
        };
        {
          name := "FREEZEREF_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1032;
        };
        {
          name := "FREEZEREF_EXISTS_MUTABLE_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1033;
        };
        {
          name := "BORROWFIELD_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1034;
        };
        {
          name := "BORROWFIELD_BAD_FIELD_ERROR";
          item := StructTuple [];
          discriminant := Some 1035;
        };
        {
          name := "BORROWFIELD_EXISTS_MUTABLE_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1036;
        };
        {
          name := "COPYLOC_UNAVAILABLE_ERROR";
          item := StructTuple [];
          discriminant := Some 1037;
        };
        {
          name := "COPYLOC_WITHOUT_COPY_ABILITY";
          item := StructTuple [];
          discriminant := Some 1038;
        };
        {
          name := "COPYLOC_EXISTS_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1039;
        };
        {
          name := "MOVELOC_UNAVAILABLE_ERROR";
          item := StructTuple [];
          discriminant := Some 1040;
        };
        {
          name := "MOVELOC_EXISTS_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1041;
        };
        {
          name := "BORROWLOC_REFERENCE_ERROR";
          item := StructTuple [];
          discriminant := Some 1042;
        };
        {
          name := "BORROWLOC_UNAVAILABLE_ERROR";
          item := StructTuple [];
          discriminant := Some 1043;
        };
        {
          name := "BORROWLOC_EXISTS_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1044;
        };
        {
          name := "CALL_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1045;
        };
        {
          name := "CALL_BORROWED_MUTABLE_REFERENCE_ERROR";
          item := StructTuple [];
          discriminant := Some 1046;
        };
        {
          name := "PACK_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1047;
        };
        {
          name := "UNPACK_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1048;
        };
        {
          name := "READREF_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1049;
        };
        {
          name := "READREF_WITHOUT_COPY_ABILITY";
          item := StructTuple [];
          discriminant := Some 1050;
        };
        {
          name := "READREF_EXISTS_MUTABLE_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1051;
        };
        {
          name := "WRITEREF_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1052;
        };
        {
          name := "WRITEREF_WITHOUT_DROP_ABILITY";
          item := StructTuple [];
          discriminant := Some 1053;
        };
        {
          name := "WRITEREF_EXISTS_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1054;
        };
        {
          name := "WRITEREF_NO_MUTABLE_REFERENCE_ERROR";
          item := StructTuple [];
          discriminant := Some 1055;
        };
        {
          name := "INTEGER_OP_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1056;
        };
        {
          name := "BOOLEAN_OP_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1057;
        };
        {
          name := "EQUALITY_OP_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1058;
        };
        {
          name := "EXISTS_WITHOUT_KEY_ABILITY_OR_BAD_ARGUMENT";
          item := StructTuple [];
          discriminant := Some 1059;
        };
        {
          name := "BORROWGLOBAL_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1060;
        };
        {
          name := "BORROWGLOBAL_WITHOUT_KEY_ABILITY";
          item := StructTuple [];
          discriminant := Some 1061;
        };
        {
          name := "MOVEFROM_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1062;
        };
        {
          name := "MOVEFROM_WITHOUT_KEY_ABILITY";
          item := StructTuple [];
          discriminant := Some 1063;
        };
        {
          name := "MOVETO_TYPE_MISMATCH_ERROR";
          item := StructTuple [];
          discriminant := Some 1064;
        };
        {
          name := "MOVETO_WITHOUT_KEY_ABILITY";
          item := StructTuple [];
          discriminant := Some 1065;
        };
        {
          name := "MODULE_ADDRESS_DOES_NOT_MATCH_SENDER";
          item := StructTuple [];
          discriminant := Some 1067;
        };
        {
          name := "NO_MODULE_HANDLES";
          item := StructTuple [];
          discriminant := Some 1068;
        };
        {
          name := "POSITIVE_STACK_SIZE_AT_BLOCK_END";
          item := StructTuple [];
          discriminant := Some 1069;
        };
        {
          name := "MISSING_ACQUIRES_ANNOTATION";
          item := StructTuple [];
          discriminant := Some 1070;
        };
        {
          name := "EXTRANEOUS_ACQUIRES_ANNOTATION";
          item := StructTuple [];
          discriminant := Some 1071;
        };
        {
          name := "DUPLICATE_ACQUIRES_ANNOTATION";
          item := StructTuple [];
          discriminant := Some 1072;
        };
        {
          name := "INVALID_ACQUIRES_ANNOTATION";
          item := StructTuple [];
          discriminant := Some 1073;
        };
        {
          name := "GLOBAL_REFERENCE_ERROR";
          item := StructTuple [];
          discriminant := Some 1074;
        };
        {
          name := "CONSTRAINT_NOT_SATISFIED";
          item := StructTuple [];
          discriminant := Some 1075;
        };
        {
          name := "NUMBER_OF_TYPE_ARGUMENTS_MISMATCH";
          item := StructTuple [];
          discriminant := Some 1076;
        };
        {
          name := "LOOP_IN_INSTANTIATION_GRAPH";
          item := StructTuple [];
          discriminant := Some 1077;
        };
        {
          name := "ZERO_SIZED_STRUCT";
          item := StructTuple [];
          discriminant := Some 1080;
        };
        {
          name := "LINKER_ERROR";
          item := StructTuple [];
          discriminant := Some 1081;
        };
        {
          name := "INVALID_CONSTANT_TYPE";
          item := StructTuple [];
          discriminant := Some 1082;
        };
        {
          name := "MALFORMED_CONSTANT_DATA";
          item := StructTuple [];
          discriminant := Some 1083;
        };
        {
          name := "EMPTY_CODE_UNIT";
          item := StructTuple [];
          discriminant := Some 1084;
        };
        {
          name := "INVALID_LOOP_SPLIT";
          item := StructTuple [];
          discriminant := Some 1085;
        };
        {
          name := "INVALID_LOOP_BREAK";
          item := StructTuple [];
          discriminant := Some 1086;
        };
        {
          name := "INVALID_LOOP_CONTINUE";
          item := StructTuple [];
          discriminant := Some 1087;
        };
        {
          name := "UNSAFE_RET_UNUSED_VALUES_WITHOUT_DROP";
          item := StructTuple [];
          discriminant := Some 1088;
        };
        {
          name := "TOO_MANY_LOCALS";
          item := StructTuple [];
          discriminant := Some 1089;
        };
        {
          name := "GENERIC_MEMBER_OPCODE_MISMATCH";
          item := StructTuple [];
          discriminant := Some 1090;
        };
        {
          name := "FUNCTION_RESOLUTION_FAILURE";
          item := StructTuple [];
          discriminant := Some 1091;
        };
        {
          name := "INVALID_OPERATION_IN_SCRIPT";
          item := StructTuple [];
          discriminant := Some 1094;
        };
        {
          name := "DUPLICATE_MODULE_NAME";
          item := StructTuple [];
          discriminant := Some 1095;
        };
        {
          name := "BACKWARD_INCOMPATIBLE_MODULE_UPDATE";
          item := StructTuple [];
          discriminant := Some 1096;
        };
        {
          name := "CYCLIC_MODULE_DEPENDENCY";
          item := StructTuple [];
          discriminant := Some 1097;
        };
        {
          name := "NUMBER_OF_ARGUMENTS_MISMATCH";
          item := StructTuple [];
          discriminant := Some 1098;
        };
        {
          name := "INVALID_PARAM_TYPE_FOR_DESERIALIZATION";
          item := StructTuple [];
          discriminant := Some 1099;
        };
        {
          name := "FAILED_TO_DESERIALIZE_ARGUMENT";
          item := StructTuple [];
          discriminant := Some 1100;
        };
        {
          name := "NUMBER_OF_SIGNER_ARGUMENTS_MISMATCH";
          item := StructTuple [];
          discriminant := Some 1101;
        };
        {
          name := "CALLED_SCRIPT_VISIBLE_FROM_NON_SCRIPT_VISIBLE";
          item := StructTuple [];
          discriminant := Some 1102;
        };
        {
          name := "EXECUTE_ENTRY_FUNCTION_CALLED_ON_NON_ENTRY_FUNCTION";
          item := StructTuple [];
          discriminant := Some 1103;
        };
        {
          name := "INVALID_FRIEND_DECL_WITH_SELF";
          item := StructTuple [];
          discriminant := Some 1104;
        };
        {
          name := "INVALID_FRIEND_DECL_WITH_MODULES_OUTSIDE_ACCOUNT_ADDRESS";
          item := StructTuple [];
          discriminant := Some 1105;
        };
        {
          name := "INVALID_FRIEND_DECL_WITH_MODULES_IN_DEPENDENCIES";
          item := StructTuple [];
          discriminant := Some 1106;
        };
        {
          name := "CYCLIC_MODULE_FRIENDSHIP";
          item := StructTuple [];
          discriminant := Some 1107;
        };
        {
          name := "INVALID_PHANTOM_TYPE_PARAM_POSITION";
          item := StructTuple [];
          discriminant := Some 1108;
        };
        {
          name := "VEC_UPDATE_EXISTS_MUTABLE_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1109;
        };
        {
          name := "VEC_BORROW_ELEMENT_EXISTS_MUTABLE_BORROW_ERROR";
          item := StructTuple [];
          discriminant := Some 1110;
        };
        {
          name := "LOOP_MAX_DEPTH_REACHED";
          item := StructTuple [];
          discriminant := Some 1111;
        };
        {
          name := "TOO_MANY_TYPE_PARAMETERS";
          item := StructTuple [];
          discriminant := Some 1112;
        };
        {
          name := "TOO_MANY_PARAMETERS";
          item := StructTuple [];
          discriminant := Some 1113;
        };
        {
          name := "TOO_MANY_BASIC_BLOCKS";
          item := StructTuple [];
          discriminant := Some 1114;
        };
        {
          name := "VALUE_STACK_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 1115;
        };
        {
          name := "TOO_MANY_TYPE_NODES";
          item := StructTuple [];
          discriminant := Some 1116;
        };
        {
          name := "VALUE_STACK_PUSH_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 1117;
        };
        {
          name := "MAX_DEPENDENCY_DEPTH_REACHED";
          item := StructTuple [];
          discriminant := Some 1118;
        };
        {
          name := "MAX_FUNCTION_DEFINITIONS_REACHED";
          item := StructTuple [];
          discriminant := Some 1119;
        };
        {
          name := "MAX_STRUCT_DEFINITIONS_REACHED";
          item := StructTuple [];
          discriminant := Some 1120;
        };
        {
          name := "MAX_FIELD_DEFINITIONS_REACHED";
          item := StructTuple [];
          discriminant := Some 1121;
        };
        {
          name := "TOO_MANY_BACK_EDGES";
          item := StructTuple [];
          discriminant := Some 1122;
        };
        {
          name := "RESERVED_VERIFICATION_ERROR_1";
          item := StructTuple [];
          discriminant := Some 1123;
        };
        {
          name := "RESERVED_VERIFICATION_ERROR_2";
          item := StructTuple [];
          discriminant := Some 1124;
        };
        {
          name := "RESERVED_VERIFICATION_ERROR_3";
          item := StructTuple [];
          discriminant := Some 1125;
        };
        {
          name := "RESERVED_VERIFICATION_ERROR_4";
          item := StructTuple [];
          discriminant := Some 1126;
        };
        {
          name := "RESERVED_VERIFICATION_ERROR_5";
          item := StructTuple [];
          discriminant := Some 1127;
        };
        {
          name := "TOO_MANY_VECTOR_ELEMENTS";
          item := StructTuple [];
          discriminant := Some 1128;
        };
        {
          name := "IDENTIFIER_TOO_LONG";
          item := StructTuple [];
          discriminant := Some 1129;
        };
        {
          name := "PROGRAM_TOO_COMPLEX";
          item := StructTuple [];
          discriminant := Some 1130;
        };
        {
          name := "UNKNOWN_INVARIANT_VIOLATION_ERROR";
          item := StructTuple [];
          discriminant := Some 2000;
        };
        {
          name := "EMPTY_VALUE_STACK";
          item := StructTuple [];
          discriminant := Some 2003;
        };
        {
          name := "PC_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 2005;
        };
        {
          name := "VERIFICATION_ERROR";
          item := StructTuple [];
          discriminant := Some 2006;
        };
        {
          name := "STORAGE_ERROR";
          item := StructTuple [];
          discriminant := Some 2008;
        };
        {
          name := "INTERNAL_TYPE_ERROR";
          item := StructTuple [];
          discriminant := Some 2009;
        };
        {
          name := "EVENT_KEY_MISMATCH";
          item := StructTuple [];
          discriminant := Some 2010;
        };
        {
          name := "UNREACHABLE";
          item := StructTuple [];
          discriminant := Some 2011;
        };
        {
          name := "VM_STARTUP_FAILURE";
          item := StructTuple [];
          discriminant := Some 2012;
        };
        {
          name := "UNEXPECTED_ERROR_FROM_KNOWN_MOVE_FUNCTION";
          item := StructTuple [];
          discriminant := Some 2015;
        };
        {
          name := "VERIFIER_INVARIANT_VIOLATION";
          item := StructTuple [];
          discriminant := Some 2016;
        };
        {
          name := "UNEXPECTED_VERIFIER_ERROR";
          item := StructTuple [];
          discriminant := Some 2017;
        };
        {
          name := "UNEXPECTED_DESERIALIZATION_ERROR";
          item := StructTuple [];
          discriminant := Some 2018;
        };
        {
          name := "FAILED_TO_SERIALIZE_WRITE_SET_CHANGES";
          item := StructTuple [];
          discriminant := Some 2019;
        };
        {
          name := "FAILED_TO_DESERIALIZE_RESOURCE";
          item := StructTuple [];
          discriminant := Some 2020;
        };
        {
          name := "TYPE_RESOLUTION_FAILURE";
          item := StructTuple [];
          discriminant := Some 2021;
        };
        {
          name := "DUPLICATE_NATIVE_FUNCTION";
          item := StructTuple [];
          discriminant := Some 2022;
        };
        {
          name := "ARITHMETIC_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 2023;
        };
        {
          name := "UNKNOWN_BINARY_ERROR";
          item := StructTuple [];
          discriminant := Some 3000;
        };
        {
          name := "MALFORMED";
          item := StructTuple [];
          discriminant := Some 3001;
        };
        {
          name := "BAD_MAGIC";
          item := StructTuple [];
          discriminant := Some 3002;
        };
        {
          name := "UNKNOWN_VERSION";
          item := StructTuple [];
          discriminant := Some 3003;
        };
        {
          name := "UNKNOWN_TABLE_TYPE";
          item := StructTuple [];
          discriminant := Some 3004;
        };
        {
          name := "UNKNOWN_SIGNATURE_TYPE";
          item := StructTuple [];
          discriminant := Some 3005;
        };
        {
          name := "UNKNOWN_SERIALIZED_TYPE";
          item := StructTuple [];
          discriminant := Some 3006;
        };
        {
          name := "UNKNOWN_OPCODE";
          item := StructTuple [];
          discriminant := Some 3007;
        };
        {
          name := "BAD_HEADER_TABLE";
          item := StructTuple [];
          discriminant := Some 3008;
        };
        {
          name := "UNEXPECTED_SIGNATURE_TYPE";
          item := StructTuple [];
          discriminant := Some 3009;
        };
        {
          name := "DUPLICATE_TABLE";
          item := StructTuple [];
          discriminant := Some 3010;
        };
        {
          name := "UNKNOWN_ABILITY";
          item := StructTuple [];
          discriminant := Some 3013;
        };
        {
          name := "UNKNOWN_NATIVE_STRUCT_FLAG";
          item := StructTuple [];
          discriminant := Some 3014;
        };
        {
          name := "BAD_U16";
          item := StructTuple [];
          discriminant := Some 3017;
        };
        {
          name := "BAD_U32";
          item := StructTuple [];
          discriminant := Some 3018;
        };
        {
          name := "BAD_U64";
          item := StructTuple [];
          discriminant := Some 3019;
        };
        {
          name := "BAD_U128";
          item := StructTuple [];
          discriminant := Some 3020;
        };
        {
          name := "BAD_U256";
          item := StructTuple [];
          discriminant := Some 3021;
        };
        {
          name := "VALUE_SERIALIZATION_ERROR";
          item := StructTuple [];
          discriminant := Some 3022;
        };
        {
          name := "VALUE_DESERIALIZATION_ERROR";
          item := StructTuple [];
          discriminant := Some 3023;
        };
        {
          name := "CODE_DESERIALIZATION_ERROR";
          item := StructTuple [];
          discriminant := Some 3024;
        };
        {
          name := "INVALID_FLAG_BITS";
          item := StructTuple [];
          discriminant := Some 3025;
        };
        {
          name := "TRAILING_BYTES";
          item := StructTuple [];
          discriminant := Some 3026;
        };
        {
          name := "UNKNOWN_RUNTIME_STATUS";
          item := StructTuple [];
          discriminant := Some 4000;
        };
        {
          name := "EXECUTED";
          item := StructTuple [];
          discriminant := Some 4001;
        };
        {
          name := "OUT_OF_GAS";
          item := StructTuple [];
          discriminant := Some 4002;
        };
        {
          name := "RESOURCE_DOES_NOT_EXIST";
          item := StructTuple [];
          discriminant := Some 4003;
        };
        {
          name := "RESOURCE_ALREADY_EXISTS";
          item := StructTuple [];
          discriminant := Some 4004;
        };
        {
          name := "MISSING_DATA";
          item := StructTuple [];
          discriminant := Some 4008;
        };
        {
          name := "DATA_FORMAT_ERROR";
          item := StructTuple [];
          discriminant := Some 4009;
        };
        {
          name := "ABORTED";
          item := StructTuple [];
          discriminant := Some 4016;
        };
        {
          name := "ARITHMETIC_ERROR";
          item := StructTuple [];
          discriminant := Some 4017;
        };
        {
          name := "VECTOR_OPERATION_ERROR";
          item := StructTuple [];
          discriminant := Some 4018;
        };
        {
          name := "EXECUTION_STACK_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 4020;
        };
        {
          name := "CALL_STACK_OVERFLOW";
          item := StructTuple [];
          discriminant := Some 4021;
        };
        {
          name := "VM_MAX_TYPE_DEPTH_REACHED";
          item := StructTuple [];
          discriminant := Some 4024;
        };
        {
          name := "VM_MAX_VALUE_DEPTH_REACHED";
          item := StructTuple [];
          discriminant := Some 4025;
        };
        {
          name := "VM_EXTENSION_ERROR";
          item := StructTuple [];
          discriminant := Some 4026;
        };
        {
          name := "STORAGE_WRITE_LIMIT_REACHED";
          item := StructTuple [];
          discriminant := Some 4027;
        };
        {
          name := "MEMORY_LIMIT_EXCEEDED";
          item := StructTuple [];
          discriminant := Some 4028;
        };
        {
          name := "VM_MAX_TYPE_NODES_REACHED";
          item := StructTuple [];
          discriminant := Some 4029;
        };
        {
          name := "UNKNOWN_STATUS";
          item := StructTuple [];
          discriminant := Some 18446744073709551615;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_marker_Copy_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_fmt_Debug_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [
              M.read (| f |);
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VALIDATION_STATUS"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_VALIDATION_STATUS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_SIGNATURE"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_SIGNATURE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_AUTH_KEY"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_AUTH_KEY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_OLD"
                          |) in
                        M.alloc (| M.read (| Value.String "SEQUENCE_NUMBER_TOO_OLD" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_NEW"
                          |) in
                        M.alloc (| M.read (| Value.String "SEQUENCE_NUMBER_TOO_NEW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INSUFFICIENT_BALANCE_FOR_TRANSACTION_FEE"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "INSUFFICIENT_BALANCE_FOR_TRANSACTION_FEE" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TRANSACTION_EXPIRED"
                          |) in
                        M.alloc (| M.read (| Value.String "TRANSACTION_EXPIRED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SENDING_ACCOUNT_DOES_NOT_EXIST"
                          |) in
                        M.alloc (| M.read (| Value.String "SENDING_ACCOUNT_DOES_NOT_EXIST" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::REJECTED_WRITE_SET"
                          |) in
                        M.alloc (| M.read (| Value.String "REJECTED_WRITE_SET" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_WRITE_SET"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_WRITE_SET" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXCEEDED_MAX_TRANSACTION_SIZE"
                          |) in
                        M.alloc (| M.read (| Value.String "EXCEEDED_MAX_TRANSACTION_SIZE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SCRIPT"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_SCRIPT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_MODULE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_MODULE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_GAS_UNITS_EXCEEDS_MAX_GAS_UNITS_BOUND"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "MAX_GAS_UNITS_EXCEEDS_MAX_GAS_UNITS_BOUND" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_GAS_UNITS_BELOW_MIN_TRANSACTION_GAS_UNITS"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "MAX_GAS_UNITS_BELOW_MIN_TRANSACTION_GAS_UNITS" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::GAS_UNIT_PRICE_BELOW_MIN_BOUND"
                          |) in
                        M.alloc (| M.read (| Value.String "GAS_UNIT_PRICE_BELOW_MIN_BOUND" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::GAS_UNIT_PRICE_ABOVE_MAX_BOUND"
                          |) in
                        M.alloc (| M.read (| Value.String "GAS_UNIT_PRICE_ABOVE_MAX_BOUND" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_GAS_SPECIFIER"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_GAS_SPECIFIER" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SENDING_ACCOUNT_FROZEN"
                          |) in
                        M.alloc (| M.read (| Value.String "SENDING_ACCOUNT_FROZEN" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNABLE_TO_DESERIALIZE_ACCOUNT"
                          |) in
                        M.alloc (| M.read (| Value.String "UNABLE_TO_DESERIALIZE_ACCOUNT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CURRENCY_INFO_DOES_NOT_EXIST"
                          |) in
                        M.alloc (| M.read (| Value.String "CURRENCY_INFO_DOES_NOT_EXIST" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_MODULE_PUBLISHER"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_MODULE_PUBLISHER" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NO_ACCOUNT_ROLE"
                          |) in
                        M.alloc (| M.read (| Value.String "NO_ACCOUNT_ROLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_CHAIN_ID"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_CHAIN_ID" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_BIG"
                          |) in
                        M.alloc (| M.read (| Value.String "SEQUENCE_NUMBER_TOO_BIG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_TRANSACTION_FEE_CURRENCY"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_TRANSACTION_FEE_CURRENCY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FEATURE_UNDER_GATING"
                          |) in
                        M.alloc (| M.read (| Value.String "FEATURE_UNDER_GATING" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "SECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SIGNERS_CONTAIN_DUPLICATES"
                          |) in
                        M.alloc (| M.read (| Value.String "SIGNERS_CONTAIN_DUPLICATES" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NONCE_INVALID"
                          |) in
                        M.alloc (| M.read (| Value.String "SEQUENCE_NONCE_INVALID" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CHAIN_ACCOUNT_INFO_DOES_NOT_EXIST"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "CHAIN_ACCOUNT_INFO_DOES_NOT_EXIST" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VERIFICATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_VERIFICATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INDEX_OUT_OF_BOUNDS"
                          |) in
                        M.alloc (| M.read (| Value.String "INDEX_OUT_OF_BOUNDS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_SIGNATURE_TOKEN"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_SIGNATURE_TOKEN" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RECURSIVE_STRUCT_DEFINITION"
                          |) in
                        M.alloc (| M.read (| Value.String "RECURSIVE_STRUCT_DEFINITION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FIELD_MISSING_TYPE_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "FIELD_MISSING_TYPE_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_FALL_THROUGH"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_FALL_THROUGH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "NEGATIVE_STACK_SIZE_WITHIN_BLOCK" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_MAIN_FUNCTION_SIGNATURE"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_MAIN_FUNCTION_SIGNATURE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DUPLICATE_ELEMENT"
                          |) in
                        M.alloc (| M.read (| Value.String "DUPLICATE_ELEMENT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_MODULE_HANDLE"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_MODULE_HANDLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNIMPLEMENTED_HANDLE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNIMPLEMENTED_HANDLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::LOOKUP_FAILED"
                          |) in
                        M.alloc (| M.read (| Value.String "LOOKUP_FAILED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TYPE_MISMATCH"
                          |) in
                        M.alloc (| M.read (| Value.String "TYPE_MISMATCH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MISSING_DEPENDENCY"
                          |) in
                        M.alloc (| M.read (| Value.String "MISSING_DEPENDENCY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::POP_WITHOUT_DROP_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "POP_WITHOUT_DROP_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BR_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BR_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::ABORT_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "ABORT_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::STLOC_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "STLOC_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::STLOC_UNSAFE_TO_DESTROY_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "STLOC_UNSAFE_TO_DESTROY_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNSAFE_RET_LOCAL_OR_RESOURCE_STILL_BORROWED"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "UNSAFE_RET_LOCAL_OR_RESOURCE_STILL_BORROWED" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RET_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "RET_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RET_BORROWED_MUTABLE_REFERENCE_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "RET_BORROWED_MUTABLE_REFERENCE_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FREEZEREF_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "FREEZEREF_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FREEZEREF_EXISTS_MUTABLE_BORROW_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "FREEZEREF_EXISTS_MUTABLE_BORROW_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BORROWFIELD_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_BAD_FIELD_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BORROWFIELD_BAD_FIELD_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_EXISTS_MUTABLE_BORROW_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "BORROWFIELD_EXISTS_MUTABLE_BORROW_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::COPYLOC_UNAVAILABLE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "COPYLOC_UNAVAILABLE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::COPYLOC_WITHOUT_COPY_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "COPYLOC_WITHOUT_COPY_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::COPYLOC_EXISTS_BORROW_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "COPYLOC_EXISTS_BORROW_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVELOC_UNAVAILABLE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVELOC_UNAVAILABLE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVELOC_EXISTS_BORROW_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVELOC_EXISTS_BORROW_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWLOC_REFERENCE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BORROWLOC_REFERENCE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWLOC_UNAVAILABLE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BORROWLOC_UNAVAILABLE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWLOC_EXISTS_BORROW_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BORROWLOC_EXISTS_BORROW_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CALL_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "CALL_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CALL_BORROWED_MUTABLE_REFERENCE_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "CALL_BORROWED_MUTABLE_REFERENCE_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::PACK_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "PACK_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNPACK_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "UNPACK_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::READREF_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "READREF_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::READREF_WITHOUT_COPY_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "READREF_WITHOUT_COPY_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::READREF_EXISTS_MUTABLE_BORROW_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "READREF_EXISTS_MUTABLE_BORROW_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::WRITEREF_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "WRITEREF_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::WRITEREF_WITHOUT_DROP_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "WRITEREF_WITHOUT_DROP_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::WRITEREF_EXISTS_BORROW_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "WRITEREF_EXISTS_BORROW_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::WRITEREF_NO_MUTABLE_REFERENCE_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "WRITEREF_NO_MUTABLE_REFERENCE_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INTEGER_OP_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "INTEGER_OP_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BOOLEAN_OP_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "BOOLEAN_OP_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EQUALITY_OP_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "EQUALITY_OP_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXISTS_WITHOUT_KEY_ABILITY_OR_BAD_ARGUMENT"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "EXISTS_WITHOUT_KEY_ABILITY_OR_BAD_ARGUMENT" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWGLOBAL_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "BORROWGLOBAL_TYPE_MISMATCH_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BORROWGLOBAL_WITHOUT_KEY_ABILITY"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "BORROWGLOBAL_WITHOUT_KEY_ABILITY" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVEFROM_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVEFROM_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVEFROM_WITHOUT_KEY_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVEFROM_WITHOUT_KEY_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVETO_TYPE_MISMATCH_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVETO_TYPE_MISMATCH_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MOVETO_WITHOUT_KEY_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "MOVETO_WITHOUT_KEY_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MODULE_ADDRESS_DOES_NOT_MATCH_SENDER"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "MODULE_ADDRESS_DOES_NOT_MATCH_SENDER" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NO_MODULE_HANDLES"
                          |) in
                        M.alloc (| M.read (| Value.String "NO_MODULE_HANDLES" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "POSITIVE_STACK_SIZE_AT_BLOCK_END" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MISSING_ACQUIRES_ANNOTATION"
                          |) in
                        M.alloc (| M.read (| Value.String "MISSING_ACQUIRES_ANNOTATION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXTRANEOUS_ACQUIRES_ANNOTATION"
                          |) in
                        M.alloc (| M.read (| Value.String "EXTRANEOUS_ACQUIRES_ANNOTATION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DUPLICATE_ACQUIRES_ANNOTATION"
                          |) in
                        M.alloc (| M.read (| Value.String "DUPLICATE_ACQUIRES_ANNOTATION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_ACQUIRES_ANNOTATION"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_ACQUIRES_ANNOTATION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::GLOBAL_REFERENCE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "GLOBAL_REFERENCE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CONSTRAINT_NOT_SATISFIED"
                          |) in
                        M.alloc (| M.read (| Value.String "CONSTRAINT_NOT_SATISFIED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "NUMBER_OF_TYPE_ARGUMENTS_MISMATCH" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::LOOP_IN_INSTANTIATION_GRAPH"
                          |) in
                        M.alloc (| M.read (| Value.String "LOOP_IN_INSTANTIATION_GRAPH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::ZERO_SIZED_STRUCT"
                          |) in
                        M.alloc (| M.read (| Value.String "ZERO_SIZED_STRUCT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::LINKER_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "LINKER_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_CONSTANT_TYPE"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_CONSTANT_TYPE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MALFORMED_CONSTANT_DATA"
                          |) in
                        M.alloc (| M.read (| Value.String "MALFORMED_CONSTANT_DATA" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EMPTY_CODE_UNIT"
                          |) in
                        M.alloc (| M.read (| Value.String "EMPTY_CODE_UNIT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_SPLIT"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_LOOP_SPLIT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_BREAK"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_LOOP_BREAK" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_CONTINUE"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_LOOP_CONTINUE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNSAFE_RET_UNUSED_VALUES_WITHOUT_DROP"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "UNSAFE_RET_UNUSED_VALUES_WITHOUT_DROP" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_LOCALS"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_LOCALS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH"
                          |) in
                        M.alloc (| M.read (| Value.String "GENERIC_MEMBER_OPCODE_MISMATCH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FUNCTION_RESOLUTION_FAILURE"
                          |) in
                        M.alloc (| M.read (| Value.String "FUNCTION_RESOLUTION_FAILURE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_OPERATION_IN_SCRIPT"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_OPERATION_IN_SCRIPT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DUPLICATE_MODULE_NAME"
                          |) in
                        M.alloc (| M.read (| Value.String "DUPLICATE_MODULE_NAME" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "BACKWARD_INCOMPATIBLE_MODULE_UPDATE" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CYCLIC_MODULE_DEPENDENCY"
                          |) in
                        M.alloc (| M.read (| Value.String "CYCLIC_MODULE_DEPENDENCY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_ARGUMENTS_MISMATCH"
                          |) in
                        M.alloc (| M.read (| Value.String "NUMBER_OF_ARGUMENTS_MISMATCH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_PARAM_TYPE_FOR_DESERIALIZATION"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "INVALID_PARAM_TYPE_FOR_DESERIALIZATION" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FAILED_TO_DESERIALIZE_ARGUMENT"
                          |) in
                        M.alloc (| M.read (| Value.String "FAILED_TO_DESERIALIZE_ARGUMENT" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_SIGNER_ARGUMENTS_MISMATCH"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "NUMBER_OF_SIGNER_ARGUMENTS_MISMATCH" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CALLED_SCRIPT_VISIBLE_FROM_NON_SCRIPT_VISIBLE"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "CALLED_SCRIPT_VISIBLE_FROM_NON_SCRIPT_VISIBLE" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXECUTE_ENTRY_FUNCTION_CALLED_ON_NON_ENTRY_FUNCTION"
                          |) in
                        M.alloc (|
                          M.read (|
                            Value.String "EXECUTE_ENTRY_FUNCTION_CALLED_ON_NON_ENTRY_FUNCTION"
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_SELF"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_FRIEND_DECL_WITH_SELF" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_MODULES_OUTSIDE_ACCOUNT_ADDRESS"
                          |) in
                        M.alloc (|
                          M.read (|
                            Value.String "INVALID_FRIEND_DECL_WITH_MODULES_OUTSIDE_ACCOUNT_ADDRESS"
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_MODULES_IN_DEPENDENCIES"
                          |) in
                        M.alloc (|
                          M.read (|
                            Value.String "INVALID_FRIEND_DECL_WITH_MODULES_IN_DEPENDENCIES"
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CYCLIC_MODULE_FRIENDSHIP"
                          |) in
                        M.alloc (| M.read (| Value.String "CYCLIC_MODULE_FRIENDSHIP" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_PHANTOM_TYPE_PARAM_POSITION"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "INVALID_PHANTOM_TYPE_PARAM_POSITION" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VEC_UPDATE_EXISTS_MUTABLE_BORROW_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "VEC_UPDATE_EXISTS_MUTABLE_BORROW_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VEC_BORROW_ELEMENT_EXISTS_MUTABLE_BORROW_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "VEC_BORROW_ELEMENT_EXISTS_MUTABLE_BORROW_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::LOOP_MAX_DEPTH_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "LOOP_MAX_DEPTH_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_TYPE_PARAMETERS"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_TYPE_PARAMETERS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_PARAMETERS"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_PARAMETERS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_BASIC_BLOCKS"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_BASIC_BLOCKS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VALUE_STACK_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "VALUE_STACK_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_TYPE_NODES"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_TYPE_NODES" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VALUE_STACK_PUSH_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "VALUE_STACK_PUSH_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_DEPENDENCY_DEPTH_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "MAX_DEPENDENCY_DEPTH_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_FUNCTION_DEFINITIONS_REACHED"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "MAX_FUNCTION_DEFINITIONS_REACHED" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_STRUCT_DEFINITIONS_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "MAX_STRUCT_DEFINITIONS_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MAX_FIELD_DEFINITIONS_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "MAX_FIELD_DEFINITIONS_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_BACK_EDGES"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_BACK_EDGES" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_1"
                          |) in
                        M.alloc (| M.read (| Value.String "RESERVED_VERIFICATION_ERROR_1" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_2"
                          |) in
                        M.alloc (| M.read (| Value.String "RESERVED_VERIFICATION_ERROR_2" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_3"
                          |) in
                        M.alloc (| M.read (| Value.String "RESERVED_VERIFICATION_ERROR_3" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_4"
                          |) in
                        M.alloc (| M.read (| Value.String "RESERVED_VERIFICATION_ERROR_4" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_5"
                          |) in
                        M.alloc (| M.read (| Value.String "RESERVED_VERIFICATION_ERROR_5" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TOO_MANY_VECTOR_ELEMENTS"
                          |) in
                        M.alloc (| M.read (| Value.String "TOO_MANY_VECTOR_ELEMENTS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::IDENTIFIER_TOO_LONG"
                          |) in
                        M.alloc (| M.read (| Value.String "IDENTIFIER_TOO_LONG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::PROGRAM_TOO_COMPLEX"
                          |) in
                        M.alloc (| M.read (| Value.String "PROGRAM_TOO_COMPLEX" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "UNKNOWN_INVARIANT_VIOLATION_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EMPTY_VALUE_STACK"
                          |) in
                        M.alloc (| M.read (| Value.String "EMPTY_VALUE_STACK" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::PC_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "PC_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VERIFICATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "VERIFICATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::STORAGE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "STORAGE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INTERNAL_TYPE_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "INTERNAL_TYPE_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EVENT_KEY_MISMATCH"
                          |) in
                        M.alloc (| M.read (| Value.String "EVENT_KEY_MISMATCH" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNREACHABLE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNREACHABLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VM_STARTUP_FAILURE"
                          |) in
                        M.alloc (| M.read (| Value.String "VM_STARTUP_FAILURE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_ERROR_FROM_KNOWN_MOVE_FUNCTION"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "UNEXPECTED_ERROR_FROM_KNOWN_MOVE_FUNCTION" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VERIFIER_INVARIANT_VIOLATION"
                          |) in
                        M.alloc (| M.read (| Value.String "VERIFIER_INVARIANT_VIOLATION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_VERIFIER_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "UNEXPECTED_VERIFIER_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_DESERIALIZATION_ERROR"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "UNEXPECTED_DESERIALIZATION_ERROR" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FAILED_TO_SERIALIZE_WRITE_SET_CHANGES"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "FAILED_TO_SERIALIZE_WRITE_SET_CHANGES" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::FAILED_TO_DESERIALIZE_RESOURCE"
                          |) in
                        M.alloc (| M.read (| Value.String "FAILED_TO_DESERIALIZE_RESOURCE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TYPE_RESOLUTION_FAILURE"
                          |) in
                        M.alloc (| M.read (| Value.String "TYPE_RESOLUTION_FAILURE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DUPLICATE_NATIVE_FUNCTION"
                          |) in
                        M.alloc (| M.read (| Value.String "DUPLICATE_NATIVE_FUNCTION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::ARITHMETIC_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "ARITHMETIC_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_BINARY_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_BINARY_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MALFORMED"
                          |) in
                        M.alloc (| M.read (| Value.String "MALFORMED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_MAGIC"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_MAGIC" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VERSION"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_VERSION" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_TABLE_TYPE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_TABLE_TYPE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SIGNATURE_TYPE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_SIGNATURE_TYPE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SERIALIZED_TYPE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_SERIALIZED_TYPE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_OPCODE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_OPCODE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_HEADER_TABLE"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_HEADER_TABLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_SIGNATURE_TYPE"
                          |) in
                        M.alloc (| M.read (| Value.String "UNEXPECTED_SIGNATURE_TYPE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DUPLICATE_TABLE"
                          |) in
                        M.alloc (| M.read (| Value.String "DUPLICATE_TABLE" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_ABILITY"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_ABILITY" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_NATIVE_STRUCT_FLAG"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_NATIVE_STRUCT_FLAG" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_U16"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_U16" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_U32"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_U32" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_U64"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_U64" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_U128"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_U128" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::BAD_U256"
                          |) in
                        M.alloc (| M.read (| Value.String "BAD_U256" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VALUE_SERIALIZATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "VALUE_SERIALIZATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VALUE_DESERIALIZATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "VALUE_DESERIALIZATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CODE_DESERIALIZATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "CODE_DESERIALIZATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::INVALID_FLAG_BITS"
                          |) in
                        M.alloc (| M.read (| Value.String "INVALID_FLAG_BITS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::TRAILING_BYTES"
                          |) in
                        M.alloc (| M.read (| Value.String "TRAILING_BYTES" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_RUNTIME_STATUS"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_RUNTIME_STATUS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXECUTED"
                          |) in
                        M.alloc (| M.read (| Value.String "EXECUTED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::OUT_OF_GAS"
                          |) in
                        M.alloc (| M.read (| Value.String "OUT_OF_GAS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESOURCE_DOES_NOT_EXIST"
                          |) in
                        M.alloc (| M.read (| Value.String "RESOURCE_DOES_NOT_EXIST" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::RESOURCE_ALREADY_EXISTS"
                          |) in
                        M.alloc (| M.read (| Value.String "RESOURCE_ALREADY_EXISTS" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MISSING_DATA"
                          |) in
                        M.alloc (| M.read (| Value.String "MISSING_DATA" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::DATA_FORMAT_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "DATA_FORMAT_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::ABORTED"
                          |) in
                        M.alloc (| M.read (| Value.String "ABORTED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::ARITHMETIC_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "ARITHMETIC_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VECTOR_OPERATION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "VECTOR_OPERATION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::EXECUTION_STACK_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "EXECUTION_STACK_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::CALL_STACK_OVERFLOW"
                          |) in
                        M.alloc (| M.read (| Value.String "CALL_STACK_OVERFLOW" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VM_MAX_TYPE_DEPTH_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "VM_MAX_TYPE_DEPTH_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VM_MAX_VALUE_DEPTH_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "VM_MAX_VALUE_DEPTH_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VM_EXTENSION_ERROR"
                          |) in
                        M.alloc (| M.read (| Value.String "VM_EXTENSION_ERROR" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::STORAGE_WRITE_LIMIT_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "STORAGE_WRITE_LIMIT_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::MEMORY_LIMIT_EXCEEDED"
                          |) in
                        M.alloc (| M.read (| Value.String "MEMORY_LIMIT_EXCEEDED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::VM_MAX_TYPE_NODES_REACHED"
                          |) in
                        M.alloc (| M.read (| Value.String "VM_MAX_TYPE_NODES_REACHED" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::vm_status::StatusCode::UNKNOWN_STATUS"
                          |) in
                        M.alloc (| M.read (| Value.String "UNKNOWN_STATUS" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_cmp_Eq_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_hash_Hash_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "u64", [], "hash", [ __H ] |),
                [ __self_discr; M.read (| state |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_cmp_PartialOrd_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialOrd",
                  Ty.path "u64",
                  [ Ty.path "u64" ],
                  "partial_cmp",
                  []
                |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_cmp_Ord_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::cmp::Ord", Ty.path "u64", [], "cmp", [] |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_convert_TryFrom_u64_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (*             type Error = &'static str; *)
    Definition _Error : Ty.t := Ty.apply (Ty.path "&") [] [ Ty.path "str" ].
    
    (*
                fn try_from(value: $repr_ty) -> Result<Self, Self::Error> {
                    match value {
                        $(
                            $value => Ok($enum_name::$variant),
                        )*
                        _ => Err("invalid StatusCode"),
                    }
                }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.read (|
            M.match_operator (|
              value,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 0
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VALIDATION_STATUS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_SIGNATURE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_AUTH_KEY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_OLD"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_NEW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 5
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INSUFFICIENT_BALANCE_FOR_TRANSACTION_FEE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 6
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TRANSACTION_EXPIRED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 7
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SENDING_ACCOUNT_DOES_NOT_EXIST"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 8
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::REJECTED_WRITE_SET"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 9
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_WRITE_SET"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 10
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EXCEEDED_MAX_TRANSACTION_SIZE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 11
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SCRIPT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 12
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_MODULE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 13
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_GAS_UNITS_EXCEEDS_MAX_GAS_UNITS_BOUND"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 14
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_GAS_UNITS_BELOW_MIN_TRANSACTION_GAS_UNITS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 15
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::GAS_UNIT_PRICE_BELOW_MIN_BOUND"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 16
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::GAS_UNIT_PRICE_ABOVE_MAX_BOUND"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 17
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_GAS_SPECIFIER"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 18
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SENDING_ACCOUNT_FROZEN"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 19
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNABLE_TO_DESERIALIZE_ACCOUNT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 20
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CURRENCY_INFO_DOES_NOT_EXIST"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 21
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_MODULE_PUBLISHER"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 22
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NO_ACCOUNT_ROLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 23
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BAD_CHAIN_ID"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 24
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NUMBER_TOO_BIG"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 25
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BAD_TRANSACTION_FEE_CURRENCY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 26
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FEATURE_UNDER_GATING"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 27
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 28
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SIGNERS_CONTAIN_DUPLICATES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 29
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::SEQUENCE_NONCE_INVALID"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 30
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CHAIN_ACCOUNT_INFO_DOES_NOT_EXIST"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1000
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VERIFICATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1001
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INDEX_OUT_OF_BOUNDS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1003
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_SIGNATURE_TOKEN"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1005
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RECURSIVE_STRUCT_DEFINITION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1006
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FIELD_MISSING_TYPE_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1007
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_FALL_THROUGH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1009
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NEGATIVE_STACK_SIZE_WITHIN_BLOCK"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1011
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_MAIN_FUNCTION_SIGNATURE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1012
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DUPLICATE_ELEMENT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1013
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_MODULE_HANDLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1014
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNIMPLEMENTED_HANDLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1017
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::LOOKUP_FAILED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1020
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TYPE_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1021
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MISSING_DEPENDENCY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1023
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::POP_WITHOUT_DROP_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1025
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BR_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1026
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::ABORT_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1027
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::STLOC_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1028
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::STLOC_UNSAFE_TO_DESTROY_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1029
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNSAFE_RET_LOCAL_OR_RESOURCE_STILL_BORROWED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1030
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RET_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1031
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RET_BORROWED_MUTABLE_REFERENCE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1032
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FREEZEREF_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1033
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FREEZEREF_EXISTS_MUTABLE_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1034
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1035
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_BAD_FIELD_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1036
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWFIELD_EXISTS_MUTABLE_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1037
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::COPYLOC_UNAVAILABLE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1038
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::COPYLOC_WITHOUT_COPY_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1039
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::COPYLOC_EXISTS_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1040
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVELOC_UNAVAILABLE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1041
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVELOC_EXISTS_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1042
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWLOC_REFERENCE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1043
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWLOC_UNAVAILABLE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1044
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWLOC_EXISTS_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1045
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CALL_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1046
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CALL_BORROWED_MUTABLE_REFERENCE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1047
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::PACK_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1048
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNPACK_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1049
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::READREF_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1050
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::READREF_WITHOUT_COPY_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1051
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::READREF_EXISTS_MUTABLE_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1052
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::WRITEREF_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1053
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::WRITEREF_WITHOUT_DROP_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1054
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::WRITEREF_EXISTS_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1055
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::WRITEREF_NO_MUTABLE_REFERENCE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1056
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INTEGER_OP_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1057
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BOOLEAN_OP_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1058
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EQUALITY_OP_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1059
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EXISTS_WITHOUT_KEY_ABILITY_OR_BAD_ARGUMENT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1060
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWGLOBAL_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1061
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BORROWGLOBAL_WITHOUT_KEY_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1062
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVEFROM_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1063
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVEFROM_WITHOUT_KEY_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1064
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVETO_TYPE_MISMATCH_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1065
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MOVETO_WITHOUT_KEY_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1067
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MODULE_ADDRESS_DOES_NOT_MATCH_SENDER"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1068
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NO_MODULE_HANDLES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1069
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::POSITIVE_STACK_SIZE_AT_BLOCK_END"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1070
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MISSING_ACQUIRES_ANNOTATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1071
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EXTRANEOUS_ACQUIRES_ANNOTATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1072
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DUPLICATE_ACQUIRES_ANNOTATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1073
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_ACQUIRES_ANNOTATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1074
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::GLOBAL_REFERENCE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1075
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CONSTRAINT_NOT_SATISFIED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1076
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_TYPE_ARGUMENTS_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1077
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::LOOP_IN_INSTANTIATION_GRAPH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1080
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::ZERO_SIZED_STRUCT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1081
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::LINKER_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1082
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_CONSTANT_TYPE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1083
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MALFORMED_CONSTANT_DATA"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1084
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EMPTY_CODE_UNIT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1085
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_SPLIT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1086
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_BREAK"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1087
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_LOOP_CONTINUE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1088
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNSAFE_RET_UNUSED_VALUES_WITHOUT_DROP"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1089
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_LOCALS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1090
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::GENERIC_MEMBER_OPCODE_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1091
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FUNCTION_RESOLUTION_FAILURE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1094
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_OPERATION_IN_SCRIPT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1095
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DUPLICATE_MODULE_NAME"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1096
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1097
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CYCLIC_MODULE_DEPENDENCY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1098
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_ARGUMENTS_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1099
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_PARAM_TYPE_FOR_DESERIALIZATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1100
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FAILED_TO_DESERIALIZE_ARGUMENT"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1101
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::NUMBER_OF_SIGNER_ARGUMENTS_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1102
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CALLED_SCRIPT_VISIBLE_FROM_NON_SCRIPT_VISIBLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1103
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EXECUTE_ENTRY_FUNCTION_CALLED_ON_NON_ENTRY_FUNCTION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1104
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_SELF"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1105
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_MODULES_OUTSIDE_ACCOUNT_ADDRESS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1106
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_FRIEND_DECL_WITH_MODULES_IN_DEPENDENCIES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1107
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CYCLIC_MODULE_FRIENDSHIP"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1108
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_PHANTOM_TYPE_PARAM_POSITION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1109
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VEC_UPDATE_EXISTS_MUTABLE_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1110
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VEC_BORROW_ELEMENT_EXISTS_MUTABLE_BORROW_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1111
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::LOOP_MAX_DEPTH_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1112
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_TYPE_PARAMETERS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1113
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_PARAMETERS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1114
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_BASIC_BLOCKS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1115
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VALUE_STACK_OVERFLOW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1116
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_TYPE_NODES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1117
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VALUE_STACK_PUSH_OVERFLOW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1118
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_DEPENDENCY_DEPTH_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1119
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_FUNCTION_DEFINITIONS_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1120
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_STRUCT_DEFINITIONS_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1121
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MAX_FIELD_DEFINITIONS_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1122
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_BACK_EDGES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1123
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_1"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1124
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_2"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1125
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_3"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1126
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_4"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1127
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESERVED_VERIFICATION_ERROR_5"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1128
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TOO_MANY_VECTOR_ELEMENTS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1129
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::IDENTIFIER_TOO_LONG"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 1130
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::PROGRAM_TOO_COMPLEX"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2000
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2003
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EMPTY_VALUE_STACK"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2005
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::PC_OVERFLOW" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2006
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VERIFICATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2008
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::STORAGE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2009
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INTERNAL_TYPE_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2010
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EVENT_KEY_MISMATCH"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2011
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::UNREACHABLE" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2012
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VM_STARTUP_FAILURE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2015
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_ERROR_FROM_KNOWN_MOVE_FUNCTION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2016
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VERIFIER_INVARIANT_VIOLATION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2017
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_VERIFIER_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2018
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_DESERIALIZATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2019
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FAILED_TO_SERIALIZE_WRITE_SET_CHANGES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2020
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::FAILED_TO_DESERIALIZE_RESOURCE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2021
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TYPE_RESOLUTION_FAILURE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2022
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DUPLICATE_NATIVE_FUNCTION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 2023
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::ARITHMETIC_OVERFLOW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3000
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_BINARY_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3001
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::MALFORMED" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3002
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_MAGIC" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3003
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_VERSION"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3004
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_TABLE_TYPE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3005
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SIGNATURE_TYPE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3006
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_SERIALIZED_TYPE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3007
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_OPCODE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3008
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::BAD_HEADER_TABLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3009
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNEXPECTED_SIGNATURE_TYPE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3010
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DUPLICATE_TABLE"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3013
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_ABILITY"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3014
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_NATIVE_STRUCT_FLAG"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3017
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_U16" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3018
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_U32" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3019
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_U64" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3020
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_U128" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3021
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::BAD_U256" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3022
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VALUE_SERIALIZATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3023
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VALUE_DESERIALIZATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3024
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CODE_DESERIALIZATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3025
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::INVALID_FLAG_BITS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 3026
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::TRAILING_BYTES"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4000
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_RUNTIME_STATUS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4001
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::EXECUTED" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4002
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::OUT_OF_GAS" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4003
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESOURCE_DOES_NOT_EXIST"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4004
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::RESOURCE_ALREADY_EXISTS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4008
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MISSING_DATA"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4009
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::DATA_FORMAT_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4016
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "move_core_types::vm_status::StatusCode::ABORTED" [] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4017
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::ARITHMETIC_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4018
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VECTOR_OPERATION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4020
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::EXECUTION_STACK_OVERFLOW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4021
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::CALL_STACK_OVERFLOW"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4024
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VM_MAX_TYPE_DEPTH_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4025
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VM_MAX_VALUE_DEPTH_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4026
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VM_EXTENSION_ERROR"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4027
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::STORAGE_WRITE_LIMIT_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4028
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::MEMORY_LIMIT_EXCEEDED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 4029
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::VM_MAX_TYPE_NODES_REACHED"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.U64 18446744073709551615
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructTuple
                            "move_core_types::vm_status::StatusCode::UNKNOWN_STATUS"
                            []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ M.read (| Value.String "invalid StatusCode" |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u64" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_u64_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (*
        pub fn status_type(self) -> StatusType {
            let major_status_number: u64 = self.into();
            if major_status_number >= VALIDATION_STATUS_MIN_CODE
                && major_status_number <= VALIDATION_STATUS_MAX_CODE
            {
                return StatusType::Validation;
            }
    
            if major_status_number >= VERIFICATION_STATUS_MIN_CODE
                && major_status_number <= VERIFICATION_STATUS_MAX_CODE
            {
                return StatusType::Verification;
            }
    
            if major_status_number >= INVARIANT_VIOLATION_STATUS_MIN_CODE
                && major_status_number <= INVARIANT_VIOLATION_STATUS_MAX_CODE
            {
                return StatusType::InvariantViolation;
            }
    
            if major_status_number >= DESERIALIZATION_STATUS_MIN_CODE
                && major_status_number <= DESERIALIZATION_STATUS_MAX_CODE
            {
                return StatusType::Deserialization;
            }
    
            if major_status_number >= EXECUTION_STATUS_MIN_CODE
                && major_status_number <= EXECUTION_STATUS_MAX_CODE
            {
                return StatusType::Execution;
            }
    
            StatusType::Unknown
        }
    *)
    Definition status_type (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ major_status_number :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.path "move_core_types::vm_status::StatusCode",
                        [ Ty.path "u64" ],
                        "into",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  BinOp.ge (|
                                    M.read (| major_status_number |),
                                    M.read (|
                                      M.read (|
                                        M.get_constant (|
                                          "move_core_types::vm_status::VALIDATION_STATUS_MIN_CODE"
                                        |)
                                      |)
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| major_status_number |),
                                      M.read (|
                                        M.read (|
                                          M.get_constant (|
                                            "move_core_types::vm_status::VALIDATION_STATUS_MAX_CODE"
                                          |)
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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
                                    "move_core_types::vm_status::StatusType::Validation"
                                    []
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  BinOp.ge (|
                                    M.read (| major_status_number |),
                                    M.read (|
                                      M.read (|
                                        M.get_constant (|
                                          "move_core_types::vm_status::VERIFICATION_STATUS_MIN_CODE"
                                        |)
                                      |)
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| major_status_number |),
                                      M.read (|
                                        M.read (|
                                          M.get_constant (|
                                            "move_core_types::vm_status::VERIFICATION_STATUS_MAX_CODE"
                                          |)
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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
                                    "move_core_types::vm_status::StatusType::Verification"
                                    []
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  BinOp.ge (|
                                    M.read (| major_status_number |),
                                    M.read (|
                                      M.read (|
                                        M.get_constant (|
                                          "move_core_types::vm_status::INVARIANT_VIOLATION_STATUS_MIN_CODE"
                                        |)
                                      |)
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| major_status_number |),
                                      M.read (|
                                        M.read (|
                                          M.get_constant (|
                                            "move_core_types::vm_status::INVARIANT_VIOLATION_STATUS_MAX_CODE"
                                          |)
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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
                                    "move_core_types::vm_status::StatusType::InvariantViolation"
                                    []
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  BinOp.ge (|
                                    M.read (| major_status_number |),
                                    M.read (|
                                      M.read (|
                                        M.get_constant (|
                                          "move_core_types::vm_status::DESERIALIZATION_STATUS_MIN_CODE"
                                        |)
                                      |)
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| major_status_number |),
                                      M.read (|
                                        M.read (|
                                          M.get_constant (|
                                            "move_core_types::vm_status::DESERIALIZATION_STATUS_MAX_CODE"
                                          |)
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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
                                    "move_core_types::vm_status::StatusType::Deserialization"
                                    []
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  BinOp.ge (|
                                    M.read (| major_status_number |),
                                    M.read (|
                                      M.read (|
                                        M.get_constant (|
                                          "move_core_types::vm_status::EXECUTION_STATUS_MIN_CODE"
                                        |)
                                      |)
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| major_status_number |),
                                      M.read (|
                                        M.read (|
                                          M.get_constant (|
                                            "move_core_types::vm_status::EXECUTION_STATUS_MAX_CODE"
                                          |)
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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
                                    "move_core_types::vm_status::StatusType::Execution"
                                    []
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "move_core_types::vm_status::StatusType::Unknown" [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_status_type : M.IsAssociatedFunction Self "status_type" status_type.
  End Impl_move_core_types_vm_status_StatusCode.
  
  Module Impl_serde_ser_Serialize_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (*
        fn serialize<S>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error>
        where
            S: ser::Serializer,
        {
            serializer.serialize_u64(( *self).into())
        }
    *)
    Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as S ], [ self; serializer ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let serializer := M.alloc (| serializer |) in
          M.call_closure (|
            M.get_trait_method (| "serde::ser::Serializer", S, [], "serialize_u64", [] |),
            [
              M.read (| serializer |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::Into",
                  Ty.path "move_core_types::vm_status::StatusCode",
                  [ Ty.path "u64" ],
                  "into",
                  []
                |),
                [ M.read (| M.read (| self |) |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::ser::Serialize"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("serialize", InstanceField.Method serialize) ].
  End Impl_serde_ser_Serialize_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_serde_de_Deserialize_for_move_core_types_vm_status_StatusCode.
    Definition Self : Ty.t := Ty.path "move_core_types::vm_status::StatusCode".
    
    (*
        fn deserialize<D>(deserializer: D) -> std::result::Result<Self, D::Error>
        where
            D: de::Deserializer<'de>,
        {
            struct StatusCodeVisitor;
            impl<'de> de::Visitor<'de> for StatusCodeVisitor {
                type Value = StatusCode;
    
                fn expecting(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
                    formatter.write_str("StatusCode as u64")
                }
    
                fn visit_u64<E>(self, v: u64) -> std::result::Result<StatusCode, E>
                where
                    E: de::Error,
                {
                    Ok(StatusCode::try_from(v).unwrap_or(StatusCode::UNKNOWN_STATUS))
                }
            }
    
            deserializer.deserialize_u64(StatusCodeVisitor)
        }
    *)
    Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ D ], [ deserializer ] =>
        ltac:(M.monadic
          (let deserializer := M.alloc (| deserializer |) in
          M.call_closure (|
            M.get_trait_method (|
              "serde::de::Deserializer",
              D,
              [],
              "deserialize_u64",
              [ Ty.path "move_core_types::vm_status::deserialize::StatusCodeVisitor" ]
            |),
            [
              M.read (| deserializer |);
              Value.StructTuple "move_core_types::vm_status::deserialize::StatusCodeVisitor" []
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::Deserialize"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("deserialize", InstanceField.Method deserialize) ].
  End Impl_serde_de_Deserialize_for_move_core_types_vm_status_StatusCode.
  
  Module Impl_core_convert_From_move_core_types_vm_status_StatusCode_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    (*
        fn from(status: StatusCode) -> u64 {
            status as u64
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ status ] =>
        ltac:(M.monadic
          (let status := M.alloc (| status |) in
          M.rust_cast (M.read (| status |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::vm_status::StatusCode" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_move_core_types_vm_status_StatusCode_for_u64.
  
  Module sub_status.
    Definition value_NFE_VECTOR_ERROR_BASE : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 0 |))).
    
    Definition value_NFE_OUT_OF_GAS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1 |))).
    
    Definition value_NFE_BCS_SERIALIZATION_FAILURE : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 453 |))).
  End sub_status.
End vm_status.
