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

Module vec.
  Module in_place_collect.
    (*
    const fn in_place_collectible<DEST, SRC>(
        step_merge: Option<NonZero<usize>>,
        step_expand: Option<NonZero<usize>>,
    ) -> bool {
        // Require matching alignments because an alignment-changing realloc is inefficient on many
        // system allocators and better implementations would require the unstable Allocator trait.
        if const { SRC::IS_ZST || DEST::IS_ZST || mem::align_of::<SRC>() != mem::align_of::<DEST>() } {
            return false;
        }
    
        match (step_merge, step_expand) {
            (Some(step_merge), Some(step_expand)) => {
                // At least N merged source items -> at most M expanded destination items
                // e.g.
                // - 1 x [u8; 4] -> 4x u8, via flatten
                // - 4 x u8 -> 1x [u8; 4], via array_chunks
                mem::size_of::<SRC>() * step_merge.get() >= mem::size_of::<DEST>() * step_expand.get()
            }
            // Fall back to other from_iter impls if an overflow occurred in the step merge/expansion
            // tracking.
            _ => false,
        }
    }
    *)
    Definition in_place_collectible (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ DEST; SRC ], [ step_merge; step_expand ] =>
        ltac:(M.monadic
          (let step_merge := M.alloc (| step_merge |) in
          let step_expand := M.alloc (| step_expand |) 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 (|
                                "alloc::vec::in_place_collect::in_place_collectible_discriminant"
                              |)) 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.Bool false |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [ M.read (| step_merge |); M.read (| step_expand |) ] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        let step_merge := M.copy (| γ1_0 |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_1,
                            "core::option::Option::Some",
                            0
                          |) in
                        let step_expand := M.copy (| γ1_0 |) in
                        M.alloc (|
                          BinOp.ge (|
                            BinOp.Wrap.mul (|
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ SRC ] |),
                                []
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::num::nonzero::NonZero")
                                    []
                                    [ Ty.path "usize" ],
                                  "get",
                                  []
                                |),
                                [ M.read (| step_merge |) ]
                              |)
                            |),
                            BinOp.Wrap.mul (|
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ DEST ] |),
                                []
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::num::nonzero::NonZero")
                                    []
                                    [ Ty.path "usize" ],
                                  "get",
                                  []
                                |),
                                [ M.read (| step_expand |) ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_in_place_collectible :
      M.IsFunction "alloc::vec::in_place_collect::in_place_collectible" in_place_collectible.
    
    (*
    const fn needs_realloc<SRC, DEST>(src_cap: usize, dst_cap: usize) -> bool {
        if const { mem::align_of::<SRC>() != mem::align_of::<DEST>() } {
            // FIXME(const-hack): use unreachable! once that works in const
            panic!("in_place_collectible() prevents this");
        }
    
        // If src type size is an integer multiple of the destination type size then
        // the caller will have calculated a `dst_cap` that is an integer multiple of
        // `src_cap` without remainder.
        if const {
            let src_sz = mem::size_of::<SRC>();
            let dest_sz = mem::size_of::<DEST>();
            dest_sz != 0 && src_sz % dest_sz == 0
        } {
            return false;
        }
    
        // type layouts don't guarantee a fit, so do a runtime check to see if
        // the allocations happen to match
        src_cap > 0 && src_cap * mem::size_of::<SRC>() != dst_cap * mem::size_of::<DEST>()
    }
    *)
    Definition needs_realloc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ SRC; DEST ], [ src_cap; dst_cap ] =>
        ltac:(M.monadic
          (let src_cap := M.alloc (| src_cap |) in
          let dst_cap := M.alloc (| dst_cap |) 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 (|
                                "alloc::vec::in_place_collect::needs_realloc_discriminant"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.call_closure (|
                                M.get_function (| "core::panicking::panic_fmt", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::Arguments",
                                      "new_const",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        Value.Array
                                          [
                                            M.read (|
                                              Value.String "in_place_collectible() prevents this"
                                            |)
                                          ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.get_constant (|
                                "alloc::vec::in_place_collect::needs_realloc_discriminant"
                              |)) 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.Bool false |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  LogicalOp.and (|
                    BinOp.gt (| M.read (| src_cap |), Value.Integer IntegerKind.Usize 0 |),
                    ltac:(M.monadic
                      (BinOp.ne (|
                        BinOp.Wrap.mul (|
                          M.read (| src_cap |),
                          M.call_closure (|
                            M.get_function (| "core::mem::size_of", [ SRC ] |),
                            []
                          |)
                        |),
                        BinOp.Wrap.mul (|
                          M.read (| dst_cap |),
                          M.call_closure (|
                            M.get_function (| "core::mem::size_of", [ DEST ] |),
                            []
                          |)
                        |)
                      |)))
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_needs_realloc :
      M.IsFunction "alloc::vec::in_place_collect::needs_realloc" needs_realloc.
    
    (* Trait *)
    (* Empty module 'InPlaceCollect' *)
    
    Module Impl_alloc_vec_in_place_collect_InPlaceCollect_where_core_iter_adapters_SourceIter_T_where_core_iter_traits_marker_InPlaceIterable_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*     type Src = <<T as SourceIter>::Source as AsVecIntoIter>::Item; *)
      Definition _Src (T : Ty.t) : Ty.t := Ty.associated.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::in_place_collect::InPlaceCollect"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Src", InstanceField.Ty (_Src T)) ].
    End Impl_alloc_vec_in_place_collect_InPlaceCollect_where_core_iter_adapters_SourceIter_T_where_core_iter_traits_marker_InPlaceIterable_T_for_T.
    
    Module Impl_alloc_vec_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_where_alloc_vec_in_place_collect_InPlaceCollect_I_where_alloc_vec_in_place_collect_AsVecIntoIter_associated_type_T_I_for_alloc_vec_Vec_T_alloc_alloc_Global.
      Definition Self (T I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ].
      
      (*
          default fn from_iter(iterator: I) -> Self {
              // Select the implementation in const eval to avoid codegen of the dead branch to improve compile times.
              let fun: fn(I) -> Vec<T> = const {
                  // See "Layout constraints" section in the module documentation. We use const conditions here
                  // since these conditions currently cannot be expressed as trait bounds
                  if in_place_collectible::<T, I::Src>(I::MERGE_BY, I::EXPAND_BY) {
                      from_iter_in_place
                  } else {
                      // fallback
                      SpecFromIterNested::<T, I>::from_iter
                  }
              };
      
              fun(iterator)
          }
      *)
      Definition from_iter (T I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T I in
        match ε, τ, α with
        | [], [], [ iterator ] =>
          ltac:(M.monadic
            (let iterator := M.alloc (| iterator |) in
            M.read (|
              let~ fun_ :=
                M.copy (|
                  M.get_constant (| "alloc::vec::in_place_collect::from_iter_discriminant" |)
                |) in
              M.alloc (| M.call_closure (| M.read (| fun_ |), [ M.read (| iterator |) ] |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "alloc::vec::spec_from_iter::SpecFromIter"
          (Self T I)
          (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
          (* Instance *) [ ("from_iter", InstanceField.Method (from_iter T I)) ].
    End Impl_alloc_vec_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_where_alloc_vec_in_place_collect_InPlaceCollect_I_where_alloc_vec_in_place_collect_AsVecIntoIter_associated_type_T_I_for_alloc_vec_Vec_T_alloc_alloc_Global.
    
    (*
    fn from_iter_in_place<I, T>(mut iterator: I) -> Vec<T>
    where
        I: Iterator<Item = T> + InPlaceCollect,
        <I as SourceIter>::Source: AsVecIntoIter,
    {
        let (src_buf, src_ptr, src_cap, mut dst_buf, dst_end, dst_cap) = unsafe {
            let inner = iterator.as_inner().as_into_iter();
            (
                inner.buf,
                inner.ptr,
                inner.cap,
                inner.buf.cast::<T>(),
                inner.end as *const T,
                // SAFETY: the multiplication can not overflow, since `inner.cap * size_of::<I::SRC>()` is the size of the allocation.
                inner.cap.unchecked_mul(mem::size_of::<I::Src>()) / mem::size_of::<T>(),
            )
        };
    
        // SAFETY: `dst_buf` and `dst_end` are the start and end of the buffer.
        let len = unsafe {
            SpecInPlaceCollect::collect_in_place(&mut iterator, dst_buf.as_ptr() as *mut T, dst_end)
        };
    
        let src = unsafe { iterator.as_inner().as_into_iter() };
        // check if SourceIter contract was upheld
        // caveat: if they weren't we might not even make it to this point
        debug_assert_eq!(src_buf, src.buf);
        // check InPlaceIterable contract. This is only possible if the iterator advanced the
        // source pointer at all. If it uses unchecked access via TrustedRandomAccess
        // then the source pointer will stay in its initial position and we can't use it as reference
        if src.ptr != src_ptr {
            debug_assert!(
                unsafe { dst_buf.add(len).cast() } <= src.ptr,
                "InPlaceIterable contract violation, write pointer advanced beyond read pointer"
            );
        }
    
        // The ownership of the source allocation and the new `T` values is temporarily moved into `dst_guard`.
        // This is safe because
        // * `forget_allocation_drop_remaining` immediately forgets the allocation
        // before any panic can occur in order to avoid any double free, and then proceeds to drop
        // any remaining values at the tail of the source.
        // * the shrink either panics without invalidating the allocation, aborts or
        //   succeeds. In the last case we disarm the guard.
        //
        // Note: This access to the source wouldn't be allowed by the TrustedRandomIteratorNoCoerce
        // contract (used by SpecInPlaceCollect below). But see the "O(1) collect" section in the
        // module documentation why this is ok anyway.
        let dst_guard =
            InPlaceDstDataSrcBufDrop { ptr: dst_buf, len, src_cap, src: PhantomData::<I::Src> };
        src.forget_allocation_drop_remaining();
    
        // Adjust the allocation if the source had a capacity in bytes that wasn't a multiple
        // of the destination type size.
        // Since the discrepancy should generally be small this should only result in some
        // bookkeeping updates and no memmove.
        if needs_realloc::<I::Src, T>(src_cap, dst_cap) {
            let alloc = Global;
            debug_assert_ne!(src_cap, 0);
            debug_assert_ne!(dst_cap, 0);
            unsafe {
                // The old allocation exists, therefore it must have a valid layout.
                let src_align = mem::align_of::<I::Src>();
                let src_size = mem::size_of::<I::Src>().unchecked_mul(src_cap);
                let old_layout = Layout::from_size_align_unchecked(src_size, src_align);
    
                // The allocation must be equal or smaller for in-place iteration to be possible
                // therefore the new layout must be ≤ the old one and therefore valid.
                let dst_align = mem::align_of::<T>();
                let dst_size = mem::size_of::<T>().unchecked_mul(dst_cap);
                let new_layout = Layout::from_size_align_unchecked(dst_size, dst_align);
    
                let result = alloc.shrink(dst_buf.cast(), old_layout, new_layout);
                let Ok(reallocated) = result else { handle_alloc_error(new_layout) };
                dst_buf = reallocated.cast::<T>();
            }
        } else {
            debug_assert_eq!(src_cap * mem::size_of::<I::Src>(), dst_cap * mem::size_of::<T>());
        }
    
        mem::forget(dst_guard);
    
        let vec = unsafe { Vec::from_parts(dst_buf, len, dst_cap) };
    
        vec
    }
    *)
    Definition from_iter_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I; T ], [ iterator ] =>
        ltac:(M.monadic
          (let iterator := M.alloc (| iterator |) in
          M.read (|
            M.match_operator (|
              let~ inner :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "alloc::vec::in_place_collect::AsVecIntoIter",
                      Ty.associated,
                      [],
                      "as_into_iter",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::adapters::SourceIter",
                          I,
                          [],
                          "as_inner",
                          []
                        |),
                        [ iterator ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| inner |),
                        "alloc::vec::into_iter::IntoIter",
                        "buf"
                      |)
                    |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| inner |),
                        "alloc::vec::into_iter::IntoIter",
                        "ptr"
                      |)
                    |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| inner |),
                        "alloc::vec::into_iter::IntoIter",
                        "cap"
                      |)
                    |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.associated ],
                        "cast",
                        [ T ]
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| inner |),
                            "alloc::vec::into_iter::IntoIter",
                            "buf"
                          |)
                        |)
                      ]
                    |);
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| inner |),
                          "alloc::vec::into_iter::IntoIter",
                          "end"
                        |)
                      |));
                    BinOp.Wrap.div (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "usize", "unchecked_mul", [] |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| inner |),
                              "alloc::vec::into_iter::IntoIter",
                              "cap"
                            |)
                          |);
                          M.call_closure (|
                            M.get_function (| "core::mem::size_of", [ Ty.associated ] |),
                            []
                          |)
                        ]
                      |),
                      M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
                    |)
                  ]
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                    let γ0_3 := M.SubPointer.get_tuple_field (| γ, 3 |) in
                    let γ0_4 := M.SubPointer.get_tuple_field (| γ, 4 |) in
                    let γ0_5 := M.SubPointer.get_tuple_field (| γ, 5 |) in
                    let src_buf := M.copy (| γ0_0 |) in
                    let src_ptr := M.copy (| γ0_1 |) in
                    let src_cap := M.copy (| γ0_2 |) in
                    let dst_buf := M.copy (| γ0_3 |) in
                    let dst_end := M.copy (| γ0_4 |) in
                    let dst_cap := M.copy (| γ0_5 |) in
                    let~ len :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "alloc::vec::in_place_collect::SpecInPlaceCollect",
                            I,
                            [ T; I ],
                            "collect_in_place",
                            []
                          |),
                          [
                            iterator;
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                  "as_ptr",
                                  []
                                |),
                                [ M.read (| dst_buf |) ]
                              |));
                            M.read (| dst_end |)
                          ]
                        |)
                      |) in
                    let~ src :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "alloc::vec::in_place_collect::AsVecIntoIter",
                            Ty.associated,
                            [],
                            "as_into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::adapters::SourceIter",
                                I,
                                [],
                                "as_inner",
                                []
                              |),
                              [ iterator ]
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use (M.alloc (| Value.Bool true |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    Value.Tuple
                                      [
                                        src_buf;
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| src |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "buf"
                                        |)
                                      ]
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                        let left_val := M.copy (| γ0_0 |) in
                                        let right_val := M.copy (| γ0_1 |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::cmp::PartialEq",
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::ptr::non_null::NonNull")
                                                              []
                                                              [ Ty.associated ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ptr::non_null::NonNull")
                                                                []
                                                                [ Ty.associated ]
                                                            ],
                                                            "eq",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| left_val |);
                                                            M.read (| right_val |)
                                                          ]
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.read (|
                                                      let~ kind :=
                                                        M.alloc (|
                                                          Value.StructTuple
                                                            "core::panicking::AssertKind::Eq"
                                                            []
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::panicking::assert_failed",
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ptr::non_null::NonNull")
                                                                []
                                                                [ Ty.associated ];
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ptr::non_null::NonNull")
                                                                []
                                                                [ Ty.associated ]
                                                            ]
                                                          |),
                                                          [
                                                            M.read (| kind |);
                                                            M.read (| left_val |);
                                                            M.read (| right_val |);
                                                            Value.StructTuple
                                                              "core::option::Option::None"
                                                              []
                                                          ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "core::ptr::non_null::NonNull")
                                          []
                                          [ Ty.associated ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::ptr::non_null::NonNull")
                                            []
                                            [ Ty.associated ]
                                        ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| src |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "ptr"
                                        |);
                                        src_ptr
                                      ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::cmp::PartialOrd",
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ptr::non_null::NonNull")
                                                                []
                                                                [ Ty.associated ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "core::ptr::non_null::NonNull")
                                                                  []
                                                                  [ Ty.associated ]
                                                              ],
                                                              "le",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::ptr::non_null::NonNull")
                                                                      []
                                                                      [ T ],
                                                                    "cast",
                                                                    [ Ty.associated ]
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "core::ptr::non_null::NonNull")
                                                                          []
                                                                          [ T ],
                                                                        "add",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (| dst_buf |);
                                                                        M.read (| len |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |);
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| src |),
                                                                "alloc::vec::into_iter::IntoIter",
                                                                "ptr"
                                                              |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::panicking::panic_fmt",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Arguments",
                                                              "new_const",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.read (|
                                                                      Value.String
                                                                        "InPlaceIterable contract violation, write pointer advanced beyond read pointer"
                                                                    |)
                                                                  ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ dst_guard :=
                      M.alloc (|
                        Value.StructRecord
                          "alloc::vec::in_place_drop::InPlaceDstDataSrcBufDrop"
                          [
                            ("ptr", M.read (| dst_buf |));
                            ("len", M.read (| len |));
                            ("src_cap", M.read (| src_cap |));
                            ("src", Value.StructTuple "core::marker::PhantomData" [])
                          ]
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::into_iter::IntoIter")
                              []
                              [ Ty.associated; Ty.path "alloc::alloc::Global" ],
                            "forget_allocation_drop_remaining",
                            []
                          |),
                          [ M.read (| src |) ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "alloc::vec::in_place_collect::needs_realloc",
                                        [ Ty.associated; T ]
                                      |),
                                      [ M.read (| src_cap |); M.read (| dst_cap |) ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ alloc :=
                                M.alloc (| Value.StructTuple "alloc::alloc::Global" [] |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              Value.Tuple
                                                [
                                                  src_cap;
                                                  M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                ]
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                  let γ0_1 :=
                                                    M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                  let left_val := M.copy (| γ0_0 |) in
                                                  let right_val := M.copy (| γ0_1 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.eq (|
                                                                  M.read (|
                                                                    M.read (| left_val |)
                                                                  |),
                                                                  M.read (|
                                                                    M.read (| right_val |)
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                let~ kind :=
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::panicking::AssertKind::Ne"
                                                                      []
                                                                  |) in
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::assert_failed",
                                                                      [
                                                                        Ty.path "usize";
                                                                        Ty.path "usize"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| kind |);
                                                                      M.read (| left_val |);
                                                                      M.read (| right_val |);
                                                                      Value.StructTuple
                                                                        "core::option::Option::None"
                                                                        []
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              Value.Tuple
                                                [
                                                  dst_cap;
                                                  M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                ]
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                  let γ0_1 :=
                                                    M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                  let left_val := M.copy (| γ0_0 |) in
                                                  let right_val := M.copy (| γ0_1 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.eq (|
                                                                  M.read (|
                                                                    M.read (| left_val |)
                                                                  |),
                                                                  M.read (|
                                                                    M.read (| right_val |)
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                let~ kind :=
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::panicking::AssertKind::Ne"
                                                                      []
                                                                  |) in
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::assert_failed",
                                                                      [
                                                                        Ty.path "usize";
                                                                        Ty.path "usize"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| kind |);
                                                                      M.read (| left_val |);
                                                                      M.read (| right_val |);
                                                                      Value.StructTuple
                                                                        "core::option::Option::None"
                                                                        []
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ src_align :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::mem::align_of", [ Ty.associated ] |),
                                    []
                                  |)
                                |) in
                              let~ src_size :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "usize",
                                      "unchecked_mul",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::mem::size_of",
                                          [ Ty.associated ]
                                        |),
                                        []
                                      |);
                                      M.read (| src_cap |)
                                    ]
                                  |)
                                |) in
                              let~ old_layout :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "from_size_align_unchecked",
                                      []
                                    |),
                                    [ M.read (| src_size |); M.read (| src_align |) ]
                                  |)
                                |) in
                              let~ dst_align :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::mem::align_of", [ T ] |),
                                    []
                                  |)
                                |) in
                              let~ dst_size :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "usize",
                                      "unchecked_mul",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_function (| "core::mem::size_of", [ T ] |),
                                        []
                                      |);
                                      M.read (| dst_cap |)
                                    ]
                                  |)
                                |) in
                              let~ new_layout :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "from_size_align_unchecked",
                                      []
                                    |),
                                    [ M.read (| dst_size |); M.read (| dst_align |) ]
                                  |)
                                |) in
                              let~ result :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::alloc::Allocator",
                                      Ty.path "alloc::alloc::Global",
                                      [],
                                      "shrink",
                                      []
                                    |),
                                    [
                                      alloc;
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::ptr::non_null::NonNull")
                                            []
                                            [ T ],
                                          "cast",
                                          [ Ty.path "u8" ]
                                        |),
                                        [ M.read (| dst_buf |) ]
                                      |);
                                      M.read (| old_layout |);
                                      M.read (| new_layout |)
                                    ]
                                  |)
                                |) in
                              M.match_operator (|
                                result,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::result::Result::Ok",
                                          0
                                        |) in
                                      let reallocated := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.write (|
                                          dst_buf,
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::ptr::non_null::NonNull")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                              "cast",
                                              [ T ]
                                            |),
                                            [ M.read (| reallocated |) ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              Value.Tuple
                                                [
                                                  M.alloc (|
                                                    BinOp.Wrap.mul (|
                                                      M.read (| src_cap |),
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::mem::size_of",
                                                          [ Ty.associated ]
                                                        |),
                                                        []
                                                      |)
                                                    |)
                                                  |);
                                                  M.alloc (|
                                                    BinOp.Wrap.mul (|
                                                      M.read (| dst_cap |),
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::mem::size_of",
                                                          [ T ]
                                                        |),
                                                        []
                                                      |)
                                                    |)
                                                  |)
                                                ]
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                  let γ0_1 :=
                                                    M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                  let left_val := M.copy (| γ0_0 |) in
                                                  let right_val := M.copy (| γ0_1 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                UnOp.not (|
                                                                  BinOp.eq (|
                                                                    M.read (|
                                                                      M.read (| left_val |)
                                                                    |),
                                                                    M.read (|
                                                                      M.read (| right_val |)
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (|
                                                                let~ kind :=
                                                                  M.alloc (|
                                                                    Value.StructTuple
                                                                      "core::panicking::AssertKind::Eq"
                                                                      []
                                                                  |) in
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::panicking::assert_failed",
                                                                      [
                                                                        Ty.path "usize";
                                                                        Ty.path "usize"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (| kind |);
                                                                      M.read (| left_val |);
                                                                      M.read (| right_val |);
                                                                      Value.StructTuple
                                                                        "core::option::Option::None"
                                                                        []
                                                                    ]
                                                                  |)
                                                                |)
                                                              |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::mem::forget",
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::in_place_drop::InPlaceDstDataSrcBufDrop")
                                []
                                [ Ty.associated; T ]
                            ]
                          |),
                          [ M.read (| dst_guard |) ]
                        |)
                      |) in
                    let~ vec :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ T; Ty.path "alloc::alloc::Global" ],
                            "from_parts",
                            []
                          |),
                          [ M.read (| dst_buf |); M.read (| len |); M.read (| dst_cap |) ]
                        |)
                      |) in
                    vec))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_iter_in_place :
      M.IsFunction "alloc::vec::in_place_collect::from_iter_in_place" from_iter_in_place.
    
    (*
    fn write_in_place_with_drop<T>(
        src_end: *const T,
    ) -> impl FnMut(InPlaceDrop<T>, T) -> Result<InPlaceDrop<T>, !> {
        move |mut sink, item| {
            unsafe {
                // the InPlaceIterable contract cannot be verified precisely here since
                // try_fold has an exclusive reference to the source pointer
                // all we can do is check if it's still in range
                debug_assert!(sink.dst as *const _ <= src_end, "InPlaceIterable contract violation");
                ptr::write(sink.dst, item);
                // Since this executes user code which can panic we have to bump the pointer
                // after each step.
                sink.dst = sink.dst.add(1);
            }
            Ok(sink)
        }
    }
    *)
    Definition write_in_place_with_drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ src_end ] =>
        ltac:(M.monadic
          (let src_end := M.alloc (| src_end |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0; α1 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let sink := M.copy (| γ |) in
                            M.match_operator (|
                              M.alloc (| α1 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let item := M.copy (| γ |) in
                                    M.read (|
                                      let~ _ :=
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  UnOp.not (|
                                                                    BinOp.le (|
                                                                      M.rust_cast
                                                                        (* MutToConstPointer *)
                                                                        (M.pointer_coercion
                                                                          (M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              sink,
                                                                              "alloc::vec::in_place_drop::InPlaceDrop",
                                                                              "dst"
                                                                            |)
                                                                          |))),
                                                                      M.read (| src_end |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::panicking::panic_fmt",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::fmt::Arguments",
                                                                        "new_const",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.alloc (|
                                                                          Value.Array
                                                                            [
                                                                              M.read (|
                                                                                Value.String
                                                                                  "InPlaceIterable contract violation"
                                                                              |)
                                                                            ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (| "core::ptr::write", [ T ] |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    sink,
                                                    "alloc::vec::in_place_drop::InPlaceDrop",
                                                    "dst"
                                                  |)
                                                |);
                                                M.read (| item |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              sink,
                                              "alloc::vec::in_place_drop::InPlaceDrop",
                                              "dst"
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    sink,
                                                    "alloc::vec::in_place_drop::InPlaceDrop",
                                                    "dst"
                                                  |)
                                                |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |) in
                                      M.alloc (|
                                        Value.StructTuple
                                          "core::result::Result::Ok"
                                          [ M.read (| sink |) ]
                                      |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_write_in_place_with_drop :
      M.IsFunction
        "alloc::vec::in_place_collect::write_in_place_with_drop"
        write_in_place_with_drop.
    
    Module write_in_place_with_drop.
      (* Error OpaqueTy *)
    End write_in_place_with_drop.
    
    (* Trait *)
    (* Empty module 'SpecInPlaceCollect' *)
    
    Module Impl_alloc_vec_in_place_collect_SpecInPlaceCollect_where_core_iter_traits_iterator_Iterator_I_T_I_for_I.
      Definition Self (T I : Ty.t) : Ty.t := I.
      
      (*
          default unsafe fn collect_in_place(&mut self, dst_buf: *mut T, end: *const T) -> usize {
              // use try-fold since
              // - it vectorizes better for some iterator adapters
              // - unlike most internal iteration methods, it only takes a &mut self
              // - it lets us thread the write pointer through its innards and get it back in the end
              let sink = InPlaceDrop { inner: dst_buf, dst: dst_buf };
              let sink =
                  self.try_fold::<_, _, Result<_, !>>(sink, write_in_place_with_drop(end)).into_ok();
              // iteration succeeded, don't drop head
              unsafe { ManuallyDrop::new(sink).dst.sub_ptr(dst_buf) }
          }
      *)
      Definition collect_in_place
          (T I : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T I in
        match ε, τ, α with
        | [], [], [ self; dst_buf; end_ ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dst_buf := M.alloc (| dst_buf |) in
            let end_ := M.alloc (| end_ |) in
            M.read (|
              let~ sink :=
                M.alloc (|
                  Value.StructRecord
                    "alloc::vec::in_place_drop::InPlaceDrop"
                    [ ("inner", M.read (| dst_buf |)); ("dst", M.read (| dst_buf |)) ]
                |) in
              let~ sink :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.apply (Ty.path "alloc::vec::in_place_drop::InPlaceDrop") [] [ T ];
                          Ty.path "never"
                        ],
                      "into_ok",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          I,
                          [],
                          "try_fold",
                          [
                            Ty.apply (Ty.path "alloc::vec::in_place_drop::InPlaceDrop") [] [ T ];
                            Ty.associated;
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::in_place_drop::InPlaceDrop")
                                  []
                                  [ T ];
                                Ty.path "never"
                              ]
                          ]
                        |),
                        [
                          M.read (| self |);
                          M.read (| sink |);
                          M.call_closure (|
                            M.get_function (|
                              "alloc::vec::in_place_collect::write_in_place_with_drop",
                              [ T ]
                            |),
                            [ M.read (| end_ |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              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.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "core::mem::manually_drop::ManuallyDrop")
                              []
                              [ Ty.apply (Ty.path "alloc::vec::in_place_drop::InPlaceDrop") [] [ T ]
                              ],
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::in_place_drop::InPlaceDrop")
                                        []
                                        [ T ]
                                    ],
                                  "new",
                                  []
                                |),
                                [ M.read (| sink |) ]
                              |)
                            |)
                          ]
                        |),
                        "alloc::vec::in_place_drop::InPlaceDrop",
                        "dst"
                      |)
                    |);
                    (* MutToConstPointer *) M.pointer_coercion (M.read (| dst_buf |))
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "alloc::vec::in_place_collect::SpecInPlaceCollect"
          (Self T I)
          (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
          (* Instance *) [ ("collect_in_place", InstanceField.Method (collect_in_place T I)) ].
    End Impl_alloc_vec_in_place_collect_SpecInPlaceCollect_where_core_iter_traits_iterator_Iterator_I_T_I_for_I.
    
    Module Impl_alloc_vec_in_place_collect_SpecInPlaceCollect_where_core_iter_traits_iterator_Iterator_I_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_T_I_for_I.
      Definition Self (T I : Ty.t) : Ty.t := I.
      
      (*
          unsafe fn collect_in_place(&mut self, dst_buf: *mut T, end: *const T) -> usize {
              let len = self.size();
              let mut drop_guard = InPlaceDrop { inner: dst_buf, dst: dst_buf };
              for i in 0..len {
                  // Safety: InplaceIterable contract guarantees that for every element we read
                  // one slot in the underlying storage will have been freed up and we can immediately
                  // write back the result.
                  unsafe {
                      let dst = dst_buf.add(i);
                      debug_assert!(dst as *const _ <= end, "InPlaceIterable contract violation");
                      ptr::write(dst, self.__iterator_get_unchecked(i));
                      // Since this executes user code which can panic we have to bump the pointer
                      // after each step.
                      drop_guard.dst = dst.add(1);
                  }
              }
              mem::forget(drop_guard);
              len
          }
      *)
      Definition collect_in_place
          (T I : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T I in
        match ε, τ, α with
        | [], [], [ self; dst_buf; end_ ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dst_buf := M.alloc (| dst_buf |) in
            let end_ := M.alloc (| end_ |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::adapters::zip::TrustedRandomAccessNoCoerce",
                      I,
                      [],
                      "size",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ drop_guard :=
                M.alloc (|
                  Value.StructRecord
                    "alloc::vec::in_place_drop::InPlaceDrop"
                    [ ("inner", M.read (| dst_buf |)); ("dst", M.read (| dst_buf |)) ]
                |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", Value.Integer IntegerKind.Usize 0);
                              ("end_", M.read (| len |))
                            ]
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let i := M.copy (| γ0_0 |) in
                                        let~ dst :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [ M.read (| dst_buf |); M.read (| i |) ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  UnOp.not (|
                                                                    BinOp.le (|
                                                                      M.rust_cast
                                                                        (* MutToConstPointer *)
                                                                        (M.pointer_coercion
                                                                          (M.read (| dst |))),
                                                                      M.read (| end_ |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::panicking::panic_fmt",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::fmt::Arguments",
                                                                        "new_const",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.alloc (|
                                                                          Value.Array
                                                                            [
                                                                              M.read (|
                                                                                Value.String
                                                                                  "InPlaceIterable contract violation"
                                                                              |)
                                                                            ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (| "core::ptr::write", [ T ] |),
                                              [
                                                M.read (| dst |);
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    I,
                                                    [],
                                                    "__iterator_get_unchecked",
                                                    []
                                                  |),
                                                  [ M.read (| self |); M.read (| i |) ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              drop_guard,
                                              "alloc::vec::in_place_drop::InPlaceDrop",
                                              "dst"
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [ M.read (| dst |); Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "alloc::vec::in_place_drop::InPlaceDrop") [] [ T ] ]
                    |),
                    [ M.read (| drop_guard |) ]
                  |)
                |) in
              len
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "alloc::vec::in_place_collect::SpecInPlaceCollect"
          (Self T I)
          (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
          (* Instance *) [ ("collect_in_place", InstanceField.Method (collect_in_place T I)) ].
    End Impl_alloc_vec_in_place_collect_SpecInPlaceCollect_where_core_iter_traits_iterator_Iterator_I_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_T_I_for_I.
    
    (* Trait *)
    (* Empty module 'AsVecIntoIter' *)
  End in_place_collect.
End vec.
