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

Module slice.
  Module sort.
    Module stable.
      Module merge.
        (*
        pub fn merge<T, F: FnMut(&T, &T) -> bool>(
            v: &mut [T],
            scratch: &mut [MaybeUninit<T>],
            mid: usize,
            is_less: &mut F,
        ) {
            let len = v.len();
        
            if mid == 0 || mid >= len || scratch.len() < cmp::min(mid, len - mid) {
                return;
            }
        
            // SAFETY: We checked that the two slices are non-empty and `mid` is in-bounds.
            // We checked that the buffer `scratch` has enough capacity to hold a copy of
            // the shorter slice. `merge_up` and `merge_down` are written in such a way that
            // they uphold the contract described in `MergeState::drop`.
            unsafe {
                // The merge process first copies the shorter run into `buf`. Then it traces
                // the newly copied run and the longer run forwards (or backwards), comparing
                // their next unconsumed elements and copying the lesser (or greater) one into `v`.
                //
                // As soon as the shorter run is fully consumed, the process is done. If the
                // longer run gets consumed first, then we must copy whatever is left of the
                // shorter run into the remaining gap in `v`.
                //
                // Intermediate state of the process is always tracked by `gap`, which serves
                // two purposes:
                //  1. Protects integrity of `v` from panics in `is_less`.
                //  2. Fills the remaining gap in `v` if the longer run gets consumed first.
        
                let buf = MaybeUninit::slice_as_mut_ptr(scratch);
        
                let v_base = v.as_mut_ptr();
                let v_mid = v_base.add(mid);
                let v_end = v_base.add(len);
        
                let left_len = mid;
                let right_len = len - mid;
        
                let left_is_shorter = left_len <= right_len;
                let save_base = if left_is_shorter { v_base } else { v_mid };
                let save_len = if left_is_shorter { left_len } else { right_len };
        
                ptr::copy_nonoverlapping(save_base, buf, save_len);
        
                let mut merge_state = MergeState { start: buf, end: buf.add(save_len), dst: save_base };
        
                if left_is_shorter {
                    merge_state.merge_up(v_mid, v_end, is_less);
                } else {
                    merge_state.merge_down(v_base, buf, v_end, is_less);
                }
                // Finally, `merge_state` gets dropped. If the shorter run was not fully
                // consumed, whatever remains of it will now be copied into the hole in `v`.
            }
        }
        *)
        Definition merge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; scratch; mid; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let scratch := M.alloc (| scratch |) in
              let mid := M.alloc (| mid |) in
              let is_less := M.alloc (| is_less |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ len :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "len",
                            []
                          |),
                          [ M.read (| v |) ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.or (|
                                      LogicalOp.or (|
                                        BinOp.eq (|
                                          M.read (| mid |),
                                          Value.Integer IntegerKind.Usize 0
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.ge (| M.read (| mid |), M.read (| len |) |)))
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.lt (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                    []
                                                    [ T ]
                                                ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| scratch |) ]
                                          |),
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::cmp::min",
                                              [ Ty.path "usize" ]
                                            |),
                                            [
                                              M.read (| mid |);
                                              BinOp.Wrap.sub (|
                                                M.read (| len |),
                                                M.read (| mid |)
                                              |)
                                            ]
                                          |)
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ buf :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                            "slice_as_mut_ptr",
                            []
                          |),
                          [ M.read (| scratch |) ]
                        |)
                      |) in
                    let~ v_base :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "as_mut_ptr",
                            []
                          |),
                          [ M.read (| v |) ]
                        |)
                      |) in
                    let~ v_mid :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*mut") [] [ T ],
                            "add",
                            []
                          |),
                          [ M.read (| v_base |); M.read (| mid |) ]
                        |)
                      |) in
                    let~ v_end :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*mut") [] [ T ],
                            "add",
                            []
                          |),
                          [ M.read (| v_base |); M.read (| len |) ]
                        |)
                      |) in
                    let~ left_len := M.copy (| mid |) in
                    let~ right_len :=
                      M.alloc (| BinOp.Wrap.sub (| M.read (| len |), M.read (| mid |) |) |) in
                    let~ left_is_shorter :=
                      M.alloc (| BinOp.le (| M.read (| left_len |), M.read (| right_len |) |) |) in
                    let~ save_base :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use left_is_shorter in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                v_base));
                            fun γ => ltac:(M.monadic v_mid)
                          ]
                        |)
                      |) in
                    let~ save_len :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use left_is_shorter in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                left_len));
                            fun γ => ltac:(M.monadic right_len)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                          [
                            (* MutToConstPointer *) M.pointer_coercion (M.read (| save_base |));
                            M.read (| buf |);
                            M.read (| save_len |)
                          ]
                        |)
                      |) in
                    let~ merge_state :=
                      M.alloc (|
                        Value.StructRecord
                          "core::slice::sort::stable::merge::MergeState"
                          [
                            ("start", M.read (| buf |));
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| buf |); M.read (| save_len |) ]
                              |));
                            ("dst", M.read (| save_base |))
                          ]
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.use left_is_shorter in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::slice::sort::stable::merge::MergeState")
                                      []
                                      [ T ],
                                    "merge_up",
                                    [ F ]
                                  |),
                                  [
                                    merge_state;
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| v_mid |));
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| v_end |));
                                    M.read (| is_less |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::slice::sort::stable::merge::MergeState")
                                      []
                                      [ T ],
                                    "merge_down",
                                    [ F ]
                                  |),
                                  [
                                    merge_state;
                                    (* MutToConstPointer *)
                                    M.pointer_coercion (M.read (| v_base |));
                                    (* MutToConstPointer *) M.pointer_coercion (M.read (| buf |));
                                    M.read (| v_end |);
                                    M.read (| is_less |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_merge : M.IsFunction "core::slice::sort::stable::merge::merge" merge.
        
        (* StructRecord
          {
            name := "MergeState";
            const_params := [];
            ty_params := [ "T" ];
            fields :=
              [
                ("start", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("end_", Ty.apply (Ty.path "*mut") [] [ T ]);
                ("dst", Ty.apply (Ty.path "*mut") [] [ T ])
              ];
          } *)
        
        Module Impl_core_slice_sort_stable_merge_MergeState_T.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "core::slice::sort::stable::merge::MergeState") [] [ T ].
          
          (*
              unsafe fn merge_up<F: FnMut(&T, &T) -> bool>(
                  &mut self,
                  mut right: *const T,
                  right_end: *const T,
                  is_less: &mut F,
              ) {
                  // SAFETY: See function safety comment.
                  unsafe {
                      let left = &mut self.start;
                      let out = &mut self.dst;
          
                      while *left != self.end && right as *const T != right_end {
                          let consume_left = !is_less(&*right, &**left);
          
                          let src = if consume_left { *left } else { right };
                          ptr::copy_nonoverlapping(src, *out, 1);
          
                          *left = left.add(consume_left as usize);
                          right = right.add(!consume_left as usize);
          
                          *out = out.add(1);
                      }
                  }
              }
          *)
          Definition merge_up
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ self; _ as right; right_end; is_less ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let right := M.alloc (| right |) in
                let right_end := M.alloc (| right_end |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  let~ left :=
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::sort::stable::merge::MergeState",
                        "start"
                      |)
                    |) in
                  let~ out :=
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::sort::stable::merge::MergeState",
                        "dst"
                      |)
                    |) in
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.and (|
                                      BinOp.ne (|
                                        M.read (| M.read (| left |) |),
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::sort::stable::merge::MergeState",
                                            "end"
                                          |)
                                        |)
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.ne (|
                                          M.rust_cast (M.read (| right |)),
                                          M.read (| right_end |)
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ consume_left :=
                                M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::function::FnMut",
                                        F,
                                        [
                                          Ty.tuple
                                            [
                                              Ty.apply (Ty.path "&") [] [ T ];
                                              Ty.apply (Ty.path "&") [] [ T ]
                                            ]
                                        ],
                                        "call_mut",
                                        []
                                      |),
                                      [
                                        M.read (| is_less |);
                                        Value.Tuple
                                          [ M.read (| right |); M.read (| M.read (| left |) |) ]
                                      ]
                                    |)
                                  |)
                                |) in
                              let~ src :=
                                M.copy (|
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.use consume_left in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            (* MutToConstPointer *)
                                            M.pointer_coercion (M.read (| M.read (| left |) |))
                                          |)));
                                      fun γ => ltac:(M.monadic right)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::copy_nonoverlapping",
                                      [ T ]
                                    |),
                                    [
                                      M.read (| src |);
                                      M.read (| M.read (| out |) |);
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.read (| left |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| left |) |);
                                      M.rust_cast (M.read (| consume_left |))
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  right,
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| right |);
                                      M.rust_cast (UnOp.not (| M.read (| consume_left |) |))
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.read (| out |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| out |) |);
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_merge_up :
            forall (T : Ty.t),
            M.IsAssociatedFunction (Self T) "merge_up" (merge_up T).
          
          (*
              unsafe fn merge_down<F: FnMut(&T, &T) -> bool>(
                  &mut self,
                  left_end: *const T,
                  right_end: *const T,
                  mut out: *mut T,
                  is_less: &mut F,
              ) {
                  // SAFETY: See function safety comment.
                  unsafe {
                      loop {
                          let left = self.dst.sub(1);
                          let right = self.end.sub(1);
                          out = out.sub(1);
          
                          let consume_left = is_less(&*right, &*left);
          
                          let src = if consume_left { left } else { right };
                          ptr::copy_nonoverlapping(src, out, 1);
          
                          self.dst = left.add(!consume_left as usize);
                          self.end = right.add(consume_left as usize);
          
                          if self.dst as *const T == left_end || self.end as *const T == right_end {
                              break;
                          }
                      }
                  }
              }
          *)
          Definition merge_down
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [ F ], [ self; left_end; right_end; out; is_less ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let left_end := M.alloc (| left_end |) in
                let right_end := M.alloc (| right_end |) in
                let out := M.alloc (| out |) in
                let is_less := M.alloc (| is_less |) in
                M.read (|
                  M.loop (|
                    ltac:(M.monadic
                      (let~ left :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "sub",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::sort::stable::merge::MergeState",
                                  "dst"
                                |)
                              |);
                              Value.Integer IntegerKind.Usize 1
                            ]
                          |)
                        |) in
                      let~ right :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "sub",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::sort::stable::merge::MergeState",
                                  "end"
                                |)
                              |);
                              Value.Integer IntegerKind.Usize 1
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          out,
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "sub",
                              []
                            |),
                            [ M.read (| out |); Value.Integer IntegerKind.Usize 1 ]
                          |)
                        |) in
                      let~ consume_left :=
                        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 (| right |); M.read (| left |) ]
                            ]
                          |)
                        |) in
                      let~ src :=
                        M.copy (|
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use consume_left in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  left));
                              fun γ => ltac:(M.monadic right)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                            [
                              (* MutToConstPointer *) M.pointer_coercion (M.read (| src |));
                              M.read (| out |);
                              Value.Integer IntegerKind.Usize 1
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::slice::sort::stable::merge::MergeState",
                            "dst"
                          |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [
                              M.read (| left |);
                              M.rust_cast (UnOp.not (| M.read (| consume_left |) |))
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::slice::sort::stable::merge::MergeState",
                            "end"
                          |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "add",
                              []
                            |),
                            [ M.read (| right |); M.rust_cast (M.read (| consume_left |)) ]
                          |)
                        |) in
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.or (|
                                      BinOp.eq (|
                                        M.rust_cast
                                          (* MutToConstPointer *)
                                          (M.pointer_coercion
                                            (M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::slice::sort::stable::merge::MergeState",
                                                "dst"
                                              |)
                                            |))),
                                        M.read (| left_end |)
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.eq (|
                                          M.rust_cast
                                            (* MutToConstPointer *)
                                            (M.pointer_coercion
                                              (M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::slice::sort::stable::merge::MergeState",
                                                  "end"
                                                |)
                                              |))),
                                          M.read (| right_end |)
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |)))
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_merge_down :
            forall (T : Ty.t),
            M.IsAssociatedFunction (Self T) "merge_down" (merge_down T).
        End Impl_core_slice_sort_stable_merge_MergeState_T.
        
        Module Impl_core_ops_drop_Drop_for_core_slice_sort_stable_merge_MergeState_T.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "core::slice::sort::stable::merge::MergeState") [] [ T ].
          
          (*
              fn drop(&mut self) {
                  // SAFETY: The user of MergeState MUST ensure, that at any point this drop
                  // impl MAY run, for example when the user provided `is_less` panics, that
                  // copying the contiguous region between `start` and `end` to `dst` will
                  // leave the input slice `v` with each original element and all possible
                  // modifications observed.
                  unsafe {
                      let len = self.end.sub_ptr(self.start);
                      ptr::copy_nonoverlapping(self.start, self.dst, len);
                  }
              }
          *)
          Definition drop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  let~ len :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ T ],
                          "sub_ptr",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::stable::merge::MergeState",
                              "end"
                            |)
                          |);
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::sort::stable::merge::MergeState",
                                "start"
                              |)
                            |))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::sort::stable::merge::MergeState",
                                "start"
                              |)
                            |));
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::sort::stable::merge::MergeState",
                              "dst"
                            |)
                          |);
                          M.read (| len |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "core::ops::drop::Drop"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("drop", InstanceField.Method (drop T)) ].
        End Impl_core_ops_drop_Drop_for_core_slice_sort_stable_merge_MergeState_T.
      End merge.
    End stable.
  End sort.
End slice.
