val 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))
val 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 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
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
/
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
t: Prims.nat{t < VConfig?.thread_count vcfg}
  -> FStar.Pervasives.Lemma
    (ensures
      (let vss = Zeta.Intermediate.Verifier.init_thread_state vcfg t in
        let vsk = Zeta.High.Verifier.init_thread_state (VConfig?.app vcfg) t in
        Zeta.Intermediate.StateRel.vtls_rel vss vsk))
Zeta.Intermediate.VerifierConfig.verifier_config Prims.nat Prims.b2t Prims.op_LessThan Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Prims.op_Equality Prims.int FStar.Classical.forall_intro Zeta.Key.base_key Prims.l_and Zeta.High.Verifier.store_contains Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.Store.store_contains_key Prims.bool Prims.l_imp Zeta.GenKey.key Zeta.Intermediate.Store.stored_key Zeta.Intermediate.Store.slot_of_key Zeta.High.Verifier.stored_key Zeta.Record.value Zeta.Intermediate.Store.stored_value Zeta.High.Verifier.stored_value Zeta.High.Verifier.add_method Zeta.Intermediate.Store.add_method_of Zeta.High.Verifier.add_method_of Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.Intermediate.Store.inuse_slot_id Zeta.Intermediate.Store.stored_base_key Zeta.Intermediate.StateRel.empty_store_rel Prims._assert Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__valid Zeta.High.Verifier.__proj__Mkvtls_t__item__valid Zeta.Thread.thread_id Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__tid Zeta.High.Verifier.__proj__Mkvtls_t__item__tid Zeta.Time.timestamp Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__clock Zeta.High.Verifier.__proj__Mkvtls_t__item__clock Zeta.High.Verifier.store_t Zeta.High.Verifier.__proj__Mkvtls_t__item__st Zeta.High.Verifier.empty_store Zeta.High.Verifier.vtls_t Zeta.High.Verifier.init_thread_state Zeta.Intermediate.Store.vstore Zeta.Intermediate.Store.empty_store Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Zeta.Intermediate.Verifier.vtls_t Zeta.Intermediate.Verifier.init_thread_state Zeta.Intermediate.StateRel.vtls_rel
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