val 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)))
val 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 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);
        ()
      | _ -> ()
    )
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
/
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

    bk: Zeta.GenericVerifier.base_key ->
    il: Zeta.High.Interleave.eac_log app n {Zeta.Generic.Interleave.length il > 0}
  -> FStar.Pervasives.Lemma
    (ensures
      (let i = Zeta.Generic.Interleave.length il - 1 in
        let il' = Zeta.Generic.Interleave.prefix il i in
        let es' = Zeta.High.Interleave.eac_state_of_key bk il' in
        let es = Zeta.High.Interleave.eac_state_of_key bk il in
        let e = Zeta.Interleave.index il i in
        es' <> es ==>
        (match es', es with
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACInit #_ #_)
            (Zeta.EAC.EACInStore #_ #_ _ _ _) ->
            AddM? e
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACInStore #_ #_ _ gk' _)
            (Zeta.EAC.EACEvictedBlum #_ #_ gk v t tid) ->
            gk' = gk /\ Zeta.Generic.Interleave.is_blum_evict il i /\
            Zeta.GenKey.to_base_key gk =
            Zeta.GenericVerifier.evict_slot (Zeta.Interleave.index il i) /\
            (let be = Zeta.Generic.Interleave.blum_evict_elem il i in
              let _ = MHDom?.r be in
              (let FStar.Pervasives.Native.Mktuple2 #_ #_ gke ve = _ in
                gke = gk /\ ve = v /\ MHDom?.t be = t /\ MHDom?.tid be = tid)
              <:
              Prims.logical)
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACInStore #_ #_ _ _ _)
            (Zeta.EAC.EACEvictedMerkle #_ #_ _ _) ->
            EvictM? e
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACEvictedBlum #_ #_ gk v t tid)
            (Zeta.EAC.EACInStore #_ #_ _ gk' _) ->
            gk = gk' /\ Zeta.Generic.Interleave.is_blum_add il i /\
            Zeta.GenKey.to_base_key gk = Zeta.GenericVerifier.add_slot (Zeta.Interleave.index il i) /\
            (let be = Zeta.Generic.Interleave.blum_add_elem il i in
              let _ = MHDom?.r be in
              (let FStar.Pervasives.Native.Mktuple2 #_ #_ gke ve = _ in
                gke = gk /\ ve = v /\ MHDom?.t be = t /\ MHDom?.tid be = tid)
              <:
              Prims.logical)
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACEvictedMerkle #_ #_ _ _)
            (Zeta.EAC.EACInStore #_ #_ _ _ _) ->
            AddM? e
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (Zeta.EAC.EACInStore #_ #_ _ _ _)
            (Zeta.EAC.EACInStore #_ #_ _ _ _) ->
            RunApp? e
          | _ -> Prims.l_False)))
Zeta.App.app_params Prims.pos Zeta.GenericVerifier.base_key Zeta.High.Interleave.eac_log Prims.b2t Prims.op_GreaterThan Zeta.Generic.Interleave.length Zeta.High.Verifier.high_verifier_spec Prims.op_Equality Zeta.EAC.eac_state Prims.bool Zeta.High.Verifier.add_method Zeta.GenKey.key Zeta.Key.base_key Zeta.GenKey.to_base_key Zeta.Record.value_t Zeta.High.Verifier.vlog_entry Zeta.GenericVerifier.is_blum_evict Zeta.Record.value Zeta.GenericVerifier.thread_id Zeta.High.Interleave.key_in_unique_store Zeta.High.Interleave.stored_tid Prims.unit Zeta.High.Interleave.ext_evict_val_is_stored_val Zeta.EAC.vlog_entry_ext Zeta.Time.timestamp Prims._assert FStar.Pervasives.Native.Mktuple2 Prims.l_True Zeta.EAC.eac_add Prims.op_disEquality Zeta.EAC.EACFail Zeta.High.Interleave.eac_state_snoc Zeta.High.Verifier.store_t Zeta.High.Interleave.thread_store_pre Prims.nat Prims.op_LessThan Zeta.Interleave.src Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.index Zeta.High.Interleave.mk_vlog_entry_ext Zeta.High.Interleave.eac_state_of_key Zeta.Generic.Interleave.verifiable_log Zeta.Generic.Interleave.prefix Prims.int Prims.op_Subtraction Prims.squash Prims.l_imp Zeta.GenericVerifier.uu___is_AddM Prims.l_and Prims.l_or Zeta.Generic.Interleave.is_blum_evict Zeta.BinTree.bin_tree_node Prims.op_LessThanOrEqual Zeta.BinTree.depth Zeta.Key.key_size Zeta.GenericVerifier.evict_slot Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.__proj__MHDom__item__t Zeta.Thread.thread_id Zeta.MultiSetHashDomain.__proj__MHDom__item__tid Prims.logical Zeta.Record.record Zeta.MultiSetHashDomain.__proj__MHDom__item__r Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.Generic.Interleave.blum_evict_elem Zeta.GenericVerifier.uu___is_EvictM Zeta.Generic.Interleave.is_blum_add Zeta.GenericVerifier.add_slot Zeta.Generic.Interleave.blum_add_elem Zeta.GenericVerifier.uu___is_RunApp FStar.Pervasives.Native.tuple2 Prims.l_False Prims.Nil FStar.Pervasives.pattern
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 _ _ _ _ ->
      assert (match es', es with | EACEvictedBlum gk v t tid, EACInStore _ gk' _ -> True);
      ()
    | _ -> ())