val init_value (k: key) : T.value
val init_value (k: key) : T.value
let init_value (k:key)
  : T.value
  = if ApplicationKey? k
    then DValue None
    else MValue ({ l = Dh_vnone (); r = Dh_vnone ()})
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' }
/
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
k: Zeta.Steel.LogEntry.Types.key -> Zeta.Steel.LogEntry.Types.value
Zeta.Steel.LogEntry.Types.key Zeta.Steel.LogEntry.Types.uu___is_ApplicationKey Zeta.Steel.LogEntry.Types.DValue FStar.Pervasives.Native.None Zeta.Steel.ApplicationTypes.value_type Prims.bool Zeta.Steel.LogEntry.Types.MValue Zeta.Steel.LogEntry.Types.Mkmval_value Zeta.Steel.LogEntry.Types.Dh_vnone Zeta.Steel.LogEntry.Types.value
let init_value (k: key) : T.value =
  
if ApplicationKey? k then DValue None else MValue ({ l = Dh_vnone (); r = Dh_vnone () })