val log_entry_hdr_parser_kind : LowParse.Spec.Base.parser_kind
let log_entry_hdr_parser_kind = LP.strong_parser_kind 1 4095 None
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.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 Zeta.Formats.Aux.Log_entry_kind
open Zeta.Formats.Aux.Addm_payload
open Zeta.Formats.Aux.Addb_payload
open Zeta.Formats.Aux.Evictm_payload
open Zeta.Formats.Aux.Evictb_payload
open Zeta.Formats.Aux.Evictbm_payload
open Zeta.Formats.Aux.Runapp_payload_hdr

type log_entry_hdr =
  | Le_payload_AddM of addm_payload
  | Le_payload_AddB of addb_payload
  | Le_payload_EvictM of evictm_payload
  | Le_payload_EvictB of evictb_payload
  | Le_payload_EvictBM of evictbm_payload
  | Le_payload_NextEpoch of unit
  | Le_payload_VerifyEpoch of unit
  | Le_payload_RunApp of runapp_payload_hdr

inline_for_extraction let tag_of_log_entry_hdr (x:log_entry_hdr) : log_entry_kind = match x with
  | Le_payload_AddM _ -> AddM
  | Le_payload_AddB _ -> AddB
  | Le_payload_EvictM _ -> EvictM
  | Le_payload_EvictB _ -> EvictB
  | Le_payload_EvictBM _ -> EvictBM
  | Le_payload_NextEpoch _ -> NextEpoch
  | Le_payload_VerifyEpoch _ -> VerifyEpoch
  | Le_payload_RunApp _ -> RunApp
/
Zeta.Formats.Aux.Runapp_payload_hdr.fsti.checked Zeta.Formats.Aux.Log_entry_kind.fsti.checked Zeta.Formats.Aux.Evictm_payload.fsti.checked Zeta.Formats.Aux.Evictbm_payload.fsti.checked Zeta.Formats.Aux.Evictb_payload.fsti.checked Zeta.Formats.Aux.Addm_payload.fsti.checked Zeta.Formats.Aux.Addb_payload.fsti.checked prims.fst.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
Zeta.Formats.Aux.Log_entry_hdr.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some
let log_entry_hdr_parser_kind =
  
LP.strong_parser_kind 1 4095 None