Commit e45d2ccb authored by Dan Frumin's avatar Dan Frumin

Add the cell example from the ADR paper

parent 98db35db
......@@ -39,6 +39,7 @@ theories/examples/stack/helping.v
theories/examples/various.v
theories/examples/or.v
theories/examples/symbol.v
theories/examples/generative.v
theories/tests/typetest.v
theories/tests/tactics.v
theories/tests/tactics2.v
(** More generative ADT example from "State-Dependent
Represenation Independence" by A. Ahmed, D. Dreyer, A. Rossberg. *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gset frac.
From iris.base_logic.lib Require Import auth.
From iris_logrel Require Import logrel examples.counter examples.lock examples.various.
(** * 5.4 Cell class *)
Definition cellτ : type :=
TForall (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
(TArrow (TVar 0) (TVar 1)))
(TArrow (TVar 0) (TArrow (TVar 1) TUnit)))).
Definition cell1 : val :=
Λ: Pack (λ: "x", ref "x", λ: "r", !"r", λ: "r" "x", "r" <- "x").
Lemma cell1_typed Γ :
typed Γ cell1 cellτ.
Proof.
unfold cellτ. unlock cell1.
solve_typed.
Qed.
Definition cell2 : val :=
Λ: let: "l" := newlock #() in
Pack ( λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in
release "l";; "v"
, λ: "r", acquire "l";;
let: "v" :=
if: !(Fst (Fst "r"))
then !(Snd "r")
else !(Snd (Fst "r")) in
release "l";;
"v"
, λ: "r" "x", acquire "l";;
(if: !(Fst (Fst "r"))
then (Snd (Fst "r")) <- "x";; (Fst (Fst "r")) <- #false
else (Snd "r") <- "x";; (Fst (Fst "r")) <- #true);;
release "l").
Lemma cell2_typed Γ :
typed Γ cell2 cellτ.
Proof.
unfold cellτ. unlock cell2.
solve_typed.
econstructor.
econstructor. 2: solve_typed.
econstructor.
eapply TPack with (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))).
asimpl.
econstructor; solve_typed.
econstructor; solve_typed.
Qed.
Definition refPool := gset ((loc * loc * loc) * loc).
Definition refPoolR := gsetUR ((loc * loc * loc) * loc).
Class refPoolG Σ := RefPoolG
{ refPool_inG :> authG Σ refPoolR }.
Section cell_refinement.
Context `{logrelG Σ, lockG Σ, refPoolG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Definition cellInt (R : D) (r1 r2 r3 r : loc) : iProp Σ :=
( (a b c : val), r ↦ₛ a r2 ↦ᵢ b r3 ↦ᵢ c
( (r1 ↦ᵢ #true R (c, a))
(r1 ↦ᵢ #false R (b, a))))%I.
Definition cellRegInv (P : refPool) (R : D) : iProp Σ :=
([ set] rs P, match rs with
| ((r1, r2, r3), r) => cellInt R r1 r2 r3 r
end)%I.
Definition cellInv γ R : iProp Σ :=
( (P : refPool), own γ ( P) cellRegInv P R)%I.
Program Definition cellR (γ : gname) : D := λne vv,
( r1 r2 r3 r : loc, vv.1 = (#r1, #r2, #r3)%V vv.2 = #r
own γ ( {[(r1, r2, r3), r]}))%I.
Next Obligation. solve_proper. Qed.
Instance cellR_persistent γ ww : PersistentP (cellR γ ww).
Proof. apply _. Qed.
Lemma cellRegInv_excl (P : refPool) R (r1 r2 r3 r : loc) (v : val) :
cellRegInv P R - r1 ↦ᵢ v - (r1, r2, r3, r) P.
Proof.
rewrite /cellRegInv.
iIntros "HP Hr1".
iAssert ((r1, r2, r3, r) P False)%I as %Hbaz.
{
iIntros (HP).
rewrite (big_sepS_elem_of _ P _ HP).
iDestruct "HP" as (a b c) "(Hr & Hr2 & Hr3 & Hrs)".
iDestruct "Hrs" as "[[Hr1' ?]|[Hr1' ?]]";
iDestruct (mapsto_valid_2 r1 with "Hr1' Hr1") as %Hfoo;
compute in Hfoo; contradiction.
}
iPureIntro. eauto.
Qed.
Lemma cellRegInv_open (P : refPool) R (r1 r2 r3 r : loc) :
(r1, r2, r3, r) P
cellRegInv P R -
(cellInt R r1 r2 r3 r) (cellInt R r1 r2 r3 r - cellRegInv P R).
Proof.
iIntros (Hrin) "Hreg".
rewrite /cellRegInv.
iDestruct (big_sepS_elem_of_acc _ P (r1, r2, r3, r) with "Hreg") as "[Hrs Hreg]"; first assumption.
by iFrame.
Qed.
Lemma refPool_alloc γ (P : refPool) (r1 r2 r3 r : loc) :
(r1, r2, r3, r) P
own γ ( P)
== own γ ( ({[(r1, r2, r3, r)]} P))
own γ ( ({[(r1, r2, r3, r)]})).
Proof.
iIntros (Hin) "HP".
iMod (own_update with "HP") as "[HP Hfrag]".
{ eapply auth_update_alloc.
eapply (gset_local_update _ _ ({[(r1, r2, r3, r)]} P)).
apply union_subseteq_r. }
iFrame.
rewrite -gset_op_union auth_frag_op.
by iDestruct "Hfrag" as "[$ _]".
Qed.
Lemma refPool_lookup γ (P : refPool) (r1 r2 r3 r : loc) :
own γ ( P) -
own γ ( {[(r1, r2), r3, r]}) -
(r1, r2, r3, r) P.
Proof.
iIntros "Ho Hrs".
iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo.
iPureIntro.
apply auth_valid_discrete in Hfoo.
simpl in Hfoo. destruct Hfoo as [Hfoo _].
revert Hfoo. rewrite left_id.
by rewrite gset_included elem_of_subseteq_singleton.
Qed.
Lemma cell2_cell1_refinement Γ :
Γ cell2 log cell1 : cellτ.
Proof.
iIntros (Δ).
unlock cell2 cell1 cellτ.
pose (N:=logrelN.@"locked").
assert (Closed (dom _ Γ) (let: "l" := newlock #() in
Pack
(λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in
release "l";; "v",
λ: "r",
acquire "l" ;;
let: "v" := if: ! (Fst (Fst "r")) then
! (Snd "r") else ! (Snd (Fst "r")) in
release "l" ;; "v",
λ: "r" "x",
acquire "l" ;;
(if: ! (Fst (Fst "r"))
then Snd (Fst "r") <- "x" ;; Fst (Fst "r") <- #false
else Snd "r" <- "x" ;;
Fst (Fst "r") <- #true) ;; release "l"))).
{ apply Closed_mono with ; eauto.
set_solver. }
assert (Closed (dom _ Γ) (Pack (λ: "x", ref "x", λ: "r", ! "r", λ: "r" "x", "r" <- "x"))).
{ apply Closed_mono with ; eauto.
set_solver. }
iApply bin_log_related_tlam; auto.
iIntros (R HR) "!#".
iApply fupd_logrel'.
iMod (own_alloc ( ( : refPoolR))) as (γ) "Ho"; first done.
iModIntro.
rel_apply_l (bin_log_related_newlock_l N (cellInv γ R)%I with "[Ho]").
{ iExists _. iFrame. unfold cellRegInv.
by rewrite big_sepS_empty. }
iIntros (lk γl) "#Hlk".
rel_let_l.
iApply (bin_log_related_pack _ (cellR γ)).
repeat iApply bin_log_related_pair.
- (* New cell *)
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (v1 v2) "/= #Hv".
rel_let_l. rel_let_r.
rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto.
iIntros "Hl".
iDestruct 1 as (P) "[Ho HP]".
rel_let_l.
rel_alloc_l as r1 "Hr1".
rel_alloc_l as r2 "Hr2".
rel_alloc_l as r3 "Hr3".
rel_alloc_r as r "Hr".
rel_let_l.
iDestruct (cellRegInv_excl with "HP Hr1") as %Hrs.
iApply fupd_logrel'.
iMod (refPool_alloc γ P r1 r2 r3 r with "Ho") as "[Ho #Hrs]"; first apply Hrs.
iModIntro.
rel_apply_l (bin_log_related_release_l with "Hlk Hl [-Hrs]"); first auto.
{ iExists _; iFrame. rewrite {2}/cellRegInv.
rewrite big_sepS_insert; last assumption.
iFrame. iExists _,_,_. iFrame. iRight; by iFrame. }
rel_let_l.
rel_vals. iModIntro. iAlways. iExists _,_,_,_. eauto.
- (* Read cell *)
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (v1 v2) "/=".
iDestruct 1 as (r1 r2 r3 r) "[% [% #Hrs]]". simplify_eq.
rel_let_l.
rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto.
iIntros "Hl".
iDestruct 1 as (P) "[Ho HP]".
rel_let_l. repeat rel_proj_l.
iDestruct (refPool_lookup with "Ho Hrs") as %Hrin.
iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin.
iDestruct "Hr" as (a b c) "(Hr & Hr2 & Hr3 & [[Hr1 #HR] | [Hr1 #HR]])";
rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l;
rel_let_r; rel_load_r.
+ rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto.
{ iExists _; iFrame. iApply "HclP".
iExists _,_,_; iFrame. iLeft; by iFrame. }
rel_let_l. rel_vals; eauto.
+ rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto.
{ iExists _; iFrame. iApply "HclP".
iExists _,_,_; iFrame. iRight; by iFrame. }
rel_let_l. rel_vals; eauto.
- (* Insert cell *)
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (v1 v2) "/=".
iDestruct 1 as (r1 r2 r3 r) "[% [% #Hrs]]". simplify_eq.
rel_let_l. rel_let_r.
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (v1 v2) "/= #Hv".
rel_let_l. rel_let_r.
rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto.
iIntros "Hl".
iDestruct 1 as (P) "[Ho HP]".
rel_let_l. repeat rel_proj_l.
iDestruct (refPool_lookup with "Ho Hrs") as %Hrin.
iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin.
iDestruct "Hr" as (a b c) "(Hr & Hr2 & Hr3 & [[Hr1 #HR] | [Hr1 #HR]])";
rel_load_l; rel_if_l; repeat rel_proj_l;
rel_store_l; rel_let_l; repeat rel_proj_l;
rel_store_l; rel_store_r; rel_let_l.
+ rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto.
{ iExists _; iFrame. iApply "HclP".
iExists _,_,_; iFrame. iRight; by iFrame. }
iApply bin_log_related_unit.
+ rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto.
{ iExists _; iFrame. iApply "HclP".
iExists _,_,_; iFrame. iLeft; by iFrame. }
iApply bin_log_related_unit.
Qed.
End cell_refinement.
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