val update_epoch_hadd
      (ehs: epoch_hashes)
      (eid: epoch_id)
      (r: T.record)
      (t: T.timestamp)
      (thread_id: T.thread_id)
    : GTot epoch_hashes
val update_epoch_hadd
      (ehs: epoch_hashes)
      (eid: epoch_id)
      (r: T.record)
      (t: T.timestamp)
      (thread_id: T.thread_id)
    : GTot epoch_hashes
let update_epoch_hadd (ehs:epoch_hashes)
                      (eid:epoch_id)
                      (r:T.record)
                      (t:T.timestamp)
                      (thread_id:T.thread_id)
  : GTot epoch_hashes
  = let eh = Map.sel ehs eid in
    let eh = { eh with hadd = update_hash_value eh.hadd r t thread_id } in
    Map.upd ehs eid eh
module Zeta.Steel.ThreadStateModel
(*
 * This module provides a logical specification for a single verifier
 * thread implemented in Steel
 **)

open FStar.Ghost
open Zeta.Steel.ApplicationResult
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.FormatsManual
open Zeta.Steel.LogEntry
module T = Zeta.Steel.FormatsManual
module P = Zeta.Steel.Parser
module L = FStar.List.Tot
module HA = Zeta.Steel.HashAccumulator
module C = FStar.Int.Cast
module KU = Zeta.Steel.KeyUtils
module A = Zeta.App
module SA = Zeta.SeqAux
open Zeta.Steel.Util
#push-options "--using_facts_from '* -FStar.Seq.Properties.slice_slice'"

type add_method =
  | MAdd
  | BAdd

[@@CAbstractStruct]
noeq
type store_entry = {
  key : T.key;
  value : (v:value { is_value_of key v });
  add_method : add_method;
  l_child_in_store : option slot;
  r_child_in_store : option slot;
  parent_slot : option (slot & bool);
}

let contents = Seq.lseq (option store_entry) (U16.v store_size)
let model_hash = HA.hash_value_t

let epoch_id = U32.t

[@@erasable]
noeq
type epoch_hash = {
  hadd: model_hash;
  hevict: model_hash;
}
let init_epoch_hash =  {
  hadd = HA.initial_hash;
  hevict = HA.initial_hash;
}
let epoch_hashes = m:Map.t epoch_id epoch_hash{ Map.domain m `Set.equal` Set.complement Set.empty }
let initial_epoch_hashes : epoch_hashes = Map.const init_epoch_hash
let app_results = Seq.seq app_result_entry
           
[@@erasable]
noeq
type thread_state_model = {
  failed : bool;
  store : contents;
  clock : T.timestamp;
  last_evict_key: T.base_key;
  epoch_hashes: epoch_hashes;
  thread_id: tid;
  processed_entries: Seq.seq log_entry;
  app_results: app_results;
  last_verified_epoch: option epoch_id;
}

let fail tsm = {tsm with failed=true}

let get_entry (tsm:thread_state_model) (s:T.slot)
  : GTot (option store_entry)
  = Seq.index tsm.store (U16.v s)

let check_slot_bounds (s:T.slot_id)
  : bool
  = U16.lt s store_size
  
let has_slot (tsm:thread_state_model) (s:T.slot_id)
  = check_slot_bounds s &&
    Some? (get_entry tsm s)

