Commit d9d7e576 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent a9ed30a3
......@@ -27,41 +27,39 @@ Context {Σ : gFunctors} `{noprolG Σ, inG Σ (graphR qevent)}.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Variable N : namespace.
Hypothesis msq : weak_queue_spec Σ.
Variable P : Z vProp.
Variable q : loc.
Implicit Types (N : namespace) (P : Z vProp) (q : loc).
Definition queue_resources G : vProp :=
Definition queue_resources P G : vProp :=
([ set] eid filter (unmatched_enq_2 G) (to_set G.(Es)),
match G.(Es) !! eid with
| Some (mkGraphEvent (Enq v) V _) => @{V.(dv_in)} P v
| _ => emp (* this is impossible *)
end)%I.
Instance queue_resources_objective G : Objective (queue_resources G).
Instance queue_resources_objective P G : Objective (queue_resources P G).
Proof.
apply big_sepS_objective => e.
destruct (G.(Es) !! e) as [[ ge ??]|]; [|apply _].
destruct ge; apply _.
Qed.
Definition QueuePerElemInv γg : vProp :=
G, msq.(QueueInv) γg G queue_resources G.
Definition QueuePerElemInv P γg : vProp :=
G, msq.(QueueInv) γg G queue_resources P G.
Local Existing Instance QueueInv_Objective.
Instance QueuePerElemInv_objective γg : Objective (QueuePerElemInv γg) := _.
Instance QueuePerElemInv_objective P γg : Objective (QueuePerElemInv P γg) := _.
Definition QueuePerElem γg : vProp :=
Definition QueuePerElem N P γg q : vProp :=
G M, msq.(QueueLocal) (N .@ "que") γg q G M
inv (N .@ "iinv") (QueuePerElemInv γg).
inv (N .@ "iinv") (QueuePerElemInv P γ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}}}
Lemma per_elem_enqueue N P γg q (x: Z) tid (DISJ: N ## histN) (NZ: 0 < x) :
{{{ QueuePerElem N P γg q P x}}}
msq.(enqueue) [ #q; #x] @ tid;
{{{ RET #; QueuePerElem γg }}}.
{{{ RET #; QueuePerElem N P γg q }}}.
Proof.
iIntros (Φ) "[Queue P] Post".
iDestruct "Queue" as (G0 M0) "[Queue #QPI]".
......@@ -86,7 +84,7 @@ Proof.
{ by rewrite EsG' Eqenq lookup_app_1_eq. }
iIntros "!>".
iAssert ( queue_resources G')%I with "[P Elems]" as "Elems'".
iAssert ( queue_resources P G')%I with "[P Elems]" as "Elems'".
{ iNext. rewrite /queue_resources.
have UMe : unmatched_enq_2 G' enqId.
{ split.
......@@ -123,10 +121,10 @@ Proof.
iExists _, _. by iFrame.
Qed.
Lemma per_elem_dequeue (DISJ: N ## histN) γg tid :
{{{ QueuePerElem γg }}}
Lemma per_elem_dequeue N P γg q tid (DISJ: N ## histN) :
{{{ QueuePerElem N P γg q }}}
msq.(dequeue) [ #q] @ tid;
{{{ (x: Z), RET #x; QueuePerElem γg (x = 0 P x) }}}.
{{{ (x: Z), RET #x; QueuePerElem N P γg q (x = 0 P x) }}}.
Proof.
iIntros (Φ) "QI Post". iDestruct "QI" as (G0 M0) "[Queue #QPI]".
iApply (wp_step_fupd _ _ _ ( _, _- _)%I with "[$Post]"); [auto..|].
......@@ -190,7 +188,7 @@ Proof.
have EqEm' : G'.(Es) !! enqId = Some (mkGraphEvent (Enq x) Venq Menq).
{ rewrite EsG' lookup_app_1_ne; [done|by rewrite -Eqdeq]. }
iAssert ( (@{Venq.(dv_in)} P x queue_resources G'))%I
iAssert ( (@{Venq.(dv_in)} P x queue_resources P G'))%I
with "[Elems]" as "[Px Elems]".
{ iNext. rewrite /queue_resources.
rewrite (_: (@{Venq.(dv_in)} P x)%I
......@@ -260,19 +258,19 @@ From gpfsl.examples.queue Require Import code_ms proof_ms_graph.
(* TODO: use ther spec_per_elem one. Need try_enq and try_deq *)
Section RSL_instance.
Context {Σ : gFunctors} `{noprolG Σ, !msqueueG Σ, !atomicG Σ}.
Context (P : lit vProp Σ) (q: loc).
Let is_queue N := QueuePerElem N (msqueue_impl_weak Σ).
Let is_queue := QueuePerElem (msqueue_impl_weak Σ).
Lemma per_elem_enqueue_inst N (DISJ: N ## histN) γg (x: Z) tid (NZ: (0 < x)%Z) :
{{{ is_queue N P q γg P x }}}
Lemma per_elem_enqueue_inst N P γg q (x: Z) tid
(NZ: (0 < x)%Z) (DISJ: N ## histN) :
{{{ is_queue N P γg q P x }}}
enqueue [ #q ; #x] @ tid;
{{{ RET #; is_queue N P q γg }}}.
{{{ RET #; is_queue N P γg q }}}.
Proof. by apply : per_elem_enqueue. Qed.
Lemma per_elem_dequeue_inst N (DISJ: N ## histN) γg tid :
{{{ is_queue N P q γg }}}
Lemma per_elem_dequeue_inst N P γg q tid (DISJ: N ## histN) :
{{{ is_queue N P γg q }}}
dequeue [ #q] @ tid;
{{{ (x: Z), RET #x; is_queue N P q γg (x = 0 P x) }}}.
{{{ (x: Z), RET #x; is_queue N P γg q (x = 0 P x) }}}.
Proof. by apply : per_elem_dequeue. Qed.
End RSL_instance.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment