val evict_add_count_rel (#app #n: _) (ep: epoch) (gk: key app) (il: eac_log app n)
    : Lemma
      (ensures
        (match eac_state_of_genkey gk il with
          | EACFail -> False
          | EACInit
          | EACInStore _ _ _
          | EACEvictedMerkle _ _ -> size (k_add_set ep gk il) = size (k_evict_set ep gk il)
          | EACEvictedBlum gke _ t _ ->
            if t.e = ep && gke = gk
            then size (k_add_set ep gk il) + 1 = size (k_evict_set ep gk il)
            else size (k_add_set ep gk il) = size (k_evict_set ep gk il))) (decreases (length il))
val evict_add_count_rel (#app #n: _) (ep: epoch) (gk: key app) (il: eac_log app n)
    : Lemma
      (ensures
        (match eac_state_of_genkey gk il with
          | EACFail -> False
          | EACInit
          | EACInStore _ _ _
          | EACEvictedMerkle _ _ -> size (k_add_set ep gk il) = size (k_evict_set ep gk il)
          | EACEvictedBlum gke _ t _ ->
            if t.e = ep && gke = gk
            then size (k_add_set ep gk il) + 1 = size (k_evict_set ep gk il)
            else size (k_add_set ep gk il) = size (k_evict_set ep gk il))) (decreases (length il))
let rec evict_add_count_rel
  (#app #n:_)
  (ep: epoch)
  (gk: key app)
  (il: eac_log app n)
  : Lemma (ensures(match eac_state_of_genkey gk il with
                   | EACFail -> False
                   | EACInit
                   | EACInStore _ _ _
                   | EACEvictedMerkle _ _ ->
                     size (k_add_set ep gk il) = size (k_evict_set ep gk il)
                   | EACEvictedBlum gke _ t _ ->
                     if t.e = ep && gke = gk then
                       size (k_add_set ep gk il) + 1 = size (k_evict_set ep gk il)
                     else
                       size (k_add_set ep gk il) = size (k_evict_set ep gk il)))
          (decreases (length il))
  = let bk = to_base_key gk in
    if length il = 0
    then (
      k_add_set_empty ep gk il;
      k_evict_set_empty ep gk il;
      eac_state_empty bk il
    )
    else (
      let i = length il - 1 in
      let il' = prefix il  i in
      k_add_set_snoc ep gk il;
      k_evict_set_snoc ep gk il;
      evict_add_count_rel ep gk il';
      eac_state_transition_snoc bk il;
      let es = eac_state_of_key bk il in
      let es' = eac_state_of_key bk il' in
      if es = es' then eac_state_unchanged_snoc ep gk il
      else ()
    )
module Zeta.High.Blum

open Zeta.High.Verifier
open Zeta.High.Thread
open Zeta.SeqIdx
open FStar.Classical

module V = Zeta.GenericVerifier
module G = Zeta.Generic.Global
module T = Zeta.Generic.Thread
module I = Zeta.Interleave
module MSD = Zeta.MultiSetHashDomain
module HV = Zeta.High.Verifier

let eac_state_transition_snoc
  (#app #n:_)
  (bk: base_key)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let es' = eac_state_of_key bk il' in
                    let es = eac_state_of_key bk il in
                    let e = index il i in
                    es' <> es ==> (
                    match es', es with
                    | EACInit, EACInStore m gk v ->
                      AddM? e
                    | EACInStore _ gk' _, EACEvictedBlum gk v t tid ->
                      gk' = gk /\ is_blum_evict il i /\
                      to_base_key gk = evict_slot (index il i) /\
                      (let be = blum_evict_elem il i in
                       let gke,ve = be.r in
                       let open Zeta.MultiSetHashDomain in
                       gke = gk /\ ve = v /\ be.t = t /\ be.tid = tid)
                    | EACInStore _ _ _, EACEvictedMerkle _ _ ->
                      EvictM? e
                    | EACEvictedBlum gk v t tid, EACInStore _ gk' _ ->
                      gk = gk' /\ is_blum_add il i /\
                      to_base_key gk = add_slot (index il i) /\
                      (let be = blum_add_elem il i in
                       let open Zeta.MultiSetHashDomain in
                       let gke, ve = be.r in
                       gke = gk /\ ve = v /\ be.t = t /\ be.tid = tid
                      )
                    | EACEvictedMerkle _ _, EACInStore _ _ _ ->
                      AddM? e
                    | EACInStore _ _ _, EACInStore _ _ _ ->
                      RunApp? e
                    | _ -> False)))
  = let i = length il - 1 in
    let il' = prefix il i in
    let es' = eac_state_of_key bk il' in
    let es = eac_state_of_key bk il in
    let ee = mk_vlog_entry_ext il i in
    let e = index il i in
    let tid = src il i in
    let st_pre = thread_store_pre tid il i in
    eac_state_snoc bk il;
    if es = es' then ()
    else
    (
      assert(es <> EACFail);
      assert(es = eac_add ee es');
      match es' with
      | EACInStore _ gk' _ -> (
        match ee with
        | EvictBlum e v_e tid_e ->
          ext_evict_val_is_stored_val il i;
          key_in_unique_store bk il' tid (stored_tid bk il')
        | _ ->  ()
      )
      | EACEvictedBlum _ _ _ _ ->
        // TODO: never seen this; fails with assert commented
        assert(match es', es with EACEvictedBlum gk v t tid, EACInStore _ gk' _ -> True);
        ()
      | _ -> ()
    )

