Commit 0495f119 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'prophecy_list' into 'master'

Prophecy variables with lists

See merge request !225
parents 9936cb12 d479c851
......@@ -67,6 +67,7 @@ theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/proph_map.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
......@@ -89,7 +90,6 @@ theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_map.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
......
From iris.algebra Require Import auth gmap.
From iris.algebra Require Import auth list gmap.
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
Local Notation proph_map P V := (gmap P (list V)).
Definition proph_val_list (P V : Type) := list (P * V).
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
gmapUR P $ exclR $ optionC $ leibnizC V.
gmapUR P $ exclR $ listC $ leibnizC V.
Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
fmap (λ v, Excl (v : option (leibnizC V))) pvs.
fmap (λ vs, Excl (vs : list (leibnizC V))) pvs.
(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
......@@ -31,83 +31,64 @@ Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
Proof. solve_inG. Qed.
Section definitions.
Context `{Countable P, pG : !proph_mapG P V Σ}.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
(list_to_map pvs : gmap P V) !! p.
Context `{pG : proph_mapG P V Σ}.
Implicit Types pvs : proph_val_list P V.
Implicit Types R : proph_map P V.
Implicit Types p : P.
Definition first_resolve_in_list (R : proph_map P V) (pvs : proph_val_list P V) :=
p v, p dom (gset _) R
first_resolve pvs p = Some v
R !! p = Some (Some v).
(** The list of resolves for [p] in [pvs]. *)
Fixpoint proph_list_resolves pvs p : list V :=
match pvs with
| [] => []
| (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
else proph_list_resolves pvs p
end.
Definition proph_map_auth (R : proph_map P V) : iProp Σ :=
own (proph_map_name pG) ( (to_proph_map R)).
Definition proph_resolves_in_list R pvs :=
map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
Definition proph_map_ctx (pvs : proph_val_list P V) (ps : gset P) : iProp Σ :=
( R, first_resolve_in_list R pvs
Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
( R, proph_resolves_in_list R pvs
dom (gset _) R ps
proph_map_auth R)%I.
own (proph_map_name pG) ( (to_proph_map R)))%I.
Definition proph_def (p : P) (vs : list V) : iProp Σ :=
own (proph_map_name pG) ( {[p := Excl vs]}).
Definition proph_def (p : P) (v: option V) : iProp Σ :=
own (proph_map_name pG) ( {[ p := Excl (v : option $ leibnizC V) ]}).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
Definition proph := proph_aux.(unseal).
Definition proph_eq :
@proph = @proph_def := proph_aux.(seal_eq).
Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
End definitions.
Section first_resolve.
Section list_resolves.
Context {P V : Type} `{Countable P}.
Implicit Type pvs : proph_val_list P V.
Implicit Type p : P.
Implicit Type v : V.
Implicit Type R : proph_map P V.
Lemma first_resolve_insert pvs p R :
first_resolve_in_list R pvs
Lemma resolves_insert pvs p R :
proph_resolves_in_list R pvs
p dom (gset _) R
first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
Proof.
intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin].
- intros ->. by rewrite lookup_insert.
- intros <-%Hf; last done. rewrite lookup_insert_ne; first done.
intros ?. subst. done.
Qed.
Lemma first_resolve_delete pvs p v R :
first_resolve_in_list R ((p, v) :: pvs)
first_resolve_in_list (delete p R) pvs.
Proof.
intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
Qed.
Lemma first_resolve_eq R p v w pvs :
first_resolve_in_list R ((p, v) :: pvs)
R !! p = Some w
w = Some v.
proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Proof.
intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
inversion Hlookup. done.
intros Hinlist Hp q vs HEq.
destruct (decide (p = q)) as [->|NEq].
- rewrite lookup_insert in HEq. by inversion HEq.
- rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
Qed.
End first_resolve.
End list_resolves.
Section to_proph_map.
Context (P V : Type) `{Countable P}.
Implicit Types p : P.
Implicit Types vs : list V.
Implicit Types R : proph_map P V.
Lemma to_proph_map_valid R : to_proph_map R.
Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
Lemma to_proph_map_insert p v R :
to_proph_map (<[p := v]> R) = <[p := Excl (v: option (leibnizC V))]> (to_proph_map R).
Lemma to_proph_map_insert p vs R :
to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizC V))]> (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_insert. Qed.
Lemma to_proph_map_delete p R :
......@@ -118,15 +99,14 @@ Section to_proph_map.
R !! p = None to_proph_map R !! p = None.
Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
Lemma proph_map_singleton_included R p v :
{[p := Excl v]} to_proph_map R R !! p = Some v.
Lemma proph_map_singleton_included R p vs :
{[p := Excl vs]} to_proph_map R R !! p = Some vs.
Proof.
rewrite singleton_included_exclusive; last by apply to_proph_map_valid.
by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
Qed.
End to_proph_map.
Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
(|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof.
......@@ -137,39 +117,59 @@ Proof.
Qed.
Section proph_map.
Context `{Countable P, !proph_mapG P V Σ}.
Context `{proph_mapG P V Σ}.
Implicit Types p : P.
Implicit Types v : option V.
Implicit Types v : V.
Implicit Types vs : list V.
Implicit Types R : proph_map P V.
Implicit Types ps : gset P.
(** General properties of mapsto *)
Global Instance proph_timeless p v : Timeless (proph p v).
Global Instance proph_timeless p vs : Timeless (proph p vs).
Proof. rewrite proph_eq /proph_def. apply _. Qed.
Lemma proph_map_alloc R p v :
p dom (gset _) R
proph_map_auth R == proph_map_auth (<[p := v]> R) proph p v.
Proof.
iIntros (Hp) "HR". rewrite /proph_map_ctx proph_eq /proph_def.
iMod (own_update with "HR") as "[HR Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) Hp). }
iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
Qed.
Lemma proph_map_remove R p v :
proph_map_auth R - proph p v == proph_map_auth (delete p R).
Lemma proph_map_new_proph p ps pvs :
p ps
proph_map_ctx pvs ps ==
proph_map_ctx pvs ({[p]} ps) proph p (proph_list_resolves pvs p).
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp").
apply auth_update_dealloc, (delete_singleton_local_update _ _ _).
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
rewrite proph_eq /proph_def.
iMod (own_update with "H●") as "[H● H◯]".
{ eapply auth_update_alloc, (alloc_singleton_local_update _ p (Excl _))=> //.
apply lookup_to_proph_map_None.
apply (not_elem_of_dom (D:=gset P)). set_solver. }
iModIntro. iFrame.
iExists (<[p := proph_list_resolves pvs p]> R). iSplitR "H●".
- iPureIntro. split.
+ apply resolves_insert; first done. set_solver.
+ rewrite dom_insert. set_solver.
- by rewrite /to_proph_map fmap_insert.
Qed.
Lemma proph_map_valid R p v : proph_map_auth R - proph p v - R !! p = Some v.
Lemma proph_map_resolve_proph p v pvs ps vs :
proph_map_ctx ((p,v) :: pvs) ps proph p vs ==
vs', vs = v::vs' proph_map_ctx pvs ps proph p vs'.
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "HR Hp")
as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2.
assert (vs = v :: proph_list_resolves pvs p) as ->.
{ rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
iMod (own_update_2 with "H● Hp") as "[H● H◯]".
{ eapply auth_update. apply: singleton_local_update.
- by rewrite /to_proph_map lookup_fmap HR.
- by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
rewrite /to_proph_map -fmap_insert.
iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
- iPureIntro. done.
- iExists _. iFrame. iPureIntro. split.
+ intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
* rewrite lookup_insert in HEq. by inversion HEq.
* rewrite lookup_insert_ne in HEq; last done.
rewrite (Hres q ws HEq).
simpl. rewrite decide_False; done.
+ assert (p dom (gset P) R) by exact: elem_of_dom_2.
rewrite dom_insert. set_solver.
Qed.
End proph_map.
From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation proph_map.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import proph_map.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......
......@@ -61,10 +61,10 @@ Section coinflip.
iModIntro. wp_seq. done.
Qed.
Definition val_to_bool (v : option val) : bool :=
Definition val_list_to_bool (v : list val) : bool :=
match v with
| Some (LitV (LitBool b)) => b
| _ => true
| LitV (LitBool b) :: _ => b
| _ => true
end.
Lemma lateChoice_spec (x: loc) :
......@@ -81,11 +81,11 @@ Section coinflip.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl".
wp_store.
iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iMod ("Hclose" $! (val_list_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_apply rand_spec; try done.
iIntros (b') "_".
wp_apply (wp_resolve_proph with "Hp").
iIntros (->). wp_seq. done.
iIntros (vs) "[HEq _]". iDestruct "HEq" as "->". wp_seq. done.
Qed.
End coinflip.
From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export proph_map.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang proph_map.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
......@@ -308,39 +309,30 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
{{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
Lemma wp_new_proph s E :
{{{ True }}}
NewProph @ s; E
{{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iSplit; first by eauto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (@proph_map_alloc with "HR") as "[HR Hp]".
{ intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
iModIntro; iSplit=> //. iFrame. iSplitL "HR".
- iExists _. iSplit; last done.
iPureIntro. split.
+ apply first_resolve_insert; auto.
+ rewrite dom_insert_L. by apply union_mono_l.
- iApply "HΦ". done.
iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_resolve_proph p v w:
{{{ proph p v }}}
ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
{{{ RET (LitV LitUnit); v = Some w }}}.
Lemma wp_resolve_proph s E p vs v :
{{{ proph p vs }}}
ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
{{{ vs', RET (LitV LitUnit); vs = v::vs' proph p vs' }}}.
Proof.
iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
iSplit=> //. iFrame.
iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ".
- iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
rewrite dom_delete. set_solver.
- iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
iModIntro. iFrame. iSplitR; first done.
iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
iApply "HΦ". iFrame.
Qed.
End lifting.
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