val application_record_v_payload_accessor_DValueSome : LL.accessor application_record_v_payload_gaccessor_DValueSome
val application_record_v_payload_accessor_DValueSome : LL.accessor application_record_v_payload_gaccessor_DValueSome
let application_record_v_payload_accessor_DValueSome =
  LL.accessor_ext
    application_record_v_payload_accessor'_DValueSome
    application_record_v_payload_clens_DValueSome
    application_record_v_payload_clens_eq_DValueSome
module Zeta.Formats.Aux.Application_record_v_payload

(* 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.Dvalue_kind

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

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

inline_for_extraction let key_of_application_record_v_payload (x:application_record_v_payload) : LP.enum_key dvalue_kind_enum =
  match x with
  | V_payload_DValueNone _ -> dvalue_kind_as_enum_key DValueNone
  | V_payload_DValueSome _ -> dvalue_kind_as_enum_key DValueSome

inline_for_extraction let application_record_v_payload_case_of_dvalue_kind (x:dvalue_kind) : Type0 =
  match x with
  | DValueNone -> unit
  | DValueSome -> application_value

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

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

inline_for_extraction let synth_application_record_v_payload_cases (x:LP.enum_key dvalue_kind_enum) (y:application_record_v_payload_case_of_dvalue_kind x)
  : LP.refine_with_tag key_of_application_record_v_payload x =
  match x with
  | DValueNone -> application_record_v_payload_refine x (V_payload_DValueNone (to_application_record_v_payload_case_of_dvalue_kind DValueNone y))
  | DValueSome -> application_record_v_payload_refine x (V_payload_DValueSome (to_application_record_v_payload_case_of_dvalue_kind DValueSome y))

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

let synth_application_record_v_payload_cases_recip_pre (k:LP.enum_key dvalue_kind_enum)
  (x:LP.refine_with_tag key_of_application_record_v_payload k) : GTot bool =
  match k with
  | DValueNone -> V_payload_DValueNone? x
  | DValueSome -> V_payload_DValueSome? x

let synth_application_record_v_payload_cases_recip_pre_intro (k:LP.enum_key dvalue_kind_enum) (x:LP.refine_with_tag key_of_application_record_v_payload k)
  : Lemma (synth_application_record_v_payload_cases_recip_pre k x == true) =
  norm_spec [delta; iota] (synth_application_record_v_payload_cases_recip_pre k x)

inline_for_extraction let synth_application_record_v_payload_cases_recip (k:LP.enum_key dvalue_kind_enum)
  (x:LP.refine_with_tag key_of_application_record_v_payload k) : (application_record_v_payload_case_of_dvalue_kind k) =
  match k with
  | DValueNone -> [@inline_let] let _ = synth_application_record_v_payload_cases_recip_pre_intro DValueNone x in
    (match x with V_payload_DValueNone y -> (from_application_record_v_payload_case_of_dvalue_kind DValueNone y))
  | DValueSome -> [@inline_let] let _ = synth_application_record_v_payload_cases_recip_pre_intro DValueSome x in
    (match x with V_payload_DValueSome y -> (from_application_record_v_payload_case_of_dvalue_kind DValueSome y))

inline_for_extraction let application_record_v_payload_sum = LP.make_sum' dvalue_kind_enum key_of_application_record_v_payload
  application_record_v_payload_case_of_dvalue_kind synth_application_record_v_payload_cases synth_application_record_v_payload_cases_recip
  (_ by (LP.make_sum_synth_case_recip_synth_case_tac ()))
  (_ by (LP.synth_case_synth_case_recip_tac ()))

noextract let parse_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : k:LP.parser_kind & LP.parser k (application_record_v_payload_case_of_dvalue_kind x) =
  match x with
  | DValueNone -> [@inline_let] let u : (k: LP.parser_kind & LP.parser k (application_record_v_payload_case_of_dvalue_kind DValueNone)) = (| _, LP.parse_empty |) in u
  | DValueSome -> [@inline_let] let u : (k: LP.parser_kind & LP.parser k (application_record_v_payload_case_of_dvalue_kind DValueSome)) = (| _, application_value_parser |) in u
  | _ -> (| _, LP.parse_false |)

noextract let serialize_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LP.serializer (dsnd (parse_application_record_v_payload_cases x)) =
  match x with
  | DValueNone -> [@inline_let] let u : LP.serializer (dsnd (parse_application_record_v_payload_cases DValueNone)) = LP.serialize_empty in u
  | DValueSome -> [@inline_let] let u : LP.serializer (dsnd (parse_application_record_v_payload_cases DValueSome)) = application_value_serializer in u
  | _ -> LP.serialize_false

inline_for_extraction noextract let size32_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LSZ.size32 (serialize_application_record_v_payload_cases x) =
  match x with
  | DValueNone -> [@inline_let] let u : LSZ.size32 (serialize_application_record_v_payload_cases DValueNone) = LSZ.size32_empty in u
  | DValueSome -> [@inline_let] let u : LSZ.size32 (serialize_application_record_v_payload_cases DValueSome) = application_value_size32 in u
  | _ -> LSZ.size32_false

inline_for_extraction noextract let validate_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LL.validator (dsnd (parse_application_record_v_payload_cases x)) =
  match x with
  | DValueNone -> [@inline_let] let u : LL.validator (dsnd (parse_application_record_v_payload_cases DValueNone)) = (LL.validate_empty ()) in u
  | DValueSome -> [@inline_let] let u : LL.validator (dsnd (parse_application_record_v_payload_cases DValueSome)) = application_value_validator in u
  | _ -> LL.validate_false ()

inline_for_extraction noextract let jump_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LL.jumper (dsnd (parse_application_record_v_payload_cases x)) =
  match x with
  | DValueNone -> [@inline_let] let u : LL.jumper (dsnd (parse_application_record_v_payload_cases DValueNone)) = LL.jump_empty in u
  | DValueSome -> [@inline_let] let u : LL.jumper (dsnd (parse_application_record_v_payload_cases DValueSome)) = application_value_jumper in u
  | _ -> LL.jump_false

inline_for_extraction noextract let read_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LL.leaf_reader (dsnd (parse_application_record_v_payload_cases x)) =
  match x with
  | DValueNone -> [@inline_let] let u : LL.leaf_reader (dsnd (parse_application_record_v_payload_cases DValueNone)) = LL.read_empty in u
  | DValueSome -> [@inline_let] let u : LL.leaf_reader (dsnd (parse_application_record_v_payload_cases DValueSome)) = application_value_reader in u
  | _ -> LL.read_false

inline_for_extraction noextract let lserialize_application_record_v_payload_cases (x:LP.sum_key application_record_v_payload_sum)
  : LL.serializer32 (serialize_application_record_v_payload_cases x) =
  match x with
  | DValueNone -> [@inline_let] let u : LL.serializer32 (serialize_application_record_v_payload_cases DValueNone) = LL.serialize32_empty in u
  | DValueSome -> [@inline_let] let u : LL.serializer32 (serialize_application_record_v_payload_cases DValueSome) = application_value_lserializer in u
  | _ -> LL.serialize32_false

let application_record_v_payload_parser =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LP.parse_sum application_record_v_payload_sum dvalue_kind_repr_parser parse_application_record_v_payload_cases

let application_record_v_payload_serializer =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LP.serialize_sum application_record_v_payload_sum dvalue_kind_repr_serializer serialize_application_record_v_payload_cases

let application_record_v_payload_bytesize (x:application_record_v_payload) : GTot nat = Seq.length (application_record_v_payload_serializer x)

let application_record_v_payload_bytesize_eq x = ()

let application_record_v_payload_size32 =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  assert_norm (LSZ.size32_sum_gen_precond (LP.get_parser_kind dvalue_kind_repr_parser) (LP.weaken_parse_cases_kind application_record_v_payload_sum parse_application_record_v_payload_cases));
  LSZ.size32_sum2 application_record_v_payload_sum dvalue_kind_repr_serializer dvalue_kind_repr_size32 serialize_application_record_v_payload_cases size32_application_record_v_payload_cases (_ by (LP.dep_enum_destr_tac ())) (_ by (LP.enum_repr_of_key_tac dvalue_kind_enum)) ()

let application_record_v_payload_validator =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LL.validate_sum application_record_v_payload_sum dvalue_kind_repr_validator dvalue_kind_repr_reader parse_application_record_v_payload_cases validate_application_record_v_payload_cases (_ by (LP.dep_maybe_enum_destr_t_tac ()))

let application_record_v_payload_jumper =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LL.jump_sum application_record_v_payload_sum dvalue_kind_repr_jumper dvalue_kind_repr_reader parse_application_record_v_payload_cases jump_application_record_v_payload_cases (_ by (LP.dep_maybe_enum_destr_t_tac ()))

let application_record_v_payload_reader =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LL.read_sum application_record_v_payload_sum dvalue_kind_repr_parser read_dvalue_kind_key dvalue_kind_repr_jumper parse_application_record_v_payload_cases read_application_record_v_payload_cases (_ by (LP.dep_enum_destr_tac ()))

let application_record_v_payload_lserializer =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LL.serialize32_sum application_record_v_payload_sum dvalue_kind_repr_serializer lserialize_dvalue_kind_key serialize_application_record_v_payload_cases lserialize_application_record_v_payload_cases (_ by (LP.dep_enum_destr_tac ()))

let lemma_valid_application_record_v_payload_valid_dvalue_kind #_ #_ s pos h =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  LL.valid_sum_elim_tag h application_record_v_payload_sum dvalue_kind_repr_parser parse_application_record_v_payload_cases s pos;
  lemma_synth_dvalue_kind_inj ();
  LL.valid_synth h parse_dvalue_kind_key synth_dvalue_kind s pos

let application_record_v_payload_gaccessor_tag =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  lemma_synth_dvalue_kind_inj ();
  lemma_synth_dvalue_kind_inv ();
  LL.gaccessor_ext
    (LL.gaccessor_compose
      (LL.gaccessor_sum_tag application_record_v_payload_sum dvalue_kind_repr_parser parse_application_record_v_payload_cases)
      (LL.gaccessor_synth_inv parse_dvalue_kind_key synth_dvalue_kind synth_dvalue_kind_inv ())
    )
    application_record_v_payload_clens_tag
    ()

let application_record_v_payload_accessor_tag =
  assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
  lemma_synth_dvalue_kind_inj ();
  lemma_synth_dvalue_kind_inv ();
  LL.accessor_ext
    (LL.accessor_compose
      (LL.accessor_sum_tag application_record_v_payload_sum dvalue_kind_repr_parser parse_application_record_v_payload_cases)
      (LL.accessor_synth_inv parse_dvalue_kind_key synth_dvalue_kind synth_dvalue_kind_inv ())
      ()
    )
    application_record_v_payload_clens_tag
    ()

let application_record_v_payload_bytesize_eqn_DValueNone x =
    assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);

  LP.serialize_sum_eq application_record_v_payload_sum dvalue_kind_repr_serializer serialize_application_record_v_payload_cases (V_payload_DValueNone x);
  (let ln = FStar.Seq.length (LP.serialize (LP.serialize_enum_key _ dvalue_kind_repr_serializer (LP.sum_enum application_record_v_payload_sum)) (key_of_application_record_v_payload (V_payload_DValueNone x))) in assert (1 <= ln /\ ln <= 1));
  (assert (FStar.Seq.length (LP.serialize LP.serialize_empty (x)) == 0))

