Commit e7cc3560 authored by Robbert Krebbers's avatar Robbert Krebbers

Seal off tpool_mapsto and heapS_mapsto to speed up unification.

parent 9e4edf44
......@@ -24,24 +24,26 @@ Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
Section definitionsS.
Context `{cfgSG Σ, invG Σ}.
Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name ( (, {[ l := (q, to_agree v) ]})).
Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
Definition heapS_mapsto_eq :
@heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux.
Definition tpool_mapsto (j : nat) (e: expr) : iProp Σ :=
Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
own cfg_name ( ({[ j := Excl e ]}, )).
Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed.
Definition tpool_mapsto := proj1_sig tpool_mapsto_aux.
Definition tpool_mapsto_eq :
@tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
Definition spec_inv (ρ : cfg lang) : iProp Σ :=
( tp σ, own cfg_name ( (to_tpool tp, to_gen_heap σ))
rtc step ρ (tp,σ))%I.
Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
inv specN (spec_inv ρ).
Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
Proof. apply _. Qed.
Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
Proof. apply _. Qed.
End definitionsS.
Typeclasses Opaque heapS_mapsto tpool_mapsto.
Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
(at level 20, q at level 50, format "l ↦ₛ{ q } v") : uPred_scope.
......@@ -107,7 +109,6 @@ Section conversions.
Lemma tpool_singleton_included' tp j e :
{[j := Excl e]} to_tpool tp to_tpool tp !! j = Excl' e.
Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
End conversions.
Section cfg.
......@@ -124,6 +125,11 @@ Section cfg.
Local Hint Resolve to_tpool_insert'.
Local Hint Resolve tpool_singleton_included.
Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
Proof. rewrite heapS_mapsto_eq. apply _. Qed.
Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
Proof. apply _. Qed.
Lemma step_insert K tp j e σ e' σ' efs :
tp !! j = Some (fill K e) head_step e σ e' σ' efs
step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
......@@ -145,7 +151,7 @@ Section cfg.
nclose specN E
spec_ctx ρ j fill K e ={E}= j fill K e'.
Proof.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
......@@ -161,7 +167,7 @@ Section cfg.
to_val e = Some v nclose specN E
spec_ctx ρ j fill K (Alloc e) ={E}= l, j fill K (Loc l) l ↦ₛ v.
Proof.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
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].
iDestruct (own_valid_2 with "Hown Hj")
......@@ -173,7 +179,8 @@ Section cfg.
{ 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. iFrame "Hj Hl". iApply "Hclose". iNext.
iExists l. rewrite heapS_mapsto_eq /heapS_mapsto_def.
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (Loc 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.
......@@ -185,7 +192,7 @@ Section cfg.
={E}= j fill K (of_val v) l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
......@@ -205,7 +212,7 @@ Section cfg.
={E}= j fill K Unit l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
......@@ -230,7 +237,7 @@ Section cfg.
={E}= j fill K (# false) l ↦ₛ{q} v'.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
......@@ -251,7 +258,7 @@ Section cfg.
={E}= j fill K (# true) l ↦ₛ v2.
Proof.
iIntros (????) "(#Hinv & Hj & Hl)"; subst.
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
......@@ -334,7 +341,7 @@ Section cfg.
nclose specN E
spec_ctx ρ j fill K (Fork e) ={E}= j', j fill K Unit j' e.
Proof.
iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
......
......@@ -31,10 +31,10 @@ Proof.
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
simpl.
rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
{ rewrite /tpool_mapsto. asimpl. iFrame. }
{ rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /=.
rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [/tpool_singleton_included Hv2 _] _].
......
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