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

Module slice.
  Module sort.
    Module shared.
      Module pivot.
        Definition value_PSEUDO_MEDIAN_REC_THRESHOLD : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 64 |))).
        
        (*
        pub fn choose_pivot<T, F: FnMut(&T, &T) -> bool>(v: &[T], is_less: &mut F) -> usize {
            // We use unsafe code and raw pointers here because we're dealing with
            // heavy recursion. Passing safe slices around would involve a lot of
            // branches and function call overhead.
        
            let len = v.len();
            if len < 8 {
                intrinsics::abort();
            }
        
            // SAFETY: a, b, c point to initialized regions of len_div_8 elements,
            // satisfying median3 and median3_rec's preconditions as v_base points
            // to an initialized region of n = len elements.
            unsafe {
                let v_base = v.as_ptr();
                let len_div_8 = len / 8;
        
                let a = v_base; // [0, floor(n/8))
                let b = v_base.add(len_div_8 * 4); // [4*floor(n/8), 5*floor(n/8))
                let c = v_base.add(len_div_8 * 7); // [7*floor(n/8), 8*floor(n/8))
        
                if len < PSEUDO_MEDIAN_REC_THRESHOLD {
                    median3(&*a, &*b, &*c, is_less).sub_ptr(v_base)
                } else {
                    median3_rec(a, b, c, len_div_8, is_less).sub_ptr(v_base)
                }
            }
        }
        *)
        Definition choose_pivot (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (| M.read (| len |), Value.Integer IntegerKind.Usize 8 |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::abort", [] |),
                                []
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ v_base :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ len_div_8 :=
                  M.alloc (|
                    BinOp.Wrap.div (| M.read (| len |), Value.Integer IntegerKind.Usize 8 |)
                  |) in
                let~ a := M.copy (| v_base |) in
                let~ b :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "add",
                        []
                      |),
                      [
                        M.read (| v_base |);
                        BinOp.Wrap.mul (|
                          M.read (| len_div_8 |),
                          Value.Integer IntegerKind.Usize 4
                        |)
                      ]
                    |)
                  |) in
                let~ c :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*const") [] [ T ],
                        "add",
                        []
                      |),
                      [
                        M.read (| v_base |);
                        BinOp.Wrap.mul (|
                          M.read (| len_div_8 |),
                          Value.Integer IntegerKind.Usize 7
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| len |),
                                M.read (|
                                  M.get_constant (|
                                    "core::slice::sort::shared::pivot::PSEUDO_MEDIAN_REC_THRESHOLD"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ T ],
                              "sub_ptr",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::median3",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| a |);
                                  M.read (| b |);
                                  M.read (| c |);
                                  M.read (| is_less |)
                                ]
                              |);
                              M.read (| v_base |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ T ],
                              "sub_ptr",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::median3_rec",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| a |);
                                  M.read (| b |);
                                  M.read (| c |);
                                  M.read (| len_div_8 |);
                                  M.read (| is_less |)
                                ]
                              |);
                              M.read (| v_base |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_choose_pivot :
          M.IsFunction "core::slice::sort::shared::pivot::choose_pivot" choose_pivot.
        
        (*
        unsafe fn median3_rec<T, F: FnMut(&T, &T) -> bool>(
            mut a: *const T,
            mut b: *const T,
            mut c: *const T,
            n: usize,
            is_less: &mut F,
        ) -> *const T {
            // SAFETY: a, b, c still point to initialized regions of n / 8 elements,
            // by the exact same logic as in choose_pivot.
            unsafe {
                if n * 8 >= PSEUDO_MEDIAN_REC_THRESHOLD {
                    let n8 = n / 8;
                    a = median3_rec(a, a.add(n8 * 4), a.add(n8 * 7), n8, is_less);
                    b = median3_rec(b, b.add(n8 * 4), b.add(n8 * 7), n8, is_less);
                    c = median3_rec(c, c.add(n8 * 4), c.add(n8 * 7), n8, is_less);
                }
                median3(&*a, &*b, &*c, is_less)
            }
        }
        *)
        Definition median3_rec (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ a; b; c; n; is_less ] =>
            ltac:(M.monadic
              (let a := M.alloc (| a |) in
              let b := M.alloc (| b |) in
              let c := M.alloc (| c |) in
              let n := M.alloc (| n |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ge (|
                                  BinOp.Wrap.mul (|
                                    M.read (| n |),
                                    Value.Integer IntegerKind.Usize 8
                                  |),
                                  M.read (|
                                    M.get_constant (|
                                      "core::slice::sort::shared::pivot::PSEUDO_MEDIAN_REC_THRESHOLD"
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ n8 :=
                            M.alloc (|
                              BinOp.Wrap.div (| M.read (| n |), Value.Integer IntegerKind.Usize 8 |)
                            |) in
                          let~ _ :=
                            M.write (|
                              a,
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::median3_rec",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| a |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| a |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 4
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| a |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 7
                                      |)
                                    ]
                                  |);
                                  M.read (| n8 |);
                                  M.read (| is_less |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              b,
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::median3_rec",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| b |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| b |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 4
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| b |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 7
                                      |)
                                    ]
                                  |);
                                  M.read (| n8 |);
                                  M.read (| is_less |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              c,
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::shared::pivot::median3_rec",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| c |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| c |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 4
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| c |);
                                      BinOp.Wrap.mul (|
                                        M.read (| n8 |),
                                        Value.Integer IntegerKind.Usize 7
                                      |)
                                    ]
                                  |);
                                  M.read (| n8 |);
                                  M.read (| is_less |)
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::sort::shared::pivot::median3", [ T; F ] |),
                    [ M.read (| a |); M.read (| b |); M.read (| c |); M.read (| is_less |) ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_median3_rec :
          M.IsFunction "core::slice::sort::shared::pivot::median3_rec" median3_rec.
        
        (*
        fn median3<T, F: FnMut(&T, &T) -> bool>(a: &T, b: &T, c: &T, is_less: &mut F) -> *const T {
            // Compiler tends to make this branchless when sensible, and avoids the
            // third comparison when not.
            let x = is_less(a, b);
            let y = is_less(a, c);
            if x == y {
                // If x=y=0 then b, c <= a. In this case we want to return max(b, c).
                // If x=y=1 then a < b, c. In this case we want to return min(b, c).
                // By toggling the outcome of b < c using XOR x we get this behavior.
                let z = is_less(b, c);
                if z ^ x { c } else { b }
            } else {
                // Either c <= a < b or b <= a < c, thus a is our median.
                a
            }
        }
        *)
        Definition median3 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ a; b; c; is_less ] =>
            ltac:(M.monadic
              (let a := M.alloc (| a |) in
              let b := M.alloc (| b |) in
              let c := M.alloc (| c |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ x :=
                  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 (| a |); M.read (| b |) ] ]
                    |)
                  |) in
                let~ y :=
                  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 (| a |); M.read (| c |) ] ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use (M.alloc (| BinOp.eq (| M.read (| x |), M.read (| y |) |) |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ z :=
                          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 (| b |); M.read (| c |) ]
                              ]
                            |)
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.bit_xor (M.read (| z |)) (M.read (| x |))
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| M.read (| c |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| M.read (| b |) |)))
                          ]
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| M.read (| a |) |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_median3 : M.IsFunction "core::slice::sort::shared::pivot::median3" median3.
      End pivot.
    End shared.
  End sort.
End slice.
