val split_at_i (#b: _) (vb: buffer b) (i: nat{i < length vb}) (h: HS.mem)
    : GTot
    (frags:
      (let src_t = Mkdtuple4?._1 vb in
        Seq.seq src_t * Seq.lseq src_t (View?.n (get_view vb)) * Seq.seq src_t)
        { let prefix, es, suffix = frags in
          B.as_seq h (as_buffer vb) == (prefix `Seq.append` (es `Seq.append` suffix)) })
let split_at_i (#b: _) (vb:buffer b) (i:nat{i < length vb}) (h:HS.mem)
    : GTot (frags:
               (let src_t = Mkdtuple4?._1 vb in
                Seq.seq src_t *
                Seq.lseq src_t (View?.n (get_view vb)) *
                Seq.seq src_t){
               let prefix, es, suffix = frags in
               B.as_seq h (as_buffer vb) ==
               (prefix `Seq.append` (es `Seq.append` suffix))
            })
    = let open FStar.Mul in
      let s0 = B.as_seq h (as_buffer vb) in
      let v = get_view vb in
      let n = View?.n v in
      let start = i * n in
      view_indexing vb i;
      length_eq vb;
      let prefix, suffix = Seq.split s0 start in
      Seq.lemma_split s0 start;
      let es, tail = Seq.split suffix n in
      Seq.lemma_split suffix n;
      prefix, es, tail
val split_at_i (#b: _) (vb: buffer b) (i: nat{i < length vb}) (h: HS.mem)
    : GTot
    (frags:
      (let src_t = Mkdtuple4?._1 vb in
        Seq.seq src_t * Seq.lseq src_t (View?.n (get_view vb)) * Seq.seq src_t)
        { let prefix, es, suffix = frags in
          B.as_seq h (as_buffer vb) == (prefix `Seq.append` (es `Seq.append` suffix)) })
let split_at_i (#b: _) (vb: buffer b) (i: nat{i < length vb}) (h: HS.mem)
    : GTot
    (frags:
      (let src_t = Mkdtuple4?._1 vb in
        Seq.seq src_t * Seq.lseq src_t (View?.n (get_view vb)) * Seq.seq src_t)
        { let prefix, es, suffix = frags in
          B.as_seq h (as_buffer vb) == (prefix `Seq.append` (es `Seq.append` suffix)) }) =
let open FStar.Mul in
let s0 = B.as_seq h (as_buffer vb) in
let v = get_view vb in
let n = View?.n v in
let start = i * n in
view_indexing vb i;
length_eq vb;
let prefix, suffix = Seq.split s0 start in
Seq.lemma_split s0 start;
let es, tail = Seq.split suffix n in
Seq.lemma_split suffix n;
prefix, es, tail
LowStar.BufferView.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
LowStar.BufferView.fst
LowStar.BufferView.buffer Prims.nat Prims.b2t Prims.op_LessThan LowStar.BufferView.length FStar.Monotonic.HyperStack.mem FStar.Seq.Base.seq FStar.Pervasives.__proj__Mkdtuple4__item___1 LowStar.Monotonic.Buffer.srel LowStar.BufferView.buffer_view FStar.Pervasives.Native.Mktuple3 FStar.Seq.Properties.lseq LowStar.BufferView.__proj__View__item__n LowStar.BufferView.get_view Prims.unit FStar.Seq.Properties.lemma_split FStar.Pervasives.Native.tuple3 Prims.eq2 LowStar.Monotonic.Buffer.as_seq FStar.Pervasives.__proj__Mkdtuple4__item___2 FStar.Pervasives.__proj__Mkdtuple4__item___3 LowStar.BufferView.as_buffer FStar.Seq.Base.append FStar.Preorder.preorder FStar.Pervasives.Native.tuple2 FStar.Seq.Properties.split LowStar.BufferView.length_eq LowStar.BufferView.view_indexing Prims.int FStar.Mul.op_Star Prims.pos LowStar.BufferView.view
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module LowStar.BufferView

noeq
type buffer_view (a:Type0) (rrel rel:B.srel a) (b:Type u#b) : Type u#b =
  | BufferView: buf:B.mbuffer a rrel rel
              -> v:view a b{B.length buf % View?.n v == 0}
              -> buffer_view a rrel rel b

let mk_buffer_view #src #rrel #rel #dest b v  = (| src, rrel, rel, BufferView b v |)

let as_buffer #b v = BufferView?.buf (Mkdtuple4?._4 v)

let as_buffer_mk_buffer_view #_ #_ #_ #_ _ _ = ()

let get_view #b v = BufferView?.v (Mkdtuple4?._4 v)

let get_view_mk_buffer_view #_ #_ #_ #_ _ _ = ()

let length #b vb = B.length (as_buffer vb) / View?.n (get_view vb)

let length_eq #_ _ = ()

#reset-options "--max_fuel 0 --max_ifuel 1"
let view_indexing #b vb i
  = let n = View?.n (get_view vb) in
    length_eq vb;
    FStar.Math.Lemmas.distributivity_add_left (length vb) (-i) n;
    let open FStar.Mul in
    assert ((length vb + (-i)) * n = length vb * n + (-i) * n);
    assert (length vb > i);
    assert (length vb + (-i) > 0);
    assert (n <= (length vb + (-i)) * n)


let split_at_i (#b: _) (vb:buffer b) (i:nat{i < length vb}) (h:HS.mem)
    : GTot (frags:
               (let src_t = Mkdtuple4?._1 vb in
                Seq.seq src_t *
                Seq.lseq src_t (View?.n (get_view vb)) *
                Seq.seq src_t){
               let prefix, es, suffix = frags in
               B.as_seq h (as_buffer vb) ==
               (prefix `Seq.append` (es `Seq.append` suffix))
val split_at_i (#b: _) (vb: buffer b) (i: nat{i < length vb}) (h: HS.mem)
    : GTot
    (frags:
      (let src_t = Mkdtuple4?._1 vb in
        Seq.seq src_t * Seq.lseq src_t (View?.n (get_view vb)) * Seq.seq src_t)
        { let prefix, es, suffix = frags in
          B.as_seq h (as_buffer vb) == (prefix `Seq.append` (es `Seq.append` suffix)) })

    vb: LowStar.BufferView.buffer b ->
    i: Prims.nat{i < LowStar.BufferView.length vb} ->
    h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot
    (frags:
      (let src_t = Mkdtuple4?._1 vb in
        (FStar.Seq.Base.seq src_t *
        FStar.Seq.Properties.lseq src_t (View?.n (LowStar.BufferView.get_view vb))) *
        FStar.Seq.Base.seq src_t)
        { let _ = frags in
          (let FStar.Pervasives.Native.Mktuple3 #_ #_ #_ prefix es suffix = _ in
            LowStar.Monotonic.Buffer.as_seq h (LowStar.BufferView.as_buffer vb) ==
            FStar.Seq.Base.append prefix (FStar.Seq.Base.append es suffix))
          <:
          Type0 })