val write_slots_prop
      (tsm: s_thread_state)
      (slots: Seq.seq s_slot_id {TSM.valid_app_slots tsm slots})
      (values: Seq.seq (A.app_value_nullable app.A.adm) {Seq.length slots = Seq.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          identical_except_store tsm tsm_))
      (decreases (Seq.length slots))
      [SMTPat (write_slots tsm slots values)]
val write_slots_prop
      (tsm: s_thread_state)
      (slots: Seq.seq s_slot_id {TSM.valid_app_slots tsm slots})
      (values: Seq.seq (A.app_value_nullable app.A.adm) {Seq.length slots = Seq.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          identical_except_store tsm tsm_))
      (decreases (Seq.length slots))
      [SMTPat (write_slots tsm slots values)]
let rec write_slots_prop (tsm: s_thread_state)
                         (slots: Seq.seq s_slot_id {TSM.valid_app_slots tsm slots})
                         (values: Seq.seq (A.app_value_nullable app.A.adm) {Seq.length slots = Seq.length values})
  : Lemma (ensures (let tsm_ = write_slots tsm slots values in
                    identical_except_store tsm tsm_))
          (decreases (Seq.length slots))
          [SMTPat (write_slots tsm slots values)]
  = let n = Seq.length slots in
    if n > 0 then
    begin
      let hd_slot = Seq.head slots in
      let tl = Seq.tail slots in
      assert (slots `Seq.equal` Seq.cons hd_slot tl);
      Classical.forall_intro (Seq.contains_cons hd_slot tl);
      let hd_value =
        match Seq.head values with
        | A.Null -> T.DValue None
        | A.DValue d -> T.DValue (Some d)
      in
      let tsm2 = update_value tsm hd_slot hd_value in
      lemma_update_value tsm hd_slot hd_value;
      assert (identical_except_store tsm tsm2);
      write_slots_prop tsm2 (Seq.tail slots) (Seq.tail values);
      ()
    end
module Zeta.Steel.AppSim

open Zeta.Steel.ThreadStateModel
open Zeta.Steel.Rel
open Zeta.Steel.LogRel
open Zeta.Steel.StoreRel
open Zeta.Steel.ThreadRelDef
open Zeta.Steel.AddMRel
open FStar.Classical

module M = Zeta.Merkle
module R = Zeta.Record
module KU = Zeta.Steel.KeyUtils
module TSM = Zeta.Steel.ThreadStateModel
module GK = Zeta.GenKey
module IS = Zeta.Intermediate.Store

module A = Zeta.App
module AT = Zeta.Steel.ApplicationTypes
module T = Zeta.Steel.FormatsManual
module U16 = FStar.UInt16
module GV = Zeta.GenericVerifier
module IV = Zeta.Intermediate.Verifier

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

let related_slots (slots: Seq.seq s_slot_id) (i_slots: Seq.seq i_slot_id)
  = let open FStar.Seq in
    length slots = length i_slots /\
    (forall i. related_slot (index slots i) (index i_slots i))

(* read_slots succeeds on the list of slots; essentially each slot is occupied and contains an app record *)
let valid_app_slots (tsm: s_thread_state) (slots: Seq.seq s_slot_id)
  = Some? (read_slots tsm slots)

let rec valid_app_slots_implies_app_recs (tsm: s_thread_state) (slots: Seq.seq s_slot_id)
  : Lemma (requires (valid_app_slots tsm slots))
          (ensures (let st = tsm.store in
                    forall i. (let s = Seq.index slots i in
                           U16.v s < U16.v AT.store_size /\
                           inuse_slot st s /\
                           T.ApplicationKey? (stored_key st s))))
          (decreases (Seq.length slots))
          [SMTPat (valid_app_slots tsm slots)]
  = let n = Seq.length slots in
    let st = tsm.store in
    if n = 0 then ()
    else
    begin
      let hd = Seq.head slots in
      let tl = Seq.tail slots in
      assert (U16.v hd < U16.v AT.store_size);
      assert (inuse_slot st hd);
      assert (T.ApplicationKey? (stored_key st hd));

      assert (valid_app_slots tsm tl);
      valid_app_slots_implies_app_recs tsm tl;

      let aux (i:_)
        : Lemma (ensures (let s = Seq.index slots i in
                          U16.v s < U16.v AT.store_size /\
                          inuse_slot st s /\
                          T.ApplicationKey? (stored_key st s)))
        = if i > 0 then
            assert (Seq.index slots i = Seq.index tl (i-1))
      in
      forall_intro aux
    end

module SA = Zeta.SeqAux

let valid_app_slots_prop (tsm: s_thread_state) (slots: Seq.seq s_slot_id) (i: SA.seq_index slots)
  : Lemma (requires (valid_app_slots tsm slots))
          (ensures (let s = Seq.index slots i in
                    let st = tsm.store in
                    U16.v s < U16.v AT.store_size /\
                    inuse_slot st s /\
                    T.ApplicationKey? (stored_key st s)))
  = let s = Seq.index slots i in
    let st = tsm.store in
    valid_app_slots_implies_app_recs tsm slots;
    eliminate forall i. (let s = Seq.index slots i in
                           U16.v s < U16.v AT.store_size /\
                           inuse_slot st s /\
                           T.ApplicationKey? (stored_key st s))
    with i

