val write_slots_non_store_prop
      (tsm: thread_state_model)
      (slots: _{TSM.valid_app_slots tsm slots})
      (values: S.seq (app_value_nullable app.adm) {S.length slots == S.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          tsm_.failed == tsm.failed /\ tsm_.clock == tsm.clock /\
          tsm_.epoch_hashes == tsm.epoch_hashes /\ tsm_.thread_id == tsm.thread_id /\
          tsm_.processed_entries == tsm.processed_entries /\ tsm_.app_results == tsm.app_results))
      (decreases (S.length slots))
val write_slots_non_store_prop
      (tsm: thread_state_model)
      (slots: _{TSM.valid_app_slots tsm slots})
      (values: S.seq (app_value_nullable app.adm) {S.length slots == S.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          tsm_.failed == tsm.failed /\ tsm_.clock == tsm.clock /\
          tsm_.epoch_hashes == tsm.epoch_hashes /\ tsm_.thread_id == tsm.thread_id /\
          tsm_.processed_entries == tsm.processed_entries /\ tsm_.app_results == tsm.app_results))
      (decreases (S.length slots))
let rec write_slots_non_store_prop
  (tsm: thread_state_model)
  (slots: _ {TSM.valid_app_slots tsm slots})
  (values: S.seq (app_value_nullable app.adm) {S.length slots == S.length values})
  : Lemma (ensures (let tsm_ = write_slots tsm slots values in
                    tsm_.failed == tsm.failed /\
                    tsm_.clock == tsm.clock /\
                    tsm_.epoch_hashes == tsm.epoch_hashes /\
                    tsm_.thread_id == tsm.thread_id /\
                    tsm_.processed_entries == tsm.processed_entries /\
                    tsm_.app_results == tsm.app_results))
          (decreases (S.length slots))
  = let tsm_ = write_slots tsm slots values in
    if S.length slots > 0 then (
      let hd_slot = S.head slots in
      let tl = S.tail slots in
      assert(slots `S.equal` S.cons hd_slot tl);
      Classical.forall_intro (Seq.contains_cons hd_slot tl);
      let hd_value =
        match Seq.head values with
        | Null -> T.DValue None
        | DValue d -> T.DValue (Some d)
      in
      let tsm = update_value tsm hd_slot hd_value in
      write_slots_non_store_prop tsm (S.tail slots) (S.tail values)
    )
module Zeta.Steel.ThreadRel

open FStar.Classical
open Zeta.Steel.ThreadSim
open Zeta.Steel.AppSim

module A = Zeta.App
module M = Zeta.Merkle
module R = Zeta.Record
module T = Zeta.Steel.FormatsManual
module S = FStar.Seq
module SA = Zeta.SeqAux
module KU = Zeta.Steel.KeyUtils
module GK = Zeta.GenKey
module IS = Zeta.Intermediate.Store
module SS = Zeta.Steel.StoreRel
module HA = Zeta.Steel.HashAccumulator
module LT = Zeta.Steel.LogEntry.Types

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

let addm_processed_entries_props (tsm: thread_state_model) (e: s_log_entry {T.AddM? e})
  : Lemma (ensures (let open T in
                    let LT.AddM s s' r = e in
                    let tsm_ = vaddm tsm s s' r in
                    tsm_.processed_entries == tsm.processed_entries))
  = ()

let addm_thread_id_prop (tsm: thread_state_model) (e: s_log_entry {T.AddM? e})
  : Lemma (ensures (let open T in
                    let AddM s s' r = e in
                    let tsm_ = vaddm tsm s s' r in
                    tsm_.thread_id == tsm.thread_id))
  = ()

let addm_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry {T.AddM? e})
  : Lemma (ensures (let open T in
                    let AddM s s' r = e in
                    let tsm_ = vaddm tsm s s' r in
                    not tsm_.failed ==> valid_log_entry e))
  = ()

#pop-options
  
