val synth_certificateExtension_cases_recip_pre
      (k: LP.maybe_enum_key extensionType_enum)
      (x: LP.refine_with_tag key_of_certificateExtension k)
    : GTot bool
val synth_certificateExtension_cases_recip_pre
      (k: LP.maybe_enum_key extensionType_enum)
      (x: LP.refine_with_tag key_of_certificateExtension k)
    : GTot bool
let synth_certificateExtension_cases_recip_pre (k:LP.maybe_enum_key extensionType_enum)
  (x:LP.refine_with_tag key_of_certificateExtension k) : GTot bool =
  match k with
  | LP.Known Status_request -> E_status_request? x
  | LP.Known Signed_certificate_timestamp -> E_signed_certificate_timestamp? x
  | LP.Known Key_share -> E_key_share? x
  | LP.Known Signature_algorithms_cert -> E_signature_algorithms_cert? x
  | LP.Known Post_handshake_auth -> E_post_handshake_auth? x
  | LP.Known Oid_filters -> E_oid_filters? x
  | LP.Known Certificate_authorities -> E_certificate_authorities? x
  | LP.Known Psk_key_exchange_modes -> E_psk_key_exchange_modes? x
  | LP.Known Cookie -> E_cookie? x
  | LP.Known Supported_versions -> E_supported_versions? x
  | LP.Known Early_data -> E_early_data? x
  | LP.Known Pre_shared_key -> E_pre_shared_key? x
  | LP.Known Session_ticket -> E_session_ticket? x
  | LP.Known Extended_master_secret -> E_extended_master_secret? x
  | LP.Known Encrypt_then_mac -> E_encrypt_then_mac? x
  | LP.Known Padding -> E_padding? x
  | LP.Known Server_certificate_type -> E_server_certificate_type? x
  | LP.Known Client_certificate_type -> E_client_certificate_type? x
  | LP.Known Application_layer_protocol_negotiation -> E_application_layer_protocol_negotiation? x
  | LP.Known Heartbeat -> E_heartbeat? x
  | LP.Known Use_srtp -> E_use_srtp? x
  | LP.Known Signature_algorithms -> E_signature_algorithms? x
  | LP.Known Ec_point_formats -> E_ec_point_formats? x
  | LP.Known Supported_groups -> E_supported_groups? x
  | LP.Known Max_fragment_length -> E_max_fragment_length? x
  | LP.Known Server_name -> E_server_name? x
  | LP.Known _ -> false
  | LP.Unknown _ -> E_Unknown_extensionType? x
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
module LT = LowParse.TacLib
module LS = LowParse.SLow
module LSZ = LowParse.SLow
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --z3rlimit 16 --z3cliopt smt.arith.nl=false --max_fuel 2 --max_ifuel 2"

friend MiTLS.Parsers.ExtensionType

// Need high Z3 limits for large sum types
#set-options "--z3rlimit 1560"

inline_for_extraction unfold let known_extensionType_as_enum_key
  (x: extensionType { norm [delta; zeta; iota; primops] (LP.list_mem x (LP.list_map fst extensionType_enum)) == true })
  : LP.enum_key extensionType_enum =
  [@inline_let] let _ = norm_spec [delta; zeta; iota; primops] (LP.list_mem x (LP.list_map fst extensionType_enum)) in x

inline_for_extraction let unknown_extensionType_as_enum_key (r:extensionType_repr) : Pure (LP.unknown_enum_repr extensionType_enum)
  (requires known_extensionType_repr r == false) (ensures fun _ -> True) =
  [@inline_let] let _ = assert_norm(LP.list_mem r (LP.list_map snd extensionType_enum) == known_extensionType_repr r) in r

inline_for_extraction let unknown_enum_repr_extensionType_as_repr (r:LP.unknown_enum_repr extensionType_enum) : Pure extensionType_repr
  (requires True) (ensures fun r -> known_extensionType_repr r == false) =
  [@inline_let] let _ = assert_norm(LP.list_mem r (LP.list_map snd extensionType_enum) == known_extensionType_repr r) in r

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

