val all_zeroes : FStar.Seq.Base.seq Prims.bool
let all_zeroes = Seq.create (U32.v n_threads) false
module Zeta.Steel.AggregateEpochHashes

open FStar.Ghost
open Steel.ST.Util
module A = Steel.ST.Array
module R = Steel.ST.Reference
module G = Steel.ST.GhostReference
module Lock = Steel.ST.CancellableSpinLock
open Zeta.Steel.ApplicationTypes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.FormatsManual
module EpochMap = Zeta.Steel.EpochMap
module T = Zeta.Steel.FormatsManual
module M = Zeta.Steel.ThreadStateModel
module HA = Zeta.Steel.HashAccumulator
open Zeta.Steel.Util
module MR = Steel.ST.MonotonicReference
module TLM = Zeta.Steel.ThreadLogMap
open Zeta.Steel.EpochHashes

#push-options "--ide_id_info_off"

let tid_bitmap = Seq.lseq bool (U32.v n_threads)
let epoch_hashes_repr = EpochMap.repr M.epoch_hash
let epoch_bitmaps_repr = EpochMap.repr tid_bitmap

let all_epoch_hashes = EpochMap.tbl epoch_hash_perm

let epoch_tid_bitmaps =
  EpochMap.tbl #(larray bool n_threads)
               #tid_bitmap
               (fun i -> array_pts_to)

let is_epoch_verified (tsm:M.thread_state_model) (eid:M.epoch_id) =
  not tsm.failed &&
  not (M.epoch_greater_than_last_verified_epoch tsm.last_verified_epoch eid)

let all_threads_epoch_hashes =
  Seq.lseq epoch_hashes_repr (U32.v n_threads)

let aggregate_epoch_hash (e0 e1:M.epoch_hash)
  : M.epoch_hash
  = { hadd = HA.aggregate_hashes e0.hadd e1.hadd;
      hevict = HA.aggregate_hashes e0.hevict e1.hevict}

let aggregate_epoch_hash_unit (i:M.epoch_hash)
  : Lemma (aggregate_epoch_hash M.init_epoch_hash i == i)
          [SMTPat (aggregate_epoch_hash M.init_epoch_hash i)]
  = HA.initial_hash_unit i.hadd;
    HA.initial_hash_unit i.hevict

let aggregate_epoch_hash_comm (i j:M.epoch_hash)
  : Lemma (aggregate_epoch_hash i j == aggregate_epoch_hash j i)
  = HA.aggregate_hashes_commutative i.hadd j.hadd;
    HA.aggregate_hashes_commutative i.hevict j.hevict

let aggregate_epoch_hash_assoc (i j k:M.epoch_hash)
  : Lemma (aggregate_epoch_hash (aggregate_epoch_hash i j) k ==
           aggregate_epoch_hash i (aggregate_epoch_hash j k))
  = HA.aggregate_hashes_associative i.hadd j.hadd k.hadd;
    HA.aggregate_hashes_associative i.hevict j.hevict k.hevict

module CE = FStar.Algebra.CommMonoid.Equiv

let aggregate_epoch_hash_equiv 
  : CE.equiv M.epoch_hash 
  = CE.EQ ( == ) (fun _ -> ()) (fun _ _ -> ()) (fun _ _ _ -> ())
let aggregate_epoch_hash_monoid
  : CE.cm M.epoch_hash aggregate_epoch_hash_equiv
  = CE.CM M.init_epoch_hash
       aggregate_epoch_hash
       aggregate_epoch_hash_unit
       aggregate_epoch_hash_assoc
       aggregate_epoch_hash_comm
       (fun _ _ _ _ -> ())

let log = Seq.seq log_entry

let tid_logs = Seq.seq (tid & log)

let maybe_log_of_tid (l:tid_logs) (t:tid)
  : option (tid & log)
  = Seq.find_r (fun (t', _) -> t' = t) l
  
let all_tid_logs = Seq.lseq (tid & log) (U32.v n_threads)
    
let thread_contrib_of_log (t:tid) (l:log)
  : epoch_hashes_repr
  = let tsm = M.verify_model (M.init_thread_state_model t) l in
    FStar.Map.map_literal
      (fun (e:M.epoch_id) ->
         if is_epoch_verified tsm e
         then Map.sel tsm.epoch_hashes e
         else M.init_epoch_hash)

let all_threads_epoch_hashes_of_logs (mlogs_v:Seq.seq (tid & log))
  : mlogs_v':Seq.seq epoch_hashes_repr { Seq.length mlogs_v' == Seq.length mlogs_v }
  = Zeta.SeqAux.map (fun tid_l -> thread_contrib_of_log (fst tid_l) (snd tid_l)) mlogs_v
                   
let aggregate_epoch_hashes_seq (epoch_hashes:Seq.seq M.epoch_hash)
  : M.epoch_hash
  = FStar.Seq.Permutation.foldm_snoc aggregate_epoch_hash_monoid epoch_hashes

let aggregate_all_threads_epoch_hashes (e:M.epoch_id)
                                       (mlogs_v:Seq.seq (tid & log))
  : M.epoch_hash
  = aggregate_epoch_hashes_seq (Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e)
                                                (all_threads_epoch_hashes_of_logs mlogs_v))

