Commit 082d7aa1 authored by Hai Dang's avatar Hai Dang
Browse files

Fix build w.r.t StackLocalLite of elim stack

parent 3c00d63c
......@@ -653,6 +653,8 @@ Proof.
(* TODO: make lemma *)
iMod (ge_list_alloc []) as (γ) "[oT #oTs]".
iMod (meta_set _ _ (γsb, γsx, γb, γx, γ) N with "Hms") as "#Hms"; [done|].
(* allocate the extra invariant for the elimination stack *)
iMod (inv_alloc N _ (ElimStackInv γg γsb γsx γb γx γ s b x true)
with "[Is Ix GM1 Hsx oT]") as "#I".
......@@ -661,8 +663,8 @@ Proof.
iApply ("Post" $! γg). iSplitR "GM2"; last by iFrame.
(* StackLocal *)
iFrame "Gn". iExists b, x, γsb, γsx, γb, γx, γ. iExists , , , , [].
iFrame "sbs sx SLs I oTs".
iFrame "Gn". iExists b, x, γsb, γsx, γb, γx, γ.
iFrame "Hms sbs sx". iExists , , , , []. iFrame "SLs I oTs".
iMod ("ELx" $! _ N _) as "$". iIntros "!>".
iPureIntro. by intros ??.
Qed.
......@@ -673,8 +675,8 @@ Lemma try_push_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
Proof.
iIntros (s tid γg G1 M V0 v Posv) "#sV0 #[Gs1 SL]".
iIntros (Φ) "AU".
iDestruct "SL" as (b x γsb γsx γb γx γ) "SL".
iDestruct "SL" as (Gb0 Mb0 Gx0 Mx0 T0) "(sbs & sx & SLb0 & ELx0 & %EL0 & LT0 & II)".
iDestruct "SL" as (b x γsb γsx γb γx γ) "(MT & sbs & sx & SL)".
iDestruct "SL" as (Gb0 Mb0 Gx0 Mx0 T0) "(SLb0 & ELx0 & %EL0 & LT0 & II)".
set E1 := G1.(Es).
(* store our local observations at an old view *)
......@@ -781,8 +783,8 @@ Proof.
rewrite -(view_at_objective_iff (graph_snap γg _ ) V').
iCombine "GEs Gs1'" as "Gs". iApply (view_at_mono with "Gs"); [done|].
iIntros "(Gs1 & Gs2)". by iApply (graph_snap_mono with "Gs1 Gs2").
- iExists _, _, _, _, _, _, _. iExists Gb0, Mb0, Gx0, Mx0, T0. iFrame "#".
by iPureIntro. }
- iExists _, _, _, _, _, _, _. iFrame "MT sbs' sx'".
iExists Gb0, Mb0, Gx0, Mx0, T0. by iFrame (EL0) "SLb0' ELx0' LT0 II". }
iAssert ( StackProps G Gb Gx' T (b1 || negb b2)
(if b1 || negb b2
......@@ -1031,14 +1033,13 @@ Proof.
iAssert (@{V'} graph_snap γg G' M')%I as "#Gs5". { iFrame "Gs' SL'". }
iAssert (@{V'} StackLocal' N γg s G' M')%I as "#SSL'".
iAssert (@{V'} StackLocal' N γg s G' M')%I with "[]" as "#SSL'".
{ (* updated StackLocal' *)
iFrame "Gs5".
iExists b, x, γsb, γsx, γb, γx, γ.
iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
(* We can just use the old observation because the observations of
exchanges SOMEHOW(?!) do not matter. *)
iExists Gb0, Mb0, Gx0, Mx0, T'.
iFrame "II LT'". iFrame "sbs' sx' SLb0' ELx0'". by iPureIntro. }
iExists Gb0, Mb0, Gx0, Mx0, T'. by iFrame (EL') "SLb0' ELx0' II LT' ". }
iAssert (StackViews γb b G' Gb T') with "[SV BI]" as "#SV'".
{ iIntros (e eV ve [[EqeV|[-> <-]]%lookup_app_1 IP]).
......@@ -1241,11 +1242,9 @@ Proof.
by apply (ElimStackLocalEvents_mono EL0). }
iAssert (@{V'} graph_snap γg G' M')%I as "#Gs3". { iFrame "Gs' SL'". }
iAssert (@{V'} StackLocal' N γg s G' M')%I as "#SSL'".
{ iFrame "Gs3".
iExists b, x, γsb, γsx, γb, γx, γ.
iExists Gb', Mb', Gx0, Mx0, T'.
iFrame "II LT'". iFrame "sbs' sx' SLb' ELx0'". by iPureIntro. }
iAssert (@{V'} StackLocal' N γg s G' M')%I with "[]" as "#SSL'".
{ iFrame "Gs3". iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
iExists Gb', Mb', Gx0, Mx0, T'. by iFrame (EL') "SLb' ELx0' II LT'". }
iAssert (StackViews γb b G' Gb' T') with "[SV BI]" as "#SV'".
{ iIntros (e eV ve [[EqeV|[-> <-]]%lookup_app_1 IP]).
......@@ -1274,8 +1273,8 @@ Lemma try_pop_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
Proof.
iIntros (s tid γg G1 M V0) "#sV0 #[Gs1 SL]".
iIntros (Φ) "AU".
iDestruct "SL" as (b x γsb γsx γb γx γ) "SL".
iDestruct "SL" as (Gb0 Mb0 Gx0 Mx0 T0) "(sbs & sx & SLb0 & ELx0 & %EL0 & LT0 & II)".
iDestruct "SL" as (b x γsb γsx γb γx γ) "(MT & sbs & sx & SL)".
iDestruct "SL" as (Gb0 Mb0 Gx0 Mx0 T0) "(SLb0 & ELx0 & %EL0 & LT0 & II)".
(* store our local observations at an old view *)
iCombine "sbs sx Gs1 SLb0 ELx0" as "THUNK".
......@@ -1391,9 +1390,8 @@ Proof.
rewrite -(view_at_objective_iff (graph_snap γg _ ) V1).
iCombine "GEs Gs1'" as "Gs". iApply (view_at_mono with "Gs"); [done|].
iIntros "(Gs1 & Gs2)". by iApply (graph_snap_mono with "Gs1 Gs2").
- iExists b, x, γsb, γsx, γb, γx, γ.
iExists Gb0, Mb0, Gx0, Mx0, T0. iFrame "#".
iPureIntro. by apply (ElimStackLocalEvents_mono EL0). }
- iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
iExists Gb0, Mb0, Gx0, Mx0, T0. by iFrame (EL0) "SLb0' ELx0' LT0 II". }
iFrame "SI' sV5 SSL'". iSplit. { iPureIntro. split; [done|by left]. }
iIntros "HΦ !>". iSplitL "HΦ".
......@@ -1811,9 +1809,8 @@ Proof.
iAssert (@{V'} graph_snap γg G' M')%I as "#Gs5". { iFrame "Gs' SL'". }
iAssert (@{V'} StackLocal' N γg s G' M')%I as "#SSL'".
{ iFrame "Gs5".
iExists b, x, γsb, γsx, γb, γx, γ. iExists Gb, Mb', Gx', Mx', T'.
iFrame "II LT'". iFrame "sbs' sx' EL' SLL'". by iPureIntro. }
{ iFrame "Gs5". iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
iExists Gb, Mb', Gx', Mx', T'. by iFrame (EL') "SLL' EL' LT' II". }
iIntros "!>".
iExists vp, V', G', psId, ppId, (Push vp), (Pop vp).
......@@ -2051,9 +2048,8 @@ Proof.
iAssert (@{V'} graph_snap γg G' M')%I as "#Gs3". { iFrame "Gs' SL'". }
iAssert (@{V'} StackLocal' N γg s G' M')%I as "#SSL'".
{ iFrame "Gs3".
iExists b, x, γsb, γsx, γb, γx, γ. iExists Gb', Mb', Gx0, Mx0, T'.
iFrame "sbs' sx' SLb' ELx0' LT' II". by iPureIntro. }
{ iFrame "Gs3". iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
iExists Gb', Mb', Gx0, Mx0, T'. by iFrame (EL') "SLb' ELx0' LT' II". }
iIntros "!>".
iExists 0, V', G', dummy_eid, ppIde, dummy_sevt, EmpPop.
......@@ -2394,9 +2390,8 @@ Proof.
iAssert (@{V'} graph_snap γg G' M')%I as "#Gs3". { iFrame "Gs' SL'". }
iAssert (@{V'} StackLocal' N γg s G' M')%I as "#SSL'".
{ iFrame "Gs3".
iExists b, x, γsb, γsx, γb, γx, γ. iExists Gb', Mb', Gx0, Mx0, T'.
iFrame "sbs' sx' SLb' ELx0' LT' II". by iPureIntro. }
{ iFrame "Gs3". iExists b, x, γsb, γsx, γb, γx, γ. iFrame "MT sbs' sx'".
iExists Gb', Mb', Gx0, Mx0, T'. by iFrame (EL') "SLb' ELx0' LT' II". }
iIntros "!>".
iExists v, V', G', psIde, ppIde, (Push v), (Pop v).
......
Supports Markdown
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