Commit c5f21766 authored by Ralf Jung's avatar Ralf Jung

fix for latest Iris

parent ddf3194b
......@@ -3,6 +3,7 @@
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
......
......@@ -66,7 +66,7 @@ Section proof.
Definition is_bag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname),
x = PairV #b lk is_lock N γ lk (bag_inv γb b))%I.
x = PairV #b lk is_lock γ lk (bag_inv γb b))%I.
Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
own γb ((1/2)%Qp, to_agree X).
......@@ -106,7 +106,7 @@ Section proof.
unfold newBag. wp_rec.
wp_alloc r as "Hr". wp_let.
iMod (own_alloc (1%Qp, to_agree )) as (γb) "[Ha Hf]"; first done.
wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]").
wp_apply (newlock_spec (bag_inv γb r) with "[Hr Ha]").
{ iExists []. iFrame. }
iIntros (lk γ) "#Hlk". wp_pures. iApply "HΦ".
rewrite /is_bag /bag_contents. iFrame.
......@@ -176,11 +176,11 @@ End proof.
Typeclasses Opaque bag_contents is_bag.
Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ :=
{| abstract_bag.is_bag := is_bag;
abstract_bag.is_bag_persistent := is_bag_persistent;
{| abstract_bag.is_bag N := is_bag;
abstract_bag.is_bag_persistent N := is_bag_persistent;
abstract_bag.bag_contents_timeless := bag_contents_timeless;
abstract_bag.bag_contents_agree := bag_contents_agree;
abstract_bag.bag_contents_update := bag_contents_update;
abstract_bag.newBag_spec := newBag_spec;
abstract_bag.newBag_spec N := newBag_spec;
abstract_bag.pushBag_spec := pushBag_spec;
abstract_bag.popBag_spec := popBag_spec |}.
......@@ -212,7 +212,7 @@ Section proof.
Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
inv N (srv_bag R γm γr s)
is_lock N γlk lk (own γr (Excl ()) R) Φ #()
is_lock γlk lk (own γr (Excl ()) R) Φ #()
WP try_srv lk #s {{ Φ }}.
Proof.
iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
......@@ -237,7 +237,7 @@ Section proof.
Lemma loop_spec R (p s: loc) (lk: val)
(γs γr γm γlk: gname) (ts: toks):
{{{ inv N (srv_bag R γm γr s) inv N (p_inv R γm γr ts p)
is_lock N γlk lk (own γr (Excl ()) R) own_γ3 ts }}}
is_lock γlk lk (own γr (Excl ()) R) own_γ3 ts }}}
loop #p #s lk
{{{ x y, RET y; finished_recp ts x y }}}.
Proof.
......@@ -272,7 +272,7 @@ Section proof.
iIntros (R Φ) "HR HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
wp_lam. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//.
iApply (newlock_spec (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _).
iApply (new_bag_spec N (p_inv' R γm γr))=>//.
......
......@@ -17,13 +17,13 @@ Definition mk_sync: val :=
"ret".
Section syncer.
Context `{!heapG Σ, !lockG Σ} (N: namespace).
Context `{!heapG Σ, !lockG Σ}.
Lemma mk_sync_spec: mk_syncer_spec mk_sync.
Proof.
iIntros (R Φ) "HR HΦ".
wp_lam. wp_bind (newlock _).
iApply (newlock_spec N R with "[HR]"); first done. iNext.
iApply (newlock_spec R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf !# HP".
......
......@@ -436,7 +436,7 @@ Lemma use_val_wit γs slots i l :
val_of <$> slots !! i = Some l.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
inversion_clear H1; rename H into H1.
......@@ -466,7 +466,7 @@ Lemma use_name_tok γs slots i γ :
name_of <$> slots !! i = Some (Some γ).
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
inversion_clear H1; rename H into H1.
......@@ -532,7 +532,7 @@ Lemma use_committed_wit γs slots i :
was_committed <$> slots !! i = Some true.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
inversion_clear H1; rename H into H1.
......@@ -555,7 +555,7 @@ Lemma use_written_wit γs slots i :
was_written <$> slots !! i = Some true.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
inversion_clear H1; rename H into H1.
......@@ -580,7 +580,7 @@ Proof.
iDestruct (own_valid with "H") as %Hvalid.
iApply (own_update with "H").
apply auth_both_valid in Hvalid as [H1 H2].
apply singleton_included in H1 as [e (H1_1 & H1_2)].
apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
rewrite lookup_fmap in H1_1.
destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
apply Some_equiv_inj in H1_1.
......@@ -611,7 +611,7 @@ Proof.
iIntros "Hs● Htok". iCombine "Hs● Htok" as "H".
iDestruct (own_valid with "H") as %Hvalid%auth_both_valid.
iPureIntro. destruct Hvalid as [H1 H2].
apply singleton_included in H1 as [e (H1_1 & H1_2)].
apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
rewrite lookup_fmap in H1_1.
destruct (slots !! i) as [[[l s] w]|]; last by inversion H1_1.
apply Some_equiv_inj in H1_1. simpl. f_equal. destruct w; last done.
......@@ -641,7 +641,7 @@ Proof.
rewrite -own_op. iDestruct (own_valid with "H") as %Hvalid.
iApply (own_update with "H").
apply auth_both_valid in Hvalid as [H1 H2].
apply singleton_included in H1 as [e (H1_1 & H1_2)].
apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
rewrite lookup_fmap in H1_1.
destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
simpl in Hlookup. inversion Hlookup; subst s.
......@@ -699,7 +699,7 @@ Proof.
apply auth_update_core_id; first apply _.
assert ( d, slots !! i = Some d) as [d Hlookup].
{ destruct (slots !! i) as [d|]; inversion H. by exists d. }
apply singleton_included. rewrite lookup_fmap. rewrite Hlookup /=.
apply singleton_included_l. rewrite lookup_fmap. rewrite Hlookup /=.
exists (of_slot_data d). split; first done.
apply Some_included. right. destruct d as [[dl ds] dw]. simpl.
repeat (apply prod_included; split; simpl);
......
......@@ -100,7 +100,7 @@ Section to_gc_map.
Lemma gc_map_singleton_included gcm l v :
{[l := Some (Excl v)]} to_gc_map gcm gcm !! l = Some v.
Proof.
rewrite singleton_included.
rewrite singleton_included_l.
setoid_rewrite Some_included_total.
intros (y & Hsome & Hincluded).
pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
......@@ -180,7 +180,7 @@ Section gc.
iDestruct (own_valid with "Hcomb") as %Hvalid.
iPureIntro.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
setoid_rewrite singleton_included in Hincluded.
setoid_rewrite singleton_included_l in Hincluded.
destruct Hincluded as (y & Hsome & _).
eapply lookup_to_gc_map_Some_2.
by apply leibniz_equiv_iff in Hsome.
......
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