val 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_))
val 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 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;
    ()
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
/
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 ->
    i_st: Zeta.Steel.Rel.i_store ->
    s: Zeta.Steel.FormatsManual.slot ->
    i_s: Zeta.Steel.Rel.i_slot_id ->
    v: Zeta.Steel.LogEntry.Types.value ->
    i_v: Zeta.Steel.Rel.i_val{IntV? i_v}
  -> FStar.Pervasives.Lemma
      (requires
        Zeta.Steel.StoreRel.related_store (Mkthread_state_model?.store tsm) i_st /\
        Zeta.Steel.Rel.related_slot s i_s /\ Zeta.Intermediate.Store.empty_slot i_st i_s /\
        Zeta.Steel.Rel.related_val v i_v)
      (ensures
        (let tsm_ = Zeta.Steel.ThreadStateModel.madd_to_store_root tsm s v in
          let st_ = Mkthread_state_model?.store tsm_ in
          let i_st_ = Zeta.Intermediate.Store.madd_to_store_root i_st i_s i_v in
          Zeta.Steel.StoreRel.related_store st_ i_st_))
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.Rel.i_store Zeta.Steel.FormatsManual.slot Zeta.Steel.Rel.i_slot_id Zeta.Steel.LogEntry.Types.value Zeta.Steel.Rel.i_val Prims.b2t Zeta.Record.uu___is_IntV Zeta.Steel.Rel.app Prims.unit FStar.Classical.forall_intro Prims.nat Prims.l_and Prims.op_LessThan FStar.Seq.Base.length FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.store_entry Zeta.Intermediate.Store.vstore_entry Zeta.Steel.Rel.i_vcfg Zeta.Steel.StoreRel.related_store_entry_opt FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.op_disEquality Prims.l_or Zeta.Intermediate.VerifierConfig.store_size FStar.Classical.Sugar.forall_elim Zeta.Intermediate.VerifierConfig.slot_id Prims.l_imp Prims.op_Equality Zeta.Intermediate.Store.get_slot Prims._assert Zeta.Intermediate.Store.identical_except Prims.eq2 Prims.bool Zeta.Steel.Rel.related_root_inv Zeta.Intermediate.Store.vstore Zeta.Intermediate.Store.inuse_slot Zeta.Intermediate.Store.get_inuse_slot Zeta.Intermediate.Store.VStoreE FStar.Pervasives.Native.Mktuple2 Zeta.GenKey.key Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Record.value Zeta.GenKey.IntK Zeta.BinTree.Root Zeta.High.Verifier.MAdd FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 Zeta.BinTree.bin_tree_dir Zeta.Intermediate.Store.madd_to_store_root FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.Steel.ThreadStateModel.madd_to_store_root FStar.Seq.Base.upd FStar.UInt16.v FStar.Pervasives.Native.Some Zeta.Steel.ThreadStateModel.Mkstore_entry Zeta.Steel.LogEntry.Types.root_key Zeta.Steel.ThreadStateModel.MAdd Zeta.Steel.LogEntry.Types.is_value_of Prims.op_Negation Zeta.Steel.ThreadStateModel.has_slot Zeta.Steel.ThreadStateModel.contents Zeta.Steel.StoreRel.related_store Zeta.Steel.Rel.related_slot Zeta.Intermediate.Store.empty_slot Zeta.Steel.Rel.related_val
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
    (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)
in
forall_intro aux;
()