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

Module intrinsics.
  (*
  pub unsafe fn drop_in_place<T: ?Sized>(to_drop: *mut T) {
      // SAFETY: see `ptr::drop_in_place`
      unsafe { crate::ptr::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::intrinsics::drop_in_place" drop_in_place.
  
  Parameter atomic_cxchg_relaxed_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_relaxed_relaxed :
    M.IsFunction "core::intrinsics::atomic_cxchg_relaxed_relaxed" atomic_cxchg_relaxed_relaxed.
  
  Parameter atomic_cxchg_relaxed_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_relaxed_acquire :
    M.IsFunction "core::intrinsics::atomic_cxchg_relaxed_acquire" atomic_cxchg_relaxed_acquire.
  
  Parameter atomic_cxchg_relaxed_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_relaxed_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchg_relaxed_seqcst" atomic_cxchg_relaxed_seqcst.
  
  Parameter atomic_cxchg_acquire_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acquire_relaxed :
    M.IsFunction "core::intrinsics::atomic_cxchg_acquire_relaxed" atomic_cxchg_acquire_relaxed.
  
  Parameter atomic_cxchg_acquire_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acquire_acquire :
    M.IsFunction "core::intrinsics::atomic_cxchg_acquire_acquire" atomic_cxchg_acquire_acquire.
  
  Parameter atomic_cxchg_acquire_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acquire_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchg_acquire_seqcst" atomic_cxchg_acquire_seqcst.
  
  Parameter atomic_cxchg_release_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_release_relaxed :
    M.IsFunction "core::intrinsics::atomic_cxchg_release_relaxed" atomic_cxchg_release_relaxed.
  
  Parameter atomic_cxchg_release_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_release_acquire :
    M.IsFunction "core::intrinsics::atomic_cxchg_release_acquire" atomic_cxchg_release_acquire.
  
  Parameter atomic_cxchg_release_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_release_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchg_release_seqcst" atomic_cxchg_release_seqcst.
  
  Parameter atomic_cxchg_acqrel_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acqrel_relaxed :
    M.IsFunction "core::intrinsics::atomic_cxchg_acqrel_relaxed" atomic_cxchg_acqrel_relaxed.
  
  Parameter atomic_cxchg_acqrel_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acqrel_acquire :
    M.IsFunction "core::intrinsics::atomic_cxchg_acqrel_acquire" atomic_cxchg_acqrel_acquire.
  
  Parameter atomic_cxchg_acqrel_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_acqrel_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchg_acqrel_seqcst" atomic_cxchg_acqrel_seqcst.
  
  Parameter atomic_cxchg_seqcst_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_seqcst_relaxed :
    M.IsFunction "core::intrinsics::atomic_cxchg_seqcst_relaxed" atomic_cxchg_seqcst_relaxed.
  
  Parameter atomic_cxchg_seqcst_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_seqcst_acquire :
    M.IsFunction "core::intrinsics::atomic_cxchg_seqcst_acquire" atomic_cxchg_seqcst_acquire.
  
  Parameter atomic_cxchg_seqcst_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchg_seqcst_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchg_seqcst_seqcst" atomic_cxchg_seqcst_seqcst.
  
  Parameter atomic_cxchgweak_relaxed_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_relaxed_relaxed :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_relaxed_relaxed"
      atomic_cxchgweak_relaxed_relaxed.
  
  Parameter atomic_cxchgweak_relaxed_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_relaxed_acquire :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_relaxed_acquire"
      atomic_cxchgweak_relaxed_acquire.
  
  Parameter atomic_cxchgweak_relaxed_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_relaxed_seqcst :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_relaxed_seqcst"
      atomic_cxchgweak_relaxed_seqcst.
  
  Parameter atomic_cxchgweak_acquire_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acquire_relaxed :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_acquire_relaxed"
      atomic_cxchgweak_acquire_relaxed.
  
  Parameter atomic_cxchgweak_acquire_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acquire_acquire :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_acquire_acquire"
      atomic_cxchgweak_acquire_acquire.
  
  Parameter atomic_cxchgweak_acquire_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acquire_seqcst :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_acquire_seqcst"
      atomic_cxchgweak_acquire_seqcst.
  
  Parameter atomic_cxchgweak_release_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_release_relaxed :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_release_relaxed"
      atomic_cxchgweak_release_relaxed.
  
  Parameter atomic_cxchgweak_release_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_release_acquire :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_release_acquire"
      atomic_cxchgweak_release_acquire.
  
  Parameter atomic_cxchgweak_release_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_release_seqcst :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_release_seqcst"
      atomic_cxchgweak_release_seqcst.
  
  Parameter atomic_cxchgweak_acqrel_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acqrel_relaxed :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_acqrel_relaxed"
      atomic_cxchgweak_acqrel_relaxed.
  
  Parameter atomic_cxchgweak_acqrel_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acqrel_acquire :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_acqrel_acquire"
      atomic_cxchgweak_acqrel_acquire.
  
  Parameter atomic_cxchgweak_acqrel_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_acqrel_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchgweak_acqrel_seqcst" atomic_cxchgweak_acqrel_seqcst.
  
  Parameter atomic_cxchgweak_seqcst_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_seqcst_relaxed :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_seqcst_relaxed"
      atomic_cxchgweak_seqcst_relaxed.
  
  Parameter atomic_cxchgweak_seqcst_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_seqcst_acquire :
    M.IsFunction
      "core::intrinsics::atomic_cxchgweak_seqcst_acquire"
      atomic_cxchgweak_seqcst_acquire.
  
  Parameter atomic_cxchgweak_seqcst_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_cxchgweak_seqcst_seqcst :
    M.IsFunction "core::intrinsics::atomic_cxchgweak_seqcst_seqcst" atomic_cxchgweak_seqcst_seqcst.
  
  Parameter atomic_load_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_load_seqcst :
    M.IsFunction "core::intrinsics::atomic_load_seqcst" atomic_load_seqcst.
  
  Parameter atomic_load_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_load_acquire :
    M.IsFunction "core::intrinsics::atomic_load_acquire" atomic_load_acquire.
  
  Parameter atomic_load_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_load_relaxed :
    M.IsFunction "core::intrinsics::atomic_load_relaxed" atomic_load_relaxed.
  
  Parameter atomic_load_unordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_load_unordered :
    M.IsFunction "core::intrinsics::atomic_load_unordered" atomic_load_unordered.
  
  Parameter atomic_store_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_store_seqcst :
    M.IsFunction "core::intrinsics::atomic_store_seqcst" atomic_store_seqcst.
  
  Parameter atomic_store_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_store_release :
    M.IsFunction "core::intrinsics::atomic_store_release" atomic_store_release.
  
  Parameter atomic_store_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_store_relaxed :
    M.IsFunction "core::intrinsics::atomic_store_relaxed" atomic_store_relaxed.
  
  Parameter atomic_store_unordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_store_unordered :
    M.IsFunction "core::intrinsics::atomic_store_unordered" atomic_store_unordered.
  
  Parameter atomic_xchg_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xchg_seqcst :
    M.IsFunction "core::intrinsics::atomic_xchg_seqcst" atomic_xchg_seqcst.
  
  Parameter atomic_xchg_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xchg_acquire :
    M.IsFunction "core::intrinsics::atomic_xchg_acquire" atomic_xchg_acquire.
  
  Parameter atomic_xchg_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xchg_release :
    M.IsFunction "core::intrinsics::atomic_xchg_release" atomic_xchg_release.
  
  Parameter atomic_xchg_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xchg_acqrel :
    M.IsFunction "core::intrinsics::atomic_xchg_acqrel" atomic_xchg_acqrel.
  
  Parameter atomic_xchg_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xchg_relaxed :
    M.IsFunction "core::intrinsics::atomic_xchg_relaxed" atomic_xchg_relaxed.
  
  Parameter atomic_xadd_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xadd_seqcst :
    M.IsFunction "core::intrinsics::atomic_xadd_seqcst" atomic_xadd_seqcst.
  
  Parameter atomic_xadd_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xadd_acquire :
    M.IsFunction "core::intrinsics::atomic_xadd_acquire" atomic_xadd_acquire.
  
  Parameter atomic_xadd_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xadd_release :
    M.IsFunction "core::intrinsics::atomic_xadd_release" atomic_xadd_release.
  
  Parameter atomic_xadd_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xadd_acqrel :
    M.IsFunction "core::intrinsics::atomic_xadd_acqrel" atomic_xadd_acqrel.
  
  Parameter atomic_xadd_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xadd_relaxed :
    M.IsFunction "core::intrinsics::atomic_xadd_relaxed" atomic_xadd_relaxed.
  
  Parameter atomic_xsub_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xsub_seqcst :
    M.IsFunction "core::intrinsics::atomic_xsub_seqcst" atomic_xsub_seqcst.
  
  Parameter atomic_xsub_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xsub_acquire :
    M.IsFunction "core::intrinsics::atomic_xsub_acquire" atomic_xsub_acquire.
  
  Parameter atomic_xsub_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xsub_release :
    M.IsFunction "core::intrinsics::atomic_xsub_release" atomic_xsub_release.
  
  Parameter atomic_xsub_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xsub_acqrel :
    M.IsFunction "core::intrinsics::atomic_xsub_acqrel" atomic_xsub_acqrel.
  
  Parameter atomic_xsub_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xsub_relaxed :
    M.IsFunction "core::intrinsics::atomic_xsub_relaxed" atomic_xsub_relaxed.
  
  Parameter atomic_and_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_and_seqcst :
    M.IsFunction "core::intrinsics::atomic_and_seqcst" atomic_and_seqcst.
  
  Parameter atomic_and_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_and_acquire :
    M.IsFunction "core::intrinsics::atomic_and_acquire" atomic_and_acquire.
  
  Parameter atomic_and_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_and_release :
    M.IsFunction "core::intrinsics::atomic_and_release" atomic_and_release.
  
  Parameter atomic_and_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_and_acqrel :
    M.IsFunction "core::intrinsics::atomic_and_acqrel" atomic_and_acqrel.
  
  Parameter atomic_and_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_and_relaxed :
    M.IsFunction "core::intrinsics::atomic_and_relaxed" atomic_and_relaxed.
  
  Parameter atomic_nand_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_nand_seqcst :
    M.IsFunction "core::intrinsics::atomic_nand_seqcst" atomic_nand_seqcst.
  
  Parameter atomic_nand_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_nand_acquire :
    M.IsFunction "core::intrinsics::atomic_nand_acquire" atomic_nand_acquire.
  
  Parameter atomic_nand_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_nand_release :
    M.IsFunction "core::intrinsics::atomic_nand_release" atomic_nand_release.
  
  Parameter atomic_nand_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_nand_acqrel :
    M.IsFunction "core::intrinsics::atomic_nand_acqrel" atomic_nand_acqrel.
  
  Parameter atomic_nand_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_nand_relaxed :
    M.IsFunction "core::intrinsics::atomic_nand_relaxed" atomic_nand_relaxed.
  
  Parameter atomic_or_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_or_seqcst :
    M.IsFunction "core::intrinsics::atomic_or_seqcst" atomic_or_seqcst.
  
  Parameter atomic_or_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_or_acquire :
    M.IsFunction "core::intrinsics::atomic_or_acquire" atomic_or_acquire.
  
  Parameter atomic_or_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_or_release :
    M.IsFunction "core::intrinsics::atomic_or_release" atomic_or_release.
  
  Parameter atomic_or_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_or_acqrel :
    M.IsFunction "core::intrinsics::atomic_or_acqrel" atomic_or_acqrel.
  
  Parameter atomic_or_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_or_relaxed :
    M.IsFunction "core::intrinsics::atomic_or_relaxed" atomic_or_relaxed.
  
  Parameter atomic_xor_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xor_seqcst :
    M.IsFunction "core::intrinsics::atomic_xor_seqcst" atomic_xor_seqcst.
  
  Parameter atomic_xor_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xor_acquire :
    M.IsFunction "core::intrinsics::atomic_xor_acquire" atomic_xor_acquire.
  
  Parameter atomic_xor_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xor_release :
    M.IsFunction "core::intrinsics::atomic_xor_release" atomic_xor_release.
  
  Parameter atomic_xor_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xor_acqrel :
    M.IsFunction "core::intrinsics::atomic_xor_acqrel" atomic_xor_acqrel.
  
  Parameter atomic_xor_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_xor_relaxed :
    M.IsFunction "core::intrinsics::atomic_xor_relaxed" atomic_xor_relaxed.
  
  Parameter atomic_max_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_max_seqcst :
    M.IsFunction "core::intrinsics::atomic_max_seqcst" atomic_max_seqcst.
  
  Parameter atomic_max_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_max_acquire :
    M.IsFunction "core::intrinsics::atomic_max_acquire" atomic_max_acquire.
  
  Parameter atomic_max_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_max_release :
    M.IsFunction "core::intrinsics::atomic_max_release" atomic_max_release.
  
  Parameter atomic_max_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_max_acqrel :
    M.IsFunction "core::intrinsics::atomic_max_acqrel" atomic_max_acqrel.
  
  Parameter atomic_max_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_max_relaxed :
    M.IsFunction "core::intrinsics::atomic_max_relaxed" atomic_max_relaxed.
  
  Parameter atomic_min_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_min_seqcst :
    M.IsFunction "core::intrinsics::atomic_min_seqcst" atomic_min_seqcst.
  
  Parameter atomic_min_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_min_acquire :
    M.IsFunction "core::intrinsics::atomic_min_acquire" atomic_min_acquire.
  
  Parameter atomic_min_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_min_release :
    M.IsFunction "core::intrinsics::atomic_min_release" atomic_min_release.
  
  Parameter atomic_min_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_min_acqrel :
    M.IsFunction "core::intrinsics::atomic_min_acqrel" atomic_min_acqrel.
  
  Parameter atomic_min_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_min_relaxed :
    M.IsFunction "core::intrinsics::atomic_min_relaxed" atomic_min_relaxed.
  
  Parameter atomic_umin_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umin_seqcst :
    M.IsFunction "core::intrinsics::atomic_umin_seqcst" atomic_umin_seqcst.
  
  Parameter atomic_umin_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umin_acquire :
    M.IsFunction "core::intrinsics::atomic_umin_acquire" atomic_umin_acquire.
  
  Parameter atomic_umin_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umin_release :
    M.IsFunction "core::intrinsics::atomic_umin_release" atomic_umin_release.
  
  Parameter atomic_umin_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umin_acqrel :
    M.IsFunction "core::intrinsics::atomic_umin_acqrel" atomic_umin_acqrel.
  
  Parameter atomic_umin_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umin_relaxed :
    M.IsFunction "core::intrinsics::atomic_umin_relaxed" atomic_umin_relaxed.
  
  Parameter atomic_umax_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umax_seqcst :
    M.IsFunction "core::intrinsics::atomic_umax_seqcst" atomic_umax_seqcst.
  
  Parameter atomic_umax_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umax_acquire :
    M.IsFunction "core::intrinsics::atomic_umax_acquire" atomic_umax_acquire.
  
  Parameter atomic_umax_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umax_release :
    M.IsFunction "core::intrinsics::atomic_umax_release" atomic_umax_release.
  
  Parameter atomic_umax_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umax_acqrel :
    M.IsFunction "core::intrinsics::atomic_umax_acqrel" atomic_umax_acqrel.
  
  Parameter atomic_umax_relaxed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_umax_relaxed :
    M.IsFunction "core::intrinsics::atomic_umax_relaxed" atomic_umax_relaxed.
  
  Parameter atomic_fence_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_fence_seqcst :
    M.IsFunction "core::intrinsics::atomic_fence_seqcst" atomic_fence_seqcst.
  
  Parameter atomic_fence_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_fence_acquire :
    M.IsFunction "core::intrinsics::atomic_fence_acquire" atomic_fence_acquire.
  
  Parameter atomic_fence_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_fence_release :
    M.IsFunction "core::intrinsics::atomic_fence_release" atomic_fence_release.
  
  Parameter atomic_fence_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_fence_acqrel :
    M.IsFunction "core::intrinsics::atomic_fence_acqrel" atomic_fence_acqrel.
  
  Parameter atomic_singlethreadfence_seqcst : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_singlethreadfence_seqcst :
    M.IsFunction
      "core::intrinsics::atomic_singlethreadfence_seqcst"
      atomic_singlethreadfence_seqcst.
  
  Parameter atomic_singlethreadfence_acquire : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_singlethreadfence_acquire :
    M.IsFunction
      "core::intrinsics::atomic_singlethreadfence_acquire"
      atomic_singlethreadfence_acquire.
  
  Parameter atomic_singlethreadfence_release : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_singlethreadfence_release :
    M.IsFunction
      "core::intrinsics::atomic_singlethreadfence_release"
      atomic_singlethreadfence_release.
  
  Parameter atomic_singlethreadfence_acqrel : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_atomic_singlethreadfence_acqrel :
    M.IsFunction
      "core::intrinsics::atomic_singlethreadfence_acqrel"
      atomic_singlethreadfence_acqrel.
  
  Parameter prefetch_read_data : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_prefetch_read_data :
    M.IsFunction "core::intrinsics::prefetch_read_data" prefetch_read_data.
  
  Parameter prefetch_write_data : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_prefetch_write_data :
    M.IsFunction "core::intrinsics::prefetch_write_data" prefetch_write_data.
  
  Parameter prefetch_read_instruction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_prefetch_read_instruction :
    M.IsFunction "core::intrinsics::prefetch_read_instruction" prefetch_read_instruction.
  
  Parameter prefetch_write_instruction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_prefetch_write_instruction :
    M.IsFunction "core::intrinsics::prefetch_write_instruction" prefetch_write_instruction.
  
  Parameter rustc_peek : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rustc_peek : M.IsFunction "core::intrinsics::rustc_peek" rustc_peek.
  
  Parameter abort : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_abort : M.IsFunction "core::intrinsics::abort" abort.
  
  Parameter unreachable : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unreachable : M.IsFunction "core::intrinsics::unreachable" unreachable.
  
  (*
  pub const unsafe fn assume(b: bool) {
      if !b {
          // SAFETY: the caller must guarantee the argument is never `false`
          unsafe { unreachable() }
      }
  }
  *)
  Definition assume (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ b ] =>
      ltac:(M.monadic
        (let b := M.alloc (| b |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use (M.alloc (| UnOp.not (| M.read (| b |) |) |)) 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::intrinsics::unreachable", [] |),
                        []
                      |)
                    |)
                  |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_assume : M.IsFunction "core::intrinsics::assume" assume.
  
  (*
  pub const fn likely(b: bool) -> bool {
      b
  }
  *)
  Definition likely (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ b ] =>
      ltac:(M.monadic
        (let b := M.alloc (| b |) in
        M.read (| b |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_likely : M.IsFunction "core::intrinsics::likely" likely.
  
  (*
  pub const fn unlikely(b: bool) -> bool {
      b
  }
  *)
  Definition unlikely (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ b ] =>
      ltac:(M.monadic
        (let b := M.alloc (| b |) in
        M.read (| b |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_unlikely : M.IsFunction "core::intrinsics::unlikely" unlikely.
  
  (*
  pub fn select_unpredictable<T>(b: bool, true_val: T, false_val: T) -> T {
      if b { true_val } else { false_val }
  }
  *)
  Definition select_unpredictable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ b; true_val; false_val ] =>
      ltac:(M.monadic
        (let b := M.alloc (| b |) in
        let true_val := M.alloc (| true_val |) in
        let false_val := M.alloc (| false_val |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use b in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  true_val));
              fun γ => ltac:(M.monadic false_val)
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_select_unpredictable :
    M.IsFunction "core::intrinsics::select_unpredictable" select_unpredictable.
  
  Parameter breakpoint : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_breakpoint : M.IsFunction "core::intrinsics::breakpoint" breakpoint.
  
  Parameter assert_inhabited : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_assert_inhabited :
    M.IsFunction "core::intrinsics::assert_inhabited" assert_inhabited.
  
  Parameter assert_zero_valid : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_assert_zero_valid :
    M.IsFunction "core::intrinsics::assert_zero_valid" assert_zero_valid.
  
  Parameter assert_mem_uninitialized_valid : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_assert_mem_uninitialized_valid :
    M.IsFunction "core::intrinsics::assert_mem_uninitialized_valid" assert_mem_uninitialized_valid.
  
  Parameter caller_location : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_caller_location : M.IsFunction "core::intrinsics::caller_location" caller_location.
  
  Parameter forget : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_forget : M.IsFunction "core::intrinsics::forget" forget.
  
  Parameter transmute : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_transmute : M.IsFunction "core::intrinsics::transmute" transmute.
  
  Parameter transmute_unchecked : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_transmute_unchecked :
    M.IsFunction "core::intrinsics::transmute_unchecked" transmute_unchecked.
  
  Parameter needs_drop : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_needs_drop : M.IsFunction "core::intrinsics::needs_drop" needs_drop.
  
  Parameter offset : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_offset : M.IsFunction "core::intrinsics::offset" offset.
  
  Parameter arith_offset : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_arith_offset : M.IsFunction "core::intrinsics::arith_offset" arith_offset.
  
  Parameter ptr_mask : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ptr_mask : M.IsFunction "core::intrinsics::ptr_mask" ptr_mask.
  
  Parameter volatile_copy_nonoverlapping_memory :
      (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_volatile_copy_nonoverlapping_memory :
    M.IsFunction
      "core::intrinsics::volatile_copy_nonoverlapping_memory"
      volatile_copy_nonoverlapping_memory.
  
  Parameter volatile_copy_memory : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_volatile_copy_memory :
    M.IsFunction "core::intrinsics::volatile_copy_memory" volatile_copy_memory.
  
  Parameter volatile_set_memory : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_volatile_set_memory :
    M.IsFunction "core::intrinsics::volatile_set_memory" volatile_set_memory.
  
  Parameter volatile_load : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_volatile_load : M.IsFunction "core::intrinsics::volatile_load" volatile_load.
  
  Parameter volatile_store : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_volatile_store : M.IsFunction "core::intrinsics::volatile_store" volatile_store.
  
  Parameter unaligned_volatile_load : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unaligned_volatile_load :
    M.IsFunction "core::intrinsics::unaligned_volatile_load" unaligned_volatile_load.
  
  Parameter unaligned_volatile_store : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unaligned_volatile_store :
    M.IsFunction "core::intrinsics::unaligned_volatile_store" unaligned_volatile_store.
  
  Parameter sqrtf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sqrtf16 : M.IsFunction "core::intrinsics::sqrtf16" sqrtf16.
  
  Parameter sqrtf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sqrtf32 : M.IsFunction "core::intrinsics::sqrtf32" sqrtf32.
  
  Parameter sqrtf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sqrtf64 : M.IsFunction "core::intrinsics::sqrtf64" sqrtf64.
  
  Parameter sqrtf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sqrtf128 : M.IsFunction "core::intrinsics::sqrtf128" sqrtf128.
  
  Parameter powif16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powif16 : M.IsFunction "core::intrinsics::powif16" powif16.
  
  Parameter powif32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powif32 : M.IsFunction "core::intrinsics::powif32" powif32.
  
  Parameter powif64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powif64 : M.IsFunction "core::intrinsics::powif64" powif64.
  
  Parameter powif128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powif128 : M.IsFunction "core::intrinsics::powif128" powif128.
  
  Parameter sinf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sinf16 : M.IsFunction "core::intrinsics::sinf16" sinf16.
  
  Parameter sinf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sinf32 : M.IsFunction "core::intrinsics::sinf32" sinf32.
  
  Parameter sinf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sinf64 : M.IsFunction "core::intrinsics::sinf64" sinf64.
  
  Parameter sinf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sinf128 : M.IsFunction "core::intrinsics::sinf128" sinf128.
  
  Parameter cosf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cosf16 : M.IsFunction "core::intrinsics::cosf16" cosf16.
  
  Parameter cosf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cosf32 : M.IsFunction "core::intrinsics::cosf32" cosf32.
  
  Parameter cosf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cosf64 : M.IsFunction "core::intrinsics::cosf64" cosf64.
  
  Parameter cosf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cosf128 : M.IsFunction "core::intrinsics::cosf128" cosf128.
  
  Parameter powf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powf16 : M.IsFunction "core::intrinsics::powf16" powf16.
  
  Parameter powf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powf32 : M.IsFunction "core::intrinsics::powf32" powf32.
  
  Parameter powf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powf64 : M.IsFunction "core::intrinsics::powf64" powf64.
  
  Parameter powf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_powf128 : M.IsFunction "core::intrinsics::powf128" powf128.
  
  Parameter expf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_expf16 : M.IsFunction "core::intrinsics::expf16" expf16.
  
  Parameter expf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_expf32 : M.IsFunction "core::intrinsics::expf32" expf32.
  
  Parameter expf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_expf64 : M.IsFunction "core::intrinsics::expf64" expf64.
  
  Parameter expf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_expf128 : M.IsFunction "core::intrinsics::expf128" expf128.
  
  Parameter exp2f16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_exp2f16 : M.IsFunction "core::intrinsics::exp2f16" exp2f16.
  
  Parameter exp2f32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_exp2f32 : M.IsFunction "core::intrinsics::exp2f32" exp2f32.
  
  Parameter exp2f64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_exp2f64 : M.IsFunction "core::intrinsics::exp2f64" exp2f64.
  
  Parameter exp2f128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_exp2f128 : M.IsFunction "core::intrinsics::exp2f128" exp2f128.
  
  Parameter logf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_logf16 : M.IsFunction "core::intrinsics::logf16" logf16.
  
  Parameter logf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_logf32 : M.IsFunction "core::intrinsics::logf32" logf32.
  
  Parameter logf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_logf64 : M.IsFunction "core::intrinsics::logf64" logf64.
  
  Parameter logf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_logf128 : M.IsFunction "core::intrinsics::logf128" logf128.
  
  Parameter log10f16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log10f16 : M.IsFunction "core::intrinsics::log10f16" log10f16.
  
  Parameter log10f32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log10f32 : M.IsFunction "core::intrinsics::log10f32" log10f32.
  
  Parameter log10f64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log10f64 : M.IsFunction "core::intrinsics::log10f64" log10f64.
  
  Parameter log10f128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log10f128 : M.IsFunction "core::intrinsics::log10f128" log10f128.
  
  Parameter log2f16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log2f16 : M.IsFunction "core::intrinsics::log2f16" log2f16.
  
  Parameter log2f32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log2f32 : M.IsFunction "core::intrinsics::log2f32" log2f32.
  
  Parameter log2f64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log2f64 : M.IsFunction "core::intrinsics::log2f64" log2f64.
  
  Parameter log2f128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_log2f128 : M.IsFunction "core::intrinsics::log2f128" log2f128.
  
  Parameter fmaf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmaf16 : M.IsFunction "core::intrinsics::fmaf16" fmaf16.
  
  Parameter fmaf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmaf32 : M.IsFunction "core::intrinsics::fmaf32" fmaf32.
  
  Parameter fmaf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmaf64 : M.IsFunction "core::intrinsics::fmaf64" fmaf64.
  
  Parameter fmaf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmaf128 : M.IsFunction "core::intrinsics::fmaf128" fmaf128.
  
  Parameter fabsf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fabsf16 : M.IsFunction "core::intrinsics::fabsf16" fabsf16.
  
  Parameter fabsf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fabsf32 : M.IsFunction "core::intrinsics::fabsf32" fabsf32.
  
  Parameter fabsf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fabsf64 : M.IsFunction "core::intrinsics::fabsf64" fabsf64.
  
  Parameter fabsf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fabsf128 : M.IsFunction "core::intrinsics::fabsf128" fabsf128.
  
  Parameter minnumf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_minnumf16 : M.IsFunction "core::intrinsics::minnumf16" minnumf16.
  
  Parameter minnumf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_minnumf32 : M.IsFunction "core::intrinsics::minnumf32" minnumf32.
  
  Parameter minnumf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_minnumf64 : M.IsFunction "core::intrinsics::minnumf64" minnumf64.
  
  Parameter minnumf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_minnumf128 : M.IsFunction "core::intrinsics::minnumf128" minnumf128.
  
  Parameter maxnumf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_maxnumf16 : M.IsFunction "core::intrinsics::maxnumf16" maxnumf16.
  
  Parameter maxnumf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_maxnumf32 : M.IsFunction "core::intrinsics::maxnumf32" maxnumf32.
  
  Parameter maxnumf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_maxnumf64 : M.IsFunction "core::intrinsics::maxnumf64" maxnumf64.
  
  Parameter maxnumf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_maxnumf128 : M.IsFunction "core::intrinsics::maxnumf128" maxnumf128.
  
  Parameter copysignf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_copysignf16 : M.IsFunction "core::intrinsics::copysignf16" copysignf16.
  
  Parameter copysignf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_copysignf32 : M.IsFunction "core::intrinsics::copysignf32" copysignf32.
  
  Parameter copysignf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_copysignf64 : M.IsFunction "core::intrinsics::copysignf64" copysignf64.
  
  Parameter copysignf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_copysignf128 : M.IsFunction "core::intrinsics::copysignf128" copysignf128.
  
  Parameter floorf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_floorf16 : M.IsFunction "core::intrinsics::floorf16" floorf16.
  
  Parameter floorf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_floorf32 : M.IsFunction "core::intrinsics::floorf32" floorf32.
  
  Parameter floorf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_floorf64 : M.IsFunction "core::intrinsics::floorf64" floorf64.
  
  Parameter floorf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_floorf128 : M.IsFunction "core::intrinsics::floorf128" floorf128.
  
  Parameter ceilf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ceilf16 : M.IsFunction "core::intrinsics::ceilf16" ceilf16.
  
  Parameter ceilf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ceilf32 : M.IsFunction "core::intrinsics::ceilf32" ceilf32.
  
  Parameter ceilf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ceilf64 : M.IsFunction "core::intrinsics::ceilf64" ceilf64.
  
  Parameter ceilf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ceilf128 : M.IsFunction "core::intrinsics::ceilf128" ceilf128.
  
  Parameter truncf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_truncf16 : M.IsFunction "core::intrinsics::truncf16" truncf16.
  
  Parameter truncf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_truncf32 : M.IsFunction "core::intrinsics::truncf32" truncf32.
  
  Parameter truncf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_truncf64 : M.IsFunction "core::intrinsics::truncf64" truncf64.
  
  Parameter truncf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_truncf128 : M.IsFunction "core::intrinsics::truncf128" truncf128.
  
  Parameter rintf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rintf16 : M.IsFunction "core::intrinsics::rintf16" rintf16.
  
  Parameter rintf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rintf32 : M.IsFunction "core::intrinsics::rintf32" rintf32.
  
  Parameter rintf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rintf64 : M.IsFunction "core::intrinsics::rintf64" rintf64.
  
  Parameter rintf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rintf128 : M.IsFunction "core::intrinsics::rintf128" rintf128.
  
  Parameter nearbyintf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_nearbyintf16 : M.IsFunction "core::intrinsics::nearbyintf16" nearbyintf16.
  
  Parameter nearbyintf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_nearbyintf32 : M.IsFunction "core::intrinsics::nearbyintf32" nearbyintf32.
  
  Parameter nearbyintf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_nearbyintf64 : M.IsFunction "core::intrinsics::nearbyintf64" nearbyintf64.
  
  Parameter nearbyintf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_nearbyintf128 : M.IsFunction "core::intrinsics::nearbyintf128" nearbyintf128.
  
  Parameter roundf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundf16 : M.IsFunction "core::intrinsics::roundf16" roundf16.
  
  Parameter roundf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundf32 : M.IsFunction "core::intrinsics::roundf32" roundf32.
  
  Parameter roundf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundf64 : M.IsFunction "core::intrinsics::roundf64" roundf64.
  
  Parameter roundf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundf128 : M.IsFunction "core::intrinsics::roundf128" roundf128.
  
  Parameter roundevenf16 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundevenf16 : M.IsFunction "core::intrinsics::roundevenf16" roundevenf16.
  
  Parameter roundevenf32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundevenf32 : M.IsFunction "core::intrinsics::roundevenf32" roundevenf32.
  
  Parameter roundevenf64 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundevenf64 : M.IsFunction "core::intrinsics::roundevenf64" roundevenf64.
  
  Parameter roundevenf128 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_roundevenf128 : M.IsFunction "core::intrinsics::roundevenf128" roundevenf128.
  
  Parameter fadd_fast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fadd_fast : M.IsFunction "core::intrinsics::fadd_fast" fadd_fast.
  
  Parameter fsub_fast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fsub_fast : M.IsFunction "core::intrinsics::fsub_fast" fsub_fast.
  
  Parameter fmul_fast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmul_fast : M.IsFunction "core::intrinsics::fmul_fast" fmul_fast.
  
  Parameter fdiv_fast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fdiv_fast : M.IsFunction "core::intrinsics::fdiv_fast" fdiv_fast.
  
  Parameter frem_fast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_frem_fast : M.IsFunction "core::intrinsics::frem_fast" frem_fast.
  
  Parameter fadd_algebraic : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fadd_algebraic : M.IsFunction "core::intrinsics::fadd_algebraic" fadd_algebraic.
  
  Parameter fsub_algebraic : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fsub_algebraic : M.IsFunction "core::intrinsics::fsub_algebraic" fsub_algebraic.
  
  Parameter fmul_algebraic : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fmul_algebraic : M.IsFunction "core::intrinsics::fmul_algebraic" fmul_algebraic.
  
  Parameter fdiv_algebraic : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_fdiv_algebraic : M.IsFunction "core::intrinsics::fdiv_algebraic" fdiv_algebraic.
  
  Parameter frem_algebraic : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_frem_algebraic : M.IsFunction "core::intrinsics::frem_algebraic" frem_algebraic.
  
  Parameter float_to_int_unchecked : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_float_to_int_unchecked :
    M.IsFunction "core::intrinsics::float_to_int_unchecked" float_to_int_unchecked.
  
  Parameter ctpop : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ctpop : M.IsFunction "core::intrinsics::ctpop" ctpop.
  
  Parameter ctlz : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ctlz : M.IsFunction "core::intrinsics::ctlz" ctlz.
  
  Parameter ctlz_nonzero : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ctlz_nonzero : M.IsFunction "core::intrinsics::ctlz_nonzero" ctlz_nonzero.
  
  Parameter cttz : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cttz : M.IsFunction "core::intrinsics::cttz" cttz.
  
  Parameter cttz_nonzero : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_cttz_nonzero : M.IsFunction "core::intrinsics::cttz_nonzero" cttz_nonzero.
  
  Parameter bswap : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_bswap : M.IsFunction "core::intrinsics::bswap" bswap.
  
  Parameter bitreverse : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_bitreverse : M.IsFunction "core::intrinsics::bitreverse" bitreverse.
  
  Parameter three_way_compare : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_three_way_compare :
    M.IsFunction "core::intrinsics::three_way_compare" three_way_compare.
  
  Parameter add_with_overflow : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_add_with_overflow :
    M.IsFunction "core::intrinsics::add_with_overflow" add_with_overflow.
  
  Parameter sub_with_overflow : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_sub_with_overflow :
    M.IsFunction "core::intrinsics::sub_with_overflow" sub_with_overflow.
  
  Parameter mul_with_overflow : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_mul_with_overflow :
    M.IsFunction "core::intrinsics::mul_with_overflow" mul_with_overflow.
  
  Parameter exact_div : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_exact_div : M.IsFunction "core::intrinsics::exact_div" exact_div.
  
  Parameter unchecked_div : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_div : M.IsFunction "core::intrinsics::unchecked_div" unchecked_div.
  
  Parameter unchecked_rem : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_rem : M.IsFunction "core::intrinsics::unchecked_rem" unchecked_rem.
  
  Parameter unchecked_shl : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_shl : M.IsFunction "core::intrinsics::unchecked_shl" unchecked_shl.
  
  Parameter unchecked_shr : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_shr : M.IsFunction "core::intrinsics::unchecked_shr" unchecked_shr.
  
  Parameter unchecked_add : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_add : M.IsFunction "core::intrinsics::unchecked_add" unchecked_add.
  
  Parameter unchecked_sub : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_sub : M.IsFunction "core::intrinsics::unchecked_sub" unchecked_sub.
  
  Parameter unchecked_mul : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_unchecked_mul : M.IsFunction "core::intrinsics::unchecked_mul" unchecked_mul.
  
  Parameter rotate_left : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rotate_left : M.IsFunction "core::intrinsics::rotate_left" rotate_left.
  
  Parameter rotate_right : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_rotate_right : M.IsFunction "core::intrinsics::rotate_right" rotate_right.
  
  Parameter wrapping_add : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_wrapping_add : M.IsFunction "core::intrinsics::wrapping_add" wrapping_add.
  
  Parameter wrapping_sub : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_wrapping_sub : M.IsFunction "core::intrinsics::wrapping_sub" wrapping_sub.
  
  Parameter wrapping_mul : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_wrapping_mul : M.IsFunction "core::intrinsics::wrapping_mul" wrapping_mul.
  
  Parameter saturating_add : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_saturating_add : M.IsFunction "core::intrinsics::saturating_add" saturating_add.
  
  Parameter saturating_sub : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_saturating_sub : M.IsFunction "core::intrinsics::saturating_sub" saturating_sub.
  
  Parameter read_via_copy : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_read_via_copy : M.IsFunction "core::intrinsics::read_via_copy" read_via_copy.
  
  Parameter write_via_move : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_write_via_move : M.IsFunction "core::intrinsics::write_via_move" write_via_move.
  
  Parameter discriminant_value : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_discriminant_value :
    M.IsFunction "core::intrinsics::discriminant_value" discriminant_value.
  
  Parameter catch_unwind : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_catch_unwind : M.IsFunction "core::intrinsics::catch_unwind" catch_unwind.
  
  Parameter nontemporal_store : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_nontemporal_store :
    M.IsFunction "core::intrinsics::nontemporal_store" nontemporal_store.
  
  Parameter ptr_offset_from : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ptr_offset_from : M.IsFunction "core::intrinsics::ptr_offset_from" ptr_offset_from.
  
  Parameter ptr_offset_from_unsigned : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_ptr_offset_from_unsigned :
    M.IsFunction "core::intrinsics::ptr_offset_from_unsigned" ptr_offset_from_unsigned.
  
  (*
  pub const fn ptr_guaranteed_cmp<T>(ptr: *const T, other: *const T) -> u8 {
      (ptr == other) as u8
  }
  *)
  Definition ptr_guaranteed_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ ptr; other ] =>
      ltac:(M.monadic
        (let ptr := M.alloc (| ptr |) in
        let other := M.alloc (| other |) in
        M.rust_cast (BinOp.eq (| M.read (| ptr |), M.read (| other |) |))))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_ptr_guaranteed_cmp :
    M.IsFunction "core::intrinsics::ptr_guaranteed_cmp" ptr_guaranteed_cmp.
  
  Parameter raw_eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_raw_eq : M.IsFunction "core::intrinsics::raw_eq" raw_eq.
  
  Parameter compare_bytes : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_compare_bytes : M.IsFunction "core::intrinsics::compare_bytes" compare_bytes.
  
  Parameter black_box : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function_black_box : M.IsFunction "core::intrinsics::black_box" black_box.
  
  (*
  pub const fn const_eval_select<ARG: Tuple, F, G, RET>(
      _arg: ARG,
      _called_in_const: F,
      _called_at_rt: G,
  ) -> RET
  where
      G: FnOnce<ARG, Output = RET>,
      F: FnOnce<ARG, Output = RET>,
  {
      unreachable!()
  }
  *)
  Definition const_eval_select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ ARG; F; G; RET ], [ _arg; _called_in_const; _called_at_rt ] =>
      ltac:(M.monadic
        (let _arg := M.alloc (| _arg |) in
        let _called_in_const := M.alloc (| _called_in_const |) in
        let _called_at_rt := M.alloc (| _called_at_rt |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_const_eval_select :
    M.IsFunction "core::intrinsics::const_eval_select" const_eval_select.
  
  (*
  pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
      false
  }
  *)
  Definition is_val_statically_known (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ _arg ] =>
      ltac:(M.monadic
        (let _arg := M.alloc (| _arg |) in
        Value.Bool false))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_val_statically_known :
    M.IsFunction "core::intrinsics::is_val_statically_known" is_val_statically_known.
  
  (*
  pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
      // SAFETY: The caller provided single non-overlapping items behind
      // pointers, so swapping them with `count: 1` is fine.
      unsafe { ptr::swap_nonoverlapping(x, y, 1) };
  }
  *)
  Definition typed_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~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::swap_nonoverlapping", [ T ] |),
                [ M.read (| x |); M.read (| y |); Value.Integer IntegerKind.Usize 1 ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_typed_swap : M.IsFunction "core::intrinsics::typed_swap" typed_swap.
  
  (*
  pub const fn ub_checks() -> bool {
      cfg!(ub_checks)
  }
  *)
  Definition ub_checks (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] => ltac:(M.monadic (Value.Bool true))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_ub_checks : M.IsFunction "core::intrinsics::ub_checks" ub_checks.
  
  (*
  pub const unsafe fn const_allocate(_size: usize, _align: usize) -> *mut u8 {
      // const eval overrides this function, but runtime code for now just returns null pointers.
      // See <https://github.com/rust-lang/rust/issues/93935>.
      crate::ptr::null_mut()
  }
  *)
  Definition const_allocate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ _size; _align ] =>
      ltac:(M.monadic
        (let _size := M.alloc (| _size |) in
        let _align := M.alloc (| _align |) in
        M.call_closure (| M.get_function (| "core::ptr::null_mut", [ Ty.path "u8" ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_const_allocate : M.IsFunction "core::intrinsics::const_allocate" const_allocate.
  
  (*
  pub const unsafe fn const_deallocate(_ptr: *mut u8, _size: usize, _align: usize) {
      // Runtime NOP
  }
  *)
  Definition const_deallocate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ _ptr; _size; _align ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        let _size := M.alloc (| _size |) in
        let _align := M.alloc (| _align |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_const_deallocate :
    M.IsFunction "core::intrinsics::const_deallocate" const_deallocate.
  
  (*
  pub unsafe fn vtable_size(_ptr: *const ()) -> usize {
      unreachable!()
  }
  *)
  Definition vtable_size (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ _ptr ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_vtable_size : M.IsFunction "core::intrinsics::vtable_size" vtable_size.
  
  (*
  pub unsafe fn vtable_align(_ptr: *const ()) -> usize {
      unreachable!()
  }
  *)
  Definition vtable_align (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ _ptr ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_vtable_align : M.IsFunction "core::intrinsics::vtable_align" vtable_align.
  
  (*
  pub const fn size_of<T>() -> usize {
      unreachable!()
  }
  *)
  Definition size_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_size_of : M.IsFunction "core::intrinsics::size_of" size_of.
  
  (*
  pub const fn min_align_of<T>() -> usize {
      unreachable!()
  }
  *)
  Definition min_align_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_align_of : M.IsFunction "core::intrinsics::min_align_of" min_align_of.
  
  (*
  pub const unsafe fn pref_align_of<T>() -> usize {
      unreachable!()
  }
  *)
  Definition pref_align_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_pref_align_of : M.IsFunction "core::intrinsics::pref_align_of" pref_align_of.
  
  (*
  pub const fn variant_count<T>() -> usize {
      unreachable!()
  }
  *)
  Definition variant_count (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_variant_count : M.IsFunction "core::intrinsics::variant_count" variant_count.
  
  (*
  pub const unsafe fn size_of_val<T: ?Sized>(_ptr: *const T) -> usize {
      unreachable!()
  }
  *)
  Definition size_of_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ _ptr ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_size_of_val : M.IsFunction "core::intrinsics::size_of_val" size_of_val.
  
  (*
  pub const unsafe fn min_align_of_val<T: ?Sized>(_ptr: *const T) -> usize {
      unreachable!()
  }
  *)
  Definition min_align_of_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ _ptr ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_align_of_val :
    M.IsFunction "core::intrinsics::min_align_of_val" min_align_of_val.
  
  (*
  pub const fn type_name<T: ?Sized>() -> &'static str {
      unreachable!()
  }
  *)
  Definition type_name (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_type_name : M.IsFunction "core::intrinsics::type_name" type_name.
  
  (*
  pub const fn type_id<T: ?Sized + 'static>() -> u128 {
      unreachable!()
  }
  *)
  Definition type_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_type_id : M.IsFunction "core::intrinsics::type_id" type_id.
  
  (*
  pub const fn aggregate_raw_ptr<P: AggregateRawPtr<D, Metadata = M>, D, M>(_data: D, _meta: M) -> P {
      // To implement a fallback we'd have to assume the layout of the pointer,
      // but the whole point of this intrinsic is that we shouldn't do that.
      unreachable!()
  }
  *)
  Definition aggregate_raw_ptr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ P; D; M_ ], [ _data; _meta ] =>
      ltac:(M.monadic
        (let _data := M.alloc (| _data |) in
        let _meta := M.alloc (| _meta |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_aggregate_raw_ptr :
    M.IsFunction "core::intrinsics::aggregate_raw_ptr" aggregate_raw_ptr.
  
  (* Trait *)
  (* Empty module 'AggregateRawPtr' *)
  
  Module Impl_core_intrinsics_AggregateRawPtr_where_core_marker_Sized_P_where_core_ptr_metadata_Thin_T_pointer_const_T_for_pointer_const_P.
    Definition Self (P T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ P ].
    
    (*     type Metadata = <P as ptr::Pointee>::Metadata; *)
    Definition _Metadata (P T : Ty.t) : Ty.t := Ty.associated.
    
    Axiom Implements :
      forall (P T : Ty.t),
      M.IsTraitInstance
        "core::intrinsics::AggregateRawPtr"
        (Self P T)
        (* Trait polymorphic types *) [ (* D *) Ty.apply (Ty.path "*const") [] [ T ] ]
        (* Instance *) [ ("Metadata", InstanceField.Ty (_Metadata P T)) ].
  End Impl_core_intrinsics_AggregateRawPtr_where_core_marker_Sized_P_where_core_ptr_metadata_Thin_T_pointer_const_T_for_pointer_const_P.
  
  Module Impl_core_intrinsics_AggregateRawPtr_where_core_marker_Sized_P_where_core_ptr_metadata_Thin_T_pointer_mut_T_for_pointer_mut_P.
    Definition Self (P T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ P ].
    
    (*     type Metadata = <P as ptr::Pointee>::Metadata; *)
    Definition _Metadata (P T : Ty.t) : Ty.t := Ty.associated.
    
    Axiom Implements :
      forall (P T : Ty.t),
      M.IsTraitInstance
        "core::intrinsics::AggregateRawPtr"
        (Self P T)
        (* Trait polymorphic types *) [ (* D *) Ty.apply (Ty.path "*mut") [] [ T ] ]
        (* Instance *) [ ("Metadata", InstanceField.Ty (_Metadata P T)) ].
  End Impl_core_intrinsics_AggregateRawPtr_where_core_marker_Sized_P_where_core_ptr_metadata_Thin_T_pointer_mut_T_for_pointer_mut_P.
  
  (*
  pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + ?Sized, M>(_ptr: *const P) -> M {
      // To implement a fallback we'd have to assume the layout of the pointer,
      // but the whole point of this intrinsic is that we shouldn't do that.
      unreachable!()
  }
  *)
  Definition ptr_metadata (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ P; M_ ], [ _ptr ] =>
      ltac:(M.monadic
        (let _ptr := M.alloc (| _ptr |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic", [] |),
            [ M.read (| Value.String "internal error: entered unreachable code" |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_ptr_metadata : M.IsFunction "core::intrinsics::ptr_metadata" ptr_metadata.
  
  (*
  pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) {
      extern "rust-intrinsic" {
          #[rustc_const_stable(feature = "const_intrinsic_copy", since = "CURRENT_RUSTC_VERSION")]
          #[rustc_nounwind]
          pub fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize);
      }
  
      ub_checks::assert_unsafe_precondition!(
          check_language_ub,
          "ptr::copy_nonoverlapping requires that both pointer arguments are aligned and non-null \
          and the specified memory ranges do not overlap",
          (
              src: *const () = src as *const (),
              dst: *mut () = dst as *mut (),
              size: usize = size_of::<T>(),
              align: usize = align_of::<T>(),
              count: usize = count,
          ) =>
          ub_checks::is_aligned_and_not_null(src, align)
              && ub_checks::is_aligned_and_not_null(dst, align)
              && ub_checks::is_nonoverlapping(src, dst, size, count)
      );
  
      // SAFETY: the safety contract for `copy_nonoverlapping` must be
      // upheld by the caller.
      unsafe { copy_nonoverlapping(src, dst, count) }
  }
  *)
  Definition copy_nonoverlapping (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ src; dst; count ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) in
        let dst := M.alloc (| dst |) in
        let count := M.alloc (| count |) 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::intrinsics::copy_nonoverlapping.precondition_check",
                            []
                          |),
                          [
                            M.rust_cast (M.read (| src |));
                            M.rust_cast (M.read (| dst |));
                            M.call_closure (|
                              M.get_function (| "core::intrinsics::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
          M.alloc (|
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::copy_nonoverlapping::copy_nonoverlapping",
                [ T ]
              |),
              [ M.read (| src |); M.read (| dst |); M.read (| count |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_copy_nonoverlapping :
    M.IsFunction "core::intrinsics::copy_nonoverlapping" copy_nonoverlapping.
  
  Module copy_nonoverlapping.
    Parameter copy_nonoverlapping : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_copy_nonoverlapping :
      M.IsFunction "core::intrinsics::copy_nonoverlapping::copy_nonoverlapping" copy_nonoverlapping.
  End copy_nonoverlapping.
  
  (*
  pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
      extern "rust-intrinsic" {
          #[rustc_const_stable(feature = "const_intrinsic_copy", since = "CURRENT_RUSTC_VERSION")]
          #[rustc_nounwind]
          fn copy<T>(src: *const T, dst: *mut T, count: usize);
      }
  
      // SAFETY: the safety contract for `copy` must be upheld by the caller.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::copy requires that both pointer arguments are aligned and non-null",
              (
                  src: *const () = src as *const (),
                  dst: *mut () = dst as *mut (),
                  align: usize = align_of::<T>(),
              ) =>
              ub_checks::is_aligned_and_not_null(src, align)
                  && ub_checks::is_aligned_and_not_null(dst, align)
          );
          copy(src, dst, count)
      }
  }
  *)
  Definition copy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ src; dst; count ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) in
        let dst := M.alloc (| dst |) in
        let count := M.alloc (| count |) 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::intrinsics::copy.precondition_check", [] |),
                          [
                            M.rust_cast (M.read (| src |));
                            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::copy::copy", [ T ] |),
              [ M.read (| src |); M.read (| dst |); M.read (| count |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_copy : M.IsFunction "core::intrinsics::copy" copy.
  
  Module copy.
    Parameter copy : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_copy : M.IsFunction "core::intrinsics::copy::copy" copy.
  End copy.
  
  (*
  pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
      extern "rust-intrinsic" {
          #[rustc_const_unstable(feature = "const_ptr_write", issue = "86302")]
          #[rustc_nounwind]
          fn write_bytes<T>(dst: *mut T, val: u8, count: usize);
      }
  
      // SAFETY: the safety contract for `write_bytes` must be upheld by the caller.
      unsafe {
          ub_checks::assert_unsafe_precondition!(
              check_language_ub,
              "ptr::write_bytes requires that the destination pointer is aligned and non-null",
              (
                  addr: *const () = dst as *const (),
                  align: usize = align_of::<T>(),
              ) => ub_checks::is_aligned_and_not_null(addr, align)
          );
          write_bytes(dst, val, count)
      }
  }
  *)
  Definition write_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dst; val; count ] =>
      ltac:(M.monadic
        (let dst := M.alloc (| dst |) in
        let val := M.alloc (| val |) in
        let count := M.alloc (| count |) 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::intrinsics::write_bytes.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_bytes::write_bytes", [ T ] |),
              [ M.read (| dst |); M.read (| val |); M.read (| count |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_write_bytes : M.IsFunction "core::intrinsics::write_bytes" write_bytes.
  
  Module write_bytes.
    Parameter write_bytes : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_write_bytes :
      M.IsFunction "core::intrinsics::write_bytes::write_bytes" write_bytes.
  End write_bytes.
End intrinsics.
