val log_entry_hdr_refine (k: LP.enum_key log_entry_kind_enum) (x: log_entry_hdr)
    : Pure (LP.refine_with_tag key_of_log_entry_hdr k)
      (requires norm [delta; iota; zeta] (key_of_log_entry_hdr x) == k)
      (ensures (fun y -> y == x))
val log_entry_hdr_refine (k: LP.enum_key log_entry_kind_enum) (x: log_entry_hdr)
    : Pure (LP.refine_with_tag key_of_log_entry_hdr k)
      (requires norm [delta; iota; zeta] (key_of_log_entry_hdr x) == k)
      (ensures (fun y -> y == x))
let log_entry_hdr_refine (k:LP.enum_key log_entry_kind_enum) (x:log_entry_hdr)
  : Pure (LP.refine_with_tag key_of_log_entry_hdr k)  (requires norm [delta; iota; zeta] (key_of_log_entry_hdr x) == k) (ensures (fun y -> y == x)) =
  [@inline_let] let _ = norm_spec [delta; iota; zeta] (key_of_log_entry_hdr x) in x
module Zeta.Formats.Aux.Log_entry_hdr

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

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

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

inline_for_extraction let key_of_log_entry_hdr (x:log_entry_hdr) : LP.enum_key log_entry_kind_enum =
  match x with
  | Le_payload_AddM _ -> log_entry_kind_as_enum_key AddM
  | Le_payload_AddB _ -> log_entry_kind_as_enum_key AddB
  | Le_payload_EvictM _ -> log_entry_kind_as_enum_key EvictM
  | Le_payload_EvictB _ -> log_entry_kind_as_enum_key EvictB
  | Le_payload_EvictBM _ -> log_entry_kind_as_enum_key EvictBM
  | Le_payload_NextEpoch _ -> log_entry_kind_as_enum_key NextEpoch
  | Le_payload_VerifyEpoch _ -> log_entry_kind_as_enum_key VerifyEpoch
  | Le_payload_RunApp _ -> log_entry_kind_as_enum_key RunApp

inline_for_extraction let log_entry_hdr_case_of_log_entry_kind (x:log_entry_kind) : Type0 =
  match x with
  | AddM -> addm_payload
  | AddB -> addb_payload
  | EvictM -> evictm_payload
  | EvictB -> evictb_payload
  | EvictBM -> evictbm_payload
  | NextEpoch -> unit
  | VerifyEpoch -> unit
  | RunApp -> runapp_payload_hdr

unfold inline_for_extraction let to_log_entry_hdr_case_of_log_entry_kind (x:log_entry_kind) (#x':log_entry_kind) (y:log_entry_hdr_case_of_log_entry_kind x')  : Pure (norm [delta_only [(`%log_entry_hdr_case_of_log_entry_kind)]; iota] (log_entry_hdr_case_of_log_entry_kind x))
  (requires (x == x')) (ensures (fun y' -> y' == y)) =
  [@inline_let] let _ = norm_spec [delta_only [(`%log_entry_hdr_case_of_log_entry_kind)] ; iota] (log_entry_hdr_case_of_log_entry_kind x) in y
/
Zeta.Formats.Aux.Log_entry_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.Log_entry_hdr.fst

    k: LowParse.Spec.Enum.enum_key Zeta.Formats.Aux.Log_entry_kind.log_entry_kind_enum ->
    x: Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr
  -> Prims.Pure
    (LowParse.Spec.Base.refine_with_tag Zeta.Formats.Aux.Log_entry_hdr.key_of_log_entry_hdr k)
LowParse.Spec.Enum.enum_key Zeta.Formats.Aux.Log_entry_kind.log_entry_kind FStar.UInt8.t Zeta.Formats.Aux.Log_entry_kind.log_entry_kind_enum Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr Prims.unit FStar.Pervasives.norm_spec Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta FStar.Pervasives.iota FStar.Pervasives.zeta Prims.Nil Zeta.Formats.Aux.Log_entry_hdr.key_of_log_entry_hdr LowParse.Spec.Base.refine_with_tag Prims.eq2 FStar.Pervasives.norm Zeta.Formats.Aux.Addm_payload.addm_payload Zeta.Formats.Aux.Log_entry_hdr.log_entry_kind_as_enum_key Zeta.Formats.Aux.Log_entry_kind.AddM Zeta.Formats.Aux.Addb_payload.addb_payload Zeta.Formats.Aux.Log_entry_kind.AddB Zeta.Formats.Aux.Evictm_payload.evictm_payload Zeta.Formats.Aux.Log_entry_kind.EvictM Zeta.Formats.Aux.Evictb_payload.evictb_payload Zeta.Formats.Aux.Log_entry_kind.EvictB Zeta.Formats.Aux.Evictbm_payload.evictbm_payload Zeta.Formats.Aux.Log_entry_kind.EvictBM Zeta.Formats.Aux.Log_entry_kind.NextEpoch Zeta.Formats.Aux.Log_entry_kind.VerifyEpoch Zeta.Formats.Aux.Runapp_payload_hdr.runapp_payload_hdr Zeta.Formats.Aux.Log_entry_kind.RunApp
let log_entry_hdr_refine (k: LP.enum_key log_entry_kind_enum) (x: log_entry_hdr)
    : Pure (LP.refine_with_tag key_of_log_entry_hdr k)
      (requires norm [delta; iota; zeta] (key_of_log_entry_hdr x) == k)
      (ensures (fun y -> y == x)) =
  
[@@ inline_let ]let _ = norm_spec [delta; iota; zeta] (key_of_log_entry_hdr x) in
x