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
Iris
c
Commits
189d129e
Commit
189d129e
authored
Jul 01, 2018
by
Dan Frumin
Browse files
Add pre_bin_op to the vcgen
parent
4827236a
Changes
5
Hide whitespace changes
Inline
Side-by-side
theories/vcgen/dcexpr.v
View file @
189d129e
...
...
@@ -204,6 +204,7 @@ Inductive dcexpr : Type :=
|
dCLoad
:
dcexpr
→
dcexpr
|
dCStore
:
dcexpr
→
dcexpr
→
dcexpr
|
dCBinOp
:
bin_op
→
dcexpr
→
dcexpr
→
dcexpr
|
dCPreBinOp
:
bin_op
→
dcexpr
→
dcexpr
→
dcexpr
|
dCUnOp
:
un_op
→
dcexpr
→
dcexpr
|
dCSeq
:
dcexpr
→
dcexpr
→
dcexpr
|
dCPar
:
dcexpr
→
dcexpr
→
dcexpr
...
...
@@ -216,6 +217,7 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
|
dCLoad
de1
=>
a_load
(
dcexpr_interp
E
de1
)
|
dCStore
de1
de2
=>
a_store
(
dcexpr_interp
E
de1
)
(
dcexpr_interp
E
de2
)
|
dCBinOp
op
de1
de2
=>
a_bin_op
op
(
dcexpr_interp
E
de1
)
(
dcexpr_interp
E
de2
)
|
dCPreBinOp
op
de1
de2
=>
a_pre_bin_op
op
(
dcexpr_interp
E
de1
)
(
dcexpr_interp
E
de2
)
|
dCUnOp
op
de
=>
a_un_op
op
(
dcexpr_interp
E
de
)
|
dCSeq
de1
de2
=>
dcexpr_interp
E
de1
;
ᶜ
dcexpr_interp
E
de2
|
dCPar
de1
de2
=>
dcexpr_interp
E
de1
|||
ᶜ
dcexpr_interp
E
de2
...
...
@@ -235,7 +237,7 @@ Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
match
de
with
|
dCRet
dv
=>
dval_wf
E
dv
|
dCAlloc
de1
|
dCLoad
de1
|
dCUnOp
_
de1
=>
dcexpr_wf
E
de1
|
dCStore
de1
de2
|
dCBinOp
_
de1
de2
|
dCSeq
de1
de2
|
dCPar
de1
de2
=>
|
dCStore
de1
de2
|
dCBinOp
_
de1
de2
|
dCPreBinOp
_
de1
de2
|
dCSeq
de1
de2
|
dCPar
de1
de2
=>
dcexpr_wf
E
de1
&&
dcexpr_wf
E
de2
|
dCUnknown
_
=>
true
end
.
...
...
@@ -260,7 +262,7 @@ Qed.
Lemma
dcexpr_wf_mono
(
E
E'
:
known_locs
)
(
de
:
dcexpr
)
:
dcexpr_wf
E
de
→
E
`
prefix_of
`
E'
→
dcexpr_wf
E'
de
.
Proof
.
induction
de
;
simplify_eq
/=
;
try
eauto
;
[
apply
dval_wf_mono
|
|
|
|]
;
induction
de
;
simplify_eq
/=
;
try
eauto
;
[
apply
dval_wf_mono
|
|
|
|
|]
;
naive_solver
.
Qed
.
...
...
@@ -413,6 +415,12 @@ Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
IntoDCexpr
E
(
a_bin_op
op
e1
e2
)
(
dCBinOp
op
de1
de2
).
Proof
.
intros
[->
?]
[->
?]
;
split
;
simpl
;
auto
.
Qed
.
Global
Instance
into_dcexpr_prebinop
E
e1
e2
op
de1
de2
:
IntoDCexpr
E
e1
de1
→
IntoDCexpr
E
e2
de2
→
IntoDCexpr
E
(
a_pre_bin_op
op
e1
e2
)
(
dCPreBinOp
op
de1
de2
).
Proof
.
intros
[->
?]
[->
?]
;
split
;
simpl
;
auto
.
Qed
.
Global
Instance
into_dcexpr_unop
E
e
op
de
:
IntoDCexpr
E
e
de
→
IntoDCexpr
E
(
a_un_op
op
e
)
(
dCUnOp
op
de
).
...
...
theories/vcgen/denv.v
View file @
189d129e
...
...
@@ -682,7 +682,7 @@ Section denv_spec.
Proof
.
Admitted
.
Lemma
denv_wf_delete_full
E
dv
i
m
m'
:
denv_wf
E
m
→
denv_delete_full
i
m
=
Some
(
m'
,
dv
)
→
denv_wf
E
m'
.
denv_wf
E
m
→
denv_delete_full
i
m
=
Some
(
m'
,
dv
)
→
denv_wf
E
m'
∧
dval_wf
E
dv
.
Proof
.
rewrite
/
denv_delete_full
.
destruct
(
denv_delete_full_aux
i
m
)
as
[[[
m0
q0
]
dv0
]|]
eqn
:
Hdel
;
last
naive_solver
.
...
...
theories/vcgen/tests/basics.v
View file @
189d129e
...
...
@@ -62,4 +62,19 @@ Section test.
(*TODO: test function call with multiple arguments *)
Lemma
test6
(
l
:
loc
)
(
z0
:
Z
)
R
:
l
↦
C
#
z0
-
∗
AWP
♯
l
+=
ᶜ
♯
1
@
R
{{
v
,
⌜
v
=
#
z0
⌝
∧
l
↦
C
[
LLvl
]
#(
z0
+
1
)
}}.
Proof
.
iIntros
"Hl"
.
vcg_solver
.
eauto
.
Qed
.
Lemma
test7
(
l
k
:
loc
)
(
z0
z1
:
Z
)
R
:
l
↦
C
#
z0
-
∗
k
↦
C
#
z1
-
∗
AWP
(
♯
l
+=
ᶜ
♯
1
)
+
ᶜ
(
∗ᶜ♯
k
)
@
R
{{
v
,
⌜
v
=
#(
z0
+
z1
)
⌝
∧
l
↦
C
[
LLvl
]
#(
z0
+
1
)
∗
k
↦
C
#
z1
}}.
Proof
.
iIntros
"Hl Hk"
.
vcg_solver
.
eauto
with
iFrame
.
Qed
.
End
test
.
theories/vcgen/vcg_solver.v
View file @
189d129e
...
...
@@ -79,7 +79,7 @@ End vcg_continue.
Arguments
vcg_wp_continuation
{
_
_
_
_
}.
Declare
Reduction
vcg_cbv
:
=
cbv
[
vcg_wp
vcg_wp_bin_op
vcg_wp_store
vcg_wp_load
vcg_wp_awp_continuation
mapsto_wand_list
].
cbv
[
vcg_wp
vcg_wp_bin_op
vcg_wp_pre_bin_op
vcg_wp_store
vcg_wp_load
vcg_wp_awp_continuation
mapsto_wand_list
].
Ltac
vcg_compute
:
=
match
goal
with
...
...
theories/vcgen/vcgen.v
View file @
189d129e
...
...
@@ -51,6 +51,15 @@ Section vcg.
|
dSome
dv
=>
Some
(
ms2
,
denv_merge
mNew1
mNew2
,
dv
)
|
dNone
|
dUnknown
_
=>
None
end
|
dCPreBinOp
op
de1
de2
=>
''
(
ms1
,
mNew1
,
dl
)
←
vcg_sp
E
ms
de1
;
i
←
is_dloc
E
dl
;
''
(
ms2
,
mNew2
,
dv2
)
←
vcg_sp
E
ms1
de2
;
''
(
ms3
,
mNew3
,
dv
)
←
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
)
;
match
dbin_op_eval
E
op
dv
dv2
with
|
dSome
dv3
=>
Some
(
ms3
,
denv_insert
i
LLvl
1
dv3
mNew3
,
dv
)
|
dNone
|
dUnknown
_
=>
None
end
|
dCUnOp
op
de
=>
''
(
ms1
,
mNew1
,
dv
)
←
vcg_sp
E
ms
de
;
match
dun_op_eval
E
op
dv
with
...
...
@@ -135,6 +144,32 @@ Section vcg.
vcg_wp_continuation
E
Φ
(
dval_interp
E
dw
)
end
%
I
.
Definition
vcg_wp_pre_bin_op
(
E
:
known_locs
)
(
op
:
bin_op
)
(
dv1
dv2
:
dval
)
(
m
:
denv
)
(
Φ
:
known_locs
→
denv
→
dval
→
iProp
Σ
)
:
iProp
Σ
:
=
match
is_dloc
E
dv1
with
|
Some
i
=>
match
denv_delete_full
i
m
with
|
Some
(
m'
,
dw
)
=>
match
dbin_op_eval
E
op
dw
dv2
with
|
dSome
dw'
=>
Φ
E
(
denv_insert
i
LLvl
1
dw'
m'
)
dw
|
mdw
=>
∃
dw'
,
⌜
doption_interp
mdw
=
Some
dw'
⌝
∧
mapsto_wand_list
E
(
denv_insert
i
LLvl
1
dw'
m'
)
(
vcg_wp_continuation
E
Φ
(
dval_interp
E
dw
))
end
|
None
=>
mapsto_wand_list
E
m
(
∃
(
v
w
:
val
),
dloc_interp
E
(
dLoc
i
)
↦
C
v
∗
⌜
bin_op_eval
op
v
(
dval_interp
E
dv2
)
=
Some
w
⌝
∗
(
dloc_interp
E
(
dLoc
i
)
↦
C
[
LLvl
]
w
-
∗
vcg_wp_continuation
E
Φ
v
))
end
|
_
=>
mapsto_wand_list
E
m
(
∃
(
l
:
loc
)
(
v
w
:
val
),
⌜
dval_interp
E
dv1
=
#
l
⌝
∗
l
↦
C
v
∗
⌜
bin_op_eval
op
v
(
dval_interp
E
dv2
)
=
Some
w
⌝
∗
(
l
↦
C
[
LLvl
]
w
-
∗
vcg_wp_continuation
E
Φ
v
))
end
%
I
.
Fixpoint
vcg_wp
(
E
:
known_locs
)
(
m
:
denv
)
(
de
:
dcexpr
)
(
R
:
iProp
Σ
)
(
Φ
:
known_locs
→
denv
→
dval
→
iProp
Σ
)
:
iProp
Σ
:
=
match
de
with
...
...
@@ -167,6 +202,19 @@ Section vcg.
|
None
=>
vcg_wp_awp_continuation
R
E
de
m
Φ
end
end
|
dCPreBinOp
op
de1
de2
=>
match
vcg_sp'
E
m
de1
with
|
Some
(
m'
,
mNew
,
dv1
)
=>
vcg_wp
E
m'
de2
R
(
λ
E
m''
dv2
,
vcg_wp_pre_bin_op
E
op
dv1
dv2
(
denv_merge
mNew
m''
)
Φ
)
|
None
=>
match
vcg_sp'
E
m
de2
with
|
Some
(
m'
,
mNew
,
dv2
)
=>
vcg_wp
E
m'
de1
R
(
λ
E
m''
dv1
,
vcg_wp_pre_bin_op
E
op
dv1
dv2
(
denv_merge
mNew
m''
)
Φ
)
|
None
=>
vcg_wp_awp_continuation
R
E
de
m
Φ
end
end
|
dCUnOp
op
de
=>
vcg_wp
E
m
de
R
(
λ
E
m
dv
,
match
dun_op_eval
E
op
dv
with
...
...
@@ -231,37 +279,35 @@ Section vcg_spec.
-
destruct
(
vcg_sp
E
ms
de
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hout
;
simplify_eq
/=.
destruct
dv1
as
[
dv1
|
|
dv1
]
;
try
destruct
dv1
;
simplify_eq
/=.
destruct
d
as
[
i
|?]
;
simplify_eq
/=.
destruct
(
denv_delete_frac_2
i
ms1
mNew1
)
as
[[[[
ms2
mNew2
]
q
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
transitivity
(
length
ms1
).
+
by
eapply
IHde
.
+
by
eapply
denv_delete_frac_2_length
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
(
denv_delete_frac_2
i
ms1
mNew1
)
as
[[[[
ms2
mNew2
]
q
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
using
denv_delete_frac_2_length
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
dv1
as
[
dv1
|
|
dv1
]
;
try
destruct
dv1
;
simplify_eq
/=.
destruct
d
as
[
i
|?]
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
(
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
))
as
[[[
ms3
mNew3
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
transitivity
(
length
ms1
).
+
by
eapply
IHde1
.
+
transitivity
(
length
ms2
).
by
eapply
IHde2
.
by
eapply
denv_delete_full_2_length
.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
(
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
))
as
[[[
ms3
mNew3
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
.
transitivity
(
length
ms2
)
;
eauto
using
denv_delete_full_2_length
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
(
dbin_op_eval
E
b
dv1
dv2
)
eqn
:
Hboe
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
dv1
as
[
dv1
|
|
dv1
]
;
try
destruct
dv1
;
simplify_eq
/=.
destruct
d
as
[
i
|?]
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
(
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
))
as
[[[
ms3
mNew3
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
destruct
(
dbin_op_eval
E
b
dv1
dv2
)
eqn
:
Hboe
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
.
transitivity
(
length
ms2
)
;
eauto
using
denv_delete_full_2_length
.
-
destruct
(
vcg_sp
E
ms
de
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde
;
simplify_eq
/=.
destruct
(
dun_op_eval
E
u
dv1
)
;
simplify_eq
/=.
by
eapply
IHde
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
(
vcg_sp
E
(
denv_unlock
mNew1
::
ms1
)
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
destruct
ms2
;
simplify_eq
/=.
transitivity
(
length
ms1
).
+
by
eapply
IHde1
.
+
apply
IHde2
in
Hde2
;
by
simplify_eq
/=.
destruct
ms2
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
.
apply
IHde2
in
Hde2
;
by
simplify_eq
/=.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hde1
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hde2
;
simplify_eq
/=.
transitivity
(
length
ms1
)
;
eauto
.
...
...
@@ -334,6 +380,31 @@ Section vcg_spec.
iExists
(
dval_interp
E
dv
).
repeat
iSplit
;
eauto
.
+
iPureIntro
.
apply
dbin_op_eval_correct
.
by
rewrite
Hboe
.
+
rewrite
-
denv_merge_interp
.
iFrame
.
-
specialize
(
IHde1
ms
).
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
;
simplify_eq
/=.
destruct
dv1
as
[
dv1
|
|
dv1
]
;
try
destruct
dv1
;
simplify_eq
/=.
destruct
d
as
[
i
|?]
;
simplify_eq
/=.
specialize
(
IHde2
ms1
).
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
;
simplify_eq
/=.
destruct
(
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
))
as
[[[
ms3
mNew3
]
dv'
]
|]
eqn
:
Hfar
;
simplify_eq
/=.
destruct
(
dbin_op_eval
E
b
dv'
dv2
)
eqn
:
Hboe
;
simplify_eq
/=.
iPoseProof
IHde1
as
"Hawp1"
;
first
done
.
iPoseProof
IHde2
as
"Hawp2"
;
first
done
.
iPoseProof
denv_delete_full_2_interp
as
"Hl"
;
first
done
.
iDestruct
(
denv_stack_interp_trans
with
"Hawp1 Hawp2"
)
as
"Hawp'"
.
iDestruct
(
denv_stack_interp_trans
with
"Hawp' Hl"
)
as
"Hawp"
.
iClear
"Hawp1 Hawp2 Hawp' Hl"
.
iApply
(
denv_stack_interp_mono
with
"Hawp"
).
iIntros
"[[Hawp1 Hawp2] Hl]"
.
iApply
(
a_pre_bin_op_spec
with
"Hawp1 Hawp2"
).
iNext
.
iIntros
(?
?)
"[% HmNew1] [% HmNew2] HR"
;
simplify_eq
/=.
iCombine
"HmNew1 HmNew2"
as
"HmNew"
.
rewrite
denv_merge_interp
.
iExists
(
dloc_interp
E
(
dLoc
i
)),
(
dval_interp
E
dv
),
(
dval_interp
E
d
).
iDestruct
(
"Hl"
with
"HmNew"
)
as
"[HmNew $]"
.
repeat
iSplit
;
eauto
.
+
iPureIntro
.
apply
dbin_op_eval_correct
.
by
rewrite
Hboe
.
+
iIntros
"Hl"
.
iFrame
.
iSplit
;
first
done
.
rewrite
-
denv_insert_interp
.
by
iFrame
.
-
specialize
(
IHde
ms
).
destruct
(
vcg_sp
E
ms
de
)
as
[[[
ms1
mNew1
]
dv1
]|]
;
simplify_eq
/=.
remember
(
dun_op_eval
E
u
dv1
)
as
Hu
;
destruct
Hu
;
simplify_eq
/=.
...
...
@@ -448,6 +519,21 @@ Section vcg_spec.
destruct
(
IHde2
_
_
_
_
Hwfms1
Hwfde2
Hsp2
)
as
(?&?&?).
repeat
split
;
eauto
.
apply
denv_wf_merge
;
eauto
.
eapply
(
dbin_op_eval_dSome_wf
_
dv1
dv2
)
;
eauto
.
-
destruct
(
vcg_sp
E
ms
de1
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hsp1
;
simplify_eq
/=.
destruct
dv1
as
[
dv1
|
|
dv1
]
;
try
destruct
dv1
;
simplify_eq
/=.
destruct
d
as
[
i
|?]
;
simplify_eq
/=.
destruct
(
vcg_sp
E
ms1
de2
)
as
[[[
ms2
mNew2
]
dv2
]|]
eqn
:
Hsp2
;
simplify_eq
/=.
destruct
(
denv_delete_full_2
i
ms2
(
denv_merge
mNew1
mNew2
))
as
[[[
ms3
mNew3
]
dv1
]|]
eqn
:
Hout1
;
simplify_eq
/=.
apply
andb_True
in
Hwfde
.
destruct
Hwfde
as
[
Hwfde1
Hwfde2
].
destruct
(
dbin_op_eval
E
b
dv1
dv2
)
eqn
:
Hboe
;
simplify_eq
/=.
destruct
(
IHde1
_
_
_
_
Hwfms
Hwfde1
Hsp1
)
as
(
Hwfms1
&
HwfNew1
&
Hwfdv1
).
destruct
(
IHde2
_
_
_
_
Hwfms1
Hwfde2
Hsp2
)
as
(?&?&?).
eapply
denv_wf_delete_full_2
in
Hout1
;
try
eassumption
.
destruct
Hout1
as
(?&?&?).
repeat
split
;
eauto
using
denv_wf_insert
,
denv_wf_merge
.
eapply
denv_wf_insert
;
eauto
.
eapply
(
dbin_op_eval_dSome_wf
_
dv
dv2
)
;
eauto
.
by
eapply
denv_wf_merge
.
-
destruct
(
vcg_sp
E
ms
de
)
as
[[[
ms1
mNew1
]
dv1
]|]
eqn
:
Hsp1
;
simplify_eq
/=.
destruct
(
IHde
_
_
_
_
Hwfms
Hwfde
Hsp1
)
as
(
Hwfms1
&
HwfNew1
&
Hwfdv1
).
destruct
(
dun_op_eval
E
u
dv1
)
as
[|?|?]
eqn
:
Hop
;
simplify_eq
/=.
...
...
@@ -551,6 +637,47 @@ Section vcg_spec.
iPureIntro
.
apply
dbin_op_eval_correct
.
by
rewrite
Hbin
.
Qed
.
Lemma
vcg_wp_pre_bin_op_correct
E
m
op
dv1
dv2
Φ
:
denv_wf
E
m
→
dval_wf
E
dv2
→
denv_interp
E
m
-
∗
vcg_wp_pre_bin_op
E
op
dv1
dv2
m
Φ
-
∗
∃
l
v
w
,
l
↦
C
v
∗
⌜
dval_interp
E
dv1
=
#
l
⌝
∗
⌜
bin_op_eval
op
v
(
dval_interp
E
dv2
)
=
Some
w
⌝
∗
(
l
↦
C
[
LLvl
]
w
-
∗
vcg_wp_continuation
E
Φ
v
).
Proof
.
iIntros
(?
?)
"Hm Hwp"
.
rewrite
/
vcg_wp_pre_bin_op
.
destruct
(
is_dloc
E
dv1
)
as
[
i
|]
eqn
:
Hloc
;
last
first
.
{
rewrite
mapsto_wand_list_spec
.
iDestruct
(
"Hwp"
with
"Hm"
)
as
(
l
v
w
)
"(%&Hl&%&Hwp)"
.
iExists
l
,
v
,
w
.
iFrame
.
eauto
.
}
apply
is_dloc_some
in
Hloc
.
simplify_eq
/=.
destruct
(
denv_delete_full
i
m
)
as
[[
m'
dw
]
|
]
eqn
:
Hdel
;
last
first
.
-
rewrite
mapsto_wand_list_spec
.
iDestruct
(
"Hwp"
with
"Hm"
)
as
(
v
w
)
"(Hl&%&Hwp)"
.
iExists
(
dloc_interp
E
(
dLoc
i
)),
v
,
w
.
iFrame
.
eauto
.
-
iDestruct
(
denv_delete_full_interp
E
with
"Hm"
)
as
"[Hm' Hl]"
;
first
eassumption
.
destruct
(
dbin_op_eval
E
op
dw
dv2
)
as
[|
dw'
|]
eqn
:
Hop
.
{
iDestruct
"Hwp"
as
(
dw'
)
"[% Hwp]"
.
iExists
(
dloc_interp
E
(
dLoc
i
)),(
dval_interp
E
dw
),(
dval_interp
E
dw'
).
iFrame
.
repeat
iSplit
;
eauto
.
iIntros
"Hl"
.
iCombine
"Hm' Hl"
as
"Hm'"
.
rewrite
denv_insert_interp
.
rewrite
mapsto_wand_list_spec
.
by
iApply
"Hwp"
.
}
{
iExists
(
dloc_interp
E
(
dLoc
i
)),(
dval_interp
E
dw
),(
dval_interp
E
dw'
).
iFrame
.
repeat
iSplit
;
eauto
;
try
iPureIntro
.
-
apply
dbin_op_eval_correct
.
by
rewrite
Hop
.
-
iIntros
"Hl"
.
iCombine
"Hm' Hl"
as
"Hm'"
.
rewrite
denv_insert_interp
.
rewrite
/
vcg_wp_continuation
.
iExists
E
,
dw
,
_
.
iFrame
.
eapply
denv_wf_delete_full
in
Hdel
;
eauto
.
destruct_and
!.
apply
dbin_op_eval_dSome_wf
in
Hop
;
eauto
.
repeat
iSplit
;
eauto
using
denv_wf_insert
.
}
{
iDestruct
"Hwp"
as
(
dw'
)
"[% Hwp]"
.
iExists
(
dloc_interp
E
(
dLoc
i
)),(
dval_interp
E
dw
),(
dval_interp
E
dw'
).
iFrame
.
repeat
iSplit
;
eauto
.
-
iPureIntro
.
apply
dbin_op_eval_correct
.
by
rewrite
Hop
.
-
iIntros
"Hl"
.
iCombine
"Hm' Hl"
as
"Hm'"
.
rewrite
denv_insert_interp
.
rewrite
mapsto_wand_list_spec
.
by
iApply
"Hwp"
.
}
Qed
.
Lemma
vcg_wp_store_correct
E
m
dv1
dv2
Φ
:
denv_wf
E
m
→
dval_wf
E
dv2
→
...
...
@@ -568,12 +695,10 @@ Section vcg_spec.
+
iExists
(
dloc_interp
E
(
dLoc
i
)),
(
dval_interp
E
dv_old
)
;
iSplit
;
first
done
.
iPoseProof
(
denv_delete_full_interp
E
)
as
"Hdel"
.
eassumption
.
iSpecialize
(
"Hdel"
with
"[$Hm]"
).
iDestruct
"Hdel"
as
"[HmDel Hl]"
;
iFrame
.
iIntros
"Hl"
.
iExists
E
,
dv2
,
(
denv_insert
i
LLvl
1
dv2
m'
)
;
repeat
(
iSplit
;
first
done
).
iSpecialize
(
"Hdel"
with
"Hm"
).
iDestruct
"Hdel"
as
"[HmDel Hl]"
;
iFrame
.
iIntros
"Hl"
.
iExists
E
,
dv2
,
(
denv_insert
i
LLvl
1
dv2
m'
)
;
repeat
(
iSplit
;
first
done
).
iSplit
.
iPureIntro
.
apply
denv_wf_insert
;
last
done
.
by
specialize
(
denv_wf_delete_full
E
dv_old
i
m
m'
Hwf
Hdel
)
as
Hdelwf
.
by
destruct
(
denv_wf_delete_full
E
dv_old
i
m
m'
Hwf
Hdel
)
as
[
Hdelwf
?]
.
rewrite
-
denv_insert_interp
.
eauto
with
iFrame
.
+
rewrite
mapsto_wand_list_spec
.
iSpecialize
(
"Hwp"
with
"[Hm]"
)
;
iFrame
.
...
...
@@ -681,6 +806,43 @@ Section vcg_spec.
{
iApply
(
denv_interp_mono
with
"HmNew"
)
;
eauto
.
}
iExists
w
.
rewrite
(
dval_interp_mono
E
E'
)
//.
iSplit
;
first
done
.
by
iApply
vcg_wp_continuation_mono
.
-
rewrite
{
1
}
/
vcg_wp
;
fold
vcg_wp
.
simpl
in
Hwf
;
apply
andb_prop_elim
in
Hwf
;
destruct
Hwf
as
[
Hwf1
Hwf2
].
destruct
(
vcg_sp'
E
m
de1
)
as
[[[
m'
mNew
]
dv1
]|]
eqn
:
Heqsp
;
last
first
.
+
destruct
(
vcg_sp'
E
m
de2
)
as
[[[
m'
mNew
]
dv2
]|]
eqn
:
Heqsp2
;
last
first
.
{
by
iApply
(
vcg_wp_awp_continuation_correct
with
"Hm Hwp"
).
}
iPoseProof
(
vcg_sp'_correct
)
as
"Hsp"
;
first
eassumption
.
specialize
(
vcg_sp'_wf
_
_
_
_
_
_
Hmwf
Hwf2
Heqsp2
)
as
(?&?&?).
iDestruct
(
"Hsp"
with
"Hm"
)
as
"[Hm' Hde2]"
.
iClear
"Hsp"
;
clear
Heqsp2
Heqsp
.
rewrite
IHde1
;
[|
done
|
done
].
iSpecialize
(
"Hm'"
with
"Hwp"
).
iApply
(
a_pre_bin_op_spec
with
"Hm' Hde2"
)
;
fold
dcexpr_interp
.
iNext
.
iIntros
(
v1
v2
)
"Hex (-> & HmNew) $"
.
iDestruct
"Hex"
as
(
E'
dv1
m''
Heq
Hpre
Hm'wf
)
"(% & Hm' & Hwp)"
;
simplify_eq
/=.
iDestruct
(
denv_interp_mono
with
"HmNew"
)
as
"HmNew"
;
eauto
.
iCombine
(
"HmNew Hm'"
)
as
"Hm"
.
rewrite
denv_merge_interp
.
iDestruct
(
vcg_wp_pre_bin_op_correct
with
"Hm Hwp"
)
as
(
l
v
w
)
"(Hl & % & % & Hwp)"
.
{
apply
denv_wf_merge
;
eauto
using
denv_wf_mono
.
}
{
eapply
dval_wf_mono
;
eauto
.
}
iExists
l
,
v
,
w
.
iFrame
.
repeat
iSplit
;
eauto
.
*
iPureIntro
.
rewrite
(
dval_interp_mono
E
E'
)
;
auto
.
*
rewrite
(
vcg_wp_continuation_mono
E
E'
)
;
auto
.
+
iPoseProof
(
vcg_sp'_correct
)
as
"Hsp"
;
first
eassumption
.
specialize
(
vcg_sp'_wf
_
_
_
_
_
_
Hmwf
Hwf1
Heqsp
)
as
(?&?&?).
iDestruct
(
"Hsp"
with
"Hm"
)
as
"[Hm' Hde1]"
;
iClear
"Hsp"
;
clear
Heqsp
.
rewrite
IHde2
;
[|
done
|
done
].
iSpecialize
(
"Hm'"
with
"Hwp"
).
iRename
"Hm'"
into
"Hde2"
.
iApply
(
a_pre_bin_op_spec
with
"Hde1 Hde2"
)
;
fold
dcexpr_interp
.
iNext
.
iIntros
(
v1
v2
)
"(-> & HmNew) Hex $"
.
iDestruct
"Hex"
as
(
E'
dv2
m2
Hpre
?
Hm'wf
)
"(% & Hm' & Hwp)"
;
simplify_eq
/=.
iDestruct
(
denv_interp_mono
with
"HmNew"
)
as
"HmNew"
;
eauto
.
iCombine
(
"HmNew Hm'"
)
as
"Hm"
.
rewrite
denv_merge_interp
.
iDestruct
(
vcg_wp_pre_bin_op_correct
with
"Hm Hwp"
)
as
(
l
v
w
)
"(Hl & % & % & Hwp)"
.
{
apply
denv_wf_merge
;
eauto
using
denv_wf_mono
.
}
{
eapply
dval_wf_mono
;
eauto
.
}
iExists
l
,
v
,
w
.
iFrame
.
repeat
iSplit
;
eauto
.
*
iPureIntro
.
rewrite
(
dval_interp_mono
E
E'
)
;
auto
.
*
rewrite
(
vcg_wp_continuation_mono
E
E'
)
;
auto
.
-
rewrite
IHde
//.
iApply
a_un_op_spec
.
iSpecialize
(
"Hm"
with
"Hwp"
).
iApply
(
awp_wand
with
"Hm"
).
iIntros
(
v
)
"Hex"
.
iDestruct
"Hex"
as
(
E'
dv
m'
Hpre
Hpre'
Hm'wf
)
"(% & Hm & Hwp)"
.
...
...
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