val certificateExtension_clens_signed_certificate_timestamp:LL.clens certificateExtension
  certificateExtension_e_signed_certificate_timestamp
val certificateExtension_clens_signed_certificate_timestamp:LL.clens certificateExtension
  certificateExtension_e_signed_certificate_timestamp
let certificateExtension_clens_signed_certificate_timestamp : LL.clens certificateExtension certificateExtension_e_signed_certificate_timestamp = {
  LL.clens_cond = (fun (x: certificateExtension) -> tag_of_certificateExtension x == Signed_certificate_timestamp);
  LL.clens_get = (fun (x: certificateExtension) -> (match x with E_signed_certificate_timestamp y -> y) <: (Ghost certificateExtension_e_signed_certificate_timestamp (requires (tag_of_certificateExtension x == Signed_certificate_timestamp)) (ensures (fun y -> True))));
}
module MiTLS.Parsers.CertificateExtension

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

open MiTLS.Parsers.ExtensionType
include MiTLS.Parsers.CertificateExtension_e_default
include MiTLS.Parsers.CertificateExtension_e_status_request
include MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp

type certificateExtension =
  | E_status_request of certificateExtension_e_status_request
  | E_signed_certificate_timestamp of certificateExtension_e_signed_certificate_timestamp
  | E_key_share of certificateExtension_e_default
  | E_signature_algorithms_cert of certificateExtension_e_default
  | E_post_handshake_auth of certificateExtension_e_default
  | E_oid_filters of certificateExtension_e_default
  | E_certificate_authorities of certificateExtension_e_default
  | E_psk_key_exchange_modes of certificateExtension_e_default
  | E_cookie of certificateExtension_e_default
  | E_supported_versions of certificateExtension_e_default
  | E_early_data of certificateExtension_e_default
  | E_pre_shared_key of certificateExtension_e_default
  | E_session_ticket of certificateExtension_e_default
  | E_extended_master_secret of certificateExtension_e_default
  | E_encrypt_then_mac of certificateExtension_e_default
  | E_padding of certificateExtension_e_default
  | E_server_certificate_type of certificateExtension_e_default
  | E_client_certificate_type of certificateExtension_e_default
  | E_application_layer_protocol_negotiation of certificateExtension_e_default
  | E_heartbeat of certificateExtension_e_default
  | E_use_srtp of certificateExtension_e_default
  | E_signature_algorithms of certificateExtension_e_default
  | E_ec_point_formats of certificateExtension_e_default
  | E_supported_groups of certificateExtension_e_default
  | E_max_fragment_length of certificateExtension_e_default
  | E_server_name of certificateExtension_e_default
  | E_Unknown_extensionType: v:extensionType_repr{not (known_extensionType_repr v)} -> x:certificateExtension_e_default -> certificateExtension

inline_for_extraction let tag_of_certificateExtension (x:certificateExtension) : extensionType = match x with
  | E_status_request _ -> Status_request
  | E_signed_certificate_timestamp _ -> Signed_certificate_timestamp
  | E_key_share _ -> Key_share
  | E_signature_algorithms_cert _ -> Signature_algorithms_cert
  | E_post_handshake_auth _ -> Post_handshake_auth
  | E_oid_filters _ -> Oid_filters
  | E_certificate_authorities _ -> Certificate_authorities
  | E_psk_key_exchange_modes _ -> Psk_key_exchange_modes
  | E_cookie _ -> Cookie
  | E_supported_versions _ -> Supported_versions
  | E_early_data _ -> Early_data
  | E_pre_shared_key _ -> Pre_shared_key
  | E_session_ticket _ -> Session_ticket
  | E_extended_master_secret _ -> Extended_master_secret
  | E_encrypt_then_mac _ -> Encrypt_then_mac
  | E_padding _ -> Padding
  | E_server_certificate_type _ -> Server_certificate_type
  | E_client_certificate_type _ -> Client_certificate_type
  | E_application_layer_protocol_negotiation _ -> Application_layer_protocol_negotiation
  | E_heartbeat _ -> Heartbeat
  | E_use_srtp _ -> Use_srtp
  | E_signature_algorithms _ -> Signature_algorithms
  | E_ec_point_formats _ -> Ec_point_formats
  | E_supported_groups _ -> Supported_groups
  | E_max_fragment_length _ -> Max_fragment_length
  | E_server_name _ -> Server_name
  | E_Unknown_extensionType v _ -> Unknown_extensionType v

