Commit e9cfcda6 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung

Use `iAsimpl` more widely.

parent 45fa0a9c
Pipeline #9979 passed with stage
in 5 minutes and 21 seconds
...@@ -165,7 +165,7 @@ Section CG_Counter. ...@@ -165,7 +165,7 @@ Section CG_Counter.
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iMod (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto. iMod (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ by iFrame "Hspec Hj". } { by iFrame "Hspec Hj". }
iModIntro. by iFrame "Hj Hx". iModIntro. by iFrame "Hj Hx".
...@@ -264,12 +264,12 @@ Section CG_Counter. ...@@ -264,12 +264,12 @@ Section CG_Counter.
iMod (steps_newlock _ _ j ((AppRCtx (RecV _)) :: K) _ with "[Hj]") iMod (steps_newlock _ _ j ((AppRCtx (RecV _)) :: K) _ with "[Hj]")
as (l) "[Hj Hl]"; eauto. as (l) "[Hj Hl]"; eauto.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=. iAsimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
iMod (step_alloc _ _ j ((AppRCtx (RecV _)) :: K) _ _ _ _ with "[Hj]") iMod (step_alloc _ _ j ((AppRCtx (RecV _)) :: K) _ _ _ _ with "[Hj]")
as (cnt') "[Hj Hcnt']"; eauto. as (cnt') "[Hj Hcnt']"; eauto.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst /=. iAsimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end. all: try match goal with |- to_val _ = _ => auto using to_of_val end.
...@@ -284,7 +284,7 @@ Section CG_Counter. ...@@ -284,7 +284,7 @@ Section CG_Counter.
iApply fupd_wp. iApply fupd_wp.
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; [iNext; iExact "Hinv"|]. iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; [iNext; iExact "Hinv"|].
(* splitting increment and read *) (* splitting increment and read *)
iApply wp_pure_step_later; trivial. iModIntro. iNext. asimpl. iApply wp_pure_step_later; trivial. iModIntro. iNext. iAsimpl.
rewrite counter_read_subst /=. rewrite counter_read_subst /=.
iApply wp_value; auto. iApply wp_value; auto.
iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl. iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl.
...@@ -296,7 +296,7 @@ Section CG_Counter. ...@@ -296,7 +296,7 @@ Section CG_Counter.
rewrite CG_locked_increment_of_val /=. rewrite CG_locked_increment_of_val /=.
destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=. destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=.
iLöb as "Hlat". iLöb as "Hlat".
iApply wp_pure_step_later; trivial. asimpl. iNext. iApply wp_pure_step_later; trivial. iAsimpl. iNext.
(* fine-grained reads the counter *) (* fine-grained reads the counter *)
iApply (wp_bind (fill [AppRCtx (RecV _)])); iApply (wp_bind (fill [AppRCtx (RecV _)]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
...@@ -306,7 +306,7 @@ Section CG_Counter. ...@@ -306,7 +306,7 @@ Section CG_Counter.
iModIntro. iNext. iIntros "Hcnt". iModIntro. iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']"). iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
iApply wp_pure_step_later; trivial. asimpl. iModIntro. iNext. iApply wp_pure_step_later; trivial. iAsimpl. iModIntro. iNext.
(* fine-grained performs increment *) (* fine-grained performs increment *)
iApply (wp_bind (fill [CasRCtx (LocV _) (NatV _); IfCtx _ _])); iApply (wp_bind (fill [CasRCtx (LocV _) (NatV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|]. iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
......
...@@ -135,24 +135,24 @@ Section proof. ...@@ -135,24 +135,24 @@ Section proof.
Proof. Proof.
iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]". iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]".
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1. iAsimpl. rewrite H1.
iMod (steps_acquire _ _ j ((AppRCtx (RecV _)) :: K) iMod (steps_acquire _ _ j ((AppRCtx (RecV _)) :: K)
_ _ with "[Hj Hl]") as "[Hj Hl]"; eauto. _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
{ simpl. iFrame "Hspec Hj Hl"; eauto. } { simpl. iFrame "Hspec Hj Hl"; eauto. }
simpl. simpl.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite H1. iAsimpl. rewrite H1.
iMod (H2 ((AppRCtx (RecV _)) :: K) with "[Hj HP]") as "[Hj HQ]"; eauto. iMod (H2 ((AppRCtx (RecV _)) :: K) with "[Hj HP]") as "[Hj HQ]"; eauto.
{ simpl. iFrame "Hspec Hj HP"; eauto. } { simpl. iFrame "Hspec Hj HP"; eauto. }
simpl. simpl.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (steps_release _ _ j ((AppRCtx (RecV _)) :: K) _ _ with "[Hj Hl]") iMod (steps_release _ _ j ((AppRCtx (RecV _)) :: K) _ _ with "[Hj Hl]")
as "[Hj Hl]"; eauto. as "[Hj Hl]"; eauto.
{ simpl. by iFrame. } { simpl. by iFrame. }
rewrite ?fill_app /=. rewrite ?fill_app /=.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iModIntro; by iFrame. iAsimpl. iModIntro; by iFrame.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end. all: try match goal with |- to_val _ = _ => auto using to_of_val end.
trivial. trivial.
......
...@@ -83,7 +83,7 @@ Section CG_Stack. ...@@ -83,7 +83,7 @@ Section CG_Stack.
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_load _ _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K) iMod (step_load _ _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
simpl. iFrame "Hspec Hj"; trivial. simpl. simpl. iFrame "Hspec Hj"; trivial. simpl.
...@@ -177,7 +177,7 @@ Section CG_Stack. ...@@ -177,7 +177,7 @@ Section CG_Stack.
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K) iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K)
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
...@@ -187,7 +187,7 @@ Section CG_Stack. ...@@ -187,7 +187,7 @@ Section CG_Stack.
_ _ _ _ with "[Hj]") as "Hj"; eauto. _ _ _ _ with "[Hj]") as "Hj"; eauto.
simpl. simpl.
iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_snd _ _ j (StoreRCtx (LocV _) :: AppRCtx (RecV _) :: K) _ _ _ _ iMod (step_snd _ _ j (StoreRCtx (LocV _) :: AppRCtx (RecV _) :: K) _ _ _ _
_ _ with "[Hj]") as "Hj"; eauto. _ _ with "[Hj]") as "Hj"; eauto.
simpl. simpl.
...@@ -197,7 +197,7 @@ Section CG_Stack. ...@@ -197,7 +197,7 @@ Section CG_Stack.
iFrame "Hspec Hj"; trivial. iFrame "Hspec Hj"; trivial.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_fst _ _ j (InjRCtx :: K) _ _ _ _ _ _ iMod (step_fst _ _ j (InjRCtx :: K) _ _ _ _ _ _
with "[Hj]") as "Hj"; eauto. with "[Hj]") as "Hj"; eauto.
simpl. simpl.
...@@ -215,14 +215,14 @@ Section CG_Stack. ...@@ -215,14 +215,14 @@ Section CG_Stack.
Proof. Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop. iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K) iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K)
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
simpl. iFrame "Hspec Hj"; trivial. simpl. simpl. iFrame "Hspec Hj"; trivial. simpl.
iMod (step_Fold _ _ j (CaseCtx _ _ :: K) iMod (step_Fold _ _ j (CaseCtx _ _ :: K)
_ _ _ _ with "[Hj]") as "Hj"; eauto. _ _ _ _ with "[Hj]") as "Hj"; eauto.
iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iModIntro. iFrame "Hj Hx"; trivial. iModIntro. iFrame "Hj Hx"; trivial.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
...@@ -336,7 +336,7 @@ Section CG_Stack. ...@@ -336,7 +336,7 @@ Section CG_Stack.
with "[Hj Hx Hl]") as "Hj"; last done; [|iFrame; iFrame "#"]. with "[Hj Hx Hl]") as "Hj"; last done; [|iFrame; iFrame "#"].
iIntros (K') "[#Hspec [Hx Hj]]". iIntros (K') "[#Hspec [Hx Hj]]".
iMod (step_rec _ _ j K' _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K' _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_load _ _ j K' _ _ _ _ iMod (step_load _ _ j K' _ _ _ _
with "[Hj Hx]") as "[Hj Hx]"; eauto. with "[Hj Hx]") as "[Hj Hx]"; eauto.
- iFrame "#"; iFrame. - iFrame "#"; iFrame.
...@@ -405,12 +405,12 @@ Section CG_Stack. ...@@ -405,12 +405,12 @@ Section CG_Stack.
Proof. Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter. iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
rewrite -CG_iter_folding. Opaque CG_iter. asimpl. rewrite -CG_iter_folding. Opaque CG_iter. iAsimpl.
iMod (step_Fold _ _ j (CaseCtx _ _ :: K) iMod (step_Fold _ _ j (CaseCtx _ _ :: K)
_ _ _ with "[Hj]") as "Hj"; eauto. _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_fst _ _ j (AppRCtx f :: AppRCtx (RecV _) :: K) _ _ _ _ iMod (step_fst _ _ j (AppRCtx f :: AppRCtx (RecV _) :: K) _ _ _ _
_ _ with "[Hj]") as "Hj"; eauto. _ _ with "[Hj]") as "Hj"; eauto.
Unshelve. Unshelve.
...@@ -426,10 +426,10 @@ Section CG_Stack. ...@@ -426,10 +426,10 @@ Section CG_Stack.
Proof. Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter. iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
rewrite -CG_iter_folding. Opaque CG_iter. asimpl. rewrite -CG_iter_folding. Opaque CG_iter. iAsimpl.
iMod (step_Fold _ _ j (CaseCtx _ _ :: K) iMod (step_Fold _ _ j (CaseCtx _ _ :: K)
_ _ _ with "[Hj]") as "Hj"; eauto. _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iAsimpl.
iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto. iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
Unshelve. Unshelve.
all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end. all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
......
...@@ -8,18 +8,6 @@ From iris.proofmode Require Import tactics. ...@@ -8,18 +8,6 @@ From iris.proofmode Require Import tactics.
Definition stackN : namespace := nroot .@ "stack". Definition stackN : namespace := nroot .@ "stack".
Ltac iAsimpl :=
repeat match goal with
| |- context [ (_ ?e)%I ] => progress (
let e' := fresh "feed" in evar (e':expr);
assert (e = e') as ->; [asimpl; unfold e'; reflexivity|];
unfold e'; clear e')
| |- context [ WP ?e @ _ {{ _ }}%I ] => progress (
let e' := fresh "feed" in evar (e':expr);
assert (e = e') as ->; [asimpl; unfold e'; reflexivity|];
unfold e'; clear e')
end.
Section Stack_refinement. Section Stack_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}. Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
......
...@@ -48,6 +48,18 @@ Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v) ...@@ -48,6 +48,18 @@ Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope. Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope.
Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope. Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope.
Ltac iAsimpl :=
repeat match goal with
| |- context [ (_ ?e)%I ] => progress (
let e' := fresh in evar (e':expr);
assert (e = e') as ->; [asimpl; unfold e'; reflexivity|];
unfold e'; clear e')
| |- context [ WP ?e @ _ {{ _ }}%I ] => progress (
let e' := fresh in evar (e':expr);
assert (e = e') as ->; [asimpl; unfold e'; reflexivity|];
unfold e'; clear e')
end.
Section conversions. Section conversions.
Context `{cfgSG Σ}. Context `{cfgSG Σ}.
......
...@@ -31,7 +31,7 @@ Proof. ...@@ -31,7 +31,7 @@ Proof.
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). } { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
simpl. simpl.
rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []). rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
{ rewrite /tpool_mapsto. asimpl. by iFrame. } { rewrite /tpool_mapsto. iAsimpl. by iFrame. }
iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]". iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'. iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /=. rewrite /tpool_mapsto /=.
......
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