val all_add_sets_equiv (e: epoch_id) (logs: verifiable_logs)
    : Lemma (requires (AH.epoch_is_certified (as_tid_logs logs) e))
      (ensures
        map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd)
          (as_tid_logs logs) ==
        Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e))
val all_add_sets_equiv (e: epoch_id) (logs: verifiable_logs)
    : Lemma (requires (AH.epoch_is_certified (as_tid_logs logs) e))
      (ensures
        map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd)
          (as_tid_logs logs) ==
        Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e))
let all_add_sets_equiv (e:epoch_id) (logs:verifiable_logs)
  : Lemma 
    (requires (AH.epoch_is_certified (as_tid_logs logs) e))
    (ensures 
      map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd) (as_tid_logs logs) ==
      Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e))
  = let s0 = map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd) (as_tid_logs logs) in
    map_ghost_spec (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd) (as_tid_logs logs);
    let s1 = Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e) in
    introduce forall i. Seq.index s0 i == Seq.index s1 i
    with (
      let tid, l = Seq.index (as_tid_logs logs) i in
      let tsm = TSM.verify_model (TSM.init_thread_state_model tid) l in
      valid_spec_rel_tsm tid l;
      assert (AH.is_epoch_verified tsm e);
      calc (==) {
        Seq.index s0 i;
      (==) { }
        (Map.sel (AH.thread_contrib_of_log tid l) e).hadd;
      (==) { thread_contrib_of_log_for_epoch e tid l }
        ms_hashfn (ThreadRel.add_set tsm (lift_epoch e));
      };
      Zeta.SeqAux.lemma_map_index ms_hashfn (all_add_sets (to_tsms logs) e) i
    );
    assert (Seq.equal s0 s1)
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)

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);
    ()

let aggregate_add_hash (logs: all_logs) (ep: epoch_id)
  : GTot hash_value_t
  = let aeh = AH.aggregate_all_threads_epoch_hashes ep (as_tid_logs logs) in
    aeh.hadd

let aggregate_evict_hash (logs: all_logs) (ep: epoch_id)
  : GTot hash_value_t
  = let aeh = AH.aggregate_all_threads_epoch_hashes ep (as_tid_logs logs) in
    aeh.hevict
  
let certified_epoch_aggregate_hashes_equal (logs: all_logs) (ep: epoch_id {AH.epoch_is_certified (as_tid_logs logs) ep})
  : Lemma (ensures (aggregate_add_hash logs ep == aggregate_evict_hash logs ep))
  = ()

let all_valid_tsms = tsms: Seq.seq thread_state_model
    { forall i. ThreadRel.valid (Seq.index tsms i) }

let all_epoch_completed (ep: epoch_id) (tsms: Seq.seq thread_state_model)
  = forall (i:Zeta.SeqAux.seq_index tsms). AH.is_epoch_verified (Seq.index tsms i) ep
  
let all_add_sets  (tsms: all_valid_tsms) (ep: epoch_id)
  : GTot (Seq.seq mset)
  = let i_ep = lift_epoch ep in
    Seq.init_ghost (Seq.length tsms) (fun i -> add_set (Seq.index tsms i) i_ep)

let all_evict_sets  (tsms: all_valid_tsms) (ep: epoch_id)
  : GTot (Seq.seq mset)
  = let i_ep = lift_epoch ep in
    Seq.init_ghost (Seq.length tsms) (fun i -> evict_set (Seq.index tsms i) i_ep)

let all_add_sets_cons (tsms: all_valid_tsms {Seq.length tsms > 0}) (ep: epoch_id)
  : Lemma (ensures (let add_sets = all_add_sets tsms ep in
                    let i_ep = lift_epoch ep in
                    Seq.tail add_sets == all_add_sets (Seq.tail tsms) ep /\
                    Seq.head add_sets == add_set (Seq.head tsms) i_ep))
  = let add_sets = all_add_sets tsms ep in
    let i_ep = lift_epoch ep in
    assert (Seq.head add_sets == add_set (Seq.head tsms) i_ep);
    let tail = Seq.tail tsms in

    let tail_add_sets = Seq.tail add_sets in
    let add_sets_tail = all_add_sets tail ep in

    let aux (i:_)
      : Lemma (ensures (Seq.index add_sets_tail i == Seq.index tail_add_sets i))
      = ()
    in
    forall_intro aux;
    assert(Seq.equal add_sets_tail tail_add_sets);
    ()

