val runapp_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry{T.RunApp? e})
    : Lemma
    (ensures
      (let open T in
        let RunApp p = e in
        let tsm_ = runapp tsm p in
        not tsm_.failed ==> valid_log_entry e))
val runapp_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry{T.RunApp? e})
    : Lemma
    (ensures
      (let open T in
        let RunApp p = e in
        let tsm_ = runapp tsm p in
        not tsm_.failed ==> valid_log_entry e))
let runapp_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry {T.RunApp? e})
  : Lemma (ensures (let open T in
                    let RunApp p = e in
                    let tsm_ = runapp tsm p in
                    not tsm_.failed ==> valid_log_entry e))
  = let open T in
    let RunApp p = e in
    let tsm_ = runapp tsm p in
    runapp_checks_unsat_prop tsm p;
    if runapp_checks_sat tsm p && not tsm_.failed then
      match AT.spec_app_parser p.fid p.rest.ebytes with
      | Some ((arg, slots), len) ->
        read_slots_valid_prop tsm slots
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
    )

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)
    )

(* do all the runapp_checks satisfy *)
let runapp_checks_sat (tsm: thread_state_model) (pl: T.runApp_payload)
  : GTot bool
  = let open T in
    if not (Map.contains app.tbl pl.fid)
    then false //unknown fid
    else (
      match AT.spec_app_parser pl.fid pl.rest.ebytes with
      | None -> false //parsing failed
      | Some ((arg, slots), len) ->
        if len <> U32.v pl.rest.len
        then false //parsing failed, some bytes not consumed
        else if not (Zeta.SeqAux.distinct_elems_comp slots)
        then false //not distinct slots
        else
          let fsig = Map.sel app.tbl pl.fid in
          match read_slots tsm slots with
          | None -> false
          | Some recs ->
            if not (check_distinct_keys recs)
            then false
            else (
              let res = fsig.f arg recs in
              match res with
              | ( Fn_failure, _, _) -> false
              | (_, res, out_vals) -> true
            )
        )

let runapp_checks_unsat_prop (tsm: thread_state_model) (pl: T.runApp_payload)
  : Lemma (ensures (not (runapp_checks_sat tsm pl) ==> fail tsm == runapp tsm pl))
  = ()

let runapp_non_store_prop (tsm: thread_state_model) (e: s_log_entry {T.RunApp? e})
  : Lemma (ensures (let open T in
                    let RunApp p = e in
                    let tsm_ = runapp tsm p in
                    tsm_.processed_entries == tsm.processed_entries /\
                    tsm_.thread_id = tsm.thread_id))
  = let open T in
    let RunApp p = e in
    let tsm_ = runapp tsm p in
    runapp_checks_unsat_prop tsm p;
    if runapp_checks_sat tsm p then
      match AT.spec_app_parser p.fid p.rest.ebytes with
      | Some ((arg, slots), len) ->
        let fsig = Map.sel app.tbl p.fid in
        match read_slots tsm slots with
        | Some recs ->
          let res = fsig.f arg recs in
          match res with
          | _, res, out_vals ->
            write_slots_non_store_prop tsm slots out_vals
/
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 -> e: Zeta.Steel.Rel.s_log_entry{RunApp? e}
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = e in
        (let Zeta.Steel.LogEntry.Types.RunApp p = _ in
          let tsm_ = Zeta.Steel.ThreadStateModel.runapp tsm p in
          Prims.op_Negation (Mkthread_state_model?.failed tsm_) ==>
          Zeta.Steel.LogRel.valid_log_entry e)
        <:
        Type0))
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.Rel.s_log_entry Prims.b2t Zeta.Steel.LogEntry.Types.uu___is_RunApp Zeta.Steel.LogEntry.Types.runApp_payload Prims.op_AmpAmp Zeta.Steel.ThreadRel.runapp_checks_sat Prims.op_Negation Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.ApplicationTypes.spec_app_parser Zeta.Steel.LogEntry.Types.__proj__MkrunApp_payload__item__fid FStar.Ghost.reveal FStar.Seq.Base.seq FStar.UInt8.t Zeta.Steel.LogEntry.Types.__proj__Mkuninterpreted__item__ebytes Zeta.Steel.LogEntry.Types.__proj__MkrunApp_payload__item__rest Zeta.Steel.ApplicationTypes.app_args Zeta.Steel.ApplicationTypes.slots Prims.nat Zeta.Steel.ThreadRel.read_slots_valid_prop Prims.unit Prims.bool Zeta.Steel.ThreadRel.runapp_checks_unsat_prop Prims.l_and Prims.eq2 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 Prims.l_imp Zeta.Steel.ThreadStateModel.app_results Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__app_results Prims.op_GreaterThan FStar.Seq.Base.length Zeta.Steel.ApplicationTypes.app_result_entry FStar.Seq.Base.equal FStar.Pervasives.Native.fst FStar.Seq.Properties.un_snoc Zeta.Steel.ThreadStateModel.runapp Prims.l_True Prims.squash Zeta.Steel.LogRel.valid_log_entry Prims.Nil FStar.Pervasives.pattern
let runapp_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry{T.RunApp? e})
    : Lemma
    (ensures
      (let open T in
        let RunApp p = e in
        let tsm_ = runapp tsm p in
        not tsm_.failed ==> valid_log_entry e)) =
  
let open T in
let RunApp p = e in
let tsm_ = runapp tsm p in
runapp_checks_unsat_prop tsm p;
if runapp_checks_sat tsm p && not tsm_.failed
then
  match AT.spec_app_parser p.fid p.rest.ebytes with
  | Some ((arg, slots), len) -> read_slots_valid_prop tsm slots