val lemma_makeAD_parseAD: i:id -> n:seqn -> ad:StatefulPlain.adata i
          -> Lemma (requires (True))
                   (ensures (parseAD (makeAD i n ad) = ad))
                   [SMTPat (makeAD i n ad)]
val lemma_makeAD_parseAD: i:id -> n:seqn -> ad:StatefulPlain.adata i
          -> Lemma (requires (True))
                   (ensures (parseAD (makeAD i n ad) = ad))
                   [SMTPat (makeAD i n ad)]
let lemma_makeAD_parseAD i n ad = cut (Bytes.equal ad (parseAD (makeAD i n ad)))
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'"

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

val lemma_makeAD_seqN: i:id -> n:seqn -> ad:StatefulPlain.adata i
          -> Lemma (requires (True))
                   (ensures (seqN i (makeAD i n ad) = n))
                   [SMTPat (makeAD i n ad)]

let lemma_makeAD_seqN i n ad = admit() 
    //TODO bytes NS 09/27
    // cut (Seq.equal (fst (Seq.split_eq (bytes_of_seq n @| ad) 8)) (bytes_of_seq n));
    // int_of_bytes_of_int (Seq.length (bytes_of_seq n)) n

#set-options "--admit_smt_queries true"
val lemma_makeAD_parseAD: i:id -> n:seqn -> ad:StatefulPlain.adata i
          -> Lemma (requires (True))
                   (ensures (parseAD (makeAD i n ad) = ad))
/
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 -> n: MiTLS.LHAEPlain.seqn -> ad: MiTLS.StatefulPlain.adata i
  -> FStar.Pervasives.Lemma (ensures MiTLS.LHAEPlain.parseAD (MiTLS.LHAEPlain.makeAD i n ad) = ad)
      [SMTPat (MiTLS.LHAEPlain.makeAD i n ad)]
MiTLS.LHAEPlain.id MiTLS.LHAEPlain.seqn MiTLS.StatefulPlain.adata Prims.cut FStar.Bytes.equal MiTLS.LHAEPlain.parseAD MiTLS.LHAEPlain.makeAD Prims.unit
let lemma_makeAD_parseAD i n ad =
  
cut (Bytes.equal ad (parseAD (makeAD i n ad)))