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

    tsm: Zeta.Steel.ThreadStateModel.thread_state_model ->
    s: Zeta.Steel.FormatsManual.slot ->
    k: Zeta.Steel.LogEntry.Types.key ->
    v: Zeta.Steel.LogEntry.Types.value ->
    s': Zeta.Steel.FormatsManual.slot ->
    d: Prims.bool ->
    d2: Prims.bool
  -> Prims.GTot
    (FStar.Pervasives.Native.option ((((((Zeta.Steel.FormatsManual.slot *
          Zeta.Steel.ThreadStateModel.store_entry) *
          Zeta.Steel.ThreadStateModel.store_entry) *
          Zeta.Steel.ThreadStateModel.store_entry) *
          Zeta.Steel.ThreadStateModel.store_entry) *
          (Zeta.Steel.FormatsManual.slot * Prims.bool)) *
          Zeta.Steel.ThreadStateModel.thread_state_model))
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.FormatsManual.slot Zeta.Steel.LogEntry.Types.key Zeta.Steel.LogEntry.Types.value Prims.bool Prims.op_BarBar Zeta.Steel.ThreadStateModel.has_slot Prims.op_Negation Zeta.Steel.LogEntry.Types.is_value_of FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple7 Zeta.Steel.ThreadStateModel.store_entry FStar.Pervasives.Native.tuple2 Zeta.Steel.ThreadStateModel.get_entry FStar.Seq.Base.index FStar.Pervasives.Native.option FStar.UInt16.v FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple7 Zeta.Steel.ThreadStateModel.Mkthread_state_model Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__clock Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_evict_key Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__epoch_hashes Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__app_results Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_verified_epoch FStar.Seq.Base.seq FStar.Seq.Base.upd Zeta.Steel.ThreadStateModel.update_parent_slot FStar.Pervasives.Native.Mktuple2 Zeta.Steel.ThreadStateModel.update_child Zeta.Steel.ThreadStateModel.mk_entry_full Zeta.Steel.ThreadStateModel.MAdd Zeta.Steel.ThreadStateModel.child_slot Zeta.Steel.ThreadStateModel.contents Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store
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 })