From 3c9fc16af13e23596779473c97215392625c8cb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 13:38:57 +0200
Subject: [PATCH] Style tweaks to rwlocks.

- Remove unneeded imports
- Remove double spaces and insert space before colons
- Shorten long lines
- Favor `(.. & .. & ..)` over nesting `[.. [.. ..]]`
- Use `injection` intro patterns
- Favor `%H` over `"%H"`
- Use `first by eauto` instead of `first eauto` since the latter does not fail if `eauto` fails
---
 iris_heap_lang/lib/rw_spin_lock.v | 165 +++++++++++++-----------------
 1 file changed, 73 insertions(+), 92 deletions(-)

diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
index f15555acb..adc93e629 100644
--- a/iris_heap_lang/lib/rw_spin_lock.v
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -1,8 +1,6 @@
-From stdpp Require Import numbers.
 From iris.algebra Require Import gmultiset.
 From iris.base_logic Require Import invariants.
 From iris.bi.lib Require Export fractional.
-From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
@@ -46,17 +44,17 @@ Section proof.
 
   Local Definition rw_state_inv (γ : gname) (l : loc) (Φ : Qp → iProp Σ) : iProp Σ :=
     ∃ z : Z, l ↦ #z ∗
-      (* We need *some* ghost state that allows us to establish a contradiction in
-         the left disjunct (where the lock is write-locked) when proving [release_reader_spec],
-         so we use a fraction of the empty authoritative reader set (the rest goes to [writer_locked].)
-         Any fraction would do, but the benefit of giving over half to [writer_locked]
-         (and keeping less than half here) is that we can prove [writer_locked_exclusive].
-      *)
+      (* We need *some* ghost state that allows us to establish a contradiction
+      in the left disjunct (where the lock is write-locked) when proving
+      [release_reader_spec], so we use a fraction of the empty authoritative
+      reader set (the rest goes to [writer_locked].) Any fraction would do, but
+      the benefit of giving over half to [writer_locked] (and keeping less than
+      half here) is that we can prove [writer_locked_exclusive]. *)
       (⌜(z = -1)%Z⌝ ∗ own γ (●{# 1/4} ∅)
       ∨ ⌜(0 ≤ z)%Z⌝ ∗ ∃ (q : Qp) (g : gmultiset Qp),
           own γ (● g) ∗
           ⌜size g = Z.to_nat z⌝ ∗
-          ⌜(set_fold Qp.add q g = 1)%Qp⌝ ∗
+          ⌜set_fold Qp.add q g = 1%Qp⌝ ∗
           Φ q
       ).
   Local Hint Extern 0 (environments.envs_entails _ (rw_state_inv _ _ _)) =>
@@ -76,20 +74,21 @@ Section proof.
   Local Definition reader_locked (γ : gname) (q : Qp) : iProp Σ := own γ (◯ {[+ q +]}).
 
   Local Definition writer_locked (γ : gname) : iProp Σ := own γ (● {# 3/4} ∅).
-  Local Lemma writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False.
+
+  Local Lemma writer_locked_exclusive γ :
+    writer_locked γ -∗ writer_locked γ -∗ False.
   Proof.
-    iIntros "H1 H2". iCombine "H1 H2" gives "%Hvalid". exfalso.
+    iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
     rewrite
       auth_auth_dfrac_op_valid
       dfrac_op_own
       dfrac_valid_own in Hvalid.
-    destruct Hvalid as [Htoomuch _].
-    contradict Htoomuch.
-    auto.
+    by destruct Hvalid as [? _].
   Qed.
-  Local Lemma writer_locked_not_reader_locked γ q : writer_locked γ -∗ reader_locked γ q -∗ False.
+  Local Lemma writer_locked_not_reader_locked γ q :
+    writer_locked γ -∗ reader_locked γ q -∗ False.
   Proof.
-    iIntros "H1 H2". iCombine "H1 H2" gives "%Hvalid". exfalso.
+    iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
     apply auth_both_dfrac_valid in Hvalid as (_ & Hvalid & _).
     generalize (Hvalid 0)=> /cmra_discrete_included_r /gmultiset_included /(_ q).
     rewrite multiplicity_empty multiplicity_singleton. by lia.
@@ -99,24 +98,23 @@ Section proof.
     is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ.
   Proof.
     iIntros "[#HΦdup [%l [-> #Hlockinv]]] #Hiff".
-    unfold is_rw_lock.
     iSplitR.
-    { iApply (internal_fractional_iff with "Hiff HΦdup").  }
+    { iApply (internal_fractional_iff with "Hiff HΦdup"). }
     iExists l; iSplitR; first done.
     iApply (inv_iff with "[Hlockinv Hiff //]"); iIntros "!> !>".
     iDestruct "Hiff" as "#Hiff".
     iClear "HΦdup Hlockinv".
     iSplit.
-    - iIntros "[%z [? Hstate]]". iExists z. iFrame.
-      iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
+    - iIntros "(%z & ? & Hstate)". iExists z. iFrame.
+      iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
       + iFrame.
       + iRight.
         iFrame.
         iExists _, _.
         iFrame.
         by iApply "Hiff".
-    - iIntros "[%z [? Hstate]]". iExists z. iFrame.
-      iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
+    - iIntros "(%z & ? & Hstate)". iExists z. iFrame.
+      iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
       + iFrame.
       + iRight.
         iFrame.
@@ -139,12 +137,12 @@ Section proof.
     own γ (● { dq } g) ∗ own γ (◯ ({[+ v +]})) ⊢ ⌜v ∈ g⌝.
   Proof.
     iIntros "[Hauth Hfrag]".
-    iCombine "Hauth Hfrag" gives "%Hvalid".
+    iCombine "Hauth Hfrag" gives %Hvalid.
     iPureIntro.
     apply (auth_valid_gmultiset_singleton _ _ _ Hvalid).
   Qed.
 
-  Local Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1}:
+  Local Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
     {{{ P }}}
       newlock #()
     {{{ lk γ, RET lk; is_rw_lock γ lk Φ }}}.
@@ -152,89 +150,82 @@ Section proof.
     iIntros (φ) "HΦ Hφ".
     wp_lam.
     iMod (own_alloc (● ∅)) as (γ) "Hγ".
-    { apply auth_auth_valid; done.  }
+    { apply auth_auth_valid; done. }
     wp_alloc l as "Hl".
     iMod (inv_alloc N _ (rw_state_inv γ l Φ) with "[-Hφ]") as "#?".
     { rewrite [P]as_fractional.
-      eauto 10 with iFrame.
-    }
+      eauto 10 with iFrame. }
     iApply "Hφ".
     iSplitR.
     { iApply fractional_internal_fractional.
-      apply (as_fractional_fractional (P:=P)).
-    }
+      apply (as_fractional_fractional (P:=P)). }
     eauto 10.
   Qed.
 
-  Local Lemma try_acquire_reader_spec γ lk Φ:
+  Local Lemma try_acquire_reader_spec γ lk Φ :
     {{{ is_rw_lock γ lk Φ }}}
       try_acquire_reader lk
-    {{{ b, RET #b; if b is true then ∃ q, reader_locked γ q ∗ Φ q else True  }}}.
+    {{{ (b : bool), RET #b; if b then ∃ q, reader_locked γ q ∗ Φ q else True }}}.
   Proof.
-    iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
+    iIntros (φ) "[#HΦdup (%l & -> & #Hlockinv)] Hφ".
     wp_lam.
     wp_bind (!_)%E.
     iInv "Hlockinv" as (z) "[> Hl Hz]".
     wp_load.
-    iSplitL "Hl Hz"; first eauto with iFrame.
+    iSplitL "Hl Hz"; first by eauto with iFrame.
     iModIntro.
     wp_pures.
     destruct (Z.le_dec 0%Z z) as [Hle|?]; last first.
     { rewrite bool_decide_false //.
       wp_pures.
       iApply "Hφ".
-      done.
-    }
+      done. }
     rewrite bool_decide_true //.
     wp_pures.
     wp_bind (CmpXchg _ _ _).
     iInv "Hlockinv" as (z') "[> Hl Hz]".
-    wp_cmpxchg as Heq|?; last first.
+    wp_cmpxchg as [= ->]|?; last first.
     { iSplitR "Hφ".
-      { eauto with iFrame.  }
+      { eauto with iFrame. }
       iModIntro.
       wp_pures.
-      by iApply "Hφ".
-    }
-    injection Heq as ->.
-    iDestruct "Hz" as "[[-> _]|[Hz_ge_0 [%q [%g Hg]]]]"; first contradiction.
+      by iApply "Hφ". }
+    iDestruct "Hz" as "[[-> _]|(Hz_ge_0 & %q & %g & Hg)]"; first done.
     iDestruct "Hg" as "(Hauth & %Hsize & %Hfold & HΦ)".
     rewrite -[q in Φ q]Qp.div_2.
     iDestruct ("HΦdup" $! (q / 2)%Qp (q / 2)%Qp with "HΦ") as "[HΦ HΦgive]".
-    iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅ ◯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
+    iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅
+      â—¯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
     { apply auth_update_alloc.
       rewrite -{2}[({[+ (q / 2)%Qp+]})]gmultiset_disj_union_left_id.
-      apply gmultiset_local_update_alloc.
-    }
+      apply gmultiset_local_update_alloc. }
     iSplitR "HΦgive Hview Hφ".
     { iExists (z + 1)%Z.
       iModIntro.
       iModIntro.
       iFrame.
       iRight.
-      iSplitL "Hz_ge_0"; first eauto with lia.
+      iSplitL "Hz_ge_0"; first by eauto with lia.
       iExists _, _.
       iFrame.
       iSplit.
       { iPureIntro.
         rewrite gmultiset_size_disj_union gmultiset_size_singleton.
-        lia.
-      }
+        lia. }
       iPureIntro.
       rewrite
         gmultiset_set_fold_disj_union
         gmultiset_set_fold_singleton
         -gmultiset_set_fold_comm_acc.
         { rewrite Qp.div_2 //. }
-        intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //.
-    }
+        intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //. }
     iModIntro.
     wp_pures.
     iApply "Hφ".
     eauto with iFrame.
   Qed.
 
-  Local Lemma acquire_reader_spec γ lk Φ:
+  Local Lemma acquire_reader_spec γ lk Φ :
     {{{ is_rw_lock γ lk Φ }}}
       acquire_reader lk
     {{{ q, RET #(); reader_locked γ q ∗ Φ q }}}.
@@ -253,101 +244,94 @@ Section proof.
       eauto.
   Qed.
 
-  Local Lemma release_reader_spec γ lk Φ q:
+  Local Lemma release_reader_spec γ lk Φ q :
     {{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
       release_reader lk
     {{{ RET #(); True }}}.
   Proof.
-    iIntros (φ) "([#HΦdup [%l [-> Hlockinv]]] & Hlocked & HΦ) Hφ".
+    iIntros (φ) "((#HΦdup & %l & -> & Hlockinv) & Hlocked & HΦ) Hφ".
     wp_lam.
     wp_bind (FAA _ _).
     iInv "Hlockinv" as (z) "[> Hl Hz]".
     wp_faa.
     unfold reader_locked.
-    iDestruct "Hz" as "[[_ Hempty]|[%Hz_ge_0 [%q' [%g (Hg & %Hsize & %Hsum & HΦq')]]]]".
+    iDestruct "Hz" as "[[_ Hempty]|(%Hz_ge_0 & %q' & %g & Hg & %Hsize & %Hsum & HΦq')]".
     { iExFalso.
-      iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
-      multiset_solver.
-    }
-    iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as "%".
-    { iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
+      iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
+      multiset_solver. }
+    iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as %?.
+    { iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
       iPureIntro.
       split; last assumption.
       apply Z2Nat.neq_0_pos.
       rewrite -Hsize gmultiset_size_empty_iff.
-      multiset_solver.
-    }
+      multiset_solver. }
     iCombine "Hg Hlocked" as "Hown".
     iMod (own_update _ _ (●(g ∖ {[+ q +]})) with "Hown") as "Hown".
     { apply auth_update_dealloc.
       replace ε with ({[+ q +]} ∖ {[+ q +]} : gmultiset Qp); last first.
-      { rewrite gmultiset_difference_diag //.  }
+      { rewrite gmultiset_difference_diag //. }
       apply gmultiset_local_update_dealloc.
-      multiset_solver.
-    }
+      multiset_solver. }
     iModIntro.
     iSplitR "Hφ".
     { iExists (z + -1)%Z.
       iFrame.
       iRight.
       iSplit.
-      { eauto with lia.  }
+      { eauto with lia. }
       iExists _, _.
-      iDestruct ("HΦdup" $! q q' with  "[HΦ HΦq']") as "HΦ"; first iFrame.
+      iDestruct ("HΦdup" $! q q' with "[$HΦ $HΦq']") as "HΦ".
       iModIntro.
       iFrame.
       iSplit.
       { iPureIntro.
         rewrite gmultiset_size_difference; last multiset_solver.
         rewrite gmultiset_size_singleton.
-        lia.
-      }
+        lia. }
       iPureIntro.
       rewrite -Hsum gmultiset_set_fold_comm_acc; last first.
-       { intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
+      { intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
       rewrite
         -gmultiset_set_fold_singleton
         -gmultiset_set_fold_disj_union
         gmultiset_disj_union_comm
         -gmultiset_disj_union_difference //.
-      multiset_solver.
-    }
+      multiset_solver. }
     wp_pures.
     by iApply "Hφ".
   Qed.
 
-  Local Lemma try_acquire_writer_spec γ lk Φ:
+  Local Lemma try_acquire_writer_spec γ lk Φ :
     {{{ is_rw_lock γ lk Φ }}}
       try_acquire_writer lk
-    {{{ b, RET #b; if b is true then writer_locked γ ∗ Φ 1%Qp else True }}}.
+    {{{ (b : bool), RET #b; if b then writer_locked γ ∗ Φ 1%Qp else True }}}.
   Proof.
-    iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
+    iIntros (φ) "(#HΦdup & %l & -> & #Hlockinv) Hφ".
     wp_lam.
     wp_bind (CmpXchg _ _ _).
     iInv ("Hlockinv") as (z) "[> Hl Hz]".
-    wp_cmpxchg as Heq|?; last first.
+    wp_cmpxchg as [= ->]|?; last first.
     { iModIntro.
       iSplitL "Hl Hz".
-      { eauto with iFrame.  }
+      { eauto with iFrame. }
       wp_pures.
-      by iApply "Hφ".
-    }
-    injection Heq as ->.
-    iDestruct "Hz" as "[[%H0_eq_1 ?]|[_ [%q [%g (Hg & %Hsize & %Hfold & HΦ)]]]]".
-    { iExFalso.  by contradict H0_eq_1.  }
-    apply gmultiset_size_empty_inv in Hsize. subst g.
+      by iApply "Hφ". }
+    iDestruct "Hz" as "[[%H0_eq_1 ?]|(_ & %q & %g & Hg & %Hsize & %Hfold & HΦ)]".
+    { done. }
+    apply gmultiset_size_empty_inv in Hsize as ->.
     rewrite gmultiset_set_fold_empty in Hfold. subst q.
     rewrite -[in (●{# 1} _)]Qp.quarter_three_quarter.
     iDestruct "Hg" as "[Hg Hg_give]".
     iModIntro.
     iSplitL "Hl Hg".
-    { eauto 10 with iFrame.  }
+    { eauto 10 with iFrame. }
     wp_pures.
     iApply "Hφ".
     by iFrame.
   Qed.
 
-  Local Lemma acquire_writer_spec γ lk Φ:
+  Local Lemma acquire_writer_spec γ lk Φ :
     {{{ is_rw_lock γ lk Φ }}}
       acquire_writer lk
     {{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}}.
@@ -366,29 +350,26 @@ Section proof.
       eauto.
   Qed.
 
-  Local Lemma release_writer_spec γ lk Φ:
+  Local Lemma release_writer_spec γ lk Φ :
     {{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
       release_writer lk
     {{{ RET #(); True }}}.
   Proof.
-    iIntros (φ) "([#HΦdup [%l [-> #Hlockinv]]] & Hlocked & HΦ) Hφ".
+    iIntros (φ) "((#HΦdup & %l & -> & #Hlockinv) & Hlocked & HΦ) Hφ".
     wp_lam.
     iInv ("Hlockinv") as (z) "[> Hl Hz]".
     wp_store.
-    iDestruct "Hz" as "[[? Hg]|[_ [% [% [Hg_owned _]]]]]"; last first.
+    iDestruct "Hz" as "[[? Hg]|(_ & % & % & Hg_owned & _)]"; last first.
     { iExFalso.
-      iCombine "Hg_owned Hlocked" gives "%Hvalid".
+      iCombine "Hg_owned Hlocked" gives %Hvalid.
       rewrite
         auth_auth_dfrac_op_valid
         dfrac_op_own
         dfrac_valid_own in Hvalid.
-      destruct Hvalid as [Htoomuch _].
-      contradict Htoomuch.
-      auto.
-    }
+      by destruct Hvalid as [? _]. }
     iCombine "Hg Hlocked" as "Hown".
     rewrite Qp.quarter_three_quarter.
-    iSplitR "Hφ"; first eauto 15 with iFrame.
+    iSplitR "Hφ"; first by eauto 15 with iFrame.
     by iApply "Hφ".
   Qed.
 End proof.
-- 
GitLab