val empty_store_rel (vcfg: verifier_config)
    : Lemma (ensures ((empty_store vcfg) `store_rel` (HV.empty_store vcfg.app)))
val empty_store_rel (vcfg: verifier_config)
    : Lemma (ensures ((empty_store vcfg) `store_rel` (HV.empty_store vcfg.app)))
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
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
/
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
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config
  -> FStar.Pervasives.Lemma
    (ensures
      Zeta.Intermediate.Store.store_rel (Zeta.Intermediate.Store.empty_store vcfg)
        (Zeta.High.Verifier.empty_store (VConfig?.app vcfg)))
Zeta.Intermediate.VerifierConfig.verifier_config FStar.Classical.forall_intro Zeta.Key.base_key Prims.l_and Prims.b2t Zeta.High.Verifier.store_contains Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.Store.store_contains_key Prims.op_Equality 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 Prims._assert Prims.op_Negation Zeta.Intermediate.Store.lemma_empty_contains_nokey Zeta.Intermediate.Store.inuse_slot_id Zeta.Intermediate.Store.stored_base_key Zeta.Intermediate.Store.is_map Zeta.High.Verifier.store_t Zeta.High.Verifier.empty_store Zeta.Intermediate.Store.vstore Zeta.Intermediate.Store.empty_store Zeta.Intermediate.Store.store_rel
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