val valid_log : l: Zeta.Steel.Rel.s_log -> Prims.logical
let valid_log (l: s_log)
  = forall i. (valid_log_entry (Seq.index l i))
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))

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

let parse_slots (fid: _) (b: T.uninterpreted {valid_app_param fid b})
  : GTot (Seq.seq s_slot_id)
  = let open T in
    let open AT in
    match spec_app_parser fid b.ebytes with
    | Some ((_,slots),_) -> slots

let valid_log_entry (e: s_log_entry)
  = let open Zeta.Steel.LogEntry.Types in
    match e with
    | AddM s s' r -> valid_slot s /\ valid_slot s' /\ True
    | AddB s ts tid r -> valid_slot s /\ True
    | EvictM e -> valid_slot e.s /\ valid_slot e.s_ /\ True
    | EvictB e -> valid_slot e.s /\ True
    | EvictBM e -> valid_slot e.s /\ valid_slot e.s_ /\ True
    | RunApp e -> valid_app_fid e.fid /\
                 valid_app_param e.fid e.rest /\
                 True
    | _ -> True

let related_log_entry (se: s_log_entry) (ie: i_log_entry)
  = let open Zeta.Steel.LogEntry.Types in
    match se, ie with
    | AddM s s' r, GV.AddM i_r i_s i_s'  ->
      related_record r i_r /\
      related_slot s i_s /\
      related_slot s' i_s'
    | AddB s t tid r, GV.AddB i_r i_s i_t i_tid ->
      related_record r i_r /\
      related_slot s i_s /\
      related_timestamp t i_t /\
      related_tid tid i_tid
    | EvictM p, GV.EvictM s s' ->
      related_slot p.s s /\
      related_slot p.s_ s'
    | EvictB p, GV.EvictB s t ->
      related_slot p.s s /\
      related_timestamp p.t t
    | EvictBM p, GV.EvictBM s s' t ->
      related_slot p.s s /\
      related_slot p.s_ s' /\
      related_timestamp p.t t
    | NextEpoch, GV.NextEpoch ->
      True
    | VerifyEpoch, GV.VerifyEpoch ->
      True
    | RunApp p, GV.RunApp f arg is ->
      p.fid = f /\
      valid_app_param f p.rest /\
      parse_arg f p.rest = arg /\
      (let ss = parse_slots f p.rest in
       Seq.length ss = Seq.length is /\
       (forall i. related_slot (Seq.index ss i) (Seq.index is i)))
    | _ -> False

val lift_log_entry (se: s_log_entry {valid_log_entry se})
  : GTot (ie: i_log_entry { related_log_entry se ie })
/
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
l: Zeta.Steel.Rel.s_log -> Prims.logical
Zeta.Steel.Rel.s_log Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.LogRel.valid_log_entry FStar.Seq.Base.index Prims.logical
let valid_log (l: s_log) =
  
forall i. (valid_log_entry (Seq.index l i))