Commit ffbf81d9 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `_open` -> `_acc` to be consistent with Iris.

parent d308a9ec
Pipeline #24435 passed with stage
in 25 minutes and 36 seconds
......@@ -149,7 +149,7 @@ There is a correspondence between the invariant rules presented in the
paper with Hoare triples and those in the formalization.
- `TINV-ALLOC` and `LTINV-ALLOC` follow from `fcinv_alloc_named`.
- `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_open`.
- `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_acc`.
- `TINV-DEALLOC` and `LTINV-DEALLOC` follow from `fcinv_cancel`.
All of these theorems are proven in `theories/iron_logic/fcinv.v`.
......@@ -184,11 +184,11 @@ is discussed above, we also provide an explicit table for convenience.
| `HOARE-FORK-EMP`/`HOARE-FORK-TRUE` | `wp_fork` | `iron/theories/heap_lang/lifting.v` |
| `INV-DUP` | `inv_persistent` | `iron/theories/heap_lang/lifting.v` |
| `INV-ALLOC` | `inv_alloc` | `iris-coq/theories/base_logic/lib/invariants.v` |
| `INV-OPEN` | `inv_open` | `iris-coq/theories/base_logic/lib/invariants.v` |
| `INV-OPEN` | `inv_acc` | `iris-coq/theories/base_logic/lib/invariants.v` |
| `TINV-SPLIT` | `fcinv_own_fractional` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-OPEN` | `fcinv_acc` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` |
| Uniform with respect to fractions | `Uniform` | `iron/theories/iron_logic/iron.v` |
| `HOARE-CONS` | `ht_vs` | `iris-coq/theories/program_logic/hoare.v` |
......@@ -218,7 +218,7 @@ is discussed above, we also provide an explicit table for convenience.
| `LTINV-SPLIT` | `fcinv_own_fractional` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-OPEN` | `fcinv_acc` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` |
| Definition of Hoare triples | `iron_wp` | `iron/theories/iron_logic/weakestpre.v` |
| Theorem 5.1 | `heap_basic_adequacy` | `iron/theories/heap_lang/adequacy.v` |
......
......@@ -9,7 +9,7 @@ Section special.
Implicit Types P : ironProp Σ.
Definition special P Ψ γ:= (P Ψ γ fcinv_own γ (1/2) fcinv_cancel_own γ (1/2))%I.
Lemma fcinv_open_special E N γ P `{!Uniform P} Ψ `{!Uniform (Ψ γ)} `{!ExistPerm (Ψ γ)}:
Lemma fcinv_acc_special E N γ P `{!Uniform P} Ψ `{!Uniform (Ψ γ)} `{!ExistPerm (Ψ γ)}:
N E
fcinv N γ (special P Ψ γ) -
fcinv_own γ (1/2) - fcinv_cancel_own γ (1/2) ={E,E∖↑N}= ( P (Ψ γ ={E∖↑N,E}= emp) (Ψ γ) (emp ={E∖↑N,E}= emp)).
......@@ -134,7 +134,7 @@ Section proof.
iIntros "#Hinv !#" (Φ) "[Hcinv Hcancel] Hcont".
wp_let.
wp_bind (FAA _ _).
iMod (fcinv_open_special with "Hinv Hcinv Hcancel") as "[[Hpt Hclose] | [Hpt Hclose]]"; first done.
iMod (fcinv_acc_special with "Hinv Hcinv Hcancel") as "[[Hpt Hclose] | [Hpt Hclose]]"; first done.
- wp_apply (iron_wp_faa with "Hpt").
iIntros "Hpt".
iMod ("Hclose" with "[$Hpt]") as "_".
......
......@@ -154,7 +154,7 @@ Section proofs.
iIntros (Φ) "(#Hdestruct & [#Hinv [Hbag1 Hbag2]] & Hinv_own & Hinv_cancel & Hcancel1 & Hcancel2 & Hown) HΦ".
iLöb as "IH". wp_rec. repeat wp_let.
wp_bind (! _)%E.
iMod (fcinv_open_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iMod (fcinv_acc_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iDestruct "Hinv'" as "[H1 | [H2 | [H3 | H4]]]".
- iDestruct "H1" as "[>Hx Hrest]".
wp_load.
......@@ -171,7 +171,7 @@ Section proofs.
wp_if.
wp_bind (Load _).
iMod (fcinv_open_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iMod (fcinv_acc_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iDestruct "Hinv'" as "[H1 | [H2 | [H3 | H4]]]".
+ iDestruct "H1" as "(>Hx & >Hy & Hrest)".
wp_load.
......@@ -303,7 +303,7 @@ Section proofs.
iIntros (Φ) "Hend HΦ".
iDestruct "Hend" as (q_en q_de x_alive y_alive ->) "(Hxalive & Hremove & Hinsert & Hinv_own & #(Hinv & Hbag1 & Hbag2))".
wp_lam. wp_proj. wp_let.
iMod (fcinv_open_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iMod (fcinv_acc_strong _ (N .@ "sts") with "Hinv Hinv_own") as "(Hinv' & Hinv_own & Hclose)"; auto.
iDestruct "Hinv'" as "[H1 | [H2 | [H3 | H4 ]]]".
- iDestruct "H1" as "(Hx & Hy & Hchoice)".
wp_store.
......@@ -328,7 +328,7 @@ Section proofs.
iIntros (Φ) "Hend HΦ".
iDestruct "Hend" as (q_en q_de x_alive y_alive ->) "(Hyalive & Hremove & Hinsert & Hinv_own & #(Hinv & Hbag1 & Hbag2))".
wp_lam. wp_proj. wp_let.
iMod (fcinv_open_strong _ (N .@ "sts") with "Hinv Hinv_own") as "[Hinv' [Hinv_own Hclose]]"; auto.
iMod (fcinv_acc_strong _ (N .@ "sts") with "Hinv Hinv_own") as "[Hinv' [Hinv_own Hclose]]"; auto.
iDestruct "Hinv'" as "[H1 | [H2 | [H3 | H4]]]".
- iDestruct "H1" as "(Hx & Hy & Hchoice)".
wp_store.
......
......@@ -242,7 +242,7 @@ Section queue_spec.
iDestruct "Hh" as (?? ?%eq_sym) "(Hγinv & Hlhptr & Hγd)"; simplify_eq.
iDestruct "Hlhptr" as (l) "Hlhptr".
wp_lam; wp_proj; wp_let. wp_load; wp_let. wp_bind (! _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh lt vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt)".
iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %->; simpl.
destruct vs as [|v vs'].
......@@ -258,7 +258,7 @@ Section queue_spec.
{ iExists lh, lt, (v :: vs'). iNext. iFrame "Hvs Hlhptr' Hlt Hγe".
iExists l'. auto with iFrame. }
clear vs'. iModIntro. wp_match. wp_proj. wp_let. wp_bind (_ <- _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh' lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt)".
iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %?%eq_sym; simplify_eq.
destruct vs as [|v' vs'].
......@@ -291,7 +291,7 @@ Section queue_spec.
"(Hγinv & Hγe' & Hltptr)"; simplify_eq.
do 2 wp_lam. wp_proj; wp_let. wp_load; wp_let.
wp_alloc ltn as "Hltn"; wp_let. wp_bind (_ <- _)%E.
iMod (fcinv_open _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] Hγinv") as "(H & Hγinv & Hclose)"; first done.
iDestruct "H" as (lh lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt')".
iDestruct (own_valid_2 with "Hγe Hγe'")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
......@@ -438,7 +438,7 @@ Section queue_bag_spec.
wp_apply (enqueue_spec (N .@ "queue") _ _ _ _ (queue_bag_queue_name γ)
with "[] Henqueue"); eauto; first by solve_ndisj.
iIntros (vs) "Hbag".
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv")
iMod (fcinv_acc _ (N .@ "inv") with "[$] Hown_inv")
as "(H & Hown_inv & Hclose)"; first by solve_ndisj.
iDestruct "H" as (xs) "[>Hqueue_contents Hall]".
iDestruct (queue_own_agree with "Hbag Hqueue_contents") as %->.
......@@ -460,7 +460,7 @@ Section queue_bag_spec.
iIntros (? Φ) "([#Hqueue #Hinv] & Hdequeue & Hown_inv) HΦ".
wp_apply (dequeue_spec (N .@ "queue") with "[] Hdequeue"); eauto; first by solve_ndisj.
iIntros (vs) "Hbag".
iMod (fcinv_open _ (N .@ "inv") with "[$] Hown_inv")
iMod (fcinv_acc _ (N .@ "inv") with "[$] Hown_inv")
as "(H & Hinv_own & Hclose)"; first by solve_ndisj.
iDestruct "H" as (xs) "[>Hqueue_contents Hall]".
iDestruct (queue_own_agree with "Hbag Hqueue_contents") as %->.
......
......@@ -43,7 +43,7 @@ Section proof1.
{ iNext. iLeft. iFrame. }
wp_apply (iron_wp_fork with "[Ht₁ Hcown₁ HΦ]").
- iNext. do 2 wp_lam. wp_alloc k as "Hk". wp_let.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(HInv & [Hcown₁ Hclose])"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(HInv & [Hcown₁ Hclose])"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]".
+ wp_store. iDestruct (transfer_combine with "Ht₁ Hs₁") as "Hs₂".
iMod ("Hclose" with "[Hcown₁ Hl Hk Hs₂]") as "_".
......@@ -52,7 +52,7 @@ Section proof1.
+ iDestruct (transfer_incompat with "Ht₁ Hs₂") as %[].
+ iDestruct (transfer_incompat with "Ht₁ Hs₃") as %[].
- iLöb as "IH". wp_rec. wp_bind (! _)%E.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(HInv & Hcown₂ & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(HInv & Hcown₂ & Hclose)"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]";
last by iDestruct (transfer_incompat with "Ht₂ Hs₃") as %[].
+ wp_load. iMod ("Hclose" with "[Hl Hs₁]").
......@@ -93,14 +93,14 @@ Section proof2.
{ iExists NONEV; eauto with iFrame. }
wp_apply (iron_wp_fork with "[Hγ HΦ]").
- iIntros "!>". do 2 wp_lam. wp_alloc k as "Hk". wp_let.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iDestruct "Hinv" as (v) ">[Hl [->|Hinv]]".
+ wp_store. iApply "HΦ". iApply "Hclose".
iLeft. iExists (SOMEV (#k)). auto 10 with iFrame.
+ iDestruct "Hinv" as (k') "(_&?&Hγ')".
by iDestruct (fcinv_own_valid with "Hγ Hγ'") as %[].
- iLöb as "IH"; wp_rec. wp_bind (! _)%E.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iDestruct "Hinv" as (v) ">[Hl [->|Hinv]]".
+ wp_load. iMod ("Hclose" with "[Hl]").
{ iLeft. iExists NONEV. eauto 10 with iFrame. }
......
......@@ -45,14 +45,14 @@ Section proof1.
wp_apply (par_spec (λ _, fcinv_own γinv (1 / 2))%I
(λ _, fcinv_own γinv (1 / 2) <affine> t γ )%I with "[Ht₁ Hcown₁] [Ht₂ Hcown₂]").
- do 2 wp_lam. wp_alloc k as "Hk". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & $ & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] [$]") as "(HInv & $ & Hclose)"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]".
+ wp_store. iDestruct (transfer_combine with "Ht₁ Hs₁") as "Hs₂".
iApply "Hclose". iNext. iRight. iLeft. eauto with iFrame.
+ iDestruct (transfer_incompat with "Ht₁ Hs₂") as %[].
+ iDestruct (transfer_incompat with "Ht₁ Hs₃") as %[].
- wp_lam. iLöb as "IH"; wp_rec. wp_bind (! _)%E.
iMod (fcinv_open _ N with "[$] [$]") as "(HInv & Hγ & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] [$]") as "(HInv & Hγ & Hclose)"; first done.
iDestruct "HInv" as ">[[Hs₁ Hl] | [[Hs₂ H] | [Hs₃ H]]]";
last (iDestruct (transfer_incompat with "Ht₂ Hs₃") as %[]).
+ wp_load. iMod ("Hclose" with "[Hl Hs₁]").
......@@ -94,13 +94,13 @@ Section proof2.
{ iExists NONEV; eauto with iFrame. }
wp_apply (par_spec (λ _, emp)%I (λ _, l -)%I with "[Hγ] [Hγc Hγ']").
- do 2 wp_lam. wp_alloc k as "Hk". wp_let.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iDestruct "Hinv" as (v) ">[Hl [->|Hinv]]".
+ wp_store. iApply "Hclose". iLeft. iExists (SOMEV (#k)). auto 10 with iFrame.
+ iDestruct "Hinv" as (k') "(_&?&Hγ')".
by iDestruct (fcinv_own_valid with "Hγ Hγ'") as %[].
- wp_lam. iLöb as "IH"; wp_rec. wp_bind (! _)%E.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγ & Hclose)"; first done.
iDestruct "Hinv" as (v) ">[Hl [->|Hinv]]".
+ wp_load. iMod ("Hclose" with "[Hl]").
{ iLeft. iExists NONEV. eauto 10 with iFrame. }
......
......@@ -96,7 +96,7 @@ Section proof.
{{{ b, RET #b; is_lock N γ lk p R if b is true then locked γ R else emp }}}.
Proof.
iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (l ->) "(#? & Hγinvc & Hγinv)". wp_lam.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[>Hl H]".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). iSplit; last done.
......@@ -124,7 +124,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hγ & HR) HΦ".
iDestruct "Hlock" as (l ->) "(#? & Hγinvc & Hγinv)". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[Hl Hinv]".
- wp_store. iMod ("Hclose" with "[HR Hl Hγ]").
{ iNext. iExists false; iFrame. }
......
......@@ -110,7 +110,7 @@ Section proof.
{{{ b, RET #b; if b is true then locked γ p R else unlocked γ p }}}.
Proof.
iIntros (Φ) "[Hl [Hγinv HC]] HΦ". iDestruct "Hl" as (l ->) "#?". wp_lam.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[>Hl H]".
- wp_cas_fail. iMod ("Hclose" with "[Hl H]").
{ iLeft. iModIntro. iExists true. iFrame. }
......@@ -139,7 +139,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & [Hγinv [HC Hγf]] & HR) HΦ".
iDestruct "Hlock" as (l ->) "#?". wp_let.
iMod (fcinv_open _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iMod (fcinv_acc _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[Hl Hinv]".
- wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv']".
iDestruct (own_valid_2 with "Hγ Hγf")
......@@ -158,7 +158,7 @@ Section proof.
{{{ is_lock N γ lk R unlocked γ 1 }}} free lk {{{ RET #(); R }}}.
Proof.
iIntros (Φ) "(Hlock & Hunlkd & Hγc) HΦ". iDestruct "Hlock" as (l ->) "#?". wp_lam.
iMod (fcinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iMod (fcinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as ([|]) "[>Hl H]".
- iDestruct "H" as (p) ">[_ Hγinv']".
by iDestruct (fcinv_own_valid with "Hγinv Hγinv'") as %?%(exclusive_l _).
......@@ -195,7 +195,7 @@ Section adequacy_proofs.
iApply (Hspec with "[$Hunlocked //]").
iIntros "!>" (_) "[Hown Hcancel]".
iDestruct "Hlock" as (l) "[% #Hinv]"; simplify_eq.
iMod (fcinv_open_strong with "Hinv Hown") as "(Hlock_inv & Hown & ?)"; first done.
iMod (fcinv_acc_strong with "Hinv Hown") as "(Hlock_inv & Hown & ?)"; first done.
iDestruct "Hlock_inv" as ([]) "[>Hl H]".
- iDestruct "H" as (p) "[? >Hown']".
by iDestruct (fcinv_own_valid with "Hown Hown'") as %Hcontra%Qp_not_plus_q_ge_1.
......
......@@ -139,7 +139,7 @@ Proof.
rewrite Some_op_opM /=. eauto with iFrame.
Qed.
Lemma fcinv_open_strong E N γ p P `{!Uniform P} :
Lemma fcinv_acc_strong E N γ p P `{!Uniform P} :
N E
fcinv N γ P -
fcinv_own γ p ={E,E∖↑N}=
......@@ -197,17 +197,17 @@ Lemma fcinv_cancel E N γ P `{!Uniform P} :
fcinv_own γ 1 ={E}= P.
Proof.
iIntros (?) "#? Hγc Hγ".
iMod (fcinv_open_strong with "[$] [$]") as "($ & Hγ & Hclose)"; first done.
iMod (fcinv_acc_strong with "[$] [$]") as "($ & Hγ & Hclose)"; first done.
iApply "Hclose"; iRight; iFrame.
Qed.
Lemma fcinv_open E N γ p P `{!Uniform P} :
Lemma fcinv_acc E N γ p P `{!Uniform P} :
N E
fcinv N γ P -
fcinv_own γ p ={E,E∖↑N}= P fcinv_own γ p ( P ={E∖↑N,E}= emp).
Proof.
iIntros (?) "#? Hγ".
iMod (fcinv_open_strong with "[$] [$]") as "($ & $ & Hclose)"; first done.
iMod (fcinv_acc_strong with "[$] [$]") as "($ & $ & Hclose)"; first done.
iIntros "!> HP". iApply "Hclose"; auto.
Qed.
End fcinv.
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