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
Tej Chajed
iris
Commits
dbe52472
Commit
dbe52472
authored
Mar 29, 2016
by
Robbert Krebbers
Browse files
Misc language clean up.
parent
27cfd068
Changes
8
Hide whitespace changes
Inline
Side-by-side
algebra/cofe.v
View file @
dbe52472
...
...
@@ -422,7 +422,6 @@ Proof.
apply
cofe_morC_map_ne
;
apply
cFunctor_contractive
=>
i
?
;
split
;
by
apply
Hfg
.
Qed
.
(** Discrete cofe *)
Section
discrete_cofe
.
Context
`
{
Equiv
A
,
@
Equivalence
A
(
≡
)}.
...
...
heap_lang/lang.v
View file @
dbe52472
...
...
@@ -228,14 +228,12 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
end
.
Solve
Obligations
with
set_solver
.
Program
Definition
wexpr'
{
X
}
(
e
:
expr
[])
:
expr
X
:
=
wexpr
_
e
.
Solve
Obligations
with
set_solver
.
Definition
wexpr'
{
X
}
(
e
:
expr
[])
:
expr
X
:
=
wexpr
(
included_nil
_
)
e
.
Definition
of_val'
{
X
}
(
v
:
val
)
:
expr
X
:
=
wexpr
(
included_nil
_
)
(
of_val
v
).
Lemma
wsubst_rec_true_prf
{
X
Y
x
}
(
H
:
X
`
included
`
x
::
Y
)
{
f
y
}
(
Hfy
:
BNamed
x
≠
f
∧
BNamed
x
≠
y
)
:
(
Hfy
:
BNamed
x
≠
f
∧
BNamed
x
≠
y
)
:
f
:
b
:
y
:
b
:
X
`
included
`
x
::
f
:
b
:
y
:
b
:
Y
.
Proof
.
set_solver
.
Qed
.
Lemma
wsubst_rec_false_prf
{
X
Y
x
}
(
H
:
X
`
included
`
x
::
Y
)
{
f
y
}
...
...
@@ -413,21 +411,6 @@ Proof.
apply
wsubst_closed
,
not_elem_of_nil
.
Qed
.
Lemma
of_val'_closed
(
v
:
val
)
:
of_val'
v
=
of_val
v
.
Proof
.
by
rewrite
/
of_val'
wexpr_id
.
Qed
.
(** to_val propagation.
TODO: automatically appliy in wp_tactics? *)
Lemma
to_val_InjL
e
v
:
to_val
e
=
Some
v
→
to_val
(
InjL
e
)
=
Some
(
InjLV
v
).
Proof
.
move
=>
H
.
simpl
.
by
rewrite
H
.
Qed
.
Lemma
to_val_InjR
e
v
:
to_val
e
=
Some
v
→
to_val
(
InjR
e
)
=
Some
(
InjRV
v
).
Proof
.
move
=>
H
.
simpl
.
by
rewrite
H
.
Qed
.
Lemma
to_val_Pair
e1
e2
v1
v2
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
to_val
(
Pair
e1
e2
)
=
Some
(
PairV
v1
v2
).
Proof
.
move
=>
H1
H2
.
simpl
.
by
rewrite
H1
H2
.
Qed
.
(** Basic properties about the language *)
Lemma
to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
.
Proof
.
by
induction
v
;
simplify_option_eq
.
Qed
.
...
...
@@ -452,10 +435,6 @@ Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Instance
fill_inj
K
:
Inj
(=)
(=)
(
fill
K
).
Proof
.
red
;
induction
K
as
[|
Ki
K
IH
]
;
naive_solver
.
Qed
.
Lemma
fill_inj'
K
e1
e2
:
fill
K
e1
=
fill
K
e2
→
e1
=
e2
.
Proof
.
eapply
fill_inj
.
Qed
.
Lemma
fill_val
K
e
:
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
).
Proof
.
intros
[
v'
Hv'
]
;
revert
v'
Hv'
.
...
...
@@ -574,16 +553,16 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
End
heap_lang
.
(** Language *)
Program
Canonical
Structur
e
heap_ectx_lang
:
e
ctx
_l
anguage
(
heap_lang
.
expr
[])
heap_lang
.
val
heap_lang
.
ectx
heap_lang
.
state
:
=
{|
of_val
:
=
heap_lang
.
of_val
;
to_val
:
=
heap_lang
.
to_val
;
empty_ectx
:
=
[]
;
comp_ectx
:
=
app
;
fill
:
=
heap_lang
.
fill
;
atomic
:
=
heap_lang
.
atomic
;
head_step
:
=
heap_lang
.
head_step
;
|}.
Program
Instanc
e
heap_ectx_lang
:
E
ctx
L
anguage
(
heap_lang
.
expr
[])
heap_lang
.
val
heap_lang
.
ectx
heap_lang
.
state
:
=
{|
of_val
:
=
heap_lang
.
of_val
;
to_val
:
=
heap_lang
.
to_val
;
empty_ectx
:
=
[]
;
comp_ectx
:
=
(++)
;
fill
:
=
heap_lang
.
fill
;
atomic
:
=
heap_lang
.
atomic
;
head_step
:
=
heap_lang
.
head_step
;
|}.
Solve
Obligations
with
eauto
using
heap_lang
.
to_of_val
,
heap_lang
.
of_to_val
,
heap_lang
.
val_stuck
,
heap_lang
.
atomic_not_val
,
heap_lang
.
atomic_step
,
heap_lang
.
fill_inj'
,
heap_lang
.
fill_not_val
,
heap_lang
.
atomic_fill
,
heap_lang
.
fill_not_val
,
heap_lang
.
atomic_fill
,
heap_lang
.
step_by_val
,
fold_right_app
,
app_eq_nil
.
Canonical
Structure
heap_lang
:
=
ectx_lang
heap_ectx_lang
.
...
...
heap_lang/lib/spawn.v
View file @
dbe52472
...
...
@@ -74,12 +74,11 @@ Proof.
solve_sep_entails
.
-
wp_focus
(
f
_
).
rewrite
wp_frame_r
wp_frame_l
.
rewrite
(
of_to_val
e
)
//.
apply
wp_mono
=>
v
.
eapply
(
inv_fsa
(
wp_fsa
_
))
with
(
N0
:
=
N
)
;
simpl
;
(* TODO: Collect these in some Hint DB? Or add to an existing one? *)
eauto
using
to_val_InjR
,
to_val_InjL
,
to_of_val
with
I
ndisj
.
eapply
(
inv_fsa
(
wp_fsa
_
))
with
(
N0
:
=
N
)
;
rewrite
/=
?to_of_val
;
eauto
with
I
ndisj
.
apply
wand_intro_l
.
rewrite
/
spawn_inv
{
1
}
later_exist
!
sep_exist_r
.
apply
exist_elim
=>
lv
.
rewrite
later_sep
.
eapply
wp_store
;
eauto
using
to_val_InjR
,
to_val_InjL
,
to_of_val
with
I
ndisj
.
eapply
wp_store
;
rewrite
/=
?to_of_val
;
eauto
with
I
ndisj
.
cancel
[
▷
(
l
↦
lv
)]%
I
.
strip_later
.
apply
wand_intro_l
.
rewrite
right_id
-
later_intro
-{
2
}[(
∃
_
,
_
↦
_
★
_
)%
I
](
exist_intro
(
InjRV
v
)).
ecancel
[
l
↦
_
]%
I
.
apply
or_intro_r'
.
rewrite
sep_elim_r
sep_elim_r
sep_elim_l
.
...
...
@@ -115,5 +114,4 @@ Proof.
wp_case
.
wp_let
.
ewp
(
eapply
wp_value
;
wp_done
).
rewrite
(
forall_elim
v
).
rewrite
!
assoc
.
eapply
wand_apply_r'
;
eauto
with
I
.
Qed
.
End
proof
.
heap_lang/lifting.v
View file @
dbe52472
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Import ownership. (* for ownP *)
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
Require
Import
tactics
.
Import
uPred
.
Local
Hint
Extern
0
(
head_reducible
_
_
)
=>
do_step
eauto
2
.
Local
Hint
Extern
0
(
head_reducible
_
_
)
=>
do_
head_
step
eauto
2
.
Section
lifting
.
Context
{
Σ
:
iFunctor
}.
...
...
@@ -27,7 +27,7 @@ Proof.
intros
.
set
(
φ
(
e'
:
expr
[])
σ
'
ef
:
=
∃
l
,
ef
=
None
∧
e'
=
Loc
l
∧
σ
'
=
<[
l
:
=
v
]>
σ
∧
σ
!!
l
=
None
).
rewrite
-(
wp_lift_atomic_head_step
(
Alloc
e
)
φ
σ
)
//
/
φ
;
last
(
by
intros
;
inv_step
;
eauto
8
)
;
last
(
by
simpl
;
eauto
).
last
(
by
intros
;
inv_
head_
step
;
eauto
8
)
;
last
(
by
simpl
;
eauto
).
apply
sep_mono
,
later_mono
;
first
done
.
apply
forall_intro
=>
v2
;
apply
forall_intro
=>
σ
2
;
apply
forall_intro
=>
ef
.
apply
wand_intro_l
.
...
...
@@ -43,7 +43,7 @@ Lemma wp_load_pst E σ l v Φ :
(
▷
ownP
σ
★
▷
(
ownP
σ
-
★
Φ
v
))
⊢
WP
Load
(
Loc
l
)
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_head_step
σ
v
σ
None
)
?right_id
//
;
last
(
by
intros
;
inv_step
;
eauto
using
to_of_val
)
;
simpl
;
by
eauto
.
last
(
by
intros
;
inv_
head_
step
;
eauto
using
to_of_val
)
;
simpl
;
by
eauto
.
Qed
.
Lemma
wp_store_pst
E
σ
l
e
v
v'
Φ
:
...
...
@@ -52,7 +52,7 @@ Lemma wp_store_pst E σ l e v v' Φ :
⊢
WP
Store
(
Loc
l
)
e
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_head_step
σ
(
LitV
LitUnit
)
(<[
l
:
=
v
]>
σ
)
None
)
?right_id
//
;
last
(
by
intros
;
inv_step
;
eauto
)
;
simpl
;
by
eauto
.
?right_id
//
;
last
(
by
intros
;
inv_
head_
step
;
eauto
)
;
simpl
;
by
eauto
.
Qed
.
Lemma
wp_cas_fail_pst
E
σ
l
e1
v1
e2
v2
v'
Φ
:
...
...
@@ -61,7 +61,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_head_step
σ
(
LitV
$
LitBool
false
)
σ
None
)
?right_id
//
;
last
(
by
intros
;
inv_step
;
eauto
)
;
?right_id
//
;
last
(
by
intros
;
inv_
head_
step
;
eauto
)
;
simpl
;
split_and
?
;
by
eauto
.
Qed
.
...
...
@@ -71,7 +71,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
⊢
WP
CAS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_head_step
σ
(
LitV
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
None
)
?right_id
//
;
last
(
by
intros
;
inv_step
;
eauto
)
;
(<[
l
:
=
v2
]>
σ
)
None
)
?right_id
//
;
last
(
by
intros
;
inv_
head_
step
;
eauto
)
;
simpl
;
split_and
?
;
by
eauto
.
Qed
.
...
...
@@ -80,7 +80,7 @@ Lemma wp_fork E e Φ :
(
▷
Φ
(
LitV
LitUnit
)
★
▷
WP
e
{{
λ
_
,
True
}})
⊢
WP
Fork
e
@
E
{{
Φ
}}.
Proof
.
rewrite
-(
wp_lift_pure_det_head_step
(
Fork
e
)
(
Lit
LitUnit
)
(
Some
e
))
//=
;
last
by
intros
;
inv_step
;
eauto
.
last
by
intros
;
inv_
head_
step
;
eauto
.
rewrite
later_sep
-(
wp_value
_
_
(
Lit
_
))
//.
Qed
.
...
...
@@ -91,7 +91,7 @@ Lemma wp_rec E f x e1 e2 v Φ :
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
App
_
_
)
(
subst'
x
e2
(
subst'
f
(
Rec
f
x
e1
)
e1
))
None
)
//=
?right_id
;
intros
;
inv_step
;
eauto
.
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_rec'
E
f
x
erec
e1
e2
v2
Φ
:
...
...
@@ -106,7 +106,7 @@ Lemma wp_un_op E op l l' Φ :
▷
Φ
(
LitV
l'
)
⊢
WP
UnOp
op
(
Lit
l
)
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
UnOp
op
_
)
(
Lit
l'
)
None
)
?right_id
-
?wp_value
//
;
intros
;
inv_step
;
eauto
.
?right_id
-
?wp_value
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_bin_op
E
op
l1
l2
l'
Φ
:
...
...
@@ -114,21 +114,21 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
▷
Φ
(
LitV
l'
)
⊢
WP
BinOp
op
(
Lit
l1
)
(
Lit
l2
)
@
E
{{
Φ
}}.
Proof
.
intros
Heval
.
rewrite
-(
wp_lift_pure_det_head_step
(
BinOp
op
_
_
)
(
Lit
l'
)
None
)
?right_id
-
?wp_value
//
;
intros
;
inv_step
;
eauto
.
?right_id
-
?wp_value
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_if_true
E
e1
e2
Φ
:
▷
WP
e1
@
E
{{
Φ
}}
⊢
WP
If
(
Lit
(
LitBool
true
))
e1
e2
@
E
{{
Φ
}}.
Proof
.
rewrite
-(
wp_lift_pure_det_head_step
(
If
_
_
_
)
e1
None
)
?right_id
//
;
intros
;
inv_step
;
eauto
.
?right_id
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_if_false
E
e1
e2
Φ
:
▷
WP
e2
@
E
{{
Φ
}}
⊢
WP
If
(
Lit
(
LitBool
false
))
e1
e2
@
E
{{
Φ
}}.
Proof
.
rewrite
-(
wp_lift_pure_det_head_step
(
If
_
_
_
)
e2
None
)
?right_id
//
;
intros
;
inv_step
;
eauto
.
?right_id
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_fst
E
e1
v1
e2
v2
Φ
:
...
...
@@ -136,7 +136,7 @@ Lemma wp_fst E e1 v1 e2 v2 Φ :
▷
Φ
v1
⊢
WP
Fst
(
Pair
e1
e2
)
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
Fst
_
)
e1
None
)
?right_id
-
?wp_value
//
;
intros
;
inv_step
;
eauto
.
?right_id
-
?wp_value
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_snd
E
e1
v1
e2
v2
Φ
:
...
...
@@ -144,7 +144,7 @@ Lemma wp_snd E e1 v1 e2 v2 Φ :
▷
Φ
v2
⊢
WP
Snd
(
Pair
e1
e2
)
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
Snd
_
)
e2
None
)
?right_id
-
?wp_value
//
;
intros
;
inv_step
;
eauto
.
?right_id
-
?wp_value
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_case_inl
E
e0
v0
e1
e2
Φ
:
...
...
@@ -152,7 +152,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Φ :
▷
WP
App
e1
e0
@
E
{{
Φ
}}
⊢
WP
Case
(
InjL
e0
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
Case
_
_
_
)
(
App
e1
e0
)
None
)
?right_id
//
;
intros
;
inv_step
;
eauto
.
(
App
e1
e0
)
None
)
?right_id
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
Lemma
wp_case_inr
E
e0
v0
e1
e2
Φ
:
...
...
@@ -160,7 +160,6 @@ Lemma wp_case_inr E e0 v0 e1 e2 Φ :
▷
WP
App
e2
e0
@
E
{{
Φ
}}
⊢
WP
Case
(
InjR
e0
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_pure_det_head_step
(
Case
_
_
_
)
(
App
e2
e0
)
None
)
?right_id
//
;
intros
;
inv_step
;
eauto
.
(
App
e2
e0
)
None
)
?right_id
//
;
intros
;
inv_
head_
step
;
eauto
.
Qed
.
End
lifting
.
heap_lang/tactics.v
View file @
dbe52472
...
...
@@ -2,18 +2,18 @@ From iris.heap_lang Require Export substitution.
From
iris
.
prelude
Require
Import
fin_maps
.
Import
heap_lang
.
(** The tactic [inv_step] performs inversion on hypotheses of the
(** The tactic [inv_
head_
step] performs inversion on hypotheses of the
shape [head_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
to values, and finite map operations. This tactic is slightly ad-hoc
and tuned for proving our lifting lemmas. *)
Ltac
inv_step
:
=
Ltac
inv_
head_
step
:
=
repeat
match
goal
with
|
_
=>
progress
simplify_map_eq
/=
(* simplify memory stuff *)
|
H
:
to_val
_
=
Some
_
|-
_
=>
apply
of_to_val
in
H
|
H
:
context
[
to_val
(
of_val
_
)]
|-
_
=>
rewrite
to_of_val
in
H
|
H
:
head_step
?e
_
_
_
_
|-
_
=>
try
(
is_var
e
;
fail
1
)
;
(* inversion yields many goals if
e
is a variable
try
(
is_var
e
;
fail
1
)
;
(* inversion yields many goals if
[e]
is a variable
and can thus better be avoided. *)
inversion
H
;
subst
;
clear
H
end
.
...
...
@@ -63,18 +63,15 @@ Ltac reshape_expr e tac :=
|
CAS
?e0
?e1
?e2
=>
go
(
CasLCtx
e1
e2
::
K
)
e0
end
in
go
(@
nil
ectx_item
)
e
.
(** The tactic [do_step tac] solves goals of the shape
[head_reducible] and [head_step] by performing a reduction step and
uses [tac] to solve any side-conditions generated by individual
steps. *)
Tactic
Notation
"do_step"
tactic3
(
tac
)
:
=
(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
[head_step] by performing a reduction step and uses [tac] to solve any
side-conditions generated by individual steps. *)
Tactic
Notation
"do_head_step"
tactic3
(
tac
)
:
=
try
match
goal
with
|-
head_reducible
_
_
=>
eexists
_
,
_
,
_
end
;
simpl
;
match
goal
with
|
|-
head_step
?e1
?
σ
1
?e2
?
σ
2
?ef
=>
first
[
apply
alloc_fresh
|
econstructor
]
;
(* If there is at least one goal left now, then do the last
goal last -- it may rely on evars being instantiaed elsewhere. *)
first
[
fail
|
rewrite
?to_of_val
;
[
tac
..|]
;
tac
;
fast_done
]
(* solve [to_val] side-conditions *)
first
[
rewrite
?to_of_val
;
reflexivity
|
simpl_subst
;
tac
;
fast_done
]
end
.
program_logic/ectx_language.v
View file @
dbe52472
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Export language.
(* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *)
Class
e
ctx
_l
anguage
(
expr
val
ectx
state
:
Type
)
:
=
EctxLanguage
{
Class
E
ctx
L
anguage
(
expr
val
ectx
state
:
Type
)
:
=
{
of_val
:
val
→
expr
;
to_val
:
expr
→
option
val
;
empty_ectx
:
ectx
;
...
...
@@ -18,14 +18,14 @@ Class ectx_language (expr val ectx state : Type) := EctxLanguage {
fill_empty
e
:
fill
empty_ectx
e
=
e
;
fill_comp
K1
K2
e
:
fill
K1
(
fill
K2
e
)
=
fill
(
comp_ectx
K1
K2
)
e
;
fill_inj
K
e1
e2
:
fill
K
e1
=
fill
K
e2
→
e1
=
e2
;
fill_inj
K
:
>
Inj
(=)
(=)
(
fill
K
)
;
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
;
(* There are a whole lot of sensible axioms we could demand for comp_ectx
and empty_ectx. However, this one is enough. *)
(* There are a whole lot of sensible axioms (like associativity, and left and
right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
positivity suffices. *)
ectx_positive
K1
K2
:
empty_ectx
=
comp_ectx
K1
K2
→
K1
=
empty_ectx
∧
K2
=
empty_ectx
;
comp_ectx
K1
K2
=
empty_ectx
→
K1
=
empty_ectx
∧
K2
=
empty_ectx
;
step_by_val
K
K'
e1
e1'
σ
1 e2
σ
2
ef
:
fill
K
e1
=
fill
K'
e1'
→
...
...
@@ -43,6 +43,7 @@ Class ectx_language (expr val ectx state : Type) := EctxLanguage {
to_val
e
=
None
→
K
=
empty_ectx
;
}.
Arguments
of_val
{
_
_
_
_
_
}
_
.
Arguments
to_val
{
_
_
_
_
_
}
_
.
Arguments
empty_ectx
{
_
_
_
_
_
}.
...
...
@@ -56,7 +57,6 @@ Arguments of_to_val {_ _ _ _ _} _ _ _.
Arguments
val_stuck
{
_
_
_
_
_
}
_
_
_
_
_
_
.
Arguments
fill_empty
{
_
_
_
_
_
}
_
.
Arguments
fill_comp
{
_
_
_
_
_
}
_
_
_
.
Arguments
fill_inj
{
_
_
_
_
_
}
_
_
_
_
.
Arguments
fill_not_val
{
_
_
_
_
_
}
_
_
_
.
Arguments
ectx_positive
{
_
_
_
_
_
}
_
_
_
.
Arguments
step_by_val
{
_
_
_
_
_
}
_
_
_
_
_
_
_
_
_
_
_
.
...
...
@@ -65,57 +65,57 @@ Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
Arguments
atomic_fill
{
_
_
_
_
_
}
_
_
_
_
.
(* From an ectx_language, we can construct a language. *)
Section
L
anguage
.
Context
{
expr
val
ectx
state
:
Type
}
{
Λ
:
e
ctx
_l
anguage
expr
val
ectx
state
}.
Section
ectx_l
anguage
.
Context
{
expr
val
ectx
state
}
{
Λ
:
E
ctx
L
anguage
expr
val
ectx
state
}.
Implicit
Types
(
e
:
expr
)
(
K
:
ectx
).
Definition
head_reducible
(
e
:
expr
)
(
σ
:
state
)
:
=
∃
e'
σ
'
ef
,
head_step
e
σ
e'
σ
'
ef
.
Inductive
prim_step
(
e1
:
expr
)
(
σ
1
:
state
)
(
e2
:
expr
)
(
σ
2
:
state
)
(
ef
:
option
expr
)
:
Prop
:
=
Ectx_step
K
e1'
e2'
:
e1
=
fill
K
e1'
→
e2
=
fill
K
e2'
→
head_step
e1'
σ
1 e2
'
σ
2
ef
→
prim_step
e1
σ
1 e2
σ
2
ef
.
(
e2
:
expr
)
(
σ
2
:
state
)
(
ef
:
option
expr
)
:
Prop
:
=
Ectx_step
K
e1'
e2'
:
e1
=
fill
K
e1'
→
e2
=
fill
K
e2'
→
head_step
e1'
σ
1 e2
'
σ
2
ef
→
prim_step
e1
σ
1 e2
σ
2
ef
.
Lemma
val_prim_stuck
e1
σ
1 e2
σ
2
ef
:
prim_step
e1
σ
1 e2
σ
2
ef
→
to_val
e1
=
None
.
Proof
.
intros
[???
->
->
?]
;
eauto
using
fill_not_val
,
val_stuck
.
Qed
.
Lemma
atomic_prim_step
e1
σ
1 e2
σ
2
ef
:
atomic
e1
→
prim_step
e1
σ
1 e2
σ
2
ef
→
is_Some
(
to_val
e2
).
atomic
e1
→
prim_step
e1
σ
1 e2
σ
2
ef
→
is_Some
(
to_val
e2
).
Proof
.
intros
Hatomic
[
K
e1'
e2'
->
->
Hstep
].
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
atomic_fill
,
val_stuck
.
eapply
atomic_step
;
first
done
.
by
rewrite
!
fill_empty
.
revert
Hatomic
;
rewrite
!
fill_empty
.
eauto
using
atomic_step
.
Qed
.
Canonical
Structure
ectx_lang
:
language
:
=
{|
language
.
expr
:
=
expr
;
language
.
val
:
=
val
;
language
.
state
:
=
state
;
language
.
of_val
:
=
of_val
;
language
.
to_val
:
=
to_val
;
language
.
atomic
:
=
atomic
;
language
.
prim_step
:
=
prim_step
;
language
.
atomic
:
=
atomic
;
language
.
prim_step
:
=
prim_step
;
language
.
to_of_val
:
=
to_of_val
;
language
.
of_to_val
:
=
of_to_val
;
language
.
val_stuck
:
=
val_prim_stuck
;
language
.
atomic_not_val
:
=
atomic_not_val
;
language
.
val_stuck
:
=
val_prim_stuck
;
language
.
atomic_not_val
:
=
atomic_not_val
;
language
.
atomic_step
:
=
atomic_prim_step
|}.
(* Some lemmas about this language *)
Lemma
head_prim_
reducible
e
σ
:
head_
reducible
e
σ
→
reducible
e
σ
.
Proof
.
intros
(
e'
&?&?&?).
do
3
eexists
.
eapply
Ectx_step
with
(
K
:
=
empty_ectx
)
;
rewrite
?fill_empty
;
done
.
Qed
.
Lemma
head_prim_
step
e1
σ
1
e
2
σ
2
ef
:
head_
step
e1
σ
1
e
2
σ
2
ef
→
prim_step
e1
σ
1
e
2
σ
2
ef
.
Proof
.
apply
Ectx_step
with
empty_ectx
;
by
rewrite
?fill_empty
.
Qed
.
Lemma
head_prim_reducible
e
σ
:
head_reducible
e
σ
→
reducible
e
σ
.
Proof
.
intros
(
e'
&
σ
'
&
ef
&?).
eexists
e'
,
σ
'
,
ef
.
by
apply
head_prim_step
.
Qed
.
Lemma
head_reducible_prim_step
e1
σ
1 e2
σ
2
ef
:
head_reducible
e1
σ
1
→
prim_step
e1
σ
1 e2
σ
2
ef
→
head_step
e1
σ
1 e2
σ
2
ef
.
Proof
.
intros
Hred
Hstep
.
destruct
Hstep
as
[?
?
?
?
?
Hstep
]
;
subst
.
rename
e1'
into
e1
.
rename
e2'
into
e2
.
destruct
Hred
as
(
e2'
&
σ
2
'
&
ef'
&
HstepK
).
destruct
(
step_by_val
K
empty_ectx
e1
(
fill
K
e1
)
σ
1 e2
'
σ
2
'
ef'
)
as
[
K'
[->
_
]%
ectx_positive
]
;
intros
(
e2''
&
σ
2
''
&
ef''
&?)
[
K
e1'
e2'
->
->
Hstep
].
destruct
(
step_by_val
K
empty_ectx
e1'
(
fill
K
e1'
)
σ
1 e2
''
σ
2
''
ef''
)
as
[
K'
[->
_
]%
symmetry
%
ectx_positive
]
;
eauto
using
fill_empty
,
fill_not_val
,
val_stuck
.
by
rewrite
!
fill_empty
.
Qed
.
...
...
@@ -129,16 +129,10 @@ Section Language.
by
exists
(
comp_ectx
K
K'
)
e1'
e2'
;
rewrite
?Heq1
?Heq2
?fill_comp
.
-
intros
e1
σ
1 e2
σ
2
?
Hnval
[
K''
e1''
e2''
Heq1
->
Hstep
].
destruct
(
step_by_val
K
K''
e1
e1''
σ
1 e2
''
σ
2
ef
)
as
[
K'
->]
;
eauto
.
rewrite
-
fill_comp
in
Heq1
;
apply
fill_inj
in
Heq1
.
rewrite
-
fill_comp
in
Heq1
;
apply
(
inj
(
fill
_
))
in
Heq1
.
exists
(
fill
K'
e2''
)
;
rewrite
-
fill_comp
;
split
;
auto
.
econstructor
;
eauto
.
Qed
.
End
Language
.
Arguments
ectx_lang
{
_
_
_
_
}
_
:
clear
implicits
.
End
ectx_language
.
\ No newline at end of file
Arguments
ectx_lang
{
_
_
_
_
}
_
.
program_logic/ectx_weakestpre.v
View file @
dbe52472
(** Some derived lemmas for ectx-based languages *)
From
iris
.
program_logic
Require
Export
ectx_language
weakestpre
lifting
.
From
iris
.
program_logic
Require
Import
ownership
.
Section
wp
.
Context
{
expr
val
ectx
state
:
Type
}
{
Λ
:
e
ctx
_l
anguage
expr
val
ectx
state
}
{
Σ
:
iFunctor
}.
Context
{
expr
val
ectx
state
}
{
Λ
:
E
ctx
L
anguage
expr
val
ectx
state
}
.
Context
{
Σ
:
iFunctor
}.
Implicit
Types
P
:
iProp
(
ectx_lang
Λ
)
Σ
.
Implicit
Types
Φ
:
val
→
iProp
(
ectx_lang
Λ
)
Σ
.
Implicit
Types
v
:
val
.
Implicit
Types
e
:
expr
.
Hint
Resolve
head_prim_reducible
head_reducible_prim_step
.
Notation
wp_fork
ef
:
=
(
default
True
ef
(
flip
(
wp
⊤
)
(
λ
_
,
True
)))%
I
.
...
...
@@ -24,20 +24,14 @@ Lemma wp_lift_head_step E1 E2
(|={
E1
,
E2
}=>
▷
ownP
σ
1
★
▷
∀
e2
σ
2
ef
,
(
■
φ
e2
σ
2
ef
∧
ownP
σ
2
)
-
★
|={
E2
,
E1
}=>
WP
e2
@
E1
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E1
{{
Φ
}}.
Proof
.
intros
.
apply
wp_lift_step
;
eauto
using
head_prim_reducible
,
head_reducible_prim_step
.
Qed
.
Proof
.
eauto
using
wp_lift_step
.
Qed
.
Lemma
wp_lift_pure_head_step
E
(
φ
:
expr
→
option
expr
→
Prop
)
Φ
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
head_reducible
e1
σ
1
)
→
(
∀
σ
1 e2
σ
2
ef
,
head_step
e1
σ
1 e2
σ
2
ef
→
σ
1
=
σ
2
∧
φ
e2
ef
)
→
(
▷
∀
e2
ef
,
■
φ
e2
ef
→
WP
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
intros
.
apply
wp_lift_pure_step
;
eauto
using
head_prim_reducible
,
head_reducible_prim_step
.
Qed
.
Proof
.
eauto
using
wp_lift_pure_step
.
Qed
.
Lemma
wp_lift_atomic_head_step
{
E
Φ
}
e1
(
φ
:
expr
→
state
→
option
expr
→
Prop
)
σ
1
:
...
...
@@ -47,10 +41,7 @@ Lemma wp_lift_atomic_head_step {E Φ} e1
head_step
e1
σ
1 e2
σ
2
ef
→
φ
e2
σ
2
ef
)
→
(
▷
ownP
σ
1
★
▷
∀
v2
σ
2
ef
,
■
φ
(
of_val
v2
)
σ
2
ef
∧
ownP
σ
2
-
★
Φ
v2
★
wp_fork
ef
)
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
intros
.
apply
wp_lift_atomic_step
;
eauto
using
head_prim_reducible
,
head_reducible_prim_step
.
Qed
.
Proof
.
eauto
using
wp_lift_atomic_step
.
Qed
.
Lemma
wp_lift_atomic_det_head_step
{
E
Φ
e1
}
σ
1
v2
σ
2
ef
:
atomic
e1
→
...
...
@@ -58,19 +49,12 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
(
∀
e2'
σ
2
'
ef'
,
head_step
e1
σ
1 e2
'
σ
2
'
ef'
→
σ
2
=
σ
2
'
∧
to_val
e2'
=
Some
v2
∧
ef
=
ef'
)
→
(
▷
ownP
σ
1
★
▷
(
ownP
σ
2
-
★
Φ
v2
★
wp_fork
ef
))
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
intros
.
apply
wp_lift_atomic_det_step
;
eauto
using
head_prim_reducible
,
head_reducible_prim_step
.
Qed
.
Proof
.
eauto
using
wp_lift_atomic_det_step
.
Qed
.
Lemma
wp_lift_pure_det_head_step
{
E
Φ
}
e1
e2
ef
:
to_val
e1
=
None
→
(
∀
σ
1
,
head_reducible
e1
σ
1
)
→
(
∀
σ
1 e2
'
σ
2
ef'
,
head_step
e1
σ
1 e2
'
σ
2
ef'
→
σ
1
=
σ
2
∧
e2
=
e2'
∧
ef
=
ef'
)
→
▷
(
WP
e2
@
E
{{
Φ
}}
★
wp_fork
ef
)
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
intros
.
apply
wp_lift_pure_det_step
;
eauto
using
head_prim_reducible
,
head_reducible_prim_step
.
Qed
.
Proof
.
eauto
using
wp_lift_pure_det_step
.
Qed
.
End
wp
.
tests/heap_lang.v
View file @
dbe52472
...
...
@@ -6,13 +6,13 @@ Import uPred.
Section
LangTests
.
Definition
add
:
expr
[]
:
=
(#
21
+
#
21
)%
E
.
Goal
∀
σ
,
head_step
add
σ
(#
42
)
σ
None
.
Proof
.
intros
;
do_step
done
.
Qed
.
Proof
.
intros
;
do_
head_
step
done
.
Qed
.
Definition
rec_app
:
expr
[]
:
=
((
rec
:
"f"
"x"
:
=
'
"f"
'
"x"
)
#
0
)%
E
.
Goal
∀
σ
,
head_step
rec_app
σ
rec_app
σ
None
.
Proof
.
intros
.
rewrite
/
rec_app
.
do_
step
simpl_subst
.
Qed
.
Proof
.
intros
.
rewrite
/
rec_app
.
do_
head_step
done
.
Qed
.
Definition
lam
:
expr
[]
:
=
(
λ
:
"x"
,
'
"x"
+
#
21
)%
E
.
Goal
∀
σ
,
head_step
(
lam
#
21
)%
E
σ
add
σ
None
.
Proof
.
intros
.
rewrite
/
lam
.
do_step
done
.
Qed
.
Proof
.
intros
.
rewrite
/
lam
.
do_
head_
step
done
.
Qed
.
End
LangTests
.
Section
LiftingTests
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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