Commit d91a46ea by Dan Frumin

Using `ref` as a name generator example from ADR

- Involves bulling the partial bijection algebra from `runST` - Thanks to Amin for suggestions
parent 78a89b31
......@@ -2,6 +2,7 @@
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/prelude/base.v
theories/prelude/hax.v
theories/prelude/bij.v
theories/F_mu_ref_conc/binder.v
theories/F_mu_ref_conc/lang.v
theories/F_mu_ref_conc/notation.v
......
......@@ -96,6 +96,23 @@ Section CG_Counter.
by iApply "Hlog".
Qed.
Lemma bin_log_FG_increment_r Γ K E1 E2 t τ (x : loc) (n : nat) :
nclose specN E1
(x ↦ₛ # n -
(x ↦ₛ #(S n) -
{E1,E2;Δ;Γ} t log fill K #() : τ) -
{E1,E2;Δ;Γ} t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unfold FG_increment. unlock. simpl_subst/=.
rel_seq_r.
rel_load_r; rel_seq_r.
rel_op_r.
rel_cas_suc_r.
rel_if_r.
by iApply "Hlog".
Qed.
Lemma FG_counter_type Γ :
typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
Proof. solve_typed. Qed.
......
......@@ -3,7 +3,149 @@ 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.
From iris_logrel Require Import logrel examples.counter examples.lock prelude.bij.
(** * 5.2 References for name generation *)
Definition nameGenTy : type := TExists (TProd (TArrow TUnit (TVar 0))
(TArrow (TVar 0) (TArrow (TVar 0) TBool))).
Definition nameGen1 : val :=
PackV (λ: <>, ref #()
,λ: "y" "z", "y" = "z").
Definition nameGen2 : expr :=
let: "x" := ref #0 in
Pack (λ: <>, FG_increment "x" #();; !"x"
,λ: "y" "z", "y" = "z").
Lemma nameGen1_typed Γ :
typed Γ nameGen1 nameGenTy.
Proof.
unlock nameGen1 nameGenTy.
apply TPack with (Tref TUnit). asimpl.
solve_typed.
Qed.
Hint Resolve nameGen1_typed : typeable.
Lemma nameGen2_typed Γ :
typed Γ nameGen2 nameGenTy.
Proof.
unlock nameGen2 nameGenTy.
econstructor. 2: solve_typed.
econstructor. cbn.
eapply TPack with TNat. asimpl.
econstructor; solve_typed.
econstructor. cbn.
econstructor. cbn. solve_typed.
econstructor; eauto; solve_typed.
econstructor; eauto; solve_typed.
Qed.
Hint Resolve nameGen2_typed : typeable.
Section namegen_refinement.
Context `{logrelG Σ, PrePBijG loc nat Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Program Definition ngR (γ : gname) : D := λne vv,
( (l : loc) (n : nat), vv.1 = #l%V vv.2 = #n
inBij γ l n)%I.
Next Obligation. solve_proper. Qed.
Instance ngR_persistent γ ww : PersistentP (ngR γ ww).
Proof. apply _. Qed.
Definition ng_Inv (γ : gname) (c : loc) : iProp Σ :=
( (n : nat) (L : gset (loc * nat)),
BIJ γ L c ↦ₛ #n
[ set] lk L, match lk with
| (l, k) => l ↦ᵢ #() k n
end)%I.
Lemma nameGen_ref1 Γ :
Γ nameGen1 log nameGen2 : nameGenTy.
Proof.
iIntros (Δ).
unlock nameGenTy nameGen1 nameGen2.
rel_alloc_r as c "Hc". rel_let_r.
iApply fupd_logrel'.
iMod alloc_empty_bij as (γ) "HB".
pose (N:=logrelN.@"ng").
iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
{ iNext. iExists 0, . iFrame.
by rewrite big_sepS_empty. }
iModIntro.
iApply (bin_log_related_pack _ (ngR γ)).
iApply bin_log_related_pair.
- (* New name *)
iApply bin_log_related_arrow_val; eauto.
iAlways.
iIntros (? ?) "/= [% %]"; simplify_eq.
rel_seq_l. rel_seq_r.
rel_alloc_l_atomic.
iInv N as (n L) "(HB & Hc & HL)" "Hcl".
iModIntro. iNext. iIntros (l') "Hl'".
rel_rec_r.
rel_apply_r (bin_log_FG_increment_r with "Hc").
{ solve_ndisj. }
iIntros "Hc".
rel_seq_r.
rel_load_r.
iAssert (⌜¬( y, (l', y) L))%I with "[HL Hl']" as %Hl'.
{ iIntros (Hy). destruct Hy as [y Hy].
rewrite (big_sepS_elem_of _ L (l',y) Hy).
iDestruct "HL" as "[Hl _]".
iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hfoo.
compute in Hfoo. eauto. }
iAssert (⌜¬( x, (x, S n) L))%I with "[HL]" as %Hc.
{ iIntros (Hx). destruct Hx as [x Hy].
rewrite (big_sepS_elem_of _ L (x,S n) Hy).
iDestruct "HL" as "[_ %]". omega. }
iApply fupd_logrel.
iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto.
iMod ("Hcl" with "[-]").
{ iNext. iExists _,_; iFrame.
rewrite big_sepS_insert; last by naive_solver.
iFrame. iSplit; eauto.
iApply (big_sepS_mono _ _ L L with "HL"); first reflexivity.
intros [l x] Hlx. apply uPred.sep_mono_r, uPred.pure_mono. eauto. }
iModIntro.
rel_vals. iModIntro. iAlways.
iExists _, _; eauto.
- (* Name comparison *)
iApply bin_log_related_arrow_val; eauto.
iAlways.
iIntros (? ?) "/= #Hv".
iDestruct "Hv" as (l n) "(% & % & #Hln)". simplify_eq.
rel_seq_l. rel_seq_r.
iApply bin_log_related_arrow_val; eauto.
iAlways.
iIntros (? ?) "/= #Hv".
iDestruct "Hv" as (l' n') "(% & % & #Hl'n')". simplify_eq.
rel_seq_l. rel_seq_r.
(* we would like to have an atomic version of `rel_op_l`? *)
rel_bind_l (#l = #l')%E.
iApply bin_log_related_wp_atomic_l.
{ solve_atomic. }
iInv N as (m L) "(>HB & >Hc & HL)" "Hcl".
iModIntro. wp_op.
rel_op_r.
iDestruct (bij_agree with "HB Hln Hl'n'") as %Hag.
destruct (decide (l = l')) as [->|Hll].
+ assert (n = n') as -> by (apply Hag; auto).
destruct (PeanoNat.Nat.eq_dec n' n'); last congruence.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _,_; iFrame. }
iApply bin_log_related_bool.
+ assert (n n') as Hnn'.
{ intros Hnn. apply Hll. by apply Hag. }
destruct (PeanoNat.Nat.eq_dec n n'); first congruence.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _,_; iFrame. }
iApply bin_log_related_bool.
Qed.
End namegen_refinement.
(** * 5.4 Cell class *)
Definition cellτ : type :=
......@@ -18,6 +160,7 @@ Proof.
unfold cellτ. unlock cell1.
solve_typed.
Qed.
Hint Resolve cell1_typed : typeable.
Definition cell2 : val :=
Λ: let: "l" := newlock #() in
......@@ -48,6 +191,7 @@ Proof.
econstructor; solve_typed.
econstructor; solve_typed.
Qed.
Hint Resolve cell2_typed : typeable.
Definition refPool := gset ((loc * loc * loc) * loc).
Definition refPoolR := gsetUR ((loc * loc * loc) * loc).
......
(** Partial bijection stuff adapted from the runST formalisation.
"A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST"
by Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
*)
From iris.algebra Require Import auth gset.
From iris.base_logic Require Export auth invariants.
From iris.proofmode Require Import tactics.
Import uPred.
Section PBij.
Variable (A B : Type).
Context `{Countable A, Countable B}.
Definition bijective (g : gset (A * B)) :=
x y, (x, y) g ( z, (x, z) g z = y) ( z, (z, y) g z = x).
Lemma empty_bijective : bijective .
Proof. by intros x y Hxy; apply not_elem_of_empty in Hxy. Qed.
Lemma bijective_extend g l l' :
bijective g ( y, (l, y) g) ( y, (y, l') g)
bijective (({[(l, l')]} : gset (A * B)) g).
Proof.
intros bij Hl Hl' x y Hxy.
apply elem_of_union in Hxy; destruct Hxy as [Hxy|Hxy].
- apply elem_of_singleton_1 in Hxy; inversion Hxy; subst.
split; intros z Hz; apply elem_of_union in Hz; destruct Hz as [Hz|Hz];
try (apply elem_of_singleton_1 in Hz; inversion Hz; subst); trivial;
try (by apply Hl in Hz); try (by apply Hl' in Hz).
- assert (x l) by (by intros Heql; subst; apply Hl in Hxy).
assert (y l') by (by intros Heql'; subst; apply Hl' in Hxy).
apply bij in Hxy; destruct Hxy as [Hxy1 Hx2].
split; intros z Hz; apply elem_of_union in Hz; destruct Hz as [Hz|Hz];
try (apply elem_of_singleton_1 in Hz; inversion Hz; subst); trivial;
try match goal with H : ?A = ?A |- _ => by contradict H end;
auto.
Qed.
Lemma bij_eq_iff g l1 l2 l1' l2' :
bijective g ((l1, l1') g) ((l2, l2') g) l1 = l2 l1' = l2'.
Proof.
intros bij Hl1 Hl2; split => Hl1eq; subst;
by pose proof (bij _ _ Hl1) as Hb1; apply Hb1 in Hl2.
Qed.
Definition bijUR := gsetUR (A * B).
Class PrePBijG Σ := prePBijG
{ prePBijG_inG :> authG Σ bijUR }.
Class PBijG Σ := pBijG
{ PBijG_inG :> authG Σ bijUR
; PBijG_name : gname }.
Section logic.
Context `{PrePBijG Σ}.
Definition BIJ_def γ (L : bijUR) : iProp Σ :=
(own γ ( L) bijective L)%I.
Definition BIJ_aux : { x | x = @BIJ_def }. by eexists. Qed.
Definition BIJ := proj1_sig BIJ_aux.
Definition BIJ_eq : @BIJ = @BIJ_def := proj2_sig BIJ_aux.
Global Instance BIJ_timeless γ L : TimelessP (BIJ γ L).
Proof. rewrite BIJ_eq /BIJ_def. apply _. Qed.
Lemma alloc_empty_bij : (|==> γ, BIJ γ )%I.
Proof.
rewrite BIJ_eq /BIJ_def.
iMod (own_alloc ( ( : bijUR))) as (γ) "H"; first done.
iModIntro; iExists _; iFrame. iPureIntro. apply empty_bijective.
Qed.
Definition inBij_def γ (a : A) (b : B) :=
own γ ( ({[ (a, b) ]} : gset (A * B))).
Definition inBij_aux : { x | x = @inBij_def }. by eexists. Qed.
Definition inBij := proj1_sig inBij_aux.
Definition inBij_eq : @inBij = @inBij_def := proj2_sig inBij_aux.
Global Instance inBij_timeless γbij l l' : TimelessP (inBij γbij l l').
Proof. rewrite inBij_eq /inBij_def. apply _. Qed.
Global Instance inBij_persistent γbij l l' : PersistentP (inBij γbij l l').
Proof. rewrite inBij_eq /inBij_def. apply _. Qed.
Lemma bij_alloc (γ : gname) (L : gset (A * B)) a b :
( y, (a, y) L) ( x, (x, b) L)
BIJ γ L ==
BIJ γ (({[(a, b)]} : gset (A * B)) L) inBij γ a b.
Proof.
iIntros (Ha Hb) "HL"; rewrite BIJ_eq /BIJ_def inBij_eq /inBij_def.
iDestruct "HL" as "[HL HL2]"; iDestruct "HL2" as %Hbij.
iMod (own_update with "HL") as "HL".
- apply auth_update_alloc.
apply (gset_local_update _ _ (({[(a, b)]} : gset (A * B)) L)).
apply union_subseteq_r.
- rewrite -gset_op_union auth_frag_op !own_op.
iDestruct "HL" as "[$ [$ _]]".
iModIntro. iPureIntro.
by apply bijective_extend.
Qed.
Lemma bij_alloc_alt (γ : gname) (L : gset (A * B)) a b :
¬( y, (a, y) L) ¬( x, (x, b) L)
BIJ γ L ==
BIJ γ (({[(a, b)]} : gset (A * B)) L) inBij γ a b.
Proof.
intros Ha Hb; eapply bij_alloc; naive_solver.
Qed.
Lemma bij_agree γ L (a a' : A) (b b' : B) :
BIJ γ L -
inBij γ a b -
inBij γ a' b' -
a = a' b = b'⌝.
Proof.
iIntros "HL H1 H2". rewrite BIJ_eq /BIJ_def inBij_eq /inBij_def.
iDestruct "HL" as "[HL HL1]"; iDestruct "HL1" as %HL.
iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_valid_discrete_2.
iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_valid_discrete_2.
iPureIntro.
destruct Hv1 as [Hv1 _]; destruct Hv2 as [Hv2 _].
apply gset_included, elem_of_subseteq_singleton in Hv1;
apply gset_included, elem_of_subseteq_singleton in Hv2.
eapply bij_eq_iff; eauto.
Qed.
End logic.
End PBij.
Arguments BIJ {_} {_} {_} {_} {_} {_} {_} {_} γ L.
Arguments inBij {_} {_} {_} {_} {_} {_} {_} {_} γ a b.
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