Library iris.locks.ticket_clh_refinement
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.locks Require Import ticket_clh_triples lock_reln.
Import uPred.
Global Set Bullet Behavior "Strict Subproofs".
Section closed.
Local Open Scope nat_scope.
Definition Kd := 100%nat.
Definition dinit := 50.
Definition Σ : gFunctors := #[ heapGF ; sheapGF ; tlockGF ;
refineGF (delayed_lang (heap_lang) Kd dinit)
(S Kd × (Kd + 3))].
Definition ticketN : namespace := nroot.@ "prot".
Lemma Σ_len: projT1 Σ = 4%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (heap_lang) Kd dinit) (S Kd × (Kd + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 4) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ simpl in ×. intros (?&_). exfalso; eauto. }
inversion g.
Grab Existential Variables.
rewrite /Kd. auto.
Qed.
Instance inGF_sheapG: sheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_tlockG: tlockG Σ.
Proof. eauto. split. try apply _; eauto. Qed.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Lemma soundness e e':
(∀ H1 H2 H3, @ctx_expr_equiv dinit Σ ticketN Kd H1 H2 H3
(@is_lock _ _ _ _ ticketN _ _ _) ∅ Bool e e') →
safe_refine (bool_refine) e' ∅ e ∅.
Proof.
intros Hpre.
case_eq (to_val e).
- intros Hv Heqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := 0%nat).
× eapply head_step_det_prim_det, heap_lang.head_step_det.
× apply heap_prim_dec.
×
iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Heqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown')".
iExists vc.
rewrite {1}/dK //= heap_lang.to_of_val.
iFrame "Hown'".
rewrite affine_elim.
iFrame. rewrite val_equiv_fix_unfold' /bool_refine. rewrite //=.
iDestruct "HVC" as (b) "(%&%)".
subst. done.
- intros Hneqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := dinit%nat).
× eapply head_step_det_prim_det, heap_lang.head_step_det.
× apply heap_prim_dec.
× iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Hneqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown1)".
iExists vc.
rewrite {1}/dK //= heap_lang.to_of_val.
iFrame.
rewrite affine_elim.
rewrite val_equiv_fix_unfold' /bool_refine. rewrite //=.
iDestruct "HVC" as (b) "(%&%)".
subst. done.
Qed.
Theorem lock_refinement e e':
type_trans ticket.acquire clh.acquire ticket.release clh.release ticket.newlock clh.newlock
∅ e e' Bool →
safe_refine (bool_refine) e' ∅ e ∅.
Proof.
assert (99 < Kd)%Z by rewrite /Kd //=.
intros. eapply soundness.
intros. eapply (fundamental ticket.acquire clh.acquire ticket.release clh.release
ticket.newlock clh.newlock).
- rewrite /ticketN /heapN; eauto with ndisj.
- rewrite /ticketN /heapN; eauto with ndisj.
- rewrite /dinit /Kd. rewrite //=.
- apply is_lock_relevant; eauto.
- apply is_lock_affine; eauto.
- apply locked_affine; eauto.
- iIntros (i K R) "(#?&#?&Hown&HR)".
iPoseProof (newlock_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
{ rewrite /ticketN /heapN; eauto with ndisj. }
{ rewrite /ticketN /heapN; eauto with ndisj. }
iSpecialize ("Hspec" with "[Hown HR]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.newlock #())) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. iSplitL; done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres".
iDestruct "Hres" as (lks γ) "(Hlock&Hown)".
iExists lks, γ. iFrame.
erewrite fill_val_dK; first done; eauto using to_of_val.
- iIntros (i K R lks l γ) "(Hlock&Hown)".
iPoseProof (acquire_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
iSpecialize ("Hspec" with "[Hlock Hown]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.acquire lks)) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres"; done.
- iIntros (i K R lks l γ) "(Hlock&Hlocked&Hown&HR)".
iPoseProof (release_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
iSpecialize ("Hspec" with "[Hlock Hlocked Hown HR]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.release lks)) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres"; done.
- eauto.
Grab Existential Variables.
eauto. eauto. eauto.
Qed.
End closed.
Print Assumptions lock_refinement.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.locks Require Import ticket_clh_triples lock_reln.
Import uPred.
Global Set Bullet Behavior "Strict Subproofs".
Section closed.
Local Open Scope nat_scope.
Definition Kd := 100%nat.
Definition dinit := 50.
Definition Σ : gFunctors := #[ heapGF ; sheapGF ; tlockGF ;
refineGF (delayed_lang (heap_lang) Kd dinit)
(S Kd × (Kd + 3))].
Definition ticketN : namespace := nroot.@ "prot".
Lemma Σ_len: projT1 Σ = 4%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (heap_lang) Kd dinit) (S Kd × (Kd + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 4) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ simpl in ×. intros (?&_). exfalso; eauto. }
inversion g.
Grab Existential Variables.
rewrite /Kd. auto.
Qed.
Instance inGF_sheapG: sheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_tlockG: tlockG Σ.
Proof. eauto. split. try apply _; eauto. Qed.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Lemma soundness e e':
(∀ H1 H2 H3, @ctx_expr_equiv dinit Σ ticketN Kd H1 H2 H3
(@is_lock _ _ _ _ ticketN _ _ _) ∅ Bool e e') →
safe_refine (bool_refine) e' ∅ e ∅.
Proof.
intros Hpre.
case_eq (to_val e).
- intros Hv Heqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := 0%nat).
× eapply head_step_det_prim_det, heap_lang.head_step_det.
× apply heap_prim_dec.
×
iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Heqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown')".
iExists vc.
rewrite {1}/dK //= heap_lang.to_of_val.
iFrame "Hown'".
rewrite affine_elim.
iFrame. rewrite val_equiv_fix_unfold' /bool_refine. rewrite //=.
iDestruct "HVC" as (b) "(%&%)".
subst. done.
- intros Hneqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := dinit%nat).
× eapply head_step_det_prim_det, heap_lang.head_step_det.
× apply heap_prim_dec.
× iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Hneqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown1)".
iExists vc.
rewrite {1}/dK //= heap_lang.to_of_val.
iFrame.
rewrite affine_elim.
rewrite val_equiv_fix_unfold' /bool_refine. rewrite //=.
iDestruct "HVC" as (b) "(%&%)".
subst. done.
Qed.
Theorem lock_refinement e e':
type_trans ticket.acquire clh.acquire ticket.release clh.release ticket.newlock clh.newlock
∅ e e' Bool →
safe_refine (bool_refine) e' ∅ e ∅.
Proof.
assert (99 < Kd)%Z by rewrite /Kd //=.
intros. eapply soundness.
intros. eapply (fundamental ticket.acquire clh.acquire ticket.release clh.release
ticket.newlock clh.newlock).
- rewrite /ticketN /heapN; eauto with ndisj.
- rewrite /ticketN /heapN; eauto with ndisj.
- rewrite /dinit /Kd. rewrite //=.
- apply is_lock_relevant; eauto.
- apply is_lock_affine; eauto.
- apply locked_affine; eauto.
- iIntros (i K R) "(#?&#?&Hown&HR)".
iPoseProof (newlock_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
{ rewrite /ticketN /heapN; eauto with ndisj. }
{ rewrite /ticketN /heapN; eauto with ndisj. }
iSpecialize ("Hspec" with "[Hown HR]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.newlock #())) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. iSplitL; done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres".
iDestruct "Hres" as (lks γ) "(Hlock&Hown)".
iExists lks, γ. iFrame.
erewrite fill_val_dK; first done; eauto using to_of_val.
- iIntros (i K R lks l γ) "(Hlock&Hown)".
iPoseProof (acquire_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
iSpecialize ("Hspec" with "[Hlock Hown]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.acquire lks)) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres"; done.
- iIntros (i K R lks l γ) "(Hlock&Hlocked&Hown&HR)".
iPoseProof (release_spec ticketN _ i K dinit (dK dinit K #())) as "Hspec".
{ rewrite /dinit; split; omega. }
{ rewrite /dK /dinit; case_match; omega. }
iSpecialize ("Hspec" with "[Hlock Hlocked Hown HR]").
{ iFrame. rewrite /dK.
assert (to_val (ectx_language.fill K (ticket.release lks)) = None) as →.
{ rewrite /ectx_language.to_val.
specialize (@fill_not_val heap_lang.expr _ _ _ _).
intros Hfill; eapply Hfill.
rewrite //=.
}
iFrame. done.
}
iApply wp_wand_l. iFrame "Hspec". iIntros "@". iIntros (v) "Hres"; done.
- eauto.
Grab Existential Variables.
eauto. eauto. eauto.
Qed.
End closed.
Print Assumptions lock_refinement.