let application_record_v_payload_bytesize_eqn_DValueSome x =
    assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);

  LP.serialize_sum_eq application_record_v_payload_sum dvalue_kind_repr_serializer serialize_application_record_v_payload_cases (V_payload_DValueSome x);
  (let ln = FStar.Seq.length (LP.serialize (LP.serialize_enum_key _ dvalue_kind_repr_serializer (LP.sum_enum application_record_v_payload_sum)) (key_of_application_record_v_payload (V_payload_DValueSome x))) in assert (1 <= ln /\ ln <= 1));
  (application_value_bytesize_eq (x))

noextract let application_record_v_payload_clens'_DValueSome : LL.clens application_record_v_payload application_value = LL.clens_sum_payload application_record_v_payload_sum (dvalue_kind_as_enum_key DValueSome)

let application_record_v_payload_gaccessor'_DValueSome : LL.gaccessor application_record_v_payload_parser application_value_parser application_record_v_payload_clens'_DValueSome =
[@inline_let] let _ =   assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
 () in
  LL.gaccessor_clens_sum_payload
    application_record_v_payload_sum
    dvalue_kind_repr_parser
    parse_application_record_v_payload_cases
    (dvalue_kind_as_enum_key DValueSome)

inline_for_extraction
let application_record_v_payload_accessor'_DValueSome : LL.accessor application_record_v_payload_gaccessor'_DValueSome =
[@inline_let] let _ =   assert_norm (LP.parse_sum_kind (LP.get_parser_kind dvalue_kind_repr_parser) application_record_v_payload_sum parse_application_record_v_payload_cases == application_record_v_payload_parser_kind);
 () in
  LL.accessor_clens_sum_payload
    application_record_v_payload_sum
    dvalue_kind_repr_jumper
    parse_application_record_v_payload_cases
    (dvalue_kind_as_enum_key DValueSome)

