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
Rice Wine
Iris
Commits
0841a63d
Commit
0841a63d
authored
Dec 07, 2017
by
Ralf Jung
Browse files
CamlCase of inductive constructors
parent
52f90871
Changes
11
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
0841a63d
...
...
@@ -20,7 +20,7 @@ Changes in and extensions of the theory:
}}`
ensures that, as usual, all invariants are preserved while
`e`
runs, but
it permits execution to get stuck. The former implies the latter. The full
judgment is
`WP e @ s; E {{ Φ }}`
, where non-stuck WP uses
*stuckness bit*
`s
=
n
ot
_s
tuck`
while stuck WP uses
`s =
m
aybe
_s
tuck`
.
=
N
ot
S
tuck`
while stuck WP uses
`s =
M
aybe
S
tuck`
.
Changes in Coq:
...
...
@@ -105,10 +105,10 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
*
Move the
`prelude`
folder to its own project: std++
*
The rules
`internal_eq_rewrite`
and
`internal_eq_rewrite_contractive`
are now
stated in the logic, i.e. they are
`iApply`
friendly.
*
Restore the original, stronger notion of atomicity alongside the
weaker
notion. These are
`Atomic
s
e`
where the stuckness bit
`s`
indicates whether
expression
`e`
is weakly (
`
s
=
not_stuck`
) or
s
trongly
(
`s = maybe_stuck
`
) atomic.
*
Restore the original, stronger notion of atomicity alongside the
weaker
notion. These are
`Atomic
a
e`
where the stuckness bit
`s`
indicates whether
expression
`e`
is weakly (
`
a
=
WeaklyAtomic`
) or strongly (
`a =
S
trongly
Atomic
`
) atomic.
## Iris 3.0.0 (released 2017-01-11)
...
...
theories/heap_lang/tactics.v
View file @
0841a63d
...
...
@@ -189,7 +189,7 @@ Definition is_atomic (e : expr) :=
end
.
Lemma
is_atomic_correct
s
e
:
is_atomic
e
→
Atomic
s
(
to_expr
e
).
Proof
.
enough
(
is_atomic
e
→
Atomic
s
trongly
_a
tomic
(
to_expr
e
)).
enough
(
is_atomic
e
→
Atomic
S
trongly
A
tomic
(
to_expr
e
)).
{
destruct
s
;
auto
using
strongly_atomic_atomic
.
}
intros
He
.
apply
ectx_language_atomic
.
-
intros
σ
e'
σ
'
ef
Hstep
;
simpl
in
*.
revert
Hstep
.
...
...
theories/program_logic/adequacy.v
View file @
0841a63d
...
...
@@ -38,20 +38,20 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val
adequate_result
t2
σ
2
v2
:
rtc
step
([
e1
],
σ
1
)
(
of_val
v2
::
t2
,
σ
2
)
→
φ
v2
;
adequate_safe
t2
σ
2 e2
:
s
=
n
ot
_s
tuck
→
s
=
N
ot
S
tuck
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
e2
∈
t2
→
(
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
)
}.
Theorem
adequate_tp_safe
{
Λ
}
(
e1
:
expr
Λ
)
t2
σ
1
σ
2
φ
:
adequate
n
ot
_s
tuck
e1
σ
1
φ
→
adequate
N
ot
S
tuck
e1
σ
1
φ
→
rtc
step
([
e1
],
σ
1
)
(
t2
,
σ
2
)
→
Forall
(
λ
e
,
is_Some
(
to_val
e
))
t2
∨
∃
t3
σ
3
,
step
(
t2
,
σ
2
)
(
t3
,
σ
3
).
Proof
.
intros
Had
?.
destruct
(
decide
(
Forall
(
λ
e
,
is_Some
(
to_val
e
))
t2
))
as
[|
Ht2
]
;
[
by
left
|].
apply
(
not_Forall_Exists
_
),
Exists_exists
in
Ht2
;
destruct
Ht2
as
(
e2
&?&
He2
).
destruct
(
adequate_safe
n
ot
_s
tuck
e1
σ
1
φ
Had
t2
σ
2 e2
)
as
[?|(
e3
&
σ
3
&
efs
&?)]
;
destruct
(
adequate_safe
N
ot
S
tuck
e1
σ
1
φ
Had
t2
σ
2 e2
)
as
[?|(
e3
&
σ
3
&
efs
&?)]
;
rewrite
?eq_None_not_Some
;
auto
.
{
exfalso
.
eauto
.
}
destruct
(
elem_of_list_split
t2
e2
)
as
(
t2'
&
t2''
&->)
;
auto
.
...
...
@@ -144,7 +144,7 @@ Qed.
Lemma
wptp_safe
n
e1
e2
t1
t2
σ
1
σ
2
Φ
:
nsteps
step
n
(
e1
::
t1
,
σ
1
)
(
t2
,
σ
2
)
→
e2
∈
t2
→
world
σ
1
∗
WP
e1
{{
Φ
}}
∗
wptp
n
ot
_s
tuck
t1
world
σ
1
∗
WP
e1
{{
Φ
}}
∗
wptp
N
ot
S
tuck
t1
⊢
▷
^(
S
(
S
n
))
⌜
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
⌝
.
Proof
.
intros
?
He2
.
rewrite
wptp_steps
//
laterN_later
.
apply
:
bupd_iter_laterN_mono
.
...
...
theories/program_logic/ectx_language.v
View file @
0841a63d
...
...
@@ -132,7 +132,7 @@ Section ectx_language.
Definition
head_atomic
(
a
:
atomicity
)
(
e
:
expr
Λ
)
:
Prop
:
=
∀
σ
e'
σ
'
efs
,
head_step
e
σ
e'
σ
'
efs
→
if
a
is
w
eakly
_a
tomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
if
a
is
W
eakly
A
tomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
(* Some lemmas about this language *)
Lemma
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
.
...
...
theories/program_logic/hoare.v
View file @
0841a63d
...
...
@@ -11,32 +11,32 @@ Instance: Params (@ht) 5.
Notation
"{{ P } } e @ s ; E {{ Φ } }"
:
=
(
ht
s
E
P
%
I
e
%
E
Φ
%
I
)
(
at
level
20
,
P
,
e
,
Φ
at
level
200
,
format
"{{ P } } e @ s ; E {{ Φ } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e @ E {{ Φ } }"
:
=
(
ht
n
ot
_s
tuck
E
P
%
I
e
%
E
Φ
%
I
)
Notation
"{{ P } } e @ E {{ Φ } }"
:
=
(
ht
N
ot
S
tuck
E
P
%
I
e
%
E
Φ
%
I
)
(
at
level
20
,
P
,
e
,
Φ
at
level
200
,
format
"{{ P } } e @ E {{ Φ } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e @ E ? {{ Φ } }"
:
=
(
ht
m
aybe
_s
tuck
E
P
%
I
e
%
E
Φ
%
I
)
Notation
"{{ P } } e @ E ? {{ Φ } }"
:
=
(
ht
M
aybe
S
tuck
E
P
%
I
e
%
E
Φ
%
I
)
(
at
level
20
,
P
,
e
,
Φ
at
level
200
,
format
"{{ P } } e @ E ? {{ Φ } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e {{ Φ } }"
:
=
(
ht
n
ot
_s
tuck
⊤
P
%
I
e
%
E
Φ
%
I
)
Notation
"{{ P } } e {{ Φ } }"
:
=
(
ht
N
ot
S
tuck
⊤
P
%
I
e
%
E
Φ
%
I
)
(
at
level
20
,
P
,
e
,
Φ
at
level
200
,
format
"{{ P } } e {{ Φ } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e ? {{ Φ } }"
:
=
(
ht
m
aybe
_s
tuck
⊤
P
%
I
e
%
E
Φ
%
I
)
Notation
"{{ P } } e ? {{ Φ } }"
:
=
(
ht
M
aybe
S
tuck
⊤
P
%
I
e
%
E
Φ
%
I
)
(
at
level
20
,
P
,
e
,
Φ
at
level
200
,
format
"{{ P } } e ? {{ Φ } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e @ s ; E {{ v , Q } }"
:
=
(
ht
s
E
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
(
at
level
20
,
P
,
e
,
Q
at
level
200
,
format
"{{ P } } e @ s ; E {{ v , Q } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e @ E {{ v , Q } }"
:
=
(
ht
n
ot
_s
tuck
E
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
Notation
"{{ P } } e @ E {{ v , Q } }"
:
=
(
ht
N
ot
S
tuck
E
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
(
at
level
20
,
P
,
e
,
Q
at
level
200
,
format
"{{ P } } e @ E {{ v , Q } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e @ E ? {{ v , Q } }"
:
=
(
ht
m
aybe
_s
tuck
E
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
Notation
"{{ P } } e @ E ? {{ v , Q } }"
:
=
(
ht
M
aybe
S
tuck
E
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
(
at
level
20
,
P
,
e
,
Q
at
level
200
,
format
"{{ P } } e @ E ? {{ v , Q } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e {{ v , Q } }"
:
=
(
ht
n
ot
_s
tuck
⊤
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
Notation
"{{ P } } e {{ v , Q } }"
:
=
(
ht
N
ot
S
tuck
⊤
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
(
at
level
20
,
P
,
e
,
Q
at
level
200
,
format
"{{ P } } e {{ v , Q } }"
)
:
stdpp_scope
.
Notation
"{{ P } } e ? {{ v , Q } }"
:
=
(
ht
m
aybe
_s
tuck
⊤
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
Notation
"{{ P } } e ? {{ v , Q } }"
:
=
(
ht
M
aybe
S
tuck
⊤
P
%
I
e
%
E
(
λ
v
,
Q
)%
I
)
(
at
level
20
,
P
,
e
,
Q
at
level
200
,
format
"{{ P } } e ? {{ v , Q } }"
)
:
stdpp_scope
.
...
...
theories/program_logic/language.v
View file @
0841a63d
...
...
@@ -53,7 +53,7 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
Instance
language_ctx_id
Λ
:
LanguageCtx
(@
id
(
expr
Λ
)).
Proof
.
constructor
;
naive_solver
.
Qed
.
Inductive
atomicity
:
=
s
trongly
_a
tomic
|
w
eakly
_a
tomic
.
Inductive
atomicity
:
=
S
trongly
A
tomic
|
W
eakly
A
tomic
.
Section
language
.
Context
{
Λ
:
language
}.
...
...
@@ -74,21 +74,21 @@ Section language.
Definition
stuck
(
e
:
expr
Λ
)
(
σ
:
state
Λ
)
:
=
to_val
e
=
None
∧
irreducible
e
σ
.
(* [Atomic
w
eakly
_a
tomic]: This (weak) form of atomicity is enough to open
(* [Atomic
W
eakly
A
tomic]: This (weak) form of atomicity is enough to open
invariants when WP ensures safety, i.e., programs never can get stuck. We
have an example in lambdaRust of an expression that is atomic in this
sense, but not in the stronger sense defined below, and we have to be able
to open invariants around that expression. See `CasStuckS` in
[lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
[Atomic
s
trongly
_a
tomic]: To open invariants with a WP that does not ensure
[Atomic
S
trongly
A
tomic]: To open invariants with a WP that does not ensure
safety, we need a stronger form of atomicity. With the above definition,
in case `e` reduces to a stuck non-value, there is no proof that the
invariants have been established again. *)
Class
Atomic
(
a
:
atomicity
)
(
e
:
expr
Λ
)
:
Prop
:
=
atomic
σ
e'
σ
'
efs
:
prim_step
e
σ
e'
σ
'
efs
→
if
a
is
w
eakly
_a
tomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
if
a
is
W
eakly
A
tomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
Inductive
step
(
ρ
1
ρ
2
:
cfg
Λ
)
:
Prop
:
=
|
step_atomic
e1
σ
1 e2
σ
2
efs
t1
t2
:
...
...
@@ -110,7 +110,7 @@ Section language.
Proof
.
by
intros
v
v'
Hv
;
apply
(
inj
Some
)
;
rewrite
-!
to_of_val
Hv
.
Qed
.
Lemma
strongly_atomic_atomic
e
:
Atomic
s
trongly
_a
tomic
e
→
Atomic
w
eakly
_a
tomic
e
.
Atomic
S
trongly
A
tomic
e
→
Atomic
W
eakly
A
tomic
e
.
Proof
.
unfold
Atomic
.
eauto
using
val_irreducible
.
Qed
.
Lemma
reducible_fill
`
{
LanguageCtx
Λ
K
}
e
σ
:
...
...
theories/program_logic/lifting.v
View file @
0841a63d
...
...
@@ -15,7 +15,7 @@ Implicit Types Φ : val Λ → iProp Σ.
Lemma
wp_lift_step
s
E
Φ
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
⌜
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
...
...
@@ -36,7 +36,7 @@ Qed.
(** Derived lifting lemmas. *)
Lemma
wp_lift_pure_step
`
{
Inhabited
(
state
Λ
)}
s
E
E'
Φ
e1
:
(
∀
σ
1
,
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1
,
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1 e2
σ
2
efs
,
prim_step
e1
σ
1 e2
σ
2
efs
→
σ
1
=
σ
2
)
→
(|={
E
,
E'
}
▷
=>
∀
e2
efs
σ
,
⌜
prim_step
e1
σ
e2
σ
efs
⌝
→
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
...
...
@@ -69,7 +69,7 @@ Qed.
Lemma
wp_lift_atomic_step
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
⌜
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
⌜
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
...
...
@@ -85,7 +85,7 @@ Proof.
Qed
.
Lemma
wp_lift_pure_det_step
`
{
Inhabited
(
state
Λ
)}
{
s
E
E'
Φ
}
e1
e2
efs
:
(
∀
σ
1
,
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1
,
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1 e2
'
σ
2
efs'
,
prim_step
e1
σ
1 e2
'
σ
2
efs'
→
σ
1
=
σ
2
∧
e2
=
e2'
∧
efs
=
efs'
)
→
(|={
E
,
E'
}
▷
=>
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
...
...
theories/program_logic/ownp.v
View file @
0841a63d
...
...
@@ -86,7 +86,7 @@ Section lifting.
Proof
.
rewrite
/
ownP
;
apply
_
.
Qed
.
Lemma
ownP_lift_step
s
E
Φ
e1
:
(|={
E
,
∅
}=>
∃
σ
1
,
⌜
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
⌝
∗
▷
ownP
σ
1
∗
(|={
E
,
∅
}=>
∃
σ
1
,
⌜
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
⌝
∗
▷
ownP
σ
1
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
-
∗
ownP
σ
2
={
∅
,
E
}=
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
...
...
@@ -119,7 +119,7 @@ Section lifting.
Qed
.
Lemma
ownP_lift_pure_step
`
{
Inhabited
(
state
Λ
)}
s
E
Φ
e1
:
(
∀
σ
1
,
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1
,
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1 e2
σ
2
efs
,
prim_step
e1
σ
1 e2
σ
2
efs
→
σ
1
=
σ
2
)
→
(
▷
∀
e2
efs
σ
,
⌜
prim_step
e1
σ
e2
σ
efs
⌝
→
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
...
...
@@ -136,7 +136,7 @@ Section lifting.
(** Derived lifting lemmas. *)
Lemma
ownP_lift_atomic_step
{
s
E
Φ
}
e1
σ
1
:
(
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
▷
ownP
σ
1
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
-
∗
ownP
σ
2
-
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
...
...
@@ -151,7 +151,7 @@ Section lifting.
Qed
.
Lemma
ownP_lift_atomic_det_step
{
s
E
Φ
e1
}
σ
1
v2
σ
2
efs
:
(
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
e2'
σ
2
'
efs'
,
prim_step
e1
σ
1 e2
'
σ
2
'
efs'
→
σ
2
=
σ
2
'
∧
to_val
e2'
=
Some
v2
∧
efs
=
efs'
)
→
▷
ownP
σ
1
∗
▷
(
ownP
σ
2
-
∗
...
...
@@ -164,7 +164,7 @@ Section lifting.
Qed
.
Lemma
ownP_lift_atomic_det_step_no_fork
{
s
E
e1
}
σ
1
v2
σ
2
:
(
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
e2'
σ
2
'
efs'
,
prim_step
e1
σ
1 e2
'
σ
2
'
efs'
→
σ
2
=
σ
2
'
∧
to_val
e2'
=
Some
v2
∧
[]
=
efs'
)
→
{{{
▷
ownP
σ
1
}}}
e1
@
s
;
E
{{{
RET
v2
;
ownP
σ
2
}}}.
...
...
@@ -174,7 +174,7 @@ Section lifting.
Qed
.
Lemma
ownP_lift_pure_det_step
`
{
Inhabited
(
state
Λ
)}
{
s
E
Φ
}
e1
e2
efs
:
(
∀
σ
1
,
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1
,
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1 e2
'
σ
2
efs'
,
prim_step
e1
σ
1 e2
'
σ
2
efs'
→
σ
1
=
σ
2
∧
e2
=
e2'
∧
efs
=
efs'
)
→
▷
(
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
...
...
@@ -184,7 +184,7 @@ Section lifting.
Qed
.
Lemma
ownP_lift_pure_det_step_no_fork
`
{
Inhabited
(
state
Λ
)}
{
s
E
Φ
}
e1
e2
:
(
∀
σ
1
,
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1
,
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
∀
σ
1 e2
'
σ
2
efs'
,
prim_step
e1
σ
1 e2
'
σ
2
efs'
→
σ
1
=
σ
2
∧
e2
=
e2'
∧
[]
=
efs'
)
→
▷
WP
e2
@
s
;
E
{{
Φ
}}
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
...
...
theories/program_logic/weakestpre.v
View file @
0841a63d
...
...
@@ -11,11 +11,11 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
}.
Notation
irisG
Λ
Σ
:
=
(
irisG'
(
state
Λ
)
Σ
).
Inductive
stuckness
:
=
n
ot
_s
tuck
|
m
aybe
_s
tuck
.
Inductive
stuckness
:
=
N
ot
S
tuck
|
M
aybe
S
tuck
.
Definition
stuckness_le
(
s1
s2
:
stuckness
)
:
bool
:
=
match
s1
,
s2
with
|
m
aybe
_s
tuck
,
n
ot
_s
tuck
=>
false
|
M
aybe
S
tuck
,
N
ot
S
tuck
=>
false
|
_
,
_
=>
true
end
.
Instance
:
PreOrder
stuckness_le
.
...
...
@@ -25,7 +25,7 @@ Qed.
Instance
:
SqSubsetEq
stuckness
:
=
stuckness_le
.
Definition
stuckness_to_atomicity
(
s
:
stuckness
)
:
atomicity
:
=
if
s
is
m
aybe
_s
tuck
then
s
trongly
_a
tomic
else
w
eakly
_a
tomic
.
if
s
is
M
aybe
S
tuck
then
S
trongly
A
tomic
else
W
eakly
A
tomic
.
Definition
wp_pre
`
{
irisG
Λ
Σ
}
(
s
:
stuckness
)
(
wp
:
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
)
:
...
...
@@ -33,7 +33,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
match
to_val
e1
with
|
Some
v
=>
|={
E
}=>
Φ
v
|
None
=>
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
n
ot
_s
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
N
ot
S
tuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
wp
E
e2
Φ
∗
[
∗
list
]
ef
∈
efs
,
wp
⊤
ef
(
λ
_
,
True
)
...
...
@@ -57,32 +57,32 @@ Instance: Params (@wp) 6.
Notation
"'WP' e @ s ; E {{ Φ } }"
:
=
(
wp
s
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"'[' 'WP' e '/' @ s ; E {{ Φ } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e @ E {{ Φ } }"
:
=
(
wp
n
ot
_s
tuck
E
e
%
E
Φ
)
Notation
"'WP' e @ E {{ Φ } }"
:
=
(
wp
N
ot
S
tuck
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"'[' 'WP' e '/' @ E {{ Φ } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e @ E ? {{ Φ } }"
:
=
(
wp
m
aybe
_s
tuck
E
e
%
E
Φ
)
Notation
"'WP' e @ E ? {{ Φ } }"
:
=
(
wp
M
aybe
S
tuck
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"'[' 'WP' e '/' @ E ? {{ Φ } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e {{ Φ } }"
:
=
(
wp
n
ot
_s
tuck
⊤
e
%
E
Φ
)
Notation
"'WP' e {{ Φ } }"
:
=
(
wp
N
ot
S
tuck
⊤
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"'[' 'WP' e '/' {{ Φ } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e ? {{ Φ } }"
:
=
(
wp
m
aybe
_s
tuck
⊤
e
%
E
Φ
)
Notation
"'WP' e ? {{ Φ } }"
:
=
(
wp
M
aybe
S
tuck
⊤
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"'[' 'WP' e '/' ? {{ Φ } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e @ s ; E {{ v , Q } }"
:
=
(
wp
s
E
e
%
E
(
λ
v
,
Q
))
(
at
level
20
,
e
,
Q
at
level
200
,
format
"'[' 'WP' e '/' @ s ; E {{ v , Q } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e @ E {{ v , Q } }"
:
=
(
wp
n
ot
_s
tuck
E
e
%
E
(
λ
v
,
Q
))
Notation
"'WP' e @ E {{ v , Q } }"
:
=
(
wp
N
ot
S
tuck
E
e
%
E
(
λ
v
,
Q
))
(
at
level
20
,
e
,
Q
at
level
200
,
format
"'[' 'WP' e '/' @ E {{ v , Q } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e @ E ? {{ v , Q } }"
:
=
(
wp
m
aybe
_s
tuck
E
e
%
E
(
λ
v
,
Q
))
Notation
"'WP' e @ E ? {{ v , Q } }"
:
=
(
wp
M
aybe
S
tuck
E
e
%
E
(
λ
v
,
Q
))
(
at
level
20
,
e
,
Q
at
level
200
,
format
"'[' 'WP' e '/' @ E ? {{ v , Q } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e {{ v , Q } }"
:
=
(
wp
n
ot
_s
tuck
⊤
e
%
E
(
λ
v
,
Q
))
Notation
"'WP' e {{ v , Q } }"
:
=
(
wp
N
ot
S
tuck
⊤
e
%
E
(
λ
v
,
Q
))
(
at
level
20
,
e
,
Q
at
level
200
,
format
"'[' 'WP' e '/' {{ v , Q } } ']'"
)
:
uPred_scope
.
Notation
"'WP' e ? {{ v , Q } }"
:
=
(
wp
m
aybe
_s
tuck
⊤
e
%
E
(
λ
v
,
Q
))
Notation
"'WP' e ? {{ v , Q } }"
:
=
(
wp
M
aybe
S
tuck
⊤
e
%
E
(
λ
v
,
Q
))
(
at
level
20
,
e
,
Q
at
level
200
,
format
"'[' 'WP' e '/' ? {{ v , Q } } ']'"
)
:
uPred_scope
.
...
...
@@ -400,3 +400,4 @@ Section proofmode_classes.
(
WP
e
@
s
;
E1
{{
Φ
}})
(
WP
e
@
s
;
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})%
I
|
100
.
Proof
.
intros
.
by
rewrite
/
ElimModal
fupd_frame_r
wand_elim_r
wp_atomic
.
Qed
.
End
proofmode_classes
.
theories/tests/heap_lang.v
View file @
0841a63d
...
...
@@ -96,5 +96,5 @@ Section LiftingTests.
Proof
.
iIntros
""
.
wp_apply
Pred_spec
.
wp_let
.
by
wp_apply
Pred_spec
.
Qed
.
End
LiftingTests
.
Lemma
heap_e_adequate
σ
:
adequate
n
ot
_s
tuck
heap_e
σ
(=
#
2
).
Lemma
heap_e_adequate
σ
:
adequate
N
ot
S
tuck
heap_e
σ
(=
#
2
).
Proof
.
eapply
(
heap_adequacy
heap
Σ
)=>
?.
by
apply
heap_e_spec
.
Qed
.
theories/tests/ipm_paper.v
View file @
0841a63d
...
...
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
mask changing update modalities directly in our proofs, but in this file we use
the first prove the rule as a lemma, and then use that. *)
Lemma
wp_inv_open
`
{
irisG
Λ
Σ
}
N
E
P
e
Φ
:
nclose
N
⊆
E
→
Atomic
w
eakly
_a
tomic
e
→
nclose
N
⊆
E
→
Atomic
W
eakly
A
tomic
e
→
inv
N
P
∗
(
▷
P
-
∗
WP
e
@
E
∖
↑
N
{{
v
,
▷
P
∗
Φ
v
}})
⊢
WP
e
@
E
{{
Φ
}}.
Proof
.
iIntros
(??)
"[#Hinv Hwp]"
.
...
...
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