Commit d523c690 authored by Ralf Jung's avatar Ralf Jung
Browse files

Strengthen auth_both_valid and auth_both_frac_valid

parent 89c45d21
......@@ -22,6 +22,9 @@ With this release, we dropped support for Coq 8.9.
`A`, and provides some useful lemmas.
* Fix direction of `auth_auth_validN` to make it consistent with similar lemmas,
e.g., `auth_auth_valid`. The direction is now `✓{n} (● a) ↔ ✓{n} a`.
* Rename `auth_both_valid` to `auth_both_valid_discrete` and
`auth_both_frac_valid` to `auth_both_frac_valid_discrete`. The old name is
used for new, stronger lemmas that do not assume discreteness.
**Changes in `proofmode`:**
......@@ -61,6 +64,9 @@ s/\bagree_op_inv'/to_agree_op_inv/g
s/\bagree_op_invL'/to_agree_op_inv_L/g
s/\bauth_auth_frac_op_invL\b/auth_auth_frac_op_inv_L/g
s/\b(excl|frac|ufrac)_auth_agreeL/\1_auth_agree_L/g
# auth_both_valid
s/\bauth_both_valid\b/auth_both_valid_discrete/g
s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
EOF
```
......
......@@ -101,6 +101,12 @@ Proof. intros. apply Auth_discrete; apply _. Qed.
Instance auth_valid : Valid (auth A) := λ x,
match auth_auth_proj x with
| Some (q, ag) =>
(* Note that this definition is not logically equivalent to the more
intuitive [✓ q ∧ ∃ a, ag ≡ to_agree a ∧ auth_frag_proj x ≼ a ∧ ✓ a]
because [∀ n, x ≼{n} y] is not logically equivalent to [x ≼ y]. We have
chosen the current definition (which quantifies over each step-index [n])
so that we can prove [cmra_valid_validN], which does not hold for the
aforementioned more intuitive definition. *)
q ( n, a, ag {n} to_agree a auth_frag_proj x {n} a {n} a)
| None => auth_frag_proj x
end.
......@@ -179,6 +185,24 @@ Proof.
rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
(** This lemma statement is a bit awkward as we cannot possibly extract a single
witness for [b ≼ a] from validity, we have to make do with one witness per step-index. *)
Lemma auth_both_frac_valid q a b :
({q} a b) q ( n, b {n} a) a.
Proof.
rewrite auth_valid_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split.
- intros Hn. split.
+ intros n. destruct (Hn n) as [? [->%(inj to_agree) [Hincl _]]]. done.
+ apply cmra_valid_validN. intros n.
destruct (Hn n) as [? [->%(inj to_agree) [_ Hval]]]. done.
- intros [Hincl Hn] n. eexists. split; first done.
split; first done. apply cmra_valid_validN. done.
Qed.
Lemma auth_both_valid a b :
( a b) ( n, b {n} a) a.
Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
Lemma auth_frag_valid a : ( a) a.
Proof. done. Qed.
Lemma auth_auth_frac_valid q a : ({q} a) q a.
......@@ -214,7 +238,7 @@ Proof.
setoid_rewrite <-(discrete_iff _ a).
setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
Qed.
Lemma auth_both_frac_valid `{!CmraDiscrete A} q a b :
Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
({q} a b) q b a a.
Proof.
rewrite auth_valid_discrete /=. apply and_iff_compat_l.
......@@ -222,8 +246,8 @@ Proof.
- by intros [?[->%(inj to_agree)]].
- naive_solver.
Qed.
Lemma auth_both_valid `{!CmraDiscrete A} a b : ( a b) b a a.
Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b : ( a b) b a a.
Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
Lemma auth_cmra_mixin : CmraMixin (auth A).
Proof.
......
......@@ -67,7 +67,7 @@ Section frac_auth.
Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma frac_auth_included `{CmraDiscrete A} q a b :
(F a F{q} b) Some b Some a.
Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed.
Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
{n} (F a F{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
......
......@@ -87,7 +87,7 @@ Section ufrac_auth.
Proof. by rewrite auth_both_validN=> -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
(U{p} a U{q} b) Some b Some a.
Proof. rewrite auth_both_valid=> -[/Some_pair_included [_ ?] _] //. Qed.
Proof. rewrite auth_both_valid_discrete=> -[/Some_pair_included [_ ?] _] //. Qed.
Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
{n} (U{p} a U{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
......
......@@ -151,7 +151,7 @@ Section auth.
Proof.
iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
iMod (own_alloc_strong ( f t f t) I) as (γ) "[% [Hγ Hγ']]";
[done|by apply auth_both_valid|].
[done|by apply auth_both_valid_discrete|].
iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
......@@ -183,7 +183,7 @@ Section auth.
iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
iModIntro. iExists t.
iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid.
iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid_discrete.
iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
{ eapply auth_update; eassumption. }
......
......@@ -110,7 +110,7 @@ Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (E false E false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid|]).
as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
......
......@@ -346,7 +346,7 @@ Section gen_heap.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
as %[Hl%gen_heap_singleton_included _]%auth_both_valid_discrete; auto.
Qed.
Lemma gen_heap_update σ l v1 v2 :
......@@ -355,7 +355,7 @@ Section gen_heap.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
as %[Hl%gen_heap_singleton_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree (v2:leibnizO _)))=> //.
......
......@@ -137,7 +137,7 @@ Section inv_heap.
v I', h !! l = Some (v, I') w, I w I' w .
Proof.
iIntros "Hl_inv H◯".
iDestruct (own_valid_2 with "H◯ Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
iDestruct (own_valid_2 with "H◯ Hl_inv") as %[Hincl Hvalid]%auth_both_valid_discrete.
iPureIntro.
move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
......@@ -150,7 +150,7 @@ Section inv_heap.
I', h !! l = Some (v, I') w, I w I' w .
Proof.
iIntros "Hl_inv H●".
iDestruct (own_valid_2 with "H● Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
iDestruct (own_valid_2 with "H● Hl_inv") as %[Hincl Hvalid]%auth_both_valid_discrete.
iPureIntro.
move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
......
......@@ -163,7 +163,7 @@ Section proph_map.
Proof.
iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid.
iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid_discrete.
assert (vs = v :: proph_list_resolves pvs p) as ->.
{ rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
iMod (own_update_2 with "H● Hp") as "[H● H◯]".
......
......@@ -37,7 +37,7 @@ Section mono_proof.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc ( (MaxNat O) (MaxNat O))) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
first by apply auth_both_valid_discrete.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0. by iFrame. }
iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
......@@ -54,7 +54,7 @@ Section mono_proof.
iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%max_nat_included _]%auth_both_valid.
as %[?%max_nat_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
......@@ -76,7 +76,7 @@ Section mono_proof.
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%max_nat_included _]%auth_both_valid.
as %[?%max_nat_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. }
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
......@@ -116,7 +116,7 @@ Section contrib_spec.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (F O F 0)) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
first by apply auth_both_valid_discrete.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0. by iFrame. }
iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
......
......@@ -86,7 +86,7 @@ Section proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
iMod (own_alloc ( (Excl' 0, GSet ) (Excl' 0, GSet ))) as (γ) "[Hγ Hγ']".
{ by apply auth_both_valid. }
{ by apply auth_both_valid_discrete. }
iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0, 0. iFrame. iLeft. by iFrame. }
......@@ -151,14 +151,14 @@ Section proof.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
iModIntro. iSplitL "Hlo Hln Hauth Haown".
{ iNext. iExists o, n. by iFrame. }
wp_pures.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
iApply wp_fupd. wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
iDestruct "Haown" as "[[Hγo' _]|Haown]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
......
......@@ -69,14 +69,14 @@ Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
iIntros (? κs).
iMod (own_alloc (E σ1 E σ1)) as (γσ) "[Hσ Hσf]";
first by apply auth_both_valid.
first by apply auth_both_valid_discrete.
iExists (λ σ κs' _, own γσ (E σ))%I, (λ _, True%I).
iFrame "Hσ".
iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
first by rewrite /ownP; iFrame.
iIntros "!> Hσ". iExists . iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
iDestruct (own_valid_2 with "Hσ Hσf")
as %[Hp%Excl_included _]%auth_both_valid; simplify_eq; auto.
as %[Hp%Excl_included _]%auth_both_valid_discrete; simplify_eq; auto.
Qed.
......@@ -91,7 +91,7 @@ Section lifting.
Proof.
iIntros "Hσ● Hσ◯". rewrite /ownP.
by iDestruct (own_valid_2 with "Hσ● Hσ◯")
as %[->%Excl_included _]%auth_both_valid.
as %[->%Excl_included _]%auth_both_valid_discrete.
Qed.
Lemma ownP_state_twice σ1 σ2 : ownP σ1 ownP σ2 False.
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
......
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