val blum_add_slot : e: Zeta.Steel.LogEntry.Types.log_entry{Zeta.Steel.ThreadRel.is_blum_add e}
  -> Zeta.Steel.LogEntry.Types.slot_id
let blum_add_slot (e:_ {is_blum_add e})
  = let open T in
    match e with
    | AddB s _ _ _ -> s
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

let to_i_tsm (tsm: valid_tsm {spec_rel_base tsm})
  : GTot (i_thread_state)
  = Zeta.Generic.Thread.state (to_i_tl tsm)

let verify_step_model_lifted_log_prop (tsm:_ {spec_rel_base tsm}) (e: s_log_entry)
  : Lemma (requires (let tsm_ = verify_step_model tsm e in
                     not tsm_.failed))
          (ensures (let tsm_ = verify_step_model tsm e in
                    let i_log = lift_log tsm.processed_entries in
                    let i_e = lift_log_entry e in
                    let i_log_ = lift_log tsm_.processed_entries in
                    let i = Seq.length i_log in
                    i_log_ == Seq.snoc i_log i_e /\
                    Seq.index i_log_ i = i_e /\
                    i_log = SA.prefix i_log_ i))
          [SMTPat (verify_step_model tsm e)]
  = let i_log = lift_log tsm.processed_entries in
    let i_e = lift_log_entry e in
    lift_log_snoc tsm.processed_entries e;
    SA.lemma_prefix1_append i_log i_e

let spec_rel_base_addm (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.AddM? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      addm_simulation tsm i_tsm e i_e
    )

let spec_rel_base_addb (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.AddB? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      addb_simulation tsm i_tsm e i_e
    )

let spec_rel_base_evictm (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.EvictM? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      evictm_simulation tsm i_tsm e i_e
    )

let spec_rel_base_evictb (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.EvictB? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      evictb_simulation tsm i_tsm e i_e
    )

let spec_rel_base_evictbm (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.EvictBM? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      evictbm_simulation tsm i_tsm e i_e
    )

let spec_rel_base_nextepoch (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.NextEpoch? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      nextepoch_simulation tsm i_tsm e i_e
    )

let spec_rel_base_verifyepoch (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.VerifyEpoch? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      verifyepoch_simulation tsm i_tsm e i_e
    )

let spec_rel_base_runapp (tsm:_ {spec_rel_base tsm}) (e: s_log_entry {T.RunApp? e})
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
  = let open T in
    let tid = tsm.TSM.thread_id in
    let i_tid = lift_tid tid in
    let tsm_ = verify_step_model tsm e in

    let i_log = lift_log tsm.processed_entries in
    let i_tsm = to_i_tsm tsm in

    if not tsm_.failed then (
      (* verify_step extends validity or fails *)
      assert(valid tsm_);

      let i_e = lift_log_entry e in
      assert (related_log_entry e i_e);

      let i_tsm_ = GV.verify_step i_e i_tsm in
      let i_log_ = lift_log tsm_.processed_entries in
      runapp_simulation tsm i_tsm e i_e
    )

let lemma_verify_step_model_spec_rel_base (tsm:_ {spec_rel_base tsm}) (e: s_log_entry)
  : Lemma (ensures (let tsm_ = verify_step_model tsm e in
                    not tsm_.failed ==> valid tsm_ /\ spec_rel_base tsm_))
          [SMTPat (verify_step_model tsm e)]
  = let open T in
    match e with
    | AddM _ _ _ -> spec_rel_base_addm tsm e
    | AddB _ _ _ _ -> spec_rel_base_addb tsm e
    | EvictM _ -> spec_rel_base_evictm tsm e
    | EvictB _ -> spec_rel_base_evictb tsm e
    | EvictBM _ -> spec_rel_base_evictbm tsm e
    | NextEpoch -> spec_rel_base_nextepoch tsm e
    | VerifyEpoch -> spec_rel_base_verifyepoch tsm e
    | RunApp _ -> spec_rel_base_runapp tsm e

let init_tsm_valid (tid: AT.tid)
  : Lemma (ensures (valid (init_thread_state_model tid)))
          [SMTPat (init_thread_state_model tid)]
  = ()

let empty_store_related ()
  : Lemma (ensures (let st = Seq.create (U16.v AT.store_size) None in
                    let i_st = IS.empty_store i_vcfg in
                    related_store st i_st))
  = let st: contents = Seq.create (U16.v AT.store_size) None in
    let i_st = IS.empty_store i_vcfg in

    let aux (i:_)
      : Lemma (ensures (related_store_entry_opt (Seq.index st i) (Seq.index i_st i)))
      = ()
    in
    forall_intro aux