let rec read_slots_valid_prop (tsm: thread_state_model) (slots: S.seq T.slot_id)
  : Lemma (ensures (let or = read_slots tsm slots in
                    Some? or ==> (forall i. valid_slot (S.index slots i))))
          (decreases (S.length slots))
  = let or = read_slots tsm slots in
    if Some? or && S.length slots > 0 then (
      let hd = S.head slots in
      let tl = S.tail slots in
      Classical.forall_intro (Seq.contains_cons hd tl);

      read_slots_valid_prop tsm tl;
      assert(valid_slot hd);
      let aux (i:_)
        : Lemma (ensures (valid_slot (S.index slots i)))
        = if i > 0 then
            assert(valid_slot (S.index tl (i-1)))
      in
      forall_intro aux
    )
/
Zeta.Steel.ThreadSim.fsti.checked Zeta.Steel.StoreRel.fsti.checked Zeta.Steel.MultiSetHash.fsti.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.IV.fst.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.AppSim.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Merkle.fsti.checked Zeta.Intermediate.Thread.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.GenKey.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Steel.ThreadRel.fst

    tsm: Zeta.Steel.ThreadStateModel.thread_state_model ->
    slots:
      FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.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.MultiSetHash.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
          Mkthread_state_model?.failed tsm_ == Mkthread_state_model?.failed tsm /\
          Mkthread_state_model?.clock tsm_ == Mkthread_state_model?.clock tsm /\
          Mkthread_state_model?.epoch_hashes tsm_ == Mkthread_state_model?.epoch_hashes tsm /\
          Mkthread_state_model?.thread_id tsm_ == Mkthread_state_model?.thread_id tsm /\
          Mkthread_state_model?.processed_entries tsm_ ==
          Mkthread_state_model?.processed_entries tsm /\
          Mkthread_state_model?.app_results tsm_ == Mkthread_state_model?.app_results tsm))
      (decreases FStar.Seq.Base.length slots)
Zeta.Steel.ThreadStateModel.thread_state_model FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.ThreadStateModel.valid_app_slots Zeta.App.app_value_nullable Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.MultiSetHash.app Prims.eq2 Prims.nat FStar.Seq.Base.length Prims.op_GreaterThan Zeta.Steel.ThreadRel.write_slots_non_store_prop FStar.Seq.Properties.tail Zeta.Steel.ThreadStateModel.update_value Zeta.Steel.LogEntry.Types.value Prims.b2t 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 Prims.unit FStar.Classical.forall_intro Prims.l_iff FStar.Seq.Properties.contains FStar.Seq.Base.cons Prims.l_or FStar.Seq.Properties.contains_cons Prims._assert FStar.Seq.Base.equal Prims.bool Prims.l_and 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.l_True Prims.squash Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Prims.Nil FStar.Pervasives.pattern
let rec write_slots_non_store_prop
      (tsm: thread_state_model)
      (slots: _{TSM.valid_app_slots tsm slots})
      (values: S.seq (app_value_nullable app.adm) {S.length slots == S.length values})
    : Lemma
      (ensures
        (let tsm_ = write_slots tsm slots values in
          tsm_.failed == tsm.failed /\ tsm_.clock == tsm.clock /\
          tsm_.epoch_hashes == tsm.epoch_hashes /\ tsm_.thread_id == tsm.thread_id /\
          tsm_.processed_entries == tsm.processed_entries /\ tsm_.app_results == tsm.app_results))
      (decreases (S.length slots)) =
  
let tsm_ = write_slots tsm slots values in
if S.length slots > 0
then
  (let hd_slot = S.head slots in
    let tl = S.tail slots in
    assert (slots `S.equal` (S.cons hd_slot tl));
    Classical.forall_intro (Seq.contains_cons hd_slot tl);
    let hd_value =
      match Seq.head values with
      | Null -> T.DValue None
      | DValue d -> T.DValue (Some d)
    in
    let tsm = update_value tsm hd_slot hd_value in
    write_slots_non_store_prop tsm (S.tail slots) (S.tail values))