fsdoc: no-summary-found
fsdoc: no-comment-found
typeabbrev Realized by uint8_t in C and int in OCaml (char does not have necessary operators...)
val bytes:t:Type0:{hasEq t}Realized in C by a pair of a length field and uint8_t* in C Realized in OCaml by a string
val reveal:Unidentified product: [bytes] (GTot (S.seq byte))representation for specs that need lemmas not defined here.
val get:Unidentified product: [b:bytes] Unidentified product: [pos:pos:u32:{<(U32.v pos, length b)}] (Pure byte ((requires True)) ((ensures ((fun y -> ==(y, S.index (reveal b) (U32.v pos)))))))If you statically know the length, it is OK to read at arbitrary indexes
val create:Unidentified product: [len:u32] Unidentified product: [v:byte] b:lbytes (U32.v len):{forall i:i:u32:{let open U32 in <^(i, len)}.{:pattern .[](b, i)} ==(.[](b, i), v)}creating byte values *
val append:Unidentified product: [b1:bytes] Unidentified product: [b2:bytes] (Pure bytes ((requires (UInt.size (+(length b1, length b2)) U32.n))) ((ensures ((fun b -> ==(reveal b, S.append (reveal b1) (reveal b2)))))))appending bytes *
let (fits_in_k_bytes (n:nat) (k:nat)):FStar.UInt.size n (op_Multiply 8 k)Interpret a sequence of bytes as a mathematical integer encoded in big endian *
val repr_bytes:Unidentified product: [n:nat] k:pos:{fits_in_k_bytes n k}repr_bytes n: The number of bytes needed to represent a nat *
A better implementation of BufferBytes, formerly found in miTLS