val write_slots_slot_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})
      (s: T.slot)
    : Lemma (requires (SA.distinct_elems slots))
      (ensures
        (let tsm_ = write_slots tsm slots values in
          let st = tsm.store in
          let st_ = tsm_.store in
          let open TSM in
          if Seq.mem s slots
          then
            inuse_slot st s /\ inuse_slot st_ s /\ stored_key st s == stored_key st_ s /\
            stored_value st_ s == to_s_value (Seq.index values (Seq.index_mem s slots)) /\
            add_method_of st s == add_method_of st_ s /\
            points_to_info st s true == points_to_info st_ s true /\
            points_to_info st s false == points_to_info st_ s false /\
            parent_info st s == parent_info st_ s
          else get_slot st s == get_slot st_ s))
      (decreases (Seq.length slots))
val write_slots_slot_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})
      (s: T.slot)
    : Lemma (requires (SA.distinct_elems slots))
      (ensures
        (let tsm_ = write_slots tsm slots values in
          let st = tsm.store in
          let st_ = tsm_.store in
          let open TSM in
          if Seq.mem s slots
          then
            inuse_slot st s /\ inuse_slot st_ s /\ stored_key st s == stored_key st_ s /\
            stored_value st_ s == to_s_value (Seq.index values (Seq.index_mem s slots)) /\
            add_method_of st s == add_method_of st_ s /\
            points_to_info st s true == points_to_info st_ s true /\
            points_to_info st s false == points_to_info st_ s false /\
            parent_info st s == parent_info st_ s
          else get_slot st s == get_slot st_ s))
      (decreases (Seq.length slots))
let rec write_slots_slot_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})
                         (s: T.slot)
  : Lemma (requires (SA.distinct_elems slots))
          (ensures (let tsm_ = write_slots tsm slots values in
                    let st = tsm.store in
                    let st_ = tsm_.store in
                    let open TSM in
                    if Seq.mem s slots then
                      inuse_slot st s /\
                      inuse_slot st_ s /\
                      stored_key st s == stored_key st_ s /\
                      stored_value st_ s == to_s_value (Seq.index values (Seq.index_mem s slots)) /\
                      add_method_of st s == add_method_of st_ s /\
                      points_to_info st s true == points_to_info st_ s true /\
                      points_to_info st s false == points_to_info st_ s false /\
                      parent_info st s == parent_info st_ s
                    else get_slot st s == get_slot st_ s))
          (decreases (Seq.length slots))
  = let n = Seq.length slots in
    let st = tsm.store in
    let tsm_ = write_slots tsm slots values in
    let st_ = tsm_.store 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
      assert (hd_value == to_s_value (Seq.head values));
      let tsm2 = update_value tsm hd_slot hd_value in
      lemma_update_value tsm hd_slot hd_value;
      write_slots_slot_prop tsm2 tl (Seq.tail values) s;
      if Seq.mem s slots then
      begin
        let i = Seq.index_mem s slots in
        if i = 0 then
        begin
          let st2 = tsm2.store in
          assert (hd_slot = s);
          assert (inuse_slot st2 s);
          assert (stored_key st2 s == stored_key st s);
          lemma_mem_head slots s;
          assert (stored_key st s == stored_key st_ s);
          assert (stored_value st_ s == to_s_value (Seq.index values i));
          ()
        end
        else
        begin
          assert (hd_slot <> s);
          let st2 = tsm2.store in
          assert (get_slot st2 s == get_slot st s);
          assert (Seq.mem s tl);
          ()
        end
      end
      else
      begin
        assert (s <> hd_slot);
        assert (not (Seq.mem s tl));
        ()
      end
    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

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

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

(* convert an nullable app value to its steel representation *)
let to_s_value (av: A.app_value_nullable app.A.adm)
  = match av with
    | A.Null -> T.DValue None
    | A.DValue d -> T.DValue (Some d)

let lemma_mem_head (slots: Seq.seq s_slot_id) (s: s_slot_id)
  : Lemma (requires (SA.distinct_elems slots /\ Seq.mem s slots /\ Seq.index_mem s slots = 0))
          (ensures (not (Seq.mem s (Seq.tail slots))))
  = let open FStar.Seq in
    let open SA in
    let tl = tail slots in
    if mem s tl then
    begin
      let i = index_mem s tl in
      assert (index tl i = s);
      assert (index slots (i+1) = s);
      lemma_elem_idx_uniq slots (i+1);
      assert (index_mem s slots = i+1); // contradiction
      ()
    end
