val check_all_ones (#e: Ghost.erased _) (a: larray bool n_threads)
    : ST bool
      (array_pts_to a e)
      (fun _ -> array_pts_to a e)
      (requires True)
      (ensures fun b -> b <==> (reveal e == all_ones))
val check_all_ones (#e: Ghost.erased _) (a: larray bool n_threads)
    : ST bool
      (array_pts_to a e)
      (fun _ -> array_pts_to a e)
      (requires True)
      (ensures fun b -> b <==> (reveal e == all_ones))
let check_all_ones (#e:Ghost.erased _)
                   (a:larray bool n_threads)
  : ST bool
    (array_pts_to a e)
    (fun _ -> array_pts_to a e)
    (requires True)
    (ensures fun b -> b <==> (reveal e == all_ones))
  = A.pts_to_length a e;
    let b = Steel.ST.Array.Util.for_all (SizeT.uint32_to_sizet n_threads) a (fun b -> b) in
    assert (b ==> Seq.equal (reveal e) all_ones);
    return b
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
module SA = Zeta.SeqAux
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

inline_for_extraction
let max_epoch_lag = 32ul
let all_hashes_size : n:U32.t{U32.v n > 0} = max_epoch_lag
let tid_bitmaps_size : n:U32.t{U32.v n > 0} = max_epoch_lag

let empty_all_processed_entries : Ghost.erased all_processed_entries =
  Seq.init #(tid & log) (U32.v n_threads) (fun i -> U16.uint_to_t i, Seq.empty)

let rec aggregate_epoch_hashes_seq_unit (s:Seq.seq M.epoch_hash)
  : Lemma
    (requires
      forall i. Seq.index s i == M.init_epoch_hash)
    (ensures
      aggregate_epoch_hashes_seq s == M.init_epoch_hash)
    (decreases Seq.length s)
  = if Seq.length s = 0 then ()
    else (
      let prefix, last = Seq.un_snoc s in
      Seq.un_snoc_snoc prefix last;
      calc (==) {
        aggregate_epoch_hashes_seq s;
        (==) {}
        aggregate_epoch_hash last (aggregate_epoch_hashes_seq prefix);
        (==) { aggregate_epoch_hash_unit (aggregate_epoch_hashes_seq prefix) }
        aggregate_epoch_hashes_seq prefix;
        (==) { aggregate_epoch_hashes_seq_unit prefix }
        M.init_epoch_hash;
      }
    )

let aggregate_all_threads_epoch_hashes_emp ()
  : Lemma (forall (e:M.epoch_id).
             aggregate_all_threads_epoch_hashes e empty_all_processed_entries ==
             M.init_epoch_hash)
  = assert (forall tid. Map.equal (thread_contrib_of_log (U16.uint_to_t tid) (snd (Seq.index empty_all_processed_entries tid)))
                             (Map.const M.init_epoch_hash));
    let all_init = (Seq.create (U32.v n_threads) (Map.const M.init_epoch_hash)) in
    assert (Seq.equal (all_threads_epoch_hashes_of_logs empty_all_processed_entries)
                      all_init);
    introduce forall (e:M.epoch_id).
                aggregate_all_threads_epoch_hashes e empty_all_processed_entries ==
                M.init_epoch_hash
    with (
      calc (==) {
        aggregate_all_threads_epoch_hashes e empty_all_processed_entries;
       (==) {}
        aggregate_epoch_hashes_seq (Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e) all_init);
       (==) { aggregate_epoch_hashes_seq_unit (Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e) all_init) }
        M.init_epoch_hash;
      }
    )

let per_thread_bitmap_and_max_emp (tid:tid) (eid:M.epoch_id)
  : Lemma
      (let tsm = M.verify_model (M.init_thread_state_model tid) Seq.empty in
       is_epoch_verified tsm eid == false)
  = ()

let create () =
  let hashes = EpochMap.create #_ #_ #epoch_hash_perm
    all_hashes_size
    (Ghost.hide M.init_epoch_hash) in
  let tid_bitmaps = EpochMap.create #(larray bool n_threads) #tid_bitmap #(fun i -> array_pts_to)
    tid_bitmaps_size
    (Ghost.hide all_zeroes) in
  let max_certified_epoch = R.alloc #(option M.epoch_id) None in
  let mlogs = TLM.alloc () in

  assert (Map.equal (map_of_seq empty_all_processed_entries)
                    (Map.const (Some (Seq.empty #log_entry))));

  rewrite (TLM.global_anchor mlogs (Map.const (Some Seq.empty)))
          (TLM.global_anchor mlogs (map_of_seq empty_all_processed_entries));

  aggregate_all_threads_epoch_hashes_emp ();
  assert (all_contributions_are_accurate (Map.const M.init_epoch_hash)
                                         empty_all_processed_entries);

  Classical.forall_intro_2 per_thread_bitmap_and_max_emp;
  intro_pure (hashes_bitmaps_max_ok (Map.const M.init_epoch_hash)
                                    (Map.const all_zeroes)
                                    None
                                    empty_all_processed_entries);

  intro_exists (Ghost.reveal empty_all_processed_entries)
               (fun mlogs_v ->
                lock_inv_body _ _ _ _
                  (Map.const M.init_epoch_hash)
                  (Map.const all_zeroes)
                  None
                  mlogs_v);

  intro_exists None
               (fun max -> exists_ (fun mlogs_v ->
                lock_inv_body _ _ _ _
                  (Map.const M.init_epoch_hash)
                  (Map.const all_zeroes)
                  max
                  mlogs_v));

  intro_exists (Map.const all_zeroes)
               (fun bitmaps_v -> exists_ (fun max -> exists_ (fun mlogs_v ->
                lock_inv_body _ _ _ _
                  (Map.const M.init_epoch_hash)
                  bitmaps_v
                  max
                  mlogs_v)));

  intro_exists (Map.const M.init_epoch_hash)
               (fun hashes_v -> (exists_ (fun bitmaps_v -> exists_ (fun max -> exists_ (fun mlogs_v ->
                lock_inv_body _ _ _ _
                  hashes_v
                  bitmaps_v
                  max
                  mlogs_v)))));

  let lock = Lock.new_cancellable_lock (lock_inv _ _ _ _) in

  let aeh = {hashes; tid_bitmaps; max_certified_epoch; mlogs; lock} in

  rewrite (TLM.tids_pts_to _ _ _ _)
          (TLM.tids_pts_to aeh.mlogs full_perm (Map.const (Some Seq.empty)) false);

  return aeh
/
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.Loops.Util.fsti.checked Steel.ST.GhostReference.fsti.checked Steel.ST.CancellableSpinLock.fsti.checked Steel.ST.Array.Util.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.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Steel.AggregateEpochHashes.fst
a: Zeta.Steel.Util.larray Prims.bool Zeta.Steel.ApplicationTypes.n_threads
  -> Steel.ST.Effect.ST Prims.bool
FStar.Ghost.erased FStar.Seq.Base.seq Prims.bool Zeta.Steel.Util.larray Zeta.Steel.ApplicationTypes.n_threads Steel.ST.Util.return FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm FStar.Ghost.reveal Steel.Effect.Common.vprop Prims.unit Prims._assert Prims.l_imp Prims.b2t FStar.Seq.Base.equal Zeta.Steel.AggregateEpochHashes.all_ones Steel.ST.Array.Util.for_all FStar.SizeT.uint32_to_sizet Steel.ST.Array.pts_to_length Zeta.Steel.Util.array_pts_to Prims.l_True Prims.l_iff Prims.eq2
let check_all_ones (#e: Ghost.erased _) (a: larray bool n_threads)
    : ST bool
      (array_pts_to a e)
      (fun _ -> array_pts_to a e)
      (requires True)
      (ensures fun b -> b <==> (reveal e == all_ones)) =
  
A.pts_to_length a e;
let b = Steel.ST.Array.Util.for_all (SizeT.uint32_to_sizet n_threads) a (fun b -> b) in
assert (b ==> Seq.equal (reveal e) all_ones);
return b