Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
c7390af8
Commit
c7390af8
authored
Mar 10, 2016
by
Ralf Jung
Browse files
new (hopefully final) notation for wp: the keyword WP
parent
462cc285
Changes
14
Hide whitespace changes
Inline
Side-by-side
barrier/client.v
View file @
c7390af8
...
...
@@ -16,7 +16,7 @@ Section client.
Local
Notation
iProp
:=
(
iPropG
heap_lang
Σ
).
Definition
y_inv
q
y
:
iProp
:=
(
∃
f
:
val
,
y
↦
{
q
}
f
★
□
∀
n
:
Z
,
#
>
f
§
n
{{
λ
v
,
v
=
§
(
n
+
42
)
}}
)
%
I
.
(
∃
f
:
val
,
y
↦
{
q
}
f
★
□
∀
n
:
Z
,
WP
f
§
n
{{
λ
v
,
v
=
§
(
n
+
42
)
}}
)
%
I
.
Lemma
y_inv_split
q
y
:
y_inv
q
y
⊢
(
y_inv
(
q
/
2
)
y
★
y_inv
(
q
/
2
)
y
).
...
...
@@ -28,7 +28,7 @@ Section client.
Lemma
worker_safe
q
(
n
:
Z
)
(
b
y
:
loc
)
:
(
heap_ctx
heapN
★
recv
heapN
N
b
(
y_inv
q
y
))
⊢
#
>
worker
n
(
%
b
)
(
%
y
)
{{
λ
_
,
True
}}
.
⊢
WP
worker
n
(
%
b
)
(
%
y
)
{{
λ
_
,
True
}}
.
Proof
.
rewrite
/
worker
.
wp_lam
.
wp_let
.
ewp
apply
wait_spec
.
rewrite
comm
.
apply
sep_mono_r
.
apply
wand_intro_l
.
...
...
@@ -42,7 +42,7 @@ Section client.
Qed
.
Lemma
client_safe
:
heapN
⊥
N
→
heap_ctx
heapN
⊢
#
>
client
{{
λ
_
,
True
}}
.
heapN
⊥
N
→
heap_ctx
heapN
⊢
WP
client
{{
λ
_
,
True
}}
.
Proof
.
intros
?
.
rewrite
/
client
.
(
ewp
eapply
wp_alloc
);
eauto
with
I
.
strip_later
.
apply
forall_intro
=>
y
.
...
...
barrier/proof.v
View file @
c7390af8
...
...
@@ -112,7 +112,7 @@ Qed.
Lemma
newbarrier_spec
(
P
:
iProp
)
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
(
heap_ctx
heapN
★
∀
l
,
recv
l
P
★
send
l
P
-
★
Φ
(
%
l
))
⊢
#
>
newbarrier
§
()
{{
Φ
}}
.
⊢
WP
newbarrier
§
()
{{
Φ
}}
.
Proof
.
intros
HN
.
rewrite
/
newbarrier
.
wp_seq
.
rewrite
-
wp_pvs
.
wp
eapply
wp_alloc
;
eauto
with
I
ndisj
.
...
...
@@ -151,7 +151,7 @@ Proof.
Qed
.
Lemma
signal_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
send
l
P
★
P
★
Φ
§
())
⊢
#
>
signal
(
%
l
)
{{
Φ
}}
.
(
send
l
P
★
P
★
Φ
§
())
⊢
WP
signal
(
%
l
)
{{
Φ
}}
.
Proof
.
rewrite
/
signal
/
send
/
barrier_ctx
.
rewrite
sep_exist_r
.
apply
exist_elim
=>
γ
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>?
.
wp_let
.
...
...
@@ -176,7 +176,7 @@ Proof.
Qed
.
Lemma
wait_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
recv
l
P
★
(
P
-
★
Φ
§
()))
⊢
#
>
wait
(
%
l
)
{{
Φ
}}
.
(
recv
l
P
★
(
P
-
★
Φ
§
()))
⊢
WP
wait
(
%
l
)
{{
Φ
}}
.
Proof
.
rename
P
into
R
.
wp_rec
.
rewrite
{
1
}/
recv
/
barrier_ctx
.
rewrite
!
sep_exist_r
.
...
...
heap_lang/derived.v
View file @
c7390af8
...
...
@@ -19,36 +19,36 @@ Implicit Types Φ : val → iProp heap_lang Σ.
(
**
Proof
rules
for
the
sugar
*
)
Lemma
wp_lam
E
x
ef
e
v
Φ
:
to_val
e
=
Some
v
→
▷
#
>
subst
'
x
e
ef
@
E
{{
Φ
}}
⊢
#
>
App
(
Lam
x
ef
)
e
@
E
{{
Φ
}}
.
▷
WP
subst
'
x
e
ef
@
E
{{
Φ
}}
⊢
WP
App
(
Lam
x
ef
)
e
@
E
{{
Φ
}}
.
Proof
.
intros
.
by
rewrite
-
wp_rec
.
Qed
.
Lemma
wp_let
E
x
e1
e2
v
Φ
:
to_val
e1
=
Some
v
→
▷
#
>
subst
'
x
e1
e2
@
E
{{
Φ
}}
⊢
#
>
Let
x
e1
e2
@
E
{{
Φ
}}
.
▷
WP
subst
'
x
e1
e2
@
E
{{
Φ
}}
⊢
WP
Let
x
e1
e2
@
E
{{
Φ
}}
.
Proof
.
apply
wp_lam
.
Qed
.
Lemma
wp_seq
E
e1
e2
v
Φ
:
to_val
e1
=
Some
v
→
▷
#
>
e2
@
E
{{
Φ
}}
⊢
#
>
Seq
e1
e2
@
E
{{
Φ
}}
.
▷
WP
e2
@
E
{{
Φ
}}
⊢
WP
Seq
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
?
.
by
rewrite
-
wp_let
.
Qed
.
Lemma
wp_skip
E
Φ
:
▷
Φ
(
LitV
LitUnit
)
⊢
#
>
Skip
@
E
{{
Φ
}}
.
Lemma
wp_skip
E
Φ
:
▷
Φ
(
LitV
LitUnit
)
⊢
WP
Skip
@
E
{{
Φ
}}
.
Proof
.
rewrite
-
wp_seq
// -wp_value //. Qed.
Lemma
wp_match_inl
E
e0
v0
x1
e1
x2
e2
Φ
:
to_val
e0
=
Some
v0
→
▷
#
>
subst
'
x1
e0
e1
@
E
{{
Φ
}}
⊢
#
>
Match
(
InjL
e0
)
x1
e1
x2
e2
@
E
{{
Φ
}}
.
▷
WP
subst
'
x1
e0
e1
@
E
{{
Φ
}}
⊢
WP
Match
(
InjL
e0
)
x1
e1
x2
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
by
rewrite
-
wp_case_inl
// -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma
wp_match_inr
E
e0
v0
x1
e1
x2
e2
Φ
:
to_val
e0
=
Some
v0
→
▷
#
>
subst
'
x2
e0
e2
@
E
{{
Φ
}}
⊢
#
>
Match
(
InjR
e0
)
x1
e1
x2
e2
@
E
{{
Φ
}}
.
▷
WP
subst
'
x2
e0
e2
@
E
{{
Φ
}}
⊢
WP
Match
(
InjR
e0
)
x1
e1
x2
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
by
rewrite
-
wp_case_inr
// -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma
wp_le
E
(
n1
n2
:
Z
)
P
Φ
:
(
n1
≤
n2
→
P
⊢
▷
Φ
(
LitV
(
LitBool
true
)))
→
(
n2
<
n1
→
P
⊢
▷
Φ
(
LitV
(
LitBool
false
)))
→
P
⊢
#
>
BinOp
LeOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
P
⊢
WP
BinOp
LeOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
wp_bin_op
//; [].
destruct
(
bool_decide_reflect
(
n1
≤
n2
));
by
eauto
with
omega
.
...
...
@@ -57,7 +57,7 @@ Qed.
Lemma
wp_lt
E
(
n1
n2
:
Z
)
P
Φ
:
(
n1
<
n2
→
P
⊢
▷
Φ
(
LitV
(
LitBool
true
)))
→
(
n2
≤
n1
→
P
⊢
▷
Φ
(
LitV
(
LitBool
false
)))
→
P
⊢
#
>
BinOp
LtOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
P
⊢
WP
BinOp
LtOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
wp_bin_op
//; [].
destruct
(
bool_decide_reflect
(
n1
<
n2
));
by
eauto
with
omega
.
...
...
@@ -66,7 +66,7 @@ Qed.
Lemma
wp_eq
E
(
n1
n2
:
Z
)
P
Φ
:
(
n1
=
n2
→
P
⊢
▷
Φ
(
LitV
(
LitBool
true
)))
→
(
n1
≠
n2
→
P
⊢
▷
Φ
(
LitV
(
LitBool
false
)))
→
P
⊢
#
>
BinOp
EqOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
P
⊢
WP
BinOp
EqOp
(
Lit
(
LitInt
n1
))
(
Lit
(
LitInt
n2
))
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
wp_bin_op
//; [].
destruct
(
bool_decide_reflect
(
n1
=
n2
));
by
eauto
with
omega
.
...
...
heap_lang/heap.v
View file @
c7390af8
...
...
@@ -142,7 +142,7 @@ Section heap.
to_val
e
=
Some
v
→
P
⊢
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊢
(
▷
∀
l
,
l
↦
v
-
★
Φ
(
LocV
l
))
→
P
⊢
#
>
Alloc
e
@
E
{{
Φ
}}
.
P
⊢
WP
Alloc
e
@
E
{{
Φ
}}
.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>
???
HP
.
trans
(
|={
E
}=>
auth_own
heap_name
∅
★
P
)
%
I
.
...
...
@@ -167,7 +167,7 @@ Section heap.
Lemma
wp_load
N
E
l
q
v
P
Φ
:
P
⊢
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊢
(
▷
l
↦
{
q
}
v
★
▷
(
l
↦
{
q
}
v
-
★
Φ
v
))
→
P
⊢
#
>
Load
(
Loc
l
)
@
E
{{
Φ
}}
.
P
⊢
WP
Load
(
Loc
l
)
@
E
{{
Φ
}}
.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>
??
HP
Φ
.
apply
(
auth_fsa
'
heap_inv
(
wp_fsa
_
)
id
)
...
...
@@ -184,7 +184,7 @@ Section heap.
to_val
e
=
Some
v
→
P
⊢
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊢
(
▷
l
↦
v
'
★
▷
(
l
↦
v
-
★
Φ
(
LitV
LitUnit
)))
→
P
⊢
#
>
Store
(
Loc
l
)
e
@
E
{{
Φ
}}
.
P
⊢
WP
Store
(
Loc
l
)
e
@
E
{{
Φ
}}
.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>
???
HP
Φ
.
apply
(
auth_fsa
'
heap_inv
(
wp_fsa
_
)
(
alter
(
λ
_
,
Frac
1
(
DecAgree
v
))
l
))
...
...
@@ -201,7 +201,7 @@ Section heap.
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
v
'
≠
v1
→
P
⊢
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊢
(
▷
l
↦
{
q
}
v
'
★
▷
(
l
↦
{
q
}
v
'
-
★
Φ
(
LitV
(
LitBool
false
))))
→
P
⊢
#
>
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
P
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>?????
HP
Φ
.
apply
(
auth_fsa
'
heap_inv
(
wp_fsa
_
)
id
)
...
...
@@ -218,7 +218,7 @@ Section heap.
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
P
⊢
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊢
(
▷
l
↦
v1
★
▷
(
l
↦
v2
-
★
Φ
(
LitV
(
LitBool
true
))))
→
P
⊢
#
>
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
P
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>
????
HP
Φ
.
apply
(
auth_fsa
'
heap_inv
(
wp_fsa
_
)
(
alter
(
λ
_
,
Frac
1
(
DecAgree
v2
))
l
))
...
...
heap_lang/lifting.v
View file @
c7390af8
...
...
@@ -15,14 +15,14 @@ Implicit Types ef : option (expr []).
(
**
Bind
.
*
)
Lemma
wp_bind
{
E
e
}
K
Φ
:
#
>
e
@
E
{{
λ
v
,
#
>
fill
K
(
of_val
v
)
@
E
{{
Φ
}}}}
⊢
#
>
fill
K
e
@
E
{{
Φ
}}
.
WP
e
@
E
{{
λ
v
,
WP
fill
K
(
of_val
v
)
@
E
{{
Φ
}}}}
⊢
WP
fill
K
e
@
E
{{
Φ
}}
.
Proof
.
apply
weakestpre
.
wp_bind
.
Qed
.
(
**
Base
axioms
for
core
primitives
of
the
language
:
Stateful
reductions
.
*
)
Lemma
wp_alloc_pst
E
σ
e
v
Φ
:
to_val
e
=
Some
v
→
(
▷
ownP
σ
★
▷
(
∀
l
,
σ
!!
l
=
None
∧
ownP
(
<
[
l
:=
v
]
>
σ
)
-
★
Φ
(
LocV
l
)))
⊢
#
>
Alloc
e
@
E
{{
Φ
}}
.
⊢
WP
Alloc
e
@
E
{{
Φ
}}
.
Proof
.
(
*
TODO
RJ
:
This
works
around
ssreflect
bug
#
22.
*
)
intros
.
set
(
φ
v
'
σ'
ef
:=
∃
l
,
...
...
@@ -39,7 +39,7 @@ Qed.
Lemma
wp_load_pst
E
σ
l
v
Φ
:
σ
!!
l
=
Some
v
→
(
▷
ownP
σ
★
▷
(
ownP
σ
-
★
Φ
v
))
⊢
#
>
Load
(
Loc
l
)
@
E
{{
Φ
}}
.
(
▷
ownP
σ
★
▷
(
ownP
σ
-
★
Φ
v
))
⊢
WP
Load
(
Loc
l
)
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
v
σ
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
using
to_of_val
.
...
...
@@ -48,7 +48,7 @@ Qed.
Lemma
wp_store_pst
E
σ
l
e
v
v
'
Φ
:
to_val
e
=
Some
v
→
σ
!!
l
=
Some
v
'
→
(
▷
ownP
σ
★
▷
(
ownP
(
<
[
l
:=
v
]
>
σ
)
-
★
Φ
(
LitV
LitUnit
)))
⊢
#
>
Store
(
Loc
l
)
e
@
E
{{
Φ
}}
.
⊢
WP
Store
(
Loc
l
)
e
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
(
LitV
LitUnit
)
(
<
[
l
:=
v
]
>
σ
)
None
)
?
right_id
//; last by intros; inv_step; eauto.
...
...
@@ -57,7 +57,7 @@ Qed.
Lemma
wp_cas_fail_pst
E
σ
l
e1
v1
e2
v2
v
'
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v
'
→
v
'
≠
v1
→
(
▷
ownP
σ
★
▷
(
ownP
σ
-
★
Φ
(
LitV
$
LitBool
false
)))
⊢
#
>
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
(
LitV
$
LitBool
false
)
σ
None
)
?
right_id
//; last by intros; inv_step; eauto.
...
...
@@ -66,7 +66,7 @@ Qed.
Lemma
wp_cas_suc_pst
E
σ
l
e1
v1
e2
v2
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v1
→
(
▷
ownP
σ
★
▷
(
ownP
(
<
[
l
:=
v2
]
>
σ
)
-
★
Φ
(
LitV
$
LitBool
true
)))
⊢
#
>
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
(
LitV
$
LitBool
true
)
(
<
[
l
:=
v2
]
>
σ
)
None
)
?
right_id
//; last by intros; inv_step; eauto.
...
...
@@ -74,7 +74,7 @@ Qed.
(
**
Base
axioms
for
core
primitives
of
the
language
:
Stateless
reductions
*
)
Lemma
wp_fork
E
e
Φ
:
(
▷
Φ
(
LitV
LitUnit
)
★
▷
#
>
e
{{
λ
_
,
True
}}
)
⊢
#
>
Fork
e
@
E
{{
Φ
}}
.
(
▷
Φ
(
LitV
LitUnit
)
★
▷
WP
e
{{
λ
_
,
True
}}
)
⊢
WP
Fork
e
@
E
{{
Φ
}}
.
Proof
.
rewrite
-
(
wp_lift_pure_det_step
(
Fork
e
)
(
Lit
LitUnit
)
(
Some
e
))
//=;
last
by
intros
;
inv_step
;
eauto
.
...
...
@@ -83,8 +83,8 @@ Qed.
Lemma
wp_rec
E
f
x
e1
e2
v
Φ
:
to_val
e2
=
Some
v
→
▷
#
>
subst
'
x
e2
(
subst
'
f
(
Rec
f
x
e1
)
e1
)
@
E
{{
Φ
}}
⊢
#
>
App
(
Rec
f
x
e1
)
e2
@
E
{{
Φ
}}
.
▷
WP
subst
'
x
e2
(
subst
'
f
(
Rec
f
x
e1
)
e1
)
@
E
{{
Φ
}}
⊢
WP
App
(
Rec
f
x
e1
)
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
App
_
_
)
(
subst
'
x
e2
(
subst
'
f
(
Rec
f
x
e1
)
e1
))
None
)
//= ?right_id;
...
...
@@ -94,13 +94,13 @@ Qed.
Lemma
wp_rec
'
E
f
x
erec
e1
e2
v2
Φ
:
e1
=
Rec
f
x
erec
→
to_val
e2
=
Some
v2
→
▷
#
>
subst
'
x
e2
(
subst
'
f
e1
erec
)
@
E
{{
Φ
}}
⊢
#
>
App
e1
e2
@
E
{{
Φ
}}
.
▷
WP
subst
'
x
e2
(
subst
'
f
e1
erec
)
@
E
{{
Φ
}}
⊢
WP
App
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
->
.
apply
wp_rec
.
Qed
.
Lemma
wp_un_op
E
op
l
l
'
Φ
:
un_op_eval
op
l
=
Some
l
'
→
▷
Φ
(
LitV
l
'
)
⊢
#
>
UnOp
op
(
Lit
l
)
@
E
{{
Φ
}}
.
▷
Φ
(
LitV
l
'
)
⊢
WP
UnOp
op
(
Lit
l
)
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
UnOp
op
_
)
(
Lit
l
'
)
None
)
?
right_id
-?
wp_value
//; intros; inv_step; eauto.
...
...
@@ -108,21 +108,21 @@ Qed.
Lemma
wp_bin_op
E
op
l1
l2
l
'
Φ
:
bin_op_eval
op
l1
l2
=
Some
l
'
→
▷
Φ
(
LitV
l
'
)
⊢
#
>
BinOp
op
(
Lit
l1
)
(
Lit
l2
)
@
E
{{
Φ
}}
.
▷
Φ
(
LitV
l
'
)
⊢
WP
BinOp
op
(
Lit
l1
)
(
Lit
l2
)
@
E
{{
Φ
}}
.
Proof
.
intros
Heval
.
rewrite
-
(
wp_lift_pure_det_step
(
BinOp
op
_
_
)
(
Lit
l
'
)
None
)
?
right_id
-?
wp_value
//; intros; inv_step; eauto.
Qed
.
Lemma
wp_if_true
E
e1
e2
Φ
:
▷
#
>
e1
@
E
{{
Φ
}}
⊢
#
>
If
(
Lit
(
LitBool
true
))
e1
e2
@
E
{{
Φ
}}
.
▷
WP
e1
@
E
{{
Φ
}}
⊢
WP
If
(
Lit
(
LitBool
true
))
e1
e2
@
E
{{
Φ
}}
.
Proof
.
rewrite
-
(
wp_lift_pure_det_step
(
If
_
_
_
)
e1
None
)
?
right_id
//; intros; inv_step; eauto.
Qed
.
Lemma
wp_if_false
E
e1
e2
Φ
:
▷
#
>
e2
@
E
{{
Φ
}}
⊢
#
>
If
(
Lit
(
LitBool
false
))
e1
e2
@
E
{{
Φ
}}
.
▷
WP
e2
@
E
{{
Φ
}}
⊢
WP
If
(
Lit
(
LitBool
false
))
e1
e2
@
E
{{
Φ
}}
.
Proof
.
rewrite
-
(
wp_lift_pure_det_step
(
If
_
_
_
)
e2
None
)
?
right_id
//; intros; inv_step; eauto.
...
...
@@ -130,7 +130,7 @@ Qed.
Lemma
wp_fst
E
e1
v1
e2
v2
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
▷
Φ
v1
⊢
#
>
Fst
(
Pair
e1
e2
)
@
E
{{
Φ
}}
.
▷
Φ
v1
⊢
WP
Fst
(
Pair
e1
e2
)
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
Fst
_
)
e1
None
)
?
right_id
-?
wp_value
//; intros; inv_step; eauto.
...
...
@@ -138,7 +138,7 @@ Qed.
Lemma
wp_snd
E
e1
v1
e2
v2
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
▷
Φ
v2
⊢
#
>
Snd
(
Pair
e1
e2
)
@
E
{{
Φ
}}
.
▷
Φ
v2
⊢
WP
Snd
(
Pair
e1
e2
)
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
Snd
_
)
e2
None
)
?
right_id
-?
wp_value
//; intros; inv_step; eauto.
...
...
@@ -146,7 +146,7 @@ Qed.
Lemma
wp_case_inl
E
e0
v0
e1
e2
Φ
:
to_val
e0
=
Some
v0
→
▷
#
>
App
e1
e0
@
E
{{
Φ
}}
⊢
#
>
Case
(
InjL
e0
)
e1
e2
@
E
{{
Φ
}}
.
▷
WP
App
e1
e0
@
E
{{
Φ
}}
⊢
WP
Case
(
InjL
e0
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
(
App
e1
e0
)
None
)
?
right_id
//; intros; inv_step; eauto.
...
...
@@ -154,7 +154,7 @@ Qed.
Lemma
wp_case_inr
E
e0
v0
e1
e2
Φ
:
to_val
e0
=
Some
v0
→
▷
#
>
App
e2
e0
@
E
{{
Φ
}}
⊢
#
>
Case
(
InjR
e0
)
e1
e2
@
E
{{
Φ
}}
.
▷
WP
App
e2
e0
@
E
{{
Φ
}}
⊢
WP
Case
(
InjR
e0
)
e1
e2
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
(
App
e2
e0
)
None
)
?
right_id
//; intros; inv_step; eauto.
...
...
heap_lang/notation.v
View file @
c7390af8
...
...
@@ -2,12 +2,12 @@ From iris.heap_lang Require Export derived.
Export
heap_lang
.
Arguments
wp
{
_
_
}
_
_
%
E
_.
Notation
"
#>
e @ E {{ Φ } }"
:=
(
wp
E
e
%
E
Φ
)
Notation
"
'WP'
e @ E {{ Φ } }"
:=
(
wp
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
#>
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
#>
e {{ Φ } }"
:=
(
wp
⊤
e
%
E
Φ
)
format
"
'WP'
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
'WP'
e {{ Φ } }"
:=
(
wp
⊤
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
#>
e {{ Φ } }"
)
:
uPred_scope
.
format
"
'WP'
e {{ Φ } }"
)
:
uPred_scope
.
Coercion
LitInt
:
Z
>->
base_lit
.
Coercion
LitBool
:
bool
>->
base_lit
.
...
...
heap_lang/par.v
View file @
c7390af8
...
...
@@ -21,9 +21,9 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma
par_spec
(
Ψ
1
Ψ
2
:
val
→
iProp
)
e
(
f1
f2
:
val
)
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
to_val
e
=
Some
(
f1
,
f2
)
%
V
→
(
heap_ctx
heapN
★
#
>
f1
§
()
{{
Ψ
1
}}
★
#
>
f2
§
()
{{
Ψ
2
}}
★
(
heap_ctx
heapN
★
WP
f1
§
()
{{
Ψ
1
}}
★
WP
f2
§
()
{{
Ψ
2
}}
★
∀
v1
v2
,
Ψ
1
v1
★
Ψ
2
v2
-
★
▷
Φ
(
v1
,
v2
)
%
V
)
⊢
#
>
par
e
{{
Φ
}}
.
⊢
WP
par
e
{{
Φ
}}
.
Proof
.
intros
.
rewrite
/
par
.
ewp
(
by
eapply
wp_value
).
wp_let
.
wp_proj
.
ewp
(
eapply
spawn_spec
;
wp_done
).
...
...
@@ -38,9 +38,9 @@ Qed.
Lemma
wp_par
(
Ψ
1
Ψ
2
:
val
→
iProp
)
(
e1
e2
:
expr
[])
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
(
heap_ctx
heapN
★
#
>
e1
{{
Ψ
1
}}
★
#
>
e2
{{
Ψ
2
}}
★
(
heap_ctx
heapN
★
WP
e1
{{
Ψ
1
}}
★
WP
e2
{{
Ψ
2
}}
★
∀
v1
v2
,
Ψ
1
v1
★
Ψ
2
v2
-
★
▷
Φ
(
v1
,
v2
)
%
V
)
⊢
#
>
ParV
e1
e2
{{
Φ
}}
.
⊢
WP
ParV
e1
e2
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
par_spec
//. repeat apply sep_mono; done || by wp_seq.
Qed
.
...
...
heap_lang/spawn.v
View file @
c7390af8
...
...
@@ -50,8 +50,8 @@ Proof. solve_proper. Qed.
Lemma
spawn_spec
(
Ψ
:
val
→
iProp
)
e
(
f
:
val
)
(
Φ
:
val
→
iProp
)
:
to_val
e
=
Some
f
→
heapN
⊥
N
→
(
heap_ctx
heapN
★
#
>
f
§
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(
%
l
))
⊢
#
>
spawn
e
{{
Φ
}}
.
(
heap_ctx
heapN
★
WP
f
§
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(
%
l
))
⊢
WP
spawn
e
{{
Φ
}}
.
Proof
.
intros
Hval
Hdisj
.
rewrite
/
spawn
.
ewp
(
by
eapply
wp_value
).
wp_let
.
wp
eapply
wp_alloc
;
eauto
with
I
.
...
...
@@ -61,9 +61,9 @@ Proof.
rewrite
!
pvs_frame_r
.
eapply
wp_strip_pvs
.
rewrite
!
sep_exist_r
.
apply
exist_elim
=>
γ
.
(
*
TODO
:
Figure
out
a
better
way
to
say
"I want to establish ▷ spawn_inv"
.
*
)
trans
(
heap_ctx
heapN
★
#
>
f
§
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(
%
l
)
%
V
)
★
trans
(
heap_ctx
heapN
★
WP
f
§
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(
%
l
)
%
V
)
★
own
γ
(
Excl
())
★
▷
(
spawn_inv
γ
l
Ψ
))
%
I
.
{
ecancel
[
#
>
_
{{
_
}}
;
_
-
★
_
;
heap_ctx
_
;
own
_
_
]
%
I
.
{
ecancel
[
WP
_
{{
_
}}
;
_
-
★
_
;
heap_ctx
_
;
own
_
_
]
%
I
.
rewrite
-
later_intro
/
spawn_inv
-
(
exist_intro
(
InjLV
§
0
)).
cancel
[
l
↦
InjLV
§
0
]
%
I
.
by
apply
or_intro_l
'
,
const_intro
.
}
rewrite
(
inv_alloc
N
)
// !pvs_frame_l. eapply wp_strip_pvs.
...
...
@@ -88,7 +88,7 @@ Qed.
Lemma
join_spec
(
Ψ
:
val
→
iProp
)
l
(
Φ
:
val
→
iProp
)
:
(
join_handle
l
Ψ
★
∀
v
,
Ψ
v
-
★
Φ
v
)
⊢
#
>
join
(
%
l
)
{{
Φ
}}
.
⊢
WP
join
(
%
l
)
{{
Φ
}}
.
Proof
.
wp_rec
.
wp_focus
(
!
_
)
%
E
.
rewrite
{
1
}/
join_handle
sep_exist_l
!
sep_exist_r
.
apply
exist_elim
=>
γ
.
...
...
heap_lang/tests.v
View file @
c7390af8
...
...
@@ -24,7 +24,7 @@ Section LiftingTests.
Definition
heap_e
:
expr
[]
:=
let:
"x"
:=
ref
§
1
in
'
"x"
<-
!
'
"x"
+
§
1
;;
!
'
"x"
.
Lemma
heap_e_spec
E
N
:
nclose
N
⊆
E
→
heap_ctx
N
⊢
#
>
heap_e
@
E
{{
λ
v
,
v
=
§
2
}}
.
nclose
N
⊆
E
→
heap_ctx
N
⊢
WP
heap_e
@
E
{{
λ
v
,
v
=
§
2
}}
.
Proof
.
rewrite
/
heap_e
=>
HN
.
rewrite
-
(
wp_mask_weaken
N
E
)
//.
wp
eapply
wp_alloc
;
eauto
.
apply
forall_intro
=>
l
;
apply
wand_intro_l
.
...
...
@@ -44,7 +44,7 @@ Section LiftingTests.
Lemma
FindPred_spec
n1
n2
E
Φ
:
n1
<
n2
→
Φ
§
(
n2
-
1
)
⊢
#
>
FindPred
§
n2
§
n1
@
E
{{
Φ
}}
.
Φ
§
(
n2
-
1
)
⊢
WP
FindPred
§
n2
§
n1
@
E
{{
Φ
}}
.
Proof
.
revert
n1
.
wp_rec
=>
n1
Hn
.
wp_let
.
wp_op
.
wp_let
.
wp_op
=>
?
;
wp_if
.
...
...
@@ -53,7 +53,7 @@ Section LiftingTests.
-
assert
(
n1
=
n2
-
1
)
as
->
by
omega
;
auto
with
I
.
Qed
.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
§
(
n
-
1
)
⊢
#
>
Pred
§
n
@
E
{{
Φ
}}
.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
§
(
n
-
1
)
⊢
WP
Pred
§
n
@
E
{{
Φ
}}
.
Proof
.
wp_lam
.
wp_op
=>
?
;
wp_if
.
-
wp_op
.
wp_op
.
...
...
@@ -63,7 +63,7 @@ Section LiftingTests.
Qed
.
Lemma
Pred_user
E
:
(
True
:
iProp
)
⊢
#
>
let
:
"x"
:=
Pred
§
42
in
^
Pred
'
"x"
@
E
{{
λ
v
,
v
=
§
40
}}
.
(
True
:
iProp
)
⊢
WP
let
:
"x"
:=
Pred
§
42
in
^
Pred
'
"x"
@
E
{{
λ
v
,
v
=
§
40
}}
.
Proof
.
intros
.
ewp
apply
Pred_spec
.
wp_let
.
ewp
apply
Pred_spec
.
auto
with
I
.
Qed
.
...
...
program_logic/adequacy.v
View file @
c7390af8
...
...
@@ -55,7 +55,7 @@ Proof.
by
rewrite
-
Permutation_middle
/=
big_op_app
.
Qed
.
Lemma
wp_adequacy_steps
P
Φ
k
n
e1
t2
σ
1
σ
2
r1
:
P
⊢
#
>
e1
{{
Φ
}}
→
P
⊢
WP
e1
{{
Φ
}}
→
nsteps
step
k
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
1
<
n
→
wsat
(
k
+
n
)
⊤
σ
1
r1
→
P
(
k
+
n
)
r1
→
...
...
@@ -69,7 +69,7 @@ Qed.
Lemma
wp_adequacy_own
Φ
e1
t2
σ
1
m
σ
2
:
✓
m
→
(
ownP
σ
1
★
ownG
m
)
⊢
#
>
e1
{{
Φ
}}
→
(
ownP
σ
1
★
ownG
m
)
⊢
WP
e1
{{
Φ
}}
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
∃
rs2
Φ
s
'
,
wptp
2
t2
(
Φ
::
Φ
s
'
)
rs2
∧
wsat
2
⊤
σ
2
(
big_op
rs2
).
Proof
.
...
...
@@ -84,7 +84,7 @@ Qed.
Theorem
wp_adequacy_result
E
φ
e
v
t2
σ
1
m
σ
2
:
✓
m
→
(
ownP
σ
1
★
ownG
m
)
⊢
#
>
e
@
E
{{
λ
v
'
,
■
φ
v
'
}}
→
(
ownP
σ
1
★
ownG
m
)
⊢
WP
e
@
E
{{
λ
v
'
,
■
φ
v
'
}}
→
rtc
step
([
e
],
σ
1
)
(
of_val
v
::
t2
,
σ
2
)
→
φ
v
.
Proof
.
...
...
@@ -110,7 +110,7 @@ Qed.
Lemma
wp_adequacy_reducible
E
Φ
e1
e2
t2
σ
1
m
σ
2
:
✓
m
→
(
ownP
σ
1
★
ownG
m
)
⊢
#
>
e1
@
E
{{
Φ
}}
→
(
ownP
σ
1
★
ownG
m
)
⊢
WP
e1
@
E
{{
Φ
}}
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
e2
∈
t2
→
(
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
).
Proof
.
...
...
@@ -128,7 +128,7 @@ Qed.
(
*
Connect
this
up
to
the
threadpool
-
semantics
.
*
)
Theorem
wp_adequacy_safe
E
Φ
e1
t2
σ
1
m
σ
2
:
✓
m
→
(
ownP
σ
1
★
ownG
m
)
⊢
#
>
e1
@
E
{{
Φ
}}
→
(
ownP
σ
1
★
ownG
m
)
⊢
WP
e1
@
E
{{
Φ
}}
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
Forall
(
λ
e
,
is_Some
(
to_val
e
))
t2
∨
∃
t3
σ
3
,
step
(
t2
,
σ
2
)
(
t3
,
σ
3
).
Proof
.
...
...
program_logic/hoare.v
View file @
c7390af8
...
...
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre viewshifts.
Definition
ht
{
Λ
Σ
}
(
E
:
coPset
)
(
P
:
iProp
Λ
Σ
)
(
e
:
expr
Λ
)
(
Φ
:
val
Λ
→
iProp
Λ
Σ
)
:
iProp
Λ
Σ
:=
(
□
(
P
→
#
>
e
@
E
{{
Φ
}}
))
%
I
.
(
□
(
P
→
WP
e
@
E
{{
Φ
}}
))
%
I
.
Instance:
Params
(
@
ht
)
3.
Notation
"{{ P } } e @ E {{ Φ } }"
:=
(
ht
E
P
e
Φ
)
...
...
@@ -38,7 +38,7 @@ Global Instance ht_mono' E :
Proper
(
flip
(
⊢
)
==>
eq
==>
pointwise_relation
_
(
⊢
)
==>
(
⊢
))
(
@
ht
Λ
Σ
E
).
Proof
.
solve_proper
.
Qed
.
Lemma
ht_alt
E
P
Φ
e
:
(
P
⊢
#
>
e
@
E
{{
Φ
}}
)
→
{{
P
}}
e
@
E
{{
Φ
}}
.
Lemma
ht_alt
E
P
Φ
e
:
(
P
⊢
WP
e
@
E
{{
Φ
}}
)
→
{{
P
}}
e
@
E
{{
Φ
}}
.
Proof
.
intros
;
rewrite
-{
1
}
always_const
.
apply
:
always_intro
.
apply
impl_intro_l
.
by
rewrite
always_const
right_id
.
...
...
program_logic/invariants.v
View file @
c7390af8
...
...
@@ -64,8 +64,8 @@ Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
Lemma
wp_open_close
E
e
N
P
Φ
R
:
atomic
e
→
nclose
N
⊆
E
→
R
⊢
inv
N
P
→
R
⊢
(
▷
P
-
★
#
>
e
@
E
∖
nclose
N
{{
λ
v
,
▷
P
★
Φ
v
}}
)
→
R
⊢
#
>
e
@
E
{{
Φ
}}
.
R
⊢
(
▷
P
-
★
WP
e
@
E
∖
nclose
N
{{
λ
v
,
▷
P
★
Φ
v
}}
)
→
R
⊢
WP
e
@
E
{{
Φ
}}
.
Proof
.
intros
.
by
apply
:
(
inv_fsa
(
wp_fsa
e
)).
Qed
.
Lemma
inv_alloc
N
E
P
:
nclose
N
⊆
E
→
▷
P
⊢
|={
E
}=>
inv
N
P
.
...
...
program_logic/lifting.v
View file @
c7390af8
...
...
@@ -23,8 +23,8 @@ Lemma wp_lift_step E1 E2
reducible
e1
σ
1
→
(
∀
e2
σ
2
ef
,
prim_step
e1
σ
1
e2
σ
2
ef
→
φ
e2
σ
2
ef
)
→
(
|={
E1
,
E2
}=>
▷
ownP
σ
1
★
▷
∀
e2
σ
2
ef
,
(
■
φ
e2
σ
2
ef
∧
ownP
σ
2
)
-
★
|={
E2
,
E1
}=>
#
>
e2
@
E1
{{
Φ
}}
★
wp_fork
ef
)
⊢
#
>
e1
@
E1
{{
Φ
}}
.
(
■
φ
e2
σ
2
ef
∧
ownP
σ
2
)
-
★
|={
E2
,
E1
}=>
WP
e2
@
E1
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E1
{{
Φ
}}
.
Proof
.
intros
?
He
Hsafe
Hstep
.
rewrite
pvs_eq
wp_eq
.
uPred
.
unseal
;
split
=>
n
r
?
Hvs
;
constructor
;
auto
.
...
...
@@ -45,7 +45,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
to_val
e1
=
None
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1
e2
σ
2
ef
,
prim_step
e1
σ
1
e2
σ
2
ef
→
σ
1
=
σ
2
∧
φ
e2
ef
)
→
(
▷
∀
e2
ef
,
■
φ
e2
ef
→
#
>
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
#
>
e1
@
E
{{
Φ
}}
.
(
▷
∀
e2
ef
,
■
φ
e2
ef
→
WP
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E
{{
Φ
}}
.
Proof
.
intros
He
Hsafe
Hstep
;
rewrite
wp_eq
;
uPred
.
unseal
.
split
=>
n
r
?
Hwp
;
constructor
;
auto
.
...
...
@@ -67,7 +67,7 @@ Lemma wp_lift_atomic_step {E Φ} e1
(
∀
e2
σ
2
ef
,
prim_step
e1
σ
1
e2
σ
2
ef
→
∃
v2
,
to_val
e2
=
Some
v2
∧
φ
v2
σ
2
ef
)
→
(
▷
ownP
σ
1
★
▷
∀
v2
σ
2
ef
,
■
φ
v2
σ
2
ef
∧
ownP
σ
2
-
★
Φ
v2
★
wp_fork
ef
)
⊢
#
>
e1
@
E
{{
Φ
}}
.
⊢
WP
e1
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_step
E
E
(
λ
e2
σ
2
ef
,
∃
v2
,
to_val
e2
=
Some
v2
∧
φ
v2
σ
2
ef
)
_
e1
σ
1
)
//; [].
...
...
@@ -86,7 +86,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
reducible
e1
σ
1
→
(
∀
e2
'
σ
2
'
ef
'
,
prim_step
e1
σ
1
e2
'
σ
2
'
ef
'
→
σ
2
=
σ
2
'
∧
to_val
e2
'
=
Some
v2
∧
ef
=
ef
'
)
→
(
▷
ownP
σ
1
★
▷
(
ownP
σ
2
-
★
Φ
v2
★
wp_fork
ef
))
⊢
#
>
e1
@
E
{{
Φ
}}
.
(
▷
ownP
σ
1
★
▷
(
ownP
σ
2
-
★
Φ
v2
★
wp_fork
ef
))
⊢
WP
e1
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_step
_
(
λ
v2
'
σ
2
'
ef
'
,
σ
2
=
σ
2
'
∧
v2
=
v2
'
∧
ef
=
ef
'
)
σ
1
)
//; last naive_solver.
...
...
@@ -101,7 +101,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
to_val
e1
=
None
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1
e2
'
σ
2
ef
'
,
prim_step
e1
σ
1
e2
'
σ
2
ef
'
→
σ
1
=
σ
2
∧
e2
=
e2
'
∧
ef
=
ef
'
)
→
▷
(
#
>
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
#
>
e1
@
E
{{
Φ
}}
.
▷
(
WP
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E
{{
Φ
}}
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_step
E
(
λ
e2
'
ef
'
,
e2
=
e2
'
∧
ef
=
ef
'
)
_
e1
)
//=.
...
...
program_logic/weakestpre.v
View file @
c7390af8
...
...
@@ -57,13 +57,12 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
Arguments
wp
{
_
_
}
_
_
_.
Instance:
Params
(
@
wp
)
4.
(
*
TODO
:
On
paper
,
'
wp
'
is
turned
into
a
keyword
.
*
)
Notation
"#> e @ E {{ Φ } }"
:=
(
wp
E
e
Φ
)
Notation
"'WP' e @ E {{ Φ } }"
:=
(
wp
E
e
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
#>
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
#>
e {{ Φ } }"
:=
(
wp
⊤
e
Φ
)
format
"
'WP'
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
'WP'
e {{ Φ } }"
:=
(
wp
⊤
e
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
#>
e {{ Φ } }"
)
:
uPred_scope
.
format
"
'WP'
e {{ Φ } }"
)
:
uPred_scope
.
Section
wp
.
Context
{
Λ
:
language
}
{
Σ
:
iFunctor
}
.
...
...
@@ -94,7 +93,7 @@ Proof.
by
intros
Φ
Φ'
?
;
apply
equiv_dist
=>
n
;
apply
wp_ne
=>
v
;
apply
equiv_dist
.
Qed
.
Lemma
wp_mask_frame_mono
E1
E2
e
Φ
Ψ
:
E1
⊆
E2
→
(
∀
v
,
Φ
v
⊢
Ψ
v
)
→
#
>
e
@
E1
{{
Φ
}}
⊢
#
>
e
@
E2
{{
Ψ
}}
.
E1
⊆
E2
→
(
∀
v
,
Φ
v
⊢
Ψ
v
)
→
WP
e
@
E1
{{
Φ
}}
⊢
WP
e
@
E2
{{
Ψ
}}
.
Proof
.
rewrite
wp_eq
.
intros
HE
H
Φ
;
split
=>
n
r
.
revert
e
r
;
induction
n
as
[
n
IH
]
using
lt_wf_ind
=>
e
r
.
...
...
@@ -122,9 +121,9 @@ Proof.
intros
He
;
destruct
3
;
[
by
rewrite
?
to_of_val
in
He
|