let related_madd_to_store_root (tsm: thread_state_model)
                               (i_st: i_store)
                               (s: T.slot) (i_s: i_slot_id)
                               (v: T.value) (i_v: i_val {Zeta.Record.IntV? i_v})
  : Lemma (requires (related_store tsm.store i_st /\ related_slot s i_s /\
                     IS.empty_slot i_st i_s /\
                     related_val v i_v))
          (ensures (let tsm_ = TSM.madd_to_store_root tsm s v in
                    let st_ = tsm_.store in
                    let i_st_ = IS.madd_to_store_root i_st i_s i_v in
                    related_store st_ i_st_))
  = let st = tsm.store in

    eliminate forall i. related_store_entry_opt (Seq.index st i) (Seq.index i_st i)
    with i_s;

    assert (not (has_slot tsm s));
    assert (LT.is_value_of T.root_key v);

    let new_entry = {
      key = T.root_key;
      value = v;
      add_method = MAdd;
      l_child_in_store = None;
      r_child_in_store = None;
      parent_slot = None;
    } in

    let st_ = Seq.upd tsm.store (U16.v s) (Some new_entry) in
    let tsm_ = madd_to_store_root tsm s v in
    assert (tsm_.store == st_);

    let i_st_ = IS.madd_to_store_root i_st i_s i_v in

    let aux (i:_)
      : Lemma (ensures (related_store_entry_opt (Seq.index st_ i) (Seq.index i_st_ i)))
      = related_root_inv ();
        if i <> i_s then
        begin
          assert (Seq.index st_ i == Seq.index st i);
          assert (IS.identical_except i_st i_st_ i_s);

          eliminate forall s'. s' <> i_s ==> IS.get_slot i_st s' = IS.get_slot i_st_ s'
          with i
        end
    in
    forall_intro aux;
    ()

let init_store_related (tid: AT.tid) (i_tid: i_tid)
  : Lemma (requires (related_tid tid i_tid))
          (ensures (let tsm = init_thread_state_model tid in
                    let i_tsm = IV.init_thread_state i_vcfg i_tid in
                    related_store tsm.store i_tsm.IV.st))
  = let tsm = init_thread_state_model tid in
    let st = tsm.store in
    let i_st = IV.init_store i_vcfg i_tid in

    let empty_st: TSM.contents = Seq.create (U16.v AT.store_size) None in
    let i_empty_st = IS.empty_store i_vcfg in

    empty_store_related ();
    assert (related_store empty_st i_empty_st);

    if i_tid = 0 then
    begin

      (* state of initial tsm before the madd *)
      let _tsm = {
        thread_id = tid;
        failed = false;
        store = Seq.create (U16.v AT.store_size) None;
        clock = TSM.zero_clock;
        last_evict_key = root_base_key;
        epoch_hashes = initial_epoch_hashes;
        processed_entries = Seq.empty;
        app_results = Seq.empty;
        last_verified_epoch = None
      } in

      let s = U16.zero in
      let i_s = 0 in
      assert (related_slot s i_s);

      let rk = T.root_key in
      let v = init_value rk in

      let i_rk: GK.key app = GK.IntK Zeta.BinTree.Root in
      let i_v = R.init_value i_rk in

      assert (related_val v i_v);

      assert (tsm == madd_to_store_root _tsm U16.zero (init_value T.root_key));
      related_madd_to_store_root _tsm i_empty_st s i_s v i_v;

      ()
    end
    else
    begin
      assert (i_st == i_empty_st);
      assert (st == empty_st);
      ()
    end

let init_state_related (tid: AT.tid) (i_tid: i_tid)
  : Lemma (requires (related_tid tid i_tid))
          (ensures (let tsm = init_thread_state_model tid in
                    let i_tsm = IV.init_thread_state i_vcfg i_tid in
                    related_tsm tsm i_tsm))
  = let tsm = init_thread_state_model tid in
    let i_tsm = IV.init_thread_state i_vcfg i_tid in

    // both models are in not failed state
    assert (not tsm.failed /\ i_tsm.IV.valid);

    // thread ids are equal by construction
    assert (related_tid tsm.thread_id i_tsm.IV.tid);
    related_timestamp_zero ();
    assert (related_timestamp tsm.clock i_tsm.IV.clock);
    Zeta.Steel.KeyUtils.related_root();

    init_store_related tid i_tid

let init_tsm_spec_rel_base (tid: AT.tid)
  : Lemma (ensures (spec_rel_base (init_thread_state_model tid)))
  = let tsm = init_thread_state_model tid in
    let i_tid = lift_tid tsm.thread_id in
    init_state_related tid i_tid;
    ()

let length tsm = Seq.length tsm.processed_entries

let prev (tsm: valid_tsm {length tsm > 0})
  : thread_state_model
  = let i = length tsm - 1 in
    run tsm.thread_id (SA.prefix tsm.processed_entries i)

let last_entry (tsm: valid_tsm {length tsm > 0})
  : GTot (e:_ { valid_log_entry e })
  = let i = length tsm - 1 in
    Seq.index tsm.processed_entries i