inline_for_extraction noextract let certificateExtension_parser_kind = LP.strong_parser_kind 6 65539 None

noextract val certificateExtension_parser: LP.parser certificateExtension_parser_kind certificateExtension

noextract val certificateExtension_serializer: LP.serializer certificateExtension_parser

noextract val certificateExtension_bytesize (x:certificateExtension) : GTot nat

noextract val certificateExtension_bytesize_eq (x:certificateExtension) : Lemma (certificateExtension_bytesize x == Seq.length (LP.serialize certificateExtension_serializer x))

val certificateExtension_parser32: LS.parser32 certificateExtension_parser

val certificateExtension_serializer32: LS.serializer32 certificateExtension_serializer

val certificateExtension_size32: LSZ.size32 certificateExtension_serializer

val certificateExtension_validator: LL.validator certificateExtension_parser

val certificateExtension_jumper: LL.jumper certificateExtension_parser

val lemma_valid_certificateExtension_valid_extensionType: #rrel: _ -> #rel: _ -> s:LL.slice rrel rel -> pos:U32.t -> h:HyperStack.mem -> Lemma
  (requires LL.valid certificateExtension_parser h s pos)
  (ensures (LL.valid extensionType_parser h s pos /\ LL.contents extensionType_parser h s pos == tag_of_certificateExtension (LL.contents certificateExtension_parser h s pos)))
  [SMTPat (LL.valid certificateExtension_parser h s pos)]

noextract let certificateExtension_clens_tag : LL.clens certificateExtension extensionType = {
  LL.clens_cond = (fun _ -> True);
  LL.clens_get = (fun (x: certificateExtension) -> tag_of_certificateExtension x);
}

val certificateExtension_gaccessor_tag : LL.gaccessor certificateExtension_parser extensionType_parser certificateExtension_clens_tag

val certificateExtension_accessor_tag : LL.accessor certificateExtension_gaccessor_tag

val certificateExtension_bytesize_eqn_status_request  (x: certificateExtension_e_status_request) : Lemma (certificateExtension_bytesize (E_status_request  x) == 2 + (certificateExtension_e_status_request_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_status_request  x))]

val certificateExtension_bytesize_eqn_signed_certificate_timestamp  (x: certificateExtension_e_signed_certificate_timestamp) : Lemma (certificateExtension_bytesize (E_signed_certificate_timestamp  x) == 2 + (certificateExtension_e_signed_certificate_timestamp_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_signed_certificate_timestamp  x))]

val certificateExtension_bytesize_eqn_key_share  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_key_share  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_key_share  x))]

val certificateExtension_bytesize_eqn_signature_algorithms_cert  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_signature_algorithms_cert  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_signature_algorithms_cert  x))]

val certificateExtension_bytesize_eqn_post_handshake_auth  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_post_handshake_auth  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_post_handshake_auth  x))]

val certificateExtension_bytesize_eqn_oid_filters  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_oid_filters  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_oid_filters  x))]

val certificateExtension_bytesize_eqn_certificate_authorities  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_certificate_authorities  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_certificate_authorities  x))]

val certificateExtension_bytesize_eqn_psk_key_exchange_modes  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_psk_key_exchange_modes  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_psk_key_exchange_modes  x))]

val certificateExtension_bytesize_eqn_cookie  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_cookie  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_cookie  x))]

val certificateExtension_bytesize_eqn_supported_versions  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_supported_versions  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_supported_versions  x))]

val certificateExtension_bytesize_eqn_early_data  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_early_data  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_early_data  x))]

val certificateExtension_bytesize_eqn_pre_shared_key  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_pre_shared_key  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_pre_shared_key  x))]

val certificateExtension_bytesize_eqn_session_ticket  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_session_ticket  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_session_ticket  x))]

val certificateExtension_bytesize_eqn_extended_master_secret  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_extended_master_secret  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_extended_master_secret  x))]

