Skip to content

GitLab

Commit dad6c7ed authored by Amin Timany's avatar Amin Timany
Browse files
Options

Update to work with latest iris

parent b1515733
Show whitespace changes
Inline Side-by-side
Showing with 39 additions and 39 deletions
F_mu_ref/lang.v
View file @ dad6c7ed
......@@ -245,4 +245,4 @@ Ltac solve_atomic :=
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 0 (language.atomic _) => solve_atomic.
Hint Extern 0 (language.atomic _) => solve_atomic : atomic.
Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
F_mu_ref/rules.v
View file @ dad6c7ed
......@@ -96,7 +96,7 @@ Section lang_rules.
l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
{ by rewrite heap_mapsto_op_eq pure_True // left_id. }
apply (anti_symm (⊢)); last by apply pure_elim_l.
rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
eapply pure_elim; [done|] => /=.
......
F_mu_ref/rules_binary.v
View file @ dad6c7ed
......@@ -63,10 +63,10 @@ Section cfg.
Proof.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e2 σ) "[Hown %]".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K e'))). }
iFrame "Hj". iApply "Hclose". iNext. iExists (fill K e'), σ.
......@@ -80,10 +80,10 @@ Section cfg.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K (Loc l)))). }
iMod (own_update with "Hown") as "[Hown Hl]".
......@@ -104,12 +104,12 @@ Section cfg.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). }
iFrame "Hj Hl". iApply "Hclose". iNext.
......@@ -126,15 +126,15 @@ Section cfg.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
subst.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K Unit))). }
iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]".
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v)); last done.
by rewrite /to_heap lookup_fmap Hl. }
......
F_mu_ref/soundness_binary.v
View file @ dad6c7ed
......@@ -31,7 +31,7 @@ Proof.
iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e'' σ) "[Hown Hsteps]".
iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /auth.auth_own /=.
iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
iMod ("Hclose" with "[-]") as "_"; [iExists _, σ; auto|].
......
F_mu_ref_conc/lang.v
View file @ dad6c7ed
......@@ -312,4 +312,4 @@ Ltac solve_atomic :=
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 0 (language.atomic _) => solve_atomic.
Hint Extern 0 (language.atomic _) => solve_atomic : atomic.
Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
F_mu_ref_conc/rules.v
View file @ dad6c7ed
......@@ -96,7 +96,7 @@ Section lang_rules.
l ↦ᵢ{q1} v1 ∗ l ↦ᵢ{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦ᵢ{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
{ by rewrite heap_mapsto_op_eq pure_True // left_id. }
apply (anti_symm (⊢)); last by apply pure_elim_l.
rewrite heapI_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
eapply pure_elim; [done|] => /=.
......
F_mu_ref_conc/rules_binary.v
View file @ dad6c7ed
......@@ -137,9 +137,9 @@ Section cfg.
Proof.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). }
iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
......@@ -154,9 +154,9 @@ Section cfg.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). }
iMod (own_update with "Hown") as "[Hown Hl]".
......@@ -177,11 +177,11 @@ Section cfg.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). }
iFrame "Hj Hl". iApply "Hclose". iNext.
......@@ -198,14 +198,14 @@ Section cfg.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K Unit))). }
iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]".
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v)); last done.
by rewrite /to_heap lookup_fmap Hl. }
......@@ -223,11 +223,11 @@ Section cfg.
iIntros (????) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#♭ false)))). }
iFrame "Hj Hl". iApply "Hclose". iNext.
......@@ -244,14 +244,14 @@ Section cfg.
iIntros (????) "(#Hinv & Hj & Hl)"; subst.
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
iDestruct (own_valid_2 _ with "[$Hown $Hl]")
iDestruct (own_valid_2 _ with "Hown Hl")
as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#♭ true)))). }
iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]".
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v2)); last done.
by rewrite /to_heap lookup_fmap Hl. }
......@@ -321,13 +321,13 @@ Section cfg.
Proof.
iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 _ with "[$Hown $Hj]")
iDestruct (own_valid_2 _ with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
assert (j < length tp) by eauto using lookup_lt_Some.
iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]".
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K Unit))). }
iMod (own_update with "[$Hown]") as "[Hown Hfork]".
iMod (own_update with "Hown") as "[Hown Hfork]".
{ eapply auth_update_alloc, prod_local_update_1,
(alloc_singleton_local_update _ (length tp) (Excl e)); last done.
rewrite lookup_insert_ne ?tpool_lookup; last omega.
......
F_mu_ref_conc/soundness_binary.v
View file @ dad6c7ed
......@@ -30,7 +30,7 @@ Proof.
iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /auth.auth_own /=.
iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
......
README.md
View file @ dad6c7ed
......@@ -5,4 +5,4 @@ This version is known to compile with:
- Coq 8.5pl2
- Ssreflect 1.6
- Autosubst 1.5
- Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/2a7755f
- Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/a7e9167
\ No newline at end of file
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