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

Module hint.
  (*
  pub const unsafe fn unreachable_unchecked() -> ! {
      ub_checks::assert_unsafe_precondition!(
          check_language_ub,
          "hint::unreachable_unchecked must never be reached",
          () => false
      );
      // SAFETY: the safety contract for `intrinsics::unreachable` must
      // be upheld by the caller.
      unsafe { intrinsics::unreachable() }
  }
  *)
  Definition unreachable_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      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::hint::unreachable_unchecked.precondition_check",
                            []
                          |),
                          []
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (| M.get_function (| "core::intrinsics::unreachable", [] |), [] |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_unreachable_unchecked :
    M.IsFunction "core::hint::unreachable_unchecked" unreachable_unchecked.
  
  (*
  pub const unsafe fn assert_unchecked(cond: bool) {
      // SAFETY: The caller promised `cond` is true.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "hint::assert_unchecked must never be called when the condition is false",
              (cond: bool = cond) => cond,
          );
          crate::intrinsics::assume(cond);
      }
  }
  *)
  Definition assert_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ cond ] =>
      ltac:(M.monadic
        (let cond := M.alloc (| cond |) 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::hint::assert_unchecked.precondition_check",
                            []
                          |),
                          [ M.read (| cond |) ]
                        |)
                      |) 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::assume", [] |),
                [ M.read (| cond |) ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_assert_unchecked : M.IsFunction "core::hint::assert_unchecked" assert_unchecked.
  
  (*
  pub fn spin_loop() {
      #[cfg(target_arch = "x86")]
      {
          // SAFETY: the `cfg` attr ensures that we only execute this on x86 targets.
          unsafe { crate::arch::x86::_mm_pause() };
      }
  
      #[cfg(target_arch = "x86_64")]
      {
          // SAFETY: the `cfg` attr ensures that we only execute this on x86_64 targets.
          unsafe { crate::arch::x86_64::_mm_pause() };
      }
  
      #[cfg(target_arch = "riscv32")]
      {
          crate::arch::riscv32::pause();
      }
  
      #[cfg(target_arch = "riscv64")]
      {
          crate::arch::riscv64::pause();
      }
  
      #[cfg(any(target_arch = "aarch64", target_arch = "arm64ec"))]
      {
          // SAFETY: the `cfg` attr ensures that we only execute this on aarch64 targets.
          unsafe { crate::arch::aarch64::__isb(crate::arch::aarch64::SY) };
      }
  
      #[cfg(all(target_arch = "arm", target_feature = "v6"))]
      {
          // SAFETY: the `cfg` attr ensures that we only execute this on arm targets
          // with support for the v6 feature.
          unsafe { crate::arch::arm::__yield() };
      }
  }
  *)
  Definition spin_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::core_arch::x86::sse2::_mm_pause", [] |),
                []
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_spin_loop : M.IsFunction "core::hint::spin_loop" spin_loop.
  
  (*
  pub const fn black_box<T>(dummy: T) -> T {
      crate::intrinsics::black_box(dummy)
  }
  *)
  Definition black_box (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dummy ] =>
      ltac:(M.monadic
        (let dummy := M.alloc (| dummy |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::black_box", [ T ] |),
          [ M.read (| dummy |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_black_box : M.IsFunction "core::hint::black_box" black_box.
  
  (*
  pub const fn must_use<T>(value: T) -> T {
      value
  }
  *)
  Definition must_use (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ value ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        M.read (| value |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_must_use : M.IsFunction "core::hint::must_use" must_use.
End hint.
