val ad_Length : i: _ -> Prims.int
let ad_Length i = 8 + StatefulPlain.ad_Length i
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 }
/
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
i: _ -> Prims.int
Prims.op_Addition MiTLS.StatefulPlain.ad_Length Prims.int
let ad_Length i =
  
8 + StatefulPlain.ad_Length i