val log_entry_hdr_clens_AddM:LL.clens log_entry_hdr addm_payload
val log_entry_hdr_clens_AddM:LL.clens log_entry_hdr addm_payload
let log_entry_hdr_clens_AddM : LL.clens log_entry_hdr addm_payload = {
  LL.clens_cond = (fun (x: log_entry_hdr) -> tag_of_log_entry_hdr x == AddM);
  LL.clens_get = (fun (x: log_entry_hdr) -> (match x with Le_payload_AddM y -> y) <: (Ghost addm_payload (requires (tag_of_log_entry_hdr x == AddM)) (ensures (fun y -> True))));
}
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

inline_for_extraction noextract let log_entry_hdr_parser_kind = LP.strong_parser_kind 1 4095 None

noextract val log_entry_hdr_parser: LP.parser log_entry_hdr_parser_kind log_entry_hdr

noextract val log_entry_hdr_serializer: LP.serializer log_entry_hdr_parser

noextract val log_entry_hdr_bytesize (x:log_entry_hdr) : GTot nat

noextract val log_entry_hdr_bytesize_eq (x:log_entry_hdr) : Lemma (log_entry_hdr_bytesize x == Seq.length (LP.serialize log_entry_hdr_serializer x))

val log_entry_hdr_size32: LSZ.size32 log_entry_hdr_serializer

val log_entry_hdr_validator: LL.validator log_entry_hdr_parser

val log_entry_hdr_jumper: LL.jumper log_entry_hdr_parser

val log_entry_hdr_reader : LL.leaf_reader log_entry_hdr_parser

val log_entry_hdr_lserializer: LL.serializer32 log_entry_hdr_serializer

val lemma_valid_log_entry_hdr_valid_log_entry_kind: #rrel: _ -> #rel: _ -> s:LL.slice rrel rel -> pos:U32.t -> h:HyperStack.mem -> Lemma
  (requires LL.valid log_entry_hdr_parser h s pos)
  (ensures (LL.valid log_entry_kind_parser h s pos /\ LL.contents log_entry_kind_parser h s pos == tag_of_log_entry_hdr (LL.contents log_entry_hdr_parser h s pos)))
  [SMTPat (LL.valid log_entry_hdr_parser h s pos)]

noextract let log_entry_hdr_clens_tag : LL.clens log_entry_hdr log_entry_kind = {
  LL.clens_cond = (fun _ -> True);
  LL.clens_get = (fun (x: log_entry_hdr) -> tag_of_log_entry_hdr x);
}

val log_entry_hdr_gaccessor_tag : LL.gaccessor log_entry_hdr_parser log_entry_kind_parser log_entry_hdr_clens_tag

val log_entry_hdr_accessor_tag : LL.accessor log_entry_hdr_gaccessor_tag

val log_entry_hdr_bytesize_eqn_AddM (x: addm_payload) : Lemma (log_entry_hdr_bytesize (Le_payload_AddM x) == 1 + (addm_payload_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_AddM x))]

val log_entry_hdr_bytesize_eqn_AddB (x: addb_payload) : Lemma (log_entry_hdr_bytesize (Le_payload_AddB x) == 1 + (addb_payload_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_AddB x))]

val log_entry_hdr_bytesize_eqn_EvictM (x: evictm_payload) : Lemma (log_entry_hdr_bytesize (Le_payload_EvictM x) == 1 + (evictm_payload_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_EvictM x))]

val log_entry_hdr_bytesize_eqn_EvictB (x: evictb_payload) : Lemma (log_entry_hdr_bytesize (Le_payload_EvictB x) == 1 + (evictb_payload_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_EvictB x))]

val log_entry_hdr_bytesize_eqn_EvictBM (x: evictbm_payload) : Lemma (log_entry_hdr_bytesize (Le_payload_EvictBM x) == 1 + (evictbm_payload_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_EvictBM x))]

val log_entry_hdr_bytesize_eqn_NextEpoch (x: unit) : Lemma (log_entry_hdr_bytesize (Le_payload_NextEpoch x) == 1 + 0) [SMTPat (log_entry_hdr_bytesize (Le_payload_NextEpoch x))]

val log_entry_hdr_bytesize_eqn_VerifyEpoch (x: unit) : Lemma (log_entry_hdr_bytesize (Le_payload_VerifyEpoch x) == 1 + 0) [SMTPat (log_entry_hdr_bytesize (Le_payload_VerifyEpoch x))]

val log_entry_hdr_bytesize_eqn_RunApp (x: runapp_payload_hdr) : Lemma (log_entry_hdr_bytesize (Le_payload_RunApp x) == 1 + (runapp_payload_hdr_bytesize (x))) [SMTPat (log_entry_hdr_bytesize (Le_payload_RunApp x))]
/
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.Low.Base.Spec.clens Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr
  Zeta.Formats.Aux.Addm_payload.addm_payload
LowParse.Low.Base.Spec.Mkclens Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr Zeta.Formats.Aux.Addm_payload.addm_payload Prims.eq2 Zeta.Formats.Aux.Log_entry_kind.log_entry_kind Zeta.Formats.Aux.Log_entry_hdr.tag_of_log_entry_hdr Zeta.Formats.Aux.Log_entry_kind.AddM Prims.l_True
let log_entry_hdr_clens_AddM:LL.clens log_entry_hdr addm_payload =
  
{
  LL.clens_cond = (fun (x: log_entry_hdr) -> tag_of_log_entry_hdr x == AddM);
  LL.clens_get
  =
  (fun (x: log_entry_hdr) ->
      (match x with | Le_payload_AddM y -> y)
      <:
      (Ghost addm_payload (requires (tag_of_log_entry_hdr x == AddM)) (ensures (fun y -> True))))
}