From 7ae12caf115df1051062ab2e91f6137c424e7d7b Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Wed, 19 Oct 2016 22:04:17 +0800
Subject: [PATCH] More docs

---
 atomic_sync.v | 14 +++++---------
 flat.v        |  2 ++
 misc.v        | 28 +++-------------------------
 simple_sync.v |  5 +++--
 sync.v        |  2 ++
 5 files changed, 15 insertions(+), 36 deletions(-)

diff --git a/atomic_sync.v b/atomic_sync.v
index 61236f4..61b3f8d 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -1,11 +1,10 @@
 From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
 From iris_atomic Require Import atomic sync misc.
 
-Definition syncR := prodR fracR (dec_agreeR val).
+Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
@@ -40,7 +39,7 @@ Section atomic_sync.
                                (∀ (v: val) (g': A),
                                   ϕ l g' -★ β x g g' v ={E}=★ Φ v)
                                ⊢ WP f' x @ E {{ Φ }} )}}.
-  (* XXX (zhen): The linear VS in the above post-condition is for the final step
+  (* The linear view shift in the above post-condition is for the final step
      of computation. The client side of such triple will have to prove that the
      specific post-condition he wants can be lvs'd from whatever threaded together
      by magic wands. The library side, when proving seq_spec, will always have
@@ -69,9 +68,7 @@ Section atomic_sync.
     iIntros (f') "#Hsynced".
     iExists γ. iFrame.
     iIntros (x). iAlways.
-    rewrite /atomic_triple'.
     iIntros (P Q) "#Hvss".
-    rewrite /synced.
     iSpecialize ("Hsynced" $! P Q x).
     iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
@@ -92,9 +89,8 @@ Section atomic_sync.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
       iVs ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iVsIntro. iSplitL "Hg2 HÏ•'".
-      * iExists g'. by iFrame.
-      * done.
+      iVsIntro. iSplitL "Hg2 HÏ•'"; last done.
+      iExists g'. by iFrame.
     - iIntros (?) "?". by iExists g0.
   Qed.
 
diff --git a/flat.v b/flat.v
index 4213ca6..3753263 100644
--- a/flat.v
+++ b/flat.v
@@ -1,3 +1,5 @@
+(* Flat Combiner *)
+
 From iris.program_logic Require Export weakestpre saved_prop.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/misc.v b/misc.v
index f916c49..3b3d2f2 100644
--- a/misc.v
+++ b/misc.v
@@ -1,35 +1,13 @@
+(* Miscellaneous lemmas *)
+
 From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import auth frac gmap dec_agree upred_big_op.
 From iris.prelude Require Import countable.
 From iris.program_logic Require Import auth.
 Import uPred.
 
 Section lemmas.
-  Lemma op_some: ∀ {A: cmraT} (a b: A), Some a ⋅ Some b = Some (a ⋅ b).
-  Proof. done. Qed.
-
-  Lemma invalid_plus: ∀ (q: Qp), ¬ ✓ (1 + q)%Qp.
-  Proof.
-    intros q H.
-    apply (Qp_not_plus_q_ge_1 q).
-    done.
-  Qed.
-
-  Lemma pair_l_frac_update (g g': val):
-    ((1 / 2)%Qp, DecAgree g) â‹… ((1 / 2)%Qp, DecAgree g) ~~> ((1 / 2)%Qp, DecAgree g') â‹… ((1 / 2)%Qp, DecAgree g').
-  Proof.
-    repeat rewrite pair_op dec_agree_idemp.
-    rewrite frac_op' Qp_div_2.
-    eapply cmra_update_exclusive.
-    done.
-  Qed.
-  
-  Lemma pair_l_frac_op (p q: Qp) (g g': val):
-    (((p, DecAgree g') â‹… (q, DecAgree g'))) ~~> ((p + q)%Qp, DecAgree g').
-  Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
-
   Lemma pair_l_frac_op' (p q: Qp) (g g': val):
      ((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') â‹… (q, DecAgree g'))).
   Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
diff --git a/simple_sync.v b/simple_sync.v
index 1192770..861e678 100644
--- a/simple_sync.v
+++ b/simple_sync.v
@@ -1,6 +1,7 @@
+(* Coarse-grained syncer *)
+
 From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
 From iris_atomic Require Import sync.
diff --git a/sync.v b/sync.v
index 7e82142..23cf715 100644
--- a/sync.v
+++ b/sync.v
@@ -1,3 +1,5 @@
+(* Syncer spec *)
+
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-- 
GitLab