val 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)]
val 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 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 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)
/
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
  -> FStar.Pervasives.Lemma (requires Zeta.Steel.AppSim.valid_app_slots tsm slots)
      (ensures
        (let st = Mkthread_state_model?.store tsm in
          forall (i: Prims.nat{i < FStar.Seq.Base.length slots}).
            let s = FStar.Seq.Base.index slots i in
            FStar.UInt16.v s < FStar.UInt16.v Zeta.Steel.ApplicationTypes.store_size /\
            Zeta.Steel.StoreRel.inuse_slot st s /\
            ApplicationKey? (Zeta.Steel.StoreRel.stored_key st s)))
      (decreases FStar.Seq.Base.length slots)
      [SMTPat (Zeta.Steel.AppSim.valid_app_slots tsm slots)]
Zeta.Steel.Rel.s_thread_state FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id Prims.op_Equality Prims.int Prims.bool FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.l_and FStar.UInt16.v FStar.Seq.Base.index Zeta.Steel.ApplicationTypes.store_size Zeta.Steel.StoreRel.inuse_slot Zeta.Steel.LogEntry.Types.uu___is_ApplicationKey Zeta.Steel.StoreRel.stored_key Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.op_GreaterThan Prims._assert Prims.op_Subtraction Zeta.Steel.AppSim.valid_app_slots_implies_app_recs Zeta.Steel.AppSim.valid_app_slots FStar.Seq.Properties.tail FStar.Seq.Properties.head Zeta.Steel.ThreadStateModel.contents Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Prims.l_Forall Prims.Cons FStar.Pervasives.smt_pat
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
  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