val lift_log_entry (se: s_log_entry {valid_log_entry se})
  : GTot (ie: i_log_entry { related_log_entry se ie })
val lift_log_entry (se: s_log_entry {valid_log_entry se})
  : GTot (ie: i_log_entry { related_log_entry se ie })
let lift_log_entry (se: s_log_entry {valid_log_entry se})
  : GTot (ie: i_log_entry { related_log_entry se ie })
  = let open Zeta.Steel.LogEntry.Types in
    let open Zeta.Steel.Rel in
    match se with
    | AddM s s' r ->
      let i_r = lift_record r in
      let i_s = lift_slot s in
      let i_s' = lift_slot s' in
      GV.AddM i_r i_s i_s'

    | AddB s t tid r ->
      let i_r = lift_record r in
      let i_s = lift_slot s in
      let i_t = lift_timestamp t in
      let i_tid = lift_tid tid in
      GV.AddB i_r i_s i_t i_tid

    | EvictM p ->
      GV.EvictM (lift_slot p.s) (lift_slot p.s_)

    
    | EvictB p ->
      GV.EvictB (lift_slot p.s) (lift_timestamp p.t)

    | EvictBM p ->
      GV.EvictBM (lift_slot p.s) (lift_slot p.s_) (lift_timestamp p.t)

    | NextEpoch ->
      GV.NextEpoch

    | VerifyEpoch ->
      GV.VerifyEpoch

    | RunApp p ->
      GV.RunApp p.fid (parse_arg p.fid p.rest) (lift_slots (parse_slots p.fid p.rest))
module Zeta.Steel.LogRel

module GV = Zeta.GenericVerifier

let rec map_ghost (p:'a -> Type0) 
                  (s:Seq.seq 'a { forall (i:Zeta.SeqAux.seq_index s). p (Seq.index s i) })
                  (f: (x:'a { p x } -> GTot 'b))
  : GTot (s':Seq.seq 'b { Seq.length s == Seq.length s' /\
                         (forall (i:Zeta.SeqAux.seq_index s). Seq.index s' i == f (Seq.index s i)) })
         (decreases (Seq.length s))
  = if Seq.length s = 0 then Seq.empty
    else (
      let prefix, last = Seq.un_snoc s in
      Seq.snoc (map_ghost p prefix f) (f last)
    )
                           
let lift_slots (s:Seq.seq s_slot_id { forall (i:Zeta.SeqAux.seq_index s). valid_slot (Seq.index s i)  })
  : GTot (is:Seq.seq i_slot_id  { Seq.length s = Seq.length is /\
                                  (forall i. related_slot (Seq.index s i) (Seq.index is i)) })
         (decreases (Seq.length s))
  = map_ghost (fun x -> valid_slot x) s lift_slot
/
Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.SeqAux.fsti.checked Zeta.GenericVerifier.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.LogRel.fst
se: Zeta.Steel.Rel.s_log_entry{Zeta.Steel.LogRel.valid_log_entry se}
  -> Prims.GTot (ie: Zeta.Steel.Rel.i_log_entry{Zeta.Steel.LogRel.related_log_entry se ie})
Zeta.Steel.Rel.s_log_entry Zeta.Steel.LogRel.valid_log_entry Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.LogEntry.Types.record Zeta.GenericVerifier.AddM Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.Steel.Rel.i_slot_id Zeta.Steel.Rel.lift_slot Zeta.Steel.Rel.i_record Zeta.Steel.Rel.related_record Zeta.Steel.Rel.lift_record Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.LogEntry.Types.thread_id Zeta.GenericVerifier.AddB Zeta.Steel.Rel.i_tid Zeta.Steel.Rel.lift_tid Zeta.Steel.Rel.i_timestamp Zeta.Steel.Rel.lift_timestamp Zeta.Steel.LogEntry.Types.evictM_payload Zeta.GenericVerifier.EvictM Zeta.Steel.LogEntry.Types.__proj__MkevictM_payload__item__s Zeta.Steel.LogEntry.Types.__proj__MkevictM_payload__item__s_ Zeta.Steel.LogEntry.Types.evictB_payload Zeta.GenericVerifier.EvictB Zeta.Steel.LogEntry.Types.__proj__MkevictB_payload__item__s Zeta.Steel.LogEntry.Types.__proj__MkevictB_payload__item__t Zeta.Steel.LogEntry.Types.evictBM_payload Zeta.GenericVerifier.EvictBM Zeta.Steel.LogEntry.Types.__proj__MkevictBM_payload__item__s Zeta.Steel.LogEntry.Types.__proj__MkevictBM_payload__item__s_ Zeta.Steel.LogEntry.Types.__proj__MkevictBM_payload__item__t Zeta.GenericVerifier.NextEpoch Zeta.GenericVerifier.VerifyEpoch Zeta.Steel.LogEntry.Types.runApp_payload Zeta.GenericVerifier.RunApp Zeta.Steel.LogEntry.Types.__proj__MkrunApp_payload__item__fid Zeta.Steel.LogRel.parse_arg Zeta.Steel.LogEntry.Types.__proj__MkrunApp_payload__item__rest Zeta.Steel.LogRel.lift_slots Zeta.Steel.LogRel.parse_slots Zeta.Steel.Rel.i_log_entry Zeta.Steel.LogRel.related_log_entry
let lift_log_entry (se: s_log_entry{valid_log_entry se})
    : GTot (ie: i_log_entry{related_log_entry se ie}) =
  
let open Zeta.Steel.LogEntry.Types in
let open Zeta.Steel.Rel in
match se with
| AddM s s' r ->
  let i_r = lift_record r in
  let i_s = lift_slot s in
  let i_s' = lift_slot s' in
  GV.AddM i_r i_s i_s'
| AddB s t tid r ->
  let i_r = lift_record r in
  let i_s = lift_slot s in
  let i_t = lift_timestamp t in
  let i_tid = lift_tid tid in
  GV.AddB i_r i_s i_t i_tid
| EvictM p -> GV.EvictM (lift_slot p.s) (lift_slot p.s_)
| EvictB p -> GV.EvictB (lift_slot p.s) (lift_timestamp p.t)
| EvictBM p -> GV.EvictBM (lift_slot p.s) (lift_slot p.s_) (lift_timestamp p.t)
| NextEpoch -> GV.NextEpoch
| VerifyEpoch -> GV.VerifyEpoch
| RunApp p -> GV.RunApp p.fid (parse_arg p.fid p.rest) (lift_slots (parse_slots p.fid p.rest))