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

Module future.
  Module async_drop.
    (*
    pub fn async_drop<T>(value: T) -> AsyncDropOwning<T> {
        AsyncDropOwning { value: MaybeUninit::new(value), dtor: None, _pinned: PhantomPinned }
    }
    *)
    Definition async_drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::future::async_drop::AsyncDropOwning"
            [
              ("value",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "new",
                    []
                  |),
                  [ M.read (| value |) ]
                |));
              ("dtor", Value.StructTuple "core::option::Option::None" []);
              ("_pinned", Value.StructTuple "core::marker::PhantomPinned" [])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_async_drop : M.IsFunction "core::future::async_drop::async_drop" async_drop.
    
    (* StructRecord
      {
        name := "AsyncDropOwning";
        const_params := [];
        ty_params := [ "T" ];
        fields :=
          [
            ("value", Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]);
            ("dtor",
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [ Ty.apply (Ty.path "core::future::async_drop::AsyncDropInPlace") [] [ T ] ]);
            ("_pinned", Ty.path "core::marker::PhantomPinned")
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_future_async_drop_AsyncDropOwning_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::async_drop::AsyncDropOwning") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("AsyncDropOwning").finish_non_exhaustive()
          }
      *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T 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::DebugStruct",
                "finish_non_exhaustive",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "AsyncDropOwning" |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_for_core_future_async_drop_AsyncDropOwning_T.
    
    Module Impl_core_future_future_Future_for_core_future_async_drop_AsyncDropOwning_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::async_drop::AsyncDropOwning") [] [ T ].
      
      (*     type Output = (); *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.tuple [].
      
      (*
          fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              // SAFETY: Self is pinned thus it is ok to store references to self
              unsafe {
                  let this = self.get_unchecked_mut();
                  let dtor = Pin::new_unchecked(
                      this.dtor.get_or_insert_with(|| async_drop_in_place(this.value.as_mut_ptr())),
                  );
                  // AsyncDestuctors are idempotent so Self gets idempotency as well
                  dtor.poll(cx)
              }
          }
      *)
      Definition poll (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let cx := M.alloc (| cx |) in
            M.read (|
              let~ this :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::pin::Pin")
                        []
                        [
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::future::async_drop::AsyncDropOwning")
                                []
                                [ T ]
                            ]
                        ],
                      "get_unchecked_mut",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ dtor :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::pin::Pin")
                        []
                        [
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::future::async_drop::AsyncDropInPlace")
                                []
                                [ T ]
                            ]
                        ],
                      "new_unchecked",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::future::async_drop::AsyncDropInPlace")
                                []
                                [ T ]
                            ],
                          "get_or_insert_with",
                          [
                            Ty.function
                              [ Ty.tuple [] ]
                              (Ty.apply
                                (Ty.path "core::future::async_drop::AsyncDropInPlace")
                                []
                                [ T ])
                          ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| this |),
                            "core::future::async_drop::AsyncDropOwning",
                            "dtor"
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.call_closure (|
                                              M.get_function (|
                                                "core::future::async_drop::async_drop_in_place",
                                                [ T ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ T ],
                                                    "as_mut_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| this |),
                                                      "core::future::async_drop::AsyncDropOwning",
                                                      "value"
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::future::future::Future",
                    Ty.apply (Ty.path "core::future::async_drop::AsyncDropInPlace") [] [ T ],
                    [],
                    "poll",
                    []
                  |),
                  [ M.read (| dtor |); M.read (| cx |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output T)); ("poll", InstanceField.Method (poll T)) ].
    End Impl_core_future_future_Future_for_core_future_async_drop_AsyncDropOwning_T.
    
    (*
    unsafe fn async_drop_in_place_raw<T: ?Sized>(
        to_drop: *mut T,
    ) -> <T as AsyncDestruct>::AsyncDestructor {
        // Code here does not matter - this is replaced by the
        // real async drop glue constructor by the compiler.
    
        // SAFETY: see comment above
        unsafe { async_drop_in_place_raw(to_drop) }
    }
    *)
    Definition async_drop_in_place_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ to_drop ] =>
        ltac:(M.monadic
          (let to_drop := M.alloc (| to_drop |) in
          M.call_closure (|
            M.get_function (| "core::future::async_drop::async_drop_in_place_raw", [ T ] |),
            [ M.read (| to_drop |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_async_drop_in_place_raw :
      M.IsFunction "core::future::async_drop::async_drop_in_place_raw" async_drop_in_place_raw.
    
    (*
    pub unsafe fn async_drop_in_place<T: ?Sized>(to_drop: *mut T) -> AsyncDropInPlace<T> {
        // SAFETY: `async_drop_in_place_raw` has the same safety requirements
        unsafe { AsyncDropInPlace(async_drop_in_place_raw(to_drop)) }
    }
    *)
    Definition async_drop_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ to_drop ] =>
        ltac:(M.monadic
          (let to_drop := M.alloc (| to_drop |) in
          Value.StructTuple
            "core::future::async_drop::AsyncDropInPlace"
            [
              M.call_closure (|
                M.get_function (| "core::future::async_drop::async_drop_in_place_raw", [ T ] |),
                [ M.read (| to_drop |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_async_drop_in_place :
      M.IsFunction "core::future::async_drop::async_drop_in_place" async_drop_in_place.
    
    (* StructTuple
      {
        name := "AsyncDropInPlace";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ Ty.associated ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_marker_Sized_T_for_core_future_async_drop_AsyncDropInPlace_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::async_drop::AsyncDropInPlace") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("AsyncDropInPlace").finish_non_exhaustive()
          }
      *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T 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::DebugStruct",
                "finish_non_exhaustive",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "AsyncDropInPlace" |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_marker_Sized_T_for_core_future_async_drop_AsyncDropInPlace_T.
    
    Module Impl_core_future_future_Future_where_core_marker_Sized_T_for_core_future_async_drop_AsyncDropInPlace_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::async_drop::AsyncDropInPlace") [] [ T ].
      
      (*     type Output = (); *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.tuple [].
      
      (*
          fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              // SAFETY: This code simply forwards poll call to the inner future
              unsafe { Pin::new_unchecked(&mut self.get_unchecked_mut().0) }.poll(cx)
          }
      *)
      Definition poll (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let cx := M.alloc (| cx |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::future::future::Future",
                Ty.associated,
                [],
                "poll",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::pin::Pin")
                      []
                      [ Ty.apply (Ty.path "&mut") [] [ Ty.associated ] ],
                    "new_unchecked",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::pin::Pin")
                            []
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::future::async_drop::AsyncDropInPlace")
                                    []
                                    [ T ]
                                ]
                            ],
                          "get_unchecked_mut",
                          []
                        |),
                        [ M.read (| self |) ]
                      |),
                      "core::future::async_drop::AsyncDropInPlace",
                      0
                    |)
                  ]
                |);
                M.read (| cx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output T)); ("poll", InstanceField.Method (poll T)) ].
    End Impl_core_future_future_Future_where_core_marker_Sized_T_for_core_future_async_drop_AsyncDropInPlace_T.
    
    (* Trait *)
    (* Empty module 'AsyncDrop' *)
    
    (* Trait *)
    (* Empty module 'AsyncDestruct' *)
    
    (*
    async unsafe fn surface_async_drop_in_place<T: AsyncDrop + ?Sized>(ptr: *mut T) {
        // SAFETY: We call this from async drop `async_drop_in_place_raw`
        //   which has the same safety requirements
        unsafe { <T as AsyncDrop>::async_drop(Pin::new_unchecked(&mut *ptr)).await }
    }
    *)
    Definition surface_async_drop_in_place
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ ptr := M.copy (| ptr |) in
                              M.use
                                (M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::future::into_future::IntoFuture",
                                        Ty.associated,
                                        [],
                                        "into_future",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::future::async_drop::AsyncDrop",
                                            T,
                                            [],
                                            "async_drop",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::pin::Pin")
                                                  []
                                                  [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                                                "new_unchecked",
                                                []
                                              |),
                                              [ M.read (| ptr |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let __awaitee := M.copy (| γ |) in
                                        M.loop (|
                                          ltac:(M.monadic
                                            (let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::future::future::Future",
                                                      Ty.associated,
                                                      [],
                                                      "poll",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::pin::Pin")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&mut")
                                                                []
                                                                [ Ty.associated ]
                                                            ],
                                                          "new_unchecked",
                                                          []
                                                        |),
                                                        [ __awaitee ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::future::get_context",
                                                          []
                                                        |),
                                                        [ M.read (| _task_context |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::task::poll::Poll::Ready",
                                                          0
                                                        |) in
                                                      let result := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (| M.break (||) |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::task::poll::Poll::Pending"
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                _task_context,
                                                M.read (|
                                                  yield (| M.alloc (| Value.Tuple [] |) |)
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                        |)))
                                  ]
                                |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_surface_async_drop_in_place :
      M.IsFunction
        "core::future::async_drop::surface_async_drop_in_place"
        surface_async_drop_in_place.
    
    Module surface_async_drop_in_place.
      (* Error OpaqueTy *)
    End surface_async_drop_in_place.
    
    (*
    async unsafe fn surface_drop_in_place<T: Drop + ?Sized>(ptr: *mut T) {
        // SAFETY: We call this from async drop `async_drop_in_place_raw`
        //   which has the same safety requirements
        unsafe { crate::ops::fallback_surface_drop(&mut *ptr) }
    }
    *)
    Definition surface_drop_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ ptr ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ ptr := M.copy (| ptr |) in
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::ops::drop::fallback_surface_drop",
                                      [ T ]
                                    |),
                                    [ M.read (| ptr |) ]
                                  |)
                                |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_surface_drop_in_place :
      M.IsFunction "core::future::async_drop::surface_drop_in_place" surface_drop_in_place.
    
    Module surface_drop_in_place.
      (* Error OpaqueTy *)
    End surface_drop_in_place.
    
    (* StructRecord
      {
        name := "Fuse";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ ("inner", Ty.apply (Ty.path "core::option::Option") [] [ T ]) ];
      } *)
    
    (*
    fn fuse<T>(inner: T) -> Fuse<T> {
        Fuse { inner: Some(inner) }
    }
    *)
    Definition fuse (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ inner ] =>
        ltac:(M.monadic
          (let inner := M.alloc (| inner |) in
          Value.StructRecord
            "core::future::async_drop::Fuse"
            [ ("inner", Value.StructTuple "core::option::Option::Some" [ M.read (| inner |) ]) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_fuse : M.IsFunction "core::future::async_drop::fuse" fuse.
    
    Module Impl_core_future_future_Future_where_core_future_future_Future_T_for_core_future_async_drop_Fuse_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::async_drop::Fuse") [] [ T ].
      
      (*     type Output = (); *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.tuple [].
      
      (*
          fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              // SAFETY: pin projection into `self.inner`
              unsafe {
                  let this = self.get_unchecked_mut();
                  if let Some(inner) = &mut this.inner {
                      ready!(Pin::new_unchecked(inner).poll(cx));
                      this.inner = None;
                  }
              }
              Poll::Ready(())
          }
      *)
      Definition poll (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let cx := M.alloc (| cx |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    let~ this :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::pin::Pin")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "core::future::async_drop::Fuse") [] [ T ] ]
                              ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| this |),
                                  "core::future::async_drop::Fuse",
                                  "inner"
                                |)
                              |) in
                            let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let inner := M.alloc (| γ1_0 |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::future::future::Future",
                                      T,
                                      [],
                                      "poll",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::pin::Pin")
                                            []
                                            [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                                          "new_unchecked",
                                          []
                                        |),
                                        [ M.read (| inner |) ]
                                      |);
                                      M.read (| cx |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::task::poll::Poll::Ready",
                                          0
                                        |) in
                                      let t := M.copy (| γ0_0 |) in
                                      t));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (|
                                          γ,
                                          "core::task::poll::Poll::Pending"
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple "core::task::poll::Poll::Pending" []
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| this |),
                                  "core::future::async_drop::Fuse",
                                  "inner"
                                |),
                                Value.StructTuple "core::option::Option::None" []
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (| Value.StructTuple "core::task::poll::Poll::Ready" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output T)); ("poll", InstanceField.Method (poll T)) ].
    End Impl_core_future_future_Future_where_core_future_future_Future_T_for_core_future_async_drop_Fuse_T.
    
    (*
    async unsafe fn slice<T>(s: *mut [T]) {
        let len = s.len();
        let ptr = s.as_mut_ptr();
        for i in 0..len {
            // SAFETY: we iterate over elements of `s` slice
            unsafe { async_drop_in_place_raw(ptr.add(i)).await }
        }
    }
    *)
    Definition slice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ s := M.copy (| s |) in
                              M.use
                                (let~ len :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*mut")
                                          []
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| s |) ]
                                    |)
                                  |) in
                                let~ ptr :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*mut")
                                          []
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                        "as_mut_ptr",
                                        []
                                      |),
                                      [ M.read (| s |) ]
                                    |)
                                  |) in
                                M.use
                                  (M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::collect::IntoIterator",
                                          Ty.apply
                                            (Ty.path "core::ops::range::Range")
                                            []
                                            [ Ty.path "usize" ],
                                          [],
                                          "into_iter",
                                          []
                                        |),
                                        [
                                          Value.StructRecord
                                            "core::ops::range::Range"
                                            [
                                              ("start", Value.Integer IntegerKind.Usize 0);
                                              ("end_", M.read (| len |))
                                            ]
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let iter := M.copy (| γ |) in
                                          M.loop (|
                                            ltac:(M.monadic
                                              (let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::iter::traits::iterator::Iterator",
                                                        Ty.apply
                                                          (Ty.path "core::ops::range::Range")
                                                          []
                                                          [ Ty.path "usize" ],
                                                        [],
                                                        "next",
                                                        []
                                                      |),
                                                      [ iter ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let _ :=
                                                          M.is_struct_tuple (|
                                                            γ,
                                                            "core::option::Option::None"
                                                          |) in
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.read (| M.break (||) |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::option::Option::Some",
                                                            0
                                                          |) in
                                                        let i := M.copy (| γ0_0 |) in
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::future::into_future::IntoFuture",
                                                                Ty.associated,
                                                                [],
                                                                "into_future",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::future::async_drop::async_drop_in_place_raw",
                                                                    [ T ]
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "*mut")
                                                                          []
                                                                          [ T ],
                                                                        "add",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| ptr |);
                                                                        M.read (| i |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let __awaitee := M.copy (| γ |) in
                                                                M.loop (|
                                                                  ltac:(M.monadic
                                                                    (let~ _ :=
                                                                      M.match_operator (|
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::future::future::Future",
                                                                              Ty.associated,
                                                                              [],
                                                                              "poll",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::pin::Pin")
                                                                                    []
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "&mut")
                                                                                        []
                                                                                        [
                                                                                          Ty.associated
                                                                                        ]
                                                                                    ],
                                                                                  "new_unchecked",
                                                                                  []
                                                                                |),
                                                                                [ __awaitee ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_function (|
                                                                                  "core::future::get_context",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    _task_context
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "core::task::poll::Poll::Ready",
                                                                                  0
                                                                                |) in
                                                                              let result :=
                                                                                M.copy (| γ0_0 |) in
                                                                              M.alloc (|
                                                                                M.never_to_any (|
                                                                                  M.read (|
                                                                                    M.break (||)
                                                                                  |)
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let _ :=
                                                                                M.is_struct_tuple (|
                                                                                  γ,
                                                                                  "core::task::poll::Poll::Pending"
                                                                                |) in
                                                                              M.alloc (|
                                                                                Value.Tuple []
                                                                              |)))
                                                                        ]
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.write (|
                                                                        _task_context,
                                                                        M.read (|
                                                                          yield (|
                                                                            M.alloc (|
                                                                              Value.Tuple []
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |)))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_slice : M.IsFunction "core::future::async_drop::slice" slice.
    
    Module slice.
      (* Error OpaqueTy *)
    End slice.
    
    (*
    async fn chain<F, G>(first: F, last: G)
    where
        F: IntoFuture<Output = ()>,
        G: IntoFuture<Output = ()>,
    {
        first.await;
        last.await;
    }
    *)
    Definition chain (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ F; G ], [ first; last ] =>
        ltac:(M.monadic
          (let first := M.alloc (| first |) in
          let last := M.alloc (| last |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ first := M.copy (| first |) in
                              let~ last := M.copy (| last |) in
                              M.use
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::future::into_future::IntoFuture",
                                          F,
                                          [],
                                          "into_future",
                                          []
                                        |),
                                        [ M.read (| first |) ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let __awaitee := M.copy (| γ |) in
                                          M.loop (|
                                            ltac:(M.monadic
                                              (let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::future::future::Future",
                                                        Ty.associated,
                                                        [],
                                                        "poll",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::pin::Pin")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&mut")
                                                                  []
                                                                  [ Ty.associated ]
                                                              ],
                                                            "new_unchecked",
                                                            []
                                                          |),
                                                          [ __awaitee ]
                                                        |);
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::future::get_context",
                                                            []
                                                          |),
                                                          [ M.read (| _task_context |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::task::poll::Poll::Ready",
                                                            0
                                                          |) in
                                                        let result := M.copy (| γ0_0 |) in
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.read (| M.break (||) |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let _ :=
                                                          M.is_struct_tuple (|
                                                            γ,
                                                            "core::task::poll::Poll::Pending"
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              let~ _ :=
                                                M.write (|
                                                  _task_context,
                                                  M.read (|
                                                    yield (| M.alloc (| Value.Tuple [] |) |)
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::future::into_future::IntoFuture",
                                          G,
                                          [],
                                          "into_future",
                                          []
                                        |),
                                        [ M.read (| last |) ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let __awaitee := M.copy (| γ |) in
                                          M.loop (|
                                            ltac:(M.monadic
                                              (let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::future::future::Future",
                                                        Ty.associated,
                                                        [],
                                                        "poll",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::pin::Pin")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&mut")
                                                                  []
                                                                  [ Ty.associated ]
                                                              ],
                                                            "new_unchecked",
                                                            []
                                                          |),
                                                          [ __awaitee ]
                                                        |);
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::future::get_context",
                                                            []
                                                          |),
                                                          [ M.read (| _task_context |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::task::poll::Poll::Ready",
                                                            0
                                                          |) in
                                                        let result := M.copy (| γ0_0 |) in
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.read (| M.break (||) |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let _ :=
                                                          M.is_struct_tuple (|
                                                            γ,
                                                            "core::task::poll::Poll::Pending"
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              let~ _ :=
                                                M.write (|
                                                  _task_context,
                                                  M.read (|
                                                    yield (| M.alloc (| Value.Tuple [] |) |)
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_chain : M.IsFunction "core::future::async_drop::chain" chain.
    
    Module chain.
      (* Error OpaqueTy *)
    End chain.
    
    (*
    async unsafe fn defer<T: ?Sized>(to_drop: *mut T) {
        // SAFETY: same safety requirements as `async_drop_in_place`
        unsafe { async_drop_in_place(to_drop) }.await
    }
    *)
    Definition defer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ to_drop ] =>
        ltac:(M.monadic
          (let to_drop := M.alloc (| to_drop |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ to_drop := M.copy (| to_drop |) in
                              M.use
                                (M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::future::into_future::IntoFuture",
                                        Ty.apply
                                          (Ty.path "core::future::async_drop::AsyncDropInPlace")
                                          []
                                          [ T ],
                                        [],
                                        "into_future",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::future::async_drop::async_drop_in_place",
                                            [ T ]
                                          |),
                                          [ M.read (| to_drop |) ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let __awaitee := M.copy (| γ |) in
                                        M.loop (|
                                          ltac:(M.monadic
                                            (let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::future::future::Future",
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::future::async_drop::AsyncDropInPlace")
                                                        []
                                                        [ T ],
                                                      [],
                                                      "poll",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::pin::Pin")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&mut")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::future::async_drop::AsyncDropInPlace")
                                                                    []
                                                                    [ T ]
                                                                ]
                                                            ],
                                                          "new_unchecked",
                                                          []
                                                        |),
                                                        [ __awaitee ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::future::get_context",
                                                          []
                                                        |),
                                                        [ M.read (| _task_context |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::task::poll::Poll::Ready",
                                                          0
                                                        |) in
                                                      let result := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (| M.break (||) |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "core::task::poll::Poll::Pending"
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                _task_context,
                                                M.read (|
                                                  yield (| M.alloc (| Value.Tuple [] |) |)
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                        |)))
                                  ]
                                |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_defer : M.IsFunction "core::future::async_drop::defer" defer.
    
    Module defer.
      (* Error OpaqueTy *)
    End defer.
    
    (*
    async unsafe fn either<O: IntoFuture<Output = ()>, M: IntoFuture<Output = ()>, T>(
        other: O,
        matched: M,
        this: *mut T,
        discr: <T as DiscriminantKind>::Discriminant,
    ) {
        // SAFETY: Guaranteed by the safety section of this funtion's documentation
        if unsafe { discriminant_value(&*this) } == discr {
            drop(other);
            matched.await
        } else {
            drop(matched);
            other.await
        }
    }
    *)
    Definition either (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as O; M_; T ], [ other; matched; this; discr ] =>
        ltac:(M.monadic
          (let other := M.alloc (| other |) in
          let matched := M.alloc (| matched |) in
          let this := M.alloc (| this |) in
          let discr := M.alloc (| discr |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ other := M.copy (| other |) in
                              let~ matched := M.copy (| matched |) in
                              let~ this := M.copy (| this |) in
                              let~ discr := M.copy (| discr |) in
                              M.use
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::cmp::PartialEq",
                                                  Ty.associated,
                                                  [ Ty.associated ],
                                                  "eq",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::intrinsics::discriminant_value",
                                                        [ T ]
                                                      |),
                                                      [ M.read (| this |) ]
                                                    |)
                                                  |);
                                                  discr
                                                ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::drop", [ O ] |),
                                              [ M.read (| other |) ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::future::into_future::IntoFuture",
                                                M_,
                                                [],
                                                "into_future",
                                                []
                                              |),
                                              [ M.read (| matched |) ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let __awaitee := M.copy (| γ |) in
                                                M.loop (|
                                                  ltac:(M.monadic
                                                    (let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::future::future::Future",
                                                              Ty.associated,
                                                              [],
                                                              "poll",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::pin::Pin")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "&mut")
                                                                        []
                                                                        [ Ty.associated ]
                                                                    ],
                                                                  "new_unchecked",
                                                                  []
                                                                |),
                                                                [ __awaitee ]
                                                              |);
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::future::get_context",
                                                                  []
                                                                |),
                                                                [ M.read (| _task_context |) ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::task::poll::Poll::Ready",
                                                                  0
                                                                |) in
                                                              let result := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (| M.break (||) |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "core::task::poll::Poll::Pending"
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        _task_context,
                                                        M.read (|
                                                          yield (| M.alloc (| Value.Tuple [] |) |)
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                                |)))
                                          ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::drop", [ M_ ] |),
                                              [ M.read (| matched |) ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::future::into_future::IntoFuture",
                                                O,
                                                [],
                                                "into_future",
                                                []
                                              |),
                                              [ M.read (| other |) ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let __awaitee := M.copy (| γ |) in
                                                M.loop (|
                                                  ltac:(M.monadic
                                                    (let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::future::future::Future",
                                                              Ty.associated,
                                                              [],
                                                              "poll",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::pin::Pin")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "&mut")
                                                                        []
                                                                        [ Ty.associated ]
                                                                    ],
                                                                  "new_unchecked",
                                                                  []
                                                                |),
                                                                [ __awaitee ]
                                                              |);
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::future::get_context",
                                                                  []
                                                                |),
                                                                [ M.read (| _task_context |) ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::task::poll::Poll::Ready",
                                                                  0
                                                                |) in
                                                              let result := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (| M.break (||) |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ,
                                                                  "core::task::poll::Poll::Pending"
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        _task_context,
                                                        M.read (|
                                                          yield (| M.alloc (| Value.Tuple [] |) |)
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                                |)))
                                          ]
                                        |)))
                                  ]
                                |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_either : M.IsFunction "core::future::async_drop::either" either.
    
    Module either.
      (* Error OpaqueTy *)
    End either.
    
    (*
    async unsafe fn deferred_drop_in_place<T>(to_drop: *mut T) {
        // SAFETY: same safety requirements as with drop_in_place (implied by
        // function's name)
        unsafe { crate::ptr::drop_in_place(to_drop) }
    }
    *)
    Definition deferred_drop_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ to_drop ] =>
        ltac:(M.monadic
          (let to_drop := M.alloc (| to_drop |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _task_context := M.copy (| γ |) in
                            M.read (|
                              let~ to_drop := M.copy (| to_drop |) in
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::ptr::drop_in_place", [ T ] |),
                                    [ M.read (| to_drop |) ]
                                  |)
                                |))
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_deferred_drop_in_place :
      M.IsFunction "core::future::async_drop::deferred_drop_in_place" deferred_drop_in_place.
    
    Module deferred_drop_in_place.
      (* Error OpaqueTy *)
    End deferred_drop_in_place.
    
    (* StructTuple
      {
        name := "Noop";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    Module Impl_core_clone_Clone_for_core_future_async_drop_Noop.
      Definition Self : Ty.t := Ty.path "core::future::async_drop::Noop".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_future_async_drop_Noop.
    
    Module Impl_core_marker_Copy_for_core_future_async_drop_Noop.
      Definition Self : Ty.t := Ty.path "core::future::async_drop::Noop".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_future_async_drop_Noop.
    
    (*
    fn noop() -> Noop {
        Noop
    }
    *)
    Definition noop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::future::async_drop::Noop" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_noop : M.IsFunction "core::future::async_drop::noop" noop.
    
    Module Impl_core_future_future_Future_for_core_future_async_drop_Noop.
      Definition Self : Ty.t := Ty.path "core::future::async_drop::Noop".
      
      (*     type Output = (); *)
      Definition _Output : Ty.t := Ty.tuple [].
      
      (*
          fn poll(self: Pin<&mut Self>, _: &mut Context<'_>) -> Poll<Self::Output> {
              Poll::Ready(())
          }
      *)
      Definition poll (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [
                fun γ =>
                  ltac:(M.monadic
                    (Value.StructTuple "core::task::poll::Poll::Ready" [ Value.Tuple [] ]))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::future::future::Future"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("poll", InstanceField.Method poll) ].
    End Impl_core_future_future_Future_for_core_future_async_drop_Noop.
  End async_drop.
End future.