inline_for_extraction let certificateExtension_case_of_extensionType (x:extensionType) : Type0 =
  match x with
  | Status_request -> certificateExtension_e_status_request
  | Signed_certificate_timestamp -> certificateExtension_e_signed_certificate_timestamp
  | Key_share -> certificateExtension_e_default
  | Signature_algorithms_cert -> certificateExtension_e_default
  | Post_handshake_auth -> certificateExtension_e_default
  | Oid_filters -> certificateExtension_e_default
  | Certificate_authorities -> certificateExtension_e_default
  | Psk_key_exchange_modes -> certificateExtension_e_default
  | Cookie -> certificateExtension_e_default
  | Supported_versions -> certificateExtension_e_default
  | Early_data -> certificateExtension_e_default
  | Pre_shared_key -> certificateExtension_e_default
  | Session_ticket -> certificateExtension_e_default
  | Extended_master_secret -> certificateExtension_e_default
  | Encrypt_then_mac -> certificateExtension_e_default
  | Padding -> certificateExtension_e_default
  | Server_certificate_type -> certificateExtension_e_default
  | Client_certificate_type -> certificateExtension_e_default
  | Application_layer_protocol_negotiation -> certificateExtension_e_default
  | Heartbeat -> certificateExtension_e_default
  | Use_srtp -> certificateExtension_e_default
  | Signature_algorithms -> certificateExtension_e_default
  | Ec_point_formats -> certificateExtension_e_default
  | Supported_groups -> certificateExtension_e_default
  | Max_fragment_length -> certificateExtension_e_default
  | Server_name -> certificateExtension_e_default
  | Unknown_extensionType _ -> squash False

unfold inline_for_extraction let certificateExtension_value_type (x:LP.maybe_enum_key extensionType_enum) =
  LP.dsum_type_of_tag' extensionType_enum certificateExtension_case_of_extensionType certificateExtension_e_default x

unfold inline_for_extraction let certificateExtension_refine (k:LP.maybe_enum_key extensionType_enum) (x:certificateExtension)
  : Pure (LP.refine_with_tag key_of_certificateExtension k)
  (requires key_of_certificateExtension x == k) (ensures fun y -> y == x) =
  [@inline_let] let _ = norm_spec [delta; iota; zeta] (key_of_certificateExtension x) in x

unfold inline_for_extraction let certificateExtension_type_of_known_case (k: LP.enum_key extensionType_enum)
  (x:extensionType) (q: squash ((k <: extensionType) == x))
  (#x' : LP.maybe_enum_key extensionType_enum) (y: certificateExtension_value_type x')
  : Pure (norm [delta_only [(`%certificateExtension_case_of_extensionType)]; iota] (certificateExtension_case_of_extensionType x))
  (requires (LP.Known k == x')) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%certificateExtension_case_of_extensionType)]; iota] (certificateExtension_case_of_extensionType k) in y

unfold inline_for_extraction let certificateExtension_known_case (k: LP.enum_key extensionType_enum)
  (x: extensionType) (y: norm [delta_only [(`%certificateExtension_case_of_extensionType)]; iota] (certificateExtension_case_of_extensionType x))
  : Pure (certificateExtension_case_of_extensionType k) (requires (k == x)) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%certificateExtension_case_of_extensionType)] ; iota] (certificateExtension_case_of_extensionType x) in y

