val lbuffer : l: Prims.nat -> Type0
let lbuffer (l:nat) = b:Buffer.buffer UInt8.t {Buffer.length b == l}
module MiTLS.Test.BufferBytes
open MiTLS

open FStar.Bytes
open FStar.Error
open FStar.Printf
open FStar.HyperStack
open FStar.HyperStack.IO
open FStar.HyperStack.ST

module BB = MiTLS.BufferBytes
/
prims.fst.checked MiTLS.BufferBytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.IO.fst.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked FStar.Buffer.fst.checked C.fst.checked
MiTLS.Test.BufferBytes.fst
l: Prims.nat -> Type0
Prims.nat FStar.Buffer.buffer FStar.UInt8.t Prims.eq2 FStar.Buffer.length
let lbuffer (l: nat) =
  
b: Buffer.buffer UInt8.t {Buffer.length b == l}