Commit dccfaef2 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (`iPoseProof` changes).

Also, some refactoring, e.g. remove useless parameter of `heap_ctx`.
parent 54ac23ef
Pipeline #21422 passed with stage
in 15 minutes and 24 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2019-11-07.1.891124d6") | (= "dev") }
"coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
]
......@@ -27,7 +27,7 @@ Proof. solve_inG. Qed.
Theorem heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ},
([ map] l v σ, l v)
WP e @ s; {{ v, |={,}=> h m, heap_ctx h [] m - ⌜φ v h⌝⎤ }}%I)
WP e @ s; {{ v, |={,}=> h m, heap_ctx h m - ⌜φ v h⌝⎤ }}%I)
adequate s e σ φ.
Proof.
(* TODO: refactor this proof so we don't have the two cases *)
......@@ -38,7 +38,7 @@ Proof.
by apply ufrac_auth_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first by apply auth_auth_valid.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iExists heap_perm, (λ σ _, heap_ctx σ), (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf".
{ iExists . rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
......@@ -56,12 +56,11 @@ Proof.
apply ufrac_auth_valid; by apply to_heap_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first by apply auth_auth_valid.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iExists heap_perm, (λ σ _, heap_ctx σ), (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf".
{ iExists . rewrite /= fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
iDestruct (big_mapsto_alt_2 with "Hσ'") as "Hσ'"; first done.
iDestruct ("Hwp" with "Hσ'") as "Hwp'".
iDestruct ("Hwp" with "[Hσ']") as "Hwp'"; first by iApply big_mapsto_alt_2.
iApply (iron_wp_wand with "Hwp'").
iIntros (v π1) "Hupd". iExists π1, ε; repeat (iSplit || iModIntro)=> //.
iIntros (π2 π3 h2 Qs Hπ) "Hctx _ _".
......@@ -103,7 +102,7 @@ Proof.
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iExists heap_perm, (λ σ _, heap_ctx σ), (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
{ iExists . rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
......@@ -113,7 +112,7 @@ Proof.
iExists π, ε; iSplit; first (by rewrite left_id_L right_id_L).
iFrame "Hσ2". iModIntro; iSplit; first done.
iIntros (π1 π2 Hπ) "Hσ2' HQs Hp' Hσ2". rewrite to_heap_empty.
iMod (heap_thread_adequacy _ _ _ (1/2 + π1)%Qp
iMod (heap_thread_adequacy _ _ (1/2 + π1)%Qp
with "Hσ2' [HQs] [Hσ' Hp'] Hσ2") as "$".
{ by rewrite -frac_op' cmra_op_opM_assoc_L -Hπ frac_op' Qp_div_2. }
{ by iApply big_sepL_replicate. }
......@@ -128,7 +127,7 @@ Proof.
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iExists heap_perm, (λ σ _, heap_ctx σ), (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
{ iExists . rewrite /= fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
......
......@@ -38,7 +38,7 @@ Definition heapG_ironInvG `{hG : heapG Σ} : ironInvG Σ := {|
fcinv_inG := heapG_fcinv_inG;
|}.
Definition heap_ctx `{hG : heapG Σ} (σ : state) (_ : list ()) (n : nat) : iProp Σ :=
Definition heap_ctx `{hG : heapG Σ} (σ : state) (n : nat) : iProp Σ :=
( πfs,
size πfs = n
own (heapG_fork_post_name hG) ( (Excl <$> πfs : gmap _ (excl (option ufrac))))
......@@ -53,7 +53,7 @@ Arguments heap_ctx : simpl never.
Instance heapG_ironG `{hG : heapG Σ} : ironG heap_lang Σ := {|
iron_invG := heapG_invG;
iron_iron_invG := heapG_ironInvG;
iron_state_interp := heap_ctx;
iron_state_interp σ _ := heap_ctx σ;
iron_fork_post _ := heap_fork_post;
|}.
......@@ -218,9 +218,9 @@ Section heap.
Qed.
(* heap_ctx manipulating lemmas *)
Lemma heap_thread_adequacy σ κ n π1 π2 σ' :
Lemma heap_thread_adequacy σ n π1 π2 σ' :
π1 ? π2 = 1%Qp
heap_ctx σ κ n -
heap_ctx σ n -
[] replicate n heap_fork_post -
heap_perm π1 -
([ map] lv σ', l v) π2 ==
......@@ -261,15 +261,15 @@ Section heap.
by rewrite -cmra_opM_opM_assoc_L /= -(comm_L _ π) cmra_op_opM_assoc_L.
Qed.
Lemma heap_thread_alloc σ κ n π :
heap_ctx σ κ n == i,
heap_ctx σ κ (S n)
Lemma heap_thread_alloc σ n π :
heap_ctx σ n == i,
heap_ctx σ (S n)
from_option perm True π
own (heapG_fork_post_name _) ( {[ i := Excl π ]}).
Proof.
iDestruct 1 as (πfs Hsize) "[Hn Hσ]".
set (i := fresh (dom (gset positive) πfs)).
assert (πfs !! i = None) by (by eapply not_elem_of_dom, is_fresh).
assert (πfs !! i = None) by (by eapply (not_elem_of_dom (D:=gset positive)), is_fresh).
iMod (own_update with "Hn") as "[Hn Hi]".
{ apply auth_update_alloc, (alloc_singleton_local_update _ i (Excl π))=> //.
by rewrite lookup_fmap fmap_None. }
......@@ -287,10 +287,10 @@ Section heap.
rewrite -cmra_opM_opM_assoc_L fmap_insert. iFrame.
Qed.
Lemma heap_alloc σ κ n l v π :
Lemma heap_alloc σ n l v π :
σ !! l = None
heap_ctx σ κ n - perm π ==
heap_ctx (<[l:=v]>σ) κ n (l v) (Some π).
heap_ctx σ n - perm π ==
heap_ctx (<[l:=v]>σ) n (l v) (Some π).
Proof.
iIntros (?). rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hp".
......@@ -301,9 +301,9 @@ Section heap.
iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
Qed.
Lemma heap_dealloc σ κ n l v π :
heap_ctx σ κ n - (l v) (Some π) ==
heap_ctx (delete l σ) κ n perm π.
Lemma heap_dealloc σ n l v π :
heap_ctx σ n - (l v) (Some π) ==
heap_ctx (delete l σ) n perm π.
Proof.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl".
......@@ -316,8 +316,8 @@ Section heap.
iModIntro. iFrame "Hl". iExists πfs. by iFrame.
Qed.
Lemma heap_valid σ κ n l q v π :
heap_ctx σ κ n - (l {q} v) π - ⌜σ !! l = Some v.
Lemma heap_valid σ n l q v π :
heap_ctx σ n - (l {q} v) π - ⌜σ !! l = Some v.
Proof.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
......@@ -325,9 +325,9 @@ Section heap.
as %Hl%ufrac_auth_included%Some_included_total%heap_singleton_included.
Qed.
Lemma heap_update σ κ n l v1 v2 π :
heap_ctx σ κ n - (l v1) π ==
heap_ctx (<[l:=v2]>σ) κ n (l v2) π.
Lemma heap_update σ n l v1 v2 π :
heap_ctx σ n - (l v1) π ==
heap_ctx (<[l:=v2]>σ) n (l v2) π.
Proof.
rewrite /heap_ctx /perm mapsto_eq /mapsto_def /=.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hl". destruct π as [π|]=>//.
......
......@@ -173,7 +173,7 @@ Section adequacy_proofs.
Lemma lock_always_freed_force_location `{!heapG Σ} l :
l #false -
σ m, heap_ctx σ [] m - ⌜σ !! l = Some #false .
σ m, heap_ctx σ m - ⌜σ !! l = Some #false .
Proof.
iStartProof (iProp _).
iIntros (π) "Hl"; iIntros (h Qs) "Hctx".
......
......@@ -109,7 +109,7 @@ Lemma wp_fork s E e π ΦΦ :
Proof.
iIntros "HΦ Hwp". iApply wp_lift_head_step_fupd; [done|].
iIntros (σ1 κ κs n) "Hσ".
iMod (heap_thread_alloc _ _ _ π with "Hσ") as (i) "(Hσ & Hp & Hi)".
iMod (heap_thread_alloc _ _ π with "Hσ") as (i) "(Hσ & Hp & Hi)".
iMod (fupd_intro_mask' E ) as "Hclose"; [set_solver|].
iModIntro; iSplit; [by auto|]; iIntros (e2 σ2 efs Hstep); inv_head_step.
iIntros "!> !>". iMod "Hclose" as "_"; iModIntro. iFrame "Hσ".
......@@ -123,7 +123,7 @@ Lemma twp_fork s E e π ΦΦ :
Proof.
iIntros "HΦ Hwp". iApply twp_lift_head_step; [done|].
iIntros (σ1 κs n) "Hσ".
iMod (heap_thread_alloc _ _ _ π with "Hσ") as (i) "(Hσ & Hp & Hi)".
iMod (heap_thread_alloc _ _ π with "Hσ") as (i) "(Hσ & Hp & Hi)".
iMod (fupd_intro_mask' E ) as "Hclose"; [set_solver|].
iModIntro; iSplit; [by auto|]; iIntros (κ e2 σ2 efs Hstep); inv_head_step.
iMod "Hclose" as "_"; iModIntro. iSplit; first done. iFrame "Hσ".
......
......@@ -152,8 +152,8 @@ Proof.
iAssert ( π3 π4, π2 = π3 ? π4 perm (π3 (π21 ? π22)) P π4)%I
with "[Hp Hp' HP]" as (π3 π4) "(>-> & >[Hp Hp'] & HP)".
{ iIntros "/= !>". destruct π22 as [π22|]; last (iExists π2, ε; by iFrame).
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (uniform with "[$HP $Hp1]") as "HP".
rewrite (comm_L _ π22). iDestruct (uniform with "HP") as "[HP Hp1]".
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (@uniform with "[$HP $Hp1]") as "HP".
rewrite (comm_L _ π22). iDestruct (@uniform with "HP") as "[HP Hp1]".
iExists (π2 / 2)%Qp, (Some (π2 / 2)%Qp). iFrame.
by rewrite /= !frac_op' Qp_div_2. }
iExists π3, π4. iModIntro; iSplit; [done|iFrame "Hp"].
......@@ -163,8 +163,8 @@ Proof.
- iAssert ( π7 π8, π21 ? π22 = π7 ? π8 (perm (π7 (π6 ? π5)) P π8))%I
with "[HP Hp Hp']" as (π7 π8) "(>-> & >[Hp Hp'] & HP)".
{ iNext. destruct π5 as [π5|]; last (iExists (π21 ? π22), ε; by iFrame).
iDestruct "Hp'" as "[Hp1 Hp2]". iDestruct (uniform with "[$HP $Hp1]") as "HP".
rewrite (comm_L _ π5). iDestruct (uniform with "HP") as "[HP Hp1]".
iDestruct "Hp'" as "[Hp1 Hp2]". iDestruct (@uniform with "[$HP $Hp1]") as "HP".
rewrite (comm_L _ π5). iDestruct (@uniform with "HP") as "[HP Hp1]".
iExists ((π21 ? π22) / 2)%Qp, (Some ((π21 ? π22) / 2)%Qp). iFrame.
by rewrite /= !frac_op' Qp_div_2. }
iMod ("Hclose" with "[Hγauth Hp HP]") as "_"; first by eauto with iFrame.
......
......@@ -52,7 +52,7 @@ Proof. split. done. apply _. Qed.
Class Uniform `{ironInvG Σ} (P : ironProp Σ) :=
uniform π1 π2 : P (Some (π1 π2)) P (Some π1) perm π2.
Arguments Uniform {_ _} _%I.
Hint Mode Uniform + + ! : typeclass_instances.
Hint Mode Uniform + - ! : typeclass_instances.
Instance: Params (@Uniform) 2 := {}.
Class ExistPerm `{ironInvG Σ} (P : ironProp Σ) :=
......
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