inline_for_extraction let synth_known_certificateExtension_cases (k:LP.enum_key extensionType_enum)
  (y:certificateExtension_value_type (LP.Known k)) : LP.refine_with_tag key_of_certificateExtension (LP.Known k) =
  match k with
  | Status_request ->
    [@inline_let] let x : certificateExtension = E_status_request (certificateExtension_type_of_known_case k Status_request () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Status_request) in
    certificateExtension_refine (LP.Known Status_request) x
  | Signed_certificate_timestamp ->
    [@inline_let] let x : certificateExtension = E_signed_certificate_timestamp (certificateExtension_type_of_known_case k Signed_certificate_timestamp () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Signed_certificate_timestamp) in
    certificateExtension_refine (LP.Known Signed_certificate_timestamp) x
  | Key_share ->
    [@inline_let] let x : certificateExtension = E_key_share (certificateExtension_type_of_known_case k Key_share () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Key_share) in
    certificateExtension_refine (LP.Known Key_share) x
  | Signature_algorithms_cert ->
    [@inline_let] let x : certificateExtension = E_signature_algorithms_cert (certificateExtension_type_of_known_case k Signature_algorithms_cert () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Signature_algorithms_cert) in
    certificateExtension_refine (LP.Known Signature_algorithms_cert) x
  | Post_handshake_auth ->
    [@inline_let] let x : certificateExtension = E_post_handshake_auth (certificateExtension_type_of_known_case k Post_handshake_auth () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Post_handshake_auth) in
    certificateExtension_refine (LP.Known Post_handshake_auth) x
  | Oid_filters ->
    [@inline_let] let x : certificateExtension = E_oid_filters (certificateExtension_type_of_known_case k Oid_filters () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Oid_filters) in
    certificateExtension_refine (LP.Known Oid_filters) x
  | Certificate_authorities ->
    [@inline_let] let x : certificateExtension = E_certificate_authorities (certificateExtension_type_of_known_case k Certificate_authorities () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Certificate_authorities) in
    certificateExtension_refine (LP.Known Certificate_authorities) x
  | Psk_key_exchange_modes ->
    [@inline_let] let x : certificateExtension = E_psk_key_exchange_modes (certificateExtension_type_of_known_case k Psk_key_exchange_modes () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Psk_key_exchange_modes) in
    certificateExtension_refine (LP.Known Psk_key_exchange_modes) x
  | Cookie ->
    [@inline_let] let x : certificateExtension = E_cookie (certificateExtension_type_of_known_case k Cookie () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Cookie) in
    certificateExtension_refine (LP.Known Cookie) x
  | Supported_versions ->
    [@inline_let] let x : certificateExtension = E_supported_versions (certificateExtension_type_of_known_case k Supported_versions () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Supported_versions) in
    certificateExtension_refine (LP.Known Supported_versions) x
  | Early_data ->
    [@inline_let] let x : certificateExtension = E_early_data (certificateExtension_type_of_known_case k Early_data () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Early_data) in
    certificateExtension_refine (LP.Known Early_data) x
  | Pre_shared_key ->
    [@inline_let] let x : certificateExtension = E_pre_shared_key (certificateExtension_type_of_known_case k Pre_shared_key () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Pre_shared_key) in
    certificateExtension_refine (LP.Known Pre_shared_key) x
  | Session_ticket ->
    [@inline_let] let x : certificateExtension = E_session_ticket (certificateExtension_type_of_known_case k Session_ticket () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Session_ticket) in
    certificateExtension_refine (LP.Known Session_ticket) x
  | Extended_master_secret ->
    [@inline_let] let x : certificateExtension = E_extended_master_secret (certificateExtension_type_of_known_case k Extended_master_secret () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Extended_master_secret) in
    certificateExtension_refine (LP.Known Extended_master_secret) x
  | Encrypt_then_mac ->
    [@inline_let] let x : certificateExtension = E_encrypt_then_mac (certificateExtension_type_of_known_case k Encrypt_then_mac () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Encrypt_then_mac) in
    certificateExtension_refine (LP.Known Encrypt_then_mac) x
  | Padding ->
    [@inline_let] let x : certificateExtension = E_padding (certificateExtension_type_of_known_case k Padding () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Padding) in
    certificateExtension_refine (LP.Known Padding) x
  | Server_certificate_type ->
    [@inline_let] let x : certificateExtension = E_server_certificate_type (certificateExtension_type_of_known_case k Server_certificate_type () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Server_certificate_type) in
    certificateExtension_refine (LP.Known Server_certificate_type) x
  | Client_certificate_type ->
    [@inline_let] let x : certificateExtension = E_client_certificate_type (certificateExtension_type_of_known_case k Client_certificate_type () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Client_certificate_type) in
    certificateExtension_refine (LP.Known Client_certificate_type) x
  | Application_layer_protocol_negotiation ->
    [@inline_let] let x : certificateExtension = E_application_layer_protocol_negotiation (certificateExtension_type_of_known_case k Application_layer_protocol_negotiation () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Application_layer_protocol_negotiation) in
    certificateExtension_refine (LP.Known Application_layer_protocol_negotiation) x
  | Heartbeat ->
    [@inline_let] let x : certificateExtension = E_heartbeat (certificateExtension_type_of_known_case k Heartbeat () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Heartbeat) in
    certificateExtension_refine (LP.Known Heartbeat) x
  | Use_srtp ->
    [@inline_let] let x : certificateExtension = E_use_srtp (certificateExtension_type_of_known_case k Use_srtp () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Use_srtp) in
    certificateExtension_refine (LP.Known Use_srtp) x
  | Signature_algorithms ->
    [@inline_let] let x : certificateExtension = E_signature_algorithms (certificateExtension_type_of_known_case k Signature_algorithms () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Signature_algorithms) in
    certificateExtension_refine (LP.Known Signature_algorithms) x
  | Ec_point_formats ->
    [@inline_let] let x : certificateExtension = E_ec_point_formats (certificateExtension_type_of_known_case k Ec_point_formats () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Ec_point_formats) in
    certificateExtension_refine (LP.Known Ec_point_formats) x
  | Supported_groups ->
    [@inline_let] let x : certificateExtension = E_supported_groups (certificateExtension_type_of_known_case k Supported_groups () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Supported_groups) in
    certificateExtension_refine (LP.Known Supported_groups) x
  | Max_fragment_length ->
    [@inline_let] let x : certificateExtension = E_max_fragment_length (certificateExtension_type_of_known_case k Max_fragment_length () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Max_fragment_length) in
    certificateExtension_refine (LP.Known Max_fragment_length) x
  | Server_name ->
    [@inline_let] let x : certificateExtension = E_server_name (certificateExtension_type_of_known_case k Server_name () y) in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Known Server_name) in
    certificateExtension_refine (LP.Known Server_name) x

