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

Module slice.
  Module sort.
    Module shared.
      Module smallsort.
        (* Trait *)
        (* Empty module 'StableSmallSortTypeImpl' *)
        
        Module Impl_core_slice_sort_shared_smallsort_StableSmallSortTypeImpl_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              default fn small_sort_threshold() -> usize {
                  // Optimal number of comparisons, and good perf.
                  SMALL_SORT_FALLBACK_THRESHOLD
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.read (|
                  M.get_constant (|
                    "core::slice::sort::shared::smallsort::SMALL_SORT_FALLBACK_THRESHOLD"
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              default fn small_sort<F: FnMut(&T, &T) -> bool>(
                  v: &mut [T],
                  _scratch: &mut [MaybeUninit<T>],
                  is_less: &mut F,
              ) {
                  if v.len() >= 2 {
                      insertion_sort_shift_left(v, 1, is_less);
                  }
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; _scratch; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let _scratch := M.alloc (| _scratch |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  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") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| v |) ]
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          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.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::StableSmallSortTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_StableSmallSortTypeImpl_for_T.
        
        Module Impl_core_slice_sort_shared_smallsort_StableSmallSortTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              fn small_sort_threshold() -> usize {
                  SMALL_SORT_GENERAL_THRESHOLD
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.read (|
                  M.get_constant (|
                    "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_THRESHOLD"
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              fn small_sort<F: FnMut(&T, &T) -> bool>(
                  v: &mut [T],
                  scratch: &mut [MaybeUninit<T>],
                  is_less: &mut F,
              ) {
                  small_sort_general_with_scratch(v, scratch, is_less);
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; scratch; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let scratch := M.alloc (| scratch |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::small_sort_general_with_scratch",
                          [ T; F ]
                        |),
                        [ M.read (| v |); M.read (| scratch |); M.read (| is_less |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::StableSmallSortTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_StableSmallSortTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
        
        (* Trait *)
        (* Empty module 'UnstableSmallSortTypeImpl' *)
        
        Module Impl_core_slice_sort_shared_smallsort_UnstableSmallSortTypeImpl_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              default fn small_sort_threshold() -> usize {
                  SMALL_SORT_FALLBACK_THRESHOLD
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.read (|
                  M.get_constant (|
                    "core::slice::sort::shared::smallsort::SMALL_SORT_FALLBACK_THRESHOLD"
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              default fn small_sort<F>(v: &mut [T], is_less: &mut F)
              where
                  F: FnMut(&T, &T) -> bool,
              {
                  small_sort_fallback(v, is_less);
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::small_sort_fallback",
                          [ T; F ]
                        |),
                        [ M.read (| v |); M.read (| is_less |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::UnstableSmallSortTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_UnstableSmallSortTypeImpl_for_T.
        
        Module Impl_core_slice_sort_shared_smallsort_UnstableSmallSortTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              fn small_sort_threshold() -> usize {
                  <T as UnstableSmallSortFreezeTypeImpl>::small_sort_threshold()
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl",
                    T,
                    [],
                    "small_sort_threshold",
                    []
                  |),
                  []
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              fn small_sort<F>(v: &mut [T], is_less: &mut F)
              where
                  F: FnMut(&T, &T) -> bool,
              {
                  <T as UnstableSmallSortFreezeTypeImpl>::small_sort(v, is_less);
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl",
                          T,
                          [],
                          "small_sort",
                          [ F ]
                        |),
                        [ M.read (| v |); M.read (| is_less |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::UnstableSmallSortTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_UnstableSmallSortTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
        
        (* Trait *)
        (* Empty module 'UnstableSmallSortFreezeTypeImpl' *)
        
        Module Impl_core_slice_sort_shared_smallsort_UnstableSmallSortFreezeTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              default fn small_sort_threshold() -> usize {
                  if (mem::size_of::<T>() * SMALL_SORT_GENERAL_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE {
                      SMALL_SORT_GENERAL_THRESHOLD
                  } else {
                      SMALL_SORT_FALLBACK_THRESHOLD
                  }
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.le (|
                                  BinOp.Wrap.mul (|
                                    M.call_closure (|
                                      M.get_function (| "core::mem::size_of", [ T ] |),
                                      []
                                    |),
                                    M.read (|
                                      M.get_constant (|
                                        "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                                      |)
                                    |)
                                  |),
                                  M.read (|
                                    M.get_constant (|
                                      "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.get_constant (|
                            "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_THRESHOLD"
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.get_constant (|
                            "core::slice::sort::shared::smallsort::SMALL_SORT_FALLBACK_THRESHOLD"
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              default fn small_sort<F>(v: &mut [T], is_less: &mut F)
              where
                  F: FnMut(&T, &T) -> bool,
              {
                  if (mem::size_of::<T>() * SMALL_SORT_GENERAL_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE {
                      small_sort_general(v, is_less);
                  } else {
                      small_sort_fallback(v, is_less);
                  }
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.le (|
                                  BinOp.Wrap.mul (|
                                    M.call_closure (|
                                      M.get_function (| "core::mem::size_of", [ T ] |),
                                      []
                                    |),
                                    M.read (|
                                      M.get_constant (|
                                        "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                                      |)
                                    |)
                                  |),
                                  M.read (|
                                    M.get_constant (|
                                      "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::smallsort::small_sort_general",
                                  [ T; F ]
                                |),
                                [ M.read (| v |); M.read (| is_less |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::smallsort::small_sort_fallback",
                                  [ T; F ]
                                |),
                                [ M.read (| v |); M.read (| is_less |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_UnstableSmallSortFreezeTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_for_T.
        
        (* Trait *)
        (* Empty module 'CopyMarker' *)
        
        Module Impl_core_slice_sort_shared_smallsort_CopyMarker_where_core_marker_Copy_T_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::CopyMarker"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *) [].
        End Impl_core_slice_sort_shared_smallsort_CopyMarker_where_core_marker_Copy_T_for_T.
        
        Module Impl_core_slice_sort_shared_smallsort_UnstableSmallSortFreezeTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_where_core_slice_sort_shared_smallsort_CopyMarker_T_for_T.
          Definition Self (T : Ty.t) : Ty.t := T.
          
          (*
              fn small_sort_threshold() -> usize {
                  if has_efficient_in_place_swap::<T>()
                      && (mem::size_of::<T>() * SMALL_SORT_NETWORK_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE
                  {
                      SMALL_SORT_NETWORK_THRESHOLD
                  } else if (mem::size_of::<T>() * SMALL_SORT_GENERAL_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE {
                      SMALL_SORT_GENERAL_THRESHOLD
                  } else {
                      SMALL_SORT_FALLBACK_THRESHOLD
                  }
              }
          *)
          Definition small_sort_threshold
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [] =>
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::slice::sort::shared::smallsort::has_efficient_in_place_swap",
                                      [ T ]
                                    |),
                                    []
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      BinOp.Wrap.mul (|
                                        M.call_closure (|
                                          M.get_function (| "core::mem::size_of", [ T ] |),
                                          []
                                        |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::sort::shared::smallsort::SMALL_SORT_NETWORK_SCRATCH_LEN"
                                          |)
                                        |)
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.get_constant (|
                            "core::slice::sort::shared::smallsort::SMALL_SORT_NETWORK_THRESHOLD"
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.le (|
                                          BinOp.Wrap.mul (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::size_of", [ T ] |),
                                              []
                                            |),
                                            M.read (|
                                              M.get_constant (|
                                                "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                                              |)
                                            |)
                                          |),
                                          M.read (|
                                            M.get_constant (|
                                              "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.get_constant (|
                                    "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_THRESHOLD"
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.get_constant (|
                                    "core::slice::sort::shared::smallsort::SMALL_SORT_FALLBACK_THRESHOLD"
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          (*
              fn small_sort<F>(v: &mut [T], is_less: &mut F)
              where
                  F: FnMut(&T, &T) -> bool,
              {
                  if has_efficient_in_place_swap::<T>()
                      && (mem::size_of::<T>() * SMALL_SORT_NETWORK_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE
                  {
                      small_sort_network(v, is_less);
                  } else if (mem::size_of::<T>() * SMALL_SORT_GENERAL_SCRATCH_LEN) <= MAX_STACK_ARRAY_SIZE {
                      small_sort_general(v, is_less);
                  } else {
                      small_sort_fallback(v, is_less);
                  }
              }
          *)
          Definition small_sort
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ v; is_less ] =>
              ltac:(M.monadic
                (let v := M.alloc (| v |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::slice::sort::shared::smallsort::has_efficient_in_place_swap",
                                      [ T ]
                                    |),
                                    []
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      BinOp.Wrap.mul (|
                                        M.call_closure (|
                                          M.get_function (| "core::mem::size_of", [ T ] |),
                                          []
                                        |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::sort::shared::smallsort::SMALL_SORT_NETWORK_SCRATCH_LEN"
                                          |)
                                        |)
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::smallsort::small_sort_network",
                                  [ T; F ]
                                |),
                                [ M.read (| v |); M.read (| is_less |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.le (|
                                          BinOp.Wrap.mul (|
                                            M.call_closure (|
                                              M.get_function (| "core::mem::size_of", [ T ] |),
                                              []
                                            |),
                                            M.read (|
                                              M.get_constant (|
                                                "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                                              |)
                                            |)
                                          |),
                                          M.read (|
                                            M.get_constant (|
                                              "core::slice::sort::shared::smallsort::MAX_STACK_ARRAY_SIZE"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::slice::sort::shared::smallsort::small_sort_general",
                                          [ T; F ]
                                        |),
                                        [ M.read (| v |); M.read (| is_less |) ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::slice::sort::shared::smallsort::small_sort_fallback",
                                          [ T; F ]
                                        |),
                                        [ M.read (| v |); M.read (| is_less |) ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("small_sort_threshold", InstanceField.Method (small_sort_threshold T));
                ("small_sort", InstanceField.Method (small_sort T))
              ].
        End Impl_core_slice_sort_shared_smallsort_UnstableSmallSortFreezeTypeImpl_where_core_slice_sort_shared_FreezeMarker_T_where_core_slice_sort_shared_smallsort_CopyMarker_T_for_T.
        
        Definition value_SMALL_SORT_FALLBACK_THRESHOLD : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 16 |))).
        
        Definition value_SMALL_SORT_GENERAL_THRESHOLD : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 32 |))).
        
        Definition value_SMALL_SORT_GENERAL_SCRATCH_LEN : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                BinOp.Wrap.add (|
                  M.read (|
                    M.get_constant (|
                      "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_THRESHOLD"
                    |)
                  |),
                  Value.Integer IntegerKind.Usize 16
                |)
              |))).
        
        Definition value_SMALL_SORT_NETWORK_THRESHOLD : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 32 |))).
        
        Definition value_SMALL_SORT_NETWORK_SCRATCH_LEN : Value.t :=
          M.run
            ltac:(M.monadic
              (M.get_constant (|
                "core::slice::sort::shared::smallsort::SMALL_SORT_NETWORK_THRESHOLD"
              |))).
        
        Definition value_MAX_STACK_ARRAY_SIZE : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 4096 |))).
        
        (*
        fn small_sort_fallback<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
            if v.len() >= 2 {
                insertion_sort_shift_left(v, 1, is_less);
            }
        }
        *)
        Definition small_sort_fallback (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                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") [] [ T ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| v |) ]
                                |),
                                Value.Integer IntegerKind.Usize 2
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        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.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_small_sort_fallback :
          M.IsFunction
            "core::slice::sort::shared::smallsort::small_sort_fallback"
            small_sort_fallback.
        
        (*
        fn small_sort_general<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
            let mut stack_array = MaybeUninit::<[T; SMALL_SORT_GENERAL_SCRATCH_LEN]>::uninit();
        
            // SAFETY: The memory is backed by `stack_array`, and the operation is safe as long as the len
            // is the same.
            let scratch = unsafe {
                slice::from_raw_parts_mut(
                    stack_array.as_mut_ptr() as *mut MaybeUninit<T>,
                    SMALL_SORT_GENERAL_SCRATCH_LEN,
                )
            };
        
            small_sort_general_with_scratch(v, scratch, is_less);
        }
        *)
        Definition small_sort_general (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ stack_array :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                          []
                          [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 48 ] [ T ]
                          ],
                        "uninit",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ scratch :=
                  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.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 48 ]
                                    [ T ]
                                ],
                              "as_mut_ptr",
                              []
                            |),
                            [ stack_array ]
                          |));
                        M.read (|
                          M.get_constant (|
                            "core::slice::sort::shared::smallsort::SMALL_SORT_GENERAL_SCRATCH_LEN"
                          |)
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::small_sort_general_with_scratch",
                        [ T; F ]
                      |),
                      [ M.read (| v |); M.read (| scratch |); M.read (| is_less |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_small_sort_general :
          M.IsFunction
            "core::slice::sort::shared::smallsort::small_sort_general"
            small_sort_general.
        
        (*
        fn small_sort_general_with_scratch<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(
            v: &mut [T],
            scratch: &mut [MaybeUninit<T>],
            is_less: &mut F,
        ) {
            let len = v.len();
            if len < 2 {
                return;
            }
        
            if scratch.len() < len + 16 {
                intrinsics::abort();
            }
        
            let v_base = v.as_mut_ptr();
            let len_div_2 = len / 2;
        
            // SAFETY: See individual comments.
            unsafe {
                let scratch_base = scratch.as_mut_ptr() as *mut T;
        
                let presorted_len = if const { mem::size_of::<T>() <= 16 } && len >= 16 {
                    // SAFETY: scratch_base is valid and has enough space.
                    sort8_stable(v_base, scratch_base, scratch_base.add(len), is_less);
                    sort8_stable(
                        v_base.add(len_div_2),
                        scratch_base.add(len_div_2),
                        scratch_base.add(len + 8),
                        is_less,
                    );
        
                    8
                } else if len >= 8 {
                    // SAFETY: scratch_base is valid and has enough space.
                    sort4_stable(v_base, scratch_base, is_less);
                    sort4_stable(v_base.add(len_div_2), scratch_base.add(len_div_2), is_less);
        
                    4
                } else {
                    ptr::copy_nonoverlapping(v_base, scratch_base, 1);
                    ptr::copy_nonoverlapping(v_base.add(len_div_2), scratch_base.add(len_div_2), 1);
        
                    1
                };
        
                for offset in [0, len_div_2] {
                    // SAFETY: at this point dst is initialized with presorted_len elements.
                    // We extend this to desired_len, src is valid for desired_len elements.
                    let src = v_base.add(offset);
                    let dst = scratch_base.add(offset);
                    let desired_len = if offset == 0 { len_div_2 } else { len - len_div_2 };
        
                    for i in presorted_len..desired_len {
                        ptr::copy_nonoverlapping(src.add(i), dst.add(i), 1);
                        insert_tail(dst, dst.add(i), is_less);
                    }
                }
        
                // SAFETY: see comment in `CopyOnDrop::drop`.
                let drop_guard = CopyOnDrop { src: scratch_base, dst: v_base, len };
        
                // SAFETY: at this point scratch_base is fully initialized, allowing us
                // to use it as the source of our merge back into the original array.
                // If a panic occurs we ensure the original array is restored to a valid
                // permutation of the input through drop_guard. This technique is similar
                // to ping-pong merging.
                bidirectional_merge(
                    &*ptr::slice_from_raw_parts(drop_guard.src, drop_guard.len),
                    drop_guard.dst,
                    is_less,
                );
                mem::forget(drop_guard);
            }
        }
        *)
        Definition small_sort_general_with_scratch
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; scratch; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let scratch := M.alloc (| scratch |) in
              let is_less := M.alloc (| is_less |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    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 (|
                                    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 (|
                                    BinOp.lt (|
                                      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 (| scratch |) ]
                                      |),
                                      BinOp.Wrap.add (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 16
                                      |)
                                    |)
                                  |)) 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::abort", [] |),
                                    []
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ v_base :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "as_mut_ptr",
                            []
                          |),
                          [ M.read (| v |) ]
                        |)
                      |) in
                    let~ len_div_2 :=
                      M.alloc (|
                        BinOp.Wrap.div (| M.read (| len |), Value.Integer IntegerKind.Usize 2 |)
                      |) in
                    let~ scratch_base :=
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| scratch |) ]
                          |))
                      |) in
                    let~ presorted_len :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      LogicalOp.and (|
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::sort::shared::smallsort::small_sort_general_with_scratch_discriminant"
                                          |)
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.ge (|
                                            M.read (| len |),
                                            Value.Integer IntegerKind.Usize 16
                                          |)))
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::sort::shared::smallsort::sort8_stable",
                                        [ T; F ]
                                      |),
                                      [
                                        M.read (| v_base |);
                                        M.read (| scratch_base |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "*mut") [] [ T ],
                                            "add",
                                            []
                                          |),
                                          [ M.read (| scratch_base |); M.read (| len |) ]
                                        |);
                                        M.read (| is_less |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::slice::sort::shared::smallsort::sort8_stable",
                                        [ T; F ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "*mut") [] [ T ],
                                            "add",
                                            []
                                          |),
                                          [ M.read (| v_base |); M.read (| len_div_2 |) ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "*mut") [] [ T ],
                                            "add",
                                            []
                                          |),
                                          [ M.read (| scratch_base |); M.read (| len_div_2 |) ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "*mut") [] [ T ],
                                            "add",
                                            []
                                          |),
                                          [
                                            M.read (| scratch_base |);
                                            BinOp.Wrap.add (|
                                              M.read (| len |),
                                              Value.Integer IntegerKind.Usize 8
                                            |)
                                          ]
                                        |);
                                        M.read (| is_less |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 8 |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.ge (|
                                                M.read (| len |),
                                                Value.Integer IntegerKind.Usize 8
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::sort::shared::smallsort::sort4_stable",
                                                [ T; F ]
                                              |),
                                              [
                                                (* MutToConstPointer *)
                                                M.pointer_coercion (M.read (| v_base |));
                                                M.read (| scratch_base |);
                                                M.read (| is_less |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::sort::shared::smallsort::sort4_stable",
                                                [ T; F ]
                                              |),
                                              [
                                                (* MutToConstPointer *)
                                                M.pointer_coercion
                                                  (M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "add",
                                                      []
                                                    |),
                                                    [ M.read (| v_base |); M.read (| len_div_2 |) ]
                                                  |));
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| scratch_base |);
                                                    M.read (| len_div_2 |)
                                                  ]
                                                |);
                                                M.read (| is_less |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Integer IntegerKind.Usize 4 |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::intrinsics::copy_nonoverlapping",
                                                [ T ]
                                              |),
                                              [
                                                (* MutToConstPointer *)
                                                M.pointer_coercion (M.read (| v_base |));
                                                M.read (| scratch_base |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::intrinsics::copy_nonoverlapping",
                                                [ T ]
                                              |),
                                              [
                                                (* MutToConstPointer *)
                                                M.pointer_coercion
                                                  (M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "add",
                                                      []
                                                    |),
                                                    [ M.read (| v_base |); M.read (| len_div_2 |) ]
                                                  |));
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| scratch_base |);
                                                    M.read (| len_div_2 |)
                                                  ]
                                                |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Integer IntegerKind.Usize 1 |)))
                                  ]
                                |)))
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 2 ]
                                  [ Ty.path "usize" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                Value.Array
                                  [ Value.Integer IntegerKind.Usize 0; M.read (| len_div_2 |) ]
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::array::iter::IntoIter")
                                                [ Value.Integer IntegerKind.Usize 2 ]
                                                [ Ty.path "usize" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let offset := M.copy (| γ0_0 |) in
                                              let~ src :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "add",
                                                      []
                                                    |),
                                                    [ M.read (| v_base |); M.read (| offset |) ]
                                                  |)
                                                |) in
                                              let~ dst :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "add",
                                                      []
                                                    |),
                                                    [ M.read (| scratch_base |); M.read (| offset |)
                                                    ]
                                                  |)
                                                |) in
                                              let~ desired_len :=
                                                M.copy (|
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.eq (|
                                                                  M.read (| offset |),
                                                                  Value.Integer IntegerKind.Usize 0
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          len_div_2));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (|
                                                            BinOp.Wrap.sub (|
                                                              M.read (| len |),
                                                              M.read (| len_div_2 |)
                                                            |)
                                                          |)))
                                                    ]
                                                  |)
                                                |) in
                                              M.use
                                                (M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::iter::traits::collect::IntoIterator",
                                                        Ty.apply
                                                          (Ty.path "core::ops::range::Range")
                                                          []
                                                          [ Ty.path "usize" ],
                                                        [],
                                                        "into_iter",
                                                        []
                                                      |),
                                                      [
                                                        Value.StructRecord
                                                          "core::ops::range::Range"
                                                          [
                                                            ("start", M.read (| presorted_len |));
                                                            ("end_", M.read (| desired_len |))
                                                          ]
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let iter := M.copy (| γ |) in
                                                        M.loop (|
                                                          ltac:(M.monadic
                                                            (let~ _ :=
                                                              M.match_operator (|
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::iter::traits::iterator::Iterator",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::ops::range::Range")
                                                                        []
                                                                        [ Ty.path "usize" ],
                                                                      [],
                                                                      "next",
                                                                      []
                                                                    |),
                                                                    [ iter ]
                                                                  |)
                                                                |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let _ :=
                                                                        M.is_struct_tuple (|
                                                                          γ,
                                                                          "core::option::Option::None"
                                                                        |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (| M.break (||) |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ0_0 :=
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          γ,
                                                                          "core::option::Option::Some",
                                                                          0
                                                                        |) in
                                                                      let i := M.copy (| γ0_0 |) in
                                                                      let~ _ :=
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::intrinsics::copy_nonoverlapping",
                                                                              [ T ]
                                                                            |),
                                                                            [
                                                                              (* MutToConstPointer *)
                                                                              M.pointer_coercion
                                                                                (M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "*mut")
                                                                                      []
                                                                                      [ T ],
                                                                                    "add",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.read (|
                                                                                      src
                                                                                    |);
                                                                                    M.read (| i |)
                                                                                  ]
                                                                                |));
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path "*mut")
                                                                                    []
                                                                                    [ T ],
                                                                                  "add",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (| dst |);
                                                                                  M.read (| i |)
                                                                                ]
                                                                              |);
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            ]
                                                                          |)
                                                                        |) in
                                                                      let~ _ :=
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::slice::sort::shared::smallsort::insert_tail",
                                                                              [ T; F ]
                                                                            |),
                                                                            [
                                                                              M.read (| dst |);
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path "*mut")
                                                                                    []
                                                                                    [ T ],
                                                                                  "add",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (| dst |);
                                                                                  M.read (| i |)
                                                                                ]
                                                                              |);
                                                                              M.read (| is_less |)
                                                                            ]
                                                                          |)
                                                                        |) in
                                                                      M.alloc (| Value.Tuple [] |)))
                                                                ]
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)))
                                                        |)))
                                                  ]
                                                |))))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    let~ drop_guard :=
                      M.alloc (|
                        Value.StructRecord
                          "core::slice::sort::shared::smallsort::CopyOnDrop"
                          [
                            ("src",
                              (* MutToConstPointer *)
                              M.pointer_coercion (M.read (| scratch_base |)));
                            ("dst", M.read (| v_base |));
                            ("len", M.read (| len |))
                          ]
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::sort::shared::smallsort::bidirectional_merge",
                            [ T; F ]
                          |),
                          [
                            M.call_closure (|
                              M.get_function (| "core::ptr::slice_from_raw_parts", [ T ] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    drop_guard,
                                    "core::slice::sort::shared::smallsort::CopyOnDrop",
                                    "src"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    drop_guard,
                                    "core::slice::sort::shared::smallsort::CopyOnDrop",
                                    "len"
                                  |)
                                |)
                              ]
                            |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                drop_guard,
                                "core::slice::sort::shared::smallsort::CopyOnDrop",
                                "dst"
                              |)
                            |);
                            M.read (| is_less |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::mem::forget",
                            [
                              Ty.apply
                                (Ty.path "core::slice::sort::shared::smallsort::CopyOnDrop")
                                []
                                [ T ]
                            ]
                          |),
                          [ M.read (| drop_guard |) ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_small_sort_general_with_scratch :
          M.IsFunction
            "core::slice::sort::shared::smallsort::small_sort_general_with_scratch"
            small_sort_general_with_scratch.
        
        (* StructRecord
          {
            name := "CopyOnDrop";
            const_params := [];
            ty_params := [ "T" ];
            fields :=
              [
                ("src", Ty.apply (Ty.path "*const") [] [ T ]);
                ("dst", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("len", Ty.path "usize")
              ];
          } *)
        
        Module Impl_core_ops_drop_Drop_for_core_slice_sort_shared_smallsort_CopyOnDrop_T.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "core::slice::sort::shared::smallsort::CopyOnDrop") [] [ T ].
          
          (*
              fn drop(&mut self) {
                  // SAFETY: `src` must contain `len` initialized elements, and dst must
                  // be valid to write `len` elements.
                  unsafe {
                      ptr::copy_nonoverlapping(self.src, self.dst, self.len);
                  }
              }
          *)
          Definition drop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::shared::smallsort::CopyOnDrop",
                              "src"
                            |)
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::shared::smallsort::CopyOnDrop",
                              "dst"
                            |)
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::shared::smallsort::CopyOnDrop",
                              "len"
                            |)
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::ops::drop::Drop"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("drop", InstanceField.Method (drop T)) ].
        End Impl_core_ops_drop_Drop_for_core_slice_sort_shared_smallsort_CopyOnDrop_T.
        
        (*
        fn small_sort_network<T, F>(v: &mut [T], is_less: &mut F)
        where
            T: FreezeMarker,
            F: FnMut(&T, &T) -> bool,
        {
            // This implementation is tuned to be efficient for integer types.
        
            let len = v.len();
            if len < 2 {
                return;
            }
        
            if len > SMALL_SORT_NETWORK_SCRATCH_LEN {
                intrinsics::abort();
            }
        
            let mut stack_array = MaybeUninit::<[T; SMALL_SORT_NETWORK_SCRATCH_LEN]>::uninit();
        
            let len_div_2 = len / 2;
            let no_merge = len < 18;
        
            let v_base = v.as_mut_ptr();
            let initial_region_len = if no_merge { len } else { len_div_2 };
            // SAFETY: Both possible values of `initial_region_len` are in-bounds.
            let mut region = unsafe { &mut *ptr::slice_from_raw_parts_mut(v_base, initial_region_len) };
        
            // Avoid compiler unrolling, we *really* don't want that to happen here for binary-size reasons.
            loop {
                let presorted_len = if region.len() >= 13 {
                    sort13_optimal(region, is_less);
                    13
                } else if region.len() >= 9 {
                    sort9_optimal(region, is_less);
                    9
                } else {
                    1
                };
        
                insertion_sort_shift_left(region, presorted_len, is_less);
        
                if no_merge {
                    return;
                }
        
                if region.as_ptr() != v_base {
                    break;
                }
        
                // SAFETY: The right side of `v` based on `len_div_2` is guaranteed in-bounds.
                unsafe {
                    region = &mut *ptr::slice_from_raw_parts_mut(v_base.add(len_div_2), len - len_div_2)
                };
            }
        
            // SAFETY: We checked that T is Freeze and thus observation safe.
            // Should is_less panic v was not modified in parity_merge and retains it's original input.
            // scratch and v must not alias and scratch has v.len() space.
            unsafe {
                let scratch_base = stack_array.as_mut_ptr() as *mut T;
                bidirectional_merge(
                    &mut *ptr::slice_from_raw_parts_mut(v_base, len),
                    scratch_base,
                    is_less,
                );
                ptr::copy_nonoverlapping(scratch_base, v_base, len);
            }
        }
        *)
        Definition small_sort_network (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ 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~ 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 (|
                                    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 (|
                                    BinOp.gt (|
                                      M.read (| len |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::slice::sort::shared::smallsort::SMALL_SORT_NETWORK_SCRATCH_LEN"
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::abort", [] |),
                                    []
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ stack_array :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 32 ]
                                  [ T ]
                              ],
                            "uninit",
                            []
                          |),
                          []
                        |)
                      |) in
                    let~ len_div_2 :=
                      M.alloc (|
                        BinOp.Wrap.div (| M.read (| len |), Value.Integer IntegerKind.Usize 2 |)
                      |) in
                    let~ no_merge :=
                      M.alloc (|
                        BinOp.lt (| M.read (| len |), Value.Integer IntegerKind.Usize 18 |)
                      |) in
                    let~ v_base :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "as_mut_ptr",
                            []
                          |),
                          [ M.read (| v |) ]
                        |)
                      |) in
                    let~ initial_region_len :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use no_merge in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                len));
                            fun γ => ltac:(M.monadic len_div_2)
                          ]
                        |)
                      |) in
                    let~ region :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                          [ M.read (| v_base |); M.read (| initial_region_len |) ]
                        |)
                      |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (let~ presorted_len :=
                            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") [] [ T ],
                                                  "len",
                                                  []
                                                |),
                                                [ M.read (| region |) ]
                                              |),
                                              Value.Integer IntegerKind.Usize 13
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::slice::sort::shared::smallsort::sort13_optimal",
                                              [ T; F ]
                                            |),
                                            [ M.read (| region |); M.read (| is_less |) ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Integer IntegerKind.Usize 13 |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (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") [] [ T ],
                                                          "len",
                                                          []
                                                        |),
                                                        [ M.read (| region |) ]
                                                      |),
                                                      Value.Integer IntegerKind.Usize 9
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::slice::sort::shared::smallsort::sort9_optimal",
                                                      [ T; F ]
                                                    |),
                                                    [ M.read (| region |); M.read (| is_less |) ]
                                                  |)
                                                |) in
                                              M.alloc (| Value.Integer IntegerKind.Usize 9 |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.alloc (| Value.Integer IntegerKind.Usize 1 |)))
                                        ]
                                      |)))
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::smallsort::insertion_sort_shift_left",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| region |);
                                  M.read (| presorted_len |);
                                  M.read (| is_less |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use no_merge 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 (|
                                          BinOp.ne (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [ M.read (| region |) ]
                                            |),
                                            (* MutToConstPointer *)
                                            M.pointer_coercion (M.read (| v_base |))
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.write (|
                              region,
                              M.call_closure (|
                                M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [ M.read (| v_base |); M.read (| len_div_2 |) ]
                                  |);
                                  BinOp.Wrap.sub (| M.read (| len |), M.read (| len_div_2 |) |)
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |) in
                    let~ scratch_base :=
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    [ T ]
                                ],
                              "as_mut_ptr",
                              []
                            |),
                            [ stack_array ]
                          |))
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::slice::sort::shared::smallsort::bidirectional_merge",
                            [ T; F ]
                          |),
                          [
                            M.call_closure (|
                              M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                              [ M.read (| v_base |); M.read (| len |) ]
                            |);
                            M.read (| scratch_base |);
                            M.read (| is_less |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                          [
                            (* MutToConstPointer *) M.pointer_coercion (M.read (| scratch_base |));
                            M.read (| v_base |);
                            M.read (| len |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_small_sort_network :
          M.IsFunction
            "core::slice::sort::shared::smallsort::small_sort_network"
            small_sort_network.
        
        (*
        unsafe fn swap_if_less<T, F>(v_base: *mut T, a_pos: usize, b_pos: usize, is_less: &mut F)
        where
            F: FnMut(&T, &T) -> bool,
        {
            // SAFETY: the caller must guarantee that `a` and `b` each added to `v_base` yield valid
            // pointers into `v_base`, and are properly aligned, and part of the same allocation.
            unsafe {
                let v_a = v_base.add(a_pos);
                let v_b = v_base.add(b_pos);
        
                // PANIC SAFETY: if is_less panics, no scratch memory was created and the slice should still be
                // in a well defined state, without duplicates.
        
                // Important to only swap if it is more and not if it is equal. is_less should return false for
                // equal, so we don't swap.
                let should_swap = is_less(&*v_b, &*v_a);
        
                // This is a branchless version of swap if.
                // The equivalent code with a branch would be:
                //
                // if should_swap {
                //     ptr::swap(left, right, 1);
                // }
        
                // The goal is to generate cmov instructions here.
                let left_swap = if should_swap { v_b } else { v_a };
                let right_swap = if should_swap { v_a } else { v_b };
        
                let right_swap_tmp = ManuallyDrop::new(ptr::read(right_swap));
                ptr::copy(left_swap, v_a, 1);
                ptr::copy_nonoverlapping(&*right_swap_tmp, v_b, 1);
            }
        }
        *)
        Definition swap_if_less (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v_base; a_pos; b_pos; is_less ] =>
            ltac:(M.monadic
              (let v_base := M.alloc (| v_base |) in
              let a_pos := M.alloc (| a_pos |) in
              let b_pos := M.alloc (| b_pos |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ v_a :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "add", [] |),
                      [ M.read (| v_base |); M.read (| a_pos |) ]
                    |)
                  |) in
                let~ v_b :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "add", [] |),
                      [ M.read (| v_base |); M.read (| b_pos |) ]
                    |)
                  |) in
                let~ should_swap :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::function::FnMut",
                        F,
                        [
                          Ty.tuple
                            [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                        ],
                        "call_mut",
                        []
                      |),
                      [ M.read (| is_less |); Value.Tuple [ M.read (| v_b |); M.read (| v_a |) ] ]
                    |)
                  |) in
                let~ left_swap :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.use should_swap in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            v_b));
                        fun γ => ltac:(M.monadic v_a)
                      ]
                    |)
                  |) in
                let~ right_swap :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.use should_swap in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            v_a));
                        fun γ => ltac:(M.monadic v_b)
                      ]
                    |)
                  |) in
                let~ right_swap_tmp :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                        "new",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_function (| "core::ptr::read", [ T ] |),
                          [ (* MutToConstPointer *) M.pointer_coercion (M.read (| right_swap |)) ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::intrinsics::copy", [ T ] |),
                      [
                        (* MutToConstPointer *) M.pointer_coercion (M.read (| left_swap |));
                        M.read (| v_a |);
                        Value.Integer IntegerKind.Usize 1
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                            [],
                            "deref",
                            []
                          |),
                          [ right_swap_tmp ]
                        |);
                        M.read (| v_b |);
                        Value.Integer IntegerKind.Usize 1
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_swap_if_less :
          M.IsFunction "core::slice::sort::shared::smallsort::swap_if_less" swap_if_less.
        
        (*
        fn sort9_optimal<T, F>(v: &mut [T], is_less: &mut F)
        where
            F: FnMut(&T, &T) -> bool,
        {
            if v.len() < 9 {
                intrinsics::abort();
            }
        
            let v_base = v.as_mut_ptr();
        
            // Optimal sorting network see:
            // https://bertdobbelaere.github.io/sorting_networks.html.
        
            // SAFETY: We checked the len.
            unsafe {
                swap_if_less(v_base, 0, 3, is_less);
                swap_if_less(v_base, 1, 7, is_less);
                swap_if_less(v_base, 2, 5, is_less);
                swap_if_less(v_base, 4, 8, is_less);
                swap_if_less(v_base, 0, 7, is_less);
                swap_if_less(v_base, 2, 4, is_less);
                swap_if_less(v_base, 3, 8, is_less);
                swap_if_less(v_base, 5, 6, is_less);
                swap_if_less(v_base, 0, 2, is_less);
                swap_if_less(v_base, 1, 3, is_less);
                swap_if_less(v_base, 4, 5, is_less);
                swap_if_less(v_base, 7, 8, is_less);
                swap_if_less(v_base, 1, 4, is_less);
                swap_if_less(v_base, 3, 6, is_less);
                swap_if_less(v_base, 5, 7, is_less);
                swap_if_less(v_base, 0, 1, is_less);
                swap_if_less(v_base, 2, 4, is_less);
                swap_if_less(v_base, 3, 5, is_less);
                swap_if_less(v_base, 6, 8, is_less);
                swap_if_less(v_base, 2, 3, is_less);
                swap_if_less(v_base, 4, 5, is_less);
                swap_if_less(v_base, 6, 7, is_less);
                swap_if_less(v_base, 1, 2, is_less);
                swap_if_less(v_base, 3, 4, is_less);
                swap_if_less(v_base, 5, 6, is_less);
            }
        }
        *)
        Definition sort9_optimal (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| v |) ]
                                  |),
                                  Value.Integer IntegerKind.Usize 9
                                |)
                              |)) 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::abort", [] |),
                                []
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ v_base :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_mut_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 2;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 7;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 1;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 2;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_sort9_optimal :
          M.IsFunction "core::slice::sort::shared::smallsort::sort9_optimal" sort9_optimal.
        
        (*
        fn sort13_optimal<T, F>(v: &mut [T], is_less: &mut F)
        where
            F: FnMut(&T, &T) -> bool,
        {
            if v.len() < 13 {
                intrinsics::abort();
            }
        
            let v_base = v.as_mut_ptr();
        
            // Optimal sorting network see:
            // https://bertdobbelaere.github.io/sorting_networks.html.
        
            // SAFETY: We checked the len.
            unsafe {
                swap_if_less(v_base, 0, 12, is_less);
                swap_if_less(v_base, 1, 10, is_less);
                swap_if_less(v_base, 2, 9, is_less);
                swap_if_less(v_base, 3, 7, is_less);
                swap_if_less(v_base, 5, 11, is_less);
                swap_if_less(v_base, 6, 8, is_less);
                swap_if_less(v_base, 1, 6, is_less);
                swap_if_less(v_base, 2, 3, is_less);
                swap_if_less(v_base, 4, 11, is_less);
                swap_if_less(v_base, 7, 9, is_less);
                swap_if_less(v_base, 8, 10, is_less);
                swap_if_less(v_base, 0, 4, is_less);
                swap_if_less(v_base, 1, 2, is_less);
                swap_if_less(v_base, 3, 6, is_less);
                swap_if_less(v_base, 7, 8, is_less);
                swap_if_less(v_base, 9, 10, is_less);
                swap_if_less(v_base, 11, 12, is_less);
                swap_if_less(v_base, 4, 6, is_less);
                swap_if_less(v_base, 5, 9, is_less);
                swap_if_less(v_base, 8, 11, is_less);
                swap_if_less(v_base, 10, 12, is_less);
                swap_if_less(v_base, 0, 5, is_less);
                swap_if_less(v_base, 3, 8, is_less);
                swap_if_less(v_base, 4, 7, is_less);
                swap_if_less(v_base, 6, 11, is_less);
                swap_if_less(v_base, 9, 10, is_less);
                swap_if_less(v_base, 0, 1, is_less);
                swap_if_less(v_base, 2, 5, is_less);
                swap_if_less(v_base, 6, 9, is_less);
                swap_if_less(v_base, 7, 8, is_less);
                swap_if_less(v_base, 10, 11, is_less);
                swap_if_less(v_base, 1, 3, is_less);
                swap_if_less(v_base, 2, 4, is_less);
                swap_if_less(v_base, 5, 6, is_less);
                swap_if_less(v_base, 9, 10, is_less);
                swap_if_less(v_base, 1, 2, is_less);
                swap_if_less(v_base, 3, 4, is_less);
                swap_if_less(v_base, 5, 7, is_less);
                swap_if_less(v_base, 6, 8, is_less);
                swap_if_less(v_base, 2, 3, is_less);
                swap_if_less(v_base, 4, 5, is_less);
                swap_if_less(v_base, 6, 7, is_less);
                swap_if_less(v_base, 8, 9, is_less);
                swap_if_less(v_base, 3, 4, is_less);
                swap_if_less(v_base, 5, 6, is_less);
            }
        }
        *)
        Definition sort13_optimal (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| v |) ]
                                  |),
                                  Value.Integer IntegerKind.Usize 13
                                |)
                              |)) 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::abort", [] |),
                                []
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ v_base :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_mut_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 12;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 10;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 9;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 11;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 11;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 7;
                        Value.Integer IntegerKind.Usize 9;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 8;
                        Value.Integer IntegerKind.Usize 10;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 2;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 7;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 9;
                        Value.Integer IntegerKind.Usize 10;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 11;
                        Value.Integer IntegerKind.Usize 12;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 9;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 8;
                        Value.Integer IntegerKind.Usize 11;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 10;
                        Value.Integer IntegerKind.Usize 12;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 11;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 9;
                        Value.Integer IntegerKind.Usize 10;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 0;
                        Value.Integer IntegerKind.Usize 1;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 9;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 7;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 10;
                        Value.Integer IntegerKind.Usize 11;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 9;
                        Value.Integer IntegerKind.Usize 10;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 1;
                        Value.Integer IntegerKind.Usize 2;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 8;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 2;
                        Value.Integer IntegerKind.Usize 3;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 4;
                        Value.Integer IntegerKind.Usize 5;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 6;
                        Value.Integer IntegerKind.Usize 7;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 8;
                        Value.Integer IntegerKind.Usize 9;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 3;
                        Value.Integer IntegerKind.Usize 4;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::swap_if_less",
                        [ T; F ]
                      |),
                      [
                        M.read (| v_base |);
                        Value.Integer IntegerKind.Usize 5;
                        Value.Integer IntegerKind.Usize 6;
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_sort13_optimal :
          M.IsFunction "core::slice::sort::shared::smallsort::sort13_optimal" sort13_optimal.
        
        (*
        unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T, is_less: &mut F) {
            // SAFETY: see individual comments.
            unsafe {
                // SAFETY: in-bounds as tail > begin.
                let mut sift = tail.sub(1);
                if !is_less(&*tail, &*sift) {
                    return;
                }
        
                // SAFETY: after this read tail is never read from again, as we only ever
                // read from sift, sift < tail and we only ever decrease sift. Thus this is
                // effectively a move, not a copy. Should a panic occur, or we have found
                // the correct insertion position, gap_guard ensures the element is moved
                // back into the array.
                let tmp = ManuallyDrop::new(tail.read());
                let mut gap_guard = CopyOnDrop { src: &*tmp, dst: tail, len: 1 };
        
                loop {
                    // SAFETY: we move sift into the gap (which is valid), and point the
                    // gap guard destination at sift, ensuring that if a panic occurs the
                    // gap is once again filled.
                    ptr::copy_nonoverlapping(sift, gap_guard.dst, 1);
                    gap_guard.dst = sift;
        
                    if sift == begin {
                        break;
                    }
        
                    // SAFETY: we checked that sift != begin, thus this is in-bounds.
                    sift = sift.sub(1);
                    if !is_less(&tmp, &*sift) {
                        break;
                    }
                }
            }
        }
        *)
        Definition insert_tail (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ begin; tail; is_less ] =>
            ltac:(M.monadic
              (let begin := M.alloc (| begin |) in
              let tail := M.alloc (| tail |) in
              let is_less := M.alloc (| is_less |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ sift :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*mut") [] [ T ],
                            "sub",
                            []
                          |),
                          [ M.read (| tail |); Value.Integer IntegerKind.Usize 1 ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::function::FnMut",
                                          F,
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply (Ty.path "&") [] [ T ];
                                                Ty.apply (Ty.path "&") [] [ T ]
                                              ]
                                          ],
                                          "call_mut",
                                          []
                                        |),
                                        [
                                          M.read (| is_less |);
                                          Value.Tuple [ M.read (| tail |); M.read (| sift |) ]
                                        ]
                                      |)
                                    |)
                                  |)) 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~ tmp :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                            "new",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*mut") [] [ T ],
                                "read",
                                []
                              |),
                              [ M.read (| tail |) ]
                            |)
                          ]
                        |)
                      |) in
                    let~ gap_guard :=
                      M.alloc (|
                        Value.StructRecord
                          "core::slice::sort::shared::smallsort::CopyOnDrop"
                          [
                            ("src",
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply
                                    (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                    []
                                    [ T ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ tmp ]
                              |));
                            ("dst", M.read (| tail |));
                            ("len", Value.Integer IntegerKind.Usize 1)
                          ]
                      |) in
                    M.loop (|
                      ltac:(M.monadic
                        (let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                              [
                                (* MutToConstPointer *) M.pointer_coercion (M.read (| sift |));
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    gap_guard,
                                    "core::slice::sort::shared::smallsort::CopyOnDrop",
                                    "dst"
                                  |)
                                |);
                                Value.Integer IntegerKind.Usize 1
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              gap_guard,
                              "core::slice::sort::shared::smallsort::CopyOnDrop",
                              "dst"
                            |),
                            M.read (| sift |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.eq (| M.read (| sift |), M.read (| begin |) |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.write (|
                            sift,
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*mut") [] [ T ],
                                "sub",
                                []
                              |),
                              [ M.read (| sift |); Value.Integer IntegerKind.Usize 1 ]
                            |)
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply (Ty.path "&") [] [ T ];
                                                  Ty.apply (Ty.path "&") [] [ T ]
                                                ]
                                            ],
                                            "call_mut",
                                            []
                                          |),
                                          [
                                            M.read (| is_less |);
                                            Value.Tuple
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::deref::Deref",
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::manually_drop::ManuallyDrop")
                                                      []
                                                      [ T ],
                                                    [],
                                                    "deref",
                                                    []
                                                  |),
                                                  [ tmp ]
                                                |);
                                                M.read (| sift |)
                                              ]
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_insert_tail :
          M.IsFunction "core::slice::sort::shared::smallsort::insert_tail" insert_tail.
        
        (*
        pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
            v: &mut [T],
            offset: usize,
            is_less: &mut F,
        ) {
            let len = v.len();
            if offset == 0 || offset > len {
                intrinsics::abort();
            }
        
            // SAFETY: see individual comments.
            unsafe {
                // We write this basic loop directly using pointers, as when we use a
                // for loop LLVM likes to unroll this loop which we do not want.
                // SAFETY: v_end is the one-past-end pointer, and we checked that
                // offset <= len, thus tail is also in-bounds.
                let v_base = v.as_mut_ptr();
                let v_end = v_base.add(len);
                let mut tail = v_base.add(offset);
                while tail != v_end {
                    // SAFETY: v_base and tail are both valid pointers to elements, and
                    // v_base < tail since we checked offset != 0.
                    insert_tail(v_base, tail, is_less);
        
                    // SAFETY: we checked that tail is not yet the one-past-end pointer.
                    tail = tail.add(1);
                }
            }
        }
        *)
        Definition insertion_sort_shift_left
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; offset; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let offset := M.alloc (| offset |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                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 (|
                                LogicalOp.or (|
                                  BinOp.eq (|
                                    M.read (| offset |),
                                    Value.Integer IntegerKind.Usize 0
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.gt (| M.read (| offset |), M.read (| len |) |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::abort", [] |),
                                []
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ v_base :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_mut_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ v_end :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "add", [] |),
                      [ M.read (| v_base |); M.read (| len |) ]
                    |)
                  |) in
                let~ tail :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "add", [] |),
                      [ M.read (| v_base |); M.read (| offset |) ]
                    |)
                  |) in
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (| M.read (| tail |), M.read (| v_end |) |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::slice::sort::shared::smallsort::insert_tail",
                                    [ T; F ]
                                  |),
                                  [ M.read (| v_base |); M.read (| tail |); M.read (| is_less |) ]
                                |)
                              |) in
                            let~ _ :=
                              M.write (|
                                tail,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                    "add",
                                    []
                                  |),
                                  [ M.read (| tail |); Value.Integer IntegerKind.Usize 1 ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_insertion_sort_shift_left :
          M.IsFunction
            "core::slice::sort::shared::smallsort::insertion_sort_shift_left"
            insertion_sort_shift_left.
        
        (*
        pub unsafe fn sort4_stable<T, F: FnMut(&T, &T) -> bool>(
            v_base: *const T,
            dst: *mut T,
            is_less: &mut F,
        ) {
            // By limiting select to picking pointers, we are guaranteed good cmov code-gen
            // regardless of type T's size. Further this only does 5 instead of 6
            // comparisons compared to a stable transposition 4 element sorting-network,
            // and always copies each element exactly once.
        
            // SAFETY: all pointers have offset at most 3 from v_base and dst, and are
            // thus in-bounds by the precondition.
            unsafe {
                // Stably create two pairs a <= b and c <= d.
                let c1 = is_less(&*v_base.add(1), &*v_base);
                let c2 = is_less(&*v_base.add(3), &*v_base.add(2));
                let a = v_base.add(c1 as usize);
                let b = v_base.add(!c1 as usize);
                let c = v_base.add(2 + c2 as usize);
                let d = v_base.add(2 + (!c2 as usize));
        
                // Compare (a, c) and (b, d) to identify max/min. We're left with two
                // unknown elements, but because we are a stable sort we must know which
                // one is leftmost and which one is rightmost.
                // c3, c4 | min max unknown_left unknown_right
                //  0,  0 |  a   d    b         c
                //  0,  1 |  a   b    c         d
                //  1,  0 |  c   d    a         b
                //  1,  1 |  c   b    a         d
                let c3 = is_less(&*c, &*a);
                let c4 = is_less(&*d, &*b);
                let min = select(c3, c, a);
                let max = select(c4, b, d);
                let unknown_left = select(c3, a, select(c4, c, b));
                let unknown_right = select(c4, d, select(c3, b, c));
        
                // Sort the last two unknown elements.
                let c5 = is_less(&*unknown_right, &*unknown_left);
                let lo = select(c5, unknown_right, unknown_left);
                let hi = select(c5, unknown_left, unknown_right);
        
                ptr::copy_nonoverlapping(min, dst, 1);
                ptr::copy_nonoverlapping(lo, dst.add(1), 1);
                ptr::copy_nonoverlapping(hi, dst.add(2), 1);
                ptr::copy_nonoverlapping(max, dst.add(3), 1);
            }
        
            #[inline(always)]
            fn select<T>(cond: bool, if_true: *const T, if_false: *const T) -> *const T {
                if cond { if_true } else { if_false }
            }
        }
        *)
        Definition sort4_stable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v_base; dst; is_less ] =>
            ltac:(M.monadic
              (let v_base := M.alloc (| v_base |) in
              let dst := M.alloc (| dst |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  let~ c1 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnMut",
                          F,
                          [
                            Ty.tuple
                              [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                          ],
                          "call_mut",
                          []
                        |),
                        [
                          M.read (| is_less |);
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); Value.Integer IntegerKind.Usize 1 ]
                              |);
                              M.read (| v_base |)
                            ]
                        ]
                      |)
                    |) in
                  let~ c2 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnMut",
                          F,
                          [
                            Ty.tuple
                              [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                          ],
                          "call_mut",
                          []
                        |),
                        [
                          M.read (| is_less |);
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); Value.Integer IntegerKind.Usize 3 ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); Value.Integer IntegerKind.Usize 2 ]
                              |)
                            ]
                        ]
                      |)
                    |) in
                  let~ a :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [ M.read (| v_base |); M.rust_cast (M.read (| c1 |)) ]
                      |)
                    |) in
                  let~ b :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [ M.read (| v_base |); M.rust_cast (UnOp.not (| M.read (| c1 |) |)) ]
                      |)
                    |) in
                  let~ c :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [
                          M.read (| v_base |);
                          BinOp.Wrap.add (|
                            Value.Integer IntegerKind.Usize 2,
                            M.rust_cast (M.read (| c2 |))
                          |)
                        ]
                      |)
                    |) in
                  let~ d :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [
                          M.read (| v_base |);
                          BinOp.Wrap.add (|
                            Value.Integer IntegerKind.Usize 2,
                            M.rust_cast (UnOp.not (| M.read (| c2 |) |))
                          |)
                        ]
                      |)
                    |) in
                  let~ c3 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnMut",
                          F,
                          [
                            Ty.tuple
                              [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                          ],
                          "call_mut",
                          []
                        |),
                        [ M.read (| is_less |); Value.Tuple [ M.read (| c |); M.read (| a |) ] ]
                      |)
                    |) in
                  let~ c4 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnMut",
                          F,
                          [
                            Ty.tuple
                              [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                          ],
                          "call_mut",
                          []
                        |),
                        [ M.read (| is_less |); Value.Tuple [ M.read (| d |); M.read (| b |) ] ]
                      |)
                    |) in
                  let~ min :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [ M.read (| c3 |); M.read (| c |); M.read (| a |) ]
                      |)
                    |) in
                  let~ max :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [ M.read (| c4 |); M.read (| b |); M.read (| d |) ]
                      |)
                    |) in
                  let~ unknown_left :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [
                          M.read (| c3 |);
                          M.read (| a |);
                          M.call_closure (|
                            M.get_function (|
                              "core::slice::sort::shared::smallsort::sort4_stable.select",
                              []
                            |),
                            [ M.read (| c4 |); M.read (| c |); M.read (| b |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ unknown_right :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [
                          M.read (| c4 |);
                          M.read (| d |);
                          M.call_closure (|
                            M.get_function (|
                              "core::slice::sort::shared::smallsort::sort4_stable.select",
                              []
                            |),
                            [ M.read (| c3 |); M.read (| b |); M.read (| c |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ c5 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnMut",
                          F,
                          [
                            Ty.tuple
                              [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                          ],
                          "call_mut",
                          []
                        |),
                        [
                          M.read (| is_less |);
                          Value.Tuple [ M.read (| unknown_right |); M.read (| unknown_left |) ]
                        ]
                      |)
                    |) in
                  let~ lo :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [ M.read (| c5 |); M.read (| unknown_right |); M.read (| unknown_left |) ]
                      |)
                    |) in
                  let~ hi :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable.select",
                          []
                        |),
                        [ M.read (| c5 |); M.read (| unknown_left |); M.read (| unknown_right |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [ M.read (| min |); M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [
                          M.read (| lo |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                          |);
                          Value.Integer IntegerKind.Usize 1
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [
                          M.read (| hi |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| dst |); Value.Integer IntegerKind.Usize 2 ]
                          |);
                          Value.Integer IntegerKind.Usize 1
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [
                          M.read (| max |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| dst |); Value.Integer IntegerKind.Usize 3 ]
                          |);
                          Value.Integer IntegerKind.Usize 1
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_sort4_stable :
          M.IsFunction "core::slice::sort::shared::smallsort::sort4_stable" sort4_stable.
        
        Module sort4_stable.
          (*
              fn select<T>(cond: bool, if_true: *const T, if_false: *const T) -> *const T {
                  if cond { if_true } else { if_false }
              }
          *)
          Definition select (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            match ε, τ, α with
            | [], [ T ], [ cond; if_true; if_false ] =>
              ltac:(M.monadic
                (let cond := M.alloc (| cond |) in
                let if_true := M.alloc (| if_true |) in
                let if_false := M.alloc (| if_false |) in
                M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use cond in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          if_true));
                      fun γ => ltac:(M.monadic if_false)
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Function_select :
            M.IsFunction "core::slice::sort::shared::smallsort::sort4_stable::select" select.
        End sort4_stable.
        
        (*
        unsafe fn sort8_stable<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(
            v_base: *mut T,
            dst: *mut T,
            scratch_base: *mut T,
            is_less: &mut F,
        ) {
            // SAFETY: these pointers are all in-bounds by the precondition of our function.
            unsafe {
                sort4_stable(v_base, scratch_base, is_less);
                sort4_stable(v_base.add(4), scratch_base.add(4), is_less);
            }
        
            // SAFETY: scratch_base[0..8] is now initialized, allowing us to merge back
            // into dst.
            unsafe {
                bidirectional_merge(&*ptr::slice_from_raw_parts(scratch_base, 8), dst, is_less);
            }
        }
        *)
        Definition sort8_stable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v_base; dst; scratch_base; is_less ] =>
            ltac:(M.monadic
              (let v_base := M.alloc (| v_base |) in
              let dst := M.alloc (| dst |) in
              let scratch_base := M.alloc (| scratch_base |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable",
                          [ T; F ]
                        |),
                        [
                          (* MutToConstPointer *) M.pointer_coercion (M.read (| v_base |));
                          M.read (| scratch_base |);
                          M.read (| is_less |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::smallsort::sort4_stable",
                          [ T; F ]
                        |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*mut") [] [ T ],
                                "add",
                                []
                              |),
                              [ M.read (| v_base |); Value.Integer IntegerKind.Usize 4 ]
                            |));
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| scratch_base |); Value.Integer IntegerKind.Usize 4 ]
                          |);
                          M.read (| is_less |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::slice::sort::shared::smallsort::bidirectional_merge",
                        [ T; F ]
                      |),
                      [
                        M.call_closure (|
                          M.get_function (| "core::ptr::slice_from_raw_parts", [ T ] |),
                          [
                            (* MutToConstPointer *) M.pointer_coercion (M.read (| scratch_base |));
                            Value.Integer IntegerKind.Usize 8
                          ]
                        |);
                        M.read (| dst |);
                        M.read (| is_less |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_sort8_stable :
          M.IsFunction "core::slice::sort::shared::smallsort::sort8_stable" sort8_stable.
        
        (*
        unsafe fn merge_up<T, F: FnMut(&T, &T) -> bool>(
            mut left_src: *const T,
            mut right_src: *const T,
            mut dst: *mut T,
            is_less: &mut F,
        ) -> ( *const T, *const T, *mut T) {
            // This is a branchless merge utility function.
            // The equivalent code with a branch would be:
            //
            // if !is_less(&*right_src, &*left_src) {
            //     ptr::copy_nonoverlapping(left_src, dst, 1);
            //     left_src = left_src.add(1);
            // } else {
            //     ptr::copy_nonoverlapping(right_src, dst, 1);
            //     right_src = right_src.add(1);
            // }
            // dst = dst.add(1);
        
            // SAFETY: The caller must guarantee that `left_src`, `right_src` are valid
            // to read and `dst` is valid to write, while not aliasing.
            unsafe {
                let is_l = !is_less(&*right_src, &*left_src);
                let src = if is_l { left_src } else { right_src };
                ptr::copy_nonoverlapping(src, dst, 1);
                right_src = right_src.add(!is_l as usize);
                left_src = left_src.add(is_l as usize);
                dst = dst.add(1);
            }
        
            (left_src, right_src, dst)
        }
        *)
        Definition merge_up (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ left_src; right_src; dst; is_less ] =>
            ltac:(M.monadic
              (let left_src := M.alloc (| left_src |) in
              let right_src := M.alloc (| right_src |) in
              let dst := M.alloc (| dst |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  let~ is_l :=
                    M.alloc (|
                      UnOp.not (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::function::FnMut",
                            F,
                            [
                              Ty.tuple
                                [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                            ],
                            "call_mut",
                            []
                          |),
                          [
                            M.read (| is_less |);
                            Value.Tuple [ M.read (| right_src |); M.read (| left_src |) ]
                          ]
                        |)
                      |)
                    |) in
                  let~ src :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use is_l in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              left_src));
                          fun γ => ltac:(M.monadic right_src)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [ M.read (| src |); M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      right_src,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [ M.read (| right_src |); M.rust_cast (UnOp.not (| M.read (| is_l |) |)) ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      left_src,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "add",
                          []
                        |),
                        [ M.read (| left_src |); M.rust_cast (M.read (| is_l |)) ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      dst,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ T ],
                          "add",
                          []
                        |),
                        [ M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (|
                  Value.Tuple [ M.read (| left_src |); M.read (| right_src |); M.read (| dst |) ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_merge_up :
          M.IsFunction "core::slice::sort::shared::smallsort::merge_up" merge_up.
        
        (*
        unsafe fn merge_down<T, F: FnMut(&T, &T) -> bool>(
            mut left_src: *const T,
            mut right_src: *const T,
            mut dst: *mut T,
            is_less: &mut F,
        ) -> ( *const T, *const T, *mut T) {
            // This is a branchless merge utility function.
            // The equivalent code with a branch would be:
            //
            // if !is_less(&*right_src, &*left_src) {
            //     ptr::copy_nonoverlapping(right_src, dst, 1);
            //     right_src = right_src.wrapping_sub(1);
            // } else {
            //     ptr::copy_nonoverlapping(left_src, dst, 1);
            //     left_src = left_src.wrapping_sub(1);
            // }
            // dst = dst.sub(1);
        
            // SAFETY: The caller must guarantee that `left_src`, `right_src` are valid
            // to read and `dst` is valid to write, while not aliasing.
            unsafe {
                let is_l = !is_less(&*right_src, &*left_src);
                let src = if is_l { right_src } else { left_src };
                ptr::copy_nonoverlapping(src, dst, 1);
                right_src = right_src.wrapping_sub(is_l as usize);
                left_src = left_src.wrapping_sub(!is_l as usize);
                dst = dst.sub(1);
            }
        
            (left_src, right_src, dst)
        }
        *)
        Definition merge_down (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ left_src; right_src; dst; is_less ] =>
            ltac:(M.monadic
              (let left_src := M.alloc (| left_src |) in
              let right_src := M.alloc (| right_src |) in
              let dst := M.alloc (| dst |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  let~ is_l :=
                    M.alloc (|
                      UnOp.not (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::function::FnMut",
                            F,
                            [
                              Ty.tuple
                                [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                            ],
                            "call_mut",
                            []
                          |),
                          [
                            M.read (| is_less |);
                            Value.Tuple [ M.read (| right_src |); M.read (| left_src |) ]
                          ]
                        |)
                      |)
                    |) in
                  let~ src :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use is_l in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              right_src));
                          fun γ => ltac:(M.monadic left_src)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [ M.read (| src |); M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      right_src,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "wrapping_sub",
                          []
                        |),
                        [ M.read (| right_src |); M.rust_cast (M.read (| is_l |)) ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      left_src,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ T ],
                          "wrapping_sub",
                          []
                        |),
                        [ M.read (| left_src |); M.rust_cast (UnOp.not (| M.read (| is_l |) |)) ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      dst,
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ T ],
                          "sub",
                          []
                        |),
                        [ M.read (| dst |); Value.Integer IntegerKind.Usize 1 ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (|
                  Value.Tuple [ M.read (| left_src |); M.read (| right_src |); M.read (| dst |) ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_merge_down :
          M.IsFunction "core::slice::sort::shared::smallsort::merge_down" merge_down.
        
        (*
        unsafe fn bidirectional_merge<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(
            v: &[T],
            dst: *mut T,
            is_less: &mut F,
        ) {
            // It helps to visualize the merge:
            //
            // Initial:
            //
            //  |dst (in dst)
            //  |left               |right
            //  v                   v
            // [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx]
            //                     ^                   ^
            //                     |left_rev           |right_rev
            //                                         |dst_rev (in dst)
            //
            // After:
            //
            //                      |dst (in dst)
            //        |left         |           |right
            //        v             v           v
            // [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx]
            //       ^             ^           ^
            //       |left_rev     |           |right_rev
            //                     |dst_rev (in dst)
            //
            // In each iteration one of left or right moves up one position, and one of
            // left_rev or right_rev moves down one position, whereas dst always moves
            // up one position and dst_rev always moves down one position. Assuming
            // the input was sorted and the comparison function is correctly implemented
            // at the end we will have left == left_rev + 1, and right == right_rev + 1,
            // fully consuming the input having written it to dst.
        
            let len = v.len();
            let src = v.as_ptr();
        
            let len_div_2 = len / 2;
        
            // SAFETY: The caller has to ensure that len >= 2.
            unsafe {
                intrinsics::assume(len_div_2 != 0); // This can avoid useless code-gen.
            }
        
            // SAFETY: no matter what the result of the user-provided comparison function
            // is, all 4 read pointers will always be in-bounds. Writing `dst` and `dst_rev`
            // will always be in bounds if the caller guarantees that `dst` is valid for
            // `v.len()` writes.
            unsafe {
                let mut left = src;
                let mut right = src.add(len_div_2);
                let mut dst = dst;
        
                let mut left_rev = src.add(len_div_2 - 1);
                let mut right_rev = src.add(len - 1);
                let mut dst_rev = dst.add(len - 1);
        
                for _ in 0..len_div_2 {
                    (left, right, dst) = merge_up(left, right, dst, is_less);
                    (left_rev, right_rev, dst_rev) = merge_down(left_rev, right_rev, dst_rev, is_less);
                }
        
                let left_end = left_rev.wrapping_add(1);
                let right_end = right_rev.wrapping_add(1);
        
                // Odd length, so one element is left unconsumed in the input.
                if len % 2 != 0 {
                    let left_nonempty = left < left_end;
                    let last_src = if left_nonempty { left } else { right };
                    ptr::copy_nonoverlapping(last_src, dst, 1);
                    left = left.add(left_nonempty as usize);
                    right = right.add((!left_nonempty) as usize);
                }
        
                // We now should have consumed the full input exactly once. This can only fail if the
                // user-provided comparison function fails to implement a strict weak ordering. In that case
                // we panic and never access the inconsistent state in dst.
                if left != left_end || right != right_end {
                    panic_on_ord_violation();
                }
            }
        }
        *)
        Definition bidirectional_merge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; dst; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let dst := M.alloc (| dst |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ src :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ len_div_2 :=
                  M.alloc (|
                    BinOp.Wrap.div (| M.read (| len |), Value.Integer IntegerKind.Usize 2 |)
                  |) in
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::assume", [] |),
                        [ BinOp.ne (| M.read (| len_div_2 |), Value.Integer IntegerKind.Usize 0 |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                let~ left := M.copy (| src |) in
                let~ right :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "add",
                        []
                      |),
                      [ M.read (| src |); M.read (| len_div_2 |) ]
                    |)
                  |) in
                let~ dst := M.copy (| dst |) in
                let~ left_rev :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "add",
                        []
                      |),
                      [
                        M.read (| src |);
                        BinOp.Wrap.sub (|
                          M.read (| len_div_2 |),
                          Value.Integer IntegerKind.Usize 1
                        |)
                      ]
                    |)
                  |) in
                let~ right_rev :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "add",
                        []
                      |),
                      [
                        M.read (| src |);
                        BinOp.Wrap.sub (| M.read (| len |), Value.Integer IntegerKind.Usize 1 |)
                      ]
                    |)
                  |) in
                let~ dst_rev :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "add", [] |),
                      [
                        M.read (| dst |);
                        BinOp.Wrap.sub (| M.read (| len |), Value.Integer IntegerKind.Usize 1 |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            Value.StructRecord
                              "core::ops::range::Range"
                              [
                                ("start", Value.Integer IntegerKind.Usize 0);
                                ("end_", M.read (| len_div_2 |))
                              ]
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::ops::range::Range")
                                            []
                                            [ Ty.path "usize" ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::slice::sort::shared::smallsort::merge_up",
                                                    [ T; F ]
                                                  |),
                                                  [
                                                    M.read (| left |);
                                                    M.read (| right |);
                                                    M.read (| dst |);
                                                    M.read (| is_less |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                    let γ0_1 :=
                                                      M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                    let γ0_2 :=
                                                      M.SubPointer.get_tuple_field (| γ, 2 |) in
                                                    let lhs := M.copy (| γ0_0 |) in
                                                    let lhs := M.copy (| γ0_1 |) in
                                                    let lhs := M.copy (| γ0_2 |) in
                                                    let~ _ :=
                                                      M.write (| left, M.read (| lhs |) |) in
                                                    let~ _ :=
                                                      M.write (| right, M.read (| lhs |) |) in
                                                    let~ _ := M.write (| dst, M.read (| lhs |) |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::slice::sort::shared::smallsort::merge_down",
                                                    [ T; F ]
                                                  |),
                                                  [
                                                    M.read (| left_rev |);
                                                    M.read (| right_rev |);
                                                    M.read (| dst_rev |);
                                                    M.read (| is_less |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                    let γ0_1 :=
                                                      M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                    let γ0_2 :=
                                                      M.SubPointer.get_tuple_field (| γ, 2 |) in
                                                    let lhs := M.copy (| γ0_0 |) in
                                                    let lhs := M.copy (| γ0_1 |) in
                                                    let lhs := M.copy (| γ0_2 |) in
                                                    let~ _ :=
                                                      M.write (| left_rev, M.read (| lhs |) |) in
                                                    let~ _ :=
                                                      M.write (| right_rev, M.read (| lhs |) |) in
                                                    let~ _ :=
                                                      M.write (| dst_rev, M.read (| lhs |) |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ left_end :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "wrapping_add",
                        []
                      |),
                      [ M.read (| left_rev |); Value.Integer IntegerKind.Usize 1 ]
                    |)
                  |) in
                let~ right_end :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "wrapping_add",
                        []
                      |),
                      [ M.read (| right_rev |); Value.Integer IntegerKind.Usize 1 ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ne (|
                                  BinOp.Wrap.rem (|
                                    M.read (| len |),
                                    Value.Integer IntegerKind.Usize 2
                                  |),
                                  Value.Integer IntegerKind.Usize 0
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ left_nonempty :=
                            M.alloc (| BinOp.lt (| M.read (| left |), M.read (| left_end |) |) |) in
                          let~ last_src :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.use left_nonempty in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      left));
                                  fun γ => ltac:(M.monadic right)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                                [
                                  M.read (| last_src |);
                                  M.read (| dst |);
                                  Value.Integer IntegerKind.Usize 1
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              left,
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| left |); M.rust_cast (M.read (| left_nonempty |)) ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              right,
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "add",
                                  []
                                |),
                                [
                                  M.read (| right |);
                                  M.rust_cast (UnOp.not (| M.read (| left_nonempty |) |))
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.or (|
                                BinOp.ne (| M.read (| left |), M.read (| left_end |) |),
                                ltac:(M.monadic
                                  (BinOp.ne (| M.read (| right |), M.read (| right_end |) |)))
                              |)
                            |)) 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::slice::sort::shared::smallsort::panic_on_ord_violation",
                                []
                              |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_bidirectional_merge :
          M.IsFunction
            "core::slice::sort::shared::smallsort::bidirectional_merge"
            bidirectional_merge.
        
        (*
        fn panic_on_ord_violation() -> ! {
            // This is indicative of a logic bug in the user-provided comparison function or Ord
            // implementation. They are expected to implement a total order as explained in the Ord
            // documentation.
            //
            // By panicking we inform the user, that they have a logic bug in their program. If a strict
            // weak ordering is not given, the concept of comparison based sorting cannot yield a sorted
            // result. E.g.: a < b < c < a
            //
            // The Ord documentation requires users to implement a total order. Arguably that's
            // unnecessarily strict in the context of sorting. Issues only arise if the weaker requirement
            // of a strict weak ordering is violated.
            //
            // The panic message talks about a total order because that's what the Ord documentation talks
            // about and requires, so as to not confuse users.
            panic!("user-provided comparison function does not correctly implement a total order");
        }
        *)
        Definition panic_on_ord_violation
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_function (| "core::panicking::panic_fmt", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (|
                              Value.String
                                "user-provided comparison function does not correctly implement a total order"
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_panic_on_ord_violation :
          M.IsFunction
            "core::slice::sort::shared::smallsort::panic_on_ord_violation"
            panic_on_ord_violation.
        
        (*
        pub(crate) const fn has_efficient_in_place_swap<T>() -> bool {
            // Heuristic that holds true on all tested 64-bit capable architectures.
            mem::size_of::<T>() <= 8 // mem::size_of::<u64>()
        }
        *)
        Definition has_efficient_in_place_swap
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T ], [] =>
            ltac:(M.monadic
              (BinOp.le (|
                M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |),
                Value.Integer IntegerKind.Usize 8
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_has_efficient_in_place_swap :
          M.IsFunction
            "core::slice::sort::shared::smallsort::has_efficient_in_place_swap"
            has_efficient_in_place_swap.
      End smallsort.
    End shared.
  End sort.
End slice.
