Commit f1a8bd8d authored by Dan Frumin's avatar Dan Frumin

Cleaner proof of the stack refinement

parent 7b1728ba
...@@ -46,7 +46,7 @@ Section Mod_refinement. ...@@ -46,7 +46,7 @@ Section Mod_refinement.
{ rewrite /prestack_owns big_sepM_empty fmap_empty. { rewrite /prestack_owns big_sepM_empty fmap_empty.
iFrame "Hemp". } iFrame "Hemp". }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]". iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
iAssert (preStackLink γ (R τi) (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK". iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
{ rewrite preStackLink_unfold. { rewrite preStackLink_unfold.
iExists _, _. iSplitR; simpl; trivial. iExists _, _. iSplitR; simpl; trivial.
iFrame "Histk". iLeft. iSplit; trivial. } iFrame "Histk". iLeft. iSplit; trivial. }
......
...@@ -11,14 +11,11 @@ Section Stack_refinement. ...@@ -11,14 +11,11 @@ Section Stack_refinement.
Implicit Types Δ : listC D. Implicit Types Δ : listC D.
Import lang. Import lang.
Program Definition R (τi : prodC valC valC -> iProp Σ) := λne ww, ( τi ww)%I.
Next Obligation. solve_proper. Qed.
Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ := Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ :=
( (istk : loc) v h, (prestack_owns γ h) ( (istk : loc) v h, (prestack_owns γ h)
stk' ↦ₛ v stk' ↦ₛ v
stk ↦ᵢ (FoldV #istk) stk ↦ᵢ (FoldV #istk)
preStackLink γ (R τi) (#istk, v) preStackLink γ τi (#istk, v)
l' ↦ₛ #false)%I. l' ↦ₛ #false)%I.
Context `{stackG Σ}. Context `{stackG Σ}.
...@@ -26,7 +23,7 @@ Section Stack_refinement. ...@@ -26,7 +23,7 @@ Section Stack_refinement.
( (istk : loc) v h, (stack_owns h) ( (istk : loc) v h, (stack_owns h)
stk' ↦ₛ v stk' ↦ₛ v
stk ↦ᵢ (FoldV #istk) stk ↦ᵢ (FoldV #istk)
StackLink (R τi) (#istk, v) StackLink τi (#istk, v)
l ↦ₛ #false)%I. l ↦ₛ #false)%I.
Lemma sinv_unfold τi stk stk' l : Lemma sinv_unfold τi stk stk' l :
sinv τi stk stk' l = sinv' stack_name τi stk stk' l. sinv τi stk stk' l = sinv' stack_name τi stk stk' l.
...@@ -38,7 +35,7 @@ Section Stack_refinement. ...@@ -38,7 +35,7 @@ Section Stack_refinement.
Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ : Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ :
N ## logrelN N ## logrelN
inv N (sinv τi st st' l) - (R τi) (v,v') - inv N (sinv τi st st' l) - τi (v,v') -
Γ (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit. Γ (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
Proof. Proof.
iIntros (?) "#Hinv #Hvv'". iIntros (Δ). iIntros (?) "#Hinv #Hvv'". iIntros (Δ).
...@@ -344,7 +341,7 @@ Section Full_refinement. ...@@ -344,7 +341,7 @@ Section Full_refinement.
{ rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty. { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
iFrame "Hemp". } iFrame "Hemp". }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]". iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
iAssert (StackLink (R τi) (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK". iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
{ rewrite StackLink_unfold. { rewrite StackLink_unfold.
iExists _, _. iSplitR; simpl; trivial. iExists _, _. iSplitR; simpl; trivial.
iFrame "Histk". iLeft. iSplit; trivial. } iFrame "Histk". iLeft. iSplit; trivial. }
......
...@@ -55,7 +55,7 @@ Section Rules_pre. ...@@ -55,7 +55,7 @@ Section Rules_pre.
( (l : loc) w, v.1 = # l l ↦ˢᵗᵏ w ( (l : loc) w, v.1 = # l l ↦ˢᵗᵏ w
((w = InjLV #() v.2 = FoldV (InjLV #())) ((w = InjLV #() v.2 = FoldV (InjLV #()))
( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
v.2 = FoldV (InjRV (PairV y2 z2)) Q (y1, y2) P(z1, z2))))%I. v.2 = FoldV (InjRV (PairV y2 z2)) Q (y1, y2) P(z1, z2))))%I.
Solve Obligations with solve_proper. Solve Obligations with solve_proper.
Global Instance StackLink_pre_contractive Q : Contractive (preStackLink_pre Q). Global Instance StackLink_pre_contractive Q : Contractive (preStackLink_pre Q).
...@@ -69,12 +69,12 @@ Section Rules_pre. ...@@ -69,12 +69,12 @@ Section Rules_pre.
((w = InjLV #() v.2 = FoldV (InjLV #())) ((w = InjLV #() v.2 = FoldV (InjLV #()))
( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
v.2 = FoldV (InjRV (PairV y2 z2)) v.2 = FoldV (InjRV (PairV y2 z2))
Q (y1, y2) preStackLink Q (z1, z2))))%I. Q (y1, y2) preStackLink Q (z1, z2))))%I.
Proof. by rewrite {1}/preStackLink fixpoint_unfold. Qed. Proof. by rewrite {1}/preStackLink fixpoint_unfold. Qed.
Global Opaque preStackLink. (* So that we can only use the unfold above. *) Global Opaque preStackLink. (* So that we can only use the unfold above. *)
Global Instance preStackLink_persistent (Q : D) v `{ vw, Persistent (Q vw)} : Global Instance preStackLink_persistent (Q : D) v :
Persistent (preStackLink Q v). Persistent (preStackLink Q v).
Proof. Proof.
rewrite /Persistent. rewrite /Persistent.
...@@ -166,10 +166,10 @@ Section Rules. ...@@ -166,10 +166,10 @@ Section Rules.
((w = InjLV #() v.2 = FoldV (InjLV #())) ((w = InjLV #() v.2 = FoldV (InjLV #()))
( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
v.2 = FoldV (InjRV (PairV y2 z2)) v.2 = FoldV (InjRV (PairV y2 z2))
Q (y1, y2) StackLink Q (z1, z2))))%I. Q (y1, y2) StackLink Q (z1, z2))))%I.
Proof. by rewrite /StackLink preStackLink_unfold. Qed. Proof. by rewrite /StackLink preStackLink_unfold. Qed.
Global Instance StackLink_persistent (Q : D) v `{ vw, Persistent (Q vw)} : Global Instance StackLink_persistent (Q : D) v :
Persistent (StackLink Q v). Persistent (StackLink Q v).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Opaque StackLink. Global Opaque StackLink.
......
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