Merge branch 'ralf/auth-valid' into 'master'

Strengthen auth_both_valid and auth_both_frac_valid

See merge request iris/iris!520

CHANGELOG.md

@@ -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
 ```
 

theories/algebra/auth.v

@@ -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.

theories/algebra/lib/frac_auth.v

@@ -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.

theories/algebra/lib/ufrac_auth.v

@@ -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.

theories/base_logic/lib/auth.v

@@ -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. }

theories/base_logic/lib/boxes.v

@@ -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".

theories/base_logic/lib/gen_heap.v

@@ -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 _)))=> //.

theories/base_logic/lib/gen_inv_heap.v

@@ -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).

theories/base_logic/lib/proph_map.v

@@ -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◯]".

theories/heap_lang/lib/counter.v

@@ -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.

theories/heap_lang/lib/ticket_lock.v

@@ -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]".

theories/program_logic/ownp.v

@@ -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.