let eac_state_unchanged_snoc
  (#app #n:_)
  (ep: epoch)
  (gk: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let bk = to_base_key gk in
                    let es' = eac_state_of_key bk il' in
                    let es = eac_state_of_key bk il in
                    es' = es ==> (not (is_blum_add_of_key ep gk il i) /\
                                  not (is_blum_evict_of_key ep gk il i))))
  = let bk = to_base_key gk in
    eac_state_snoc bk il

#push-options "--z3rlimit_factor 3"
/
Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.High.Thread.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.TSLog.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.Generic.Global.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Blum.fst
ep: Zeta.Time.epoch -> gk: Zeta.GenKey.key app -> il: Zeta.High.Interleave.eac_log app n
  -> FStar.Pervasives.Lemma
      (ensures
        ((match Zeta.High.Interleave.eac_state_of_genkey gk il with
            | Zeta.EAC.EACFail #_ #_ -> Prims.l_False
            | Zeta.EAC.EACInit #_ #_ ->
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_add_set ep gk il) =
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_evict_set ep gk il)
            | Zeta.EAC.EACInStore #_ #_ _ _ _ ->
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_add_set ep gk il) =
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_evict_set ep gk il)
            | Zeta.EAC.EACEvictedMerkle #_ #_ _ _ ->
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_add_set ep gk il) =
              Zeta.MultiSet.size (Zeta.Generic.Blum.k_evict_set ep gk il)
            | Zeta.EAC.EACEvictedBlum #_ #_ gke _ t _ ->
              (match Mktimestamp?.e t = ep && gke = gk with
                | true ->
                  Zeta.MultiSet.size (Zeta.Generic.Blum.k_add_set ep gk il) + 1 =
                  Zeta.MultiSet.size (Zeta.Generic.Blum.k_evict_set ep gk il)
                | _ ->
                  Zeta.MultiSet.size (Zeta.Generic.Blum.k_add_set ep gk il) =
                  Zeta.MultiSet.size (Zeta.Generic.Blum.k_evict_set ep gk il))
              <:
              Type0)
          <:
          Type0)) (decreases Zeta.Generic.Interleave.length il)
Zeta.App.app_params Prims.pos Zeta.Time.epoch Zeta.GenKey.key Zeta.High.Interleave.eac_log Prims.op_Equality Prims.int Zeta.Generic.Interleave.length Zeta.High.Verifier.high_verifier_spec Zeta.High.Interleave.eac_state_empty Prims.unit Zeta.Generic.Blum.k_evict_set_empty Zeta.Generic.Blum.k_add_set_empty Prims.bool Zeta.EAC.eac_state Zeta.High.Blum.eac_state_unchanged_snoc Zeta.High.Interleave.eac_state_of_key Zeta.High.Blum.eac_state_transition_snoc Zeta.High.Blum.evict_add_count_rel Zeta.Generic.Blum.k_evict_set_snoc Zeta.Generic.Blum.k_add_set_snoc Zeta.Generic.Interleave.verifiable_log Prims.b2t Prims.nat Zeta.Generic.Interleave.prefix Prims.op_Subtraction Zeta.Key.base_key Zeta.GenKey.to_base_key Prims.l_True Prims.squash Zeta.High.Interleave.eac_state_of_genkey Prims.l_False Zeta.MultiSet.size Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.ms_hashfn_dom_cmp Zeta.Generic.Blum.k_add_set Zeta.Generic.Blum.k_evict_set Zeta.High.Verifier.add_method Zeta.Record.value_t Zeta.Time.timestamp Zeta.GenericVerifier.thread_id Prims.op_AmpAmp Zeta.Time.__proj__Mktimestamp__item__e Prims.op_Addition Prims.Nil FStar.Pervasives.pattern
let rec evict_add_count_rel (#app #n: _) (ep: epoch) (gk: key app) (il: eac_log app n)
    : Lemma
      (ensures
        (match eac_state_of_genkey gk il with
          | EACFail -> False
          | EACInit
          | EACInStore _ _ _
          | EACEvictedMerkle _ _ -> size (k_add_set ep gk il) = size (k_evict_set ep gk il)
          | EACEvictedBlum gke _ t _ ->
            if t.e = ep && gke = gk
            then size (k_add_set ep gk il) + 1 = size (k_evict_set ep gk il)
            else size (k_add_set ep gk il) = size (k_evict_set ep gk il))) (decreases (length il)) =
  
let bk = to_base_key gk in
if length il = 0
then
  (k_add_set_empty ep gk il;
    k_evict_set_empty ep gk il;
    eac_state_empty bk il)
else
  (let i = length il - 1 in
    let il' = prefix il i in
    k_add_set_snoc ep gk il;
    k_evict_set_snoc ep gk il;
    evict_add_count_rel ep gk il';
    eac_state_transition_snoc bk il;
    let es = eac_state_of_key bk il in
    let es' = eac_state_of_key bk il' in
    if es = es' then eac_state_unchanged_snoc ep gk il)