val certificateExtension_bytesize_eqn_encrypt_then_mac  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_encrypt_then_mac  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_encrypt_then_mac  x))]

val certificateExtension_bytesize_eqn_padding  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_padding  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_padding  x))]

val certificateExtension_bytesize_eqn_server_certificate_type  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_server_certificate_type  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_server_certificate_type  x))]

val certificateExtension_bytesize_eqn_client_certificate_type  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_client_certificate_type  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_client_certificate_type  x))]

val certificateExtension_bytesize_eqn_application_layer_protocol_negotiation  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_application_layer_protocol_negotiation  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_application_layer_protocol_negotiation  x))]

val certificateExtension_bytesize_eqn_heartbeat  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_heartbeat  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_heartbeat  x))]

val certificateExtension_bytesize_eqn_use_srtp  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_use_srtp  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_use_srtp  x))]

val certificateExtension_bytesize_eqn_signature_algorithms  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_signature_algorithms  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_signature_algorithms  x))]

val certificateExtension_bytesize_eqn_ec_point_formats  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_ec_point_formats  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_ec_point_formats  x))]

val certificateExtension_bytesize_eqn_supported_groups  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_supported_groups  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_supported_groups  x))]

val certificateExtension_bytesize_eqn_max_fragment_length  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_max_fragment_length  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_max_fragment_length  x))]

val certificateExtension_bytesize_eqn_server_name  (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_server_name  x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_server_name  x))]

val certificateExtension_bytesize_eqn_Unknown_extensionType (v: extensionType_repr { not (known_extensionType_repr v) } ) (x: certificateExtension_e_default) : Lemma (certificateExtension_bytesize (E_Unknown_extensionType v x) == 2 + (certificateExtension_e_default_bytesize (x))) [SMTPat (certificateExtension_bytesize (E_Unknown_extensionType v x))]

noextract let certificateExtension_clens_status_request : LL.clens certificateExtension certificateExtension_e_status_request = {
  LL.clens_cond = (fun (x: certificateExtension) -> tag_of_certificateExtension x == Status_request);
  LL.clens_get = (fun (x: certificateExtension) -> (match x with E_status_request y -> y) <: (Ghost certificateExtension_e_status_request (requires (tag_of_certificateExtension x == Status_request)) (ensures (fun y -> True))));
}

val certificateExtension_gaccessor_status_request : LL.gaccessor certificateExtension_parser certificateExtension_e_status_request_parser certificateExtension_clens_status_request

val certificateExtension_accessor_status_request : LL.accessor certificateExtension_gaccessor_status_request
/
prims.fst.checked MiTLS.Parsers.ExtensionType.fsti.checked MiTLS.Parsers.CertificateExtension_e_status_request.fsti.checked MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp.fsti.checked MiTLS.Parsers.CertificateExtension_e_default.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.CertificateExtension.fsti
LowParse.Low.Base.Spec.clens MiTLS.Parsers.CertificateExtension.certificateExtension
  MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp.certificateExtension_e_signed_certificate_timestamp

LowParse.Low.Base.Spec.Mkclens MiTLS.Parsers.CertificateExtension.certificateExtension MiTLS.Parsers.CertificateExtension_e_signed_certificate_timestamp.certificateExtension_e_signed_certificate_timestamp Prims.eq2 MiTLS.Parsers.ExtensionType.extensionType MiTLS.Parsers.CertificateExtension.tag_of_certificateExtension MiTLS.Parsers.ExtensionType.Signed_certificate_timestamp Prims.l_True
let certificateExtension_clens_signed_certificate_timestamp:LL.clens certificateExtension
  certificateExtension_e_signed_certificate_timestamp =
  
{
  LL.clens_cond
  =
  (fun (x: certificateExtension) -> tag_of_certificateExtension x == Signed_certificate_timestamp);
  LL.clens_get
  =
  (fun (x: certificateExtension) ->
      (match x with | E_signed_certificate_timestamp y -> y)
      <:
      (Ghost certificateExtension_e_signed_certificate_timestamp
          (requires (tag_of_certificateExtension x == Signed_certificate_timestamp))
          (ensures (fun y -> True))))
}