Commit 3a6db102 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

fixing

parent 169cdda5
......@@ -208,13 +208,13 @@ Section MSQueue.
inversion H. rewrite <- H2. clear H. clear H1. clear H2.
iClear "Hγm◯".
iMod (own_lat_auth_update_fork _ _ _ with "Hγm●") as "[Hγm● Hγm◯]".
(* iMod (ghost_var_update _ (Lout, γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)". *)
wp_load.
iCombine "Hγ" "HTrade" as "HTrade". rewrite bi.sep_or_l.
rewrite unit_tok_exclusive. iDestruct "HTrade" as "[HF|[Hγ Hl']]"; try done.
iDestruct "Hl'" as "(Hl' & Pv & Hγ')".
iMod (ghost_var_update _ (Lout, γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm● Hγ' Hr]") as "_".
{ iNext. iExists h, t, Lout, γ'. iFrame.
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm● Hγ Hr]") as "_".
{ iNext. iExists h, t, Lout, γ. iFrame.
iExists ((l', v, γ') :: L'). iFrame. iExists d, l. iFrame. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if.
......@@ -225,9 +225,11 @@ Section MSQueue.
iCombine "Hhc" "Hhq" as "Hh". wp_store.
iDestruct "Hh" as "(Hhc & Hhq)".
iMod (ghost_var_update _ (Lout ++ [(l', v, γ')], γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iDestruct (own_lat_auth_max _ _ with "[Hγm● Hγm◯]") as %Hpre. iFrame.
iRename "Hγm◯" into "H".
iMod (own_lat_auth_update _ _ _ (Lout ++ [(l', v, γ')] ++ Lin'') _ with "Hγm●") as "[Hγm● Hγm◯]".
iDestruct (own_lat_auth_max _ _ with "[Hγm● H]") as %Hpre. iFrame.
iMod ("Hclose" with "[Hhq Htq Hr Hγc● Hγm●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists Lin''. iFrame. }
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists Lin''. rewrite app_assoc. iFrame. }
iModIntro. wp_seq. wp_load. wp_proj.
iApply "Post".
iSplitR "Pv".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment