val addm_simulation (tsm: s_thread_state) (i_tsm: i_thread_state) (se: s_log_entry) (ie: i_log_entry)
  : Lemma (requires (related_tsm tsm i_tsm /\
                     related_log_entry se ie /\
                     LT.AddM? se /\ not tsm.failed))
          (ensures (let LT.AddM s s' r = se in
                    let GV.AddM ir is is' = ie in
                    let tsm_ = vaddm tsm s s' r in
                    let i_tsm_ = IV.addm ir is is' i_tsm in
                    (not tsm_.failed) ==> related_tsm tsm_ i_tsm_))
val addm_simulation (tsm: s_thread_state) (i_tsm: i_thread_state) (se: s_log_entry) (ie: i_log_entry)
  : Lemma (requires (related_tsm tsm i_tsm /\
                     related_log_entry se ie /\
                     LT.AddM? se /\ not tsm.failed))
          (ensures (let LT.AddM s s' r = se in
                    let GV.AddM ir is is' = ie in
                    let tsm_ = vaddm tsm s s' r in
                    let i_tsm_ = IV.addm ir is is' i_tsm in
                    (not tsm_.failed) ==> related_tsm tsm_ i_tsm_))
let addm_simulation (tsm: s_thread_state) (i_tsm: i_thread_state) (se: s_log_entry) (ie: i_log_entry)
  : Lemma (requires (related_tsm tsm i_tsm /\
                     related_log_entry se ie /\
                     LT.AddM? se /\ not tsm.failed))
          (ensures (let LT.AddM s s' r = se in
                    let GV.AddM ir is is' = ie in
                    let tsm_ = vaddm tsm s s' r in
                    let i_tsm_ = IV.addm ir is is' i_tsm in
                    (not tsm_.failed) ==> related_tsm tsm_ i_tsm_))
  = let LT.AddM s s' r = se in
    let GV.AddM ir is is' = ie in
    let a = AMP s r s' tsm in
    let i_a = IV.AMP is ir is' i_tsm in

    lemma_related_implies_all_props tsm.store i_tsm.IV.st;
    addm_prop tsm s s' r;

    let tsm_ = vaddm tsm s s' r in
    if not tsm_.failed then
    begin
      assert (addm_precond a /\ addm_postcond a tsm_);
      assert (related_addm_param a i_a);

      let i_tsm_ = IV.addm ir is is' i_tsm in
      assert (IV.addm_precond i_a /\ IV.addm_postcond i_a i_tsm_);

      related_addm_postcond a i_a tsm_ i_tsm_;
      ()
    end
module Zeta.Steel.ThreadSim

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 U32 = FStar.UInt32

let related_key_inj_1 (sk:s_base_key) (ik0 ik1:i_base_key)
  : Lemma 
    (requires
      related_base_key sk ik0 /\
      related_base_key sk ik1)
    (ensures
      ik0 == ik1)
    [SMTPat (related_base_key sk ik0);
     SMTPat (related_base_key sk ik1)]
  = KeyUtils.lift_lower_inv ik0;
    KeyUtils.lift_lower_inv ik1

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


