val int_appfn_succ (#vcfg: _) (a: appfn_rel_t vcfg) : GTot bool
val int_appfn_succ (#vcfg: _) (a: appfn_rel_t vcfg) : GTot bool
let int_appfn_succ (#vcfg:_) (a: appfn_rel_t vcfg)
  : GTot bool
  = let GV.RunApp f p _ = a.e in
    let ss = int_slots a in
    contains_distinct_app_keys a &&
    S.length ss = appfn_arity f &&
    (let rs = int_reads a in
     let fn = appfn f in
     let rc,_,_ = fn p rs in
     rc = Fn_success
    )
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)

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))

let lemma_appfn_slot_key_rel (#vcfg:_) (a: appfn_rel_t vcfg)
  : Lemma (ensures (slot_key_list_rel (int_store a) (hi_store a) (int_slots a) (hi_slots a)))
  = ()

let to_hv_store (#vcfg:_) (vsk: HV.vtls_t vcfg.app)
  : HV.store_t vcfg.app
  = vsk.st

let contains_distinct_app_keys_rel_aux (#vcfg:_)
  (vss: vtls_t vcfg {vss.valid})
  (vsk: _ {vtls_rel vss vsk})
  (ss: _ {all_slots_inuse vss.st ss})
  (ks: _ {let sts = vss.st in
          let stk = to_hv_store vsk in
          slot_key_list_rel sts stk ss ks})
  : Lemma (ensures (let intspec = int_verifier_spec vcfg in
                    let hispec = HV.high_verifier_spec vcfg.app in
                    GV.contains_distinct_app_keys #intspec vss ss <==>
                    GV.contains_distinct_app_keys #hispec vsk ks))
  = ()

let contains_distinct_app_keys_rel (#vcfg:_) (a: appfn_rel_t vcfg)
  : Lemma (ensures (let intspec = int_verifier_spec vcfg in
                    let hispec = HV.high_verifier_spec vcfg.app in
                    GV.contains_distinct_app_keys #intspec (int_state a) (int_slots a) <==>
                    GV.contains_distinct_app_keys #hispec (hi_state a) (hi_slots a)))
  = let vss = int_state a in
    let vsk = hi_state a in
    let ss = int_slots a in
    let ks = hi_slots a in
    contains_distinct_app_keys_rel_aux vss vsk ss ks

let contains_distinct_app_keys (#vcfg:_) (a: appfn_rel_t vcfg)
  : GTot bool
  = let intspec = int_verifier_spec vcfg in
    let hispec = HV.high_verifier_spec vcfg.app in
    GV.contains_distinct_app_keys_comp #intspec (int_state a) (int_slots a) &&
    GV.contains_distinct_app_keys_comp #hispec (hi_state a) (hi_slots a)

let distinct_slots (#vcfg:_) (ss: S.seq (slot_id vcfg))
  = forall i1 i2. i1 <> i2 ==> S.index ss i1 <> S.index ss i2

let int_slots_distinct (#vcfg:_) (a: appfn_rel_t vcfg {contains_distinct_app_keys a})
  : Lemma (ensures (distinct_slots (int_slots a)))
  = let ss = int_slots a in
    let aux (i1 i2:_)
      : Lemma (i1 <> i2 ==> S.index ss i1 <> S.index ss i2)
      = if i1 <> i2 then (
          ()
        )
    in
    forall_intro_2 aux

let int_reads (#vcfg:_) (a: appfn_rel_t vcfg {contains_distinct_app_keys a})
  : GTot (S.seq (app_record vcfg.app.adm))
  = let intspec = int_verifier_spec vcfg in
    GV.reads #intspec (int_state a) (int_slots a)

let hi_reads (#vcfg:_) (a: appfn_rel_t vcfg {contains_distinct_app_keys a})
  : GTot (S.seq (app_record vcfg.app.adm))
  = let hispec = HV.high_verifier_spec vcfg.app in
    GV.reads #hispec (hi_state a) (hi_slots a)

let reads_rel (#vcfg:_) (a: appfn_rel_t vcfg)
  : Lemma (requires (contains_distinct_app_keys a))
          (ensures (int_reads a == hi_reads a))
  = let intspec = int_verifier_spec vcfg in
    let hispec = HV.high_verifier_spec vcfg.app in
    let vss = int_state a in
    let ss = int_slots a in
    let rss = GV.reads #intspec vss ss in

    let vsk = hi_state a  in
    let ks = hi_slots a in
    let rsk = GV.reads #hispec vsk ks in

    assert(S.length rss = S.length rsk);
    let aux (i:_)
      : Lemma (ensures (S.index rss i == S.index rsk i))
      = ()
    in
    forall_intro aux;
    assert(S.equal rss rsk)
/
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
a: Zeta.Intermediate.StateRel.appfn_rel_t vcfg -> Prims.GTot Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.StateRel.appfn_rel_t Zeta.App.appfn_id Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Prims.op_AmpAmp Zeta.Intermediate.StateRel.contains_distinct_app_keys Prims.op_Equality Prims.nat FStar.Seq.Base.length Zeta.Intermediate.VerifierConfig.slot_id Zeta.App.appfn_arity Zeta.App.fn_return_code Zeta.App.interp_code Zeta.App.__proj__Mkapp_params__item__adm Zeta.App.__proj__Mkfn_sig__item__fres_t FStar.Map.sel Zeta.App.fn_id Zeta.App.fn_sig Zeta.App.__proj__Mkapp_params__item__tbl Zeta.App.app_value_nullable Prims.eq2 Zeta.App.__proj__Mkfn_sig__item__arity Zeta.App.Fn_success Prims.bool FStar.Pervasives.Native.tuple3 Zeta.App.app_fn_t Zeta.App.__proj__Mkfn_sig__item__farg_t Zeta.App.appfn Zeta.App.app_record Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.StateRel.int_reads Zeta.Intermediate.StateRel.all_slots_inuse Zeta.Intermediate.StateRel.int_store Zeta.Intermediate.StateRel.int_slots Zeta.Intermediate.Verifier.logS_entry Prims.l_and Prims.b2t Zeta.GenericVerifier.is_appfn Zeta.Intermediate.StateRel.valid_logS_entry Zeta.Intermediate.StateRel.__proj__AFR__item__vss Zeta.Intermediate.StateRel.__proj__AFR__item__e
let int_appfn_succ (#vcfg: _) (a: appfn_rel_t vcfg) : GTot bool =
  
let GV.RunApp f p _ = a.e in
let ss = int_slots a in
contains_distinct_app_keys a && S.length ss = appfn_arity f &&
(let rs = int_reads a in
  let fn = appfn f in
  let rc, _, _ = fn p rs in
  rc = Fn_success)