/
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} ->
    s: Zeta.Steel.FormatsManual.slot
  -> FStar.Pervasives.Lemma (requires Zeta.SeqAux.distinct_elems slots)
      (ensures
        (let tsm_ = Zeta.Steel.ThreadStateModel.write_slots tsm slots values in
          let st = Mkthread_state_model?.store tsm in
          let st_ = Mkthread_state_model?.store tsm_ in
          (match FStar.Seq.Properties.mem s slots with
            | true ->
              Zeta.Steel.StoreRel.inuse_slot st s /\ Zeta.Steel.StoreRel.inuse_slot st_ s /\
              Zeta.Steel.StoreRel.stored_key st s == Zeta.Steel.StoreRel.stored_key st_ s /\
              Zeta.Steel.StoreRel.stored_value st_ s ==
              Zeta.Steel.AppSim.to_s_value (FStar.Seq.Base.index values
                    (FStar.Seq.Properties.index_mem s slots)) /\
              Zeta.Steel.StoreRel.add_method_of st s == Zeta.Steel.StoreRel.add_method_of st_ s /\
              Zeta.Steel.StoreRel.points_to_info st s true ==
              Zeta.Steel.StoreRel.points_to_info st_ s true /\
              Zeta.Steel.StoreRel.points_to_info st s false ==
              Zeta.Steel.StoreRel.points_to_info st_ s false /\
              Zeta.Steel.StoreRel.parent_info st s == Zeta.Steel.StoreRel.parent_info st_ s
            | _ -> Zeta.Steel.StoreRel.get_slot st s == Zeta.Steel.StoreRel.get_slot st_ s)
          <:
          Type0))
      (decreases FStar.Seq.Base.length slots)
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 Zeta.Steel.FormatsManual.slot Prims.op_GreaterThan FStar.Seq.Properties.mem Prims.int Prims.unit Prims._assert Prims.eq2 Zeta.Steel.LogEntry.Types.value Zeta.Steel.StoreRel.stored_value Zeta.Steel.AppSim.to_s_value FStar.Seq.Base.index Zeta.Steel.LogEntry.Types.key Zeta.Steel.StoreRel.stored_key Zeta.Steel.AppSim.lemma_mem_head Zeta.Steel.StoreRel.inuse_slot Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.ThreadStateModel.contents Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Prims.bool FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.store_entry Zeta.Steel.StoreRel.get_slot Prims.op_disEquality FStar.Seq.Properties.index_mem Prims.op_Negation Zeta.Steel.AppSim.write_slots_slot_prop FStar.Seq.Properties.tail Zeta.Steel.StoreRel.lemma_update_value Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.update_value FStar.Seq.Properties.head Prims.l_and Zeta.Steel.LogEntry.Types.is_value_of Zeta.Steel.ThreadStateModel.key_of_slot 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 FStar.Seq.Properties.contains_cons FStar.Seq.Base.equal Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id 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 Zeta.SeqAux.distinct_elems Prims.squash Zeta.Steel.ThreadStateModel.add_method Zeta.Steel.StoreRel.add_method_of Zeta.Steel.StoreRel.points_to_info FStar.Pervasives.Native.tuple2 Zeta.Steel.StoreRel.parent_info Prims.Nil FStar.Pervasives.pattern
let rec write_slots_slot_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})
      (s: T.slot)
    : Lemma (requires (SA.distinct_elems slots))
      (ensures
        (let tsm_ = write_slots tsm slots values in
          let st = tsm.store in
          let st_ = tsm_.store in
          let open TSM in
          if Seq.mem s slots
          then
            inuse_slot st s /\ inuse_slot st_ s /\ stored_key st s == stored_key st_ s /\
            stored_value st_ s == to_s_value (Seq.index values (Seq.index_mem s slots)) /\
            add_method_of st s == add_method_of st_ s /\
            points_to_info st s true == points_to_info st_ s true /\
            points_to_info st s false == points_to_info st_ s false /\
            parent_info st s == parent_info st_ s
          else get_slot st s == get_slot st_ s))
      (decreases (Seq.length slots)) =
  
let n = Seq.length slots in
let st = tsm.store in
let tsm_ = write_slots tsm slots values in
let st_ = tsm_.store 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
  assert (hd_value == to_s_value (Seq.head values));
  let tsm2 = update_value tsm hd_slot hd_value in
  lemma_update_value tsm hd_slot hd_value;
  write_slots_slot_prop tsm2 tl (Seq.tail values) s;
  if Seq.mem s slots
  then
    let i = Seq.index_mem s slots in
    if i = 0
    then
      let st2 = tsm2.store in
      assert (hd_slot = s);
      assert (inuse_slot st2 s);
      assert (stored_key st2 s == stored_key st s);
      lemma_mem_head slots s;
      assert (stored_key st s == stored_key st_ s);
      assert (stored_value st_ s == to_s_value (Seq.index values i));
      ()
    else
      (assert (hd_slot <> s);
        let st2 = tsm2.store in
        assert (get_slot st2 s == get_slot st s);
        assert (Seq.mem s tl);
        ())
  else
    (assert (s <> hd_slot);
      assert (not (Seq.mem s tl));
      ())