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

Module slice.
  Module sort.
    Module unstable.
      Module quicksort.
        (*
        pub(crate) fn quicksort<'a, T, F>(
            mut v: &'a mut [T],
            mut ancestor_pivot: Option<&'a T>,
            mut limit: u32,
            is_less: &mut F,
        ) where
            F: FnMut(&T, &T) -> bool,
        {
            loop {
                if v.len() <= T::small_sort_threshold() {
                    T::small_sort(v, is_less);
                    return;
                }
        
                // If too many bad pivot choices were made, simply fall back to heapsort in order to
                // guarantee `O(N x log(N))` worst-case.
                if limit == 0 {
                    heapsort::heapsort(v, is_less);
                    return;
                }
        
                limit -= 1;
        
                // Choose a pivot and try guessing whether the slice is already sorted.
                let pivot_pos = choose_pivot(v, is_less);
        
                // If the chosen pivot is equal to the predecessor, then it's the smallest element in the
                // slice. Partition the slice into elements equal to and elements greater than the pivot.
                // This case is usually hit when the slice contains many duplicate elements.
                if let Some(p) = ancestor_pivot {
                    // SAFETY: We assume choose_pivot yields an in-bounds position.
                    if !is_less(p, unsafe { v.get_unchecked(pivot_pos) }) {
                        let num_lt = partition(v, pivot_pos, &mut |a, b| !is_less(b, a));
        
                        // Continue sorting elements greater than the pivot. We know that `num_lt` contains
                        // the pivot. So we can continue after `num_lt`.
                        v = &mut v[(num_lt + 1)..];
                        ancestor_pivot = None;
                        continue;
                    }
                }
        
                // Partition the slice.
                let num_lt = partition(v, pivot_pos, is_less);
                // SAFETY: partition ensures that `num_lt` will be in-bounds.
                unsafe { intrinsics::assume(num_lt < v.len()) };
        
                // Split the slice into `left`, `pivot`, and `right`.
                let (left, right) = v.split_at_mut(num_lt);
                let (pivot, right) = right.split_at_mut(1);
                let pivot = &pivot[0];
        
                // Recurse into the left side. We have a fixed recursion limit, testing shows no real
                // benefit for recursing into the shorter side.
                quicksort(left, ancestor_pivot, limit, is_less);
        
                // Continue with the right side.
                v = right;
                ancestor_pivot = Some(pivot);
            }
        }
        *)
        Definition quicksort (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; ancestor_pivot; limit; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let ancestor_pivot := M.alloc (| ancestor_pivot |) in
              let limit := M.alloc (| limit |) in
              let is_less := M.alloc (| is_less |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.le (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "len",
                                                []
                                              |),
                                              [ M.read (| v |) ]
                                            |),
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::slice::sort::shared::smallsort::UnstableSmallSortTypeImpl",
                                                T,
                                                [],
                                                "small_sort_threshold",
                                                []
                                              |),
                                              []
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::slice::sort::shared::smallsort::UnstableSmallSortTypeImpl",
                                                  T,
                                                  [],
                                                  "small_sort",
                                                  [ F ]
                                                |),
                                                [ M.read (| v |); M.read (| is_less |) ]
                                              |)
                                            |) in
                                          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.eq (|
                                            M.read (| limit |),
                                            Value.Integer IntegerKind.U32 0
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::slice::sort::unstable::heapsort::heapsort",
                                                  [ T; F ]
                                                |),
                                                [ M.read (| v |); M.read (| is_less |) ]
                                              |)
                                            |) in
                                          M.return_ (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            let β := limit in
                            M.write (|
                              β,
                              BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.U32 1 |)
                            |) in
                          let~ pivot_pos :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::choose_pivot",
                                  [ T; F ]
                                |),
                                [ M.read (| v |); M.read (| is_less |) ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := ancestor_pivot in
                                    let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let p := M.copy (| γ0_0 |) 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.read (| p |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                                "get_unchecked",
                                                                [ Ty.path "usize" ]
                                                              |),
                                                              [
                                                                M.read (| v |);
                                                                M.read (| pivot_pos |)
                                                              ]
                                                            |)
                                                          ]
                                                      ]
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ num_lt :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::slice::sort::unstable::quicksort::partition",
                                                          [
                                                            T;
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.apply (Ty.path "&") [] [ T ];
                                                                    Ty.apply (Ty.path "&") [] [ T ]
                                                                  ]
                                                              ]
                                                              (Ty.path "bool")
                                                          ]
                                                        |),
                                                        [
                                                          M.read (| v |);
                                                          M.read (| pivot_pos |);
                                                          M.alloc (|
                                                            M.closure
                                                              (fun γ =>
                                                                ltac:(M.monadic
                                                                  match γ with
                                                                  | [ α0; α1 ] =>
                                                                    ltac:(M.monadic
                                                                      (M.match_operator (|
                                                                        M.alloc (| α0 |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let a :=
                                                                                M.copy (| γ |) in
                                                                              M.match_operator (|
                                                                                M.alloc (| α1 |),
                                                                                [
                                                                                  fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      (let b :=
                                                                                        M.copy (|
                                                                                          γ
                                                                                        |) in
                                                                                      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 (|
                                                                                                  b
                                                                                                |);
                                                                                                M.read (|
                                                                                                  a
                                                                                                |)
                                                                                              ]
                                                                                          ]
                                                                                        |)
                                                                                      |)))
                                                                                ]
                                                                              |)))
                                                                        ]
                                                                      |)))
                                                                  | _ =>
                                                                    M.impossible
                                                                      "wrong number of arguments"
                                                                  end))
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      v,
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::index::IndexMut",
                                                          Ty.apply (Ty.path "slice") [] [ T ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::ops::range::RangeFrom")
                                                              []
                                                              [ Ty.path "usize" ]
                                                          ],
                                                          "index_mut",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| v |);
                                                          Value.StructRecord
                                                            "core::ops::range::RangeFrom"
                                                            [
                                                              ("start",
                                                                BinOp.Wrap.add (|
                                                                  M.read (| num_lt |),
                                                                  Value.Integer IntegerKind.Usize 1
                                                                |))
                                                            ]
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      ancestor_pivot,
                                                      Value.StructTuple
                                                        "core::option::Option::None"
                                                        []
                                                    |) in
                                                  M.continue (||)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ num_lt :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::unstable::quicksort::partition",
                                  [ T; F ]
                                |),
                                [ M.read (| v |); M.read (| pivot_pos |); M.read (| is_less |) ]
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::assume", [] |),
                                [
                                  BinOp.lt (|
                                    M.read (| num_lt |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ T ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| v |) ]
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ T ],
                                  "split_at_mut",
                                  []
                                |),
                                [ M.read (| v |); M.read (| num_lt |) ]
                              |)
                            |),
                            [
                              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 left := M.copy (| γ0_0 |) in
                                  let right := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ T ],
                                          "split_at_mut",
                                          []
                                        |),
                                        [ M.read (| right |); Value.Integer IntegerKind.Usize 1 ]
                                      |)
                                    |),
                                    [
                                      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 pivot := M.copy (| γ0_0 |) in
                                          let right := M.copy (| γ0_1 |) in
                                          let~ pivot :=
                                            M.alloc (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| pivot |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::slice::sort::unstable::quicksort::quicksort",
                                                  [ T; F ]
                                                |),
                                                [
                                                  M.read (| left |);
                                                  M.read (| ancestor_pivot |);
                                                  M.read (| limit |);
                                                  M.read (| is_less |)
                                                ]
                                              |)
                                            |) in
                                          let~ _ := M.write (| v, M.read (| right |) |) in
                                          let~ _ :=
                                            M.write (|
                                              ancestor_pivot,
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ M.read (| pivot |) ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |)))
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_quicksort :
          M.IsFunction "core::slice::sort::unstable::quicksort::quicksort" quicksort.
        
        (*
        pub(crate) fn partition<T, F>(v: &mut [T], pivot: usize, is_less: &mut F) -> usize
        where
            F: FnMut(&T, &T) -> bool,
        {
            let len = v.len();
        
            // Allows for panic-free code-gen by proving this property to the compiler.
            if len == 0 {
                return 0;
            }
        
            if pivot >= len {
                intrinsics::abort();
            }
        
            // SAFETY: We checked that `pivot` is in-bounds.
            unsafe {
                // Place the pivot at the beginning of slice.
                v.swap_unchecked(0, pivot);
            }
            let (pivot, v_without_pivot) = v.split_at_mut(1);
        
            // Assuming that Rust generates noalias LLVM IR we can be sure that a partition function
            // signature of the form `(v: &mut [T], pivot: &T)` guarantees that pivot and v can't alias.
            // Having this guarantee is crucial for optimizations. It's possible to copy the pivot value
            // into a stack value, but this creates issues for types with interior mutability mandating
            // a drop guard.
            let pivot = &mut pivot[0];
        
            // This construct is used to limit the LLVM IR generated, which saves large amounts of
            // compile-time by only instantiating the code that is needed. Idea by Frank Steffahn.
            let num_lt = (const { inst_partition::<T, F>() })(v_without_pivot, pivot, is_less);
        
            if num_lt >= len {
                intrinsics::abort();
            }
        
            // SAFETY: We checked that `num_lt` is in-bounds.
            unsafe {
                // Place the pivot between the two partitions.
                v.swap_unchecked(0, num_lt);
            }
        
            num_lt
        }
        *)
        Definition partition (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; pivot; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let pivot := M.alloc (| pivot |) 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.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) 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.Integer IntegerKind.Usize 0 |) |)
                                |)
                              |)));
                          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.ge (| M.read (| pivot |), 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~ _ :=
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ T ],
                              "swap_unchecked",
                              []
                            |),
                            [ M.read (| v |); Value.Integer IntegerKind.Usize 0; M.read (| pivot |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "split_at_mut",
                            []
                          |),
                          [ M.read (| v |); Value.Integer IntegerKind.Usize 1 ]
                        |)
                      |),
                      [
                        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 pivot := M.copy (| γ0_0 |) in
                            let v_without_pivot := M.copy (| γ0_1 |) in
                            let~ pivot :=
                              M.alloc (|
                                M.SubPointer.get_array_field (|
                                  M.read (| pivot |),
                                  M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                |)
                              |) in
                            let~ num_lt :=
                              M.alloc (|
                                M.call_closure (|
                                  M.read (|
                                    M.get_constant (|
                                      "core::slice::sort::unstable::quicksort::partition_discriminant"
                                    |)
                                  |),
                                  [
                                    M.read (| v_without_pivot |);
                                    M.read (| pivot |);
                                    M.read (| is_less |)
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.ge (| M.read (| num_lt |), 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~ _ :=
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "swap_unchecked",
                                      []
                                    |),
                                    [
                                      M.read (| v |);
                                      Value.Integer IntegerKind.Usize 0;
                                      M.read (| num_lt |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |) in
                            num_lt))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_partition :
          M.IsFunction "core::slice::sort::unstable::quicksort::partition" partition.
        
        (*
        const fn inst_partition<T, F: FnMut(&T, &T) -> bool>() -> fn(&mut [T], &T, &mut F) -> usize {
            const MAX_BRANCHLESS_PARTITION_SIZE: usize = 96;
            if mem::size_of::<T>() <= MAX_BRANCHLESS_PARTITION_SIZE {
                // Specialize for types that are relatively cheap to copy, where branchless optimizations
                // have large leverage e.g. `u64` and `String`.
                cfg_if! {
                    if #[cfg(feature = "optimize_for_size")] {
                        partition_lomuto_branchless_simple::<T, F>
                    } else {
                        partition_lomuto_branchless_cyclic::<T, F>
                    }
                }
            } else {
                partition_hoare_branchy_cyclic::<T, F>
            }
        }
        *)
        Definition inst_partition (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [] =>
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.le (|
                                M.call_closure (|
                                  M.get_function (| "core::mem::size_of", [ T ] |),
                                  []
                                |),
                                M.read (|
                                  M.get_constant (|
                                    "core::slice::sort::unstable::quicksort::inst_partition::MAX_BRANCHLESS_PARTITION_SIZE"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          (* ReifyFnPointer *)
                          M.pointer_coercion
                            (M.get_function (|
                              "core::slice::sort::unstable::quicksort::partition_lomuto_branchless_cyclic",
                              [ T; F ]
                            |))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          (* ReifyFnPointer *)
                          M.pointer_coercion
                            (M.get_function (|
                              "core::slice::sort::unstable::quicksort::partition_hoare_branchy_cyclic",
                              [ T; F ]
                            |))
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_inst_partition :
          M.IsFunction "core::slice::sort::unstable::quicksort::inst_partition" inst_partition.
        
        Module inst_partition.
          Definition value_MAX_BRANCHLESS_PARTITION_SIZE : Value.t :=
            M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 96 |))).
        End inst_partition.
        
        (*
        fn partition_hoare_branchy_cyclic<T, F>(v: &mut [T], pivot: &T, is_less: &mut F) -> usize
        where
            F: FnMut(&T, &T) -> bool,
        {
            let len = v.len();
        
            if len == 0 {
                return 0;
            }
        
            // Optimized for large types that are expensive to move. Not optimized for integers. Optimized
            // for small code-gen, assuming that is_less is an expensive operation that generates
            // substantial amounts of code or a call. And that copying elements will likely be a call to
            // memcpy. Using 2 `ptr::copy_nonoverlapping` has the chance to be faster than
            // `ptr::swap_nonoverlapping` because `memcpy` can use wide SIMD based on runtime feature
            // detection. Benchmarks support this analysis.
        
            let mut gap_opt: Option<GapGuard<T>> = None;
        
            // SAFETY: The left-to-right scanning loop performs a bounds check, where we know that `left >=
            // v_base && left < right && right <= v_base.add(len)`. The right-to-left scanning loop performs
            // a bounds check ensuring that `right` is in-bounds. We checked that `len` is more than zero,
            // which means that unconditional `right = right.sub(1)` is safe to do. The exit check makes
            // sure that `left` and `right` never alias, making `ptr::copy_nonoverlapping` safe. The
            // drop-guard `gap` ensures that should `is_less` panic we always overwrite the duplicate in the
            // input. `gap.pos` stores the previous value of `right` and starts at `right` and so it too is
            // in-bounds. We never pass the saved `gap.value` to `is_less` while it is inside the `GapGuard`
            // thus any changes via interior mutability will be observed.
            unsafe {
                let v_base = v.as_mut_ptr();
        
                let mut left = v_base;
                let mut right = v_base.add(len);
        
                loop {
                    // Find the first element greater than the pivot.
                    while left < right && is_less(&*left, pivot) {
                        left = left.add(1);
                    }
        
                    // Find the last element equal to the pivot.
                    loop {
                        right = right.sub(1);
                        if left >= right || is_less(&*right, pivot) {
                            break;
                        }
                    }
        
                    if left >= right {
                        break;
                    }
        
                    // Swap the found pair of out-of-order elements via cyclic permutation.
                    let is_first_swap_pair = gap_opt.is_none();
        
                    if is_first_swap_pair {
                        gap_opt = Some(GapGuard { pos: right, value: ManuallyDrop::new(ptr::read(left)) });
                    }
        
                    let gap = gap_opt.as_mut().unwrap_unchecked();
        
                    // Single place where we instantiate ptr::copy_nonoverlapping in the partition.
                    if !is_first_swap_pair {
                        ptr::copy_nonoverlapping(left, gap.pos, 1);
                    }
                    gap.pos = right;
                    ptr::copy_nonoverlapping(right, left, 1);
        
                    left = left.add(1);
                }
        
                left.sub_ptr(v_base)
        
                // `gap_opt` goes out of scope and overwrites the last wrong-side element on the right side
                // with the first wrong-side element of the left side that was initially overwritten by the
                // first wrong-side element on the right side element.
            }
        }
        *)
        Definition partition_hoare_branchy_cyclic
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; pivot; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let pivot := M.alloc (| pivot |) 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.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) 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.Integer IntegerKind.Usize 0 |) |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ gap_opt :=
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |) 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~ left := M.copy (| v_base |) in
                    let~ right :=
                      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~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.loop (|
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.and (|
                                                BinOp.lt (|
                                                  M.read (| left |),
                                                  M.read (| right |)
                                                |),
                                                ltac:(M.monadic
                                                  (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 (| left |); M.read (| pivot |) ]
                                                    ]
                                                  |)))
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            left,
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [ M.read (| left |); 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 [] |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)))
                            |) in
                          let~ _ :=
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.write (|
                                    right,
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*mut") [] [ T ],
                                        "sub",
                                        []
                                      |),
                                      [ M.read (| right |); Value.Integer IntegerKind.Usize 1 ]
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.or (|
                                                BinOp.ge (|
                                                  M.read (| left |),
                                                  M.read (| right |)
                                                |),
                                                ltac:(M.monadic
                                                  (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 |); M.read (| pivot |) ]
                                                    ]
                                                  |)))
                                              |)
                                            |)) 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.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (| M.read (| left |), M.read (| right |) |)
                                        |)) 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~ is_first_swap_pair :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::slice::sort::unstable::quicksort::GapGuard")
                                        []
                                        [ T ]
                                    ],
                                  "is_none",
                                  []
                                |),
                                [ gap_opt ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use is_first_swap_pair in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        gap_opt,
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [
                                            Value.StructRecord
                                              "core::slice::sort::unstable::quicksort::GapGuard"
                                              [
                                                ("pos", M.read (| right |));
                                                ("value",
                                                  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 (| left |))
                                                        ]
                                                      |)
                                                    ]
                                                  |))
                                              ]
                                          ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ gap :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "&mut")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path
                                              "core::slice::sort::unstable::quicksort::GapGuard")
                                            []
                                            [ T ]
                                        ]
                                    ],
                                  "unwrap_unchecked",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path
                                              "core::slice::sort::unstable::quicksort::GapGuard")
                                            []
                                            [ T ]
                                        ],
                                      "as_mut",
                                      []
                                    |),
                                    [ gap_opt ]
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (| M.read (| is_first_swap_pair |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::intrinsics::copy_nonoverlapping",
                                            [ T ]
                                          |),
                                          [
                                            (* MutToConstPointer *)
                                            M.pointer_coercion (M.read (| left |));
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| gap |),
                                                "core::slice::sort::unstable::quicksort::GapGuard",
                                                "pos"
                                              |)
                                            |);
                                            Value.Integer IntegerKind.Usize 1
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| gap |),
                                "core::slice::sort::unstable::quicksort::GapGuard",
                                "pos"
                              |),
                              M.read (| right |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                                [
                                  (* MutToConstPointer *) M.pointer_coercion (M.read (| right |));
                                  M.read (| left |);
                                  Value.Integer IntegerKind.Usize 1
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              left,
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| left |); Value.Integer IntegerKind.Usize 1 ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ T ],
                          "sub_ptr",
                          []
                        |),
                        [
                          M.read (| left |);
                          (* MutToConstPointer *) M.pointer_coercion (M.read (| v_base |))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_partition_hoare_branchy_cyclic :
          M.IsFunction
            "core::slice::sort::unstable::quicksort::partition_hoare_branchy_cyclic"
            partition_hoare_branchy_cyclic.
        
        (* StructRecord
          {
            name := "PartitionState";
            const_params := [];
            ty_params := [ "T" ];
            fields :=
              [
                ("right", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("num_lt", Ty.path "usize");
                ("gap",
                  Ty.apply (Ty.path "core::slice::sort::unstable::quicksort::GapGuardRaw") [] [ T ])
              ];
          } *)
        
        (*
        fn partition_lomuto_branchless_cyclic<T, F>(v: &mut [T], pivot: &T, is_less: &mut F) -> usize
        where
            F: FnMut(&T, &T) -> bool,
        {
            // Novel partition implementation by Lukas Bergdoll and Orson Peters. Branchless Lomuto
            // partition paired with a cyclic permutation.
            // https://github.com/Voultapher/sort-research-rs/blob/main/writeup/lomcyc_partition/text.md
        
            let len = v.len();
            let v_base = v.as_mut_ptr();
        
            if len == 0 {
                return 0;
            }
        
            // SAFETY: We checked that `len` is more than zero, which means that reading `v_base` is safe to
            // do. From there we have a bounded loop where `v_base.add(i)` is guaranteed in-bounds. `v` and
            // `pivot` can't alias because of type system rules. The drop-guard `gap` ensures that should
            // `is_less` panic we always overwrite the duplicate in the input. `gap.pos` stores the previous
            // value of `right` and starts at `v_base` and so it too is in-bounds. Given `UNROLL_LEN == 2`
            // after the main loop we either have A) the last element in `v` that has not yet been processed
            // because `len % 2 != 0`, or B) all elements have been processed except the gap value that was
            // saved at the beginning with `ptr::read(v_base)`. In the case A) the loop will iterate twice,
            // first performing loop_body to take care of the last element that didn't fit into the unroll.
            // After that the behavior is the same as for B) where we use the saved value as `right` to
            // overwrite the duplicate. If this very last call to `is_less` panics the saved value will be
            // copied back including all possible changes via interior mutability. If `is_less` does not
            // panic and the code continues we overwrite the duplicate and do `right = right.add(1)`, this
            // is safe to do with `&mut *gap.value` because `T` is the same as `[T; 1]` and generating a
            // pointer one past the allocation is safe.
            unsafe {
                let mut loop_body = |state: &mut PartitionState<T>| {
                    let right_is_lt = is_less(&*state.right, pivot);
                    let left = v_base.add(state.num_lt);
        
                    ptr::copy(left, state.gap.pos, 1);
                    ptr::copy_nonoverlapping(state.right, left, 1);
        
                    state.gap.pos = state.right;
                    state.num_lt += right_is_lt as usize;
        
                    state.right = state.right.add(1);
                };
        
                // Ideally we could just use GapGuard in PartitionState, but the reference that is
                // materialized with `&mut state` when calling `loop_body` would create a mutable reference
                // to the parent struct that contains the gap value, invalidating the reference pointer
                // created from a reference to the gap value in the cleanup loop. This is only an issue
                // under Stacked Borrows, Tree Borrows accepts the intuitive code using GapGuard as valid.
                let mut gap_value = ManuallyDrop::new(ptr::read(v_base));
        
                let mut state = PartitionState {
                    num_lt: 0,
                    right: v_base.add(1),
        
                    gap: GapGuardRaw { pos: v_base, value: &mut *gap_value },
                };
        
                // Manual unrolling that works well on x86, Arm and with opt-level=s without murdering
                // compile-times. Leaving this to the compiler yields ok to bad results.
                let unroll_len = const { if mem::size_of::<T>() <= 16 { 2 } else { 1 } };
        
                let unroll_end = v_base.add(len - (unroll_len - 1));
                while state.right < unroll_end {
                    if unroll_len == 2 {
                        loop_body(&mut state);
                        loop_body(&mut state);
                    } else {
                        loop_body(&mut state);
                    }
                }
        
                // Single instantiate `loop_body` for both the unroll cleanup and cyclic permutation
                // cleanup. Optimizes binary-size and compile-time.
                let end = v_base.add(len);
                loop {
                    let is_done = state.right == end;
                    state.right = if is_done { state.gap.value } else { state.right };
        
                    loop_body(&mut state);
        
                    if is_done {
                        mem::forget(state.gap);
                        break;
                    }
                }
        
                state.num_lt
            }
        }
        *)
        Definition partition_lomuto_branchless_cyclic
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; pivot; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let pivot := M.alloc (| pivot |) 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~ 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.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) 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.Integer IntegerKind.Usize 0 |) |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ loop_body :=
                      M.alloc (|
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let state := M.copy (| γ |) in
                                          M.read (|
                                            let~ right_is_lt :=
                                              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 (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| state |),
                                                            "core::slice::sort::unstable::quicksort::PartitionState",
                                                            "right"
                                                          |)
                                                        |);
                                                        M.read (| pivot |)
                                                      ]
                                                  ]
                                                |)
                                              |) in
                                            let~ left :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v_base |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| state |),
                                                        "core::slice::sort::unstable::quicksort::PartitionState",
                                                        "num_lt"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::intrinsics::copy",
                                                    [ T ]
                                                  |),
                                                  [
                                                    (* MutToConstPointer *)
                                                    M.pointer_coercion (M.read (| left |));
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| state |),
                                                          "core::slice::sort::unstable::quicksort::PartitionState",
                                                          "gap"
                                                        |),
                                                        "core::slice::sort::unstable::quicksort::GapGuardRaw",
                                                        "pos"
                                                      |)
                                                    |);
                                                    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.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| state |),
                                                          "core::slice::sort::unstable::quicksort::PartitionState",
                                                          "right"
                                                        |)
                                                      |));
                                                    M.read (| left |);
                                                    Value.Integer IntegerKind.Usize 1
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| state |),
                                                    "core::slice::sort::unstable::quicksort::PartitionState",
                                                    "gap"
                                                  |),
                                                  "core::slice::sort::unstable::quicksort::GapGuardRaw",
                                                  "pos"
                                                |),
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| state |),
                                                    "core::slice::sort::unstable::quicksort::PartitionState",
                                                    "right"
                                                  |)
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β :=
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| state |),
                                                  "core::slice::sort::unstable::quicksort::PartitionState",
                                                  "num_lt"
                                                |) in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.add (|
                                                  M.read (| β |),
                                                  M.rust_cast (M.read (| right_is_lt |))
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| state |),
                                                  "core::slice::sort::unstable::quicksort::PartitionState",
                                                  "right"
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| state |),
                                                        "core::slice::sort::unstable::quicksort::PartitionState",
                                                        "right"
                                                      |)
                                                    |);
                                                    Value.Integer IntegerKind.Usize 1
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |) in
                    let~ gap_value :=
                      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 (| v_base |)) ]
                            |)
                          ]
                        |)
                      |) in
                    let~ state :=
                      M.alloc (|
                        Value.StructRecord
                          "core::slice::sort::unstable::quicksort::PartitionState"
                          [
                            ("num_lt", Value.Integer IntegerKind.Usize 0);
                            ("right",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); Value.Integer IntegerKind.Usize 1 ]
                              |));
                            ("gap",
                              Value.StructRecord
                                "core::slice::sort::unstable::quicksort::GapGuardRaw"
                                [
                                  ("pos", M.read (| v_base |));
                                  ("value",
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::DerefMut",
                                        Ty.apply
                                          (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                          []
                                          [ T ],
                                        [],
                                        "deref_mut",
                                        []
                                      |),
                                      [ gap_value ]
                                    |))
                                ])
                          ]
                      |) in
                    let~ unroll_len :=
                      M.copy (|
                        M.get_constant (|
                          "core::slice::sort::unstable::quicksort::partition_lomuto_branchless_cyclic_discriminant"
                        |)
                      |) in
                    let~ unroll_end :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*mut") [] [ T ],
                            "add",
                            []
                          |),
                          [
                            M.read (| v_base |);
                            BinOp.Wrap.sub (|
                              M.read (| len |),
                              BinOp.Wrap.sub (|
                                M.read (| unroll_len |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              state,
                                              "core::slice::sort::unstable::quicksort::PartitionState",
                                              "right"
                                            |)
                                          |),
                                          M.read (| unroll_end |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.eq (|
                                                  M.read (| unroll_len |),
                                                  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_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  Ty.function
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&mut")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::slice::sort::unstable::quicksort::PartitionState")
                                                                []
                                                                [ T ]
                                                            ]
                                                        ]
                                                    ]
                                                    (Ty.tuple []),
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&mut")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::slice::sort::unstable::quicksort::PartitionState")
                                                              []
                                                              [ T ]
                                                          ]
                                                      ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ loop_body; Value.Tuple [ state ] ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  Ty.function
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&mut")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::slice::sort::unstable::quicksort::PartitionState")
                                                                []
                                                                [ T ]
                                                            ]
                                                        ]
                                                    ]
                                                    (Ty.tuple []),
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&mut")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::slice::sort::unstable::quicksort::PartitionState")
                                                              []
                                                              [ T ]
                                                          ]
                                                      ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ loop_body; Value.Tuple [ state ] ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  Ty.function
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&mut")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::slice::sort::unstable::quicksort::PartitionState")
                                                                []
                                                                [ T ]
                                                            ]
                                                        ]
                                                    ]
                                                    (Ty.tuple []),
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&mut")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::slice::sort::unstable::quicksort::PartitionState")
                                                              []
                                                              [ T ]
                                                          ]
                                                      ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ loop_body; Value.Tuple [ state ] ]
                                              |)
                                            |) 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 [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ 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~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (let~ is_done :=
                            M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    state,
                                    "core::slice::sort::unstable::quicksort::PartitionState",
                                    "right"
                                  |)
                                |),
                                M.read (| end_ |)
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                state,
                                "core::slice::sort::unstable::quicksort::PartitionState",
                                "right"
                              |),
                              M.read (|
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use is_done in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            state,
                                            "core::slice::sort::unstable::quicksort::PartitionState",
                                            "gap"
                                          |),
                                          "core::slice::sort::unstable::quicksort::GapGuardRaw",
                                          "value"
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.SubPointer.get_struct_record_field (|
                                          state,
                                          "core::slice::sort::unstable::quicksort::PartitionState",
                                          "right"
                                        |)))
                                  ]
                                |)
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnMut",
                                  Ty.function
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&mut")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path
                                                  "core::slice::sort::unstable::quicksort::PartitionState")
                                                []
                                                [ T ]
                                            ]
                                        ]
                                    ]
                                    (Ty.tuple []),
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&mut")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path
                                                "core::slice::sort::unstable::quicksort::PartitionState")
                                              []
                                              [ T ]
                                          ]
                                      ]
                                  ],
                                  "call_mut",
                                  []
                                |),
                                [ loop_body; Value.Tuple [ state ] ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use is_done in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::mem::forget",
                                                [
                                                  Ty.apply
                                                    (Ty.path
                                                      "core::slice::sort::unstable::quicksort::GapGuardRaw")
                                                    []
                                                    [ T ]
                                                ]
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    state,
                                                    "core::slice::sort::unstable::quicksort::PartitionState",
                                                    "gap"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.break (||)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)))
                      |) in
                    M.SubPointer.get_struct_record_field (|
                      state,
                      "core::slice::sort::unstable::quicksort::PartitionState",
                      "num_lt"
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_partition_lomuto_branchless_cyclic :
          M.IsFunction
            "core::slice::sort::unstable::quicksort::partition_lomuto_branchless_cyclic"
            partition_lomuto_branchless_cyclic.
        
        (* StructRecord
          {
            name := "GapGuard";
            const_params := [];
            ty_params := [ "T" ];
            fields :=
              [
                ("pos", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("value", Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ])
              ];
          } *)
        
        Module Impl_core_ops_drop_Drop_for_core_slice_sort_unstable_quicksort_GapGuard_T.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "core::slice::sort::unstable::quicksort::GapGuard") [] [ T ].
          
          (*
              fn drop(&mut self) {
                  // SAFETY: `self` MUST be constructed in a way that makes copying the gap value into
                  // `self.pos` sound.
                  unsafe {
                      ptr::copy_nonoverlapping(&*self.value, self.pos, 1);
                  }
              }
          *)
          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.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::sort::unstable::quicksort::GapGuard",
                                "value"
                              |)
                            ]
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::unstable::quicksort::GapGuard",
                              "pos"
                            |)
                          |);
                          Value.Integer IntegerKind.Usize 1
                        ]
                      |)
                    |) 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_unstable_quicksort_GapGuard_T.
        
        (* StructRecord
          {
            name := "GapGuardRaw";
            const_params := [];
            ty_params := [ "T" ];
            fields :=
              [
                ("pos", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("value", Ty.apply (Ty.path "*mut") [] [ T ])
              ];
          } *)
        
        Module Impl_core_ops_drop_Drop_for_core_slice_sort_unstable_quicksort_GapGuardRaw_T.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "core::slice::sort::unstable::quicksort::GapGuardRaw") [] [ T ].
          
          (*
              fn drop(&mut self) {
                  // SAFETY: `self` MUST be constructed in a way that makes copying the gap value into
                  // `self.pos` sound.
                  unsafe {
                      ptr::copy_nonoverlapping(self.value, self.pos, 1);
                  }
              }
          *)
          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 ] |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::sort::unstable::quicksort::GapGuardRaw",
                                "value"
                              |)
                            |));
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::unstable::quicksort::GapGuardRaw",
                              "pos"
                            |)
                          |);
                          Value.Integer IntegerKind.Usize 1
                        ]
                      |)
                    |) 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_unstable_quicksort_GapGuardRaw_T.
      End quicksort.
    End unstable.
  End sort.
End slice.
