val try_increment_max
      (#hashes_v #bitmaps_v #mlogs_v: erased _)
      (hashes: all_epoch_hashes)
      (bitmaps: epoch_tid_bitmaps)
      (max: R.ref (option M.epoch_id))
    : STT bool
      (((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
          `star`
          (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
        `star`
        (exists_ (fun max_v ->
                (R.pts_to max full max_v)
                `star`
                (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v mlogs_v)))))
      (fun b ->
          ((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
            `star`
            (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
          `star`
          (exists_ (fun (max_v': option M.epoch_id) ->
                  (R.pts_to max full max_v')
                  `star`
                  (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)))))
val try_increment_max
      (#hashes_v #bitmaps_v #mlogs_v: erased _)
      (hashes: all_epoch_hashes)
      (bitmaps: epoch_tid_bitmaps)
      (max: R.ref (option M.epoch_id))
    : STT bool
      (((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
          `star`
          (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
        `star`
        (exists_ (fun max_v ->
                (R.pts_to max full max_v)
                `star`
                (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v mlogs_v)))))
      (fun b ->
          ((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
            `star`
            (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
          `star`
          (exists_ (fun (max_v': option M.epoch_id) ->
                  (R.pts_to max full max_v')
                  `star`
                  (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)))))
let try_increment_max (#hashes_v:erased _)
                      (#bitmaps_v:erased _)
                      (#mlogs_v:erased _)
                      (hashes: all_epoch_hashes)
                      (bitmaps: epoch_tid_bitmaps)
                      (max:R.ref (option M.epoch_id))
  : STT bool
    (EpochMap.full_perm hashes M.init_epoch_hash hashes_v `star`
     EpochMap.full_perm bitmaps all_zeroes bitmaps_v `star`
     exists_ (fun max_v ->
       R.pts_to max full max_v `star`
       pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v mlogs_v)))
    (fun b ->
      EpochMap.full_perm hashes M.init_epoch_hash hashes_v `star`
      EpochMap.full_perm bitmaps all_zeroes bitmaps_v `star`
      exists_ (fun (max_v':option M.epoch_id) ->
        R.pts_to max full max_v' `star`
        pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)))
  = let max_v = elim_exists () in
    let e = R.read max in
    let v =  //v is the epoch we will try to certify
      match e with
      | None -> Some 0ul  //if previous value of max epoch id is None, try for 0th
      | Some e -> check_overflow_add32 e 1ul in
    match v with
    | None ->
      intro_exists_erased max_v (fun max_v' ->
        R.pts_to max full max_v' `star`
        pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v));
      return false

    | Some e' ->
      let ready = check_bitmap_for_epoch bitmaps e' in
      if not ready
      then (
        intro_exists_erased max_v (fun max_v' ->
          R.pts_to max full max_v' `star`
          pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v));
        return false
      )
      else (
        let b = check_hash_equality_for_epoch hashes e' in
        if not b
        then (
          intro_exists_erased max_v (fun max_v' ->
            R.pts_to max full max_v' `star`
            pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v));
          return false
        )
        else (
          R.write max (Some e');
          elim_pure _;
          intro_pure (hashes_bitmaps_max_ok hashes_v bitmaps_v (Some e') mlogs_v);
          intro_exists (Some e') (fun max_v' ->
            R.pts_to max full max_v' `star`
            pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v));
           return true
        )
      )
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

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

let check_bitmap_for_epoch (#bm:erased _)
                           (tid_bitmaps: epoch_tid_bitmaps)
                           (e:M.epoch_id)
  : ST bool
    (EpochMap.full_perm tid_bitmaps all_zeroes bm)
    (fun b -> EpochMap.full_perm tid_bitmaps all_zeroes bm)
    (requires True)
    (ensures fun b -> b ==> Map.sel bm e == all_ones)
  = let res = EpochMap.get tid_bitmaps e in
    match res with
    | EpochMap.Found a ->
      rewrite (EpochMap.get_post all_zeroes bm EpochMap.empty_borrows tid_bitmaps e res)
              (EpochMap.perm tid_bitmaps all_zeroes bm (PartialMap.upd EpochMap.empty_borrows e a) `star`
               array_pts_to a (Map.sel bm e));
      let b = check_all_ones a in
      EpochMap.ghost_put tid_bitmaps e a _;
      return b

    | _ ->
      rewrite (EpochMap.get_post all_zeroes bm EpochMap.empty_borrows tid_bitmaps e res)
              (EpochMap.full_perm tid_bitmaps all_zeroes bm);
      return false

let check_hash_equality_for_epoch (#hashes_v:erased epoch_hashes_repr)
                                  (hashes:all_epoch_hashes)
                                  (e:M.epoch_id)
  : ST bool
    (EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
    (fun _ -> EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
    (requires True)
    (ensures fun b ->
      let ha = Map.sel hashes_v e in
      b ==> ha.hadd == ha.hevict)
  = let res = EpochMap.get hashes e in
    match res with
    | EpochMap.Found ehs ->
      rewrite (EpochMap.get_post M.init_epoch_hash hashes_v EpochMap.empty_borrows hashes e res)
              (EpochMap.perm hashes M.init_epoch_hash hashes_v (PartialMap.upd EpochMap.empty_borrows e ehs) `star`
               epoch_hash_perm e ehs (Map.sel hashes_v e));
      rewrite (epoch_hash_perm e ehs (Map.sel hashes_v e)) //TODO: mark epoch_hash_perm reduce
              (HA.ha_val ehs.hadd (Map.sel hashes_v e).hadd `star`
               HA.ha_val ehs.hevict (Map.sel hashes_v e).hevict);
      let b = HA.compare ehs.hadd ehs.hevict in
      rewrite (HA.ha_val ehs.hadd (Map.sel hashes_v e).hadd `star`
               HA.ha_val ehs.hevict (Map.sel hashes_v e).hevict)
              (epoch_hash_perm e ehs (Map.sel hashes_v e));
      EpochMap.ghost_put hashes e ehs _;
      return  b

    | _ ->
      rewrite (EpochMap.get_post M.init_epoch_hash hashes_v EpochMap.empty_borrows hashes e res)
              (EpochMap.full_perm hashes M.init_epoch_hash hashes_v);
      return false

let epoch_ready_if_bitmap_set (hashes:epoch_hashes_repr)
                              (bitmaps:epoch_bitmaps_repr)
                              (max:_)
                              (mlogs_v:_)
                              (e:M.epoch_id)
  : Lemma
    (requires
      Some? max /\
      hashes_bitmaps_max_ok hashes bitmaps max mlogs_v /\
      Map.sel bitmaps e == all_ones)
    (ensures
      epoch_is_complete mlogs_v e /\
      Map.sel hashes e == aggregate_all_threads_epoch_hashes e mlogs_v)
  = ()

let _max_is_correct (hashes:_)
                    (bitmaps:_)
                    (max:_)
                    (mlogs_v:_)
  : Lemma
    (requires Some? max /\ hashes_bitmaps_max_ok hashes bitmaps max mlogs_v)
    (ensures  max_is_correct mlogs_v (Some?.v max))
  = ()
/
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

    hashes: Zeta.Steel.AggregateEpochHashes.all_epoch_hashes ->
    bitmaps: Zeta.Steel.AggregateEpochHashes.epoch_tid_bitmaps ->
    max:
      Steel.ST.Reference.ref (FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.epoch_id)
  -> Steel.ST.Effect.STT Prims.bool
FStar.Ghost.erased Zeta.Steel.AggregateEpochHashes.epoch_hashes_repr Zeta.Steel.AggregateEpochHashes.epoch_bitmaps_repr Zeta.Steel.AggregateEpochHashes.all_processed_entries Zeta.Steel.AggregateEpochHashes.all_epoch_hashes Zeta.Steel.AggregateEpochHashes.epoch_tid_bitmaps Steel.ST.Reference.ref FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.epoch_id Steel.ST.Util.return Prims.bool FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.Effect.Common.VStar Zeta.Steel.EpochMap.perm Zeta.Steel.EpochHashes.epoch_hashes_t Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.EpochHashes.epoch_hash_perm Zeta.Steel.ThreadStateModel.init_epoch_hash FStar.Ghost.reveal Zeta.Steel.EpochMap.empty_borrows Zeta.Steel.Util.larray Zeta.Steel.ApplicationTypes.n_threads Zeta.Steel.AggregateEpochHashes.tid_bitmap Steel.ST.Array.array FStar.Seq.Base.seq Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm Steel.Effect.Common.vprop Zeta.Steel.AggregateEpochHashes.all_zeroes Steel.ST.Util.exists_ Steel.ST.Reference.pts_to Zeta.Steel.Util.full Steel.ST.Util.pure Zeta.Steel.AggregateEpochHashes.hashes_bitmaps_max_ok Prims.unit Steel.ST.Util.intro_exists_erased Steel.Effect.Common.star FStar.UInt32.t Prims.op_Negation Steel.ST.Util.intro_exists FStar.Pervasives.Native.Some Steel.ST.Util.intro_pure Steel.ST.Util.elim_pure Steel.ST.Reference.write Zeta.Steel.AggregateEpochHashes.check_hash_equality_for_epoch Zeta.Steel.AggregateEpochHashes.check_bitmap_for_epoch FStar.UInt32.__uint_to_t Zeta.Steel.Util.check_overflow_add32 Steel.ST.Reference.read Steel.ST.Util.elim_exists Zeta.Steel.EpochMap.full_perm Zeta.Steel.Util.array_pts_to
let try_increment_max
      (#hashes_v #bitmaps_v #mlogs_v: erased _)
      (hashes: all_epoch_hashes)
      (bitmaps: epoch_tid_bitmaps)
      (max: R.ref (option M.epoch_id))
    : STT bool
      (((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
          `star`
          (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
        `star`
        (exists_ (fun max_v ->
                (R.pts_to max full max_v)
                `star`
                (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v mlogs_v)))))
      (fun b ->
          ((EpochMap.full_perm hashes M.init_epoch_hash hashes_v)
            `star`
            (EpochMap.full_perm bitmaps all_zeroes bitmaps_v))
          `star`
          (exists_ (fun (max_v': option M.epoch_id) ->
                  (R.pts_to max full max_v')
                  `star`
                  (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v))))) =
  
let max_v = elim_exists () in
let e = R.read max in
let v =
  match e with
  | None -> Some 0ul
  | Some e -> check_overflow_add32 e 1ul
in
match v with
| None ->
  intro_exists_erased max_v
    (fun max_v' ->
        (R.pts_to max full max_v')
        `star`
        (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)));
  return false
| Some e' ->
  let ready = check_bitmap_for_epoch bitmaps e' in
  if not ready
  then
    (intro_exists_erased max_v
        (fun max_v' ->
            (R.pts_to max full max_v')
            `star`
            (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)));
      return false)
  else
    (let b = check_hash_equality_for_epoch hashes e' in
      if not b
      then
        (intro_exists_erased max_v
            (fun max_v' ->
                (R.pts_to max full max_v')
                `star`
                (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)));
          return false)
      else
        (R.write max (Some e');
          elim_pure _;
          intro_pure (hashes_bitmaps_max_ok hashes_v bitmaps_v (Some e') mlogs_v);
          intro_exists (Some e')
            (fun max_v' ->
                (R.pts_to max full max_v')
                `star`
                (pure (hashes_bitmaps_max_ok hashes_v bitmaps_v max_v' mlogs_v)));
          return true))