val valid_app_fid : sfid: Zeta.Steel.Rel.s_fid -> Prims.bool
let valid_app_fid (sfid: s_fid)
  = Map.contains app.tbl sfid
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

let valid_app_record (b: T.uninterpreted)
  = match ApplicationRecord.spec_parser_app_record b.ebytes with
    | None -> False
    | Some _ -> True

let parse_app_record_local (b: T.uninterpreted {valid_app_record b})
  : GTot s_record
  = let open AT in
    let open T in
    match ApplicationRecord.spec_parser_app_record b.ebytes with
    | Some ((k,v), _) -> (ApplicationKey k, DValue v)
/
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
sfid: Zeta.Steel.Rel.s_fid -> Prims.bool
Zeta.Steel.Rel.s_fid FStar.Map.contains Zeta.App.fn_id Zeta.App.fn_sig Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.Rel.app Zeta.App.__proj__Mkapp_params__item__tbl Prims.bool
let valid_app_fid (sfid: s_fid) =
  
Map.contains app.tbl sfid