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
Fairis
Commits
98318d33
Commit
98318d33
authored
Feb 02, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
extend derived lifting lemmas to deal with fork (puts them on-par with the hoare lifting lemmas)
parent
03ee69f3
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
53 additions
and
42 deletions
+53
-42
barrier/lifting.v
barrier/lifting.v
+21
-21
iris/hoare_lifting.v
iris/hoare_lifting.v
+4
-0
iris/lifting.v
iris/lifting.v
+28
-21
No files found.
barrier/lifting.v
View file @
98318d33
...
...
@@ -23,21 +23,22 @@ Lemma wp_alloc_pst E σ e v Q :
Proof
.
(
*
TODO
RJ
:
Without
the
set
,
ssreflect
rewrite
doesn
'
t
work
.
Figure
out
why
or
reprot
a
bug
.
*
)
intros
.
set
(
φ
v
'
σ'
:=
∃
l
,
v
'
=
LocV
l
∧
σ'
=
<
[
l
:=
v
]
>
σ
∧
σ
!!
l
=
None
).
intros
.
set
(
φ
v
'
σ'
ef
:=
∃
l
,
ef
=
@
None
expr
∧
v
'
=
LocV
l
∧
σ'
=
<
[
l
:=
v
]
>
σ
∧
σ
!!
l
=
None
).
rewrite
-
(
wp_lift_atomic_step
(
Alloc
e
)
φ
σ
)
// /φ;
last
by
intros
;
inv_step
;
eauto
8.
apply
sep_mono
,
later_mono
;
first
done
.
apply
forall_intro
=>
e2
;
apply
forall_intro
=>
σ
2
;
apply
wand_intro_l
.
apply
forall_intro
=>
e2
;
apply
forall_intro
=>
σ
2
;
apply
forall_intro
=>
ef
.
apply
wand_intro_l
.
rewrite
always_and_sep_l
'
-
associative
-
always_and_sep_l
'
.
apply
const_elim_l
=>-
[
l
[
->
[
->
?
]]].
by
rewrite
(
forall_elim
l
)
const_equiv
// left_id wand_elim_r.
apply
const_elim_l
=>-
[
l
[
->
[
->
[
->
?
]
]]].
by
rewrite
(
forall_elim
l
)
right_id
const_equiv
// left_id wand_elim_r.
Qed
.
Lemma
wp_load_pst
E
σ
l
v
Q
:
σ
!!
l
=
Some
v
→
(
ownP
σ
★
▷
(
ownP
σ
-
★
Q
v
))
⊑
wp
E
(
Load
(
Loc
l
))
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_atomic_det_step
σ
v
σ
)
//;
intros
;
rewrite
-
(
wp_lift_atomic_det_step
σ
v
σ
None
)
?
right_id
//;
last
(
by
intros
;
inv_step
;
eauto
).
Qed
.
...
...
@@ -46,7 +47,7 @@ Lemma wp_store_pst E σ l e v v' Q :
(
ownP
σ
★
▷
(
ownP
(
<
[
l
:=
v
]
>
σ
)
-
★
Q
LitUnitV
))
⊑
wp
E
(
Store
(
Loc
l
)
e
)
Q
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
LitUnitV
(
<
[
l
:=
v
]
>
σ
)
)
//;
rewrite
-
(
wp_lift_atomic_det_step
σ
LitUnitV
(
<
[
l
:=
v
]
>
σ
)
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
...
...
@@ -54,7 +55,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v
'
→
v
'
≠
v1
→
(
ownP
σ
★
▷
(
ownP
σ
-
★
Q
LitFalseV
))
⊑
wp
E
(
Cas
(
Loc
l
)
e1
e2
)
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_atomic_det_step
σ
LitFalseV
σ
)
//;
intros
;
rewrite
-
(
wp_lift_atomic_det_step
σ
LitFalseV
σ
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
...
...
@@ -63,7 +64,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
(
ownP
σ
★
▷
(
ownP
(
<
[
l
:=
v2
]
>
σ
)
-
★
Q
LitTrueV
))
⊑
wp
E
(
Cas
(
Loc
l
)
e1
e2
)
Q
.
Proof
.
intros
.
rewrite
-
(
wp_lift_atomic_det_step
σ
LitTrueV
(
<
[
l
:=
v2
]
>
σ
)
)
//;
rewrite
-
(
wp_lift_atomic_det_step
σ
LitTrueV
(
<
[
l
:=
v2
]
>
σ
)
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
...
...
@@ -71,26 +72,25 @@ Qed.
Lemma
wp_fork
E
e
:
▷
wp
(
Σ
:=
Σ
)
coPset_all
e
(
λ
_
,
True
)
⊑
wp
E
(
Fork
e
)
(
λ
v
,
■
(
v
=
LitUnitV
)).
Proof
.
rewrite
-
(
wp_lift_pure_step
E
(
λ
e
'
ef
,
e
'
=
LitUnit
∧
ef
=
Some
e
))
//=;
rewrite
-
(
wp_lift_pure_
det_
step
(
Fork
e
)
LitUnit
(
Some
e
))
//=;
last
by
intros
;
inv_step
;
eauto
.
apply
later_mono
,
forall_intro
=>
e2
;
apply
forall_intro
=>
ef
.
apply
impl_intro_l
,
const_elim_l
=>-
[
->
->
]
/=
.
apply
sep_intro_True_l
;
last
done
.
by
rewrite
-
wp_value
'
//; apply const_intro.
apply
later_mono
,
sep_intro_True_l
;
last
done
.
by
rewrite
-
(
wp_value
'
_
_
LitUnit
)
//; apply const_intro.
Qed
.
Lemma
wp_rec
E
ef
e
v
Q
:
to_val
e
=
Some
v
→
▷
wp
E
ef
.[
Rec
ef
,
e
/
]
Q
⊑
wp
E
(
App
(
Rec
ef
)
e
)
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
App
_
_
)
ef
.[
Rec
ef
,
e
/
])
//=;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
App
_
_
)
ef
.[
Rec
ef
,
e
/
]
None
)
?
right_id
//=;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
Lemma
wp_plus
E
n1
n2
Q
:
▷
Q
(
LitNatV
(
n1
+
n2
))
⊑
wp
E
(
Plus
(
LitNat
n1
)
(
LitNat
n2
))
Q
.
Proof
.
rewrite
-
(
wp_lift_pure_det_step
(
Plus
_
_
)
(
LitNat
(
n1
+
n2
))
)
//
=
;
rewrite
-
(
wp_lift_pure_det_step
(
Plus
_
_
)
(
LitNat
(
n1
+
n2
))
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
by
rewrite
-
wp_value
'
.
Qed
.
...
...
@@ -99,7 +99,7 @@ Lemma wp_le_true E n1 n2 Q :
n1
≤
n2
→
▷
Q
LitTrueV
⊑
wp
E
(
Le
(
LitNat
n1
)
(
LitNat
n2
))
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Le
_
_
)
LitTrue
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Le
_
_
)
LitTrue
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
with
lia
.
by
rewrite
-
wp_value
'
.
Qed
.
...
...
@@ -108,7 +108,7 @@ Lemma wp_le_false E n1 n2 Q :
n1
>
n2
→
▷
Q
LitFalseV
⊑
wp
E
(
Le
(
LitNat
n1
)
(
LitNat
n2
))
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Le
_
_
)
LitFalse
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Le
_
_
)
LitFalse
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
with
lia
.
by
rewrite
-
wp_value
'
.
Qed
.
...
...
@@ -117,7 +117,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
▷
Q
v1
⊑
wp
E
(
Fst
(
Pair
e1
e2
))
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Fst
_
)
e1
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Fst
_
)
e1
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
by
rewrite
-
wp_value
'
.
Qed
.
...
...
@@ -126,7 +126,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
▷
Q
v2
⊑
wp
E
(
Snd
(
Pair
e1
e2
))
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Snd
_
)
e2
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Snd
_
)
e2
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
by
rewrite
-
wp_value
'
.
Qed
.
...
...
@@ -135,7 +135,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val
e0
=
Some
v0
→
▷
wp
E
e1
.[
e0
/
]
Q
⊑
wp
E
(
Case
(
InjL
e0
)
e1
e2
)
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
e1
.[
e0
/
]
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
e1
.[
e0
/
]
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
...
...
@@ -143,7 +143,7 @@ Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val
e0
=
Some
v0
→
▷
wp
E
e2
.[
e0
/
]
Q
⊑
wp
E
(
Case
(
InjR
e0
)
e1
e2
)
Q
.
Proof
.
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
e2
.[
e0
/
]
)
//
=
;
intros
;
rewrite
-
(
wp_lift_pure_det_step
(
Case
_
_
_
)
e2
.[
e0
/
]
None
)
?
right_id
//;
last
by
intros
;
inv_step
;
eauto
.
Qed
.
...
...
iris/hoare_lifting.v
View file @
98318d33
...
...
@@ -44,6 +44,7 @@ Proof.
rewrite
{
1
}/
ht
-
always_wand_impl
always_elim
wand_elim_r
;
apply
wp_mono
=>
v
.
by
apply
const_intro
.
Qed
.
Lemma
ht_lift_atomic_step
E
(
φ
:
expr
Λ
→
state
Λ
→
option
(
expr
Λ
)
→
Prop
)
P
e1
σ
1
:
atomic
e1
→
...
...
@@ -70,6 +71,7 @@ Proof.
rewrite
-
(
exist_intro
σ
2
)
-
(
exist_intro
ef
)
(
of_to_val
e2
)
//.
by
rewrite
-
always_and_sep_r
'
;
apply
and_intro
;
try
apply
const_intro
.
Qed
.
Lemma
ht_lift_pure_step
E
(
φ
:
expr
Λ
→
option
(
expr
Λ
)
→
Prop
)
P
P
'
Q
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
...
...
@@ -95,6 +97,7 @@ Proof.
rewrite
{
1
}/
ht
-
always_wand_impl
always_elim
wand_elim_r
;
apply
wp_mono
=>
v
.
by
apply
const_intro
.
Qed
.
Lemma
ht_lift_pure_det_step
E
(
φ
:
expr
Λ
→
option
(
expr
Λ
)
→
Prop
)
P
P
'
Q
e1
e2
ef
:
to_val
e1
=
None
→
...
...
@@ -114,4 +117,5 @@ Proof.
rewrite
-
always_and_sep_l
'
-
associative
;
apply
const_elim_l
=>-
[
??
];
subst
.
by
rewrite
/=
/
ht
always_elim
impl_elim_r
.
Qed
.
End
lifting
.
iris/lifting.v
View file @
98318d33
...
...
@@ -56,53 +56,60 @@ Qed.
Opaque
uPred_holds
.
Import
uPred
.
Lemma
wp_lift_atomic_step
{
E
Q
}
e1
(
φ
:
val
Λ
→
state
Λ
→
Prop
)
σ
1
:
Lemma
wp_lift_atomic_step
{
E
Q
}
e1
(
φ
:
val
Λ
→
state
Λ
→
option
(
expr
Λ
)
→
Prop
)
σ
1
:
to_val
e1
=
None
→
reducible
e1
σ
1
→
(
∀
e
'
σ'
ef
,
prim_step
e1
σ
1
e
'
σ'
ef
→
∃
v
'
,
ef
=
None
∧
to_val
e
'
=
Some
v
'
∧
φ
v
'
σ'
)
→
(
ownP
σ
1
★
▷
∀
v2
σ
2
,
(
■
φ
v2
σ
2
∧
ownP
σ
2
-
★
Q
v2
))
⊑
wp
E
e1
Q
.
(
∀
e
'
σ'
ef
,
prim_step
e1
σ
1
e
'
σ'
ef
→
∃
v
'
,
to_val
e
'
=
Some
v
'
∧
φ
v
'
σ'
ef
)
→
(
ownP
σ
1
★
▷
∀
v2
σ
2
ef
,
■
φ
v2
σ
2
ef
∧
ownP
σ
2
-
★
Q
v2
★
default
True
ef
(
flip
(
wp
coPset_all
)
(
λ
_
,
True
)))
⊑
wp
E
e1
Q
.
Proof
.
intros
He
Hsafe
Hstep
.
rewrite
-
(
wp_lift_step
E
E
(
λ
e
'
σ'
ef
,
∃
v
'
,
ef
=
None
∧
to_val
e
'
=
Some
v
'
∧
φ
v
'
σ'
)
_
e1
σ
1
)
//; [].
(
λ
e
'
σ'
ef
,
∃
v
'
,
to_val
e
'
=
Some
v
'
∧
φ
v
'
σ'
ef
)
_
e1
σ
1
)
//; [].
rewrite
-
pvs_intro
.
apply
sep_mono
,
later_mono
;
first
done
.
apply
forall_intro
=>
e2
'
;
apply
forall_intro
=>
σ
2
'
.
apply
forall_intro
=>
ef
;
apply
wand_intro_l
.
rewrite
always_and_sep_l
'
-
associative
-
always_and_sep_l
'
.
apply
const_elim_l
=>-
[
v2
'
[
->
[
Hv
?
]]]
/=
.
rewrite
-
pvs_intro
right_id
-
wp_value
'
;
last
by
eassumption
.
rewrite
(
forall_elim
v2
'
)
(
forall_elim
σ
2
'
)
const_equiv
//.
by
rewrite
left_id
wand_elim_r
.
apply
const_elim_l
=>-
[
v2
'
[
Hv
?
]]
/=
.
rewrite
-
pvs_intro
.
rewrite
(
forall_elim
v2
'
)
(
forall_elim
σ
2
'
)
(
forall_elim
ef
)
const_equiv
//.
rewrite
left_id
wand_elim_r
.
apply
sep_mono
;
last
done
.
(
*
FIXME
RJ
why
can
'
t
I
do
this
rewrite
before
doing
sep_mono
?
*
)
by
rewrite
-
(
wp_value
'
_
_
e2
'
).
Qed
.
Lemma
wp_lift_atomic_det_step
{
E
Q
e1
}
σ
1
v2
σ
2
:
Lemma
wp_lift_atomic_det_step
{
E
Q
e1
}
σ
1
v2
σ
2
ef
:
to_val
e1
=
None
→
reducible
e1
σ
1
→
(
∀
e
'
σ'
ef
,
prim_step
e1
σ
1
e
'
σ'
ef
→
ef
=
None
∧
e
'
=
of_val
v2
∧
σ'
=
σ
2
)
→
(
ownP
σ
1
★
▷
(
ownP
σ
2
-
★
Q
v2
))
⊑
wp
E
e1
Q
.
(
∀
e
'
σ'
ef
'
,
prim_step
e1
σ
1
e
'
σ'
ef
'
→
ef
'
=
ef
∧
e
'
=
of_val
v2
∧
σ'
=
σ
2
)
→
(
ownP
σ
1
★
▷
(
ownP
σ
2
-
★
Q
v2
★
default
True
ef
(
flip
(
wp
coPset_all
)
(
λ
_
,
True
))))
⊑
wp
E
e1
Q
.
Proof
.
intros
He
Hsafe
Hstep
.
rewrite
-
(
wp_lift_atomic_step
_
(
λ
v
'
σ'
,
v
'
=
v2
∧
σ'
=
σ
2
)
σ
1
)
//; last first.
rewrite
-
(
wp_lift_atomic_step
_
(
λ
v
'
σ'
ef
'
,
v
'
=
v2
∧
σ'
=
σ
2
∧
ef
'
=
ef
)
σ
1
)
//;
last
first
.
{
intros
.
exists
v2
.
apply
Hstep
in
H
.
destruct_conjs
;
subst
.
eauto
using
to_of_val
.
}
apply
sep_mono
,
later_mono
;
first
done
.
apply
forall_intro
=>
e2
'
;
apply
forall_intro
=>
σ
2
'
.
apply
forall_intro
=>
e2
'
;
apply
forall_intro
=>
σ
2
'
;
apply
forall_intro
=>
ef
'
.
apply
wand_intro_l
.
rewrite
always_and_sep_l
'
-
associative
-
always_and_sep_l
'
.
apply
const_elim_l
=>-
[
->
->
]
/=
.
apply
const_elim_l
=>-
[
->
[
->
->
]
]
/=
.
by
rewrite
wand_elim_r
.
Qed
.
Lemma
wp_lift_pure_det_step
{
E
Q
}
e1
e2
:
Lemma
wp_lift_pure_det_step
{
E
Q
}
e1
e2
ef
:
to_val
e1
=
None
→
(
∀
σ
1
,
reducible
e1
σ
1
)
→
(
∀
σ
1
e
'
σ'
ef
,
prim_step
e1
σ
1
e
'
σ'
ef
→
σ
1
=
σ'
∧
ef
=
Non
e
∧
e
'
=
e2
)
→
(
▷
wp
E
e2
Q
)
⊑
wp
E
e1
Q
.
(
∀
σ
1
e
'
σ'
ef
'
,
prim_step
e1
σ
1
e
'
σ'
ef
'
→
σ
1
=
σ'
∧
ef
'
=
e
f
∧
e
'
=
e2
)
→
▷
(
wp
E
e2
Q
★
default
True
ef
(
flip
(
wp
coPset_all
)
(
λ
_
,
True
))
)
⊑
wp
E
e1
Q
.
Proof
.
intros
.
rewrite
-
(
wp_lift_pure_step
E
(
λ
e
'
ef
,
ef
=
None
∧
e
'
=
e2
)
_
e1
)
//=.
apply
later_mono
,
forall_intro
=>
e
'
;
apply
forall_intro
=>
ef
.
apply
impl_intro_l
,
const_elim_l
=>-
[
->
->
]
/=
.
by
rewrite
right_id
.
intros
.
rewrite
-
(
wp_lift_pure_step
E
(
λ
e
'
ef
'
,
ef
'
=
ef
∧
e
'
=
e2
)
_
e1
)
//=.
apply
later_mono
,
forall_intro
=>
e
'
;
apply
forall_intro
=>
ef
'
.
apply
impl_intro_l
,
const_elim_l
=>-
[
->
->
]
/=
;
done
.
Qed
.
End
lifting
.
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