val 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))
val 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))
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)))
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))}
/
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

    b: Prims.bool ->
    tsm: Zeta.Steel.ThreadStateModel.thread_state_model ->
    e: Zeta.Steel.ThreadStateModel.epoch_id ->
    r: Zeta.Steel.LogEntry.Types.record ->
    ts: Zeta.Steel.LogEntry.Types.timestamp ->
    thread_id: Zeta.Steel.LogEntry.Types.thread_id ->
    ht: Zeta.Steel.VerifierSteps.htype
  -> FStar.Pervasives.Lemma (requires FStar.Map.contains (Mkthread_state_model?.epoch_hashes tsm) e)
      (ensures
        Zeta.Steel.VerifierSteps.maybe_update_epoch_hash b tsm e r ts thread_id ht ==
        Zeta.Steel.Util.update_if b
          tsm
          (Zeta.Steel.VerifierSteps.update_epoch_hash tsm e r ts thread_id ht))
Prims.bool Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.LogEntry.Types.record Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.LogEntry.Types.thread_id Zeta.Steel.VerifierSteps.htype Prims._assert FStar.Map.equal Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__epoch_hashes FStar.Map.upd FStar.Map.sel Prims.unit Prims.b2t FStar.Map.contains Prims.squash Prims.eq2 Zeta.Steel.VerifierSteps.maybe_update_epoch_hash Zeta.Steel.Util.update_if Zeta.Steel.VerifierSteps.update_epoch_hash Prims.Nil FStar.Pervasives.pattern
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)))