let union_all_add_set (tsms: all_valid_tsms) (ep: epoch_id)
  : GTot mset
  =  union_all (all_add_sets tsms ep)

let union_all_evict_set (tsms: all_valid_tsms) (ep: epoch_id)
  : GTot mset
  = let i_ep= lift_epoch ep in
    let sms = Seq.init_ghost (Seq.length tsms) (fun i -> evict_set (Seq.index tsms i) i_ep) in
    union_all sms

let to_tsms (logs: verifiable_logs)
  : all_valid_tsms
  = let tid_logs = as_tid_logs logs in
    let tsms = Zeta.SeqAux.map (fun (tid, _) -> AH.tsm_of_log tid_logs tid) tid_logs in
    assert (forall (tid:tid). Seq.index tsms (U16.v tid) == AH.tsm_of_log tid_logs tid);
    introduce forall (tid:tid). let tsm = AH.tsm_of_log tid_logs tid in 
                           not (tsm.failed) /\
                           tsm.thread_id == tid /\
                           tsm == run tid tsm.processed_entries
    with (
      let tsm = AH.tsm_of_log tid_logs tid in
      TSM.verify_model_thread_id_inv (init_thread_state_model tid) 
                                     (AH.log_of_tid tid_logs tid);
      TSM.tsm_entries_invariant_steps tid (AH.log_of_tid tid_logs tid)                                     
    );
    tsms


#push-options "--fuel 1 --ifuel 1 --query_stats"
let valid_spec_rel_tsm (t:tid) (l:log)
  : Lemma 
    (let tsm = TSM.verify_model (TSM.init_thread_state_model t) l in
     tsm.failed \/ (
     ThreadRel.valid tsm /\
     ThreadRel.spec_rel tsm))
  = let tsm = TSM.verify_model (TSM.init_thread_state_model t) l in
    TSM.tsm_entries_invariant_steps t l;
    if tsm.failed
    then ()
    else (
      ThreadRel.valid_implies_spec_rel tsm
    )


let thread_contrib_of_log_for_epoch (e:epoch_id) (t:tid) (l:log) 
  : Lemma 
    (requires (
      let tsm = TSM.verify_model (TSM.init_thread_state_model t) l in
      AH.is_epoch_verified tsm e))
    (ensures (
      let tsm = TSM.verify_model (TSM.init_thread_state_model t) l in    
      valid_spec_rel_tsm t l;
      Map.sel (AH.thread_contrib_of_log t l) e ==  Map.sel tsm.epoch_hashes e /\
      (Map.sel tsm.epoch_hashes e == ({ hadd = ms_hashfn (ThreadRel.add_set tsm (lift_epoch e));
                                        hevict = ms_hashfn (ThreadRel.evict_set tsm (lift_epoch e))}))))
  = let tsm = TSM.verify_model (TSM.init_thread_state_model t) l in
    valid_spec_rel_tsm t l;
    ThreadRel.valid_hadd_prop e tsm;
    ThreadRel.valid_hevict_prop e tsm

