val makeAD: i:id -> ct:contentType -> Tot (lbytes (ad_Length i))
val makeAD: i:id -> ct:contentType -> Tot (lbytes (ad_Length i))
let makeAD i ct =
    (ctBytes ct) @| versionBytes (pv_of_id i)
module MiTLS.StatefulPlain
open MiTLS

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

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.Content

module Range = MiTLS.Range
open MiTLS.Range

// Defines additional data and an abstract "plain i ad rg" plaintext
// typed interface from the more concrete & TLS-specific type
// "Content.fragment i". (Type abstraction helps with modularity, but
// not with privacy in this case.)

// This module is used only up to TLS 1.2

type id = i:id { ID12? i }

let ad_Length i = 3
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.StatefulPlain.fst
i: MiTLS.StatefulPlain.id -> ct: MiTLS.Content.contentType
  -> FStar.Bytes.lbytes (MiTLS.StatefulPlain.ad_Length i)
MiTLS.StatefulPlain.id MiTLS.Content.contentType FStar.Bytes.op_At_Bar MiTLS.Content.ctBytes MiTLS.TLSConstants.versionBytes MiTLS.TLSInfo.pv_of_id FStar.Bytes.lbytes MiTLS.StatefulPlain.ad_Length
let makeAD i ct =
  
(ctBytes ct) @| versionBytes (pv_of_id i)