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

Module slice.
  Module sort.
    Module stable.
      (*
      pub fn sort<T, F: FnMut(&T, &T) -> bool, BufT: BufGuard<T>>(v: &mut [T], is_less: &mut F) {
          // Arrays of zero-sized types are always all-equal, and thus sorted.
          if T::IS_ZST {
              return;
          }
      
          // Instrumenting the standard library showed that 90+% of the calls to sort
          // by rustc are either of size 0 or 1.
          let len = v.len();
          if intrinsics::likely(len < 2) {
              return;
          }
      
          cfg_if! {
              if #[cfg(any(feature = "optimize_for_size", target_pointer_width = "16"))] {
                  let alloc_len = len / 2;
      
                  cfg_if! {
                      if #[cfg(target_pointer_width = "16")] {
                          let mut heap_buf = BufT::with_capacity(alloc_len);
                          let scratch = heap_buf.as_uninit_slice_mut();
                      } else {
                          // For small inputs 4KiB of stack storage suffices, which allows us to avoid
                          // calling the (de-)allocator. Benchmarks showed this was quite beneficial.
                          let mut stack_buf = AlignedStorage::<T, 4096>::new();
                          let stack_scratch = stack_buf.as_uninit_slice_mut();
                          let mut heap_buf;
                          let scratch = if stack_scratch.len() >= alloc_len {
                              stack_scratch
                          } else {
                              heap_buf = BufT::with_capacity(alloc_len);
                              heap_buf.as_uninit_slice_mut()
                          };
                      }
                  }
      
                  tiny::mergesort(v, scratch, is_less);
              } else {
                  // More advanced sorting methods than insertion sort are faster if called in
                  // a hot loop for small inputs, but for general-purpose code the small
                  // binary size of insertion sort is more important. The instruction cache in
                  // modern processors is very valuable, and for a single sort call in general
                  // purpose code any gains from an advanced method are cancelled by i-cache
                  // misses during the sort, and thrashing the i-cache for surrounding code.
                  const MAX_LEN_ALWAYS_INSERTION_SORT: usize = 20;
                  if intrinsics::likely(len <= MAX_LEN_ALWAYS_INSERTION_SORT) {
                      insertion_sort_shift_left(v, 1, is_less);
                      return;
                  }
      
                  driftsort_main::<T, F, BufT>(v, is_less);
              }
          }
      }
      *)
      Definition sort (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F; BufT ], [ v; is_less ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ len :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| v |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::likely", [] |),
                                    [
                                      BinOp.lt (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 2
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::likely", [] |),
                                    [
                                      BinOp.le (|
                                        M.read (| len |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::sort::stable::sort::MAX_LEN_ALWAYS_INSERTION_SORT"
                                          |)
                                        |)
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::slice::sort::shared::smallsort::insertion_sort_shift_left",
                                          [ T; F ]
                                        |),
                                        [
                                          M.read (| v |);
                                          Value.Integer IntegerKind.Usize 1;
                                          M.read (| is_less |)
                                        ]
                                      |)
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::stable::driftsort_main",
                          [ T; F; BufT ]
                        |),
                        [ M.read (| v |); M.read (| is_less |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_sort : M.IsFunction "core::slice::sort::stable::sort" sort.
      
      Module sort.
        Definition value_MAX_LEN_ALWAYS_INSERTION_SORT : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 20 |))).
      End sort.
      
      (*
      fn driftsort_main<T, F: FnMut(&T, &T) -> bool, BufT: BufGuard<T>>(v: &mut [T], is_less: &mut F) {
          // By allocating n elements of memory we can ensure the entire input can
          // be sorted using stable quicksort, which allows better performance on
          // random and low-cardinality distributions. However, we still want to
          // reduce our memory usage to n / 2 for large inputs. We do this by scaling
          // our allocation as max(n / 2, min(n, 8MB)), ensuring we scale like n for
          // small inputs and n / 2 for large inputs, without a sudden drop off. We
          // also need to ensure our alloc >= MIN_SMALL_SORT_SCRATCH_LEN, as the
          // small-sort always needs this much memory.
          const MAX_FULL_ALLOC_BYTES: usize = 8_000_000; // 8MB
          let max_full_alloc = MAX_FULL_ALLOC_BYTES / mem::size_of::<T>();
          let len = v.len();
          let alloc_len =
              cmp::max(cmp::max(len / 2, cmp::min(len, max_full_alloc)), SMALL_SORT_GENERAL_SCRATCH_LEN);
      
          // For small inputs 4KiB of stack storage suffices, which allows us to avoid
          // calling the (de-)allocator. Benchmarks showed this was quite beneficial.
          let mut stack_buf = AlignedStorage::<T, 4096>::new();
          let stack_scratch = stack_buf.as_uninit_slice_mut();
          let mut heap_buf;
          let scratch = if stack_scratch.len() >= alloc_len {
              stack_scratch
          } else {
              heap_buf = BufT::with_capacity(alloc_len);
              heap_buf.as_uninit_slice_mut()
          };
      
          // For small inputs using quicksort is not yet beneficial, and a single
          // small-sort or two small-sorts plus a single merge outperforms it, so use
          // eager mode.
          let eager_sort = len <= T::small_sort_threshold() * 2;
          crate::slice::sort::stable::drift::sort(v, scratch, eager_sort, is_less);
      }
      *)
      Definition driftsort_main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F; BufT ], [ v; is_less ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            let is_less := M.alloc (| is_less |) in
            M.read (|
              let~ max_full_alloc :=
                M.alloc (|
                  BinOp.Wrap.div (|
                    M.read (|
                      M.get_constant (|
                        "core::slice::sort::stable::driftsort_main::MAX_FULL_ALLOC_BYTES"
                      |)
                    |),
                    M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                  |)
                |) in
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "len", [] |),
                    [ M.read (| v |) ]
                  |)
                |) in
              let~ alloc_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::cmp::max", [ Ty.path "usize" ] |),
                    [
                      M.call_closure (|
                        M.get_function (| "core::cmp::max", [ Ty.path "usize" ] |),
                        [
                          BinOp.Wrap.div (| M.read (| len |), Value.Integer IntegerKind.Usize 2 |);
                          M.call_closure (|
                            M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                            [ M.read (| len |); M.read (| max_full_alloc |) ]
                          |)
                        ]
                      |);
                      M.read (|
                        M.get_constant (|
                          "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ stack_buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::slice::sort::stable::AlignedStorage")
                        [ Value.Integer IntegerKind.Usize 4096 ]
                        [ T ],
                      "new",
                      []
                    |),
                    []
                  |)
                |) in
              let~ stack_scratch :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::slice::sort::stable::AlignedStorage")
                        [ Value.Integer IntegerKind.Usize 4096 ]
                        [ T ],
                      "as_uninit_slice_mut",
                      []
                    |),
                    [ stack_buf ]
                  |)
                |) in
              let~ heap_buf := M.copy (| Value.DeclaredButUndefined |) in
              let~ scratch :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ge (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                            []
                                            [ T ]
                                        ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| stack_scratch |) ]
                                  |),
                                  M.read (| alloc_len |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          stack_scratch));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.read (|
                              let~ _ :=
                                M.write (|
                                  heap_buf,
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::slice::sort::stable::BufGuard",
                                      BufT,
                                      [ T ],
                                      "with_capacity",
                                      []
                                    |),
                                    [ M.read (| alloc_len |) ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::slice::sort::stable::BufGuard",
                                    BufT,
                                    [ T ],
                                    "as_uninit_slice_mut",
                                    []
                                  |),
                                  [ heap_buf ]
                                |)
                              |)
                            |)
                          |)))
                    ]
                  |)
                |) in
              let~ eager_sort :=
                M.alloc (|
                  BinOp.le (|
                    M.read (| len |),
                    BinOp.Wrap.mul (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::slice::sort::shared::smallsort::StableSmallSortTypeImpl",
                          T,
                          [],
                          "small_sort_threshold",
                          []
                        |),
                        []
                      |),
                      Value.Integer IntegerKind.Usize 2
                    |)
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::sort::stable::drift::sort", [ T; F ] |),
                    [
                      M.read (| v |);
                      M.read (| scratch |);
                      M.read (| eager_sort |);
                      M.read (| is_less |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_driftsort_main :
        M.IsFunction "core::slice::sort::stable::driftsort_main" driftsort_main.
      
      Module driftsort_main.
        Definition value_MAX_FULL_ALLOC_BYTES : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 8000000 |))).
      End driftsort_main.
      
      (* Trait *)
      (* Empty module 'BufGuard' *)
      
      (* StructRecord
        {
          name := "AlignedStorage";
          const_params := [ "N" ];
          ty_params := [ "T" ];
          fields :=
            [
              ("_align", Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 0 ] [ T ]);
              ("storage",
                Ty.apply
                  (Ty.path "array")
                  [ N ]
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ])
            ];
        } *)
      
      Module Impl_core_slice_sort_stable_AlignedStorage_N_T.
        Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::slice::sort::stable::AlignedStorage") [ N ] [ T ].
        
        (*
            fn new() -> Self {
                Self { _align: [], storage: [const { MaybeUninit::uninit() }; N] }
            }
        *)
        Definition new
            (N : Value.t)
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self N T in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "core::slice::sort::stable::AlignedStorage"
                [
                  ("_align", Value.Array []);
                  ("storage",
                    repeat (|
                      M.read (|
                        M.get_constant (| "core::slice::sort::stable::new_discriminant" |)
                      |),
                      N
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (N : Value.t) (T : Ty.t),
          M.IsAssociatedFunction (Self N T) "new" (new N T).
        
        (*
            fn as_uninit_slice_mut(&mut self) -> &mut [MaybeUninit<T>] {
                let len = N / mem::size_of::<T>();
        
                // SAFETY: `_align` ensures we are correctly aligned.
                unsafe { core::slice::from_raw_parts_mut(self.storage.as_mut_ptr().cast(), len) }
            }
        *)
        Definition as_uninit_slice_mut
            (N : Value.t)
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self N T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    BinOp.Wrap.div (|
                      M.read (| M.get_constant (| "core::slice::sort::stable::N" |) |),
                      M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::slice::raw::from_raw_parts_mut",
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "*mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                []
                                [ Ty.path "u8" ]
                            ],
                          "cast",
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ Ty.path "u8" ]
                                ],
                              "as_mut_ptr",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::sort::stable::AlignedStorage",
                                "storage"
                              |)
                            ]
                          |)
                        ]
                      |);
                      M.read (| len |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_as_uninit_slice_mut :
          forall (N : Value.t) (T : Ty.t),
          M.IsAssociatedFunction (Self N T) "as_uninit_slice_mut" (as_uninit_slice_mut N T).
      End Impl_core_slice_sort_stable_AlignedStorage_N_T.
    End stable.
  End sort.
End slice.