let rec map_ghost (f:'a -> GTot 'b) (x:Seq.seq 'a)
  : GTot (Seq.seq 'b)
         (decreases (Seq.length x))
  = if Seq.length x = 0 then Seq.empty
    else let prefix, last = Seq.un_snoc x in
         Seq.snoc (map_ghost f prefix) (f last)

let rec map_ghost_spec (f:'a -> GTot 'b) (x:Seq.seq 'a)
  : Lemma (ensures (Seq.length (map_ghost f x) == Seq.length x /\
                   (forall (i:Zeta.SeqAux.seq_index x).
                     Seq.index (map_ghost f x) i == f (Seq.index x i))))
          (decreases (Seq.length x))
  = if Seq.length x = 0 then ()
    else let prefix, last = Seq.un_snoc x in
         map_ghost_spec f prefix
/
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
e: Zeta.Steel.ThreadStateModel.epoch_id -> logs: Zeta.Steel.GlobalRel.verifiable_logs
  -> FStar.Pervasives.Lemma
      (requires
        Zeta.Steel.AggregateEpochHashes.epoch_is_certified (Zeta.Steel.GlobalRel.as_tid_logs logs) e
      )
      (ensures
        Zeta.Steel.GlobalRel.map_ghost (fun tid_l ->
              Mkepoch_hash?.hadd (FStar.Map.sel (Zeta.Steel.AggregateEpochHashes.thread_contrib_of_log
                        (FStar.Pervasives.Native.fst tid_l)
                        (FStar.Pervasives.Native.snd tid_l))
                    e))
          (Zeta.Steel.GlobalRel.as_tid_logs logs) ==
        Zeta.SeqAux.map Zeta.Steel.MultiSetHash.ms_hashfn
          (Zeta.Steel.GlobalRel.all_add_sets (Zeta.Steel.GlobalRel.to_tsms logs) e))
Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.GlobalRel.verifiable_logs Prims._assert FStar.Seq.Base.equal Zeta.Steel.ThreadStateModel.model_hash Prims.unit FStar.Classical.Sugar.forall_intro Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.eq2 FStar.Seq.Base.index Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadStateModel.log Zeta.SeqAux.lemma_map_index Zeta.Steel.MultiSetHash.mset Zeta.Steel.HashAccumulator.hash_value_t Zeta.Steel.MultiSetHash.ms_hashfn Zeta.Steel.GlobalRel.all_add_sets Zeta.Steel.GlobalRel.to_tsms FStar.Calc.calc_finish Zeta.Steel.ThreadRel.add_set Zeta.Steel.Rel.lift_epoch Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hadd FStar.Map.sel Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.AggregateEpochHashes.thread_contrib_of_log FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Zeta.Steel.GlobalRel.thread_contrib_of_log_for_epoch Zeta.Steel.AggregateEpochHashes.is_epoch_verified Zeta.Steel.GlobalRel.valid_spec_rel_tsm Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.verify_model Zeta.Steel.ThreadStateModel.init_thread_state_model FStar.Pervasives.Native.tuple2 Zeta.Steel.GlobalRel.as_tid_logs FStar.Seq.Base.seq Prims.op_Equality Zeta.SeqAux.map Zeta.Steel.GlobalRel.map_ghost_spec Zeta.Steel.AggregateEpochHashes.log FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd Zeta.Steel.GlobalRel.map_ghost Zeta.Steel.AggregateEpochHashes.epoch_is_certified FStar.Pervasives.pattern
let all_add_sets_equiv (e: epoch_id) (logs: verifiable_logs)
    : Lemma (requires (AH.epoch_is_certified (as_tid_logs logs) e))
      (ensures
        map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd)
          (as_tid_logs logs) ==
        Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e)) =
  
let s0 =
  map_ghost (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd)
    (as_tid_logs logs)
in
map_ghost_spec (fun tid_l -> (Map.sel (AH.thread_contrib_of_log (fst tid_l) (snd tid_l)) e).hadd)
  (as_tid_logs logs);
let s1 = Zeta.SeqAux.map ms_hashfn (all_add_sets (to_tsms logs) e) in
introduce forall i . Seq.index s0 i == Seq.index s1 i
with (let tid, l = Seq.index (as_tid_logs logs) i in
  let tsm = TSM.verify_model (TSM.init_thread_state_model tid) l in
  valid_spec_rel_tsm tid l;
  assert (AH.is_epoch_verified tsm e);
  calc ( == ) {
    Seq.index s0 i;
    ( == ) { () }
    (Map.sel (AH.thread_contrib_of_log tid l) e).hadd;
    ( == ) { thread_contrib_of_log_for_epoch e tid l }
    ms_hashfn (ThreadRel.add_set tsm (lift_epoch e));
  };
  Zeta.SeqAux.lemma_map_index ms_hashfn (all_add_sets (to_tsms logs) e) i);
assert (Seq.equal s0 s1)