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

Module slice.
  Module raw.
    (*
    pub const unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] {
        // SAFETY: the caller must uphold the safety contract for `from_raw_parts`.
        unsafe {
            ub_checks::assert_unsafe_precondition!(
                check_language_ub,
                "slice::from_raw_parts requires the pointer to be aligned and non-null, and the total size of the slice not to exceed `isize::MAX`",
                (
                    data: *mut () = data as *mut (),
                    size: usize = size_of::<T>(),
                    align: usize = align_of::<T>(),
                    len: usize = len,
                ) =>
                ub_checks::is_aligned_and_not_null(data, align)
                    && ub_checks::is_valid_allocation_size(size, len)
            );
            &*ptr::slice_from_raw_parts(data, len)
        }
    }
    *)
    Definition from_raw_parts (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ data; len ] =>
        ltac:(M.monadic
          (let data := M.alloc (| data |) in
          let len := M.alloc (| len |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::check_language_ub", [] |),
                              []
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::slice::raw::from_raw_parts.precondition_check",
                              []
                            |),
                            [
                              M.rust_cast (M.read (| data |));
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ T ] |),
                                []
                              |);
                              M.call_closure (|
                                M.get_function (| "core::mem::align_of", [ T ] |),
                                []
                              |);
                              M.read (| len |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::slice_from_raw_parts", [ T ] |),
                [ M.read (| data |); M.read (| len |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_raw_parts : M.IsFunction "core::slice::raw::from_raw_parts" from_raw_parts.
    
    (*
    pub const unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] {
        // SAFETY: the caller must uphold the safety contract for `from_raw_parts_mut`.
        unsafe {
            ub_checks::assert_unsafe_precondition!(
                check_language_ub,
                "slice::from_raw_parts_mut requires the pointer to be aligned and non-null, and the total size of the slice not to exceed `isize::MAX`",
                (
                    data: *mut () = data as *mut (),
                    size: usize = size_of::<T>(),
                    align: usize = align_of::<T>(),
                    len: usize = len,
                ) =>
                ub_checks::is_aligned_and_not_null(data, align)
                    && ub_checks::is_valid_allocation_size(size, len)
            );
            &mut *ptr::slice_from_raw_parts_mut(data, len)
        }
    }
    *)
    Definition from_raw_parts_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ data; len ] =>
        ltac:(M.monadic
          (let data := M.alloc (| data |) in
          let len := M.alloc (| len |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::check_language_ub", [] |),
                              []
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::slice::raw::from_raw_parts_mut.precondition_check",
                              []
                            |),
                            [
                              M.rust_cast (M.read (| data |));
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ T ] |),
                                []
                              |);
                              M.call_closure (|
                                M.get_function (| "core::mem::align_of", [ T ] |),
                                []
                              |);
                              M.read (| len |)
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                [ M.read (| data |); M.read (| len |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_raw_parts_mut :
      M.IsFunction "core::slice::raw::from_raw_parts_mut" from_raw_parts_mut.
    
    (*
    pub const fn from_ref<T>(s: &T) -> &[T] {
        array::from_ref(s)
    }
    *)
    Definition from_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.call_closure (|
            M.get_function (| "core::array::from_ref", [ T ] |),
            [ M.read (| s |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_ref : M.IsFunction "core::slice::raw::from_ref" from_ref.
    
    (*
    pub const fn from_mut<T>(s: &mut T) -> &mut [T] {
        array::from_mut(s)
    }
    *)
    Definition from_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.call_closure (|
            M.get_function (| "core::array::from_mut", [ T ] |),
            [ M.read (| s |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_mut : M.IsFunction "core::slice::raw::from_mut" from_mut.
    
    (*
    pub const unsafe fn from_ptr_range<'a, T>(range: Range<*const T>) -> &'a [T] {
        // SAFETY: the caller must uphold the safety contract for `from_ptr_range`.
        unsafe { from_raw_parts(range.start, range.end.sub_ptr(range.start)) }
    }
    *)
    Definition from_ptr_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ range ] =>
        ltac:(M.monadic
          (let range := M.alloc (| range |) in
          M.call_closure (|
            M.get_function (| "core::slice::raw::from_raw_parts", [ T ] |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (| range, "core::ops::range::Range", "start" |)
              |);
              M.call_closure (|
                M.get_associated_function (| Ty.apply (Ty.path "*const") [] [ T ], "sub_ptr", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      range,
                      "core::ops::range::Range",
                      "end"
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      range,
                      "core::ops::range::Range",
                      "start"
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_ptr_range : M.IsFunction "core::slice::raw::from_ptr_range" from_ptr_range.
    
    (*
    pub const unsafe fn from_mut_ptr_range<'a, T>(range: Range<*mut T>) -> &'a mut [T] {
        // SAFETY: the caller must uphold the safety contract for `from_mut_ptr_range`.
        unsafe { from_raw_parts_mut(range.start, range.end.sub_ptr(range.start)) }
    }
    *)
    Definition from_mut_ptr_range (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ range ] =>
        ltac:(M.monadic
          (let range := M.alloc (| range |) in
          M.call_closure (|
            M.get_function (| "core::slice::raw::from_raw_parts_mut", [ T ] |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (| range, "core::ops::range::Range", "start" |)
              |);
              M.call_closure (|
                M.get_associated_function (| Ty.apply (Ty.path "*mut") [] [ T ], "sub_ptr", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      range,
                      "core::ops::range::Range",
                      "end"
                    |)
                  |);
                  (* MutToConstPointer *)
                  M.pointer_coercion
                    (M.read (|
                      M.SubPointer.get_struct_record_field (|
                        range,
                        "core::ops::range::Range",
                        "start"
                      |)
                    |))
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_mut_ptr_range :
      M.IsFunction "core::slice::raw::from_mut_ptr_range" from_mut_ptr_range.
  End raw.
End slice.