(* the prev of a valid tsm is also valid *)
let valid_prev (tsm: valid_tsm {length tsm > 0} )
  : Lemma (ensures (valid (prev tsm)))
          [SMTPat (prev tsm)]
  = let _tsm = prev tsm in
    let e = last_entry tsm in

    let l = tsm.processed_entries in
    let i = length tsm - 1 in
    let _l = SA.prefix l i in

    // from definition of valid_tsm and run
    assert (tsm == run tsm.thread_id tsm.processed_entries);
    assert (tsm == verify_step_model _tsm e);

    // from last assert, _tsm cannot be in failed state
    assert (not _tsm.failed);

    // definition of prev
    assert (_tsm == run tsm.thread_id _l);

    run_implies_processed_entries tsm.thread_id _l;
    assert (_tsm.processed_entries == _l);

    ()

let lemma_prev_log_prefix (tsm: valid_tsm {length tsm > 0 })
  : Lemma (ensures (let _tsm = prev tsm in
                    let l = tsm.processed_entries in
                    let i = length tsm - 1 in
                    _tsm.processed_entries == SA.prefix l i))
          [SMTPat (prev tsm)]
  = let _tsm = prev tsm in
    let e = last_entry tsm in

    let l = tsm.processed_entries in
    let i = Seq.length l - 1 in
    let _l = SA.prefix l i in

    // from definition of valid_tsm and run
    assert (tsm == run tsm.thread_id tsm.processed_entries);
    assert (tsm == verify_step_model _tsm e);

    // from last assert, _tsm cannot be in failed state
    assert (not _tsm.failed);

    // definition of prev
    assert (_tsm == run tsm.thread_id _l);

    run_implies_processed_entries tsm.thread_id _l;
    assert (_tsm.processed_entries == _l);

    ()

let spec_rel_base_snoc (tsm: valid_tsm {length tsm > 0})
  : Lemma (requires (let _tsm = prev tsm in
                     spec_rel_base _tsm))
          (ensures (spec_rel_base tsm))
  = let _tsm = prev tsm in
    let e = last_entry tsm in
    assert (tsm == verify_step_model _tsm e);
    lemma_verify_step_model_spec_rel_base _tsm e

let rec valid_implies_spec_rel_base (tsm: valid_tsm)
  : Lemma (ensures (spec_rel_base tsm))
          (decreases (length tsm))
          [SMTPat (valid tsm)]
  = let tid = tsm.thread_id in
    let i_tid = lift_tid tid in
    if length tsm = 0 then
      init_tsm_spec_rel_base tid
    else
    begin
      let _tsm = prev tsm in
      valid_implies_spec_rel_base _tsm;
      spec_rel_base_snoc tsm
    end

module GT = Zeta.Generic.Thread

let init_add_set_empty (tsm: valid_tsm {length tsm = 0}) (ep: epoch_id)
  : Lemma (ensures (add_set tsm (lift_epoch ep) == Zeta.MultiSet.empty))
  = let i_ep = lift_epoch ep in
    let tid = tsm.thread_id in
    let l = tsm.processed_entries in

    assert (tsm == init_thread_state_model tid);

    let i_tl = to_ilog tsm in
    assert (GT.length i_tl = 0);

    let add_seq = GT.add_seq i_ep i_tl in

    GT.add_seq_empty i_ep i_tl;
    assert (Seq.length add_seq = 0);

    let open Zeta.MultiSetHashDomain in
    Zeta.MultiSet.zero_length_implies_empty #_ #(ms_hashfn_dom_cmp app) add_seq

let init_hadd_correct (tsm: valid_tsm {length tsm = 0}) (ep: epoch_id)
  : Lemma (ensures (let i_ep = lift_epoch ep in
                    let eh = Map.sel tsm.epoch_hashes ep in
                    eh.hadd == ms_hashfn (add_set tsm i_ep)))
  = let i_ep = lift_epoch ep in
    init_add_set_empty tsm ep;
    lemma_hashfn_empty ();
    assert (ms_hashfn (add_set tsm i_ep) == HA.initial_hash);
    assert (tsm.epoch_hashes == initial_epoch_hashes);
    ()

let is_blum_add e =
  let open T in
  match e with
  | AddB _ _ _ _ -> true
  | _ -> false

let blum_add_timestamp (e:_ {is_blum_add e})
  = let open T in
    match e with
    | AddB _  t _ _ -> t

let blum_add_tid (e: _ {is_blum_add e})
  = let open T in
    match e with
    | AddB _ _ tid _ -> tid

let blum_add_record (e:_ {is_blum_add e})
  = let open T in
    match e with
    | AddB _ _ _ r -> r
/
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
e: Zeta.Steel.LogEntry.Types.log_entry{Zeta.Steel.ThreadRel.is_blum_add e}
  -> Zeta.Steel.LogEntry.Types.slot_id
Zeta.Steel.LogEntry.Types.log_entry Prims.b2t Zeta.Steel.ThreadRel.is_blum_add Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.LogEntry.Types.thread_id Zeta.Steel.LogEntry.Types.record
let blum_add_slot (e: _{is_blum_add e}) =
  
let open T in match e with | AddB s _ _ _ -> s