val lbytes_eq: #n:size_t -> b1:buffer uint8 -> b2:buffer uint8 -> Stack bool
  (requires fun h -> len b1 == n /\ len b2 == n /\ live h b1 /\ live h b2)
  (ensures  fun h0 r h1 -> 
    modifies loc_none h0 h1 /\ 
    (r <==> Seq.equal (as_seq h0 b1) (as_seq h0 b2)))
let lbytes_eq #n b1 b2 =
  let open LowStar.BufferOps in
  let h0 = get() in
  let inv h i b =
    modifies loc_none h0 h /\
    i <= U32.v n /\
    (if b then 
       0 < i /\ Seq.index (as_seq h0 b1) (i-1) <> Seq.index (as_seq h0 b2) (i-1)
     else
       forall (j:nat).j < i ==> Seq.index (as_seq h0 b1) j == Seq.index (as_seq h0 b2) j)
  in
  let _, b = C.Loops.interruptible_for 0ul n inv (fun i -> b1.(i) <> b2.(i)) in
  not b
val lbytes_eq: #n:size_t -> b1:buffer uint8 -> b2:buffer uint8 -> Stack bool
  (requires fun h -> len b1 == n /\ len b2 == n /\ live h b1 /\ live h b2)
  (ensures  fun h0 r h1 -> 
    modifies loc_none h0 h1 /\ 
    (r <==> Seq.equal (as_seq h0 b1) (as_seq h0 b2)))
let lbytes_eq #n b1 b2 =
let open LowStar.BufferOps in
let h0 = get () in
let inv h i b =
  modifies loc_none h0 h /\ i <= U32.v n /\
  (if b
    then 0 < i /\ Seq.index (as_seq h0 b1) (i - 1) <> Seq.index (as_seq h0 b2) (i - 1)
    else forall (j: nat). j < i ==> Seq.index (as_seq h0 b1) j == Seq.index (as_seq h0 b2) j)
in
let _, b = C.Loops.interruptible_for 0ul n inv (fun i -> b1.(i) <> b2.(i)) in
not b
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
Lib.IntTypes.size_t LowStar.Buffer.buffer Lib.IntTypes.uint8 FStar.UInt32.t Prims.bool Prims.op_Negation FStar.Pervasives.Native.tuple2 C.Loops.interruptible_for FStar.UInt32.__uint_to_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_LessThan Prims.op_disEquality Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC LowStar.BufferOps.op_Array_Access LowStar.Buffer.trivial_preorder FStar.Monotonic.HyperStack.mem Prims.int Prims.logical LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none FStar.Seq.Base.index LowStar.Monotonic.Buffer.as_seq Prims.op_Subtraction Prims.l_Forall Prims.nat Prims.l_imp Prims.eq2 FStar.HyperStack.ST.get
module Lib.RawBuffer

friend Lib.IntTypes

open LowStar.Buffer

open FStar.HyperStack.ST

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

open Lib.IntTypes

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 lbytes_eq: #n:size_t -> b1:buffer uint8 -> b2:buffer uint8 -> Stack bool
  (requires fun h -> len b1 == n /\ len b2 == n /\ live h b1 /\ live h b2)
  (ensures  fun h0 r h1 -> 
    modifies loc_none h0 h1 /\ 
    (r <==> Seq.equal (as_seq h0 b1) (as_seq h0 b2)))
b1: LowStar.Buffer.buffer Lib.IntTypes.uint8 -> b2: LowStar.Buffer.buffer Lib.IntTypes.uint8
  -> FStar.HyperStack.ST.Stack Prims.bool