Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
7522d558
Commit
7522d558
authored
Jun 19, 2016
by
Robbert Krebbers
Browse files
Put quantifiers in pvs and wp definition in same order as wsat.
parent
75bfd4ef
Pipeline
#1498
passed with stage
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
program_logic/adequacy.v
View file @
7522d558
...
...
@@ -96,7 +96,7 @@ Proof.
inversion
Hwptp
as
[|??
r
??
rs
Hwp
_
]
;
clear
Hwptp
;
subst
.
move
:
Hwp
.
rewrite
wp_eq
.
uPred
.
unseal
=>
/
wp_value_inv
Hwp
.
rewrite
pvs_eq
in
Hwp
.
destruct
(
Hwp
(
big_op
rs
)
2
∅
σ
2
)
as
[
r'
[]]
;
rewrite
?right_id_L
;
auto
.
destruct
(
Hwp
2
∅
σ
2
(
big_op
rs
))
as
[
r'
[]]
;
rewrite
?right_id_L
;
auto
.
Qed
.
Lemma
ht_adequacy_result
E
φ
e
v
t2
σ
1
m
σ
2
:
...
...
program_logic/lifting.v
View file @
7522d558
...
...
@@ -28,13 +28,13 @@ Lemma wp_lift_step E1 E2
Proof
.
intros
?
He
Hsafe
Hstep
.
rewrite
pvs_eq
wp_eq
.
uPred
.
unseal
;
split
=>
n
r
?
Hvs
;
constructor
;
auto
.
intros
rf
k
Ef
σ
1
'
???
;
destruct
(
Hvs
rf
(
S
k
)
Ef
σ
1
'
)
intros
k
Ef
σ
1
'
rf
???
;
destruct
(
Hvs
(
S
k
)
Ef
σ
1
'
rf
)
as
(
r'
&(
r1
&
r2
&?&?&
Hwp
)&
Hws
)
;
auto
;
clear
Hvs
;
cofe_subst
r'
.
destruct
(
wsat_update_pst
k
(
E2
∪
Ef
)
σ
1
σ
1
'
r1
(
r2
⋅
rf
))
as
[->
Hws'
].
{
apply
equiv_dist
.
rewrite
-(
ownP_spec
k
)
;
auto
.
}
{
by
rewrite
assoc
.
}
constructor
;
[
done
|
intros
e2
σ
2
ef
?
;
specialize
(
Hws'
σ
2
)].
destruct
(
λ
H1
H2
H3
,
Hwp
e2
σ
2
ef
k
(
update_pst
σ
2
r1
)
H1
H2
H3
rf
k
Ef
σ
2
)
destruct
(
λ
H1
H2
H3
,
Hwp
e2
σ
2
ef
k
(
update_pst
σ
2
r1
)
H1
H2
H3
k
Ef
σ
2
rf
)
as
(
r'
&(
r1'
&
r2'
&?&?&?)&?)
;
auto
;
cofe_subst
r'
.
{
split
.
by
eapply
Hstep
.
apply
ownP_spec
;
auto
.
}
{
rewrite
(
comm
_
r2
)
-
assoc
;
eauto
using
wsat_le
.
}
...
...
@@ -49,7 +49,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
Proof
.
intros
He
Hsafe
Hstep
;
rewrite
wp_eq
;
uPred
.
unseal
.
split
=>
n
r
?
Hwp
;
constructor
;
auto
.
intros
rf
k
Ef
σ
1
???
;
split
;
[
done
|].
destruct
n
as
[|
n
]
;
first
lia
.
intros
k
Ef
σ
1
rf
???
;
split
;
[
done
|].
destruct
n
as
[|
n
]
;
first
lia
.
intros
e2
σ
2
ef
?
;
destruct
(
Hstep
σ
1 e2
σ
2
ef
)
;
auto
;
subst
.
destruct
(
Hwp
e2
ef
k
r
)
as
(
r1
&
r2
&
Hr
&?&?)
;
auto
.
exists
r1
,
r2
;
split_and
?
;
try
done
.
...
...
program_logic/pviewshifts.v
View file @
7522d558
...
...
@@ -11,14 +11,14 @@ Local Hint Extern 10 (✓{_} _) =>
end
;
solve_validN
.
Program
Definition
pvs_def
{
Λ
Σ
}
(
E1
E2
:
coPset
)
(
P
:
iProp
Λ
Σ
)
:
iProp
Λ
Σ
:
=
{|
uPred_holds
n
r1
:
=
∀
rf
k
Ef
σ
,
{|
uPred_holds
n
r1
:
=
∀
k
Ef
σ
rf
,
0
<
k
≤
n
→
E1
∪
E2
⊥
Ef
→
wsat
k
(
E1
∪
Ef
)
σ
(
r1
⋅
rf
)
→
∃
r2
,
P
k
r2
∧
wsat
k
(
E2
∪
Ef
)
σ
(
r2
⋅
rf
)
|}.
Next
Obligation
.
intros
Λ
Σ
E1
E2
P
n
r1
r2
HP
[
r3
Hr2
]
rf
k
Ef
σ
??.
intros
Λ
Σ
E1
E2
P
n
r1
r2
HP
[
r3
Hr2
]
k
Ef
σ
rf
??.
rewrite
(
dist_le
_
_
_
_
Hr2
)
;
last
lia
.
intros
Hws
.
destruct
(
HP
(
r3
⋅
rf
)
k
Ef
σ
)
as
(
r'
&?&
Hws'
)
;
rewrite
?(
assoc
op
)
;
auto
.
destruct
(
HP
k
Ef
σ
(
r3
⋅
rf
))
as
(
r'
&?&
Hws'
)
;
rewrite
?(
assoc
op
)
;
auto
.
exists
(
r'
⋅
r3
)
;
rewrite
-
assoc
;
split
;
last
done
.
apply
uPred_mono
with
r'
;
eauto
using
cmra_includedN_l
.
Qed
.
...
...
@@ -63,8 +63,8 @@ Proof. intros ?????. exfalso. omega. Qed.
Global
Instance
pvs_ne
E1
E2
n
:
Proper
(
dist
n
==>
dist
n
)
(@
pvs
Λ
Σ
E1
E2
).
Proof
.
rewrite
pvs_eq
.
intros
P
Q
HPQ
;
split
=>
n'
r1
??
;
simpl
;
split
;
intros
HP
rf
k
Ef
σ
???
;
destruct
(
HP
rf
k
Ef
σ
)
as
(
r2
&?&?)
;
auto
;
intros
P
Q
HPQ
;
split
=>
n'
r1
??
;
simpl
;
split
;
intros
HP
k
Ef
σ
rf
???
;
destruct
(
HP
k
Ef
σ
rf
)
as
(
r2
&?&?)
;
auto
;
exists
r2
;
split_and
?
;
auto
;
apply
HPQ
;
eauto
.
Qed
.
Global
Instance
pvs_proper
E1
E2
:
Proper
((
≡
)
==>
(
≡
))
(@
pvs
Λ
Σ
E1
E2
).
...
...
@@ -72,46 +72,46 @@ Proof. apply ne_proper, _. Qed.
Lemma
pvs_intro
E
P
:
P
={
E
}=>
P
.
Proof
.
rewrite
pvs_eq
.
split
=>
n
r
?
HP
rf
k
Ef
σ
???
;
exists
r
;
split
;
last
done
.
rewrite
pvs_eq
.
split
=>
n
r
?
HP
k
Ef
σ
rf
???
;
exists
r
;
split
;
last
done
.
apply
uPred_closed
with
n
;
eauto
.
Qed
.
Lemma
pvs_mono
E1
E2
P
Q
:
(
P
⊢
Q
)
→
(|={
E1
,
E2
}=>
P
)
={
E1
,
E2
}=>
Q
.
Proof
.
rewrite
pvs_eq
.
intros
HPQ
;
split
=>
n
r
?
HP
rf
k
Ef
σ
???.
destruct
(
HP
rf
k
Ef
σ
)
as
(
r2
&?&?)
;
eauto
.
rewrite
pvs_eq
.
intros
HPQ
;
split
=>
n
r
?
HP
k
Ef
σ
rf
???.
destruct
(
HP
k
Ef
σ
rf
)
as
(
r2
&?&?)
;
eauto
.
exists
r2
;
eauto
using
uPred_in_entails
.
Qed
.
Lemma
pvs_timeless
E
P
:
TimelessP
P
→
▷
P
={
E
}=>
P
.
Proof
.
rewrite
pvs_eq
uPred
.
timelessP_spec
=>
HP
.
uPred
.
unseal
;
split
=>-[|
n
]
r
?
HP'
rf
k
Ef
σ
???
;
first
lia
.
uPred
.
unseal
;
split
=>-[|
n
]
r
?
HP'
k
Ef
σ
rf
???
;
first
lia
.
exists
r
;
split
;
last
done
.
apply
HP
,
uPred_closed
with
n
;
eauto
using
cmra_validN_le
.
Qed
.
Lemma
pvs_trans
E1
E2
E3
P
:
E2
⊆
E1
∪
E3
→
(|={
E1
,
E2
}=>
|={
E2
,
E3
}=>
P
)
={
E1
,
E3
}=>
P
.
Proof
.
rewrite
pvs_eq
.
intros
?
;
split
=>
n
r1
?
HP1
rf
k
Ef
σ
???.
destruct
(
HP1
rf
k
Ef
σ
)
as
(
r2
&
HP2
&?)
;
auto
.
rewrite
pvs_eq
.
intros
?
;
split
=>
n
r1
?
HP1
k
Ef
σ
rf
???.
destruct
(
HP1
k
Ef
σ
rf
)
as
(
r2
&
HP2
&?)
;
auto
.
Qed
.
Lemma
pvs_mask_frame
E1
E2
Ef
P
:
Ef
⊥
E1
∪
E2
→
(|={
E1
,
E2
}=>
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=>
P
.
Proof
.
rewrite
pvs_eq
.
intros
?
;
split
=>
n
r
?
HP
rf
k
Ef'
σ
???.
destruct
(
HP
rf
k
(
Ef
∪
Ef'
)
σ
)
as
(
r'
&?&?)
;
rewrite
?(
assoc_L
_
)
;
eauto
.
rewrite
pvs_eq
.
intros
?
;
split
=>
n
r
?
HP
k
Ef'
σ
rf
???.
destruct
(
HP
k
(
Ef
∪
Ef'
)
σ
rf
)
as
(
r'
&?&?)
;
rewrite
?(
assoc_L
_
)
;
eauto
.
by
exists
r'
;
rewrite
-(
assoc_L
_
).
Qed
.
Lemma
pvs_frame_r
E1
E2
P
Q
:
(|={
E1
,
E2
}=>
P
)
★
Q
={
E1
,
E2
}=>
P
★
Q
.
Proof
.
rewrite
pvs_eq
.
uPred
.
unseal
;
split
;
intros
n
r
?
(
r1
&
r2
&
Hr
&
HP
&?)
rf
k
Ef
σ
???.
destruct
(
HP
(
r2
⋅
rf
)
k
Ef
σ
)
as
(
r'
&?&?)
;
eauto
.
rewrite
pvs_eq
.
uPred
.
unseal
;
split
;
intros
n
r
?
(
r1
&
r2
&
Hr
&
HP
&?)
k
Ef
σ
rf
???.
destruct
(
HP
k
Ef
σ
(
r2
⋅
rf
))
as
(
r'
&?&?)
;
eauto
.
{
by
rewrite
assoc
-(
dist_le
_
_
_
_
Hr
)
;
last
lia
.
}
exists
(
r'
⋅
r2
)
;
split
;
last
by
rewrite
-
assoc
.
exists
r'
,
r2
;
split_and
?
;
auto
.
apply
uPred_closed
with
n
;
auto
.
Qed
.
Lemma
pvs_openI
i
P
:
ownI
i
P
={{[
i
]},
∅
}=>
▷
P
.
Proof
.
rewrite
pvs_eq
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
Hinv
rf
[|
k
]
Ef
σ
???
;
try
lia
.
rewrite
pvs_eq
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
Hinv
[|
k
]
Ef
σ
rf
???
;
try
lia
.
apply
ownI_spec
in
Hinv
;
last
auto
.
destruct
(
wsat_open
k
Ef
σ
(
r
⋅
rf
)
i
P
)
as
(
rP
&?&?)
;
auto
.
{
rewrite
lookup_wld_op_l
?Hinv
;
eauto
;
apply
dist_le
with
(
S
n
)
;
eauto
.
}
...
...
@@ -121,7 +121,7 @@ Qed.
Lemma
pvs_closeI
i
P
:
ownI
i
P
∧
▷
P
={
∅
,{[
i
]}}=>
True
.
Proof
.
rewrite
pvs_eq
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
[?
HP
]
rf
[|
k
]
Ef
σ
?
HE
?
;
try
lia
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
[?
HP
]
[|
k
]
Ef
σ
rf
?
HE
?
;
try
lia
.
exists
∅
;
split
;
[
done
|].
rewrite
left_id
;
apply
wsat_close
with
P
r
.
-
apply
ownI_spec
,
uPred_closed
with
(
S
n
)
;
auto
.
...
...
@@ -133,7 +133,7 @@ Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m
~~>
:
P
→
ownG
m
={
E
}=>
∃
m'
,
■
P
m'
∧
ownG
m'
.
Proof
.
rewrite
pvs_eq
.
intros
Hup
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
/
ownG_spec
Hinv
rf
[|
k
]
Ef
σ
???
;
try
lia
.
uPred
.
unseal
;
split
=>
-[|
n
]
r
?
/
ownG_spec
Hinv
[|
k
]
Ef
σ
rf
???
;
try
lia
.
destruct
(
wsat_update_gst
k
(
E
∪
Ef
)
σ
r
rf
m
P
)
as
(
m'
&?&?)
;
eauto
.
{
apply
cmra_includedN_le
with
(
S
n
)
;
auto
.
}
by
exists
(
update_gst
m'
r
)
;
split
;
[
exists
m'
;
split
;
[|
apply
ownG_spec
]|].
...
...
@@ -141,7 +141,7 @@ Qed.
Lemma
pvs_allocI
E
P
:
¬
set_finite
E
→
▷
P
={
E
}=>
∃
i
,
■
(
i
∈
E
)
∧
ownI
i
P
.
Proof
.
rewrite
pvs_eq
.
intros
?
;
rewrite
/
ownI
;
uPred
.
unseal
.
split
=>
-[|
n
]
r
?
HP
rf
[|
k
]
Ef
σ
???
;
try
lia
.
split
=>
-[|
n
]
r
?
HP
[|
k
]
Ef
σ
rf
???
;
try
lia
.
destruct
(
wsat_alloc
k
E
Ef
σ
rf
P
r
)
as
(
i
&?&?&?)
;
auto
.
{
apply
uPred_closed
with
n
;
eauto
.
}
exists
(
Res
{[
i
:
=
to_agree
(
Next
(
iProp_unfold
P
))
]}
∅
∅
).
...
...
program_logic/weakestpre.v
View file @
7522d558
...
...
@@ -10,7 +10,7 @@ Local Hint Extern 10 (✓{_} _) =>
end
;
solve_validN
.
Record
wp_go
{
Λ
Σ
}
(
E
:
coPset
)
(
Φ
Φ
fork
:
expr
Λ
→
nat
→
iRes
Λ
Σ
→
Prop
)
(
k
:
nat
)
(
rf
:
iRes
Λ
Σ
)
(
e1
:
expr
Λ
)
(
σ
1
:
state
Λ
)
:
=
{
(
k
:
nat
)
(
σ
1
:
state
Λ
)
(
rf
:
iRes
Λ
Σ
)
(
e1
:
expr
Λ
)
:
=
{
wf_safe
:
reducible
e1
σ
1
;
wp_step
e2
σ
2
ef
:
prim_step
e1
σ
1 e2
σ
2
ef
→
...
...
@@ -24,11 +24,11 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
|
wp_pre_value
n
r
v
:
(|={
E
}=>
Φ
v
)%
I
n
r
→
wp_pre
E
Φ
(
of_val
v
)
n
r
|
wp_pre_step
n
r1
e1
:
to_val
e1
=
None
→
(
∀
rf
k
Ef
σ
1
,
(
∀
k
Ef
σ
1
rf
,
0
<
k
<
n
→
E
⊥
Ef
→
wsat
(
S
k
)
(
E
∪
Ef
)
σ
1
(
r1
⋅
rf
)
→
wp_go
(
E
∪
Ef
)
(
wp_pre
E
Φ
)
(
wp_pre
⊤
(
λ
_
,
True
%
I
))
k
rf
e1
σ
1
)
→
(
wp_pre
⊤
(
λ
_
,
True
%
I
))
k
σ
1
rf
e1
)
→
wp_pre
E
Φ
e1
n
r1
.
Program
Definition
wp_def
{
Λ
Σ
}
(
E
:
coPset
)
(
e
:
expr
Λ
)
(
Φ
:
val
Λ
→
iProp
Λ
Σ
)
:
iProp
Λ
Σ
:
=
{|
uPred_holds
:
=
wp_pre
E
Φ
e
|}.
...
...
@@ -37,8 +37,8 @@ Next Obligation.
induction
n
as
[
n
IH
]
using
lt_wf_ind
;
intros
Φ
E
e
r1
r1'
.
destruct
1
as
[|
n
r1
e1
?
Hgo
].
-
constructor
;
eauto
using
uPred_mono
.
-
intros
[
rf'
Hr
]
;
constructor
;
[
done
|
intros
rf
k
Ef
σ
1
???].
destruct
(
Hgo
(
rf'
⋅
rf
)
k
Ef
σ
1
)
as
[
Hsafe
Hstep
]
;
-
intros
[
rf'
Hr
]
;
constructor
;
[
done
|
intros
k
Ef
σ
1
rf
???].
destruct
(
Hgo
k
Ef
σ
1
(
rf'
⋅
rf
))
as
[
Hsafe
Hstep
]
;
rewrite
?assoc
-?(
dist_le
_
_
_
_
Hr
)
;
auto
;
constructor
;
[
done
|].
intros
e2
σ
2
ef
?
;
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
auto
.
exists
r2
,
(
r2'
⋅
rf'
)
;
split_and
?
;
eauto
10
using
(
IH
k
),
cmra_includedN_l
.
...
...
@@ -85,8 +85,8 @@ Proof.
induction
n'
as
[
n'
IH
]
using
lt_wf_ind
=>
e
r
.
destruct
3
as
[
n'
r
v
HpvsQ
|
n'
r
e1
?
Hgo
].
{
constructor
.
by
eapply
pvs_ne
,
HpvsQ
;
eauto
.
}
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
destruct
(
Hgo
rf
k
Ef
σ
1
)
as
[
Hsafe
Hstep
]
;
auto
.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
destruct
(
Hgo
k
Ef
σ
1
rf
)
as
[
Hsafe
Hstep
]
;
auto
.
split
;
[
done
|
intros
e2
σ
2
ef
?].
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
auto
.
exists
r2
,
r2'
;
split_and
?
;
[|
eapply
IH
|]
;
eauto
.
...
...
@@ -104,10 +104,10 @@ Proof.
revert
e
r
;
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
e
r
.
destruct
2
as
[
n'
r
v
HpvsQ
|
n'
r
e1
?
Hgo
].
{
constructor
;
eapply
pvs_mask_frame_mono
,
HpvsQ
;
eauto
.
}
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
assert
(
E2
∪
Ef
=
E1
∪
(
E2
∖
E1
∪
Ef
))
as
HE'
.
{
by
rewrite
assoc_L
-
union_difference_L
.
}
destruct
(
Hgo
rf
k
((
E2
∖
E1
)
∪
Ef
)
σ
1
)
as
[
Hsafe
Hstep
]
;
rewrite
-
?HE'
;
auto
.
destruct
(
Hgo
k
((
E2
∖
E1
)
∪
Ef
)
σ
1
rf
)
as
[
Hsafe
Hstep
]
;
rewrite
-
?HE'
;
auto
.
split
;
[
done
|
intros
e2
σ
2
ef
?].
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
auto
.
exists
r2
,
r2'
;
split_and
?
;
[
rewrite
HE'
|
eapply
IH
|]
;
eauto
.
...
...
@@ -127,7 +127,7 @@ Qed.
Lemma
wp_step_inv
E
Ef
Φ
e
k
n
σ
r
rf
:
to_val
e
=
None
→
0
<
k
<
n
→
E
⊥
Ef
→
wp_def
E
e
Φ
n
r
→
wsat
(
S
k
)
(
E
∪
Ef
)
σ
(
r
⋅
rf
)
→
wp_go
(
E
∪
Ef
)
(
λ
e
,
wp_def
E
e
Φ
)
(
λ
e
,
wp_def
⊤
e
(
λ
_
,
True
%
I
))
k
rf
e
σ
.
wp_go
(
E
∪
Ef
)
(
λ
e
,
wp_def
E
e
Φ
)
(
λ
e
,
wp_def
⊤
e
(
λ
_
,
True
%
I
))
k
σ
rf
e
.
Proof
.
intros
He
;
destruct
3
;
[
by
rewrite
?to_of_val
in
He
|
eauto
].
Qed
.
...
...
@@ -140,8 +140,8 @@ Proof.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
;
[
apply
of_to_val
in
He
;
subst
|].
{
constructor
;
eapply
pvs_trans'
,
pvs_mono
,
Hvs
;
eauto
.
split
=>
???
;
apply
wp_value_inv
.
}
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
rewrite
pvs_eq
in
Hvs
.
destruct
(
Hvs
rf
(
S
k
)
Ef
σ
1
)
as
(
r'
&
Hwp
&?)
;
auto
.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
rewrite
pvs_eq
in
Hvs
.
destruct
(
Hvs
(
S
k
)
Ef
σ
1
rf
)
as
(
r'
&
Hwp
&?)
;
auto
.
eapply
wp_step_inv
with
(
S
k
)
r'
;
eauto
.
Qed
.
Lemma
wp_pvs
E
e
Φ
:
WP
e
@
E
{{
v
,
|={
E
}=>
Φ
v
}}
⊢
WP
e
@
E
{{
Φ
}}.
...
...
@@ -150,7 +150,7 @@ Proof.
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
e
r
Hr
H
Φ
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
;
[
apply
of_to_val
in
He
;
subst
|].
{
constructor
;
apply
pvs_trans'
,
(
wp_value_inv
_
(
pvs
E
E
∘
Φ
))
;
auto
.
}
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
destruct
(
wp_step_inv
E
Ef
(
pvs
E
E
∘
Φ
)
e
k
n
σ
1
r
rf
)
as
[?
Hstep
]
;
auto
.
split
;
[
done
|
intros
e2
σ
2
ef
?].
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&
Hwp'
&?)
;
auto
.
...
...
@@ -161,8 +161,8 @@ Lemma wp_atomic E1 E2 e Φ :
(|={
E1
,
E2
}=>
WP
e
@
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})
⊢
WP
e
@
E1
{{
Φ
}}.
Proof
.
rewrite
wp_eq
pvs_eq
.
intros
?
He
;
split
=>
n
r
?
Hvs
;
constructor
.
eauto
using
atomic_not_val
.
intros
rf
k
Ef
σ
1
???.
destruct
(
Hvs
rf
(
S
k
)
Ef
σ
1
)
as
(
r'
&
Hwp
&?)
;
auto
.
eauto
using
atomic_not_val
.
intros
k
Ef
σ
1
rf
???.
destruct
(
Hvs
(
S
k
)
Ef
σ
1
rf
)
as
(
r'
&
Hwp
&?)
;
auto
.
destruct
(
wp_step_inv
E2
Ef
(
pvs_def
E2
E1
∘
Φ
)
e
k
(
S
k
)
σ
1
r'
rf
)
as
[
Hsafe
Hstep
]
;
auto
using
atomic_not_val
;
[].
split
;
[
done
|]=>
e2
σ
2
ef
?.
...
...
@@ -170,7 +170,7 @@ Proof.
destruct
Hwp'
as
[
k
r2
v
Hvs'
|
k
r2
e2
Hgo
]
;
[|
destruct
(
atomic_step
e
σ
1 e2
σ
2
ef
)
;
naive_solver
].
rewrite
-
pvs_eq
in
Hvs'
.
apply
pvs_trans
in
Hvs'
;
auto
.
rewrite
pvs_eq
in
Hvs'
.
destruct
(
Hvs'
(
r2'
⋅
rf
)
k
Ef
σ
2
)
as
(
r3
&[])
;
rewrite
?assoc
;
auto
.
destruct
(
Hvs'
k
Ef
σ
2
(
r2'
⋅
rf
))
as
(
r3
&[])
;
rewrite
?assoc
;
auto
.
exists
r3
,
r2'
;
split_and
?
;
last
done
.
-
by
rewrite
-
assoc
.
-
constructor
;
apply
pvs_intro
;
auto
.
...
...
@@ -183,8 +183,8 @@ Proof.
destruct
1
as
[|
n
r
e
?
Hgo
]=>?.
{
constructor
.
rewrite
-
uPred_sep_eq
;
apply
pvs_frame_r
;
auto
.
uPred
.
unseal
;
exists
r
,
rR
;
eauto
.
}
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
destruct
(
Hgo
(
rR
⋅
rf
)
k
Ef
σ
1
)
as
[
Hsafe
Hstep
]
;
auto
.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
destruct
(
Hgo
k
Ef
σ
1
(
rR
⋅
rf
)
)
as
[
Hsafe
Hstep
]
;
auto
.
{
by
rewrite
assoc
.
}
split
;
[
done
|
intros
e2
σ
2
ef
?].
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
auto
.
...
...
@@ -199,27 +199,27 @@ Lemma wp_frame_step_r E E1 E2 e Φ R :
Proof
.
rewrite
wp_eq
pvs_eq
=>
He
??.
uPred
.
unseal
;
split
;
intros
n
r'
Hvalid
(
r
&
rR
&
Hr
&
Hwp
&
HR
)
;
cofe_subst
.
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
??
Hws1
.
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
??
Hws1
.
destruct
Hwp
as
[|
n
r
e
?
Hgo
]
;
[
by
rewrite
to_of_val
in
He
|].
(* "execute" HR *)
destruct
(
HR
(
r
⋅
rf
)
(
S
k
)
(
E
∪
Ef
)
σ
1
)
as
(
s
&
Hvs
&
Hws2
)
;
auto
.
destruct
(
HR
(
S
k
)
(
E
∪
Ef
)
σ
1
(
r
⋅
rf
)
)
as
(
s
&
Hvs
&
Hws2
)
;
auto
.
{
eapply
wsat_proper
,
Hws1
;
first
by
set_solver
+.
by
rewrite
assoc
[
rR
⋅
_
]
comm
.
}
clear
Hws1
HR
.
(* Take a step *)
destruct
(
Hgo
(
s
⋅
rf
)
k
(
E2
∪
Ef
)
σ
1
)
as
[
Hsafe
Hstep
]
;
auto
.
destruct
(
Hgo
k
(
E2
∪
Ef
)
σ
1
(
s
⋅
rf
)
)
as
[
Hsafe
Hstep
]
;
auto
.
{
eapply
wsat_proper
,
Hws2
;
first
by
set_solver
+.
by
rewrite
!
assoc
[
s
⋅
_
]
comm
.
}
clear
Hgo
.
split
;
[
done
|
intros
e2
σ
2
ef
?].
destruct
(
Hstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&
Hws3
&?&?)
;
auto
.
clear
Hws2
.
(* Execute 2nd part of the view shift *)
destruct
(
Hvs
(
r2
⋅
r2'
⋅
rf
)
k
(
E
∪
Ef
)
σ
2
)
as
(
t
&
HR
&
Hws4
)
;
auto
.
destruct
(
Hvs
k
(
E
∪
Ef
)
σ
2
(
r2
⋅
r2'
⋅
rf
))
as
(
t
&
HR
&
Hws4
)
;
auto
.
{
eapply
wsat_proper
,
Hws3
;
first
by
set_solver
+.
by
rewrite
!
assoc
[
_
⋅
s
]
comm
!
assoc
.
}
clear
Hvs
Hws3
.
(* Execute the rest of e *)
exists
(
r2
⋅
t
),
r2'
.
split_and
?
;
auto
.
exists
(
r2
⋅
t
),
r2'
;
split_and
?
;
auto
.
-
eapply
wsat_proper
,
Hws4
;
first
by
set_solver
+.
by
rewrite
!
assoc
[
_
⋅
t
]
comm
.
-
rewrite
-
uPred_sep_eq
.
move
:
wp_frame_r
.
rewrite
wp_eq
=>
Hframe
.
...
...
@@ -234,8 +234,8 @@ Proof.
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
e
r
?.
destruct
1
as
[|
n
r
e
?
Hgo
].
{
rewrite
-
wp_eq
.
apply
pvs_wp
;
rewrite
?wp_eq
;
done
.
}
constructor
;
auto
using
fill_not_val
=>
rf
k
Ef
σ
1
???.
destruct
(
Hgo
rf
k
Ef
σ
1
)
as
[
Hsafe
Hstep
]
;
auto
.
constructor
;
auto
using
fill_not_val
=>
k
Ef
σ
1
rf
???.
destruct
(
Hgo
k
Ef
σ
1
rf
)
as
[
Hsafe
Hstep
]
;
auto
.
split
.
{
destruct
Hsafe
as
(
e2
&
σ
2
&
ef
&?).
by
exists
(
K
e2
),
σ
2
,
ef
;
apply
fill_step
.
}
...
...
program_logic/weakestpre_fix.v
View file @
7522d558
...
...
@@ -18,7 +18,7 @@ Local Notation coPsetC := (leibnizC (coPset)).
Program
Definition
wp_pre
(
wp
:
coPsetC
-
n
>
exprC
Λ
-
n
>
(
valC
Λ
-
n
>
iProp
)
-
n
>
iProp
)
(
E
:
coPset
)
(
e1
:
expr
Λ
)
(
Φ
:
valC
Λ
-
n
>
iProp
)
:
iProp
:
=
{|
uPred_holds
n
r1
:
=
∀
rf
k
Ef
σ
1
,
{|
uPred_holds
n
r1
:
=
∀
k
Ef
σ
1
rf
,
0
≤
k
<
n
→
E
⊥
Ef
→
wsat
(
S
k
)
(
E
∪
Ef
)
σ
1
(
r1
⋅
rf
)
→
(
∀
v
,
to_val
e1
=
Some
v
→
...
...
@@ -31,9 +31,9 @@ Program Definition wp_pre
wp
E
e2
Φ
k
r2
∧
default
True
ef
(
λ
ef
,
wp
⊤
ef
(
cconst
True
%
I
)
k
r2'
)))
|}.
Next
Obligation
.
intros
wp
E
e1
Φ
n
r1
r2
Hwp
[
r3
Hr2
]
rf
k
Ef
σ
1
??.
intros
wp
E
e1
Φ
n
r1
r2
Hwp
[
r3
Hr2
]
k
Ef
σ
1
rf
??.
rewrite
(
dist_le
_
_
_
_
Hr2
)
;
last
lia
.
intros
Hws
.
destruct
(
Hwp
(
r3
⋅
rf
)
k
Ef
σ
1
)
as
[
Hval
Hstep
]
;
rewrite
?assoc
;
auto
.
destruct
(
Hwp
k
Ef
σ
1
(
r3
⋅
rf
))
as
[
Hval
Hstep
]
;
rewrite
?assoc
;
auto
.
split
.
-
intros
v
Hv
.
destruct
(
Hval
v
Hv
)
as
[
r4
[??]].
exists
(
r4
⋅
r3
).
rewrite
-
assoc
.
eauto
using
uPred_mono
,
cmra_includedN_l
.
...
...
@@ -51,8 +51,8 @@ Lemma wp_pre_contractive' n E e Φ1 Φ2 r
(
∀
i
:
nat
,
i
<
n
→
wp1
≡
{
i
}
≡
wp2
)
→
Φ
1
≡
{
n
}
≡
Φ
2
→
wp_pre
wp1
E
e
Φ
1
n
r
→
wp_pre
wp2
E
e
Φ
2
n
r
.
Proof
.
intros
HI
H
Φ
Hwp
rf
k
Ef
σ
1
???.
destruct
(
Hwp
rf
k
Ef
σ
1
)
as
[
Hval
Hstep
]
;
auto
.
intros
HI
H
Φ
Hwp
k
Ef
σ
1
rf
???.
destruct
(
Hwp
k
Ef
σ
1
rf
)
as
[
Hval
Hstep
]
;
auto
.
split
.
{
intros
v
?.
destruct
(
Hval
v
)
as
(
r2
&?&?)
;
auto
.
exists
r2
.
split
;
[
apply
H
Φ
|]
;
auto
.
}
...
...
@@ -95,25 +95,25 @@ Proof.
-
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
r1
E
e
Φ
?
Hwp
.
case
EQ
:
(
to_val
e
)=>[
v
|].
+
rewrite
-(
of_to_val
_
_
EQ
)
{
IH
}.
constructor
.
rewrite
pvs_eq
.
intros
rf
[|
k
]
Ef
σ
???
;
first
omega
.
intros
[|
k
]
Ef
σ
rf
???
;
first
omega
.
apply
wp_fix_unfold
in
Hwp
;
last
done
.
destruct
(
Hwp
rf
k
Ef
σ
)
;
auto
.
+
constructor
;
[
done
|]=>
rf
k
Ef
σ
1
???.
destruct
(
Hwp
k
Ef
σ
rf
)
;
auto
.
+
constructor
;
[
done
|]=>
k
Ef
σ
1
rf
???.
apply
wp_fix_unfold
in
Hwp
;
last
done
.
destruct
(
Hwp
rf
k
Ef
σ
1
)
as
[
Hval
[
Hred
Hpstep
]]
;
auto
.
destruct
(
Hwp
k
Ef
σ
1
rf
)
as
[
Hval
[
Hred
Hpstep
]]
;
auto
.
split
;
[
done
|]=>
e2
σ
2
ef
?.
destruct
(
Hpstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
[
done
..|].
exists
r2
,
r2'
;
split_and
?
;
auto
.
intros
?
->.
change
(
weakestpre
.
wp_pre
⊤
(
cconst
True
%
I
)
e'
k
r2'
)
;
eauto
.
-
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
r1
E
e
Φ
?
Hwp
.
apply
wp_fix_unfold
;
[
done
|]=>
rf
k
Ef
σ
1
???.
split
.
apply
wp_fix_unfold
;
[
done
|]=>
k
Ef
σ
1
rf
???.
split
.
+
intros
v
Hval
.
destruct
Hwp
as
[???
Hpvs
|]
;
rewrite
?to_of_val
in
Hval
;
simplify_eq
/=.
rewrite
pvs_eq
in
Hpvs
.
destruct
(
Hpvs
rf
(
S
k
)
Ef
σ
1
)
as
(
r2
&?&?)
;
eauto
.
destruct
(
Hpvs
(
S
k
)
Ef
σ
1
rf
)
as
(
r2
&?&?)
;
eauto
.
+
intros
Hval
?.
destruct
Hwp
as
[|????
Hwp
]
;
rewrite
?to_of_val
in
Hval
;
simplify_eq
/=.
edestruct
(
Hwp
rf
k
Ef
σ
1
)
as
[?
Hpstep
]
;
auto
.
edestruct
(
Hwp
k
Ef
σ
1
rf
)
as
[?
Hpstep
]
;
auto
.
split
;
[
done
|]=>
e2
σ
2
ef
?.
destruct
(
Hpstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&?&?&?)
;
auto
.
exists
r2
,
r2'
.
destruct
ef
;
simpl
;
auto
.
...
...
Write
Preview
Supports
Markdown
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