Commit 16a8dd51 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Proof almost finished

parent 033b99da
......@@ -64,26 +64,84 @@ Section MSQueue.
Context (P : Z iProp Σ).
Fixpoint link_inv (L: list (loc * Z)): iProp Σ :=
Fixpoint link_inv' (L: list (loc * Z)) (next_link: base_lit): iProp Σ :=
(match L with
| [] => True
| (h, d) :: L' => match L' with
| [] => h #0
| (l, v) :: L'' => h #l link_inv L'
end
| [(h, _)] => h #next_link
| (h, _) :: ((l, _) :: _) as L' => h #l link_inv' L' next_link
end)%I.
Definition link_inv (L: list (loc * Z)): iProp Σ :=
link_inv' L 0.
Lemma tail_recursive_expansion (L: list (loc * Z)):
L = [] (L' t v, L = L' ++ [(t, v)]).
Proof.
induction L as [|(t', v')]; auto. right.
destruct IHL.
- rewrite H. by exists nil, t', v'.
- destruct H as [L' [t [v]]]. rewrite H. by exists ((t', v') :: L'), t, v.
Qed.
Lemma link_inv_expand (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit):
(link_inv' L nl L = L' ++ [(l, v)] link_inv' L' l l #nl)%I.
Proof.
iInduction L' as [|[l' v'] L'] "IH" forall (L); iIntros "H %".
- iSplitR. done. rewrite app_nil_l in a. by rewrite a.
- rewrite a.
replace (((l', v') :: L') ++ [(l, v)]) with ((l', v') :: (L' ++ [(l, v)])) by done.
destruct L' as [|[l'' v''] L'].
+ rewrite app_nil_l. iDestruct "H" as "(Hl & Hr)". iFrame.
+ iDestruct "H" as "(H & H2)". iDestruct ("IH" with "[H2]") as "IH'". (*iApply "H2".*) admit.
iFrame. by iApply "IH'".
Admitted.
Lemma link_inv_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit) :
(link_inv' L' l l #nl L = L' ++ [(l, v)] link_inv' L nl)%I.
Proof.
iInduction L' as [|[l' v'] L'] "IH" forall (L); iIntros "H %"; rewrite a.
- rewrite app_nil_l. by iDestruct "H" as "(_ & H)".
- replace (((l', v') :: L') ++ [(l, v)]) with ((l', v') :: (L' ++ [(l, v)])) by done.
destruct L' as [|[l'' v''] L'].
+ by rewrite app_nil_l.
+ iDestruct "H" as "((H & H2) & H3)".
iDestruct ("IH" with "[H2 H3]") as "IH'". iFrame. iFrame. by iApply "IH'".
Qed.
Fixpoint value_inv (Lin: list (loc * Z)): iProp Σ :=
(match Lin with
| [] => True
| (l, v) :: L' => (l + 1) #v P(v) value_inv L'
| [] => True
| (l, v) :: L' => (l + 1) #v P(v) value_inv L'
end)%I.
Lemma value_inv_rev_expand (L L': list (loc * Z)) (l: loc) (v: Z) :
(value_inv L L = L' ++ [(l, v)] value_inv L' (l + 1) #v P(v))%I.
Proof.
iInduction L' as [|[l' v'] L''] "IH" forall (L).
- iIntros "H %". iSplitR. done. rewrite app_nil_l in a. rewrite a.
iDestruct "H" as "(H1 & H2 & _)". iFrame.
- iIntros "H %". rewrite a.
replace (((l', v') :: L'') ++ [(l, v)]) with ((l', v') :: (L'' ++ [(l, v)])) by done.
iDestruct "H" as "(Hl & HPv & Hr)". iFrame.
iDestruct ("IH" with "Hr") as "IH'". by iApply "IH'".
Qed.
Lemma value_inv_rev_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) :
(value_inv L' (l + 1) #v P(v) L = L' ++ [(l, v)] value_inv L)%I.
Proof.
iInduction L' as [|[l' v'] L''] "IH" forall (L); iIntros "H %"; rewrite a.
- rewrite app_nil_l. iDestruct "H" as "(_ & H1 & H2)". iFrame.
- replace (((l', v') :: L'') ++ [(l, v)]) with ((l', v') :: (L'' ++ [(l, v)])) by done.
iDestruct "H" as "((H & H2 & H3) & H4 & H5)".
iDestruct ("IH" with "[H3 H4 H5]") as "IH'". iFrame. iFrame. by iApply "IH'".
Qed.
Definition queue_inv_s (q: loc) (γc γp: gname): iProp Σ :=
( (h t: loc) (Lout: list (loc * Z)),
q {1/2} #h (q + 1) {1/2} #t own γc ( (Excl' (Lout)))
( (Lin Lout_rest: list (loc * Z)) (d: Z),
Lout = Lout_rest ++ [(h, d)] own γp ({1/2} (ListSome (Lout ++ Lin) : my_master_cmra)) link_inv ([(h, d)] ++ Lin) value_inv Lin)
Lout = Lout_rest ++ [(h, d)]
own γp ({1/2} (ListSome (Lout ++ Lin) : my_master_cmra)) link_inv ([(h, d)] ++ Lin) value_inv Lin)
)%I.
Definition queueN : namespace := nroot .@ "queue".
......@@ -112,7 +170,8 @@ Section MSQueue.
iDestruct "Hh" as "[Hhq Hhc]".
iDestruct "Ht" as "(Htq & Htp)".
iMod (inv_alloc queueN _ (queue_inv_s q γc γp) with "[Hhq Htq Hl Hγc● Hγp●1]") as "#Hinv".
{ iNext. iExists _, _, _. iFrame. iExists _, nil, 0. iFrame. rewrite app_nil_l. rewrite app_nil_r. rewrite loc_add_0. by iFrame. }
{ iNext. iExists _, _, _. iFrame. iExists _, nil, 0. iFrame. rewrite app_nil_l.
rewrite app_nil_r. rewrite loc_add_0. by iFrame. }
iModIntro. iApply "Post".
iExists γc, γp.
iSplitL "Hinv". iExists q. eauto.
......@@ -158,37 +217,53 @@ Section MSQueue.
Proof.
intros. iIntros "(#Hq & Hp & Px) Post".
iDestruct "Hq" as (l ->) "#Hinv".
iDestruct "Hp" as (t vt L) "[Htp Hγp●2]".
iDestruct "Hp" as (t' tv' L) "[Htp Hγp●2]".
wp_lam. wp_let.
wp_alloc n as "(Hnl & Hnd)". lia. rewrite big_sepL_singleton. wp_let.
wp_op. wp_store. wp_op. wp_load. wp_let. wp_op.
wp_bind (_ <- _)%E.
iInv queueN as (h t' Lout) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iInv queueN as (h t Lout) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Htp Htq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (Lin Lout_rest d) "(>H & >Hγp●1 & Hl & Hv)". iDestruct "H" as %H1.
destruct Lin as [|[l' v] L'] eqn:HL.
- rewrite app_nil_r. iDestruct (own_lat_auth_frac_agree _ _ _ _ _ _ with "[Hγp●1 Hγp●2]") as %H2.
iCombine "Hγp●1" "Hγp●2" as "Hγp●". iFrame.
rewrite H1 in H2. apply app_inj_tail in H2 as [H2 H3]. inversion H3. simplify_eq.
rewrite app_nil_r. iDestruct "Hl" as ">Htl". unfold link_inv.
rewrite loc_add_0. wp_store. iClear "Hv".
iCombine "Hγp●1" "Hγp●2" as "Hγp●".
iMod (@own_lat_auth_update (leibnizO (loc * Z)) _ _ _ _ _ _ (Lout_rest ++ [(h, d)] ++ [(n, x)]) _ with "Hγp●") as "[[Hγp●1 Hγp●2] _]".
iMod ("Hclose" with "[Hhq Htq Htl Hnl Hnd Hγc● Hγp●1 Px]") as "_".
{ iNext. iExists _, _, _. iFrame. iExists _, Lout_rest, d. rewrite app_assoc. iFrame.
rewrite loc_add_0. by iFrame. }
iModIntro. wp_seq. wp_op. wp_bind (_ <- _)%E.
iInv queueN as (h' t Lout') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Htp Htq") as %?. simplify_eq.
iCombine "Htp" "Htq" as "Ht". wp_store.
iDestruct "Ht" as "[Htp Htq]".
iMod ("Hclose" with "[Hhq Htq Hγc● HL]") as "_".
{ iNext. iExists _, _, _. iFrame. }
iModIntro. wp_seq. iApply "Post".
iSplitL. rewrite app_assoc. iExists _, x, (Lout_rest ++ [(t, d)]). iFrame.
by iLeft.
- admit.
Admitted.
iDestruct "HL" as (Lin Lout_rest d) "(>H1 & >Hγp●1 & Hl & Hv)".
iDestruct "H1" as %H1.
assert (H2: L_rest t tv, [(h, d)] ++ Lin = L_rest ++ [(t, tv)]).
{ destruct (tail_recursive_expansion Lin). rewrite H. by exists nil, h, d.
destruct H as [L' [t [v]]]. rewrite H. by exists ([(h, d)] ++ L'), t, v. }
destruct H2 as [L_rest [t [tv]]].
iDestruct (own_lat_auth_frac_agree _ _ _ _ _ _ with "[Hγp●1 Hγp●2]") as %H3.
{ iCombine "Hγp●1" "Hγp●2" as "Hγp●". iFrame. }
rewrite H1 in H3. rewrite <- app_assoc in H3. rewrite H in H3.
rewrite app_assoc in H3. apply app_inj_tail in H3 as [H2 H3].
inversion H3. simplify_eq. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite H. iCombine "Hγp●1" "Hγp●2" as "Hγp●".
iAssert ( (link_inv' L_rest t t #0))%I with "[Hl]" as "Ht".
{ destruct L_rest as [|[l' v] L'] eqn:HL.
- rewrite app_nil_l in H. inversion H. rewrite app_nil_l. iFrame.
- iDestruct (link_inv_expand with "Hl") as "Hl". by iApply "Hl". }
iDestruct "Ht" as "[Hl Ht]".
rewrite loc_add_0. wp_store.
iMod (@own_lat_auth_update (leibnizO (loc * Z)) _ _ _ _ _ _ (Lout_rest ++ [(h, d)] ++ Lin ++ [(n, x)]) _ with "Hγp●") as "[[Hγp●1 Hγp●2] _]".
iMod ("Hclose" with "[Hhq Htq Ht Hl Hv Hnl Hnd Hγc● Hγp●1 Px]") as "_".
{ iNext. iExists _, _, _. iFrame. iExists (Lin ++ [(n, x)]), Lout_rest, d. rewrite app_assoc. iFrame.
rewrite app_assoc. rewrite H. rewrite loc_add_0.
iDestruct (value_inv_rev_expand_rev (Lin ++ [(n, x)]) Lin n x) as "Hvalue".
iDestruct ("Hvalue" with "[Hv Hnd Px]") as "Hv". by iFrame.
iDestruct (link_inv_expand_rev ((L_rest ++ [(t, tv)]) ++ [(n, x)]) (L_rest ++ [(t, tv)]) n x 0) as "Hlink".
iDestruct (link_inv_expand_rev (L_rest ++ [(t, tv)]) L_rest t tv n) as "Hlink'".
iDestruct ("Hlink'" with "[Hl Ht]") as "Hl". iFrame.
iDestruct ("Hlink" with "[Hl Hnl]") as "Hl". iFrame. by iApply "Hl".
iSplitR. done. iSplitL "Hl". by iApply "Hl". by iApply "Hv". }
iModIntro. wp_seq. wp_op. wp_bind (_ <- _)%E.
iInv queueN as (h' t' Lout') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Htp Htq") as %?. simplify_eq.
iCombine "Htp" "Htq" as "Ht". wp_store.
iDestruct "Ht" as "[Htp Htq]".
iMod ("Hclose" with "[Hhq Htq Hγc● HL]") as "_".
{ iNext. iExists _, _, _. iFrame. }
iModIntro. wp_seq. iApply "Post".
iSplitL. rewrite app_assoc. iExists _, x, (Lout_rest ++ [(h, d)] ++ Lin).
rewrite app_assoc. rewrite app_assoc. iFrame. by iLeft.
Admitted.
Lemma tryDeq_spec q γc γp:
{{{ Queue q γc γp Consumer q γc }}}
......
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