val alertBytes_then_parse (a: alert) : Lemma (parse (alertBytes a) == Correct a)
val alertBytes_then_parse (a: alert) : Lemma (parse (alertBytes a) == Correct a)
let alertBytes_then_parse (a:alert) : Lemma (parse (alertBytes a) == Correct a) = 
  LowParseWrappers.lemma_inverse_serializer32_parser32_constant_length alert_serializer32 2 () alert_parser32 "" a
module MiTLS.Alert
open MiTLS

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

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

module Range = MiTLS.Range
open MiTLS.Range

//16-05-29 not much protocol left; consider merging with TLSError

(* Conversions *)

val alertBytes: alert -> Tot (lbytes 2)
let alertBytes = 
  LowParseWrappers.wrap_serializer32_constant_length alert_serializer32 2 ()

val parse: pinverse_t alertBytes 
// eta-expansion required for KaRaMeL extraction
let parse x = 
  LowParseWrappers.wrap_parser32_constant_length 
    alert_serializer32 2 () alert_parser32
    "" //(perror __SOURCE_FILE__ __LINE__ "")
    x
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.LowParseWrappers.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Alert.fst
a: MiTLS.Parsers.Alert.alert
  -> FStar.Pervasives.Lemma
    (ensures MiTLS.Alert.parse (MiTLS.Alert.alertBytes a) == FStar.Error.Correct a)
MiTLS.Parsers.Alert.alert MiTLS.LowParseWrappers.lemma_inverse_serializer32_parser32_constant_length MiTLS.Parsers.Alert.alert_parser_kind MiTLS.Parsers.Alert.alert_parser MiTLS.Parsers.Alert.alert_serializer MiTLS.Parsers.Alert.alert_serializer32 MiTLS.Parsers.Alert.alert_parser32 Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Error.optResult MiTLS.TLSError.error MiTLS.Alert.parse MiTLS.Alert.alertBytes FStar.Error.Correct Prims.Nil FStar.Pervasives.pattern
let alertBytes_then_parse (a: alert) : Lemma (parse (alertBytes a) == Correct a) =
  
LowParseWrappers.lemma_inverse_serializer32_parser32_constant_length alert_serializer32
  2
  ()
  alert_parser32
  ""
  a