let split_tid (mlogs_v:Seq.lseq 'a (U32.v n_threads))
              (t:tid)
  = let prefix= Seq.slice mlogs_v 0 (U16.v t) in
    let suffix = Seq.slice mlogs_v (U16.v t + 1) (U32.v n_threads) in
    prefix, Seq.index mlogs_v (U16.v t), suffix

let aggregate_all_threads_epoch_hashes_seq_permute (ehs:Seq.lseq M.epoch_hash (U32.v n_threads))
                                                   (t:tid)
  : Lemma (
      let prefix, et, suffix = split_tid ehs t in
      aggregate_epoch_hashes_seq ehs ==
      aggregate_epoch_hash et (aggregate_epoch_hashes_seq (Seq.append prefix suffix)))
  = let open FStar.Seq.Permutation in
    let seq_lhs = ehs in
    let seq_prefix, i, seq_suffix = split_tid seq_lhs t in
    let seq_rhs = Seq.snoc (Seq.append seq_prefix seq_suffix) i in
    let permutation_fun
      : index_fun seq_lhs
      = fun l -> 
          if l < U16.v t
          then l
          else if l > U16.v t
          then l - 1
          else Seq.length seq_lhs - 1
    in
    FStar.Seq.Permutation.reveal_is_permutation seq_lhs seq_rhs permutation_fun;
    assert (is_permutation seq_lhs seq_rhs permutation_fun);
    FStar.Seq.Permutation.foldm_snoc_perm aggregate_epoch_hash_monoid seq_lhs seq_rhs permutation_fun;
    assert (aggregate_epoch_hashes_seq seq_lhs == aggregate_epoch_hashes_seq seq_rhs);
    let s, last = Seq.un_snoc seq_rhs in
    Seq.un_snoc_snoc (Seq.append seq_prefix seq_suffix) i;
    assert (s `Seq.equal` Seq.append seq_prefix seq_suffix); ()

let rec all_threads_epoch_hashes_of_logs_append (mlogs_v mlogs_v':Seq.seq (tid & log))
  : Lemma (ensures
             (all_threads_epoch_hashes_of_logs (mlogs_v `Seq.append` mlogs_v'))  `Seq.equal`
             (all_threads_epoch_hashes_of_logs mlogs_v `Seq.append` all_threads_epoch_hashes_of_logs mlogs_v'))
          (decreases (Seq.length mlogs_v'))
  = if Seq.length mlogs_v' = 0 then ()
    else (
      let prefix, last = Seq.un_snoc mlogs_v' in
      all_threads_epoch_hashes_of_logs_append mlogs_v prefix
    )


let all_processed_entries = 
    s:all_tid_logs { forall (i:nat{i < Seq.length s}). U16.v (fst (Seq.index s i)) == i }

let aggregate_all_threads_epoch_hashes_permute (e:M.epoch_id)
                                               (mlogs_v:all_processed_entries)
                                               (t:tid)
  : Lemma (
      let prefix, et, suffix = split_tid mlogs_v t in
      aggregate_all_threads_epoch_hashes e mlogs_v ==
      aggregate_epoch_hash
        (Map.sel (thread_contrib_of_log t (snd et)) e)
        (aggregate_all_threads_epoch_hashes e (Seq.append prefix suffix)))
  = let lprefix, et, lsuffix = split_tid mlogs_v t in
    let lhs = Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e)
                              (all_threads_epoch_hashes_of_logs mlogs_v) in
    aggregate_all_threads_epoch_hashes_seq_permute lhs t;
    let prefix, it, suffix = split_tid lhs t in
    let f = (fun (s:epoch_hashes_repr) -> Map.sel s e) in
    let lp_ls = (Seq.append lprefix lsuffix) in
    let lmap = (Zeta.SeqAux.map f (all_threads_epoch_hashes_of_logs lp_ls)) in
    let ps = (Seq.append prefix suffix) in
    assert (Seq.equal (Zeta.SeqAux.map f (all_threads_epoch_hashes_of_logs lp_ls))
                      (Seq.append prefix suffix))

(* Global monotonic log of entries *)

let map_of_seq (a:all_processed_entries)
  : TLM.repr
  = FStar.Map.map_literal (fun (tid:tid) -> Some (snd (Seq.index a (U16.v tid))))

let log_of_tid (a:all_processed_entries) (t:tid) = snd (Seq.index a (U16.v t))
    
let tsm_of_log (mlogs_v:all_processed_entries) (t:tid) =
  M.verify_model (M.init_thread_state_model t)
                 (log_of_tid mlogs_v t)

let committed_tsm_of_logs (mlogs_v:all_processed_entries) (t:tid) =
   M.verify_model (M.init_thread_state_model t)
                  (M.committed_log_entries (log_of_tid mlogs_v t))

let all_contributions_are_accurate (global:epoch_hashes_repr)
                                   (mlogs_v:all_processed_entries)
  : prop
  = forall (e:M.epoch_id). Map.sel global e == aggregate_all_threads_epoch_hashes e mlogs_v
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadLogMap.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.EpochMap.fsti.checked Zeta.Steel.EpochHashes.fst.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.SeqAux.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.MonotonicReference.fsti.checked Steel.ST.GhostReference.fsti.checked Steel.ST.CancellableSpinLock.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Zeta.Steel.AggregateEpochHashes.fsti
FStar.Seq.Base.seq Prims.bool
FStar.Seq.Base.create Prims.bool FStar.UInt32.v Zeta.Steel.ApplicationTypes.n_threads
let all_zeroes =
  
Seq.create (U32.v n_threads) false