val is_eac_state_instore : k: Zeta.GenericVerifier.base_key -> il: Zeta.High.Interleave.verifiable_log app n
  -> Prims.GTot Prims.bool
let is_eac_state_instore (#app #n:_) (k:base_key) (il: verifiable_log app n)
  = let es = eac_state_of_key k il in
    let open Zeta.BinTree in
    k = Root && es = EACInit || EACInStore? es
module Zeta.High.Interleave

open FStar.Seq
open Zeta.Interleave
open Zeta.App
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.GenericVerifier
open Zeta.High.Verifier
open Zeta.EAC
open Zeta.Generic.Interleave

module V = Zeta.GenericVerifier
module T = Zeta.Generic.Thread
module G = Zeta.Generic.Global
module GI = Zeta.Generic.Interleave
module HV = Zeta.High.Verifier
module I = Zeta.Interleave
module S = FStar.Seq
module SA = Zeta.SeqAux
module EAC=Zeta.EAC
module MSD = Zeta.MultiSetHashDomain

let ilog (app: app_params) = Zeta.Generic.Interleave.ilog (high_verifier_spec app)

let verifiable_log (app:_) (n:nat)
  = il:ilog app n {verifiable il}

let thread_store (#app #n:_) (tid: nat{tid < n}) (il: verifiable_log app n)
  = let vs = thread_state tid il in
    vs.st

let thread_store_pre (#app #n:_) (tid: nat{tid < n}) (il: verifiable_log app n) (i: seq_index il)
  = let vs = thread_state_pre tid il i in
    vs.st

let thread_store_post (#app #n:_) (tid: nat{tid < n}) (il: verifiable_log app n) (i: seq_index il)
  = let vs = thread_state_post tid il i in
    vs.st

val runapp_refs_only_leafkeys (#app #n:_) (il: verifiable_log app n) (i:_ {RunApp? (index il i)}) (k: base_key)
  : Lemma (ensures (let e = index il i in
                    e `refs_key` k ==> is_leaf_key k))

val not_refs_implies_store_unchanged  (#app #n:_) (k:base_key) (t:nat{t < n})
  (il: verifiable_log app n) (i:seq_index il)
  : Lemma (ensures (let e = I.index il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    not (e `exp_refs_key` k) ==>
                    store_contains st_pre k ==>
                    (store_contains st_post k /\
                     stored_key st_post k == stored_key st_pre k /\
                     stored_value st_post k == stored_value st_pre k)))

val runapp_doesnot_change_store_keys (#app #n:_) (k:base_key)
  (il: verifiable_log app n) (i: seq_index il {is_appfn il i})
  : Lemma (ensures (let t = src il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    store_contains st_post k = store_contains st_pre k))

val blum_evict_elem_props
  (#app #n:_)
  (il: verifiable_log app n)
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let e = I.index il i in
                    let MSD.MHDom (gk,vk) t_e tid_e = blum_evict_elem il i in
                    let tid = I.src il i in
                    let st_pre = thread_store_pre tid il i in
                    let k = V.evict_slot e in
                    k = to_base_key gk /\
                    store_contains st_pre k /\
                    gk = stored_key st_pre k /\
                    vk = stored_value st_pre k /\
                    t_e = V.blum_evict_timestamp e /\
                    tid_e = tid))
          [SMTPat (blum_evict_elem il i)]

let has_some_add_of_key (#app #n:_) (bk: base_key) (il: verifiable_log app n)
  = exists i. HV.is_add_of_key bk (I.index il i)

let has_some_ref_to_key (#app #n:_) (bk: base_key) (il: verifiable_log app n)
  = exists i. HV.refs_key (I.index il i) bk

let exists_in_some_store (#app #n:_) (bk: base_key)  (il: verifiable_log app n)
  = exists tid. store_contains (thread_store tid il) bk

val mk_vlog_entry_ext (#app: app_params) (#n:nat) (il: verifiable_log app n) (i: seq_index il)
  : GTot (vlog_entry_ext app)

val vlog_entry_ext_prop (#app #n:_) (il: verifiable_log app n) (i: seq_index il)
  : Lemma (ensures (let ee = mk_vlog_entry_ext il i in
                    let e = I.index il i in
                    e = to_vlog_entry ee))
          [SMTPat (mk_vlog_entry_ext il i)]

val vlog_ext_of_il_log (#app: app_params) (#n:nat) (il: verifiable_log app n)
  : GTot (seq (vlog_entry_ext app))

val is_eac (#app #n:_) (il: verifiable_log app n)
  : GTot (b:bool{b <==> eac (vlog_ext_of_il_log il)})

(* state after processing the i'th element *)
val eac_state_of_key (#app #n:_) (k: base_key) (il: verifiable_log app n)
  : GTot (eac_state app k)

let eac_state_of_key_pre (#app #n:_) (k: base_key) (il: verifiable_log app n) (i: seq_index il)
  = let il' = prefix il i in
    eac_state_of_key k il'

let eac_state_of_key_post (#app #n:_) (k: base_key) (il: verifiable_log app n) (i: seq_index il)
  = let il' = prefix il (i+1) in
    eac_state_of_key k il'

(* is the key k in evicted state in *)
let is_eac_state_evicted (#app #n:_) (k: base_key) (il: verifiable_log app n): GTot bool
  = EACEvictedMerkle? (eac_state_of_key k il) ||
    EACEvictedBlum? (eac_state_of_key k il)

let is_eac_state_active (#app #n:_) (k: base_key) (il: verifiable_log app n)
  = let es = eac_state_of_key k il in
    es <> EACInit && es <> EACFail
/
Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.EAC.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.High.Interleave.fsti
k: Zeta.GenericVerifier.base_key -> il: Zeta.High.Interleave.verifiable_log app n
  -> Prims.GTot Prims.bool
Zeta.App.app_params Prims.nat Zeta.GenericVerifier.base_key Zeta.High.Interleave.verifiable_log Prims.op_BarBar Prims.op_AmpAmp Prims.op_Equality Zeta.BinTree.bin_tree_node Zeta.BinTree.Root Zeta.EAC.eac_state Zeta.EAC.EACInit Zeta.EAC.uu___is_EACInStore Zeta.High.Interleave.eac_state_of_key Prims.bool
let is_eac_state_instore (#app #n: _) (k: base_key) (il: verifiable_log app n) =
  
let es = eac_state_of_key k il in
let open Zeta.BinTree in k = Root && es = EACInit || EACInStore? es