val 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)))
val 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 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
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"
/
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.ThreadStateModel.thread_state_model ->
    s: Zeta.Steel.LogEntry.Types.slot_id ->
    s': Zeta.Steel.LogEntry.Types.slot_id ->
    r: Zeta.Steel.Rel.s_record
  -> FStar.Pervasives.Lemma
      (requires Zeta.Steel.StoreRel.all_props (Mkthread_state_model?.store tsm))
      (ensures
        (let tsm_ = Zeta.Steel.ThreadStateModel.vaddm tsm s s' r in
          let a = Zeta.Steel.AddMRel.AMP s r s' tsm in
          Zeta.Steel.AddMRel.addm_precond a /\ Zeta.Steel.AddMRel.addm_postcond a tsm_ \/
          Mkthread_state_model?.failed tsm_))
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.LogEntry.Types.slot_id Zeta.Steel.Rel.s_record Prims.op_BarBar Prims.op_Negation Zeta.Steel.ThreadStateModel.check_slot_bounds Prims.unit Prims._assert Prims.b2t Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Prims.l_not Zeta.Steel.AddMRel.addm_precond0 Prims.bool Zeta.Steel.LogEntry.Types.key Zeta.Steel.LogEntry.Types.value Zeta.Steel.ThreadStateModel.get_entry Zeta.Steel.AddMRel.addm_precond1 Zeta.Steel.ThreadStateModel.store_entry Zeta.Steel.KeyUtils.is_proper_descendent FStar.Pervasives.Native.uu___is_Some Zeta.Steel.ThreadStateModel.to_merkle_value Prims.l_False Zeta.Steel.LogEntry.Types.mval_value Zeta.Steel.FormatsManual.eq_value Zeta.Steel.ThreadStateModel.init_value Zeta.Steel.AddMRel.addm_precond Prims.eq2 Zeta.Steel.AddMRel.addm_value_pre Zeta.Steel.AddMRel.addm_key Zeta.Steel.ThreadStateModel.points_to_some_slot Zeta.Steel.StoreRel.identical_except2 Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.Steel.AddMRel.addm_slot Zeta.Steel.AddMRel.addm_anc_slot Zeta.Steel.AddMRel.addm_has_desc_slot Zeta.Steel.AddMRel.addm_slot_postcond Zeta.Steel.AddMRel.addm_anc_slot_postcond Zeta.Steel.StoreRel.lemma_update_value Zeta.Steel.LogEntry.Types.MValue Zeta.Steel.ThreadStateModel.update_value Zeta.Steel.AddMRel.addm_anc_val_postcond Zeta.Steel.ThreadStateModel.update_merkle_value Zeta.Steel.ThreadStateModel.zero Zeta.Steel.StoreRel.lemma_madd_to_store Zeta.Steel.StoreRel.madd_to_store_reqs Prims.l_and Prims.op_Equality Prims.nat FStar.Seq.Base.length FStar.Pervasives.Native.option Prims.l_Forall Zeta.Steel.FormatsManual.slot Prims.l_imp Zeta.Steel.ThreadStateModel.has_slot Zeta.Steel.LogEntry.Types.uu___is_ApplicationKey Zeta.Steel.ThreadStateModel.key_of_slot Zeta.Steel.ThreadStateModel.madd_to_store Zeta.Steel.AddMRel.addm_value_postcond Zeta.Steel.AddMRel.addm_anc_points_null Zeta.Steel.AddMRel.addm_precond2 Zeta.Steel.KeyUtils.base_key Zeta.Steel.LogEntry.Types.hash_value Zeta.Steel.LogEntry.Types.vbool Zeta.Steel.KeyUtils.eq_base_key Prims.op_AmpAmp Zeta.Steel.KeyUtils.eq_u256 Zeta.Steel.LogEntry.Types.Vfalse Zeta.Steel.AddMRel.addm_anc_points_to_desc FStar.Classical.forall_intro_2 Prims.l_iff Zeta.Steel.KeyUtils.is_desc Zeta.Steel.KeyUtils.is_proper_descendent_correct Zeta.Steel.AddMRel.addm_anc_points_to_key Zeta.Steel.StoreRel.identical_except3 Zeta.Steel.AddMRel.addm_desc_slot Zeta.Steel.AddMRel.addm_desc_slot_postcond Zeta.Steel.AddMRel.addm_slot_points_postcond Zeta.Steel.StoreRel.lemma_madd_to_store_split Zeta.Steel.ThreadStateModel.madd_to_store_split Zeta.Steel.StoreRel.stored_value Zeta.Steel.LogEntry.Types.Vtrue Zeta.Steel.AddMRel.addm_desc_dir Zeta.Steel.KeyUtils.desc_dir Zeta.Steel.Rel.s_hashfn Zeta.Steel.LogEntry.Types.descendent_hash Zeta.Steel.ThreadStateModel.desc_hash_dir Zeta.Steel.ThreadStateModel.to_base_key Zeta.Steel.LogEntry.Types.is_value_of Zeta.Steel.ThreadStateModel.__proj__Mkstore_entry__item__key Zeta.Steel.ThreadStateModel.__proj__Mkstore_entry__item__value Zeta.Steel.AddMRel.addm_param Zeta.Steel.AddMRel.AMP Zeta.Steel.ThreadStateModel.vaddm Zeta.Steel.StoreRel.all_props Prims.squash Prims.l_or Zeta.Steel.AddMRel.addm_postcond Prims.Nil FStar.Pervasives.pattern
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
  (assert (~(addm_precond0 a));
    assert (tsm_.failed);
    ())
else
  match r with
  | gk, gv ->
    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
      if not (KU.is_proper_descendent k k')
      then
        (assert (~(addm_precond1 a));
          assert (tsm_.failed);
          ())
      else
        if Some? (get_entry tsm s)
        then
          (assert (~(addm_precond1 a));
            assert (tsm_.failed);
            ())
        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 _ ->
              assert (addm_precond2 a);
              assert (addm_anc_points_null a);
              if not (T.eq_value gv (init_value gk))
              then
                (assert (addm_value_pre a =!= init_value (addm_key a));
                  assert (~(addm_precond a));
                  assert (tsm_.failed);
                  ())
              else
                if TSM.points_to_some_slot tsm s' d
                then
                  (assert (tsm_.failed);
                    assert (~(addm_precond a));
                    ())
                else
                  (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));
                    ())
            | T.Dh_vsome { T.dhd_key = k2 ; T.dhd_h = h2 ; T.evicted_to_blum = b2 } ->
              if KeyUtils.eq_base_key k2 k
              then
                (assert (addm_anc_points_to_key a);
                  if not (KeyUtils.eq_u256 h2 h && b2 = T.Vfalse)
                  then
                    (assert (tsm_.failed);
                      assert (~(addm_precond a));
                      ())
                  else
                    if TSM.points_to_some_slot tsm s' d
                    then
                      (assert (tsm_.failed);
                        assert (~(addm_precond a));
                        ())
                    else
                      (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));
                        ()))
              else
                if not (T.eq_value gv (init_value gk))
                then
                  (assert (tsm_.failed);
                    assert (~(addm_precond a));
                    ())
                else
                  if not (KU.is_proper_descendent k2 k)
                  then
                    (assert (tsm_.failed);
                      assert (~(addm_precond a));
                      ())
                  else
                    (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
                        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));
                            ())
                      else
                        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));
                        ())