Add some comments

theories/examples/graph/graph.v

@@ -25,13 +25,14 @@ Definition pair_in_set `{Countable A} (Ps : gset (A * A)) (S : gset A) : Prop
 Definition pair_in_bound (Ps : gset (event_id * event_id)) (n : event_id) : Prop
   := set_Forall (λ p, p.1 < n ∧ p.2 < n)%nat Ps.
 
+(* We don't need so ⊆ (po ∪ com)+ because we don't have po. The view inclusion
+  relation includes po, among other relations. *)
 Record graph {A : Type} := mkGraph {
   Es  : event_list A;
   com : gset (event_id * event_id) ;
   so  : gset (event_id * event_id) ;
   gcons_com_included_dec : bool_decide (pair_in_bound com (length Es));
   gcons_so_included_dec  : bool_decide (pair_in_bound so (length Es)) ;
-  (* TODO: so ⊆ (po ∪ com)+ ? *)
 }.
 
 Global Arguments graph : clear implicits.

theories/examples/queue/proof_per_elem_graph.v

@@ -57,6 +57,7 @@ Definition QueuePerElem γg : vProp :=
   ∃ G M, msq.(QueueLocal) (N .@ "que") γg q G M ∗
          inv (N .@ "iinv") (QueuePerElemInv γg).
 
+(* TODO: we can prove logically-atomic spec here. *)
 Lemma per_elem_enqueue (DISJ: N ## histN) γg (x: Z) tid (NZ: 0 < x) :
   {{{ QueuePerElem γg ∗ ▷ P x}}}
       msq.(enqueue) [ #q; #x] @ tid; ⊤