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

Module task.
  Module wake.
    (* StructRecord
      {
        name := "RawWaker";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("data", Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ]);
            ("vtable", Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::RawWakerVTable" ])
          ];
      } *)
    
    Module Impl_core_marker_StructuralPartialEq_for_core_task_wake_RawWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWaker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_task_wake_RawWaker.
    
    Module Impl_core_cmp_PartialEq_for_core_task_wake_RawWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWaker".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |)
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::RawWakerVTable" ],
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::RawWakerVTable" ] ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_task_wake_RawWaker.
    
    Module Impl_core_fmt_Debug_for_core_task_wake_RawWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWaker".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "RawWaker" |);
                M.read (| Value.String "data" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::RawWaker",
                  "data"
                |);
                M.read (| Value.String "vtable" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::task::wake::RawWaker",
                    "vtable"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_RawWaker.
    
    Module Impl_core_task_wake_RawWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWaker".
      
      (*
          pub const fn new(data: *const (), vtable: &'static RawWakerVTable) -> RawWaker {
              RawWaker { data, vtable }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ data; vtable ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let vtable := M.alloc (| vtable |) in
            Value.StructRecord
              "core::task::wake::RawWaker"
              [ ("data", M.read (| data |)); ("vtable", M.read (| vtable |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          const NOOP: RawWaker = {
              const VTABLE: RawWakerVTable = RawWakerVTable::new(
                  // Cloning just returns a new no-op raw waker
                  |_| RawWaker::NOOP,
                  // `wake` does nothing
                  |_| {},
                  // `wake_by_ref` does nothing
                  |_| {},
                  // Dropping does nothing as we don't allocate anything
                  |_| {},
              );
              RawWaker::new(ptr::null(), &VTABLE)
          };
      *)
      (* Ty.path "core::task::wake::RawWaker" *)
      Definition value_NOOP : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::task::wake::RawWaker", "new", [] |),
                [
                  M.call_closure (| M.get_function (| "core::ptr::null", [ Ty.tuple [] ] |), [] |);
                  M.get_constant (| "core::task::wake::NOOP::VTABLE" |)
                ]
              |)
            |))).
      
      Axiom AssociatedConstant_value_NOOP : M.IsAssociatedConstant Self "value_NOOP" value_NOOP.
    End Impl_core_task_wake_RawWaker.
    
    (* StructRecord
      {
        name := "RawWakerVTable";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("clone",
              Ty.function
                [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ] ]
                (Ty.path "core::task::wake::RawWaker"));
            ("wake", Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ] ] (Ty.tuple []));
            ("wake_by_ref",
              Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ] ] (Ty.tuple []));
            ("drop", Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ] ] (Ty.tuple []))
          ];
      } *)
    
    Module Impl_core_marker_StructuralPartialEq_for_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_task_wake_RawWakerVTable.
    
    Module Impl_core_cmp_PartialEq_for_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::RawWakerVTable",
                        "clone"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "core::task::wake::RawWakerVTable",
                        "clone"
                      |)
                    |)
                  |),
                  ltac:(M.monadic
                    (BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::task::wake::RawWakerVTable",
                          "wake"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "core::task::wake::RawWakerVTable",
                          "wake"
                        |)
                      |)
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::RawWakerVTable",
                        "wake_by_ref"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "core::task::wake::RawWakerVTable",
                        "wake_by_ref"
                      |)
                    |)
                  |)))
              |),
              ltac:(M.monadic
                (BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::RawWakerVTable",
                      "drop"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::task::wake::RawWakerVTable",
                      "drop"
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_task_wake_RawWakerVTable.
    
    Module Impl_core_marker_Copy_for_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_task_wake_RawWakerVTable.
    
    Module Impl_core_clone_Clone_for_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                Value.DeclaredButUndefined,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        Value.DeclaredButUndefined,
                                        [ fun γ => ltac:(M.monadic (M.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_task_wake_RawWakerVTable.
    
    Module Impl_core_fmt_Debug_for_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field4_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "RawWakerVTable" |);
                M.read (| Value.String "clone" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::RawWakerVTable",
                  "clone"
                |);
                M.read (| Value.String "wake" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::RawWakerVTable",
                  "wake"
                |);
                M.read (| Value.String "wake_by_ref" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::RawWakerVTable",
                  "wake_by_ref"
                |);
                M.read (| Value.String "drop" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::task::wake::RawWakerVTable",
                    "drop"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_RawWakerVTable.
    
    Module Impl_core_task_wake_RawWakerVTable.
      Definition Self : Ty.t := Ty.path "core::task::wake::RawWakerVTable".
      
      (*
          pub const fn new(
              clone: unsafe fn( *const ()) -> RawWaker,
              wake: unsafe fn( *const ()),
              wake_by_ref: unsafe fn( *const ()),
              drop: unsafe fn( *const ()),
          ) -> Self {
              Self { clone, wake, wake_by_ref, drop }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ clone; wake; wake_by_ref; drop ] =>
          ltac:(M.monadic
            (let clone := M.alloc (| clone |) in
            let wake := M.alloc (| wake |) in
            let wake_by_ref := M.alloc (| wake_by_ref |) in
            let drop := M.alloc (| drop |) in
            Value.StructRecord
              "core::task::wake::RawWakerVTable"
              [
                ("clone", M.read (| clone |));
                ("wake", M.read (| wake |));
                ("wake_by_ref", M.read (| wake_by_ref |));
                ("drop", M.read (| drop |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    End Impl_core_task_wake_RawWakerVTable.
    
    (*
    Enum ExtData
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Some";
            item :=
              StructTuple
                [ Ty.apply (Ty.path "&mut") [] [ Ty.dyn [ ("core::any::Any::Trait", []) ] ] ];
            discriminant := None;
          };
          {
            name := "None";
            item := StructTuple [ Ty.tuple [] ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_core_task_wake_ExtData.
      Definition Self : Ty.t := Ty.path "core::task::wake::ExtData".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::task::wake::ExtData::Some",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "Some" |); __self_0 ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::task::wake::ExtData::None",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "None" |); __self_0 ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_ExtData.
    
    (* StructRecord
      {
        name := "Context";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("waker", Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::Waker" ]);
            ("local_waker", Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::LocalWaker" ]);
            ("ext",
              Ty.apply
                (Ty.path "core::panic::unwind_safe::AssertUnwindSafe")
                []
                [ Ty.path "core::task::wake::ExtData" ]);
            ("_marker",
              Ty.apply
                (Ty.path "core::marker::PhantomData")
                []
                [
                  Ty.function
                    [ Ty.apply (Ty.path "&") [] [ Ty.tuple [] ] ]
                    (Ty.apply (Ty.path "&") [] [ Ty.tuple [] ])
                ]);
            ("_marker2",
              Ty.apply
                (Ty.path "core::marker::PhantomData")
                []
                [ Ty.apply (Ty.path "*mut") [] [ Ty.tuple [] ] ])
          ];
      } *)
    
    Module Impl_core_task_wake_Context.
      Definition Self : Ty.t := Ty.path "core::task::wake::Context".
      
      (*
          pub const fn from_waker(waker: &'a Waker) -> Self {
              ContextBuilder::from_waker(waker).build()
          }
      *)
      Definition from_waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ waker ] =>
          ltac:(M.monadic
            (let waker := M.alloc (| waker |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::task::wake::ContextBuilder",
                "build",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::task::wake::ContextBuilder",
                    "from_waker",
                    []
                  |),
                  [ M.read (| waker |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_waker : M.IsAssociatedFunction Self "from_waker" from_waker.
      
      (*
          pub const fn waker(&self) -> &'a Waker {
              &self.waker
          }
      *)
      Definition waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::task::wake::Context",
                "waker"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_waker : M.IsAssociatedFunction Self "waker" waker.
      
      (*
          pub const fn local_waker(&self) -> &'a LocalWaker {
              &self.local_waker
          }
      *)
      Definition local_waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::task::wake::Context",
                "local_waker"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_local_waker : M.IsAssociatedFunction Self "local_waker" local_waker.
      
      (*
          pub const fn ext(&mut self) -> &mut dyn Any {
              // FIXME: this field makes Context extra-weird about unwind safety
              // can we justify AssertUnwindSafe if we stabilize this? do we care?
              match &mut self.ext.0 {
                  ExtData::Some(data) => *data,
                  ExtData::None(unit) => unit,
              }
          }
      *)
      Definition ext (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::Context",
                      "ext"
                    |),
                    "core::panic::unwind_safe::AssertUnwindSafe",
                    0
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::task::wake::ExtData::Some",
                          0
                        |) in
                      let data := M.alloc (| γ1_0 |) in
                      M.alloc (| M.read (| M.read (| data |) |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::task::wake::ExtData::None",
                          0
                        |) in
                      let unit_ := M.alloc (| γ1_0 |) in
                      M.alloc (| M.read (| unit_ |) |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_ext : M.IsAssociatedFunction Self "ext" ext.
    End Impl_core_task_wake_Context.
    
    Module Impl_core_fmt_Debug_for_core_task_wake_Context.
      Definition Self : Ty.t := Ty.path "core::task::wake::Context".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("Context").field("waker", &self.waker).finish()
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::builders::DebugStruct",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "field",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_struct",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Context" |) ]
                      |)
                    |);
                    M.read (| Value.String "waker" |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::Context",
                      "waker"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_Context.
    
    (* StructRecord
      {
        name := "ContextBuilder";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("waker", Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::Waker" ]);
            ("local_waker", Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::LocalWaker" ]);
            ("ext", Ty.path "core::task::wake::ExtData");
            ("_marker",
              Ty.apply
                (Ty.path "core::marker::PhantomData")
                []
                [
                  Ty.function
                    [ Ty.apply (Ty.path "&") [] [ Ty.tuple [] ] ]
                    (Ty.apply (Ty.path "&") [] [ Ty.tuple [] ])
                ]);
            ("_marker2",
              Ty.apply
                (Ty.path "core::marker::PhantomData")
                []
                [ Ty.apply (Ty.path "*mut") [] [ Ty.tuple [] ] ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_task_wake_ContextBuilder.
      Definition Self : Ty.t := Ty.path "core::task::wake::ContextBuilder".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field5_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "ContextBuilder" |);
                M.read (| Value.String "waker" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::ContextBuilder",
                  "waker"
                |);
                M.read (| Value.String "local_waker" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::ContextBuilder",
                  "local_waker"
                |);
                M.read (| Value.String "ext" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::ContextBuilder",
                  "ext"
                |);
                M.read (| Value.String "_marker" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::ContextBuilder",
                  "_marker"
                |);
                M.read (| Value.String "_marker2" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::task::wake::ContextBuilder",
                    "_marker2"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_ContextBuilder.
    
    Module Impl_core_task_wake_ContextBuilder.
      Definition Self : Ty.t := Ty.path "core::task::wake::ContextBuilder".
      
      (*
          pub const fn from_waker(waker: &'a Waker) -> Self {
              // SAFETY: LocalWaker is just Waker without thread safety
              let local_waker = unsafe { transmute(waker) };
              Self {
                  waker: waker,
                  local_waker,
                  ext: ExtData::None(()),
                  _marker: PhantomData,
                  _marker2: PhantomData,
              }
          }
      *)
      Definition from_waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ waker ] =>
          ltac:(M.monadic
            (let waker := M.alloc (| waker |) in
            M.read (|
              let~ local_waker :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute",
                      [
                        Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::Waker" ];
                        Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::LocalWaker" ]
                      ]
                    |),
                    [ M.read (| waker |) ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::task::wake::ContextBuilder"
                  [
                    ("waker", M.read (| waker |));
                    ("local_waker", M.read (| local_waker |));
                    ("ext", Value.StructTuple "core::task::wake::ExtData::None" [ Value.Tuple [] ]);
                    ("_marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("_marker2", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_waker : M.IsAssociatedFunction Self "from_waker" from_waker.
      
      (*
          pub const fn from(cx: &'a mut Context<'_>) -> Self {
              let ext = match &mut cx.ext.0 {
                  ExtData::Some(ext) => ExtData::Some( *ext),
                  ExtData::None(()) => ExtData::None(()),
              };
              Self {
                  waker: cx.waker,
                  local_waker: cx.local_waker,
                  ext,
                  _marker: PhantomData,
                  _marker2: PhantomData,
              }
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ cx ] =>
          ltac:(M.monadic
            (let cx := M.alloc (| cx |) in
            M.read (|
              let~ ext :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (|
                      M.SubPointer.get_struct_tuple_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| cx |),
                          "core::task::wake::Context",
                          "ext"
                        |),
                        "core::panic::unwind_safe::AssertUnwindSafe",
                        0
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::task::wake::ExtData::Some",
                              0
                            |) in
                          let ext := M.alloc (| γ1_0 |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::task::wake::ExtData::Some"
                              [ M.read (| M.read (| ext |) |) ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let γ1_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::task::wake::ExtData::None",
                              0
                            |) in
                          M.alloc (|
                            Value.StructTuple "core::task::wake::ExtData::None" [ Value.Tuple [] ]
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::task::wake::ContextBuilder"
                  [
                    ("waker",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| cx |),
                          "core::task::wake::Context",
                          "waker"
                        |)
                      |));
                    ("local_waker",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| cx |),
                          "core::task::wake::Context",
                          "local_waker"
                        |)
                      |));
                    ("ext", M.read (| ext |));
                    ("_marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("_marker2", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from : M.IsAssociatedFunction Self "from" from.
      
      (*
          pub const fn waker(self, waker: &'a Waker) -> Self {
              Self { waker, ..self }
          }
      *)
      Definition waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; waker ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let waker := M.alloc (| waker |) in
            M.struct_record_update (M.read (| self |)) [ ("waker", M.read (| waker |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_waker : M.IsAssociatedFunction Self "waker" waker.
      
      (*
          pub const fn local_waker(self, local_waker: &'a LocalWaker) -> Self {
              Self { local_waker, ..self }
          }
      *)
      Definition local_waker (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; local_waker ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let local_waker := M.alloc (| local_waker |) in
            M.struct_record_update
              (M.read (| self |))
              [ ("local_waker", M.read (| local_waker |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_local_waker : M.IsAssociatedFunction Self "local_waker" local_waker.
      
      (*
          pub const fn ext(self, data: &'a mut dyn Any) -> Self {
              Self { ext: ExtData::Some(data), ..self }
          }
      *)
      Definition ext (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; data ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let data := M.alloc (| data |) in
            M.struct_record_update
              (M.read (| self |))
              [ ("ext", Value.StructTuple "core::task::wake::ExtData::Some" [ M.read (| data |) ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_ext : M.IsAssociatedFunction Self "ext" ext.
      
      (*
          pub const fn build(self) -> Context<'a> {
              let ContextBuilder { waker, local_waker, ext, _marker, _marker2 } = self;
              Context { waker, local_waker, ext: AssertUnwindSafe(ext), _marker, _marker2 }
          }
      *)
      Definition build (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::ContextBuilder",
                          "waker"
                        |) in
                      let γ0_1 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::ContextBuilder",
                          "local_waker"
                        |) in
                      let γ0_2 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::ContextBuilder",
                          "ext"
                        |) in
                      let γ0_3 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::ContextBuilder",
                          "_marker"
                        |) in
                      let γ0_4 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::ContextBuilder",
                          "_marker2"
                        |) in
                      let waker := M.copy (| γ0_0 |) in
                      let local_waker := M.copy (| γ0_1 |) in
                      let ext := M.copy (| γ0_2 |) in
                      let _marker := M.copy (| γ0_3 |) in
                      let _marker2 := M.copy (| γ0_4 |) in
                      M.alloc (|
                        Value.StructRecord
                          "core::task::wake::Context"
                          [
                            ("waker", M.read (| waker |));
                            ("local_waker", M.read (| local_waker |));
                            ("ext",
                              Value.StructTuple
                                "core::panic::unwind_safe::AssertUnwindSafe"
                                [ M.read (| ext |) ]);
                            ("_marker", M.read (| _marker |));
                            ("_marker2", M.read (| _marker2 |))
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_build : M.IsAssociatedFunction Self "build" build.
    End Impl_core_task_wake_ContextBuilder.
    
    (* StructRecord
      {
        name := "Waker";
        const_params := [];
        ty_params := [];
        fields := [ ("waker", Ty.path "core::task::wake::RawWaker") ];
      } *)
    
    Module Impl_core_marker_Unpin_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Unpin"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Unpin_for_core_task_wake_Waker.
    
    Module Impl_core_marker_Send_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Send"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_for_core_task_wake_Waker.
    
    Module Impl_core_marker_Sync_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Sync"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_for_core_task_wake_Waker.
    
    Module Impl_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      (*
          pub fn wake(self) {
              // The actual wakeup call is delegated through a virtual function call
              // to the implementation which is defined by the executor.
      
              // Don't call `drop` -- the waker will be consumed by `wake`.
              let this = ManuallyDrop::new(self);
      
              // SAFETY: This is safe because `Waker::from_raw` is the only way
              // to initialize `wake` and `data` requiring the user to acknowledge
              // that the contract of `RawWaker` is upheld.
              unsafe { (this.waker.vtable.wake)(this.waker.data) };
          }
      *)
      Definition wake (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ this :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::manually_drop::ManuallyDrop")
                        []
                        [ Ty.path "core::task::wake::Waker" ],
                      "new",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply
                                    (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                    []
                                    [ Ty.path "core::task::wake::Waker" ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ this ]
                              |),
                              "core::task::wake::Waker",
                              "waker"
                            |),
                            "core::task::wake::RawWaker",
                            "vtable"
                          |)
                        |),
                        "core::task::wake::RawWakerVTable",
                        "wake"
                      |)
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                  []
                                  [ Ty.path "core::task::wake::Waker" ],
                                [],
                                "deref",
                                []
                              |),
                              [ this ]
                            |),
                            "core::task::wake::Waker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "data"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wake : M.IsAssociatedFunction Self "wake" wake.
      
      (*
          pub fn wake_by_ref(&self) {
              // The actual wakeup call is delegated through a virtual function call
              // to the implementation which is defined by the executor.
      
              // SAFETY: see `wake`
              unsafe { (self.waker.vtable.wake_by_ref)(self.waker.data) }
          }
      *)
      Definition wake_by_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::Waker",
                        "waker"
                      |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |)
                  |),
                  "core::task::wake::RawWakerVTable",
                  "wake_by_ref"
                |)
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::Waker",
                      "waker"
                    |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wake_by_ref : M.IsAssociatedFunction Self "wake_by_ref" wake_by_ref.
      
      (*
          pub fn will_wake(&self, other: &Waker) -> bool {
              // We optimize this by comparing vtable addresses instead of vtable contents.
              // This is permitted since the function is documented as best-effort.
              let RawWaker { data: a_data, vtable: a_vtable } = self.waker;
              let RawWaker { data: b_data, vtable: b_vtable } = other.waker;
              a_data == b_data && ptr::eq(a_vtable, b_vtable)
          }
      *)
      Definition will_wake (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::Waker",
                  "waker"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::RawWaker",
                          "data"
                        |) in
                      let γ0_1 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::RawWaker",
                          "vtable"
                        |) in
                      let a_data := M.copy (| γ0_0 |) in
                      let a_vtable := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "core::task::wake::Waker",
                          "waker"
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_record_field (|
                                  γ,
                                  "core::task::wake::RawWaker",
                                  "data"
                                |) in
                              let γ0_1 :=
                                M.SubPointer.get_struct_record_field (|
                                  γ,
                                  "core::task::wake::RawWaker",
                                  "vtable"
                                |) in
                              let b_data := M.copy (| γ0_0 |) in
                              let b_vtable := M.copy (| γ0_1 |) in
                              M.alloc (|
                                LogicalOp.and (|
                                  BinOp.eq (| M.read (| a_data |), M.read (| b_data |) |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_function (|
                                        "core::ptr::eq",
                                        [ Ty.path "core::task::wake::RawWakerVTable" ]
                                      |),
                                      [ M.read (| a_vtable |); M.read (| b_vtable |) ]
                                    |)))
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_will_wake : M.IsAssociatedFunction Self "will_wake" will_wake.
      
      (*
          pub const unsafe fn new(data: *const (), vtable: &'static RawWakerVTable) -> Self {
              Waker { waker: RawWaker { data, vtable } }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ data; vtable ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let vtable := M.alloc (| vtable |) in
            Value.StructRecord
              "core::task::wake::Waker"
              [
                ("waker",
                  Value.StructRecord
                    "core::task::wake::RawWaker"
                    [ ("data", M.read (| data |)); ("vtable", M.read (| vtable |)) ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub const unsafe fn from_raw(waker: RawWaker) -> Waker {
              Waker { waker }
          }
      *)
      Definition from_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ waker ] =>
          ltac:(M.monadic
            (let waker := M.alloc (| waker |) in
            Value.StructRecord "core::task::wake::Waker" [ ("waker", M.read (| waker |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_raw : M.IsAssociatedFunction Self "from_raw" from_raw.
      
      (*
          pub const fn noop() -> &'static Waker {
              const WAKER: &Waker = &Waker { waker: RawWaker::NOOP };
              WAKER
          }
      *)
      Definition noop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic (M.read (| M.get_constant (| "core::task::wake::noop::WAKER" |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_noop : M.IsAssociatedFunction Self "noop" noop.
      
      (*
          pub fn data(&self) -> *const () {
              self.waker.data
          }
      *)
      Definition data (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::Waker",
                  "waker"
                |),
                "core::task::wake::RawWaker",
                "data"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data : M.IsAssociatedFunction Self "data" data.
      
      (*
          pub fn vtable(&self) -> &'static RawWakerVTable {
              self.waker.vtable
          }
      *)
      Definition vtable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::Waker",
                  "waker"
                |),
                "core::task::wake::RawWaker",
                "vtable"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_vtable : M.IsAssociatedFunction Self "vtable" vtable.
    End Impl_core_task_wake_Waker.
    
    Module Impl_core_clone_Clone_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      (*
          fn clone(&self) -> Self {
              Waker {
                  // SAFETY: This is safe because `Waker::from_raw` is the only way
                  // to initialize `clone` and `data` requiring the user to acknowledge
                  // that the contract of [`RawWaker`] is upheld.
                  waker: unsafe { (self.waker.vtable.clone)(self.waker.data) },
              }
          }
      *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::task::wake::Waker"
              [
                ("waker",
                  M.call_closure (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::task::wake::Waker",
                              "waker"
                            |),
                            "core::task::wake::RawWaker",
                            "vtable"
                          |)
                        |),
                        "core::task::wake::RawWakerVTable",
                        "clone"
                      |)
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::task::wake::Waker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "data"
                        |)
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn clone_from(&mut self, source: &Self) {
              if !self.will_wake(source) {
                  *self = source.clone();
              }
          }
      *)
      Definition clone_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; source ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let source := M.alloc (| source |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::task::wake::Waker",
                                  "will_wake",
                                  []
                                |),
                                [ M.read (| self |); M.read (| source |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.write (|
                          M.read (| self |),
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "core::task::wake::Waker",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| source |) ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("clone", InstanceField.Method clone); ("clone_from", InstanceField.Method clone_from)
          ].
    End Impl_core_clone_Clone_for_core_task_wake_Waker.
    
    Module Impl_core_ops_drop_Drop_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      (*
          fn drop(&mut self) {
              // SAFETY: This is safe because `Waker::from_raw` is the only way
              // to initialize `drop` and `data` requiring the user to acknowledge
              // that the contract of `RawWaker` is upheld.
              unsafe { (self.waker.vtable.drop)(self.waker.data) }
          }
      *)
      Definition drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::Waker",
                        "waker"
                      |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |)
                  |),
                  "core::task::wake::RawWakerVTable",
                  "drop"
                |)
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::Waker",
                      "waker"
                    |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::drop::Drop"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method drop) ].
    End Impl_core_ops_drop_Drop_for_core_task_wake_Waker.
    
    Module Impl_core_fmt_Debug_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              let vtable_ptr = self.waker.vtable as *const RawWakerVTable;
              f.debug_struct("Waker")
                  .field("data", &self.waker.data)
                  .field("vtable", &vtable_ptr)
                  .finish()
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ vtable_ptr :=
                M.copy (|
                  M.use
                    (M.alloc (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::task::wake::Waker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "vtable"
                        |)
                      |)
                    |))
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "finish",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::builders::DebugStruct",
                            "field",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Formatter",
                                  "debug_struct",
                                  []
                                |),
                                [ M.read (| f |); M.read (| Value.String "Waker" |) ]
                              |)
                            |);
                            M.read (| Value.String "data" |);
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::task::wake::Waker",
                                "waker"
                              |),
                              "core::task::wake::RawWaker",
                              "data"
                            |)
                          ]
                        |);
                        M.read (| Value.String "vtable" |);
                        vtable_ptr
                      ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_Waker.
    
    (* StructRecord
      {
        name := "LocalWaker";
        const_params := [];
        ty_params := [];
        fields := [ ("waker", Ty.path "core::task::wake::RawWaker") ];
      } *)
    
    Module Impl_core_marker_Unpin_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Unpin"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Unpin_for_core_task_wake_LocalWaker.
    
    Module Impl_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      (*
          pub fn wake(self) {
              // The actual wakeup call is delegated through a virtual function call
              // to the implementation which is defined by the executor.
      
              // Don't call `drop` -- the waker will be consumed by `wake`.
              let this = ManuallyDrop::new(self);
      
              // SAFETY: This is safe because `Waker::from_raw` is the only way
              // to initialize `wake` and `data` requiring the user to acknowledge
              // that the contract of `RawWaker` is upheld.
              unsafe { (this.waker.vtable.wake)(this.waker.data) };
          }
      *)
      Definition wake (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ this :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::manually_drop::ManuallyDrop")
                        []
                        [ Ty.path "core::task::wake::LocalWaker" ],
                      "new",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply
                                    (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                    []
                                    [ Ty.path "core::task::wake::LocalWaker" ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ this ]
                              |),
                              "core::task::wake::LocalWaker",
                              "waker"
                            |),
                            "core::task::wake::RawWaker",
                            "vtable"
                          |)
                        |),
                        "core::task::wake::RawWakerVTable",
                        "wake"
                      |)
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                  []
                                  [ Ty.path "core::task::wake::LocalWaker" ],
                                [],
                                "deref",
                                []
                              |),
                              [ this ]
                            |),
                            "core::task::wake::LocalWaker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "data"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wake : M.IsAssociatedFunction Self "wake" wake.
      
      (*
          pub fn wake_by_ref(&self) {
              // The actual wakeup call is delegated through a virtual function call
              // to the implementation which is defined by the executor.
      
              // SAFETY: see `wake`
              unsafe { (self.waker.vtable.wake_by_ref)(self.waker.data) }
          }
      *)
      Definition wake_by_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::LocalWaker",
                        "waker"
                      |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |)
                  |),
                  "core::task::wake::RawWakerVTable",
                  "wake_by_ref"
                |)
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::LocalWaker",
                      "waker"
                    |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wake_by_ref : M.IsAssociatedFunction Self "wake_by_ref" wake_by_ref.
      
      (*
          pub fn will_wake(&self, other: &LocalWaker) -> bool {
              // We optimize this by comparing vtable addresses instead of vtable contents.
              // This is permitted since the function is documented as best-effort.
              let RawWaker { data: a_data, vtable: a_vtable } = self.waker;
              let RawWaker { data: b_data, vtable: b_vtable } = other.waker;
              a_data == b_data && ptr::eq(a_vtable, b_vtable)
          }
      *)
      Definition will_wake (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::LocalWaker",
                  "waker"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::RawWaker",
                          "data"
                        |) in
                      let γ0_1 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::task::wake::RawWaker",
                          "vtable"
                        |) in
                      let a_data := M.copy (| γ0_0 |) in
                      let a_vtable := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "core::task::wake::LocalWaker",
                          "waker"
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_record_field (|
                                  γ,
                                  "core::task::wake::RawWaker",
                                  "data"
                                |) in
                              let γ0_1 :=
                                M.SubPointer.get_struct_record_field (|
                                  γ,
                                  "core::task::wake::RawWaker",
                                  "vtable"
                                |) in
                              let b_data := M.copy (| γ0_0 |) in
                              let b_vtable := M.copy (| γ0_1 |) in
                              M.alloc (|
                                LogicalOp.and (|
                                  BinOp.eq (| M.read (| a_data |), M.read (| b_data |) |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_function (|
                                        "core::ptr::eq",
                                        [ Ty.path "core::task::wake::RawWakerVTable" ]
                                      |),
                                      [ M.read (| a_vtable |); M.read (| b_vtable |) ]
                                    |)))
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_will_wake : M.IsAssociatedFunction Self "will_wake" will_wake.
      
      (*
          pub const unsafe fn new(data: *const (), vtable: &'static RawWakerVTable) -> Self {
              LocalWaker { waker: RawWaker { data, vtable } }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ data; vtable ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let vtable := M.alloc (| vtable |) in
            Value.StructRecord
              "core::task::wake::LocalWaker"
              [
                ("waker",
                  Value.StructRecord
                    "core::task::wake::RawWaker"
                    [ ("data", M.read (| data |)); ("vtable", M.read (| vtable |)) ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub const unsafe fn from_raw(waker: RawWaker) -> LocalWaker {
              Self { waker }
          }
      *)
      Definition from_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ waker ] =>
          ltac:(M.monadic
            (let waker := M.alloc (| waker |) in
            Value.StructRecord "core::task::wake::LocalWaker" [ ("waker", M.read (| waker |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_raw : M.IsAssociatedFunction Self "from_raw" from_raw.
      
      (*
          pub const fn noop() -> &'static LocalWaker {
              const WAKER: &LocalWaker = &LocalWaker { waker: RawWaker::NOOP };
              WAKER
          }
      *)
      Definition noop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic (M.read (| M.get_constant (| "core::task::wake::noop::WAKER" |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_noop : M.IsAssociatedFunction Self "noop" noop.
      
      (*
          pub fn data(&self) -> *const () {
              self.waker.data
          }
      *)
      Definition data (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::LocalWaker",
                  "waker"
                |),
                "core::task::wake::RawWaker",
                "data"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data : M.IsAssociatedFunction Self "data" data.
      
      (*
          pub fn vtable(&self) -> &'static RawWakerVTable {
              self.waker.vtable
          }
      *)
      Definition vtable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::task::wake::LocalWaker",
                  "waker"
                |),
                "core::task::wake::RawWaker",
                "vtable"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_vtable : M.IsAssociatedFunction Self "vtable" vtable.
    End Impl_core_task_wake_LocalWaker.
    
    Module Impl_core_clone_Clone_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      (*
          fn clone(&self) -> Self {
              LocalWaker {
                  // SAFETY: This is safe because `Waker::from_raw` is the only way
                  // to initialize `clone` and `data` requiring the user to acknowledge
                  // that the contract of [`RawWaker`] is upheld.
                  waker: unsafe { (self.waker.vtable.clone)(self.waker.data) },
              }
          }
      *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::task::wake::LocalWaker"
              [
                ("waker",
                  M.call_closure (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::task::wake::LocalWaker",
                              "waker"
                            |),
                            "core::task::wake::RawWaker",
                            "vtable"
                          |)
                        |),
                        "core::task::wake::RawWakerVTable",
                        "clone"
                      |)
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::task::wake::LocalWaker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "data"
                        |)
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn clone_from(&mut self, source: &Self) {
              if !self.will_wake(source) {
                  *self = source.clone();
              }
          }
      *)
      Definition clone_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; source ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let source := M.alloc (| source |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::task::wake::LocalWaker",
                                  "will_wake",
                                  []
                                |),
                                [ M.read (| self |); M.read (| source |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.write (|
                          M.read (| self |),
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "core::task::wake::LocalWaker",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| source |) ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("clone", InstanceField.Method clone); ("clone_from", InstanceField.Method clone_from)
          ].
    End Impl_core_clone_Clone_for_core_task_wake_LocalWaker.
    
    Module Impl_core_convert_AsRef_core_task_wake_LocalWaker_for_core_task_wake_Waker.
      Definition Self : Ty.t := Ty.path "core::task::wake::Waker".
      
      (*
          fn as_ref(&self) -> &LocalWaker {
              // SAFETY: LocalWaker is just Waker without thread safety
              unsafe { transmute(self) }
          }
      *)
      Definition as_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::transmute",
                [
                  Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::Waker" ];
                  Ty.apply (Ty.path "&") [] [ Ty.path "core::task::wake::LocalWaker" ]
                ]
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsRef"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::task::wake::LocalWaker" ]
          (* Instance *) [ ("as_ref", InstanceField.Method as_ref) ].
    End Impl_core_convert_AsRef_core_task_wake_LocalWaker_for_core_task_wake_Waker.
    
    Module Impl_core_ops_drop_Drop_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      (*
          fn drop(&mut self) {
              // SAFETY: This is safe because `LocalWaker::from_raw` is the only way
              // to initialize `drop` and `data` requiring the user to acknowledge
              // that the contract of `RawWaker` is upheld.
              unsafe { (self.waker.vtable.drop)(self.waker.data) }
          }
      *)
      Definition drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::task::wake::LocalWaker",
                        "waker"
                      |),
                      "core::task::wake::RawWaker",
                      "vtable"
                    |)
                  |),
                  "core::task::wake::RawWakerVTable",
                  "drop"
                |)
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::task::wake::LocalWaker",
                      "waker"
                    |),
                    "core::task::wake::RawWaker",
                    "data"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::drop::Drop"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method drop) ].
    End Impl_core_ops_drop_Drop_for_core_task_wake_LocalWaker.
    
    Module Impl_core_fmt_Debug_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              let vtable_ptr = self.waker.vtable as *const RawWakerVTable;
              f.debug_struct("LocalWaker")
                  .field("data", &self.waker.data)
                  .field("vtable", &vtable_ptr)
                  .finish()
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ vtable_ptr :=
                M.copy (|
                  M.use
                    (M.alloc (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::task::wake::LocalWaker",
                            "waker"
                          |),
                          "core::task::wake::RawWaker",
                          "vtable"
                        |)
                      |)
                    |))
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "finish",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::builders::DebugStruct",
                            "field",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Formatter",
                                  "debug_struct",
                                  []
                                |),
                                [ M.read (| f |); M.read (| Value.String "LocalWaker" |) ]
                              |)
                            |);
                            M.read (| Value.String "data" |);
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::task::wake::LocalWaker",
                                "waker"
                              |),
                              "core::task::wake::RawWaker",
                              "data"
                            |)
                          ]
                        |);
                        M.read (| Value.String "vtable" |);
                        vtable_ptr
                      ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_task_wake_LocalWaker.
    
    Module Impl_core_marker_Send_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Send"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_for_core_task_wake_LocalWaker.
    
    Module Impl_core_marker_Sync_for_core_task_wake_LocalWaker.
      Definition Self : Ty.t := Ty.path "core::task::wake::LocalWaker".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Sync"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_for_core_task_wake_LocalWaker.
  End wake.
End task.
