val lemma_runapp_simulates_spec
      (#vcfg:_)
      (vs:vtls_t vcfg{vs.valid})
      (vs':_ {vtls_rel vs vs'})
      (e:logS_entry vcfg{GV.is_appfn e})
  : Lemma (requires (valid_logS_entry vs e))
          (ensures (let ek = to_logk_entry vs e in
                    vtls_rel (GV.verify_step e vs) (GV.verify_step ek vs')))
val lemma_runapp_simulates_spec
      (#vcfg:_)
      (vs:vtls_t vcfg{vs.valid})
      (vs':_ {vtls_rel vs vs'})
      (e:logS_entry vcfg{GV.is_appfn e})
  : Lemma (requires (valid_logS_entry vs e))
          (ensures (let ek = to_logk_entry vs e in
                    vtls_rel (GV.verify_step e vs) (GV.verify_step ek vs')))
let lemma_runapp_simulates_spec
      (#vcfg:_)
      (vss:vtls_t vcfg{vss.valid})
      (vsk:_ {vtls_rel vss vsk})
      (e:logS_entry vcfg{GV.is_appfn e})
  : Lemma (requires (valid_logS_entry vss e))
          (ensures (let ek = to_logk_entry vss e in
                    vtls_rel (GV.verify_step e vss) (GV.verify_step ek vsk)))
  = let a = AFR vss vsk e in
    let ek = hi_entry a in
    let vss_ = GV.verify_step e vss in
    let vsk_: HV.vtls_t vcfg.app = GV.verify_step ek vsk in
    let GV.RunApp f p ss = e in
    let ks = hi_slots a in
    let stk = hi_store a in
    let sts = vss.st in

    contains_distinct_app_keys_rel a;
    if contains_distinct_app_keys a && S.length ss = appfn_arity f then (
      reads_rel a;
      lemma_appfn_succ_rel a;
      if int_appfn_succ a then (
        assert (hi_appfn_succ a);
        writes_rel a;
        let wss = int_writes a in
        let wsk = hi_writes a in
        assert (wss == wsk);
        assert(vss_ == puts vss ss wss);
        assert(vsk_ == HV.puts vsk ks wsk);
        assert (vss_.valid = vsk_.valid);
        assert (vss_.clock = vsk_.clock);
        assert (vss_.tid = vsk_.tid);
        lemma_contains_only_app_keys a;
        let sts_ = vss_.st in
        let stk_ = vsk_.st in
        assert (vss_.st == puts_store vss.st ss wss);
        assert (vsk_.st == HV.puts_store stk ks wsk);
        assert(HV.contains_only_app_keys stk ks);
        int_slots_distinct a;
        lemma_puts_store_rel sts stk ss ks wss
      )
      else (
        assert (GV.contains_distinct_app_keys_comp vss ss);
        assert (S.length ss = appfn_arity f);
        let fn = appfn f in
        let rc,_,_ = fn p (hi_reads a) in
        assert (rc == Fn_failure);
        let rs = GV.reads vss ss in
        assert(rs == int_reads a);
        assert (not (vss_.valid));
        assert (not (vsk_.valid))
      )
    )
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)

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
    )

let hi_appfn_succ (#vcfg:_) (a: appfn_rel_t vcfg)
  : GTot bool
  = let GV.RunApp f p _ = (hi_entry a) in
    let ks = hi_slots a in
    contains_distinct_app_keys a &&
    S.length ks = appfn_arity f &&
    (let rs = hi_reads a in
     let fn = appfn f in
     let rc,_,_ = fn p rs in
     rc = Fn_success
    )

let lemma_appfn_succ_rel (#vcfg:_) (a: appfn_rel_t vcfg)
  : Lemma (ensures (int_appfn_succ a = hi_appfn_succ a))
  = if contains_distinct_app_keys a then
      let ss = int_slots a in
      let ks = hi_slots a in
      let GV.RunApp f p _ = a.e in

      if S.length ss = appfn_arity f then
        reads_rel a

let int_writes (#vcfg:_) (a: appfn_rel_t vcfg {int_appfn_succ a})
  : GTot (ws:S.seq (app_value_nullable vcfg.app.adm){S.length ws = S.length (int_slots a)})
  = let GV.RunApp f p _ = a.e in
    let ss = int_slots a in
    let rs = int_reads a in
    let fn = appfn f in
    let _,_,ws = fn p rs in
    ws

let hi_writes (#vcfg:_) (a: appfn_rel_t vcfg {hi_appfn_succ a})
  : GTot (ws:S.seq (app_value_nullable vcfg.app.adm){S.length ws = S.length (hi_slots a)})
  = let GV.RunApp f p _ = a.e in
    let ss = hi_slots a in
    let rs = hi_reads a in
    let fn = appfn f in
    let _,_,ws = fn p rs in
    ws

let writes_rel (#vcfg:_) (a: appfn_rel_t vcfg {int_appfn_succ a})
  : Lemma (ensures (hi_appfn_succ a /\ int_writes a == hi_writes a))
  = lemma_appfn_succ_rel a;
    assert(hi_appfn_succ a);
    reads_rel a

open Zeta.AppSimulate

let int_res (#vcfg:_) (a: appfn_rel_t vcfg {int_appfn_succ a})
  : GTot (appfn_call_res vcfg.app)
  = let GV.RunApp f p _ = a.e in
    let ss = int_slots a in
    let rs = int_reads a in
    let fn = appfn f in
    let rc,o,_ = fn p rs in
    {fid_cr = f; arg_cr = p; inp_cr = rs; res_cr = o}

let int_res_is_gv_res (#vcfg:_) (a: appfn_rel_t vcfg {int_appfn_succ a})
  : Lemma (ensures (GV.appfn_result a.e a.vss = int_res a))
  = ()

let hi_res (#vcfg:_) (a: appfn_rel_t vcfg {hi_appfn_succ a})
  : GTot (appfn_call_res vcfg.app)
  = let GV.RunApp f p _ = hi_entry a in
    let ss = hi_slots a in
    let rs = hi_reads a in
    let fn = appfn f in
    let fc,o,_ = fn p rs in
    {fid_cr = f; arg_cr = p; inp_cr = rs; res_cr = o}

let hi_res_is_gv_res (#vcfg:_) (a: appfn_rel_t vcfg {hi_appfn_succ a})
  : Lemma (ensures (GV.appfn_result (hi_entry a) (hi_state a) = hi_res a))
  = ()

let lemma_res_rel (#vcfg:_) (a: appfn_rel_t vcfg {int_appfn_succ a})
  : Lemma (ensures (hi_appfn_succ a /\
                    int_res a = hi_res a))
  = lemma_appfn_succ_rel a;
    reads_rel a

let lemma_contains_only_app_keys (#vcfg:_) (a: appfn_rel_t vcfg{contains_distinct_app_keys a})
  : Lemma (ensures (contains_only_app_keys (int_store a) (int_slots a)))
  = ()

#push-options "--fuel 1 --ifuel 1 --query_stats"

let lemma_puts_store_rel
  (#vcfg:_)
  (sts: vstore vcfg)
  (stk: _ {store_rel sts stk})
  (ss: S.seq (slot_id vcfg) {contains_only_app_keys sts ss /\ distinct_slots ss})
  (ks: S.seq base_key {slot_key_list_rel sts stk ss ks})
  (ws: S.seq (app_value_nullable vcfg.app.adm){S.length ws = S.length ss})
  : Lemma (requires (HV.contains_only_app_keys stk ks))
          (ensures (let sts_ = puts_store sts ss ws in
                    let stk_ = HV.puts_store stk ks ws in
                    store_rel sts_ stk_))
  = let sts_ = puts_store sts ss ws in
    let stk_ = HV.puts_store stk ks ws in
    assert(is_map sts_);
    let aux (k:_)
      : Lemma (ensures (store_rel_key sts_ stk_ k))
      = if S.mem k ks then (
          let i = S.index_mem k ks in
          eliminate forall i. (stored_base_key sts (S.index ss i) = S.index ks i) with i;
          let si = S.index ss i in
          assert(HV.stored_value stk_ k = AppV (S.index ws i));
          puts_preserves sts ss ws si;
          puts_ref_value sts ss ws si;
          SA.lemma_elem_idx_uniq ss i;
          assert (i = S.index_mem si ss);
          assert (stored_value sts_ si = AppV (S.index ws i));
          ()
        )
        else (
          assert (stk_ k = stk k);
          if HV.store_contains stk_ k then (
             assert (HV.store_contains stk k);
             assert (store_contains_key sts k);
             let si = slot_of_key sts k in
             puts_preserves sts ss ws si;
             if S.mem si ss then (
               let i = S.index_mem si ss in
               eliminate forall i. (stored_base_key sts (S.index ss i) = S.index ks i) with i
             )
             else puts_preserves_non_ref sts ss ws si
          )
          else (
            assert(not (HV.store_contains stk k));
            assert (not (store_contains_key sts k));
            if store_contains_key sts_ k then (
               let si = slot_of_key sts_ k in
               puts_preserves sts ss ws si
            )
          )
        )
    in
    forall_intro aux

#pop-options

#push-options "--z3rlimit_factor 8"
/
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

    vs: Zeta.Intermediate.Verifier.vtls_t vcfg {Mkvtls_t?.valid vs} ->
    vs': Zeta.High.Verifier.vtls_t (VConfig?.app vcfg) {Zeta.Intermediate.StateRel.vtls_rel vs vs'} ->
    e: Zeta.Intermediate.Verifier.logS_entry vcfg {Zeta.GenericVerifier.is_appfn e}
  -> FStar.Pervasives.Lemma (requires Zeta.Intermediate.StateRel.valid_logS_entry vs e)
      (ensures
        (let ek = Zeta.Intermediate.StateRel.to_logk_entry vs e in
          Zeta.Intermediate.StateRel.vtls_rel (Zeta.GenericVerifier.verify_step e vs)
            (Zeta.GenericVerifier.verify_step ek vs')))
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Verifier.vtls_t Prims.b2t Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__valid Zeta.High.Verifier.vtls_t Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.StateRel.vtls_rel Zeta.Intermediate.Verifier.logS_entry Zeta.GenericVerifier.is_appfn Zeta.Intermediate.Verifier.int_verifier_spec Zeta.App.appfn_id Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app 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.App.appfn_arity Zeta.Intermediate.StateRel.int_appfn_succ Zeta.Intermediate.StateRel.lemma_puts_store_rel Prims.unit Zeta.Intermediate.StateRel.int_slots_distinct Prims._assert Zeta.High.Verifier.contains_only_app_keys Prims.eq2 Zeta.High.Verifier.store_t Zeta.High.Verifier.__proj__Mkvtls_t__item__st Zeta.High.Verifier.puts_store Zeta.Intermediate.Store.vstore Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Zeta.Intermediate.Store.puts_store Zeta.Intermediate.StateRel.lemma_contains_only_app_keys 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 Prims.bool Zeta.High.Verifier.__proj__Mkvtls_t__item__valid Zeta.High.Verifier.puts Zeta.Intermediate.Verifier.puts Zeta.App.app_value_nullable Zeta.App.__proj__Mkapp_params__item__adm Prims.l_or Zeta.Intermediate.VerifierConfig.slot_id Zeta.Intermediate.StateRel.int_slots Zeta.Key.base_key Zeta.Intermediate.StateRel.hi_slots Zeta.Intermediate.StateRel.hi_writes Zeta.Intermediate.StateRel.int_writes Zeta.Intermediate.StateRel.writes_rel Zeta.Intermediate.StateRel.hi_appfn_succ Zeta.App.fn_return_code Zeta.App.interp_code 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.__proj__Mkfn_sig__item__arity Prims.op_Negation Zeta.App.app_record Zeta.Intermediate.StateRel.int_reads Zeta.GenericVerifier.reads Zeta.App.Fn_failure FStar.Pervasives.Native.tuple3 Zeta.Intermediate.StateRel.hi_reads Zeta.App.app_fn_t Zeta.App.__proj__Mkfn_sig__item__farg_t Zeta.App.appfn Zeta.GenericVerifier.contains_distinct_app_keys_comp Zeta.Intermediate.StateRel.lemma_appfn_succ_rel Zeta.Intermediate.StateRel.reads_rel Zeta.Intermediate.StateRel.contains_distinct_app_keys_rel Zeta.Intermediate.StateRel.hi_store Zeta.GenericVerifier.verify_step Zeta.High.Verifier.high_verifier_spec Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Intermediate.Logs.logK_entry Zeta.Intermediate.StateRel.hi_entry Zeta.Intermediate.StateRel.appfn_rel_t Zeta.Intermediate.StateRel.AFR Zeta.Intermediate.StateRel.valid_logS_entry Prims.squash Zeta.Intermediate.StateRel.to_logk_entry Prims.Nil FStar.Pervasives.pattern
let lemma_runapp_simulates_spec
      (#vcfg: _)
      (vss: vtls_t vcfg {vss.valid})
      (vsk: _{vtls_rel vss vsk})
      (e: logS_entry vcfg {GV.is_appfn e})
    : Lemma (requires (valid_logS_entry vss e))
      (ensures
        (let ek = to_logk_entry vss e in
          vtls_rel (GV.verify_step e vss) (GV.verify_step ek vsk))) =
  
let a = AFR vss vsk e in
let ek = hi_entry a in
let vss_ = GV.verify_step e vss in
let vsk_:HV.vtls_t vcfg.app = GV.verify_step ek vsk in
let GV.RunApp f p ss = e in
let ks = hi_slots a in
let stk = hi_store a in
let sts = vss.st in
contains_distinct_app_keys_rel a;
if contains_distinct_app_keys a && S.length ss = appfn_arity f
then
  (reads_rel a;
    lemma_appfn_succ_rel a;
    if int_appfn_succ a
    then
      (assert (hi_appfn_succ a);
        writes_rel a;
        let wss = int_writes a in
        let wsk = hi_writes a in
        assert (wss == wsk);
        assert (vss_ == puts vss ss wss);
        assert (vsk_ == HV.puts vsk ks wsk);
        assert (vss_.valid = vsk_.valid);
        assert (vss_.clock = vsk_.clock);
        assert (vss_.tid = vsk_.tid);
        lemma_contains_only_app_keys a;
        let sts_ = vss_.st in
        let stk_ = vsk_.st in
        assert (vss_.st == puts_store vss.st ss wss);
        assert (vsk_.st == HV.puts_store stk ks wsk);
        assert (HV.contains_only_app_keys stk ks);
        int_slots_distinct a;
        lemma_puts_store_rel sts stk ss ks wss)
    else
      (assert (GV.contains_distinct_app_keys_comp vss ss);
        assert (S.length ss = appfn_arity f);
        let fn = appfn f in
        let rc, _, _ = fn p (hi_reads a) in
        assert (rc == Fn_failure);
        let rs = GV.reads vss ss in
        assert (rs == int_reads a);
        assert (not (vss_.valid));
        assert (not (vsk_.valid))))