let madd_to_store_root (tsm: thread_state_model) (s: T.slot) (v: T.value)
  : thread_state_model
  = if has_slot tsm s 
    || not (is_value_of root_key v)
    then tsm
    else
      let new_entry = {
        key = root_key;
        value = v;
        add_method = MAdd;
        l_child_in_store = None;
        r_child_in_store = None;
        parent_slot = None;
      } in
      let store' = Seq.upd tsm.store (U16.v s) (Some new_entry) in
      { tsm with store = store' }

let init_value (k:key)
  : T.value
  = if ApplicationKey? k
    then DValue None
    else MValue ({ l = Dh_vnone (); r = Dh_vnone ()})

inline_for_extraction
let zero_clock = { epoch = 0ul; counter = 0ul }

let init_thread_state_model tid
  : thread_state_model
  = let tsm = {
      thread_id = tid;
      failed = false;
      store = Seq.create (U16.v store_size) None;
      clock = zero_clock;
      last_evict_key = root_base_key;
      epoch_hashes = initial_epoch_hashes;
      processed_entries = Seq.empty;
      app_results = Seq.empty;
      last_verified_epoch = None;
    } in
    if U16.v tid = 0 then 
      madd_to_store_root tsm U16.zero (init_value root_key)
    else tsm
  
let put_entry (tsm:thread_state_model) (s:T.slot) (r:store_entry)
  : thread_state_model
  = {tsm with store=Seq.upd tsm.store (U16.v s) (Some r)}

let key_of_slot (tsm:thread_state_model) (s:T.slot { has_slot tsm s })
  : GTot key
  = let Some v = get_entry tsm s in
    v.key

let update_value (tsm:thread_state_model)
                 (s:T.slot{has_slot tsm s})
                 (r:T.value {is_value_of (key_of_slot tsm s) r})
  : thread_state_model
  = let Some v = get_entry tsm s in
    put_entry tsm s ({v with value = r})

let evict_entry (tsm:thread_state_model) (s:T.slot)
  : thread_state_model
  = {tsm with store=Seq.upd tsm.store (U16.v s) None }

let mk_entry_full (k:key)
                  (v:T.value{is_value_of k v})
                  (a:add_method)
                  (l r:option T.slot)
                  (p:option (T.slot & bool))
  : store_entry
  = {
      key = k;
      value = v;
      add_method = a;
      l_child_in_store = l;
      r_child_in_store = r;
      parent_slot = p
    }

let mk_entry (k:key) (v:T.value{is_value_of k v}) (a:add_method) 
  : store_entry
  = mk_entry_full k v a None None None

let update_clock (tsm:thread_state_model) (ts:T.timestamp)
  : thread_state_model
  = { tsm with clock = ts }

let update_last_evict_key (tsm: thread_state_model) (k: T.base_key)
  : thread_state_model
  = { tsm with last_evict_key = k }
  
let update_hash_value (ha:HA.hash_value_t)
                      (r:T.record)
                      (t:T.timestamp)
                      (tid:T.thread_id)
  : GTot HA.hash_value_t
  = let sr : T.stamped_record = { record = r; timestamp = t; thread_id = tid} in
    let b = spec_serializer_stamped_record sr in
    serialized_stamped_record_length sr;
    let iv = spec_serializer_iv t in
    serialized_iv_length t;
    let h = HA.hash_one_value iv b in
    HA.aggregate_hashes ha h
/
Zeta.Steel.Util.fst.checked Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.HashValue.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.BitUtils.fsti.checked Zeta.Steel.ApplicationResult.fsti.checked Zeta.SeqAux.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Set.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Steel.ThreadStateModel.fst

    ehs: Zeta.Steel.ThreadStateModel.epoch_hashes ->
    eid: Zeta.Steel.ThreadStateModel.epoch_id ->
    r: Zeta.Steel.LogEntry.Types.record ->
    t: Zeta.Steel.LogEntry.Types.timestamp ->
    thread_id: Zeta.Steel.LogEntry.Types.thread_id
  -> Prims.GTot Zeta.Steel.ThreadStateModel.epoch_hashes
Zeta.Steel.ThreadStateModel.epoch_hashes Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.LogEntry.Types.record Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.LogEntry.Types.thread_id FStar.Map.upd Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.ThreadStateModel.Mkepoch_hash Zeta.Steel.ThreadStateModel.update_hash_value Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hadd Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hevict FStar.Map.sel
let update_epoch_hadd
      (ehs: epoch_hashes)
      (eid: epoch_id)
      (r: T.record)
      (t: T.timestamp)
      (thread_id: T.thread_id)
    : GTot epoch_hashes =
  
let eh = Map.sel ehs eid in
let eh = { eh with hadd = update_hash_value eh.hadd r t thread_id } in
Map.upd ehs eid eh