Commit 467cf3a7 authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

prove spec_abs with spec_abs_graph

parent 99396012
......@@ -158,6 +158,7 @@ theories/examples/queue/spec_abs.v
theories/examples/queue/spec_abs_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_abs_graph_abs.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
......
From gpfsl.logic Require Import logatom proofmode.
From gpfsl.examples.queue Require Export event spec_abs_graph spec_abs.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Section abs_graph.
Context `{!noprolG Σ, !inG Σ (graphR qevent)}.
Context (sq : spec_abs_graph.strong_queue_spec Σ).
Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
Definition isQueue N γq q : vProp Σ := γa γg,
γq = encode (γa, γg)
sq.(QueueLocal) N γa γg q .
Definition Queue γq (_ : loc) Q : vProp Σ := γa γg G,
γq = encode (γa, γg)
sq.(QueueInv) γa γg Q G.
#[global] Instance Queue_objective γq q Q : Objective (Queue γq q Q) := _.
#[global] Instance Queue_timeless γq q Q : Timeless (Queue γq q Q) := _.
#[global] Instance isQueue_persistent N γq q : Persistent (isQueue N γq q) := _.
Lemma new_queue_spec :
new_queue_spec' sq.(spec_abs_graph.new_queue) isQueue Queue.
Proof.
iIntros (N tid Φ) "_ Post".
iApply (sq.(spec_abs_graph.new_queue_spec) with "[%//]").
iIntros "!> * [#QL LI]".
remember (encode (γa, γg)) as γq eqn:Hγq.
iApply "Post". iSplit.
- iExists _,_. iFrame (Hγq) "QL".
- iExists _,_,_. iFrame (Hγq) "LI".
Qed.
Lemma enqueue_spec :
enqueue_spec' sq.(spec_abs_graph.enqueue) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
awp_apply (sq.(spec_abs_graph.enqueue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
iIntros (V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (enqE := mkGraphEvent enq Venq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
destruct F as (? & _ & ? & ? & ? & ENQ & HenqId & EsG' & ?).
iExists Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
+ subst V'. iApply (monPred_in_mono with "⊒V'"). simpl.
change (enqE.(ge_view).(dv_comm) enqE.(ge_view).(dv_wrt)).
apply: QC.(wkq_cons_enqueue_release G').
* rewrite EsG'. apply lookup_app_1_eq.
* by exists v.
+ iPureIntro. split; [|done]. trans Venq.(dv_in); [done|]. apply dv_in_com.
Qed.
Lemma dequeue_spec :
dequeue_spec' sq.(spec_abs_graph.dequeue) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
awp_apply (sq.(spec_abs_graph.dequeue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
iIntros (v V' Q' G' enqId deqId enq deq Venq Vdeq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (deqE := mkGraphEvent deq Vdeq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|CASE]).
- destruct CASE as (-> & ? & ?). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by left.
- destruct CASE as (-> & ? & ENQ & DEQ & ? & ? & EsG' & SoG' & ComG' & ? & ? & ?
& enqE & ? & ? & ? & ?).
rewrite /is_enqueue in ENQ. rewrite /is_dequeue in DEQ. subst enq deq.
iExists v, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
{ iDestruct (view_at_elim with "⊒V' QL'") as "{QL QL'} QL'".
rewrite QueueLocal_graph_snap.
iApply (graph_snap_lookup _ _ _ enqId with "QL'"); [|done].
apply list_lookup_fmap_inv'. exists enqE. split; [done|].
eapply prefix_lookup; [done|by eexists]. }
iPureIntro. by right.
Qed.
Lemma try_enq_spec :
try_enq_spec' sq.(spec_abs_graph.try_enq _ _) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
awp_apply (sq.(spec_abs_graph.try_enq_spec _ _) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
iIntros (b V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (enqE := mkGraphEvent enq Venq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
destruct F as (? & _ & ? & ? & CASE). destruct b.
- destruct CASE as (? & ENQ & HenqId & EsG' & ?).
iExists true, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
+ subst V'. iApply (monPred_in_mono with "⊒V'"). simpl.
change (enqE.(ge_view).(dv_comm) enqE.(ge_view).(dv_wrt)).
apply: QC.(wkq_cons_enqueue_release G').
* rewrite EsG'. apply lookup_app_1_eq.
* by exists v.
+ iPureIntro. split; [|done]. trans Venq.(dv_in); [done|]. apply dv_in_com.
- destruct CASE as [-> ->].
iExists false, V, Q.
iSplitL; [|by auto]. iFrame "Q ⊒V". done.
Qed.
Lemma try_deq_spec :
try_deq_spec' sq.(spec_abs_graph.try_deq _ _) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
awp_apply (sq.(spec_abs_graph.try_deq_spec _ _) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
iIntros (v V' Q' G' enqId deqId enq deq Venq Vdeq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (deqE := mkGraphEvent deq Vdeq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|[CASE|CASE]]).
- destruct CASE as (-> & ? & ->). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by left.
- destruct CASE as (-> & ? & ?). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by right; left.
- destruct CASE as (-> & ? & ENQ & DEQ & ? & ? & EsG' & SoG' & ComG' & ? & ? & ?
& enqE & ? & ? & ? & ?).
rewrite /is_enqueue in ENQ. rewrite /is_dequeue in DEQ. subst enq deq.
iExists v, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
{ iDestruct (view_at_elim with "⊒V' QL'") as "{QL QL'} QL'".
rewrite QueueLocal_graph_snap.
iApply (graph_snap_lookup _ _ _ enqId with "QL'"); [|done].
apply list_lookup_fmap_inv'. exists enqE. split; [done|].
eapply prefix_lookup; [done|by eexists]. }
iPureIntro. by right; right.
Qed.
End abs_graph.
Program Definition abs_graph_abs_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : spec_abs_graph.strong_queue_spec Σ) : queue_spec Σ := {|
spec_abs.Queue := Queue sq ;
spec_abs.isQueue := isQueue sq ;
spec_abs.Queue_Objective := Queue_objective sq ;
spec_abs.Queue_Timeless := Queue_timeless sq ;
spec_abs.isQueue_Persistent := isQueue_persistent sq ;
spec_abs.new_queue_spec := new_queue_spec sq ;
spec_abs.enqueue_spec := enqueue_spec sq ;
spec_abs.dequeue_spec := dequeue_spec sq ;
spec_abs.try_enq_spec := try_enq_spec sq ;
spec_abs.try_deq_spec := try_deq_spec sq ;
|}%I.
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