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

Module vec.
  Module drain.
    (* StructRecord
      {
        name := "Drain";
        const_params := [];
        ty_params := [ "T"; "A" ];
        fields :=
          [
            ("tail_start", Ty.path "usize");
            ("tail_len", Ty.path "usize");
            ("iter", Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ]);
            ("vec",
              Ty.apply
                (Ty.path "core::ptr::non_null::NonNull")
                []
                [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ] ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_tuple("Drain").field(&self.iter.as_slice()).finish()
          }
      *)
      Definition fmt (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        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::builders::DebugTuple",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugTuple",
                    "field",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Drain" |) ]
                      |)
                    |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                          "as_slice",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::vec::drain::Drain",
                            "iter"
                          |)
                        ]
                      |)
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T A)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          pub fn as_slice(&self) -> &[T] {
              self.iter.as_slice()
          }
      *)
      Definition as_slice (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                "as_slice",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::vec::drain::Drain",
                  "iter"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_slice :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "as_slice" (as_slice T A).
      
      (*
          pub fn allocator(&self) -> &A {
              unsafe { self.vec.as_ref().allocator() }
          }
      *)
      Definition allocator (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                "allocator",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ] ],
                    "as_ref",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::vec::drain::Drain",
                      "vec"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_allocator :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "allocator" (allocator T A).
      
      (*
          pub fn keep_rest(self) {
              // At this moment layout looks like this:
              //
              // [head] [yielded by next] [unyielded] [yielded by next_back] [tail]
              //        ^-- start         \_________/-- unyielded_len        \____/-- self.tail_len
              //                          ^-- unyielded_ptr                  ^-- tail
              //
              // Normally `Drop` impl would drop [unyielded] and then move [tail] to the `start`.
              // Here we want to
              // 1. Move [unyielded] to `start`
              // 2. Move [tail] to a new start at `start + len(unyielded)`
              // 3. Update length of the original vec to `len(head) + len(unyielded) + len(tail)`
              //    a. In case of ZST, this is the only thing we want to do
              // 4. Do *not* drop self, as everything is put in a consistent state already, there is nothing to do
              let mut this = ManuallyDrop::new(self);
      
              unsafe {
                  let source_vec = this.vec.as_mut();
      
                  let start = source_vec.len();
                  let tail = this.tail_start;
      
                  let unyielded_len = this.iter.len();
                  let unyielded_ptr = this.iter.as_slice().as_ptr();
      
                  // ZSTs have no identity, so we don't need to move them around.
                  if !T::IS_ZST {
                      let start_ptr = source_vec.as_mut_ptr().add(start);
      
                      // memmove back unyielded elements
                      if unyielded_ptr != start_ptr {
                          let src = unyielded_ptr;
                          let dst = start_ptr;
      
                          ptr::copy(src, dst, unyielded_len);
                      }
      
                      // memmove back untouched tail
                      if tail != (start + unyielded_len) {
                          let src = source_vec.as_ptr().add(tail);
                          let dst = start_ptr.add(unyielded_len);
                          ptr::copy(src, dst, this.tail_len);
                      }
                  }
      
                  source_vec.set_len(start + unyielded_len + this.tail_len);
              }
          }
      *)
      Definition keep_rest (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ this :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::manually_drop::ManuallyDrop")
                        []
                        [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                      "new",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ source_vec :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::ptr::non_null::NonNull")
                        []
                        [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ] ],
                      "as_mut",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::DerefMut",
                            Ty.apply
                              (Ty.path "core::mem::manually_drop::ManuallyDrop")
                              []
                              [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                            [],
                            "deref_mut",
                            []
                          |),
                          [ this ]
                        |),
                        "alloc::vec::drain::Drain",
                        "vec"
                      |)
                    ]
                  |)
                |) in
              let~ start :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                      "len",
                      []
                    |),
                    [ M.read (| source_vec |) ]
                  |)
                |) in
              let~ tail :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "core::mem::manually_drop::ManuallyDrop")
                          []
                          [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ this ]
                    |),
                    "alloc::vec::drain::Drain",
                    "tail_start"
                  |)
                |) in
              let~ unyielded_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::exact_size::ExactSizeIterator",
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                      [],
                      "len",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "core::mem::manually_drop::ManuallyDrop")
                              []
                              [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                            [],
                            "deref",
                            []
                          |),
                          [ this ]
                        |),
                        "alloc::vec::drain::Drain",
                        "iter"
                      |)
                    ]
                  |)
                |) in
              let~ unyielded_ptr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                          "as_slice",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                  []
                                  [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                                [],
                                "deref",
                                []
                              |),
                              [ this ]
                            |),
                            "alloc::vec::drain::Drain",
                            "iter"
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.read (|
                                  M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ start_ptr :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*mut") [] [ T ],
                                "add",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                                    "as_mut_ptr",
                                    []
                                  |),
                                  [ M.read (| source_vec |) ]
                                |);
                                M.read (| start |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ne (|
                                          M.read (| unyielded_ptr |),
                                          (* MutToConstPointer *)
                                          M.pointer_coercion (M.read (| start_ptr |))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ src := M.copy (| unyielded_ptr |) in
                                  let~ dst := M.copy (| start_ptr |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "core::intrinsics::copy", [ T ] |),
                                        [
                                          M.read (| src |);
                                          M.read (| dst |);
                                          M.read (| unyielded_len |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.ne (|
                                        M.read (| tail |),
                                        BinOp.Wrap.add (|
                                          M.read (| start |),
                                          M.read (| unyielded_len |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ src :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*const") [] [ T ],
                                        "add",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                                            "as_ptr",
                                            []
                                          |),
                                          [ M.read (| source_vec |) ]
                                        |);
                                        M.read (| tail |)
                                      ]
                                    |)
                                  |) in
                                let~ dst :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*mut") [] [ T ],
                                        "add",
                                        []
                                      |),
                                      [ M.read (| start_ptr |); M.read (| unyielded_len |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "core::intrinsics::copy", [ T ] |),
                                      [
                                        M.read (| src |);
                                        M.read (| dst |);
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.apply
                                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::drain::Drain")
                                                      []
                                                      [ T; A ]
                                                  ],
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [ this ]
                                            |),
                                            "alloc::vec::drain::Drain",
                                            "tail_len"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                      "set_len",
                      []
                    |),
                    [
                      M.read (| source_vec |);
                      BinOp.Wrap.add (|
                        BinOp.Wrap.add (| M.read (| start |), M.read (| unyielded_len |) |),
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                  []
                                  [ Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ] ],
                                [],
                                "deref",
                                []
                              |),
                              [ this ]
                            |),
                            "alloc::vec::drain::Drain",
                            "tail_len"
                          |)
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_keep_rest :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "keep_rest" (keep_rest T A).
    End Impl_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_convert_AsRef_where_core_alloc_Allocator_A_slice_T_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          fn as_ref(&self) -> &[T] {
              self.as_slice()
          }
      *)
      Definition as_ref (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ],
                "as_slice",
                []
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::convert::AsRef"
          (Self T A)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *) [ ("as_ref", InstanceField.Method (as_ref T A)) ].
    End Impl_core_convert_AsRef_where_core_alloc_Allocator_A_slice_T_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_marker_Sync_A_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::marker::Sync"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_marker_Sync_A_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_marker_Send_where_core_marker_Send_T_where_core_marker_Send_A_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::marker::Send"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_where_core_marker_Send_T_where_core_marker_Send_A_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*     type Item = T; *)
      Definition _Item (T A : Ty.t) : Ty.t := T.
      
      (*
          fn next(&mut self) -> Option<T> {
              self.iter.next().map(|elt| unsafe { ptr::read(elt as *const _) })
          }
      *)
      Definition next (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        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.apply (Ty.path "&") [] [ T ] ],
                "map",
                [ T; Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] T ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                    [],
                    "next",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::vec::drain::Drain",
                      "iter"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let elt := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_function (| "core::ptr::read", [ T ] |),
                                    [ M.read (| M.use (M.alloc (| M.read (| elt |) |)) |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              self.iter.size_hint()
          }
      *)
      Definition size_hint (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::vec::drain::Drain",
                  "iter"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T A));
            ("next", InstanceField.Method (next T A));
            ("size_hint", InstanceField.Method (size_hint T A))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          fn next_back(&mut self) -> Option<T> {
              self.iter.next_back().map(|elt| unsafe { ptr::read(elt as *const _) })
          }
      *)
      Definition next_back (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        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.apply (Ty.path "&") [] [ T ] ],
                "map",
                [ T; Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] T ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::double_ended::DoubleEndedIterator",
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                    [],
                    "next_back",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::vec::drain::Drain",
                      "iter"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let elt := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_function (| "core::ptr::read", [ T ] |),
                                    [ M.read (| M.use (M.alloc (| M.read (| elt |) |)) |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("next_back", InstanceField.Method (next_back T A)) ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          fn drop(&mut self) {
              /// Moves back the un-`Drain`ed elements to restore the original `Vec`.
              struct DropGuard<'r, 'a, T, A: Allocator>(&'r mut Drain<'a, T, A>);
      
              impl<'r, 'a, T, A: Allocator> Drop for DropGuard<'r, 'a, T, A> {
                  fn drop(&mut self) {
                      if self.0.tail_len > 0 {
                          unsafe {
                              let source_vec = self.0.vec.as_mut();
                              // memmove back untouched tail, update to new length
                              let start = source_vec.len();
                              let tail = self.0.tail_start;
                              if tail != start {
                                  let src = source_vec.as_ptr().add(tail);
                                  let dst = source_vec.as_mut_ptr().add(start);
                                  ptr::copy(src, dst, self.0.tail_len);
                              }
                              source_vec.set_len(start + self.0.tail_len);
                          }
                      }
                  }
              }
      
              let iter = mem::take(&mut self.iter);
              let drop_len = iter.len();
      
              let mut vec = self.vec;
      
              if T::IS_ZST {
                  // ZSTs have no identity, so we don't need to move them around, we only need to drop the correct amount.
                  // this can be achieved by manipulating the Vec length instead of moving values out from `iter`.
                  unsafe {
                      let vec = vec.as_mut();
                      let old_len = vec.len();
                      vec.set_len(old_len + drop_len + self.tail_len);
                      vec.truncate(old_len + self.tail_len);
                  }
      
                  return;
              }
      
              // ensure elements are moved back into their appropriate places, even when drop_in_place panics
              let _guard = DropGuard(self);
      
              if drop_len == 0 {
                  return;
              }
      
              // as_slice() must only be called when iter.len() is > 0 because
              // it also gets touched by vec::Splice which may turn it into a dangling pointer
              // which would make it and the vec pointer point to different allocations which would
              // lead to invalid pointer arithmetic below.
              let drop_ptr = iter.as_slice().as_ptr();
      
              unsafe {
                  // drop_ptr comes from a slice::Iter which only gives us a &[T] but for drop_in_place
                  // a pointer with mutable provenance is necessary. Therefore we must reconstruct
                  // it from the original vec but also avoid creating a &mut to the front since that could
                  // invalidate raw pointers to it which some unsafe code might rely on.
                  let vec_ptr = vec.as_mut().as_mut_ptr();
                  let drop_offset = drop_ptr.sub_ptr(vec_ptr);
                  let to_drop = ptr::slice_from_raw_parts_mut(vec_ptr.add(drop_offset), drop_len);
                  ptr::drop_in_place(to_drop);
              }
          }
      *)
      Definition drop (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ iter :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::mem::take",
                          [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ] ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::vec::drain::Drain",
                            "iter"
                          |)
                        ]
                      |)
                    |) in
                  let~ drop_len :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::exact_size::ExactSizeIterator",
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                          [],
                          "len",
                          []
                        |),
                        [ iter ]
                      |)
                    |) in
                  let~ vec :=
                    M.copy (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::vec::drain::Drain",
                        "vec"
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    let~ vec :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ] ],
                                            "as_mut",
                                            []
                                          |),
                                          [ vec ]
                                        |)
                                      |) in
                                    let~ old_len :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| vec |) ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                                            "set_len",
                                            []
                                          |),
                                          [
                                            M.read (| vec |);
                                            BinOp.Wrap.add (|
                                              BinOp.Wrap.add (|
                                                M.read (| old_len |),
                                                M.read (| drop_len |)
                                              |),
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "alloc::vec::drain::Drain",
                                                  "tail_len"
                                                |)
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                                            "truncate",
                                            []
                                          |),
                                          [
                                            M.read (| vec |);
                                            BinOp.Wrap.add (|
                                              M.read (| old_len |),
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "alloc::vec::drain::Drain",
                                                  "tail_len"
                                                |)
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _guard :=
                    M.alloc (|
                      Value.StructTuple "alloc::vec::drain::drop::DropGuard" [ M.read (| self |) ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (|
                                    M.read (| drop_len |),
                                    Value.Integer IntegerKind.Usize 0
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ drop_ptr :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "as_ptr",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                              "as_slice",
                              []
                            |),
                            [ iter ]
                          |)
                        ]
                      |)
                    |) in
                  let~ vec_ptr :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                          "as_mut_ptr",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::ptr::non_null::NonNull")
                                []
                                [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ] ],
                              "as_mut",
                              []
                            |),
                            [ vec ]
                          |)
                        ]
                      |)
                    |) in
                  let~ drop_offset :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "sub_ptr",
                          []
                        |),
                        [
                          M.read (| drop_ptr |);
                          (* MutToConstPointer *) M.pointer_coercion (M.read (| vec_ptr |))
                        ]
                      |)
                    |) in
                  let~ to_drop :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| vec_ptr |); M.read (| drop_offset |) ]
                          |);
                          M.read (| drop_len |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::ptr::drop_in_place",
                          [ Ty.apply (Ty.path "slice") [] [ T ] ]
                        |),
                        [ M.read (| to_drop |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::ops::drop::Drop"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method (drop T A)) ].
    End Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      (*
          fn is_empty(&self) -> bool {
              self.iter.is_empty()
          }
      *)
      Definition is_empty (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::exact_size::ExactSizeIterator",
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                [],
                "is_empty",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::vec::drain::Drain",
                  "iter"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("is_empty", InstanceField.Method (is_empty T A)) ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::drain::Drain") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_vec_drain_Drain_T_A.
  End drain.
End vec.