let addm_prop (tsm: thread_state_model) (s s': T.slot_id) (r: s_record)
  : Lemma (requires (all_props tsm.store))
          (ensures (let tsm_ = vaddm tsm s s' r in
                    let a = AMP s r s' tsm in
                    (addm_precond a /\ addm_postcond a tsm_) \/
                    (tsm_.failed)))
  = let tsm_ = vaddm tsm s s' r in
    let a = AMP s r s' tsm in
    if not (check_slot_bounds s)
     || not (check_slot_bounds s')
    then
    begin
      assert(~ (addm_precond0 a));
      assert(tsm_.failed);
      ()
    end
    else
    begin
      match r with
      | ( gk, gv ) ->
      begin
        (* check store contains slot s' *)
        match get_entry tsm s' with
        | None ->
          assert (~ (addm_precond1 a));
          assert (tsm_.failed);
          ()
        | Some r' ->
          let k' = to_base_key r'.key in
          let v' = r'.value in
          let k = to_base_key gk in
          (* check k is a proper desc of k' *)
          if not (KU.is_proper_descendent k k') then
          begin
            assert (~ (addm_precond1 a));
            assert (tsm_.failed);
            ()
          end
          (* check store does not contain slot s *)
          else if Some? (get_entry tsm s) then
          begin
            assert (~ (addm_precond1 a));
            assert (tsm_.failed);
            ()
          end
          (* check v' is a merkle value *)
          else match to_merkle_value v' with
          | None -> assert (False); ()
          | Some v' ->
            let d = KU.desc_dir k k' in
            let dh' = desc_hash_dir v' d in
            let h = s_hashfn gv in

            assert (addm_precond1 a);

            match dh' with
            | T.Dh_vnone _ -> (* k' has no child in direction d *)
              // case A: of addm
              assert (addm_precond2 a);
              assert (addm_anc_points_null a);
              (* first add must be init value *)
              if not (T.eq_value gv (init_value gk)) then
              begin
                assert (addm_value_pre a =!= init_value (addm_key a));
                assert (~ (addm_precond a));
                assert (tsm_.failed);
                ()
              end
              else if TSM.points_to_some_slot tsm s' d then
              begin
                assert (tsm_.failed);
                assert (~ (addm_precond a));
                ()
              end
              else
              begin
                (* all preconditions are satisifed through case A *)
                assert (addm_precond a);
                assert (addm_value_postcond a gv);
                let tsm' = madd_to_store tsm s gk gv s' d in
                assert (madd_to_store_reqs tsm s gk gv s' d);
                lemma_madd_to_store tsm s gk gv s' d;
                let v'_upd = update_merkle_value v' d k zero false in
                assert (addm_anc_val_postcond a v'_upd);
                assert (tsm_ == update_value tsm' s' (T.MValue v'_upd));
                lemma_update_value tsm' s' (T.MValue v'_upd);
                assert (addm_anc_slot_postcond a tsm_.store);
                assert (addm_slot_postcond a tsm_.store);
                assert (~ (addm_has_desc_slot a));
                assert (identical_except2 tsm_.store tsm.store (addm_slot a) (addm_anc_slot a));
                ()
              end
            | T.Dh_vsome {T.dhd_key=k2; T.dhd_h=h2; T.evicted_to_blum = b2} ->
              if KeyUtils.eq_base_key k2 k then (* k is a child of k' *)
              begin
                // case B:
                assert (addm_anc_points_to_key a);
                (* check hashes match and k was not evicted to blum *)
                if not (KeyUtils.eq_u256 h2 h && b2 = T.Vfalse) then
                begin
                  assert (tsm_.failed);
                  assert (~ (addm_precond a));
                  ()
                end
                (* check slot s' does not contain a desc along direction d *)
                else if TSM.points_to_some_slot tsm s' d then
                begin
                  assert (tsm_.failed);
                  assert (~ (addm_precond a));
                  ()
                end
                else
                begin
                  assert (tsm_ == madd_to_store tsm s gk gv s' d);
                  lemma_madd_to_store tsm s gk gv s' d;
                  assert (addm_precond2 a);   
                  FStar.Classical.forall_intro_2 KeyUtils.is_proper_descendent_correct;
                  assert (addm_anc_points_to_desc a ==> (addm_value_pre a == init_value (addm_key a)));
                  assert (addm_precond a);
                  assert (identical_except2 tsm_.store tsm.store (addm_slot a) (addm_anc_slot a));
                  ()
                end
              end
              else if not (T.eq_value gv (init_value gk)) then
              begin
                assert (tsm_.failed);
                assert (~ (addm_precond a));
                ()
              end
              else if not (KU.is_proper_descendent k2 k) then
              begin
                assert (tsm_.failed);
                assert (~ (addm_precond a));
                ()
              end
              else
              begin
                // Case C:
                assert (addm_anc_points_to_desc a);
                let d2 = KU.desc_dir k2 k in
                assert (d2 == addm_desc_dir a);
                let Some mv = to_merkle_value gv in
                let mv_upd = update_merkle_value mv d2 k2 h2 (b2=T.Vtrue) in
                assert (addm_value_postcond a (T.MValue mv_upd));
                let v'_upd = update_merkle_value v' d k zero false in
                assert (addm_anc_val_postcond a v'_upd);
                if TSM.points_to_some_slot tsm s' d then
                begin
                  let tsm' =
                    madd_to_store_split tsm s gk (T.MValue mv_upd) s' d d2 in
                  if tsm_.failed then ()
                  else (
                    lemma_madd_to_store_split tsm s gk (T.MValue mv_upd) s' d d2;
                    assert (addm_slot_points_postcond a tsm'.store);
                    assert (addm_slot_postcond a tsm'.store);
                    assert (tsm_ == update_value tsm' s' (T.MValue v'_upd));
                    lemma_update_value tsm' s' (T.MValue v'_upd);
                    assert (addm_slot_postcond a tsm_.store);
                    assert (addm_anc_slot_postcond a tsm_.store);
                    assert (addm_has_desc_slot a);
                    assert (addm_desc_slot_postcond a tsm_.store);
                    assert (identical_except3 tsm_.store tsm.store (addm_slot a) (addm_anc_slot a) (addm_desc_slot a));
                    ()
                  )
                end
                else
                begin
                  let tsm' = madd_to_store tsm s gk (T.MValue mv_upd) s' d in
                  assert (stored_value tsm'.store s == T.MValue mv_upd);
                  assert (madd_to_store_reqs tsm s gk (T.MValue mv_upd) s' d);
                  lemma_madd_to_store tsm s gk (T.MValue mv_upd) s' d;

                  assert (tsm_ == update_value tsm' s' (T.MValue v'_upd));
                  lemma_update_value tsm' s' (T.MValue v'_upd);
                  assert (addm_slot_postcond a tsm_.store);
                  assert (addm_anc_slot_postcond a tsm_.store);
                  assert (~ (addm_has_desc_slot a));
                  ()
                end
              end
      end
    end

#pop-options

#push-options "--fuel 1 --ifuel 1 --query_stats"
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.RelHashFunction.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.IV.fst.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.HashFunction.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Steel.ThreadSim.fst

    tsm: Zeta.Steel.Rel.s_thread_state ->
    i_tsm: Zeta.Steel.Rel.i_thread_state ->
    se: Zeta.Steel.Rel.s_log_entry ->
    ie: Zeta.Steel.Rel.i_log_entry
  -> FStar.Pervasives.Lemma
      (requires
        Zeta.Steel.ThreadRelDef.related_tsm tsm i_tsm /\ Zeta.Steel.LogRel.related_log_entry se ie /\
        AddM? se /\ Prims.op_Negation (Mkthread_state_model?.failed tsm))
      (ensures
        (let _ = se in
          (let Zeta.Steel.LogEntry.Types.AddM s s' r = _ in
            let _ = ie in
            (let Zeta.GenericVerifier.AddM #_ ir is is' = _ in
              let tsm_ = Zeta.Steel.ThreadStateModel.vaddm tsm s s' r in
              let i_tsm_ = Zeta.Intermediate.Verifier.addm ir is is' i_tsm in
              Prims.op_Negation (Mkthread_state_model?.failed tsm_) ==>
              Zeta.Steel.ThreadRelDef.related_tsm tsm_ i_tsm_)
            <:
            Type0)
          <:
          Type0))
Zeta.Steel.Rel.s_thread_state Zeta.Steel.Rel.i_thread_state Zeta.Steel.Rel.s_log_entry Zeta.Steel.Rel.i_log_entry Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.LogEntry.Types.record Zeta.Record.record Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Prims.op_Negation Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Prims.unit Zeta.Steel.AddMRel.related_addm_postcond Prims._assert Prims.l_and Zeta.Intermediate.Verifier.addm_precond Zeta.Intermediate.Verifier.addm_postcond Zeta.Intermediate.Verifier.vtls_t Prims.l_or Zeta.Intermediate.Verifier.AMP Prims.l_not Prims.b2t Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__valid Zeta.Intermediate.Verifier.addm Zeta.Steel.AddMRel.related_addm_param Zeta.Steel.AddMRel.addm_precond Zeta.Steel.AddMRel.addm_postcond Prims.bool Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.vaddm Zeta.Steel.ThreadSim.addm_prop Zeta.Steel.StoreRel.lemma_related_implies_all_props Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Zeta.Intermediate.Verifier.addm_param Zeta.Steel.AddMRel.addm_param Zeta.Steel.AddMRel.AMP Zeta.Steel.ThreadRelDef.related_tsm Zeta.Steel.LogRel.related_log_entry Zeta.Steel.LogEntry.Types.uu___is_AddM Prims.squash Prims.l_imp Prims.Nil FStar.Pervasives.pattern
let addm_simulation
      (tsm: s_thread_state)
      (i_tsm: i_thread_state)
      (se: s_log_entry)
      (ie: i_log_entry)
    : Lemma
      (requires (related_tsm tsm i_tsm /\ related_log_entry se ie /\ LT.AddM? se /\ not tsm.failed))
      (ensures
        (let LT.AddM s s' r = se in
          let GV.AddM ir is is' = ie in
          let tsm_ = vaddm tsm s s' r in
          let i_tsm_ = IV.addm ir is is' i_tsm in
          (not tsm_.failed) ==> related_tsm tsm_ i_tsm_)) =
  
let LT.AddM s s' r = se in
let GV.AddM ir is is' = ie in
let a = AMP s r s' tsm in
let i_a = IV.AMP is ir is' i_tsm in
lemma_related_implies_all_props tsm.store i_tsm.IV.st;
addm_prop tsm s s' r;
let tsm_ = vaddm tsm s s' r in
if not tsm_.failed
then
  (assert (addm_precond a /\ addm_postcond a tsm_);
    assert (related_addm_param a i_a);
    let i_tsm_ = IV.addm ir is is' i_tsm in
    assert (IV.addm_precond i_a /\ IV.addm_postcond i_a i_tsm_);
    related_addm_postcond a i_a tsm_ i_tsm_;
    ())