val aggregate_epoch_hash (b0 b1: bool) (e0 e1: M.epoch_hash) : M.epoch_hash
val aggregate_epoch_hash (b0 b1: bool) (e0 e1: M.epoch_hash) : M.epoch_hash
let aggregate_epoch_hash (b0 b1:bool) (e0 e1:M.epoch_hash)
  : M.epoch_hash
  = { hadd = update_if b0 e0.hadd (HA.aggregate_hashes e0.hadd e1.hadd);
      hevict = update_if b1 e0.hevict (HA.aggregate_hashes e0.hevict e1.hevict) }
module Zeta.Steel.VerifierSteps
friend Zeta.Steel.VerifierTypes
open Zeta.Steel.VerifierTypes
open FStar.Ghost
open Steel.ST.Util
module G = Steel.ST.GhostReference
module R = Steel.ST.Reference
module A = Steel.ST.Array
module Lock = Steel.ST.CancellableSpinLock
module TLM = Zeta.Steel.ThreadLogMap
open Zeta.Steel.ApplicationTypes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.LogEntry
open Zeta.Steel.Util
open Zeta.Steel.IV
module T = Zeta.Steel.FormatsManual
module M = Zeta.Steel.ThreadStateModel
module AEH = Zeta.Steel.AggregateEpochHashes
module Cast = FStar.Int.Cast
open Zeta.Steel.EpochHashes
module KU = Zeta.Steel.KeyUtils
module EH = Zeta.Steel.EpochHashes
module HA = Zeta.Steel.HashAccumulator
#push-options "--ide_id_info_off"
#push-options "--query_stats --fuel 0 --ifuel 1"


let fail (#tsm:M.thread_state_model)
         (t:thread_state_t)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.fail tsm))
  = R.write t.failed true

