val all_app_fcrs_rel (ep: epoch_id) (logs: verifiable_logs)
  : Lemma (ensures (let s_fcrs = all_app_fcrs ep logs in
                    let i_logs = to_ilog logs in
                    let i_ep = lift_epoch ep in
                    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
                    s_fcrs = i_fcrs))
val all_app_fcrs_rel (ep: epoch_id) (logs: verifiable_logs)
  : Lemma (ensures (let s_fcrs = all_app_fcrs ep logs in
                    let i_logs = to_ilog logs in
                    let i_ep = lift_epoch ep in
                    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
                    s_fcrs = i_fcrs))
let all_app_fcrs_rel (ep: epoch_id) (logs: verifiable_logs)
  : Lemma (ensures (let s_fcrs = all_app_fcrs ep logs in
                    let i_logs = to_ilog logs in
                    let i_ep = lift_epoch ep in
                    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
                    s_fcrs = i_fcrs))
  = let s_fcrs = all_app_fcrs ep logs in
    let i_logs = to_ilog logs in
    let i_ep = lift_epoch ep in
    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in

    let aux (i:_)
      : Lemma (ensures (Seq.index s_fcrs i == Seq.index i_fcrs i))
      = let t = U16.uint_to_t i in
        let tl = index logs t in
        assert(app_fcrs ep tl == Seq.index s_fcrs i);
        spec_rel_implies_same_fcrs ep tl;
        ()
    in
    forall_intro aux;
    assert(Seq.equal s_fcrs i_fcrs);
    ()
module Zeta.Steel.GlobalRel

open FStar.Classical
open Zeta.MultiSet.SSeq
module GT = Zeta.Generic.Thread
module TSM = Zeta.Steel.ThreadStateModel
module HA = Zeta.Steel.HashAccumulator
module MS = Zeta.MultiSet
module ThreadRel = Zeta.Steel.ThreadRel

let to_ilog_idx (logs: verifiable_logs) (i: nat{i < n_threads_v})
  : GTot (l:i_log {GT.verifiable (i,l)})
  = let t = U16.uint_to_t i in
    let tl = index logs t in
    let tsm = to_tsm tl in
    let (_,l) = to_ilog tsm in
    l

let to_ilog (logs: verifiable_logs)
  : GTot (i_logs: i_verifiable_logs {Seq.length i_logs = n_threads_v})
  = Seq.init_ghost n_threads_v (fun i -> to_ilog_idx logs i)
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRel.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.SSeq.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.SSeq.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Zeta.Steel.GlobalRel.fst
ep: Zeta.Steel.ThreadStateModel.epoch_id -> logs: Zeta.Steel.GlobalRel.verifiable_logs
  -> FStar.Pervasives.Lemma
    (ensures
      (let s_fcrs = Zeta.Steel.GlobalRel.all_app_fcrs ep logs in
        let i_logs = Zeta.Steel.GlobalRel.to_ilog logs in
        let i_ep = Zeta.Steel.Rel.lift_epoch ep in
        let i_fcrs = Zeta.Generic.Global.app_fcrs_within_ep i_ep i_logs in
        s_fcrs = i_fcrs))
Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.GlobalRel.verifiable_logs Prims.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.seq Zeta.AppSimulate.appfn_call_res Zeta.Steel.Rel.app FStar.Classical.forall_intro Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.Steel.Thread.spec_rel_implies_same_fcrs Zeta.Steel.Thread.app_fcrs Zeta.Steel.Thread.verifiable_log Zeta.Steel.GlobalRel.index FStar.UInt16.t FStar.UInt16.uint_to_t Zeta.SSeq.sseq Zeta.Generic.Global.app_fcrs_within_ep Zeta.Steel.Rel.i_epoch Zeta.Steel.Rel.lift_epoch Zeta.Steel.GlobalRel.i_verifiable_logs Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size Zeta.GenericVerifier.verifier_log Zeta.Steel.GlobalRel.n_threads_v Zeta.Steel.GlobalRel.to_ilog Zeta.Steel.GlobalRel.all_app_fcrs
let all_app_fcrs_rel (ep: epoch_id) (logs: verifiable_logs)
    : Lemma
    (ensures
      (let s_fcrs = all_app_fcrs ep logs in
        let i_logs = to_ilog logs in
        let i_ep = lift_epoch ep in
        let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
        s_fcrs = i_fcrs)) =
  
let s_fcrs = all_app_fcrs ep logs in
let i_logs = to_ilog logs in
let i_ep = lift_epoch ep in
let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
let aux (i: _) : Lemma (ensures (Seq.index s_fcrs i == Seq.index i_fcrs i)) =
  let t = U16.uint_to_t i in
  let tl = index logs t in
  assert (app_fcrs ep tl == Seq.index s_fcrs i);
  spec_rel_implies_same_fcrs ep tl;
  ()
in
forall_intro aux;
assert (Seq.equal s_fcrs i_fcrs);
()