val parseAD: b:bytes { length b >= 8 } -> Tot bytes
val parseAD: b:bytes { length b >= 8 } -> Tot bytes
let parseAD b = snd(split b 8ul)
module MiTLS.LHAEPlain
open MiTLS

open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
module Parse = MiTLS.Parse
open MiTLS.Parse

module Range = MiTLS.Range
let range = Range.range
let rbytes = Range.rbytes

//--------------------------------------------------------------------
// `Plain' interface towards LHAE
//--------------------------------------------------------------------

// We define payloads and additional data from those of StatefulPlain,
// adding an 8-byte sequence number to its additional data.

type id = i:id { ID12? i }

type seqn = n:nat{repr_bytes n <= 8}
let ad_Length i = 8 + StatefulPlain.ad_Length i
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StatefulPlain.fst.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.LHAEPlain.fst
b: FStar.Bytes.bytes{FStar.Bytes.length b >= 8} -> FStar.Bytes.bytes
FStar.Bytes.bytes Prims.b2t Prims.op_GreaterThanOrEqual FStar.Bytes.length FStar.Pervasives.Native.snd FStar.Bytes.split FStar.UInt32.__uint_to_t
let parseAD b =
  
snd (split b 8ul)