inline_for_extraction let synth_certificateExtension_cases (x:LP.maybe_enum_key extensionType_enum)
  (y:certificateExtension_value_type x) : LP.refine_with_tag key_of_certificateExtension x =
  match x with
  | LP.Unknown v ->
    [@inline_let] let x : certificateExtension = E_Unknown_extensionType (unknown_enum_repr_extensionType_as_repr v) y in
    [@inline_let] let _ = assert_norm (key_of_certificateExtension x == LP.Unknown v) in
    certificateExtension_refine (LP.Unknown v) x
  | LP.Known k -> synth_known_certificateExtension_cases k y

unfold inline_for_extraction let from_certificateExtension_case_of_extensionType (#x':extensionType) (x:extensionType)
  (y: norm [delta_only [(`%certificateExtension_case_of_extensionType)]; iota] (certificateExtension_case_of_extensionType x))
  : Pure (certificateExtension_case_of_extensionType x') (requires (x == x')) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%certificateExtension_case_of_extensionType)] ; iota] (certificateExtension_case_of_extensionType x) in y
/
prims.fst.checked MiTLS.Parsers.ExtensionType.fst.checked LowStar.Buffer.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.AllIntegers.fst.checked LowParse.Spec.fst.checked LowParse.SLow.fst.checked LowParse.Low.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Tactics.Effect.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.fst

    k: LowParse.Spec.Enum.maybe_enum_key MiTLS.Parsers.ExtensionType.extensionType_enum ->
    x:
      LowParse.Spec.Base.refine_with_tag MiTLS.Parsers.CertificateExtension.key_of_certificateExtension
        k
  -> Prims.GTot Prims.bool
LowParse.Spec.Enum.maybe_enum_key MiTLS.Parsers.ExtensionType.extensionType FStar.UInt16.t MiTLS.Parsers.ExtensionType.extensionType_enum LowParse.Spec.Base.refine_with_tag MiTLS.Parsers.CertificateExtension.certificateExtension MiTLS.Parsers.CertificateExtension.key_of_certificateExtension MiTLS.Parsers.CertificateExtension.uu___is_E_status_request MiTLS.Parsers.CertificateExtension.uu___is_E_signed_certificate_timestamp MiTLS.Parsers.CertificateExtension.uu___is_E_key_share MiTLS.Parsers.CertificateExtension.uu___is_E_signature_algorithms_cert MiTLS.Parsers.CertificateExtension.uu___is_E_post_handshake_auth MiTLS.Parsers.CertificateExtension.uu___is_E_oid_filters MiTLS.Parsers.CertificateExtension.uu___is_E_certificate_authorities MiTLS.Parsers.CertificateExtension.uu___is_E_psk_key_exchange_modes MiTLS.Parsers.CertificateExtension.uu___is_E_cookie MiTLS.Parsers.CertificateExtension.uu___is_E_supported_versions MiTLS.Parsers.CertificateExtension.uu___is_E_early_data MiTLS.Parsers.CertificateExtension.uu___is_E_pre_shared_key MiTLS.Parsers.CertificateExtension.uu___is_E_session_ticket MiTLS.Parsers.CertificateExtension.uu___is_E_extended_master_secret MiTLS.Parsers.CertificateExtension.uu___is_E_encrypt_then_mac MiTLS.Parsers.CertificateExtension.uu___is_E_padding MiTLS.Parsers.CertificateExtension.uu___is_E_server_certificate_type MiTLS.Parsers.CertificateExtension.uu___is_E_client_certificate_type MiTLS.Parsers.CertificateExtension.uu___is_E_application_layer_protocol_negotiation MiTLS.Parsers.CertificateExtension.uu___is_E_heartbeat MiTLS.Parsers.CertificateExtension.uu___is_E_use_srtp MiTLS.Parsers.CertificateExtension.uu___is_E_signature_algorithms MiTLS.Parsers.CertificateExtension.uu___is_E_ec_point_formats MiTLS.Parsers.CertificateExtension.uu___is_E_supported_groups MiTLS.Parsers.CertificateExtension.uu___is_E_max_fragment_length MiTLS.Parsers.CertificateExtension.uu___is_E_server_name LowParse.Spec.Enum.enum_key LowParse.Spec.Enum.unknown_enum_repr MiTLS.Parsers.CertificateExtension.uu___is_E_Unknown_extensionType Prims.bool
let synth_certificateExtension_cases_recip_pre
      (k: LP.maybe_enum_key extensionType_enum)
      (x: LP.refine_with_tag key_of_certificateExtension k)
    : GTot bool =
  
match k with
| LP.Known Status_request -> E_status_request? x
| LP.Known Signed_certificate_timestamp -> E_signed_certificate_timestamp? x
| LP.Known Key_share -> E_key_share? x
| LP.Known Signature_algorithms_cert -> E_signature_algorithms_cert? x
| LP.Known Post_handshake_auth -> E_post_handshake_auth? x
| LP.Known Oid_filters -> E_oid_filters? x
| LP.Known Certificate_authorities -> E_certificate_authorities? x
| LP.Known Psk_key_exchange_modes -> E_psk_key_exchange_modes? x
| LP.Known Cookie -> E_cookie? x
| LP.Known Supported_versions -> E_supported_versions? x
| LP.Known Early_data -> E_early_data? x
| LP.Known Pre_shared_key -> E_pre_shared_key? x
| LP.Known Session_ticket -> E_session_ticket? x
| LP.Known Extended_master_secret -> E_extended_master_secret? x
| LP.Known Encrypt_then_mac -> E_encrypt_then_mac? x
| LP.Known Padding -> E_padding? x
| LP.Known Server_certificate_type -> E_server_certificate_type? x
| LP.Known Client_certificate_type -> E_client_certificate_type? x
| LP.Known Application_layer_protocol_negotiation -> E_application_layer_protocol_negotiation? x
| LP.Known Heartbeat -> E_heartbeat? x
| LP.Known Use_srtp -> E_use_srtp? x
| LP.Known Signature_algorithms -> E_signature_algorithms? x
| LP.Known Ec_point_formats -> E_ec_point_formats? x
| LP.Known Supported_groups -> E_supported_groups? x
| LP.Known Max_fragment_length -> E_max_fragment_length? x
| LP.Known Server_name -> E_server_name? x
| LP.Known _ -> false
| LP.Unknown _ -> E_Unknown_extensionType? x