val parse_arg (fid: i_fid) (b: T.uninterpreted{valid_app_param fid b}) : GTot (appfn_arg fid)
val parse_arg (fid: i_fid) (b: T.uninterpreted{valid_app_param fid b}) : GTot (appfn_arg fid)
let parse_arg (fid: i_fid) (b: T.uninterpreted {valid_app_param fid b})
  : GTot (appfn_arg fid)
  = let open T in
    let open AT in
    match spec_app_parser fid b.ebytes with
    | Some ((arg, _), _) -> arg
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)

let valid_app_fid (sfid: s_fid)
  = Map.contains app.tbl sfid

let lif_app_fid (sfid: s_fid {valid_app_fid sfid})
  : i_fid
  = sfid

let valid_app_param (fid: i_fid) (b: T.uninterpreted)
  = let open T in
    let open AT in
    match spec_app_parser fid b.ebytes with
    | None -> False
    | Some ((arg, slots), len) ->
      len == U32.v b.len /\
      (forall i. valid_slot (Seq.index slots i))
/
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

    fid: Zeta.Steel.Rel.i_fid ->
    b: Zeta.Steel.LogEntry.Types.uninterpreted{Zeta.Steel.LogRel.valid_app_param fid b}
  -> Prims.GTot (Zeta.App.appfn_arg fid)
Zeta.Steel.Rel.i_fid Zeta.Steel.LogEntry.Types.uninterpreted Zeta.Steel.LogRel.valid_app_param Zeta.Steel.ApplicationTypes.spec_app_parser FStar.Ghost.reveal FStar.Seq.Base.seq FStar.UInt8.t Zeta.Steel.LogEntry.Types.__proj__Mkuninterpreted__item__ebytes Zeta.Steel.ApplicationTypes.app_args Zeta.Steel.ApplicationTypes.slots Prims.nat Zeta.App.appfn_arg Zeta.Steel.Rel.app
let parse_arg (fid: i_fid) (b: T.uninterpreted{valid_app_param fid b}) : GTot (appfn_arg fid) =
  
let open T in let open AT in match spec_app_parser fid b.ebytes with | Some ((arg, _), _) -> arg