Add doc and other minor fixes

atomic.v

+(* Logically atomic triple *)
+
 From iris.program_logic Require Export hoare weakestpre pviewshifts.
 From iris.prelude Require Export coPset.
 Import uPred.
@@ -6,9 +8,9 @@ Section atomic.
   Context `{irisG Λ Σ} (A: Type).
 
   Definition atomic_triple_base
-             (α: A → iProp Σ)
-             (β: A → val _ → iProp Σ)
-             (Ei Eo: coPset)
+             (α: A → iProp Σ) (* atomic pre-condition *)
+             (β: A → val _ → iProp Σ) (* atomic post-condition *)
+             (Ei Eo: coPset) (* inside/outside masks *)
              (e: expr _) P Q : iProp Σ :=
     ((P ={Eo, Ei}=> ∃ x:A,
                        α x ★

evmap.v

-(* evmap.v -- generalized heap-like monoid *)
+(* evmap.v -- generalized heap-like monoid composite *)
 From iris.program_logic Require Export invariants weakestpre.
 From iris.algebra Require Export auth frac gmap dec_agree.
 From iris.proofmode Require Import tactics.
 
 Section evmap.
-  Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A(* , CMRADiscrete Q *)}.
+  Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
   Definition evkR := prodR Q (dec_agreeR A).
   Definition evmapR := gmapUR K evkR.
   Definition evidenceR := authR evmapR.
@@ -14,6 +14,7 @@ Section evmap.
   Instance subG_evidenceΣ {Σ} : subG evidenceΣ Σ → evidenceG Σ.
   Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
+  (* Some basic supporting lemmas *)
   Lemma map_agree_eq m m' (hd: K) (p q: Q) (x y: A):
     m !! hd = Some (p, DecAgree y) →
     m = {[hd := (q, DecAgree x)]} ⋅ m' → x = y.
@@ -48,6 +49,7 @@ Section evmapR.
   Context (K A: Type) `{Countable K, EqDecision A}.
   Context `{!inG Σ (authR (evmapR K A unitR))}.
 
+  (* Evidence that k immutably maps to some fixed v *)
   Definition ev γm (k : K) (v: A) := own γm (◯ {[ k := ((), DecAgree v) ]})%I.
 
   Global Instance persistent_ev γm k v : PersistentP (ev γm k v).
@@ -91,6 +93,17 @@ Section evmapR.
       exfalso. subst. rewrite H0 in H1.
       by destruct H1 as [? ?].
   Qed.
+
+  Lemma ev_map_witness γm m hd x:
+    ev γm hd x ★ own γm (● m) ⊢ m !! hd = Some (∅, DecAgree x).
+  Proof.
+    iIntros "[#Hev Hom]".
+    destruct (m !! hd) as [[[] agy]|] eqn:Heqn.
+    - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame.
+      by subst.
+    - iExFalso. iApply map_agree_none'=>//.
+      by iFrame.
+  Qed.
   
   Lemma evmap_frag_agree_split γm p q1 q2 (a1 a2: A):
     own γm (◯ {[p := (q1, DecAgree a1)]}) ★
@@ -111,4 +124,3 @@ Section evmapR.
       apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
   Qed.
 End evmapR.
-

flat.v

@@ -345,8 +345,8 @@ Section proof.
     - iDestruct (big_sepM_delete_later _ m with "HRs") as "[Hp Hrs]"=>//.
       iDestruct "Hp" as (?) "[>% [Hpr ?]]"; subst.
       iDestruct "Hpr" as (ts' p') "(>% & >Hp' & Hp)".
-      subst. iDestruct (map_agree_eq' _ _ γs m with "[Hom Hhd]") as %H=>//; first iFrame.
-      inversion H. subst.
+      subst. iDestruct (ev_map_witness _ _ _ m with "[Hom Hhd]") as %H=>//; first iFrame.
+      rewrite Heqn in H. inversion H. subst.
       iDestruct (evmap_frag_agree_split with "[Hp']") as "%"; first iFrame "Hev Hp'". subst.
       destruct ts' as [[[[γx γ1] γ3] γ4] γq].
       iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
@@ -356,32 +356,32 @@ Section proof.
         wp_load. iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
         { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
           iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
-          iFrame. iExists #p'. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p'.
+          iFrame. iExists #p. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p.
           iSplitR; first auto. iFrame.
           iRight. iLeft. iExists f, x. iFrame. }
         iVsIntro. wp_match.
         wp_bind (try_srv _ _). iApply try_srv_spec=>//.
         iFrame "#". wp_seq.
-        iAssert (∃ hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
+        iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
         by iApply ("IH" with "Ho3 Hhd").
       + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
         wp_load.
         iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
         { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
           iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
-          iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
+          iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
           iSplitR; first auto. iFrame.
           iRight. iRight. iLeft. iExists f, x. iFrame. }
         iVsIntro. wp_match.
         wp_bind (try_srv _ _). iApply try_srv_spec=>//.
         iFrame "#". wp_seq.
-        iAssert (∃ hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
+        iAssert (∃ hd, evs γs hd #p)%I with "[Hhd]" as "Hhd"; eauto.
         by iApply ("IH" with "Ho3 Hhd").
        + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
           wp_load. iVs ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
           { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
             iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
-            iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
+            iFrame. iExists #p. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p.
             iSplitR; first auto. iFrame.
             iLeft. iExists y. iFrame. }
           iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.

peritem.v

@@ -197,13 +197,10 @@ Lemma new_stack_spec' Φ RI:
     - destruct (decide (x = x')) as [->|Hneq].
       + iIntros (hd _) "(HR & Hom & Hxs)".
         simpl. iDestruct "Hxs" as (hd' q) "[Hhd [#Hev Hxs']]".
-        rewrite /ev. destruct (m !! hd) as [[q' [x|]]|] eqn:Heqn.
-        * iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
-          iDestruct (map_agree_eq' _ _ _ m with "[Hom]") as %H'=>//; first iFrame=>//.
-          subst. iExists hd. inversion H'. subst. destruct q'. by iFrame.
-        * iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
-          iDestruct (map_agree_eq' _ _ _ m with "[Hom]") as "%"=>//; first iFrame=>//.
-        * iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame=>//.
+        rewrite /evs.
+        iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
+        iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
+        iExists hd. by iFrame.
       + iIntros (hd ?).
         assert (x ∈ xs'); first set_solver.
         iIntros "(HRs & Hom & Hxs')".