val 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))
val 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 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
    )
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
/
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
  -> FStar.Pervasives.Lemma
      (ensures
        (let or = Zeta.Steel.ThreadStateModel.read_slots tsm slots in
          Some? or ==>
          (forall (i: Prims.nat{i < FStar.Seq.Base.length slots}).
              Zeta.Steel.Rel.valid_slot (FStar.Seq.Base.index slots i))))
      (decreases FStar.Seq.Base.length slots)
Zeta.Steel.ThreadStateModel.thread_state_model FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.slot_id Prims.op_AmpAmp FStar.Pervasives.Native.uu___is_Some Zeta.App.app_record Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.ApplicationTypes.aprm Prims.l_and Prims.eq2 Prims.nat FStar.Seq.Base.length Zeta.Steel.ThreadStateModel.valid_app_slots Prims.op_GreaterThan FStar.Classical.forall_intro Prims.b2t Prims.op_LessThan Zeta.Steel.Rel.valid_slot FStar.Seq.Base.index Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert Prims.op_Subtraction Prims.bool Zeta.Steel.ThreadRel.read_slots_valid_prop Prims.l_iff FStar.Seq.Properties.contains FStar.Seq.Base.cons Prims.l_or FStar.Seq.Properties.contains_cons FStar.Seq.Properties.tail FStar.Seq.Properties.head FStar.Pervasives.Native.option Prims.l_Forall Zeta.Steel.ThreadStateModel.has_slot Zeta.Steel.LogEntry.Types.uu___is_ApplicationKey Zeta.Steel.ThreadStateModel.key_of_slot Zeta.Steel.ThreadStateModel.read_slots Prims.l_imp
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)