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

Module hint.
  Module unreachable_unchecked.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| UnOp.not (| Value.Bool false |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: hint::unreachable_unchecked must never be reached"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::hint::unreachable_unchecked::precondition_check" precondition_check.
  End unreachable_unchecked.
  
  Module assert_unchecked.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ cond ] =>
        ltac:(M.monadic
          (let cond := M.alloc (| cond |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| UnOp.not (| M.read (| cond |) |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: hint::assert_unchecked must never be called when the condition is false"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::hint::assert_unchecked::precondition_check" precondition_check.
  End assert_unchecked.
End hint.

Module intrinsics.
  Module copy_nonoverlapping.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ src; dst; size; align; count ] =>
        ltac:(M.monadic
          (let src := M.alloc (| src |) in
          let dst := M.alloc (| dst |) in
          let size := M.alloc (| size |) in
          let align := M.alloc (| align |) in
          let count := M.alloc (| count |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::ub_checks::is_aligned_and_not_null",
                                    []
                                  |),
                                  [ M.read (| src |); M.read (| align |) ]
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::ub_checks::is_aligned_and_not_null",
                                      []
                                    |),
                                    [
                                      (* MutToConstPointer *) M.pointer_coercion (M.read (| dst |));
                                      M.read (| align |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_function (| "core::ub_checks::is_nonoverlapping", [] |),
                                  [
                                    M.read (| src |);
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| dst |));
                                    M.read (| size |);
                                    M.read (| count |)
                                  ]
                                |)))
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::intrinsics::copy_nonoverlapping::precondition_check" precondition_check.
  End copy_nonoverlapping.
  
  Module copy.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ src; dst; align ] =>
        ltac:(M.monadic
          (let src := M.alloc (| src |) in
          let dst := M.alloc (| dst |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            LogicalOp.and (|
                              M.call_closure (|
                                M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                                [ M.read (| src |); M.read (| align |) ]
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_function (|
                                    "core::ub_checks::is_aligned_and_not_null",
                                    []
                                  |),
                                  [
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| dst |));
                                    M.read (| align |)
                                  ]
                                |)))
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::copy requires that both pointer arguments are aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::intrinsics::copy::precondition_check" precondition_check.
  End copy.
  
  Module write_bytes.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [ M.read (| addr |); M.read (| align |) ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::write_bytes requires that the destination pointer is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::intrinsics::write_bytes::precondition_check" precondition_check.
  End write_bytes.
End intrinsics.

Module ptr.
  Module swap_nonoverlapping.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x; y; size; align; count ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          let y := M.alloc (| y |) in
          let size := M.alloc (| size |) in
          let align := M.alloc (| align |) in
          let count := M.alloc (| count |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::ub_checks::is_aligned_and_not_null",
                                    []
                                  |),
                                  [
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| x |));
                                    M.read (| align |)
                                  ]
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::ub_checks::is_aligned_and_not_null",
                                      []
                                    |),
                                    [
                                      (* MutToConstPointer *) M.pointer_coercion (M.read (| y |));
                                      M.read (| align |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_function (| "core::ub_checks::is_nonoverlapping", [] |),
                                  [
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| x |));
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| y |));
                                    M.read (| size |);
                                    M.read (| count |)
                                  ]
                                |)))
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::swap_nonoverlapping requires that both pointer arguments are aligned and non-null and the specified memory ranges do not overlap"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::swap_nonoverlapping::precondition_check" precondition_check.
  End swap_nonoverlapping.
  
  Module replace.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [ M.read (| addr |); M.read (| align |) ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::replace requires that the pointer argument is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::replace::precondition_check" precondition_check.
  End replace.
  
  Module read.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [ M.read (| addr |); M.read (| align |) ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::read requires that the pointer argument is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::read::precondition_check" precondition_check.
  End read.
  
  Module write.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [
                                (* MutToConstPointer *) M.pointer_coercion (M.read (| addr |));
                                M.read (| align |)
                              ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::write requires that the pointer argument is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::write::precondition_check" precondition_check.
  End write.
  
  Module read_volatile.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [ M.read (| addr |); M.read (| align |) ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::read_volatile requires that the pointer argument is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::read_volatile::precondition_check" precondition_check.
  End read_volatile.
  
  Module write_volatile.
    (*
                const fn precondition_check($($name:$ty),* ) {
                    if !$e {
                        ::core::panicking::panic_nounwind(
                            concat!("unsafe precondition(s) violated: ", $message)
                        );
                    }
                }
    *)
    Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr; align ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          let align := M.alloc (| align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::is_aligned_and_not_null", [] |),
                              [
                                (* MutToConstPointer *) M.pointer_coercion (M.read (| addr |));
                                M.read (| align |)
                              ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_nounwind", [] |),
                          [
                            M.read (|
                              Value.String
                                "unsafe precondition(s) violated: ptr::write_volatile requires that the pointer argument is aligned and non-null"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_precondition_check :
      M.IsFunction "core::ptr::write_volatile::precondition_check" precondition_check.
  End write_volatile.
End ptr.

Module ub_checks.
  (*
  pub(crate) const fn check_language_ub() -> bool {
      #[inline]
      fn runtime() -> bool {
          // Disable UB checks in Miri.
          !cfg!(miri)
      }
  
      #[inline]
      const fn comptime() -> bool {
          // Always disable UB checks.
          false
      }
  
      // Only used for UB checks so we may const_eval_select.
      intrinsics::ub_checks() && const_eval_select((), comptime, runtime)
  }
  *)
  Definition check_language_ub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (LogicalOp.and (|
          M.call_closure (| M.get_function (| "core::intrinsics::ub_checks", [] |), [] |),
          ltac:(M.monadic
            (M.call_closure (|
              M.get_function (|
                "core::intrinsics::const_eval_select",
                [
                  Ty.tuple [];
                  Ty.function [] (Ty.path "bool");
                  Ty.function [] (Ty.path "bool");
                  Ty.path "bool"
                ]
              |),
              [
                Value.Tuple [];
                M.get_function (| "core::ub_checks::check_language_ub.comptime", [] |);
                M.get_function (| "core::ub_checks::check_language_ub.runtime", [] |)
              ]
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_check_language_ub :
    M.IsFunction "core::ub_checks::check_language_ub" check_language_ub.
  
  Module check_language_ub.
    (*
        fn runtime() -> bool {
            // Disable UB checks in Miri.
            !cfg!(miri)
        }
    *)
    Definition runtime (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (UnOp.not (| Value.Bool false |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_runtime : M.IsFunction "core::ub_checks::check_language_ub::runtime" runtime.
    
    (*
        const fn comptime() -> bool {
            // Always disable UB checks.
            false
        }
    *)
    Definition comptime (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.Bool false))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_comptime : M.IsFunction "core::ub_checks::check_language_ub::comptime" comptime.
  End check_language_ub.
  
  (*
  pub(crate) const fn is_aligned_and_not_null(ptr: *const (), align: usize) -> bool {
      !ptr.is_null() && ptr.is_aligned_to(align)
  }
  *)
  Definition is_aligned_and_not_null (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ ptr; align ] =>
      ltac:(M.monadic
        (let ptr := M.alloc (| ptr |) in
        let align := M.alloc (| align |) in
        LogicalOp.and (|
          UnOp.not (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ],
                "is_null",
                []
              |),
              [ M.read (| ptr |) ]
            |)
          |),
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ],
                "is_aligned_to",
                []
              |),
              [ M.read (| ptr |); M.read (| align |) ]
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_aligned_and_not_null :
    M.IsFunction "core::ub_checks::is_aligned_and_not_null" is_aligned_and_not_null.
  
  (*
  pub(crate) const fn is_valid_allocation_size(size: usize, len: usize) -> bool {
      let max_len = if size == 0 { usize::MAX } else { isize::MAX as usize / size };
      len <= max_len
  }
  *)
  Definition is_valid_allocation_size (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ size; len ] =>
      ltac:(M.monadic
        (let size := M.alloc (| size |) in
        let len := M.alloc (| len |) in
        M.read (|
          let~ max_len :=
            M.copy (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (| M.read (| size |), Value.Integer IntegerKind.Usize 0 |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.get_constant (| "core::num::MAX" |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        BinOp.Wrap.div (|
                          M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |)),
                          M.read (| size |)
                        |)
                      |)))
                ]
              |)
            |) in
          M.alloc (| BinOp.le (| M.read (| len |), M.read (| max_len |) |) |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_valid_allocation_size :
    M.IsFunction "core::ub_checks::is_valid_allocation_size" is_valid_allocation_size.
  
  (*
  pub(crate) const fn is_nonoverlapping(
      src: *const (),
      dst: *const (),
      size: usize,
      count: usize,
  ) -> bool {
      #[inline]
      fn runtime(src: *const (), dst: *const (), size: usize, count: usize) -> bool {
          let src_usize = src.addr();
          let dst_usize = dst.addr();
          let Some(size) = size.checked_mul(count) else {
              crate::panicking::panic_nounwind(
                  "is_nonoverlapping: `size_of::<T>() * count` overflows a usize",
              )
          };
          let diff = src_usize.abs_diff(dst_usize);
          // If the absolute distance between the ptrs is at least as big as the size of the buffer,
          // they do not overlap.
          diff >= size
      }
  
      #[inline]
      const fn comptime(_: *const (), _: *const (), _: usize, _: usize) -> bool {
          true
      }
  
      // This is just for safety checks so we can const_eval_select.
      const_eval_select((src, dst, size, count), comptime, runtime)
  }
  *)
  Definition is_nonoverlapping (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ src; dst; size; count ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) in
        let dst := M.alloc (| dst |) in
        let size := M.alloc (| size |) in
        let count := M.alloc (| count |) in
        M.call_closure (|
          M.get_function (|
            "core::intrinsics::const_eval_select",
            [
              Ty.tuple
                [
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.path "usize";
                  Ty.path "usize"
                ];
              Ty.function
                [
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.path "usize";
                  Ty.path "usize"
                ]
                (Ty.path "bool");
              Ty.function
                [
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ];
                  Ty.path "usize";
                  Ty.path "usize"
                ]
                (Ty.path "bool");
              Ty.path "bool"
            ]
          |),
          [
            Value.Tuple
              [ M.read (| src |); M.read (| dst |); M.read (| size |); M.read (| count |) ];
            M.get_function (| "core::ub_checks::is_nonoverlapping.comptime", [] |);
            M.get_function (| "core::ub_checks::is_nonoverlapping.runtime", [] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_nonoverlapping :
    M.IsFunction "core::ub_checks::is_nonoverlapping" is_nonoverlapping.
  
  Module is_nonoverlapping.
    (*
        fn runtime(src: *const (), dst: *const (), size: usize, count: usize) -> bool {
            let src_usize = src.addr();
            let dst_usize = dst.addr();
            let Some(size) = size.checked_mul(count) else {
                crate::panicking::panic_nounwind(
                    "is_nonoverlapping: `size_of::<T>() * count` overflows a usize",
                )
            };
            let diff = src_usize.abs_diff(dst_usize);
            // If the absolute distance between the ptrs is at least as big as the size of the buffer,
            // they do not overlap.
            diff >= size
        }
    *)
    Definition runtime (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ src; dst; size; count ] =>
        ltac:(M.monadic
          (let src := M.alloc (| src |) in
          let dst := M.alloc (| dst |) in
          let size := M.alloc (| size |) in
          let count := M.alloc (| count |) in
          M.read (|
            let~ src_usize :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ],
                    "addr",
                    []
                  |),
                  [ M.read (| src |) ]
                |)
              |) in
            let~ dst_usize :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "*const") [] [ Ty.tuple [] ],
                    "addr",
                    []
                  |),
                  [ M.read (| dst |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "usize", "checked_mul", [] |),
                  [ M.read (| size |); M.read (| count |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let size := M.copy (| γ0_0 |) in
                    let~ diff :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "usize", "abs_diff", [] |),
                          [ M.read (| src_usize |); M.read (| dst_usize |) ]
                        |)
                      |) in
                    M.alloc (| BinOp.ge (| M.read (| diff |), M.read (| size |) |) |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_runtime : M.IsFunction "core::ub_checks::is_nonoverlapping::runtime" runtime.
    
    (*
        const fn comptime(_: *const (), _: *const (), _: usize, _: usize) -> bool {
            true
        }
    *)
    Definition comptime (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ β0; β1; β2; β3 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          let β1 := M.alloc (| β1 |) in
          let β2 := M.alloc (| β2 |) in
          let β3 := M.alloc (| β3 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    β1,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            β2,
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    β3,
                                    [ fun γ => ltac:(M.monadic (Value.Bool true)) ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_comptime : M.IsFunction "core::ub_checks::is_nonoverlapping::comptime" comptime.
  End is_nonoverlapping.
End ub_checks.

Module char.
  Module convert.
    Module from_u32_unchecked.
      (*
                  const fn precondition_check($($name:$ty),* ) {
                      if !$e {
                          ::core::panicking::panic_nounwind(
                              concat!("unsafe precondition(s) violated: ", $message)
                          );
                      }
                  }
      *)
      Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ i ] =>
          ltac:(M.monadic
            (let i := M.alloc (| i |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [
                                      Ty.path "char";
                                      Ty.path "core::char::convert::CharTryFromError"
                                    ],
                                  "is_ok",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::char::convert::char_try_from_u32",
                                        []
                                      |),
                                      [ M.read (| i |) ]
                                    |)
                                  |)
                                ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_nounwind", [] |),
                            [
                              M.read (|
                                Value.String
                                  "unsafe precondition(s) violated: invalid value for `char`"
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_precondition_check :
        M.IsFunction
          "core::char::convert::from_u32_unchecked::precondition_check"
          precondition_check.
    End from_u32_unchecked.
  End convert.
End char.

Module slice.
  Module raw.
    Module from_raw_parts.
      (*
                  const fn precondition_check($($name:$ty),* ) {
                      if !$e {
                          ::core::panicking::panic_nounwind(
                              concat!("unsafe precondition(s) violated: ", $message)
                          );
                      }
                  }
      *)
      Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ data; size; align; len ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let size := M.alloc (| size |) in
            let align := M.alloc (| align |) in
            let len := M.alloc (| len |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::ub_checks::is_aligned_and_not_null",
                                    []
                                  |),
                                  [
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| data |));
                                    M.read (| align |)
                                  ]
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::ub_checks::is_valid_allocation_size",
                                      []
                                    |),
                                    [ M.read (| size |); M.read (| len |) ]
                                  |)))
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_nounwind", [] |),
                            [
                              M.read (|
                                Value.String
                                  "unsafe precondition(s) violated: slice::from_raw_parts requires the pointer to be aligned and non-null, and the total size of the slice not to exceed `isize::MAX`"
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_precondition_check :
        M.IsFunction "core::slice::raw::from_raw_parts::precondition_check" precondition_check.
    End from_raw_parts.
    
    Module from_raw_parts_mut.
      (*
                  const fn precondition_check($($name:$ty),* ) {
                      if !$e {
                          ::core::panicking::panic_nounwind(
                              concat!("unsafe precondition(s) violated: ", $message)
                          );
                      }
                  }
      *)
      Definition precondition_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ data; size; align; len ] =>
          ltac:(M.monadic
            (let data := M.alloc (| data |) in
            let size := M.alloc (| size |) in
            let align := M.alloc (| align |) in
            let len := M.alloc (| len |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::ub_checks::is_aligned_and_not_null",
                                    []
                                  |),
                                  [
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| data |));
                                    M.read (| align |)
                                  ]
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_function (|
                                      "core::ub_checks::is_valid_allocation_size",
                                      []
                                    |),
                                    [ M.read (| size |); M.read (| len |) ]
                                  |)))
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_nounwind", [] |),
                            [
                              M.read (|
                                Value.String
                                  "unsafe precondition(s) violated: slice::from_raw_parts_mut requires the pointer to be aligned and non-null, and the total size of the slice not to exceed `isize::MAX`"
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_precondition_check :
        M.IsFunction "core::slice::raw::from_raw_parts_mut::precondition_check" precondition_check.
    End from_raw_parts_mut.
  End raw.
End slice.
