val slot_key_list_rel : sts: Zeta.Intermediate.Store.vstore vcfg ->
    stk: Zeta.High.Verifier.store_t (VConfig?.app vcfg) {Zeta.Intermediate.Store.store_rel sts stk} ->
    ss:
      FStar.Seq.Base.seq (Zeta.Intermediate.VerifierConfig.slot_id vcfg)
        {Zeta.Intermediate.StateRel.all_slots_inuse sts ss} ->
    ks: FStar.Seq.Base.seq Zeta.Key.base_key
  -> Prims.logical
let slot_key_list_rel (#vcfg:_)
  (sts: vstore vcfg)
  (stk: _ {store_rel sts stk})
  (ss: _ {all_slots_inuse sts ss})
  (ks: S.seq base_key)
  = S.length ss = S.length ks /\
    (forall i. (stored_base_key sts (S.index ss i) = S.index ks i))
module Zeta.Intermediate.StateRel

open FStar.Classical
open Zeta.BinTree
open Zeta.SeqIdx
open Zeta.App
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.HashFunction

module SA = Zeta.SeqAux

let empty_store_rel
  (vcfg: verifier_config)
  : Lemma (ensures (empty_store vcfg `store_rel` HV.empty_store vcfg.app))
  = let sts = empty_store vcfg in
    let stk = HV.empty_store vcfg.app in

    assert(is_map sts);
    let aux (k:_)
      : Lemma (ensures ((store_contains_key sts k = HV.store_contains stk k) /\
                       (store_contains_key sts k ==>
                       (let s = slot_of_key sts k in
                       stored_key sts s = HV.stored_key stk k /\
                       stored_value sts s = HV.stored_value stk k /\
                       add_method_of sts s = HV.add_method_of stk k))))
      = lemma_empty_contains_nokey #vcfg k;
        assert(not (store_contains_key sts k));
        assert(not (HV.store_contains stk k));
        ()
    in
    forall_intro aux

let lemma_empty_vtls_rel
  (#vcfg: verifier_config)
  (t:nat{t < vcfg.thread_count})
  : Lemma (ensures (let vss = init_thread_state vcfg t in
                    let vsk = HV.init_thread_state vcfg.app t in
                    vtls_rel vss vsk))
  = let vss = init_thread_state vcfg t in
    let sts = vss.st in
    let _sts = empty_store vcfg in
    let vsk = HV.init_thread_state vcfg.app t in
    let _stk = HV.empty_store vcfg.app in
    let stk = vsk.st in
    assert(vss.valid = vsk.valid /\ vss.tid = vsk.tid /\ vss.clock = vsk.clock);
    empty_store_rel vcfg;
    if t = 0 then
      let aux (k:_)
        : Lemma (ensures ((store_contains_key sts k = HV.store_contains stk k) /\
                         (store_contains_key sts k ==>
                         (let s = slot_of_key sts k in
                         stored_key sts s = HV.stored_key stk k /\
                         stored_value sts s = HV.stored_value stk k /\
                         add_method_of sts s = HV.add_method_of stk k))))
        = ()
      in
      forall_intro aux

(* all slots in a sequence in use *)
let all_slots_inuse (#vcfg:_) (st: vstore vcfg) (ss: S.seq (slot_id vcfg))
  = forall i. (inuse_slot st (S.index ss i))

let all_slots_inuse_comp (#vcfg:_) (st: vstore vcfg) (ss: S.seq (slot_id vcfg))
  : b:bool {b <==> all_slots_inuse st ss}
  = not (exists_elems_with_prop_comp (fun s -> empty_slot st s) ss)

noeq type appfn_rel_t (vcfg: verifier_config) =
  | AFR: vss: vtls_t vcfg {vss.valid} ->
         vsk: _ {vtls_rel vss vsk} ->
         e: logS_entry vcfg {GV.is_appfn e /\ valid_logS_entry vss e} -> appfn_rel_t vcfg

let int_state (#vcfg:_) (a: appfn_rel_t vcfg)
  = a.vss

let int_store (#vcfg:_) (a: appfn_rel_t vcfg)
  = a.vss.st

let hi_state (#vcfg:_)  (a: appfn_rel_t vcfg)
  : HV.vtls_t vcfg.app
  = a.vsk

let hi_store (#vcfg:_) (a: appfn_rel_t vcfg)
  : HV.store_t vcfg.app
  = (hi_state a).st

let int_slots (#vcfg:_) (a: appfn_rel_t vcfg)
  : ss:S.seq (slot_id vcfg) {all_slots_inuse (int_store a) ss}
  = GV.RunApp?.rs a.e

let hi_entry (#vcfg:_) (a: appfn_rel_t vcfg)
  : logK_entry vcfg.app
  = to_logk_entry a.vss a.e

let hi_slots (#vcfg:_) (a: appfn_rel_t vcfg)
  : S.seq base_key
  = GV.RunApp?.rs (hi_entry a)
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Key.fsti.checked Zeta.HashFunction.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.StateRel.fst

    sts: Zeta.Intermediate.Store.vstore vcfg ->
    stk: Zeta.High.Verifier.store_t (VConfig?.app vcfg) {Zeta.Intermediate.Store.store_rel sts stk} ->
    ss:
      FStar.Seq.Base.seq (Zeta.Intermediate.VerifierConfig.slot_id vcfg)
        {Zeta.Intermediate.StateRel.all_slots_inuse sts ss} ->
    ks: FStar.Seq.Base.seq Zeta.Key.base_key
  -> Prims.logical
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore Zeta.High.Verifier.store_t Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.Store.store_rel FStar.Seq.Base.seq Zeta.Intermediate.VerifierConfig.slot_id Zeta.Intermediate.StateRel.all_slots_inuse Zeta.Key.base_key Prims.l_and Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length Prims.l_Forall Prims.op_LessThan Zeta.Intermediate.Store.stored_base_key FStar.Seq.Base.index Prims.logical
let slot_key_list_rel
      (#vcfg: _)
      (sts: vstore vcfg)
      (stk: _{store_rel sts stk})
      (ss: _{all_slots_inuse sts ss})
      (ks: S.seq base_key)
     =
  
S.length ss = S.length ks /\ (forall i. (stored_base_key sts (S.index ss i) = S.index ks i))