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

Module ptr.
  (*
  pub unsafe fn drop_in_place<T: ?Sized>(to_drop: *mut T) {
      // Code here does not matter - this is replaced by the
      // real drop glue by the compiler.
  
      // SAFETY: see comment above
      unsafe { drop_in_place(to_drop) }
  }
  *)
  Definition drop_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ to_drop ] =>
      ltac:(M.monadic
        (let to_drop := M.alloc (| to_drop |) in
        M.call_closure (|
          M.get_function (| "core::ptr::drop_in_place", [ T ] |),
          [ M.read (| to_drop |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_drop_in_place : M.IsFunction "core::ptr::drop_in_place" drop_in_place.
  
  (*
  pub const fn null<T: ?Sized + Thin>() -> *const T {
      from_raw_parts(without_provenance::<()>(0), ())
  }
  *)
  Definition null (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (| "core::ptr::metadata::from_raw_parts", [ T; Ty.tuple [] ] |),
          [
            M.call_closure (|
              M.get_function (| "core::ptr::without_provenance", [ Ty.tuple [] ] |),
              [ Value.Integer IntegerKind.Usize 0 ]
            |);
            Value.Tuple []
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_null : M.IsFunction "core::ptr::null" null.
  
  (*
  pub const fn null_mut<T: ?Sized + Thin>() -> *mut T {
      from_raw_parts_mut(without_provenance_mut::<()>(0), ())
  }
  *)
  Definition null_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (| "core::ptr::metadata::from_raw_parts_mut", [ T; Ty.tuple [] ] |),
          [
            M.call_closure (|
              M.get_function (| "core::ptr::without_provenance_mut", [ Ty.tuple [] ] |),
              [ Value.Integer IntegerKind.Usize 0 ]
            |);
            Value.Tuple []
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_null_mut : M.IsFunction "core::ptr::null_mut" null_mut.
  
  (*
  pub const fn without_provenance<T>(addr: usize) -> *const T {
      // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
      // We use transmute rather than a cast so tools like Miri can tell that this
      // is *not* the same as with_exposed_provenance.
      // SAFETY: every valid integer is also a valid pointer (as long as you don't dereference that
      // pointer).
      unsafe { mem::transmute(addr) }
  }
  *)
  Definition without_provenance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ addr ] =>
      ltac:(M.monadic
        (let addr := M.alloc (| addr |) in
        M.call_closure (|
          M.get_function (|
            "core::intrinsics::transmute",
            [ Ty.path "usize"; Ty.apply (Ty.path "*const") [] [ T ] ]
          |),
          [ M.read (| addr |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_without_provenance :
    M.IsFunction "core::ptr::without_provenance" without_provenance.
  
  (*
  pub const fn dangling<T>() -> *const T {
      without_provenance(mem::align_of::<T>())
  }
  *)
  Definition dangling (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (| "core::ptr::without_provenance", [ T ] |),
          [ M.call_closure (| M.get_function (| "core::mem::align_of", [ T ] |), [] |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_dangling : M.IsFunction "core::ptr::dangling" dangling.
  
  (*
  pub const fn without_provenance_mut<T>(addr: usize) -> *mut T {
      // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
      // We use transmute rather than a cast so tools like Miri can tell that this
      // is *not* the same as with_exposed_provenance.
      // SAFETY: every valid integer is also a valid pointer (as long as you don't dereference that
      // pointer).
      unsafe { mem::transmute(addr) }
  }
  *)
  Definition without_provenance_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ addr ] =>
      ltac:(M.monadic
        (let addr := M.alloc (| addr |) in
        M.call_closure (|
          M.get_function (|
            "core::intrinsics::transmute",
            [ Ty.path "usize"; Ty.apply (Ty.path "*mut") [] [ T ] ]
          |),
          [ M.read (| addr |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_without_provenance_mut :
    M.IsFunction "core::ptr::without_provenance_mut" without_provenance_mut.
  
  (*
  pub const fn dangling_mut<T>() -> *mut T {
      without_provenance_mut(mem::align_of::<T>())
  }
  *)
  Definition dangling_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (| "core::ptr::without_provenance_mut", [ T ] |),
          [ M.call_closure (| M.get_function (| "core::mem::align_of", [ T ] |), [] |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_dangling_mut : M.IsFunction "core::ptr::dangling_mut" dangling_mut.
  
  (*
  pub fn with_exposed_provenance<T>(addr: usize) -> *const T
  where
      T: Sized,
  {
      // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
      addr as *const T
  }
  *)
  Definition with_exposed_provenance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ addr ] =>
      ltac:(M.monadic
        (let addr := M.alloc (| addr |) in
        M.rust_cast (M.read (| addr |))))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_with_exposed_provenance :
    M.IsFunction "core::ptr::with_exposed_provenance" with_exposed_provenance.
  
  (*
  pub fn with_exposed_provenance_mut<T>(addr: usize) -> *mut T
  where
      T: Sized,
  {
      // FIXME(strict_provenance_magic): I am magic and should be a compiler intrinsic.
      addr as *mut T
  }
  *)
  Definition with_exposed_provenance_mut
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [ T ], [ addr ] =>
      ltac:(M.monadic
        (let addr := M.alloc (| addr |) in
        M.rust_cast (M.read (| addr |))))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_with_exposed_provenance_mut :
    M.IsFunction "core::ptr::with_exposed_provenance_mut" with_exposed_provenance_mut.
  
  (*
  pub const fn from_ref<T: ?Sized>(r: &T) -> *const T {
      r
  }
  *)
  Definition from_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ r ] =>
      ltac:(M.monadic
        (let r := M.alloc (| r |) in
        M.read (| r |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_ref : M.IsFunction "core::ptr::from_ref" from_ref.
  
  (*
  pub const fn from_mut<T: ?Sized>(r: &mut T) -> *mut T {
      r
  }
  *)
  Definition from_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ r ] =>
      ltac:(M.monadic
        (let r := M.alloc (| r |) in
        M.read (| r |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_mut : M.IsFunction "core::ptr::from_mut" from_mut.
  
  (*
  pub const fn slice_from_raw_parts<T>(data: *const T, len: usize) -> *const [T] {
      from_raw_parts(data, len)
  }
  *)
  Definition slice_from_raw_parts (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ data; len ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let len := M.alloc (| len |) in
        M.call_closure (|
          M.get_function (|
            "core::ptr::metadata::from_raw_parts",
            [ Ty.apply (Ty.path "slice") [] [ T ]; T ]
          |),
          [ M.read (| data |); M.read (| len |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_slice_from_raw_parts :
    M.IsFunction "core::ptr::slice_from_raw_parts" slice_from_raw_parts.
  
  (*
  pub const fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T] {
      from_raw_parts_mut(data, len)
  }
  *)
  Definition slice_from_raw_parts_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ data; len ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let len := M.alloc (| len |) in
        M.call_closure (|
          M.get_function (|
            "core::ptr::metadata::from_raw_parts_mut",
            [ Ty.apply (Ty.path "slice") [] [ T ]; T ]
          |),
          [ M.read (| data |); M.read (| len |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_slice_from_raw_parts_mut :
    M.IsFunction "core::ptr::slice_from_raw_parts_mut" slice_from_raw_parts_mut.
  
  (*
  pub const unsafe fn swap<T>(x: *mut T, y: *mut T) {
      // Give ourselves some scratch space to work with.
      // We do not have to worry about drops: `MaybeUninit` does nothing when dropped.
      let mut tmp = MaybeUninit::<T>::uninit();
  
      // Perform the swap
      // SAFETY: the caller must guarantee that `x` and `y` are
      // valid for writes and properly aligned. `tmp` cannot be
      // overlapping either `x` or `y` because `tmp` was just allocated
      // on the stack as a separate allocated object.
      unsafe {
          copy_nonoverlapping(x, tmp.as_mut_ptr(), 1);
          copy(y, x, 1); // `x` and `y` may overlap
          copy_nonoverlapping(tmp.as_ptr(), y, 1);
      }
  }
  *)
  Definition swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ x; y ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        let y := M.alloc (| y |) in
        M.read (|
          let~ tmp :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                  "uninit",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                [
                  (* MutToConstPointer *) M.pointer_coercion (M.read (| x |));
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "as_mut_ptr",
                      []
                    |),
                    [ tmp ]
                  |);
                  Value.Integer IntegerKind.Usize 1
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::copy", [ T ] |),
                [
                  (* MutToConstPointer *) M.pointer_coercion (M.read (| y |));
                  M.read (| x |);
                  Value.Integer IntegerKind.Usize 1
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ tmp ]
                  |);
                  M.read (| y |);
                  Value.Integer IntegerKind.Usize 1
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_swap : M.IsFunction "core::ptr::swap" swap.
  
  (*
  pub const unsafe fn swap_nonoverlapping<T>(x: *mut T, y: *mut T, count: usize) {
      #[allow(unused)]
      macro_rules! attempt_swap_as_chunks {
          ($ChunkTy:ty) => {
              if mem::align_of::<T>() >= mem::align_of::<$ChunkTy>()
                  && mem::size_of::<T>() % mem::size_of::<$ChunkTy>() == 0
              {
                  let x: *mut $ChunkTy = x.cast();
                  let y: *mut $ChunkTy = y.cast();
                  let count = count * (mem::size_of::<T>() / mem::size_of::<$ChunkTy>());
                  // SAFETY: these are the same bytes that the caller promised were
                  // ok, just typed as `MaybeUninit<ChunkTy>`s instead of as `T`s.
                  // The `if` condition above ensures that we're not violating
                  // alignment requirements, and that the division is exact so
                  // that we don't lose any bytes off the end.
                  return unsafe { swap_nonoverlapping_simple_untyped(x, y, count) };
              }
          };
      }
  
      ub_checks::assert_unsafe_precondition!(
          check_language_ub,
          "ptr::swap_nonoverlapping requires that both pointer arguments are aligned and non-null \
          and the specified memory ranges do not overlap",
          (
              x: *mut () = x as *mut (),
              y: *mut () = y as *mut (),
              size: usize = size_of::<T>(),
              align: usize = align_of::<T>(),
              count: usize = count,
          ) =>
          ub_checks::is_aligned_and_not_null(x, align)
              && ub_checks::is_aligned_and_not_null(y, align)
              && ub_checks::is_nonoverlapping(x, y, size, count)
      );
  
      // Split up the slice into small power-of-two-sized chunks that LLVM is able
      // to vectorize (unless it's a special type with more-than-pointer alignment,
      // because we don't want to pessimize things like slices of SIMD vectors.)
      if mem::align_of::<T>() <= mem::size_of::<usize>()
          && (!mem::size_of::<T>().is_power_of_two()
              || mem::size_of::<T>() > mem::size_of::<usize>() * 2)
      {
          attempt_swap_as_chunks!(usize);
          attempt_swap_as_chunks!(u8);
      }
  
      // SAFETY: Same preconditions as this function
      unsafe { swap_nonoverlapping_simple_untyped(x, y, count) }
  }
  *)
  Definition swap_nonoverlapping (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ x; y; count ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        let y := M.alloc (| y |) in
        let count := M.alloc (| count |) in
        M.catch_return (|
          ltac:(M.monadic
            (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_function (|
                                "core::ptr::swap_nonoverlapping.precondition_check",
                                []
                              |),
                              [
                                M.rust_cast (M.read (| x |));
                                M.rust_cast (M.read (| y |));
                                M.call_closure (|
                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                  []
                                |);
                                M.call_closure (|
                                  M.get_function (| "core::mem::align_of", [ T ] |),
                                  []
                                |);
                                M.read (| count |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.call_closure (|
                                    M.get_function (| "core::mem::align_of", [ T ] |),
                                    []
                                  |),
                                  M.call_closure (|
                                    M.get_function (| "core::mem::size_of", [ Ty.path "usize" ] |),
                                    []
                                  |)
                                |),
                                ltac:(M.monadic
                                  (LogicalOp.or (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "usize",
                                          "is_power_of_two",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_function (| "core::mem::size_of", [ T ] |),
                                            []
                                          |)
                                        ]
                                      |)
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.gt (|
                                        M.call_closure (|
                                          M.get_function (| "core::mem::size_of", [ T ] |),
                                          []
                                        |),
                                        BinOp.Wrap.mul (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::mem::size_of",
                                              [ Ty.path "usize" ]
                                            |),
                                            []
                                          |),
                                          Value.Integer IntegerKind.Usize 2
                                        |)
                                      |)))
                                  |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          BinOp.ge (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::align_of", [ T ] |),
                                              []
                                            |),
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::mem::align_of",
                                                [ Ty.path "usize" ]
                                              |),
                                              []
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.eq (|
                                              BinOp.Wrap.rem (|
                                                M.call_closure (|
                                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                                  []
                                                |),
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::mem::size_of",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  []
                                                |)
                                              |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "cast",
                                                [ Ty.path "usize" ]
                                              |),
                                              [ M.read (| x |) ]
                                            |)
                                          |) in
                                        let~ y :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "cast",
                                                [ Ty.path "usize" ]
                                              |),
                                              [ M.read (| y |) ]
                                            |)
                                          |) in
                                        let~ count :=
                                          M.alloc (|
                                            BinOp.Wrap.mul (|
                                              M.read (| count |),
                                              BinOp.Wrap.div (|
                                                M.call_closure (|
                                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                                  []
                                                |),
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::mem::size_of",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  []
                                                |)
                                              |)
                                            |)
                                          |) in
                                        M.return_ (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::ptr::swap_nonoverlapping_simple_untyped",
                                              [ Ty.path "usize" ]
                                            |),
                                            [ M.read (| x |); M.read (| y |); M.read (| count |) ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          BinOp.ge (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::align_of", [ T ] |),
                                              []
                                            |),
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::mem::align_of",
                                                [ Ty.path "u8" ]
                                              |),
                                              []
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.eq (|
                                              BinOp.Wrap.rem (|
                                                M.call_closure (|
                                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                                  []
                                                |),
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::mem::size_of",
                                                    [ Ty.path "u8" ]
                                                  |),
                                                  []
                                                |)
                                              |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "cast",
                                                [ Ty.path "u8" ]
                                              |),
                                              [ M.read (| x |) ]
                                            |)
                                          |) in
                                        let~ y :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "cast",
                                                [ Ty.path "u8" ]
                                              |),
                                              [ M.read (| y |) ]
                                            |)
                                          |) in
                                        let~ count :=
                                          M.alloc (|
                                            BinOp.Wrap.mul (|
                                              M.read (| count |),
                                              BinOp.Wrap.div (|
                                                M.call_closure (|
                                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                                  []
                                                |),
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::mem::size_of",
                                                    [ Ty.path "u8" ]
                                                  |),
                                                  []
                                                |)
                                              |)
                                            |)
                                          |) in
                                        M.return_ (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::ptr::swap_nonoverlapping_simple_untyped",
                                              [ Ty.path "u8" ]
                                            |),
                                            [ M.read (| x |); M.read (| y |); M.read (| count |) ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::ptr::swap_nonoverlapping_simple_untyped", [ T ] |),
                  [ M.read (| x |); M.read (| y |); M.read (| count |) ]
                |)
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_swap_nonoverlapping :
    M.IsFunction "core::ptr::swap_nonoverlapping" swap_nonoverlapping.
  
  (*
  const unsafe fn swap_nonoverlapping_simple_untyped<T>(x: *mut T, y: *mut T, count: usize) {
      let x = x.cast::<MaybeUninit<T>>();
      let y = y.cast::<MaybeUninit<T>>();
      let mut i = 0;
      while i < count {
          // SAFETY: By precondition, `i` is in-bounds because it's below `n`
          let x = unsafe { x.add(i) };
          // SAFETY: By precondition, `i` is in-bounds because it's below `n`
          // and it's distinct from `x` since the ranges are non-overlapping
          let y = unsafe { y.add(i) };
  
          // If we end up here, it's because we're using a simple type -- like
          // a small power-of-two-sized thing -- or a special type with particularly
          // large alignment, particularly SIMD types.
          // Thus, we're fine just reading-and-writing it, as either it's small
          // and that works well anyway or it's special and the type's author
          // presumably wanted things to be done in the larger chunk.
  
          // SAFETY: we're only ever given pointers that are valid to read/write,
          // including being aligned, and nothing here panics so it's drop-safe.
          unsafe {
              let a: MaybeUninit<T> = read(x);
              let b: MaybeUninit<T> = read(y);
              write(x, b);
              write(y, a);
          }
  
          i += 1;
      }
  }
  *)
  Definition swap_nonoverlapping_simple_untyped
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [ T ], [ x; y; count ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        let y := M.alloc (| y |) in
        let count := M.alloc (| count |) in
        M.read (|
          let~ x :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "*mut") [] [ T ],
                  "cast",
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                |),
                [ M.read (| x |) ]
              |)
            |) in
          let~ y :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "*mut") [] [ T ],
                  "cast",
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                |),
                [ M.read (| y |) ]
              |)
            |) in
          let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
          M.loop (|
            ltac:(M.monadic
              (M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.alloc (| BinOp.lt (| M.read (| i |), M.read (| count |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ x :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*mut")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              "add",
                              []
                            |),
                            [ M.read (| x |); M.read (| i |) ]
                          |)
                        |) in
                      let~ y :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*mut")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              "add",
                              []
                            |),
                            [ M.read (| y |); M.read (| i |) ]
                          |)
                        |) in
                      let~ _ :=
                        let~ a :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::ptr::read",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                              |),
                              [ (* MutToConstPointer *) M.pointer_coercion (M.read (| x |)) ]
                            |)
                          |) in
                        let~ b :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::ptr::read",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                              |),
                              [ (* MutToConstPointer *) M.pointer_coercion (M.read (| y |)) ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::ptr::write",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                              |),
                              [ M.read (| x |); M.read (| b |) ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::ptr::write",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ]
                              |),
                              [ M.read (| y |); M.read (| a |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |) in
                      let~ _ :=
                        let β := i in
                        M.write (|
                          β,
                          BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            let~ _ :=
                              M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                            M.alloc (| Value.Tuple [] |)
                          |)
                        |)
                      |)))
                ]
              |)))
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_swap_nonoverlapping_simple_untyped :
    M.IsFunction "core::ptr::swap_nonoverlapping_simple_untyped" swap_nonoverlapping_simple_untyped.
  
  (*
  pub const unsafe fn replace<T>(dst: *mut T, src: T) -> T {
      // SAFETY: the caller must guarantee that `dst` is valid to be
      // cast to a mutable reference (valid for writes, aligned, initialized),
      // and cannot overlap `src` since `dst` must point to a distinct
      // allocated object.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::replace requires that the pointer argument is aligned and non-null",
              (
                  addr: *const () = dst as *const (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          mem::replace(&mut *dst, src)
      }
  }
  *)
  Definition replace (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dst; src ] =>
      ltac:(M.monadic
        (let dst := M.alloc (| dst |) in
        let src := M.alloc (| src |) 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_function (| "core::ptr::replace.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| dst |));
                            M.call_closure (|
                              M.get_function (| "core::mem::align_of", [ T ] |),
                              []
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::mem::replace", [ T ] |),
              [ M.read (| dst |); M.read (| src |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_replace : M.IsFunction "core::ptr::replace" replace.
  
  (*
  pub const unsafe fn read<T>(src: *const T) -> T {
      // It would be semantically correct to implement this via `copy_nonoverlapping`
      // and `MaybeUninit`, as was done before PR #109035. Calling `assume_init`
      // provides enough information to know that this is a typed operation.
  
      // However, as of March 2023 the compiler was not capable of taking advantage
      // of that information. Thus, the implementation here switched to an intrinsic,
      // which lowers to `_0 = *src` in MIR, to address a few issues:
      //
      // - Using `MaybeUninit::assume_init` after a `copy_nonoverlapping` was not
      //   turning the untyped copy into a typed load. As such, the generated
      //   `load` in LLVM didn't get various metadata, such as `!range` (#73258),
      //   `!nonnull`, and `!noundef`, resulting in poorer optimization.
      // - Going through the extra local resulted in multiple extra copies, even
      //   in optimized MIR.  (Ignoring StorageLive/Dead, the intrinsic is one
      //   MIR statement, while the previous implementation was eight.)  LLVM
      //   could sometimes optimize them away, but because `read` is at the core
      //   of so many things, not having them in the first place improves what we
      //   hand off to the backend.  For example, `mem::replace::<Big>` previously
      //   emitted 4 `alloca` and 6 `memcpy`s, but is now 1 `alloc` and 3 `memcpy`s.
      // - In general, this approach keeps us from getting any more bugs (like
      //   #106369) that boil down to "`read(p)` is worse than `*p`", as this
      //   makes them look identical to the backend (or other MIR consumers).
      //
      // Future enhancements to MIR optimizations might well allow this to return
      // to the previous implementation, rather than using an intrinsic.
  
      // SAFETY: the caller must guarantee that `src` is valid for reads.
      unsafe {
          #[cfg(debug_assertions)] // Too expensive to always enable (for now?)
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::read requires that the pointer argument is aligned and non-null",
              (
                  addr: *const () = src as *const (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          crate::intrinsics::read_via_copy(src)
      }
  }
  *)
  Definition read (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ src ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) 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_function (| "core::ptr::read.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| src |));
                            M.call_closure (|
                              M.get_function (| "core::mem::align_of", [ T ] |),
                              []
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::read_via_copy", [ T ] |),
              [ M.read (| src |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_read : M.IsFunction "core::ptr::read" read.
  
  (*
  pub const unsafe fn read_unaligned<T>(src: *const T) -> T {
      let mut tmp = MaybeUninit::<T>::uninit();
      // SAFETY: the caller must guarantee that `src` is valid for reads.
      // `src` cannot overlap `tmp` because `tmp` was just allocated on
      // the stack as a separate allocated object.
      //
      // Also, since we just wrote a valid value into `tmp`, it is guaranteed
      // to be properly initialized.
      unsafe {
          copy_nonoverlapping(src as *const u8, tmp.as_mut_ptr() as *mut u8, mem::size_of::<T>());
          tmp.assume_init()
      }
  }
  *)
  Definition read_unaligned (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ src ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) in
        M.read (|
          let~ tmp :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                  "uninit",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ Ty.path "u8" ] |),
                [
                  M.rust_cast (M.read (| src |));
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                        "as_mut_ptr",
                        []
                      |),
                      [ tmp ]
                    |));
                  M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                "assume_init",
                []
              |),
              [ M.read (| tmp |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_read_unaligned : M.IsFunction "core::ptr::read_unaligned" read_unaligned.
  
  (*
  pub const unsafe fn write<T>(dst: *mut T, src: T) {
      // Semantically, it would be fine for this to be implemented as a
      // `copy_nonoverlapping` and appropriate drop suppression of `src`.
  
      // However, implementing via that currently produces more MIR than is ideal.
      // Using an intrinsic keeps it down to just the simple `*dst = move src` in
      // MIR (11 statements shorter, at the time of writing), and also allows
      // `src` to stay an SSA value in codegen_ssa, rather than a memory one.
  
      // SAFETY: the caller must guarantee that `dst` is valid for writes.
      // `dst` cannot overlap `src` because the caller has mutable access
      // to `dst` while `src` is owned by this function.
      unsafe {
          #[cfg(debug_assertions)] // Too expensive to always enable (for now?)
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::write requires that the pointer argument is aligned and non-null",
              (
                  addr: *mut () = dst as *mut (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          intrinsics::write_via_move(dst, src)
      }
  }
  *)
  Definition write (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dst; src ] =>
      ltac:(M.monadic
        (let dst := M.alloc (| dst |) in
        let src := M.alloc (| src |) 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_function (| "core::ptr::write.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| dst |));
                            M.call_closure (|
                              M.get_function (| "core::mem::align_of", [ T ] |),
                              []
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::write_via_move", [ T ] |),
              [ M.read (| dst |); M.read (| src |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_write : M.IsFunction "core::ptr::write" write.
  
  (*
  pub const unsafe fn write_unaligned<T>(dst: *mut T, src: T) {
      // SAFETY: the caller must guarantee that `dst` is valid for writes.
      // `dst` cannot overlap `src` because the caller has mutable access
      // to `dst` while `src` is owned by this function.
      unsafe {
          copy_nonoverlapping((&raw const src) as *const u8, dst as *mut u8, mem::size_of::<T>());
          // We are calling the intrinsic directly to avoid function calls in the generated code.
          intrinsics::forget(src);
      }
  }
  *)
  Definition write_unaligned (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dst; src ] =>
      ltac:(M.monadic
        (let dst := M.alloc (| dst |) in
        let src := M.alloc (| src |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ Ty.path "u8" ] |),
                [
                  M.rust_cast src;
                  M.rust_cast (M.read (| dst |));
                  M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::forget", [ T ] |),
                [ M.read (| src |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_write_unaligned : M.IsFunction "core::ptr::write_unaligned" write_unaligned.
  
  (*
  pub unsafe fn read_volatile<T>(src: *const T) -> T {
      // SAFETY: the caller must uphold the safety contract for `volatile_load`.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::read_volatile requires that the pointer argument is aligned and non-null",
              (
                  addr: *const () = src as *const (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          intrinsics::volatile_load(src)
      }
  }
  *)
  Definition read_volatile (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ src ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) 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_function (| "core::ptr::read_volatile.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| src |));
                            M.call_closure (|
                              M.get_function (| "core::mem::align_of", [ T ] |),
                              []
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::volatile_load", [ T ] |),
              [ M.read (| src |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_read_volatile : M.IsFunction "core::ptr::read_volatile" read_volatile.
  
  (*
  pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
      // SAFETY: the caller must uphold the safety contract for `volatile_store`.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::write_volatile requires that the pointer argument is aligned and non-null",
              (
                  addr: *mut () = dst as *mut (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          intrinsics::volatile_store(dst, src);
      }
  }
  *)
  Definition write_volatile (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dst; src ] =>
      ltac:(M.monadic
        (let dst := M.alloc (| dst |) in
        let src := M.alloc (| src |) 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_function (| "core::ptr::write_volatile.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| dst |));
                            M.call_closure (|
                              M.get_function (| "core::mem::align_of", [ T ] |),
                              []
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::volatile_store", [ T ] |),
                [ M.read (| dst |); M.read (| src |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_write_volatile : M.IsFunction "core::ptr::write_volatile" write_volatile.
  
  (*
  pub(crate) const unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
      // FIXME(#75598): Direct use of these intrinsics improves codegen significantly at opt-level <=
      // 1, where the method versions of these operations are not inlined.
      use intrinsics::{
          assume, cttz_nonzero, exact_div, mul_with_overflow, unchecked_rem, unchecked_shl,
          unchecked_shr, unchecked_sub, wrapping_add, wrapping_mul, wrapping_sub,
      };
  
      /// Calculate multiplicative modular inverse of `x` modulo `m`.
      ///
      /// This implementation is tailored for `align_offset` and has following preconditions:
      ///
      /// * `m` is a power-of-two;
      /// * `x < m`; (if `x ≥ m`, pass in `x % m` instead)
      ///
      /// Implementation of this function shall not panic. Ever.
      #[inline]
      const unsafe fn mod_inv(x: usize, m: usize) -> usize {
          /// Multiplicative modular inverse table modulo 2⁴ = 16.
          ///
          /// Note, that this table does not contain values where inverse does not exist (i.e., for
          /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.)
          const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15];
          /// Modulo for which the `INV_TABLE_MOD_16` is intended.
          const INV_TABLE_MOD: usize = 16;
  
          // SAFETY: `m` is required to be a power-of-two, hence non-zero.
          let m_minus_one = unsafe { unchecked_sub(m, 1) };
          let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize;
          let mut mod_gate = INV_TABLE_MOD;
          // We iterate "up" using the following formula:
          //
          // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$
          //
          // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can
          // finally reduce the computation to our desired `m` by taking `inverse mod m`.
          //
          // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop
          // will always finish in at most 4 iterations.
          loop {
              // y = y * (2 - xy) mod n
              //
              // Note, that we use wrapping operations here intentionally – the original formula
              // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod
              // usize::MAX` instead, because we take the result `mod n` at the end
              // anyway.
              if mod_gate >= m {
                  break;
              }
              inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse)));
              let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate);
              if overflow {
                  break;
              }
              mod_gate = new_gate;
          }
          inverse & m_minus_one
      }
  
      let stride = mem::size_of::<T>();
  
      // SAFETY: This is just an inlined `p.addr()` (which is not
      // a `const fn` so we cannot call it).
      // During const eval, we hook this function to ensure that the pointer never
      // has provenance, making this sound.
      let addr: usize = unsafe { mem::transmute(p) };
  
      // SAFETY: `a` is a power-of-two, therefore non-zero.
      let a_minus_one = unsafe { unchecked_sub(a, 1) };
  
      if stride == 0 {
          // SPECIAL_CASE: handle 0-sized types. No matter how many times we step, the address will
          // stay the same, so no offset will be able to align the pointer unless it is already
          // aligned. This branch _will_ be optimized out as `stride` is known at compile-time.
          let p_mod_a = addr & a_minus_one;
          return if p_mod_a == 0 { 0 } else { usize::MAX };
      }
  
      // SAFETY: `stride == 0` case has been handled by the special case above.
      let a_mod_stride = unsafe { unchecked_rem(a, stride) };
      if a_mod_stride == 0 {
          // SPECIAL_CASE: In cases where the `a` is divisible by `stride`, byte offset to align a
          // pointer can be computed more simply through `-p (mod a)`. In the off-chance the byte
          // offset is not a multiple of `stride`, the input pointer was misaligned and no pointer
          // offset will be able to produce a `p` aligned to the specified `a`.
          //
          // The naive `-p (mod a)` equation inhibits LLVM's ability to select instructions
          // like `lea`. We compute `(round_up_to_next_alignment(p, a) - p)` instead. This
          // redistributes operations around the load-bearing, but pessimizing `and` instruction
          // sufficiently for LLVM to be able to utilize the various optimizations it knows about.
          //
          // LLVM handles the branch here particularly nicely. If this branch needs to be evaluated
          // at runtime, it will produce a mask `if addr_mod_stride == 0 { 0 } else { usize::MAX }`
          // in a branch-free way and then bitwise-OR it with whatever result the `-p mod a`
          // computation produces.
  
          let aligned_address = wrapping_add(addr, a_minus_one) & wrapping_sub(0, a);
          let byte_offset = wrapping_sub(aligned_address, addr);
          // FIXME: Remove the assume after <https://github.com/llvm/llvm-project/issues/62502>
          // SAFETY: Masking by `-a` can only affect the low bits, and thus cannot have reduced
          // the value by more than `a-1`, so even though the intermediate values might have
          // wrapped, the byte_offset is always in `[0, a)`.
          unsafe { assume(byte_offset < a) };
  
          // SAFETY: `stride == 0` case has been handled by the special case above.
          let addr_mod_stride = unsafe { unchecked_rem(addr, stride) };
  
          return if addr_mod_stride == 0 {
              // SAFETY: `stride` is non-zero. This is guaranteed to divide exactly as well, because
              // addr has been verified to be aligned to the original type’s alignment requirements.
              unsafe { exact_div(byte_offset, stride) }
          } else {
              usize::MAX
          };
      }
  
      // GENERAL_CASE: From here on we’re handling the very general case where `addr` may be
      // misaligned, there isn’t an obvious relationship between `stride` and `a` that we can take an
      // advantage of, etc. This case produces machine code that isn’t particularly high quality,
      // compared to the special cases above. The code produced here is still within the realm of
      // miracles, given the situations this case has to deal with.
  
      // SAFETY: a is power-of-two hence non-zero. stride == 0 case is handled above.
      // FIXME(const-hack) replace with min
      let gcdpow = unsafe {
          let x = cttz_nonzero(stride);
          let y = cttz_nonzero(a);
          if x < y { x } else { y }
      };
      // SAFETY: gcdpow has an upper-bound that’s at most the number of bits in a `usize`.
      let gcd = unsafe { unchecked_shl(1usize, gcdpow) };
      // SAFETY: gcd is always greater or equal to 1.
      if addr & unsafe { unchecked_sub(gcd, 1) } == 0 {
          // This branch solves for the following linear congruence equation:
          //
          // ` p + so = 0 mod a `
          //
          // `p` here is the pointer value, `s` - stride of `T`, `o` offset in `T`s, and `a` - the
          // requested alignment.
          //
          // With `g = gcd(a, s)`, and the above condition asserting that `p` is also divisible by
          // `g`, we can denote `a' = a/g`, `s' = s/g`, `p' = p/g`, then this becomes equivalent to:
          //
          // ` p' + s'o = 0 mod a' `
          // ` o = (a' - (p' mod a')) * (s'^-1 mod a') `
          //
          // The first term is "the relative alignment of `p` to `a`" (divided by the `g`), the
          // second term is "how does incrementing `p` by `s` bytes change the relative alignment of
          // `p`" (again divided by `g`). Division by `g` is necessary to make the inverse well
          // formed if `a` and `s` are not co-prime.
          //
          // Furthermore, the result produced by this solution is not "minimal", so it is necessary
          // to take the result `o mod lcm(s, a)`. This `lcm(s, a)` is the same as `a'`.
  
          // SAFETY: `gcdpow` has an upper-bound not greater than the number of trailing 0-bits in
          // `a`.
          let a2 = unsafe { unchecked_shr(a, gcdpow) };
          // SAFETY: `a2` is non-zero. Shifting `a` by `gcdpow` cannot shift out any of the set bits
          // in `a` (of which it has exactly one).
          let a2minus1 = unsafe { unchecked_sub(a2, 1) };
          // SAFETY: `gcdpow` has an upper-bound not greater than the number of trailing 0-bits in
          // `a`.
          let s2 = unsafe { unchecked_shr(stride & a_minus_one, gcdpow) };
          // SAFETY: `gcdpow` has an upper-bound not greater than the number of trailing 0-bits in
          // `a`. Furthermore, the subtraction cannot overflow, because `a2 = a >> gcdpow` will
          // always be strictly greater than `(p % a) >> gcdpow`.
          let minusp2 = unsafe { unchecked_sub(a2, unchecked_shr(addr & a_minus_one, gcdpow)) };
          // SAFETY: `a2` is a power-of-two, as proven above. `s2` is strictly less than `a2`
          // because `(s % a) >> gcdpow` is strictly less than `a >> gcdpow`.
          return wrapping_mul(minusp2, unsafe { mod_inv(s2, a2) }) & a2minus1;
      }
  
      // Cannot be aligned at all.
      usize::MAX
  }
  *)
  Definition align_offset (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ p; a ] =>
      ltac:(M.monadic
        (let p := M.alloc (| p |) in
        let a := M.alloc (| a |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ stride :=
                M.alloc (|
                  M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                |) in
              let~ addr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute",
                      [ Ty.apply (Ty.path "*const") [] [ T ]; Ty.path "usize" ]
                    |),
                    [ M.read (| p |) ]
                  |)
                |) in
              let~ a_minus_one :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [ M.read (| a |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (| M.read (| stride |), Value.Integer IntegerKind.Usize 0 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ p_mod_a :=
                                M.alloc (|
                                  BinOp.bit_and (M.read (| addr |)) (M.read (| a_minus_one |))
                                |) in
                              M.return_ (|
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.eq (|
                                                  M.read (| p_mod_a |),
                                                  Value.Integer IntegerKind.Usize 0
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                                      fun γ =>
                                        ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ a_mod_stride :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_rem", [ Ty.path "usize" ] |),
                    [ M.read (| a |); M.read (| stride |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (| a_mod_stride |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ aligned_address :=
                                M.alloc (|
                                  BinOp.bit_and
                                    (M.call_closure (|
                                      M.get_function (|
                                        "core::intrinsics::wrapping_add",
                                        [ Ty.path "usize" ]
                                      |),
                                      [ M.read (| addr |); M.read (| a_minus_one |) ]
                                    |))
                                    (M.call_closure (|
                                      M.get_function (|
                                        "core::intrinsics::wrapping_sub",
                                        [ Ty.path "usize" ]
                                      |),
                                      [ Value.Integer IntegerKind.Usize 0; M.read (| a |) ]
                                    |))
                                |) in
                              let~ byte_offset :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::wrapping_sub",
                                      [ Ty.path "usize" ]
                                    |),
                                    [ M.read (| aligned_address |); M.read (| addr |) ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::assume", [] |),
                                    [ BinOp.lt (| M.read (| byte_offset |), M.read (| a |) |) ]
                                  |)
                                |) in
                              let~ addr_mod_stride :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_rem",
                                      [ Ty.path "usize" ]
                                    |),
                                    [ M.read (| addr |); M.read (| stride |) ]
                                  |)
                                |) in
                              M.return_ (|
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.eq (|
                                                  M.read (| addr_mod_stride |),
                                                  Value.Integer IntegerKind.Usize 0
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::intrinsics::exact_div",
                                                [ Ty.path "usize" ]
                                              |),
                                              [ M.read (| byte_offset |); M.read (| stride |) ]
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ gcdpow :=
                M.copy (|
                  let~ x :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::cttz_nonzero", [ Ty.path "usize" ] |),
                        [ M.read (| stride |) ]
                      |)
                    |) in
                  let~ y :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::cttz_nonzero", [ Ty.path "usize" ] |),
                        [ M.read (| a |) ]
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.alloc (| BinOp.lt (| M.read (| x |), M.read (| y |) |) |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          x));
                      fun γ => ltac:(M.monadic y)
                    ]
                  |)
                |) in
              let~ gcd :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::unchecked_shl",
                      [ Ty.path "usize"; Ty.path "u32" ]
                    |),
                    [ Value.Integer IntegerKind.Usize 1; M.read (| gcdpow |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                BinOp.bit_and
                                  (M.read (| addr |))
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_sub",
                                      [ Ty.path "usize" ]
                                    |),
                                    [ M.read (| gcd |); Value.Integer IntegerKind.Usize 1 ]
                                  |)),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ a2 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_shr",
                                      [ Ty.path "usize"; Ty.path "u32" ]
                                    |),
                                    [ M.read (| a |); M.read (| gcdpow |) ]
                                  |)
                                |) in
                              let~ a2minus1 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_sub",
                                      [ Ty.path "usize" ]
                                    |),
                                    [ M.read (| a2 |); Value.Integer IntegerKind.Usize 1 ]
                                  |)
                                |) in
                              let~ s2 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_shr",
                                      [ Ty.path "usize"; Ty.path "u32" ]
                                    |),
                                    [
                                      BinOp.bit_and
                                        (M.read (| stride |))
                                        (M.read (| a_minus_one |));
                                      M.read (| gcdpow |)
                                    ]
                                  |)
                                |) in
                              let~ minusp2 :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::unchecked_sub",
                                      [ Ty.path "usize" ]
                                    |),
                                    [
                                      M.read (| a2 |);
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::intrinsics::unchecked_shr",
                                          [ Ty.path "usize"; Ty.path "u32" ]
                                        |),
                                        [
                                          BinOp.bit_and
                                            (M.read (| addr |))
                                            (M.read (| a_minus_one |));
                                          M.read (| gcdpow |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              M.return_ (|
                                BinOp.bit_and
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::wrapping_mul",
                                      [ Ty.path "usize" ]
                                    |),
                                    [
                                      M.read (| minusp2 |);
                                      M.call_closure (|
                                        M.get_function (| "core::ptr::align_offset.mod_inv", [] |),
                                        [ M.read (| s2 |); M.read (| a2 |) ]
                                      |)
                                    ]
                                  |))
                                  (M.read (| a2minus1 |))
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.get_constant (| "core::num::MAX" |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_align_offset : M.IsFunction "core::ptr::align_offset" align_offset.
  
  Module align_offset.
    (*
        const unsafe fn mod_inv(x: usize, m: usize) -> usize {
            /// Multiplicative modular inverse table modulo 2⁴ = 16.
            ///
            /// Note, that this table does not contain values where inverse does not exist (i.e., for
            /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.)
            const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15];
            /// Modulo for which the `INV_TABLE_MOD_16` is intended.
            const INV_TABLE_MOD: usize = 16;
    
            // SAFETY: `m` is required to be a power-of-two, hence non-zero.
            let m_minus_one = unsafe { unchecked_sub(m, 1) };
            let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize;
            let mut mod_gate = INV_TABLE_MOD;
            // We iterate "up" using the following formula:
            //
            // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$
            //
            // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can
            // finally reduce the computation to our desired `m` by taking `inverse mod m`.
            //
            // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop
            // will always finish in at most 4 iterations.
            loop {
                // y = y * (2 - xy) mod n
                //
                // Note, that we use wrapping operations here intentionally – the original formula
                // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod
                // usize::MAX` instead, because we take the result `mod n` at the end
                // anyway.
                if mod_gate >= m {
                    break;
                }
                inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse)));
                let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate);
                if overflow {
                    break;
                }
                mod_gate = new_gate;
            }
            inverse & m_minus_one
        }
    *)
    Definition mod_inv (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; m ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let m := M.alloc (| m |) in
          M.read (|
            let~ m_minus_one :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                  [ M.read (| m |); Value.Integer IntegerKind.Usize 1 ]
                |)
              |) in
            let~ inverse :=
              M.alloc (|
                M.rust_cast
                  (M.read (|
                    M.SubPointer.get_array_field (|
                      M.get_constant (| "core::ptr::align_offset::mod_inv::INV_TABLE_MOD_16" |),
                      M.alloc (|
                        BinOp.Wrap.shr (|
                          BinOp.bit_and
                            (M.read (| x |))
                            (BinOp.Wrap.sub (|
                              M.read (|
                                M.get_constant (|
                                  "core::ptr::align_offset::mod_inv::INV_TABLE_MOD"
                                |)
                              |),
                              Value.Integer IntegerKind.Usize 1
                            |)),
                          Value.Integer IntegerKind.I32 1
                        |)
                      |)
                    |)
                  |))
              |) in
            let~ mod_gate :=
              M.copy (| M.get_constant (| "core::ptr::align_offset::mod_inv::INV_TABLE_MOD" |) |) in
            let~ _ :=
              M.loop (|
                ltac:(M.monadic
                  (let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (| M.read (| mod_gate |), M.read (| m |) |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.write (|
                      inverse,
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::wrapping_mul", [ Ty.path "usize" ] |),
                        [
                          M.read (| inverse |);
                          M.call_closure (|
                            M.get_function (|
                              "core::intrinsics::wrapping_sub",
                              [ Ty.path "usize" ]
                            |),
                            [
                              Value.Integer IntegerKind.Usize 2;
                              M.call_closure (|
                                M.get_function (|
                                  "core::intrinsics::wrapping_mul",
                                  [ Ty.path "usize" ]
                                |),
                                [ M.read (| x |); M.read (| inverse |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::mul_with_overflow",
                          [ Ty.path "usize" ]
                        |),
                        [ M.read (| mod_gate |); M.read (| mod_gate |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let new_gate := M.copy (| γ0_0 |) in
                          let overflow := M.copy (| γ0_1 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use overflow in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ := M.write (| mod_gate, M.read (| new_gate |) |) in
                          M.alloc (| Value.Tuple [] |)))
                    ]
                  |)))
              |) in
            M.alloc (| BinOp.bit_and (M.read (| inverse |)) (M.read (| m_minus_one |)) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_mod_inv : M.IsFunction "core::ptr::align_offset::mod_inv" mod_inv.
    
    Module mod_inv.
      Definition value_INV_TABLE_MOD_16 : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.Array
                [
                  Value.Integer IntegerKind.U8 1;
                  Value.Integer IntegerKind.U8 11;
                  Value.Integer IntegerKind.U8 13;
                  Value.Integer IntegerKind.U8 7;
                  Value.Integer IntegerKind.U8 9;
                  Value.Integer IntegerKind.U8 3;
                  Value.Integer IntegerKind.U8 5;
                  Value.Integer IntegerKind.U8 15
                ]
            |))).
      
      Definition value_INV_TABLE_MOD : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 16 |))).
    End mod_inv.
  End align_offset.
  
  (*
  pub fn eq<T: ?Sized>(a: *const T, b: *const T) -> bool {
      a == b
  }
  *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ a; b ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        BinOp.eq (| M.read (| a |), M.read (| b |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_eq : M.IsFunction "core::ptr::eq" eq.
  
  (*
  pub fn addr_eq<T: ?Sized, U: ?Sized>(p: *const T, q: *const U) -> bool {
      (p as *const ()) == (q as *const ())
  }
  *)
  Definition addr_eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; U ], [ p; q ] =>
      ltac:(M.monadic
        (let p := M.alloc (| p |) in
        let q := M.alloc (| q |) in
        BinOp.eq (| M.rust_cast (M.read (| p |)), M.rust_cast (M.read (| q |)) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_addr_eq : M.IsFunction "core::ptr::addr_eq" addr_eq.
  
  (*
  pub fn fn_addr_eq<T: FnPtr, U: FnPtr>(f: T, g: U) -> bool {
      f.addr() == g.addr()
  }
  *)
  Definition fn_addr_eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; U ], [ f; g ] =>
      ltac:(M.monadic
        (let f := M.alloc (| f |) in
        let g := M.alloc (| g |) in
        BinOp.eq (|
          M.call_closure (|
            M.get_trait_method (| "core::marker::FnPtr", T, [], "addr", [] |),
            [ M.read (| f |) ]
          |),
          M.call_closure (|
            M.get_trait_method (| "core::marker::FnPtr", U, [], "addr", [] |),
            [ M.read (| g |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_fn_addr_eq : M.IsFunction "core::ptr::fn_addr_eq" fn_addr_eq.
  
  (*
  pub fn hash<T: ?Sized, S: hash::Hasher>(hashee: *const T, into: &mut S) {
      use crate::hash::Hash;
      hashee.hash(into);
  }
  *)
  Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; _ as S ], [ hashee; into ] =>
      ltac:(M.monadic
        (let hashee := M.alloc (| hashee |) in
        let into := M.alloc (| into |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::hash::Hash",
                  Ty.apply (Ty.path "*const") [] [ T ],
                  [],
                  "hash",
                  [ S ]
                |),
                [ hashee; M.read (| into |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_hash : M.IsFunction "core::ptr::hash" hash.
  
  Module Impl_core_cmp_PartialEq_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn eq(&self, other: &Self) -> bool {
            self.addr() == other.addr()
        }
    *)
    Definition eq (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F 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_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
              [ M.read (| M.read (| self |) |) ]
            |),
            M.call_closure (|
              M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
              [ M.read (| M.read (| other |) |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq F)) ].
  End Impl_core_cmp_PartialEq_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_cmp_Eq_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self F) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_cmp_PartialOrd_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
            self.addr().partial_cmp(&other.addr())
        }
    *)
    Definition partial_cmp (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F 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 "*const") [] [ Ty.tuple [] ],
              [ Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ] ],
              "partial_cmp",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| self |) |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| other |) |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp F)) ].
  End Impl_core_cmp_PartialOrd_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_cmp_Ord_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn cmp(&self, other: &Self) -> Ordering {
            self.addr().cmp(&other.addr())
        }
    *)
    Definition cmp (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F 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 "*const") [] [ Ty.tuple [] ],
              [],
              "cmp",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| self |) |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| other |) |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp F)) ].
  End Impl_core_cmp_Ord_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_hash_Hash_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn hash<HH: hash::Hasher>(&self, state: &mut HH) {
            state.write_usize(self.addr() as _)
        }
    *)
    Definition hash (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F in
      match ε, τ, α with
      | [], [ HH ], [ 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::Hasher", HH, [], "write_usize", [] |),
            [
              M.read (| state |);
              M.rust_cast
                (M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| self |) |) ]
                |))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash F)) ].
  End Impl_core_hash_Hash_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_fmt_Pointer_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::pointer_fmt_inner(self.addr() as _, f)
        }
    *)
    Definition fmt (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F 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_function (| "core::fmt::pointer_fmt_inner", [] |),
            [
              M.rust_cast
                (M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| self |) |) ]
                |));
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::fmt::Pointer"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt F)) ].
  End Impl_core_fmt_Pointer_where_core_marker_FnPtr_F_for_F.
  
  Module Impl_core_fmt_Debug_where_core_marker_FnPtr_F_for_F.
    Definition Self (F : Ty.t) : Ty.t := F.
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::pointer_fmt_inner(self.addr() as _, f)
        }
    *)
    Definition fmt (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self F 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_function (| "core::fmt::pointer_fmt_inner", [] |),
            [
              M.rust_cast
                (M.call_closure (|
                  M.get_trait_method (| "core::marker::FnPtr", F, [], "addr", [] |),
                  [ M.read (| M.read (| self |) |) ]
                |));
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (F : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self F)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt F)) ].
  End Impl_core_fmt_Debug_where_core_marker_FnPtr_F_for_F.
End ptr.
