val to_i_tsm (tsm: valid_tsm{spec_rel_base tsm}) : GTot (i_thread_state)
val to_i_tsm (tsm: valid_tsm{spec_rel_base tsm}) : GTot (i_thread_state)
let to_i_tsm (tsm: valid_tsm {spec_rel_base tsm})
  : GTot (i_thread_state)
  = Zeta.Generic.Thread.state (to_i_tl tsm)
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

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

let verify_step_model_processed_entries_prop (tsm: thread_state_model) (e: s_log_entry)
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> tsm_.processed_entries == Seq.snoc tsm.processed_entries e))
          [SMTPat (verify_step_model tsm e)]
  = let open T in
    if not tsm.failed then
      match e with
      | AddM _ _ _ -> addm_processed_entries_props tsm e
      | RunApp _ -> runapp_non_store_prop tsm e
      | _ -> ()

let verify_step_model_thread_id_prop (tsm: thread_state_model) (e: s_log_entry)
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    tsm_.thread_id = tsm.thread_id))
          [SMTPat (verify_step_model tsm e)]
  = let open T in
    match e with
    | AddM _ _ _ -> addm_thread_id_prop tsm e
    | RunApp _ -> runapp_non_store_prop tsm e
    | _ -> ()

let verify_step_model_valid_log_entry_prop (tsm: thread_state_model) (e: s_log_entry)
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid_log_entry e))
          [SMTPat (verify_step_model tsm e)]
  = let open T in
    let tsm_ = verify_step_model tsm e in
    if not tsm_.failed then (
      match e with
      | AddM _ _ _ -> addm_valid_log_entry_prop tsm e
      | RunApp _ -> runapp_valid_log_entry_prop tsm e
      | _ -> ()
    )

let rec run_implies_processed_entries (tid: AT.tid) (l: s_log)
  : Lemma (ensures (let tsm = run tid l in
                    tsm.failed \/
                    tsm.processed_entries == l))
          (decreases (S.length l))
  = let tsm = run tid l in
    if S.length l = 0 then
      S.lemma_empty l
    else (
      let i = S.length l - 1 in
      let l' = SA.prefix l i in
      let e = S.index l i in
      run_implies_processed_entries tid l';
      let tsm' = run tid l' in

      if not tsm'.failed && not tsm.failed then (
        verify_step_model_processed_entries_prop tsm' e;
        SA.lemma_hprefix_append_telem l
      )
    )

let rec run_implies_thread_id (tid: AT.tid) (l: s_log)
  : Lemma (ensures (let tsm = run tid l in
                    tsm.thread_id = tid))
          (decreases (S.length l))
  = let tsm = run tid l in
    if S.length l > 0 then (
      let i = S.length l - 1 in
      let l' = SA.prefix l i in
      let e = S.index l i in
      run_implies_thread_id tid l';
      verify_step_model_thread_id_prop (run tid l') e;
      ()
    )

let run_implies_valid (tid: AT.tid) (l: s_log)
  : Lemma (ensures (let tsm = run tid l in
                    tsm.failed \/ valid tsm))
  = let tsm = run tid l in
    run_implies_processed_entries tid l;
    run_implies_thread_id tid l

let rec run_implies_valid_log (tid: AT.tid) (l: s_log)
  : Lemma (ensures (let tsm = run tid l in
                    not tsm.failed ==> valid_log l))
          (decreases (S.length l))
  = let tsm = run tid l in
    if S.length l > 0 then (
      let i = S.length l - 1 in
      let l' = SA.prefix l i in
      let e = S.index l i in
      let tsm' = run tid l' in
      run_implies_valid_log tid l';
      verify_step_model_valid_log_entry_prop (run tid l') e;
      if not tsm.failed then (
        assert(valid_log l');
        assert(valid_log_entry e);
        let aux (j:_)
          : Lemma (ensures (valid_log_entry (S.index l j)))
          = if j < i then
              eliminate forall i. valid_log_entry (S.index l' i) with j
        in
        forall_intro aux
      )
    )

let valid_implies_valid_log (tsm: valid_tsm)
  : Lemma (ensures (valid_log tsm.processed_entries))
  = run_implies_valid tsm.thread_id tsm.processed_entries;
    run_implies_valid_log tsm.thread_id tsm.processed_entries

let verify_step_model_extends_validity (tsm: valid_tsm) (e: s_log_entry)
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_))
          [SMTPat (verify_step_model tsm e)]
  = let l = tsm.processed_entries in
    let t = tsm.thread_id in
    let l_ = SA.append1 l e in
    let tsm_ = run t l_ in
    SA.lemma_prefix1_append l e;
    assert(l == SA.prefix l_ (S.length l));
    run_implies_valid t l_

let to_i_tl (tsm: valid_tsm {spec_rel_base tsm})
  : GTot (Zeta.Intermediate.Thread.verifiable_log i_vcfg)
  = let i_log = lift_log tsm.processed_entries in
    let i_tid = lift_tid tsm.thread_id in
    i_tid, i_log
/
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.ThreadRel.valid_tsm{Zeta.Steel.ThreadRel.spec_rel_base tsm}
  -> Prims.GTot Zeta.Steel.Rel.i_thread_state
Zeta.Steel.ThreadRel.valid_tsm Zeta.Steel.ThreadRel.spec_rel_base Zeta.Generic.Thread.state Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.Steel.ThreadRel.to_i_tl Zeta.Steel.Rel.i_thread_state
let to_i_tsm (tsm: valid_tsm{spec_rel_base tsm}) : GTot (i_thread_state) =
  
Zeta.Generic.Thread.state (to_i_tl tsm)