val blit: src:buffer U8.t -> idx_src:U32.t -> dst:buffer uint8 -> idx_dst:U32.t -> len:U32.t -> ST unit
  (requires  fun h -> 
    live h src /\ live h dst /\ 
    U32.v idx_src + U32.v len <= length src /\
    U32.v idx_dst + U32.v len <= length dst /\
    disjoint src dst)
  (ensures   fun h0 _ h1 -> 
    modifies (loc_buffer dst) h0 h1 /\
    live h1 dst /\
    (forall (i:nat). i < U32.v len ==>
      Seq.index (as_seq h1 dst) (U32.v idx_dst + i) ==
      Lib.RawIntTypes.u8_from_UInt8 (Seq.index (as_seq h0 src) (U32.v idx_src + i))) /\
    Seq.slice (as_seq h1 dst) 0 (U32.v idx_dst) ==
    Seq.slice (as_seq h0 dst) 0 (U32.v idx_dst) /\
    Seq.slice (as_seq h1 dst) (U32.v idx_dst + U32.v len) (length dst) ==
    Seq.slice (as_seq h0 dst) (U32.v idx_dst + U32.v len) (length dst))
let blit src idx_src dst idx_dst len =
  let h0 = get () in
  blit src idx_src dst idx_dst len;
  let h1 = get () in
  assert (forall (i:nat). i < U32.v len ==>
      Seq.index (as_seq h1 dst) (U32.v idx_dst + i) ==
      Seq.index (Seq.slice (as_seq h1 dst) (U32.v idx_dst) (U32.v idx_dst + U32.v len)) i)
val blit: src:buffer U8.t -> idx_src:U32.t -> dst:buffer uint8 -> idx_dst:U32.t -> len:U32.t -> ST unit
  (requires  fun h -> 
    live h src /\ live h dst /\ 
    U32.v idx_src + U32.v len <= length src /\
    U32.v idx_dst + U32.v len <= length dst /\
    disjoint src dst)
  (ensures   fun h0 _ h1 -> 
    modifies (loc_buffer dst) h0 h1 /\
    live h1 dst /\
    (forall (i:nat). i < U32.v len ==>
      Seq.index (as_seq h1 dst) (U32.v idx_dst + i) ==
      Lib.RawIntTypes.u8_from_UInt8 (Seq.index (as_seq h0 src) (U32.v idx_src + i))) /\
    Seq.slice (as_seq h1 dst) 0 (U32.v idx_dst) ==
    Seq.slice (as_seq h0 dst) 0 (U32.v idx_dst) /\
    Seq.slice (as_seq h1 dst) (U32.v idx_dst + U32.v len) (length dst) ==
    Seq.slice (as_seq h0 dst) (U32.v idx_dst + U32.v len) (length dst))
let blit src idx_src dst idx_dst len =
let h0 = get () in
blit src idx_src dst idx_dst len;
let h1 = get () in
assert (forall (i: nat).
      i < U32.v len ==>
      Seq.index (as_seq h1 dst) (U32.v idx_dst + i) ==
      Seq.index (Seq.slice (as_seq h1 dst) (U32.v idx_dst) (U32.v idx_dst + U32.v len)) i)
Lib.RawBuffer.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked C.Loops.fst.checked
Lib.RawBuffer.fst
LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Lib.IntTypes.uint8 Prims._assert Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan FStar.UInt32.v Prims.eq2 FStar.Seq.Base.index LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder Prims.op_Addition FStar.Seq.Base.slice Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.blit
module Lib.RawBuffer

friend Lib.IntTypes

open LowStar.Buffer

open FStar.HyperStack.ST

module U8 = FStar.UInt8
module U32 = FStar.UInt32

open Lib.IntTypes
val blit: src:buffer U8.t -> idx_src:U32.t -> dst:buffer uint8 -> idx_dst:U32.t -> len:U32.t -> ST unit
  (requires  fun h -> 
    live h src /\ live h dst /\ 
    U32.v idx_src + U32.v len <= length src /\
    U32.v idx_dst + U32.v len <= length dst /\
    disjoint src dst)
  (ensures   fun h0 _ h1 -> 
    modifies (loc_buffer dst) h0 h1 /\
    live h1 dst /\
    (forall (i:nat). i < U32.v len ==>
      Seq.index (as_seq h1 dst) (U32.v idx_dst + i) ==
      Lib.RawIntTypes.u8_from_UInt8 (Seq.index (as_seq h0 src) (U32.v idx_src + i))) /\
    Seq.slice (as_seq h1 dst) 0 (U32.v idx_dst) ==
    Seq.slice (as_seq h0 dst) 0 (U32.v idx_dst) /\
    Seq.slice (as_seq h1 dst) (U32.v idx_dst + U32.v len) (length dst) ==
    Seq.slice (as_seq h0 dst) (U32.v idx_dst + U32.v len) (length dst))

    src: LowStar.Buffer.buffer FStar.UInt8.t ->
    idx_src: FStar.UInt32.t ->
    dst: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    idx_dst: FStar.UInt32.t ->
    len: FStar.UInt32.t
  -> FStar.HyperStack.ST.ST Prims.unit