val eac_state_of_genkey (#app #n: _) (gk: key app) (il: verifiable_log app n)
    : GTot (eac_state app (to_base_key gk))
val eac_state_of_genkey (#app #n: _) (gk: key app) (il: verifiable_log app n)
    : GTot (eac_state app (to_base_key gk))
let eac_state_of_genkey (#app #n:_) (gk: key app) (il: verifiable_log app n)
  : GTot (eac_state app (to_base_key gk))
  = let k = to_base_key gk in
    let es = eac_state_of_key k il in
    if EAC.is_eac_state_active es then
      if gk = to_gen_key es then es
      else EACInit
    else 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

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
/
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
gk: Zeta.GenKey.key app -> il: Zeta.High.Interleave.verifiable_log app n
  -> Prims.GTot (Zeta.EAC.eac_state app (Zeta.GenKey.to_base_key gk))
Zeta.App.app_params Prims.nat Zeta.GenKey.key Zeta.High.Interleave.verifiable_log Zeta.EAC.is_eac_state_active Prims.op_Equality Zeta.EAC.to_gen_key Prims.bool Zeta.EAC.EACInit Zeta.GenKey.to_base_key Zeta.EAC.eac_state Zeta.High.Interleave.eac_state_of_key Zeta.Key.base_key
let eac_state_of_genkey (#app #n: _) (gk: key app) (il: verifiable_log app n)
    : GTot (eac_state app (to_base_key gk)) =
  
let k = to_base_key gk in
let es = eac_state_of_key k il in
if EAC.is_eac_state_active es then if gk = to_gen_key es then es else EACInit else es