From cee441f9c019a1c3d21740f7822c663e459d7440 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 7 Oct 2021 12:09:17 +0200
Subject: [PATCH] Add some comments
---
theories/examples/graph/graph.v | 3 ++-
theories/examples/queue/proof_per_elem_graph.v | 1 +
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/theories/examples/graph/graph.v b/theories/examples/graph/graph.v
index f179212b..8e5ff9c1 100644
--- a/theories/examples/graph/graph.v
+++ b/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.
diff --git a/theories/examples/queue/proof_per_elem_graph.v b/theories/examples/queue/proof_per_elem_graph.v
index 651e05e4..2bdac0e1 100644
--- a/theories/examples/queue/proof_per_elem_graph.v
+++ b/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; ⊤
--
GitLab