Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Paolo G. Giarrusso
examples
Commits
fcd5c1de
Commit
fcd5c1de
authored
Jun 04, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Get rid of `ρ` argument of `spec_ctx`.
parent
d4f41539
Changes
8
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
208 additions
and
203 deletions
+208
-203
theories/logrel/F_mu_ref_conc/examples/counter.v
theories/logrel/F_mu_ref_conc/examples/counter.v
+15
-15
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel/F_mu_ref_conc/examples/fact.v
+11
-11
theories/logrel/F_mu_ref_conc/examples/lock.v
theories/logrel/F_mu_ref_conc/examples/lock.v
+15
-15
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+34
-34
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+7
-7
theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/logrel/F_mu_ref_conc/fundamental_binary.v
+67
-67
theories/logrel/F_mu_ref_conc/rules_binary.v
theories/logrel/F_mu_ref_conc/rules_binary.v
+55
-52
theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/logrel/F_mu_ref_conc/soundness_binary.v
+4
-2
No files found.
theories/logrel/F_mu_ref_conc/examples/counter.v
View file @
fcd5c1de
...
...
@@ -60,21 +60,21 @@ Section CG_Counter.
Hint
Rewrite
CG_increment_subst
:
autosubst
.
Lemma
steps_CG_increment
E
ρ
j
K
x
n
:
Lemma
steps_CG_increment
E
j
K
x
n
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
x
↦ₛ
(#
nv
n
)
∗
j
⤇
fill
K
(
App
(
CG_increment
(
Loc
x
))
Unit
)
spec_ctx
∗
x
↦ₛ
(#
nv
n
)
∗
j
⤇
fill
K
(
App
(
CG_increment
(
Loc
x
))
Unit
)
⊢
|={
E
}=>
j
⤇
fill
K
(
Unit
)
∗
x
↦ₛ
(#
nv
(
S
n
)).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx Hj]]"
.
unfold
CG_increment
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
step_load
_
_
j
((
BinOpRCtx
_
(#
nv
_
)
::
StoreRCtx
(
LocV
_
)
::
K
))
iMod
(
step_load
_
j
((
BinOpRCtx
_
(#
nv
_
)
::
StoreRCtx
(
LocV
_
)
::
K
))
_
_
_
with
"[Hj Hx]"
)
as
"[Hj Hx]"
;
eauto
.
{
iFrame
"Hspec Hj"
;
trivial
.
}
simpl
.
iMod
(
do_step_pure
_
_
_
((
StoreRCtx
(
LocV
_
))
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
iMod
(
do_step_pure
_
_
((
StoreRCtx
(
LocV
_
))
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iMod
(
step_store
_
_
j
K
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
iMod
(
step_store
_
j
K
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
iModIntro
;
iFrame
.
Qed
.
...
...
@@ -108,15 +108,15 @@ Section CG_Counter.
Hint
Rewrite
CG_locked_increment_subst
:
autosubst
.
Lemma
steps_CG_locked_increment
E
ρ
j
K
x
n
l
:
Lemma
steps_CG_locked_increment
E
j
K
x
n
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
x
↦ₛ
(#
nv
n
)
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
x
↦ₛ
(#
nv
n
)
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
CG_locked_increment
(
Loc
x
)
(
Loc
l
))
Unit
)
={
E
}=
∗
j
⤇
fill
K
Unit
∗
x
↦ₛ
(#
nv
S
n
)
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
iMod
(
steps_with_lock
_
_
j
K
_
_
_
_
UnitV
UnitV
with
"[$Hj Hx $Hl]"
)
as
"Hj"
;
eauto
.
_
j
K
_
_
_
_
UnitV
UnitV
with
"[$Hj Hx $Hl]"
)
as
"Hj"
;
eauto
.
-
iIntros
(
K'
)
"[#Hspec Hxj]"
.
iApply
steps_CG_increment
;
by
try
iFrame
.
-
by
iFrame
.
...
...
@@ -151,16 +151,16 @@ Section CG_Counter.
Hint
Rewrite
counter_read_subst
:
autosubst
.
Lemma
steps_counter_read
E
ρ
j
K
x
n
:
Lemma
steps_counter_read
E
j
K
x
n
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
x
↦ₛ
(#
nv
n
)
spec_ctx
∗
x
↦ₛ
(#
nv
n
)
∗
j
⤇
fill
K
(
App
(
counter_read
(
Loc
x
))
Unit
)
={
E
}=
∗
j
⤇
fill
K
(#
n
n
)
∗
x
↦ₛ
(#
nv
n
).
Proof
.
intros
HNE
.
iIntros
"[#Hspec [Hx Hj]]"
.
unfold
counter_read
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
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
.
Qed
.
...
...
@@ -247,17 +247,17 @@ Section CG_Counter.
Lemma
FG_CG_counter_refinement
:
[]
⊨
FG_counter
≤
log
≤
CG_counter
:
TProd
(
TArrow
TUnit
TUnit
)
(
TArrow
TUnit
TNat
).
Proof
.
iIntros
(
Δ
[|??]
ρ
?)
"#(Hspec & HΓ)"
;
iIntros
(
j
K
)
"Hj"
;
last
first
.
iIntros
(
Δ
[|??]
?)
"#(Hspec & HΓ)"
;
iIntros
(
j
K
)
"Hj"
;
last
first
.
{
iDestruct
(
interp_env_length
with
"HΓ"
)
as
%[=].
}
iClear
"HΓ"
.
cbn
-[
FG_counter
CG_counter
].
rewrite
?empty_env_subst
/
CG_counter
/
FG_counter
.
iApply
fupd_wp
.
iMod
(
steps_newlock
_
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
iMod
(
steps_newlock
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
as
(
l
)
"[Hj Hl]"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
step_alloc
_
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
iMod
(
step_alloc
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
as
(
cnt'
)
"[Hj Hcnt']"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
...
...
@@ -308,7 +308,7 @@ Section CG_Counter.
+
(* CAS succeeds *)
(* In this case, we perform increment in the coarse-grained one *)
iMod
(
steps_CG_locked_increment
_
_
_
_
_
_
_
_
with
"[Hj Hl Hcnt']"
)
as
"[Hj [Hcnt' Hl]]"
.
_
_
_
_
_
_
_
with
"[Hj Hl Hcnt']"
)
as
"[Hj [Hcnt' Hl]]"
.
{
iFrame
"Hspec Hcnt' Hl Hj"
;
trivial
.
}
iApply
(
wp_cas_suc
with
"[Hcnt]"
)
;
auto
.
iModIntro
.
iNext
.
iIntros
"Hcnt"
.
...
...
theories/logrel/F_mu_ref_conc/examples/fact.v
View file @
fcd5c1de
...
...
@@ -68,7 +68,7 @@ Section fact_equiv.
Lemma
fact_fact_acc_refinement
:
[]
⊨
fact
≤
log
≤
fact_acc
:
(
TArrow
TNat
TNat
).
Proof
.
iIntros
(?
vs
ρ
_
)
"[#HE HΔ]"
.
iIntros
(?
vs
_
)
"[#HE HΔ]"
.
iDestruct
(
interp_env_length
with
"HΔ"
)
as
%?
;
destruct
vs
;
simplify_eq
.
iClear
"HΔ"
.
simpl
.
iIntros
(
j
K
)
"Hj"
;
simpl
.
...
...
@@ -87,7 +87,7 @@ Section fact_equiv.
-
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
;
asimpl
.
rewrite
fact_acc_body_unfold
.
iMod
(
do_step_pure
_
_
_
(
AppLCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
AppLCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
rewrite
-
fact_acc_body_unfold
.
simpl
;
asimpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
...
...
@@ -95,7 +95,7 @@ Section fact_equiv.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
iApply
wp_value
.
simpl
.
iMod
(
do_step_pure
_
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
...
...
@@ -106,7 +106,7 @@ Section fact_equiv.
-
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
;
asimpl
.
rewrite
fact_acc_body_unfold
.
iMod
(
do_step_pure
_
_
_
(
AppLCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
AppLCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
rewrite
-
fact_acc_body_unfold
.
simpl
;
asimpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
...
...
@@ -114,7 +114,7 @@ Section fact_equiv.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
iApply
wp_value
.
simpl
.
iMod
(
do_step_pure
_
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
...
...
@@ -124,11 +124,11 @@ Section fact_equiv.
iApply
(
wp_bind
(
fill
[
AppRCtx
(
RecV
_
)])).
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
;
iApply
wp_value
;
simpl
.
iMod
(
do_step_pure
_
_
_
(
LetInCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
LetInCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
asimpl
.
iMod
(
do_step_pure
_
_
_
(
LetInCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
LetInCtx
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
asimpl
.
...
...
@@ -146,7 +146,7 @@ Section fact_equiv.
Lemma
fact_acc_fact_refinement
:
[]
⊨
fact_acc
≤
log
≤
fact
:
(
TArrow
TNat
TNat
).
Proof
.
iIntros
(?
vs
ρ
_
)
"[#HE HΔ]"
.
iIntros
(?
vs
_
)
"[#HE HΔ]"
.
iDestruct
(
interp_env_length
with
"HΔ"
)
as
%?
;
destruct
vs
;
simplify_eq
.
iClear
"HΔ"
.
simpl
.
iIntros
(
j
K
)
"Hj"
;
simpl
.
...
...
@@ -173,7 +173,7 @@ Section fact_equiv.
iNext
;
simpl
;
asimpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
;
asimpl
.
iMod
(
do_step_pure
_
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iApply
(
wp_bind
(
fill
[
IfCtx
_
_
])).
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
...
...
@@ -198,12 +198,12 @@ Section fact_equiv.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
iApply
wp_value
.
simpl
.
iMod
(
do_step_pure
_
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
(
IfCtx
_
_
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
auto
.
simpl
.
iApply
wp_pure_step_later
;
auto
.
iNext
;
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
auto
.
iMod
(
do_step_pure
_
_
_
(
AppRCtx
(
RecV
_
)
::
BinOpRCtx
_
(#
nv
_
)
::
_
)
iMod
(
do_step_pure
_
_
(
AppRCtx
(
RecV
_
)
::
BinOpRCtx
_
(#
nv
_
)
::
_
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iApply
(
wp_bind
(
fill
[
LetInCtx
_
])).
...
...
theories/logrel/F_mu_ref_conc/examples/lock.v
View file @
fcd5c1de
...
...
@@ -84,29 +84,29 @@ Section proof.
Context
`
{
cfgSG
Σ
}.
Context
`
{
heapIG
Σ
}.
Lemma
steps_newlock
E
ρ
j
K
:
Lemma
steps_newlock
E
j
K
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
j
⤇
fill
K
newlock
spec_ctx
∗
j
⤇
fill
K
newlock
⊢
|={
E
}=>
∃
l
,
j
⤇
fill
K
(
Loc
l
)
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec Hj]"
.
by
iMod
(
step_alloc
_
_
j
K
with
"[Hj]"
)
as
"Hj"
;
eauto
.
by
iMod
(
step_alloc
_
j
K
with
"[Hj]"
)
as
"Hj"
;
eauto
.
Qed
.
Typeclasses
Opaque
newlock
.
Global
Opaque
newlock
.
Lemma
steps_acquire
E
ρ
j
K
l
:
Lemma
steps_acquire
E
j
K
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
acquire
(
Loc
l
))
spec_ctx
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
acquire
(
Loc
l
))
⊢
|={
E
}=>
j
⤇
fill
K
Unit
∗
l
↦ₛ
(#
♭
v
true
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hl Hj]]"
.
unfold
acquire
.
iMod
(
step_rec
_
_
j
K
with
"[Hj]"
)
as
"Hj"
;
eauto
.
done
.
iMod
(
step_cas_suc
_
_
j
((
IfCtx
_
_
)
::
K
)
iMod
(
step_rec
_
j
K
with
"[Hj]"
)
as
"Hj"
;
eauto
.
done
.
iMod
(
step_cas_suc
_
j
((
IfCtx
_
_
)
::
K
)
_
_
_
_
_
_
_
_
_
with
"[Hj Hl]"
)
as
"[Hj Hl]"
;
trivial
.
{
simpl
.
iFrame
"Hspec Hj Hl"
;
eauto
.
}
iMod
(
step_if_true
_
_
j
K
_
_
_
with
"[Hj]"
)
as
"Hj"
;
trivial
.
iMod
(
step_if_true
_
j
K
_
_
_
with
"[Hj]"
)
as
"Hj"
;
trivial
.
{
by
iFrame
.
}
by
iIntros
"!> {$Hj $Hl}"
.
Unshelve
.
all
:
trivial
.
...
...
@@ -115,9 +115,9 @@ Section proof.
Typeclasses
Opaque
acquire
.
Global
Opaque
acquire
.
Lemma
steps_release
E
ρ
j
K
l
b
:
Lemma
steps_release
E
j
K
l
b
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
l
↦ₛ
(#
♭
v
b
)
∗
j
⤇
fill
K
(
App
release
(
Loc
l
))
spec_ctx
∗
l
↦ₛ
(#
♭
v
b
)
∗
j
⤇
fill
K
(
App
release
(
Loc
l
))
⊢
|={
E
}=>
j
⤇
fill
K
Unit
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hl Hj]]"
.
unfold
release
.
...
...
@@ -129,26 +129,26 @@ Section proof.
Typeclasses
Opaque
release
.
Global
Opaque
release
.
Lemma
steps_with_lock
E
ρ
j
K
e
l
P
Q
v
w
:
Lemma
steps_with_lock
E
j
K
e
l
P
Q
v
w
:
nclose
specN
⊆
E
→
(* (∀ f, e.[f] = e) (* e is a closed term *) → *)
(
∀
K'
,
spec_ctx
ρ
∗
P
∗
j
⤇
fill
K'
(
App
e
(
of_val
w
))
(
∀
K'
,
spec_ctx
∗
P
∗
j
⤇
fill
K'
(
App
e
(
of_val
w
))
⊢
|={
E
}=>
j
⤇
fill
K'
(
of_val
v
)
∗
Q
)
→
spec_ctx
ρ
∗
P
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
P
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
with_lock
e
(
Loc
l
))
(
of_val
w
))
⊢
|={
E
}=>
j
⤇
fill
K
(
of_val
v
)
∗
Q
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
He
)
"[#Hspec [HP [Hl Hj]]]"
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
steps_acquire
_
_
j
(
SeqCtx
_
::
K
)
with
"[$Hj Hl]"
)
as
"[Hj Hl]"
;
iMod
(
steps_acquire
_
j
(
SeqCtx
_
::
K
)
with
"[$Hj Hl]"
)
as
"[Hj Hl]"
;
auto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
He
(
LetInCtx
_
::
K
)
with
"[$Hj HP]"
)
as
"[Hj HQ]"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
steps_release
_
_
j
(
SeqCtx
_
::
K
)
_
_
with
"[$Hj $Hl]"
)
iMod
(
steps_release
_
j
(
SeqCtx
_
::
K
)
_
_
with
"[$Hj $Hl]"
)
as
"[Hj Hl]"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
View file @
fcd5c1de
...
...
@@ -81,18 +81,18 @@ Section CG_Stack.
Hint
Rewrite
CG_push_subst
:
autosubst
.
Lemma
steps_CG_push
E
ρ
j
K
st
v
w
:
Lemma
steps_CG_push
E
j
K
st
v
w
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
v
∗
j
⤇
fill
K
(
App
(
CG_push
(
Loc
st
))
(
of_val
w
))
spec_ctx
∗
st
↦ₛ
v
∗
j
⤇
fill
K
(
App
(
CG_push
(
Loc
st
))
(
of_val
w
))
⊢
|={
E
}=>
j
⤇
fill
K
Unit
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
)).
Proof
.
intros
HNE
.
iIntros
"[#Hspec [Hx Hj]]"
.
unfold
CG_push
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
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
.
simpl
.
iMod
(
step_store
_
_
j
K
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
iMod
(
step_store
_
j
K
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
{
rewrite
/=
!
to_of_val
//.
}
iModIntro
.
by
iFrame
.
Qed
.
...
...
@@ -124,14 +124,14 @@ Section CG_Stack.
Hint
Rewrite
CG_locked_push_subst
:
autosubst
.
Lemma
steps_CG_locked_push
E
ρ
j
K
st
w
v
l
:
Lemma
steps_CG_locked_push
E
j
K
st
w
v
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
CG_locked_push
(
Loc
st
)
(
Loc
l
))
(
of_val
w
))
⊢
|={
E
}=>
j
⤇
fill
K
Unit
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
))
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
intros
HNE
.
iIntros
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_push
.
iMod
(
steps_with_lock
_
_
_
_
_
_
(
st
↦ₛ
v
)%
I
_
UnitV
with
"[$Hj $Hx $Hl]"
)
iMod
(
steps_with_lock
_
_
_
_
_
(
st
↦ₛ
v
)%
I
_
UnitV
with
"[$Hj $Hx $Hl]"
)
as
"Hj"
;
auto
.
iIntros
(
K'
)
"[#Hspec Hxj]"
.
iApply
steps_CG_push
;
first
done
.
by
iFrame
.
...
...
@@ -164,46 +164,46 @@ Section CG_Stack.
Hint
Rewrite
CG_pop_subst
:
autosubst
.
Lemma
steps_CG_pop_suc
E
ρ
j
K
st
v
w
:
Lemma
steps_CG_pop_suc
E
j
K
st
v
w
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
))
∗
spec_ctx
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
))
∗
j
⤇
fill
K
(
App
(
CG_pop
(
Loc
st
))
Unit
)
⊢
|={
E
}=>
j
⤇
fill
K
(
InjR
(
of_val
w
))
∗
st
↦ₛ
v
.
Proof
.
intros
HNE
.
iIntros
"[#Hspec [Hx Hj]]"
.
unfold
CG_pop
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
step_load
_
_
_
(
UnfoldCtx
::
CaseCtx
_
_
::
K
)
with
"[$Hj $Hx]"
)
iMod
(
step_load
_
_
(
UnfoldCtx
::
CaseCtx
_
_
::
K
)
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
simpl
.
iMod
(
do_step_pure
_
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
do_step_pure
_
_
_
(
StoreRCtx
(
LocV
_
)
::
SeqCtx
_
::
K
)
iMod
(
do_step_pure
_
_
(
StoreRCtx
(
LocV
_
)
::
SeqCtx
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iMod
(
step_store
_
_
j
(
SeqCtx
_
::
K
)
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
iMod
(
step_store
_
j
(
SeqCtx
_
::
K
)
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
using
to_of_val
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
_
(
InjRCtx
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
(
InjRCtx
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
by
iFrame
"Hj Hx"
.
Qed
.
Lemma
steps_CG_pop_fail
E
ρ
j
K
st
:
Lemma
steps_CG_pop_fail
E
j
K
st
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
)
∗
spec_ctx
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
)
∗
j
⤇
fill
K
(
App
(
CG_pop
(
Loc
st
))
Unit
)
⊢
|={
E
}=>
j
⤇
fill
K
(
InjL
Unit
)
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx Hj]]"
.
unfold
CG_pop
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
step_load
_
_
j
(
UnfoldCtx
::
CaseCtx
_
_
::
K
)
iMod
(
step_load
_
j
(
UnfoldCtx
::
CaseCtx
_
_
::
K
)
_
_
_
with
"[$Hj $Hx]"
)
as
"[Hj Hx]"
;
eauto
.
iMod
(
do_step_pure
_
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
by
iFrame
"Hj Hx"
;
trivial
.
...
...
@@ -237,28 +237,28 @@ Section CG_Stack.
Hint
Rewrite
CG_locked_pop_subst
:
autosubst
.
Lemma
steps_CG_locked_pop_suc
E
ρ
j
K
st
v
w
l
:
Lemma
steps_CG_locked_pop_suc
E
j
K
st
v
w
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
))
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
))
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
CG_locked_pop
(
Loc
st
)
(
Loc
l
))
Unit
)
⊢
|={
E
}=>
j
⤇
fill
K
(
InjR
(
of_val
w
))
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_pop
.
iMod
(
steps_with_lock
_
_
_
_
_
_
(
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
)))%
I
iMod
(
steps_with_lock
_
_
_
_
_
(
st
↦ₛ
FoldV
(
InjRV
(
PairV
w
v
)))%
I
_
(
InjRV
w
)
UnitV
with
"[$Hj $Hx $Hl]"
)
as
"Hj"
;
eauto
.
iIntros
(
K'
)
"[#Hspec Hxj]"
.
iApply
steps_CG_pop_suc
;
eauto
.
Qed
.
Lemma
steps_CG_locked_pop_fail
E
ρ
j
K
st
l
:
Lemma
steps_CG_locked_pop_fail
E
j
K
st
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
)
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
)
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
CG_locked_pop
(
Loc
st
)
(
Loc
l
))
Unit
)
⊢
|={
E
}=>
j
⤇
fill
K
(
InjL
Unit
)
∗
st
↦ₛ
FoldV
(
InjLV
UnitV
)
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_pop
.
iMod
(
steps_with_lock
_
_
_
_
_
_
(
st
↦ₛ
FoldV
(
InjLV
UnitV
))%
I
_
iMod
(
steps_with_lock
_
_
_
_
_
(
st
↦ₛ
FoldV
(
InjLV
UnitV
))%
I
_
(
InjLV
UnitV
)
UnitV
with
"[$Hj $Hx $Hl]"
)
as
"Hj"
;
eauto
.
iIntros
(
K'
)
"[#Hspec Hxj] /="
.
...
...
@@ -293,14 +293,14 @@ Section CG_Stack.
Hint
Rewrite
CG_snap_subst
:
autosubst
.
Lemma
steps_CG_snap
E
ρ
j
K
st
v
l
:
Lemma
steps_CG_snap
E
j
K
st
v
l
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
)
spec_ctx
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
)
∗
j
⤇
fill
K
(
App
(
CG_snap
(
Loc
st
)
(
Loc
l
))
Unit
)
⊢
|={
E
}=>
j
⤇
(
fill
K
(
of_val
v
))
∗
st
↦ₛ
v
∗
l
↦ₛ
(#
♭
v
false
).
Proof
.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_snap
.
iMod
(
steps_with_lock
_
_
_
_
_
_
(
st
↦ₛ
v
)%
I
_
v
UnitV
iMod
(
steps_with_lock
_
_
_
_
_
(
st
↦ₛ
v
)%
I
_
v
UnitV
with
"[$Hj $Hx $Hl]"
)
as
"Hj"
;
eauto
.
iIntros
(
K'
)
"[#Hspec [Hx Hj]]"
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
...
...
@@ -353,9 +353,9 @@ Section CG_Stack.
Hint
Rewrite
CG_iter_subst
:
autosubst
.
Lemma
steps_CG_iter
E
ρ
j
K
f
v
w
:
Lemma
steps_CG_iter
E
j
K
f
v
w
:
nclose
specN
⊆
E
→
spec_ctx
ρ
spec_ctx
∗
j
⤇
fill
K
(
App
(
CG_iter
(
of_val
f
))
(
Fold
(
InjR
(
Pair
(
of_val
w
)
(
of_val
v
)))))
⊢
|={
E
}=>
...
...
@@ -366,22 +366,22 @@ Section CG_Stack.
iIntros
(
HNE
)
"[#Hspec Hj]"
.
unfold
CG_iter
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
do_step_pure
_
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
do_step_pure
_
_
_
(
AppRCtx
f
::
SeqCtx
_
::
K
)
with
"[$Hj]"
)
iMod
(
do_step_pure
_
_
(
AppRCtx
f
::
SeqCtx
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
Qed
.
Lemma
steps_CG_iter_end
E
ρ
j
K
f
:
Lemma
steps_CG_iter_end
E
j
K
f
:
nclose
specN
⊆
E
→
spec_ctx
ρ
∗
j
⤇
fill
K
(
App
(
CG_iter
(
of_val
f
))
(
Fold
(
InjL
Unit
)))
spec_ctx
∗
j
⤇
fill
K
(
App
(
CG_iter
(
of_val
f
))
(
Fold
(
InjL
Unit
)))
⊢
|={
E
}=>
j
⤇
fill
K
Unit
.
Proof
.
iIntros
(
HNE
)
"[#Hspec Hj]"
.
unfold
CG_iter
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
_
(
CaseCtx
_
_
::
K
)
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iAsimpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
Qed
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
View file @
fcd5c1de
...
...
@@ -20,7 +20,7 @@ Section Stack_refinement.
(
TArrow
(
TArrow
(
TVar
0
)
TUnit
)
TUnit
)).
Proof
.
(* executing the preambles *)
iIntros
(
Δ
[|??]
ρ
?)
"#[Hspec HΓ]"
;
iIntros
(
j
K
)
"Hj"
;
last
first
.
iIntros
(
Δ
[|??]
?)
"#[Hspec HΓ]"
;
iIntros
(
j
K
)
"Hj"
;
last
first
.
{
iDestruct
(
interp_env_length
with
"HΓ"
)
as
%[=].
}
iClear
"HΓ"
.
cbn
-[
FG_stack
CG_stack
].
rewrite
?empty_env_subst
/
CG_stack
/
FG_stack
.
...
...
@@ -29,11 +29,11 @@ Section Stack_refinement.
clear
j
K
.
iAlways
.
iIntros
(
τ
i
)
"%"
.
iIntros
(
j
K
)
"Hj /="
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iApply
wp_pure_step_later
;
auto
.
iNext
.
iMod
(
steps_newlock
_
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
iMod
(
steps_newlock
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
as
(
l
)
"[Hj Hl]"
;
eauto
.
iMod
(
do_step_pure
_
_
j
K
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
iMod
(
do_step_pure
_
j
K
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
simpl
.
iAsimpl
.
iMod
(
step_alloc
_
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
iMod
(
step_alloc
_
j
(
LetInCtx
_
::
K
)
with
"[$Hj]"
)
as
(
stk'
)
"[Hj Hstk']"
;
eauto
.
simpl
.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
...
...
@@ -110,7 +110,7 @@ Section Stack_refinement.
*
(* CAS succeeds *)
(* In this case, the specification pushes *)
iMod
"Hstk'"
.
iMod
"Hl"
.
iMod
(
steps_CG_locked_push
_
_
j
K
with
"[Hj Hl Hstk']"
)
iMod
(
steps_CG_locked_push
_
j
K
with
"[Hj Hl Hstk']"
)
as
"[Hj [Hstk' Hl]]"
;
first
solve_ndisj
.
{
rewrite
CG_locked_push_of_val
.
by
iFrame
"Hspec Hstk' Hj"
.
}
iApply
(
wp_cas_suc
with
"Hstk"
)
;
auto
.
...
...
@@ -250,7 +250,7 @@ Section Stack_refinement.
iApply
(
wp_bind
(
fill
[
FoldCtx
;
AppRCtx
_
]))
;
iApply
wp_wand_l
;
iSplitR
;
[
iIntros
(
w
)
"Hw"
;
iExact
"Hw"
|].
iInv
stackN
as
(
istk3
w
h
)
"[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]"
"Hclose"
.
iMod
(
steps_CG_snap
_
_
_
(
AppRCtx
_
::
K
)
iMod
(
steps_CG_snap
_
_
(
AppRCtx
_
::
K
)
with
"[Hstk' Hj Hl]"
)
as
"[Hj [Hstk' Hl]]"
;
first
solve_ndisj
.
{
rewrite
?fill_app
.
simpl
.
by
iFrame
"Hspec Hstk' Hl Hj"
.
}
iApply
(
wp_load
with
"[$Hstk]"
).
iNext
.
iIntros
"Hstk"
.
...
...
@@ -308,7 +308,7 @@ Section Stack_refinement.
iAsimpl
.
replace
(
CG_iter
(
of_val
f2
))
with
(
of_val
(
CG_iterV
(
of_val
f2
)))
by
(
by
rewrite
CG_iter_of_val
).
iMod
(
step_snd
_
_
_
(
AppRCtx
_
::
K
)
with
"[$Hspec Hj]"
)
as
"Hj"
;
iMod
(
step_snd
_
_
(
AppRCtx
_
::
K
)
with
"[$Hspec Hj]"
)
as
"Hj"
;
[|
|
|
simpl
;
by
iFrame
"Hj"
|]
;
rewrite
?to_of_val
;
auto
.
iApply
wp_pure_step_later
;
trivial
.
iNext
.
simpl
.
...
...
theories/logrel/F_mu_ref_conc/fundamental_binary.v
View file @
fcd5c1de
...
...
@@ -8,9 +8,9 @@ Section bin_log_def.
Context
`
{
heapIG
Σ
,
cfgSG
Σ
}.
Notation
D
:
=
(
prodC
valC
valC
-
n
>
iProp
Σ
).
Definition
bin_log_related
(
Γ
:
list
type
)
(
e
e'
:
expr
)
(
τ
:
type
)
:
=
∀
Δ
vvs
ρ
,
Definition
bin_log_related
(
Γ
:
list
type
)
(
e
e'
:
expr
)
(
τ
:
type
)
:
=
∀
Δ
vvs
,
env_Persistent
Δ
→
spec_ctx
ρ
∧
spec_ctx
∧
⟦
Γ
⟧
*
Δ
vvs
⊢
⟦
τ
⟧ₑ
Δ
(
e
.[
env_subst
(
vvs
.*
1
)],
e'
.[
env_subst
(
vvs
.*
2
)]).
End
bin_log_def
.