Make authoritative part of auth fractional

CHANGELOG.md

@@ -112,6 +112,13 @@ Changes in Coq:
   `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
   smarter to no longer unfold lambdas/recs that occur behind definitions.
 * Export the fact that `iPreProp` is a COFE.
+* The CMRA `auth` now can have fractional authoritative parts. So now `auth` has
+  3 types of elements: the fractional authoritative `●{q} a`, the full
+  authoritative `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are
+  only possible with the full authoritative element `● a`, while fractional
+  authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a
+  consequence, `auth` is no longer a COFE and does not preserve Leibniz
+  equality.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/algebra/agree.v

@@ -28,7 +28,8 @@ Proof.
 
 (** Note that the projection [agree_car] is not non-expansive, so it cannot be
 used in the logic. If you need to get a witness out, you should use the
-lemma [to_agree_uninjN] instead. *)
+lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
+internally in this file.  *)
 Record agree (A : Type) : Type := {
   agree_car : list A;
   agree_not_nil : bool_decide (agree_car = []) = false

theories/algebra/frac_auth.v

@@ -2,6 +2,13 @@ From iris.algebra Require Export frac auth.
 From iris.algebra Require Export updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 
+(** Authoritative CMRA where the NON-authoritative parts can be fractional.
+  This CMRA allows the original non-authoritative element `◯ a` to be split into
+  fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
+  using the original `◯ a`. Currently, however, this CMRA hides the ability to
+  split the authoritative part into fractions.
+*)
+
 Definition frac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR fracR A)).
 Definition frac_authUR (A : cmraT) : ucmraT :=
@@ -35,18 +42,18 @@ Section frac_auth.
   Proof. solve_proper. Qed.
 
   Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (●! a).
-  Proof. intros; apply Auth_discrete; apply _. Qed.
+  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
   Global Instance frac_auth_frag_discrete a : Discrete a → Discrete (◯! a).
-  Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
+  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
 
   Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a).
-  Proof. done. Qed.
+  Proof. by rewrite auth_both_validN. Qed.
   Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a).
-  Proof. done. Qed.
+  Proof. intros. by apply auth_both_valid. Qed.
 
   Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b.
   Proof.
-    rewrite auth_validN_eq /= => -[Hincl Hvalid].
+    rewrite auth_both_validN /= => -[Hincl Hvalid].
     by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
   Qed.
   Lemma frac_auth_agree a b : ✓ (●! a ⋅ ◯! b) → a ≡ b.
@@ -57,10 +64,10 @@ Section frac_auth.
   Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●! a ⋅ ◯!{q} b) → Some b ≼{n} Some a.
-  Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
+  Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
   Lemma frac_auth_included `{CmraDiscrete A} q a b :
     ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a.
-  Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
+  Proof. by rewrite auth_valid_discrete_2 /= => -[/Some_pair_included [_ ?] _]. Qed.
   Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
     ✓{n} (●! a ⋅ ◯!{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
@@ -70,8 +77,8 @@ Section frac_auth.
 
   Lemma frac_auth_auth_validN n a : ✓{n} (●! a) ↔ ✓{n} a.
   Proof.
-    split; [by intros [_ [??]]|].
-    by repeat split; simpl; auto using ucmra_unit_leastN.
+    rewrite auth_auth_frac_validN Some_validN. split.
+    by intros [?[]]. intros. by split.
   Qed.
   Lemma frac_auth_auth_valid a : ✓ (●! a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.

theories/base_logic/lib/auth.v

@@ -94,7 +94,7 @@ Section auth.
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
-  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
+  Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
   Global Instance auth_own_sep_homomorphism γ :
     WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ).
   Proof. split; try apply _. apply auth_own_op. Qed.
@@ -107,8 +107,8 @@ Section auth.
     ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌝ ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
-    iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
-    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
+      [done|by apply auth_valid_discrete_2|].
     iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
     { iNext. rewrite /auth_inv. iExists t. by iFrame. }
     eauto.

theories/base_logic/lib/boxes.v

 From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import auth gmap agree.
+From iris.algebra Require Import excl auth gmap agree.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
+  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete_2.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
@@ -110,7 +110,7 @@ Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
-    as (γ) "[Hdom Hγ]"; first done.
+    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_valid_discrete_2|]).
   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

@@ -76,7 +76,7 @@ Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+  { rewrite -auth_auth_valid. exact: to_gen_heap_valid. }
   iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
 Qed.
 
@@ -105,7 +105,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+    f_equiv. rewrite -auth_frag_valid op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
@@ -122,8 +122,8 @@ Section gen_heap.
 
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
   Proof.
-    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
-    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
+    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
+    by apply pure_mono=> /singleton_valid [??].
   Qed.
   Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
   Proof.

theories/base_logic/lib/proph_map.v

-From iris.algebra Require Import auth list gmap.
+From iris.algebra Require Import auth excl list gmap.
 From iris.base_logic.lib Require Export own.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -111,7 +111,7 @@ Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
 Proof.
   iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { apply: auth_auth_valid. exact: to_proph_map_valid. }
+  { rewrite -auth_auth_valid. exact: to_proph_map_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. split =>//.
 Qed.

theories/base_logic/lib/wsat.v

@@ -110,10 +110,10 @@ Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
-  rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
+  rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
   iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
-  rewrite left_id_L lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+  rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
   case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
   iExists Q; iSplit; first done.
   iAssert (invariant_unfold Q ≡ invariant_unfold P)%I as "?".
@@ -197,7 +197,8 @@ End wsat.
 Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
-  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
+  iMod (own_alloc (● (∅ : gmap positive _))) as (γI) "HI";
+    first by rewrite -auth_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ γI γE γD).

theories/heap_lang/lib/counter.v

@@ -36,7 +36,8 @@ Section mono_proof.
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
+      first by apply auth_valid_discrete_2.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
@@ -113,7 +114,8 @@ Section contrib_spec.
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']";
+      first by apply auth_valid_discrete_2.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.

theories/heap_lang/lib/ticket_lock.v

@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import auth gset.
+From iris.algebra Require Import excl auth gset.
 From iris.heap_lang.lib Require Export lock.
 Set Default Proof Using "Type".
 Import uPred.
@@ -76,7 +76,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%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by rewrite -auth_both_op. }
+    { by apply auth_valid_discrete_2. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }

theories/program_logic/ownp.v

 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
-From iris.algebra Require Import auth.
+From iris.algebra Require Import excl auth.
 From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 
@@ -53,7 +53,8 @@ Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (? κs).
-  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done.
+  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
+    first by apply auth_valid_discrete_2.
   iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I.
   iFrame "Hσ".
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
@@ -68,7 +69,8 @@ Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
 Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
-  iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
+  iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
+    first by apply auth_valid_discrete_2.
   iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";