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

Module ptr.
  Module non_null.
    (* StructRecord
      {
        name := "NonNull";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ ("pointer", Ty.apply (Ty.path "*const") [] [ T ]) ];
      } *)
    
    Module Impl_core_marker_Send_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Send"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Sync"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          pub const fn dangling() -> Self {
              // SAFETY: mem::align_of() returns a non-zero usize which is then casted
              // to a *mut T. Therefore, `ptr` is not null and the conditions for
              // calling new_unchecked() are respected.
              unsafe {
                  let ptr = crate::ptr::dangling_mut::<T>();
                  NonNull::new_unchecked(ptr)
              }
          }
      *)
      Definition dangling (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.read (|
              let~ ptr :=
                M.alloc (|
                  M.call_closure (| M.get_function (| "core::ptr::dangling_mut", [ T ] |), [] |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "new_unchecked",
                    []
                  |),
                  [ M.read (| ptr |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_dangling :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "dangling" (dangling T).
      
      (*
          pub const unsafe fn as_uninit_ref<'a>(self) -> &'a MaybeUninit<T> {
              // SAFETY: the caller must guarantee that `self` meets all the
              // requirements for a reference.
              unsafe { &*self.cast().as_ptr() }
          }
      *)
      Definition as_uninit_ref
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                "as_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "cast",
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_uninit_ref :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_uninit_ref" (as_uninit_ref T).
      
      (*
          pub const unsafe fn as_uninit_mut<'a>(self) -> &'a mut MaybeUninit<T> {
              // SAFETY: the caller must guarantee that `self` meets all the
              // requirements for a reference.
              unsafe { &mut *self.cast().as_ptr() }
          }
      *)
      Definition as_uninit_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                "as_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "cast",
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_uninit_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_uninit_mut" (as_uninit_mut T).
      (*
          pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
              // SAFETY: the caller must guarantee that `ptr` is non-null.
              unsafe {
                  assert_unsafe_precondition!(
                      check_language_ub,
                      "NonNull::new_unchecked requires that the pointer is non-null",
                      (ptr: *mut () = ptr as *mut ()) => !ptr.is_null()
                  );
                  NonNull { pointer: ptr as _ }
              }
          }
      *)
      Definition new_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ ptr ] =>
          ltac:(M.monadic
            (let ptr := M.alloc (| ptr |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::ub_checks::check_language_ub", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.new_unchecked",
                                []
                              |),
                              [ M.rust_cast (M.read (| ptr |)) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::ptr::non_null::NonNull"
                  [
                    ("pointer",
                      M.rust_cast (* MutToConstPointer *) (M.pointer_coercion (M.read (| ptr |))))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_unchecked :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new_unchecked" (new_unchecked T).
      
      (*
          pub const fn new(ptr: *mut T) -> Option<Self> {
              if !ptr.is_null() {
                  // SAFETY: The pointer is already checked and is not null
                  Some(unsafe { Self::new_unchecked(ptr) })
              } else {
                  None
              }
          }
      *)
      Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ ptr ] =>
          ltac:(M.monadic
            (let ptr := M.alloc (| ptr |) 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.apply (Ty.path "*mut") [] [ T ],
                                  "is_null",
                                  []
                                |),
                                [ M.read (| ptr |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "new_unchecked",
                                []
                              |),
                              [ M.read (| ptr |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new" (new T).
      
      (*
          pub const fn from_raw_parts(
              data_pointer: NonNull<()>,
              metadata: <T as super::Pointee>::Metadata,
          ) -> NonNull<T> {
              // SAFETY: The result of `ptr::from::raw_parts_mut` is non-null because `data_pointer` is.
              unsafe {
                  NonNull::new_unchecked(super::from_raw_parts_mut(data_pointer.as_ptr(), metadata))
              }
          }
      *)
      Definition from_raw_parts
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ data_pointer; metadata ] =>
          ltac:(M.monadic
            (let data_pointer := M.alloc (| data_pointer |) in
            let metadata := M.alloc (| metadata |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "core::ptr::metadata::from_raw_parts_mut",
                    [ T; Ty.tuple [] ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.tuple [] ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| data_pointer |) ]
                    |);
                    M.read (| metadata |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_raw_parts :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "from_raw_parts" (from_raw_parts T).
      
      (*
          pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata) {
              (self.cast(), super::metadata(self.as_ptr()))
          }
      *)
      Definition to_raw_parts
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "cast",
                    [ Ty.tuple [] ]
                  |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_function (| "core::ptr::metadata::metadata", [ T ] |),
                  [
                    (* MutToConstPointer *)
                    M.pointer_coercion
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| self |) ]
                      |))
                  ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_raw_parts :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "to_raw_parts" (to_raw_parts T).
      
      (*
          pub fn addr(self) -> NonZero<usize> {
              // SAFETY: The pointer is guaranteed by the type to be non-null,
              // meaning that the address will be non-zero.
              unsafe { NonZero::new_unchecked(self.pointer.addr()) }
          }
      *)
      Definition addr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.apply (Ty.path "*const") [] [ T ], "addr", [] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ptr::non_null::NonNull",
                        "pointer"
                      |)
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_addr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "addr" (addr T).
      
      (*
          pub fn with_addr(self, addr: NonZero<usize>) -> Self {
              // SAFETY: The result of `ptr::from::with_addr` is non-null because `addr` is guaranteed to be non-zero.
              unsafe { NonNull::new_unchecked(self.pointer.with_addr(addr.get()) as *mut _) }
          }
      *)
      Definition with_addr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; addr ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let addr := M.alloc (| addr |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "new_unchecked",
                []
              |),
              [
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ T ],
                      "with_addr",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                          "get",
                          []
                        |),
                        [ M.read (| addr |) ]
                      |)
                    ]
                  |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_with_addr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "with_addr" (with_addr T).
      
      (*
          pub fn map_addr(self, f: impl FnOnce(NonZero<usize>) -> NonZero<usize>) -> Self {
              self.with_addr(f(self.addr()))
          }
      *)
      Definition map_addr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ impl_FnOnce_NonZero_usize___arrow_NonZero_usize_ ], [ 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.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "with_addr",
                []
              |),
              [
                M.read (| self |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    impl_FnOnce_NonZero_usize___arrow_NonZero_usize_,
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                    ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "addr",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_map_addr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "map_addr" (map_addr T).
      
      (*
          pub const fn as_ptr(self) -> *mut T {
              self.pointer as *mut T
          }
      *)
      Definition as_ptr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast
              (M.read (|
                M.SubPointer.get_struct_record_field (|
                  self,
                  "core::ptr::non_null::NonNull",
                  "pointer"
                |)
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_ptr" (as_ptr T).
      
      (*
          pub const unsafe fn as_ref<'a>(&self) -> &'a T {
              // SAFETY: the caller must guarantee that `self` meets all the
              // requirements for a reference.
              // `cast_const` avoids a mutable raw pointer deref.
              unsafe { &*self.as_ptr().cast_const() }
          }
      *)
      Definition as_ref (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "cast_const", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| M.read (| self |) |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ref :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_ref" (as_ref T).
      
      (*
          pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T {
              // SAFETY: the caller must guarantee that `self` meets all the
              // requirements for a mutable reference.
              unsafe { &mut *self.as_ptr() }
          }
      *)
      Definition as_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_ptr",
                []
              |),
              [ M.read (| M.read (| self |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_mut" (as_mut T).
      
      (*
          pub const fn cast<U>(self) -> NonNull<U> {
              // SAFETY: `self` is a `NonNull` pointer which is necessarily non-null
              unsafe { NonNull { pointer: self.as_ptr() as *mut U } }
          }
      *)
      Definition cast (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ U ], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  (* MutToConstPointer *)
                  M.pointer_coercion
                    (M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| self |) ]
                      |))))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_cast :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "cast" (cast T).
      
      (*
          pub const unsafe fn offset(self, count: isize) -> Self
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `offset`.
              // Additionally safety contract of `offset` guarantees that the resulting pointer is
              // pointing to an allocation, there can't be an allocation at null, thus it's safe to
              // construct `NonNull`.
              unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } }
          }
      *)
      Definition offset (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::offset",
                      [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "isize" ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.read (| count |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_offset :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "offset" (offset T).
      
      (*
          pub const unsafe fn byte_offset(self, count: isize) -> Self {
              // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has
              // the same safety contract.
              // Additionally safety contract of `offset` guarantees that the resulting pointer is
              // pointing to an allocation, there can't be an allocation at null, thus it's safe to
              // construct `NonNull`.
              unsafe { NonNull { pointer: self.pointer.byte_offset(count) } }
          }
      *)
      Definition byte_offset (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ T ],
                      "byte_offset",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.read (| count |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_byte_offset :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "byte_offset" (byte_offset T).
      
      (*
          pub const unsafe fn add(self, count: usize) -> Self
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `offset`.
              // Additionally safety contract of `offset` guarantees that the resulting pointer is
              // pointing to an allocation, there can't be an allocation at null, thus it's safe to
              // construct `NonNull`.
              unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } }
          }
      *)
      Definition add (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::offset",
                      [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "usize" ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.read (| count |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_add :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "add" (add T).
      
      (*
          pub const unsafe fn byte_add(self, count: usize) -> Self {
              // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same
              // safety contract.
              // Additionally safety contract of `add` guarantees that the resulting pointer is pointing
              // to an allocation, there can't be an allocation at null, thus it's safe to construct
              // `NonNull`.
              unsafe { NonNull { pointer: self.pointer.byte_add(count) } }
          }
      *)
      Definition byte_add (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ T ],
                      "byte_add",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.read (| count |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_byte_add :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "byte_add" (byte_add T).
      
      (*
          pub const unsafe fn sub(self, count: usize) -> Self
          where
              T: Sized,
          {
              if T::IS_ZST {
                  // Pointer arithmetic does nothing when the pointee is a ZST.
                  self
              } else {
                  // SAFETY: the caller must uphold the safety contract for `offset`.
                  // Because the pointee is *not* a ZST, that means that `count` is
                  // at most `isize::MAX`, and thus the negation cannot overflow.
                  unsafe { self.offset((count as isize).unchecked_neg()) }
              }
          }
      *)
      Definition sub (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      self));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "offset",
                            []
                          |),
                          [
                            M.read (| self |);
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "isize", "unchecked_neg", [] |),
                              [ M.rust_cast (M.read (| count |)) ]
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_sub :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "sub" (sub T).
      
      (*
          pub const unsafe fn byte_sub(self, count: usize) -> Self {
              // SAFETY: the caller must uphold the safety contract for `sub` and `byte_sub` has the same
              // safety contract.
              // Additionally safety contract of `sub` guarantees that the resulting pointer is pointing
              // to an allocation, there can't be an allocation at null, thus it's safe to construct
              // `NonNull`.
              unsafe { NonNull { pointer: self.pointer.byte_sub(count) } }
          }
      *)
      Definition byte_sub (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let count := M.alloc (| count |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ T ],
                      "byte_sub",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ptr::non_null::NonNull",
                          "pointer"
                        |)
                      |);
                      M.read (| count |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_byte_sub :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "byte_sub" (byte_sub T).
      
      (*
          pub const unsafe fn offset_from(self, origin: NonNull<T>) -> isize
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `offset_from`.
              unsafe { self.pointer.offset_from(origin.pointer) }
          }
      *)
      Definition offset_from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; origin ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let origin := M.alloc (| origin |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "offset_from",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    origin,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_offset_from :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "offset_from" (offset_from T).
      
      (*
          pub const unsafe fn byte_offset_from<U: ?Sized>(self, origin: NonNull<U>) -> isize {
              // SAFETY: the caller must uphold the safety contract for `byte_offset_from`.
              unsafe { self.pointer.byte_offset_from(origin.pointer) }
          }
      *)
      Definition byte_offset_from
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ U ], [ self; origin ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let origin := M.alloc (| origin |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "byte_offset_from",
                [ U ]
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    origin,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_byte_offset_from :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "byte_offset_from" (byte_offset_from T).
      
      (*
          pub const unsafe fn sub_ptr(self, subtracted: NonNull<T>) -> usize
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `sub_ptr`.
              unsafe { self.pointer.sub_ptr(subtracted.pointer) }
          }
      *)
      Definition sub_ptr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; subtracted ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let subtracted := M.alloc (| subtracted |) in
            M.call_closure (|
              M.get_associated_function (| Ty.apply (Ty.path "*const") [] [ T ], "sub_ptr", [] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    subtracted,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_sub_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "sub_ptr" (sub_ptr T).
      
      (*
          pub const unsafe fn read(self) -> T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `read`.
              unsafe { ptr::read(self.pointer) }
          }
      *)
      Definition read (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::ptr::read", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "read" (read T).
      
      (*
          pub unsafe fn read_volatile(self) -> T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `read_volatile`.
              unsafe { ptr::read_volatile(self.pointer) }
          }
      *)
      Definition read_volatile
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::ptr::read_volatile", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_volatile :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "read_volatile" (read_volatile T).
      
      (*
          pub const unsafe fn read_unaligned(self) -> T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `read_unaligned`.
              unsafe { ptr::read_unaligned(self.pointer) }
          }
      *)
      Definition read_unaligned
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::ptr::read_unaligned", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_read_unaligned :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "read_unaligned" (read_unaligned T).
      
      (*
          pub const unsafe fn copy_to(self, dest: NonNull<T>, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy`.
              unsafe { ptr::copy(self.pointer, dest.as_ptr(), count) }
          }
      *)
      Definition copy_to (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; dest; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dest := M.alloc (| dest |) in
            let count := M.alloc (| count |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::copy", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| dest |) ]
                |);
                M.read (| count |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_copy_to :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "copy_to" (copy_to T).
      
      (*
          pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull<T>, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy_nonoverlapping`.
              unsafe { ptr::copy_nonoverlapping(self.pointer, dest.as_ptr(), count) }
          }
      *)
      Definition copy_to_nonoverlapping
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; dest; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dest := M.alloc (| dest |) in
            let count := M.alloc (| count |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| dest |) ]
                |);
                M.read (| count |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_copy_to_nonoverlapping :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "copy_to_nonoverlapping" (copy_to_nonoverlapping T).
      
      (*
          pub const unsafe fn copy_from(self, src: NonNull<T>, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy`.
              unsafe { ptr::copy(src.pointer, self.as_ptr(), count) }
          }
      *)
      Definition copy_from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; src; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let src := M.alloc (| src |) in
            let count := M.alloc (| count |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::copy", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    src,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| count |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_copy_from :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "copy_from" (copy_from T).
      
      (*
          pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull<T>, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy_nonoverlapping`.
              unsafe { ptr::copy_nonoverlapping(src.pointer, self.as_ptr(), count) }
          }
      *)
      Definition copy_from_nonoverlapping
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; src; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let src := M.alloc (| src |) in
            let count := M.alloc (| count |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    src,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| count |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_copy_from_nonoverlapping :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "copy_from_nonoverlapping" (copy_from_nonoverlapping T).
      
      (*
          pub unsafe fn drop_in_place(self) {
              // SAFETY: the caller must uphold the safety contract for `drop_in_place`.
              unsafe { ptr::drop_in_place(self.as_ptr()) }
          }
      *)
      Definition drop_in_place
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::ptr::drop_in_place", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_drop_in_place :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "drop_in_place" (drop_in_place T).
      
      (*
          pub const unsafe fn write(self, val: T)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `write`.
              unsafe { ptr::write(self.as_ptr(), val) }
          }
      *)
      Definition write (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; val ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let val := M.alloc (| val |) in
            M.call_closure (|
              M.get_function (| "core::ptr::write", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| val |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_write :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "write" (write T).
      
      (*
          pub const unsafe fn write_bytes(self, val: u8, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `write_bytes`.
              unsafe { ptr::write_bytes(self.as_ptr(), val, count) }
          }
      *)
      Definition write_bytes (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; val; count ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let val := M.alloc (| val |) in
            let count := M.alloc (| count |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::write_bytes", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| val |);
                M.read (| count |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_write_bytes :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "write_bytes" (write_bytes T).
      
      (*
          pub unsafe fn write_volatile(self, val: T)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `write_volatile`.
              unsafe { ptr::write_volatile(self.as_ptr(), val) }
          }
      *)
      Definition write_volatile
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; val ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let val := M.alloc (| val |) in
            M.call_closure (|
              M.get_function (| "core::ptr::write_volatile", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| val |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_write_volatile :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "write_volatile" (write_volatile T).
      
      (*
          pub const unsafe fn write_unaligned(self, val: T)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `write_unaligned`.
              unsafe { ptr::write_unaligned(self.as_ptr(), val) }
          }
      *)
      Definition write_unaligned
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; val ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let val := M.alloc (| val |) in
            M.call_closure (|
              M.get_function (| "core::ptr::write_unaligned", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| val |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_write_unaligned :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "write_unaligned" (write_unaligned T).
      
      (*
          pub unsafe fn replace(self, src: T) -> T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `replace`.
              unsafe { ptr::replace(self.as_ptr(), src) }
          }
      *)
      Definition replace (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; src ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let src := M.alloc (| src |) in
            M.call_closure (|
              M.get_function (| "core::ptr::replace", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| src |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_replace :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "replace" (replace T).
      
      (*
          pub const unsafe fn swap(self, with: NonNull<T>)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `swap`.
              unsafe { ptr::swap(self.as_ptr(), with.as_ptr()) }
          }
      *)
      Definition swap (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; with_ ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let with_ := M.alloc (| with_ |) in
            M.call_closure (|
              M.get_function (| "core::ptr::swap", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| with_ |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_swap :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "swap" (swap T).
      
      (*
          pub const fn align_offset(self, align: usize) -> usize
          where
              T: Sized,
          {
              if !align.is_power_of_two() {
                  panic!("align_offset: align is not a power-of-two");
              }
      
              {
                  // SAFETY: `align` has been checked to be a power of 2 above.
                  unsafe { ptr::align_offset(self.pointer, align) }
              }
          }
      *)
      Definition align_offset
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; align ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let align := M.alloc (| align |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "usize",
                                    "is_power_of_two",
                                    []
                                  |),
                                  [ M.read (| align |) ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic_fmt", [] |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::Arguments",
                                    "new_const",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      Value.Array
                                        [
                                          M.read (|
                                            Value.String "align_offset: align is not a power-of-two"
                                          |)
                                        ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::ptr::align_offset", [ T ] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ptr::non_null::NonNull",
                        "pointer"
                      |)
                    |);
                    M.read (| align |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_align_offset :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "align_offset" (align_offset T).
      
      (*
          pub const fn is_aligned(self) -> bool
          where
              T: Sized,
          {
              self.pointer.is_aligned()
          }
      *)
      Definition is_aligned (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "is_aligned",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_aligned :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "is_aligned" (is_aligned T).
      
      (*
          pub const fn is_aligned_to(self, align: usize) -> bool {
              self.pointer.is_aligned_to(align)
          }
      *)
      Definition is_aligned_to
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; align ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let align := M.alloc (| align |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "is_aligned_to",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ptr::non_null::NonNull",
                    "pointer"
                  |)
                |);
                M.read (| align |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_aligned_to :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "is_aligned_to" (is_aligned_to T).
    End Impl_core_ptr_non_null_NonNull_T.
    
    
    Module Impl_core_ptr_non_null_NonNull_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::ptr::non_null::NonNull")
          []
          [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self {
              // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null
              unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) }
          }
      *)
      Definition slice_from_raw_parts
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ data; len ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let len := M.alloc (| len |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| data |) ]
                    |);
                    M.read (| len |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_from_raw_parts :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_from_raw_parts" (slice_from_raw_parts T).
      
      (*
          pub const fn len(self) -> usize {
              self.as_ptr().len()
          }
      *)
      Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "len",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "len" (len T).
      
      (*
          pub const fn is_empty(self) -> bool {
              self.len() == 0
          }
      *)
      Definition is_empty (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.eq (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::ptr::non_null::NonNull")
                    []
                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                  "len",
                  []
                |),
                [ M.read (| self |) ]
              |),
              Value.Integer IntegerKind.Usize 0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_empty :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "is_empty" (is_empty T).
      
      (*
          pub const fn as_non_null_ptr(self) -> NonNull<T> {
              self.cast()
          }
      *)
      Definition as_non_null_ptr
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "cast",
                [ T ]
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_non_null_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_non_null_ptr" (as_non_null_ptr T).
      
      (*
          pub const fn as_mut_ptr(self) -> *mut T {
              self.as_non_null_ptr().as_ptr()
          }
      *)
      Definition as_mut_ptr (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "as_non_null_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_mut_ptr" (as_mut_ptr T).
      
      (*
          pub const unsafe fn as_uninit_slice<'a>(self) -> &'a [MaybeUninit<T>] {
              // SAFETY: the caller must uphold the safety contract for `as_uninit_slice`.
              unsafe { slice::from_raw_parts(self.cast().as_ptr(), self.len()) }
          }
      *)
      Definition as_uninit_slice
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (|
                "core::slice::raw::from_raw_parts",
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
              |),
              [
                (* MutToConstPointer *)
                M.pointer_coercion
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::ptr::non_null::NonNull")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::ptr::non_null::NonNull")
                            []
                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                          "cast",
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                        |),
                        [ M.read (| self |) ]
                      |)
                    ]
                  |));
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "len",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_uninit_slice :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_uninit_slice" (as_uninit_slice T).
      
      (*
          pub const unsafe fn as_uninit_slice_mut<'a>(self) -> &'a mut [MaybeUninit<T>] {
              // SAFETY: the caller must uphold the safety contract for `as_uninit_slice_mut`.
              unsafe { slice::from_raw_parts_mut(self.cast().as_ptr(), self.len()) }
          }
      *)
      Definition as_uninit_slice_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (|
                "core::slice::raw::from_raw_parts_mut",
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ptr::non_null::NonNull")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        "cast",
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::ptr::non_null::NonNull")
                      []
                      [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "len",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_uninit_slice_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_uninit_slice_mut" (as_uninit_slice_mut T).
      
      (*
          pub unsafe fn get_unchecked_mut<I>(self, index: I) -> NonNull<I::Output>
          where
              I: SliceIndex<[T]>,
          {
              // SAFETY: the caller ensures that `self` is dereferenceable and `index` in-bounds.
              // As a consequence, the resulting pointer cannot be null.
              unsafe { NonNull::new_unchecked(self.as_ptr().get_unchecked_mut(index)) }
          }
      *)
      Definition get_unchecked_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ _ as I ], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.associated ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                    "get_unchecked_mut",
                    [ I ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ptr::non_null::NonNull")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| index |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_unchecked_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_unchecked_mut" (get_unchecked_mut T).
    End Impl_core_ptr_non_null_NonNull_slice_T.
    
    Module Impl_core_clone_Clone_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn clone(&self) -> Self {
              *self
          }
      *)
      Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
    End Impl_core_clone_Clone_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_marker_Copy_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Copy"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Sized_U_where_core_marker_Unsize_T_U_core_ptr_non_null_NonNull_U_for_core_ptr_non_null_NonNull_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::ops::unsize::CoerceUnsized"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ] ]
          (* Instance *) [].
    End Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Sized_U_where_core_marker_Unsize_T_U_core_ptr_non_null_NonNull_U_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_ops_unsize_DispatchFromDyn_where_core_marker_Sized_T_where_core_marker_Sized_U_where_core_marker_Unsize_T_U_core_ptr_non_null_NonNull_U_for_core_ptr_non_null_NonNull_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::ops::unsize::DispatchFromDyn"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ] ]
          (* Instance *) [].
    End Impl_core_ops_unsize_DispatchFromDyn_where_core_marker_Sized_T_where_core_marker_Sized_U_where_core_marker_Unsize_T_U_core_ptr_non_null_NonNull_U_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::pin::PinCoerceUnsized"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_fmt_Debug_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              fmt::Pointer::fmt(&self.as_ptr(), f)
          }
      *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::fmt::Pointer",
                Ty.apply (Ty.path "*mut") [] [ T ],
                [],
                "fmt",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                M.read (| f |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_fmt_Pointer_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              fmt::Pointer::fmt(&self.as_ptr(), f)
          }
      *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::fmt::Pointer",
                Ty.apply (Ty.path "*mut") [] [ T ],
                [],
                "fmt",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                M.read (| f |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Pointer"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Pointer_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_cmp_Eq_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn eq(&self, other: &Self) -> bool {
              self.as_ptr() == other.as_ptr()
          }
      *)
      Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                  "as_ptr",
                  []
                |),
                [ M.read (| M.read (| self |) |) ]
              |),
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                  "as_ptr",
                  []
                |),
                [ M.read (| M.read (| other |) |) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
    End Impl_core_cmp_PartialEq_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_cmp_Ord_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn cmp(&self, other: &Self) -> Ordering {
              self.as_ptr().cmp(&other.as_ptr())
          }
      *)
      Definition cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::Ord",
                Ty.apply (Ty.path "*mut") [] [ T ],
                [],
                "cmp",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| other |) |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Ord"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method (cmp T)) ].
    End Impl_core_cmp_Ord_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
              self.as_ptr().partial_cmp(&other.as_ptr())
          }
      *)
      Definition partial_cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.apply (Ty.path "*mut") [] [ T ],
                [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                "partial_cmp",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| other |) |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp T)) ].
    End Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_hash_Hash_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn hash<H: hash::Hasher>(&self, state: &mut H) {
              self.as_ptr().hash(state)
          }
      *)
      Definition hash (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::hash::Hash",
                Ty.apply (Ty.path "*mut") [] [ T ],
                [],
                "hash",
                [ H ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                M.read (| state |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::hash::Hash"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method (hash T)) ].
    End Impl_core_hash_Hash_where_core_marker_Sized_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_convert_From_where_core_marker_Sized_T_core_ptr_unique_Unique_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn from(unique: Unique<T>) -> Self {
              unique.as_non_null_ptr()
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ unique ] =>
          ltac:(M.monadic
            (let unique := M.alloc (| unique |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::unique::Unique") [] [ T ],
                "as_non_null_ptr",
                []
              |),
              [ M.read (| unique |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "core::ptr::unique::Unique") [] [ T ] ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_marker_Sized_T_core_ptr_unique_Unique_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_convert_From_where_core_marker_Sized_T_ref_mut_T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn from(reference: &mut T) -> Self {
              // SAFETY: A mutable reference cannot be null.
              unsafe { NonNull { pointer: reference as *mut T } }
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ reference ] =>
          ltac:(M.monadic
            (let reference := M.alloc (| reference |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [
                ("pointer",
                  (* MutToConstPointer *)
                  M.pointer_coercion (M.read (| M.use (M.alloc (| M.read (| reference |) |)) |)))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "&mut") [] [ T ] ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_marker_Sized_T_ref_mut_T_for_core_ptr_non_null_NonNull_T.
    
    Module Impl_core_convert_From_where_core_marker_Sized_T_ref__T_for_core_ptr_non_null_NonNull_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ].
      
      (*
          fn from(reference: &T) -> Self {
              // SAFETY: A reference cannot be null.
              unsafe { NonNull { pointer: reference as *const T } }
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ reference ] =>
          ltac:(M.monadic
            (let reference := M.alloc (| reference |) in
            Value.StructRecord
              "core::ptr::non_null::NonNull"
              [ ("pointer", M.read (| M.use (M.alloc (| M.read (| reference |) |)) |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "&") [] [ T ] ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_marker_Sized_T_ref__T_for_core_ptr_non_null_NonNull_T.
  End non_null.
End ptr.
