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

Module ptr.
  Module const_ptr.
    Module Impl_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
      
      (*
          pub const fn is_null(self) -> bool {
              #[inline]
              fn runtime_impl(ptr: *const u8) -> bool {
                  ptr.addr() == 0
              }
      
              #[inline]
              const fn const_impl(ptr: *const u8) -> bool {
                  match (ptr).guaranteed_eq(null_mut()) {
                      Some(res) => res,
                      // To remain maximally convervative, we stop execution when we don't
                      // know whether the pointer is null or not.
                      // We can *not* return `false` here, that would be unsound in `NonNull::new`!
                      None => panic!("null-ness of this pointer cannot be determined in const context"),
                  }
              }
      
              // Compare via a cast to a thin pointer, so fat pointers are only
              // considering their "data" part for null-ness.
              const_eval_select((self as *const u8,), const_impl, runtime_impl)
          }
      *)
      Definition is_null (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::intrinsics::const_eval_select",
                [
                  Ty.tuple [ Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ] ];
                  Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ] ] (Ty.path "bool");
                  Ty.function [ Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ] ] (Ty.path "bool");
                  Ty.path "bool"
                ]
              |),
              [
                Value.Tuple [ M.rust_cast (M.read (| self |)) ];
                M.get_associated_function (| Self, "const_impl.is_null", [] |);
                M.get_associated_function (| Self, "runtime_impl.is_null", [] |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_null :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "is_null" (is_null T).
      
      (*
          pub const fn cast<U>(self) -> *const U {
              self as _
          }
      *)
      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
            M.rust_cast (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 fn with_metadata_of<U>(self, meta: *const U) -> *const U
          where
              U: ?Sized,
          {
              from_raw_parts::<U>(self as *const (), metadata(meta))
          }
      *)
      Definition with_metadata_of
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ U ], [ self; meta ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let meta := M.alloc (| meta |) in
            M.call_closure (|
              M.get_function (| "core::ptr::metadata::from_raw_parts", [ U; Ty.tuple [] ] |),
              [
                M.rust_cast (M.read (| self |));
                M.call_closure (|
                  M.get_function (| "core::ptr::metadata::metadata", [ U ] |),
                  [ M.read (| meta |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_with_metadata_of :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "with_metadata_of" (with_metadata_of T).
      
      (*
          pub const fn cast_mut(self) -> *mut T {
              self as _
          }
      *)
      Definition cast_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.rust_cast (M.read (| self |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_cast_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "cast_mut" (cast_mut T).
      
      (*
          pub fn addr(self) -> usize {
              // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
              // SAFETY: Pointer-to-integer transmutes are valid (if you are okay with losing the
              // provenance).
              unsafe { mem::transmute(self.cast::<()>()) }
          }
      *)
      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_function (|
                "core::intrinsics::transmute",
                [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ]; Ty.path "usize" ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ T ],
                    "cast",
                    [ Ty.tuple [] ]
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_addr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "addr" (addr T).
      
      (*
          pub fn expose_provenance(self) -> usize {
              // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
              self.cast::<()>() as usize
          }
      *)
      Definition expose_provenance
          (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.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "*const") [] [ T ],
                  "cast",
                  [ Ty.tuple [] ]
                |),
                [ M.read (| self |) ]
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_expose_provenance :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "expose_provenance" (expose_provenance T).
      
      (*
          pub fn with_addr(self, addr: usize) -> Self {
              // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
              //
              // In the mean-time, this operation is defined to be "as if" it was
              // a wrapping_offset, so we can emulate it as such. This should properly
              // restore pointer provenance even under today's compiler.
              let self_addr = self.addr() as isize;
              let dest_addr = addr as isize;
              let offset = dest_addr.wrapping_sub(self_addr);
      
              // This is the canonical desugaring of this operation
              self.wrapping_byte_offset(offset)
          }
      *)
      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.read (|
              let~ self_addr :=
                M.alloc (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "addr",
                        []
                      |),
                      [ M.read (| self |) ]
                    |))
                |) in
              let~ dest_addr := M.alloc (| M.rust_cast (M.read (| addr |)) |) in
              let~ offset :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "isize", "wrapping_sub", [] |),
                    [ M.read (| dest_addr |); M.read (| self_addr |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ T ],
                    "wrapping_byte_offset",
                    []
                  |),
                  [ M.read (| self |); M.read (| offset |) ]
                |)
              |)
            |)))
        | _, _, _ => 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(usize) -> 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_usize__arrow_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 "*const") [] [ T ], "with_addr", [] |),
              [
                M.read (| self |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    impl_FnOnce_usize__arrow_usize,
                    [ Ty.tuple [ Ty.path "usize" ] ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*const") [] [ 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 to_raw_parts(self) -> ( *const (), <T as super::Pointee>::Metadata) {
              (self.cast(), metadata(self))
          }
      *)
      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 "*const") [] [ T ],
                    "cast",
                    [ Ty.tuple [] ]
                  |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_function (| "core::ptr::metadata::metadata", [ T ] |),
                  [ 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 const unsafe fn as_ref<'a>(self) -> Option<&'a T> {
              // SAFETY: the caller must guarantee that `self` is valid
              // for a reference if it isn't null.
              if self.is_null() { None } else { unsafe { Some(&*self) } }
          }
      *)
      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.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*const") [] [ T ],
                                "is_null",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple "core::option::Option::Some" [ 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_ref_unchecked<'a>(self) -> &'a T {
              // SAFETY: the caller must guarantee that `self` is valid for a reference
              unsafe { &*self }
          }
      *)
      Definition as_ref_unchecked
          (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 (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ref_unchecked :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_ref_unchecked" (as_ref_unchecked T).
      
      (*
          pub const unsafe fn as_uninit_ref<'a>(self) -> Option<&'a MaybeUninit<T>>
          where
              T: Sized,
          {
              // SAFETY: the caller must guarantee that `self` meets all the
              // requirements for a reference.
              if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit<T>) }) }
          }
      *)
      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.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*const") [] [ T ],
                                "is_null",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ M.rust_cast (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 offset(self, count: isize) -> *const T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `offset`.
              unsafe { intrinsics::offset(self, 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
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::offset",
                [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "isize" ]
              |),
              [ M.read (| self |); 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`.
              unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
          }
      *)
      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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "offset",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => 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 fn wrapping_offset(self, count: isize) -> *const T
          where
              T: Sized,
          {
              // SAFETY: the `arith_offset` intrinsic has no prerequisites to be called.
              unsafe { intrinsics::arith_offset(self, count) }
          }
      *)
      Definition wrapping_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
            M.call_closure (|
              M.get_function (| "core::intrinsics::arith_offset", [ T ] |),
              [ M.read (| self |); M.read (| count |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_offset :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_offset" (wrapping_offset T).
      
      (*
          pub const fn wrapping_byte_offset(self, count: isize) -> Self {
              self.cast::<u8>().wrapping_offset(count).with_metadata_of(self)
          }
      *)
      Definition wrapping_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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "wrapping_offset",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_byte_offset :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_byte_offset" (wrapping_byte_offset T).
      
      (*
          pub fn mask(self, mask: usize) -> *const T {
              intrinsics::ptr_mask(self.cast::<()>(), mask).with_metadata_of(self)
          }
      *)
      Definition mask (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; mask ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let mask := M.alloc (| mask |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::ptr_mask", [ Ty.tuple [] ] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.tuple [] ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| mask |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_mask :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "mask" (mask T).
      
      (*
          pub const unsafe fn offset_from(self, origin: *const T) -> isize
          where
              T: Sized,
          {
              let pointee_size = mem::size_of::<T>();
              assert!(0 < pointee_size && pointee_size <= isize::MAX as usize);
              // SAFETY: the caller must uphold the safety contract for `ptr_offset_from`.
              unsafe { intrinsics::ptr_offset_from(self, origin) }
          }
      *)
      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.read (|
              let~ pointee_size :=
                M.alloc (|
                  M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                LogicalOp.and (|
                                  BinOp.lt (|
                                    Value.Integer IntegerKind.Usize 0,
                                    M.read (| pointee_size |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| pointee_size |),
                                      M.rust_cast
                                        (M.read (| M.get_constant (| "core::num::MAX" |) |))
                                    |)))
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::intrinsics::ptr_offset_from", [ T ] |),
                  [ M.read (| self |); M.read (| origin |) ]
                |)
              |)
            |)))
        | _, _, _ => 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: *const U) -> isize {
              // SAFETY: the caller must uphold the safety contract for `offset_from`.
              unsafe { self.cast::<u8>().offset_from(origin.cast::<u8>()) }
          }
      *)
      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") [] [ Ty.path "u8" ],
                "offset_from",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ T ],
                    "cast",
                    [ Ty.path "u8" ]
                  |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ U ],
                    "cast",
                    [ Ty.path "u8" ]
                  |),
                  [ M.read (| origin |) ]
                |)
              ]
            |)))
        | _, _, _ => 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, origin: *const T) -> usize
          where
              T: Sized,
          {
              const fn runtime_ptr_ge(this: *const (), origin: *const ()) -> bool {
                  fn runtime(this: *const (), origin: *const ()) -> bool {
                      this >= origin
                  }
                  const fn comptime(_: *const (), _: *const ()) -> bool {
                      true
                  }
      
                  #[allow(unused_unsafe)]
                  intrinsics::const_eval_select((this, origin), comptime, runtime)
              }
      
              ub_checks::assert_unsafe_precondition!(
                  check_language_ub,
                  "ptr::sub_ptr requires `self >= origin`",
                  (
                      this: *const () = self as *const (),
                      origin: *const () = origin as *const (),
                  ) => runtime_ptr_ge(this, origin)
              );
      
              let pointee_size = mem::size_of::<T>();
              assert!(0 < pointee_size && pointee_size <= isize::MAX as usize);
              // SAFETY: the caller must uphold the safety contract for `ptr_offset_from_unsigned`.
              unsafe { intrinsics::ptr_offset_from_unsigned(self, origin) }
          }
      *)
      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; origin ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let origin := M.alloc (| origin |) 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.sub_ptr",
                                []
                              |),
                              [ M.rust_cast (M.read (| self |)); M.rust_cast (M.read (| origin |)) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ pointee_size :=
                M.alloc (|
                  M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                LogicalOp.and (|
                                  BinOp.lt (|
                                    Value.Integer IntegerKind.Usize 0,
                                    M.read (| pointee_size |)
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| pointee_size |),
                                      M.rust_cast
                                        (M.read (| M.get_constant (| "core::num::MAX" |) |))
                                    |)))
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::intrinsics::ptr_offset_from_unsigned", [ T ] |),
                  [ M.read (| self |); M.read (| origin |) ]
                |)
              |)
            |)))
        | _, _, _ => 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 fn guaranteed_eq(self, other: *const T) -> Option<bool>
          where
              T: Sized,
          {
              match intrinsics::ptr_guaranteed_cmp(self, other) {
                  2 => None,
                  other => Some(other == 1),
              }
          }
      *)
      Definition guaranteed_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
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::ptr_guaranteed_cmp", [ T ] |),
                    [ M.read (| self |); M.read (| other |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (|
                          M.read (| γ |),
                          Value.Integer IntegerKind.U8 2
                        |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let other := M.copy (| γ |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ BinOp.eq (| M.read (| other |), Value.Integer IntegerKind.U8 1 |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_guaranteed_eq :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "guaranteed_eq" (guaranteed_eq T).
      
      (*
          pub const fn guaranteed_ne(self, other: *const T) -> Option<bool>
          where
              T: Sized,
          {
              match self.guaranteed_eq(other) {
                  None => None,
                  Some(eq) => Some(!eq),
              }
          }
      *)
      Definition guaranteed_ne
          (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.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ T ],
                      "guaranteed_eq",
                      []
                    |),
                    [ M.read (| self |); M.read (| other |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let eq := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ UnOp.not (| M.read (| eq |) |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_guaranteed_ne :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "guaranteed_ne" (guaranteed_ne T).
      
      (*
          pub const unsafe fn add(self, count: usize) -> Self
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `offset`.
              unsafe { intrinsics::offset(self, 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
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::offset",
                [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "usize" ]
              |),
              [ M.read (| self |); 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`.
              unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
          }
      *)
      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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "add",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => 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 "*const") [] [ 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`.
              unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
          }
      *)
      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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "sub",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => 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 fn wrapping_add(self, count: usize) -> Self
          where
              T: Sized,
          {
              self.wrapping_offset(count as isize)
          }
      *)
      Definition wrapping_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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "wrapping_offset",
                []
              |),
              [ M.read (| self |); M.rust_cast (M.read (| count |)) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_add :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_add" (wrapping_add T).
      
      (*
          pub const fn wrapping_byte_add(self, count: usize) -> Self {
              self.cast::<u8>().wrapping_add(count).with_metadata_of(self)
          }
      *)
      Definition wrapping_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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "wrapping_add",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_byte_add :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_byte_add" (wrapping_byte_add T).
      
      (*
          pub const fn wrapping_sub(self, count: usize) -> Self
          where
              T: Sized,
          {
              self.wrapping_offset((count as isize).wrapping_neg())
          }
      *)
      Definition wrapping_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.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ T ],
                "wrapping_offset",
                []
              |),
              [
                M.read (| self |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "isize", "wrapping_neg", [] |),
                  [ M.rust_cast (M.read (| count |)) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_sub :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_sub" (wrapping_sub T).
      
      (*
          pub const fn wrapping_byte_sub(self, count: usize) -> Self {
              self.cast::<u8>().wrapping_sub(count).with_metadata_of(self)
          }
      *)
      Definition wrapping_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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "with_metadata_of",
                [ T ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                    "wrapping_sub",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "cast",
                        [ Ty.path "u8" ]
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| count |)
                  ]
                |);
                M.read (| self |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrapping_byte_sub :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrapping_byte_sub" (wrapping_byte_sub T).
      
      (*
          pub const unsafe fn read(self) -> T
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `read`.
              unsafe { read(self) }
          }
      *)
      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 (| self |) ]
            |)))
        | _, _, _ => 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 { read_volatile(self) }
          }
      *)
      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 (| self |) ]
            |)))
        | _, _, _ => 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 { read_unaligned(self) }
          }
      *)
      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 (| self |) ]
            |)))
        | _, _, _ => 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: *mut T, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy`.
              unsafe { copy(self, dest, 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 (| self |); 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: *mut T, count: usize)
          where
              T: Sized,
          {
              // SAFETY: the caller must uphold the safety contract for `copy_nonoverlapping`.
              unsafe { copy_nonoverlapping(self, dest, 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 (| self |); 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 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
              let ret = unsafe { align_offset(self, align) };
      
              // Inform Miri that we want to consider the resulting pointer to be suitably aligned.
              #[cfg(miri)]
              if ret != usize::MAX {
                  intrinsics::miri_promise_symbolic_alignment(self.wrapping_add(ret).cast(), align);
              }
      
              ret
          }
      *)
      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
              let~ ret :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ptr::align_offset", [ T ] |),
                    [ M.read (| self |); M.read (| align |) ]
                  |)
                |) in
              ret
            |)))
        | _, _, _ => 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.is_aligned_to(mem::align_of::<T>())
          }
      *)
      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_to",
                []
              |),
              [
                M.read (| self |);
                M.call_closure (| M.get_function (| "core::mem::align_of", [ T ] |), [] |)
              ]
            |)))
        | _, _, _ => 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 {
              if !align.is_power_of_two() {
                  panic!("is_aligned_to: align is not a power-of-two");
              }
      
              #[inline]
              fn runtime_impl(ptr: *const (), align: usize) -> bool {
                  ptr.addr() & (align - 1) == 0
              }
      
              #[inline]
              const fn const_impl(ptr: *const (), align: usize) -> bool {
                  // We can't use the address of `self` in a `const fn`, so we use `align_offset` instead.
                  ptr.align_offset(align) == 0
              }
      
              // The cast to `()` is used to
              //   1. deal with fat pointers; and
              //   2. ensure that `align_offset` (in `const_impl`) doesn't actually try to compute an offset.
              const_eval_select((self.cast::<()>(), align), const_impl, runtime_impl)
          }
      *)
      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.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
                                              "is_aligned_to: 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::intrinsics::const_eval_select",
                    [
                      Ty.tuple [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ]; Ty.path "usize" ];
                      Ty.function
                        [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ]; Ty.path "usize" ]
                        (Ty.path "bool");
                      Ty.function
                        [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ]; Ty.path "usize" ]
                        (Ty.path "bool");
                      Ty.path "bool"
                    ]
                  |),
                  [
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*const") [] [ T ],
                            "cast",
                            [ Ty.tuple [] ]
                          |),
                          [ M.read (| self |) ]
                        |);
                        M.read (| align |)
                      ];
                    M.get_associated_function (| Self, "const_impl.is_aligned_to", [] |);
                    M.get_associated_function (| Self, "runtime_impl.is_aligned_to", [] |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => 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_pointer_const_T.
    
    Module Impl_pointer_const_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          pub const fn len(self) -> usize {
              metadata(self)
          }
      *)
      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_function (|
                "core::ptr::metadata::metadata",
                [ Ty.apply (Ty.path "slice") [] [ T ] ]
              |),
              [ 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 "*const") [] [ 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_ptr(self) -> *const T {
              self as *const 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 (| self |))))
        | _, _, _ => 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 unsafe fn get_unchecked<I>(self, index: I) -> *const I::Output
          where
              I: SliceIndex<[T]>,
          {
              // SAFETY: the caller ensures that `self` is dereferenceable and `index` in-bounds.
              unsafe { index.get_unchecked(self) }
          }
      *)
      Definition get_unchecked
          (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_trait_method (|
                "core::slice::index::SliceIndex",
                I,
                [ Ty.apply (Ty.path "slice") [] [ T ] ],
                "get_unchecked",
                []
              |),
              [ M.read (| index |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_unchecked :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_unchecked" (get_unchecked T).
      
      (*
          pub const unsafe fn as_uninit_slice<'a>(self) -> Option<&'a [MaybeUninit<T>]> {
              if self.is_null() {
                  None
              } else {
                  // SAFETY: the caller must uphold the safety contract for `as_uninit_slice`.
                  Some(unsafe { slice::from_raw_parts(self as *const MaybeUninit<T>, 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.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*const")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                "is_null",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_function (|
                                "core::slice::raw::from_raw_parts",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                              |),
                              [
                                M.rust_cast (M.read (| self |));
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ 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).
    End Impl_pointer_const_slice_T.
    
    Module Impl_pointer_const_array_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
      
      (*
          pub const fn as_ptr(self) -> *const T {
              self as *const T
          }
      *)
      Definition as_ptr
          (N : Value.t)
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast (M.read (| self |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ptr :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "as_ptr" (as_ptr N T).
      
      (*
          pub const fn as_slice(self) -> *const [T] {
              self
          }
      *)
      Definition as_slice
          (N : Value.t)
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_slice :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "as_slice" (as_slice N T).
    End Impl_pointer_const_array_N_T.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
      
      (*
          fn eq(&self, other: &*const T) -> bool {
              *self == *other
          }
      *)
      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.read (| M.read (| self |) |), 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_pointer_const_T.
    
    Module Impl_core_cmp_Eq_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ 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_pointer_const_T.
    
    Module Impl_core_cmp_Ord_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
      
      (*
          fn cmp(&self, other: &*const T) -> Ordering {
              if self < other {
                  Less
              } else if self == other {
                  Equal
              } else {
                  Greater
              }
          }
      *)
      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.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialOrd",
                                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "*const") [] [ T ] ]
                                ],
                                "lt",
                                []
                              |),
                              [ self; M.alloc (| M.read (| other |) |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::cmp::Ordering::Less" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "*const") [] [ T ] ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [ self; other ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (| Value.StructTuple "core::cmp::Ordering::Greater" [] |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_pointer_const_T.
    
    Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
      
      (*
          fn partial_cmp(&self, other: &*const T) -> Option<Ordering> {
              Some(self.cmp(other))
          }
      *)
      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
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::Ord",
                    Ty.apply (Ty.path "*const") [] [ T ],
                    [],
                    "cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn lt(&self, other: &*const T) -> bool {
              *self < *other
          }
      *)
      Definition lt (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.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn le(&self, other: &*const T) -> bool {
              *self <= *other
          }
      *)
      Definition le (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.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn gt(&self, other: &*const T) -> bool {
              *self > *other
          }
      *)
      Definition gt (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.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ge(&self, other: &*const T) -> bool {
              *self >= *other
          }
      *)
      Definition ge (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.ge (| M.read (| M.read (| self |) |), 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));
            ("lt", InstanceField.Method (lt T));
            ("le", InstanceField.Method (le T));
            ("gt", InstanceField.Method (gt T));
            ("ge", InstanceField.Method (ge T))
          ].
    End Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_pointer_const_T.
  End const_ptr.
End ptr.
