let slice_ b (s:nat) (e:nat{s <= e /\ e <= length b}) = slice b (U32.uint_to_t s) (U32.uint_to_t e)
let slice_ b (s: nat) (e: nat{s <= e /\ e <= length b}) =
slice b (U32.uint_to_t s) (U32.uint_to_t e)
FStar.Bytes.fsti.checked
prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Char.fsti.checked
FStar.Bytes.fsti
FStar.Bytes.bytes Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Bytes.length FStar.Bytes.slice FStar.UInt32.uint_to_t Prims.eq2 FStar.Seq.Base.seq FStar.Bytes.byte FStar.Bytes.reveal FStar.Seq.Base.slice FStar.UInt32.v
(*
   Copyright 2008-2017 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.
*)
(*
A standard library for manipulation of value bytes.

This model is realized by Bytes.bytes in OCaml and by
struct {uintX_t size; char *bytes} (or similar) in C.

This file is essentially a specialized version of FStar.Seq,
with lemmas and refinements taylored for typical operations on
bytes, and with support for machine integers and C-extractible versions
(which Seq does not provide.)

@summary Value bytes standard library
*)
module FStar.Bytes

module S = FStar.Seq
module U = FStar.UInt
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Str = FStar.String
module Chr = FStar.Char

unfold let u8 = U8.t
unfold let u16 = U16.t
unfold let u32 = U32.t

(** Realized by uint8_t in C and int in OCaml (char does not have necessary operators...) *)
unfold type byte = u8

(** Realized in C by a pair of a length field and uint8_t* in C
    Realized in OCaml by a string *)
val bytes : t:Type0{hasEq t}
val len : bytes -> u32

unfold let length b = FStar.UInt32.v (len b)

(**  representation for specs that need lemmas not defined here. *)
val reveal:
    bytes
  -> GTot (S.seq byte)

val length_reveal:
    x:bytes
  -> Lemma (ensures (S.length (reveal x) = length x))
          [SMTPatOr [[SMTPat (S.length (reveal x))];
                     [SMTPat (len x)]]]

val hide:
    s:S.seq byte{S.length s < pow2 32}
  -> GTot bytes

val hide_reveal:
    x:bytes
  -> Lemma (ensures (hide (reveal x) = x))
          [SMTPat (reveal x)]

val reveal_hide:
    x:S.seq byte{S.length x < pow2 32}
  -> Lemma (ensures (reveal (hide x) == x))
          [SMTPat (hide x)]

type lbytes (l:nat) = b:bytes{length b = l}
type kbytes (k:nat) = b:bytes{length b < pow2 k}

let lbytes32 (l:UInt32.t) = b:bytes{len b = l}

val empty_bytes : lbytes 0
val empty_unique:
    b:bytes
  -> Lemma (length b = 0 ==> b = empty_bytes)
    [SMTPat (len b)]

(** If you statically know the length, it is OK to read at arbitrary indexes *)
val get:
    b:bytes
  -> pos:u32{U32.v pos < length b}
  -> Pure byte
    (requires True)
    (ensures (fun y -> y == S.index (reveal b) (U32.v pos)))

unfold let op_String_Access = get

unfold let index (b:bytes) (i:nat{i < length b}) = get b (U32.uint_to_t i)

let equal b1 b2 =
  length b1 = length b2 /\
  (forall (i:u32{U32.v i < length b1}).{:pattern (b1.[i]); (b2.[i])} b1.[i] == b2.[i])

val extensionality:
    b1:bytes
  -> b2:bytes
  -> Lemma (requires (equal b1 b2))
          (ensures (b1 = b2))

(** creating byte values **)
val create:
    len:u32
  -> v:byte
  -> b:lbytes (U32.v len){forall (i:u32{U32.(i <^ len)}).{:pattern b.[i]} b.[i] == v}

unfold
let create_ (n:nat{FStar.UInt.size n U32.n}) v = create (U32.uint_to_t n) v

val init:
    len:u32
  -> f:(i:u32{U32.(i <^ len)} -> byte)
  -> b:lbytes (U32.v len){forall (i:u32{U32.(i <^ len)}).{:pattern b.[i]} b.[i] == f i}

// this is a hack JROESCH
val abyte (b:byte) : lbytes 1
    (* admit () create 1ul b *)

val twobytes (b:byte*byte) : lbytes 2
    // init 2ul (fun i -> if i = 0ul then fst b else snd b)

(** appending bytes **)
val append:
    b1:bytes
  -> b2:bytes
  -> Pure bytes
         (requires (UInt.size (length b1 + length b2) U32.n))
         (ensures (fun b -> reveal b == S.append (reveal b1) (reveal b2)))
unfold let op_At_Bar = append

val slice:
    b:bytes
  -> s:u32
  -> e:u32{U32.(s <=^ e) /\ U32.v e <= length b}
val slice_ : b: FStar.Bytes.bytes -> s: Prims.nat -> e: Prims.nat{s <= e /\ e <= FStar.Bytes.length b}
  -> r:
    FStar.Bytes.bytes
      { FStar.Bytes.reveal r ==
        FStar.Seq.Base.slice (FStar.Bytes.reveal b)
          (FStar.UInt32.v (FStar.UInt32.uint_to_t s))
          (FStar.UInt32.v (FStar.UInt32.uint_to_t e)) }
b: FStar.Bytes.bytes -> s: Prims.nat -> e: Prims.nat{s <= e /\ e <= FStar.Bytes.length b}
  -> r:
    FStar.Bytes.bytes
      { FStar.Bytes.reveal r ==
        FStar.Seq.Base.slice (FStar.Bytes.reveal b)
          (FStar.UInt32.v (FStar.UInt32.uint_to_t s))
          (FStar.UInt32.v (FStar.UInt32.uint_to_t e)) }