Commit 65393b24 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris and get rid of more forced notation scopes.

parent aee54795
......@@ -6,7 +6,7 @@ This version is known to compile with:
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee)
- Iris version [978965301130a145155e03e4858eef3f86f2c705](https://gitlab.mpi-sws.org/FP/iris-coq/tree/978965301130a145155e03e4858eef3f86f2c705)
- Iris version [f96a894b14fe7095bb5ac5b937abd31e40316858](https://gitlab.mpi-sws.org/FP/iris-coq/tree/f96a894b14fe7095bb5ac5b937abd31e40316858)
# Compilation
......
......@@ -119,7 +119,7 @@ Section CG_Counter.
(Hspec : nclose specN E1) :
x ↦ₛ #n -
(x ↦ₛ #n - {E1,E2;Δ;Γ} t log fill K #n : τ) -
{E1,E2;Δ;Γ} t log fill K ((counter_read $/ LitV (Loc x)) #())%E : τ.
{E1,E2;Δ;Γ} t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
Proof.
iIntros "Hx Hlog".
unfold counter_read. unlock. simpl.
......@@ -136,7 +136,7 @@ Section CG_Counter.
(( n : nat, x ↦ᵢ #n R n) ={E2,E1}= True)
( m, x ↦ᵢ # (S m) R m -
{E2,E1;Δ;Γ} fill K #() log t : τ))
- ({E1,E1;Δ;Γ} fill K ((FG_increment $/ LitV (Loc x)) #())%E log t : τ).
- ({E1,E1;Δ;Γ} fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
Proof.
iIntros "#H".
unfold FG_increment. unlock. simpl.
......@@ -178,7 +178,7 @@ Section CG_Counter.
(( n : nat, x ↦ᵢ #n R n) ={E2,E1}= True)
( m : nat, x ↦ᵢ #m R m -
{E2,E1;Δ;Γ} fill K #m log t : τ))
- {E1,E1;Δ;Γ} fill K ((counter_read $/ LitV (Loc x)) #())%E log t : τ.
- {E1,E1;Δ;Γ} fill K ((counter_read $/ LitV (Loc x)) #()) log t : τ.
Proof.
iIntros "#H".
unfold counter_read. unlock. simpl.
......
......@@ -72,7 +72,7 @@ Section Refinement.
choiceN E1
spec_ctx ρ -
{E1,E2;Δ;Γ} t log fill K #b : τ -
{E1,E2;Δ;Γ} t log fill K (rand #())%E : τ.
{E1,E2;Δ;Γ} t log fill K (rand #()) : τ.
Proof.
iIntros (??) "#Hs Hlog".
unfold rand. unlock.
......
......@@ -103,7 +103,7 @@ Section proof.
Lemma steps_release ρ j K l (b : bool)
(Hcl : nclose specN E1) :
spec_ctx ρ - l ↦ₛ #b - j fill K (release #l)
={E1}= j fill K (#())%E l ↦ₛ #false.
={E1}= j fill K #() l ↦ₛ #false.
Proof.
iIntros "#Hspec Hl Hj". unfold release. unlock.
tp_rec j.
......
......@@ -442,7 +442,7 @@ Lemma tac_rel_cas_fail_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) e t
v v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) 1 = Some 2
tres = fill K (#false)%E
tres = fill K #false
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
......@@ -478,7 +478,7 @@ Lemma tac_rel_cas_suc_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) e t e
v = v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v2)%I) 1 = Some 2
tres = fill K (# true)%E
tres = fill K # true
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
......
......@@ -236,7 +236,7 @@ Lemma tac_tp_cas_fail `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I
v' v1
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j fill K' (# false)%E)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3
(Esnoc (Esnoc Enil i2 (j fill K' #false)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3
(Δ3 |={E1,E2}=> Q)
(Δ1 |={E1,E2}=> Q).
Proof.
......@@ -287,7 +287,7 @@ Lemma tac_tp_cas_suc `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1 e
envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I
v' = v1
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j fill K' (# true)%E)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3
(Esnoc (Esnoc Enil i2 (j fill K' #true)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3
(Δ3 |={E1,E2}=> Q)
(Δ1 |={E1,E2}=> Q).
Proof.
......
......@@ -53,10 +53,10 @@ Section properties.
iFrame "Hj". iAlways. iIntros ([v1 v2]) "Hvv".
iSpecialize ("H" $! v1 v2 with "Hvv Hs []").
{ iAlways. iApply "HΓ". }
assert (Closed ((rec: f x := eb) v1)%E).
assert (Closed ((rec: f x := eb) v1)).
{ unfold Closed in *. simpl.
intros. split_and?; auto. apply of_val_closed. }
assert (Closed ((rec: f' x' := eb') v2)%E).
assert (Closed ((rec: f' x' := eb') v2)).
{ unfold Closed in *. simpl.
intros. split_and?; auto. apply of_val_closed. }
rewrite /env_subst. rewrite !Closed_subst_p_id. done.
......@@ -442,8 +442,8 @@ Section properties.
Lemma bin_log_related_store_l Δ Γ E1 E2 K l e v' t τ :
to_val e = Some v'
(|={E1,E2}=> v, l ↦ᵢ v
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K (#())%E log t : τ))
- {E1,E1;Δ;Γ} fill K (#l <- e)%E log t : τ.
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K #() log t : τ))
- {E1,E1;Δ;Γ} fill K (#l <- e) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply bin_log_related_wp_atomic_l; auto.
......@@ -454,7 +454,7 @@ Section properties.
Lemma bin_log_related_store_l' Δ Γ E K l e v v' t τ :
(to_val e = Some v')
(l ↦ᵢ v) -
(l ↦ᵢ v' - {E,E;Δ;Γ} fill K (#())%E log t : τ)
(l ↦ᵢ v' - {E,E;Δ;Γ} fill K #() log t : τ)
- {E,E;Δ;Γ} fill K (#l <- e) log t : τ.
Proof.
iIntros (?) "Hl Hlog".
......
......@@ -60,30 +60,30 @@ Section rules.
Lemma step_alloc E ρ j K e v:
to_val e = Some v nclose specN E
spec_ctx ρ j fill K (ref e)%E ={E}= l, j fill K (#l)%E l ↦ₛ v.
spec_ctx ρ j fill K (ref e) ={E}= l, j fill K #l l ↦ₛ v.
Proof.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
destruct (exist_fresh (dom (gset loc) σ)) as [l Hl%not_elem_of_dom].
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]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit (Loc l))))). }
singleton_local_update, (exclusive_local_update _ (Excl (fill K #l))). }
iMod (own_update with "Hown") as "[Hown Hl]".
{ eapply auth_update_alloc, prod_local_update_2,
(alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
by apply lookup_to_gen_heap_None. }
iExists l. rewrite heapS_mapsto_eq /heapS_mapsto_def.
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (Lit (Loc l))]> tp), (<[l:=v]>σ).
iExists (<[j:=fill K #l]> tp), (<[l:=v]>σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_load E ρ j K l q v:
nclose specN E
spec_ctx ρ j fill K (! #l)%E l ↦ₛ{q} v
spec_ctx ρ j fill K (! #l) l ↦ₛ{q} v
={E}= j fill K (v : expr) l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
......@@ -103,8 +103,8 @@ Section rules.
Lemma step_store E ρ j K l v' e v:
to_val e = Some v nclose specN E
spec_ctx ρ j fill K (#l <- e)%E l ↦ₛ v'
={E}= j fill K (#())%E l ↦ₛ v.
spec_ctx ρ j fill K (#l <- e) l ↦ₛ v'
={E}= j fill K #() l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
......@@ -115,21 +115,21 @@ Section rules.
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
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))). }
(exclusive_local_update _ (Excl (fill K #()))). }
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, to_agree v)); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (#())%E]> tp), (<[l:=v]>σ).
iExists (<[j:=fill K #()]> tp), (<[l:=v]>σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_cas_fail E ρ j K l q v' e1 v1 e2 v2:
to_val e1 = Some v1 to_val e2 = Some v2 nclose specN E v' v1
spec_ctx ρ j fill K (CAS (# l) e1 e2) l ↦ₛ{q} v'
={E}= j fill K (# false)%E l ↦ₛ{q} v'.
spec_ctx ρ j fill K (CAS #l e1 e2) l ↦ₛ{q} v'
={E}= j fill K #false l ↦ₛ{q} v'.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
......@@ -140,17 +140,17 @@ Section rules.
as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
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)%E))). }
(exclusive_local_update _ (Excl (fill K #false))). }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (# false)%E]> tp), σ.
iExists (<[j:=fill K #false]> tp), σ.
rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_cas_suc E ρ j K l e1 v1 v1' e2 v2:
to_val e1 = Some v1 to_val e2 = Some v2 nclose specN E v1 = v1'
spec_ctx ρ j fill K (CAS (# l) e1 e2) l ↦ₛ v1'
={E}= j fill K (# true)%E l ↦ₛ v2.
spec_ctx ρ j fill K (CAS #l e1 e2) l ↦ₛ v1'
={E}= j fill K #true l ↦ₛ v2.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)"; subst.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
......@@ -161,13 +161,13 @@ Section rules.
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
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)%E))). }
(exclusive_local_update _ (Excl (fill K #true))). }
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, to_agree v2)); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (# true)%E]> tp), (<[l:=v2]>σ).
iExists (<[j:=fill K #true]> tp), (<[l:=v2]>σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
......@@ -241,7 +241,7 @@ Section rules.
Lemma step_fork E ρ j K e :
nclose specN E
spec_ctx ρ j fill K (Fork e) ={E}= j', j fill K (#())%E j' e.
spec_ctx ρ j fill K (Fork e) ={E}= j', j fill K #() j' e.
Proof.
iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
......@@ -250,14 +250,14 @@ Section rules.
assert (j < length tp) by eauto using lookup_lt_Some.
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))). }
singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
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.
by rewrite lookup_ge_None_2. }
iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
iExists (<[j:=fill K (#())%E]> tp ++ [e]), σ.
iExists (<[j:=fill K #()]> tp ++ [e]), σ.
rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
eapply rtc_r, step_insert; eauto. econstructor; eauto.
Qed.
......
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