let fail_as (#tsm:M.thread_state_model)
            (t:thread_state_t)
            (tsm':M.thread_state_model)
  : ST bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm tsm'))
    (requires tsm' == M.fail tsm)
    (ensures fun _ -> True)
  = R.write t.failed true;
    let b = true in
    intro_thread_state_inv_core (update_if b tsm tsm') t;
    return b


let extend_processed_entries #o
                             (#tsm:M.thread_state_model)
                             (t:thread_state_t)
                             (le:log_entry)
  : STGhost unit o
    (thread_state_inv_core t (M.verify_log_entry tsm le))
    (fun _ -> thread_state_inv t (M.verify_step_model tsm le))
    (requires
      not tsm.failed /\
      tsm_entries_invariant tsm /\
      t.thread_id == tsm.thread_id /\
      not (VerifyEpoch? le))
    (ensures fun _ -> True)
  = M.tsm_entries_invariant_verify_step tsm le;
    rewrite
        (thread_state_inv_core t _)
        (thread_state_inv_core t (M.verify_log_entry tsm le));
    G.write t.processed_entries (Seq.snoc tsm.processed_entries le);
    intro_thread_state_inv_core (M.verify_step_model tsm le) t;
    intro_thread_state_inv t

let maybe_extend_processed_entries #o
                                   (#tsm:M.thread_state_model)
                                   (t:thread_state_t)
                                   (b:bool)
                                   (le:log_entry)
  : STGhost unit o
    (thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm le)))
    (fun _ -> thread_state_inv t (update_if b tsm (M.verify_step_model tsm le)))
    (requires
      not tsm.failed /\
      tsm_entries_invariant tsm /\
      t.thread_id == tsm.thread_id /\
      not (VerifyEpoch? le))
    (ensures fun _ -> True)
  = if b
    then (
      rewrite
        (thread_state_inv_core t _)
        (thread_state_inv_core t (M.verify_log_entry tsm le));
      extend_processed_entries t le;
      rewrite
        (thread_state_inv t _)
        (thread_state_inv t (update_if b tsm (M.verify_step_model tsm le)))
    )
    else (
      rewrite (thread_state_inv_core t _)
              (thread_state_inv_core t (update_if b tsm (M.verify_step_model tsm le)));
      intro_thread_state_inv t
    )

let to_base_key (x:T.key)
  : ST T.base_key
    emp (fun _ -> emp)
    (requires True)
    (ensures fun b -> b == M.to_base_key x)
  = match x with
    | InternalKey k -> return k
    | ApplicationKey k ->
      let k' = Zeta.Steel.Application.key_type_to_base_key k in
      return k'

////////////////////////////////////////////////////////////////////////////////
//check_failed
////////////////////////////////////////////////////////////////////////////////

let check_failed #tsm t
  = elim_thread_state_inv t;
    let b = R.read t.failed in
    intro_thread_state_inv t;
    return b

////////////////////////////////////////////////////////////////////////////////
//vaddm
////////////////////////////////////////////////////////////////////////////////

#push-options "--ifuel 2"
let rewrite_with_squash #o (p q:vprop)
                        (f:unit -> squash (p == q))
  : STGhostT unit o p (fun _ -> q)
  = f();
    rewrite p q


let spec_madd_to_store_split (tsm:M.thread_state_model)
                        (s:slot)
                        (k:key)
                        (v:T.value)
                        (s':slot)
                        (d d2:bool)
  : GTot (option (slot &
                  M.store_entry &
                  M.store_entry &
                  M.store_entry &
                  M.store_entry &
                  (slot & bool) &
                  M.thread_state_model))
  = let st = tsm.store in
    if M.has_slot tsm s
    || not (is_value_of k v)
    || not (M.has_slot tsm s')
    then None
    else
      match M.get_entry tsm s' with
      | Some r' ->
        let p = (s', d) in
        let s2_opt = M.child_slot r' d in
        match s2_opt with
        | None -> None
        | Some s2 ->
          match Seq.index st (U16.v s2) with
          | None -> None
          | Some r2 ->
                 let open M in
                 let e = mk_entry_full k v M.MAdd None None (Some p) in
                 let e = update_child e d2 s2 in
                 let e' = update_child r' d s in
                 let p2new = s, d2 in
                 let e2 = update_parent_slot r2 p2new in
                 let st = Seq.upd st (U16.v s) (Some e) in
                 let st = Seq.upd st (U16.v s') (Some e') in
                 let st = Seq.upd st (U16.v s2) (Some e2) in
                 Some (s2, e, e', e2, r2, p2new, { tsm with store = st })

let madd_to_store_split (#tsm:M.thread_state_model)
                        (t:thread_state_t)
                        (s:T.slot)
                        (k:key)
                        (v:T.value)
                        (s':T.slot)
                        (d:bool)
                        (d2:bool)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.madd_to_store_split tsm s k v s' d d2))
  = let b = (T.is_value_of k v) in
    if not b
    then (fail t; return ())
    else (
      let ropt = A.read t.store (u16_as_size_t s) in
      let ropt' = A.read t.store (u16_as_size_t s') in
      match ropt with
      | Some _ -> fail t; return ()
      | _ ->
        match ropt' with
        | None -> fail t; return ()
        | Some r' ->
          let p = (s', d) in
          let s2_opt = M.child_slot r' d in
          match s2_opt with
          | None -> fail t; return ()
          | Some s2 ->
            let r2opt = A.read t.store (u16_as_size_t s2) in
            match r2opt with
            | None -> fail t; return ()
            | Some r2 ->
              let e = M.mk_entry_full k v M.MAdd None None (Some p) in
              let e = M.update_child e d2 s2 in
              let e' = M.update_child r' d s in
              let p2new = s, d2 in
              let e2 = M.update_parent_slot r2 p2new in
              A.write t.store (u16_as_size_t s) (Some e);
              A.write t.store (u16_as_size_t s') (Some e');
              A.write t.store (u16_as_size_t s2) (Some e2);
              return ())

let madd_to_store (#tsm:M.thread_state_model)
                  (t:thread_state_t)
                  (s:T.slot)
                  (k:key)
                  (v:T.value)
                  (s':T.slot)
                  (d:bool)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.madd_to_store tsm s k v s' d))
  = let b = (T.is_value_of k v) in
    if not b
    then (fail t; return ())
    else (
      let ropt = A.read t.store (u16_as_size_t s) in
      let ropt' = A.read t.store (u16_as_size_t s') in
      match ropt with
      | Some _ -> fail t; return ()
      | _ ->
        match ropt' with
        | None -> fail t; return ()
        | Some r' ->
          let new_entry : M.store_entry = {
            key = k;
            value = v;
            add_method = M.MAdd;
            l_child_in_store = None;
            r_child_in_store = None;
            parent_slot = Some (s', d)
          } in
          A.write t.store (u16_as_size_t s) (Some new_entry);
          let r' : M.store_entry =
            if d
            then { r' with l_child_in_store = Some s }
            else { r' with r_child_in_store = Some s }
          in
          A.write t.store (u16_as_size_t s') (Some r');
          return ()
    )

let entry_points_to_some_slot (r:M.store_entry)
                              (d:bool)
  : bool
  = if d
    then Some? (r.l_child_in_store)
    else Some? (r.r_child_in_store)

let update_value (#tsm:M.thread_state_model)
                 (t:thread_state_t)
                 (s:slot { M.has_slot tsm s })
                 (r:value { T.is_value_of (M.key_of_slot tsm s) r})
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.update_value tsm s r))
  = let Some v = A.read t.store (u16_as_size_t s) in
    A.write t.store (u16_as_size_t s) (Some ({v with M.value = r}));
    ()


#restart-solver
#push-options "--z3rlimit_factor 2"
let vaddm_core (#tsm:M.thread_state_model)
               (t:thread_state_t)
               (s s':slot_id)
               (r:T.record)
  : STT bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (AddM s s' r))))
  = let b = not (M.check_slot_bounds s)
          || not (M.check_slot_bounds s') in
    if b then (fail t; return true)
    else (
      let gk, gv = r in
      let ropt = A.read t.store (u16_as_size_t s') in
      match ropt with
      | None -> (fail t; return true)
      | Some r' ->
        let k' = to_base_key r'.key in
        let v' = r'.value in
        let k = to_base_key gk in
        (* check k is a proper desc of k' *)
        if not (KU.is_proper_descendent k k')
        then (fail t; return true)
        (* check store does not contain slot s *)
        else (
          let sopt = A.read t.store (u16_as_size_t s) in
          match sopt with
          | Some _ -> fail t; return true
          | _ ->
             match M.to_merkle_value v' with
             | None -> fail t; return true
             | Some v' ->
               let d = KU.desc_dir k k' in
               let dh' = M.desc_hash_dir v' d in
               let h = HashValue.hash_value t.hasher gv in
               match dh' returns
                     (STT bool
                          (thread_state_inv_core t tsm)
                          (fun b -> thread_state_inv_core t (update_if b tsm (M.vaddm tsm s s' r))))
               with
               | T.Dh_vnone _ -> (* k' has no child in direction d *)
                 (* first add must be init value *)
                 if not (T.eq_value gv (M.init_value gk))
                 then (let b = fail_as t _ in return b)
                 else if entry_points_to_some_slot r' d
                 then (let b = fail_as t _ in return b)
                 else (
                   madd_to_store t s gk gv s' d;

                   let v'_upd = M.update_merkle_value v' d k M.zero false in
                   update_value t s' (T.MValue v'_upd);
                   return true
                 )
               | T.Dh_vsome {T.dhd_key=k2; T.dhd_h=h2; T.evicted_to_blum = b2} ->
                 if KeyUtils.eq_base_key k2 k
                 then (
                   if not (T.eq_u256 h2 h && b2 = T.Vfalse)
                   then (let b = fail_as t _ in return b)
                   else if entry_points_to_some_slot r' d
                   then (let b = fail_as t _ in return b)
                   else (madd_to_store t s gk gv s' d;
                         assert_ (thread_state_inv_core t (M.vaddm tsm s s' r));
                         let b = true in
//                         intro_thread_state_inv_core (update_if b tsm (M.vaddm tsm s s' p)) t;
                         return b)
                 )
                 else if not (T.eq_value gv (M.init_value gk))
                 then (let b = fail_as t _ in return b)
                 (* check k2 is a proper desc of k *)
                 else if not (KU.is_proper_descendent k2 k)
                 then (let b = fail_as t _ in return b)
                 else (
                   let d2 = KU.desc_dir k2 k in
                   let Some mv = M.to_merkle_value gv in
                   let mv_upd = M.update_merkle_value mv d2 k2 h2 (b2=T.Vtrue) in
                   let v'_upd = M.update_merkle_value v' d k M.zero false in
                   let b = entry_points_to_some_slot r' d in
                   if b returns
                     (STT bool
                          (thread_state_inv_core t tsm)
                          (fun b -> thread_state_inv_core t (update_if b tsm (M.vaddm tsm s s' r))))
                   then (
                     madd_to_store_split t s gk (MValue mv_upd) s' d d2;
                     update_value t s' (MValue v'_upd);
                     let b = true in
                     return b
                   )
                   else (
                     madd_to_store t s gk (MValue mv_upd) s' d;
                     update_value t s' (MValue v'_upd);
                     let b = true in
                     return b
                   )
                 )))

let vaddm (#tsm:M.thread_state_model)
          (t:thread_state_t)
          (s s':slot_id)
          (r:T.record)
  : ST bool
    (thread_state_inv t tsm)
    (fun b ->
      thread_state_inv t
           (update_if b tsm (M.verify_step_model tsm (AddM s s' r))))
    (requires not tsm.failed)
    (ensures fun _ -> True)
  = elim_thread_state_inv _;
    let b = vaddm_core t s s' r in
    maybe_extend_processed_entries t _ _;
    return b

////////////////////////////////////////////////////////////////////////////////
//vaddb
////////////////////////////////////////////////////////////////////////////////

let next (t:T.timestamp)
  : option T.timestamp
  = match Zeta.Steel.Util.check_overflow_add32 t.counter 1ul with
    | None -> None
    | Some ctr -> Some ({ t with counter = ctr })

type htype =
  | HAdd
  | HEvict

let update_hash (c:M.epoch_hash)
                (r:T.record)
                (t:T.timestamp)
                (thread_id:T.thread_id)
                (ht:htype)
  : GTot M.epoch_hash
  = match ht with
    | HAdd -> { c with hadd = M.update_hash_value c.hadd r t thread_id }
    | HEvict -> { c with hevict = M.update_hash_value c.hevict r t thread_id }

let update_epoch_hash (tsm:M.thread_state_model)
                      (e:M.epoch_id)
                      (r:T.record)
                      (ts:T.timestamp)
                      (thread_id:T.thread_id)
                      (ht:htype)
   : M.thread_state_model
  = let c = Map.sel tsm.epoch_hashes e in
    {tsm with epoch_hashes =
                   Map.upd tsm.epoch_hashes
                      e
                      (update_hash c r ts thread_id ht)}

let maybe_update_epoch_hash (b:bool)
                            (tsm:M.thread_state_model)
                            (e:M.epoch_id)
                            (r:T.record)
                            (ts:T.timestamp)
                            (thread_id:T.thread_id)
                            (ht:htype)
   : M.thread_state_model
  = let c = Map.sel tsm.epoch_hashes e in
    {tsm with epoch_hashes =
                   Map.upd tsm.epoch_hashes
                      e
                      (update_if b c (update_hash c r ts thread_id ht))}

let maybe_update_epoch_hash_equiv
                          (b:bool)
                          (tsm:M.thread_state_model)
                          (e:M.epoch_id)
                          (r:T.record)
                          (ts:T.timestamp)
                          (thread_id:T.thread_id)
                          (ht:htype)
  : Lemma (requires
            Map.contains tsm.epoch_hashes e)
          (ensures
            maybe_update_epoch_hash b tsm e r ts thread_id ht ==
            update_if b tsm (update_epoch_hash tsm e r ts thread_id ht))
  = if b then ()
    else assert (Map.equal tsm.epoch_hashes (Map.upd tsm.epoch_hashes e (Map.sel tsm.epoch_hashes e)))

let unfold_epoch_hash_perm #o (k:M.epoch_id) (v:epoch_hashes_t) (c:M.epoch_hash)
  : STGhostT unit o
    (epoch_hash_perm k v c)
    (fun _ ->
      HA.ha_val v.hadd c.hadd `star`
      HA.ha_val v.hevict c.hevict)
  = rewrite (epoch_hash_perm k v c)
            (HA.ha_val v.hadd c.hadd `star`
             HA.ha_val v.hevict c.hevict)

let fold_epoch_hash_perm #o
                         (k:M.epoch_id)
                         (v:epoch_hashes_t)
                         (#had #hev:HA.hash_value_t)
                         (c:M.epoch_hash)
  : STGhost unit o
    (HA.ha_val v.hadd had `star`
     HA.ha_val v.hevict hev)
    (fun _ -> epoch_hash_perm k v c)
    (requires
      c.hadd == had /\
      c.hevict == hev)
    (ensures fun _ -> True)
  = rewrite (HA.ha_val v.hadd had `star`
             HA.ha_val v.hevict hev)
            (epoch_hash_perm k v c)


let ha_add (#v:erased (HA.hash_value_t))
           (ha:HA.ha)
           (l:U32.t)
           (#bs:erased bytes { U32.v l <= Seq.length bs /\ Seq.length bs <= HA.max_input_length })
           (#ivv:erased bytes { Seq.length ivv == HA.iv_len })
           (iv:A.array U8.t)
           (input:A.array U8.t)
  : STT bool
       (HA.ha_val ha v `star`
        array_pts_to input bs `star`
        array_pts_to iv ivv)
       (fun b ->
         array_pts_to input bs `star`
         array_pts_to iv ivv `star`
         HA.ha_val ha (HA.maybe_aggregate_hashes b v
                         (HA.hash_one_value ivv (Seq.slice bs 0 (U32.v l)))))
  = A.pts_to_length input _;
    A.pts_to_length iv _;
    let x = HA.add ha iv input l in
    return x


let new_epoch (e:M.epoch_id)
  : STT EH.epoch_hashes_t
    emp
    (fun v -> EH.epoch_hash_perm e v M.init_epoch_hash)
  = let hadd = HA.create () in
    let hev = HA.create () in
    let eh : EH.epoch_hashes_t = { hadd = hadd; hevict = hev } in
    rewrite (HA.ha_val hadd _ `star` HA.ha_val hev _)
            (EH.epoch_hash_perm e eh M.init_epoch_hash);
    return eh

let epoch_map_add (#v:Type0)
               (#contents:Type0)
               (#vp:M.epoch_id -> v -> contents -> vprop)
               (#init:Ghost.erased contents)
               (#m:Ghost.erased (EpochMap.repr contents))
               (a:EpochMap.tbl vp)
               (i:M.epoch_id)
               (x:v)
               (c:Ghost.erased contents)
  : STT unit
    (EpochMap.full_perm a init m `star`
     vp i x c)
    (fun _ ->
      EpochMap.full_perm a init (Map.upd m i c))
  = EpochMap.put a i x _;
    assert (PartialMap.remove (EpochMap.empty_borrows #v) i `PartialMap.equal`
            EpochMap.empty_borrows #v);
    rewrite (EpochMap.perm a _ _ (PartialMap.remove EpochMap.empty_borrows i))
            (EpochMap.full_perm a init (Map.upd m i c))

let get_or_init_post #v #c (#vp:M.epoch_id -> v -> c -> vprop)
                     (eht:EpochMap.tbl vp)
                     (e:M.epoch_id)
                     (def:erased c)
                     (repr:_)
                     (res:option v)

 = match res with
   | None -> EpochMap.full_perm eht def repr
   | Some v -> EpochMap.perm eht def repr (PartialMap.upd EpochMap.empty_borrows e v) `star`
              vp e v (Map.sel repr e)

inline_for_extraction
let get_or_init_eht #v #c (#vp:M.epoch_id -> v -> c -> vprop) (#repr:erased (EpochMap.repr c))
                           (eht:EpochMap.tbl vp)
                           (e:M.epoch_id)
                           (#def:erased c)
                           (init: (e:M.epoch_id -> STT v emp (fun v -> vp e v def)))
  : STT (option v)
        (EpochMap.full_perm eht def repr)
        (fun res -> get_or_init_post eht e def repr res)
  = let vopt = EpochMap.get eht e in
    match vopt with
    | EpochMap.NotFound ->
      rewrite (EpochMap.get_post _ _ _ _ _ vopt)
              (EpochMap.full_perm eht def repr);
      return None


    | EpochMap.Found v ->
      rewrite (EpochMap.get_post _ _ _ _ _ vopt)
              (get_or_init_post eht e def repr (Some v));
      return (Some v)

    | EpochMap.Fresh ->
      rewrite (EpochMap.get_post _ _ _ _ _ vopt)
              (EpochMap.full_perm eht def repr);
      let v = init e in
      epoch_map_add eht e v _;
      assert (repr `Map.equal` Map.upd repr e def);
      rewrite (EpochMap.full_perm eht _ _)
              (EpochMap.full_perm eht def repr);
      //This additional get is redundant
      //but the EHT is ephemeral and we can't prove that we can
      //get what we just put
      let vopt_again = EpochMap.get eht e in
      match vopt_again with
      | EpochMap.Found v ->
        rewrite (EpochMap.get_post _ _ _ _ _ vopt_again)
                (get_or_init_post eht e def repr (Some v));
        return (Some v)

      | _ ->
        rewrite (EpochMap.get_post _ _ _ _ _ vopt_again)
                (get_or_init_post eht e def repr None);
        return None

#push-options "--z3rlimit_factor 4"

let remove_upd (x:M.epoch_id)
  : Lemma (forall v. PartialMap.remove (PartialMap.upd EpochMap.empty_borrows x v) x
                == EpochMap.empty_borrows)
  = ()
#push-options "--print_implicits"
let ghost_put_back (#o:_)
              (#v:Type) 
              (#c:Type)
              (#vp:M.epoch_id -> v -> c -> vprop)
              (#init:Ghost.erased c)
              (#m:Ghost.erased (EpochMap.repr c))
              (a:EpochMap.tbl vp)
              (i:M.epoch_id)
              (x:v)
              (content:Ghost.erased c)
  : STGhostT unit o
      (EpochMap.perm a init m (PartialMap.upd EpochMap.empty_borrows i x) `star` vp i x content)
      (fun _ -> EpochMap.full_perm a init (Map.upd m i content))
  = EpochMap.ghost_put a i x content;
    rewrite (EpochMap.perm _ _ _ _)
            (EpochMap.full_perm a init (Map.upd m i content))


let serialize_iv_alt (a:A.array U8.t { A.length a == 96 })
                     (v: timestamp)
  : Steel.ST.Util.ST (Ghost.erased (Seq.seq U8.t))
    (iv_buffer_inv a)
    (fun bs -> array_pts_to a bs)
    (requires True)
    (ensures fun bs -> 
      seq_suffix_is_zero bs timestamp_len /\
      spec_serializer_iv v == Ghost.reveal bs)
  = rewrite (iv_buffer_inv a)
            (exists_ (fun bs -> 
              array_pts_to a bs `star`
              pure (seq_suffix_is_zero bs 8)));
    Zeta.Steel.IV.serialize_iv a v;
    let bs = elim_exists () in
    elim_pure _;
    return bs

let intro_iv_buffer_inv (#o:_) (#bs:Ghost.erased (Seq.seq U8.t))
                        (a:A.array U8.t { A.length a == 96 })
  : STGhost unit o
    (array_pts_to a bs)
    (fun _ -> iv_buffer_inv a)
    (requires seq_suffix_is_zero bs timestamp_len)
    (ensures fun _ -> True)
  = intro_pure (seq_suffix_is_zero bs 8);
    intro_exists_erased bs 
         (fun bs -> 
           array_pts_to a bs `star`
           pure (seq_suffix_is_zero bs 8));
    rewrite (exists_ _)
            (iv_buffer_inv a)

let update_ht (#tsm:M.thread_state_model)
              (t:thread_state_t)
              (e:M.epoch_id)
              (r:T.record)
              (ts:T.timestamp)
              (thread_id:T.thread_id)
              (ht:htype)
  : STT bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm (update_epoch_hash tsm e r ts thread_id ht)))
  = let vopt = get_or_init_eht t.epoch_hashes e new_epoch in
    match vopt with
    | None ->
      rewrite (get_or_init_post _ _ _ _ vopt)
              (EpochMap.full_perm t.epoch_hashes M.init_epoch_hash tsm.epoch_hashes);
      return false

    | Some v ->
      rewrite (get_or_init_post _ _ _ _ vopt)
              (EpochMap.perm t.epoch_hashes M.init_epoch_hash tsm.epoch_hashes
                             (PartialMap.upd EpochMap.empty_borrows e v) `star`
               EH.epoch_hash_perm e v (Map.sel tsm.epoch_hashes e));
      unfold_epoch_hash_perm _ _ _;
      let sr = {
        record = r;
        timestamp = ts;
        thread_id = thread_id
      } in
      serialized_iv_length ts;
      let iv_t = serialize_iv_alt t.iv_buffer ts in
      serialized_stamped_record_length sr;
      let n = serialize_stamped_record 4096ul 0ul t.serialization_buffer sr in
      let bs = elim_exists () in
      elim_pure ( _ /\ _ /\ _ /\ _);
      let ha = if ht = HAdd then v.hadd else v.hevict in
      let b =
        match ht
              returns (STT bool
                           (HA.ha_val v.hadd (Map.sel tsm.epoch_hashes e).hadd `star`
                            HA.ha_val v.hevict (Map.sel tsm.epoch_hashes e).hevict `star`
                            array_pts_to t.serialization_buffer bs `star`
                            array_pts_to t.iv_buffer iv_t
                            )
                           (fun b ->
                             array_pts_to t.serialization_buffer bs `star`
                             array_pts_to t.iv_buffer iv_t `star`                             
                             EH.epoch_hash_perm e v
                              (update_if b (Map.sel tsm.epoch_hashes e)
                                           (update_hash (Map.sel tsm.epoch_hashes e) r ts thread_id ht))))
        with
        | HAdd ->
          let b = ha_add v.hadd n t.iv_buffer t.serialization_buffer in
          fold_epoch_hash_perm e v
               (update_if b (Map.sel tsm.epoch_hashes e)
                            (update_hash (Map.sel tsm.epoch_hashes e) r ts thread_id HAdd));
          return b
        | HEvict ->
          let b = ha_add v.hevict n t.iv_buffer t.serialization_buffer in
          fold_epoch_hash_perm e v
               (update_if b (Map.sel tsm.epoch_hashes e)
                            (update_hash (Map.sel tsm.epoch_hashes e) r ts thread_id HEvict));
          return b
      in
      ghost_put_back t.epoch_hashes e v _;
      intro_exists _ (array_pts_to t.serialization_buffer);
      intro_iv_buffer_inv t.iv_buffer;
//      intro_exists _ (array_pts_to t.iv_buffer);
      maybe_update_epoch_hash_equiv b tsm e r ts thread_id ht;
      rewrite (thread_state_inv_core t (maybe_update_epoch_hash b tsm e r ts thread_id ht))
              (thread_state_inv_core t (update_if b tsm (update_epoch_hash tsm e r ts thread_id ht)));
      return b
#pop-options

let vaddb_core (#tsm:M.thread_state_model)
          (t:thread_state_t)
          (s:slot_id)
          (ts:timestamp)
          (thread_id:T.thread_id)
          (r:T.record)
  : STT bool
       (thread_state_inv_core t tsm)
       (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (AddB s ts thread_id r))))
  = let b = M.check_slot_bounds s in
    if not b then (fail t; return true)
    else (
      let (k, v) = r in
      if M.is_root_key k then (fail t; return true)
      else (
        let ropt = A.read t.store (u16_as_size_t s) in
        if Some? ropt then (fail t; return true) //slot is already full
        else (
          let lve = R.read t.last_verified_epoch in
          if not (M.epoch_greater_than_last_verified_epoch lve (M.epoch_of_timestamp ts))
          then (fail t; return true)
          else
            //add hash (k, v, t, thread_id) to hadd.[epoch_of_timestamp t]
            let ok = update_ht t (M.epoch_of_timestamp ts) r ts thread_id HAdd in
            if ok
            then (
              rewrite (thread_state_inv_core t _)
                      (thread_state_inv_core t (update_epoch_hash tsm (M.epoch_of_timestamp ts) r ts thread_id HAdd));
              let ts_opt = next ts in
              match ts_opt with
              | None -> fail t; return true
              | Some t' ->
                let clock = R.read t.clock in
                let next_clock = M.max clock t' in
                if clock `M.timestamp_lt` next_clock
                then (
                  R.write t.last_evict_key root_base_key;
                  R.write t.clock next_clock;
                  A.write t.store (u16_as_size_t s) (Some (M.mk_entry k v M.BAdd));
                  return true
                )
                else (
                  R.write t.clock next_clock;
                  A.write t.store (u16_as_size_t s) (Some (M.mk_entry k v M.BAdd));
                  return true
                )
            )
            else (
              rewrite (thread_state_inv_core t _) (thread_state_inv_core t tsm);
              return ok
            )
          )
        )
      )

let vaddb (#tsm:M.thread_state_model)
          (t:thread_state_t)
          (s:slot_id)
          (ts:timestamp)
          (thread_id:T.thread_id)
          (r:T.record)
  = elim_thread_state_inv _;
    let b = vaddb_core t s ts thread_id r in
    maybe_extend_processed_entries t _ _;
    return b

////////////////////////////////////////////////////////////////////////////////
//vevictm
////////////////////////////////////////////////////////////////////////////////



let evict_from_store (#tsm:M.thread_state_model)
                     (t:thread_state_t)
                     (s:slot)
                     (s':slot { M.has_slot tsm s' })
                     (d:bool)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.mevict_from_store tsm s s' d))
  = let Some r' = A.read t.store (u16_as_size_t s') in
    let e' =
        if d
        then { r' with M.l_child_in_store = None }
        else { r' with M.r_child_in_store = None }
    in
    A.write t.store (u16_as_size_t s') (Some e');
    A.write t.store (u16_as_size_t s) None;
    ()

let vevictm_core (#tsm:M.thread_state_model)
                 (t:thread_state_t)
                 (s s':slot_id)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.verify_log_entry tsm (EvictM ({s; s_=s'}))))
  = if not (M.check_slot_bounds s)
    || not (M.check_slot_bounds s')
    then (R.write t.failed true; ())
    else if s = s'
    then (R.write t.failed true; ())
    else (
      let e = A.read t.store (u16_as_size_t s) in
      let e' = A.read t.store (u16_as_size_t s') in
      match e, e' with
      | None, _
      | _, None -> R.write t.failed true; ()
      | Some r, Some r' ->
        let gk = r.M.key in
        let v = r.M.value in
        let gk' = r'.M.key in
        let v' = r'.M.value in
        let k = to_base_key gk in
        let k' = to_base_key gk' in
        (* check k is a proper descendent of k' *)
        if not (KU.is_proper_descendent k k')
        then (R.write t.failed true; ())
        (* check k does not have a (merkle) child in the store *)
        else if entry_points_to_some_slot r true
             ||  entry_points_to_some_slot r false
        then (R.write t.failed true; ())
        else (
          let d = KU.desc_dir k k' in
          let Some v' = M.to_merkle_value v' in
          let dh' = M.desc_hash_dir v' d in
          let h = HashValue.hash_value t.hasher v in
          match dh' with
          | T.Dh_vnone _ -> fail t; ()
          | T.Dh_vsome {T.dhd_key=k2; T.dhd_h=h2; T.evicted_to_blum = b2} ->
            if not (T.eq_base_key k2 k) then (fail t; ())
            else
              let has_parent_slot = Some? r.M.parent_slot in
              if has_parent_slot
              then begin
                let p_slot = Some?.v r.M.parent_slot in
                let b1 = fst p_slot <> s' in
                let b2 = snd p_slot <> d in
                if b1 || b2
                then (fail t; ())
                else begin
                  let v'_upd = M.update_merkle_value v' d k h false in
                  update_value t s' (T.MValue v'_upd);
                  evict_from_store t s s' d;
                  ()
                end
              end
              else begin
                let b = entry_points_to_some_slot r' d in
                if b
                then (fail t; ())
                else begin
                  let v'_upd = M.update_merkle_value v' d k h false in
                  update_value t s' (T.MValue v'_upd);
                  evict_from_store t s s' d;
                  ()
                end
              end
        )
      )

let vevictm (#tsm:M.thread_state_model)
            (t:thread_state_t)
            (s s':slot_id)
  = elim_thread_state_inv _;
    vevictm_core t s s';
    extend_processed_entries t _


////////////////////////////////////////////////////////////////////////////////
//vevictb
////////////////////////////////////////////////////////////////////////////////
let sat_evictb_checks (#tsm:M.thread_state_model)
                      (t:thread_state_t)
                      (s:slot)
                      (ts:timestamp)
  : ST bool
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t tsm)
    (requires True)
    (ensures fun b -> b == M.sat_evictb_checks tsm s ts)
  = let ropt = A.read t.store (u16_as_size_t s) in
    match ropt with
    | None ->
      return false
    | Some r ->
      let k = r.key in
      let bk = to_base_key k in
      let v = r.value in
      let clock = R.read t.clock in
      let lek = R.read t.last_evict_key in
      let b =
        not (M.is_root_key k) &&
        (* check time of evict < current time *)
        (clock, lek) `M.tk_lt` (ts,bk) &&
        (* check k has no (merkle) children n the store *)
        not (entry_points_to_some_slot r true) &&
        not (entry_points_to_some_slot r false)
      in
      return b

let vevictb_update_hash_clock (#tsm:M.thread_state_model)
                              (t:thread_state_t)
                              (s:slot)
                              (ts:timestamp { M.sat_evictb_checks tsm s ts })
   : ST bool
     (thread_state_inv_core t tsm)
     (fun b -> thread_state_inv_core t (update_if b tsm (M.vevictb_update_hash_clock tsm s ts)))
     (requires tsm.thread_id == t.thread_id)
     (ensures fun _ -> True)
   = let Some r = A.read t.store (u16_as_size_t s) in
     let k = r.key in
     let bk = to_base_key k in
     let v = r.value in
     (* update evict hash *)
     let e = M.epoch_of_timestamp ts in
     let b = update_ht t e (k, v) ts t.thread_id HEvict in
     if b
     then (
       R.write t.clock ts;
       R.write t.last_evict_key bk;
       return b
     )
     else (
       rewrite (thread_state_inv_core t _) (thread_state_inv_core t tsm);
       return b
     )

let vevictb_core (#tsm:M.thread_state_model)
                 (t:thread_state_t)
                 (s:slot_id)
                 (ts:timestamp)
  : ST bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (EvictB ({s; t=ts})))))
    (requires t.thread_id == tsm.thread_id)
    (ensures fun _ -> True)
  = let bounds_failed = not (M.check_slot_bounds s) in
    if bounds_failed //not hoisting this leads to weirdness
    then (
      R.write t.failed true;
      return true
    )
    else (
      let b = sat_evictb_checks t s ts in
      if not b
      then (
        fail t;
        return true
      )
      else (
        let Some r = A.read t.store (u16_as_size_t s) in
        let add_method_not_badd = r.add_method <> M.BAdd in
        if add_method_not_badd
        returns STT bool (thread_state_inv_core t tsm)
                         (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (EvictB ({s; t=ts})))))
        then ( fail t; return true )
        else (
          let b = vevictb_update_hash_clock t s ts in
          if b
          then (
            A.write t.store (u16_as_size_t s) None;
            return true
          )
          else (
            rewrite (thread_state_inv_core t _)
                    (thread_state_inv_core t tsm);
            return false
          )
        )
      )
    )

let vevictb (#tsm:M.thread_state_model)
            (t:thread_state_t)
            (s:slot_id)
            (ts:timestamp)
  = elim_thread_state_inv _;
    let b = vevictb_core t s ts in
    maybe_extend_processed_entries t _ _;
    return b

////////////////////////////////////////////////////////////////////////////////
//vevictbm: A bit delicate. TODO should debug the SMT queries.
////////////////////////////////////////////////////////////////////////////////

let vevictbm_core (#tsm:M.thread_state_model)
                  (t:thread_state_t)
                  (s s':slot_id)
                  (ts:timestamp)
  : ST bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (EvictBM ({s; s_=s'; t=ts})))))
    (t.thread_id == tsm.thread_id)
    (fun _ -> True)
  = let bounds_failed =
          not (M.check_slot_bounds s)
        || not (M.check_slot_bounds s')
    in
    if bounds_failed then fail_as t _
    else if s = s' then fail_as t _
    else let se_checks = sat_evictb_checks t s ts in
         if not se_checks then fail_as t _
         else let ropt = A.read t.store (u16_as_size_t s') in
              match ropt with
              | None -> fail_as t _
              | Some r' ->
                let Some r = A.read t.store (u16_as_size_t s) in
                let add_method_not_madd = r.add_method <> M.MAdd in
                if add_method_not_madd
                returns STT bool (thread_state_inv_core t tsm)
                                 (fun b -> thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm (EvictBM ({s; s_=s'; t=ts})))))
                then (let b = fail_as t _ in return b)
                else (
                  let gk = r.key in
                  let gk' = r'.key in
                  let v' = r'.value in
                  let k = to_base_key gk in
                  let k' = to_base_key gk' in
                  if not (KU.is_proper_descendent k k')
                  then let b = fail_as t _ in return b
                  else (
                    let Some mv' = M.to_merkle_value v' in
                    let d = KU.desc_dir k k' in
                    let dh' = M.desc_hash_dir mv' d in
                    match dh' returns
                          (STT bool (thread_state_inv_core t tsm)
                                    (fun b -> thread_state_inv_core t (update_if b tsm (M.vevictbm tsm s s' ts))))
                    with
                    | T.Dh_vnone _ ->
                      let b = fail_as t _ in return b

                    | T.Dh_vsome {T.dhd_key=k2;
                                  T.dhd_h=h2;
                                  T.evicted_to_blum = b2} ->
                      if (not (T.eq_base_key k2 k)) || (b2 = T.Vtrue)
                      then let b = fail_as t _ in return b
                      else let parent_slot_none = None? r.parent_slot in
                           if parent_slot_none
                           then let b = fail_as t _ in return b
                           else begin
                             let parent_slot = Some?.v r.parent_slot in
                             let b1 = fst parent_slot <> s' in
                             let b2 = snd parent_slot <> d in
                             if b1 || b2
                             then let b = fail_as t _ in return b
                             else begin
                               let b = vevictb_update_hash_clock t s ts in
                               if b
                               then (
                                 // rewrite (thread_state_inv_core t _)
                                 //         (thread_state_inv_core t (M.vevictb_update_hash_clock tsm s ts));
                                 let mv'_upd = M.update_merkle_value mv' d k h2 true in
                                 update_value t s' (MValue mv'_upd);
                                 evict_from_store t s s' d;
                                 return true
                               )
                               else (
                                 rewrite (thread_state_inv_core t _)
                                         (thread_state_inv_core t tsm);
                                 return false
                               )
                             end
                           end))

let vevictbm (#tsm:M.thread_state_model)
             (t:thread_state_t)
             (s s':slot_id)
             (ts:timestamp)
  = elim_thread_state_inv _;
    let b = vevictbm_core t s s' ts in
    maybe_extend_processed_entries t b _;
    return b

////////////////////////////////////////////////////////////////////////////////
// nextepoch
////////////////////////////////////////////////////////////////////////////////

let nextepoch_core (#tsm:M.thread_state_model)
                   (t:thread_state_t)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.verify_log_entry tsm NextEpoch))
  = let c = R.read t.clock in
    let e = M.epoch_of_timestamp c in
    let res = st_check_overflow_add32 e 1ul in //Ugh. need this wrapper, else weirdness
    match res with
    | None ->
      fail t; ()
    | Some nxt ->
      let c = { epoch = nxt; counter = 0ul } in
      R.write t.clock c;
      R.write t.last_evict_key root_base_key;
      ()

let nextepoch (#tsm:M.thread_state_model)
              (t:thread_state_t)
  = elim_thread_state_inv _;
    nextepoch_core t;
    extend_processed_entries t _

////////////////////////////////////////////////////////////////////////////////
//verify_epoch: One of the most delicate functions in the API is
//verify_epoch, since it involves working with the aggregate epoch state
////////////////////////////////////////////////////////////////////////////////
let spec_verify_epoch (tsm:M.thread_state_model)
  = M.verify_step_model tsm VerifyEpoch

let aggregate_one_epoch_hash (source:AEH.epoch_hashes_repr)
                             (dest:AEH.epoch_hashes_repr)
                             (e:M.epoch_id)
  : AEH.epoch_hashes_repr
  = Map.upd dest e (AEH.aggregate_epoch_hash
                      (Map.sel dest e)
                      (Map.sel source e))
/
Zeta.Steel.VerifierTypes.fst.checked Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadLogMap.fsti.checked Zeta.Steel.LogEntry.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.IV.fst.checked Zeta.Steel.HashValue.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.Steel.Application.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Zeta.SeqAux.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.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.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.Int.Cast.fst.checked FStar.Ghost.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
Zeta.Steel.VerifierSteps.fst

    b0: Prims.bool ->
    b1: Prims.bool ->
    e0: Zeta.Steel.ThreadStateModel.epoch_hash ->
    e1: Zeta.Steel.ThreadStateModel.epoch_hash
  -> Zeta.Steel.ThreadStateModel.epoch_hash
Prims.bool Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.ThreadStateModel.Mkepoch_hash Zeta.Steel.Util.update_if Zeta.Steel.ThreadStateModel.model_hash Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hadd Zeta.Steel.HashAccumulator.aggregate_hashes Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hevict
let aggregate_epoch_hash (b0 b1: bool) (e0 e1: M.epoch_hash) : M.epoch_hash =
  
{
  hadd = update_if b0 e0.hadd (HA.aggregate_hashes e0.hadd e1.hadd);
  hevict = update_if b1 e0.hevict (HA.aggregate_hashes e0.hevict e1.hevict)
}