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
Iris
examples
Commits
380623ef
Commit
380623ef
authored
Dec 21, 2018
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix some deprecation warnings.
parent
86a81cbe
Pipeline
#13758
passed with stage
in 7 minutes and 6 seconds
Changes
4
Pipelines
22
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
19 additions
and
19 deletions
+19
-19
theories/logrel/F_mu_ref/fundamental_binary.v
theories/logrel/F_mu_ref/fundamental_binary.v
+8
-8
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+1
-1
theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/logrel/F_mu_ref_conc/fundamental_binary.v
+8
-8
theories/spanning_tree/spanning.v
theories/spanning_tree/spanning.v
+2
-2
No files found.
theories/logrel/F_mu_ref/fundamental_binary.v
View file @
380623ef
...
...
@@ -39,7 +39,7 @@ Section fundamental.
⤇
fill
K
(
of_val
v'
)
∗
interp
τ
Δ
(
v
,
v'
)
}}.
Proof
.
iIntros
(
Hlog
Δ
vvs
K
ρ
?)
"[#Hρ [HΓ Hj]]"
.
asimpl
.
iApply
(
Hlog
with
"[HΓ]
*
"
)
;
iFrame
.
eauto
.
iApply
(
Hlog
with
"[HΓ]"
)
;
iFrame
.
eauto
.
Qed
.
Notation
"'` H"
:
=
(
bin_log_related_alt
H
)
(
at
level
8
).
...
...
@@ -93,7 +93,7 @@ Section fundamental.
iIntros
(
Δ
vvs
ρ
?)
"#[Hρ HΓ]"
;
iIntros
(
K
)
"Hj /="
.
smart_wp_bind
(
SndCtx
)
v
v'
"[Hv #Hiv]"
(
'
`
IHHtyped
_
_
_
(
SndCtx
::
K
))
;
cbn
.
iDestruct
"Hiv"
as
([
w1
w1'
]
[
w2
w2'
])
"#[% [Hw1 Hw2]]"
;
simplify_eq
.
iMod
(
step_snd
_
_
K
(
of_val
w1'
)
(
of_val
w2'
)
with
"
*
[-]"
)
as
"Hw"
;
eauto
.
iMod
(
step_snd
_
_
K
(
of_val
w1'
)
(
of_val
w2'
)
with
"[-]"
)
as
"Hw"
;
eauto
.
iApply
wp_pure_step_later
;
auto
.
iApply
wp_value
;
auto
.
Qed
.
...
...
@@ -137,13 +137,13 @@ Section fundamental.
(
'
`
IHHtyped1
_
_
_
((
CaseCtx
_
_
)
::
K
))
;
cbn
.
iDestruct
"Hiv"
as
"[Hiv|Hiv]"
.
-
iDestruct
"Hiv"
as
([
w
w'
])
"[% Hw]"
;
simplify_eq
.
iMod
(
step_case_inl
_
_
K
(
of_val
w'
)
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_case_inl
_
_
K
(
of_val
w'
)
with
"[-]"
)
as
"Hz"
;
eauto
.
simpl
.
iApply
wp_pure_step_later
;
auto
1
using
to_of_val
.
iNext
.
asimpl
.
iApply
(
'
`
IHHtyped2
_
((
w
,
w'
)
::
vvs
))
;
repeat
iSplit
;
eauto
.
iApply
interp_env_cons
;
auto
.
-
iDestruct
"Hiv"
as
([
w
w'
])
"[% Hw]"
;
simplify_eq
.
iMod
(
step_case_inr
_
_
K
(
of_val
w'
)
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_case_inr
_
_
K
(
of_val
w'
)
with
"[-]"
)
as
"Hz"
;
eauto
.
simpl
.
iApply
wp_pure_step_later
;
auto
1
using
to_of_val
.
iNext
.
asimpl
.
iApply
(
'
`
IHHtyped3
_
((
w
,
w'
)
::
vvs
))
;
repeat
iSplit
;
eauto
.
...
...
@@ -161,7 +161,7 @@ Section fundamental.
iIntros
([
v
v'
])
"#Hiv"
.
iIntros
(
K'
)
"Hj"
.
iDestruct
(
interp_env_length
with
"HΓ"
)
as
%?.
iApply
wp_pure_step_later
;
auto
1
using
to_of_val
.
iNext
.
iMod
(
step_lam
_
_
K'
_
(
of_val
v'
)
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_lam
_
_
K'
_
(
of_val
v'
)
with
"[-]"
)
as
"Hz"
;
eauto
.
asimpl
.
iApply
(
'
`
IHHtyped
_
((
v
,
v'
)
::
vvs
))
;
repeat
iSplit
;
eauto
.
iApply
interp_env_cons
;
iSplit
;
auto
.
Qed
.
...
...
@@ -176,7 +176,7 @@ Section fundamental.
(
'
`
IHHtyped1
_
_
_
(((
AppLCtx
(
e2'
.[
env_subst
(
vvs
.*
2
)])))
::
K
))
;
cbn
.
smart_wp_bind
(
AppRCtx
v
)
w
w'
"[Hw #Hiw]"
(
'
`
IHHtyped2
_
_
_
((
AppRCtx
v'
)
::
K
))
;
cbn
.
iApply
(
"Hiv"
$!
(
w
,
w'
)
with
"Hiw
*
"
)
;
simpl
;
eauto
.
iApply
(
"Hiv"
$!
(
w
,
w'
)
with
"Hiw"
)
;
simpl
;
eauto
.
Qed
.
Lemma
bin_log_related_tlam
Γ
e
e'
τ
...
...
@@ -187,7 +187,7 @@ Section fundamental.
iApply
wp_value
.
iExists
(
TLamV
_
).
iIntros
"{$Hj} /= !#"
;
iIntros
(
τ
i
?
K'
)
"Hv /="
.
iApply
wp_pure_step_later
;
auto
;
iNext
.
iMod
(
step_tlam
_
_
K'
(
e'
.[
env_subst
(
vvs
.*
2
)])
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_tlam
_
_
K'
(
e'
.[
env_subst
(
vvs
.*
2
)])
with
"[-]"
)
as
"Hz"
;
eauto
.
iApply
'
`
IHHtyped
;
repeat
iSplit
;
eauto
.
by
iApply
interp_env_ren
.
Qed
.
...
...
@@ -232,7 +232,7 @@ Section fundamental.
rewrite
/=
fixpoint_interp_rec1_eq
/=.
change
(
fixpoint
_
)
with
(
interp
(
TRec
τ
)
Δ
).
iDestruct
"Hiw"
as
([
w
w'
])
"#[% Hiz]"
;
simplify_eq
/=.
iMod
(
step_Fold
_
_
K
(
of_val
w'
)
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_Fold
_
_
K
(
of_val
w'
)
with
"[-]"
)
as
"Hz"
;
eauto
.
iApply
wp_pure_step_later
;
cbn
;
auto
.
iNext
.
iApply
wp_value
;
auto
.
iExists
_;
iFrame
"Hz"
.
by
rewrite
-
interp_subst
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
View file @
380623ef
...
...
@@ -59,7 +59,7 @@ Section Rules.
iDestruct
"H"
as
(
l
w
)
"[% [#Hl [#Hr|Hr]]]"
;
subst
.
{
iExists
l
,
w
;
iAlways
;
eauto
.
}
iDestruct
"Hr"
as
(
y1
z1
y2
z2
)
"[#H1 [#H2 [#HQ H']]]"
.
rewrite
later_forall
.
iDestruct
(
"IH"
with
"
*
H'"
)
as
"#H''"
.
iClear
"H'"
.
rewrite
later_forall
.
iDestruct
(
"IH"
with
"H'"
)
as
"#H''"
.
iClear
"H'"
.
iAlways
.
eauto
20
.
Qed
.
...
...
theories/logrel/F_mu_ref_conc/fundamental_binary.v
View file @
380623ef
...
...
@@ -39,7 +39,7 @@ Section fundamental.
j
⤇
fill
K
(
of_val
v'
)
∗
interp
τ
Δ
(
v
,
v'
)
}}.
Proof
.
iIntros
(
Hlog
Δ
vvs
ρ
j
K
?)
"(#Hs & HΓ & Hj)"
.
iApply
(
Hlog
with
"[HΓ]
*
"
)
;
iFrame
;
eauto
.
iApply
(
Hlog
with
"[HΓ]"
)
;
iFrame
;
eauto
.
Qed
.
Notation
"'` H"
:
=
(
bin_log_related_alt
H
)
(
at
level
8
).
...
...
@@ -212,7 +212,7 @@ Section fundamental.
iDestruct
(
interp_env_length
with
"HΓ"
)
as
%?.
iApply
wp_pure_step_later
;
auto
1
using
to_of_val
.
iNext
.
iApply
fupd_wp
.
iMod
(
step_rec
_
_
j'
K'
_
(
of_val
v'
)
v'
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_rec
_
_
j'
K'
_
(
of_val
v'
)
v'
with
"[-]"
)
as
"Hz"
;
eauto
.
asimpl
.
change
(
Rec
?e
)
with
(
of_val
(
RecV
e
)).
iApply
(
'
`
IHHtyped
_
((
_
,
_
)
::
(
v
,
v'
)
::
vvs
))
;
repeat
iSplit
;
eauto
.
iModIntro
.
...
...
@@ -231,7 +231,7 @@ Section fundamental.
iDestruct
(
interp_env_length
with
"HΓ"
)
as
%?.
iApply
wp_pure_step_later
;
auto
1
using
to_of_val
.
iNext
.
iApply
fupd_wp
.
iMod
(
step_lam
_
_
j'
K'
_
(
of_val
v'
)
v'
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_lam
_
_
j'
K'
_
(
of_val
v'
)
v'
with
"[-]"
)
as
"Hz"
;
eauto
.
asimpl
.
iFrame
"#"
.
change
(
Lam
?e
)
with
(
of_val
(
LamV
e
)).
iApply
(
'
`
IHHtyped
_
((
v
,
v'
)
::
vvs
))
;
repeat
iSplit
;
eauto
.
iModIntro
.
...
...
@@ -281,7 +281,7 @@ Section fundamental.
(
'
`
IHHtyped1
_
_
_
j
(((
AppLCtx
(
e2'
.[
env_subst
(
vvs
.*
2
)])))
::
K
))
;
cbn
.
smart_wp_bind
(
AppRCtx
v
)
w
w'
"[Hw #Hiw]"
(
'
`
IHHtyped2
_
_
_
j
((
AppRCtx
v'
)
::
K
))
;
cbn
.
iApply
(
"Hiv"
$!
(
w
,
w'
)
with
"Hiw
*
"
)
;
simpl
;
eauto
.
iApply
(
"Hiv"
$!
(
w
,
w'
)
with
"Hiw"
)
;
simpl
;
eauto
.
Qed
.
Lemma
bin_log_related_tlam
Γ
e
e'
τ
...
...
@@ -293,7 +293,7 @@ Section fundamental.
iIntros
"{$Hj} /= !#"
;
iIntros
(
τ
i
?
j'
K'
)
"Hv /="
.
iApply
wp_pure_step_later
;
auto
.
iNext
.
iApply
fupd_wp
.
iMod
(
step_tlam
_
_
j'
K'
(
e'
.[
env_subst
(
vvs
.*
2
)])
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_tlam
_
_
j'
K'
(
e'
.[
env_subst
(
vvs
.*
2
)])
with
"[-]"
)
as
"Hz"
;
eauto
.
iApply
'
`
IHHtyped
;
repeat
iSplit
;
eauto
.
iModIntro
.
rewrite
interp_env_ren
;
auto
.
Qed
.
...
...
@@ -338,7 +338,7 @@ Section fundamental.
change
(
fixpoint
_
)
with
(
interp
(
TRec
τ
)
Δ
).
iDestruct
"Hiw"
as
([
w
w'
])
"#[% Hiz]"
;
simplify_eq
/=.
iApply
fupd_wp
.
iMod
(
step_Fold
_
_
j
K
(
of_val
w'
)
w'
with
"
*
[-]"
)
as
"Hz"
;
eauto
.
iMod
(
step_Fold
_
_
j
K
(
of_val
w'
)
w'
with
"[-]"
)
as
"Hz"
;
eauto
.
iApply
wp_pure_step_later
;
auto
.
iModIntro
.
iApply
wp_value
.
iNext
;
iExists
_;
iFrame
"Hz"
.
by
rewrite
-
interp_subst
.
...
...
@@ -350,7 +350,7 @@ Section fundamental.
Proof
.
iIntros
(
Δ
vvs
ρ
?)
"#(Hs & HΓ)"
;
iIntros
(
j
K
)
"Hj /="
.
iApply
fupd_wp
.
iMod
(
step_fork
_
_
j
K
with
"
*
[-]"
)
as
(
j'
)
"[Hj Hj']"
;
eauto
.
iMod
(
step_fork
_
_
j
K
with
"[-]"
)
as
(
j'
)
"[Hj Hj']"
;
eauto
.
iApply
wp_fork
;
iModIntro
.
rewrite
-
bi
.
later_sep
.
iNext
;
iSplitL
"Hj"
.
-
iExists
UnitV
;
eauto
.
-
iApply
wp_wand_l
;
iSplitR
;
[|
iApply
(
'
`
IHHtyped
_
_
_
_
[])]
;
eauto
.
...
...
@@ -363,7 +363,7 @@ Section fundamental.
iIntros
(
Δ
vvs
ρ
?)
"#(Hs & HΓ)"
;
iIntros
(
j
K
)
"Hj /="
.
smart_wp_bind
(
AllocCtx
)
v
v'
"[Hv #Hiv]"
(
'
`
IHHtyped
_
_
_
j
(
AllocCtx
::
K
)).
iApply
fupd_wp
.
iMod
(
step_alloc
_
_
j
K
(
of_val
v'
)
v'
with
"
*
[-]"
)
as
(
l'
)
"[Hj Hl]"
;
eauto
.
iMod
(
step_alloc
_
_
j
K
(
of_val
v'
)
v'
with
"[-]"
)
as
(
l'
)
"[Hj Hl]"
;
eauto
.
iApply
wp_atomic
;
eauto
.
iApply
wp_alloc
;
eauto
.
do
2
iModIntro
.
iNext
.
iIntros
(
l
)
"Hl'"
.
...
...
theories/spanning_tree/spanning.v
View file @
380623ef
...
...
@@ -340,7 +340,7 @@ Section Helpers.
(
child_to_val
u1
)
=
SOMEV
#
l
∧
l
∈
dom
(
gset
_
)
g
))
as
Hlf
.
{
destruct
u1
as
[
l1
|]
;
[
right
|
by
left
].
exists
l1
;
split
;
trivial
.
eapply
(
Hgmx
l
)
;
rewrite
//
/
get_left
Hgl
;
auto
.
}
iApply
(
"IH"
with
"[#]
*
[K1] [Hx11]"
)
;
auto
.
iApply
(
"IH"
with
"[#] [K1] [Hx11]"
)
;
auto
.
(* symbolically executing the left part of the par. *)
wp_lam
;
repeat
wp_proj
.
assert
((
child_to_val
u2
)
=
NONEV
...
...
@@ -348,7 +348,7 @@ Section Helpers.
(
child_to_val
u2
)
=
SOMEV
#
l
∧
l
∈
dom
(
gset
_
)
g
))
as
Hrh
.
{
destruct
u2
as
[
l2
|]
;
[
right
|
by
left
].
exists
l2
;
split
;
trivial
.
eapply
(
Hgmx
l
)
;
rewrite
//
/
get_right
Hgl
;
auto
.
}
iApply
(
"IH"
with
"[#]
*
[K2] [Hx12]"
)
;
auto
.
iApply
(
"IH"
with
"[#] [K2] [Hx12]"
)
;
auto
.
(* continuing after both children are processed *)
iNext
.
iIntros
(
vl
vr
)
"([Hvl K1] & Hvr & K2 & K2')"
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment