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

Module slice.
  Module rotate.
    (*
    pub unsafe fn ptr_rotate<T>(mut left: usize, mut mid: *mut T, mut right: usize) {
        type BufType = [usize; 32];
        if T::IS_ZST {
            return;
        }
        loop {
            // N.B. the below algorithms can fail if these cases are not checked
            if (right == 0) || (left == 0) {
                return;
            }
            if !cfg!(feature = "optimize_for_size")
                && ((left + right < 24) || (mem::size_of::<T>() > mem::size_of::<[usize; 4]>()))
            {
                // Algorithm 1
                // Microbenchmarks indicate that the average performance for random shifts is better all
                // the way until about `left + right == 32`, but the worst case performance breaks even
                // around 16. 24 was chosen as middle ground. If the size of `T` is larger than 4
                // `usize`s, this algorithm also outperforms other algorithms.
                // SAFETY: callers must ensure `mid - left` is valid for reading and writing.
                let x = unsafe { mid.sub(left) };
                // beginning of first round
                // SAFETY: see previous comment.
                let mut tmp: T = unsafe { x.read() };
                let mut i = right;
                // `gcd` can be found before hand by calculating `gcd(left + right, right)`,
                // but it is faster to do one loop which calculates the gcd as a side effect, then
                // doing the rest of the chunk
                let mut gcd = right;
                // benchmarks reveal that it is faster to swap temporaries all the way through instead
                // of reading one temporary once, copying backwards, and then writing that temporary at
                // the very end. This is possibly due to the fact that swapping or replacing temporaries
                // uses only one memory address in the loop instead of needing to manage two.
                loop {
                    // [long-safety-expl]
                    // SAFETY: callers must ensure `[left, left+mid+right)` are all valid for reading and
                    // writing.
                    //
                    // - `i` start with `right` so `mid-left <= x+i = x+right = mid-left+right < mid+right`
                    // - `i <= left+right-1` is always true
                    //   - if `i < left`, `right` is added so `i < left+right` and on the next
                    //     iteration `left` is removed from `i` so it doesn't go further
                    //   - if `i >= left`, `left` is removed immediately and so it doesn't go further.
                    // - overflows cannot happen for `i` since the function's safety contract ask for
                    //   `mid+right-1 = x+left+right` to be valid for writing
                    // - underflows cannot happen because `i` must be bigger or equal to `left` for
                    //   a subtraction of `left` to happen.
                    //
                    // So `x+i` is valid for reading and writing if the caller respected the contract
                    tmp = unsafe { x.add(i).replace(tmp) };
                    // instead of incrementing `i` and then checking if it is outside the bounds, we
                    // check if `i` will go outside the bounds on the next increment. This prevents
                    // any wrapping of pointers or `usize`.
                    if i >= left {
                        i -= left;
                        if i == 0 {
                            // end of first round
                            // SAFETY: tmp has been read from a valid source and x is valid for writing
                            // according to the caller.
                            unsafe { x.write(tmp) };
                            break;
                        }
                        // this conditional must be here if `left + right >= 15`
                        if i < gcd {
                            gcd = i;
                        }
                    } else {
                        i += right;
                    }
                }
                // finish the chunk with more rounds
                for start in 1..gcd {
                    // SAFETY: `gcd` is at most equal to `right` so all values in `1..gcd` are valid for
                    // reading and writing as per the function's safety contract, see [long-safety-expl]
                    // above
                    tmp = unsafe { x.add(start).read() };
                    // [safety-expl-addition]
                    //
                    // Here `start < gcd` so `start < right` so `i < right+right`: `right` being the
                    // greatest common divisor of `(left+right, right)` means that `left = right` so
                    // `i < left+right` so `x+i = mid-left+i` is always valid for reading and writing
                    // according to the function's safety contract.
                    i = start + right;
                    loop {
                        // SAFETY: see [long-safety-expl] and [safety-expl-addition]
                        tmp = unsafe { x.add(i).replace(tmp) };
                        if i >= left {
                            i -= left;
                            if i == start {
                                // SAFETY: see [long-safety-expl] and [safety-expl-addition]
                                unsafe { x.add(start).write(tmp) };
                                break;
                            }
                        } else {
                            i += right;
                        }
                    }
                }
                return;
            // `T` is not a zero-sized type, so it's okay to divide by its size.
            } else if !cfg!(feature = "optimize_for_size")
                && cmp::min(left, right) <= mem::size_of::<BufType>() / mem::size_of::<T>()
            {
                // Algorithm 2
                // The `[T; 0]` here is to ensure this is appropriately aligned for T
                let mut rawarray = MaybeUninit::<(BufType, [T; 0])>::uninit();
                let buf = rawarray.as_mut_ptr() as *mut T;
                // SAFETY: `mid-left <= mid-left+right < mid+right`
                let dim = unsafe { mid.sub(left).add(right) };
                if left <= right {
                    // SAFETY:
                    //
                    // 1) The `else if` condition about the sizes ensures `[mid-left; left]` will fit in
                    //    `buf` without overflow and `buf` was created just above and so cannot be
                    //    overlapped with any value of `[mid-left; left]`
                    // 2) [mid-left, mid+right) are all valid for reading and writing and we don't care
                    //    about overlaps here.
                    // 3) The `if` condition about `left <= right` ensures writing `left` elements to
                    //    `dim = mid-left+right` is valid because:
                    //    - `buf` is valid and `left` elements were written in it in 1)
                    //    - `dim+left = mid-left+right+left = mid+right` and we write `[dim, dim+left)`
                    unsafe {
                        // 1)
                        ptr::copy_nonoverlapping(mid.sub(left), buf, left);
                        // 2)
                        ptr::copy(mid, mid.sub(left), right);
                        // 3)
                        ptr::copy_nonoverlapping(buf, dim, left);
                    }
                } else {
                    // SAFETY: same reasoning as above but with `left` and `right` reversed
                    unsafe {
                        ptr::copy_nonoverlapping(mid, buf, right);
                        ptr::copy(mid.sub(left), dim, left);
                        ptr::copy_nonoverlapping(buf, mid.sub(left), right);
                    }
                }
                return;
            } else if left >= right {
                // Algorithm 3
                // There is an alternate way of swapping that involves finding where the last swap
                // of this algorithm would be, and swapping using that last chunk instead of swapping
                // adjacent chunks like this algorithm is doing, but this way is still faster.
                loop {
                    // SAFETY:
                    // `left >= right` so `[mid-right, mid+right)` is valid for reading and writing
                    // Subtracting `right` from `mid` each turn is counterbalanced by the addition and
                    // check after it.
                    unsafe {
                        ptr::swap_nonoverlapping(mid.sub(right), mid, right);
                        mid = mid.sub(right);
                    }
                    left -= right;
                    if left < right {
                        break;
                    }
                }
            } else {
                // Algorithm 3, `left < right`
                loop {
                    // SAFETY: `[mid-left, mid+left)` is valid for reading and writing because
                    // `left < right` so `mid+left < mid+right`.
                    // Adding `left` to `mid` each turn is counterbalanced by the subtraction and check
                    // after it.
                    unsafe {
                        ptr::swap_nonoverlapping(mid.sub(left), mid, left);
                        mid = mid.add(left);
                    }
                    right -= left;
                    if right < left {
                        break;
                    }
                }
            }
        }
    }
    *)
    Definition ptr_rotate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ _ as left; mid; _ as right ] =>
        ltac:(M.monadic
          (let left := M.alloc (| left |) in
          let mid := M.alloc (| mid |) in
          let right := M.alloc (| right |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  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 (|
                                          LogicalOp.or (|
                                            BinOp.eq (|
                                              M.read (| right |),
                                              Value.Integer IntegerKind.Usize 0
                                            |),
                                            ltac:(M.monadic
                                              (BinOp.eq (|
                                                M.read (| left |),
                                                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.Tuple [] |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          UnOp.not (| Value.Bool false |),
                                          ltac:(M.monadic
                                            (LogicalOp.or (|
                                              BinOp.lt (|
                                                BinOp.Wrap.add (|
                                                  M.read (| left |),
                                                  M.read (| right |)
                                                |),
                                                Value.Integer IntegerKind.Usize 24
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.gt (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::mem::size_of",
                                                      [ T ]
                                                    |),
                                                    []
                                                  |),
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::mem::size_of",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "array")
                                                          [ Value.Integer IntegerKind.Usize 4 ]
                                                          [ Ty.path "usize" ]
                                                      ]
                                                    |),
                                                    []
                                                  |)
                                                |)))
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "sub",
                                                []
                                              |),
                                              [ M.read (| mid |); M.read (| left |) ]
                                            |)
                                          |) in
                                        let~ tmp :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "read",
                                                []
                                              |),
                                              [ M.read (| x |) ]
                                            |)
                                          |) in
                                        let~ i := M.copy (| right |) in
                                        let~ gcd := M.copy (| right |) in
                                        let~ _ :=
                                          M.loop (|
                                            ltac:(M.monadic
                                              (let~ _ :=
                                                M.write (|
                                                  tmp,
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "replace",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply (Ty.path "*mut") [] [ T ],
                                                          "add",
                                                          []
                                                        |),
                                                        [ M.read (| x |); M.read (| i |) ]
                                                      |);
                                                      M.read (| tmp |)
                                                    ]
                                                  |)
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.ge (|
                                                              M.read (| i |),
                                                              M.read (| left |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        let β := i in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.sub (|
                                                            M.read (| β |),
                                                            M.read (| left |)
                                                          |)
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      BinOp.eq (|
                                                                        M.read (| i |),
                                                                        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 (|
                                                                      let~ _ :=
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "*mut")
                                                                                []
                                                                                [ T ],
                                                                              "write",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (| x |);
                                                                              M.read (| tmp |)
                                                                            ]
                                                                          |)
                                                                        |) in
                                                                      M.break (||)
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    BinOp.lt (|
                                                                      M.read (| i |),
                                                                      M.read (| gcd |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              let~ _ :=
                                                                M.write (| gcd, M.read (| i |) |) in
                                                              M.alloc (| Value.Tuple [] |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let~ _ :=
                                                        let β := i in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.add (|
                                                            M.read (| β |),
                                                            M.read (| right |)
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                          |) in
                                        let~ _ :=
                                          M.use
                                            (M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::collect::IntoIterator",
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::Range")
                                                      []
                                                      [ Ty.path "usize" ],
                                                    [],
                                                    "into_iter",
                                                    []
                                                  |),
                                                  [
                                                    Value.StructRecord
                                                      "core::ops::range::Range"
                                                      [
                                                        ("start",
                                                          Value.Integer IntegerKind.Usize 1);
                                                        ("end_", M.read (| gcd |))
                                                      ]
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let iter := M.copy (| γ |) in
                                                    M.loop (|
                                                      ltac:(M.monadic
                                                        (let~ _ :=
                                                          M.match_operator (|
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::iter::traits::iterator::Iterator",
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::Range")
                                                                    []
                                                                    [ Ty.path "usize" ],
                                                                  [],
                                                                  "next",
                                                                  []
                                                                |),
                                                                [ iter ]
                                                              |)
                                                            |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let _ :=
                                                                    M.is_struct_tuple (|
                                                                      γ,
                                                                      "core::option::Option::None"
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (| M.break (||) |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ0_0 :=
                                                                    M.SubPointer.get_struct_tuple_field (|
                                                                      γ,
                                                                      "core::option::Option::Some",
                                                                      0
                                                                    |) in
                                                                  let start := M.copy (| γ0_0 |) in
                                                                  let~ _ :=
                                                                    M.write (|
                                                                      tmp,
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path "*mut")
                                                                            []
                                                                            [ T ],
                                                                          "read",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "*mut")
                                                                                []
                                                                                [ T ],
                                                                              "add",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (| x |);
                                                                              M.read (| start |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) in
                                                                  let~ _ :=
                                                                    M.write (|
                                                                      i,
                                                                      BinOp.Wrap.add (|
                                                                        M.read (| start |),
                                                                        M.read (| right |)
                                                                      |)
                                                                    |) in
                                                                  M.loop (|
                                                                    ltac:(M.monadic
                                                                      (let~ _ :=
                                                                        M.write (|
                                                                          tmp,
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "*mut")
                                                                                []
                                                                                [ T ],
                                                                              "replace",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path "*mut")
                                                                                    []
                                                                                    [ T ],
                                                                                  "add",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (| x |);
                                                                                  M.read (| i |)
                                                                                ]
                                                                              |);
                                                                              M.read (| tmp |)
                                                                            ]
                                                                          |)
                                                                        |) in
                                                                      M.match_operator (|
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ :=
                                                                                M.use
                                                                                  (M.alloc (|
                                                                                    BinOp.ge (|
                                                                                      M.read (|
                                                                                        i
                                                                                      |),
                                                                                      M.read (|
                                                                                        left
                                                                                      |)
                                                                                    |)
                                                                                  |)) in
                                                                              let _ :=
                                                                                M.is_constant_or_break_match (|
                                                                                  M.read (| γ |),
                                                                                  Value.Bool true
                                                                                |) in
                                                                              let~ _ :=
                                                                                let β := i in
                                                                                M.write (|
                                                                                  β,
                                                                                  BinOp.Wrap.sub (|
                                                                                    M.read (| β |),
                                                                                    M.read (|
                                                                                      left
                                                                                    |)
                                                                                  |)
                                                                                |) in
                                                                              M.match_operator (|
                                                                                M.alloc (|
                                                                                  Value.Tuple []
                                                                                |),
                                                                                [
                                                                                  fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      (let γ :=
                                                                                        M.use
                                                                                          (M.alloc (|
                                                                                            BinOp.eq (|
                                                                                              M.read (|
                                                                                                i
                                                                                              |),
                                                                                              M.read (|
                                                                                                start
                                                                                              |)
                                                                                            |)
                                                                                          |)) 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_associated_function (|
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "*mut")
                                                                                                      []
                                                                                                      [
                                                                                                        T
                                                                                                      ],
                                                                                                    "write",
                                                                                                    []
                                                                                                  |),
                                                                                                  [
                                                                                                    M.call_closure (|
                                                                                                      M.get_associated_function (|
                                                                                                        Ty.apply
                                                                                                          (Ty.path
                                                                                                            "*mut")
                                                                                                          []
                                                                                                          [
                                                                                                            T
                                                                                                          ],
                                                                                                        "add",
                                                                                                        []
                                                                                                      |),
                                                                                                      [
                                                                                                        M.read (|
                                                                                                          x
                                                                                                        |);
                                                                                                        M.read (|
                                                                                                          start
                                                                                                        |)
                                                                                                      ]
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      tmp
                                                                                                    |)
                                                                                                  ]
                                                                                                |)
                                                                                              |) in
                                                                                            M.break (||)
                                                                                          |)
                                                                                        |)
                                                                                      |)));
                                                                                  fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      (M.alloc (|
                                                                                        Value.Tuple
                                                                                          []
                                                                                      |)))
                                                                                ]
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let~ _ :=
                                                                                let β := i in
                                                                                M.write (|
                                                                                  β,
                                                                                  BinOp.Wrap.add (|
                                                                                    M.read (| β |),
                                                                                    M.read (|
                                                                                      right
                                                                                    |)
                                                                                  |)
                                                                                |) in
                                                                              M.alloc (|
                                                                                Value.Tuple []
                                                                              |)))
                                                                        ]
                                                                      |)))
                                                                  |)))
                                                            ]
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                    |)))
                                              ]
                                            |)) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                LogicalOp.and (|
                                                  UnOp.not (| Value.Bool false |),
                                                  ltac:(M.monadic
                                                    (BinOp.le (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::cmp::min",
                                                          [ Ty.path "usize" ]
                                                        |),
                                                        [ M.read (| left |); M.read (| right |) ]
                                                      |),
                                                      BinOp.Wrap.div (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::mem::size_of",
                                                            [
                                                              Ty.apply
                                                                (Ty.path "array")
                                                                [ Value.Integer IntegerKind.Usize 32
                                                                ]
                                                                [ Ty.path "usize" ]
                                                            ]
                                                          |),
                                                          []
                                                        |),
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::mem::size_of",
                                                            [ T ]
                                                          |),
                                                          []
                                                        |)
                                                      |)
                                                    |)))
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ rawarray :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::mem::maybe_uninit::MaybeUninit")
                                                          []
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "array")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      32
                                                                  ]
                                                                  [ Ty.path "usize" ];
                                                                Ty.apply
                                                                  (Ty.path "array")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      0
                                                                  ]
                                                                  [ T ]
                                                              ]
                                                          ],
                                                        "uninit",
                                                        []
                                                      |),
                                                      []
                                                    |)
                                                  |) in
                                                let~ buf :=
                                                  M.alloc (|
                                                    M.rust_cast
                                                      (M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "array")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        32
                                                                    ]
                                                                    [ Ty.path "usize" ];
                                                                  Ty.apply
                                                                    (Ty.path "array")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        0
                                                                    ]
                                                                    [ T ]
                                                                ]
                                                            ],
                                                          "as_mut_ptr",
                                                          []
                                                        |),
                                                        [ rawarray ]
                                                      |))
                                                  |) in
                                                let~ dim :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply (Ty.path "*mut") [] [ T ],
                                                        "add",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply (Ty.path "*mut") [] [ T ],
                                                            "sub",
                                                            []
                                                          |),
                                                          [ M.read (| mid |); M.read (| left |) ]
                                                        |);
                                                        M.read (| right |)
                                                      ]
                                                    |)
                                                  |) in
                                                let~ _ :=
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.le (|
                                                                  M.read (| left |),
                                                                  M.read (| right |)
                                                                |)
                                                              |)) 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.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "*mut")
                                                                          []
                                                                          [ T ],
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| mid |);
                                                                        M.read (| left |)
                                                                      ]
                                                                    |));
                                                                  M.read (| buf |);
                                                                  M.read (| left |)
                                                                ]
                                                              |)
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::intrinsics::copy",
                                                                  [ T ]
                                                                |),
                                                                [
                                                                  (* MutToConstPointer *)
                                                                  M.pointer_coercion
                                                                    (M.read (| mid |));
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path "*mut")
                                                                        []
                                                                        [ T ],
                                                                      "sub",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| mid |);
                                                                      M.read (| left |)
                                                                    ]
                                                                  |);
                                                                  M.read (| right |)
                                                                ]
                                                              |)
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::intrinsics::copy_nonoverlapping",
                                                                  [ T ]
                                                                |),
                                                                [
                                                                  (* MutToConstPointer *)
                                                                  M.pointer_coercion
                                                                    (M.read (| buf |));
                                                                  M.read (| dim |);
                                                                  M.read (| left |)
                                                                ]
                                                              |)
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::intrinsics::copy_nonoverlapping",
                                                                  [ T ]
                                                                |),
                                                                [
                                                                  (* MutToConstPointer *)
                                                                  M.pointer_coercion
                                                                    (M.read (| mid |));
                                                                  M.read (| buf |);
                                                                  M.read (| right |)
                                                                ]
                                                              |)
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::intrinsics::copy",
                                                                  [ T ]
                                                                |),
                                                                [
                                                                  (* MutToConstPointer *)
                                                                  M.pointer_coercion
                                                                    (M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path "*mut")
                                                                          []
                                                                          [ T ],
                                                                        "sub",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| mid |);
                                                                        M.read (| left |)
                                                                      ]
                                                                    |));
                                                                  M.read (| dim |);
                                                                  M.read (| left |)
                                                                ]
                                                              |)
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::intrinsics::copy_nonoverlapping",
                                                                  [ T ]
                                                                |),
                                                                [
                                                                  (* MutToConstPointer *)
                                                                  M.pointer_coercion
                                                                    (M.read (| buf |));
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path "*mut")
                                                                        []
                                                                        [ T ],
                                                                      "sub",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| mid |);
                                                                      M.read (| left |)
                                                                    ]
                                                                  |);
                                                                  M.read (| right |)
                                                                ]
                                                              |)
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (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.loop (|
                                                    ltac:(M.monadic
                                                      (let~ _ :=
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_function (|
                                                                "core::ptr::swap_nonoverlapping",
                                                                [ T ]
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "*mut")
                                                                      []
                                                                      [ T ],
                                                                    "sub",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| mid |);
                                                                    M.read (| right |)
                                                                  ]
                                                                |);
                                                                M.read (| mid |);
                                                                M.read (| right |)
                                                              ]
                                                            |)
                                                          |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            mid,
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                                "sub",
                                                                []
                                                              |),
                                                              [ M.read (| mid |); M.read (| right |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |) in
                                                      let~ _ :=
                                                        let β := left in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.sub (|
                                                            M.read (| β |),
                                                            M.read (| right |)
                                                          |)
                                                        |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    BinOp.lt (|
                                                                      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 [] |)))
                                                        ]
                                                      |)))
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.loop (|
                                                    ltac:(M.monadic
                                                      (let~ _ :=
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_function (|
                                                                "core::ptr::swap_nonoverlapping",
                                                                [ T ]
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "*mut")
                                                                      []
                                                                      [ T ],
                                                                    "sub",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| mid |);
                                                                    M.read (| left |)
                                                                  ]
                                                                |);
                                                                M.read (| mid |);
                                                                M.read (| left |)
                                                              ]
                                                            |)
                                                          |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            mid,
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                                "add",
                                                                []
                                                              |),
                                                              [ M.read (| mid |); M.read (| left |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |) in
                                                      let~ _ :=
                                                        let β := right in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.sub (|
                                                            M.read (| β |),
                                                            M.read (| left |)
                                                          |)
                                                        |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    BinOp.lt (|
                                                                      M.read (| right |),
                                                                      M.read (| left |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (| M.break (||) |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |)))
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                      |)
                    |)
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_ptr_rotate : M.IsFunction "core::slice::rotate::ptr_rotate" ptr_rotate.
    
    Module ptr_rotate.
      Axiom BufType :
        (Ty.path "core::slice::rotate::ptr_rotate::BufType") =
          (Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "usize" ]).
    End ptr_rotate.
  End rotate.
End slice.