#pop-options

#push-options "--z3rlimit_factor 3"

(* the key of the i'th record returned by read_slots is the key stored in i'th slot *)
let rec read_slots_key_idx (tsm: s_thread_state) (slots: Seq.seq s_slot_id) (i: SA.seq_index slots)
  : Lemma (requires (not tsm.failed /\ valid_app_slots tsm slots))
          (ensures (let s = Seq.index slots i in
                    let Some recs = read_slots tsm slots in
                    let keys = SA.map fst recs in
                    let ak1,_ = Seq.index recs i in
                    let st = tsm.store in
                    let T.ApplicationKey ak2 = stored_key st s in
                    ak1 = ak2 /\
                    ak1 = Seq.index keys i))
          (decreases (Seq.length slots))
  = let n = Seq.length slots in
    if n > 0 && i > 0 then
      read_slots_key_idx tsm (Seq.tail slots) (i-1)

let rec read_slots_val_idx (tsm: s_thread_state) (slots: Seq.seq s_slot_id) (i: SA.seq_index slots)
  : Lemma (requires (not tsm.failed /\ valid_app_slots tsm slots))
          (ensures (let s = Seq.index slots i in
                    let Some recs = read_slots tsm slots in
                    let _,av1 = Seq.index recs i in
                    let v = stored_value tsm.store s in
                    match v with
                    | T.MValue _ -> False
                    | T.DValue v -> match v with
                                 | None -> av1 = A.Null
                                 | Some v -> av1 = A.DValue v))
          (decreases (Seq.length slots))
  = let n = Seq.length slots in
    if n > 0 && i > 0 then
      read_slots_val_idx tsm (Seq.tail slots) (i-1)

#pop-options
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRelDef.fst.checked Zeta.Steel.StoreRel.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogRel.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AddMRel.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt16.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Steel.AppSim.fst

    tsm: Zeta.Steel.Rel.s_thread_state ->
    slots:
      FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id
        {Zeta.Steel.ThreadStateModel.valid_app_slots tsm slots} ->
    values:
      FStar.Seq.Base.seq (Zeta.App.app_value_nullable (Mkapp_params?.adm Zeta.Steel.Rel.app))
        {FStar.Seq.Base.length slots = FStar.Seq.Base.length values}
  -> FStar.Pervasives.Lemma
      (ensures
        (let tsm_ = Zeta.Steel.ThreadStateModel.write_slots tsm slots values in
          Zeta.Steel.StoreRel.identical_except_store tsm tsm_))
      (decreases FStar.Seq.Base.length slots)
      [SMTPat (Zeta.Steel.ThreadStateModel.write_slots tsm slots values)]
Zeta.Steel.Rel.s_thread_state FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id Zeta.Steel.ThreadStateModel.valid_app_slots Zeta.App.app_value_nullable Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.Rel.app Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length Prims.op_GreaterThan Prims.unit Zeta.Steel.AppSim.write_slots_prop FStar.Seq.Properties.tail Prims._assert Zeta.Steel.StoreRel.identical_except_store Zeta.Steel.StoreRel.lemma_update_value Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.update_value Zeta.Steel.LogEntry.Types.value Prims.l_and Zeta.Steel.LogEntry.Types.is_value_of Zeta.Steel.ThreadStateModel.key_of_slot FStar.Seq.Properties.head Zeta.Steel.LogEntry.Types.DValue FStar.Pervasives.Native.None Zeta.Steel.ApplicationTypes.value_type Zeta.App.app_value FStar.Pervasives.Native.Some FStar.Classical.forall_intro Prims.l_iff FStar.Seq.Properties.contains FStar.Seq.Base.cons Prims.l_or Prims.eq2 FStar.Seq.Properties.contains_cons FStar.Seq.Base.equal Prims.bool Prims.l_True Prims.squash Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_verified_epoch Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__clock Zeta.Steel.KeyUtils.base_key Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_evict_key Zeta.Steel.ThreadStateModel.epoch_hashes Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__epoch_hashes Zeta.Steel.ThreadStateModel.app_results Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__app_results Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.ThreadStateModel.write_slots Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let rec write_slots_prop
      (tsm: s_thread_state)
      (slots: Seq.seq s_slot_id {TSM.valid_app_slots tsm slots})
      (values: Seq.seq (A.app_value_nullable app.A.adm) {Seq.length slots = Seq.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          identical_except_store tsm tsm_))
      (decreases (Seq.length slots))
      [SMTPat (write_slots tsm slots values)] =
  
let n = Seq.length slots in
if n > 0
then
  let hd_slot = Seq.head slots in
  let tl = Seq.tail slots in
  assert (slots `Seq.equal` (Seq.cons hd_slot tl));
  Classical.forall_intro (Seq.contains_cons hd_slot tl);
  let hd_value =
    match Seq.head values with
    | A.Null -> T.DValue None
    | A.DValue d -> T.DValue (Some d)
  in
  let tsm2 = update_value tsm hd_slot hd_value in
  lemma_update_value tsm hd_slot hd_value;
  assert (identical_except_store tsm tsm2);
  write_slots_prop tsm2 (Seq.tail slots) (Seq.tail values);
  ()