let op_String_Access = get
let op_String_Access =
get
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.get
(*
   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)))
val op_String_Access : b: FStar.Bytes.bytes -> pos: FStar.Bytes.u32{FStar.UInt32.v pos < FStar.Bytes.length b}
  -> Prims.Pure FStar.Bytes.byte
b: FStar.Bytes.bytes -> pos: FStar.Bytes.u32{FStar.UInt32.v pos < FStar.Bytes.length b}
  -> Prims.Pure FStar.Bytes.byte