Commit 8f90c564 authored by Dan Frumin's avatar Dan Frumin
Browse files

bump iris

parent 2d33ef80
......@@ -64,7 +64,7 @@ Section namegen_refinement.
{ iIntros (Hy). destruct Hy as [y Hy].
rewrite (big_sepS_elem_of _ L (l',y) Hy).
iDestruct "HL" as "[Hl _]".
iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
compute in Hfoo. eauto. }
iAssert (( x, (x, S n) L) False)%I with "[HL]" as %Hc.
{ iIntros (Hx). destruct Hx as [x Hy].
......
......@@ -108,38 +108,41 @@ Section rules.
rel_values.
Qed.
(* Lemma par_l_1' Q K e1 e2 t : *)
(* (REL e1 << t : ()) -∗ *)
(* (WP e2 {{ _, Q }}) -∗ *)
(* (Q -∗ REL #() << fill K (#() : expr) : ()) -∗ *)
(* REL (e1 ∥ e2) << fill K t : (). *)
(* Proof. *)
(* iIntros "He1 He2 Ht". *)
(* rel_pures_l. rel_rec_l. *)
(* rel_pures_l. *)
(* pose (N:=nroot.@"par"). *)
(* rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj". *)
(* iModIntro. wp_bind (spawn _). *)
(* iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]"). *)
(* - wp_pures. wp_bind e1. *)
(* rewrite -fill_app. *)
(* iMod ("He1" with "Hspec Hj") as "He1". *)
(* iApply (wp_wand with "He1"). *)
(* iIntros (?) "P". wp_pures. *)
(* by iDestruct "P" as (v') "[Hj [-> ->]]". *)
(* - iNext. iIntros (l) "hndl". iSimpl. *)
(* wp_pures. wp_bind e2. *)
(* iApply (wp_wand with "He2"). iIntros (?) "HQ". *)
(* wp_pures. *)
(* wp_apply (join_spec with "hndl"). *)
(* iIntros (?) "Hj". *)
(* iSpecialize ("Ht" with "HQ"). *)
(* rewrite refines_eq /refines_def. *)
(* rewrite fill_app. *)
(* iMod ("Ht" with "Hspec Hj") as "Ht". *)
(* rewrite wp_value_inv. iMod "Ht" as (?) "[Ht [_ ->]]". *)
(* wp_pures. iExists #(). eauto with iFrame. *)
(* Qed. *)
Lemma par_l_1' Q K e1 e2 t :
(REL e1 << t : ()) -
(WP e2 {{ _, Q }}) -
(Q - REL #() << fill K (#() : expr) : ()) -
REL (e1 e2) << fill K t : ().
Proof.
iIntros "He1 He2 Ht".
rel_pures_l. rel_rec_l.
rel_pures_l.
pose (N:=nroot.@"par").
iApply refines_split. iIntros (k) "Hk".
rel_bind_l (spawn _). iApply refines_wp_l.
rewrite refines_right_bind.
iApply (spawn_spec N (λ _, refines_right k (fill K #()))%I with "[He1 Hk]").
- wp_pures. wp_bind e1.
rewrite refines_eq /refines_def.
iAssert (spec_ctx) with "[Hk]" as "#Hs".
{ iDestruct "Hk" as "[$ _]". }
iMod ("He1" with "Hk") as "He1".
iApply (wp_wand with "He1").
iIntros (?) "P". wp_pures.
rewrite /refines_right.
iDestruct "P" as (v') "[Hj [-> ->]]".
iFrame "Hs". by rewrite fill_app.
- iNext. iIntros (l) "Hl". simpl.
rel_pures_l. rel_bind_l e2.
iApply refines_wp_l.
iApply (wp_wand with "He2"). iIntros (?) "HQ".
simpl. rel_pures_l. rel_bind_l (spawn.join _).
iApply refines_wp_l.
wp_apply (join_spec with "Hl").
iIntros (?) "Hk".
iSpecialize ("Ht" with "HQ"). simpl.
rel_pures_l. iApply (refines_combine with "Ht Hk").
Qed.
(* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
(* ↑ relocN ⊆ E → *)
......@@ -209,14 +212,17 @@ Section rules.
tp_pure i (App _ _). simpl.
rel_pures_r.
rel_bind_r e2.
iApply refines_spec_ctx. iIntros "#Hs".
iApply (par_l_1' (i (#c2 <- InjR (#();; #())))%I
iApply (par_l_1' (refines_right i (#c2 <- InjR (#();; #())))%I
with "He2 [He1 Hi]").
{ rewrite refines_eq /refines_def.
tp_bind i e1.
iMod ("He1" with "Hs Hi") as "He1". simpl.
rewrite refines_right_bind.
iAssert (spec_ctx) with "[Hi]" as "#Hs".
{ iDestruct "Hi" as "[$ _]". }
iMod ("He1" with "Hi") as "He1". simpl.
iApply (wp_wand with "He1"). iIntros (?).
iDestruct 1 as (?) "[Hi [-> ->]]". done. }
iDestruct 1 as (?) "[Hi [-> ->]]".
rewrite /refines_right. by iFrame. }
iIntros "Hi". simpl. rel_pures_r.
tp_pures i. tp_store i.
rel_rec_r. rel_load_r. rel_pures_r. rel_values.
......
......@@ -47,7 +47,9 @@ Section refinement.
Lemma ticket_nondup γ n : ticket γ n - ticket γ n - False.
Proof.
iIntros "Ht1 Ht2".
iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
iDestruct (own_valid_2 with "Ht1 Ht2") as %Hfoo.
revert Hfoo. rewrite -auth_frag_op auth_frag_valid.
intros ?%gset_disj_valid_op.
set_solver.
Qed.
......
......@@ -232,7 +232,7 @@ Section proofs.
iDestruct "Hx'" as "[Hx' Hx'1]".
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
{ iCombine "Hx Hx1" as "Hx".
iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
{ iNext. iExists (S n).
......@@ -244,7 +244,7 @@ Section proofs.
iDestruct (mapsto_agree with "Hx Hx1") as %->.
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
{ iCombine "Hx Hx1" as "Hx".
iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
rel_store_r.
......
......@@ -83,12 +83,6 @@ Definition CG_mkstack : val := λ: <>,
value that is being offered and a potential thread with the
continuation that accepts the offer, if it is present. *)
Canonical Structure ectx_itemO := leibnizO ectx_item.
(* TODO: move !! *)
Canonical Structure ref_idO := leibnizO ref_id.
Global Instance ref_id_inhabited : Inhabited ref_id.
Proof. split. apply (RefId 0 []). Qed.
Definition offerReg := gmap loc (val * gname * ref_id).
Definition offerRegR :=
gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
......
......@@ -37,7 +37,7 @@ Section rules.
is_offer γ1 l P1 Q1 - is_offer γ2 l P2 Q2 - False.
Proof.
iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %?. contradiction.
iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[? _]. contradiction.
Qed.
Lemma make_is_offer γ l P Q : l #0 - P - is_offer γ l P Q.
......
......@@ -53,6 +53,16 @@ End lrel_ofe.
Arguments lrelC : clear implicits.
Record ref_id := RefId {
tp_id : nat;
tp_ctx : list ectx_item }.
Canonical Structure ectx_itemO := leibnizO ectx_item.
Canonical Structure ref_idO := leibnizO ref_id.
Global Instance ref_id_inhabited : Inhabited ref_id.
Proof. split. apply (RefId 0 []). Qed.
Section semtypes.
Context `{relocG Σ}.
......@@ -60,10 +70,6 @@ Section semtypes.
Implicit Types E : coPset.
Implicit Types A B : lrel Σ.
Record ref_id := RefId {
tp_id : nat;
tp_ctx : list ectx_item }.
Definition rhs_t := sum expr ref_id.
Definition in_1 : expr -> rhs_t := inl.
Definition in_2 : ref_id -> rhs_t := inr.
......@@ -187,7 +193,7 @@ Section semtypes_properties.
iInv (relocN.@"ref".@(l, l1')) as (? ?) "[>Hl ?]" "Hcl".
iInv (relocN.@"ref".@(l, l2')) as (? ?) "[>Hl' ?]" "Hcl'".
simpl. iExFalso.
iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
compute in Hfoo. eauto.
Qed.
......
......@@ -168,7 +168,8 @@ Section mapsto.
rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
f_equiv=> /=.
rewrite -pair_op singleton_op right_id -pair_op.
move=> [_ Hv]. move:Hv => /=.
rewrite auth_frag_valid pair_valid.
intros [_ Hv]. move:Hv => /=.
rewrite singleton_valid.
by move=> [_] /to_agree_op_inv_L [->].
Qed.
......
(** Autosubst helper lemmata *)
From Autosubst Require Export Autosubst.
From iris.algebra Require Export base.
From iris.prelude Require Export prelude.
Section Autosubst_Lemmas.
Context {term : Type} {Ids_term : Ids term}
......
Supports Markdown
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