val 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))
val 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 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)
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"
/
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 ->
    i: Zeta.SeqAux.seq_index slots
  -> FStar.Pervasives.Lemma
      (requires
        Prims.op_Negation (Mkthread_state_model?.failed tsm) /\
        Zeta.Steel.AppSim.valid_app_slots tsm slots)
      (ensures
        (let s = FStar.Seq.Base.index slots i in
          let _ = Zeta.Steel.ThreadStateModel.read_slots tsm slots in
          (let FStar.Pervasives.Native.Some #_ recs = _ in
            let keys = Zeta.SeqAux.map FStar.Pervasives.Native.fst recs in
            let _ = FStar.Seq.Base.index recs i in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ ak1 _ = _ in
              let st = Mkthread_state_model?.store tsm in
              let _ = Zeta.Steel.StoreRel.stored_key st s in
              (let Zeta.Steel.LogEntry.Types.ApplicationKey ak2 = _ in
                ak1 = ak2 /\ ak1 = FStar.Seq.Base.index keys i)
              <:
              Type0)
            <:
            Type0)
          <:
          Type0))
      (decreases FStar.Seq.Base.length slots)
Zeta.Steel.Rel.s_thread_state FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id Zeta.SeqAux.seq_index Prims.op_AmpAmp Prims.op_GreaterThan Zeta.Steel.AppSim.read_slots_key_idx FStar.Seq.Properties.tail Prims.op_Subtraction Prims.bool Prims.unit Prims.nat FStar.Seq.Base.length Prims.l_and Prims.b2t Prims.op_Negation Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.AppSim.valid_app_slots Prims.squash Zeta.App.app_record Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.ApplicationTypes.aprm Prims.eq2 Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.ThreadStateModel.valid_app_slots Zeta.App.app_key Zeta.App.app_value_nullable Zeta.Steel.ApplicationTypes.key_type Prims.op_Equality FStar.Seq.Base.index Zeta.Steel.LogEntry.Types.key Zeta.Steel.StoreRel.stored_key Zeta.Steel.ThreadStateModel.contents Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.SeqAux.map FStar.Pervasives.Native.fst FStar.Pervasives.Native.option Prims.l_Forall Prims.op_LessThan Zeta.Steel.ThreadStateModel.has_slot Zeta.Steel.LogEntry.Types.uu___is_ApplicationKey Zeta.Steel.ThreadStateModel.key_of_slot Zeta.Steel.ThreadStateModel.read_slots Prims.Nil FStar.Pervasives.pattern
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)