val seqN: i:id -> adata i -> Tot seqn
val seqN: i:id -> adata i -> Tot seqn
let seqN i ad =
//18-02-26 review?
//    let snb,ad = FStar.Bytes.split_eq ad 8 in //TODO bytes NS 09/27
    let snb,ad = FStar.Bytes.split ad 8ul in    
    seq_of_bytes snb
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

val parseAD: b:bytes { length b >= 8 } -> Tot bytes
let parseAD b = snd(split b 8ul)

type adata (i:id) = b:lbytes (ad_Length i)
  { exists (ad:StatefulPlain.adata i). ad == parseAD b}

#set-options "--admit_smt_queries true"
let makeAD i seqn (ad:StatefulPlain.adata i) : adata i =
  let b = bytes_of_seq seqn @| ad in
  cut(Bytes.equal ad (parseAD b));
  b
#reset-options

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"
/
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: MiTLS.LHAEPlain.id -> ad: MiTLS.LHAEPlain.adata i -> MiTLS.LHAEPlain.seqn
MiTLS.LHAEPlain.id MiTLS.LHAEPlain.adata FStar.Bytes.bytes MiTLS.Parse.seq_of_bytes MiTLS.LHAEPlain.seqn FStar.Pervasives.Native.tuple2 Prims.eq2 FStar.Seq.Base.seq FStar.UInt8.t FStar.Pervasives.Native.Mktuple2 FStar.Bytes.reveal FStar.Seq.Properties.split FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t FStar.Bytes.split FStar.UInt32.__uint_to_t
let seqN i ad =
  
let snb, ad = FStar.Bytes.split ad 8ul in
seq_of_bytes snb