let application_record_v_payload_clens_eq_DValueSome : squash (LL.clens_eq application_record_v_payload_clens'_DValueSome application_record_v_payload_clens_DValueSome) =
    (_ by (LL.sum_accessor_ext (`application_record_v_payload)))

let application_record_v_payload_gaccessor_DValueSome =
  LL.gaccessor_ext
    application_record_v_payload_gaccessor'_DValueSome
    application_record_v_payload_clens_DValueSome
    application_record_v_payload_clens_eq_DValueSome
/
Zeta.Formats.Aux.Dvalue_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.Application_record_v_payload.fst
LowParse.Low.Base.accessor Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_gaccessor_DValueSome

LowParse.Low.Base.accessor_ext Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_parser_kind Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_parser Zeta.Formats.Aux.Application_value.application_value_parser_kind Zeta.Formats.Aux.Application_value.application_value Zeta.Formats.Aux.Application_value.application_value_parser Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_clens'_DValueSome Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_gaccessor'_DValueSome Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_accessor'_DValueSome Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_clens_DValueSome Zeta.Formats.Aux.Application_record_v_payload.application_record_v_payload_clens_eq_DValueSome
let application_record_v_payload_accessor_DValueSome =
  
LL.accessor_ext application_record_v_payload_accessor'_DValueSome
  application_record_v_payload_clens_DValueSome
  application_record_v_payload_clens_eq_DValueSome