val valid_app_record : b: Zeta.Steel.LogEntry.Types.uninterpreted -> Prims.GTot Prims.logical
let valid_app_record (b: T.uninterpreted)
  = match ApplicationRecord.spec_parser_app_record b.ebytes with
    | None -> False
    | Some _ -> True
module Zeta.Steel.LogRel

(* This module sets up the relationship between steel log-related concepts and the corresponding spec level ones *)

open Zeta.App
open Zeta.Steel.KeyUtils
open Zeta.Steel.Rel

module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module L = FStar.List.Tot
module GK = Zeta.GenKey
module K = Zeta.Key
module M = Zeta.Merkle
module GV = Zeta.GenericVerifier
module IL = Zeta.Intermediate.Logs
module IV = Zeta.Intermediate.Verifier
module AT = Zeta.Steel.ApplicationTypes
module T = Zeta.Steel.FormatsManual
module TSM = Zeta.Steel.ThreadStateModel
module SA = Zeta.SeqAux
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.ApplicationRecord.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Logs.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked
Zeta.Steel.LogRel.fsti
b: Zeta.Steel.LogEntry.Types.uninterpreted -> Prims.GTot Prims.logical
Zeta.Steel.LogEntry.Types.uninterpreted Zeta.Steel.ApplicationRecord.spec_parser_app_record FStar.Ghost.reveal FStar.Seq.Base.seq FStar.UInt8.t Zeta.Steel.LogEntry.Types.__proj__Mkuninterpreted__item__ebytes Prims.l_False FStar.Pervasives.Native.tuple2 Zeta.Steel.ApplicationTypes.key_type FStar.Pervasives.Native.option Zeta.Steel.ApplicationTypes.value_type Prims.nat Prims.l_True Prims.logical
let valid_app_record (b: T.uninterpreted) =
  
match ApplicationRecord.spec_parser_app_record b.ebytes with
| None -> False
| Some _ -> True