val read_record_cases (x: LP.sum_key record_sum) : LL.leaf_reader (dsnd (parse_record_cases x))
val read_record_cases (x: LP.sum_key record_sum) : LL.leaf_reader (dsnd (parse_record_cases x))
let read_record_cases (x:LP.sum_key record_sum)
  : LL.leaf_reader (dsnd (parse_record_cases x)) =
  match x with
  | Key_internal -> [@inline_let] let u : LL.leaf_reader (dsnd (parse_record_cases Key_internal)) = internal_record_reader in u
  | Key_application -> [@inline_let] let u : LL.leaf_reader (dsnd (parse_record_cases Key_application)) = application_record_reader in u
  | _ -> LL.read_false
module Zeta.Formats.Aux.Record

(* 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 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 Zeta.Formats.Aux.Key_kind

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

inline_for_extraction unfold let key_kind_as_enum_key (x:key_kind) : Pure (LP.enum_key key_kind_enum)
  (requires norm [delta; zeta; iota; primops] (LP.list_mem x (LP.list_map fst key_kind_enum)) == true) (ensures fun _ -> True) =
  [@inline_let] let _ = norm_spec [delta; zeta; iota; primops] (LP.list_mem x (LP.list_map fst key_kind_enum)) in x

inline_for_extraction let key_of_record (x:record) : LP.enum_key key_kind_enum =
  match x with
  | Record_kv_key_internal _ -> key_kind_as_enum_key Key_internal
  | Record_kv_key_application _ -> key_kind_as_enum_key Key_application

inline_for_extraction let record_case_of_key_kind (x:key_kind) : Type0 =
  match x with
  | Key_internal -> internal_record
  | Key_application -> application_record

unfold inline_for_extraction let to_record_case_of_key_kind (x:key_kind) (#x':key_kind) (y:record_case_of_key_kind x')  : Pure (norm [delta_only [(`%record_case_of_key_kind)]; iota] (record_case_of_key_kind x))
  (requires (x == x')) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%record_case_of_key_kind)] ; iota] (record_case_of_key_kind x) in y

unfold inline_for_extraction let record_refine (k:LP.enum_key key_kind_enum) (x:record)
  : Pure (LP.refine_with_tag key_of_record k)  (requires norm [delta; iota; zeta] (key_of_record x) == k) (ensures (fun y -> y == x)) =
  [@inline_let] let _ = norm_spec [delta; iota; zeta] (key_of_record x) in x

inline_for_extraction let synth_record_cases (x:LP.enum_key key_kind_enum) (y:record_case_of_key_kind x)
  : LP.refine_with_tag key_of_record x =
  match x with
  | Key_internal -> record_refine x (Record_kv_key_internal (to_record_case_of_key_kind Key_internal y))
  | Key_application -> record_refine x (Record_kv_key_application (to_record_case_of_key_kind Key_application y))

unfold inline_for_extraction let from_record_case_of_key_kind (#x':key_kind) (x:key_kind)
  (y: norm [delta_only [(`%record_case_of_key_kind)]; iota] (record_case_of_key_kind x))
  : Pure (record_case_of_key_kind x') (requires (x == x')) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%record_case_of_key_kind)] ; iota] (record_case_of_key_kind x) in y

let synth_record_cases_recip_pre (k:LP.enum_key key_kind_enum)
  (x:LP.refine_with_tag key_of_record k) : GTot bool =
  match k with
  | Key_internal -> Record_kv_key_internal? x
  | Key_application -> Record_kv_key_application? x

let synth_record_cases_recip_pre_intro (k:LP.enum_key key_kind_enum) (x:LP.refine_with_tag key_of_record k)
  : Lemma (synth_record_cases_recip_pre k x == true) =
  norm_spec [delta; iota] (synth_record_cases_recip_pre k x)

inline_for_extraction let synth_record_cases_recip (k:LP.enum_key key_kind_enum)
  (x:LP.refine_with_tag key_of_record k) : (record_case_of_key_kind k) =
  match k with
  | Key_internal -> [@inline_let] let _ = synth_record_cases_recip_pre_intro Key_internal x in
    (match x with Record_kv_key_internal y -> (from_record_case_of_key_kind Key_internal y))
  | Key_application -> [@inline_let] let _ = synth_record_cases_recip_pre_intro Key_application x in
    (match x with Record_kv_key_application y -> (from_record_case_of_key_kind Key_application y))

inline_for_extraction let record_sum = LP.make_sum' key_kind_enum key_of_record
  record_case_of_key_kind synth_record_cases synth_record_cases_recip
  (_ by (LP.make_sum_synth_case_recip_synth_case_tac ()))
  (_ by (LP.synth_case_synth_case_recip_tac ()))

noextract let parse_record_cases (x:LP.sum_key record_sum)
  : k:LP.parser_kind & LP.parser k (record_case_of_key_kind x) =
  match x with
  | Key_internal -> [@inline_let] let u : (k: LP.parser_kind & LP.parser k (record_case_of_key_kind Key_internal)) = (| _, internal_record_parser |) in u
  | Key_application -> [@inline_let] let u : (k: LP.parser_kind & LP.parser k (record_case_of_key_kind Key_application)) = (| _, application_record_parser |) in u
  | _ -> (| _, LP.parse_false |)

noextract let serialize_record_cases (x:LP.sum_key record_sum)
  : LP.serializer (dsnd (parse_record_cases x)) =
  match x with
  | Key_internal -> [@inline_let] let u : LP.serializer (dsnd (parse_record_cases Key_internal)) = internal_record_serializer in u
  | Key_application -> [@inline_let] let u : LP.serializer (dsnd (parse_record_cases Key_application)) = application_record_serializer in u
  | _ -> LP.serialize_false

inline_for_extraction noextract let size32_record_cases (x:LP.sum_key record_sum)
  : LSZ.size32 (serialize_record_cases x) =
  match x with
  | Key_internal -> [@inline_let] let u : LSZ.size32 (serialize_record_cases Key_internal) = internal_record_size32 in u
  | Key_application -> [@inline_let] let u : LSZ.size32 (serialize_record_cases Key_application) = application_record_size32 in u
  | _ -> LSZ.size32_false

inline_for_extraction noextract let validate_record_cases (x:LP.sum_key record_sum)
  : LL.validator (dsnd (parse_record_cases x)) =
  match x with
  | Key_internal -> [@inline_let] let u : LL.validator (dsnd (parse_record_cases Key_internal)) = internal_record_validator in u
  | Key_application -> [@inline_let] let u : LL.validator (dsnd (parse_record_cases Key_application)) = application_record_validator in u
  | _ -> LL.validate_false ()

inline_for_extraction noextract let jump_record_cases (x:LP.sum_key record_sum)
  : LL.jumper (dsnd (parse_record_cases x)) =
  match x with
  | Key_internal -> [@inline_let] let u : LL.jumper (dsnd (parse_record_cases Key_internal)) = internal_record_jumper in u
  | Key_application -> [@inline_let] let u : LL.jumper (dsnd (parse_record_cases Key_application)) = application_record_jumper in u
  | _ -> LL.jump_false
/
Zeta.Formats.Aux.Key_kind.fst.checked prims.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
Zeta.Formats.Aux.Record.fst
x: LowParse.Spec.Sum.sum_key Zeta.Formats.Aux.Record.record_sum
  -> LowParse.Low.Base.leaf_reader (FStar.Pervasives.dsnd (Zeta.Formats.Aux.Record.parse_record_cases
              x))
LowParse.Spec.Sum.sum_key Zeta.Formats.Aux.Record.record_sum LowParse.Low.Base.leaf_reader Prims.__proj__Mkdtuple2__item___1 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Zeta.Formats.Aux.Record.record_case_of_key_kind Zeta.Formats.Aux.Key_kind.Key_internal Zeta.Formats.Aux.Record.parse_record_cases FStar.Pervasives.dsnd Zeta.Formats.Aux.Internal_record.internal_record_reader Zeta.Formats.Aux.Key_kind.Key_application Zeta.Formats.Aux.Application_record.application_record_reader Zeta.Formats.Aux.Key_kind.key_kind LowParse.Low.Combinators.read_false
let read_record_cases (x: LP.sum_key record_sum) : LL.leaf_reader (dsnd (parse_record_cases x)) =
  
match x with
| Key_internal ->
  [@@ inline_let ]let u:LL.leaf_reader (dsnd (parse_record_cases Key_internal)) =
    internal_record_reader
  in
  u
| Key_application ->
  [@@ inline_let ]let u:LL.leaf_reader (dsnd (parse_record_cases Key_application)) =
    application_record_reader
  in
  u
| _ -> LL.read_false