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

Module errors.
  Axiom VMResult :
    forall (T : Ty.t),
    (Ty.apply (Ty.path "move_binary_format::errors::VMResult") [] [ T ]) =
      (Ty.apply
        (Ty.path "core::result::Result")
        []
        [ T; Ty.path "move_binary_format::errors::VMError" ]).
  
  Axiom BinaryLoaderResult :
    forall (T : Ty.t),
    (Ty.apply (Ty.path "move_binary_format::errors::BinaryLoaderResult") [] [ T ]) =
      (Ty.apply
        (Ty.path "core::result::Result")
        []
        [ T; Ty.path "move_binary_format::errors::PartialVMError" ]).
  
  Axiom PartialVMResult :
    forall (T : Ty.t),
    (Ty.apply (Ty.path "move_binary_format::errors::PartialVMResult") [] [ T ]) =
      (Ty.apply
        (Ty.path "core::result::Result")
        []
        [ T; Ty.path "move_binary_format::errors::PartialVMError" ]).
  
  (*
  Enum Location
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Undefined";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Module";
          item := StructTuple [ Ty.path "move_core_types::language_storage::ModuleId" ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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_binary_format::errors::Location::Undefined"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_binary_format::errors::Location::Undefined" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::errors::Location::Module",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_binary_format::errors::Location::Module"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::language_storage::ModuleId",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_Location.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_binary_format::errors::Location::Undefined"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Undefined" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::errors::Location::Module",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Module" |); __self_0 ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_Location.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| 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_binary_format_errors_Location.
  
  Module Impl_core_cmp_Ord_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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_binary_format::errors::Location" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::errors::Location" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
                  [ __self_discr; __arg1_discr ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_binary_format::errors::Location::Module",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_binary_format::errors::Location::Module",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::Ord",
                                  Ty.path "move_core_types::language_storage::ModuleId",
                                  [],
                                  "cmp",
                                  []
                                |),
                                [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let cmp := M.copy (| γ |) in
                    cmp))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_Location.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_Location.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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_binary_format::errors::Location" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::errors::Location" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_binary_format::errors::Location::Module",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_binary_format::errors::Location::Module",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::language_storage::ModuleId" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_core_types::language_storage::ModuleId" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_Location.
  
  Module Impl_core_cmp_PartialOrd_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (* 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_binary_format::errors::Location" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::errors::Location" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_binary_format::errors::Location::Module",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "move_binary_format::errors::Location::Module",
                        0
                      |) in
                    let __arg1_0 := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          Ty.path "move_core_types::language_storage::ModuleId",
                          [ Ty.path "move_core_types::language_storage::ModuleId" ],
                          "partial_cmp",
                          []
                        |),
                        [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          Ty.path "isize",
                          [ Ty.path "isize" ],
                          "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_binary_format_errors_Location.
  
  (* StructRecord
    {
      name := "ExecutionState";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("stack_trace",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple
                  [
                    Ty.path "move_core_types::language_storage::ModuleId";
                    Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                    Ty.path "u16"
                  ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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
          Value.StructRecord
            "move_binary_format::errors::ExecutionState"
            [
              ("stack_trace",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_core_types::language_storage::ModuleId";
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::ExecutionState",
                      "stack_trace"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_binary_format_errors_ExecutionState.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "ExecutionState" |);
              M.read (| Value.String "stack_trace" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_binary_format::errors::ExecutionState",
                  "stack_trace"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_ExecutionState.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| 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_binary_format_errors_ExecutionState.
  
  Module Impl_core_cmp_Ord_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::Ord",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.tuple
                    [
                      Ty.path "move_core_types::language_storage::ModuleId";
                      Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                      Ty.path "u16"
                    ];
                  Ty.path "alloc::alloc::Global"
                ],
              [],
              "cmp",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_ExecutionState.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_ExecutionState.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.tuple
                    [
                      Ty.path "move_core_types::language_storage::ModuleId";
                      Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                      Ty.path "u16"
                    ];
                  Ty.path "alloc::alloc::Global"
                ],
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.tuple
                      [
                        Ty.path "move_core_types::language_storage::ModuleId";
                        Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                        Ty.path "u16"
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]
              ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_ExecutionState.
  
  Module Impl_core_cmp_PartialOrd_for_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.tuple
                    [
                      Ty.path "move_core_types::language_storage::ModuleId";
                      Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                      Ty.path "u16"
                    ];
                  Ty.path "alloc::alloc::Global"
                ],
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.tuple
                      [
                        Ty.path "move_core_types::language_storage::ModuleId";
                        Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                        Ty.path "u16"
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]
              ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "move_binary_format::errors::ExecutionState",
                "stack_trace"
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_ExecutionState.
  
  Module Impl_move_binary_format_errors_ExecutionState.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::ExecutionState".
    
    (*
        pub fn new(stack_trace: Vec<(ModuleId, FunctionDefinitionIndex, CodeOffset)>) -> Self {
            Self { stack_trace }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ stack_trace ] =>
        ltac:(M.monadic
          (let stack_trace := M.alloc (| stack_trace |) in
          Value.StructRecord
            "move_binary_format::errors::ExecutionState"
            [ ("stack_trace", M.read (| stack_trace |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn stack_trace(&self) -> &Vec<(ModuleId, FunctionDefinitionIndex, CodeOffset)> {
            &self.stack_trace
        }
    *)
    Definition stack_trace (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "move_binary_format::errors::ExecutionState",
            "stack_trace"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_stack_trace : M.IsAssociatedFunction Self "stack_trace" stack_trace.
  End Impl_move_binary_format_errors_ExecutionState.
  
  (* StructTuple
    {
      name := "VMError";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "alloc::boxed::Box")
            []
            [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ]
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (* 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
          Value.StructTuple
            "move_binary_format::errors::VMError"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::boxed::Box")
                    []
                    [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_binary_format::errors::VMError",
                    0
                  |)
                ]
              |)
            ]))
      | _, _, _ => 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_binary_format_errors_VMError.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (* 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
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| 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_binary_format_errors_VMError.
  
  Module Impl_core_cmp_Ord_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::Ord",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ],
              [],
              "cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_binary_format::errors::VMError",
                0
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_VMError.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_VMError.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ],
              [
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ]
              ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_binary_format::errors::VMError",
                0
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_VMError.
  
  Module Impl_core_cmp_PartialOrd_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (* 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.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ],
              [
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ]
              ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_binary_format::errors::VMError",
                0
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_VMError.
  
  (* StructRecord
    {
      name := "VMError_";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("major_status", Ty.path "move_core_types::vm_status::StatusCode");
          ("sub_status", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ]);
          ("message",
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "alloc::string::String" ]);
          ("exec_state",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "move_binary_format::errors::ExecutionState" ]);
          ("location", Ty.path "move_binary_format::errors::Location");
          ("indices",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                Ty.path "alloc::alloc::Global"
              ]);
          ("offsets",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple
                  [
                    Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                    Ty.path "u16"
                  ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (* 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
          Value.StructRecord
            "move_binary_format::errors::VMError_"
            [
              ("major_status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "move_core_types::vm_status::StatusCode",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "major_status"
                    |)
                  ]
                |));
              ("sub_status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "sub_status"
                    |)
                  ]
                |));
              ("message",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "alloc::string::String" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "message"
                    |)
                  ]
                |));
              ("exec_state",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "move_binary_format::errors::ExecutionState" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "exec_state"
                    |)
                  ]
                |));
              ("location",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "move_binary_format::errors::Location",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "location"
                    |)
                  ]
                |));
              ("indices",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "indices"
                    |)
                  ]
                |));
              ("offsets",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "offsets"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_binary_format_errors_VMError_.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (* 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
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              Value.DeclaredButUndefined,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      Value.DeclaredButUndefined,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              Value.DeclaredButUndefined,
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      Value.DeclaredButUndefined,
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              Value.DeclaredButUndefined,
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| 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_binary_format_errors_VMError_.
  
  Module Impl_core_cmp_Ord_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (* 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 (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::Ord",
                    Ty.path "move_core_types::vm_status::StatusCode",
                    [],
                    "cmp",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "major_status"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_binary_format::errors::VMError_",
                      "major_status"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::Ord",
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                            [],
                            "cmp",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::Ord",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.path "alloc::string::String" ],
                                    [],
                                    "cmp",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::errors::VMError_",
                                      "message"
                                    |);
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| other |),
                                      "move_binary_format::errors::VMError_",
                                      "message"
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::Ord",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "move_binary_format::errors::ExecutionState"
                                              ],
                                            [],
                                            "cmp",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_binary_format::errors::VMError_",
                                              "exec_state"
                                            |);
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| other |),
                                              "move_binary_format::errors::VMError_",
                                              "exec_state"
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::cmp::Ordering::Equal"
                                              |) in
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::Ord",
                                                    Ty.path "move_binary_format::errors::Location",
                                                    [],
                                                    "cmp",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "move_binary_format::errors::VMError_",
                                                      "location"
                                                    |);
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| other |),
                                                      "move_binary_format::errors::VMError_",
                                                      "location"
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::cmp::Ordering::Equal"
                                                      |) in
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::cmp::Ord",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::IndexKind";
                                                                    Ty.path "u16"
                                                                  ];
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [],
                                                            "cmp",
                                                            []
                                                          |),
                                                          [
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_binary_format::errors::VMError_",
                                                              "indices"
                                                            |);
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| other |),
                                                              "move_binary_format::errors::VMError_",
                                                              "indices"
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let _ :=
                                                              M.is_struct_tuple (|
                                                                γ,
                                                                "core::cmp::Ordering::Equal"
                                                              |) in
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::cmp::Ord",
                                                                  Ty.apply
                                                                    (Ty.path "alloc::vec::Vec")
                                                                    []
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.path
                                                                            "move_binary_format::file_format::FunctionDefinitionIndex";
                                                                          Ty.path "u16"
                                                                        ];
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ],
                                                                  [],
                                                                  "cmp",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "move_binary_format::errors::VMError_",
                                                                    "offsets"
                                                                  |);
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| other |),
                                                                    "move_binary_format::errors::VMError_",
                                                                    "offsets"
                                                                  |)
                                                                ]
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let cmp := M.copy (| γ |) in
                                                            cmp))
                                                      ]
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let cmp := M.copy (| γ |) in
                                                    cmp))
                                              ]
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let cmp := M.copy (| γ |) in
                                            cmp))
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let cmp := M.copy (| γ |) in
                                    cmp))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let cmp := M.copy (| γ |) in
                            cmp))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let cmp := M.copy (| γ |) in
                    cmp))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_VMError_.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_errors_VMError_.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (* 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
          LogicalOp.and (|
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    LogicalOp.and (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.path "move_core_types::vm_status::StatusCode",
                          [ Ty.path "move_core_types::vm_status::StatusCode" ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_binary_format::errors::VMError_",
                            "major_status"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "move_binary_format::errors::VMError_",
                            "major_status"
                          |)
                        ]
                      |),
                      ltac:(M.monadic
                        (M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                            [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ] ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |)
                          ]
                        |)))
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "alloc::string::String" ],
                          [
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "alloc::string::String" ]
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_binary_format::errors::VMError_",
                            "message"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "move_binary_format::errors::VMError_",
                            "message"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "move_binary_format::errors::ExecutionState" ],
                        [
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "move_binary_format::errors::ExecutionState" ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_binary_format::errors::VMError_",
                          "exec_state"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "move_binary_format::errors::VMError_",
                          "exec_state"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "move_binary_format::errors::Location",
                      [ Ty.path "move_binary_format::errors::Location" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::errors::VMError_",
                        "location"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "move_binary_format::errors::VMError_",
                        "location"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                          Ty.path "alloc::alloc::Global"
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "indices"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_binary_format::errors::VMError_",
                      "indices"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.tuple
                        [
                          Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                          Ty.path "u16"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_binary_format::errors::VMError_",
                    "offsets"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "move_binary_format::errors::VMError_",
                    "offsets"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_binary_format_errors_VMError_.
  
  Module Impl_core_cmp_PartialOrd_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (* 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 (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Ty.path "move_core_types::vm_status::StatusCode",
                    [ Ty.path "move_core_types::vm_status::StatusCode" ],
                    "partial_cmp",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError_",
                      "major_status"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_binary_format::errors::VMError_",
                      "major_status"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Equal" |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialOrd",
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                            [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ] ],
                            "partial_cmp",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "move_binary_format::errors::VMError_",
                              "sub_status"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let _ := M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Equal" |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.path "alloc::string::String" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "alloc::string::String" ]
                                    ],
                                    "partial_cmp",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::errors::VMError_",
                                      "message"
                                    |);
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| other |),
                                      "move_binary_format::errors::VMError_",
                                      "message"
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let _ :=
                                      M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Equal" |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialOrd",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "move_binary_format::errors::ExecutionState"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::errors::ExecutionState"
                                                ]
                                            ],
                                            "partial_cmp",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_binary_format::errors::VMError_",
                                              "exec_state"
                                            |);
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| other |),
                                              "move_binary_format::errors::VMError_",
                                              "exec_state"
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let _ :=
                                              M.is_struct_tuple (|
                                                γ0_0,
                                                "core::cmp::Ordering::Equal"
                                              |) in
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::PartialOrd",
                                                    Ty.path "move_binary_format::errors::Location",
                                                    [ Ty.path "move_binary_format::errors::Location"
                                                    ],
                                                    "partial_cmp",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "move_binary_format::errors::VMError_",
                                                      "location"
                                                    |);
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| other |),
                                                      "move_binary_format::errors::VMError_",
                                                      "location"
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let _ :=
                                                      M.is_struct_tuple (|
                                                        γ0_0,
                                                        "core::cmp::Ordering::Equal"
                                                      |) in
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::cmp::PartialOrd",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::IndexKind";
                                                                    Ty.path "u16"
                                                                  ];
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                []
                                                                [
                                                                  Ty.tuple
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::IndexKind";
                                                                      Ty.path "u16"
                                                                    ];
                                                                  Ty.path "alloc::alloc::Global"
                                                                ]
                                                            ],
                                                            "partial_cmp",
                                                            []
                                                          |),
                                                          [
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_binary_format::errors::VMError_",
                                                              "indices"
                                                            |);
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| other |),
                                                              "move_binary_format::errors::VMError_",
                                                              "indices"
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let _ :=
                                                              M.is_struct_tuple (|
                                                                γ0_0,
                                                                "core::cmp::Ordering::Equal"
                                                              |) in
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::cmp::PartialOrd",
                                                                  Ty.apply
                                                                    (Ty.path "alloc::vec::Vec")
                                                                    []
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.path
                                                                            "move_binary_format::file_format::FunctionDefinitionIndex";
                                                                          Ty.path "u16"
                                                                        ];
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "alloc::vec::Vec")
                                                                      []
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::file_format::FunctionDefinitionIndex";
                                                                            Ty.path "u16"
                                                                          ];
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ]
                                                                  ],
                                                                  "partial_cmp",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "move_binary_format::errors::VMError_",
                                                                    "offsets"
                                                                  |);
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| other |),
                                                                    "move_binary_format::errors::VMError_",
                                                                    "offsets"
                                                                  |)
                                                                ]
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let cmp := M.copy (| γ |) in
                                                            cmp))
                                                      ]
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let cmp := M.copy (| γ |) in
                                                    cmp))
                                              ]
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let cmp := M.copy (| γ |) in
                                            cmp))
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let cmp := M.copy (| γ |) in
                                    cmp))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let cmp := M.copy (| γ |) in
                            cmp))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let cmp := M.copy (| γ |) in
                    cmp))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_VMError_.
  
  Module Impl_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (*
        pub fn major_status(&self) -> StatusCode {
            self.0.major_status
        }
    *)
    Definition major_status (ε : 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.SubPointer.get_struct_record_field (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_binary_format::errors::VMError",
                  0
                |)
              |),
              "move_binary_format::errors::VMError_",
              "major_status"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_major_status : M.IsAssociatedFunction Self "major_status" major_status.
    
    (*
        pub fn sub_status(&self) -> Option<u64> {
            self.0.sub_status
        }
    *)
    Definition sub_status (ε : 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.SubPointer.get_struct_record_field (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_binary_format::errors::VMError",
                  0
                |)
              |),
              "move_binary_format::errors::VMError_",
              "sub_status"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_sub_status : M.IsAssociatedFunction Self "sub_status" sub_status.
    
    (*
        pub fn message(&self) -> Option<&String> {
            self.0.message.as_ref()
        }
    *)
    Definition message (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "alloc::string::String" ],
              "as_ref",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_binary_format::errors::VMError",
                    0
                  |)
                |),
                "move_binary_format::errors::VMError_",
                "message"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_message : M.IsAssociatedFunction Self "message" message.
    
    (*
        pub fn exec_state(&self) -> Option<&ExecutionState> {
            self.0.exec_state.as_ref()
        }
    *)
    Definition exec_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [ Ty.path "move_binary_format::errors::ExecutionState" ],
              "as_ref",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_binary_format::errors::VMError",
                    0
                  |)
                |),
                "move_binary_format::errors::VMError_",
                "exec_state"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_exec_state : M.IsAssociatedFunction Self "exec_state" exec_state.
    
    (*
        pub fn remove_exec_state(&mut self) {
            self.0.exec_state = None;
        }
    *)
    Definition remove_exec_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError",
                      0
                    |)
                  |),
                  "move_binary_format::errors::VMError_",
                  "exec_state"
                |),
                Value.StructTuple "core::option::Option::None" []
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_remove_exec_state :
      M.IsAssociatedFunction Self "remove_exec_state" remove_exec_state.
    
    (*
        pub fn location(&self) -> &Location {
            &self.0.location
        }
    *)
    Definition location (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_record_field (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |)
            |),
            "move_binary_format::errors::VMError_",
            "location"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_location : M.IsAssociatedFunction Self "location" location.
    
    (*
        pub fn indices(&self) -> &Vec<(IndexKind, TableIndex)> {
            &self.0.indices
        }
    *)
    Definition indices (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_record_field (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |)
            |),
            "move_binary_format::errors::VMError_",
            "indices"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_indices : M.IsAssociatedFunction Self "indices" indices.
    
    (*
        pub fn offsets(&self) -> &Vec<(FunctionDefinitionIndex, CodeOffset)> {
            &self.0.offsets
        }
    *)
    Definition offsets (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_record_field (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |)
            |),
            "move_binary_format::errors::VMError_",
            "offsets"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_offsets : M.IsAssociatedFunction Self "offsets" offsets.
    
    (*
        pub fn status_type(&self) -> StatusType {
            self.0.major_status.status_type()
        }
    *)
    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.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::vm_status::StatusCode",
              "status_type",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "move_binary_format::errors::VMError",
                      0
                    |)
                  |),
                  "move_binary_format::errors::VMError_",
                  "major_status"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_status_type : M.IsAssociatedFunction Self "status_type" status_type.
    
    (*
        pub fn all_data(
            self,
        ) -> (
            StatusCode,
            Option<u64>,
            Option<String>,
            Option<ExecutionState>,
            Location,
            Vec<(IndexKind, TableIndex)>,
            Vec<(FunctionDefinitionIndex, CodeOffset)>,
        ) {
            let VMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                location,
                indices,
                offsets,
            } = *self.0;
            (
                major_status,
                sub_status,
                message,
                exec_state,
                location,
                indices,
                offsets,
            )
        }
    *)
    Definition all_data (ε : 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 (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  self,
                  "move_binary_format::errors::VMError",
                  0
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "major_status"
                      |) in
                    let γ0_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "sub_status"
                      |) in
                    let γ0_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "message"
                      |) in
                    let γ0_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "exec_state"
                      |) in
                    let γ0_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "location"
                      |) in
                    let γ0_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "indices"
                      |) in
                    let γ0_6 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "offsets"
                      |) in
                    let major_status := M.copy (| γ0_0 |) in
                    let sub_status := M.copy (| γ0_1 |) in
                    let message := M.copy (| γ0_2 |) in
                    let exec_state := M.copy (| γ0_3 |) in
                    let location := M.copy (| γ0_4 |) in
                    let indices := M.copy (| γ0_5 |) in
                    let offsets := M.copy (| γ0_6 |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          M.read (| major_status |);
                          M.read (| sub_status |);
                          M.read (| message |);
                          M.read (| exec_state |);
                          M.read (| location |);
                          M.read (| indices |);
                          M.read (| offsets |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_all_data : M.IsAssociatedFunction Self "all_data" all_data.
    
    (*
        pub fn to_partial(self) -> PartialVMError {
            let VMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
                ..
            } = *self.0;
            PartialVMError(Box::new(PartialVMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
            }))
        }
    *)
    Definition to_partial (ε : 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 (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  self,
                  "move_binary_format::errors::VMError",
                  0
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "major_status"
                      |) in
                    let γ0_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "sub_status"
                      |) in
                    let γ0_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "message"
                      |) in
                    let γ0_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "exec_state"
                      |) in
                    let γ0_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "indices"
                      |) in
                    let γ0_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "offsets"
                      |) in
                    let major_status := M.copy (| γ0_0 |) in
                    let sub_status := M.copy (| γ0_1 |) in
                    let message := M.copy (| γ0_2 |) in
                    let exec_state := M.copy (| γ0_3 |) in
                    let indices := M.copy (| γ0_4 |) in
                    let offsets := M.copy (| γ0_5 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_binary_format::errors::PartialVMError"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.path "move_binary_format::errors::PartialVMError_";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            [
                              Value.StructRecord
                                "move_binary_format::errors::PartialVMError_"
                                [
                                  ("major_status", M.read (| major_status |));
                                  ("sub_status", M.read (| sub_status |));
                                  ("message", M.read (| message |));
                                  ("exec_state", M.read (| exec_state |));
                                  ("indices", M.read (| indices |));
                                  ("offsets", M.read (| offsets |))
                                ]
                            ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_partial : M.IsAssociatedFunction Self "to_partial" to_partial.
  End Impl_move_binary_format_errors_VMError.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Debug::fmt(&self.0, f)
        }
    *)
    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_trait_method (|
              "core::fmt::Debug",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "move_binary_format::errors::VMError_"; Ty.path "alloc::alloc::Global" ],
              [],
              "fmt",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::VMError",
                0
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_VMError.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_VMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError_".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let Self {
                major_status,
                sub_status,
                message,
                exec_state,
                location,
                indices,
                offsets,
            } = self;
            f.debug_struct("VMError")
                .field("major_status", major_status)
                .field("sub_status", sub_status)
                .field("message", message)
                .field("exec_state", exec_state)
                .field("location", location)
                .field("indices", indices)
                .field("offsets", offsets)
                .finish()
        }
    *)
    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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "major_status"
                      |) in
                    let γ1_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "sub_status"
                      |) in
                    let γ1_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "message"
                      |) in
                    let γ1_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "exec_state"
                      |) in
                    let γ1_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "location"
                      |) in
                    let γ1_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "indices"
                      |) in
                    let γ1_6 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::VMError_",
                        "offsets"
                      |) in
                    let major_status := M.alloc (| γ1_0 |) in
                    let sub_status := M.alloc (| γ1_1 |) in
                    let message := M.alloc (| γ1_2 |) in
                    let exec_state := M.alloc (| γ1_3 |) in
                    let location := M.alloc (| γ1_4 |) in
                    let indices := M.alloc (| γ1_5 |) in
                    let offsets := M.alloc (| γ1_6 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugStruct",
                          "finish",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::builders::DebugStruct",
                              "field",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::builders::DebugStruct",
                                  "field",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::builders::DebugStruct",
                                      "field",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::builders::DebugStruct",
                                          "field",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::fmt::builders::DebugStruct",
                                              "field",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::builders::DebugStruct",
                                                  "field",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::builders::DebugStruct",
                                                      "field",
                                                      []
                                                    |),
                                                    [
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Formatter",
                                                            "debug_struct",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| f |);
                                                            M.read (| Value.String "VMError" |)
                                                          ]
                                                        |)
                                                      |);
                                                      M.read (| Value.String "major_status" |);
                                                      M.read (| major_status |)
                                                    ]
                                                  |);
                                                  M.read (| Value.String "sub_status" |);
                                                  M.read (| sub_status |)
                                                ]
                                              |);
                                              M.read (| Value.String "message" |);
                                              M.read (| message |)
                                            ]
                                          |);
                                          M.read (| Value.String "exec_state" |);
                                          M.read (| exec_state |)
                                        ]
                                      |);
                                      M.read (| Value.String "location" |);
                                      M.read (| location |)
                                    ]
                                  |);
                                  M.read (| Value.String "indices" |);
                                  M.read (| indices |)
                                ]
                              |);
                              M.read (| Value.String "offsets" |);
                              M.read (| offsets |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_VMError_.
  
  Module Impl_core_error_Error_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_move_binary_format_errors_VMError.
  
  (* StructTuple
    {
      name := "PartialVMError";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "alloc::boxed::Box")
            []
            [ Ty.path "move_binary_format::errors::PartialVMError_"; Ty.path "alloc::alloc::Global"
            ]
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_PartialVMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError".
    
    (* 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
          Value.StructTuple
            "move_binary_format::errors::PartialVMError"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::boxed::Box")
                    []
                    [
                      Ty.path "move_binary_format::errors::PartialVMError_";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_binary_format::errors::PartialVMError",
                    0
                  |)
                ]
              |)
            ]))
      | _, _, _ => 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_binary_format_errors_PartialVMError.
  
  (* StructRecord
    {
      name := "PartialVMError_";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("major_status", Ty.path "move_core_types::vm_status::StatusCode");
          ("sub_status", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ]);
          ("message",
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "alloc::string::String" ]);
          ("exec_state",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "move_binary_format::errors::ExecutionState" ]);
          ("indices",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                Ty.path "alloc::alloc::Global"
              ]);
          ("offsets",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple
                  [
                    Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                    Ty.path "u16"
                  ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_errors_PartialVMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError_".
    
    (* 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
          Value.StructRecord
            "move_binary_format::errors::PartialVMError_"
            [
              ("major_status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "move_core_types::vm_status::StatusCode",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "major_status"
                    |)
                  ]
                |));
              ("sub_status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "sub_status"
                    |)
                  ]
                |));
              ("message",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "alloc::string::String" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "message"
                    |)
                  ]
                |));
              ("exec_state",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "move_binary_format::errors::ExecutionState" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "exec_state"
                    |)
                  ]
                |));
              ("indices",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "indices"
                    |)
                  ]
                |));
              ("offsets",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::errors::PartialVMError_",
                      "offsets"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_binary_format_errors_PartialVMError_.
  
  Module Impl_move_binary_format_errors_PartialVMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError".
    
    (*
        pub fn all_data(
            self,
        ) -> (
            StatusCode,
            Option<u64>,
            Option<String>,
            Option<ExecutionState>,
            Vec<(IndexKind, TableIndex)>,
            Vec<(FunctionDefinitionIndex, CodeOffset)>,
        ) {
            let PartialVMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
            } = *self.0;
            (
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
            )
        }
    *)
    Definition all_data (ε : 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 (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  self,
                  "move_binary_format::errors::PartialVMError",
                  0
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "major_status"
                      |) in
                    let γ0_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "sub_status"
                      |) in
                    let γ0_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "message"
                      |) in
                    let γ0_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "exec_state"
                      |) in
                    let γ0_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "indices"
                      |) in
                    let γ0_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "offsets"
                      |) in
                    let major_status := M.copy (| γ0_0 |) in
                    let sub_status := M.copy (| γ0_1 |) in
                    let message := M.copy (| γ0_2 |) in
                    let exec_state := M.copy (| γ0_3 |) in
                    let indices := M.copy (| γ0_4 |) in
                    let offsets := M.copy (| γ0_5 |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          M.read (| major_status |);
                          M.read (| sub_status |);
                          M.read (| message |);
                          M.read (| exec_state |);
                          M.read (| indices |);
                          M.read (| offsets |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_all_data : M.IsAssociatedFunction Self "all_data" all_data.
    
    (*
        pub fn finish(self, location: Location) -> VMError {
            let PartialVMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
            } = *self.0;
            VMError(Box::new(VMError_ {
                major_status,
                sub_status,
                message,
                exec_state,
                location,
                indices,
                offsets,
            }))
        }
    *)
    Definition finish (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; location ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let location := M.alloc (| location |) in
          M.read (|
            M.match_operator (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  self,
                  "move_binary_format::errors::PartialVMError",
                  0
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "major_status"
                      |) in
                    let γ0_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "sub_status"
                      |) in
                    let γ0_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "message"
                      |) in
                    let γ0_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "exec_state"
                      |) in
                    let γ0_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "indices"
                      |) in
                    let γ0_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "offsets"
                      |) in
                    let major_status := M.copy (| γ0_0 |) in
                    let sub_status := M.copy (| γ0_1 |) in
                    let message := M.copy (| γ0_2 |) in
                    let exec_state := M.copy (| γ0_3 |) in
                    let indices := M.copy (| γ0_4 |) in
                    let offsets := M.copy (| γ0_5 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_binary_format::errors::VMError"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.path "move_binary_format::errors::VMError_";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            [
                              Value.StructRecord
                                "move_binary_format::errors::VMError_"
                                [
                                  ("major_status", M.read (| major_status |));
                                  ("sub_status", M.read (| sub_status |));
                                  ("message", M.read (| message |));
                                  ("exec_state", M.read (| exec_state |));
                                  ("location", M.read (| location |));
                                  ("indices", M.read (| indices |));
                                  ("offsets", M.read (| offsets |))
                                ]
                            ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_finish : M.IsAssociatedFunction Self "finish" finish.
    
    (*
        pub fn new(major_status: StatusCode) -> Self {
            Self(Box::new(PartialVMError_ {
                major_status,
                sub_status: None,
                message: None,
                exec_state: None,
                indices: vec![],
                offsets: vec![],
            }))
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ major_status ] =>
        ltac:(M.monadic
          (let major_status := M.alloc (| major_status |) in
          Value.StructTuple
            "move_binary_format::errors::PartialVMError"
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::boxed::Box")
                    []
                    [
                      Ty.path "move_binary_format::errors::PartialVMError_";
                      Ty.path "alloc::alloc::Global"
                    ],
                  "new",
                  []
                |),
                [
                  Value.StructRecord
                    "move_binary_format::errors::PartialVMError_"
                    [
                      ("major_status", M.read (| major_status |));
                      ("sub_status", Value.StructTuple "core::option::Option::None" []);
                      ("message", Value.StructTuple "core::option::Option::None" []);
                      ("exec_state", Value.StructTuple "core::option::Option::None" []);
                      ("indices",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "new",
                            []
                          |),
                          []
                        |));
                      ("offsets",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path
                                      "move_binary_format::file_format::FunctionDefinitionIndex";
                                    Ty.path "u16"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "new",
                            []
                          |),
                          []
                        |))
                    ]
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn major_status(&self) -> StatusCode {
            self.0.major_status
        }
    *)
    Definition major_status (ε : 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.SubPointer.get_struct_record_field (|
              M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_binary_format::errors::PartialVMError",
                  0
                |)
              |),
              "move_binary_format::errors::PartialVMError_",
              "major_status"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_major_status : M.IsAssociatedFunction Self "major_status" major_status.
    
    (*
        pub fn with_sub_status(mut self, sub_status: u64) -> Self {
            debug_assert!(self.0.sub_status.is_none());
            self.0.sub_status = Some(sub_status);
            self
        }
    *)
    Definition with_sub_status (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; sub_status ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let sub_status := M.alloc (| sub_status |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "u64" ],
                                            "is_none",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  self,
                                                  "move_binary_format::errors::PartialVMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::PartialVMError_",
                                              "sub_status"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String
                                            "assertion failed: self.0.sub_status.is_none()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (|
                      self,
                      "move_binary_format::errors::PartialVMError",
                      0
                    |)
                  |),
                  "move_binary_format::errors::PartialVMError_",
                  "sub_status"
                |),
                Value.StructTuple "core::option::Option::Some" [ M.read (| sub_status |) ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_with_sub_status :
      M.IsAssociatedFunction Self "with_sub_status" with_sub_status.
    
    (*
        pub fn with_message(mut self, message: String) -> Self {
            debug_assert!(self.0.message.is_none());
            self.0.message = Some(message);
            self
        }
    *)
    Definition with_message (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; message ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let message := M.alloc (| message |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "alloc::string::String" ],
                                            "is_none",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  self,
                                                  "move_binary_format::errors::PartialVMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::PartialVMError_",
                                              "message"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String "assertion failed: self.0.message.is_none()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (|
                      self,
                      "move_binary_format::errors::PartialVMError",
                      0
                    |)
                  |),
                  "move_binary_format::errors::PartialVMError_",
                  "message"
                |),
                Value.StructTuple "core::option::Option::Some" [ M.read (| message |) ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_with_message : M.IsAssociatedFunction Self "with_message" with_message.
    
    (*
        pub fn with_exec_state(mut self, exec_state: ExecutionState) -> Self {
            debug_assert!(self.0.exec_state.is_none());
            self.0.exec_state = Some(exec_state);
            self
        }
    *)
    Definition with_exec_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; exec_state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let exec_state := M.alloc (| exec_state |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "move_binary_format::errors::ExecutionState"
                                              ],
                                            "is_none",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  self,
                                                  "move_binary_format::errors::PartialVMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::PartialVMError_",
                                              "exec_state"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String
                                            "assertion failed: self.0.exec_state.is_none()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (|
                      self,
                      "move_binary_format::errors::PartialVMError",
                      0
                    |)
                  |),
                  "move_binary_format::errors::PartialVMError_",
                  "exec_state"
                |),
                Value.StructTuple "core::option::Option::Some" [ M.read (| exec_state |) ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_with_exec_state :
      M.IsAssociatedFunction Self "with_exec_state" with_exec_state.
    
    (*
        pub fn at_index(mut self, kind: IndexKind, index: TableIndex) -> Self {
            self.0.indices.push((kind, index));
            self
        }
    *)
    Definition at_index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; kind; index ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let kind := M.alloc (| kind |) in
          let index := M.alloc (| index |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (|
                        M.SubPointer.get_struct_tuple_field (|
                          self,
                          "move_binary_format::errors::PartialVMError",
                          0
                        |)
                      |),
                      "move_binary_format::errors::PartialVMError_",
                      "indices"
                    |);
                    Value.Tuple [ M.read (| kind |); M.read (| index |) ]
                  ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_at_index : M.IsAssociatedFunction Self "at_index" at_index.
    
    (*
        pub fn at_indices(mut self, additional_indices: Vec<(IndexKind, TableIndex)>) -> Self {
            self.0.indices.extend(additional_indices);
            self
        }
    *)
    Definition at_indices (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; additional_indices ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let additional_indices := M.alloc (| additional_indices |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::Extend",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [ Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ] ],
                    "extend",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (|
                        M.SubPointer.get_struct_tuple_field (|
                          self,
                          "move_binary_format::errors::PartialVMError",
                          0
                        |)
                      |),
                      "move_binary_format::errors::PartialVMError_",
                      "indices"
                    |);
                    M.read (| additional_indices |)
                  ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_at_indices : M.IsAssociatedFunction Self "at_indices" at_indices.
    
    (*
        pub fn at_code_offset(mut self, function: FunctionDefinitionIndex, offset: CodeOffset) -> Self {
            self.0.offsets.push((function, offset));
            self
        }
    *)
    Definition at_code_offset (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; function; offset ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let function := M.alloc (| function |) in
          let offset := M.alloc (| offset |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (|
                        M.SubPointer.get_struct_tuple_field (|
                          self,
                          "move_binary_format::errors::PartialVMError",
                          0
                        |)
                      |),
                      "move_binary_format::errors::PartialVMError_",
                      "offsets"
                    |);
                    Value.Tuple [ M.read (| function |); M.read (| offset |) ]
                  ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_at_code_offset :
      M.IsAssociatedFunction Self "at_code_offset" at_code_offset.
    
    (*
        pub fn at_code_offsets(
            mut self,
            additional_offsets: Vec<(FunctionDefinitionIndex, CodeOffset)>,
        ) -> Self {
            self.0.offsets.extend(additional_offsets);
            self
        }
    *)
    Definition at_code_offsets (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; additional_offsets ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let additional_offsets := M.alloc (| additional_offsets |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::Extend",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                            Ty.path "u16"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.tuple
                        [
                          Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                          Ty.path "u16"
                        ]
                    ],
                    "extend",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.tuple
                            [
                              Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                              Ty.path "u16"
                            ];
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (|
                        M.SubPointer.get_struct_tuple_field (|
                          self,
                          "move_binary_format::errors::PartialVMError",
                          0
                        |)
                      |),
                      "move_binary_format::errors::PartialVMError_",
                      "offsets"
                    |);
                    M.read (| additional_offsets |)
                  ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_at_code_offsets :
      M.IsAssociatedFunction Self "at_code_offsets" at_code_offsets.
    
    (*
        pub fn append_message_with_separator(
            mut self,
            separator: char,
            additional_message: String,
        ) -> Self {
            match self.0.message.as_mut() {
                Some(msg) => {
                    if !msg.is_empty() {
                        msg.push(separator);
                    }
                    msg.push_str(&additional_message);
                }
                None => self.0.message = Some(additional_message),
            };
            self
        }
    *)
    Definition append_message_with_separator
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; separator; additional_message ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let separator := M.alloc (| separator |) in
          let additional_message := M.alloc (| additional_message |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "alloc::string::String" ],
                      "as_mut",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            self,
                            "move_binary_format::errors::PartialVMError",
                            0
                          |)
                        |),
                        "move_binary_format::errors::PartialVMError_",
                        "message"
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let msg := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "alloc::string::String",
                                            "is_empty",
                                            []
                                          |),
                                          [ M.read (| msg |) ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "alloc::string::String",
                                        "push",
                                        []
                                      |),
                                      [ M.read (| msg |); M.read (| separator |) ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloc::string::String",
                              "push_str",
                              []
                            |),
                            [
                              M.read (| msg |);
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.path "alloc::string::String",
                                  [],
                                  "deref",
                                  []
                                |),
                                [ additional_message ]
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              self,
                              "move_binary_format::errors::PartialVMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::PartialVMError_",
                          "message"
                        |),
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ M.read (| additional_message |) ]
                      |)))
                ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_append_message_with_separator :
      M.IsAssociatedFunction Self "append_message_with_separator" append_message_with_separator.
  End Impl_move_binary_format_errors_PartialVMError.
  
  Module Impl_core_fmt_Display_for_move_binary_format_errors_Location.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::Location".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            match self {
                Location::Undefined => write!(f, "UNDEFINED"),
                Location::Module(id) => write!(f, "Module {:?}", id),
            }
        }
    *)
    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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_binary_format::errors::Location::Undefined"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "UNDEFINED" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_binary_format::errors::Location::Module",
                        0
                      |) in
                    let id := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (| Value.Array [ M.read (| Value.String "Module " |) ] |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_debug",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "move_core_types::language_storage::ModuleId"
                                            ]
                                        ]
                                      |),
                                      [ id ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_binary_format_errors_Location.
  
  Module Impl_core_fmt_Display_for_move_binary_format_errors_PartialVMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let mut status = format!("PartialVMError with status {:#?}", self.0.major_status);
    
            if let Some(sub_status) = self.0.sub_status {
                status = format!("{} with sub status {}", status, sub_status);
            }
    
            if let Some(msg) = &self.0.message {
                status = format!("{} and message {}", status, msg);
            }
    
            for (kind, index) in &self.0.indices {
                status = format!("{} at index {} for {}", status, index, kind);
            }
            for (fdef, code_offset) in &self.0.offsets {
                status = format!(
                    "{} at code offset {} in function definition {}",
                    status, code_offset, fdef
                );
            }
    
            write!(f, "{}", status)
        }
    *)
    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.read (|
            let~ status :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                  [
                    M.read (|
                      let~ res :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "alloc::fmt::format", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1_formatted",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [ M.read (| Value.String "PartialVMError with status " |) ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_debug",
                                            [ Ty.path "move_core_types::vm_status::StatusCode" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  M.read (| self |),
                                                  "move_binary_format::errors::PartialVMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::PartialVMError_",
                                              "major_status"
                                            |)
                                          ]
                                        |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Placeholder",
                                            "new",
                                            []
                                          |),
                                          [
                                            Value.Integer IntegerKind.Usize 0;
                                            Value.UnicodeChar 32;
                                            Value.StructTuple
                                              "core::fmt::rt::Alignment::Unknown"
                                              [];
                                            Value.Integer IntegerKind.U32 4;
                                            Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                            Value.StructTuple "core::fmt::rt::Count::Implied" []
                                          ]
                                        |)
                                      ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::UnsafeArg",
                                      "new",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |) in
                      res
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::PartialVMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::PartialVMError_",
                          "sub_status"
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let sub_status := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.write (|
                          status,
                          M.call_closure (|
                            M.get_function (|
                              "core::hint::must_use",
                              [ Ty.path "alloc::string::String" ]
                            |),
                            [
                              M.read (|
                                let~ res :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "alloc::fmt::format", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_v1",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.read (| Value.String "" |);
                                                  M.read (| Value.String " with sub status " |)
                                                ]
                                            |);
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "alloc::string::String" ]
                                                    |),
                                                    [ status ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "u64" ]
                                                    |),
                                                    [ sub_status ]
                                                  |)
                                                ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                res
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (|
                              M.SubPointer.get_struct_tuple_field (|
                                M.read (| self |),
                                "move_binary_format::errors::PartialVMError",
                                0
                              |)
                            |),
                            "move_binary_format::errors::PartialVMError_",
                            "message"
                          |)
                        |) in
                      let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let msg := M.alloc (| γ1_0 |) in
                      let~ _ :=
                        M.write (|
                          status,
                          M.call_closure (|
                            M.get_function (|
                              "core::hint::must_use",
                              [ Ty.path "alloc::string::String" ]
                            |),
                            [
                              M.read (|
                                let~ res :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "alloc::fmt::format", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_v1",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.read (| Value.String "" |);
                                                  M.read (| Value.String " and message " |)
                                                ]
                                            |);
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "alloc::string::String" ]
                                                    |),
                                                    [ status ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [ Ty.path "alloc::string::String" ]
                                                      ]
                                                    |),
                                                    [ msg ]
                                                  |)
                                                ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                res
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::PartialVMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::PartialVMError_",
                          "indices"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [
                                          Ty.tuple
                                            [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16"
                                            ]
                                        ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let γ0_0 := M.read (| γ0_0 |) in
                                      let γ2_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ2_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let kind := M.alloc (| γ2_0 |) in
                                      let index := M.alloc (| γ2_1 |) in
                                      let~ _ :=
                                        M.write (|
                                          status,
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::hint::must_use",
                                              [ Ty.path "alloc::string::String" ]
                                            |),
                                            [
                                              M.read (|
                                                let~ res :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (| "alloc::fmt::format", [] |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (| Value.String "" |);
                                                                  M.read (|
                                                                    Value.String " at index "
                                                                  |);
                                                                  M.read (| Value.String " for " |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.path
                                                                          "alloc::string::String"
                                                                      ]
                                                                    |),
                                                                    [ status ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u16" ]
                                                                      ]
                                                                    |),
                                                                    [ index ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::IndexKind"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ kind ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                res
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path
                                      "move_binary_format::file_format::FunctionDefinitionIndex";
                                    Ty.path "u16"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::PartialVMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::PartialVMError_",
                          "offsets"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FunctionDefinitionIndex";
                                              Ty.path "u16"
                                            ]
                                        ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let γ0_0 := M.read (| γ0_0 |) in
                                      let γ2_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ2_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let fdef := M.alloc (| γ2_0 |) in
                                      let code_offset := M.alloc (| γ2_1 |) in
                                      let~ _ :=
                                        M.write (|
                                          status,
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::hint::must_use",
                                              [ Ty.path "alloc::string::String" ]
                                            |),
                                            [
                                              M.read (|
                                                let~ res :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (| "alloc::fmt::format", [] |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (| Value.String "" |);
                                                                  M.read (|
                                                                    Value.String " at code offset "
                                                                  |);
                                                                  M.read (|
                                                                    Value.String
                                                                      " in function definition "
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.path
                                                                          "alloc::string::String"
                                                                      ]
                                                                    |),
                                                                    [ status ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u16" ]
                                                                      ]
                                                                    |),
                                                                    [ code_offset ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::file_format::FunctionDefinitionIndex"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ fdef ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                res
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
                [
                  M.read (| f |);
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                    [
                      M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "alloc::string::String" ]
                              |),
                              [ status ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_binary_format_errors_PartialVMError.
  
  Module Impl_core_fmt_Display_for_move_binary_format_errors_VMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::VMError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let mut status = format!("VMError with status {:#?}", self.0.major_status);
    
            if let Some(sub_status) = self.0.sub_status {
                status = format!("{} with sub status {}", status, sub_status);
            }
    
            status = format!("{} at location {}", status, self.0.location);
    
            if let Some(msg) = &self.0.message {
                status = format!("{} and message {}", status, msg);
            }
    
            for (kind, index) in &self.0.indices {
                status = format!("{} at index {} for {}", status, index, kind);
            }
            for (fdef, code_offset) in &self.0.offsets {
                status = format!(
                    "{} at code offset {} in function definition {}",
                    status, code_offset, fdef
                );
            }
    
            write!(f, "{}", status)
        }
    *)
    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.read (|
            let~ status :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                  [
                    M.read (|
                      let~ res :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "alloc::fmt::format", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1_formatted",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array [ M.read (| Value.String "VMError with status " |) ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_debug",
                                            [ Ty.path "move_core_types::vm_status::StatusCode" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  M.read (| self |),
                                                  "move_binary_format::errors::VMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::VMError_",
                                              "major_status"
                                            |)
                                          ]
                                        |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Placeholder",
                                            "new",
                                            []
                                          |),
                                          [
                                            Value.Integer IntegerKind.Usize 0;
                                            Value.UnicodeChar 32;
                                            Value.StructTuple
                                              "core::fmt::rt::Alignment::Unknown"
                                              [];
                                            Value.Integer IntegerKind.U32 4;
                                            Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                            Value.StructTuple "core::fmt::rt::Count::Implied" []
                                          ]
                                        |)
                                      ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::UnsafeArg",
                                      "new",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |) in
                      res
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::VMError_",
                          "sub_status"
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let sub_status := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.write (|
                          status,
                          M.call_closure (|
                            M.get_function (|
                              "core::hint::must_use",
                              [ Ty.path "alloc::string::String" ]
                            |),
                            [
                              M.read (|
                                let~ res :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "alloc::fmt::format", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_v1",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.read (| Value.String "" |);
                                                  M.read (| Value.String " with sub status " |)
                                                ]
                                            |);
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "alloc::string::String" ]
                                                    |),
                                                    [ status ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "u64" ]
                                                    |),
                                                    [ sub_status ]
                                                  |)
                                                ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                res
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.write (|
                status,
                M.call_closure (|
                  M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                  [
                    M.read (|
                      let~ res :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "alloc::fmt::format", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (| Value.String "" |);
                                        M.read (| Value.String " at location " |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "alloc::string::String" ]
                                          |),
                                          [ status ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "move_binary_format::errors::Location" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  M.read (| self |),
                                                  "move_binary_format::errors::VMError",
                                                  0
                                                |)
                                              |),
                                              "move_binary_format::errors::VMError_",
                                              "location"
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |) in
                      res
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (|
                              M.SubPointer.get_struct_tuple_field (|
                                M.read (| self |),
                                "move_binary_format::errors::VMError",
                                0
                              |)
                            |),
                            "move_binary_format::errors::VMError_",
                            "message"
                          |)
                        |) in
                      let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let msg := M.alloc (| γ1_0 |) in
                      let~ _ :=
                        M.write (|
                          status,
                          M.call_closure (|
                            M.get_function (|
                              "core::hint::must_use",
                              [ Ty.path "alloc::string::String" ]
                            |),
                            [
                              M.read (|
                                let~ res :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "alloc::fmt::format", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_v1",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.read (| Value.String "" |);
                                                  M.read (| Value.String " and message " |)
                                                ]
                                            |);
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [ Ty.path "alloc::string::String" ]
                                                    |),
                                                    [ status ]
                                                  |);
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::rt::Argument",
                                                      "new_display",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [ Ty.path "alloc::string::String" ]
                                                      ]
                                                    |),
                                                    [ msg ]
                                                  |)
                                                ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                res
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16" ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::VMError_",
                          "indices"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [
                                          Ty.tuple
                                            [ Ty.path "move_binary_format::IndexKind"; Ty.path "u16"
                                            ]
                                        ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let γ0_0 := M.read (| γ0_0 |) in
                                      let γ2_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ2_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let kind := M.alloc (| γ2_0 |) in
                                      let index := M.alloc (| γ2_1 |) in
                                      let~ _ :=
                                        M.write (|
                                          status,
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::hint::must_use",
                                              [ Ty.path "alloc::string::String" ]
                                            |),
                                            [
                                              M.read (|
                                                let~ res :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (| "alloc::fmt::format", [] |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (| Value.String "" |);
                                                                  M.read (|
                                                                    Value.String " at index "
                                                                  |);
                                                                  M.read (| Value.String " for " |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.path
                                                                          "alloc::string::String"
                                                                      ]
                                                                    |),
                                                                    [ status ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u16" ]
                                                                      ]
                                                                    |),
                                                                    [ index ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::IndexKind"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ kind ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                res
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path
                                      "move_binary_format::file_format::FunctionDefinitionIndex";
                                    Ty.path "u16"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_binary_format::errors::VMError",
                              0
                            |)
                          |),
                          "move_binary_format::errors::VMError_",
                          "offsets"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FunctionDefinitionIndex";
                                              Ty.path "u16"
                                            ]
                                        ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let γ0_0 := M.read (| γ0_0 |) in
                                      let γ2_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ2_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let fdef := M.alloc (| γ2_0 |) in
                                      let code_offset := M.alloc (| γ2_1 |) in
                                      let~ _ :=
                                        M.write (|
                                          status,
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::hint::must_use",
                                              [ Ty.path "alloc::string::String" ]
                                            |),
                                            [
                                              M.read (|
                                                let~ res :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (| "alloc::fmt::format", [] |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (| Value.String "" |);
                                                                  M.read (|
                                                                    Value.String " at code offset "
                                                                  |);
                                                                  M.read (|
                                                                    Value.String
                                                                      " in function definition "
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.path
                                                                          "alloc::string::String"
                                                                      ]
                                                                    |),
                                                                    [ status ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u16" ]
                                                                      ]
                                                                    |),
                                                                    [ code_offset ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_display",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::file_format::FunctionDefinitionIndex"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ fdef ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                res
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
                [
                  M.read (| f |);
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                    [
                      M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "alloc::string::String" ]
                              |),
                              [ status ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_binary_format_errors_VMError.
  
  (*
  pub fn offset_out_of_bounds(
      status: StatusCode,
      kind: IndexKind,
      target_offset: usize,
      target_pool_len: usize,
      cur_function: FunctionDefinitionIndex,
      cur_bytecode_offset: CodeOffset,
  ) -> PartialVMError {
      let msg = format!(
          "Index {} out of bounds for {} at bytecode offset {} in function {} while indexing {}",
          target_offset, target_pool_len, cur_bytecode_offset, cur_function, kind
      );
      PartialVMError::new(status)
          .with_message(msg)
          .at_code_offset(cur_function, cur_bytecode_offset)
  }
  *)
  Definition offset_out_of_bounds (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ status; kind; target_offset; target_pool_len; cur_function; cur_bytecode_offset ] =>
      ltac:(M.monadic
        (let status := M.alloc (| status |) in
        let kind := M.alloc (| kind |) in
        let target_offset := M.alloc (| target_offset |) in
        let target_pool_len := M.alloc (| target_pool_len |) in
        let cur_function := M.alloc (| cur_function |) in
        let cur_bytecode_offset := M.alloc (| cur_bytecode_offset |) in
        M.read (|
          let~ msg :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                [
                  M.read (|
                    let~ res :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "alloc::fmt::format", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (| Value.String "Index " |);
                                      M.read (| Value.String " out of bounds for " |);
                                      M.read (| Value.String " at bytecode offset " |);
                                      M.read (| Value.String " in function " |);
                                      M.read (| Value.String " while indexing " |)
                                    ]
                                |);
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [ target_offset ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [ target_pool_len ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "u16" ]
                                        |),
                                        [ cur_bytecode_offset ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::FunctionDefinitionIndex"
                                          ]
                                        |),
                                        [ cur_function ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "move_binary_format::IndexKind" ]
                                        |),
                                        [ kind ]
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    res
                  |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_binary_format::errors::PartialVMError",
                "at_code_offset",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_binary_format::errors::PartialVMError",
                    "with_message",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::errors::PartialVMError",
                        "new",
                        []
                      |),
                      [ M.read (| status |) ]
                    |);
                    M.read (| msg |)
                  ]
                |);
                M.read (| cur_function |);
                M.read (| cur_bytecode_offset |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_offset_out_of_bounds :
    M.IsFunction "move_binary_format::errors::offset_out_of_bounds" offset_out_of_bounds.
  
  (*
  pub fn bounds_error(
      status: StatusCode,
      kind: IndexKind,
      idx: TableIndex,
      len: usize,
  ) -> PartialVMError {
      let msg = format!(
          "Index {} out of bounds for {} while indexing {}",
          idx, len, kind
      );
      PartialVMError::new(status)
          .at_index(kind, idx)
          .with_message(msg)
  }
  *)
  Definition bounds_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ status; kind; idx; len ] =>
      ltac:(M.monadic
        (let status := M.alloc (| status |) in
        let kind := M.alloc (| kind |) in
        let idx := M.alloc (| idx |) in
        let len := M.alloc (| len |) in
        M.read (|
          let~ msg :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                [
                  M.read (|
                    let~ res :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "alloc::fmt::format", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (| Value.String "Index " |);
                                      M.read (| Value.String " out of bounds for " |);
                                      M.read (| Value.String " while indexing " |)
                                    ]
                                |);
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "u16" ]
                                        |),
                                        [ idx ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [ len ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "move_binary_format::IndexKind" ]
                                        |),
                                        [ kind ]
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    res
                  |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_binary_format::errors::PartialVMError",
                "with_message",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_binary_format::errors::PartialVMError",
                    "at_index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::errors::PartialVMError",
                        "new",
                        []
                      |),
                      [ M.read (| status |) ]
                    |);
                    M.read (| kind |);
                    M.read (| idx |)
                  ]
                |);
                M.read (| msg |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_bounds_error :
    M.IsFunction "move_binary_format::errors::bounds_error" bounds_error.
  
  (*
  pub fn verification_error(status: StatusCode, kind: IndexKind, idx: TableIndex) -> PartialVMError {
      PartialVMError::new(status).at_index(kind, idx)
  }
  *)
  Definition verification_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ status; kind; idx ] =>
      ltac:(M.monadic
        (let status := M.alloc (| status |) in
        let kind := M.alloc (| kind |) in
        let idx := M.alloc (| idx |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "move_binary_format::errors::PartialVMError",
            "at_index",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_binary_format::errors::PartialVMError",
                "new",
                []
              |),
              [ M.read (| status |) ]
            |);
            M.read (| kind |);
            M.read (| idx |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verification_error :
    M.IsFunction "move_binary_format::errors::verification_error" verification_error.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_PartialVMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Debug::fmt(&self.0, f)
        }
    *)
    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_trait_method (|
              "core::fmt::Debug",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [
                  Ty.path "move_binary_format::errors::PartialVMError_";
                  Ty.path "alloc::alloc::Global"
                ],
              [],
              "fmt",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_binary_format::errors::PartialVMError",
                0
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => 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_binary_format_errors_PartialVMError.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_errors_PartialVMError_.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError_".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let Self {
                major_status,
                sub_status,
                message,
                exec_state,
                indices,
                offsets,
            } = self;
            f.debug_struct("PartialVMError")
                .field("major_status", major_status)
                .field("sub_status", sub_status)
                .field("message", message)
                .field("exec_state", exec_state)
                .field("indices", indices)
                .field("offsets", offsets)
                .finish()
        }
    *)
    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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "major_status"
                      |) in
                    let γ1_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "sub_status"
                      |) in
                    let γ1_2 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "message"
                      |) in
                    let γ1_3 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "exec_state"
                      |) in
                    let γ1_4 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "indices"
                      |) in
                    let γ1_5 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "move_binary_format::errors::PartialVMError_",
                        "offsets"
                      |) in
                    let major_status := M.alloc (| γ1_0 |) in
                    let sub_status := M.alloc (| γ1_1 |) in
                    let message := M.alloc (| γ1_2 |) in
                    let exec_state := M.alloc (| γ1_3 |) in
                    let indices := M.alloc (| γ1_4 |) in
                    let offsets := M.alloc (| γ1_5 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugStruct",
                          "finish",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::builders::DebugStruct",
                              "field",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::builders::DebugStruct",
                                  "field",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::builders::DebugStruct",
                                      "field",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::builders::DebugStruct",
                                          "field",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::fmt::builders::DebugStruct",
                                              "field",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::builders::DebugStruct",
                                                  "field",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::Formatter",
                                                        "debug_struct",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| f |);
                                                        M.read (| Value.String "PartialVMError" |)
                                                      ]
                                                    |)
                                                  |);
                                                  M.read (| Value.String "major_status" |);
                                                  M.read (| major_status |)
                                                ]
                                              |);
                                              M.read (| Value.String "sub_status" |);
                                              M.read (| sub_status |)
                                            ]
                                          |);
                                          M.read (| Value.String "message" |);
                                          M.read (| message |)
                                        ]
                                      |);
                                      M.read (| Value.String "exec_state" |);
                                      M.read (| exec_state |)
                                    ]
                                  |);
                                  M.read (| Value.String "indices" |);
                                  M.read (| indices |)
                                ]
                              |);
                              M.read (| Value.String "offsets" |);
                              M.read (| offsets |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_errors_PartialVMError_.
  
  Module Impl_core_error_Error_for_move_binary_format_errors_PartialVMError.
    Definition Self : Ty.t := Ty.path "move_binary_format::errors::PartialVMError".
    
    (*
        fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
            None
        }
    *)
    Definition source (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple "core::option::Option::None" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("source", InstanceField.Method source) ].
  End Impl_core_error_Error_for_move_binary_format_errors_PartialVMError.
End errors.
