Commit 57c68486 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update to new Iris and tweak stuff.

parent 9e4c88e4
......@@ -113,11 +113,9 @@ Section typed_interp.
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext.
iIntros {l} "Hl".
iIntros {l} "Hl". iPvsIntro.
iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial].
trivial.
iNext; iExists _; iFrame "Hl"; trivial.
[| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
- (* Load *)
smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst.
......@@ -126,9 +124,7 @@ Section typed_interp.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hw1". iNext.
iIntros "Hw1". iSplitL; trivial.
iNext; iExists _. iFrame "Hw1"; trivial.
iFrame "Hw1". iIntros "> Hw1". iPvsIntro. iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
......@@ -140,8 +136,7 @@ Section typed_interp.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hz1".
iIntros "> Hz1".
iSplitL; [|iPvsIntro; trivial].
iNext; iExists _. iFrame "Hz1"; trivial.
iIntros "> Hz1". iPvsIntro.
iSplitL; [|iPvsIntro; trivial]. eauto.
Qed.
End typed_interp.
......@@ -206,7 +206,7 @@ Section lang_rules.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Φ :
to_val e = Some v
ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LocV l))
ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) ={E}= Φ (LocV l))
WP Alloc e @ E {{ Φ }}.
Proof.
intros. set (φ e' σ' ef := l,
......@@ -225,7 +225,7 @@ Section lang_rules.
Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v
ownP σ (ownP σ - Φ v) WP Load (Loc l) @ E {{ Φ }}.
ownP σ (ownP σ ={E}= Φ v) WP Load (Loc l) @ E {{ Φ }}.
Proof.
intros.
rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //; cbn; eauto.
......@@ -234,7 +234,7 @@ Section lang_rules.
Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v σ !! l = Some v'
ownP σ (ownP (<[l:=v]>σ) - Φ UnitV) WP Store (Loc l) e @ E {{ Φ }}.
ownP σ (ownP (<[l:=v]>σ) ={E}= Φ UnitV) WP Store (Loc l) e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (UnitV) (<[l:=v]>σ) None)
?right_id //; cbn; eauto.
......@@ -243,15 +243,15 @@ Section lang_rules.
Lemma wp_alloc N E e v Φ :
to_val e = Some v nclose N E
heap_ctx N ( l, l v - Φ (LocV l)) WP Alloc e @ E {{ Φ }}.
heap_ctx N ( l, l v ={E}= Φ (LocV l)) WP Alloc e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
iIntros {l} "[% Hheap]". iPvsIntro. iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hheap". iSplit; first iPureIntro.
{ by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
......@@ -260,29 +260,29 @@ Section lang_rules.
Lemma wp_load N E l q v Φ :
nclose N E
heap_ctx N l {q} v (l {q} v - Φ v)
heap_ctx N l {q} v (l {q} v ={E}= Φ v)
WP Load (Loc l) @ E {{ Φ }}.
Proof.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iExists _; iSplit; first done.
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
rewrite of_heap_singleton_op //. by iFrame.
Qed.
Lemma wp_store N E l v' e v Φ :
to_val e = Some v nclose N E
heap_ctx N l v' (l v - Φ UnitV)
heap_ctx N l v' (l v ={E}= Φ UnitV)
WP Store (Loc l) e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
rewrite of_heap_singleton_op //; eauto. by iFrame.
Qed.
......@@ -314,31 +314,31 @@ Section lang_rules.
Lemma wp_Fold E e v Φ :
to_val e = Some v
Φ v WP Unfold (Fold e) @ E {{ Φ }}.
(|={E}=> Φ v) WP Unfold (Fold e) @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Unfold _) (of_val v) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- rewrite right_id -wp_value_pvs'; auto using uPred.later_mono.
- intros. inv_step; auto.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v1 WP Fst (Pair e1 e2) @ E {{ Φ }}.
(|={E}=> Φ v1) WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- rewrite right_id; auto using uPred.later_mono, wp_value_pvs'.
- intros. inv_step; auto.
Qed.
Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v2 WP Snd (Pair e1 e2) @ E {{ Φ }}.
(|={E}=> Φ v2) WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Snd (Pair _ _)) (of_val v2) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- rewrite right_id; auto using uPred.later_mono, wp_value_pvs'.
- intros. inv_step; auto.
Qed.
......@@ -349,7 +349,7 @@ Section lang_rules.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step
(Case (InjL _) _ _) (e1.[of_val v0/]) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- rewrite right_id; auto using uPred.later_mono, wp_value_pvs'.
- intros. inv_step; auto.
Qed.
......@@ -360,7 +360,7 @@ Section lang_rules.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step
(Case (InjR _) _ _) (e2.[of_val v0/]) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- rewrite right_id; auto using uPred.later_mono, wp_value_pvs'.
- intros. inv_step; auto.
Qed.
End lang_rules.
......@@ -289,6 +289,7 @@ Section CG_Counter.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=".
iPvsIntro.
(* establishing the invariant *)
iAssert (( n, l ↦ₛ (v false) cnt ↦ᵢ (v n) cnt' ↦ₛ (v n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv".
......@@ -316,14 +317,14 @@ Section CG_Counter.
iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iApply wp_load; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt".
iIntros "> {$Hcnt} Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_lam; trivial. asimpl. iNext.
(* fine-grained performs increment *)
iApply (@wp_bind _ _ _ [IfCtx _ _; CasRCtx (LocV _) (NatV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_nat_bin_op; simpl.
iNext.
iNext. iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> (N .@4) as {n'} "[Hl [Hcnt Hcnt']]".
......@@ -336,7 +337,7 @@ Section CG_Counter.
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt".
iNext; iFrame "Hcnt"; iIntros "Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_true. iNext. iApply wp_value; trivial.
iExists UnitV; iFrame; auto.
......@@ -345,7 +346,7 @@ Section CG_Counter.
iApply (wp_cas_fail _ _ _ _ (v n')); simpl; trivial;
[inversion 1; subst; auto | | iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt".
iNext; iFrame "Hcnt"; iIntros "Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of read *)
......@@ -362,7 +363,7 @@ Section CG_Counter.
{ by iFrame "Hspec Hcnt' Hj". }
iApply wp_load; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iFrame "Hcnt"; iIntros "> Hcnt".
iFrame "Hcnt"; iIntros "> Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iExists (v _); eauto.
Unshelve.
......
......@@ -61,10 +61,10 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _); AllocCtx; FoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {istk} "Histk".
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iPvsIntro. iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {stk} "Hstk".
simpl. iApply wp_lam; trivial. iNext. simpl.
simpl. iApply wp_lam; trivial. iPvsIntro. iNext. simpl.
rewrite FG_push_subst FG_pop_subst FG_iter_subst. simpl. asimpl.
(* establishing the invariant *)
iPvs (own_alloc ( ( : stackUR))) as {γ} "Hemp".
......@@ -115,7 +115,7 @@ Section Stack_refinement.
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv (N .@4) as {istk v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Hstk".
iNext. iIntros "Hstk".
iNext. iIntros "Hstk". iPvsIntro.
iSplitL "Hoe Hstk' HLK Hl Hstk".
iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk".
clear v h.
......@@ -125,7 +125,7 @@ Section Stack_refinement.
FoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
iApply wp_alloc; simpl; trivial; [by rewrite to_of_val|].
iFrame "Hheap". iNext. iIntros {ltmp} "Hltmp".
iFrame "Hheap". iNext. iIntros {ltmp} "Hltmp". iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
iInv (N .@4) as {istk2 v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
......@@ -137,7 +137,6 @@ Section Stack_refinement.
iPvs (steps_CG_locked_push _ _ _ j K _ _ _ _ _ with "[Hj Hl Hstk']")
as "[Hj [Hstk' Hl]]".
{ rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
iApply wp_pvs.
iApply (wp_cas_suc _ _ _ _ _ _ _ _ _ _ _); simpl; trivial.
iFrame "Hheap Hstk". iNext. iIntros "Hstk".
iSplitR "Hj".
......@@ -153,7 +152,7 @@ Section Stack_refinement.
iApply wp_if_true. iNext; iApply wp_value; trivial.
iExists UnitV; eauto.
* iApply (wp_cas_fail _ _ _ _ _ _ _ _ _ _ _ _ _ _); simpl; trivial.
iFrame "Hheap Hstk". iNext. iIntros "Hstk".
iFrame "Hheap Hstk". iNext. iIntros "Hstk". iPvsIntro.
iSplitR "Hj".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
......@@ -169,9 +168,7 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _); UnfoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv (N .@4) as {istk v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
iApply wp_pvs.
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Hstk".
iIntros "> Hstk".
iApply (wp_load _ _ _ _ _ _ _). iIntros "{$Hheap $Hstk} > Hstk".
(* Checking whether the stack is empty *)
iDestruct (StackLink_dup with "[HLK]") as "[HLK HLK']"; trivial.
rewrite {2}StackLink_unfold.
......@@ -186,7 +183,7 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
iApply wp_Fold; simpl; auto using to_of_val.
iNext. iApply wp_lam; auto using to_of_val. iNext. asimpl.
iNext. iPvsIntro. iApply wp_lam; auto using to_of_val. iNext. asimpl.
clear h.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
......@@ -195,7 +192,7 @@ Section Stack_refinement.
as "[Histk HLoe]".
{ by iFrame "Hmpt". }
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Histk".
iIntros "> Histk". iSplitR "Hj".
iIntros "> Histk". iPvsIntro. iSplitR "Hj".
{ iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl".
iDestruct ("HLoe" with "[Histk]") as "[Hh _]"; trivial.
}
......@@ -210,7 +207,7 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
iApply wp_Fold; simpl; auto using to_of_val.
iNext. iApply wp_lam; auto using to_of_val. iNext. asimpl.
iNext. iApply wp_lam; auto using to_of_val. iPvsIntro. iNext. asimpl.
clear h.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
......@@ -219,7 +216,7 @@ Section Stack_refinement.
as "[Histk HLoe]".
{ by iFrame "Hmpt". }
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Histk".
iIntros "> Histk".
iIntros "> Histk". iPvsIntro.
iDestruct ("HLoe" with "[Histk]") as "[Hh Hmpt]"; trivial.
iSplitR "Hj Hmpt HLK'".
{ iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
......@@ -232,7 +229,7 @@ Section Stack_refinement.
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
asimpl. iApply wp_snd; [simpl; by rewrite ?to_of_val |
simpl; by rewrite ?to_of_val |].
simpl. iNext.
simpl. iNext. iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
clear istk3 h. asimpl.
......@@ -242,9 +239,8 @@ Section Stack_refinement.
destruct (decide (istk2 = istk3)) as [|Hneq]; subst.
-- (* CAS succeeds *)
(* In this case, the specification pushes *)
iApply wp_pvs.
iApply (wp_cas_suc _ _ _ _ _ _ _ _ _ _ _).
iFrame "Hheap Hstk". iIntros "> Hstk {HLK'}".
iIntros "{$Hheap $Hstk} > Hstk {HLK'}".
iDestruct (StackLink_dup with "[HLK]") as "[HLK HLK']"; trivial.
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as {istk4 w2} "[% [Hmpt' HLK']]"; simplify_eq/=.
......@@ -260,8 +256,7 @@ Section Stack_refinement.
with "[Hj Hstk' Hl]") as "[Hj [Hstk' Hl]]".
{ by iFrame "Hspec Hstk' Hl Hj". }
iPvsIntro. iSplitR "Hj".
{ iNext.
iClear "Hmpt Hmpt' HLK". rewrite StackLink_unfold.
{ iIntros "{Hmpt Hmpt' HLK} >". rewrite StackLink_unfold.
iDestruct "HLK''" as {istk5 w2} "[% [Hmpt HLK]]"; simplify_eq/=.
iExists istk5, _, _. iFrame "Hoe Hstk' Hstk Hl".
rewrite StackLink_unfold.
......@@ -273,13 +268,13 @@ Section Stack_refinement.
iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
iApply wp_fst; [simpl; by rewrite ?to_of_val |
simpl; by rewrite ?to_of_val |].
iNext. iApply wp_value; simpl.
iNext. iPvsIntro. iApply wp_value; simpl.
{ by rewrite to_of_val. }
iExists (InjRV _); iFrame "Hj".
iRight. iExists (_, _). iSplit; trivial.
-- (* CAS will fail *)
iApply (wp_cas_fail _ _ _ _ _ _ _ _ _ _ _ _ _ _).
iFrame "Hheap Hstk". iIntros "> Hstk". iSplitR "Hj".
iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro. iSplitR "Hj".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of iter *)
......@@ -301,7 +296,7 @@ Section Stack_refinement.
with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]".
{ rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". }
iApply (wp_load _ _ _ _ _ _ _).
iFrame "Hheap Hstk". iIntros "> Hstk".
iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
iDestruct (StackLink_dup with "HLK") as "[HLK HLK']".
iSplitR "Hj HLK'".
{ iNext. iExists _, _, _; by iFrame "Hoe Hstk' Hstk HLK Hl". }
......@@ -315,7 +310,7 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [CaseCtx _ _; LoadCtx]); iApply wp_wand_l;
iSplitR; [iIntros {v} "Hw"; iExact "Hw"|].
iApply wp_Fold; simpl; trivial.
iNext. simpl.
iNext. iPvsIntro. simpl.
iApply (@wp_bind _ _ _ [CaseCtx _ _]); iApply wp_wand_l;
iSplitR; [iIntros {v} "Hw"; iExact "Hw"|].
rewrite StackLink_unfold.
......@@ -324,9 +319,7 @@ Section Stack_refinement.
iDestruct (stack_owns_later_open_close with "[Hmpt Hoe]")
as "[Histk HLoe]".
{ by iFrame "Hmpt". }
iApply wp_pvs.
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Histk".
iIntros "> Histk".
iApply (wp_load _ _ _ _ _ _ _). iIntros "{$Hheap $Histk} > Histk".
iDestruct ("HLoe" with "[Histk]") as "[Hh Hmpt]"; trivial.
iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
* rewrite CG_iter_of_val.
......@@ -349,7 +342,7 @@ Section Stack_refinement.
iNext.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _); AppRCtx _]);
iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
iApply wp_fst; simpl; rewrite ?to_of_val; trivial. iNext.
iApply wp_fst; simpl; rewrite ?to_of_val; trivial. iNext. iPvsIntro.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
rewrite StackLink_unfold.
......
......@@ -73,12 +73,11 @@ Section typed_interp.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
inversion H; subst.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]"; simplify_eq.
iPvs (step_fst _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
_ _ _ with "* [-]") as "Hw".
iFrame "Hspec Hv"; trivial.
iApply wp_fst; eauto using to_of_val; cbn.
iApply wp_fst; try iPvsIntro; eauto using to_of_val; cbn.
(* unshelving *)
Unshelve. all: eauto using to_of_val.
Qed.
......@@ -197,7 +196,7 @@ Section typed_interp.
iDestruct "Hiv" as {n} "[% %]"; subst; simpl.
iDestruct "Hiw" as {n'} "[% %]"; subst; simpl.
iPvs (step_nat_bin_op _ _ _ j K _ _ _ _ with "* [-]") as "Hz".
iFrame "Hspec Hw"; trivial. iApply wp_nat_bin_op. iNext.
iFrame "Hspec Hw"; trivial. iApply wp_nat_bin_op. iNext. iPvsIntro.
iExists _; iSplitL; eauto.
destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; iExists _; iSplit; trivial.
......@@ -342,7 +341,7 @@ Section typed_interp.
iApply wp_pvs.
iPvs (step_alloc _ _ _ j K (# v') v' _ _ with "* [-]") as {l'} "[Hj Hl']"; eauto.
iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext. iIntros {l} "Hl".
iIntros "{$Hheap} >". iIntros {l} "Hl". iPvsIntro.
iAssert (( w : val * val, l ↦ᵢ w.1 l' ↦ₛ w.2
((@interp _ _ _ (N .@ 1) τ) Δ) w)%I)
with "[Hl Hl']" as "Hinv".
......@@ -384,7 +383,7 @@ Section typed_interp.
iFrame "Hspec Hv"; trivial.
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
SolveDisj 2 l.
iFrame "Hw1". iIntros "> Hw1". iSplitL "Hw1 Hw2".
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
+ iNext; iExists w; by iFrame.
+ iPvsIntro.
destruct w as [w1 w2]; iExists w2; iFrame "Hv Hw3"; trivial.
......@@ -413,8 +412,7 @@ Section typed_interp.
iFrame "Hspec Hw Hw2"; trivial.
iApply (wp_store (N .@ 2)); auto using to_of_val.
SolveDisj 2 l.
iFrame "Hheap Hw1". iIntros "> Hw1".
iSplitL "Hw1 Hw2".
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
+ iNext; iExists (w, w'); by iFrame.
+ iPvsIntro. iExists UnitV; iFrame "Hw" ; iSplit; trivial.
(* unshelving *)
......@@ -450,8 +448,7 @@ Section typed_interp.
repeat subst; trivial. }
iApply (wp_cas_suc (N .@ 2)); eauto using to_of_val.
SolveDisj 2 l.
iFrame "Hheap Hw1". iIntros "> Hw1".
iSplitL "Hw1 Hw2".
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists (v true); iFrame "Hw"; eauto.
+ iPvs (step_cas_fail _ _ _ j K (l.2) 1 (z2) (# w') w' (# u') u' _ _ _
......@@ -461,7 +458,7 @@ Section typed_interp.
iDestruct "Hiw" as "%". iDestruct "Hw3" as "%"; subst; eauto. }
iApply (wp_cas_fail (N .@ 2)); eauto using to_of_val.
SolveDisj 2 l.
iFrame "Hheap Hw1". iIntros "> Hw1". iSplitL "Hw1 Hw2".
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists (v false); iFrame "Hw". iExists _; iSplit; trivial.
(* unshelving *)
......
......@@ -28,7 +28,7 @@ Section typed_interp.
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ]"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
......@@ -43,7 +43,7 @@ Section typed_interp.
smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHHtyped2.
iDestruct "Hv" as {n} "%"; iDestruct "Hv'" as {n'} "%"; subst. simpl.
iApply wp_nat_bin_op. iNext; destruct op; simpl;
iApply wp_nat_bin_op. iNext; iPvsIntro; destruct op; simpl;
try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec;
eauto 10.
- (* pair *)
......@@ -131,11 +131,9 @@ Section typed_interp.
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext.
iIntros {l} "Hl".
iIntros {l} "Hl". iPvsIntro.
iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial].
trivial.
iNext; iExists _; iFrame "Hl"; trivial.
[| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
- (* Load *)
smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst.
......@@ -144,9 +142,7 @@ Section typed_interp.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hw1". iNext.
iIntros "Hw1". iSplitL; trivial.
iNext; iExists _. iFrame "Hw1"; trivial.
iFrame "Hw1". iIntros "> Hw1". iPvsIntro; iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
......@@ -158,9 +154,7 @@ Section typed_interp.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hz1".
iIntros "> Hz1".
iSplitL; [|iPvsIntro; trivial].
iNext; iExists _. iFrame "Hz1"; trivial.
iIntros "> Hz1". iPvsIntro. iSplitL; [|iPvsIntro; trivial]; eauto.
- (* CAS *)
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHHtyped2; cbn.
......@@ -172,15 +166,12 @@ Section typed_interp.
destruct (val_dec_eq v2 w) as [|Hneq]; subst.
+ iApply (wp_cas_suc N); eauto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hw1".
iNext. iIntros "Hw1".
iFrame "Hheap Hw1". iIntros "> Hw1"; iPvsIntro.
iSplitL; [|iPvsIntro]; eauto.
+ iApply (wp_cas_fail N); eauto using to_of_val.
clear Hneq. specialize (HNLdisj l); set_solver_ndisj.
(* Weird that Hneq above makes set_solver_ndisj diverge or
take exceptionally long!?!? *)
iFrame "Hheap Hw1".
iNext. iIntros "Hw1".
iSplitL; [|iPvsIntro]; eauto.
iFrame "Hheap Hw1". iIntros "> Hw1". iPvsIntro. iSplitL; [|iPvsIntro]; eauto.
Qed.
End typed_interp.
......@@ -214,7 +214,7 @@ Section lang_rules.
by apply pure_elim_r.
Qed.
Lemma heap_mapsto_dup_invalid l v1 v2 : l ↦ᵢ v1 l ↦ᵢ v2 False%I.
Lemma heap_mapsto_dup_invalid l v1 v2 : l ↦ᵢ v1 l ↦ᵢ v2 False.
Proof.
rewrite heap_mapsto_op /heapI_mapsto auth_own_valid.
iIntros "[_ Hv]". iDestruct "Hv" as %Hv.
......@@ -227,7 +227,7 @@ Section lang_rules.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Φ :
to_val e = Some v
ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LocV l))
ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) ={E}= Φ (LocV l))
WP Alloc e @ E {{ Φ }}.
Proof.
intros. set (φ e' σ' ef :=
......@@ -246,7 +246,7 @@ Section lang_rules.
Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v
ownP σ (ownP σ - Φ v) WP Load (Loc l) @ E {{ Φ }}.
ownP σ (ownP σ ={E}= Φ v) WP Load (Loc l) @ E {{ Φ }}.
Proof.
intros.
rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //; cbn; eauto.
......@@ -255,7 +255,7 @@ Section lang_rules.
Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v σ !! l = Some v'
ownP σ (ownP (<[l:=v]>σ) - Φ UnitV) WP Store (Loc l) e @ E {{ Φ }}.
ownP σ (ownP (<[l:=v]>σ) ={E}= Φ UnitV) WP Store (Loc l) e @</